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 ( ( 𝐴 ∈ HAtoms ∧ 𝐵 ∈ HAtoms ∧ 𝐴 ≠ 𝐵 ) → ∃ 𝑥 ∈ HAtoms ( 𝑥 ≠ 𝐴 ∧ 𝑥 ≠ 𝐵 ∧ 𝑥 ⊆ ( 𝐴 ∨ℋ 𝐵 ) ) )

Proof

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