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

Theorem olm11 35303
Description: The meet of an ortholattice element with one equals itself. (chm1i 28871 analog.) (Contributed by NM, 22-May-2012.)
Hypotheses
Ref Expression
olm1.b 𝐵 = (Base‘𝐾)
olm1.m = (meet‘𝐾)
olm1.u 1 = (1.‘𝐾)
Assertion
Ref Expression
olm11 ((𝐾 ∈ OL ∧ 𝑋𝐵) → (𝑋 1 ) = 𝑋)

Proof of Theorem olm11
StepHypRef Expression
1 olop 35290 . . . . . . 7 (𝐾 ∈ OL → 𝐾 ∈ OP)
21adantr 474 . . . . . 6 ((𝐾 ∈ OL ∧ 𝑋𝐵) → 𝐾 ∈ OP)
3 eqid 2826 . . . . . . 7 (0.‘𝐾) = (0.‘𝐾)
4 olm1.u . . . . . . 7 1 = (1.‘𝐾)
5 eqid 2826 . . . . . . 7 (oc‘𝐾) = (oc‘𝐾)
63, 4, 5opoc1 35278 . . . . . 6 (𝐾 ∈ OP → ((oc‘𝐾)‘ 1 ) = (0.‘𝐾))
72, 6syl 17 . . . . 5 ((𝐾 ∈ OL ∧ 𝑋𝐵) → ((oc‘𝐾)‘ 1 ) = (0.‘𝐾))
87oveq2d 6922 . . . 4 ((𝐾 ∈ OL ∧ 𝑋𝐵) → (((oc‘𝐾)‘𝑋)(join‘𝐾)((oc‘𝐾)‘ 1 )) = (((oc‘𝐾)‘𝑋)(join‘𝐾)(0.‘𝐾)))
9 olm1.b . . . . . . 7 𝐵 = (Base‘𝐾)
109, 5opoccl 35270 . . . . . 6 ((𝐾 ∈ OP ∧ 𝑋𝐵) → ((oc‘𝐾)‘𝑋) ∈ 𝐵)
111, 10sylan 577 . . . . 5 ((𝐾 ∈ OL ∧ 𝑋𝐵) → ((oc‘𝐾)‘𝑋) ∈ 𝐵)
12 eqid 2826 . . . . . 6 (join‘𝐾) = (join‘𝐾)
139, 12, 3olj01 35301 . . . . 5 ((𝐾 ∈ OL ∧ ((oc‘𝐾)‘𝑋) ∈ 𝐵) → (((oc‘𝐾)‘𝑋)(join‘𝐾)(0.‘𝐾)) = ((oc‘𝐾)‘𝑋))
1411, 13syldan 587 . . . 4 ((𝐾 ∈ OL ∧ 𝑋𝐵) → (((oc‘𝐾)‘𝑋)(join‘𝐾)(0.‘𝐾)) = ((oc‘𝐾)‘𝑋))
158, 14eqtrd 2862 . . 3 ((𝐾 ∈ OL ∧ 𝑋𝐵) → (((oc‘𝐾)‘𝑋)(join‘𝐾)((oc‘𝐾)‘ 1 )) = ((oc‘𝐾)‘𝑋))
1615fveq2d 6438 . 2 ((𝐾 ∈ OL ∧ 𝑋𝐵) → ((oc‘𝐾)‘(((oc‘𝐾)‘𝑋)(join‘𝐾)((oc‘𝐾)‘ 1 ))) = ((oc‘𝐾)‘((oc‘𝐾)‘𝑋)))
179, 4op1cl 35261 . . . 4 (𝐾 ∈ OP → 1𝐵)
182, 17syl 17 . . 3 ((𝐾 ∈ OL ∧ 𝑋𝐵) → 1𝐵)
19 olm1.m . . . 4 = (meet‘𝐾)
209, 12, 19, 5oldmj4 35300 . . 3 ((𝐾 ∈ OL ∧ 𝑋𝐵1𝐵) → ((oc‘𝐾)‘(((oc‘𝐾)‘𝑋)(join‘𝐾)((oc‘𝐾)‘ 1 ))) = (𝑋 1 ))
2118, 20mpd3an3 1592 . 2 ((𝐾 ∈ OL ∧ 𝑋𝐵) → ((oc‘𝐾)‘(((oc‘𝐾)‘𝑋)(join‘𝐾)((oc‘𝐾)‘ 1 ))) = (𝑋 1 ))
229, 5opococ 35271 . . 3 ((𝐾 ∈ OP ∧ 𝑋𝐵) → ((oc‘𝐾)‘((oc‘𝐾)‘𝑋)) = 𝑋)
231, 22sylan 577 . 2 ((𝐾 ∈ OL ∧ 𝑋𝐵) → ((oc‘𝐾)‘((oc‘𝐾)‘𝑋)) = 𝑋)
2416, 21, 233eqtr3d 2870 1 ((𝐾 ∈ OL ∧ 𝑋𝐵) → (𝑋 1 ) = 𝑋)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 386   = wceq 1658  wcel 2166  cfv 6124  (class class class)co 6906  Basecbs 16223  occoc 16314  joincjn 17298  meetcmee 17299  0.cp0 17391  1.cp1 17392  OPcops 35248  OLcol 35250
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1896  ax-4 1910  ax-5 2011  ax-6 2077  ax-7 2114  ax-8 2168  ax-9 2175  ax-10 2194  ax-11 2209  ax-12 2222  ax-13 2391  ax-ext 2804  ax-rep 4995  ax-sep 5006  ax-nul 5014  ax-pow 5066  ax-pr 5128  ax-un 7210
This theorem depends on definitions:  df-bi 199  df-an 387  df-or 881  df-3an 1115  df-tru 1662  df-ex 1881  df-nf 1885  df-sb 2070  df-mo 2606  df-eu 2641  df-clab 2813  df-cleq 2819  df-clel 2822  df-nfc 2959  df-ne 3001  df-ral 3123  df-rex 3124  df-reu 3125  df-rab 3127  df-v 3417  df-sbc 3664  df-csb 3759  df-dif 3802  df-un 3804  df-in 3806  df-ss 3813  df-nul 4146  df-if 4308  df-pw 4381  df-sn 4399  df-pr 4401  df-op 4405  df-uni 4660  df-iun 4743  df-br 4875  df-opab 4937  df-mpt 4954  df-id 5251  df-xp 5349  df-rel 5350  df-cnv 5351  df-co 5352  df-dm 5353  df-rn 5354  df-res 5355  df-ima 5356  df-iota 6087  df-fun 6126  df-fn 6127  df-f 6128  df-f1 6129  df-fo 6130  df-f1o 6131  df-fv 6132  df-riota 6867  df-ov 6909  df-oprab 6910  df-proset 17282  df-poset 17300  df-lub 17328  df-glb 17329  df-join 17330  df-meet 17331  df-p0 17393  df-p1 17394  df-lat 17400  df-oposet 35252  df-ol 35254
This theorem is referenced by:  olm12  35304  lhpmcvr3  36101  trljat1  36242  trljat2  36243  cdlemc1  36267  cdlemc6  36272  cdleme0cp  36290  cdleme0cq  36291  cdleme1  36303  cdleme4  36314  cdleme5  36316  cdleme8  36326  cdleme9  36329  cdleme10  36330  cdleme20c  36387  cdleme20j  36394  cdleme22e  36420  cdleme22eALTN  36421  cdleme30a  36454  cdleme35b  36526  cdleme35e  36529  cdleme42a  36547  trlcoabs2N  36798  trlcolem  36802  cdlemi1  36894  cdlemk4  36910  dia2dimlem1  37140  cdlemn10  37282  dihglbcpreN  37376
  Copyright terms: Public domain W3C validator