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

Theorem trlcoabs 33987
Description: Absorption into a composition by joining with trace. (Contributed by NM, 22-Jul-2013.)
Hypotheses
Ref Expression
trlcoabs.l  |-  .<_  =  ( le `  K )
trlcoabs.j  |-  .\/  =  ( join `  K )
trlcoabs.a  |-  A  =  ( Atoms `  K )
trlcoabs.h  |-  H  =  ( LHyp `  K
)
trlcoabs.t  |-  T  =  ( ( LTrn `  K
) `  W )
trlcoabs.r  |-  R  =  ( ( trL `  K
) `  W )
Assertion
Ref Expression
trlcoabs  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( F  e.  T  /\  G  e.  T )  /\  ( P  e.  A  /\  -.  P  .<_  W ) )  ->  ( (
( F  o.  G
) `  P )  .\/  ( R `  F
) )  =  ( ( G `  P
)  .\/  ( R `  F ) ) )

Proof of Theorem trlcoabs
StepHypRef Expression
1 trlcoabs.l . . . . 5  |-  .<_  =  ( le `  K )
2 trlcoabs.a . . . . 5  |-  A  =  ( Atoms `  K )
3 trlcoabs.h . . . . 5  |-  H  =  ( LHyp `  K
)
4 trlcoabs.t . . . . 5  |-  T  =  ( ( LTrn `  K
) `  W )
51, 2, 3, 4ltrncoval 33409 . . . 4  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( F  e.  T  /\  G  e.  T )  /\  P  e.  A )  ->  (
( F  o.  G
) `  P )  =  ( F `  ( G `  P ) ) )
653adant3r 1261 . . 3  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( F  e.  T  /\  G  e.  T )  /\  ( P  e.  A  /\  -.  P  .<_  W ) )  ->  ( ( F  o.  G ) `  P )  =  ( F `  ( G `
 P ) ) )
76oveq1d 6320 . 2  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( F  e.  T  /\  G  e.  T )  /\  ( P  e.  A  /\  -.  P  .<_  W ) )  ->  ( (
( F  o.  G
) `  P )  .\/  ( R `  F
) )  =  ( ( F `  ( G `  P )
)  .\/  ( R `  F ) ) )
8 simp1 1005 . . 3  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( F  e.  T  /\  G  e.  T )  /\  ( P  e.  A  /\  -.  P  .<_  W ) )  ->  ( K  e.  HL  /\  W  e.  H ) )
9 simp2l 1031 . . 3  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( F  e.  T  /\  G  e.  T )  /\  ( P  e.  A  /\  -.  P  .<_  W ) )  ->  F  e.  T )
101, 2, 3, 4ltrnel 33403 . . . 4  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  G  e.  T  /\  ( P  e.  A  /\  -.  P  .<_  W ) )  ->  ( ( G `  P )  e.  A  /\  -.  ( G `  P )  .<_  W ) )
11103adant2l 1258 . . 3  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( F  e.  T  /\  G  e.  T )  /\  ( P  e.  A  /\  -.  P  .<_  W ) )  ->  ( ( G `  P )  e.  A  /\  -.  ( G `  P )  .<_  W ) )
12 trlcoabs.j . . . 4  |-  .\/  =  ( join `  K )
13 trlcoabs.r . . . 4  |-  R  =  ( ( trL `  K
) `  W )
141, 12, 2, 3, 4, 13trljat3 33433 . . 3  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  F  e.  T  /\  ( ( G `  P )  e.  A  /\  -.  ( G `  P )  .<_  W ) )  ->  ( ( G `  P )  .\/  ( R `  F
) )  =  ( ( F `  ( G `  P )
)  .\/  ( R `  F ) ) )
158, 9, 11, 14syl3anc 1264 . 2  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( F  e.  T  /\  G  e.  T )  /\  ( P  e.  A  /\  -.  P  .<_  W ) )  ->  ( ( G `  P )  .\/  ( R `  F
) )  =  ( ( F `  ( G `  P )
)  .\/  ( R `  F ) ) )
167, 15eqtr4d 2473 1  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( F  e.  T  /\  G  e.  T )  /\  ( P  e.  A  /\  -.  P  .<_  W ) )  ->  ( (
( F  o.  G
) `  P )  .\/  ( R `  F
) )  =  ( ( G `  P
)  .\/  ( R `  F ) ) )
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    -> wi 4    /\ wa 370    /\ w3a 982    = wceq 1437    e. wcel 1870   class class class wbr 4426    o. ccom 4858   ` cfv 5601  (class class class)co 6305   lecple 15150   joincjn 16131   Atomscatm 32528   HLchlt 32615   LHypclh 33248   LTrncltrn 33365   trLctrl 33423
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-5 1751  ax-6 1797  ax-7 1841  ax-8 1872  ax-9 1874  ax-10 1889  ax-11 1894  ax-12 1907  ax-13 2055  ax-ext 2407  ax-rep 4538  ax-sep 4548  ax-nul 4556  ax-pow 4603  ax-pr 4661  ax-un 6597
This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-3an 984  df-tru 1440  df-ex 1660  df-nf 1664  df-sb 1790  df-eu 2270  df-mo 2271  df-clab 2415  df-cleq 2421  df-clel 2424  df-nfc 2579  df-ne 2627  df-ral 2787  df-rex 2788  df-reu 2789  df-rab 2791  df-v 3089  df-sbc 3306  df-csb 3402  df-dif 3445  df-un 3447  df-in 3449  df-ss 3456  df-nul 3768  df-if 3916  df-pw 3987  df-sn 4003  df-pr 4005  df-op 4009  df-uni 4223  df-iun 4304  df-iin 4305  df-br 4427  df-opab 4485  df-mpt 4486  df-id 4769  df-xp 4860  df-rel 4861  df-cnv 4862  df-co 4863  df-dm 4864  df-rn 4865  df-res 4866  df-ima 4867  df-iota 5565  df-fun 5603  df-fn 5604  df-f 5605  df-f1 5606  df-fo 5607  df-f1o 5608  df-fv 5609  df-riota 6267  df-ov 6308  df-oprab 6309  df-mpt2 6310  df-1st 6807  df-2nd 6808  df-map 7482  df-preset 16115  df-poset 16133  df-plt 16146  df-lub 16162  df-glb 16163  df-join 16164  df-meet 16165  df-p0 16227  df-p1 16228  df-lat 16234  df-clat 16296  df-oposet 32441  df-ol 32443  df-oml 32444  df-covers 32531  df-ats 32532  df-atl 32563  df-cvlat 32587  df-hlat 32616  df-psubsp 32767  df-pmap 32768  df-padd 33060  df-lhyp 33252  df-laut 33253  df-ldil 33368  df-ltrn 33369  df-trl 33424
This theorem is referenced by:  cdlemk48  34216
  Copyright terms: Public domain W3C validator