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

Theorem ltrnco 34382
Description: The composition of two translations is a translation. Part of proof of Lemma G of [Crawley] p. 116, line 15 on p. 117. (Contributed by NM, 31-May-2013.)
Hypotheses
Ref Expression
ltrnco.h  |-  H  =  ( LHyp `  K
)
ltrnco.t  |-  T  =  ( ( LTrn `  K
) `  W )
Assertion
Ref Expression
ltrnco  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  F  e.  T  /\  G  e.  T
)  ->  ( F  o.  G )  e.  T
)

Proof of Theorem ltrnco
Dummy variables  q  p are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 simp1 988 . . 3  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  F  e.  T  /\  G  e.  T
)  ->  ( K  e.  HL  /\  W  e.  H ) )
2 ltrnco.h . . . . 5  |-  H  =  ( LHyp `  K
)
3 eqid 2443 . . . . 5  |-  ( (
LDil `  K ) `  W )  =  ( ( LDil `  K
) `  W )
4 ltrnco.t . . . . 5  |-  T  =  ( ( LTrn `  K
) `  W )
52, 3, 4ltrnldil 33785 . . . 4  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  F  e.  T
)  ->  F  e.  ( ( LDil `  K
) `  W )
)
653adant3 1008 . . 3  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  F  e.  T  /\  G  e.  T
)  ->  F  e.  ( ( LDil `  K
) `  W )
)
72, 3, 4ltrnldil 33785 . . . 4  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  G  e.  T
)  ->  G  e.  ( ( LDil `  K
) `  W )
)
873adant2 1007 . . 3  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  F  e.  T  /\  G  e.  T
)  ->  G  e.  ( ( LDil `  K
) `  W )
)
92, 3ldilco 33779 . . 3  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  F  e.  ( ( LDil `  K
) `  W )  /\  G  e.  (
( LDil `  K ) `  W ) )  -> 
( F  o.  G
)  e.  ( (
LDil `  K ) `  W ) )
101, 6, 8, 9syl3anc 1218 . 2  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  F  e.  T  /\  G  e.  T
)  ->  ( F  o.  G )  e.  ( ( LDil `  K
) `  W )
)
11 simp11 1018 . . . . 5  |-  ( ( ( ( K  e.  HL  /\  W  e.  H )  /\  F  e.  T  /\  G  e.  T )  /\  (
p  e.  ( Atoms `  K )  /\  q  e.  ( Atoms `  K )
)  /\  ( -.  p ( le `  K ) W  /\  -.  q ( le `  K ) W ) )  ->  ( K  e.  HL  /\  W  e.  H ) )
12 simp2l 1014 . . . . . 6  |-  ( ( ( ( K  e.  HL  /\  W  e.  H )  /\  F  e.  T  /\  G  e.  T )  /\  (
p  e.  ( Atoms `  K )  /\  q  e.  ( Atoms `  K )
)  /\  ( -.  p ( le `  K ) W  /\  -.  q ( le `  K ) W ) )  ->  p  e.  ( Atoms `  K )
)
13 simp3l 1016 . . . . . 6  |-  ( ( ( ( K  e.  HL  /\  W  e.  H )  /\  F  e.  T  /\  G  e.  T )  /\  (
p  e.  ( Atoms `  K )  /\  q  e.  ( Atoms `  K )
)  /\  ( -.  p ( le `  K ) W  /\  -.  q ( le `  K ) W ) )  ->  -.  p
( le `  K
) W )
1412, 13jca 532 . . . . 5  |-  ( ( ( ( K  e.  HL  /\  W  e.  H )  /\  F  e.  T  /\  G  e.  T )  /\  (
p  e.  ( Atoms `  K )  /\  q  e.  ( Atoms `  K )
)  /\  ( -.  p ( le `  K ) W  /\  -.  q ( le `  K ) W ) )  ->  ( p  e.  ( Atoms `  K )  /\  -.  p ( le
`  K ) W ) )
15 simp2r 1015 . . . . . 6  |-  ( ( ( ( K  e.  HL  /\  W  e.  H )  /\  F  e.  T  /\  G  e.  T )  /\  (
p  e.  ( Atoms `  K )  /\  q  e.  ( Atoms `  K )
)  /\  ( -.  p ( le `  K ) W  /\  -.  q ( le `  K ) W ) )  ->  q  e.  ( Atoms `  K )
)
16 simp3r 1017 . . . . . 6  |-  ( ( ( ( K  e.  HL  /\  W  e.  H )  /\  F  e.  T  /\  G  e.  T )  /\  (
p  e.  ( Atoms `  K )  /\  q  e.  ( Atoms `  K )
)  /\  ( -.  p ( le `  K ) W  /\  -.  q ( le `  K ) W ) )  ->  -.  q
( le `  K
) W )
1715, 16jca 532 . . . . 5  |-  ( ( ( ( K  e.  HL  /\  W  e.  H )  /\  F  e.  T  /\  G  e.  T )  /\  (
p  e.  ( Atoms `  K )  /\  q  e.  ( Atoms `  K )
)  /\  ( -.  p ( le `  K ) W  /\  -.  q ( le `  K ) W ) )  ->  ( q  e.  ( Atoms `  K )  /\  -.  q ( le
`  K ) W ) )
18 simp12 1019 . . . . 5  |-  ( ( ( ( K  e.  HL  /\  W  e.  H )  /\  F  e.  T  /\  G  e.  T )  /\  (
p  e.  ( Atoms `  K )  /\  q  e.  ( Atoms `  K )
)  /\  ( -.  p ( le `  K ) W  /\  -.  q ( le `  K ) W ) )  ->  F  e.  T )
19 simp13 1020 . . . . 5  |-  ( ( ( ( K  e.  HL  /\  W  e.  H )  /\  F  e.  T  /\  G  e.  T )  /\  (
p  e.  ( Atoms `  K )  /\  q  e.  ( Atoms `  K )
)  /\  ( -.  p ( le `  K ) W  /\  -.  q ( le `  K ) W ) )  ->  G  e.  T )
20 eqid 2443 . . . . . 6  |-  ( le
`  K )  =  ( le `  K
)
21 eqid 2443 . . . . . 6  |-  ( join `  K )  =  (
join `  K )
22 eqid 2443 . . . . . 6  |-  ( meet `  K )  =  (
meet `  K )
23 eqid 2443 . . . . . 6  |-  ( Atoms `  K )  =  (
Atoms `  K )
2420, 21, 22, 23, 2, 4cdlemg41 34381 . . . . 5  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( ( p  e.  ( Atoms `  K
)  /\  -.  p
( le `  K
) W )  /\  ( q  e.  (
Atoms `  K )  /\  -.  q ( le `  K ) W ) )  /\  ( F  e.  T  /\  G  e.  T ) )  -> 
( ( p (
join `  K )
( ( F  o.  G ) `  p
) ) ( meet `  K ) W )  =  ( ( q ( join `  K
) ( ( F  o.  G ) `  q ) ) (
meet `  K ) W ) )
2511, 14, 17, 18, 19, 24syl122anc 1227 . . . 4  |-  ( ( ( ( K  e.  HL  /\  W  e.  H )  /\  F  e.  T  /\  G  e.  T )  /\  (
p  e.  ( Atoms `  K )  /\  q  e.  ( Atoms `  K )
)  /\  ( -.  p ( le `  K ) W  /\  -.  q ( le `  K ) W ) )  ->  ( (
p ( join `  K
) ( ( F  o.  G ) `  p ) ) (
meet `  K ) W )  =  ( ( q ( join `  K ) ( ( F  o.  G ) `
 q ) ) ( meet `  K
) W ) )
26253exp 1186 . . 3  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  F  e.  T  /\  G  e.  T
)  ->  ( (
p  e.  ( Atoms `  K )  /\  q  e.  ( Atoms `  K )
)  ->  ( ( -.  p ( le `  K ) W  /\  -.  q ( le `  K ) W )  ->  ( ( p ( join `  K
) ( ( F  o.  G ) `  p ) ) (
meet `  K ) W )  =  ( ( q ( join `  K ) ( ( F  o.  G ) `
 q ) ) ( meet `  K
) W ) ) ) )
2726ralrimivv 2822 . 2  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  F  e.  T  /\  G  e.  T
)  ->  A. p  e.  ( Atoms `  K ) A. q  e.  ( Atoms `  K ) ( ( -.  p ( le `  K ) W  /\  -.  q
( le `  K
) W )  -> 
( ( p (
join `  K )
( ( F  o.  G ) `  p
) ) ( meet `  K ) W )  =  ( ( q ( join `  K
) ( ( F  o.  G ) `  q ) ) (
meet `  K ) W ) ) )
2820, 21, 22, 23, 2, 3, 4isltrn 33782 . . 3  |-  ( ( K  e.  HL  /\  W  e.  H )  ->  ( ( F  o.  G )  e.  T  <->  ( ( F  o.  G
)  e.  ( (
LDil `  K ) `  W )  /\  A. p  e.  ( Atoms `  K ) A. q  e.  ( Atoms `  K )
( ( -.  p
( le `  K
) W  /\  -.  q ( le `  K ) W )  ->  ( ( p ( join `  K
) ( ( F  o.  G ) `  p ) ) (
meet `  K ) W )  =  ( ( q ( join `  K ) ( ( F  o.  G ) `
 q ) ) ( meet `  K
) W ) ) ) ) )
29283ad2ant1 1009 . 2  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  F  e.  T  /\  G  e.  T
)  ->  ( ( F  o.  G )  e.  T  <->  ( ( F  o.  G )  e.  ( ( LDil `  K
) `  W )  /\  A. p  e.  (
Atoms `  K ) A. q  e.  ( Atoms `  K ) ( ( -.  p ( le
`  K ) W  /\  -.  q ( le `  K ) W )  ->  (
( p ( join `  K ) ( ( F  o.  G ) `
 p ) ) ( meet `  K
) W )  =  ( ( q (
join `  K )
( ( F  o.  G ) `  q
) ) ( meet `  K ) W ) ) ) ) )
3010, 27, 29mpbir2and 913 1  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  F  e.  T  /\  G  e.  T
)  ->  ( F  o.  G )  e.  T
)
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    -> wi 4    <-> wb 184    /\ wa 369    /\ w3a 965    = wceq 1369    e. wcel 1756   A.wral 2730   class class class wbr 4307    o. ccom 4859   ` cfv 5433  (class class class)co 6106   lecple 14260   joincjn 15129   meetcmee 15130   Atomscatm 32927   HLchlt 33014   LHypclh 33647   LDilcldil 33763   LTrncltrn 33764
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-8 1758  ax-9 1760  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2423  ax-rep 4418  ax-sep 4428  ax-nul 4436  ax-pow 4485  ax-pr 4546  ax-un 6387  ax-riotaBAD 32623
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 966  df-3an 967  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-eu 2257  df-mo 2258  df-clab 2430  df-cleq 2436  df-clel 2439  df-nfc 2577  df-ne 2622  df-nel 2623  df-ral 2735  df-rex 2736  df-reu 2737  df-rmo 2738  df-rab 2739  df-v 2989  df-sbc 3202  df-csb 3304  df-dif 3346  df-un 3348  df-in 3350  df-ss 3357  df-nul 3653  df-if 3807  df-pw 3877  df-sn 3893  df-pr 3895  df-op 3899  df-uni 4107  df-iun 4188  df-iin 4189  df-br 4308  df-opab 4366  df-mpt 4367  df-id 4651  df-xp 4861  df-rel 4862  df-cnv 4863  df-co 4864  df-dm 4865  df-rn 4866  df-res 4867  df-ima 4868  df-iota 5396  df-fun 5435  df-fn 5436  df-f 5437  df-f1 5438  df-fo 5439  df-f1o 5440  df-fv 5441  df-riota 6067  df-ov 6109  df-oprab 6110  df-mpt2 6111  df-1st 6592  df-2nd 6593  df-undef 6807  df-map 7231  df-poset 15131  df-plt 15143  df-lub 15159  df-glb 15160  df-join 15161  df-meet 15162  df-p0 15224  df-p1 15225  df-lat 15231  df-clat 15293  df-oposet 32840  df-ol 32842  df-oml 32843  df-covers 32930  df-ats 32931  df-atl 32962  df-cvlat 32986  df-hlat 33015  df-llines 33161  df-lplanes 33162  df-lvols 33163  df-lines 33164  df-psubsp 33166  df-pmap 33167  df-padd 33459  df-lhyp 33651  df-laut 33652  df-ldil 33767  df-ltrn 33768  df-trl 33822
This theorem is referenced by:  trlcocnv  34383  trlcoabs2N  34385  trlcoat  34386  trlconid  34388  trlcolem  34389  trlcone  34391  cdlemg44  34396  cdlemg46  34398  cdlemg47  34399  trljco  34403  tgrpgrplem  34412  tendoidcl  34432  tendococl  34435  tendoplcl2  34441  tendoplco2  34442  tendoplcl  34444  tendo0co2  34451  tendoicl  34459  cdlemh1  34478  cdlemh2  34479  cdlemh  34480  cdlemi2  34482  cdlemi  34483  cdlemk2  34495  cdlemk3  34496  cdlemk4  34497  cdlemk8  34501  cdlemk9  34502  cdlemk9bN  34503  cdlemkvcl  34505  cdlemk10  34506  cdlemk11  34512  cdlemk12  34513  cdlemk14  34517  cdlemk11u  34534  cdlemk12u  34535  cdlemk37  34577  cdlemkfid1N  34584  cdlemkid1  34585  cdlemk45  34610  cdlemk47  34612  cdlemk48  34613  cdlemk50  34615  cdlemk52  34617  cdlemk53a  34618  cdlemk54  34621  cdlemk55a  34622  cdlemk55u1  34628  cdlemk55u  34629  tendospcanN  34687  dvalveclem  34689  dialss  34710  dia2dimlem4  34731  dvhvaddcl  34759  diblss  34834  cdlemn3  34861  dihopelvalcpre  34912  dih1  34950  dihglbcpreN  34964  dihjatcclem3  35084  dihjatcclem4  35085
  Copyright terms: Public domain W3C validator