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→ 𝐵 ) |
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→ 𝐵 ) |