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

Metamath Proof Explorer

Theorem lautcnv

Description: The converse of a lattice automorphism is a lattice automorphism. (Contributed by NM, 10-May-2013)

Ref Expression
Hypothesis lautcnv.i ⊢ 𝐼 = ( LAut ‘ 𝐾 )
Assertion lautcnv ( ( 𝐾 ∈ 𝑉 ∧ 𝐹 ∈ 𝐼 ) → ◡ 𝐹 ∈ 𝐼 )

Proof

Step Hyp Ref Expression
1 lautcnv.i ⊢ 𝐼 = ( LAut ‘ 𝐾 )
2 eqid ⊢ ( Base ‘ 𝐾 ) = ( Base ‘ 𝐾 )
3 2 1 laut1o ⊢ ( ( 𝐾 ∈ 𝑉 ∧ 𝐹 ∈ 𝐼 ) → 𝐹 : ( Base ‘ 𝐾 ) –1-1-onto→ ( Base ‘ 𝐾 ) )
4 f1ocnv ⊢ ( 𝐹 : ( Base ‘ 𝐾 ) –1-1-onto→ ( Base ‘ 𝐾 ) → ◡ 𝐹 : ( Base ‘ 𝐾 ) –1-1-onto→ ( Base ‘ 𝐾 ) )
5 3 4 syl ⊢ ( ( 𝐾 ∈ 𝑉 ∧ 𝐹 ∈ 𝐼 ) → ◡ 𝐹 : ( Base ‘ 𝐾 ) –1-1-onto→ ( Base ‘ 𝐾 ) )
6 eqid ⊢ ( le ‘ 𝐾 ) = ( le ‘ 𝐾 )
7 2 6 1 lautcnvle ⊢ ( ( ( 𝐾 ∈ 𝑉 ∧ 𝐹 ∈ 𝐼 ) ∧ ( 𝑥 ∈ ( Base ‘ 𝐾 ) ∧ 𝑦 ∈ ( Base ‘ 𝐾 ) ) ) → ( 𝑥 ( le ‘ 𝐾 ) 𝑦 ↔ ( ◡ 𝐹 ‘ 𝑥 ) ( le ‘ 𝐾 ) ( ◡ 𝐹 ‘ 𝑦 ) ) )
8 7 ralrimivva ⊢ ( ( 𝐾 ∈ 𝑉 ∧ 𝐹 ∈ 𝐼 ) → ∀ 𝑥 ∈ ( Base ‘ 𝐾 ) ∀ 𝑦 ∈ ( Base ‘ 𝐾 ) ( 𝑥 ( le ‘ 𝐾 ) 𝑦 ↔ ( ◡ 𝐹 ‘ 𝑥 ) ( le ‘ 𝐾 ) ( ◡ 𝐹 ‘ 𝑦 ) ) )
9 2 6 1 islaut ⊢ ( 𝐾 ∈ 𝑉 → ( ◡ 𝐹 ∈ 𝐼 ↔ ( ◡ 𝐹 : ( Base ‘ 𝐾 ) –1-1-onto→ ( Base ‘ 𝐾 ) ∧ ∀ 𝑥 ∈ ( Base ‘ 𝐾 ) ∀ 𝑦 ∈ ( Base ‘ 𝐾 ) ( 𝑥 ( le ‘ 𝐾 ) 𝑦 ↔ ( ◡ 𝐹 ‘ 𝑥 ) ( le ‘ 𝐾 ) ( ◡ 𝐹 ‘ 𝑦 ) ) ) ) )
10 9 adantr ⊢ ( ( 𝐾 ∈ 𝑉 ∧ 𝐹 ∈ 𝐼 ) → ( ◡ 𝐹 ∈ 𝐼 ↔ ( ◡ 𝐹 : ( Base ‘ 𝐾 ) –1-1-onto→ ( Base ‘ 𝐾 ) ∧ ∀ 𝑥 ∈ ( Base ‘ 𝐾 ) ∀ 𝑦 ∈ ( Base ‘ 𝐾 ) ( 𝑥 ( le ‘ 𝐾 ) 𝑦 ↔ ( ◡ 𝐹 ‘ 𝑥 ) ( le ‘ 𝐾 ) ( ◡ 𝐹 ‘ 𝑦 ) ) ) ) )
11 5 8 10 mpbir2and ⊢ ( ( 𝐾 ∈ 𝑉 ∧ 𝐹 ∈ 𝐼 ) → ◡ 𝐹 ∈ 𝐼 )