Metamath Proof Explorer

Theorem lauteq

Description: A lattice automorphism argument is equal to its value if all atoms are equal to their values. (Contributed by NM, 24-May-2012)

Ref Expression
Hypotheses lauteq.b ⊢ 𝐵 = ( Base ‘ 𝐾 )
lauteq.a ⊢ 𝐴 = ( Atoms ‘ 𝐾 )
lauteq.i ⊢ 𝐼 = ( LAut ‘ 𝐾 )
Assertion lauteq ( ( ( 𝐾 ∈ HL ∧ 𝐹 ∈ 𝐼 ∧ 𝑋 ∈ 𝐵 ) ∧ ∀ 𝑝 ∈ 𝐴 ( 𝐹 ‘ 𝑝 ) = 𝑝 ) → ( 𝐹 ‘ 𝑋 ) = 𝑋 )

Proof

Step Hyp Ref Expression
1 lauteq.b ⊢ 𝐵 = ( Base ‘ 𝐾 )
2 lauteq.a ⊢ 𝐴 = ( Atoms ‘ 𝐾 )
3 lauteq.i ⊢ 𝐼 = ( LAut ‘ 𝐾 )
4 simpl1 ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝐹 ∈ 𝐼 ∧ 𝑋 ∈ 𝐵 ) ∧ 𝑝 ∈ 𝐴 ) → 𝐾 ∈ HL )
5 simpl2 ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝐹 ∈ 𝐼 ∧ 𝑋 ∈ 𝐵 ) ∧ 𝑝 ∈ 𝐴 ) → 𝐹 ∈ 𝐼 )
6 1 2 atbase ⊢ ( 𝑝 ∈ 𝐴 → 𝑝 ∈ 𝐵 )
7 6 adantl ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝐹 ∈ 𝐼 ∧ 𝑋 ∈ 𝐵 ) ∧ 𝑝 ∈ 𝐴 ) → 𝑝 ∈ 𝐵 )
8 simpl3 ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝐹 ∈ 𝐼 ∧ 𝑋 ∈ 𝐵 ) ∧ 𝑝 ∈ 𝐴 ) → 𝑋 ∈ 𝐵 )
9 eqid ⊢ ( le ‘ 𝐾 ) = ( le ‘ 𝐾 )
10 1 9 3 lautle ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝐹 ∈ 𝐼 ) ∧ ( 𝑝 ∈ 𝐵 ∧ 𝑋 ∈ 𝐵 ) ) → ( 𝑝 ( le ‘ 𝐾 ) 𝑋 ↔ ( 𝐹 ‘ 𝑝 ) ( le ‘ 𝐾 ) ( 𝐹 ‘ 𝑋 ) ) )
11 4 5 7 8 10 syl22anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝐹 ∈ 𝐼 ∧ 𝑋 ∈ 𝐵 ) ∧ 𝑝 ∈ 𝐴 ) → ( 𝑝 ( le ‘ 𝐾 ) 𝑋 ↔ ( 𝐹 ‘ 𝑝 ) ( le ‘ 𝐾 ) ( 𝐹 ‘ 𝑋 ) ) )
12 breq1 ⊢ ( ( 𝐹 ‘ 𝑝 ) = 𝑝 → ( ( 𝐹 ‘ 𝑝 ) ( le ‘ 𝐾 ) ( 𝐹 ‘ 𝑋 ) ↔ 𝑝 ( le ‘ 𝐾 ) ( 𝐹 ‘ 𝑋 ) ) )
13 11 12 sylan9bb ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝐹 ∈ 𝐼 ∧ 𝑋 ∈ 𝐵 ) ∧ 𝑝 ∈ 𝐴 ) ∧ ( 𝐹 ‘ 𝑝 ) = 𝑝 ) → ( 𝑝 ( le ‘ 𝐾 ) 𝑋 ↔ 𝑝 ( le ‘ 𝐾 ) ( 𝐹 ‘ 𝑋 ) ) )
14 13 bicomd ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝐹 ∈ 𝐼 ∧ 𝑋 ∈ 𝐵 ) ∧ 𝑝 ∈ 𝐴 ) ∧ ( 𝐹 ‘ 𝑝 ) = 𝑝 ) → ( 𝑝 ( le ‘ 𝐾 ) ( 𝐹 ‘ 𝑋 ) ↔ 𝑝 ( le ‘ 𝐾 ) 𝑋 ) )
15 14 ex ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝐹 ∈ 𝐼 ∧ 𝑋 ∈ 𝐵 ) ∧ 𝑝 ∈ 𝐴 ) → ( ( 𝐹 ‘ 𝑝 ) = 𝑝 → ( 𝑝 ( le ‘ 𝐾 ) ( 𝐹 ‘ 𝑋 ) ↔ 𝑝 ( le ‘ 𝐾 ) 𝑋 ) ) )
16 15 ralimdva ⊢ ( ( 𝐾 ∈ HL ∧ 𝐹 ∈ 𝐼 ∧ 𝑋 ∈ 𝐵 ) → ( ∀ 𝑝 ∈ 𝐴 ( 𝐹 ‘ 𝑝 ) = 𝑝 → ∀ 𝑝 ∈ 𝐴 ( 𝑝 ( le ‘ 𝐾 ) ( 𝐹 ‘ 𝑋 ) ↔ 𝑝 ( le ‘ 𝐾 ) 𝑋 ) ) )
17 16 imp ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝐹 ∈ 𝐼 ∧ 𝑋 ∈ 𝐵 ) ∧ ∀ 𝑝 ∈ 𝐴 ( 𝐹 ‘ 𝑝 ) = 𝑝 ) → ∀ 𝑝 ∈ 𝐴 ( 𝑝 ( le ‘ 𝐾 ) ( 𝐹 ‘ 𝑋 ) ↔ 𝑝 ( le ‘ 𝐾 ) 𝑋 ) )
18 simpl1 ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝐹 ∈ 𝐼 ∧ 𝑋 ∈ 𝐵 ) ∧ ∀ 𝑝 ∈ 𝐴 ( 𝐹 ‘ 𝑝 ) = 𝑝 ) → 𝐾 ∈ HL )
19 simpl2 ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝐹 ∈ 𝐼 ∧ 𝑋 ∈ 𝐵 ) ∧ ∀ 𝑝 ∈ 𝐴 ( 𝐹 ‘ 𝑝 ) = 𝑝 ) → 𝐹 ∈ 𝐼 )
20 simpl3 ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝐹 ∈ 𝐼 ∧ 𝑋 ∈ 𝐵 ) ∧ ∀ 𝑝 ∈ 𝐴 ( 𝐹 ‘ 𝑝 ) = 𝑝 ) → 𝑋 ∈ 𝐵 )
21 1 3 lautcl ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝐹 ∈ 𝐼 ) ∧ 𝑋 ∈ 𝐵 ) → ( 𝐹 ‘ 𝑋 ) ∈ 𝐵 )
22 18 19 20 21 syl21anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝐹 ∈ 𝐼 ∧ 𝑋 ∈ 𝐵 ) ∧ ∀ 𝑝 ∈ 𝐴 ( 𝐹 ‘ 𝑝 ) = 𝑝 ) → ( 𝐹 ‘ 𝑋 ) ∈ 𝐵 )
23 1 9 2 hlateq ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝐹 ‘ 𝑋 ) ∈ 𝐵 ∧ 𝑋 ∈ 𝐵 ) → ( ∀ 𝑝 ∈ 𝐴 ( 𝑝 ( le ‘ 𝐾 ) ( 𝐹 ‘ 𝑋 ) ↔ 𝑝 ( le ‘ 𝐾 ) 𝑋 ) ↔ ( 𝐹 ‘ 𝑋 ) = 𝑋 ) )
24 18 22 20 23 syl3anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝐹 ∈ 𝐼 ∧ 𝑋 ∈ 𝐵 ) ∧ ∀ 𝑝 ∈ 𝐴 ( 𝐹 ‘ 𝑝 ) = 𝑝 ) → ( ∀ 𝑝 ∈ 𝐴 ( 𝑝 ( le ‘ 𝐾 ) ( 𝐹 ‘ 𝑋 ) ↔ 𝑝 ( le ‘ 𝐾 ) 𝑋 ) ↔ ( 𝐹 ‘ 𝑋 ) = 𝑋 ) )
25 17 24 mpbid ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝐹 ∈ 𝐼 ∧ 𝑋 ∈ 𝐵 ) ∧ ∀ 𝑝 ∈ 𝐴 ( 𝐹 ‘ 𝑝 ) = 𝑝 ) → ( 𝐹 ‘ 𝑋 ) = 𝑋 )