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 ⊢ B = Base K
lauteq.a ⊢ A = Atoms ⁡ K
lauteq.i ⊢ I = LAut ⁡ K
Assertion lauteq ⊢ K ∈ HL ∧ F ∈ I ∧ X ∈ B ∧ ∀ p ∈ A F ⁡ p = p → F ⁡ X = X

Proof

Step Hyp Ref Expression
1 lauteq.b ⊢ B = Base K
2 lauteq.a ⊢ A = Atoms ⁡ K
3 lauteq.i ⊢ I = LAut ⁡ K
4 simpl1 ⊢ K ∈ HL ∧ F ∈ I ∧ X ∈ B ∧ p ∈ A → K ∈ HL
5 simpl2 ⊢ K ∈ HL ∧ F ∈ I ∧ X ∈ B ∧ p ∈ A → F ∈ I
6 1 2 atbase ⊢ p ∈ A → p ∈ B
7 6 adantl ⊢ K ∈ HL ∧ F ∈ I ∧ X ∈ B ∧ p ∈ A → p ∈ B
8 simpl3 ⊢ K ∈ HL ∧ F ∈ I ∧ X ∈ B ∧ p ∈ A → X ∈ B
9 eqid ⊢ ≤ K = ≤ K
10 1 9 3 lautle ⊢ K ∈ HL ∧ F ∈ I ∧ p ∈ B ∧ X ∈ B → p ≤ K X ↔ F ⁡ p ≤ K F ⁡ X
11 4 5 7 8 10 syl22anc ⊢ K ∈ HL ∧ F ∈ I ∧ X ∈ B ∧ p ∈ A → p ≤ K X ↔ F ⁡ p ≤ K F ⁡ X
12 breq1 ⊢ F ⁡ p = p → F ⁡ p ≤ K F ⁡ X ↔ p ≤ K F ⁡ X
13 11 12 sylan9bb ⊢ K ∈ HL ∧ F ∈ I ∧ X ∈ B ∧ p ∈ A ∧ F ⁡ p = p → p ≤ K X ↔ p ≤ K F ⁡ X
14 13 bicomd ⊢ K ∈ HL ∧ F ∈ I ∧ X ∈ B ∧ p ∈ A ∧ F ⁡ p = p → p ≤ K F ⁡ X ↔ p ≤ K X
15 14 ex ⊢ K ∈ HL ∧ F ∈ I ∧ X ∈ B ∧ p ∈ A → F ⁡ p = p → p ≤ K F ⁡ X ↔ p ≤ K X
16 15 ralimdva ⊢ K ∈ HL ∧ F ∈ I ∧ X ∈ B → ∀ p ∈ A F ⁡ p = p → ∀ p ∈ A p ≤ K F ⁡ X ↔ p ≤ K X
17 16 imp ⊢ K ∈ HL ∧ F ∈ I ∧ X ∈ B ∧ ∀ p ∈ A F ⁡ p = p → ∀ p ∈ A p ≤ K F ⁡ X ↔ p ≤ K X
18 simpl1 ⊢ K ∈ HL ∧ F ∈ I ∧ X ∈ B ∧ ∀ p ∈ A F ⁡ p = p → K ∈ HL
19 simpl2 ⊢ K ∈ HL ∧ F ∈ I ∧ X ∈ B ∧ ∀ p ∈ A F ⁡ p = p → F ∈ I
20 simpl3 ⊢ K ∈ HL ∧ F ∈ I ∧ X ∈ B ∧ ∀ p ∈ A F ⁡ p = p → X ∈ B
21 1 3 lautcl ⊢ K ∈ HL ∧ F ∈ I ∧ X ∈ B → F ⁡ X ∈ B
22 18 19 20 21 syl21anc ⊢ K ∈ HL ∧ F ∈ I ∧ X ∈ B ∧ ∀ p ∈ A F ⁡ p = p → F ⁡ X ∈ B
23 1 9 2 hlateq ⊢ K ∈ HL ∧ F ⁡ X ∈ B ∧ X ∈ B → ∀ p ∈ A p ≤ K F ⁡ X ↔ p ≤ K X ↔ F ⁡ X = X
24 18 22 20 23 syl3anc ⊢ K ∈ HL ∧ F ∈ I ∧ X ∈ B ∧ ∀ p ∈ A F ⁡ p = p → ∀ p ∈ A p ≤ K F ⁡ X ↔ p ≤ K X ↔ F ⁡ X = X
25 17 24 mpbid ⊢ K ∈ HL ∧ F ∈ I ∧ X ∈ B ∧ ∀ p ∈ A F ⁡ p = p → F ⁡ X = X