Proof of Theorem fh1
Step | Hyp | Ref
| Expression |
1 | | chincl 29857 |
. . . . . . . 8
⊢ ((𝐴 ∈
Cℋ ∧ 𝐵 ∈ Cℋ )
→ (𝐴 ∩ 𝐵) ∈
Cℋ ) |
2 | | chincl 29857 |
. . . . . . . 8
⊢ ((𝐴 ∈
Cℋ ∧ 𝐶 ∈ Cℋ )
→ (𝐴 ∩ 𝐶) ∈
Cℋ ) |
3 | | chjcl 29715 |
. . . . . . . 8
⊢ (((𝐴 ∩ 𝐵) ∈ Cℋ
∧ (𝐴 ∩ 𝐶) ∈
Cℋ ) → ((𝐴 ∩ 𝐵) ∨ℋ (𝐴 ∩ 𝐶)) ∈ Cℋ
) |
4 | 1, 2, 3 | syl2an 596 |
. . . . . . 7
⊢ (((𝐴 ∈
Cℋ ∧ 𝐵 ∈ Cℋ )
∧ (𝐴 ∈
Cℋ ∧ 𝐶 ∈ Cℋ ))
→ ((𝐴 ∩ 𝐵) ∨ℋ (𝐴 ∩ 𝐶)) ∈ Cℋ
) |
5 | 4 | anandis 675 |
. . . . . 6
⊢ ((𝐴 ∈
Cℋ ∧ (𝐵 ∈ Cℋ
∧ 𝐶 ∈
Cℋ )) → ((𝐴 ∩ 𝐵) ∨ℋ (𝐴 ∩ 𝐶)) ∈ Cℋ
) |
6 | | chjcl 29715 |
. . . . . . . 8
⊢ ((𝐵 ∈
Cℋ ∧ 𝐶 ∈ Cℋ )
→ (𝐵
∨ℋ 𝐶)
∈ Cℋ ) |
7 | | chincl 29857 |
. . . . . . . 8
⊢ ((𝐴 ∈
Cℋ ∧ (𝐵 ∨ℋ 𝐶) ∈ Cℋ )
→ (𝐴 ∩ (𝐵 ∨ℋ 𝐶)) ∈
Cℋ ) |
8 | 6, 7 | sylan2 593 |
. . . . . . 7
⊢ ((𝐴 ∈
Cℋ ∧ (𝐵 ∈ Cℋ
∧ 𝐶 ∈
Cℋ )) → (𝐴 ∩ (𝐵 ∨ℋ 𝐶)) ∈ Cℋ
) |
9 | | chsh 29582 |
. . . . . . 7
⊢ ((𝐴 ∩ (𝐵 ∨ℋ 𝐶)) ∈ Cℋ
→ (𝐴 ∩ (𝐵 ∨ℋ 𝐶)) ∈
Sℋ ) |
10 | 8, 9 | syl 17 |
. . . . . 6
⊢ ((𝐴 ∈
Cℋ ∧ (𝐵 ∈ Cℋ
∧ 𝐶 ∈
Cℋ )) → (𝐴 ∩ (𝐵 ∨ℋ 𝐶)) ∈ Sℋ
) |
11 | 5, 10 | jca 512 |
. . . . 5
⊢ ((𝐴 ∈
Cℋ ∧ (𝐵 ∈ Cℋ
∧ 𝐶 ∈
Cℋ )) → (((𝐴 ∩ 𝐵) ∨ℋ (𝐴 ∩ 𝐶)) ∈ Cℋ
∧ (𝐴 ∩ (𝐵 ∨ℋ 𝐶)) ∈
Sℋ )) |
12 | 11 | 3impb 1114 |
. . . 4
⊢ ((𝐴 ∈
Cℋ ∧ 𝐵 ∈ Cℋ
∧ 𝐶 ∈
Cℋ ) → (((𝐴 ∩ 𝐵) ∨ℋ (𝐴 ∩ 𝐶)) ∈ Cℋ
∧ (𝐴 ∩ (𝐵 ∨ℋ 𝐶)) ∈
Sℋ )) |
13 | 12 | adantr 481 |
. . 3
⊢ (((𝐴 ∈
Cℋ ∧ 𝐵 ∈ Cℋ
∧ 𝐶 ∈
Cℋ ) ∧ (𝐴 𝐶ℋ 𝐵 ∧ 𝐴 𝐶ℋ 𝐶)) → (((𝐴 ∩ 𝐵) ∨ℋ (𝐴 ∩ 𝐶)) ∈ Cℋ
∧ (𝐴 ∩ (𝐵 ∨ℋ 𝐶)) ∈
Sℋ )) |
14 | | ledi 29898 |
. . . 4
⊢ ((𝐴 ∈
Cℋ ∧ 𝐵 ∈ Cℋ
∧ 𝐶 ∈
Cℋ ) → ((𝐴 ∩ 𝐵) ∨ℋ (𝐴 ∩ 𝐶)) ⊆ (𝐴 ∩ (𝐵 ∨ℋ 𝐶))) |
15 | 14 | adantr 481 |
. . 3
⊢ (((𝐴 ∈
Cℋ ∧ 𝐵 ∈ Cℋ
∧ 𝐶 ∈
Cℋ ) ∧ (𝐴 𝐶ℋ 𝐵 ∧ 𝐴 𝐶ℋ 𝐶)) → ((𝐴 ∩ 𝐵) ∨ℋ (𝐴 ∩ 𝐶)) ⊆ (𝐴 ∩ (𝐵 ∨ℋ 𝐶))) |
16 | | incom 4140 |
. . . . . . . 8
⊢ (𝐴 ∩ (𝐵 ∨ℋ 𝐶)) = ((𝐵 ∨ℋ 𝐶) ∩ 𝐴) |
17 | 16 | a1i 11 |
. . . . . . 7
⊢ (((𝐴 ∈
Cℋ ∧ 𝐵 ∈ Cℋ )
∧ (𝐴 ∈
Cℋ ∧ 𝐶 ∈ Cℋ ))
→ (𝐴 ∩ (𝐵 ∨ℋ 𝐶)) = ((𝐵 ∨ℋ 𝐶) ∩ 𝐴)) |
18 | | chdmj1 29887 |
. . . . . . . . 9
⊢ (((𝐴 ∩ 𝐵) ∈ Cℋ
∧ (𝐴 ∩ 𝐶) ∈
Cℋ ) → (⊥‘((𝐴 ∩ 𝐵) ∨ℋ (𝐴 ∩ 𝐶))) = ((⊥‘(𝐴 ∩ 𝐵)) ∩ (⊥‘(𝐴 ∩ 𝐶)))) |
19 | 1, 2, 18 | syl2an 596 |
. . . . . . . 8
⊢ (((𝐴 ∈
Cℋ ∧ 𝐵 ∈ Cℋ )
∧ (𝐴 ∈
Cℋ ∧ 𝐶 ∈ Cℋ ))
→ (⊥‘((𝐴
∩ 𝐵)
∨ℋ (𝐴
∩ 𝐶))) =
((⊥‘(𝐴 ∩
𝐵)) ∩
(⊥‘(𝐴 ∩
𝐶)))) |
20 | | chdmm1 29883 |
. . . . . . . . 9
⊢ ((𝐴 ∈
Cℋ ∧ 𝐵 ∈ Cℋ )
→ (⊥‘(𝐴
∩ 𝐵)) =
((⊥‘𝐴)
∨ℋ (⊥‘𝐵))) |
21 | | chdmm1 29883 |
. . . . . . . . 9
⊢ ((𝐴 ∈
Cℋ ∧ 𝐶 ∈ Cℋ )
→ (⊥‘(𝐴
∩ 𝐶)) =
((⊥‘𝐴)
∨ℋ (⊥‘𝐶))) |
22 | 20, 21 | ineqan12d 4154 |
. . . . . . . 8
⊢ (((𝐴 ∈
Cℋ ∧ 𝐵 ∈ Cℋ )
∧ (𝐴 ∈
Cℋ ∧ 𝐶 ∈ Cℋ ))
→ ((⊥‘(𝐴
∩ 𝐵)) ∩
(⊥‘(𝐴 ∩
𝐶))) =
(((⊥‘𝐴)
∨ℋ (⊥‘𝐵)) ∩ ((⊥‘𝐴) ∨ℋ
(⊥‘𝐶)))) |
23 | 19, 22 | eqtrd 2780 |
. . . . . . 7
⊢ (((𝐴 ∈
Cℋ ∧ 𝐵 ∈ Cℋ )
∧ (𝐴 ∈
Cℋ ∧ 𝐶 ∈ Cℋ ))
→ (⊥‘((𝐴
∩ 𝐵)
∨ℋ (𝐴
∩ 𝐶))) =
(((⊥‘𝐴)
∨ℋ (⊥‘𝐵)) ∩ ((⊥‘𝐴) ∨ℋ
(⊥‘𝐶)))) |
24 | 17, 23 | ineq12d 4153 |
. . . . . 6
⊢ (((𝐴 ∈
Cℋ ∧ 𝐵 ∈ Cℋ )
∧ (𝐴 ∈
Cℋ ∧ 𝐶 ∈ Cℋ ))
→ ((𝐴 ∩ (𝐵 ∨ℋ 𝐶)) ∩ (⊥‘((𝐴 ∩ 𝐵) ∨ℋ (𝐴 ∩ 𝐶)))) = (((𝐵 ∨ℋ 𝐶) ∩ 𝐴) ∩ (((⊥‘𝐴) ∨ℋ
(⊥‘𝐵)) ∩
((⊥‘𝐴)
∨ℋ (⊥‘𝐶))))) |
25 | 24 | 3impdi 1349 |
. . . . 5
⊢ ((𝐴 ∈
Cℋ ∧ 𝐵 ∈ Cℋ
∧ 𝐶 ∈
Cℋ ) → ((𝐴 ∩ (𝐵 ∨ℋ 𝐶)) ∩ (⊥‘((𝐴 ∩ 𝐵) ∨ℋ (𝐴 ∩ 𝐶)))) = (((𝐵 ∨ℋ 𝐶) ∩ 𝐴) ∩ (((⊥‘𝐴) ∨ℋ
(⊥‘𝐵)) ∩
((⊥‘𝐴)
∨ℋ (⊥‘𝐶))))) |
26 | 25 | adantr 481 |
. . . 4
⊢ (((𝐴 ∈
Cℋ ∧ 𝐵 ∈ Cℋ
∧ 𝐶 ∈
Cℋ ) ∧ (𝐴 𝐶ℋ 𝐵 ∧ 𝐴 𝐶ℋ 𝐶)) → ((𝐴 ∩ (𝐵 ∨ℋ 𝐶)) ∩ (⊥‘((𝐴 ∩ 𝐵) ∨ℋ (𝐴 ∩ 𝐶)))) = (((𝐵 ∨ℋ 𝐶) ∩ 𝐴) ∩ (((⊥‘𝐴) ∨ℋ
(⊥‘𝐵)) ∩
((⊥‘𝐴)
∨ℋ (⊥‘𝐶))))) |
27 | | inass 4159 |
. . . . . . 7
⊢ (((𝐵 ∨ℋ 𝐶) ∩ 𝐴) ∩ (((⊥‘𝐴) ∨ℋ
(⊥‘𝐵)) ∩
((⊥‘𝐴)
∨ℋ (⊥‘𝐶)))) = ((𝐵 ∨ℋ 𝐶) ∩ (𝐴 ∩ (((⊥‘𝐴) ∨ℋ
(⊥‘𝐵)) ∩
((⊥‘𝐴)
∨ℋ (⊥‘𝐶))))) |
28 | | cmcm2 29974 |
. . . . . . . . . . . . . 14
⊢ ((𝐴 ∈
Cℋ ∧ 𝐵 ∈ Cℋ )
→ (𝐴
𝐶ℋ 𝐵 ↔ 𝐴 𝐶ℋ
(⊥‘𝐵))) |
29 | | choccl 29664 |
. . . . . . . . . . . . . . 15
⊢ (𝐵 ∈
Cℋ → (⊥‘𝐵) ∈ Cℋ
) |
30 | | cmbr3 29966 |
. . . . . . . . . . . . . . 15
⊢ ((𝐴 ∈
Cℋ ∧ (⊥‘𝐵) ∈ Cℋ )
→ (𝐴
𝐶ℋ (⊥‘𝐵) ↔ (𝐴 ∩ ((⊥‘𝐴) ∨ℋ
(⊥‘𝐵))) =
(𝐴 ∩
(⊥‘𝐵)))) |
31 | 29, 30 | sylan2 593 |
. . . . . . . . . . . . . 14
⊢ ((𝐴 ∈
Cℋ ∧ 𝐵 ∈ Cℋ )
→ (𝐴
𝐶ℋ (⊥‘𝐵) ↔ (𝐴 ∩ ((⊥‘𝐴) ∨ℋ
(⊥‘𝐵))) =
(𝐴 ∩
(⊥‘𝐵)))) |
32 | 28, 31 | bitrd 278 |
. . . . . . . . . . . . 13
⊢ ((𝐴 ∈
Cℋ ∧ 𝐵 ∈ Cℋ )
→ (𝐴
𝐶ℋ 𝐵 ↔ (𝐴 ∩ ((⊥‘𝐴) ∨ℋ
(⊥‘𝐵))) =
(𝐴 ∩
(⊥‘𝐵)))) |
33 | 32 | biimpa 477 |
. . . . . . . . . . . 12
⊢ (((𝐴 ∈
Cℋ ∧ 𝐵 ∈ Cℋ )
∧ 𝐴
𝐶ℋ 𝐵) → (𝐴 ∩ ((⊥‘𝐴) ∨ℋ
(⊥‘𝐵))) =
(𝐴 ∩
(⊥‘𝐵))) |
34 | 33 | 3adantl3 1167 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈
Cℋ ∧ 𝐵 ∈ Cℋ
∧ 𝐶 ∈
Cℋ ) ∧ 𝐴 𝐶ℋ 𝐵) → (𝐴 ∩ ((⊥‘𝐴) ∨ℋ
(⊥‘𝐵))) =
(𝐴 ∩
(⊥‘𝐵))) |
35 | 34 | adantrr 714 |
. . . . . . . . . 10
⊢ (((𝐴 ∈
Cℋ ∧ 𝐵 ∈ Cℋ
∧ 𝐶 ∈
Cℋ ) ∧ (𝐴 𝐶ℋ 𝐵 ∧ 𝐴 𝐶ℋ 𝐶)) → (𝐴 ∩ ((⊥‘𝐴) ∨ℋ
(⊥‘𝐵))) =
(𝐴 ∩
(⊥‘𝐵))) |
36 | | cmcm2 29974 |
. . . . . . . . . . . . . 14
⊢ ((𝐴 ∈
Cℋ ∧ 𝐶 ∈ Cℋ )
→ (𝐴
𝐶ℋ 𝐶 ↔ 𝐴 𝐶ℋ
(⊥‘𝐶))) |
37 | | choccl 29664 |
. . . . . . . . . . . . . . 15
⊢ (𝐶 ∈
Cℋ → (⊥‘𝐶) ∈ Cℋ
) |
38 | | cmbr3 29966 |
. . . . . . . . . . . . . . 15
⊢ ((𝐴 ∈
Cℋ ∧ (⊥‘𝐶) ∈ Cℋ )
→ (𝐴
𝐶ℋ (⊥‘𝐶) ↔ (𝐴 ∩ ((⊥‘𝐴) ∨ℋ
(⊥‘𝐶))) =
(𝐴 ∩
(⊥‘𝐶)))) |
39 | 37, 38 | sylan2 593 |
. . . . . . . . . . . . . 14
⊢ ((𝐴 ∈
Cℋ ∧ 𝐶 ∈ Cℋ )
→ (𝐴
𝐶ℋ (⊥‘𝐶) ↔ (𝐴 ∩ ((⊥‘𝐴) ∨ℋ
(⊥‘𝐶))) =
(𝐴 ∩
(⊥‘𝐶)))) |
40 | 36, 39 | bitrd 278 |
. . . . . . . . . . . . 13
⊢ ((𝐴 ∈
Cℋ ∧ 𝐶 ∈ Cℋ )
→ (𝐴
𝐶ℋ 𝐶 ↔ (𝐴 ∩ ((⊥‘𝐴) ∨ℋ
(⊥‘𝐶))) =
(𝐴 ∩
(⊥‘𝐶)))) |
41 | 40 | biimpa 477 |
. . . . . . . . . . . 12
⊢ (((𝐴 ∈
Cℋ ∧ 𝐶 ∈ Cℋ )
∧ 𝐴
𝐶ℋ 𝐶) → (𝐴 ∩ ((⊥‘𝐴) ∨ℋ
(⊥‘𝐶))) =
(𝐴 ∩
(⊥‘𝐶))) |
42 | 41 | 3adantl2 1166 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈
Cℋ ∧ 𝐵 ∈ Cℋ
∧ 𝐶 ∈
Cℋ ) ∧ 𝐴 𝐶ℋ 𝐶) → (𝐴 ∩ ((⊥‘𝐴) ∨ℋ
(⊥‘𝐶))) =
(𝐴 ∩
(⊥‘𝐶))) |
43 | 42 | adantrl 713 |
. . . . . . . . . 10
⊢ (((𝐴 ∈
Cℋ ∧ 𝐵 ∈ Cℋ
∧ 𝐶 ∈
Cℋ ) ∧ (𝐴 𝐶ℋ 𝐵 ∧ 𝐴 𝐶ℋ 𝐶)) → (𝐴 ∩ ((⊥‘𝐴) ∨ℋ
(⊥‘𝐶))) =
(𝐴 ∩
(⊥‘𝐶))) |
44 | 35, 43 | ineq12d 4153 |
. . . . . . . . 9
⊢ (((𝐴 ∈
Cℋ ∧ 𝐵 ∈ Cℋ
∧ 𝐶 ∈
Cℋ ) ∧ (𝐴 𝐶ℋ 𝐵 ∧ 𝐴 𝐶ℋ 𝐶)) → ((𝐴 ∩ ((⊥‘𝐴) ∨ℋ
(⊥‘𝐵))) ∩
(𝐴 ∩
((⊥‘𝐴)
∨ℋ (⊥‘𝐶)))) = ((𝐴 ∩ (⊥‘𝐵)) ∩ (𝐴 ∩ (⊥‘𝐶)))) |
45 | | inindi 4166 |
. . . . . . . . 9
⊢ (𝐴 ∩ (((⊥‘𝐴) ∨ℋ
(⊥‘𝐵)) ∩
((⊥‘𝐴)
∨ℋ (⊥‘𝐶)))) = ((𝐴 ∩ ((⊥‘𝐴) ∨ℋ
(⊥‘𝐵))) ∩
(𝐴 ∩
((⊥‘𝐴)
∨ℋ (⊥‘𝐶)))) |
46 | | inindi 4166 |
. . . . . . . . 9
⊢ (𝐴 ∩ ((⊥‘𝐵) ∩ (⊥‘𝐶))) = ((𝐴 ∩ (⊥‘𝐵)) ∩ (𝐴 ∩ (⊥‘𝐶))) |
47 | 44, 45, 46 | 3eqtr4g 2805 |
. . . . . . . 8
⊢ (((𝐴 ∈
Cℋ ∧ 𝐵 ∈ Cℋ
∧ 𝐶 ∈
Cℋ ) ∧ (𝐴 𝐶ℋ 𝐵 ∧ 𝐴 𝐶ℋ 𝐶)) → (𝐴 ∩ (((⊥‘𝐴) ∨ℋ
(⊥‘𝐵)) ∩
((⊥‘𝐴)
∨ℋ (⊥‘𝐶)))) = (𝐴 ∩ ((⊥‘𝐵) ∩ (⊥‘𝐶)))) |
48 | 47 | ineq2d 4152 |
. . . . . . 7
⊢ (((𝐴 ∈
Cℋ ∧ 𝐵 ∈ Cℋ
∧ 𝐶 ∈
Cℋ ) ∧ (𝐴 𝐶ℋ 𝐵 ∧ 𝐴 𝐶ℋ 𝐶)) → ((𝐵 ∨ℋ 𝐶) ∩ (𝐴 ∩ (((⊥‘𝐴) ∨ℋ
(⊥‘𝐵)) ∩
((⊥‘𝐴)
∨ℋ (⊥‘𝐶))))) = ((𝐵 ∨ℋ 𝐶) ∩ (𝐴 ∩ ((⊥‘𝐵) ∩ (⊥‘𝐶))))) |
49 | 27, 48 | eqtrid 2792 |
. . . . . 6
⊢ (((𝐴 ∈
Cℋ ∧ 𝐵 ∈ Cℋ
∧ 𝐶 ∈
Cℋ ) ∧ (𝐴 𝐶ℋ 𝐵 ∧ 𝐴 𝐶ℋ 𝐶)) → (((𝐵 ∨ℋ 𝐶) ∩ 𝐴) ∩ (((⊥‘𝐴) ∨ℋ
(⊥‘𝐵)) ∩
((⊥‘𝐴)
∨ℋ (⊥‘𝐶)))) = ((𝐵 ∨ℋ 𝐶) ∩ (𝐴 ∩ ((⊥‘𝐵) ∩ (⊥‘𝐶))))) |
50 | | in12 4160 |
. . . . . 6
⊢ ((𝐵 ∨ℋ 𝐶) ∩ (𝐴 ∩ ((⊥‘𝐵) ∩ (⊥‘𝐶)))) = (𝐴 ∩ ((𝐵 ∨ℋ 𝐶) ∩ ((⊥‘𝐵) ∩ (⊥‘𝐶)))) |
51 | 49, 50 | eqtrdi 2796 |
. . . . 5
⊢ (((𝐴 ∈
Cℋ ∧ 𝐵 ∈ Cℋ
∧ 𝐶 ∈
Cℋ ) ∧ (𝐴 𝐶ℋ 𝐵 ∧ 𝐴 𝐶ℋ 𝐶)) → (((𝐵 ∨ℋ 𝐶) ∩ 𝐴) ∩ (((⊥‘𝐴) ∨ℋ
(⊥‘𝐵)) ∩
((⊥‘𝐴)
∨ℋ (⊥‘𝐶)))) = (𝐴 ∩ ((𝐵 ∨ℋ 𝐶) ∩ ((⊥‘𝐵) ∩ (⊥‘𝐶))))) |
52 | | chdmj1 29887 |
. . . . . . . . . . 11
⊢ ((𝐵 ∈
Cℋ ∧ 𝐶 ∈ Cℋ )
→ (⊥‘(𝐵
∨ℋ 𝐶))
= ((⊥‘𝐵) ∩
(⊥‘𝐶))) |
53 | 52 | ineq2d 4152 |
. . . . . . . . . 10
⊢ ((𝐵 ∈
Cℋ ∧ 𝐶 ∈ Cℋ )
→ ((𝐵
∨ℋ 𝐶)
∩ (⊥‘(𝐵
∨ℋ 𝐶)))
= ((𝐵
∨ℋ 𝐶)
∩ ((⊥‘𝐵)
∩ (⊥‘𝐶)))) |
54 | | chocin 29853 |
. . . . . . . . . . 11
⊢ ((𝐵 ∨ℋ 𝐶) ∈
Cℋ → ((𝐵 ∨ℋ 𝐶) ∩ (⊥‘(𝐵 ∨ℋ 𝐶))) = 0ℋ) |
55 | 6, 54 | syl 17 |
. . . . . . . . . 10
⊢ ((𝐵 ∈
Cℋ ∧ 𝐶 ∈ Cℋ )
→ ((𝐵
∨ℋ 𝐶)
∩ (⊥‘(𝐵
∨ℋ 𝐶)))
= 0ℋ) |
56 | 53, 55 | eqtr3d 2782 |
. . . . . . . . 9
⊢ ((𝐵 ∈
Cℋ ∧ 𝐶 ∈ Cℋ )
→ ((𝐵
∨ℋ 𝐶)
∩ ((⊥‘𝐵)
∩ (⊥‘𝐶))) =
0ℋ) |
57 | 56 | ineq2d 4152 |
. . . . . . . 8
⊢ ((𝐵 ∈
Cℋ ∧ 𝐶 ∈ Cℋ )
→ (𝐴 ∩ ((𝐵 ∨ℋ 𝐶) ∩ ((⊥‘𝐵) ∩ (⊥‘𝐶)))) = (𝐴 ∩
0ℋ)) |
58 | | chm0 29849 |
. . . . . . . 8
⊢ (𝐴 ∈
Cℋ → (𝐴 ∩ 0ℋ) =
0ℋ) |
59 | 57, 58 | sylan9eqr 2802 |
. . . . . . 7
⊢ ((𝐴 ∈
Cℋ ∧ (𝐵 ∈ Cℋ
∧ 𝐶 ∈
Cℋ )) → (𝐴 ∩ ((𝐵 ∨ℋ 𝐶) ∩ ((⊥‘𝐵) ∩ (⊥‘𝐶)))) = 0ℋ) |
60 | 59 | 3impb 1114 |
. . . . . 6
⊢ ((𝐴 ∈
Cℋ ∧ 𝐵 ∈ Cℋ
∧ 𝐶 ∈
Cℋ ) → (𝐴 ∩ ((𝐵 ∨ℋ 𝐶) ∩ ((⊥‘𝐵) ∩ (⊥‘𝐶)))) = 0ℋ) |
61 | 60 | adantr 481 |
. . . . 5
⊢ (((𝐴 ∈
Cℋ ∧ 𝐵 ∈ Cℋ
∧ 𝐶 ∈
Cℋ ) ∧ (𝐴 𝐶ℋ 𝐵 ∧ 𝐴 𝐶ℋ 𝐶)) → (𝐴 ∩ ((𝐵 ∨ℋ 𝐶) ∩ ((⊥‘𝐵) ∩ (⊥‘𝐶)))) = 0ℋ) |
62 | 51, 61 | eqtrd 2780 |
. . . 4
⊢ (((𝐴 ∈
Cℋ ∧ 𝐵 ∈ Cℋ
∧ 𝐶 ∈
Cℋ ) ∧ (𝐴 𝐶ℋ 𝐵 ∧ 𝐴 𝐶ℋ 𝐶)) → (((𝐵 ∨ℋ 𝐶) ∩ 𝐴) ∩ (((⊥‘𝐴) ∨ℋ
(⊥‘𝐵)) ∩
((⊥‘𝐴)
∨ℋ (⊥‘𝐶)))) = 0ℋ) |
63 | 26, 62 | eqtrd 2780 |
. . 3
⊢ (((𝐴 ∈
Cℋ ∧ 𝐵 ∈ Cℋ
∧ 𝐶 ∈
Cℋ ) ∧ (𝐴 𝐶ℋ 𝐵 ∧ 𝐴 𝐶ℋ 𝐶)) → ((𝐴 ∩ (𝐵 ∨ℋ 𝐶)) ∩ (⊥‘((𝐴 ∩ 𝐵) ∨ℋ (𝐴 ∩ 𝐶)))) = 0ℋ) |
64 | | pjoml 29794 |
. . 3
⊢
(((((𝐴 ∩ 𝐵) ∨ℋ (𝐴 ∩ 𝐶)) ∈ Cℋ
∧ (𝐴 ∩ (𝐵 ∨ℋ 𝐶)) ∈
Sℋ ) ∧ (((𝐴 ∩ 𝐵) ∨ℋ (𝐴 ∩ 𝐶)) ⊆ (𝐴 ∩ (𝐵 ∨ℋ 𝐶)) ∧ ((𝐴 ∩ (𝐵 ∨ℋ 𝐶)) ∩ (⊥‘((𝐴 ∩ 𝐵) ∨ℋ (𝐴 ∩ 𝐶)))) = 0ℋ)) → ((𝐴 ∩ 𝐵) ∨ℋ (𝐴 ∩ 𝐶)) = (𝐴 ∩ (𝐵 ∨ℋ 𝐶))) |
65 | 13, 15, 63, 64 | syl12anc 834 |
. 2
⊢ (((𝐴 ∈
Cℋ ∧ 𝐵 ∈ Cℋ
∧ 𝐶 ∈
Cℋ ) ∧ (𝐴 𝐶ℋ 𝐵 ∧ 𝐴 𝐶ℋ 𝐶)) → ((𝐴 ∩ 𝐵) ∨ℋ (𝐴 ∩ 𝐶)) = (𝐴 ∩ (𝐵 ∨ℋ 𝐶))) |
66 | 65 | eqcomd 2746 |
1
⊢ (((𝐴 ∈
Cℋ ∧ 𝐵 ∈ Cℋ
∧ 𝐶 ∈
Cℋ ) ∧ (𝐴 𝐶ℋ 𝐵 ∧ 𝐴 𝐶ℋ 𝐶)) → (𝐴 ∩ (𝐵 ∨ℋ 𝐶)) = ((𝐴 ∩ 𝐵) ∨ℋ (𝐴 ∩ 𝐶))) |