Metamath Proof Explorer

Theorem lautcnvle

Description: Less-than or equal property of lattice automorphism converse. (Contributed by NM, 19-May-2012)

Ref Expression
Hypotheses lautcnvle.b ⊢ 𝐵 = ( Base ‘ 𝐾 )
lautcnvle.l ⊢ ≤ = ( le ‘ 𝐾 )
lautcnvle.i ⊢ 𝐼 = ( LAut ‘ 𝐾 )
Assertion lautcnvle ( ( ( 𝐾 ∈ 𝑉 ∧ 𝐹 ∈ 𝐼 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ) → ( 𝑋 ≤ 𝑌 ↔ ( ◡ 𝐹 ‘ 𝑋 ) ≤ ( ◡ 𝐹 ‘ 𝑌 ) ) )

Proof

Step Hyp Ref Expression
1 lautcnvle.b ⊢ 𝐵 = ( Base ‘ 𝐾 )
2 lautcnvle.l ⊢ ≤ = ( le ‘ 𝐾 )
3 lautcnvle.i ⊢ 𝐼 = ( LAut ‘ 𝐾 )
4 simpl ⊢ ( ( ( 𝐾 ∈ 𝑉 ∧ 𝐹 ∈ 𝐼 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ) → ( 𝐾 ∈ 𝑉 ∧ 𝐹 ∈ 𝐼 ) )
5 1 3 laut1o ⊢ ( ( 𝐾 ∈ 𝑉 ∧ 𝐹 ∈ 𝐼 ) → 𝐹 : 𝐵 –1-1-onto→ 𝐵 )
6 5 adantr ⊢ ( ( ( 𝐾 ∈ 𝑉 ∧ 𝐹 ∈ 𝐼 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ) → 𝐹 : 𝐵 –1-1-onto→ 𝐵 )
7 simprl ⊢ ( ( ( 𝐾 ∈ 𝑉 ∧ 𝐹 ∈ 𝐼 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ) → 𝑋 ∈ 𝐵 )
8 f1ocnvdm ⊢ ( ( 𝐹 : 𝐵 –1-1-onto→ 𝐵 ∧ 𝑋 ∈ 𝐵 ) → ( ◡ 𝐹 ‘ 𝑋 ) ∈ 𝐵 )
9 6 7 8 syl2anc ⊢ ( ( ( 𝐾 ∈ 𝑉 ∧ 𝐹 ∈ 𝐼 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ) → ( ◡ 𝐹 ‘ 𝑋 ) ∈ 𝐵 )
10 simprr ⊢ ( ( ( 𝐾 ∈ 𝑉 ∧ 𝐹 ∈ 𝐼 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ) → 𝑌 ∈ 𝐵 )
11 f1ocnvdm ⊢ ( ( 𝐹 : 𝐵 –1-1-onto→ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( ◡ 𝐹 ‘ 𝑌 ) ∈ 𝐵 )
12 6 10 11 syl2anc ⊢ ( ( ( 𝐾 ∈ 𝑉 ∧ 𝐹 ∈ 𝐼 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ) → ( ◡ 𝐹 ‘ 𝑌 ) ∈ 𝐵 )
13 1 2 3 lautle ⊢ ( ( ( 𝐾 ∈ 𝑉 ∧ 𝐹 ∈ 𝐼 ) ∧ ( ( ◡ 𝐹 ‘ 𝑋 ) ∈ 𝐵 ∧ ( ◡ 𝐹 ‘ 𝑌 ) ∈ 𝐵 ) ) → ( ( ◡ 𝐹 ‘ 𝑋 ) ≤ ( ◡ 𝐹 ‘ 𝑌 ) ↔ ( 𝐹 ‘ ( ◡ 𝐹 ‘ 𝑋 ) ) ≤ ( 𝐹 ‘ ( ◡ 𝐹 ‘ 𝑌 ) ) ) )
14 4 9 12 13 syl12anc ⊢ ( ( ( 𝐾 ∈ 𝑉 ∧ 𝐹 ∈ 𝐼 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ) → ( ( ◡ 𝐹 ‘ 𝑋 ) ≤ ( ◡ 𝐹 ‘ 𝑌 ) ↔ ( 𝐹 ‘ ( ◡ 𝐹 ‘ 𝑋 ) ) ≤ ( 𝐹 ‘ ( ◡ 𝐹 ‘ 𝑌 ) ) ) )
15 f1ocnvfv2 ⊢ ( ( 𝐹 : 𝐵 –1-1-onto→ 𝐵 ∧ 𝑋 ∈ 𝐵 ) → ( 𝐹 ‘ ( ◡ 𝐹 ‘ 𝑋 ) ) = 𝑋 )
16 6 7 15 syl2anc ⊢ ( ( ( 𝐾 ∈ 𝑉 ∧ 𝐹 ∈ 𝐼 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ) → ( 𝐹 ‘ ( ◡ 𝐹 ‘ 𝑋 ) ) = 𝑋 )
17 f1ocnvfv2 ⊢ ( ( 𝐹 : 𝐵 –1-1-onto→ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( 𝐹 ‘ ( ◡ 𝐹 ‘ 𝑌 ) ) = 𝑌 )
18 6 10 17 syl2anc ⊢ ( ( ( 𝐾 ∈ 𝑉 ∧ 𝐹 ∈ 𝐼 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ) → ( 𝐹 ‘ ( ◡ 𝐹 ‘ 𝑌 ) ) = 𝑌 )
19 16 18 breq12d ⊢ ( ( ( 𝐾 ∈ 𝑉 ∧ 𝐹 ∈ 𝐼 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ) → ( ( 𝐹 ‘ ( ◡ 𝐹 ‘ 𝑋 ) ) ≤ ( 𝐹 ‘ ( ◡ 𝐹 ‘ 𝑌 ) ) ↔ 𝑋 ≤ 𝑌 ) )
20 14 19 bitr2d ⊢ ( ( ( 𝐾 ∈ 𝑉 ∧ 𝐹 ∈ 𝐼 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ) → ( 𝑋 ≤ 𝑌 ↔ ( ◡ 𝐹 ‘ 𝑋 ) ≤ ( ◡ 𝐹 ‘ 𝑌 ) ) )