Proof of Theorem fh2
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 | | chdmj1 29887 |
. . . . . . . . . . 11
⊢ (((𝐴 ∩ 𝐵) ∈ Cℋ
∧ (𝐴 ∩ 𝐶) ∈
Cℋ ) → (⊥‘((𝐴 ∩ 𝐵) ∨ℋ (𝐴 ∩ 𝐶))) = ((⊥‘(𝐴 ∩ 𝐵)) ∩ (⊥‘(𝐴 ∩ 𝐶)))) |
17 | 1, 2, 16 | syl2an 596 |
. . . . . . . . . 10
⊢ (((𝐴 ∈
Cℋ ∧ 𝐵 ∈ Cℋ )
∧ (𝐴 ∈
Cℋ ∧ 𝐶 ∈ Cℋ ))
→ (⊥‘((𝐴
∩ 𝐵)
∨ℋ (𝐴
∩ 𝐶))) =
((⊥‘(𝐴 ∩
𝐵)) ∩
(⊥‘(𝐴 ∩
𝐶)))) |
18 | | chdmm1 29883 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈
Cℋ ∧ 𝐵 ∈ Cℋ )
→ (⊥‘(𝐴
∩ 𝐵)) =
((⊥‘𝐴)
∨ℋ (⊥‘𝐵))) |
19 | 18 | adantr 481 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈
Cℋ ∧ 𝐵 ∈ Cℋ )
∧ (𝐴 ∈
Cℋ ∧ 𝐶 ∈ Cℋ ))
→ (⊥‘(𝐴
∩ 𝐵)) =
((⊥‘𝐴)
∨ℋ (⊥‘𝐵))) |
20 | 19 | ineq1d 4151 |
. . . . . . . . . 10
⊢ (((𝐴 ∈
Cℋ ∧ 𝐵 ∈ Cℋ )
∧ (𝐴 ∈
Cℋ ∧ 𝐶 ∈ Cℋ ))
→ ((⊥‘(𝐴
∩ 𝐵)) ∩
(⊥‘(𝐴 ∩
𝐶))) =
(((⊥‘𝐴)
∨ℋ (⊥‘𝐵)) ∩ (⊥‘(𝐴 ∩ 𝐶)))) |
21 | 17, 20 | eqtrd 2780 |
. . . . . . . . 9
⊢ (((𝐴 ∈
Cℋ ∧ 𝐵 ∈ Cℋ )
∧ (𝐴 ∈
Cℋ ∧ 𝐶 ∈ Cℋ ))
→ (⊥‘((𝐴
∩ 𝐵)
∨ℋ (𝐴
∩ 𝐶))) =
(((⊥‘𝐴)
∨ℋ (⊥‘𝐵)) ∩ (⊥‘(𝐴 ∩ 𝐶)))) |
22 | 21 | 3impdi 1349 |
. . . . . . . 8
⊢ ((𝐴 ∈
Cℋ ∧ 𝐵 ∈ Cℋ
∧ 𝐶 ∈
Cℋ ) → (⊥‘((𝐴 ∩ 𝐵) ∨ℋ (𝐴 ∩ 𝐶))) = (((⊥‘𝐴) ∨ℋ
(⊥‘𝐵)) ∩
(⊥‘(𝐴 ∩
𝐶)))) |
23 | 22 | ineq2d 4152 |
. . . . . . 7
⊢ ((𝐴 ∈
Cℋ ∧ 𝐵 ∈ Cℋ
∧ 𝐶 ∈
Cℋ ) → ((𝐴 ∩ (𝐵 ∨ℋ 𝐶)) ∩ (⊥‘((𝐴 ∩ 𝐵) ∨ℋ (𝐴 ∩ 𝐶)))) = ((𝐴 ∩ (𝐵 ∨ℋ 𝐶)) ∩ (((⊥‘𝐴) ∨ℋ
(⊥‘𝐵)) ∩
(⊥‘(𝐴 ∩
𝐶))))) |
24 | 23 | adantr 481 |
. . . . . 6
⊢ (((𝐴 ∈
Cℋ ∧ 𝐵 ∈ Cℋ
∧ 𝐶 ∈
Cℋ ) ∧ (𝐵 𝐶ℋ 𝐴 ∧ 𝐵 𝐶ℋ 𝐶)) → ((𝐴 ∩ (𝐵 ∨ℋ 𝐶)) ∩ (⊥‘((𝐴 ∩ 𝐵) ∨ℋ (𝐴 ∩ 𝐶)))) = ((𝐴 ∩ (𝐵 ∨ℋ 𝐶)) ∩ (((⊥‘𝐴) ∨ℋ
(⊥‘𝐵)) ∩
(⊥‘(𝐴 ∩
𝐶))))) |
25 | | in4 4165 |
. . . . . . 7
⊢ ((𝐴 ∩ (𝐵 ∨ℋ 𝐶)) ∩ (((⊥‘𝐴) ∨ℋ
(⊥‘𝐵)) ∩
(⊥‘(𝐴 ∩
𝐶)))) = ((𝐴 ∩ ((⊥‘𝐴) ∨ℋ
(⊥‘𝐵))) ∩
((𝐵 ∨ℋ
𝐶) ∩
(⊥‘(𝐴 ∩
𝐶)))) |
26 | | cmcm2 29974 |
. . . . . . . . . . . . 13
⊢ ((𝐴 ∈
Cℋ ∧ 𝐵 ∈ Cℋ )
→ (𝐴
𝐶ℋ 𝐵 ↔ 𝐴 𝐶ℋ
(⊥‘𝐵))) |
27 | | cmcm 29972 |
. . . . . . . . . . . . 13
⊢ ((𝐴 ∈
Cℋ ∧ 𝐵 ∈ Cℋ )
→ (𝐴
𝐶ℋ 𝐵 ↔ 𝐵 𝐶ℋ 𝐴)) |
28 | | choccl 29664 |
. . . . . . . . . . . . . 14
⊢ (𝐵 ∈
Cℋ → (⊥‘𝐵) ∈ Cℋ
) |
29 | | cmbr3 29966 |
. . . . . . . . . . . . . 14
⊢ ((𝐴 ∈
Cℋ ∧ (⊥‘𝐵) ∈ Cℋ )
→ (𝐴
𝐶ℋ (⊥‘𝐵) ↔ (𝐴 ∩ ((⊥‘𝐴) ∨ℋ
(⊥‘𝐵))) =
(𝐴 ∩
(⊥‘𝐵)))) |
30 | 28, 29 | sylan2 593 |
. . . . . . . . . . . . 13
⊢ ((𝐴 ∈
Cℋ ∧ 𝐵 ∈ Cℋ )
→ (𝐴
𝐶ℋ (⊥‘𝐵) ↔ (𝐴 ∩ ((⊥‘𝐴) ∨ℋ
(⊥‘𝐵))) =
(𝐴 ∩
(⊥‘𝐵)))) |
31 | 26, 27, 30 | 3bitr3d 309 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈
Cℋ ∧ 𝐵 ∈ Cℋ )
→ (𝐵
𝐶ℋ 𝐴 ↔ (𝐴 ∩ ((⊥‘𝐴) ∨ℋ
(⊥‘𝐵))) =
(𝐴 ∩
(⊥‘𝐵)))) |
32 | 31 | biimpa 477 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈
Cℋ ∧ 𝐵 ∈ Cℋ )
∧ 𝐵
𝐶ℋ 𝐴) → (𝐴 ∩ ((⊥‘𝐴) ∨ℋ
(⊥‘𝐵))) =
(𝐴 ∩
(⊥‘𝐵))) |
33 | | incom 4140 |
. . . . . . . . . . 11
⊢ (𝐴 ∩ (⊥‘𝐵)) = ((⊥‘𝐵) ∩ 𝐴) |
34 | 32, 33 | eqtrdi 2796 |
. . . . . . . . . 10
⊢ (((𝐴 ∈
Cℋ ∧ 𝐵 ∈ Cℋ )
∧ 𝐵
𝐶ℋ 𝐴) → (𝐴 ∩ ((⊥‘𝐴) ∨ℋ
(⊥‘𝐵))) =
((⊥‘𝐵) ∩
𝐴)) |
35 | 34 | 3adantl3 1167 |
. . . . . . . . 9
⊢ (((𝐴 ∈
Cℋ ∧ 𝐵 ∈ Cℋ
∧ 𝐶 ∈
Cℋ ) ∧ 𝐵 𝐶ℋ 𝐴) → (𝐴 ∩ ((⊥‘𝐴) ∨ℋ
(⊥‘𝐵))) =
((⊥‘𝐵) ∩
𝐴)) |
36 | 35 | adantrr 714 |
. . . . . . . 8
⊢ (((𝐴 ∈
Cℋ ∧ 𝐵 ∈ Cℋ
∧ 𝐶 ∈
Cℋ ) ∧ (𝐵 𝐶ℋ 𝐴 ∧ 𝐵 𝐶ℋ 𝐶)) → (𝐴 ∩ ((⊥‘𝐴) ∨ℋ
(⊥‘𝐵))) =
((⊥‘𝐵) ∩
𝐴)) |
37 | 36 | ineq1d 4151 |
. . . . . . 7
⊢ (((𝐴 ∈
Cℋ ∧ 𝐵 ∈ Cℋ
∧ 𝐶 ∈
Cℋ ) ∧ (𝐵 𝐶ℋ 𝐴 ∧ 𝐵 𝐶ℋ 𝐶)) → ((𝐴 ∩ ((⊥‘𝐴) ∨ℋ
(⊥‘𝐵))) ∩
((𝐵 ∨ℋ
𝐶) ∩
(⊥‘(𝐴 ∩
𝐶)))) =
(((⊥‘𝐵) ∩
𝐴) ∩ ((𝐵 ∨ℋ 𝐶) ∩ (⊥‘(𝐴 ∩ 𝐶))))) |
38 | 25, 37 | eqtrid 2792 |
. . . . . 6
⊢ (((𝐴 ∈
Cℋ ∧ 𝐵 ∈ Cℋ
∧ 𝐶 ∈
Cℋ ) ∧ (𝐵 𝐶ℋ 𝐴 ∧ 𝐵 𝐶ℋ 𝐶)) → ((𝐴 ∩ (𝐵 ∨ℋ 𝐶)) ∩ (((⊥‘𝐴) ∨ℋ
(⊥‘𝐵)) ∩
(⊥‘(𝐴 ∩
𝐶)))) =
(((⊥‘𝐵) ∩
𝐴) ∩ ((𝐵 ∨ℋ 𝐶) ∩ (⊥‘(𝐴 ∩ 𝐶))))) |
39 | 24, 38 | eqtrd 2780 |
. . . . 5
⊢ (((𝐴 ∈
Cℋ ∧ 𝐵 ∈ Cℋ
∧ 𝐶 ∈
Cℋ ) ∧ (𝐵 𝐶ℋ 𝐴 ∧ 𝐵 𝐶ℋ 𝐶)) → ((𝐴 ∩ (𝐵 ∨ℋ 𝐶)) ∩ (⊥‘((𝐴 ∩ 𝐵) ∨ℋ (𝐴 ∩ 𝐶)))) = (((⊥‘𝐵) ∩ 𝐴) ∩ ((𝐵 ∨ℋ 𝐶) ∩ (⊥‘(𝐴 ∩ 𝐶))))) |
40 | | in4 4165 |
. . . . 5
⊢
(((⊥‘𝐵)
∩ 𝐴) ∩ ((𝐵 ∨ℋ 𝐶) ∩ (⊥‘(𝐴 ∩ 𝐶)))) = (((⊥‘𝐵) ∩ (𝐵 ∨ℋ 𝐶)) ∩ (𝐴 ∩ (⊥‘(𝐴 ∩ 𝐶)))) |
41 | 39, 40 | eqtrdi 2796 |
. . . 4
⊢ (((𝐴 ∈
Cℋ ∧ 𝐵 ∈ Cℋ
∧ 𝐶 ∈
Cℋ ) ∧ (𝐵 𝐶ℋ 𝐴 ∧ 𝐵 𝐶ℋ 𝐶)) → ((𝐴 ∩ (𝐵 ∨ℋ 𝐶)) ∩ (⊥‘((𝐴 ∩ 𝐵) ∨ℋ (𝐴 ∩ 𝐶)))) = (((⊥‘𝐵) ∩ (𝐵 ∨ℋ 𝐶)) ∩ (𝐴 ∩ (⊥‘(𝐴 ∩ 𝐶))))) |
42 | | ococ 29764 |
. . . . . . . . . . 11
⊢ (𝐵 ∈
Cℋ → (⊥‘(⊥‘𝐵)) = 𝐵) |
43 | 42 | oveq1d 7286 |
. . . . . . . . . 10
⊢ (𝐵 ∈
Cℋ → ((⊥‘(⊥‘𝐵)) ∨ℋ 𝐶) = (𝐵 ∨ℋ 𝐶)) |
44 | 43 | ineq2d 4152 |
. . . . . . . . 9
⊢ (𝐵 ∈
Cℋ → ((⊥‘𝐵) ∩ ((⊥‘(⊥‘𝐵)) ∨ℋ 𝐶)) = ((⊥‘𝐵) ∩ (𝐵 ∨ℋ 𝐶))) |
45 | 44 | 3ad2ant2 1133 |
. . . . . . . 8
⊢ ((𝐴 ∈
Cℋ ∧ 𝐵 ∈ Cℋ
∧ 𝐶 ∈
Cℋ ) → ((⊥‘𝐵) ∩ ((⊥‘(⊥‘𝐵)) ∨ℋ 𝐶)) = ((⊥‘𝐵) ∩ (𝐵 ∨ℋ 𝐶))) |
46 | 45 | adantr 481 |
. . . . . . 7
⊢ (((𝐴 ∈
Cℋ ∧ 𝐵 ∈ Cℋ
∧ 𝐶 ∈
Cℋ ) ∧ (𝐵 𝐶ℋ 𝐴 ∧ 𝐵 𝐶ℋ 𝐶)) → ((⊥‘𝐵) ∩
((⊥‘(⊥‘𝐵)) ∨ℋ 𝐶)) = ((⊥‘𝐵) ∩ (𝐵 ∨ℋ 𝐶))) |
47 | | cmcm3 29973 |
. . . . . . . . . . 11
⊢ ((𝐵 ∈
Cℋ ∧ 𝐶 ∈ Cℋ )
→ (𝐵
𝐶ℋ 𝐶 ↔ (⊥‘𝐵) 𝐶ℋ 𝐶)) |
48 | | cmbr3 29966 |
. . . . . . . . . . . 12
⊢
(((⊥‘𝐵)
∈ Cℋ ∧ 𝐶 ∈ Cℋ )
→ ((⊥‘𝐵)
𝐶ℋ 𝐶 ↔ ((⊥‘𝐵) ∩ ((⊥‘(⊥‘𝐵)) ∨ℋ 𝐶)) = ((⊥‘𝐵) ∩ 𝐶))) |
49 | 28, 48 | sylan 580 |
. . . . . . . . . . 11
⊢ ((𝐵 ∈
Cℋ ∧ 𝐶 ∈ Cℋ )
→ ((⊥‘𝐵)
𝐶ℋ 𝐶 ↔ ((⊥‘𝐵) ∩ ((⊥‘(⊥‘𝐵)) ∨ℋ 𝐶)) = ((⊥‘𝐵) ∩ 𝐶))) |
50 | 47, 49 | bitrd 278 |
. . . . . . . . . 10
⊢ ((𝐵 ∈
Cℋ ∧ 𝐶 ∈ Cℋ )
→ (𝐵
𝐶ℋ 𝐶 ↔ ((⊥‘𝐵) ∩ ((⊥‘(⊥‘𝐵)) ∨ℋ 𝐶)) = ((⊥‘𝐵) ∩ 𝐶))) |
51 | 50 | biimpa 477 |
. . . . . . . . 9
⊢ (((𝐵 ∈
Cℋ ∧ 𝐶 ∈ Cℋ )
∧ 𝐵
𝐶ℋ 𝐶) → ((⊥‘𝐵) ∩ ((⊥‘(⊥‘𝐵)) ∨ℋ 𝐶)) = ((⊥‘𝐵) ∩ 𝐶)) |
52 | 51 | 3adantl1 1165 |
. . . . . . . 8
⊢ (((𝐴 ∈
Cℋ ∧ 𝐵 ∈ Cℋ
∧ 𝐶 ∈
Cℋ ) ∧ 𝐵 𝐶ℋ 𝐶) → ((⊥‘𝐵) ∩
((⊥‘(⊥‘𝐵)) ∨ℋ 𝐶)) = ((⊥‘𝐵) ∩ 𝐶)) |
53 | 52 | adantrl 713 |
. . . . . . 7
⊢ (((𝐴 ∈
Cℋ ∧ 𝐵 ∈ Cℋ
∧ 𝐶 ∈
Cℋ ) ∧ (𝐵 𝐶ℋ 𝐴 ∧ 𝐵 𝐶ℋ 𝐶)) → ((⊥‘𝐵) ∩
((⊥‘(⊥‘𝐵)) ∨ℋ 𝐶)) = ((⊥‘𝐵) ∩ 𝐶)) |
54 | 46, 53 | eqtr3d 2782 |
. . . . . 6
⊢ (((𝐴 ∈
Cℋ ∧ 𝐵 ∈ Cℋ
∧ 𝐶 ∈
Cℋ ) ∧ (𝐵 𝐶ℋ 𝐴 ∧ 𝐵 𝐶ℋ 𝐶)) → ((⊥‘𝐵) ∩ (𝐵 ∨ℋ 𝐶)) = ((⊥‘𝐵) ∩ 𝐶)) |
55 | 54 | ineq1d 4151 |
. . . . 5
⊢ (((𝐴 ∈
Cℋ ∧ 𝐵 ∈ Cℋ
∧ 𝐶 ∈
Cℋ ) ∧ (𝐵 𝐶ℋ 𝐴 ∧ 𝐵 𝐶ℋ 𝐶)) → (((⊥‘𝐵) ∩ (𝐵 ∨ℋ 𝐶)) ∩ (𝐴 ∩ (⊥‘(𝐴 ∩ 𝐶)))) = (((⊥‘𝐵) ∩ 𝐶) ∩ (𝐴 ∩ (⊥‘(𝐴 ∩ 𝐶))))) |
56 | | inass 4159 |
. . . . . . . . 9
⊢
(((⊥‘𝐵)
∩ 𝐶) ∩ (𝐴 ∩ (⊥‘(𝐴 ∩ 𝐶)))) = ((⊥‘𝐵) ∩ (𝐶 ∩ (𝐴 ∩ (⊥‘(𝐴 ∩ 𝐶))))) |
57 | | in12 4160 |
. . . . . . . . . . . 12
⊢ (𝐶 ∩ (𝐴 ∩ (⊥‘(𝐴 ∩ 𝐶)))) = (𝐴 ∩ (𝐶 ∩ (⊥‘(𝐴 ∩ 𝐶)))) |
58 | | inass 4159 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∩ 𝐶) ∩ (⊥‘(𝐴 ∩ 𝐶))) = (𝐴 ∩ (𝐶 ∩ (⊥‘(𝐴 ∩ 𝐶)))) |
59 | 57, 58 | eqtr4i 2771 |
. . . . . . . . . . 11
⊢ (𝐶 ∩ (𝐴 ∩ (⊥‘(𝐴 ∩ 𝐶)))) = ((𝐴 ∩ 𝐶) ∩ (⊥‘(𝐴 ∩ 𝐶))) |
60 | | chocin 29853 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∩ 𝐶) ∈ Cℋ
→ ((𝐴 ∩ 𝐶) ∩ (⊥‘(𝐴 ∩ 𝐶))) = 0ℋ) |
61 | 2, 60 | syl 17 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈
Cℋ ∧ 𝐶 ∈ Cℋ )
→ ((𝐴 ∩ 𝐶) ∩ (⊥‘(𝐴 ∩ 𝐶))) = 0ℋ) |
62 | 59, 61 | eqtrid 2792 |
. . . . . . . . . 10
⊢ ((𝐴 ∈
Cℋ ∧ 𝐶 ∈ Cℋ )
→ (𝐶 ∩ (𝐴 ∩ (⊥‘(𝐴 ∩ 𝐶)))) = 0ℋ) |
63 | 62 | ineq2d 4152 |
. . . . . . . . 9
⊢ ((𝐴 ∈
Cℋ ∧ 𝐶 ∈ Cℋ )
→ ((⊥‘𝐵)
∩ (𝐶 ∩ (𝐴 ∩ (⊥‘(𝐴 ∩ 𝐶))))) = ((⊥‘𝐵) ∩
0ℋ)) |
64 | 56, 63 | eqtrid 2792 |
. . . . . . . 8
⊢ ((𝐴 ∈
Cℋ ∧ 𝐶 ∈ Cℋ )
→ (((⊥‘𝐵)
∩ 𝐶) ∩ (𝐴 ∩ (⊥‘(𝐴 ∩ 𝐶)))) = ((⊥‘𝐵) ∩
0ℋ)) |
65 | 64 | 3adant2 1130 |
. . . . . . 7
⊢ ((𝐴 ∈
Cℋ ∧ 𝐵 ∈ Cℋ
∧ 𝐶 ∈
Cℋ ) → (((⊥‘𝐵) ∩ 𝐶) ∩ (𝐴 ∩ (⊥‘(𝐴 ∩ 𝐶)))) = ((⊥‘𝐵) ∩
0ℋ)) |
66 | | chm0 29849 |
. . . . . . . . 9
⊢
((⊥‘𝐵)
∈ Cℋ → ((⊥‘𝐵) ∩ 0ℋ) =
0ℋ) |
67 | 28, 66 | syl 17 |
. . . . . . . 8
⊢ (𝐵 ∈
Cℋ → ((⊥‘𝐵) ∩ 0ℋ) =
0ℋ) |
68 | 67 | 3ad2ant2 1133 |
. . . . . . 7
⊢ ((𝐴 ∈
Cℋ ∧ 𝐵 ∈ Cℋ
∧ 𝐶 ∈
Cℋ ) → ((⊥‘𝐵) ∩ 0ℋ) =
0ℋ) |
69 | 65, 68 | eqtrd 2780 |
. . . . . 6
⊢ ((𝐴 ∈
Cℋ ∧ 𝐵 ∈ Cℋ
∧ 𝐶 ∈
Cℋ ) → (((⊥‘𝐵) ∩ 𝐶) ∩ (𝐴 ∩ (⊥‘(𝐴 ∩ 𝐶)))) = 0ℋ) |
70 | 69 | adantr 481 |
. . . . 5
⊢ (((𝐴 ∈
Cℋ ∧ 𝐵 ∈ Cℋ
∧ 𝐶 ∈
Cℋ ) ∧ (𝐵 𝐶ℋ 𝐴 ∧ 𝐵 𝐶ℋ 𝐶)) → (((⊥‘𝐵) ∩ 𝐶) ∩ (𝐴 ∩ (⊥‘(𝐴 ∩ 𝐶)))) = 0ℋ) |
71 | 55, 70 | eqtrd 2780 |
. . . 4
⊢ (((𝐴 ∈
Cℋ ∧ 𝐵 ∈ Cℋ
∧ 𝐶 ∈
Cℋ ) ∧ (𝐵 𝐶ℋ 𝐴 ∧ 𝐵 𝐶ℋ 𝐶)) → (((⊥‘𝐵) ∩ (𝐵 ∨ℋ 𝐶)) ∩ (𝐴 ∩ (⊥‘(𝐴 ∩ 𝐶)))) = 0ℋ) |
72 | 41, 71 | eqtrd 2780 |
. . 3
⊢ (((𝐴 ∈
Cℋ ∧ 𝐵 ∈ Cℋ
∧ 𝐶 ∈
Cℋ ) ∧ (𝐵 𝐶ℋ 𝐴 ∧ 𝐵 𝐶ℋ 𝐶)) → ((𝐴 ∩ (𝐵 ∨ℋ 𝐶)) ∩ (⊥‘((𝐴 ∩ 𝐵) ∨ℋ (𝐴 ∩ 𝐶)))) = 0ℋ) |
73 | | pjoml 29794 |
. . 3
⊢
(((((𝐴 ∩ 𝐵) ∨ℋ (𝐴 ∩ 𝐶)) ∈ Cℋ
∧ (𝐴 ∩ (𝐵 ∨ℋ 𝐶)) ∈
Sℋ ) ∧ (((𝐴 ∩ 𝐵) ∨ℋ (𝐴 ∩ 𝐶)) ⊆ (𝐴 ∩ (𝐵 ∨ℋ 𝐶)) ∧ ((𝐴 ∩ (𝐵 ∨ℋ 𝐶)) ∩ (⊥‘((𝐴 ∩ 𝐵) ∨ℋ (𝐴 ∩ 𝐶)))) = 0ℋ)) → ((𝐴 ∩ 𝐵) ∨ℋ (𝐴 ∩ 𝐶)) = (𝐴 ∩ (𝐵 ∨ℋ 𝐶))) |
74 | 13, 15, 72, 73 | syl12anc 834 |
. 2
⊢ (((𝐴 ∈
Cℋ ∧ 𝐵 ∈ Cℋ
∧ 𝐶 ∈
Cℋ ) ∧ (𝐵 𝐶ℋ 𝐴 ∧ 𝐵 𝐶ℋ 𝐶)) → ((𝐴 ∩ 𝐵) ∨ℋ (𝐴 ∩ 𝐶)) = (𝐴 ∩ (𝐵 ∨ℋ 𝐶))) |
75 | 74 | eqcomd 2746 |
1
⊢ (((𝐴 ∈
Cℋ ∧ 𝐵 ∈ Cℋ
∧ 𝐶 ∈
Cℋ ) ∧ (𝐵 𝐶ℋ 𝐴 ∧ 𝐵 𝐶ℋ 𝐶)) → (𝐴 ∩ (𝐵 ∨ℋ 𝐶)) = ((𝐴 ∩ 𝐵) ∨ℋ (𝐴 ∩ 𝐶))) |