Metamath Proof Explorer

Theorem mrsubco

Description: The composition of two substitutions is a substitution. (Contributed by Mario Carneiro, 18-Jul-2016)

Ref Expression
Hypothesis mrsubco.s 
|- S = ( mRSubst ` T )
Assertion mrsubco 
|- ( ( F e. ran S /\ G e. ran S ) -> ( F o. G ) e. ran S )

Proof

Step Hyp Ref Expression
1 mrsubco.s 
 |-  S = ( mRSubst ` T )
2 eqid 
 |-  ( mREx ` T ) = ( mREx ` T )
3 1 2 mrsubf 
 |-  ( F e. ran S -> F : ( mREx ` T ) --> ( mREx ` T ) )
4 3 adantr 
 |-  ( ( F e. ran S /\ G e. ran S ) -> F : ( mREx ` T ) --> ( mREx ` T ) )
5 1 2 mrsubf 
 |-  ( G e. ran S -> G : ( mREx ` T ) --> ( mREx ` T ) )
6 5 adantl 
 |-  ( ( F e. ran S /\ G e. ran S ) -> G : ( mREx ` T ) --> ( mREx ` T ) )
7 fco 
 |-  ( ( F : ( mREx ` T ) --> ( mREx ` T ) /\ G : ( mREx ` T ) --> ( mREx ` T ) ) -> ( F o. G ) : ( mREx ` T ) --> ( mREx ` T ) )
8 4 6 7 syl2anc 
 |-  ( ( F e. ran S /\ G e. ran S ) -> ( F o. G ) : ( mREx ` T ) --> ( mREx ` T ) )
9 6 adantr 
 |-  ( ( ( F e. ran S /\ G e. ran S ) /\ c e. ( ( mCN ` T ) \ ( mVR ` T ) ) ) -> G : ( mREx ` T ) --> ( mREx ` T ) )
10 eldifi 
 |-  ( c e. ( ( mCN ` T ) \ ( mVR ` T ) ) -> c e. ( mCN ` T ) )
11 elun1 
 |-  ( c e. ( mCN ` T ) -> c e. ( ( mCN ` T ) u. ( mVR ` T ) ) )
12 10 11 syl 
 |-  ( c e. ( ( mCN ` T ) \ ( mVR ` T ) ) -> c e. ( ( mCN ` T ) u. ( mVR ` T ) ) )
13 12 adantl 
 |-  ( ( ( F e. ran S /\ G e. ran S ) /\ c e. ( ( mCN ` T ) \ ( mVR ` T ) ) ) -> c e. ( ( mCN ` T ) u. ( mVR ` T ) ) )
14 13 s1cld 
 |-  ( ( ( F e. ran S /\ G e. ran S ) /\ c e. ( ( mCN ` T ) \ ( mVR ` T ) ) ) -> <" c "> e. Word ( ( mCN ` T ) u. ( mVR ` T ) ) )
15 n0i 
 |-  ( F e. ran S -> -. ran S = (/) )
16 1 rnfvprc 
 |-  ( -. T e. _V -> ran S = (/) )
17 15 16 nsyl2 
 |-  ( F e. ran S -> T e. _V )
18 17 adantr 
 |-  ( ( F e. ran S /\ G e. ran S ) -> T e. _V )
19 18 adantr 
 |-  ( ( ( F e. ran S /\ G e. ran S ) /\ c e. ( ( mCN ` T ) \ ( mVR ` T ) ) ) -> T e. _V )
20 eqid 
 |-  ( mCN ` T ) = ( mCN ` T )
21 eqid 
 |-  ( mVR ` T ) = ( mVR ` T )
22 20 21 2 mrexval 
 |-  ( T e. _V -> ( mREx ` T ) = Word ( ( mCN ` T ) u. ( mVR ` T ) ) )
23 19 22 syl 
 |-  ( ( ( F e. ran S /\ G e. ran S ) /\ c e. ( ( mCN ` T ) \ ( mVR ` T ) ) ) -> ( mREx ` T ) = Word ( ( mCN ` T ) u. ( mVR ` T ) ) )
