Metamath Proof Explorer

Theorem ltrn2ateq

Description: Property of the equality of a lattice translation with its value. (Contributed by NM, 27-May-2012)

Ref Expression
Hypotheses ltrn2eq.l ⊢ ≤ ˙ = ≤ K
ltrn2eq.a ⊢ A = Atoms ⁡ K
ltrn2eq.h ⊢ H = LHyp ⁡ K
ltrn2eq.t ⊢ T = LTrn ⁡ K ⁡ W
Assertion ltrn2ateq ⊢ K ∈ HL ∧ W ∈ H ∧ F ∈ T ∧ P ∈ A ∧ ¬ P ≤ ˙ W ∧ Q ∈ A ∧ ¬ Q ≤ ˙ W → F ⁡ P = P ↔ F ⁡ Q = Q

Proof

Step Hyp Ref Expression
1 ltrn2eq.l ⊢ ≤ ˙ = ≤ K
2 ltrn2eq.a ⊢ A = Atoms ⁡ K
3 ltrn2eq.h ⊢ H = LHyp ⁡ K
4 ltrn2eq.t ⊢ T = LTrn ⁡ K ⁡ W
5 eqid ⊢ Base K = Base K
6 5 1 2 3 4 ltrnideq ⊢ K ∈ HL ∧ W ∈ H ∧ F ∈ T ∧ P ∈ A ∧ ¬ P ≤ ˙ W → F = I ↾ Base K ↔ F ⁡ P = P
7 6 3adant3r3 ⊢ K ∈ HL ∧ W ∈ H ∧ F ∈ T ∧ P ∈ A ∧ ¬ P ≤ ˙ W ∧ Q ∈ A ∧ ¬ Q ≤ ˙ W → F = I ↾ Base K ↔ F ⁡ P = P
8 5 1 2 3 4 ltrnideq ⊢ K ∈ HL ∧ W ∈ H ∧ F ∈ T ∧ Q ∈ A ∧ ¬ Q ≤ ˙ W → F = I ↾ Base K ↔ F ⁡ Q = Q
9 8 3adant3r2 ⊢ K ∈ HL ∧ W ∈ H ∧ F ∈ T ∧ P ∈ A ∧ ¬ P ≤ ˙ W ∧ Q ∈ A ∧ ¬ Q ≤ ˙ W → F = I ↾ Base K ↔ F ⁡ Q = Q
10 7 9 bitr3d ⊢ K ∈ HL ∧ W ∈ H ∧ F ∈ T ∧ P ∈ A ∧ ¬ P ≤ ˙ W ∧ Q ∈ A ∧ ¬ Q ≤ ˙ W → F ⁡ P = P ↔ F ⁡ Q = Q