| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | atom1d 32373 | . . 3
⊢ (𝐴 ∈ HAtoms ↔
∃𝑦 ∈ ℋ
(𝑦 ≠
0ℎ ∧ 𝐴 = (span‘{𝑦}))) | 
| 2 |  | atom1d 32373 | . . 3
⊢ (𝐵 ∈ HAtoms ↔
∃𝑧 ∈ ℋ
(𝑧 ≠
0ℎ ∧ 𝐵 = (span‘{𝑧}))) | 
| 3 |  | reeanv 3228 | . . . 4
⊢
(∃𝑦 ∈
ℋ ∃𝑧 ∈
ℋ ((𝑦 ≠
0ℎ ∧ 𝐴 = (span‘{𝑦})) ∧ (𝑧 ≠ 0ℎ ∧ 𝐵 = (span‘{𝑧}))) ↔ (∃𝑦 ∈ ℋ (𝑦 ≠ 0ℎ ∧
𝐴 = (span‘{𝑦})) ∧ ∃𝑧 ∈ ℋ (𝑧 ≠ 0ℎ ∧
𝐵 = (span‘{𝑧})))) | 
| 4 |  | an4 656 | . . . . . 6
⊢ (((𝑦 ≠ 0ℎ ∧
𝐴 = (span‘{𝑦})) ∧ (𝑧 ≠ 0ℎ ∧ 𝐵 = (span‘{𝑧}))) ↔ ((𝑦 ≠ 0ℎ ∧ 𝑧 ≠ 0ℎ)
∧ (𝐴 =
(span‘{𝑦}) ∧
𝐵 = (span‘{𝑧})))) | 
| 5 |  | neeq1 3002 | . . . . . . . . . 10
⊢ (𝐴 = (span‘{𝑦}) → (𝐴 ≠ 𝐵 ↔ (span‘{𝑦}) ≠ 𝐵)) | 
| 6 |  | neeq2 3003 | . . . . . . . . . 10
⊢ (𝐵 = (span‘{𝑧}) → ((span‘{𝑦}) ≠ 𝐵 ↔ (span‘{𝑦}) ≠ (span‘{𝑧}))) | 
| 7 | 5, 6 | sylan9bb 509 | . . . . . . . . 9
⊢ ((𝐴 = (span‘{𝑦}) ∧ 𝐵 = (span‘{𝑧})) → (𝐴 ≠ 𝐵 ↔ (span‘{𝑦}) ≠ (span‘{𝑧}))) | 
| 8 | 7 | adantl 481 | . . . . . . . 8
⊢ ((((𝑦 ∈ ℋ ∧ 𝑧 ∈ ℋ) ∧ (𝑦 ≠ 0ℎ ∧
𝑧 ≠
0ℎ)) ∧ (𝐴 = (span‘{𝑦}) ∧ 𝐵 = (span‘{𝑧}))) → (𝐴 ≠ 𝐵 ↔ (span‘{𝑦}) ≠ (span‘{𝑧}))) | 
| 9 |  | hvaddcl 31032 | . . . . . . . . . . . . . 14
⊢ ((𝑦 ∈ ℋ ∧ 𝑧 ∈ ℋ) → (𝑦 +ℎ 𝑧) ∈
ℋ) | 
| 10 | 9 | adantr 480 | . . . . . . . . . . . . 13
⊢ (((𝑦 ∈ ℋ ∧ 𝑧 ∈ ℋ) ∧
(span‘{𝑦}) ≠
(span‘{𝑧})) →
(𝑦 +ℎ
𝑧) ∈
ℋ) | 
| 11 |  | hvaddeq0 31089 | . . . . . . . . . . . . . . . 16
⊢ ((𝑦 ∈ ℋ ∧ 𝑧 ∈ ℋ) → ((𝑦 +ℎ 𝑧) = 0ℎ ↔
𝑦 = (-1
·ℎ 𝑧))) | 
| 12 |  | sneq 4635 | . . . . . . . . . . . . . . . . . . . 20
⊢ (𝑦 = (-1
·ℎ 𝑧) → {𝑦} = {(-1 ·ℎ
𝑧)}) | 
| 13 | 12 | fveq2d 6909 | . . . . . . . . . . . . . . . . . . 19
⊢ (𝑦 = (-1
·ℎ 𝑧) → (span‘{𝑦}) = (span‘{(-1
·ℎ 𝑧)})) | 
| 14 |  | neg1cn 12381 | . . . . . . . . . . . . . . . . . . . 20
⊢ -1 ∈
ℂ | 
| 15 |  | neg1ne0 12383 | . . . . . . . . . . . . . . . . . . . 20
⊢ -1 ≠
0 | 
| 16 |  | spansncol 31588 | . . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑧 ∈ ℋ ∧ -1 ∈
ℂ ∧ -1 ≠ 0) → (span‘{(-1
·ℎ 𝑧)}) = (span‘{𝑧})) | 
| 17 | 14, 15, 16 | mp3an23 1454 | . . . . . . . . . . . . . . . . . . 19
⊢ (𝑧 ∈ ℋ →
(span‘{(-1 ·ℎ 𝑧)}) = (span‘{𝑧})) | 
| 18 | 13, 17 | sylan9eqr 2798 | . . . . . . . . . . . . . . . . . 18
⊢ ((𝑧 ∈ ℋ ∧ 𝑦 = (-1
·ℎ 𝑧)) → (span‘{𝑦}) = (span‘{𝑧})) | 
| 19 | 18 | ex 412 | . . . . . . . . . . . . . . . . 17
⊢ (𝑧 ∈ ℋ → (𝑦 = (-1
·ℎ 𝑧) → (span‘{𝑦}) = (span‘{𝑧}))) | 
| 20 | 19 | adantl 481 | . . . . . . . . . . . . . . . 16
⊢ ((𝑦 ∈ ℋ ∧ 𝑧 ∈ ℋ) → (𝑦 = (-1
·ℎ 𝑧) → (span‘{𝑦}) = (span‘{𝑧}))) | 
| 21 | 11, 20 | sylbid 240 | . . . . . . . . . . . . . . 15
⊢ ((𝑦 ∈ ℋ ∧ 𝑧 ∈ ℋ) → ((𝑦 +ℎ 𝑧) = 0ℎ →
(span‘{𝑦}) =
(span‘{𝑧}))) | 
| 22 | 21 | necon3d 2960 | . . . . . . . . . . . . . 14
⊢ ((𝑦 ∈ ℋ ∧ 𝑧 ∈ ℋ) →
((span‘{𝑦}) ≠
(span‘{𝑧}) →
(𝑦 +ℎ
𝑧) ≠
0ℎ)) | 
| 23 | 22 | imp 406 | . . . . . . . . . . . . 13
⊢ (((𝑦 ∈ ℋ ∧ 𝑧 ∈ ℋ) ∧
(span‘{𝑦}) ≠
(span‘{𝑧})) →
(𝑦 +ℎ
𝑧) ≠
0ℎ) | 
| 24 |  | spansna 32370 | . . . . . . . . . . . . 13
⊢ (((𝑦 +ℎ 𝑧) ∈ ℋ ∧ (𝑦 +ℎ 𝑧) ≠ 0ℎ)
→ (span‘{(𝑦
+ℎ 𝑧)})
∈ HAtoms) | 
| 25 | 10, 23, 24 | syl2anc 584 | . . . . . . . . . . . 12
⊢ (((𝑦 ∈ ℋ ∧ 𝑧 ∈ ℋ) ∧
(span‘{𝑦}) ≠
(span‘{𝑧})) →
(span‘{(𝑦
+ℎ 𝑧)})
∈ HAtoms) | 
| 26 | 25 | adantlr 715 | . . . . . . . . . . 11
⊢ ((((𝑦 ∈ ℋ ∧ 𝑧 ∈ ℋ) ∧ (𝑦 ≠ 0ℎ ∧
𝑧 ≠
0ℎ)) ∧ (span‘{𝑦}) ≠ (span‘{𝑧})) → (span‘{(𝑦 +ℎ 𝑧)}) ∈ HAtoms) | 
| 27 | 26 | adantlr 715 | . . . . . . . . . 10
⊢
(((((𝑦 ∈
ℋ ∧ 𝑧 ∈
ℋ) ∧ (𝑦 ≠
0ℎ ∧ 𝑧 ≠ 0ℎ)) ∧ (𝐴 = (span‘{𝑦}) ∧ 𝐵 = (span‘{𝑧}))) ∧ (span‘{𝑦}) ≠ (span‘{𝑧})) → (span‘{(𝑦 +ℎ 𝑧)}) ∈ HAtoms) | 
| 28 |  | eqeq2 2748 | . . . . . . . . . . . . . . . 16
⊢ (𝐴 = (span‘{𝑦}) → ((span‘{(𝑦 +ℎ 𝑧)}) = 𝐴 ↔ (span‘{(𝑦 +ℎ 𝑧)}) = (span‘{𝑦}))) | 
| 29 | 28 | biimpd 229 | . . . . . . . . . . . . . . 15
⊢ (𝐴 = (span‘{𝑦}) → ((span‘{(𝑦 +ℎ 𝑧)}) = 𝐴 → (span‘{(𝑦 +ℎ 𝑧)}) = (span‘{𝑦}))) | 
| 30 |  | spansneleqi 31589 | . . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑦 +ℎ 𝑧) ∈ ℋ →
((span‘{(𝑦
+ℎ 𝑧)}) =
(span‘{𝑦}) →
(𝑦 +ℎ
𝑧) ∈
(span‘{𝑦}))) | 
| 31 | 9, 30 | syl 17 | . . . . . . . . . . . . . . . . . . 19
⊢ ((𝑦 ∈ ℋ ∧ 𝑧 ∈ ℋ) →
((span‘{(𝑦
+ℎ 𝑧)}) =
(span‘{𝑦}) →
(𝑦 +ℎ
𝑧) ∈
(span‘{𝑦}))) | 
| 32 |  | elspansn 31586 | . . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑦 ∈ ℋ → ((𝑦 +ℎ 𝑧) ∈ (span‘{𝑦}) ↔ ∃𝑣 ∈ ℂ (𝑦 +ℎ 𝑧) = (𝑣 ·ℎ 𝑦))) | 
| 33 | 32 | adantr 480 | . . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑦 ∈ ℋ ∧ 𝑧 ∈ ℋ) → ((𝑦 +ℎ 𝑧) ∈ (span‘{𝑦}) ↔ ∃𝑣 ∈ ℂ (𝑦 +ℎ 𝑧) = (𝑣 ·ℎ 𝑦))) | 
| 34 |  | addcl 11238 | . . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝑣 ∈ ℂ ∧ -1 ∈
ℂ) → (𝑣 + -1)
∈ ℂ) | 
| 35 | 14, 34 | mpan2 691 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑣 ∈ ℂ → (𝑣 + -1) ∈
ℂ) | 
| 36 | 35 | ad2antlr 727 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ ((((𝑦 ∈ ℋ ∧ 𝑧 ∈ ℋ) ∧ 𝑣 ∈ ℂ) ∧ (𝑦 +ℎ 𝑧) = (𝑣 ·ℎ 𝑦)) → (𝑣 + -1) ∈ ℂ) | 
| 37 |  | hvmulcl 31033 | . . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝑣 ∈ ℂ ∧ 𝑦 ∈ ℋ) → (𝑣
·ℎ 𝑦) ∈ ℋ) | 
| 38 | 37 | ancoms 458 | . . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝑦 ∈ ℋ ∧ 𝑣 ∈ ℂ) → (𝑣
·ℎ 𝑦) ∈ ℋ) | 
| 39 | 38 | adantlr 715 | . . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (((𝑦 ∈ ℋ ∧ 𝑧 ∈ ℋ) ∧ 𝑣 ∈ ℂ) → (𝑣
·ℎ 𝑦) ∈ ℋ) | 
| 40 |  | simpll 766 | . . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (((𝑦 ∈ ℋ ∧ 𝑧 ∈ ℋ) ∧ 𝑣 ∈ ℂ) → 𝑦 ∈
ℋ) | 
| 41 |  | simplr 768 | . . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (((𝑦 ∈ ℋ ∧ 𝑧 ∈ ℋ) ∧ 𝑣 ∈ ℂ) → 𝑧 ∈
ℋ) | 
| 42 |  | hvsubadd 31097 | . . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (((𝑣
·ℎ 𝑦) ∈ ℋ ∧ 𝑦 ∈ ℋ ∧ 𝑧 ∈ ℋ) → (((𝑣 ·ℎ 𝑦) −ℎ
𝑦) = 𝑧 ↔ (𝑦 +ℎ 𝑧) = (𝑣 ·ℎ 𝑦))) | 
| 43 | 39, 40, 41, 42 | syl3anc 1372 | . . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (((𝑦 ∈ ℋ ∧ 𝑧 ∈ ℋ) ∧ 𝑣 ∈ ℂ) → (((𝑣
·ℎ 𝑦) −ℎ 𝑦) = 𝑧 ↔ (𝑦 +ℎ 𝑧) = (𝑣 ·ℎ 𝑦))) | 
| 44 | 43 | biimpar 477 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((((𝑦 ∈ ℋ ∧ 𝑧 ∈ ℋ) ∧ 𝑣 ∈ ℂ) ∧ (𝑦 +ℎ 𝑧) = (𝑣 ·ℎ 𝑦)) → ((𝑣 ·ℎ 𝑦) −ℎ
𝑦) = 𝑧) | 
| 45 |  | hvsubval 31036 | . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (((𝑣
·ℎ 𝑦) ∈ ℋ ∧ 𝑦 ∈ ℋ) → ((𝑣 ·ℎ 𝑦) −ℎ
𝑦) = ((𝑣 ·ℎ 𝑦) +ℎ (-1
·ℎ 𝑦))) | 
| 46 | 37, 45 | sylancom 588 | . . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝑣 ∈ ℂ ∧ 𝑦 ∈ ℋ) → ((𝑣
·ℎ 𝑦) −ℎ 𝑦) = ((𝑣 ·ℎ 𝑦) +ℎ (-1
·ℎ 𝑦))) | 
| 47 |  | ax-hvdistr2 31029 | . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((𝑣 ∈ ℂ ∧ -1 ∈
ℂ ∧ 𝑦 ∈
ℋ) → ((𝑣 + -1)
·ℎ 𝑦) = ((𝑣 ·ℎ 𝑦) +ℎ (-1
·ℎ 𝑦))) | 
| 48 | 14, 47 | mp3an2 1450 | . . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝑣 ∈ ℂ ∧ 𝑦 ∈ ℋ) → ((𝑣 + -1)
·ℎ 𝑦) = ((𝑣 ·ℎ 𝑦) +ℎ (-1
·ℎ 𝑦))) | 
| 49 | 46, 48 | eqtr4d 2779 | . . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝑣 ∈ ℂ ∧ 𝑦 ∈ ℋ) → ((𝑣
·ℎ 𝑦) −ℎ 𝑦) = ((𝑣 + -1) ·ℎ
𝑦)) | 
| 50 | 49 | ancoms 458 | . . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝑦 ∈ ℋ ∧ 𝑣 ∈ ℂ) → ((𝑣
·ℎ 𝑦) −ℎ 𝑦) = ((𝑣 + -1) ·ℎ
𝑦)) | 
| 51 | 50 | adantlr 715 | . . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (((𝑦 ∈ ℋ ∧ 𝑧 ∈ ℋ) ∧ 𝑣 ∈ ℂ) → ((𝑣
·ℎ 𝑦) −ℎ 𝑦) = ((𝑣 + -1) ·ℎ
𝑦)) | 
| 52 | 51 | adantr 480 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((((𝑦 ∈ ℋ ∧ 𝑧 ∈ ℋ) ∧ 𝑣 ∈ ℂ) ∧ (𝑦 +ℎ 𝑧) = (𝑣 ·ℎ 𝑦)) → ((𝑣 ·ℎ 𝑦) −ℎ
𝑦) = ((𝑣 + -1) ·ℎ
𝑦)) | 
| 53 | 44, 52 | eqtr3d 2778 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ ((((𝑦 ∈ ℋ ∧ 𝑧 ∈ ℋ) ∧ 𝑣 ∈ ℂ) ∧ (𝑦 +ℎ 𝑧) = (𝑣 ·ℎ 𝑦)) → 𝑧 = ((𝑣 + -1) ·ℎ
𝑦)) | 
| 54 |  | oveq1 7439 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑤 = (𝑣 + -1) → (𝑤 ·ℎ 𝑦) = ((𝑣 + -1) ·ℎ
𝑦)) | 
| 55 | 54 | rspceeqv 3644 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝑣 + -1) ∈ ℂ ∧
𝑧 = ((𝑣 + -1) ·ℎ
𝑦)) → ∃𝑤 ∈ ℂ 𝑧 = (𝑤 ·ℎ 𝑦)) | 
| 56 | 36, 53, 55 | syl2anc 584 | . . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝑦 ∈ ℋ ∧ 𝑧 ∈ ℋ) ∧ 𝑣 ∈ ℂ) ∧ (𝑦 +ℎ 𝑧) = (𝑣 ·ℎ 𝑦)) → ∃𝑤 ∈ ℂ 𝑧 = (𝑤 ·ℎ 𝑦)) | 
| 57 | 56 | rexlimdva2 3156 | . . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑦 ∈ ℋ ∧ 𝑧 ∈ ℋ) →
(∃𝑣 ∈ ℂ
(𝑦 +ℎ
𝑧) = (𝑣 ·ℎ 𝑦) → ∃𝑤 ∈ ℂ 𝑧 = (𝑤 ·ℎ 𝑦))) | 
| 58 | 33, 57 | sylbid 240 | . . . . . . . . . . . . . . . . . . 19
⊢ ((𝑦 ∈ ℋ ∧ 𝑧 ∈ ℋ) → ((𝑦 +ℎ 𝑧) ∈ (span‘{𝑦}) → ∃𝑤 ∈ ℂ 𝑧 = (𝑤 ·ℎ 𝑦))) | 
| 59 | 31, 58 | syld 47 | . . . . . . . . . . . . . . . . . 18
⊢ ((𝑦 ∈ ℋ ∧ 𝑧 ∈ ℋ) →
((span‘{(𝑦
+ℎ 𝑧)}) =
(span‘{𝑦}) →
∃𝑤 ∈ ℂ
𝑧 = (𝑤 ·ℎ 𝑦))) | 
| 60 |  | elspansn 31586 | . . . . . . . . . . . . . . . . . . 19
⊢ (𝑦 ∈ ℋ → (𝑧 ∈ (span‘{𝑦}) ↔ ∃𝑤 ∈ ℂ 𝑧 = (𝑤 ·ℎ 𝑦))) | 
| 61 | 60 | adantr 480 | . . . . . . . . . . . . . . . . . 18
⊢ ((𝑦 ∈ ℋ ∧ 𝑧 ∈ ℋ) → (𝑧 ∈ (span‘{𝑦}) ↔ ∃𝑤 ∈ ℂ 𝑧 = (𝑤 ·ℎ 𝑦))) | 
| 62 | 59, 61 | sylibrd 259 | . . . . . . . . . . . . . . . . 17
⊢ ((𝑦 ∈ ℋ ∧ 𝑧 ∈ ℋ) →
((span‘{(𝑦
+ℎ 𝑧)}) =
(span‘{𝑦}) →
𝑧 ∈ (span‘{𝑦}))) | 
| 63 | 62 | adantr 480 | . . . . . . . . . . . . . . . 16
⊢ (((𝑦 ∈ ℋ ∧ 𝑧 ∈ ℋ) ∧ 𝑧 ≠ 0ℎ)
→ ((span‘{(𝑦
+ℎ 𝑧)}) =
(span‘{𝑦}) →
𝑧 ∈ (span‘{𝑦}))) | 
| 64 |  | spansneleq 31590 | . . . . . . . . . . . . . . . . . 18
⊢ ((𝑦 ∈ ℋ ∧ 𝑧 ≠ 0ℎ)
→ (𝑧 ∈
(span‘{𝑦}) →
(span‘{𝑧}) =
(span‘{𝑦}))) | 
| 65 |  | eqcom 2743 | . . . . . . . . . . . . . . . . . 18
⊢
((span‘{𝑧}) =
(span‘{𝑦}) ↔
(span‘{𝑦}) =
(span‘{𝑧})) | 
| 66 | 64, 65 | imbitrdi 251 | . . . . . . . . . . . . . . . . 17
⊢ ((𝑦 ∈ ℋ ∧ 𝑧 ≠ 0ℎ)
→ (𝑧 ∈
(span‘{𝑦}) →
(span‘{𝑦}) =
(span‘{𝑧}))) | 
| 67 | 66 | adantlr 715 | . . . . . . . . . . . . . . . 16
⊢ (((𝑦 ∈ ℋ ∧ 𝑧 ∈ ℋ) ∧ 𝑧 ≠ 0ℎ)
→ (𝑧 ∈
(span‘{𝑦}) →
(span‘{𝑦}) =
(span‘{𝑧}))) | 
| 68 | 63, 67 | syld 47 | . . . . . . . . . . . . . . 15
⊢ (((𝑦 ∈ ℋ ∧ 𝑧 ∈ ℋ) ∧ 𝑧 ≠ 0ℎ)
→ ((span‘{(𝑦
+ℎ 𝑧)}) =
(span‘{𝑦}) →
(span‘{𝑦}) =
(span‘{𝑧}))) | 
| 69 | 29, 68 | sylan9r 508 | . . . . . . . . . . . . . 14
⊢ ((((𝑦 ∈ ℋ ∧ 𝑧 ∈ ℋ) ∧ 𝑧 ≠ 0ℎ)
∧ 𝐴 =
(span‘{𝑦})) →
((span‘{(𝑦
+ℎ 𝑧)}) =
𝐴 → (span‘{𝑦}) = (span‘{𝑧}))) | 
| 70 | 69 | necon3d 2960 | . . . . . . . . . . . . 13
⊢ ((((𝑦 ∈ ℋ ∧ 𝑧 ∈ ℋ) ∧ 𝑧 ≠ 0ℎ)
∧ 𝐴 =
(span‘{𝑦})) →
((span‘{𝑦}) ≠
(span‘{𝑧}) →
(span‘{(𝑦
+ℎ 𝑧)})
≠ 𝐴)) | 
| 71 | 70 | adantlrl 720 | . . . . . . . . . . . 12
⊢ ((((𝑦 ∈ ℋ ∧ 𝑧 ∈ ℋ) ∧ (𝑦 ≠ 0ℎ ∧
𝑧 ≠
0ℎ)) ∧ 𝐴 = (span‘{𝑦})) → ((span‘{𝑦}) ≠ (span‘{𝑧}) → (span‘{(𝑦 +ℎ 𝑧)}) ≠ 𝐴)) | 
| 72 | 71 | adantrr 717 | . . . . . . . . . . 11
⊢ ((((𝑦 ∈ ℋ ∧ 𝑧 ∈ ℋ) ∧ (𝑦 ≠ 0ℎ ∧
𝑧 ≠
0ℎ)) ∧ (𝐴 = (span‘{𝑦}) ∧ 𝐵 = (span‘{𝑧}))) → ((span‘{𝑦}) ≠ (span‘{𝑧}) → (span‘{(𝑦 +ℎ 𝑧)}) ≠ 𝐴)) | 
| 73 | 72 | imp 406 | . . . . . . . . . 10
⊢
(((((𝑦 ∈
ℋ ∧ 𝑧 ∈
ℋ) ∧ (𝑦 ≠
0ℎ ∧ 𝑧 ≠ 0ℎ)) ∧ (𝐴 = (span‘{𝑦}) ∧ 𝐵 = (span‘{𝑧}))) ∧ (span‘{𝑦}) ≠ (span‘{𝑧})) → (span‘{(𝑦 +ℎ 𝑧)}) ≠ 𝐴) | 
| 74 |  | eqeq2 2748 | . . . . . . . . . . . . . . . 16
⊢ (𝐵 = (span‘{𝑧}) → ((span‘{(𝑦 +ℎ 𝑧)}) = 𝐵 ↔ (span‘{(𝑦 +ℎ 𝑧)}) = (span‘{𝑧}))) | 
| 75 | 74 | biimpd 229 | . . . . . . . . . . . . . . 15
⊢ (𝐵 = (span‘{𝑧}) → ((span‘{(𝑦 +ℎ 𝑧)}) = 𝐵 → (span‘{(𝑦 +ℎ 𝑧)}) = (span‘{𝑧}))) | 
| 76 |  | spansneleqi 31589 | . . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑦 +ℎ 𝑧) ∈ ℋ →
((span‘{(𝑦
+ℎ 𝑧)}) =
(span‘{𝑧}) →
(𝑦 +ℎ
𝑧) ∈
(span‘{𝑧}))) | 
| 77 | 9, 76 | syl 17 | . . . . . . . . . . . . . . . . . . 19
⊢ ((𝑦 ∈ ℋ ∧ 𝑧 ∈ ℋ) →
((span‘{(𝑦
+ℎ 𝑧)}) =
(span‘{𝑧}) →
(𝑦 +ℎ
𝑧) ∈
(span‘{𝑧}))) | 
| 78 |  | elspansn 31586 | . . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑧 ∈ ℋ → ((𝑦 +ℎ 𝑧) ∈ (span‘{𝑧}) ↔ ∃𝑣 ∈ ℂ (𝑦 +ℎ 𝑧) = (𝑣 ·ℎ 𝑧))) | 
| 79 | 78 | adantl 481 | . . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑦 ∈ ℋ ∧ 𝑧 ∈ ℋ) → ((𝑦 +ℎ 𝑧) ∈ (span‘{𝑧}) ↔ ∃𝑣 ∈ ℂ (𝑦 +ℎ 𝑧) = (𝑣 ·ℎ 𝑧))) | 
| 80 | 35 | ad2antlr 727 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ ((((𝑦 ∈ ℋ ∧ 𝑧 ∈ ℋ) ∧ 𝑣 ∈ ℂ) ∧ (𝑦 +ℎ 𝑧) = (𝑣 ·ℎ 𝑧)) → (𝑣 + -1) ∈ ℂ) | 
| 81 |  | hvmulcl 31033 | . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((𝑣 ∈ ℂ ∧ 𝑧 ∈ ℋ) → (𝑣
·ℎ 𝑧) ∈ ℋ) | 
| 82 | 81 | ancoms 458 | . . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝑧 ∈ ℋ ∧ 𝑣 ∈ ℂ) → (𝑣
·ℎ 𝑧) ∈ ℋ) | 
| 83 | 82 | adantll 714 | . . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (((𝑦 ∈ ℋ ∧ 𝑧 ∈ ℋ) ∧ 𝑣 ∈ ℂ) → (𝑣
·ℎ 𝑧) ∈ ℋ) | 
| 84 |  | hvsubadd 31097 | . . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (((𝑣
·ℎ 𝑧) ∈ ℋ ∧ 𝑧 ∈ ℋ ∧ 𝑦 ∈ ℋ) → (((𝑣 ·ℎ 𝑧) −ℎ
𝑧) = 𝑦 ↔ (𝑧 +ℎ 𝑦) = (𝑣 ·ℎ 𝑧))) | 
| 85 | 83, 41, 40, 84 | syl3anc 1372 | . . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (((𝑦 ∈ ℋ ∧ 𝑧 ∈ ℋ) ∧ 𝑣 ∈ ℂ) → (((𝑣
·ℎ 𝑧) −ℎ 𝑧) = 𝑦 ↔ (𝑧 +ℎ 𝑦) = (𝑣 ·ℎ 𝑧))) | 
| 86 |  | ax-hvcom 31021 | . . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝑦 ∈ ℋ ∧ 𝑧 ∈ ℋ) → (𝑦 +ℎ 𝑧) = (𝑧 +ℎ 𝑦)) | 
| 87 | 86 | adantr 480 | . . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (((𝑦 ∈ ℋ ∧ 𝑧 ∈ ℋ) ∧ 𝑣 ∈ ℂ) → (𝑦 +ℎ 𝑧) = (𝑧 +ℎ 𝑦)) | 
| 88 | 87 | eqeq1d 2738 | . . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (((𝑦 ∈ ℋ ∧ 𝑧 ∈ ℋ) ∧ 𝑣 ∈ ℂ) → ((𝑦 +ℎ 𝑧) = (𝑣 ·ℎ 𝑧) ↔ (𝑧 +ℎ 𝑦) = (𝑣 ·ℎ 𝑧))) | 
| 89 | 85, 88 | bitr4d 282 | . . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (((𝑦 ∈ ℋ ∧ 𝑧 ∈ ℋ) ∧ 𝑣 ∈ ℂ) → (((𝑣
·ℎ 𝑧) −ℎ 𝑧) = 𝑦 ↔ (𝑦 +ℎ 𝑧) = (𝑣 ·ℎ 𝑧))) | 
| 90 | 89 | biimpar 477 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((((𝑦 ∈ ℋ ∧ 𝑧 ∈ ℋ) ∧ 𝑣 ∈ ℂ) ∧ (𝑦 +ℎ 𝑧) = (𝑣 ·ℎ 𝑧)) → ((𝑣 ·ℎ 𝑧) −ℎ
𝑧) = 𝑦) | 
| 91 |  | hvsubval 31036 | . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (((𝑣
·ℎ 𝑧) ∈ ℋ ∧ 𝑧 ∈ ℋ) → ((𝑣 ·ℎ 𝑧) −ℎ
𝑧) = ((𝑣 ·ℎ 𝑧) +ℎ (-1
·ℎ 𝑧))) | 
| 92 | 81, 91 | sylancom 588 | . . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝑣 ∈ ℂ ∧ 𝑧 ∈ ℋ) → ((𝑣
·ℎ 𝑧) −ℎ 𝑧) = ((𝑣 ·ℎ 𝑧) +ℎ (-1
·ℎ 𝑧))) | 
| 93 |  | ax-hvdistr2 31029 | . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((𝑣 ∈ ℂ ∧ -1 ∈
ℂ ∧ 𝑧 ∈
ℋ) → ((𝑣 + -1)
·ℎ 𝑧) = ((𝑣 ·ℎ 𝑧) +ℎ (-1
·ℎ 𝑧))) | 
| 94 | 14, 93 | mp3an2 1450 | . . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝑣 ∈ ℂ ∧ 𝑧 ∈ ℋ) → ((𝑣 + -1)
·ℎ 𝑧) = ((𝑣 ·ℎ 𝑧) +ℎ (-1
·ℎ 𝑧))) | 
| 95 | 92, 94 | eqtr4d 2779 | . . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝑣 ∈ ℂ ∧ 𝑧 ∈ ℋ) → ((𝑣
·ℎ 𝑧) −ℎ 𝑧) = ((𝑣 + -1) ·ℎ
𝑧)) | 
| 96 | 95 | ancoms 458 | . . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝑧 ∈ ℋ ∧ 𝑣 ∈ ℂ) → ((𝑣
·ℎ 𝑧) −ℎ 𝑧) = ((𝑣 + -1) ·ℎ
𝑧)) | 
| 97 | 96 | adantll 714 | . . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (((𝑦 ∈ ℋ ∧ 𝑧 ∈ ℋ) ∧ 𝑣 ∈ ℂ) → ((𝑣
·ℎ 𝑧) −ℎ 𝑧) = ((𝑣 + -1) ·ℎ
𝑧)) | 
| 98 | 97 | adantr 480 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((((𝑦 ∈ ℋ ∧ 𝑧 ∈ ℋ) ∧ 𝑣 ∈ ℂ) ∧ (𝑦 +ℎ 𝑧) = (𝑣 ·ℎ 𝑧)) → ((𝑣 ·ℎ 𝑧) −ℎ
𝑧) = ((𝑣 + -1) ·ℎ
𝑧)) | 
| 99 | 90, 98 | eqtr3d 2778 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ ((((𝑦 ∈ ℋ ∧ 𝑧 ∈ ℋ) ∧ 𝑣 ∈ ℂ) ∧ (𝑦 +ℎ 𝑧) = (𝑣 ·ℎ 𝑧)) → 𝑦 = ((𝑣 + -1) ·ℎ
𝑧)) | 
| 100 |  | oveq1 7439 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑤 = (𝑣 + -1) → (𝑤 ·ℎ 𝑧) = ((𝑣 + -1) ·ℎ
𝑧)) | 
| 101 | 100 | rspceeqv 3644 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝑣 + -1) ∈ ℂ ∧
𝑦 = ((𝑣 + -1) ·ℎ
𝑧)) → ∃𝑤 ∈ ℂ 𝑦 = (𝑤 ·ℎ 𝑧)) | 
| 102 | 80, 99, 101 | syl2anc 584 | . . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝑦 ∈ ℋ ∧ 𝑧 ∈ ℋ) ∧ 𝑣 ∈ ℂ) ∧ (𝑦 +ℎ 𝑧) = (𝑣 ·ℎ 𝑧)) → ∃𝑤 ∈ ℂ 𝑦 = (𝑤 ·ℎ 𝑧)) | 
| 103 | 102 | rexlimdva2 3156 | . . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑦 ∈ ℋ ∧ 𝑧 ∈ ℋ) →
(∃𝑣 ∈ ℂ
(𝑦 +ℎ
𝑧) = (𝑣 ·ℎ 𝑧) → ∃𝑤 ∈ ℂ 𝑦 = (𝑤 ·ℎ 𝑧))) | 
| 104 | 79, 103 | sylbid 240 | . . . . . . . . . . . . . . . . . . 19
⊢ ((𝑦 ∈ ℋ ∧ 𝑧 ∈ ℋ) → ((𝑦 +ℎ 𝑧) ∈ (span‘{𝑧}) → ∃𝑤 ∈ ℂ 𝑦 = (𝑤 ·ℎ 𝑧))) | 
| 105 | 77, 104 | syld 47 | . . . . . . . . . . . . . . . . . 18
⊢ ((𝑦 ∈ ℋ ∧ 𝑧 ∈ ℋ) →
((span‘{(𝑦
+ℎ 𝑧)}) =
(span‘{𝑧}) →
∃𝑤 ∈ ℂ
𝑦 = (𝑤 ·ℎ 𝑧))) | 
| 106 |  | elspansn 31586 | . . . . . . . . . . . . . . . . . . 19
⊢ (𝑧 ∈ ℋ → (𝑦 ∈ (span‘{𝑧}) ↔ ∃𝑤 ∈ ℂ 𝑦 = (𝑤 ·ℎ 𝑧))) | 
| 107 | 106 | adantl 481 | . . . . . . . . . . . . . . . . . 18
⊢ ((𝑦 ∈ ℋ ∧ 𝑧 ∈ ℋ) → (𝑦 ∈ (span‘{𝑧}) ↔ ∃𝑤 ∈ ℂ 𝑦 = (𝑤 ·ℎ 𝑧))) | 
| 108 | 105, 107 | sylibrd 259 | . . . . . . . . . . . . . . . . 17
⊢ ((𝑦 ∈ ℋ ∧ 𝑧 ∈ ℋ) →
((span‘{(𝑦
+ℎ 𝑧)}) =
(span‘{𝑧}) →
𝑦 ∈ (span‘{𝑧}))) | 
| 109 | 108 | adantr 480 | . . . . . . . . . . . . . . . 16
⊢ (((𝑦 ∈ ℋ ∧ 𝑧 ∈ ℋ) ∧ 𝑦 ≠ 0ℎ)
→ ((span‘{(𝑦
+ℎ 𝑧)}) =
(span‘{𝑧}) →
𝑦 ∈ (span‘{𝑧}))) | 
| 110 |  | spansneleq 31590 | . . . . . . . . . . . . . . . . 17
⊢ ((𝑧 ∈ ℋ ∧ 𝑦 ≠ 0ℎ)
→ (𝑦 ∈
(span‘{𝑧}) →
(span‘{𝑦}) =
(span‘{𝑧}))) | 
| 111 | 110 | adantll 714 | . . . . . . . . . . . . . . . 16
⊢ (((𝑦 ∈ ℋ ∧ 𝑧 ∈ ℋ) ∧ 𝑦 ≠ 0ℎ)
→ (𝑦 ∈
(span‘{𝑧}) →
(span‘{𝑦}) =
(span‘{𝑧}))) | 
| 112 | 109, 111 | syld 47 | . . . . . . . . . . . . . . 15
⊢ (((𝑦 ∈ ℋ ∧ 𝑧 ∈ ℋ) ∧ 𝑦 ≠ 0ℎ)
→ ((span‘{(𝑦
+ℎ 𝑧)}) =
(span‘{𝑧}) →
(span‘{𝑦}) =
(span‘{𝑧}))) | 
| 113 | 75, 112 | sylan9r 508 | . . . . . . . . . . . . . 14
⊢ ((((𝑦 ∈ ℋ ∧ 𝑧 ∈ ℋ) ∧ 𝑦 ≠ 0ℎ)
∧ 𝐵 =
(span‘{𝑧})) →
((span‘{(𝑦
+ℎ 𝑧)}) =
𝐵 → (span‘{𝑦}) = (span‘{𝑧}))) | 
| 114 | 113 | necon3d 2960 | . . . . . . . . . . . . 13
⊢ ((((𝑦 ∈ ℋ ∧ 𝑧 ∈ ℋ) ∧ 𝑦 ≠ 0ℎ)
∧ 𝐵 =
(span‘{𝑧})) →
((span‘{𝑦}) ≠
(span‘{𝑧}) →
(span‘{(𝑦
+ℎ 𝑧)})
≠ 𝐵)) | 
| 115 | 114 | adantlrr 721 | . . . . . . . . . . . 12
⊢ ((((𝑦 ∈ ℋ ∧ 𝑧 ∈ ℋ) ∧ (𝑦 ≠ 0ℎ ∧
𝑧 ≠
0ℎ)) ∧ 𝐵 = (span‘{𝑧})) → ((span‘{𝑦}) ≠ (span‘{𝑧}) → (span‘{(𝑦 +ℎ 𝑧)}) ≠ 𝐵)) | 
| 116 | 115 | adantrl 716 | . . . . . . . . . . 11
⊢ ((((𝑦 ∈ ℋ ∧ 𝑧 ∈ ℋ) ∧ (𝑦 ≠ 0ℎ ∧
𝑧 ≠
0ℎ)) ∧ (𝐴 = (span‘{𝑦}) ∧ 𝐵 = (span‘{𝑧}))) → ((span‘{𝑦}) ≠ (span‘{𝑧}) → (span‘{(𝑦 +ℎ 𝑧)}) ≠ 𝐵)) | 
| 117 | 116 | imp 406 | . . . . . . . . . 10
⊢
(((((𝑦 ∈
ℋ ∧ 𝑧 ∈
ℋ) ∧ (𝑦 ≠
0ℎ ∧ 𝑧 ≠ 0ℎ)) ∧ (𝐴 = (span‘{𝑦}) ∧ 𝐵 = (span‘{𝑧}))) ∧ (span‘{𝑦}) ≠ (span‘{𝑧})) → (span‘{(𝑦 +ℎ 𝑧)}) ≠ 𝐵) | 
| 118 |  | spanpr 31600 | . . . . . . . . . . . . . 14
⊢ ((𝑦 ∈ ℋ ∧ 𝑧 ∈ ℋ) →
(span‘{(𝑦
+ℎ 𝑧)})
⊆ (span‘{𝑦,
𝑧})) | 
| 119 | 118 | adantr 480 | . . . . . . . . . . . . 13
⊢ (((𝑦 ∈ ℋ ∧ 𝑧 ∈ ℋ) ∧ (𝐴 = (span‘{𝑦}) ∧ 𝐵 = (span‘{𝑧}))) → (span‘{(𝑦 +ℎ 𝑧)}) ⊆ (span‘{𝑦, 𝑧})) | 
| 120 |  | oveq12 7441 | . . . . . . . . . . . . . 14
⊢ ((𝐴 = (span‘{𝑦}) ∧ 𝐵 = (span‘{𝑧})) → (𝐴 ∨ℋ 𝐵) = ((span‘{𝑦}) ∨ℋ (span‘{𝑧}))) | 
| 121 |  | df-pr 4628 | . . . . . . . . . . . . . . . . 17
⊢ {𝑦, 𝑧} = ({𝑦} ∪ {𝑧}) | 
| 122 | 121 | fveq2i 6908 | . . . . . . . . . . . . . . . 16
⊢
(span‘{𝑦,
𝑧}) = (span‘({𝑦} ∪ {𝑧})) | 
| 123 |  | snssi 4807 | . . . . . . . . . . . . . . . . 17
⊢ (𝑦 ∈ ℋ → {𝑦} ⊆
ℋ) | 
| 124 |  | snssi 4807 | . . . . . . . . . . . . . . . . 17
⊢ (𝑧 ∈ ℋ → {𝑧} ⊆
ℋ) | 
| 125 |  | spanun 31565 | . . . . . . . . . . . . . . . . 17
⊢ (({𝑦} ⊆ ℋ ∧ {𝑧} ⊆ ℋ) →
(span‘({𝑦} ∪
{𝑧})) = ((span‘{𝑦}) +ℋ
(span‘{𝑧}))) | 
| 126 | 123, 124,
125 | syl2an 596 | . . . . . . . . . . . . . . . 16
⊢ ((𝑦 ∈ ℋ ∧ 𝑧 ∈ ℋ) →
(span‘({𝑦} ∪
{𝑧})) = ((span‘{𝑦}) +ℋ
(span‘{𝑧}))) | 
| 127 | 122, 126 | eqtrid 2788 | . . . . . . . . . . . . . . 15
⊢ ((𝑦 ∈ ℋ ∧ 𝑧 ∈ ℋ) →
(span‘{𝑦, 𝑧}) = ((span‘{𝑦}) +ℋ
(span‘{𝑧}))) | 
| 128 |  | spansnch 31580 | . . . . . . . . . . . . . . . 16
⊢ (𝑦 ∈ ℋ →
(span‘{𝑦}) ∈
Cℋ ) | 
| 129 |  | spansnj 31667 | . . . . . . . . . . . . . . . 16
⊢
(((span‘{𝑦})
∈ Cℋ ∧ 𝑧 ∈ ℋ) → ((span‘{𝑦}) +ℋ
(span‘{𝑧})) =
((span‘{𝑦})
∨ℋ (span‘{𝑧}))) | 
| 130 | 128, 129 | sylan 580 | . . . . . . . . . . . . . . 15
⊢ ((𝑦 ∈ ℋ ∧ 𝑧 ∈ ℋ) →
((span‘{𝑦})
+ℋ (span‘{𝑧})) = ((span‘{𝑦}) ∨ℋ (span‘{𝑧}))) | 
| 131 | 127, 130 | eqtr2d 2777 | . . . . . . . . . . . . . 14
⊢ ((𝑦 ∈ ℋ ∧ 𝑧 ∈ ℋ) →
((span‘{𝑦})
∨ℋ (span‘{𝑧})) = (span‘{𝑦, 𝑧})) | 
| 132 | 120, 131 | sylan9eqr 2798 | . . . . . . . . . . . . 13
⊢ (((𝑦 ∈ ℋ ∧ 𝑧 ∈ ℋ) ∧ (𝐴 = (span‘{𝑦}) ∧ 𝐵 = (span‘{𝑧}))) → (𝐴 ∨ℋ 𝐵) = (span‘{𝑦, 𝑧})) | 
| 133 | 119, 132 | sseqtrrd 4020 | . . . . . . . . . . . 12
⊢ (((𝑦 ∈ ℋ ∧ 𝑧 ∈ ℋ) ∧ (𝐴 = (span‘{𝑦}) ∧ 𝐵 = (span‘{𝑧}))) → (span‘{(𝑦 +ℎ 𝑧)}) ⊆ (𝐴 ∨ℋ 𝐵)) | 
| 134 | 133 | adantlr 715 | . . . . . . . . . . 11
⊢ ((((𝑦 ∈ ℋ ∧ 𝑧 ∈ ℋ) ∧ (𝑦 ≠ 0ℎ ∧
𝑧 ≠
0ℎ)) ∧ (𝐴 = (span‘{𝑦}) ∧ 𝐵 = (span‘{𝑧}))) → (span‘{(𝑦 +ℎ 𝑧)}) ⊆ (𝐴 ∨ℋ 𝐵)) | 
| 135 | 134 | adantr 480 | . . . . . . . . . 10
⊢
(((((𝑦 ∈
ℋ ∧ 𝑧 ∈
ℋ) ∧ (𝑦 ≠
0ℎ ∧ 𝑧 ≠ 0ℎ)) ∧ (𝐴 = (span‘{𝑦}) ∧ 𝐵 = (span‘{𝑧}))) ∧ (span‘{𝑦}) ≠ (span‘{𝑧})) → (span‘{(𝑦 +ℎ 𝑧)}) ⊆ (𝐴 ∨ℋ 𝐵)) | 
| 136 |  | neeq1 3002 | . . . . . . . . . . . 12
⊢ (𝑥 = (span‘{(𝑦 +ℎ 𝑧)}) → (𝑥 ≠ 𝐴 ↔ (span‘{(𝑦 +ℎ 𝑧)}) ≠ 𝐴)) | 
| 137 |  | neeq1 3002 | . . . . . . . . . . . 12
⊢ (𝑥 = (span‘{(𝑦 +ℎ 𝑧)}) → (𝑥 ≠ 𝐵 ↔ (span‘{(𝑦 +ℎ 𝑧)}) ≠ 𝐵)) | 
| 138 |  | sseq1 4008 | . . . . . . . . . . . 12
⊢ (𝑥 = (span‘{(𝑦 +ℎ 𝑧)}) → (𝑥 ⊆ (𝐴 ∨ℋ 𝐵) ↔ (span‘{(𝑦 +ℎ 𝑧)}) ⊆ (𝐴 ∨ℋ 𝐵))) | 
| 139 | 136, 137,
138 | 3anbi123d 1437 | . . . . . . . . . . 11
⊢ (𝑥 = (span‘{(𝑦 +ℎ 𝑧)}) → ((𝑥 ≠ 𝐴 ∧ 𝑥 ≠ 𝐵 ∧ 𝑥 ⊆ (𝐴 ∨ℋ 𝐵)) ↔ ((span‘{(𝑦 +ℎ 𝑧)}) ≠ 𝐴 ∧ (span‘{(𝑦 +ℎ 𝑧)}) ≠ 𝐵 ∧ (span‘{(𝑦 +ℎ 𝑧)}) ⊆ (𝐴 ∨ℋ 𝐵)))) | 
| 140 | 139 | rspcev 3621 | . . . . . . . . . 10
⊢
(((span‘{(𝑦
+ℎ 𝑧)})
∈ HAtoms ∧ ((span‘{(𝑦 +ℎ 𝑧)}) ≠ 𝐴 ∧ (span‘{(𝑦 +ℎ 𝑧)}) ≠ 𝐵 ∧ (span‘{(𝑦 +ℎ 𝑧)}) ⊆ (𝐴 ∨ℋ 𝐵))) → ∃𝑥 ∈ HAtoms (𝑥 ≠ 𝐴 ∧ 𝑥 ≠ 𝐵 ∧ 𝑥 ⊆ (𝐴 ∨ℋ 𝐵))) | 
| 141 | 27, 73, 117, 135, 140 | syl13anc 1373 | . . . . . . . . 9
⊢
(((((𝑦 ∈
ℋ ∧ 𝑧 ∈
ℋ) ∧ (𝑦 ≠
0ℎ ∧ 𝑧 ≠ 0ℎ)) ∧ (𝐴 = (span‘{𝑦}) ∧ 𝐵 = (span‘{𝑧}))) ∧ (span‘{𝑦}) ≠ (span‘{𝑧})) → ∃𝑥 ∈ HAtoms (𝑥 ≠ 𝐴 ∧ 𝑥 ≠ 𝐵 ∧ 𝑥 ⊆ (𝐴 ∨ℋ 𝐵))) | 
| 142 | 141 | ex 412 | . . . . . . . 8
⊢ ((((𝑦 ∈ ℋ ∧ 𝑧 ∈ ℋ) ∧ (𝑦 ≠ 0ℎ ∧
𝑧 ≠
0ℎ)) ∧ (𝐴 = (span‘{𝑦}) ∧ 𝐵 = (span‘{𝑧}))) → ((span‘{𝑦}) ≠ (span‘{𝑧}) → ∃𝑥 ∈ HAtoms (𝑥 ≠ 𝐴 ∧ 𝑥 ≠ 𝐵 ∧ 𝑥 ⊆ (𝐴 ∨ℋ 𝐵)))) | 
| 143 | 8, 142 | sylbid 240 | . . . . . . 7
⊢ ((((𝑦 ∈ ℋ ∧ 𝑧 ∈ ℋ) ∧ (𝑦 ≠ 0ℎ ∧
𝑧 ≠
0ℎ)) ∧ (𝐴 = (span‘{𝑦}) ∧ 𝐵 = (span‘{𝑧}))) → (𝐴 ≠ 𝐵 → ∃𝑥 ∈ HAtoms (𝑥 ≠ 𝐴 ∧ 𝑥 ≠ 𝐵 ∧ 𝑥 ⊆ (𝐴 ∨ℋ 𝐵)))) | 
| 144 | 143 | expl 457 | . . . . . 6
⊢ ((𝑦 ∈ ℋ ∧ 𝑧 ∈ ℋ) → (((𝑦 ≠ 0ℎ ∧
𝑧 ≠
0ℎ) ∧ (𝐴 = (span‘{𝑦}) ∧ 𝐵 = (span‘{𝑧}))) → (𝐴 ≠ 𝐵 → ∃𝑥 ∈ HAtoms (𝑥 ≠ 𝐴 ∧ 𝑥 ≠ 𝐵 ∧ 𝑥 ⊆ (𝐴 ∨ℋ 𝐵))))) | 
| 145 | 4, 144 | biimtrid 242 | . . . . 5
⊢ ((𝑦 ∈ ℋ ∧ 𝑧 ∈ ℋ) → (((𝑦 ≠ 0ℎ ∧
𝐴 = (span‘{𝑦})) ∧ (𝑧 ≠ 0ℎ ∧ 𝐵 = (span‘{𝑧}))) → (𝐴 ≠ 𝐵 → ∃𝑥 ∈ HAtoms (𝑥 ≠ 𝐴 ∧ 𝑥 ≠ 𝐵 ∧ 𝑥 ⊆ (𝐴 ∨ℋ 𝐵))))) | 
| 146 | 145 | rexlimivv 3200 | . . . 4
⊢
(∃𝑦 ∈
ℋ ∃𝑧 ∈
ℋ ((𝑦 ≠
0ℎ ∧ 𝐴 = (span‘{𝑦})) ∧ (𝑧 ≠ 0ℎ ∧ 𝐵 = (span‘{𝑧}))) → (𝐴 ≠ 𝐵 → ∃𝑥 ∈ HAtoms (𝑥 ≠ 𝐴 ∧ 𝑥 ≠ 𝐵 ∧ 𝑥 ⊆ (𝐴 ∨ℋ 𝐵)))) | 
| 147 | 3, 146 | sylbir 235 | . . 3
⊢
((∃𝑦 ∈
ℋ (𝑦 ≠
0ℎ ∧ 𝐴 = (span‘{𝑦})) ∧ ∃𝑧 ∈ ℋ (𝑧 ≠ 0ℎ ∧ 𝐵 = (span‘{𝑧}))) → (𝐴 ≠ 𝐵 → ∃𝑥 ∈ HAtoms (𝑥 ≠ 𝐴 ∧ 𝑥 ≠ 𝐵 ∧ 𝑥 ⊆ (𝐴 ∨ℋ 𝐵)))) | 
| 148 | 1, 2, 147 | syl2anb 598 | . 2
⊢ ((𝐴 ∈ HAtoms ∧ 𝐵 ∈ HAtoms) → (𝐴 ≠ 𝐵 → ∃𝑥 ∈ HAtoms (𝑥 ≠ 𝐴 ∧ 𝑥 ≠ 𝐵 ∧ 𝑥 ⊆ (𝐴 ∨ℋ 𝐵)))) | 
| 149 | 148 | 3impia 1117 | 1
⊢ ((𝐴 ∈ HAtoms ∧ 𝐵 ∈ HAtoms ∧ 𝐴 ≠ 𝐵) → ∃𝑥 ∈ HAtoms (𝑥 ≠ 𝐴 ∧ 𝑥 ≠ 𝐵 ∧ 𝑥 ⊆ (𝐴 ∨ℋ 𝐵))) |