24 14 23 eleqtrrd 
 |-  ( ( ( F e. ran S /\ G e. ran S ) /\ c e. ( ( mCN ` T ) \ ( mVR ` T ) ) ) -> <" c "> e. ( mREx ` T ) )
25 fvco3 
 |-  ( ( G : ( mREx ` T ) --> ( mREx ` T ) /\ <" c "> e. ( mREx ` T ) ) -> ( ( F o. G ) ` <" c "> ) = ( F ` ( G ` <" c "> ) ) )
26 9 24 25 syl2anc 
 |-  ( ( ( F e. ran S /\ G e. ran S ) /\ c e. ( ( mCN ` T ) \ ( mVR ` T ) ) ) -> ( ( F o. G ) ` <" c "> ) = ( F ` ( G ` <" c "> ) ) )
27 1 2 21 20 mrsubcn 
 |-  ( ( G e. ran S /\ c e. ( ( mCN ` T ) \ ( mVR ` T ) ) ) -> ( G ` <" c "> ) = <" c "> )
28 27 adantll 
 |-  ( ( ( F e. ran S /\ G e. ran S ) /\ c e. ( ( mCN ` T ) \ ( mVR ` T ) ) ) -> ( G ` <" c "> ) = <" c "> )
29 28 fveq2d 
 |-  ( ( ( F e. ran S /\ G e. ran S ) /\ c e. ( ( mCN ` T ) \ ( mVR ` T ) ) ) -> ( F ` ( G ` <" c "> ) ) = ( F ` <" c "> ) )
30 1 2 21 20 mrsubcn 
 |-  ( ( F e. ran S /\ c e. ( ( mCN ` T ) \ ( mVR ` T ) ) ) -> ( F ` <" c "> ) = <" c "> )
31 30 adantlr 
 |-  ( ( ( F e. ran S /\ G e. ran S ) /\ c e. ( ( mCN ` T ) \ ( mVR ` T ) ) ) -> ( F ` <" c "> ) = <" c "> )
32 26 29 31 3eqtrd 
 |-  ( ( ( F e. ran S /\ G e. ran S ) /\ c e. ( ( mCN ` T ) \ ( mVR ` T ) ) ) -> ( ( F o. G ) ` <" c "> ) = <" c "> )
33 32 ralrimiva 
 |-  ( ( F e. ran S /\ G e. ran S ) -> A. c e. ( ( mCN ` T ) \ ( mVR ` T ) ) ( ( F o. G ) ` <" c "> ) = <" c "> )
34 1 2 mrsubccat 
 |-  ( ( G e. ran S /\ x e. ( mREx ` T ) /\ y e. ( mREx ` T ) ) -> ( G ` ( x ++ y ) ) = ( ( G ` x ) ++ ( G ` y ) ) )
35 34 3expb 
 |-  ( ( G e. ran S /\ ( x e. ( mREx ` T ) /\ y e. ( mREx ` T ) ) ) -> ( G ` ( x ++ y ) ) = ( ( G ` x ) ++ ( G ` y ) ) )
36 35 adantll 
 |-  ( ( ( F e. ran S /\ G e. ran S ) /\ ( x e. ( mREx ` T ) /\ y e. ( mREx ` T ) ) ) -> ( G ` ( x ++ y ) ) = ( ( G ` x ) ++ ( G ` y ) ) )
37 36 fveq2d 
 |-  ( ( ( F e. ran S /\ G e. ran S ) /\ ( x e. ( mREx ` T ) /\ y e. ( mREx ` T ) ) ) -> ( F ` ( G ` ( x ++ y ) ) ) = ( F ` ( ( G ` x ) ++ ( G ` y ) ) ) )
38 simpll 
 |-  ( ( ( F e. ran S /\ G e. ran S ) /\ ( x e. ( mREx ` T ) /\ y e. ( mREx ` T ) ) ) -> F e. ran S )
39 6 adantr 
 |-  ( ( ( F e. ran S /\ G e. ran S ) /\ ( x e. ( mREx ` T ) /\ y e. ( mREx ` T ) ) ) -> G : ( mREx ` T ) --> ( mREx ` T ) )
40 simprl 
 |-  ( ( ( F e. ran S /\ G e. ran S ) /\ ( x e. ( mREx ` T ) /\ y e. ( mREx ` T ) ) ) -> x e. ( mREx ` T ) )
