HomeHome Hilbert Space Explorer < Previous   Next >
Related theorems
Unicode version
Theorem superpos 10189
Description: Superposition Principle. If A and B are distinct atoms, there exists a third atom, distinct from A and B, that is the superposition of A and B. Definition 3.4-3(a) in [MegillPavicic] p. 2345 (PDF p. 8).
Assertion
Ref Expression
superpos |- ((A e. Atoms /\ B e. Atoms /\ A =/= B) -> E.x e. Atoms (x =/= A /\ x =/= B /\ x (_ (A vH B)))
Distinct variable groups:   x,A   x,B
Proof of Theorem superpos
StepHypRef Expression
1 reeanv 1770 . . . 4 |- (E.y e. H~ E.z e. H~ ((y =/= 0h /\ A = (span` {y})) /\ (z =/= 0h /\ B = (span` {z}))) <-> (E.y e. H~ (y =/= 0h /\ A = (span` {y})) /\ E.z e. H~ (z =/= 0h /\ B = (span` {z}))))
2 neeq1 1582 . . . . . . . . . . 11 |- (A = (span` {y}) -> (A =/= B <-> (span` {y}) =/= B))
3 neeq2 1583 . . . . . . . . . . 11 |- (B = (span` {z}) -> ((span` {y}) =/= B <-> (span` {y}) =/= (span` {z})))
42, 3sylan9bb 538 . . . . . . . . . 10 |- ((A = (span` {y}) /\ B = (span` {z})) -> (A =/= B <-> (span` {y}) =/= (span` {z})))
54adantl 388 . . . . . . . . 9 |- ((((y e. H~ /\ z e. H~) /\ (y =/= 0h /\ z =/= 0h)) /\ (A = (span` {y}) /\ B = (span` {z}))) -> (A =/= B <-> (span` {y}) =/= (span` {z})))
6 neeq1 1582 . . . . . . . . . . . . 13 |- (x = (span` {(y +h z)}) -> (x =/= A <-> (span` {(y +h z)}) =/= A))
7 neeq1 1582 . . . . . . . . . . . . 13 |- (x = (span` {(y +h z)}) -> (x =/= B <-> (span` {(y +h z)}) =/= B))
8 sseq1 2072 . . . . . . . . . . . . 13 |- (x = (span` {(y +h z)}) -> (x (_ (A vH B) <-> (span` {(y +h z)}) (_ (A vH B)))
96, 7, 83anbi123d 890 . . . . . . . . . . . 12 |- (x = (span` {(y +h z)}) -> ((x =/= A /\ x =/= B /\ x (_ (A vH B)) <-> ((span` {(y +h z)}) =/= A /\ (span` {(y +h z)}) =/= B /\ (span` {(y +h z)}) (_ (A vH B))))
109rcla4ev 1868 . . . . . . . . . . 11 |- (((span` {(y +h z)}) e. Atoms /\ ((span` {(y +h z)}) =/= A /\ (span` {(y +h z)}) =/= B /\ (span` {(y +h z)}) (_ (A vH B))) -> E.x e. Atoms (x =/= A /\ x =/= B /\ x (_ (A vH B)))
11 spansnat 10185 . . . . . . . . . . . . . 14 |- (((y +h z) e. H~ /\ (y +h z) =/= 0h) -> (span` {(y +h z)}) e. Atoms)
12 hvaddclt 8803 . . . . . . . . . . . . . . 15 |- ((y e. H~ /\ z e. H~) -> (y +h z) e. H~)
1312adantr 389 . . . . . . . . . . . . . 14 |- (((y e. H~ /\ z e. H~) /\ (span` {y}) =/= (span` {z})) -> (y +h z) e. H~)
14 hvaddeq0t 8857 . . . . . . . . . . . . . . . . 17 |- ((y e. H~ /\ z e. H~) -> ((y +h z) = 0h <-> y = (-u1 .h z)))
15 sneq 2407 . . . . . . . . . . . . . . . . . . . . 21 |- (y = (-u1 .h z) -> {y} = {(-u1 .h z)})
1615fveq2d 3713 . . . . . . . . . . . . . . . . . . . 20 |- (y = (-u1 .h z) -> (span` {y}) = (span` {(-u1 .h z)}))
17 ax1cn 5241 . . . . . . . . . . . . . . . . . . . . . 22 |- 1 e. CC
1817negcl 5341 . . . . . . . . . . . . . . . . . . . . 21 |- -u1 e. CC
19 ax1ne0 5252 . . . . . . . . . . . . . . . . . . . . . 22 |- 1 =/= 0
2017, 19negn0 5764 . . . . . . . . . . . . . . . . . . . . 21 |- -u1 =/= 0
21 spansncol 9407 . . . . . . . . . . . . . . . . . . . . 21 |- ((z e. H~ /\ -u1 e. CC /\ -u1 =/= 0) -> (span` {(-u1 .h z)}) = (span` {z}))
2218, 20, 21mp3an23 905 . . . . . . . . . . . . . . . . . . . 20 |- (z e. H~ -> (span` {(-u1 .h z)}) = (span` {z}))
2316, 22sylan9eqr 1521 . . . . . . . . . . . . . . . . . . 19 |- ((z e. H~ /\ y = (-u1 .h z)) -> (span` {y}) = (span` {z}))
2423ex 373 . . . . . . . . . . . . . . . . . 18 |- (z e. H~ -> (y = (-u1 .h z) -> (span` {y}) = (span` {z})))
2524adantl 388 . . . . . . . . . . . . . . . . 17 |- ((y e. H~ /\ z e. H~) -> (y = (-u1 .h z) -> (span` {y}) = (span` {z})))
2614, 25sylbid 203 . . . . . . . . . . . . . . . 16 |- ((y e. H~ /\ z e. H~) -> ((y +h z) = 0h -> (span` {y}) = (span` {z})))
2726necon3d 1596 . . . . . . . . . . . . . . 15 |- ((y e. H~ /\ z e. H~) -> ((span` {y}) =/= (span` {z}) -> (y +h z) =/= 0h))
2827imp 350 . . . . . . . . . . . . . 14 |- (((y e. H~ /\ z e. H~) /\ (span` {y}) =/= (span` {z})) -> (y +h z) =/= 0h)
2911, 13, 28sylanc 471 . . . . . . . . . . . . 13 |- (((y e. H~ /\ z e. H~) /\ (span` {y}) =/= (span` {z})) -> (span` {(y +h z)}) e. Atoms)
3029adantlr 393 . . . . . . . . . . . 12 |- ((((y e. H~ /\ z e. H~) /\ (y =/= 0h /\ z =/= 0h)) /\ (span` {y}) =/= (span` {z})) -> (span` {(y +h z)}) e. Atoms)
3130adantlr 393 . . . . . . . . . . 11 |- (((((y e. H~ /\ z e. H~) /\ (y =/= 0h /\ z =/= 0h)) /\ (A = (span` {y}) /\ B = (span` {z}))) /\ (span` {y}) =/= (span` {z})) -> (span` {(y +h z)}) e. Atoms)
32 eqeq2 1476 . . . . . . . . . . . . . . . . . 18 |- (A = (span` {y}) -> ((span` {(y +h z)}) = A <-> (span` {(y +h z)}) = (span` {y})))
3332biimpd 153 . . . . . . . . . . . . . . . . 17 |- (A = (span` {y}) -> ((span` {(y +h z)}) = A -> (span` {(y +h z)}) = (span` {y})))
34 spansneleqi 9408 . . . . . . . . . . . . . . . . . . . . . 22 |- ((y +h z) e. H~ -> ((span` {(y +h z)}) = (span` {y}) -> (y +h z) e. (span` {y})))
3512, 34syl 10 . . . . . . . . . . . . . . . . . . . . 21 |- ((y e. H~ /\ z e. H~) -> ((span` {(y +h z)}) = (span` {y}) -> (y +h z) e. (span` {y})))
36 elspansnt 9405 . . . . . . . . . . . . . . . . . . . . . . 23 |- (y e. H~ -> ((y +h z) e. (span` {y}) <-> E.v e. CC (y +h z) = (v .h y)))
3736adantr 389 . . . . . . . . . . . . . . . . . . . . . 22 |- ((y e. H~ /\ z e. H~) -> ((y +h z) e. (span` {y}) <-> E.v e. CC (y +h z) = (v .h y)))
38 opreq1 3953 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- (w = (v + -u1) -> (w .h y) = ((v + -u1) .h y))
3938eqeq2d 1478 . . . . . . . . . . . . . . . . . . . . . . . . . 26 |- (w = (v + -u1) -> (z = (w .h y) <-> z = ((v + -u1) .h y)))
4039rcla4ev 1868 . . . . . . . . . . . . . . . . . . . . . . . . 25 |- (((v + -u1) e. CC /\ z = ((v + -u1) .h y)) -> E.w e. CC z = (w .h y))
41 axaddcl 5243 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ((v e. CC /\ -u1 e. CC) -> (v + -u1) e. CC)
4218, 41mpan2 694 . . . . . . . . . . . . . . . . . . . . . . . . . 26 |- (v e. CC -> (v + -u1) e. CC)
4342ad2antlr 405 . . . . . . . . . . . . . . . . . . . . . . . . 25 |- ((((y e. H~ /\ z e. H~) /\ v e. CC) /\ (y +h z) = (v .h y)) -> (v + -u1) e. CC)
44 hvsubaddt 8865 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- (((v .h y) e. H~ /\ y e. H~ /\ z e. H~) -> (((v .h y) -h y) = z <-> (y +h z) = (v .h y)))
45 hvmulclt 8804 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- ((v e. CC /\ y e. H~) -> (v .h y) e. H~)
4645ancoms 436 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ((y e. H~ /\ v e. CC) -> (v .h y) e. H~)
4746adantlr 393 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- (((y e. H~ /\ z e. H~) /\ v e. CC) -> (v .h y) e. H~)
48 simpll 412 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- (((y e. H~ /\ z e. H~) /\ v e. CC) -> y e. H~)
49 simplr 413 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- (((y e. H~ /\ z e. H~) /\ v e. CC) -> z e. H~)
5044, 47, 48, 49syl3anc 856 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- (((y e. H~ /\ z e. H~) /\ v e. CC) -> (((v .h y) -h y) = z <-> (y +h z) = (v .h y)))
5150biimpar 417 . . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ((((y e. H~ /\ z e. H~) /\ v e. CC) /\ (y +h z) = (v .h y)) -> ((v .h y) -h y) = z)
52 hvsubvalt 8807 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- (((v .h y) e. H~ /\ y e. H~) -> ((v .h y) -h y) = ((v .h y) +h (-u1 .h y)))
53 pm3.27 323 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- ((v e.