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 𝐵 = ( Base ‘ 𝐾 )
ldil1o.h 𝐻 = ( LHyp ‘ 𝐾 )
ldil1o.d 𝐷 = ( ( LDil ‘ 𝐾 ) ‘ 𝑊 )
Assertion ldil1o ( ( ( 𝐾𝑉𝑊𝐻 ) ∧ 𝐹𝐷 ) → 𝐹 : 𝐵1-1-onto𝐵 )

Proof

Step Hyp Ref Expression
1 ldil1o.b 𝐵 = ( Base ‘ 𝐾 )
2 ldil1o.h 𝐻 = ( LHyp ‘ 𝐾 )
3 ldil1o.d 𝐷 = ( ( LDil ‘ 𝐾 ) ‘ 𝑊 )
4 simpll ( ( ( 𝐾𝑉𝑊𝐻 ) ∧ 𝐹𝐷 ) → 𝐾𝑉 )
5 eqid ( LAut ‘ 𝐾 ) = ( LAut ‘ 𝐾 )
6 2 5 3 ldillaut ( ( ( 𝐾𝑉𝑊𝐻 ) ∧ 𝐹𝐷 ) → 𝐹 ∈ ( LAut ‘ 𝐾 ) )
7 1 5 laut1o ( ( 𝐾𝑉𝐹 ∈ ( LAut ‘ 𝐾 ) ) → 𝐹 : 𝐵1-1-onto𝐵 )
8 4 6 7 syl2anc ( ( ( 𝐾𝑉𝑊𝐻 ) ∧ 𝐹𝐷 ) → 𝐹 : 𝐵1-1-onto𝐵 )