| Step | Hyp | Ref
| Expression |
| 1 | | sumdmdi.1 |
. . . . . . . 8
⊢ 𝐴 ∈
Cℋ |
| 2 | | sumdmdi.2 |
. . . . . . . 8
⊢ 𝐵 ∈
Cℋ |
| 3 | 1, 2 | chjcli 31476 |
. . . . . . 7
⊢ (𝐴 ∨ℋ 𝐵) ∈
Cℋ |
| 4 | 3 | cheli 31251 |
. . . . . 6
⊢ (𝑦 ∈ (𝐴 ∨ℋ 𝐵) → 𝑦 ∈ ℋ) |
| 5 | | spansnsh 31580 |
. . . . . . . . . . . . 13
⊢ (𝑦 ∈ ℋ →
(span‘{𝑦}) ∈
Sℋ ) |
| 6 | 2 | chshii 31246 |
. . . . . . . . . . . . 13
⊢ 𝐵 ∈
Sℋ |
| 7 | | shsub2 31344 |
. . . . . . . . . . . . 13
⊢
(((span‘{𝑦})
∈ Sℋ ∧ 𝐵 ∈ Sℋ )
→ (span‘{𝑦})
⊆ (𝐵
+ℋ (span‘{𝑦}))) |
| 8 | 5, 6, 7 | sylancl 586 |
. . . . . . . . . . . 12
⊢ (𝑦 ∈ ℋ →
(span‘{𝑦}) ⊆
(𝐵 +ℋ
(span‘{𝑦}))) |
| 9 | | spansnid 31582 |
. . . . . . . . . . . 12
⊢ (𝑦 ∈ ℋ → 𝑦 ∈ (span‘{𝑦})) |
| 10 | 8, 9 | sseldd 3984 |
. . . . . . . . . . 11
⊢ (𝑦 ∈ ℋ → 𝑦 ∈ (𝐵 +ℋ (span‘{𝑦}))) |
| 11 | 10 | ad2antrl 728 |
. . . . . . . . . 10
⊢
((∀𝑥 ∈
HAtoms ((𝑥
∨ℋ 𝐵)
∩ (𝐴
∨ℋ 𝐵))
⊆ (((𝑥
∨ℋ 𝐵)
∩ 𝐴)
∨ℋ 𝐵)
∧ (𝑦 ∈ ℋ
∧ ¬ 𝑦 ∈ (𝐴 +ℋ 𝐵))) → 𝑦 ∈ (𝐵 +ℋ (span‘{𝑦}))) |
| 12 | | elin 3967 |
. . . . . . . . . . 11
⊢ (𝑦 ∈ ((𝐵 +ℋ (span‘{𝑦})) ∩ (𝐴 ∨ℋ 𝐵)) ↔ (𝑦 ∈ (𝐵 +ℋ (span‘{𝑦})) ∧ 𝑦 ∈ (𝐴 ∨ℋ 𝐵))) |
| 13 | | df-ne 2941 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑦 ≠ 0ℎ
↔ ¬ 𝑦 =
0ℎ) |
| 14 | | spansna 32369 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑦 ∈ ℋ ∧ 𝑦 ≠ 0ℎ)
→ (span‘{𝑦})
∈ HAtoms) |
| 15 | 13, 14 | sylan2br 595 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑦 ∈ ℋ ∧ ¬
𝑦 = 0ℎ)
→ (span‘{𝑦})
∈ HAtoms) |
| 16 | | oveq1 7438 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑥 = (span‘{𝑦}) → (𝑥 ∨ℋ 𝐵) = ((span‘{𝑦}) ∨ℋ 𝐵)) |
| 17 | 16 | ineq1d 4219 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑥 = (span‘{𝑦}) → ((𝑥 ∨ℋ 𝐵) ∩ (𝐴 ∨ℋ 𝐵)) = (((span‘{𝑦}) ∨ℋ 𝐵) ∩ (𝐴 ∨ℋ 𝐵))) |
| 18 | 16 | ineq1d 4219 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑥 = (span‘{𝑦}) → ((𝑥 ∨ℋ 𝐵) ∩ 𝐴) = (((span‘{𝑦}) ∨ℋ 𝐵) ∩ 𝐴)) |
| 19 | 18 | oveq1d 7446 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑥 = (span‘{𝑦}) → (((𝑥 ∨ℋ 𝐵) ∩ 𝐴) ∨ℋ 𝐵) = ((((span‘{𝑦}) ∨ℋ 𝐵) ∩ 𝐴) ∨ℋ 𝐵)) |
| 20 | 17, 19 | sseq12d 4017 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑥 = (span‘{𝑦}) → (((𝑥 ∨ℋ 𝐵) ∩ (𝐴 ∨ℋ 𝐵)) ⊆ (((𝑥 ∨ℋ 𝐵) ∩ 𝐴) ∨ℋ 𝐵) ↔ (((span‘{𝑦}) ∨ℋ 𝐵) ∩ (𝐴 ∨ℋ 𝐵)) ⊆ ((((span‘{𝑦}) ∨ℋ 𝐵) ∩ 𝐴) ∨ℋ 𝐵))) |
| 21 | 20 | rspcv 3618 |
. . . . . . . . . . . . . . . . . . 19
⊢
((span‘{𝑦})
∈ HAtoms → (∀𝑥 ∈ HAtoms ((𝑥 ∨ℋ 𝐵) ∩ (𝐴 ∨ℋ 𝐵)) ⊆ (((𝑥 ∨ℋ 𝐵) ∩ 𝐴) ∨ℋ 𝐵) → (((span‘{𝑦}) ∨ℋ 𝐵) ∩ (𝐴 ∨ℋ 𝐵)) ⊆ ((((span‘{𝑦}) ∨ℋ 𝐵) ∩ 𝐴) ∨ℋ 𝐵))) |
| 22 | 15, 21 | syl 17 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑦 ∈ ℋ ∧ ¬
𝑦 = 0ℎ)
→ (∀𝑥 ∈
HAtoms ((𝑥
∨ℋ 𝐵)
∩ (𝐴
∨ℋ 𝐵))
⊆ (((𝑥
∨ℋ 𝐵)
∩ 𝐴)
∨ℋ 𝐵)
→ (((span‘{𝑦})
∨ℋ 𝐵)
∩ (𝐴
∨ℋ 𝐵))
⊆ ((((span‘{𝑦})
∨ℋ 𝐵)
∩ 𝐴)
∨ℋ 𝐵))) |
| 23 | | spansnj 31666 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝐵 ∈
Cℋ ∧ 𝑦 ∈ ℋ) → (𝐵 +ℋ (span‘{𝑦})) = (𝐵 ∨ℋ (span‘{𝑦}))) |
| 24 | | spansnch 31579 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑦 ∈ ℋ →
(span‘{𝑦}) ∈
Cℋ ) |
| 25 | | chjcom 31525 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝐵 ∈
Cℋ ∧ (span‘{𝑦}) ∈ Cℋ )
→ (𝐵
∨ℋ (span‘{𝑦})) = ((span‘{𝑦}) ∨ℋ 𝐵)) |
| 26 | 24, 25 | sylan2 593 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝐵 ∈
Cℋ ∧ 𝑦 ∈ ℋ) → (𝐵 ∨ℋ (span‘{𝑦})) = ((span‘{𝑦}) ∨ℋ 𝐵)) |
| 27 | 23, 26 | eqtrd 2777 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝐵 ∈
Cℋ ∧ 𝑦 ∈ ℋ) → (𝐵 +ℋ (span‘{𝑦})) = ((span‘{𝑦}) ∨ℋ 𝐵)) |
| 28 | 2, 27 | mpan 690 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑦 ∈ ℋ → (𝐵 +ℋ
(span‘{𝑦})) =
((span‘{𝑦})
∨ℋ 𝐵)) |
| 29 | 28 | ineq1d 4219 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑦 ∈ ℋ → ((𝐵 +ℋ
(span‘{𝑦})) ∩
(𝐴 ∨ℋ
𝐵)) = (((span‘{𝑦}) ∨ℋ 𝐵) ∩ (𝐴 ∨ℋ 𝐵))) |
| 30 | 28 | ineq1d 4219 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑦 ∈ ℋ → ((𝐵 +ℋ
(span‘{𝑦})) ∩
𝐴) = (((span‘{𝑦}) ∨ℋ 𝐵) ∩ 𝐴)) |
| 31 | 30 | oveq1d 7446 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑦 ∈ ℋ → (((𝐵 +ℋ
(span‘{𝑦})) ∩
𝐴) ∨ℋ
𝐵) = ((((span‘{𝑦}) ∨ℋ 𝐵) ∩ 𝐴) ∨ℋ 𝐵)) |
| 32 | 29, 31 | sseq12d 4017 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑦 ∈ ℋ → (((𝐵 +ℋ
(span‘{𝑦})) ∩
(𝐴 ∨ℋ
𝐵)) ⊆ (((𝐵 +ℋ
(span‘{𝑦})) ∩
𝐴) ∨ℋ
𝐵) ↔
(((span‘{𝑦})
∨ℋ 𝐵)
∩ (𝐴
∨ℋ 𝐵))
⊆ ((((span‘{𝑦})
∨ℋ 𝐵)
∩ 𝐴)
∨ℋ 𝐵))) |
| 33 | 32 | adantr 480 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑦 ∈ ℋ ∧ ¬
𝑦 = 0ℎ)
→ (((𝐵
+ℋ (span‘{𝑦})) ∩ (𝐴 ∨ℋ 𝐵)) ⊆ (((𝐵 +ℋ (span‘{𝑦})) ∩ 𝐴) ∨ℋ 𝐵) ↔ (((span‘{𝑦}) ∨ℋ 𝐵) ∩ (𝐴 ∨ℋ 𝐵)) ⊆ ((((span‘{𝑦}) ∨ℋ 𝐵) ∩ 𝐴) ∨ℋ 𝐵))) |
| 34 | 22, 33 | sylibrd 259 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑦 ∈ ℋ ∧ ¬
𝑦 = 0ℎ)
→ (∀𝑥 ∈
HAtoms ((𝑥
∨ℋ 𝐵)
∩ (𝐴
∨ℋ 𝐵))
⊆ (((𝑥
∨ℋ 𝐵)
∩ 𝐴)
∨ℋ 𝐵)
→ ((𝐵
+ℋ (span‘{𝑦})) ∩ (𝐴 ∨ℋ 𝐵)) ⊆ (((𝐵 +ℋ (span‘{𝑦})) ∩ 𝐴) ∨ℋ 𝐵))) |
| 35 | 34 | com12 32 |
. . . . . . . . . . . . . . . 16
⊢
(∀𝑥 ∈
HAtoms ((𝑥
∨ℋ 𝐵)
∩ (𝐴
∨ℋ 𝐵))
⊆ (((𝑥
∨ℋ 𝐵)
∩ 𝐴)
∨ℋ 𝐵)
→ ((𝑦 ∈ ℋ
∧ ¬ 𝑦 =
0ℎ) → ((𝐵 +ℋ (span‘{𝑦})) ∩ (𝐴 ∨ℋ 𝐵)) ⊆ (((𝐵 +ℋ (span‘{𝑦})) ∩ 𝐴) ∨ℋ 𝐵))) |
| 36 | 35 | expdimp 452 |
. . . . . . . . . . . . . . 15
⊢
((∀𝑥 ∈
HAtoms ((𝑥
∨ℋ 𝐵)
∩ (𝐴
∨ℋ 𝐵))
⊆ (((𝑥
∨ℋ 𝐵)
∩ 𝐴)
∨ℋ 𝐵)
∧ 𝑦 ∈ ℋ)
→ (¬ 𝑦 =
0ℎ → ((𝐵 +ℋ (span‘{𝑦})) ∩ (𝐴 ∨ℋ 𝐵)) ⊆ (((𝐵 +ℋ (span‘{𝑦})) ∩ 𝐴) ∨ℋ 𝐵))) |
| 37 | | ssid 4006 |
. . . . . . . . . . . . . . . 16
⊢ 𝐵 ⊆ 𝐵 |
| 38 | | sneq 4636 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑦 = 0ℎ →
{𝑦} =
{0ℎ}) |
| 39 | 38 | fveq2d 6910 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑦 = 0ℎ →
(span‘{𝑦}) =
(span‘{0ℎ})) |
| 40 | | spansn0 31560 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
(span‘{0ℎ}) =
0ℋ |
| 41 | 39, 40 | eqtrdi 2793 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑦 = 0ℎ →
(span‘{𝑦}) =
0ℋ) |
| 42 | 41 | oveq2d 7447 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑦 = 0ℎ →
(𝐵 +ℋ
(span‘{𝑦})) = (𝐵 +ℋ
0ℋ)) |
| 43 | 6 | shs0i 31468 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝐵 +ℋ
0ℋ) = 𝐵 |
| 44 | 42, 43 | eqtrdi 2793 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑦 = 0ℎ →
(𝐵 +ℋ
(span‘{𝑦})) = 𝐵) |
| 45 | 44 | ineq1d 4219 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑦 = 0ℎ →
((𝐵 +ℋ
(span‘{𝑦})) ∩
(𝐴 ∨ℋ
𝐵)) = (𝐵 ∩ (𝐴 ∨ℋ 𝐵))) |
| 46 | | inss1 4237 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝐵 ∩ (𝐴 ∨ℋ 𝐵)) ⊆ 𝐵 |
| 47 | 2, 1 | chub2i 31489 |
. . . . . . . . . . . . . . . . . . . 20
⊢ 𝐵 ⊆ (𝐴 ∨ℋ 𝐵) |
| 48 | 37, 47 | ssini 4240 |
. . . . . . . . . . . . . . . . . . 19
⊢ 𝐵 ⊆ (𝐵 ∩ (𝐴 ∨ℋ 𝐵)) |
| 49 | 46, 48 | eqssi 4000 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝐵 ∩ (𝐴 ∨ℋ 𝐵)) = 𝐵 |
| 50 | 45, 49 | eqtrdi 2793 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑦 = 0ℎ →
((𝐵 +ℋ
(span‘{𝑦})) ∩
(𝐴 ∨ℋ
𝐵)) = 𝐵) |
| 51 | 44 | ineq1d 4219 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑦 = 0ℎ →
((𝐵 +ℋ
(span‘{𝑦})) ∩
𝐴) = (𝐵 ∩ 𝐴)) |
| 52 | 51 | oveq1d 7446 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑦 = 0ℎ →
(((𝐵 +ℋ
(span‘{𝑦})) ∩
𝐴) ∨ℋ
𝐵) = ((𝐵 ∩ 𝐴) ∨ℋ 𝐵)) |
| 53 | 2, 1 | chincli 31479 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝐵 ∩ 𝐴) ∈
Cℋ |
| 54 | 53, 2 | chjcomi 31487 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝐵 ∩ 𝐴) ∨ℋ 𝐵) = (𝐵 ∨ℋ (𝐵 ∩ 𝐴)) |
| 55 | 2, 1 | chabs1i 31537 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝐵 ∨ℋ (𝐵 ∩ 𝐴)) = 𝐵 |
| 56 | 54, 55 | eqtri 2765 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝐵 ∩ 𝐴) ∨ℋ 𝐵) = 𝐵 |
| 57 | 52, 56 | eqtrdi 2793 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑦 = 0ℎ →
(((𝐵 +ℋ
(span‘{𝑦})) ∩
𝐴) ∨ℋ
𝐵) = 𝐵) |
| 58 | 50, 57 | sseq12d 4017 |
. . . . . . . . . . . . . . . 16
⊢ (𝑦 = 0ℎ →
(((𝐵 +ℋ
(span‘{𝑦})) ∩
(𝐴 ∨ℋ
𝐵)) ⊆ (((𝐵 +ℋ
(span‘{𝑦})) ∩
𝐴) ∨ℋ
𝐵) ↔ 𝐵 ⊆ 𝐵)) |
| 59 | 37, 58 | mpbiri 258 |
. . . . . . . . . . . . . . 15
⊢ (𝑦 = 0ℎ →
((𝐵 +ℋ
(span‘{𝑦})) ∩
(𝐴 ∨ℋ
𝐵)) ⊆ (((𝐵 +ℋ
(span‘{𝑦})) ∩
𝐴) ∨ℋ
𝐵)) |
| 60 | 36, 59 | pm2.61d2 181 |
. . . . . . . . . . . . . 14
⊢
((∀𝑥 ∈
HAtoms ((𝑥
∨ℋ 𝐵)
∩ (𝐴
∨ℋ 𝐵))
⊆ (((𝑥
∨ℋ 𝐵)
∩ 𝐴)
∨ℋ 𝐵)
∧ 𝑦 ∈ ℋ)
→ ((𝐵
+ℋ (span‘{𝑦})) ∩ (𝐴 ∨ℋ 𝐵)) ⊆ (((𝐵 +ℋ (span‘{𝑦})) ∩ 𝐴) ∨ℋ 𝐵)) |
| 61 | 60 | adantrr 717 |
. . . . . . . . . . . . 13
⊢
((∀𝑥 ∈
HAtoms ((𝑥
∨ℋ 𝐵)
∩ (𝐴
∨ℋ 𝐵))
⊆ (((𝑥
∨ℋ 𝐵)
∩ 𝐴)
∨ℋ 𝐵)
∧ (𝑦 ∈ ℋ
∧ ¬ 𝑦 ∈ (𝐴 +ℋ 𝐵))) → ((𝐵 +ℋ (span‘{𝑦})) ∩ (𝐴 ∨ℋ 𝐵)) ⊆ (((𝐵 +ℋ (span‘{𝑦})) ∩ 𝐴) ∨ℋ 𝐵)) |
| 62 | 1, 2 | sumdmdlem 32437 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑦 ∈ ℋ ∧ ¬
𝑦 ∈ (𝐴 +ℋ 𝐵)) → ((𝐵 +ℋ (span‘{𝑦})) ∩ 𝐴) = (𝐵 ∩ 𝐴)) |
| 63 | 62 | oveq1d 7446 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑦 ∈ ℋ ∧ ¬
𝑦 ∈ (𝐴 +ℋ 𝐵)) → (((𝐵 +ℋ (span‘{𝑦})) ∩ 𝐴) ∨ℋ 𝐵) = ((𝐵 ∩ 𝐴) ∨ℋ 𝐵)) |
| 64 | 63, 56 | eqtrdi 2793 |
. . . . . . . . . . . . . . 15
⊢ ((𝑦 ∈ ℋ ∧ ¬
𝑦 ∈ (𝐴 +ℋ 𝐵)) → (((𝐵 +ℋ (span‘{𝑦})) ∩ 𝐴) ∨ℋ 𝐵) = 𝐵) |
| 65 | 1 | chshii 31246 |
. . . . . . . . . . . . . . . 16
⊢ 𝐴 ∈
Sℋ |
| 66 | 6, 65 | shsub2i 31392 |
. . . . . . . . . . . . . . 15
⊢ 𝐵 ⊆ (𝐴 +ℋ 𝐵) |
| 67 | 64, 66 | eqsstrdi 4028 |
. . . . . . . . . . . . . 14
⊢ ((𝑦 ∈ ℋ ∧ ¬
𝑦 ∈ (𝐴 +ℋ 𝐵)) → (((𝐵 +ℋ (span‘{𝑦})) ∩ 𝐴) ∨ℋ 𝐵) ⊆ (𝐴 +ℋ 𝐵)) |
| 68 | 67 | adantl 481 |
. . . . . . . . . . . . 13
⊢
((∀𝑥 ∈
HAtoms ((𝑥
∨ℋ 𝐵)
∩ (𝐴
∨ℋ 𝐵))
⊆ (((𝑥
∨ℋ 𝐵)
∩ 𝐴)
∨ℋ 𝐵)
∧ (𝑦 ∈ ℋ
∧ ¬ 𝑦 ∈ (𝐴 +ℋ 𝐵))) → (((𝐵 +ℋ (span‘{𝑦})) ∩ 𝐴) ∨ℋ 𝐵) ⊆ (𝐴 +ℋ 𝐵)) |
| 69 | 61, 68 | sstrd 3994 |
. . . . . . . . . . . 12
⊢
((∀𝑥 ∈
HAtoms ((𝑥
∨ℋ 𝐵)
∩ (𝐴
∨ℋ 𝐵))
⊆ (((𝑥
∨ℋ 𝐵)
∩ 𝐴)
∨ℋ 𝐵)
∧ (𝑦 ∈ ℋ
∧ ¬ 𝑦 ∈ (𝐴 +ℋ 𝐵))) → ((𝐵 +ℋ (span‘{𝑦})) ∩ (𝐴 ∨ℋ 𝐵)) ⊆ (𝐴 +ℋ 𝐵)) |
| 70 | 69 | sseld 3982 |
. . . . . . . . . . 11
⊢
((∀𝑥 ∈
HAtoms ((𝑥
∨ℋ 𝐵)
∩ (𝐴
∨ℋ 𝐵))
⊆ (((𝑥
∨ℋ 𝐵)
∩ 𝐴)
∨ℋ 𝐵)
∧ (𝑦 ∈ ℋ
∧ ¬ 𝑦 ∈ (𝐴 +ℋ 𝐵))) → (𝑦 ∈ ((𝐵 +ℋ (span‘{𝑦})) ∩ (𝐴 ∨ℋ 𝐵)) → 𝑦 ∈ (𝐴 +ℋ 𝐵))) |
| 71 | 12, 70 | biimtrrid 243 |
. . . . . . . . . 10
⊢
((∀𝑥 ∈
HAtoms ((𝑥
∨ℋ 𝐵)
∩ (𝐴
∨ℋ 𝐵))
⊆ (((𝑥
∨ℋ 𝐵)
∩ 𝐴)
∨ℋ 𝐵)
∧ (𝑦 ∈ ℋ
∧ ¬ 𝑦 ∈ (𝐴 +ℋ 𝐵))) → ((𝑦 ∈ (𝐵 +ℋ (span‘{𝑦})) ∧ 𝑦 ∈ (𝐴 ∨ℋ 𝐵)) → 𝑦 ∈ (𝐴 +ℋ 𝐵))) |
| 72 | 11, 71 | mpand 695 |
. . . . . . . . 9
⊢
((∀𝑥 ∈
HAtoms ((𝑥
∨ℋ 𝐵)
∩ (𝐴
∨ℋ 𝐵))
⊆ (((𝑥
∨ℋ 𝐵)
∩ 𝐴)
∨ℋ 𝐵)
∧ (𝑦 ∈ ℋ
∧ ¬ 𝑦 ∈ (𝐴 +ℋ 𝐵))) → (𝑦 ∈ (𝐴 ∨ℋ 𝐵) → 𝑦 ∈ (𝐴 +ℋ 𝐵))) |
| 73 | 72 | exp32 420 |
. . . . . . . 8
⊢
(∀𝑥 ∈
HAtoms ((𝑥
∨ℋ 𝐵)
∩ (𝐴
∨ℋ 𝐵))
⊆ (((𝑥
∨ℋ 𝐵)
∩ 𝐴)
∨ℋ 𝐵)
→ (𝑦 ∈ ℋ
→ (¬ 𝑦 ∈
(𝐴 +ℋ
𝐵) → (𝑦 ∈ (𝐴 ∨ℋ 𝐵) → 𝑦 ∈ (𝐴 +ℋ 𝐵))))) |
| 74 | 73 | com34 91 |
. . . . . . 7
⊢
(∀𝑥 ∈
HAtoms ((𝑥
∨ℋ 𝐵)
∩ (𝐴
∨ℋ 𝐵))
⊆ (((𝑥
∨ℋ 𝐵)
∩ 𝐴)
∨ℋ 𝐵)
→ (𝑦 ∈ ℋ
→ (𝑦 ∈ (𝐴 ∨ℋ 𝐵) → (¬ 𝑦 ∈ (𝐴 +ℋ 𝐵) → 𝑦 ∈ (𝐴 +ℋ 𝐵))))) |
| 75 | | pm2.18 128 |
. . . . . . 7
⊢ ((¬
𝑦 ∈ (𝐴 +ℋ 𝐵) → 𝑦 ∈ (𝐴 +ℋ 𝐵)) → 𝑦 ∈ (𝐴 +ℋ 𝐵)) |
| 76 | 74, 75 | syl8 76 |
. . . . . 6
⊢
(∀𝑥 ∈
HAtoms ((𝑥
∨ℋ 𝐵)
∩ (𝐴
∨ℋ 𝐵))
⊆ (((𝑥
∨ℋ 𝐵)
∩ 𝐴)
∨ℋ 𝐵)
→ (𝑦 ∈ ℋ
→ (𝑦 ∈ (𝐴 ∨ℋ 𝐵) → 𝑦 ∈ (𝐴 +ℋ 𝐵)))) |
| 77 | 4, 76 | syl5 34 |
. . . . 5
⊢
(∀𝑥 ∈
HAtoms ((𝑥
∨ℋ 𝐵)
∩ (𝐴
∨ℋ 𝐵))
⊆ (((𝑥
∨ℋ 𝐵)
∩ 𝐴)
∨ℋ 𝐵)
→ (𝑦 ∈ (𝐴 ∨ℋ 𝐵) → (𝑦 ∈ (𝐴 ∨ℋ 𝐵) → 𝑦 ∈ (𝐴 +ℋ 𝐵)))) |
| 78 | 77 | pm2.43d 53 |
. . . 4
⊢
(∀𝑥 ∈
HAtoms ((𝑥
∨ℋ 𝐵)
∩ (𝐴
∨ℋ 𝐵))
⊆ (((𝑥
∨ℋ 𝐵)
∩ 𝐴)
∨ℋ 𝐵)
→ (𝑦 ∈ (𝐴 ∨ℋ 𝐵) → 𝑦 ∈ (𝐴 +ℋ 𝐵))) |
| 79 | 78 | ssrdv 3989 |
. . 3
⊢
(∀𝑥 ∈
HAtoms ((𝑥
∨ℋ 𝐵)
∩ (𝐴
∨ℋ 𝐵))
⊆ (((𝑥
∨ℋ 𝐵)
∩ 𝐴)
∨ℋ 𝐵)
→ (𝐴
∨ℋ 𝐵)
⊆ (𝐴
+ℋ 𝐵)) |
| 80 | 1, 2 | chsleji 31477 |
. . 3
⊢ (𝐴 +ℋ 𝐵) ⊆ (𝐴 ∨ℋ 𝐵) |
| 81 | 79, 80 | jctil 519 |
. 2
⊢
(∀𝑥 ∈
HAtoms ((𝑥
∨ℋ 𝐵)
∩ (𝐴
∨ℋ 𝐵))
⊆ (((𝑥
∨ℋ 𝐵)
∩ 𝐴)
∨ℋ 𝐵)
→ ((𝐴
+ℋ 𝐵)
⊆ (𝐴
∨ℋ 𝐵)
∧ (𝐴
∨ℋ 𝐵)
⊆ (𝐴
+ℋ 𝐵))) |
| 82 | | eqss 3999 |
. 2
⊢ ((𝐴 +ℋ 𝐵) = (𝐴 ∨ℋ 𝐵) ↔ ((𝐴 +ℋ 𝐵) ⊆ (𝐴 ∨ℋ 𝐵) ∧ (𝐴 ∨ℋ 𝐵) ⊆ (𝐴 +ℋ 𝐵))) |
| 83 | 81, 82 | sylibr 234 |
1
⊢
(∀𝑥 ∈
HAtoms ((𝑥
∨ℋ 𝐵)
∩ (𝐴
∨ℋ 𝐵))
⊆ (((𝑥
∨ℋ 𝐵)
∩ 𝐴)
∨ℋ 𝐵)
→ (𝐴
+ℋ 𝐵) =
(𝐴 ∨ℋ
𝐵)) |