Users' Mathboxes Mathbox for Norm Megill < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  cmtcomlemN Structured version   Visualization version   GIF version

Theorem cmtcomlemN 35057
Description: Lemma for cmtcomN 35058. (cmcmlem 28781 analog.) (Contributed by NM, 7-Nov-2011.) (New usage is discouraged.)
Hypotheses
Ref Expression
cmtcom.b 𝐵 = (Base‘𝐾)
cmtcom.c 𝐶 = (cm‘𝐾)
Assertion
Ref Expression
cmtcomlemN ((𝐾 ∈ OML ∧ 𝑋𝐵𝑌𝐵) → (𝑋𝐶𝑌𝑌𝐶𝑋))

Proof of Theorem cmtcomlemN
StepHypRef Expression
1 omllat 35051 . . . . . . . . . . . 12 (𝐾 ∈ OML → 𝐾 ∈ Lat)
213ad2ant1 1128 . . . . . . . . . . 11 ((𝐾 ∈ OML ∧ 𝑋𝐵𝑌𝐵) → 𝐾 ∈ Lat)
3 omlop 35050 . . . . . . . . . . . . 13 (𝐾 ∈ OML → 𝐾 ∈ OP)
4 cmtcom.b . . . . . . . . . . . . . 14 𝐵 = (Base‘𝐾)
5 eqid 2761 . . . . . . . . . . . . . 14 (oc‘𝐾) = (oc‘𝐾)
64, 5opoccl 35003 . . . . . . . . . . . . 13 ((𝐾 ∈ OP ∧ 𝑋𝐵) → ((oc‘𝐾)‘𝑋) ∈ 𝐵)
73, 6sylan 489 . . . . . . . . . . . 12 ((𝐾 ∈ OML ∧ 𝑋𝐵) → ((oc‘𝐾)‘𝑋) ∈ 𝐵)
873adant3 1127 . . . . . . . . . . 11 ((𝐾 ∈ OML ∧ 𝑋𝐵𝑌𝐵) → ((oc‘𝐾)‘𝑋) ∈ 𝐵)
9 simp3 1133 . . . . . . . . . . 11 ((𝐾 ∈ OML ∧ 𝑋𝐵𝑌𝐵) → 𝑌𝐵)
10 eqid 2761 . . . . . . . . . . . 12 (le‘𝐾) = (le‘𝐾)
11 eqid 2761 . . . . . . . . . . . 12 (join‘𝐾) = (join‘𝐾)
124, 10, 11latlej2 17283 . . . . . . . . . . 11 ((𝐾 ∈ Lat ∧ ((oc‘𝐾)‘𝑋) ∈ 𝐵𝑌𝐵) → 𝑌(le‘𝐾)(((oc‘𝐾)‘𝑋)(join‘𝐾)𝑌))
132, 8, 9, 12syl3anc 1477 . . . . . . . . . 10 ((𝐾 ∈ OML ∧ 𝑋𝐵𝑌𝐵) → 𝑌(le‘𝐾)(((oc‘𝐾)‘𝑋)(join‘𝐾)𝑌))
144, 11latjcl 17273 . . . . . . . . . . . 12 ((𝐾 ∈ Lat ∧ ((oc‘𝐾)‘𝑋) ∈ 𝐵𝑌𝐵) → (((oc‘𝐾)‘𝑋)(join‘𝐾)𝑌) ∈ 𝐵)
152, 8, 9, 14syl3anc 1477 . . . . . . . . . . 11 ((𝐾 ∈ OML ∧ 𝑋𝐵𝑌𝐵) → (((oc‘𝐾)‘𝑋)(join‘𝐾)𝑌) ∈ 𝐵)
16 eqid 2761 . . . . . . . . . . . 12 (meet‘𝐾) = (meet‘𝐾)
174, 10, 16latleeqm2 17302 . . . . . . . . . . 11 ((𝐾 ∈ Lat ∧ 𝑌𝐵 ∧ (((oc‘𝐾)‘𝑋)(join‘𝐾)𝑌) ∈ 𝐵) → (𝑌(le‘𝐾)(((oc‘𝐾)‘𝑋)(join‘𝐾)𝑌) ↔ ((((oc‘𝐾)‘𝑋)(join‘𝐾)𝑌)(meet‘𝐾)𝑌) = 𝑌))
182, 9, 15, 17syl3anc 1477 . . . . . . . . . 10 ((𝐾 ∈ OML ∧ 𝑋𝐵𝑌𝐵) → (𝑌(le‘𝐾)(((oc‘𝐾)‘𝑋)(join‘𝐾)𝑌) ↔ ((((oc‘𝐾)‘𝑋)(join‘𝐾)𝑌)(meet‘𝐾)𝑌) = 𝑌))
1913, 18mpbid 222 . . . . . . . . 9 ((𝐾 ∈ OML ∧ 𝑋𝐵𝑌𝐵) → ((((oc‘𝐾)‘𝑋)(join‘𝐾)𝑌)(meet‘𝐾)𝑌) = 𝑌)
2019oveq2d 6831 . . . . . . . 8 ((𝐾 ∈ OML ∧ 𝑋𝐵𝑌𝐵) → ((((oc‘𝐾)‘𝑋)(join‘𝐾)((oc‘𝐾)‘𝑌))(meet‘𝐾)((((oc‘𝐾)‘𝑋)(join‘𝐾)𝑌)(meet‘𝐾)𝑌)) = ((((oc‘𝐾)‘𝑋)(join‘𝐾)((oc‘𝐾)‘𝑌))(meet‘𝐾)𝑌))
21 omlol 35049 . . . . . . . . . 10 (𝐾 ∈ OML → 𝐾 ∈ OL)
22213ad2ant1 1128 . . . . . . . . 9 ((𝐾 ∈ OML ∧ 𝑋𝐵𝑌𝐵) → 𝐾 ∈ OL)
2333ad2ant1 1128 . . . . . . . . . . 11 ((𝐾 ∈ OML ∧ 𝑋𝐵𝑌𝐵) → 𝐾 ∈ OP)
244, 5opoccl 35003 . . . . . . . . . . 11 ((𝐾 ∈ OP ∧ 𝑌𝐵) → ((oc‘𝐾)‘𝑌) ∈ 𝐵)
2523, 9, 24syl2anc 696 . . . . . . . . . 10 ((𝐾 ∈ OML ∧ 𝑋𝐵𝑌𝐵) → ((oc‘𝐾)‘𝑌) ∈ 𝐵)
264, 11latjcl 17273 . . . . . . . . . 10 ((𝐾 ∈ Lat ∧ ((oc‘𝐾)‘𝑋) ∈ 𝐵 ∧ ((oc‘𝐾)‘𝑌) ∈ 𝐵) → (((oc‘𝐾)‘𝑋)(join‘𝐾)((oc‘𝐾)‘𝑌)) ∈ 𝐵)
272, 8, 25, 26syl3anc 1477 . . . . . . . . 9 ((𝐾 ∈ OML ∧ 𝑋𝐵𝑌𝐵) → (((oc‘𝐾)‘𝑋)(join‘𝐾)((oc‘𝐾)‘𝑌)) ∈ 𝐵)
284, 16latmassOLD 35038 . . . . . . . . 9 ((𝐾 ∈ OL ∧ ((((oc‘𝐾)‘𝑋)(join‘𝐾)((oc‘𝐾)‘𝑌)) ∈ 𝐵 ∧ (((oc‘𝐾)‘𝑋)(join‘𝐾)𝑌) ∈ 𝐵𝑌𝐵)) → (((((oc‘𝐾)‘𝑋)(join‘𝐾)((oc‘𝐾)‘𝑌))(meet‘𝐾)(((oc‘𝐾)‘𝑋)(join‘𝐾)𝑌))(meet‘𝐾)𝑌) = ((((oc‘𝐾)‘𝑋)(join‘𝐾)((oc‘𝐾)‘𝑌))(meet‘𝐾)((((oc‘𝐾)‘𝑋)(join‘𝐾)𝑌)(meet‘𝐾)𝑌)))
2922, 27, 15, 9, 28syl13anc 1479 . . . . . . . 8 ((𝐾 ∈ OML ∧ 𝑋𝐵𝑌𝐵) → (((((oc‘𝐾)‘𝑋)(join‘𝐾)((oc‘𝐾)‘𝑌))(meet‘𝐾)(((oc‘𝐾)‘𝑋)(join‘𝐾)𝑌))(meet‘𝐾)𝑌) = ((((oc‘𝐾)‘𝑋)(join‘𝐾)((oc‘𝐾)‘𝑌))(meet‘𝐾)((((oc‘𝐾)‘𝑋)(join‘𝐾)𝑌)(meet‘𝐾)𝑌)))
304, 11, 16, 5oldmm1 35026 . . . . . . . . . 10 ((𝐾 ∈ OL ∧ 𝑋𝐵𝑌𝐵) → ((oc‘𝐾)‘(𝑋(meet‘𝐾)𝑌)) = (((oc‘𝐾)‘𝑋)(join‘𝐾)((oc‘𝐾)‘𝑌)))
3121, 30syl3an1 1167 . . . . . . . . 9 ((𝐾 ∈ OML ∧ 𝑋𝐵𝑌𝐵) → ((oc‘𝐾)‘(𝑋(meet‘𝐾)𝑌)) = (((oc‘𝐾)‘𝑋)(join‘𝐾)((oc‘𝐾)‘𝑌)))
3231oveq1d 6830 . . . . . . . 8 ((𝐾 ∈ OML ∧ 𝑋𝐵𝑌𝐵) → (((oc‘𝐾)‘(𝑋(meet‘𝐾)𝑌))(meet‘𝐾)𝑌) = ((((oc‘𝐾)‘𝑋)(join‘𝐾)((oc‘𝐾)‘𝑌))(meet‘𝐾)𝑌))
3320, 29, 323eqtr4rd 2806 . . . . . . 7 ((𝐾 ∈ OML ∧ 𝑋𝐵𝑌𝐵) → (((oc‘𝐾)‘(𝑋(meet‘𝐾)𝑌))(meet‘𝐾)𝑌) = (((((oc‘𝐾)‘𝑋)(join‘𝐾)((oc‘𝐾)‘𝑌))(meet‘𝐾)(((oc‘𝐾)‘𝑋)(join‘𝐾)𝑌))(meet‘𝐾)𝑌))
3433adantr 472 . . . . . 6 (((𝐾 ∈ OML ∧ 𝑋𝐵𝑌𝐵) ∧ 𝑋 = ((𝑋(meet‘𝐾)𝑌)(join‘𝐾)(𝑋(meet‘𝐾)((oc‘𝐾)‘𝑌)))) → (((oc‘𝐾)‘(𝑋(meet‘𝐾)𝑌))(meet‘𝐾)𝑌) = (((((oc‘𝐾)‘𝑋)(join‘𝐾)((oc‘𝐾)‘𝑌))(meet‘𝐾)(((oc‘𝐾)‘𝑋)(join‘𝐾)𝑌))(meet‘𝐾)𝑌))
354, 11, 16, 5oldmj4 35033 . . . . . . . . . . . . 13 ((𝐾 ∈ OL ∧ 𝑋𝐵𝑌𝐵) → ((oc‘𝐾)‘(((oc‘𝐾)‘𝑋)(join‘𝐾)((oc‘𝐾)‘𝑌))) = (𝑋(meet‘𝐾)𝑌))
3621, 35syl3an1 1167 . . . . . . . . . . . 12 ((𝐾 ∈ OML ∧ 𝑋𝐵𝑌𝐵) → ((oc‘𝐾)‘(((oc‘𝐾)‘𝑋)(join‘𝐾)((oc‘𝐾)‘𝑌))) = (𝑋(meet‘𝐾)𝑌))
374, 11, 16, 5oldmj2 35031 . . . . . . . . . . . . 13 ((𝐾 ∈ OL ∧ 𝑋𝐵𝑌𝐵) → ((oc‘𝐾)‘(((oc‘𝐾)‘𝑋)(join‘𝐾)𝑌)) = (𝑋(meet‘𝐾)((oc‘𝐾)‘𝑌)))
3821, 37syl3an1 1167 . . . . . . . . . . . 12 ((𝐾 ∈ OML ∧ 𝑋𝐵𝑌𝐵) → ((oc‘𝐾)‘(((oc‘𝐾)‘𝑋)(join‘𝐾)𝑌)) = (𝑋(meet‘𝐾)((oc‘𝐾)‘𝑌)))
3936, 38oveq12d 6833 . . . . . . . . . . 11 ((𝐾 ∈ OML ∧ 𝑋𝐵𝑌𝐵) → (((oc‘𝐾)‘(((oc‘𝐾)‘𝑋)(join‘𝐾)((oc‘𝐾)‘𝑌)))(join‘𝐾)((oc‘𝐾)‘(((oc‘𝐾)‘𝑋)(join‘𝐾)𝑌))) = ((𝑋(meet‘𝐾)𝑌)(join‘𝐾)(𝑋(meet‘𝐾)((oc‘𝐾)‘𝑌))))
4039eqeq2d 2771 . . . . . . . . . 10 ((𝐾 ∈ OML ∧ 𝑋𝐵𝑌𝐵) → (𝑋 = (((oc‘𝐾)‘(((oc‘𝐾)‘𝑋)(join‘𝐾)((oc‘𝐾)‘𝑌)))(join‘𝐾)((oc‘𝐾)‘(((oc‘𝐾)‘𝑋)(join‘𝐾)𝑌))) ↔ 𝑋 = ((𝑋(meet‘𝐾)𝑌)(join‘𝐾)(𝑋(meet‘𝐾)((oc‘𝐾)‘𝑌)))))
4140biimpar 503 . . . . . . . . 9 (((𝐾 ∈ OML ∧ 𝑋𝐵𝑌𝐵) ∧ 𝑋 = ((𝑋(meet‘𝐾)𝑌)(join‘𝐾)(𝑋(meet‘𝐾)((oc‘𝐾)‘𝑌)))) → 𝑋 = (((oc‘𝐾)‘(((oc‘𝐾)‘𝑋)(join‘𝐾)((oc‘𝐾)‘𝑌)))(join‘𝐾)((oc‘𝐾)‘(((oc‘𝐾)‘𝑋)(join‘𝐾)𝑌))))
4241fveq2d 6358 . . . . . . . 8 (((𝐾 ∈ OML ∧ 𝑋𝐵𝑌𝐵) ∧ 𝑋 = ((𝑋(meet‘𝐾)𝑌)(join‘𝐾)(𝑋(meet‘𝐾)((oc‘𝐾)‘𝑌)))) → ((oc‘𝐾)‘𝑋) = ((oc‘𝐾)‘(((oc‘𝐾)‘(((oc‘𝐾)‘𝑋)(join‘𝐾)((oc‘𝐾)‘𝑌)))(join‘𝐾)((oc‘𝐾)‘(((oc‘𝐾)‘𝑋)(join‘𝐾)𝑌)))))
434, 11, 16, 5oldmj4 35033 . . . . . . . . . 10 ((𝐾 ∈ OL ∧ (((oc‘𝐾)‘𝑋)(join‘𝐾)((oc‘𝐾)‘𝑌)) ∈ 𝐵 ∧ (((oc‘𝐾)‘𝑋)(join‘𝐾)𝑌) ∈ 𝐵) → ((oc‘𝐾)‘(((oc‘𝐾)‘(((oc‘𝐾)‘𝑋)(join‘𝐾)((oc‘𝐾)‘𝑌)))(join‘𝐾)((oc‘𝐾)‘(((oc‘𝐾)‘𝑋)(join‘𝐾)𝑌)))) = ((((oc‘𝐾)‘𝑋)(join‘𝐾)((oc‘𝐾)‘𝑌))(meet‘𝐾)(((oc‘𝐾)‘𝑋)(join‘𝐾)𝑌)))
4422, 27, 15, 43syl3anc 1477 . . . . . . . . 9 ((𝐾 ∈ OML ∧ 𝑋𝐵𝑌𝐵) → ((oc‘𝐾)‘(((oc‘𝐾)‘(((oc‘𝐾)‘𝑋)(join‘𝐾)((oc‘𝐾)‘𝑌)))(join‘𝐾)((oc‘𝐾)‘(((oc‘𝐾)‘𝑋)(join‘𝐾)𝑌)))) = ((((oc‘𝐾)‘𝑋)(join‘𝐾)((oc‘𝐾)‘𝑌))(meet‘𝐾)(((oc‘𝐾)‘𝑋)(join‘𝐾)𝑌)))
4544adantr 472 . . . . . . . 8 (((𝐾 ∈ OML ∧ 𝑋𝐵𝑌𝐵) ∧ 𝑋 = ((𝑋(meet‘𝐾)𝑌)(join‘𝐾)(𝑋(meet‘𝐾)((oc‘𝐾)‘𝑌)))) → ((oc‘𝐾)‘(((oc‘𝐾)‘(((oc‘𝐾)‘𝑋)(join‘𝐾)((oc‘𝐾)‘𝑌)))(join‘𝐾)((oc‘𝐾)‘(((oc‘𝐾)‘𝑋)(join‘𝐾)𝑌)))) = ((((oc‘𝐾)‘𝑋)(join‘𝐾)((oc‘𝐾)‘𝑌))(meet‘𝐾)(((oc‘𝐾)‘𝑋)(join‘𝐾)𝑌)))
4642, 45eqtr2d 2796 . . . . . . 7 (((𝐾 ∈ OML ∧ 𝑋𝐵𝑌𝐵) ∧ 𝑋 = ((𝑋(meet‘𝐾)𝑌)(join‘𝐾)(𝑋(meet‘𝐾)((oc‘𝐾)‘𝑌)))) → ((((oc‘𝐾)‘𝑋)(join‘𝐾)((oc‘𝐾)‘𝑌))(meet‘𝐾)(((oc‘𝐾)‘𝑋)(join‘𝐾)𝑌)) = ((oc‘𝐾)‘𝑋))
4746oveq1d 6830 . . . . . 6 (((𝐾 ∈ OML ∧ 𝑋𝐵𝑌𝐵) ∧ 𝑋 = ((𝑋(meet‘𝐾)𝑌)(join‘𝐾)(𝑋(meet‘𝐾)((oc‘𝐾)‘𝑌)))) → (((((oc‘𝐾)‘𝑋)(join‘𝐾)((oc‘𝐾)‘𝑌))(meet‘𝐾)(((oc‘𝐾)‘𝑋)(join‘𝐾)𝑌))(meet‘𝐾)𝑌) = (((oc‘𝐾)‘𝑋)(meet‘𝐾)𝑌))
4834, 47eqtrd 2795 . . . . 5 (((𝐾 ∈ OML ∧ 𝑋𝐵𝑌𝐵) ∧ 𝑋 = ((𝑋(meet‘𝐾)𝑌)(join‘𝐾)(𝑋(meet‘𝐾)((oc‘𝐾)‘𝑌)))) → (((oc‘𝐾)‘(𝑋(meet‘𝐾)𝑌))(meet‘𝐾)𝑌) = (((oc‘𝐾)‘𝑋)(meet‘𝐾)𝑌))
4948oveq2d 6831 . . . 4 (((𝐾 ∈ OML ∧ 𝑋𝐵𝑌𝐵) ∧ 𝑋 = ((𝑋(meet‘𝐾)𝑌)(join‘𝐾)(𝑋(meet‘𝐾)((oc‘𝐾)‘𝑌)))) → ((𝑋(meet‘𝐾)𝑌)(join‘𝐾)(((oc‘𝐾)‘(𝑋(meet‘𝐾)𝑌))(meet‘𝐾)𝑌)) = ((𝑋(meet‘𝐾)𝑌)(join‘𝐾)(((oc‘𝐾)‘𝑋)(meet‘𝐾)𝑌)))
50 simp1 1131 . . . . . . 7 ((𝐾 ∈ OML ∧ 𝑋𝐵𝑌𝐵) → 𝐾 ∈ OML)
514, 16latmcl 17274 . . . . . . . 8 ((𝐾 ∈ Lat ∧ 𝑋𝐵𝑌𝐵) → (𝑋(meet‘𝐾)𝑌) ∈ 𝐵)
521, 51syl3an1 1167 . . . . . . 7 ((𝐾 ∈ OML ∧ 𝑋𝐵𝑌𝐵) → (𝑋(meet‘𝐾)𝑌) ∈ 𝐵)
5350, 52, 93jca 1123 . . . . . 6 ((𝐾 ∈ OML ∧ 𝑋𝐵𝑌𝐵) → (𝐾 ∈ OML ∧ (𝑋(meet‘𝐾)𝑌) ∈ 𝐵𝑌𝐵))
544, 10, 16latmle2 17299 . . . . . . 7 ((𝐾 ∈ Lat ∧ 𝑋𝐵𝑌𝐵) → (𝑋(meet‘𝐾)𝑌)(le‘𝐾)𝑌)
551, 54syl3an1 1167 . . . . . 6 ((𝐾 ∈ OML ∧ 𝑋𝐵𝑌𝐵) → (𝑋(meet‘𝐾)𝑌)(le‘𝐾)𝑌)
564, 10, 11, 16, 5omllaw2N 35053 . . . . . 6 ((𝐾 ∈ OML ∧ (𝑋(meet‘𝐾)𝑌) ∈ 𝐵𝑌𝐵) → ((𝑋(meet‘𝐾)𝑌)(le‘𝐾)𝑌 → ((𝑋(meet‘𝐾)𝑌)(join‘𝐾)(((oc‘𝐾)‘(𝑋(meet‘𝐾)𝑌))(meet‘𝐾)𝑌)) = 𝑌))
5753, 55, 56sylc 65 . . . . 5 ((𝐾 ∈ OML ∧ 𝑋𝐵𝑌𝐵) → ((𝑋(meet‘𝐾)𝑌)(join‘𝐾)(((oc‘𝐾)‘(𝑋(meet‘𝐾)𝑌))(meet‘𝐾)𝑌)) = 𝑌)
5857adantr 472 . . . 4 (((𝐾 ∈ OML ∧ 𝑋𝐵𝑌𝐵) ∧ 𝑋 = ((𝑋(meet‘𝐾)𝑌)(join‘𝐾)(𝑋(meet‘𝐾)((oc‘𝐾)‘𝑌)))) → ((𝑋(meet‘𝐾)𝑌)(join‘𝐾)(((oc‘𝐾)‘(𝑋(meet‘𝐾)𝑌))(meet‘𝐾)𝑌)) = 𝑌)
594, 16latmcom 17297 . . . . . . 7 ((𝐾 ∈ Lat ∧ 𝑋𝐵𝑌𝐵) → (𝑋(meet‘𝐾)𝑌) = (𝑌(meet‘𝐾)𝑋))
601, 59syl3an1 1167 . . . . . 6 ((𝐾 ∈ OML ∧ 𝑋𝐵𝑌𝐵) → (𝑋(meet‘𝐾)𝑌) = (𝑌(meet‘𝐾)𝑋))
614, 16latmcom 17297 . . . . . . 7 ((𝐾 ∈ Lat ∧ ((oc‘𝐾)‘𝑋) ∈ 𝐵𝑌𝐵) → (((oc‘𝐾)‘𝑋)(meet‘𝐾)𝑌) = (𝑌(meet‘𝐾)((oc‘𝐾)‘𝑋)))
622, 8, 9, 61syl3anc 1477 . . . . . 6 ((𝐾 ∈ OML ∧ 𝑋𝐵𝑌𝐵) → (((oc‘𝐾)‘𝑋)(meet‘𝐾)𝑌) = (𝑌(meet‘𝐾)((oc‘𝐾)‘𝑋)))
6360, 62oveq12d 6833 . . . . 5 ((𝐾 ∈ OML ∧ 𝑋𝐵𝑌𝐵) → ((𝑋(meet‘𝐾)𝑌)(join‘𝐾)(((oc‘𝐾)‘𝑋)(meet‘𝐾)𝑌)) = ((𝑌(meet‘𝐾)𝑋)(join‘𝐾)(𝑌(meet‘𝐾)((oc‘𝐾)‘𝑋))))
6463adantr 472 . . . 4 (((𝐾 ∈ OML ∧ 𝑋𝐵𝑌𝐵) ∧ 𝑋 = ((𝑋(meet‘𝐾)𝑌)(join‘𝐾)(𝑋(meet‘𝐾)((oc‘𝐾)‘𝑌)))) → ((𝑋(meet‘𝐾)𝑌)(join‘𝐾)(((oc‘𝐾)‘𝑋)(meet‘𝐾)𝑌)) = ((𝑌(meet‘𝐾)𝑋)(join‘𝐾)(𝑌(meet‘𝐾)((oc‘𝐾)‘𝑋))))
6549, 58, 643eqtr3d 2803 . . 3 (((𝐾 ∈ OML ∧ 𝑋𝐵𝑌𝐵) ∧ 𝑋 = ((𝑋(meet‘𝐾)𝑌)(join‘𝐾)(𝑋(meet‘𝐾)((oc‘𝐾)‘𝑌)))) → 𝑌 = ((𝑌(meet‘𝐾)𝑋)(join‘𝐾)(𝑌(meet‘𝐾)((oc‘𝐾)‘𝑋))))
6665ex 449 . 2 ((𝐾 ∈ OML ∧ 𝑋𝐵𝑌𝐵) → (𝑋 = ((𝑋(meet‘𝐾)𝑌)(join‘𝐾)(𝑋(meet‘𝐾)((oc‘𝐾)‘𝑌))) → 𝑌 = ((𝑌(meet‘𝐾)𝑋)(join‘𝐾)(𝑌(meet‘𝐾)((oc‘𝐾)‘𝑋)))))
67 cmtcom.c . . 3 𝐶 = (cm‘𝐾)
684, 11, 16, 5, 67cmtvalN 35020 . 2 ((𝐾 ∈ OML ∧ 𝑋𝐵𝑌𝐵) → (𝑋𝐶𝑌𝑋 = ((𝑋(meet‘𝐾)𝑌)(join‘𝐾)(𝑋(meet‘𝐾)((oc‘𝐾)‘𝑌)))))
694, 11, 16, 5, 67cmtvalN 35020 . . 3 ((𝐾 ∈ OML ∧ 𝑌𝐵𝑋𝐵) → (𝑌𝐶𝑋𝑌 = ((𝑌(meet‘𝐾)𝑋)(join‘𝐾)(𝑌(meet‘𝐾)((oc‘𝐾)‘𝑋)))))
70693com23 1121 . 2 ((𝐾 ∈ OML ∧ 𝑋𝐵𝑌𝐵) → (𝑌𝐶𝑋𝑌 = ((𝑌(meet‘𝐾)𝑋)(join‘𝐾)(𝑌(meet‘𝐾)((oc‘𝐾)‘𝑋)))))
7166, 68, 703imtr4d 283 1 ((𝐾 ∈ OML ∧ 𝑋𝐵𝑌𝐵) → (𝑋𝐶𝑌𝑌𝐶𝑋))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196  wa 383  w3a 1072   = wceq 1632  wcel 2140   class class class wbr 4805  cfv 6050  (class class class)co 6815  Basecbs 16080  lecple 16171  occoc 16172  joincjn 17166  meetcmee 17167  Latclat 17267  OPcops 34981  cmccmtN 34982  OLcol 34983  OMLcoml 34984
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1871  ax-4 1886  ax-5 1989  ax-6 2055  ax-7 2091  ax-8 2142  ax-9 2149  ax-10 2169  ax-11 2184  ax-12 2197  ax-13 2392  ax-ext 2741  ax-rep 4924  ax-sep 4934  ax-nul 4942  ax-pow 4993  ax-pr 5056  ax-un 7116
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3an 1074  df-tru 1635  df-ex 1854  df-nf 1859  df-sb 2048  df-eu 2612  df-mo 2613  df-clab 2748  df-cleq 2754  df-clel 2757  df-nfc 2892  df-ne 2934  df-ral 3056  df-rex 3057  df-reu 3058  df-rab 3060  df-v 3343  df-sbc 3578  df-csb 3676  df-dif 3719  df-un 3721  df-in 3723  df-ss 3730  df-nul 4060  df-if 4232  df-pw 4305  df-sn 4323  df-pr 4325  df-op 4329  df-uni 4590  df-iun 4675  df-br 4806  df-opab 4866  df-mpt 4883  df-id 5175  df-xp 5273  df-rel 5274  df-cnv 5275  df-co 5276  df-dm 5277  df-rn 5278  df-res 5279  df-ima 5280  df-iota 6013  df-fun 6052  df-fn 6053  df-f 6054  df-f1 6055  df-fo 6056  df-f1o 6057  df-fv 6058  df-riota 6776  df-ov 6818  df-oprab 6819  df-preset 17150  df-poset 17168  df-lub 17196  df-glb 17197  df-join 17198  df-meet 17199  df-lat 17268  df-oposet 34985  df-cmtN 34986  df-ol 34987  df-oml 34988
This theorem is referenced by:  cmtcomN  35058
  Copyright terms: Public domain W3C validator