Metamath Proof Explorer


Theorem laut11

Description: One-to-one property of a lattice automorphism. (Contributed by NM, 20-May-2012)

Ref Expression
Hypotheses laut1o.b 𝐵 = ( Base ‘ 𝐾 )
laut1o.i 𝐼 = ( LAut ‘ 𝐾 )
Assertion laut11 ( ( ( 𝐾𝑉𝐹𝐼 ) ∧ ( 𝑋𝐵𝑌𝐵 ) ) → ( ( 𝐹𝑋 ) = ( 𝐹𝑌 ) ↔ 𝑋 = 𝑌 ) )

Proof

Step Hyp Ref Expression
1 laut1o.b 𝐵 = ( Base ‘ 𝐾 )
2 laut1o.i 𝐼 = ( LAut ‘ 𝐾 )
3 1 2 laut1o ( ( 𝐾𝑉𝐹𝐼 ) → 𝐹 : 𝐵1-1-onto𝐵 )
4 f1of1 ( 𝐹 : 𝐵1-1-onto𝐵𝐹 : 𝐵1-1𝐵 )
5 3 4 syl ( ( 𝐾𝑉𝐹𝐼 ) → 𝐹 : 𝐵1-1𝐵 )
6 f1fveq ( ( 𝐹 : 𝐵1-1𝐵 ∧ ( 𝑋𝐵𝑌𝐵 ) ) → ( ( 𝐹𝑋 ) = ( 𝐹𝑌 ) ↔ 𝑋 = 𝑌 ) )
7 5 6 sylan ( ( ( 𝐾𝑉𝐹𝐼 ) ∧ ( 𝑋𝐵𝑌𝐵 ) ) → ( ( 𝐹𝑋 ) = ( 𝐹𝑌 ) ↔ 𝑋 = 𝑌 ) )