ltrn2ateq

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

	Ref	Expression
Hypotheses	ltrn2eq.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
	ltrn2eq.a	$⊢ A = Atoms (K)$
	ltrn2eq.h	$⊢ H = LHyp (K)$
	ltrn2eq.t	$⊢ T = LTrn (K) (W)$
Assertion	ltrn2ateq	$⊢ ((K \in HL \land W \in H) \land (F \in T \land (P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W))) \to (F (P) = P \leftrightarrow F (Q) = Q)$

Step	Hyp	Ref	Expression
1		ltrn2eq.l	$⊢ \underset{˙}{\leq} = \leq_{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 \in HL \land W \in H) \land F \in T \land (P \in A \land \neg P \underset{˙}{\leq} W)) \to (F = {I ↾}_{{Base}_{K}} \leftrightarrow F (P) = P)$
7	6	3adant3r3	$⊢ ((K \in HL \land W \in H) \land (F \in T \land (P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W))) \to (F = {I ↾}_{{Base}_{K}} \leftrightarrow F (P) = P)$
8	5 1 2 3 4	ltrnideq	$⊢ ((K \in HL \land W \in H) \land F \in T \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \to (F = {I ↾}_{{Base}_{K}} \leftrightarrow F (Q) = Q)$
9	8	3adant3r2	$⊢ ((K \in HL \land W \in H) \land (F \in T \land (P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W))) \to (F = {I ↾}_{{Base}_{K}} \leftrightarrow F (Q) = Q)$
10	7 9	bitr3d	$⊢ ((K \in HL \land W \in H) \land (F \in T \land (P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W))) \to (F (P) = P \leftrightarrow F (Q) = Q)$

Metamath Proof Explorer