ldilco

Description: The composition of two lattice automorphisms is a lattice automorphism. (Contributed by NM, 19-Apr-2013)

	Ref	Expression
Hypotheses	ldilco.h	$⊢ H = LHyp (K)$
	ldilco.d	$⊢ D = LDil (K) (W)$
Assertion	ldilco	$⊢ ((K \in V \land W \in H) \land F \in D \land G \in D) \to F \circ G \in D$

Proof

Step	Hyp	Ref	Expression
1		ldilco.h	$⊢ H = LHyp (K)$
2		ldilco.d	$⊢ D = LDil (K) (W)$
3		simp1l	$⊢ ((K \in V \land W \in H) \land F \in D \land G \in D) \to K \in V$
4		eqid	$⊢ LAut (K) = LAut (K)$
5	1 4 2	ldillaut	$⊢ ((K \in V \land W \in H) \land F \in D) \to F \in LAut (K)$
6	5	3adant3	$⊢ ((K \in V \land W \in H) \land F \in D \land G \in D) \to F \in LAut (K)$
7	1 4 2	ldillaut	$⊢ ((K \in V \land W \in H) \land G \in D) \to G \in LAut (K)$
8	7	3adant2	$⊢ ((K \in V \land W \in H) \land F \in D \land G \in D) \to G \in LAut (K)$
9	4	lautco	$⊢ (K \in V \land F \in LAut (K) \land G \in LAut (K)) \to F \circ G \in LAut (K)$
10	3 6 8 9	syl3anc	$⊢ ((K \in V \land W \in H) \land F \in D \land G \in D) \to F \circ G \in LAut (K)$
11		simp11	$⊢ (((K \in V \land W \in H) \land F \in D \land G \in D) \land x \in {Base}_{K} \land x \leq_{K} W) \to (K \in V \land W \in H)$
12		simp13	$⊢ (((K \in V \land W \in H) \land F \in D \land G \in D) \land x \in {Base}_{K} \land x \leq_{K} W) \to G \in D$
13		eqid	$⊢ {Base}_{K} = {Base}_{K}$
14	13 1 2	ldil1o	$⊢ ((K \in V \land W \in H) \land G \in D) \to G : {Base}_{K} \underset{1-1 onto}{⟶} {Base}_{K}$
15	11 12 14	syl2anc	$⊢ (((K \in V \land W \in H) \land F \in D \land G \in D) \land x \in {Base}_{K} \land x \leq_{K} W) \to G : {Base}_{K} \underset{1-1 onto}{⟶} {Base}_{K}$
16		f1of	$⊢ G : {Base}_{K} \underset{1-1 onto}{⟶} {Base}_{K} \to G : {Base}_{K} ⟶ {Base}_{K}$
17	15 16	syl	$⊢ (((K \in V \land W \in H) \land F \in D \land G \in D) \land x \in {Base}_{K} \land x \leq_{K} W) \to G : {Base}_{K} ⟶ {Base}_{K}$
18		simp2	$⊢ (((K \in V \land W \in H) \land F \in D \land G \in D) \land x \in {Base}_{K} \land x \leq_{K} W) \to x \in {Base}_{K}$
19		fvco3	$⊢ (G : {Base}_{K} ⟶ {Base}_{K} \land x \in {Base}_{K}) \to (F \circ G) (x) = F (G (x))$
20	17 18 19	syl2anc	$⊢ (((K \in V \land W \in H) \land F \in D \land G \in D) \land x \in {Base}_{K} \land x \leq_{K} W) \to (F \circ G) (x) = F (G (x))$
21		simp3	$⊢ (((K \in V \land W \in H) \land F \in D \land G \in D) \land x \in {Base}_{K} \land x \leq_{K} W) \to x \leq_{K} W$
22		eqid	$⊢ \leq_{K} = \leq_{K}$
23	13 22 1 2	ldilval	$⊢ ((K \in V \land W \in H) \land G \in D \land (x \in {Base}_{K} \land x \leq_{K} W)) \to G (x) = x$
24	11 12 18 21 23	syl112anc	$⊢ (((K \in V \land W \in H) \land F \in D \land G \in D) \land x \in {Base}_{K} \land x \leq_{K} W) \to G (x) = x$
25	24	fveq2d	$⊢ (((K \in V \land W \in H) \land F \in D \land G \in D) \land x \in {Base}_{K} \land x \leq_{K} W) \to F (G (x)) = F (x)$
26		simp12	$⊢ (((K \in V \land W \in H) \land F \in D \land G \in D) \land x \in {Base}_{K} \land x \leq_{K} W) \to F \in D$
27	13 22 1 2	ldilval	$⊢ ((K \in V \land W \in H) \land F \in D \land (x \in {Base}_{K} \land x \leq_{K} W)) \to F (x) = x$
28	11 26 18 21 27	syl112anc	$⊢ (((K \in V \land W \in H) \land F \in D \land G \in D) \land x \in {Base}_{K} \land x \leq_{K} W) \to F (x) = x$
29	20 25 28	3eqtrd	$⊢ (((K \in V \land W \in H) \land F \in D \land G \in D) \land x \in {Base}_{K} \land x \leq_{K} W) \to (F \circ G) (x) = x$
30	29	3exp	$⊢ ((K \in V \land W \in H) \land F \in D \land G \in D) \to (x \in {Base}_{K} \to (x \leq_{K} W \to (F \circ G) (x) = x))$
31	30	ralrimiv	$⊢ ((K \in V \land W \in H) \land F \in D \land G \in D) \to \forall x \in {Base}_{K} (x \leq_{K} W \to (F \circ G) (x) = x)$
32	13 22 1 4 2	isldil	$⊢ (K \in V \land W \in H) \to (F \circ G \in D \leftrightarrow (F \circ G \in LAut (K) \land \forall x \in {Base}_{K} (x \leq_{K} W \to (F \circ G) (x) = x)))$
33	32	3ad2ant1	$⊢ ((K \in V \land W \in H) \land F \in D \land G \in D) \to (F \circ G \in D \leftrightarrow (F \circ G \in LAut (K) \land \forall x \in {Base}_{K} (x \leq_{K} W \to (F \circ G) (x) = x)))$
34	10 31 33	mpbir2and	$⊢ ((K \in V \land W \in H) \land F \in D \land G \in D) \to F \circ G \in D$

Metamath Proof Explorer

Theorem ldilco

Proof