Mathbox for Norm Megill < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  ldilco Structured version   Unicode version

Theorem ldilco 30913
 Description: The composition of two lattice automorphisms is a lattice automorphism. (Contributed by NM, 19-Apr-2013.)
Hypotheses
Ref Expression
ldilco.h
ldilco.d
Assertion
Ref Expression
ldilco

Proof of Theorem ldilco
Dummy variable is distinct from all other variables.
StepHypRef Expression
1 simp1l 981 . . 3
2 ldilco.h . . . . 5
3 eqid 2436 . . . . 5
4 ldilco.d . . . . 5
52, 3, 4ldillaut 30908 . . . 4
72, 3, 4ldillaut 30908 . . . 4
93lautco 30894 . . 3
101, 6, 8, 9syl3anc 1184 . 2
11 simp11 987 . . . . . . . 8
12 simp13 989 . . . . . . . 8
13 eqid 2436 . . . . . . . . 9
1413, 2, 4ldil1o 30909 . . . . . . . 8
1511, 12, 14syl2anc 643 . . . . . . 7
16 f1of 5674 . . . . . . 7
1715, 16syl 16 . . . . . 6
18 simp2 958 . . . . . 6
19 fvco3 5800 . . . . . 6
2017, 18, 19syl2anc 643 . . . . 5
21 simp3 959 . . . . . . 7
22 eqid 2436 . . . . . . . 8
2313, 22, 2, 4ldilval 30910 . . . . . . 7
2411, 12, 18, 21, 23syl112anc 1188 . . . . . 6
2524fveq2d 5732 . . . . 5
26 simp12 988 . . . . . 6
2713, 22, 2, 4ldilval 30910 . . . . . 6
2811, 26, 18, 21, 27syl112anc 1188 . . . . 5
2920, 25, 283eqtrd 2472 . . . 4
30293exp 1152 . . 3
3130ralrimiv 2788 . 2
3213, 22, 2, 3, 4isldil 30907 . . 3