Metamath Proof Explorer

Theorem superpos

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 MegPav2000 p. 2345 (PDF p. 8). (Contributed by NM, 9-Jun-2006) (New usage is discouraged.)

Ref Expression
Assertion superpos 
|- ( ( A e. HAtoms /\ B e. HAtoms /\ A =/= B ) -> E. x e. HAtoms ( x =/= A /\ x =/= B /\ x C_ ( A vH B ) ) )

Proof

Step Hyp Ref Expression
1 atom1d 
 |-  ( A e. HAtoms <-> E. y e. ~H ( y =/= 0h /\ A = ( span ` { y } ) ) )
2 atom1d 
 |-  ( B e. HAtoms <-> E. z e. ~H ( z =/= 0h /\ B = ( span ` { z } ) ) )
3 reeanv 
 |-  ( 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 } ) ) ) )
4 an4 
 |-  ( ( ( y =/= 0h /\ A = ( span ` { y } ) ) /\ ( z =/= 0h /\ B = ( span ` { z } ) ) ) <-> ( ( y =/= 0h /\ z =/= 0h ) /\ ( A = ( span ` { y } ) /\ B = ( span ` { z } ) ) ) )
5 neeq1 
 |-  ( A = ( span ` { y } ) -> ( A =/= B <-> ( span ` { y } ) =/= B ) )
6 neeq2 
 |-  ( B = ( span ` { z } ) -> ( ( span ` { y } ) =/= B <-> ( span ` { y } ) =/= ( span ` { z } ) ) )
7 5 6 sylan9bb 
 |-  ( ( A = ( span ` { y } ) /\ B = ( span ` { z } ) ) -> ( A =/= B <-> ( span ` { y } ) =/= ( span ` { z } ) ) )
8 7 adantl 
 |-  ( ( ( ( y e. ~H /\ z e. ~H ) /\ ( y =/= 0h /\ z =/= 0h ) ) /\ ( A = ( span ` { y } ) /\ B = ( span ` { z } ) ) ) -> ( A =/= B <-> ( span ` { y } ) =/= ( span ` { z } ) ) )
9 hvaddcl 
 |-  ( ( y e. ~H /\ z e. ~H ) -> ( y +h z ) e. ~H )
10 9 adantr 
 |-  ( ( ( y e. ~H /\ z e. ~H ) /\ ( span ` { y } ) =/= ( span ` { z } ) ) -> ( y +h z ) e. ~H )
11 hvaddeq0 
 |-  ( ( y e. ~H /\ z e. ~H ) -> ( ( y +h z ) = 0h <-> y = ( -u 1 .h z ) ) )
12 sneq 
 |-  ( y = ( -u 1 .h z ) -> { y } = { ( -u 1 .h z ) } )
13 12 fveq2d 
 |-  ( y = ( -u 1 .h z ) -> ( span ` { y } ) = ( span ` { ( -u 1 .h z ) } ) )
14 neg1cn 
 |-  -u 1 e. CC
15 neg1ne0 
 |-  -u 1 =/= 0
16 spansncol 
 |-  ( ( z e. ~H /\ -u 1 e. CC /\ -u 1 =/= 0 ) -> ( span ` { ( -u 1 .h z ) } ) = ( span ` { z } ) )
17 14 15 16 mp3an23 
 |-  ( z e. ~H -> ( span ` { ( -u 1 .h z ) } ) = ( span ` { z } ) )
18 13 17 sylan9eqr 
 |-  ( ( z e. ~H /\ y = ( -u 1 .h z ) ) -> ( span ` { y } ) = ( span ` { z } ) )
19 18 ex 
 |-  ( z e. ~H -> ( y = ( -u 1 .h z ) -> ( span ` { y } ) = ( span ` { z } ) ) )
20 19 adantl 
 |-  ( ( y e. ~H /\ z e. ~H ) -> ( y = ( -u 1 .h z ) -> ( span ` { y } ) = ( span ` { z } ) ) )
21 11 20 sylbid 
 |-  ( ( y e. ~H /\ z e. ~H ) -> ( ( y +h z ) = 0h -> ( span ` { y } ) = ( span ` { z } ) ) )
