ldilval

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

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

Step	Hyp	Ref	Expression
1		ldilval.b	$⊢ B = {Base}_{K}$
2		ldilval.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
3		ldilval.h	$⊢ H = LHyp (K)$
4		ldilval.d	$⊢ D = LDil (K) (W)$
5		eqid	$⊢ LAut (K) = LAut (K)$
6	1 2 3 5 4	isldil	$⊢ (K \in V \land W \in H) \to (F \in D \leftrightarrow (F \in LAut (K) \land \forall x \in B (x \underset{˙}{\leq} W \to F (x) = x)))$
7		simpr	$⊢ (F \in LAut (K) \land \forall x \in B (x \underset{˙}{\leq} W \to F (x) = x)) \to \forall x \in B (x \underset{˙}{\leq} W \to F (x) = x)$
8	6 7	biimtrdi	$⊢ (K \in V \land W \in H) \to (F \in D \to \forall x \in B (x \underset{˙}{\leq} W \to F (x) = x))$
9		breq1	$⊢ x = X \to (x \underset{˙}{\leq} W \leftrightarrow X \underset{˙}{\leq} W)$
10		fveq2	$⊢ x = X \to F (x) = F (X)$
11		id	$⊢ x = X \to x = X$
12	10 11	eqeq12d	$⊢ x = X \to (F (x) = x \leftrightarrow F (X) = X)$
13	9 12	imbi12d	$⊢ x = X \to ((x \underset{˙}{\leq} W \to F (x) = x) \leftrightarrow (X \underset{˙}{\leq} W \to F (X) = X))$
14	13	rspccv	$⊢ \forall x \in B (x \underset{˙}{\leq} W \to F (x) = x) \to (X \in B \to (X \underset{˙}{\leq} W \to F (X) = X))$
15	14	impd	$⊢ \forall x \in B (x \underset{˙}{\leq} W \to F (x) = x) \to ((X \in B \land X \underset{˙}{\leq} W) \to F (X) = X)$
16	8 15	syl6	$⊢ (K \in V \land W \in H) \to (F \in D \to ((X \in B \land X \underset{˙}{\leq} W) \to F (X) = X))$
17	16	3imp	$⊢ ((K \in V \land W \in H) \land F \in D \land (X \in B \land X \underset{˙}{\leq} W)) \to F (X) = X$

Metamath Proof Explorer