This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem ldil1o

Description: A lattice dilation is a one-to-one onto function. (Contributed by NM, 19-Apr-2013)

Ref Expression
Hypotheses ldil1o.b ⊢ B = Base K
ldil1o.h ⊢ H = LHyp ⁡ K
ldil1o.d ⊢ D = LDil ⁡ K ⁡ W
Assertion ldil1o ⊢ K ∈ V ∧ W ∈ H ∧ F ∈ D → F : B ⟶ 1-1 onto B

Proof

Step Hyp Ref Expression
1 ldil1o.b ⊢ B = Base K
2 ldil1o.h ⊢ H = LHyp ⁡ K
3 ldil1o.d ⊢ D = LDil ⁡ K ⁡ W
4 simpll ⊢ K ∈ V ∧ W ∈ H ∧ F ∈ D → K ∈ V
5 eqid ⊢ LAut ⁡ K = LAut ⁡ K
6 2 5 3 ldillaut ⊢ K ∈ V ∧ W ∈ H ∧ F ∈ D → F ∈ LAut ⁡ K
7 1 5 laut1o ⊢ K ∈ V ∧ F ∈ LAut ⁡ K → F : B ⟶ 1-1 onto B
8 4 6 7 syl2anc ⊢ K ∈ V ∧ W ∈ H ∧ F ∈ D → F : B ⟶ 1-1 onto B