ltrnval1

Description: Value of a lattice translation under its co-atom. (Contributed by NM, 20-May-2012)

	Ref	Expression
Hypotheses	ltrnval1.b	$⊢ B = {Base}_{K}$
	ltrnval1.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
	ltrnval1.h	$⊢ H = LHyp (K)$
	ltrnval1.t	$⊢ T = LTrn (K) (W)$
Assertion	ltrnval1	$⊢ ((K \in V \land W \in H) \land F \in T \land (X \in B \land X \underset{˙}{\leq} W)) \to F (X) = X$

Step	Hyp	Ref	Expression
1		ltrnval1.b	$⊢ B = {Base}_{K}$
2		ltrnval1.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
3		ltrnval1.h	$⊢ H = LHyp (K)$
4		ltrnval1.t	$⊢ T = LTrn (K) (W)$
5		eqid	$⊢ LDil (K) (W) = LDil (K) (W)$
6	3 5 4	ltrnldil	$⊢ ((K \in V \land W \in H) \land F \in T) \to F \in LDil (K) (W)$
7	6	3adant3	$⊢ ((K \in V \land W \in H) \land F \in T \land (X \in B \land X \underset{˙}{\leq} W)) \to F \in LDil (K) (W)$
8	1 2 3 5	ldilval	$⊢ ((K \in V \land W \in H) \land F \in LDil (K) (W) \land (X \in B \land X \underset{˙}{\leq} W)) \to F (X) = X$
9	7 8	syld3an2	$⊢ ((K \in V \land W \in H) \land F \in T \land (X \in B \land X \underset{˙}{\leq} W)) \to F (X) = X$

Metamath Proof Explorer