22 21 necon3d 
 |-  ( ( y e. ~H /\ z e. ~H ) -> ( ( span ` { y } ) =/= ( span ` { z } ) -> ( y +h z ) =/= 0h ) )
23 22 imp 
 |-  ( ( ( y e. ~H /\ z e. ~H ) /\ ( span ` { y } ) =/= ( span ` { z } ) ) -> ( y +h z ) =/= 0h )
24 spansna 
 |-  ( ( ( y +h z ) e. ~H /\ ( y +h z ) =/= 0h ) -> ( span ` { ( y +h z ) } ) e. HAtoms )
25 10 23 24 syl2anc 
 |-  ( ( ( y e. ~H /\ z e. ~H ) /\ ( span ` { y } ) =/= ( span ` { z } ) ) -> ( span ` { ( y +h z ) } ) e. HAtoms )
26 25 adantlr 
 |-  ( ( ( ( y e. ~H /\ z e. ~H ) /\ ( y =/= 0h /\ z =/= 0h ) ) /\ ( span ` { y } ) =/= ( span ` { z } ) ) -> ( span ` { ( y +h z ) } ) e. HAtoms )
27 26 adantlr 
 |-  ( ( ( ( ( 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. HAtoms )
28 eqeq2 
 |-  ( A = ( span ` { y } ) -> ( ( span ` { ( y +h z ) } ) = A <-> ( span ` { ( y +h z ) } ) = ( span ` { y } ) ) )
29 28 biimpd 
 |-  ( A = ( span ` { y } ) -> ( ( span ` { ( y +h z ) } ) = A -> ( span ` { ( y +h z ) } ) = ( span ` { y } ) ) )
30 spansneleqi 
 |-  ( ( y +h z ) e. ~H -> ( ( span ` { ( y +h z ) } ) = ( span ` { y } ) -> ( y +h z ) e. ( span ` { y } ) ) )
31 9 30 syl 
 |-  ( ( y e. ~H /\ z e. ~H ) -> ( ( span ` { ( y +h z ) } ) = ( span ` { y } ) -> ( y +h z ) e. ( span ` { y } ) ) )
32 elspansn 
 |-  ( y e. ~H -> ( ( y +h z ) e. ( span ` { y } ) <-> E. v e. CC ( y +h z ) = ( v .h y ) ) )
33 32 adantr 
 |-  ( ( y e. ~H /\ z e. ~H ) -> ( ( y +h z ) e. ( span ` { y } ) <-> E. v e. CC ( y +h z ) = ( v .h y ) ) )
34 addcl 
 |-  ( ( v e. CC /\ -u 1 e. CC ) -> ( v + -u 1 ) e. CC )
35 14 34 mpan2 
 |-  ( v e. CC -> ( v + -u 1 ) e. CC )
36 35 ad2antlr 
 |-  ( ( ( ( y e. ~H /\ z e. ~H ) /\ v e. CC ) /\ ( y +h z ) = ( v .h y ) ) -> ( v + -u 1 ) e. CC )
37 hvmulcl 
 |-  ( ( v e. CC /\ y e. ~H ) -> ( v .h y ) e. ~H )
38 37 ancoms 
 |-  ( ( y e. ~H /\ v e. CC ) -> ( v .h y ) e. ~H )
39 38 adantlr 
 |-  ( ( ( y e. ~H /\ z e. ~H ) /\ v e. CC ) -> ( v .h y ) e. ~H )
40 simpll 
 |-  ( ( ( y e. ~H /\ z e. ~H ) /\ v e. CC ) -> y e. ~H )
41 simplr 
 |-  ( ( ( y e. ~H /\ z e. ~H ) /\ v e. CC ) -> z e. ~H )
42 hvsubadd 
 |-  ( ( ( v .h y ) e. ~H /\ y e. ~H /\ z e. ~H ) -> ( ( ( v .h y ) -h y ) = z <-> ( y +h z ) = ( v .h y ) ) )
43 39 40 41 42 syl3anc 
 |-  ( ( ( y e. ~H /\ z e. ~H ) /\ v e. CC ) -> ( ( ( v .h y ) -h y ) = z <-> ( y +h z ) = ( v .h y ) ) )
44 43 biimpar 
 |-  ( ( ( ( y e. ~H /\ z e. ~H ) /\ v e. CC ) /\ ( y +h z ) = ( v .h y ) ) -> ( ( v .h y ) -h y ) = z )
45 hvsubval 
 |-  ( ( ( v .h y ) e. ~H /\ y e. ~H ) -> ( ( v .h y ) -h y ) = ( ( v .h y ) +h ( -u 1 .h y ) ) )
46 37 45 sylancom 
 |-  ( ( v e. CC /\ y e. ~H ) -> ( ( v .h y ) -h y ) = ( ( v .h y ) +h ( -u 1 .h y ) ) )
47 ax-hvdistr2 
 |-  ( ( v e. CC /\ -u 1 e. CC /\ y e. ~H ) -> ( ( v + -u 1 ) .h y ) = ( ( v .h y ) +h ( -u 1 .h y ) ) )
48 14 47 mp3an2 
 |-  ( ( v e. CC /\ y e. ~H ) -> ( ( v + -u 1 ) .h y ) = ( ( v .h y ) +h ( -u 1 .h y ) ) )
49 46 48 eqtr4d 
 |-  ( ( v e. CC /\ y e. ~H ) -> ( ( v .h y ) -h y ) = ( ( v + -u 1 ) .h y ) )
50 49 ancoms 
 |-  ( ( y e. ~H /\ v e. CC ) -> ( ( v .h y ) -h y ) = ( ( v + -u 1 ) .h y ) )
51 50 adantlr 
 |-  ( ( ( y e. ~H /\ z e. ~H ) /\ v e. CC ) -> ( ( v .h y ) -h y ) = ( ( v + -u 1 ) .h y ) )
52 51 adantr 
 |-  ( ( ( ( y e. ~H /\ z e. ~H ) /\ v e. CC ) /\ ( y +h z ) = ( v .h y ) ) -> ( ( v .h y ) -h y ) = ( ( v + -u 1 ) .h y ) )
53 44 52 eqtr3d 
 |-  ( ( ( ( y e. ~H /\ z e. ~H ) /\ v e. CC ) /\ ( y +h z ) = ( v .h y ) ) -> z = ( ( v + -u 1 ) .h y ) )
54 oveq1 
 |-  ( w = ( v + -u 1 ) -> ( w .h y ) = ( ( v + -u 1 ) .h y ) )
55 54 rspceeqv 
 |-  ( ( ( v + -u 1 ) e. CC /\ z = ( ( v + -u 1 ) .h y ) ) -> E. w e. CC z = ( w .h y ) )
56 36 53 55 syl2anc 
 |-  ( ( ( ( y e. ~H /\ z e. ~H ) /\ v e. CC ) /\ ( y +h z ) = ( v .h y ) ) -> E. w e. CC z = ( w .h y ) )
57 56 rexlimdva2 
 |-  ( ( y e. ~H /\ z e. ~H ) -> ( E. v e. CC ( y +h z ) = ( v .h y ) -> E. w e. CC z = ( w .h y ) ) )
58 33 57 sylbid 
 |-  ( ( y e. ~H /\ z e. ~H ) -> ( ( y +h z ) e. ( span ` { y } ) -> E. w e. CC z = ( w .h y ) ) )
59 31 58 syld 
 |-  ( ( y e. ~H /\ z e. ~H ) -> ( ( span ` { ( y +h z ) } ) = ( span ` { y } ) -> E. w e. CC z = ( w .h y ) ) )
60 elspansn 
 |-  ( y e. ~H -> ( z e. ( span ` { y } ) <-> E. w e. CC z = ( w .h y ) ) )
61 60 adantr 
 |-  ( ( y e. ~H /\ z e. ~H ) -> ( z e. ( span ` { y } ) <-> E. w e. CC z = ( w .h y ) ) )
62 59 61 sylibrd 
 |-  ( ( y e. ~H /\ z e. ~H ) -> ( ( span ` { ( y +h z ) } ) = ( span ` { y } ) -> z e. ( span ` { y } ) ) )
63 62 adantr 
 |-  ( ( ( y e. ~H /\ z e. ~H ) /\ z =/= 0h ) -> ( ( span ` { ( y +h z ) } ) = ( span ` { y } ) -> z e. ( span ` { y } ) ) )
64 spansneleq 
 |-  ( ( y e. ~H /\ z =/= 0h ) -> ( z e. ( span ` { y } ) -> ( span ` { z } ) = ( span ` { y } ) ) )
65 eqcom 
 |-  ( ( span ` { z } ) = ( span ` { y } ) <-> ( span ` { y } ) = ( span ` { z } ) )
66 64 65 syl6ib 
 |-  ( ( y e. ~H /\ z =/= 0h ) -> ( z e. ( span ` { y } ) -> ( span ` { y } ) = ( span ` { z } ) ) )
67 66 adantlr 
 |-  ( ( ( y e. ~H /\ z e. ~H ) /\ z =/= 0h ) -> ( z e. ( span ` { y } ) -> ( span ` { y } ) = ( span ` { z } ) ) )
68 63 67 syld 
 |-  ( ( ( y e. ~H /\ z e. ~H ) /\ z =/= 0h ) -> ( ( span ` { ( y +h z ) } ) = ( span ` { y } ) -> ( span ` { y } ) = ( span ` { z } ) ) )
69 29 68 sylan9r 
 |-  ( ( ( ( y e. ~H /\ z e. ~H ) /\ z =/= 0h ) /\ A = ( span ` { y } ) ) -> ( ( span ` { ( y +h z ) } ) = A -> ( span ` { y } ) = ( span ` { z } ) ) )
70 69 necon3d 
 |-  ( ( ( ( y e. ~H /\ z e. ~H ) /\ z =/= 0h ) /\ A = ( span ` { y } ) ) -> ( ( span ` { y } ) =/= ( span ` { z } ) -> ( span ` { ( y +h z ) } ) =/= A ) )
71 70 adantlrl 
 |-  ( ( ( ( y e. ~H /\ z e. ~H ) /\ ( y =/= 0h /\ z =/= 0h ) ) /\ A = ( span ` { y } ) ) -> ( ( span ` { y } ) =/= ( span ` { z } ) -> ( span ` { ( y +h z ) } ) =/= A ) )
72 71 adantrr 
 |-  ( ( ( ( y e. ~H /\ z e. ~H ) /\ ( y =/= 0h /\ z =/= 0h ) ) /\ ( A = ( span ` { y } ) /\ B = ( span ` { z } ) ) ) -> ( ( span ` { y } ) =/= ( span ` { z } ) -> ( span ` { ( y +h z ) } ) =/= A ) )
73 72 imp 
 |-  ( ( ( ( ( y e. ~H /\ z e. ~H ) /\ ( y =/= 0h /\ z =/= 0h ) ) /\ ( A = ( span ` { y } ) /\ B = ( span ` { z } ) ) ) /\ ( span ` { y } ) =/= ( span ` { z } ) ) -> ( span ` { ( y +h z ) } ) =/= A )
74 eqeq2 
 |-  ( B = ( span ` { z } ) -> ( ( span ` { ( y +h z ) } ) = B <-> ( span ` { ( y +h z ) } ) = ( span ` { z } ) ) )
75 74 biimpd 
 |-  ( B = ( span ` { z } ) -> ( ( span ` { ( y +h z ) } ) = B -> ( span ` { ( y +h z ) } ) = ( span ` { z } ) ) )
76 spansneleqi 
 |-  ( ( y +h z ) e. ~H -> ( ( span ` { ( y +h z ) } ) = ( span ` { z } ) -> ( y +h z ) e. ( span ` { z } ) ) )
77 9 76 syl 
 |-  ( ( y e. ~H /\ z e. ~H ) -> ( ( span ` { ( y +h z ) } ) = ( span ` { z } ) -> ( y +h z ) e. ( span ` { z } ) ) )
78 elspansn 
 |-  ( z e. ~H -> ( ( y +h z ) e. ( span ` { z } ) <-> E. v e. CC ( y +h z ) = ( v .h z ) ) )
79 78 adantl 
 |-  ( ( y e. ~H /\ z e. ~H ) -> ( ( y +h z ) e. ( span ` { z } ) <-> E. v e. CC ( y +h z ) = ( v .h z ) ) )
80 35 ad2antlr 
 |-  ( ( ( ( y e. ~H /\ z e. ~H ) /\ v e. CC ) /\ ( y +h z ) = ( v .h z ) ) -> ( v + -u 1 ) e. CC )
81 hvmulcl 
 |-  ( ( v e. CC /\ z e. ~H ) -> ( v .h z ) e. ~H )
82 81 ancoms 
 |-  ( ( z e. ~H /\ v e. CC ) -> ( v .h z ) e. ~H )
83 82 adantll 
 |-  ( ( ( y e. ~H /\ z e. ~H ) /\ v e. CC ) -> ( v .h z ) e. ~H )
84 hvsubadd 
 |-  ( ( ( v .h z ) e. ~H /\ z e. ~H /\ y e. ~H ) -> ( ( ( v .h z ) -h z ) = y <-> ( z +h y ) = ( v .h z ) ) )
85 83 41 40 84 syl3anc 
 |-  ( ( ( y e. ~H /\ z e. ~H ) /\ v e. CC ) -> ( ( ( v .h z ) -h z ) = y <-> ( z +h y ) = ( v .h z ) ) )
86 ax-hvcom 
 |-  ( ( y e. ~H /\ z e. ~H ) -> ( y +h z ) = ( z +h y ) )
87 86 adantr 
 |-  ( ( ( y e. ~H /\ z e. ~H ) /\ v e. CC ) -> ( y +h z ) = ( z +h y ) )
88 87 eqeq1d 
 |-  ( ( ( y e. ~H /\ z e. ~H ) /\ v e. CC ) -> ( ( y +h z ) = ( v .h z ) <-> ( z +h y ) = ( v .h z ) ) )
89 85 88 bitr4d 
 |-  ( ( ( y e. ~H /\ z e. ~H ) /\ v e. CC ) -> ( ( ( v .h z ) -h z ) = y <-> ( y +h z ) = ( v .h z ) ) )
90 89 biimpar 
 |-  ( ( ( ( y e. ~H /\ z e. ~H ) /\ v e. CC ) /\ ( y +h z ) = ( v .h z ) ) -> ( ( v .h z ) -h z ) = y )
91 hvsubval 
 |-  ( ( ( v .h z ) e. ~H /\ z e. ~H ) -> ( ( v .h z ) -h z ) = ( ( v .h z ) +h ( -u 1 .h z ) ) )
92 81 91 sylancom 
 |-  ( ( v e. CC /\ z e. ~H ) -> ( ( v .h z ) -h z ) = ( ( v .h z ) +h ( -u 1 .h z ) ) )
93 ax-hvdistr2 
 |-  ( ( v e. CC /\ -u 1 e. CC /\ z e. ~H ) -> ( ( v + -u 1 ) .h z ) = ( ( v .h z ) +h ( -u 1 .h z ) ) )
94 14 93 mp3an2 
 |-  ( ( v e. CC /\ z e. ~H ) -> ( ( v + -u 1 ) .h z ) = ( ( v .h z ) +h ( -u 1 .h z ) ) )
95 92 94 eqtr4d 
 |-  ( ( v e. CC /\ z e. ~H ) -> ( ( v .h z ) -h z ) = ( ( v + -u 1 ) .h z ) )
96 95 ancoms 
 |-  ( ( z e. ~H /\ v e. CC ) -> ( ( v .h z ) -h z ) = ( ( v + -u 1 ) .h z ) )
97 96 adantll 
 |-  ( ( ( y e. ~H /\ z e. ~H ) /\ v e. CC ) -> ( ( v .h z ) -h z ) = ( ( v + -u 1 ) .h z ) )
98 97 adantr 
 |-  ( ( ( ( y e. ~H /\ z e. ~H ) /\ v e. CC ) /\ ( y +h z ) = ( v .h z ) ) -> ( ( v .h z ) -h z ) = ( ( v + -u 1 ) .h z ) )
99 90 98 eqtr3d 
 |-  ( ( ( ( y e. ~H /\ z e. ~H ) /\ v e. CC ) /\ ( y +h z ) = ( v .h z ) ) -> y = ( ( v + -u 1 ) .h z ) )
100 oveq1 
 |-  ( w = ( v + -u 1 ) -> ( w .h z ) = ( ( v + -u 1 ) .h z ) )
101 100 rspceeqv 
 |-  ( ( ( v + -u 1 ) e. CC /\ y = ( ( v + -u 1 ) .h z ) ) -> E. w e. CC y = ( w .h z ) )
102 80 99 101 syl2anc 
 |-  ( ( ( ( y e. ~H /\ z e. ~H ) /\ v e. CC ) /\ ( y +h z ) = ( v .h z ) ) -> E. w e. CC y = ( w .h z ) )
103 102 rexlimdva2 
 |-  ( ( y e. ~H /\ z e. ~H ) -> ( E. v e. CC ( y +h z ) = ( v .h z ) -> E. w e. CC y = ( w .h z ) ) )
104 79 103 sylbid 
 |-  ( ( y e. ~H /\ z e. ~H ) -> ( ( y +h z ) e. ( span ` { z } ) -> E. w e. CC y = ( w .h z ) ) )
105 77 104 syld 
 |-  ( ( y e. ~H /\ z e. ~H ) -> ( ( span ` { ( y +h z ) } ) = ( span ` { z } ) -> E. w e. CC y = ( w .h z ) ) )
106 elspansn 
 |-  ( z e. ~H -> ( y e. ( span ` { z } ) <-> E. w e. CC y = ( w .h z ) ) )
107 106 adantl 
 |-  ( ( y e. ~H /\ z e. ~H ) -> ( y e. ( span ` { z } ) <-> E. w e. CC y = ( w .h z ) ) )
108 105 107 sylibrd 
 |-  ( ( y e. ~H /\ z e. ~H ) -> ( ( span ` { ( y +h z ) } ) = ( span ` { z } ) -> y e. ( span ` { z } ) ) )
109 108 adantr 
 |-  ( ( ( y e. ~H /\ z e. ~H ) /\ y =/= 0h ) -> ( ( span ` { ( y +h z ) } ) = ( span ` { z } ) -> y e. ( span ` { z } ) ) )
110 spansneleq 
 |-  ( ( z e. ~H /\ y =/= 0h ) -> ( y e. ( span ` { z } ) -> ( span ` { y } ) = ( span ` { z } ) ) )
111 110 adantll 
 |-  ( ( ( y e. ~H /\ z e. ~H ) /\ y =/= 0h ) -> ( y e. ( span ` { z } ) -> ( span ` { y } ) = ( span ` { z } ) ) )
112 109 111 syld 
 |-  ( ( ( y e. ~H /\ z e. ~H ) /\ y =/= 0h ) -> ( ( span ` { ( y +h z ) } ) = ( span ` { z } ) -> ( span ` { y } ) = ( span ` { z } ) ) )
113 75 112 sylan9r 
 |-  ( ( ( ( y e. ~H /\ z e. ~H ) /\ y =/= 0h ) /\ B = ( span ` { z } ) ) -> ( ( span ` { ( y +h z ) } ) = B -> ( span ` { y } ) = ( span ` { z } ) ) )
114 113 necon3d 
 |-  ( ( ( ( y e. ~H /\ z e. ~H ) /\ y =/= 0h ) /\ B = ( span ` { z } ) ) -> ( ( span ` { y } ) =/= ( span ` { z } ) -> ( span ` { ( y +h z ) } ) =/= B ) )
115 114 adantlrr 
 |-  ( ( ( ( y e. ~H /\ z e. ~H ) /\ ( y =/= 0h /\ z =/= 0h ) ) /\ B = ( span ` { z } ) ) -> ( ( span ` { y } ) =/= ( span ` { z } ) -> ( span ` { ( y +h z ) } ) =/= B ) )
116 115 adantrl 
 |-  ( ( ( ( y e. ~H /\ z e. ~H ) /\ ( y =/= 0h /\ z =/= 0h ) ) /\ ( A = ( span ` { y } ) /\ B = ( span ` { z } ) ) ) -> ( ( span ` { y } ) =/= ( span ` { z } ) -> ( span ` { ( y +h z ) } ) =/= B ) )
117 116 imp 
 |-  ( ( ( ( ( y e. ~H /\ z e. ~H ) /\ ( y =/= 0h /\ z =/= 0h ) ) /\ ( A = ( span ` { y } ) /\ B = ( span ` { z } ) ) ) /\ ( span ` { y } ) =/= ( span ` { z } ) ) -> ( span ` { ( y +h z ) } ) =/= B )
118 spanpr 
 |-  ( ( y e. ~H /\ z e. ~H ) -> ( span ` { ( y +h z ) } ) C_ ( span ` { y , z } ) )
119 118 adantr 
 |-  ( ( ( y e. ~H /\ z e. ~H ) /\ ( A = ( span ` { y } ) /\ B = ( span ` { z } ) ) ) -> ( span ` { ( y +h z ) } ) C_ ( span ` { y , z } ) )
120 oveq12 
 |-  ( ( A = ( span ` { y } ) /\ B = ( span ` { z } ) ) -> ( A vH B ) = ( ( span ` { y } ) vH ( span ` { z } ) ) )
121 df-pr 
 |-  { y , z } = ( { y } u. { z } )
122 121 fveq2i 
 |-  ( span ` { y , z } ) = ( span ` ( { y } u. { z } ) )
123 snssi 
 |-  ( y e. ~H -> { y } C_ ~H )
124 snssi 
 |-  ( z e. ~H -> { z } C_ ~H )
125 spanun 
 |-  ( ( { y } C_ ~H /\ { z } C_ ~H ) -> ( span ` ( { y } u. { z } ) ) = ( ( span ` { y } ) +H ( span ` { z } ) ) )
126 123 124 125 syl2an 
 |-  ( ( y e. ~H /\ z e. ~H ) -> ( span ` ( { y } u. { z } ) ) = ( ( span ` { y } ) +H ( span ` { z } ) ) )
127 122 126 syl5eq 
 |-  ( ( y e. ~H /\ z e. ~H ) -> ( span ` { y , z } ) = ( ( span ` { y } ) +H ( span ` { z } ) ) )
128 spansnch 
 |-  ( y e. ~H -> ( span ` { y } ) e. CH )
129 spansnj 
 |-  ( ( ( span ` { y } ) e. CH /\ z e. ~H ) -> ( ( span ` { y } ) +H ( span ` { z } ) ) = ( ( span ` { y } ) vH ( span ` { z } ) ) )
130 128 129 sylan 
 |-  ( ( y e. ~H /\ z e. ~H ) -> ( ( span ` { y } ) +H ( span ` { z } ) ) = ( ( span ` { y } ) vH ( span ` { z } ) ) )
131 127 130 eqtr2d 
 |-  ( ( y e. ~H /\ z e. ~H ) -> ( ( span ` { y } ) vH ( span ` { z } ) ) = ( span ` { y , z } ) )
132 120 131 sylan9eqr 
 |-  ( ( ( y e. ~H /\ z e. ~H ) /\ ( A = ( span ` { y } ) /\ B = ( span ` { z } ) ) ) -> ( A vH B ) = ( span ` { y , z } ) )
133 119 132 sseqtrrd 
 |-  ( ( ( y e. ~H /\ z e. ~H ) /\ ( A = ( span ` { y } ) /\ B = ( span ` { z } ) ) ) -> ( span ` { ( y +h z ) } ) C_ ( A vH B ) )
134 133 adantlr 
 |-  ( ( ( ( y e. ~H /\ z e. ~H ) /\ ( y =/= 0h /\ z =/= 0h ) ) /\ ( A = ( span ` { y } ) /\ B = ( span ` { z } ) ) ) -> ( span ` { ( y +h z ) } ) C_ ( A vH B ) )
135 134 adantr 
 |-  ( ( ( ( ( y e. ~H /\ z e. ~H ) /\ ( y =/= 0h /\ z =/= 0h ) ) /\ ( A = ( span ` { y } ) /\ B = ( span ` { z } ) ) ) /\ ( span ` { y } ) =/= ( span ` { z } ) ) -> ( span ` { ( y +h z ) } ) C_ ( A vH B ) )
136 neeq1 
 |-  ( x = ( span ` { ( y +h z ) } ) -> ( x =/= A <-> ( span ` { ( y +h z ) } ) =/= A ) )
137 neeq1 
 |-  ( x = ( span ` { ( y +h z ) } ) -> ( x =/= B <-> ( span ` { ( y +h z ) } ) =/= B ) )
138 sseq1 
 |-  ( x = ( span ` { ( y +h z ) } ) -> ( x C_ ( A vH B ) <-> ( span ` { ( y +h z ) } ) C_ ( A vH B ) ) )
139 136 137 138 3anbi123d 
 |-  ( x = ( span ` { ( y +h z ) } ) -> ( ( x =/= A /\ x =/= B /\ x C_ ( A vH B ) ) <-> ( ( span ` { ( y +h z ) } ) =/= A /\ ( span ` { ( y +h z ) } ) =/= B /\ ( span ` { ( y +h z ) } ) C_ ( A vH B ) ) ) )
