Proof of Theorem fh1
| Step | Hyp | Ref
| Expression |
| 1 | | chincl 31518 |
. . . . . . . 8
⊢ ((𝐴 ∈
Cℋ ∧ 𝐵 ∈ Cℋ )
→ (𝐴 ∩ 𝐵) ∈
Cℋ ) |
| 2 | | chincl 31518 |
. . . . . . . 8
⊢ ((𝐴 ∈
Cℋ ∧ 𝐶 ∈ Cℋ )
→ (𝐴 ∩ 𝐶) ∈
Cℋ ) |
| 3 | | chjcl 31376 |
. . . . . . . 8
⊢ (((𝐴 ∩ 𝐵) ∈ Cℋ
∧ (𝐴 ∩ 𝐶) ∈
Cℋ ) → ((𝐴 ∩ 𝐵) ∨ℋ (𝐴 ∩ 𝐶)) ∈ Cℋ
) |
| 4 | 1, 2, 3 | syl2an 596 |
. . . . . . 7
⊢ (((𝐴 ∈
Cℋ ∧ 𝐵 ∈ Cℋ )
∧ (𝐴 ∈
Cℋ ∧ 𝐶 ∈ Cℋ ))
→ ((𝐴 ∩ 𝐵) ∨ℋ (𝐴 ∩ 𝐶)) ∈ Cℋ
) |
| 5 | 4 | anandis 678 |
. . . . . 6
⊢ ((𝐴 ∈
Cℋ ∧ (𝐵 ∈ Cℋ
∧ 𝐶 ∈
Cℋ )) → ((𝐴 ∩ 𝐵) ∨ℋ (𝐴 ∩ 𝐶)) ∈ Cℋ
) |
| 6 | | chjcl 31376 |
. . . . . . . 8
⊢ ((𝐵 ∈
Cℋ ∧ 𝐶 ∈ Cℋ )
→ (𝐵
∨ℋ 𝐶)
∈ Cℋ ) |
| 7 | | chincl 31518 |
. . . . . . . 8
⊢ ((𝐴 ∈
Cℋ ∧ (𝐵 ∨ℋ 𝐶) ∈ Cℋ )
→ (𝐴 ∩ (𝐵 ∨ℋ 𝐶)) ∈
Cℋ ) |
| 8 | 6, 7 | sylan2 593 |
. . . . . . 7
⊢ ((𝐴 ∈
Cℋ ∧ (𝐵 ∈ Cℋ
∧ 𝐶 ∈
Cℋ )) → (𝐴 ∩ (𝐵 ∨ℋ 𝐶)) ∈ Cℋ
) |
| 9 | | chsh 31243 |
. . . . . . 7
⊢ ((𝐴 ∩ (𝐵 ∨ℋ 𝐶)) ∈ Cℋ
→ (𝐴 ∩ (𝐵 ∨ℋ 𝐶)) ∈
Sℋ ) |
| 10 | 8, 9 | syl 17 |
. . . . . 6
⊢ ((𝐴 ∈
Cℋ ∧ (𝐵 ∈ Cℋ
∧ 𝐶 ∈
Cℋ )) → (𝐴 ∩ (𝐵 ∨ℋ 𝐶)) ∈ Sℋ
) |
| 11 | 5, 10 | jca 511 |
. . . . 5
⊢ ((𝐴 ∈
Cℋ ∧ (𝐵 ∈ Cℋ
∧ 𝐶 ∈
Cℋ )) → (((𝐴 ∩ 𝐵) ∨ℋ (𝐴 ∩ 𝐶)) ∈ Cℋ
∧ (𝐴 ∩ (𝐵 ∨ℋ 𝐶)) ∈
Sℋ )) |
| 12 | 11 | 3impb 1115 |
. . . 4
⊢ ((𝐴 ∈
Cℋ ∧ 𝐵 ∈ Cℋ
∧ 𝐶 ∈
Cℋ ) → (((𝐴 ∩ 𝐵) ∨ℋ (𝐴 ∩ 𝐶)) ∈ Cℋ
∧ (𝐴 ∩ (𝐵 ∨ℋ 𝐶)) ∈
Sℋ )) |
| 13 | 12 | adantr 480 |
. . 3
⊢ (((𝐴 ∈
Cℋ ∧ 𝐵 ∈ Cℋ
∧ 𝐶 ∈
Cℋ ) ∧ (𝐴 𝐶ℋ 𝐵 ∧ 𝐴 𝐶ℋ 𝐶)) → (((𝐴 ∩ 𝐵) ∨ℋ (𝐴 ∩ 𝐶)) ∈ Cℋ
∧ (𝐴 ∩ (𝐵 ∨ℋ 𝐶)) ∈
Sℋ )) |
| 14 | | ledi 31559 |
. . . 4
⊢ ((𝐴 ∈
Cℋ ∧ 𝐵 ∈ Cℋ
∧ 𝐶 ∈
Cℋ ) → ((𝐴 ∩ 𝐵) ∨ℋ (𝐴 ∩ 𝐶)) ⊆ (𝐴 ∩ (𝐵 ∨ℋ 𝐶))) |
| 15 | 14 | adantr 480 |
. . 3
⊢ (((𝐴 ∈
Cℋ ∧ 𝐵 ∈ Cℋ
∧ 𝐶 ∈
Cℋ ) ∧ (𝐴 𝐶ℋ 𝐵 ∧ 𝐴 𝐶ℋ 𝐶)) → ((𝐴 ∩ 𝐵) ∨ℋ (𝐴 ∩ 𝐶)) ⊆ (𝐴 ∩ (𝐵 ∨ℋ 𝐶))) |
| 16 | | incom 4209 |
. . . . . . . 8
⊢ (𝐴 ∩ (𝐵 ∨ℋ 𝐶)) = ((𝐵 ∨ℋ 𝐶) ∩ 𝐴) |
| 17 | 16 | a1i 11 |
. . . . . . 7
⊢ (((𝐴 ∈
Cℋ ∧ 𝐵 ∈ Cℋ )
∧ (𝐴 ∈
Cℋ ∧ 𝐶 ∈ Cℋ ))
→ (𝐴 ∩ (𝐵 ∨ℋ 𝐶)) = ((𝐵 ∨ℋ 𝐶) ∩ 𝐴)) |
| 18 | | chdmj1 31548 |
. . . . . . . . 9
⊢ (((𝐴 ∩ 𝐵) ∈ Cℋ
∧ (𝐴 ∩ 𝐶) ∈
Cℋ ) → (⊥‘((𝐴 ∩ 𝐵) ∨ℋ (𝐴 ∩ 𝐶))) = ((⊥‘(𝐴 ∩ 𝐵)) ∩ (⊥‘(𝐴 ∩ 𝐶)))) |
| 19 | 1, 2, 18 | syl2an 596 |
. . . . . . . 8
⊢ (((𝐴 ∈
Cℋ ∧ 𝐵 ∈ Cℋ )
∧ (𝐴 ∈
Cℋ ∧ 𝐶 ∈ Cℋ ))
→ (⊥‘((𝐴
∩ 𝐵)
∨ℋ (𝐴
∩ 𝐶))) =
((⊥‘(𝐴 ∩
𝐵)) ∩
(⊥‘(𝐴 ∩
𝐶)))) |
| 20 | | chdmm1 31544 |
. . . . . . . . 9
⊢ ((𝐴 ∈
Cℋ ∧ 𝐵 ∈ Cℋ )
→ (⊥‘(𝐴
∩ 𝐵)) =
((⊥‘𝐴)
∨ℋ (⊥‘𝐵))) |
| 21 | | chdmm1 31544 |
. . . . . . . . 9
⊢ ((𝐴 ∈
Cℋ ∧ 𝐶 ∈ Cℋ )
→ (⊥‘(𝐴
∩ 𝐶)) =
((⊥‘𝐴)
∨ℋ (⊥‘𝐶))) |
| 22 | 20, 21 | ineqan12d 4222 |
. . . . . . . 8
⊢ (((𝐴 ∈
Cℋ ∧ 𝐵 ∈ Cℋ )
∧ (𝐴 ∈
Cℋ ∧ 𝐶 ∈ Cℋ ))
→ ((⊥‘(𝐴
∩ 𝐵)) ∩
(⊥‘(𝐴 ∩
𝐶))) =
(((⊥‘𝐴)
∨ℋ (⊥‘𝐵)) ∩ ((⊥‘𝐴) ∨ℋ
(⊥‘𝐶)))) |
| 23 | 19, 22 | eqtrd 2777 |
. . . . . . 7
⊢ (((𝐴 ∈
Cℋ ∧ 𝐵 ∈ Cℋ )
∧ (𝐴 ∈
Cℋ ∧ 𝐶 ∈ Cℋ ))
→ (⊥‘((𝐴
∩ 𝐵)
∨ℋ (𝐴
∩ 𝐶))) =
(((⊥‘𝐴)
∨ℋ (⊥‘𝐵)) ∩ ((⊥‘𝐴) ∨ℋ
(⊥‘𝐶)))) |
| 24 | 17, 23 | ineq12d 4221 |
. . . . . 6
⊢ (((𝐴 ∈
Cℋ ∧ 𝐵 ∈ Cℋ )
∧ (𝐴 ∈
Cℋ ∧ 𝐶 ∈ Cℋ ))
→ ((𝐴 ∩ (𝐵 ∨ℋ 𝐶)) ∩ (⊥‘((𝐴 ∩ 𝐵) ∨ℋ (𝐴 ∩ 𝐶)))) = (((𝐵 ∨ℋ 𝐶) ∩ 𝐴) ∩ (((⊥‘𝐴) ∨ℋ
(⊥‘𝐵)) ∩
((⊥‘𝐴)
∨ℋ (⊥‘𝐶))))) |
| 25 | 24 | 3impdi 1351 |
. . . . 5
⊢ ((𝐴 ∈
Cℋ ∧ 𝐵 ∈ Cℋ
∧ 𝐶 ∈
Cℋ ) → ((𝐴 ∩ (𝐵 ∨ℋ 𝐶)) ∩ (⊥‘((𝐴 ∩ 𝐵) ∨ℋ (𝐴 ∩ 𝐶)))) = (((𝐵 ∨ℋ 𝐶) ∩ 𝐴) ∩ (((⊥‘𝐴) ∨ℋ
(⊥‘𝐵)) ∩
((⊥‘𝐴)
∨ℋ (⊥‘𝐶))))) |
| 26 | 25 | adantr 480 |
. . . 4
⊢ (((𝐴 ∈
Cℋ ∧ 𝐵 ∈ Cℋ
∧ 𝐶 ∈
Cℋ ) ∧ (𝐴 𝐶ℋ 𝐵 ∧ 𝐴 𝐶ℋ 𝐶)) → ((𝐴 ∩ (𝐵 ∨ℋ 𝐶)) ∩ (⊥‘((𝐴 ∩ 𝐵) ∨ℋ (𝐴 ∩ 𝐶)))) = (((𝐵 ∨ℋ 𝐶) ∩ 𝐴) ∩ (((⊥‘𝐴) ∨ℋ
(⊥‘𝐵)) ∩
((⊥‘𝐴)
∨ℋ (⊥‘𝐶))))) |
| 27 | | inass 4228 |
. . . . . . 7
⊢ (((𝐵 ∨ℋ 𝐶) ∩ 𝐴) ∩ (((⊥‘𝐴) ∨ℋ
(⊥‘𝐵)) ∩
((⊥‘𝐴)
∨ℋ (⊥‘𝐶)))) = ((𝐵 ∨ℋ 𝐶) ∩ (𝐴 ∩ (((⊥‘𝐴) ∨ℋ
(⊥‘𝐵)) ∩
((⊥‘𝐴)
∨ℋ (⊥‘𝐶))))) |
| 28 | | cmcm2 31635 |
. . . . . . . . . . . . . 14
⊢ ((𝐴 ∈
Cℋ ∧ 𝐵 ∈ Cℋ )
→ (𝐴
𝐶ℋ 𝐵 ↔ 𝐴 𝐶ℋ
(⊥‘𝐵))) |
| 29 | | choccl 31325 |
. . . . . . . . . . . . . . 15
⊢ (𝐵 ∈
Cℋ → (⊥‘𝐵) ∈ Cℋ
) |
| 30 | | cmbr3 31627 |
. . . . . . . . . . . . . . 15
⊢ ((𝐴 ∈
Cℋ ∧ (⊥‘𝐵) ∈ Cℋ )
→ (𝐴
𝐶ℋ (⊥‘𝐵) ↔ (𝐴 ∩ ((⊥‘𝐴) ∨ℋ
(⊥‘𝐵))) =
(𝐴 ∩
(⊥‘𝐵)))) |
| 31 | 29, 30 | sylan2 593 |
. . . . . . . . . . . . . 14
⊢ ((𝐴 ∈
Cℋ ∧ 𝐵 ∈ Cℋ )
→ (𝐴
𝐶ℋ (⊥‘𝐵) ↔ (𝐴 ∩ ((⊥‘𝐴) ∨ℋ
(⊥‘𝐵))) =
(𝐴 ∩
(⊥‘𝐵)))) |
| 32 | 28, 31 | bitrd 279 |
. . . . . . . . . . . . 13
⊢ ((𝐴 ∈
Cℋ ∧ 𝐵 ∈ Cℋ )
→ (𝐴
𝐶ℋ 𝐵 ↔ (𝐴 ∩ ((⊥‘𝐴) ∨ℋ
(⊥‘𝐵))) =
(𝐴 ∩
(⊥‘𝐵)))) |
| 33 | 32 | biimpa 476 |
. . . . . . . . . . . 12
⊢ (((𝐴 ∈
Cℋ ∧ 𝐵 ∈ Cℋ )
∧ 𝐴
𝐶ℋ 𝐵) → (𝐴 ∩ ((⊥‘𝐴) ∨ℋ
(⊥‘𝐵))) =
(𝐴 ∩
(⊥‘𝐵))) |
| 34 | 33 | 3adantl3 1169 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈
Cℋ ∧ 𝐵 ∈ Cℋ
∧ 𝐶 ∈
Cℋ ) ∧ 𝐴 𝐶ℋ 𝐵) → (𝐴 ∩ ((⊥‘𝐴) ∨ℋ
(⊥‘𝐵))) =
(𝐴 ∩
(⊥‘𝐵))) |
| 35 | 34 | adantrr 717 |
. . . . . . . . . 10
⊢ (((𝐴 ∈
Cℋ ∧ 𝐵 ∈ Cℋ
∧ 𝐶 ∈
Cℋ ) ∧ (𝐴 𝐶ℋ 𝐵 ∧ 𝐴 𝐶ℋ 𝐶)) → (𝐴 ∩ ((⊥‘𝐴) ∨ℋ
(⊥‘𝐵))) =
(𝐴 ∩
(⊥‘𝐵))) |
| 36 | | cmcm2 31635 |
. . . . . . . . . . . . . 14
⊢ ((𝐴 ∈
Cℋ ∧ 𝐶 ∈ Cℋ )
→ (𝐴
𝐶ℋ 𝐶 ↔ 𝐴 𝐶ℋ
(⊥‘𝐶))) |
| 37 | | choccl 31325 |
. . . . . . . . . . . . . . 15
⊢ (𝐶 ∈
Cℋ → (⊥‘𝐶) ∈ Cℋ
) |
| 38 | | cmbr3 31627 |
. . . . . . . . . . . . . . 15
⊢ ((𝐴 ∈
Cℋ ∧ (⊥‘𝐶) ∈ Cℋ )
→ (𝐴
𝐶ℋ (⊥‘𝐶) ↔ (𝐴 ∩ ((⊥‘𝐴) ∨ℋ
(⊥‘𝐶))) =
(𝐴 ∩
(⊥‘𝐶)))) |
| 39 | 37, 38 | sylan2 593 |
. . . . . . . . . . . . . 14
⊢ ((𝐴 ∈
Cℋ ∧ 𝐶 ∈ Cℋ )
→ (𝐴
𝐶ℋ (⊥‘𝐶) ↔ (𝐴 ∩ ((⊥‘𝐴) ∨ℋ
(⊥‘𝐶))) =
(𝐴 ∩
(⊥‘𝐶)))) |
| 40 | 36, 39 | bitrd 279 |
. . . . . . . . . . . . 13
⊢ ((𝐴 ∈
Cℋ ∧ 𝐶 ∈ Cℋ )
→ (𝐴
𝐶ℋ 𝐶 ↔ (𝐴 ∩ ((⊥‘𝐴) ∨ℋ
(⊥‘𝐶))) =
(𝐴 ∩
(⊥‘𝐶)))) |
| 41 | 40 | biimpa 476 |
. . . . . . . . . . . 12
⊢ (((𝐴 ∈
Cℋ ∧ 𝐶 ∈ Cℋ )
∧ 𝐴
𝐶ℋ 𝐶) → (𝐴 ∩ ((⊥‘𝐴) ∨ℋ
(⊥‘𝐶))) =
(𝐴 ∩
(⊥‘𝐶))) |
| 42 | 41 | 3adantl2 1168 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈
Cℋ ∧ 𝐵 ∈ Cℋ
∧ 𝐶 ∈
Cℋ ) ∧ 𝐴 𝐶ℋ 𝐶) → (𝐴 ∩ ((⊥‘𝐴) ∨ℋ
(⊥‘𝐶))) =
(𝐴 ∩
(⊥‘𝐶))) |
| 43 | 42 | adantrl 716 |
. . . . . . . . . 10
⊢ (((𝐴 ∈
Cℋ ∧ 𝐵 ∈ Cℋ
∧ 𝐶 ∈
Cℋ ) ∧ (𝐴 𝐶ℋ 𝐵 ∧ 𝐴 𝐶ℋ 𝐶)) → (𝐴 ∩ ((⊥‘𝐴) ∨ℋ
(⊥‘𝐶))) =
(𝐴 ∩
(⊥‘𝐶))) |
| 44 | 35, 43 | ineq12d 4221 |
. . . . . . . . 9
⊢ (((𝐴 ∈
Cℋ ∧ 𝐵 ∈ Cℋ
∧ 𝐶 ∈
Cℋ ) ∧ (𝐴 𝐶ℋ 𝐵 ∧ 𝐴 𝐶ℋ 𝐶)) → ((𝐴 ∩ ((⊥‘𝐴) ∨ℋ
(⊥‘𝐵))) ∩
(𝐴 ∩
((⊥‘𝐴)
∨ℋ (⊥‘𝐶)))) = ((𝐴 ∩ (⊥‘𝐵)) ∩ (𝐴 ∩ (⊥‘𝐶)))) |
| 45 | | inindi 4235 |
. . . . . . . . 9
⊢ (𝐴 ∩ (((⊥‘𝐴) ∨ℋ
(⊥‘𝐵)) ∩
((⊥‘𝐴)
∨ℋ (⊥‘𝐶)))) = ((𝐴 ∩ ((⊥‘𝐴) ∨ℋ
(⊥‘𝐵))) ∩
(𝐴 ∩
((⊥‘𝐴)
∨ℋ (⊥‘𝐶)))) |
| 46 | | inindi 4235 |
. . . . . . . . 9
⊢ (𝐴 ∩ ((⊥‘𝐵) ∩ (⊥‘𝐶))) = ((𝐴 ∩ (⊥‘𝐵)) ∩ (𝐴 ∩ (⊥‘𝐶))) |
| 47 | 44, 45, 46 | 3eqtr4g 2802 |
. . . . . . . 8
⊢ (((𝐴 ∈
Cℋ ∧ 𝐵 ∈ Cℋ
∧ 𝐶 ∈
Cℋ ) ∧ (𝐴 𝐶ℋ 𝐵 ∧ 𝐴 𝐶ℋ 𝐶)) → (𝐴 ∩ (((⊥‘𝐴) ∨ℋ
(⊥‘𝐵)) ∩
((⊥‘𝐴)
∨ℋ (⊥‘𝐶)))) = (𝐴 ∩ ((⊥‘𝐵) ∩ (⊥‘𝐶)))) |
| 48 | 47 | ineq2d 4220 |
. . . . . . 7
⊢ (((𝐴 ∈
Cℋ ∧ 𝐵 ∈ Cℋ
∧ 𝐶 ∈
Cℋ ) ∧ (𝐴 𝐶ℋ 𝐵 ∧ 𝐴 𝐶ℋ 𝐶)) → ((𝐵 ∨ℋ 𝐶) ∩ (𝐴 ∩ (((⊥‘𝐴) ∨ℋ
(⊥‘𝐵)) ∩
((⊥‘𝐴)
∨ℋ (⊥‘𝐶))))) = ((𝐵 ∨ℋ 𝐶) ∩ (𝐴 ∩ ((⊥‘𝐵) ∩ (⊥‘𝐶))))) |
| 49 | 27, 48 | eqtrid 2789 |
. . . . . 6
⊢ (((𝐴 ∈
Cℋ ∧ 𝐵 ∈ Cℋ
∧ 𝐶 ∈
Cℋ ) ∧ (𝐴 𝐶ℋ 𝐵 ∧ 𝐴 𝐶ℋ 𝐶)) → (((𝐵 ∨ℋ 𝐶) ∩ 𝐴) ∩ (((⊥‘𝐴) ∨ℋ
(⊥‘𝐵)) ∩
((⊥‘𝐴)
∨ℋ (⊥‘𝐶)))) = ((𝐵 ∨ℋ 𝐶) ∩ (𝐴 ∩ ((⊥‘𝐵) ∩ (⊥‘𝐶))))) |
| 50 | | in12 4229 |
. . . . . 6
⊢ ((𝐵 ∨ℋ 𝐶) ∩ (𝐴 ∩ ((⊥‘𝐵) ∩ (⊥‘𝐶)))) = (𝐴 ∩ ((𝐵 ∨ℋ 𝐶) ∩ ((⊥‘𝐵) ∩ (⊥‘𝐶)))) |
| 51 | 49, 50 | eqtrdi 2793 |
. . . . 5
⊢ (((𝐴 ∈
Cℋ ∧ 𝐵 ∈ Cℋ
∧ 𝐶 ∈
Cℋ ) ∧ (𝐴 𝐶ℋ 𝐵 ∧ 𝐴 𝐶ℋ 𝐶)) → (((𝐵 ∨ℋ 𝐶) ∩ 𝐴) ∩ (((⊥‘𝐴) ∨ℋ
(⊥‘𝐵)) ∩
((⊥‘𝐴)
∨ℋ (⊥‘𝐶)))) = (𝐴 ∩ ((𝐵 ∨ℋ 𝐶) ∩ ((⊥‘𝐵) ∩ (⊥‘𝐶))))) |
| 52 | | chdmj1 31548 |
. . . . . . . . . . 11
⊢ ((𝐵 ∈
Cℋ ∧ 𝐶 ∈ Cℋ )
→ (⊥‘(𝐵
∨ℋ 𝐶))
= ((⊥‘𝐵) ∩
(⊥‘𝐶))) |
| 53 | 52 | ineq2d 4220 |
. . . . . . . . . 10
⊢ ((𝐵 ∈
Cℋ ∧ 𝐶 ∈ Cℋ )
→ ((𝐵
∨ℋ 𝐶)
∩ (⊥‘(𝐵
∨ℋ 𝐶)))
= ((𝐵
∨ℋ 𝐶)
∩ ((⊥‘𝐵)
∩ (⊥‘𝐶)))) |
| 54 | | chocin 31514 |
. . . . . . . . . . 11
⊢ ((𝐵 ∨ℋ 𝐶) ∈
Cℋ → ((𝐵 ∨ℋ 𝐶) ∩ (⊥‘(𝐵 ∨ℋ 𝐶))) = 0ℋ) |
| 55 | 6, 54 | syl 17 |
. . . . . . . . . 10
⊢ ((𝐵 ∈
Cℋ ∧ 𝐶 ∈ Cℋ )
→ ((𝐵
∨ℋ 𝐶)
∩ (⊥‘(𝐵
∨ℋ 𝐶)))
= 0ℋ) |
| 56 | 53, 55 | eqtr3d 2779 |
. . . . . . . . 9
⊢ ((𝐵 ∈
Cℋ ∧ 𝐶 ∈ Cℋ )
→ ((𝐵
∨ℋ 𝐶)
∩ ((⊥‘𝐵)
∩ (⊥‘𝐶))) =
0ℋ) |
| 57 | 56 | ineq2d 4220 |
. . . . . . . 8
⊢ ((𝐵 ∈
Cℋ ∧ 𝐶 ∈ Cℋ )
→ (𝐴 ∩ ((𝐵 ∨ℋ 𝐶) ∩ ((⊥‘𝐵) ∩ (⊥‘𝐶)))) = (𝐴 ∩
0ℋ)) |
| 58 | | chm0 31510 |
. . . . . . . 8
⊢ (𝐴 ∈
Cℋ → (𝐴 ∩ 0ℋ) =
0ℋ) |
| 59 | 57, 58 | sylan9eqr 2799 |
. . . . . . 7
⊢ ((𝐴 ∈
Cℋ ∧ (𝐵 ∈ Cℋ
∧ 𝐶 ∈
Cℋ )) → (𝐴 ∩ ((𝐵 ∨ℋ 𝐶) ∩ ((⊥‘𝐵) ∩ (⊥‘𝐶)))) = 0ℋ) |
| 60 | 59 | 3impb 1115 |
. . . . . 6
⊢ ((𝐴 ∈
Cℋ ∧ 𝐵 ∈ Cℋ
∧ 𝐶 ∈
Cℋ ) → (𝐴 ∩ ((𝐵 ∨ℋ 𝐶) ∩ ((⊥‘𝐵) ∩ (⊥‘𝐶)))) = 0ℋ) |
| 61 | 60 | adantr 480 |
. . . . 5
⊢ (((𝐴 ∈
Cℋ ∧ 𝐵 ∈ Cℋ
∧ 𝐶 ∈
Cℋ ) ∧ (𝐴 𝐶ℋ 𝐵 ∧ 𝐴 𝐶ℋ 𝐶)) → (𝐴 ∩ ((𝐵 ∨ℋ 𝐶) ∩ ((⊥‘𝐵) ∩ (⊥‘𝐶)))) = 0ℋ) |
| 62 | 51, 61 | eqtrd 2777 |
. . . 4
⊢ (((𝐴 ∈
Cℋ ∧ 𝐵 ∈ Cℋ
∧ 𝐶 ∈
Cℋ ) ∧ (𝐴 𝐶ℋ 𝐵 ∧ 𝐴 𝐶ℋ 𝐶)) → (((𝐵 ∨ℋ 𝐶) ∩ 𝐴) ∩ (((⊥‘𝐴) ∨ℋ
(⊥‘𝐵)) ∩
((⊥‘𝐴)
∨ℋ (⊥‘𝐶)))) = 0ℋ) |
| 63 | 26, 62 | eqtrd 2777 |
. . 3
⊢ (((𝐴 ∈
Cℋ ∧ 𝐵 ∈ Cℋ
∧ 𝐶 ∈
Cℋ ) ∧ (𝐴 𝐶ℋ 𝐵 ∧ 𝐴 𝐶ℋ 𝐶)) → ((𝐴 ∩ (𝐵 ∨ℋ 𝐶)) ∩ (⊥‘((𝐴 ∩ 𝐵) ∨ℋ (𝐴 ∩ 𝐶)))) = 0ℋ) |
| 64 | | pjoml 31455 |
. . 3
⊢
(((((𝐴 ∩ 𝐵) ∨ℋ (𝐴 ∩ 𝐶)) ∈ Cℋ
∧ (𝐴 ∩ (𝐵 ∨ℋ 𝐶)) ∈
Sℋ ) ∧ (((𝐴 ∩ 𝐵) ∨ℋ (𝐴 ∩ 𝐶)) ⊆ (𝐴 ∩ (𝐵 ∨ℋ 𝐶)) ∧ ((𝐴 ∩ (𝐵 ∨ℋ 𝐶)) ∩ (⊥‘((𝐴 ∩ 𝐵) ∨ℋ (𝐴 ∩ 𝐶)))) = 0ℋ)) → ((𝐴 ∩ 𝐵) ∨ℋ (𝐴 ∩ 𝐶)) = (𝐴 ∩ (𝐵 ∨ℋ 𝐶))) |
| 65 | 13, 15, 63, 64 | syl12anc 837 |
. 2
⊢ (((𝐴 ∈
Cℋ ∧ 𝐵 ∈ Cℋ
∧ 𝐶 ∈
Cℋ ) ∧ (𝐴 𝐶ℋ 𝐵 ∧ 𝐴 𝐶ℋ 𝐶)) → ((𝐴 ∩ 𝐵) ∨ℋ (𝐴 ∩ 𝐶)) = (𝐴 ∩ (𝐵 ∨ℋ 𝐶))) |
| 66 | 65 | eqcomd 2743 |
1
⊢ (((𝐴 ∈
Cℋ ∧ 𝐵 ∈ Cℋ
∧ 𝐶 ∈
Cℋ ) ∧ (𝐴 𝐶ℋ 𝐵 ∧ 𝐴 𝐶ℋ 𝐶)) → (𝐴 ∩ (𝐵 ∨ℋ 𝐶)) = ((𝐴 ∩ 𝐵) ∨ℋ (𝐴 ∩ 𝐶))) |