Theorem ltrn1o 37750

Description: A lattice translation is a one-to-one onto function. (Contributed by NM, 20-May-2012.)

Hypotheses

Ref	Expression
ltrn1o.b	⊢ 𝐵 = (Base‘𝐾)
ltrn1o.h	⊢ 𝐻 = (LHyp‘𝐾)
ltrn1o.t	⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊)

Assertion

Ref	Expression
ltrn1o	⊢ (((𝐾 ∈ 𝑉 ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇) → 𝐹:𝐵–1-1-onto→𝐵)

Proof of Theorem ltrn1o

Step	Hyp	Ref	Expression
1		simpll 767	. 2 ⊢ (((𝐾 ∈ 𝑉 ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇) → 𝐾 ∈ 𝑉)
2		ltrn1o.h	. . 3 ⊢ 𝐻 = (LHyp‘𝐾)
3		eqid 2738	. . 3 ⊢ (LAut‘𝐾) = (LAut‘𝐾)
4		ltrn1o.t	. . 3 ⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊)
5	2, 3, 4	ltrnlaut 37749	. 2 ⊢ (((𝐾 ∈ 𝑉 ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇) → 𝐹 ∈ (LAut‘𝐾))
6		ltrn1o.b	. . 3 ⊢ 𝐵 = (Base‘𝐾)
7	6, 3	laut1o 37711	. 2 ⊢ ((𝐾 ∈ 𝑉 ∧ 𝐹 ∈ (LAut‘𝐾)) → 𝐹:𝐵–1-1-onto→𝐵)
8	1, 5, 7	syl2anc 587	1 ⊢ (((𝐾 ∈ 𝑉 ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇) → 𝐹:𝐵–1-1-onto→𝐵)

Syntax hints:   → wi 4   ∧ wa 399   = wceq 1542   ∈ wcel 2113  –1-1-onto→wf1o 6332  ‘cfv 6333  Basecbs 16579  LHypclh 37610  LAutclaut 37611  LTrncltrn 37727

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1916  ax-6 1974  ax-7 2019  ax-8 2115  ax-9 2123  ax-10 2144  ax-11 2161  ax-12 2178  ax-ext 2710  ax-rep 5151  ax-sep 5164  ax-nul 5171  ax-pow 5229  ax-pr 5293  ax-un 7473

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 847  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1787  df-nf 1791  df-sb 2074  df-mo 2540  df-eu 2570  df-clab 2717  df-cleq 2730  df-clel 2811  df-nfc 2881  df-ne 2935  df-ral 3058  df-rex 3059  df-reu 3060  df-rab 3062  df-v 3399  df-sbc 3680  df-csb 3789  df-dif 3844  df-un 3846  df-in 3848  df-ss 3858  df-nul 4210  df-if 4412  df-pw 4487  df-sn 4514  df-pr 4516  df-op 4520  df-uni 4794  df-iun 4880  df-br 5028  df-opab 5090  df-mpt 5108  df-id 5425  df-xp 5525  df-rel 5526  df-cnv 5527  df-co 5528  df-dm 5529  df-rn 5530  df-res 5531  df-ima 5532  df-iota 6291  df-fun 6335  df-fn 6336  df-f 6337  df-f1 6338  df-fo 6339  df-f1o 6340  df-fv 6341  df-ov 7167  df-oprab 7168  df-mpo 7169  df-map 8432  df-laut 37615  df-ldil 37730  df-ltrn 37731

This theorem is referenced by:  ltrncnvnid  37753  ltrncoidN  37754  ltrnid  37761  ltrncnvatb  37764  ltrncnvel  37768  ltrncoval  37771  ltrncnv  37772  ltrneq2  37774  trlcnv  37791  ltrniotacnvval  38208  cdlemg17h  38294  trlcoabs2N  38348  trlcoat  38349  trlcone  38354  cdlemg47a  38360  cdlemg46  38361  cdlemg47  38362  trljco  38366  tgrpgrplem  38375  tendo0pl  38417  tendoipl  38423  cdlemi2  38445  cdlemk2  38458  cdlemk4  38460  cdlemk8  38464  cdlemkid2  38550  cdlemk45  38573  cdlemk53b  38582  cdlemk53  38583  cdlemk55a  38585  tendocnv  38647  dvhgrp  38733  dvhopN  38742  cdlemn3  38823  cdlemn8  38830  cdlemn9  38831  dihordlem7b  38841  dihopelvalcpre  38874  dihmeetlem1N  38916  dihglblem5apreN  38917