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

Theorem ltrnco 34849
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 𝐻 = (LHyp‘𝐾)
ltrnco.t 𝑇 = ((LTrn‘𝐾)‘𝑊)
Assertion
Ref Expression
ltrnco (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝐹𝑇𝐺𝑇) → (𝐹𝐺) ∈ 𝑇)

Proof of Theorem ltrnco
Dummy variables 𝑞 𝑝 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 simp1 1053 . . 3 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝐹𝑇𝐺𝑇) → (𝐾 ∈ HL ∧ 𝑊𝐻))
2 ltrnco.h . . . . 5 𝐻 = (LHyp‘𝐾)
3 eqid 2609 . . . . 5 ((LDil‘𝐾)‘𝑊) = ((LDil‘𝐾)‘𝑊)
4 ltrnco.t . . . . 5 𝑇 = ((LTrn‘𝐾)‘𝑊)
52, 3, 4ltrnldil 34250 . . . 4 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝐹𝑇) → 𝐹 ∈ ((LDil‘𝐾)‘𝑊))
653adant3 1073 . . 3 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝐹𝑇𝐺𝑇) → 𝐹 ∈ ((LDil‘𝐾)‘𝑊))
72, 3, 4ltrnldil 34250 . . . 4 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝐺𝑇) → 𝐺 ∈ ((LDil‘𝐾)‘𝑊))
873adant2 1072 . . 3 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝐹𝑇𝐺𝑇) → 𝐺 ∈ ((LDil‘𝐾)‘𝑊))
92, 3ldilco 34244 . . 3 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝐹 ∈ ((LDil‘𝐾)‘𝑊) ∧ 𝐺 ∈ ((LDil‘𝐾)‘𝑊)) → (𝐹𝐺) ∈ ((LDil‘𝐾)‘𝑊))
101, 6, 8, 9syl3anc 1317 . 2 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝐹𝑇𝐺𝑇) → (𝐹𝐺) ∈ ((LDil‘𝐾)‘𝑊))
11 simp11 1083 . . . . 5 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝐹𝑇𝐺𝑇) ∧ (𝑝 ∈ (Atoms‘𝐾) ∧ 𝑞 ∈ (Atoms‘𝐾)) ∧ (¬ 𝑝(le‘𝐾)𝑊 ∧ ¬ 𝑞(le‘𝐾)𝑊)) → (𝐾 ∈ HL ∧ 𝑊𝐻))
12 simp2l 1079 . . . . . 6 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝐹𝑇𝐺𝑇) ∧ (𝑝 ∈ (Atoms‘𝐾) ∧ 𝑞 ∈ (Atoms‘𝐾)) ∧ (¬ 𝑝(le‘𝐾)𝑊 ∧ ¬ 𝑞(le‘𝐾)𝑊)) → 𝑝 ∈ (Atoms‘𝐾))
13 simp3l 1081 . . . . . 6 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝐹𝑇𝐺𝑇) ∧ (𝑝 ∈ (Atoms‘𝐾) ∧ 𝑞 ∈ (Atoms‘𝐾)) ∧ (¬ 𝑝(le‘𝐾)𝑊 ∧ ¬ 𝑞(le‘𝐾)𝑊)) → ¬ 𝑝(le‘𝐾)𝑊)
1412, 13jca 552 . . . . 5 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝐹𝑇𝐺𝑇) ∧ (𝑝 ∈ (Atoms‘𝐾) ∧ 𝑞 ∈ (Atoms‘𝐾)) ∧ (¬ 𝑝(le‘𝐾)𝑊 ∧ ¬ 𝑞(le‘𝐾)𝑊)) → (𝑝 ∈ (Atoms‘𝐾) ∧ ¬ 𝑝(le‘𝐾)𝑊))
15 simp2r 1080 . . . . . 6 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝐹𝑇𝐺𝑇) ∧ (𝑝 ∈ (Atoms‘𝐾) ∧ 𝑞 ∈ (Atoms‘𝐾)) ∧ (¬ 𝑝(le‘𝐾)𝑊 ∧ ¬ 𝑞(le‘𝐾)𝑊)) → 𝑞 ∈ (Atoms‘𝐾))
16 simp3r 1082 . . . . . 6 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝐹𝑇𝐺𝑇) ∧ (𝑝 ∈ (Atoms‘𝐾) ∧ 𝑞 ∈ (Atoms‘𝐾)) ∧ (¬ 𝑝(le‘𝐾)𝑊 ∧ ¬ 𝑞(le‘𝐾)𝑊)) → ¬ 𝑞(le‘𝐾)𝑊)
1715, 16jca 552 . . . . 5 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝐹𝑇𝐺𝑇) ∧ (𝑝 ∈ (Atoms‘𝐾) ∧ 𝑞 ∈ (Atoms‘𝐾)) ∧ (¬ 𝑝(le‘𝐾)𝑊 ∧ ¬ 𝑞(le‘𝐾)𝑊)) → (𝑞 ∈ (Atoms‘𝐾) ∧ ¬ 𝑞(le‘𝐾)𝑊))
18 simp12 1084 . . . . 5 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝐹𝑇𝐺𝑇) ∧ (𝑝 ∈ (Atoms‘𝐾) ∧ 𝑞 ∈ (Atoms‘𝐾)) ∧ (¬ 𝑝(le‘𝐾)𝑊 ∧ ¬ 𝑞(le‘𝐾)𝑊)) → 𝐹𝑇)
19 simp13 1085 . . . . 5 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝐹𝑇𝐺𝑇) ∧ (𝑝 ∈ (Atoms‘𝐾) ∧ 𝑞 ∈ (Atoms‘𝐾)) ∧ (¬ 𝑝(le‘𝐾)𝑊 ∧ ¬ 𝑞(le‘𝐾)𝑊)) → 𝐺𝑇)
20 eqid 2609 . . . . . 6 (le‘𝐾) = (le‘𝐾)
21 eqid 2609 . . . . . 6 (join‘𝐾) = (join‘𝐾)
22 eqid 2609 . . . . . 6 (meet‘𝐾) = (meet‘𝐾)
23 eqid 2609 . . . . . 6 (Atoms‘𝐾) = (Atoms‘𝐾)
2420, 21, 22, 23, 2, 4cdlemg41 34848 . . . . 5 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ ((𝑝 ∈ (Atoms‘𝐾) ∧ ¬ 𝑝(le‘𝐾)𝑊) ∧ (𝑞 ∈ (Atoms‘𝐾) ∧ ¬ 𝑞(le‘𝐾)𝑊)) ∧ (𝐹𝑇𝐺𝑇)) → ((𝑝(join‘𝐾)((𝐹𝐺)‘𝑝))(meet‘𝐾)𝑊) = ((𝑞(join‘𝐾)((𝐹𝐺)‘𝑞))(meet‘𝐾)𝑊))
2511, 14, 17, 18, 19, 24syl122anc 1326 . . . 4 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝐹𝑇𝐺𝑇) ∧ (𝑝 ∈ (Atoms‘𝐾) ∧ 𝑞 ∈ (Atoms‘𝐾)) ∧ (¬ 𝑝(le‘𝐾)𝑊 ∧ ¬ 𝑞(le‘𝐾)𝑊)) → ((𝑝(join‘𝐾)((𝐹𝐺)‘𝑝))(meet‘𝐾)𝑊) = ((𝑞(join‘𝐾)((𝐹𝐺)‘𝑞))(meet‘𝐾)𝑊))
26253exp 1255 . . 3 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝐹𝑇𝐺𝑇) → ((𝑝 ∈ (Atoms‘𝐾) ∧ 𝑞 ∈ (Atoms‘𝐾)) → ((¬ 𝑝(le‘𝐾)𝑊 ∧ ¬ 𝑞(le‘𝐾)𝑊) → ((𝑝(join‘𝐾)((𝐹𝐺)‘𝑝))(meet‘𝐾)𝑊) = ((𝑞(join‘𝐾)((𝐹𝐺)‘𝑞))(meet‘𝐾)𝑊))))
2726ralrimivv 2952 . 2 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝐹𝑇𝐺𝑇) → ∀𝑝 ∈ (Atoms‘𝐾)∀𝑞 ∈ (Atoms‘𝐾)((¬ 𝑝(le‘𝐾)𝑊 ∧ ¬ 𝑞(le‘𝐾)𝑊) → ((𝑝(join‘𝐾)((𝐹𝐺)‘𝑝))(meet‘𝐾)𝑊) = ((𝑞(join‘𝐾)((𝐹𝐺)‘𝑞))(meet‘𝐾)𝑊)))
2820, 21, 22, 23, 2, 3, 4isltrn 34247 . . 3 ((𝐾 ∈ HL ∧ 𝑊𝐻) → ((𝐹𝐺) ∈ 𝑇 ↔ ((𝐹𝐺) ∈ ((LDil‘𝐾)‘𝑊) ∧ ∀𝑝 ∈ (Atoms‘𝐾)∀𝑞 ∈ (Atoms‘𝐾)((¬ 𝑝(le‘𝐾)𝑊 ∧ ¬ 𝑞(le‘𝐾)𝑊) → ((𝑝(join‘𝐾)((𝐹𝐺)‘𝑝))(meet‘𝐾)𝑊) = ((𝑞(join‘𝐾)((𝐹𝐺)‘𝑞))(meet‘𝐾)𝑊)))))
29283ad2ant1 1074 . 2 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝐹𝑇𝐺𝑇) → ((𝐹𝐺) ∈ 𝑇 ↔ ((𝐹𝐺) ∈ ((LDil‘𝐾)‘𝑊) ∧ ∀𝑝 ∈ (Atoms‘𝐾)∀𝑞 ∈ (Atoms‘𝐾)((¬ 𝑝(le‘𝐾)𝑊 ∧ ¬ 𝑞(le‘𝐾)𝑊) → ((𝑝(join‘𝐾)((𝐹𝐺)‘𝑝))(meet‘𝐾)𝑊) = ((𝑞(join‘𝐾)((𝐹𝐺)‘𝑞))(meet‘𝐾)𝑊)))))
3010, 27, 29mpbir2and 958 1 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝐹𝑇𝐺𝑇) → (𝐹𝐺) ∈ 𝑇)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 194  wa 382  w3a 1030   = wceq 1474  wcel 1976  wral 2895   class class class wbr 4577  ccom 5032  cfv 5790  (class class class)co 6527  lecple 15724  joincjn 16716  meetcmee 16717  Atomscatm 33392  HLchlt 33479  LHypclh 34112  LDilcldil 34228  LTrncltrn 34229
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1712  ax-4 1727  ax-5 1826  ax-6 1874  ax-7 1921  ax-8 1978  ax-9 1985  ax-10 2005  ax-11 2020  ax-12 2033  ax-13 2233  ax-ext 2589  ax-rep 4693  ax-sep 4703  ax-nul 4712  ax-pow 4764  ax-pr 4828  ax-un 6825  ax-riotaBAD 33081
This theorem depends on definitions:  df-bi 195  df-or 383  df-an 384  df-3or 1031  df-3an 1032  df-tru 1477  df-ex 1695  df-nf 1700  df-sb 1867  df-eu 2461  df-mo 2462  df-clab 2596  df-cleq 2602  df-clel 2605  df-nfc 2739  df-ne 2781  df-nel 2782  df-ral 2900  df-rex 2901  df-reu 2902  df-rmo 2903  df-rab 2904  df-v 3174  df-sbc 3402  df-csb 3499  df-dif 3542  df-un 3544  df-in 3546  df-ss 3553  df-nul 3874  df-if 4036  df-pw 4109  df-sn 4125  df-pr 4127  df-op 4131  df-uni 4367  df-iun 4451  df-iin 4452  df-br 4578  df-opab 4638  df-mpt 4639  df-id 4943  df-xp 5034  df-rel 5035  df-cnv 5036  df-co 5037  df-dm 5038  df-rn 5039  df-res 5040  df-ima 5041  df-iota 5754  df-fun 5792  df-fn 5793  df-f 5794  df-f1 5795  df-fo 5796  df-f1o 5797  df-fv 5798  df-riota 6489  df-ov 6530  df-oprab 6531  df-mpt2 6532  df-1st 7037  df-2nd 7038  df-undef 7264  df-map 7724  df-preset 16700  df-poset 16718  df-plt 16730  df-lub 16746  df-glb 16747  df-join 16748  df-meet 16749  df-p0 16811  df-p1 16812  df-lat 16818  df-clat 16880  df-oposet 33305  df-ol 33307  df-oml 33308  df-covers 33395  df-ats 33396  df-atl 33427  df-cvlat 33451  df-hlat 33480  df-llines 33626  df-lplanes 33627  df-lvols 33628  df-lines 33629  df-psubsp 33631  df-pmap 33632  df-padd 33924  df-lhyp 34116  df-laut 34117  df-ldil 34232  df-ltrn 34233  df-trl 34288
This theorem is referenced by:  trlcocnv  34850  trlcoabs2N  34852  trlcoat  34853  trlconid  34855  trlcolem  34856  trlcone  34858  cdlemg44  34863  cdlemg46  34865  cdlemg47  34866  trljco  34870  tgrpgrplem  34879  tendoidcl  34899  tendococl  34902  tendoplcl2  34908  tendoplco2  34909  tendoplcl  34911  tendo0co2  34918  tendoicl  34926  cdlemh1  34945  cdlemh2  34946  cdlemh  34947  cdlemi2  34949  cdlemi  34950  cdlemk2  34962  cdlemk3  34963  cdlemk4  34964  cdlemk8  34968  cdlemk9  34969  cdlemk9bN  34970  cdlemkvcl  34972  cdlemk10  34973  cdlemk11  34979  cdlemk12  34980  cdlemk14  34984  cdlemk11u  35001  cdlemk12u  35002  cdlemk37  35044  cdlemkfid1N  35051  cdlemkid1  35052  cdlemk45  35077  cdlemk47  35079  cdlemk48  35080  cdlemk50  35082  cdlemk52  35084  cdlemk53a  35085  cdlemk54  35088  cdlemk55a  35089  cdlemk55u1  35095  cdlemk55u  35096  tendospcanN  35154  dvalveclem  35156  dialss  35177  dia2dimlem4  35198  dvhvaddcl  35226  diblss  35301  cdlemn3  35328  dihopelvalcpre  35379  dih1  35417  dihglbcpreN  35431  dihjatcclem3  35551  dihjatcclem4  35552
  Copyright terms: Public domain W3C validator