41 39 40 ffvelcdmd 
 |-  ( ( ( F e. ran S /\ G e. ran S ) /\ ( x e. ( mREx ` T ) /\ y e. ( mREx ` T ) ) ) -> ( G ` x ) e. ( mREx ` T ) )
42 simprr 
 |-  ( ( ( F e. ran S /\ G e. ran S ) /\ ( x e. ( mREx ` T ) /\ y e. ( mREx ` T ) ) ) -> y e. ( mREx ` T ) )
43 39 42 ffvelcdmd 
 |-  ( ( ( F e. ran S /\ G e. ran S ) /\ ( x e. ( mREx ` T ) /\ y e. ( mREx ` T ) ) ) -> ( G ` y ) e. ( mREx ` T ) )
44 1 2 mrsubccat 
 |-  ( ( F e. ran S /\ ( G ` x ) e. ( mREx ` T ) /\ ( G ` y ) e. ( mREx ` T ) ) -> ( F ` ( ( G ` x ) ++ ( G ` y ) ) ) = ( ( F ` ( G ` x ) ) ++ ( F ` ( G ` y ) ) ) )
45 38 41 43 44 syl3anc 
 |-  ( ( ( F e. ran S /\ G e. ran S ) /\ ( x e. ( mREx ` T ) /\ y e. ( mREx ` T ) ) ) -> ( F ` ( ( G ` x ) ++ ( G ` y ) ) ) = ( ( F ` ( G ` x ) ) ++ ( F ` ( G ` y ) ) ) )
46 37 45 eqtrd 
 |-  ( ( ( F e. ran S /\ G e. ran S ) /\ ( x e. ( mREx ` T ) /\ y e. ( mREx ` T ) ) ) -> ( F ` ( G ` ( x ++ y ) ) ) = ( ( F ` ( G ` x ) ) ++ ( F ` ( G ` y ) ) ) )
47 18 22 syl 
 |-  ( ( F e. ran S /\ G e. ran S ) -> ( mREx ` T ) = Word ( ( mCN ` T ) u. ( mVR ` T ) ) )
48 47 adantr 
 |-  ( ( ( F e. ran S /\ G e. ran S ) /\ ( x e. ( mREx ` T ) /\ y e. ( mREx ` T ) ) ) -> ( mREx ` T ) = Word ( ( mCN ` T ) u. ( mVR ` T ) ) )
49 40 48 eleqtrd 
 |-  ( ( ( F e. ran S /\ G e. ran S ) /\ ( x e. ( mREx ` T ) /\ y e. ( mREx ` T ) ) ) -> x e. Word ( ( mCN ` T ) u. ( mVR ` T ) ) )
50 42 48 eleqtrd 
 |-  ( ( ( F e. ran S /\ G e. ran S ) /\ ( x e. ( mREx ` T ) /\ y e. ( mREx ` T ) ) ) -> y e. Word ( ( mCN ` T ) u. ( mVR ` T ) ) )
51 ccatcl 
 |-  ( ( x e. Word ( ( mCN ` T ) u. ( mVR ` T ) ) /\ y e. Word ( ( mCN ` T ) u. ( mVR ` T ) ) ) -> ( x ++ y ) e. Word ( ( mCN ` T ) u. ( mVR ` T ) ) )
52 49 50 51 syl2anc 
 |-  ( ( ( F e. ran S /\ G e. ran S ) /\ ( x e. ( mREx ` T ) /\ y e. ( mREx ` T ) ) ) -> ( x ++ y ) e. Word ( ( mCN ` T ) u. ( mVR ` T ) ) )
53 52 48 eleqtrrd 
 |-  ( ( ( F e. ran S /\ G e. ran S ) /\ ( x e. ( mREx ` T ) /\ y e. ( mREx ` T ) ) ) -> ( x ++ y ) e. ( mREx ` T ) )
54 fvco3 
 |-  ( ( G : ( mREx ` T ) --> ( mREx ` T ) /\ ( x ++ y ) e. ( mREx ` T ) ) -> ( ( F o. G ) ` ( x ++ y ) ) = ( F ` ( G ` ( x ++ y ) ) ) )
55 39 53 54 syl2anc 
 |-  ( ( ( F e. ran S /\ G e. ran S ) /\ ( x e. ( mREx ` T ) /\ y e. ( mREx ` T ) ) ) -> ( ( F o. G ) ` ( x ++ y ) ) = ( F ` ( G ` ( x ++ y ) ) ) )
56 fvco3 
 |-  ( ( G : ( mREx ` T ) --> ( mREx ` T ) /\ x e. ( mREx ` T ) ) -> ( ( F o. G ) ` x ) = ( F ` ( G ` x ) ) )
57 39 40 56 syl2anc 
 |-  ( ( ( F e. ran S /\ G e. ran S ) /\ ( x e. ( mREx ` T ) /\ y e. ( mREx ` T ) ) ) -> ( ( F o. G ) ` x ) = ( F ` ( G ` x ) ) )
58 fvco3 
 |-  ( ( G : ( mREx ` T ) --> ( mREx ` T ) /\ y e. ( mREx ` T ) ) -> ( ( F o. G ) ` y ) = ( F ` ( G ` y ) ) )
59 39 42 58 syl2anc 
 |-  ( ( ( F e. ran S /\ G e. ran S ) /\ ( x e. ( mREx ` T ) /\ y e. ( mREx ` T ) ) ) -> ( ( F o. G ) ` y ) = ( F ` ( G ` y ) ) )
60 57 59 oveq12d 
 |-  ( ( ( F e. ran S /\ G e. ran S ) /\ ( x e. ( mREx ` T ) /\ y e. ( mREx ` T ) ) ) -> ( ( ( F o. G ) ` x ) ++ ( ( F o. G ) ` y ) ) = ( ( F ` ( G ` x ) ) ++ ( F ` ( G ` y ) ) ) )
61 46 55 60 3eqtr4d 
 |-  ( ( ( F e. ran S /\ G e. ran S ) /\ ( x e. ( mREx ` T ) /\ y e. ( mREx ` T ) ) ) -> ( ( F o. G ) ` ( x ++ y ) ) = ( ( ( F o. G ) ` x ) ++ ( ( F o. G ) ` y ) ) )
62 61 ralrimivva 
 |-  ( ( F e. ran S /\ G e. ran S ) -> A. x e. ( mREx ` T ) A. y e. ( mREx ` T ) ( ( F o. G ) ` ( x ++ y ) ) = ( ( ( F o. G ) ` x ) ++ ( ( F o. G ) ` y ) ) )
63 1 2 21 20 elmrsubrn 
 |-  ( T e. _V -> ( ( F o. G ) e. ran S <-> ( ( F o. G ) : ( mREx ` T ) --> ( mREx ` T ) /\ A. c e. ( ( mCN ` T ) \ ( mVR ` T ) ) ( ( F o. G ) ` <" c "> ) = <" c "> /\ A. x e. ( mREx ` T ) A. y e. ( mREx ` T ) ( ( F o. G ) ` ( x ++ y ) ) = ( ( ( F o. G ) ` x ) ++ ( ( F o. G ) ` y ) ) ) ) )
64 18 63 syl 
 |-  ( ( F e. ran S /\ G e. ran S ) -> ( ( F o. G ) e. ran S <-> ( ( F o. G ) : ( mREx ` T ) --> ( mREx ` T ) /\ A. c e. ( ( mCN ` T ) \ ( mVR ` T ) ) ( ( F o. G ) ` <" c "> ) = <" c "> /\ A. x e. ( mREx ` T ) A. y e. ( mREx ` T ) ( ( F o. G ) ` ( x ++ y ) ) = ( ( ( F o. G ) ` x ) ++ ( ( F o. G ) ` y ) ) ) ) )
65 8 33 62 64 mpbir3and 
 |-  ( ( F e. ran S /\ G e. ran S ) -> ( F o. G ) e. ran S )