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

Metamath Proof Explorer

Theorem lautlt

Description: Less-than property of a lattice automorphism. (Contributed by NM, 20-May-2012)

Ref Expression
Hypotheses lautlt.b ⊢ 𝐵 = ( Base ‘ 𝐾 )
lautlt.s ⊢ < = ( lt ‘ 𝐾 )
lautlt.i ⊢ 𝐼 = ( LAut ‘ 𝐾 )
Assertion lautlt ( ( 𝐾 ∈ 𝐴 ∧ ( 𝐹 ∈ 𝐼 ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ) → ( 𝑋 < 𝑌 ↔ ( 𝐹 ‘ 𝑋 ) < ( 𝐹 ‘ 𝑌 ) ) )

Proof

Step Hyp Ref Expression
1 lautlt.b ⊢ 𝐵 = ( Base ‘ 𝐾 )
2 lautlt.s ⊢ < = ( lt ‘ 𝐾 )
3 lautlt.i ⊢ 𝐼 = ( LAut ‘ 𝐾 )
4 simpl ⊢ ( ( 𝐾 ∈ 𝐴 ∧ ( 𝐹 ∈ 𝐼 ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ) → 𝐾 ∈ 𝐴 )
5 simpr1 ⊢ ( ( 𝐾 ∈ 𝐴 ∧ ( 𝐹 ∈ 𝐼 ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ) → 𝐹 ∈ 𝐼 )
6 simpr2 ⊢ ( ( 𝐾 ∈ 𝐴 ∧ ( 𝐹 ∈ 𝐼 ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ) → 𝑋 ∈ 𝐵 )
7 simpr3 ⊢ ( ( 𝐾 ∈ 𝐴 ∧ ( 𝐹 ∈ 𝐼 ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ) → 𝑌 ∈ 𝐵 )
8 eqid ⊢ ( le ‘ 𝐾 ) = ( le ‘ 𝐾 )
9 1 8 3 lautle ⊢ ( ( ( 𝐾 ∈ 𝐴 ∧ 𝐹 ∈ 𝐼 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ) → ( 𝑋 ( le ‘ 𝐾 ) 𝑌 ↔ ( 𝐹 ‘ 𝑋 ) ( le ‘ 𝐾 ) ( 𝐹 ‘ 𝑌 ) ) )
10 4 5 6 7 9 syl22anc ⊢ ( ( 𝐾 ∈ 𝐴 ∧ ( 𝐹 ∈ 𝐼 ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ) → ( 𝑋 ( le ‘ 𝐾 ) 𝑌 ↔ ( 𝐹 ‘ 𝑋 ) ( le ‘ 𝐾 ) ( 𝐹 ‘ 𝑌 ) ) )
11 1 3 laut11 ⊢ ( ( ( 𝐾 ∈ 𝐴 ∧ 𝐹 ∈ 𝐼 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ) → ( ( 𝐹 ‘ 𝑋 ) = ( 𝐹 ‘ 𝑌 ) ↔ 𝑋 = 𝑌 ) )
12 4 5 6 7 11 syl22anc ⊢ ( ( 𝐾 ∈ 𝐴 ∧ ( 𝐹 ∈ 𝐼 ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ) → ( ( 𝐹 ‘ 𝑋 ) = ( 𝐹 ‘ 𝑌 ) ↔ 𝑋 = 𝑌 ) )
13 12 bicomd ⊢ ( ( 𝐾 ∈ 𝐴 ∧ ( 𝐹 ∈ 𝐼 ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ) → ( 𝑋 = 𝑌 ↔ ( 𝐹 ‘ 𝑋 ) = ( 𝐹 ‘ 𝑌 ) ) )
14 13 necon3bid ⊢ ( ( 𝐾 ∈ 𝐴 ∧ ( 𝐹 ∈ 𝐼 ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ) → ( 𝑋 ≠ 𝑌 ↔ ( 𝐹 ‘ 𝑋 ) ≠ ( 𝐹 ‘ 𝑌 ) ) )
15 10 14 anbi12d ⊢ ( ( 𝐾 ∈ 𝐴 ∧ ( 𝐹 ∈ 𝐼 ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ) → ( ( 𝑋 ( le ‘ 𝐾 ) 𝑌 ∧ 𝑋 ≠ 𝑌 ) ↔ ( ( 𝐹 ‘ 𝑋 ) ( le ‘ 𝐾 ) ( 𝐹 ‘ 𝑌 ) ∧ ( 𝐹 ‘ 𝑋 ) ≠ ( 𝐹 ‘ 𝑌 ) ) ) )
16 8 2 pltval ⊢ ( ( 𝐾 ∈ 𝐴 ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( 𝑋 < 𝑌 ↔ ( 𝑋 ( le ‘ 𝐾 ) 𝑌 ∧ 𝑋 ≠ 𝑌 ) ) )
17 16 3adant3r1 ⊢ ( ( 𝐾 ∈ 𝐴 ∧ ( 𝐹 ∈ 𝐼 ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ) → ( 𝑋 < 𝑌 ↔ ( 𝑋 ( le ‘ 𝐾 ) 𝑌 ∧ 𝑋 ≠ 𝑌 ) ) )
18 1 3 lautcl ⊢ ( ( ( 𝐾 ∈ 𝐴 ∧ 𝐹 ∈ 𝐼 ) ∧ 𝑋 ∈ 𝐵 ) → ( 𝐹 ‘ 𝑋 ) ∈ 𝐵 )
19 4 5 6 18 syl21anc ⊢ ( ( 𝐾 ∈ 𝐴 ∧ ( 𝐹 ∈ 𝐼 ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ) → ( 𝐹 ‘ 𝑋 ) ∈ 𝐵 )
20 1 3 lautcl ⊢ ( ( ( 𝐾 ∈ 𝐴 ∧ 𝐹 ∈ 𝐼 ) ∧ 𝑌 ∈ 𝐵 ) → ( 𝐹 ‘ 𝑌 ) ∈ 𝐵 )
21 4 5 7 20 syl21anc ⊢ ( ( 𝐾 ∈ 𝐴 ∧ ( 𝐹 ∈ 𝐼 ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ) → ( 𝐹 ‘ 𝑌 ) ∈ 𝐵 )
22 8 2 pltval ⊢ ( ( 𝐾 ∈ 𝐴 ∧ ( 𝐹 ‘ 𝑋 ) ∈ 𝐵 ∧ ( 𝐹 ‘ 𝑌 ) ∈ 𝐵 ) → ( ( 𝐹 ‘ 𝑋 ) < ( 𝐹 ‘ 𝑌 ) ↔ ( ( 𝐹 ‘ 𝑋 ) ( le ‘ 𝐾 ) ( 𝐹 ‘ 𝑌 ) ∧ ( 𝐹 ‘ 𝑋 ) ≠ ( 𝐹 ‘ 𝑌 ) ) ) )
23 4 19 21 22 syl3anc ⊢ ( ( 𝐾 ∈ 𝐴 ∧ ( 𝐹 ∈ 𝐼 ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ) → ( ( 𝐹 ‘ 𝑋 ) < ( 𝐹 ‘ 𝑌 ) ↔ ( ( 𝐹 ‘ 𝑋 ) ( le ‘ 𝐾 ) ( 𝐹 ‘ 𝑌 ) ∧ ( 𝐹 ‘ 𝑋 ) ≠ ( 𝐹 ‘ 𝑌 ) ) ) )
24 15 17 23 3bitr4d ⊢ ( ( 𝐾 ∈ 𝐴 ∧ ( 𝐹 ∈ 𝐼 ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ) → ( 𝑋 < 𝑌 ↔ ( 𝐹 ‘ 𝑋 ) < ( 𝐹 ‘ 𝑌 ) ) )