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

Theorem omlfh3N 37010
Description: Foulis-Holland Theorem, part 3. Dual of omlfh1N 37009. (Contributed by NM, 8-Nov-2011.) (New usage is discouraged.)
Hypotheses
Ref Expression
omlfh1.b 𝐵 = (Base‘𝐾)
omlfh1.j = (join‘𝐾)
omlfh1.m = (meet‘𝐾)
omlfh1.c 𝐶 = (cm‘𝐾)
Assertion
Ref Expression
omlfh3N ((𝐾 ∈ OML ∧ (𝑋𝐵𝑌𝐵𝑍𝐵) ∧ (𝑋𝐶𝑌𝑋𝐶𝑍)) → (𝑋 (𝑌 𝑍)) = ((𝑋 𝑌) (𝑋 𝑍)))

Proof of Theorem omlfh3N
StepHypRef Expression
1 omlfh1.b . . . . . . 7 𝐵 = (Base‘𝐾)
2 eqid 2737 . . . . . . 7 (oc‘𝐾) = (oc‘𝐾)
3 omlfh1.c . . . . . . 7 𝐶 = (cm‘𝐾)
41, 2, 3cmt4N 37003 . . . . . 6 ((𝐾 ∈ OML ∧ 𝑋𝐵𝑌𝐵) → (𝑋𝐶𝑌 ↔ ((oc‘𝐾)‘𝑋)𝐶((oc‘𝐾)‘𝑌)))
543adant3r3 1186 . . . . 5 ((𝐾 ∈ OML ∧ (𝑋𝐵𝑌𝐵𝑍𝐵)) → (𝑋𝐶𝑌 ↔ ((oc‘𝐾)‘𝑋)𝐶((oc‘𝐾)‘𝑌)))
61, 2, 3cmt4N 37003 . . . . . 6 ((𝐾 ∈ OML ∧ 𝑋𝐵𝑍𝐵) → (𝑋𝐶𝑍 ↔ ((oc‘𝐾)‘𝑋)𝐶((oc‘𝐾)‘𝑍)))
763adant3r2 1185 . . . . 5 ((𝐾 ∈ OML ∧ (𝑋𝐵𝑌𝐵𝑍𝐵)) → (𝑋𝐶𝑍 ↔ ((oc‘𝐾)‘𝑋)𝐶((oc‘𝐾)‘𝑍)))
85, 7anbi12d 634 . . . 4 ((𝐾 ∈ OML ∧ (𝑋𝐵𝑌𝐵𝑍𝐵)) → ((𝑋𝐶𝑌𝑋𝐶𝑍) ↔ (((oc‘𝐾)‘𝑋)𝐶((oc‘𝐾)‘𝑌) ∧ ((oc‘𝐾)‘𝑋)𝐶((oc‘𝐾)‘𝑍))))
9 simpl 486 . . . . 5 ((𝐾 ∈ OML ∧ (𝑋𝐵𝑌𝐵𝑍𝐵)) → 𝐾 ∈ OML)
10 omlop 36992 . . . . . . . 8 (𝐾 ∈ OML → 𝐾 ∈ OP)
1110adantr 484 . . . . . . 7 ((𝐾 ∈ OML ∧ (𝑋𝐵𝑌𝐵𝑍𝐵)) → 𝐾 ∈ OP)
12 simpr1 1196 . . . . . . 7 ((𝐾 ∈ OML ∧ (𝑋𝐵𝑌𝐵𝑍𝐵)) → 𝑋𝐵)
131, 2opoccl 36945 . . . . . . 7 ((𝐾 ∈ OP ∧ 𝑋𝐵) → ((oc‘𝐾)‘𝑋) ∈ 𝐵)
1411, 12, 13syl2anc 587 . . . . . 6 ((𝐾 ∈ OML ∧ (𝑋𝐵𝑌𝐵𝑍𝐵)) → ((oc‘𝐾)‘𝑋) ∈ 𝐵)
15 simpr2 1197 . . . . . . 7 ((𝐾 ∈ OML ∧ (𝑋𝐵𝑌𝐵𝑍𝐵)) → 𝑌𝐵)
161, 2opoccl 36945 . . . . . . 7 ((𝐾 ∈ OP ∧ 𝑌𝐵) → ((oc‘𝐾)‘𝑌) ∈ 𝐵)
1711, 15, 16syl2anc 587 . . . . . 6 ((𝐾 ∈ OML ∧ (𝑋𝐵𝑌𝐵𝑍𝐵)) → ((oc‘𝐾)‘𝑌) ∈ 𝐵)
18 simpr3 1198 . . . . . . 7 ((𝐾 ∈ OML ∧ (𝑋𝐵𝑌𝐵𝑍𝐵)) → 𝑍𝐵)
191, 2opoccl 36945 . . . . . . 7 ((𝐾 ∈ OP ∧ 𝑍𝐵) → ((oc‘𝐾)‘𝑍) ∈ 𝐵)
2011, 18, 19syl2anc 587 . . . . . 6 ((𝐾 ∈ OML ∧ (𝑋𝐵𝑌𝐵𝑍𝐵)) → ((oc‘𝐾)‘𝑍) ∈ 𝐵)
2114, 17, 203jca 1130 . . . . 5 ((𝐾 ∈ OML ∧ (𝑋𝐵𝑌𝐵𝑍𝐵)) → (((oc‘𝐾)‘𝑋) ∈ 𝐵 ∧ ((oc‘𝐾)‘𝑌) ∈ 𝐵 ∧ ((oc‘𝐾)‘𝑍) ∈ 𝐵))
22 omlfh1.j . . . . . . . 8 = (join‘𝐾)
23 omlfh1.m . . . . . . . 8 = (meet‘𝐾)
241, 22, 23, 3omlfh1N 37009 . . . . . . 7 ((𝐾 ∈ OML ∧ (((oc‘𝐾)‘𝑋) ∈ 𝐵 ∧ ((oc‘𝐾)‘𝑌) ∈ 𝐵 ∧ ((oc‘𝐾)‘𝑍) ∈ 𝐵) ∧ (((oc‘𝐾)‘𝑋)𝐶((oc‘𝐾)‘𝑌) ∧ ((oc‘𝐾)‘𝑋)𝐶((oc‘𝐾)‘𝑍))) → (((oc‘𝐾)‘𝑋) (((oc‘𝐾)‘𝑌) ((oc‘𝐾)‘𝑍))) = ((((oc‘𝐾)‘𝑋) ((oc‘𝐾)‘𝑌)) (((oc‘𝐾)‘𝑋) ((oc‘𝐾)‘𝑍))))
2524fveq2d 6721 . . . . . 6 ((𝐾 ∈ OML ∧ (((oc‘𝐾)‘𝑋) ∈ 𝐵 ∧ ((oc‘𝐾)‘𝑌) ∈ 𝐵 ∧ ((oc‘𝐾)‘𝑍) ∈ 𝐵) ∧ (((oc‘𝐾)‘𝑋)𝐶((oc‘𝐾)‘𝑌) ∧ ((oc‘𝐾)‘𝑋)𝐶((oc‘𝐾)‘𝑍))) → ((oc‘𝐾)‘(((oc‘𝐾)‘𝑋) (((oc‘𝐾)‘𝑌) ((oc‘𝐾)‘𝑍)))) = ((oc‘𝐾)‘((((oc‘𝐾)‘𝑋) ((oc‘𝐾)‘𝑌)) (((oc‘𝐾)‘𝑋) ((oc‘𝐾)‘𝑍)))))
26253exp 1121 . . . . 5 (𝐾 ∈ OML → ((((oc‘𝐾)‘𝑋) ∈ 𝐵 ∧ ((oc‘𝐾)‘𝑌) ∈ 𝐵 ∧ ((oc‘𝐾)‘𝑍) ∈ 𝐵) → ((((oc‘𝐾)‘𝑋)𝐶((oc‘𝐾)‘𝑌) ∧ ((oc‘𝐾)‘𝑋)𝐶((oc‘𝐾)‘𝑍)) → ((oc‘𝐾)‘(((oc‘𝐾)‘𝑋) (((oc‘𝐾)‘𝑌) ((oc‘𝐾)‘𝑍)))) = ((oc‘𝐾)‘((((oc‘𝐾)‘𝑋) ((oc‘𝐾)‘𝑌)) (((oc‘𝐾)‘𝑋) ((oc‘𝐾)‘𝑍)))))))
279, 21, 26sylc 65 . . . 4 ((𝐾 ∈ OML ∧ (𝑋𝐵𝑌𝐵𝑍𝐵)) → ((((oc‘𝐾)‘𝑋)𝐶((oc‘𝐾)‘𝑌) ∧ ((oc‘𝐾)‘𝑋)𝐶((oc‘𝐾)‘𝑍)) → ((oc‘𝐾)‘(((oc‘𝐾)‘𝑋) (((oc‘𝐾)‘𝑌) ((oc‘𝐾)‘𝑍)))) = ((oc‘𝐾)‘((((oc‘𝐾)‘𝑋) ((oc‘𝐾)‘𝑌)) (((oc‘𝐾)‘𝑋) ((oc‘𝐾)‘𝑍))))))
288, 27sylbid 243 . . 3 ((𝐾 ∈ OML ∧ (𝑋𝐵𝑌𝐵𝑍𝐵)) → ((𝑋𝐶𝑌𝑋𝐶𝑍) → ((oc‘𝐾)‘(((oc‘𝐾)‘𝑋) (((oc‘𝐾)‘𝑌) ((oc‘𝐾)‘𝑍)))) = ((oc‘𝐾)‘((((oc‘𝐾)‘𝑋) ((oc‘𝐾)‘𝑌)) (((oc‘𝐾)‘𝑋) ((oc‘𝐾)‘𝑍))))))
29283impia 1119 . 2 ((𝐾 ∈ OML ∧ (𝑋𝐵𝑌𝐵𝑍𝐵) ∧ (𝑋𝐶𝑌𝑋𝐶𝑍)) → ((oc‘𝐾)‘(((oc‘𝐾)‘𝑋) (((oc‘𝐾)‘𝑌) ((oc‘𝐾)‘𝑍)))) = ((oc‘𝐾)‘((((oc‘𝐾)‘𝑋) ((oc‘𝐾)‘𝑌)) (((oc‘𝐾)‘𝑋) ((oc‘𝐾)‘𝑍)))))
30 omlol 36991 . . . . . 6 (𝐾 ∈ OML → 𝐾 ∈ OL)
3130adantr 484 . . . . 5 ((𝐾 ∈ OML ∧ (𝑋𝐵𝑌𝐵𝑍𝐵)) → 𝐾 ∈ OL)
32 omllat 36993 . . . . . . 7 (𝐾 ∈ OML → 𝐾 ∈ Lat)
3332adantr 484 . . . . . 6 ((𝐾 ∈ OML ∧ (𝑋𝐵𝑌𝐵𝑍𝐵)) → 𝐾 ∈ Lat)
341, 22latjcl 17945 . . . . . 6 ((𝐾 ∈ Lat ∧ ((oc‘𝐾)‘𝑌) ∈ 𝐵 ∧ ((oc‘𝐾)‘𝑍) ∈ 𝐵) → (((oc‘𝐾)‘𝑌) ((oc‘𝐾)‘𝑍)) ∈ 𝐵)
3533, 17, 20, 34syl3anc 1373 . . . . 5 ((𝐾 ∈ OML ∧ (𝑋𝐵𝑌𝐵𝑍𝐵)) → (((oc‘𝐾)‘𝑌) ((oc‘𝐾)‘𝑍)) ∈ 𝐵)
361, 22, 23, 2oldmm2 36969 . . . . 5 ((𝐾 ∈ OL ∧ 𝑋𝐵 ∧ (((oc‘𝐾)‘𝑌) ((oc‘𝐾)‘𝑍)) ∈ 𝐵) → ((oc‘𝐾)‘(((oc‘𝐾)‘𝑋) (((oc‘𝐾)‘𝑌) ((oc‘𝐾)‘𝑍)))) = (𝑋 ((oc‘𝐾)‘(((oc‘𝐾)‘𝑌) ((oc‘𝐾)‘𝑍)))))
3731, 12, 35, 36syl3anc 1373 . . . 4 ((𝐾 ∈ OML ∧ (𝑋𝐵𝑌𝐵𝑍𝐵)) → ((oc‘𝐾)‘(((oc‘𝐾)‘𝑋) (((oc‘𝐾)‘𝑌) ((oc‘𝐾)‘𝑍)))) = (𝑋 ((oc‘𝐾)‘(((oc‘𝐾)‘𝑌) ((oc‘𝐾)‘𝑍)))))
381, 22, 23, 2oldmj4 36975 . . . . . 6 ((𝐾 ∈ OL ∧ 𝑌𝐵𝑍𝐵) → ((oc‘𝐾)‘(((oc‘𝐾)‘𝑌) ((oc‘𝐾)‘𝑍))) = (𝑌 𝑍))
3931, 15, 18, 38syl3anc 1373 . . . . 5 ((𝐾 ∈ OML ∧ (𝑋𝐵𝑌𝐵𝑍𝐵)) → ((oc‘𝐾)‘(((oc‘𝐾)‘𝑌) ((oc‘𝐾)‘𝑍))) = (𝑌 𝑍))
4039oveq2d 7229 . . . 4 ((𝐾 ∈ OML ∧ (𝑋𝐵𝑌𝐵𝑍𝐵)) → (𝑋 ((oc‘𝐾)‘(((oc‘𝐾)‘𝑌) ((oc‘𝐾)‘𝑍)))) = (𝑋 (𝑌 𝑍)))
4137, 40eqtr2d 2778 . . 3 ((𝐾 ∈ OML ∧ (𝑋𝐵𝑌𝐵𝑍𝐵)) → (𝑋 (𝑌 𝑍)) = ((oc‘𝐾)‘(((oc‘𝐾)‘𝑋) (((oc‘𝐾)‘𝑌) ((oc‘𝐾)‘𝑍)))))
42413adant3 1134 . 2 ((𝐾 ∈ OML ∧ (𝑋𝐵𝑌𝐵𝑍𝐵) ∧ (𝑋𝐶𝑌𝑋𝐶𝑍)) → (𝑋 (𝑌 𝑍)) = ((oc‘𝐾)‘(((oc‘𝐾)‘𝑋) (((oc‘𝐾)‘𝑌) ((oc‘𝐾)‘𝑍)))))
431, 23latmcl 17946 . . . . . 6 ((𝐾 ∈ Lat ∧ ((oc‘𝐾)‘𝑋) ∈ 𝐵 ∧ ((oc‘𝐾)‘𝑌) ∈ 𝐵) → (((oc‘𝐾)‘𝑋) ((oc‘𝐾)‘𝑌)) ∈ 𝐵)
4433, 14, 17, 43syl3anc 1373 . . . . 5 ((𝐾 ∈ OML ∧ (𝑋𝐵𝑌𝐵𝑍𝐵)) → (((oc‘𝐾)‘𝑋) ((oc‘𝐾)‘𝑌)) ∈ 𝐵)
451, 23latmcl 17946 . . . . . 6 ((𝐾 ∈ Lat ∧ ((oc‘𝐾)‘𝑋) ∈ 𝐵 ∧ ((oc‘𝐾)‘𝑍) ∈ 𝐵) → (((oc‘𝐾)‘𝑋) ((oc‘𝐾)‘𝑍)) ∈ 𝐵)
4633, 14, 20, 45syl3anc 1373 . . . . 5 ((𝐾 ∈ OML ∧ (𝑋𝐵𝑌𝐵𝑍𝐵)) → (((oc‘𝐾)‘𝑋) ((oc‘𝐾)‘𝑍)) ∈ 𝐵)
471, 22, 23, 2oldmj1 36972 . . . . 5 ((𝐾 ∈ OL ∧ (((oc‘𝐾)‘𝑋) ((oc‘𝐾)‘𝑌)) ∈ 𝐵 ∧ (((oc‘𝐾)‘𝑋) ((oc‘𝐾)‘𝑍)) ∈ 𝐵) → ((oc‘𝐾)‘((((oc‘𝐾)‘𝑋) ((oc‘𝐾)‘𝑌)) (((oc‘𝐾)‘𝑋) ((oc‘𝐾)‘𝑍)))) = (((oc‘𝐾)‘(((oc‘𝐾)‘𝑋) ((oc‘𝐾)‘𝑌))) ((oc‘𝐾)‘(((oc‘𝐾)‘𝑋) ((oc‘𝐾)‘𝑍)))))
4831, 44, 46, 47syl3anc 1373 . . . 4 ((𝐾 ∈ OML ∧ (𝑋𝐵𝑌𝐵𝑍𝐵)) → ((oc‘𝐾)‘((((oc‘𝐾)‘𝑋) ((oc‘𝐾)‘𝑌)) (((oc‘𝐾)‘𝑋) ((oc‘𝐾)‘𝑍)))) = (((oc‘𝐾)‘(((oc‘𝐾)‘𝑋) ((oc‘𝐾)‘𝑌))) ((oc‘𝐾)‘(((oc‘𝐾)‘𝑋) ((oc‘𝐾)‘𝑍)))))
491, 22, 23, 2oldmm4 36971 . . . . . 6 ((𝐾 ∈ OL ∧ 𝑋𝐵𝑌𝐵) → ((oc‘𝐾)‘(((oc‘𝐾)‘𝑋) ((oc‘𝐾)‘𝑌))) = (𝑋 𝑌))
5031, 12, 15, 49syl3anc 1373 . . . . 5 ((𝐾 ∈ OML ∧ (𝑋𝐵𝑌𝐵𝑍𝐵)) → ((oc‘𝐾)‘(((oc‘𝐾)‘𝑋) ((oc‘𝐾)‘𝑌))) = (𝑋 𝑌))
511, 22, 23, 2oldmm4 36971 . . . . . 6 ((𝐾 ∈ OL ∧ 𝑋𝐵𝑍𝐵) → ((oc‘𝐾)‘(((oc‘𝐾)‘𝑋) ((oc‘𝐾)‘𝑍))) = (𝑋 𝑍))
5231, 12, 18, 51syl3anc 1373 . . . . 5 ((𝐾 ∈ OML ∧ (𝑋𝐵𝑌𝐵𝑍𝐵)) → ((oc‘𝐾)‘(((oc‘𝐾)‘𝑋) ((oc‘𝐾)‘𝑍))) = (𝑋 𝑍))
5350, 52oveq12d 7231 . . . 4 ((𝐾 ∈ OML ∧ (𝑋𝐵𝑌𝐵𝑍𝐵)) → (((oc‘𝐾)‘(((oc‘𝐾)‘𝑋) ((oc‘𝐾)‘𝑌))) ((oc‘𝐾)‘(((oc‘𝐾)‘𝑋) ((oc‘𝐾)‘𝑍)))) = ((𝑋 𝑌) (𝑋 𝑍)))
5448, 53eqtr2d 2778 . . 3 ((𝐾 ∈ OML ∧ (𝑋𝐵𝑌𝐵𝑍𝐵)) → ((𝑋 𝑌) (𝑋 𝑍)) = ((oc‘𝐾)‘((((oc‘𝐾)‘𝑋) ((oc‘𝐾)‘𝑌)) (((oc‘𝐾)‘𝑋) ((oc‘𝐾)‘𝑍)))))
55543adant3 1134 . 2 ((𝐾 ∈ OML ∧ (𝑋𝐵𝑌𝐵𝑍𝐵) ∧ (𝑋𝐶𝑌𝑋𝐶𝑍)) → ((𝑋 𝑌) (𝑋 𝑍)) = ((oc‘𝐾)‘((((oc‘𝐾)‘𝑋) ((oc‘𝐾)‘𝑌)) (((oc‘𝐾)‘𝑋) ((oc‘𝐾)‘𝑍)))))
5629, 42, 553eqtr4d 2787 1 ((𝐾 ∈ OML ∧ (𝑋𝐵𝑌𝐵𝑍𝐵) ∧ (𝑋𝐶𝑌𝑋𝐶𝑍)) → (𝑋 (𝑌 𝑍)) = ((𝑋 𝑌) (𝑋 𝑍)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 209  wa 399  w3a 1089   = wceq 1543  wcel 2110   class class class wbr 5053  cfv 6380  (class class class)co 7213  Basecbs 16760  occoc 16810  joincjn 17818  meetcmee 17819  Latclat 17937  OPcops 36923  cmccmtN 36924  OLcol 36925  OMLcoml 36926
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2016  ax-8 2112  ax-9 2120  ax-10 2141  ax-11 2158  ax-12 2175  ax-ext 2708  ax-rep 5179  ax-sep 5192  ax-nul 5199  ax-pow 5258  ax-pr 5322  ax-un 7523
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 848  df-3an 1091  df-tru 1546  df-fal 1556  df-ex 1788  df-nf 1792  df-sb 2071  df-mo 2539  df-eu 2568  df-clab 2715  df-cleq 2729  df-clel 2816  df-nfc 2886  df-ne 2941  df-ral 3066  df-rex 3067  df-reu 3068  df-rab 3070  df-v 3410  df-sbc 3695  df-csb 3812  df-dif 3869  df-un 3871  df-in 3873  df-ss 3883  df-nul 4238  df-if 4440  df-pw 4515  df-sn 4542  df-pr 4544  df-op 4548  df-uni 4820  df-iun 4906  df-br 5054  df-opab 5116  df-mpt 5136  df-id 5455  df-xp 5557  df-rel 5558  df-cnv 5559  df-co 5560  df-dm 5561  df-rn 5562  df-res 5563  df-ima 5564  df-iota 6338  df-fun 6382  df-fn 6383  df-f 6384  df-f1 6385  df-fo 6386  df-f1o 6387  df-fv 6388  df-riota 7170  df-ov 7216  df-oprab 7217  df-proset 17802  df-poset 17820  df-lub 17852  df-glb 17853  df-join 17854  df-meet 17855  df-p0 17931  df-lat 17938  df-oposet 36927  df-cmtN 36928  df-ol 36929  df-oml 36930
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator