Theorem ltrnco 41551

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.

Step	Hyp	Ref	Expression
1		simp1 1154	. . 3 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))
2		ltrnco.h	. . . . 5 ⊢ 𝐻 = (LHyp‘𝐾)
3		eqid 2765	. . . . 5 ⊢ ((LDil‘𝐾)‘𝑊) = ((LDil‘𝐾)‘𝑊)
4		ltrnco.t	. . . . 5 ⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊)
5	2, 3, 4	ltrnldil 40954	. . . 4 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇) → 𝐹 ∈ ((LDil‘𝐾)‘𝑊))
6	5	3adant3 1150	. . 3 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) → 𝐹 ∈ ((LDil‘𝐾)‘𝑊))
7	2, 3, 4	ltrnldil 40954	. . . 4 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐺 ∈ 𝑇) → 𝐺 ∈ ((LDil‘𝐾)‘𝑊))
8	7	3adant2 1149	. . 3 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) → 𝐺 ∈ ((LDil‘𝐾)‘𝑊))
9	2, 3	ldilco 40948	. . 3 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ ((LDil‘𝐾)‘𝑊) ∧ 𝐺 ∈ ((LDil‘𝐾)‘𝑊)) → (𝐹 ∘ 𝐺) ∈ ((LDil‘𝐾)‘𝑊))
10	1, 6, 8, 9	syl3anc 1398	. 2 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) → (𝐹 ∘ 𝐺) ∈ ((LDil‘𝐾)‘𝑊))
11		simp11 1222	. . . . 5 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ (𝑝 ∈ (Atoms‘𝐾) ∧ 𝑞 ∈ (Atoms‘𝐾)) ∧ (¬ 𝑝(le‘𝐾)𝑊 ∧ ¬ 𝑞(le‘𝐾)𝑊)) → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))
12		simp2l 1218	. . . . . 6 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ (𝑝 ∈ (Atoms‘𝐾) ∧ 𝑞 ∈ (Atoms‘𝐾)) ∧ (¬ 𝑝(le‘𝐾)𝑊 ∧ ¬ 𝑞(le‘𝐾)𝑊)) → 𝑝 ∈ (Atoms‘𝐾))
13		simp3l 1220	. . . . . 6 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ (𝑝 ∈ (Atoms‘𝐾) ∧ 𝑞 ∈ (Atoms‘𝐾)) ∧ (¬ 𝑝(le‘𝐾)𝑊 ∧ ¬ 𝑞(le‘𝐾)𝑊)) → ¬ 𝑝(le‘𝐾)𝑊)
14	12, 13	jca 521	. . . . 5 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ (𝑝 ∈ (Atoms‘𝐾) ∧ 𝑞 ∈ (Atoms‘𝐾)) ∧ (¬ 𝑝(le‘𝐾)𝑊 ∧ ¬ 𝑞(le‘𝐾)𝑊)) → (𝑝 ∈ (Atoms‘𝐾) ∧ ¬ 𝑝(le‘𝐾)𝑊))
15		simp2r 1219	. . . . . 6 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ (𝑝 ∈ (Atoms‘𝐾) ∧ 𝑞 ∈ (Atoms‘𝐾)) ∧ (¬ 𝑝(le‘𝐾)𝑊 ∧ ¬ 𝑞(le‘𝐾)𝑊)) → 𝑞 ∈ (Atoms‘𝐾))
16		simp3r 1221	. . . . . 6 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ (𝑝 ∈ (Atoms‘𝐾) ∧ 𝑞 ∈ (Atoms‘𝐾)) ∧ (¬ 𝑝(le‘𝐾)𝑊 ∧ ¬ 𝑞(le‘𝐾)𝑊)) → ¬ 𝑞(le‘𝐾)𝑊)
17	15, 16	jca 521	. . . . 5 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ (𝑝 ∈ (Atoms‘𝐾) ∧ 𝑞 ∈ (Atoms‘𝐾)) ∧ (¬ 𝑝(le‘𝐾)𝑊 ∧ ¬ 𝑞(le‘𝐾)𝑊)) → (𝑞 ∈ (Atoms‘𝐾) ∧ ¬ 𝑞(le‘𝐾)𝑊))
18		simp12 1223	. . . . 5 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ (𝑝 ∈ (Atoms‘𝐾) ∧ 𝑞 ∈ (Atoms‘𝐾)) ∧ (¬ 𝑝(le‘𝐾)𝑊 ∧ ¬ 𝑞(le‘𝐾)𝑊)) → 𝐹 ∈ 𝑇)
19		simp13 1224	. . . . 5 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ (𝑝 ∈ (Atoms‘𝐾) ∧ 𝑞 ∈ (Atoms‘𝐾)) ∧ (¬ 𝑝(le‘𝐾)𝑊 ∧ ¬ 𝑞(le‘𝐾)𝑊)) → 𝐺 ∈ 𝑇)
20		eqid 2765	. . . . . 6 ⊢ (le‘𝐾) = (le‘𝐾)
21		eqid 2765	. . . . . 6 ⊢ (join‘𝐾) = (join‘𝐾)
22		eqid 2765	. . . . . 6 ⊢ (meet‘𝐾) = (meet‘𝐾)
23		eqid 2765	. . . . . 6 ⊢ (Atoms‘𝐾) = (Atoms‘𝐾)
24	20, 21, 22, 23, 2, 4	cdlemg41 41550	. . . . 5 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ ((𝑝 ∈ (Atoms‘𝐾) ∧ ¬ 𝑝(le‘𝐾)𝑊) ∧ (𝑞 ∈ (Atoms‘𝐾) ∧ ¬ 𝑞(le‘𝐾)𝑊)) ∧ (𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇)) → ((𝑝(join‘𝐾)((𝐹 ∘ 𝐺)‘𝑝))(meet‘𝐾)𝑊) = ((𝑞(join‘𝐾)((𝐹 ∘ 𝐺)‘𝑞))(meet‘𝐾)𝑊))
25	11, 14, 17, 18, 19, 24	syl122anc 1406	. . . 4 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ (𝑝 ∈ (Atoms‘𝐾) ∧ 𝑞 ∈ (Atoms‘𝐾)) ∧ (¬ 𝑝(le‘𝐾)𝑊 ∧ ¬ 𝑞(le‘𝐾)𝑊)) → ((𝑝(join‘𝐾)((𝐹 ∘ 𝐺)‘𝑝))(meet‘𝐾)𝑊) = ((𝑞(join‘𝐾)((𝐹 ∘ 𝐺)‘𝑞))(meet‘𝐾)𝑊))
26	25	3exp 1137	. . 3 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) → ((𝑝 ∈ (Atoms‘𝐾) ∧ 𝑞 ∈ (Atoms‘𝐾)) → ((¬ 𝑝(le‘𝐾)𝑊 ∧ ¬ 𝑞(le‘𝐾)𝑊) → ((𝑝(join‘𝐾)((𝐹 ∘ 𝐺)‘𝑝))(meet‘𝐾)𝑊) = ((𝑞(join‘𝐾)((𝐹 ∘ 𝐺)‘𝑞))(meet‘𝐾)𝑊))))
27	26	ralrimivv 3208	. 2 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) → ∀𝑝 ∈ (Atoms‘𝐾)∀𝑞 ∈ (Atoms‘𝐾)((¬ 𝑝(le‘𝐾)𝑊 ∧ ¬ 𝑞(le‘𝐾)𝑊) → ((𝑝(join‘𝐾)((𝐹 ∘ 𝐺)‘𝑝))(meet‘𝐾)𝑊) = ((𝑞(join‘𝐾)((𝐹 ∘ 𝐺)‘𝑞))(meet‘𝐾)𝑊)))
28	20, 21, 22, 23, 2, 3, 4	isltrn 40951	. . 3 ⊢ ((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) → ((𝐹 ∘ 𝐺) ∈ 𝑇 ↔ ((𝐹 ∘ 𝐺) ∈ ((LDil‘𝐾)‘𝑊) ∧ ∀𝑝 ∈ (Atoms‘𝐾)∀𝑞 ∈ (Atoms‘𝐾)((¬ 𝑝(le‘𝐾)𝑊 ∧ ¬ 𝑞(le‘𝐾)𝑊) → ((𝑝(join‘𝐾)((𝐹 ∘ 𝐺)‘𝑝))(meet‘𝐾)𝑊) = ((𝑞(join‘𝐾)((𝐹 ∘ 𝐺)‘𝑞))(meet‘𝐾)𝑊)))))
29	28	3ad2ant1 1151	. 2 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) → ((𝐹 ∘ 𝐺) ∈ 𝑇 ↔ ((𝐹 ∘ 𝐺) ∈ ((LDil‘𝐾)‘𝑊) ∧ ∀𝑝 ∈ (Atoms‘𝐾)∀𝑞 ∈ (Atoms‘𝐾)((¬ 𝑝(le‘𝐾)𝑊 ∧ ¬ 𝑞(le‘𝐾)𝑊) → ((𝑝(join‘𝐾)((𝐹 ∘ 𝐺)‘𝑝))(meet‘𝐾)𝑊) = ((𝑞(join‘𝐾)((𝐹 ∘ 𝐺)‘𝑞))(meet‘𝐾)𝑊)))))
30	10, 27, 29	mpbir2and 726	1 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) → (𝐹 ∘ 𝐺) ∈ 𝑇)