140 139 rspcev 
 |-  ( ( ( span ` { ( y +h z ) } ) e. HAtoms /\ ( ( span ` { ( y +h z ) } ) =/= A /\ ( span ` { ( y +h z ) } ) =/= B /\ ( span ` { ( y +h z ) } ) C_ ( A vH B ) ) ) -> E. x e. HAtoms ( x =/= A /\ x =/= B /\ x C_ ( A vH B ) ) )
141 27 73 117 135 140 syl13anc 
 |-  ( ( ( ( ( y e. ~H /\ z e. ~H ) /\ ( y =/= 0h /\ z =/= 0h ) ) /\ ( A = ( span ` { y } ) /\ B = ( span ` { z } ) ) ) /\ ( span ` { y } ) =/= ( span ` { z } ) ) -> E. x e. HAtoms ( x =/= A /\ x =/= B /\ x C_ ( A vH B ) ) )
142 141 ex 
 |-  ( ( ( ( y e. ~H /\ z e. ~H ) /\ ( y =/= 0h /\ z =/= 0h ) ) /\ ( A = ( span ` { y } ) /\ B = ( span ` { z } ) ) ) -> ( ( span ` { y } ) =/= ( span ` { z } ) -> E. x e. HAtoms ( x =/= A /\ x =/= B /\ x C_ ( A vH B ) ) ) )
