lautco

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

		Ref	Expression
	Hypothesis	lautco.i	$⊢ I = LAut (K)$
	Assertion	lautco	$⊢ (K \in V \land F \in I \land G \in I) \to F \circ G \in I$

Proof

Step	Hyp	Ref	Expression
1		lautco.i	$⊢ I = LAut (K)$
2		eqid	$⊢ {Base}_{K} = {Base}_{K}$
3	2 1	laut1o	$⊢ (K \in V \land F \in I) \to F : {Base}_{K} \underset{1-1 onto}{⟶} {Base}_{K}$
4	3	3adant3	$⊢ (K \in V \land F \in I \land G \in I) \to F : {Base}_{K} \underset{1-1 onto}{⟶} {Base}_{K}$
5	2 1	laut1o	$⊢ (K \in V \land G \in I) \to G : {Base}_{K} \underset{1-1 onto}{⟶} {Base}_{K}$
6	5	3adant2	$⊢ (K \in V \land F \in I \land G \in I) \to G : {Base}_{K} \underset{1-1 onto}{⟶} {Base}_{K}$
7		f1oco	$⊢ (F : {Base}_{K} \underset{1-1 onto}{⟶} {Base}_{K} \land G : {Base}_{K} \underset{1-1 onto}{⟶} {Base}_{K}) \to (F \circ G) : {Base}_{K} \underset{1-1 onto}{⟶} {Base}_{K}$
8	4 6 7	syl2anc	$⊢ (K \in V \land F \in I \land G \in I) \to (F \circ G) : {Base}_{K} \underset{1-1 onto}{⟶} {Base}_{K}$
9		simpl1	$⊢ ((K \in V \land F \in I \land G \in I) \land (x \in {Base}_{K} \land y \in {Base}_{K})) \to K \in V$
10		simpl2	$⊢ ((K \in V \land F \in I \land G \in I) \land (x \in {Base}_{K} \land y \in {Base}_{K})) \to F \in I$
11		simpl3	$⊢ ((K \in V \land F \in I \land G \in I) \land (x \in {Base}_{K} \land y \in {Base}_{K})) \to G \in I$
12		simprl	$⊢ ((K \in V \land F \in I \land G \in I) \land (x \in {Base}_{K} \land y \in {Base}_{K})) \to x \in {Base}_{K}$
13	2 1	lautcl	$⊢ ((K \in V \land G \in I) \land x \in {Base}_{K}) \to G (x) \in {Base}_{K}$
14	9 11 12 13	syl21anc	$⊢ ((K \in V \land F \in I \land G \in I) \land (x \in {Base}_{K} \land y \in {Base}_{K})) \to G (x) \in {Base}_{K}$
15		simprr	$⊢ ((K \in V \land F \in I \land G \in I) \land (x \in {Base}_{K} \land y \in {Base}_{K})) \to y \in {Base}_{K}$
16	2 1	lautcl	$⊢ ((K \in V \land G \in I) \land y \in {Base}_{K}) \to G (y) \in {Base}_{K}$
17	9 11 15 16	syl21anc	$⊢ ((K \in V \land F \in I \land G \in I) \land (x \in {Base}_{K} \land y \in {Base}_{K})) \to G (y) \in {Base}_{K}$
18		eqid	$⊢ \leq_{K} = \leq_{K}$
19	2 18 1	lautle	$⊢ ((K \in V \land F \in I) \land (G (x) \in {Base}_{K} \land G (y) \in {Base}_{K})) \to (G (x) \leq_{K} G (y) \leftrightarrow F (G (x)) \leq_{K} F (G (y)))$
20	9 10 14 17 19	syl22anc	$⊢ ((K \in V \land F \in I \land G \in I) \land (x \in {Base}_{K} \land y \in {Base}_{K})) \to (G (x) \leq_{K} G (y) \leftrightarrow F (G (x)) \leq_{K} F (G (y)))$
21	2 18 1	lautle	$⊢ ((K \in V \land G \in I) \land (x \in {Base}_{K} \land y \in {Base}_{K})) \to (x \leq_{K} y \leftrightarrow G (x) \leq_{K} G (y))$
22	21	3adantl2	$⊢ ((K \in V \land F \in I \land G \in I) \land (x \in {Base}_{K} \land y \in {Base}_{K})) \to (x \leq_{K} y \leftrightarrow G (x) \leq_{K} G (y))$
23		f1of	$⊢ G : {Base}_{K} \underset{1-1 onto}{⟶} {Base}_{K} \to G : {Base}_{K} ⟶ {Base}_{K}$
24	6 23	syl	$⊢ (K \in V \land F \in I \land G \in I) \to G : {Base}_{K} ⟶ {Base}_{K}$
25		simpl	$⊢ (x \in {Base}_{K} \land y \in {Base}_{K}) \to x \in {Base}_{K}$
26		fvco3	$⊢ (G : {Base}_{K} ⟶ {Base}_{K} \land x \in {Base}_{K}) \to (F \circ G) (x) = F (G (x))$
27	24 25 26	syl2an	$⊢ ((K \in V \land F \in I \land G \in I) \land (x \in {Base}_{K} \land y \in {Base}_{K})) \to (F \circ G) (x) = F (G (x))$
28		simpr	$⊢ (x \in {Base}_{K} \land y \in {Base}_{K}) \to y \in {Base}_{K}$
29		fvco3	$⊢ (G : {Base}_{K} ⟶ {Base}_{K} \land y \in {Base}_{K}) \to (F \circ G) (y) = F (G (y))$
30	24 28 29	syl2an	$⊢ ((K \in V \land F \in I \land G \in I) \land (x \in {Base}_{K} \land y \in {Base}_{K})) \to (F \circ G) (y) = F (G (y))$
31	27 30	breq12d	$⊢ ((K \in V \land F \in I \land G \in I) \land (x \in {Base}_{K} \land y \in {Base}_{K})) \to ((F \circ G) (x) \leq_{K} (F \circ G) (y) \leftrightarrow F (G (x)) \leq_{K} F (G (y)))$
32	20 22 31	3bitr4d	$⊢ ((K \in V \land F \in I \land G \in I) \land (x \in {Base}_{K} \land y \in {Base}_{K})) \to (x \leq_{K} y \leftrightarrow (F \circ G) (x) \leq_{K} (F \circ G) (y))$
33	32	ralrimivva	$⊢ (K \in V \land F \in I \land G \in I) \to \forall x \in {Base}_{K} \forall y \in {Base}_{K} (x \leq_{K} y \leftrightarrow (F \circ G) (x) \leq_{K} (F \circ G) (y))$
34	2 18 1	islaut	$⊢ K \in V \to (F \circ G \in I \leftrightarrow ((F \circ G) : {Base}_{K} \underset{1-1 onto}{⟶} {Base}_{K} \land \forall x \in {Base}_{K} \forall y \in {Base}_{K} (x \leq_{K} y \leftrightarrow (F \circ G) (x) \leq_{K} (F \circ G) (y))))$
35	34	3ad2ant1	$⊢ (K \in V \land F \in I \land G \in I) \to (F \circ G \in I \leftrightarrow ((F \circ G) : {Base}_{K} \underset{1-1 onto}{⟶} {Base}_{K} \land \forall x \in {Base}_{K} \forall y \in {Base}_{K} (x \leq_{K} y \leftrightarrow (F \circ G) (x) \leq_{K} (F \circ G) (y))))$
36	8 33 35	mpbir2and	$⊢ (K \in V \land F \in I \land G \in I) \to F \circ G \in I$

Metamath Proof Explorer

Theorem lautco

Proof