This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem 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 e. V /\ W e. H ) /\ F e. D /\ G e. D ) -> ( F o. G ) e. D )

Proof

Step Hyp Ref Expression
1 ldilco.h 
 |-  H = ( LHyp ` K )
2 ldilco.d 
 |-  D = ( ( LDil ` K ) ` W )
3 simp1l 
 |-  ( ( ( K e. V /\ W e. H ) /\ F e. D /\ G e. D ) -> K e. V )
4 eqid 
 |-  ( LAut ` K ) = ( LAut ` K )
5 1 4 2 ldillaut 
 |-  ( ( ( K e. V /\ W e. H ) /\ F e. D ) -> F e. ( LAut ` K ) )
6 5 3adant3 
 |-  ( ( ( K e. V /\ W e. H ) /\ F e. D /\ G e. D ) -> F e. ( LAut ` K ) )
7 1 4 2 ldillaut 
 |-  ( ( ( K e. V /\ W e. H ) /\ G e. D ) -> G e. ( LAut ` K ) )
8 7 3adant2 
 |-  ( ( ( K e. V /\ W e. H ) /\ F e. D /\ G e. D ) -> G e. ( LAut ` K ) )
9 4 lautco 
 |-  ( ( K e. V /\ F e. ( LAut ` K ) /\ G e. ( LAut ` K ) ) -> ( F o. G ) e. ( LAut ` K ) )
10 3 6 8 9 syl3anc 
 |-  ( ( ( K e. V /\ W e. H ) /\ F e. D /\ G e. D ) -> ( F o. G ) e. ( LAut ` K ) )
11 simp11 
 |-  ( ( ( ( K e. V /\ W e. H ) /\ F e. D /\ G e. D ) /\ x e. ( Base ` K ) /\ x ( le ` K ) W ) -> ( K e. V /\ W e. H ) )
12 simp13 
 |-  ( ( ( ( K e. V /\ W e. H ) /\ F e. D /\ G e. D ) /\ x e. ( Base ` K ) /\ x ( le ` K ) W ) -> G e. D )
13 eqid 
 |-  ( Base ` K ) = ( Base ` K )
14 13 1 2 ldil1o 
 |-  ( ( ( K e. V /\ W e. H ) /\ G e. D ) -> G : ( Base ` K ) -1-1-onto-> ( Base ` K ) )
15 11 12 14 syl2anc 
 |-  ( ( ( ( K e. V /\ W e. H ) /\ F e. D /\ G e. D ) /\ x e. ( Base ` K ) /\ x ( le ` K ) W ) -> G : ( Base ` K ) -1-1-onto-> ( Base ` K ) )
16 f1of 
 |-  ( G : ( Base ` K ) -1-1-onto-> ( Base ` K ) -> G : ( Base ` K ) --> ( Base ` K ) )
17 15 16 syl 
 |-  ( ( ( ( K e. V /\ W e. H ) /\ F e. D /\ G e. D ) /\ x e. ( Base ` K ) /\ x ( le ` K ) W ) -> G : ( Base ` K ) --> ( Base ` K ) )
18 simp2 
 |-  ( ( ( ( K e. V /\ W e. H ) /\ F e. D /\ G e. D ) /\ x e. ( Base ` K ) /\ x ( le ` K ) W ) -> x e. ( Base ` K ) )
19 fvco3 
 |-  ( ( G : ( Base ` K ) --> ( Base ` K ) /\ x e. ( Base ` K ) ) -> ( ( F o. G ) ` x ) = ( F ` ( G ` x ) ) )
20 17 18 19 syl2anc 
 |-  ( ( ( ( K e. V /\ W e. H ) /\ F e. D /\ G e. D ) /\ x e. ( Base ` K ) /\ x ( le ` K ) W ) -> ( ( F o. G ) ` x ) = ( F ` ( G ` x ) ) )
21 simp3 
 |-  ( ( ( ( K e. V /\ W e. H ) /\ F e. D /\ G e. D ) /\ x e. ( Base ` K ) /\ x ( le ` K ) W ) -> x ( le ` K ) W )
22 eqid 
 |-  ( le ` K ) = ( le ` K )
23 13 22 1 2 ldilval 
 |-  ( ( ( K e. V /\ W e. H ) /\ G e. D /\ ( x e. ( Base ` K ) /\ x ( le ` K ) W ) ) -> ( G ` x ) = x )
24 11 12 18 21 23 syl112anc 
 |-  ( ( ( ( K e. V /\ W e. H ) /\ F e. D /\ G e. D ) /\ x e. ( Base ` K ) /\ x ( le ` K ) W ) -> ( G ` x ) = x )
25 24 fveq2d 
 |-  ( ( ( ( K e. V /\ W e. H ) /\ F e. D /\ G e. D ) /\ x e. ( Base ` K ) /\ x ( le ` K ) W ) -> ( F ` ( G ` x ) ) = ( F ` x ) )
26 simp12 
 |-  ( ( ( ( K e. V /\ W e. H ) /\ F e. D /\ G e. D ) /\ x e. ( Base ` K ) /\ x ( le ` K ) W ) -> F e. D )
27 13 22 1 2 ldilval 
 |-  ( ( ( K e. V /\ W e. H ) /\ F e. D /\ ( x e. ( Base ` K ) /\ x ( le ` K ) W ) ) -> ( F ` x ) = x )
28 11 26 18 21 27 syl112anc 
 |-  ( ( ( ( K e. V /\ W e. H ) /\ F e. D /\ G e. D ) /\ x e. ( Base ` K ) /\ x ( le ` K ) W ) -> ( F ` x ) = x )
29 20 25 28 3eqtrd 
 |-  ( ( ( ( K e. V /\ W e. H ) /\ F e. D /\ G e. D ) /\ x e. ( Base ` K ) /\ x ( le ` K ) W ) -> ( ( F o. G ) ` x ) = x )
30 29 3exp 
 |-  ( ( ( K e. V /\ W e. H ) /\ F e. D /\ G e. D ) -> ( x e. ( Base ` K ) -> ( x ( le ` K ) W -> ( ( F o. G ) ` x ) = x ) ) )
31 30 ralrimiv 
 |-  ( ( ( K e. V /\ W e. H ) /\ F e. D /\ G e. D ) -> A. x e. ( Base ` K ) ( x ( le ` K ) W -> ( ( F o. G ) ` x ) = x ) )
32 13 22 1 4 2 isldil 
 |-  ( ( K e. V /\ W e. H ) -> ( ( F o. G ) e. D <-> ( ( F o. G ) e. ( LAut ` K ) /\ A. x e. ( Base ` K ) ( x ( le ` K ) W -> ( ( F o. G ) ` x ) = x ) ) ) )
33 32 3ad2ant1 
 |-  ( ( ( K e. V /\ W e. H ) /\ F e. D /\ G e. D ) -> ( ( F o. G ) e. D <-> ( ( F o. G ) e. ( LAut ` K ) /\ A. x e. ( Base ` K ) ( x ( le ` K ) W -> ( ( F o. G ) ` x ) = x ) ) ) )
34 10 31 33 mpbir2and 
 |-  ( ( ( K e. V /\ W e. H ) /\ F e. D /\ G e. D ) -> ( F o. G ) e. D )