ldilcnv

Description: The converse of a lattice dilation is a lattice dilation. (Contributed by NM, 10-May-2013)

	Ref	Expression
Hypotheses	ldilcnv.h	$⊢ H = LHyp (K)$
	ldilcnv.d	$⊢ D = LDil (K) (W)$
Assertion	ldilcnv	$⊢ ((K \in HL \land W \in H) \land F \in D) \to F^{-1} \in D$

Proof

Step	Hyp	Ref	Expression
1		ldilcnv.h	$⊢ H = LHyp (K)$
2		ldilcnv.d	$⊢ D = LDil (K) (W)$
3		simpll	$⊢ ((K \in HL \land W \in H) \land F \in D) \to K \in HL$
4		eqid	$⊢ LAut (K) = LAut (K)$
5	1 4 2	ldillaut	$⊢ ((K \in HL \land W \in H) \land F \in D) \to F \in LAut (K)$
6	4	lautcnv	$⊢ (K \in HL \land F \in LAut (K)) \to F^{-1} \in LAut (K)$
7	3 5 6	syl2anc	$⊢ ((K \in HL \land W \in H) \land F \in D) \to F^{-1} \in LAut (K)$
8		eqid	$⊢ {Base}_{K} = {Base}_{K}$
9		eqid	$⊢ \leq_{K} = \leq_{K}$
10	8 9 1 2	ldilval	$⊢ ((K \in HL \land W \in H) \land F \in D \land (x \in {Base}_{K} \land x \leq_{K} W)) \to F (x) = x$
11	10	3expa	$⊢ (((K \in HL \land W \in H) \land F \in D) \land (x \in {Base}_{K} \land x \leq_{K} W)) \to F (x) = x$
12	11	3impb	$⊢ (((K \in HL \land W \in H) \land F \in D) \land x \in {Base}_{K} \land x \leq_{K} W) \to F (x) = x$
13	12	fveq2d	$⊢ (((K \in HL \land W \in H) \land F \in D) \land x \in {Base}_{K} \land x \leq_{K} W) \to F^{-1} (F (x)) = F^{-1} (x)$
14	8 1 2	ldil1o	$⊢ ((K \in HL \land W \in H) \land F \in D) \to F : {Base}_{K} \underset{1-1 onto}{⟶} {Base}_{K}$
15	14	3ad2ant1	$⊢ (((K \in HL \land W \in H) \land F \in D) \land x \in {Base}_{K} \land x \leq_{K} W) \to F : {Base}_{K} \underset{1-1 onto}{⟶} {Base}_{K}$
16		simp2	$⊢ (((K \in HL \land W \in H) \land F \in D) \land x \in {Base}_{K} \land x \leq_{K} W) \to x \in {Base}_{K}$
17		f1ocnvfv1	$⊢ (F : {Base}_{K} \underset{1-1 onto}{⟶} {Base}_{K} \land x \in {Base}_{K}) \to F^{-1} (F (x)) = x$
18	15 16 17	syl2anc	$⊢ (((K \in HL \land W \in H) \land F \in D) \land x \in {Base}_{K} \land x \leq_{K} W) \to F^{-1} (F (x)) = x$
19	13 18	eqtr3d	$⊢ (((K \in HL \land W \in H) \land F \in D) \land x \in {Base}_{K} \land x \leq_{K} W) \to F^{-1} (x) = x$
20	19	3exp	$⊢ ((K \in HL \land W \in H) \land F \in D) \to (x \in {Base}_{K} \to (x \leq_{K} W \to F^{-1} (x) = x))$
21	20	ralrimiv	$⊢ ((K \in HL \land W \in H) \land F \in D) \to \forall x \in {Base}_{K} (x \leq_{K} W \to F^{-1} (x) = x)$
22	8 9 1 4 2	isldil	$⊢ (K \in HL \land W \in H) \to (F^{-1} \in D \leftrightarrow (F^{-1} \in LAut (K) \land \forall x \in {Base}_{K} (x \leq_{K} W \to F^{-1} (x) = x)))$
23	22	adantr	$⊢ ((K \in HL \land W \in H) \land F \in D) \to (F^{-1} \in D \leftrightarrow (F^{-1} \in LAut (K) \land \forall x \in {Base}_{K} (x \leq_{K} W \to F^{-1} (x) = x)))$
24	7 21 23	mpbir2and	$⊢ ((K \in HL \land W \in H) \land F \in D) \to F^{-1} \in D$

Metamath Proof Explorer

Theorem ldilcnv

Proof