This proof depends on syntax axioms:  ¬ wn 3   → wi 4   ↔ wb 209   ∧ wa 401   ∧ w3a 1103   = wceq 1570   ∈ wcel 2146  ∀wral 3081   class class class wbr 5111   ∘ ccom 5667  ‘cfv 6540  (class class class)co 7419  lecple 17339  joincjn 18389  meetcmee 18390  Atomscatm 40095  HLchlt 40182  LHypclh 40816  LDilcldil 40932  LTrncltrn 40933

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2148  ax-9 2156  ax-10 2179  ax-11 2195  ax-12 2216  ax-ext 2737  ax-rep 5240  ax-sep 5259  ax-nul 5271  ax-pow 5338  ax-pr 5406  ax-un 7742  ax-riotaBAD 39785

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2100  df-mo 2569  df-eu 2599  df-clab 2744  df-cleq 2757  df-clel 2840  df-nfc 2914  df-ne 2961  df-ral 3082  df-rex 3092  df-rmo 3371  df-reu 3372  df-rab 3419  df-v 3459  df-sbc 3747  df-csb 3855  df-dif 3909  df-un 3911  df-in 3913  df-ss 3923  df-nul 4287  df-if 4490  df-pw 4566  df-sn 4592  df-pr 4594  df-op 4598  df-uni 4875  df-iun 4960  df-iin 4961  df-br 5112  df-opab 5176  df-mpt 5195  df-id 5558  df-xp 5669  df-rel 5670  df-cnv 5671  df-co 5672  df-dm 5673  df-rn 5674  df-res 5675  df-ima 5676  df-iota 6496  df-fun 6542  df-fn 6543  df-f 6544  df-f1 6545  df-fo 6546  df-f1o 6547  df-fv 6548  df-riota 7376  df-ov 7422  df-oprab 7423  df-mpo 7424  df-1st 7992  df-2nd 7993  df-undef 8275  df-map 8832  df-proset 18372  df-poset 18391  df-plt 18406  df-lub 18422  df-glb 18423  df-join 18424  df-meet 18425  df-p0 18501  df-p1 18502  df-lat 18510  df-clat 18577  df-oposet 40008  df-ol 40010  df-oml 40011  df-covers 40098  df-ats 40099  df-atl 40130  df-cvlat 40154  df-hlat 40183  df-llines 40330  df-lplanes 40331  df-lvols 40332  df-lines 40333  df-psubsp 40335  df-pmap 40336  df-padd 40628  df-lhyp 40820  df-laut 40821  df-ldil 40936  df-ltrn 40937  df-trl 40991

