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	⊢ ( ( 𝐾 ∈ 𝑉 ∧ 𝐹 ∈ 𝐼 ) → ◡ 𝐹 ∈ 𝐼 )