143 8 142 sylbid 
 |-  ( ( ( ( y e. ~H /\ z e. ~H ) /\ ( y =/= 0h /\ z =/= 0h ) ) /\ ( A = ( span ` { y } ) /\ B = ( span ` { z } ) ) ) -> ( A =/= B -> E. x e. HAtoms ( x =/= A /\ x =/= B /\ x C_ ( A vH B ) ) ) )
144 143 expl 
 |-  ( ( y e. ~H /\ z e. ~H ) -> ( ( ( y =/= 0h /\ z =/= 0h ) /\ ( A = ( span ` { y } ) /\ B = ( span ` { z } ) ) ) -> ( A =/= B -> E. x e. HAtoms ( x =/= A /\ x =/= B /\ x C_ ( A vH B ) ) ) ) )
145 4 144 syl5bi 
 |-  ( ( y e. ~H /\ z e. ~H ) -> ( ( ( y =/= 0h /\ A = ( span ` { y } ) ) /\ ( z =/= 0h /\ B = ( span ` { z } ) ) ) -> ( A =/= B -> E. x e. HAtoms ( x =/= A /\ x =/= B /\ x C_ ( A vH B ) ) ) ) )
146 145 rexlimivv 
 |-  ( E. y e. ~H E. z e. ~H ( ( y =/= 0h /\ A = ( span ` { y } ) ) /\ ( z =/= 0h /\ B = ( span ` { z } ) ) ) -> ( A =/= B -> E. x e. HAtoms ( x =/= A /\ x =/= B /\ x C_ ( A vH B ) ) ) )
147 3 146 sylbir 
 |-  ( ( E. y e. ~H ( y =/= 0h /\ A = ( span ` { y } ) ) /\ E. z e. ~H ( z =/= 0h /\ B = ( span ` { z } ) ) ) -> ( A =/= B -> E. x e. HAtoms ( x =/= A /\ x =/= B /\ x C_ ( A vH B ) ) ) )
148 1 2 147 syl2anb 
 |-  ( ( A e. HAtoms /\ B e. HAtoms ) -> ( A =/= B -> E. x e. HAtoms ( x =/= A /\ x =/= B /\ x C_ ( A vH B ) ) ) )
149 148 3impia 
 |-  ( ( A e. HAtoms /\ B e. HAtoms /\ A =/= B ) -> E. x e. HAtoms ( x =/= A /\ x =/= B /\ x C_ ( A vH B ) ) )