This theorem is used by:  trlcocnv  41552  trlcoabs2N  41554  trlcoat  41555  trlconid  41557  trlcolem  41558  trlcone  41560  cdlemg44  41565  cdlemg46  41567  cdlemg47  41568  trljco  41572  tgrpgrplem  41581  tendoidcl  41601  tendococl  41604  tendoplcl2  41610  tendoplco2  41611  tendoplcl  41613  tendo0co2  41620  tendoicl  41628  cdlemh1  41647  cdlemh2  41648  cdlemh  41649  cdlemi2  41651  cdlemi  41652  cdlemk2  41664  cdlemk3  41665  cdlemk4  41666  cdlemk8  41670  cdlemk9  41671  cdlemk9bN  41672  cdlemkvcl  41674  cdlemk10  41675  cdlemk11  41681  cdlemk12  41682  cdlemk14  41686  cdlemk11u  41703  cdlemk12u  41704  cdlemk37  41746  cdlemkfid1N  41753  cdlemkid1  41754  cdlemk45  41779  cdlemk47  41781  cdlemk48  41782  cdlemk50  41784  cdlemk52  41786  cdlemk53a  41787  cdlemk54  41790  cdlemk55a  41791  cdlemk55u1  41797  cdlemk55u  41798  tendospcanN  41855  dvalveclem  41857  dialss  41878  dia2dimlem4  41899  dvhvaddcl  41927  diblss  42002  cdlemn3  42029  dihopelvalcpre  42080  dih1  42118  dihglbcpreN  42132  dihjatcclem3  42252  dihjatcclem4  42253