Theorem superpos 10281

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

Step	Hyp	Ref	Expression
1		reeanv 1778	. . . 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 1590	. . . . . . . . . . 11 |- (A = (span` {y}) -> (A =/= B <-> (span` {y}) =/= B))
3		neeq2 1591	. . . . . . . . . . 11 |- (B = (span` {z}) -> ((span` {y}) =/= B <-> (span` {y}) =/= (span` {z})))
4	2, 3	sylan9bb 540	. . . . . . . . . 10 |- ((A = (span` {y}) /\ B = (span` {z})) -> (A =/= B <-> (span` {y}) =/= (span` {z})))
5	4	adantl 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 1590	. . . . . . . . . . . . 13 |- (x = (span` {(y +h z)}) -> (x =/= A <-> (span` {(y +h z)}) =/= A))
7		neeq1 1590	. . . . . . . . . . . . 13 |- (x = (span` {(y +h z)}) -> (x =/= B <-> (span` {(y +h z)}) =/= B))
8		sseq1 2082	. . . . . . . . . . . . 13 |- (x = (span` {(y +h z)}) -> (x (_ (A vH B) <-> (span` {(y +h z)}) (_ (A vH B)))
9	6, 7, 8	3anbi123d 893	. . . . . . . . . . . 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))))
10	9	rcla4ev 1877	. . . . . . . . . . 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 10277	. . . . . . . . . . . . . 14 |- (((y +h z) e. H~ /\ (y +h z) =/= 0h) -> (span` {(y +h z)}) e. Atoms)
12		hvaddclt 8882	. . . . . . . . . . . . . . 15 |- ((y e. H~ /\ z e. H~) -> (y +h z) e. H~)
13	12	adantr 389	. . . . . . . . . . . . . 14 |- (((y e. H~ /\ z e. H~) /\ (span` {y}) =/= (span` {z})) -> (y +h z) e. H~)
14		hvaddeq0t 8936	. . . . . . . . . . . . . . . . 17 |- ((y e. H~ /\ z e. H~) -> ((y +h z) = 0h <-> y = (-u1 .h z)))
15		sneq 2417	. . . . . . . . . . . . . . . . . . . . 21 |- (y = (-u1 .h z) -> {y} = {(-u1 .h z)})
16	15	fveq2d 3728	. . . . . . . . . . . . . . . . . . . 20 |- (y = (-u1 .h z) -> (span` {y}) = (span` {(-u1 .h z)}))
17		ax1cn 5269	. . . . . . . . . . . . . . . . . . . . . 22 |- 1 e. CC
18	17	negcl 5369	. . . . . . . . . . . . . . . . . . . . 21 |- -u1 e. CC
19		ax1ne0 5280	. . . . . . . . . . . . . . . . . . . . . 22 |- 1 =/= 0
20	17, 19	negn0 5808	. . . . . . . . . . . . . . . . . . . . 21 |- -u1 =/= 0
21		spansncol 9491	. . . . . . . . . . . . . . . . . . . . 21 |- ((z e. H~ /\ -u1 e. CC /\ -u1 =/= 0) -> (span` {(-u1 .h z)}) = (span` {z}))
22	18, 20, 21	mp3an23 908	. . . . . . . . . . . . . . . . . . . 20 |- (z e. H~ -> (span` {(-u1 .h z)}) = (span` {z}))
23	16, 22	sylan9eqr 1529	. . . . . . . . . . . . . . . . . . 19 |- ((z e. H~ /\ y = (-u1 .h z)) -> (span` {y}) = (span` {z}))
24	23	ex 373	. . . . . . . . . . . . . . . . . 18 |- (z e. H~ -> (y = (-u1 .h z) -> (span` {y}) = (span` {z})))
25	24	adantl 388	. . . . . . . . . . . . . . . . 17 |- ((y e. H~ /\ z e. H~) -> (y = (-u1 .h z) -> (span` {y}) = (span` {z})))
26	14, 25	sylbid 203	. . . . . . . . . . . . . . . 16 |- ((y e. H~ /\ z e. H~) -> ((y +h z) = 0h -> (span` {y}) = (span` {z})))
27	26	necon3d 1604	. . . . . . . . . . . . . . 15 |- ((y e. H~ /\ z e. H~) -> ((span` {y}) =/= (span` {z}) -> (y +h z) =/= 0h))
28	27	imp 350	. . . . . . . . . . . . . 14 |- (((y e. H~ /\ z e. H~) /\ (span` {y}) =/= (span` {z})) -> (y +h z) =/= 0h)
29	11, 13, 28	sylanc 471	. . . . . . . . . . . . 13 |- (((y e. H~ /\ z e. H~) /\ (span` {y}) =/= (span` {z})) -> (span` {(y +h z)}) e. Atoms)
30	29	adantlr 393	. . . . . . . . . . . 12 |- ((((y e. H~ /\ z e. H~) /\ (y =/= 0h /\ z =/= 0h)) /\ (span` {y}) =/= (span` {z})) -> (span` {(y +h z)}) e. Atoms)
31	30	adantlr 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 1484	. . . . . . . . . . . . . . . . . 18 |- (A = (span` {y}) -> ((span` {(y +h z)}) = A <-> (span` {(y +h z)}) = (span` {y})))
33	32	biimpd 153	. . . . . . . . . . . . . . . . 17 |- (A = (span` {y}) -> ((span` {(y +h z)}) = A -> (span` {(y +h z)}) = (span` {y})))
34		spansneleqi 9492	. . . . . . . . . . . . . . . . . . . . . 22 |- ((y +h z) e. H~ -> ((span` {(y +h z)}) = (span` {y}) -> (y +h z) e. (span` {y})))
35	12, 34	syl 10	. . . . . . . . . . . . . . . . . . . . 21 |- ((y e. H~ /\ z e. H~) -> ((span` {(y +h z)}) = (span` {y}) -> (y +h z) e. (span` {y})))
36		elspansnt 9489	. . . . . . . . . . . . . . . . . . . . . . 23 |- (y e. H~ -> ((y +h z) e. (span` {y}) <-> E.v e. CC (y +h z) = (v .h y)))
37	36	adantr 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 3968	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- (w = (v + -u1) -> (w .h y) = ((v + -u1) .h y))
39	38	eqeq2d 1486	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- (w = (v + -u1) -> (z = (w .h y) <-> z = ((v + -u1) .h y)))
40	39	rcla4ev 1877	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- (((v + -u1) e. CC /\ z = ((v + -u1) .h y)) -> E.w e. CC z = (w .h y))
41		axaddcl 5271	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ((v e. CC /\ -u1 e. CC) -> (v + -u1) e. CC)
42	18, 41	mpan2 696	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- (v e. CC -> (v + -u1) e. CC)
43	42	ad2antlr 405	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ((((y e. H~ /\ z e. H~) /\ v e. CC) /\ (y +h z) = (v .h y)) -> (v + -u1) e. CC)
44		hvsubaddt 8944	. . . . . . . . . . . . . . . . . . . . . . . . . . . 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 8883	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- ((v e. CC /\ y e. H~) -> (v .h y) e. H~)
46	45	ancoms 436	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ((y e. H~ /\ v e. CC) -> (v .h y) e. H~)
47	46	adantlr 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~)
50	44, 47, 48, 49	syl3anc 858	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- (((y e. H~ /\ z e. H~) /\ v e. CC) -> (((v .h y) -h y) = z <-> (y +h z) = (v .h y)))
51	50	biimpar 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 8886	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- (((v .h y) e. H~ /\ y e. H~) -> ((v .h y) -h y) = ((v .h y) +h (-u1 .h y)))
53	45, 52	sylancom 475	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- ((v