Proof of Theorem cvrexch
| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | cvrexch.b | . . 3
⊢ 𝐵 = (Base‘𝐾) | 
| 2 |  | cvrexch.j | . . 3
⊢  ∨ =
(join‘𝐾) | 
| 3 |  | cvrexch.m | . . 3
⊢  ∧ =
(meet‘𝐾) | 
| 4 |  | cvrexch.c | . . 3
⊢ 𝐶 = ( ⋖ ‘𝐾) | 
| 5 | 1, 2, 3, 4 | cvrexchlem 39422 | . 2
⊢ ((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → ((𝑋 ∧ 𝑌)𝐶𝑌 → 𝑋𝐶(𝑋 ∨ 𝑌))) | 
| 6 |  | simp1 1136 | . . . . 5
⊢ ((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → 𝐾 ∈ HL) | 
| 7 |  | hlop 39364 | . . . . . . 7
⊢ (𝐾 ∈ HL → 𝐾 ∈ OP) | 
| 8 | 7 | 3ad2ant1 1133 | . . . . . 6
⊢ ((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → 𝐾 ∈ OP) | 
| 9 |  | simp3 1138 | . . . . . 6
⊢ ((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → 𝑌 ∈ 𝐵) | 
| 10 |  | eqid 2736 | . . . . . . 7
⊢
(oc‘𝐾) =
(oc‘𝐾) | 
| 11 | 1, 10 | opoccl 39196 | . . . . . 6
⊢ ((𝐾 ∈ OP ∧ 𝑌 ∈ 𝐵) → ((oc‘𝐾)‘𝑌) ∈ 𝐵) | 
| 12 | 8, 9, 11 | syl2anc 584 | . . . . 5
⊢ ((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → ((oc‘𝐾)‘𝑌) ∈ 𝐵) | 
| 13 |  | simp2 1137 | . . . . . 6
⊢ ((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → 𝑋 ∈ 𝐵) | 
| 14 | 1, 10 | opoccl 39196 | . . . . . 6
⊢ ((𝐾 ∈ OP ∧ 𝑋 ∈ 𝐵) → ((oc‘𝐾)‘𝑋) ∈ 𝐵) | 
| 15 | 8, 13, 14 | syl2anc 584 | . . . . 5
⊢ ((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → ((oc‘𝐾)‘𝑋) ∈ 𝐵) | 
| 16 | 1, 2, 3, 4 | cvrexchlem 39422 | . . . . 5
⊢ ((𝐾 ∈ HL ∧
((oc‘𝐾)‘𝑌) ∈ 𝐵 ∧ ((oc‘𝐾)‘𝑋) ∈ 𝐵) → ((((oc‘𝐾)‘𝑌) ∧ ((oc‘𝐾)‘𝑋))𝐶((oc‘𝐾)‘𝑋) → ((oc‘𝐾)‘𝑌)𝐶(((oc‘𝐾)‘𝑌) ∨ ((oc‘𝐾)‘𝑋)))) | 
| 17 | 6, 12, 15, 16 | syl3anc 1372 | . . . 4
⊢ ((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → ((((oc‘𝐾)‘𝑌) ∧ ((oc‘𝐾)‘𝑋))𝐶((oc‘𝐾)‘𝑋) → ((oc‘𝐾)‘𝑌)𝐶(((oc‘𝐾)‘𝑌) ∨ ((oc‘𝐾)‘𝑋)))) | 
| 18 |  | hlol 39363 | . . . . . . 7
⊢ (𝐾 ∈ HL → 𝐾 ∈ OL) | 
| 19 | 1, 2, 3, 10 | oldmj1 39223 | . . . . . . 7
⊢ ((𝐾 ∈ OL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → ((oc‘𝐾)‘(𝑋 ∨ 𝑌)) = (((oc‘𝐾)‘𝑋) ∧ ((oc‘𝐾)‘𝑌))) | 
| 20 | 18, 19 | syl3an1 1163 | . . . . . 6
⊢ ((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → ((oc‘𝐾)‘(𝑋 ∨ 𝑌)) = (((oc‘𝐾)‘𝑋) ∧ ((oc‘𝐾)‘𝑌))) | 
| 21 |  | hllat 39365 | . . . . . . . 8
⊢ (𝐾 ∈ HL → 𝐾 ∈ Lat) | 
| 22 | 21 | 3ad2ant1 1133 | . . . . . . 7
⊢ ((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → 𝐾 ∈ Lat) | 
| 23 | 1, 3 | latmcom 18509 | . . . . . . 7
⊢ ((𝐾 ∈ Lat ∧
((oc‘𝐾)‘𝑋) ∈ 𝐵 ∧ ((oc‘𝐾)‘𝑌) ∈ 𝐵) → (((oc‘𝐾)‘𝑋) ∧ ((oc‘𝐾)‘𝑌)) = (((oc‘𝐾)‘𝑌) ∧ ((oc‘𝐾)‘𝑋))) | 
| 24 | 22, 15, 12, 23 | syl3anc 1372 | . . . . . 6
⊢ ((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (((oc‘𝐾)‘𝑋) ∧ ((oc‘𝐾)‘𝑌)) = (((oc‘𝐾)‘𝑌) ∧ ((oc‘𝐾)‘𝑋))) | 
| 25 | 20, 24 | eqtrd 2776 | . . . . 5
⊢ ((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → ((oc‘𝐾)‘(𝑋 ∨ 𝑌)) = (((oc‘𝐾)‘𝑌) ∧ ((oc‘𝐾)‘𝑋))) | 
| 26 | 25 | breq1d 5152 | . . . 4
⊢ ((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (((oc‘𝐾)‘(𝑋 ∨ 𝑌))𝐶((oc‘𝐾)‘𝑋) ↔ (((oc‘𝐾)‘𝑌) ∧ ((oc‘𝐾)‘𝑋))𝐶((oc‘𝐾)‘𝑋))) | 
| 27 | 1, 2, 3, 10 | oldmm1 39219 | . . . . . . 7
⊢ ((𝐾 ∈ OL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → ((oc‘𝐾)‘(𝑋 ∧ 𝑌)) = (((oc‘𝐾)‘𝑋) ∨ ((oc‘𝐾)‘𝑌))) | 
| 28 | 18, 27 | syl3an1 1163 | . . . . . 6
⊢ ((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → ((oc‘𝐾)‘(𝑋 ∧ 𝑌)) = (((oc‘𝐾)‘𝑋) ∨ ((oc‘𝐾)‘𝑌))) | 
| 29 | 1, 2 | latjcom 18493 | . . . . . . 7
⊢ ((𝐾 ∈ Lat ∧
((oc‘𝐾)‘𝑋) ∈ 𝐵 ∧ ((oc‘𝐾)‘𝑌) ∈ 𝐵) → (((oc‘𝐾)‘𝑋) ∨ ((oc‘𝐾)‘𝑌)) = (((oc‘𝐾)‘𝑌) ∨ ((oc‘𝐾)‘𝑋))) | 
| 30 | 22, 15, 12, 29 | syl3anc 1372 | . . . . . 6
⊢ ((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (((oc‘𝐾)‘𝑋) ∨ ((oc‘𝐾)‘𝑌)) = (((oc‘𝐾)‘𝑌) ∨ ((oc‘𝐾)‘𝑋))) | 
| 31 | 28, 30 | eqtrd 2776 | . . . . 5
⊢ ((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → ((oc‘𝐾)‘(𝑋 ∧ 𝑌)) = (((oc‘𝐾)‘𝑌) ∨ ((oc‘𝐾)‘𝑋))) | 
| 32 | 31 | breq2d 5154 | . . . 4
⊢ ((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (((oc‘𝐾)‘𝑌)𝐶((oc‘𝐾)‘(𝑋 ∧ 𝑌)) ↔ ((oc‘𝐾)‘𝑌)𝐶(((oc‘𝐾)‘𝑌) ∨ ((oc‘𝐾)‘𝑋)))) | 
| 33 | 17, 26, 32 | 3imtr4d 294 | . . 3
⊢ ((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (((oc‘𝐾)‘(𝑋 ∨ 𝑌))𝐶((oc‘𝐾)‘𝑋) → ((oc‘𝐾)‘𝑌)𝐶((oc‘𝐾)‘(𝑋 ∧ 𝑌)))) | 
| 34 | 1, 2 | latjcl 18485 | . . . . 5
⊢ ((𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋 ∨ 𝑌) ∈ 𝐵) | 
| 35 | 21, 34 | syl3an1 1163 | . . . 4
⊢ ((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋 ∨ 𝑌) ∈ 𝐵) | 
| 36 | 1, 10, 4 | cvrcon3b 39279 | . . . 4
⊢ ((𝐾 ∈ OP ∧ 𝑋 ∈ 𝐵 ∧ (𝑋 ∨ 𝑌) ∈ 𝐵) → (𝑋𝐶(𝑋 ∨ 𝑌) ↔ ((oc‘𝐾)‘(𝑋 ∨ 𝑌))𝐶((oc‘𝐾)‘𝑋))) | 
| 37 | 8, 13, 35, 36 | syl3anc 1372 | . . 3
⊢ ((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋𝐶(𝑋 ∨ 𝑌) ↔ ((oc‘𝐾)‘(𝑋 ∨ 𝑌))𝐶((oc‘𝐾)‘𝑋))) | 
| 38 | 1, 3 | latmcl 18486 | . . . . 5
⊢ ((𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋 ∧ 𝑌) ∈ 𝐵) | 
| 39 | 21, 38 | syl3an1 1163 | . . . 4
⊢ ((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋 ∧ 𝑌) ∈ 𝐵) | 
| 40 | 1, 10, 4 | cvrcon3b 39279 | . . . 4
⊢ ((𝐾 ∈ OP ∧ (𝑋 ∧ 𝑌) ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → ((𝑋 ∧ 𝑌)𝐶𝑌 ↔ ((oc‘𝐾)‘𝑌)𝐶((oc‘𝐾)‘(𝑋 ∧ 𝑌)))) | 
| 41 | 8, 39, 9, 40 | syl3anc 1372 | . . 3
⊢ ((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → ((𝑋 ∧ 𝑌)𝐶𝑌 ↔ ((oc‘𝐾)‘𝑌)𝐶((oc‘𝐾)‘(𝑋 ∧ 𝑌)))) | 
| 42 | 33, 37, 41 | 3imtr4d 294 | . 2
⊢ ((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋𝐶(𝑋 ∨ 𝑌) → (𝑋 ∧ 𝑌)𝐶𝑌)) | 
| 43 | 5, 42 | impbid 212 | 1
⊢ ((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → ((𝑋 ∧ 𝑌)𝐶𝑌 ↔ 𝑋𝐶(𝑋 ∨ 𝑌))) |