Metamath Proof Explorer

Theorem mrsubvrs

Description: The set of variables in a substitution is the union, indexed by the variables in the original expression, of the variables in the substitution to that variable. (Contributed by Mario Carneiro, 18-Jul-2016)

Ref Expression
Hypotheses mrsubco.s 
|- S = ( mRSubst ` T )
mrsubvrs.v 
|- V = ( mVR ` T )
mrsubvrs.r 
|- R = ( mREx ` T )
Assertion mrsubvrs 
|- ( ( F e. ran S /\ X e. R ) -> ( ran ( F ` X ) i^i V ) = U_ x e. ( ran X i^i V ) ( ran ( F ` <" x "> ) i^i V ) )

Proof

Step Hyp Ref Expression
1 mrsubco.s 
 |-  S = ( mRSubst ` T )
2 mrsubvrs.v 
 |-  V = ( mVR ` T )
3 mrsubvrs.r 
 |-  R = ( mREx ` T )
4 n0i 
 |-  ( F e. ran S -> -. ran S = (/) )
5 1 rnfvprc 
 |-  ( -. T e. _V -> ran S = (/) )
6 4 5 nsyl2 
 |-  ( F e. ran S -> T e. _V )
7 eqid 
 |-  ( mCN ` T ) = ( mCN ` T )
8 7 2 3 mrexval 
 |-  ( T e. _V -> R = Word ( ( mCN ` T ) u. V ) )
9 6 8 syl 
 |-  ( F e. ran S -> R = Word ( ( mCN ` T ) u. V ) )
10 9 eleq2d 
 |-  ( F e. ran S -> ( X e. R <-> X e. Word ( ( mCN ` T ) u. V ) ) )
11 fveq2 
 |-  ( v = (/) -> ( F ` v ) = ( F ` (/) ) )
12 11 rneqd 
 |-  ( v = (/) -> ran ( F ` v ) = ran ( F ` (/) ) )
13 12 ineq1d 
 |-  ( v = (/) -> ( ran ( F ` v ) i^i V ) = ( ran ( F ` (/) ) i^i V ) )
14 rneq 
 |-  ( v = (/) -> ran v = ran (/) )
15 rn0 
 |-  ran (/) = (/)
16 14 15 eqtrdi 
 |-  ( v = (/) -> ran v = (/) )
17 16 ineq1d 
 |-  ( v = (/) -> ( ran v i^i V ) = ( (/) i^i V ) )
18 0in 
 |-  ( (/) i^i V ) = (/)
19 17 18 eqtrdi 
 |-  ( v = (/) -> ( ran v i^i V ) = (/) )
20 19 iuneq1d 
 |-  ( v = (/) -> U_ x e. ( ran v i^i V ) ( ran ( F ` <" x "> ) i^i V ) = U_ x e. (/) ( ran ( F ` <" x "> ) i^i V ) )
21 0iun 
 |-  U_ x e. (/) ( ran ( F ` <" x "> ) i^i V ) = (/)
22 20 21 eqtrdi 
 |-  ( v = (/) -> U_ x e. ( ran v i^i V ) ( ran ( F ` <" x "> ) i^i V ) = (/) )
23 13 22 eqeq12d 
 |-  ( v = (/) -> ( ( ran ( F ` v ) i^i V ) = U_ x e. ( ran v i^i V ) ( ran ( F ` <" x "> ) i^i V ) <-> ( ran ( F ` (/) ) i^i V ) = (/) ) )
24 23 imbi2d 
 |-  ( v = (/) -> ( ( F e. ran S -> ( ran ( F ` v ) i^i V ) = U_ x e. ( ran v i^i V ) ( ran ( F ` <" x "> ) i^i V ) ) <-> ( F e. ran S -> ( ran ( F ` (/) ) i^i V ) = (/) ) ) )
25 fveq2 
 |-  ( v = y -> ( F ` v ) = ( F ` y ) )
26 25 rneqd 
 |-  ( v = y -> ran ( F ` v ) = ran ( F ` y ) )
27 26 ineq1d 
 |-  ( v = y -> ( ran ( F ` v ) i^i V ) = ( ran ( F ` y ) i^i V ) )
28 rneq 
 |-  ( v = y -> ran v = ran y )
29 28 ineq1d 
 |-  ( v = y -> ( ran v i^i V ) = ( ran y i^i V ) )
30 29 iuneq1d 
 |-  ( v = y -> U_ x e. ( ran v i^i V ) ( ran ( F ` <" x "> ) i^i V ) = U_ x e. ( ran y i^i V ) ( ran ( F ` <" x "> ) i^i V ) )
31 27 30 eqeq12d 
 |-  ( v = y -> ( ( ran ( F ` v ) i^i V ) = U_ x e. ( ran v i^i V ) ( ran ( F ` <" x "> ) i^i V ) <-> ( ran ( F ` y ) i^i V ) = U_ x e. ( ran y i^i V ) ( ran ( F ` <" x "> ) i^i V ) ) )
32 31 imbi2d 
 |-  ( v = y -> ( ( F e. ran S -> ( ran ( F ` v ) i^i V ) = U_ x e. ( ran v i^i V ) ( ran ( F ` <" x "> ) i^i V ) ) <-> ( F e. ran S -> ( ran ( F ` y ) i^i V ) = U_ x e. ( ran y i^i V ) ( ran ( F ` <" x "> ) i^i V ) ) ) )
33 fveq2 
 |-  ( v = ( y ++ <" z "> ) -> ( F ` v ) = ( F ` ( y ++ <" z "> ) ) )
34 33 rneqd 
 |-  ( v = ( y ++ <" z "> ) -> ran ( F ` v ) = ran ( F ` ( y ++ <" z "> ) ) )
35 34 ineq1d 
 |-  ( v = ( y ++ <" z "> ) -> ( ran ( F ` v ) i^i V ) = ( ran ( F ` ( y ++ <" z "> ) ) i^i V ) )
36 rneq 
 |-  ( v = ( y ++ <" z "> ) -> ran v = ran ( y ++ <" z "> ) )
37 36 ineq1d 
 |-  ( v = ( y ++ <" z "> ) -> ( ran v i^i V ) = ( ran ( y ++ <" z "> ) i^i V ) )
38 37 iuneq1d 
 |-  ( v = ( y ++ <" z "> ) -> U_ x e. ( ran v i^i V ) ( ran ( F ` <" x "> ) i^i V ) = U_ x e. ( ran ( y ++ <" z "> ) i^i V ) ( ran ( F ` <" x "> ) i^i V ) )
39 35 38 eqeq12d 
 |-  ( v = ( y ++ <" z "> ) -> ( ( ran ( F ` v ) i^i V ) = U_ x e. ( ran v i^i V ) ( ran ( F ` <" x "> ) i^i V ) <-> ( ran ( F ` ( y ++ <" z "> ) ) i^i V ) = U_ x e. ( ran ( y ++ <" z "> ) i^i V ) ( ran ( F ` <" x "> ) i^i V ) ) )
40 39 imbi2d 
 |-  ( v = ( y ++ <" z "> ) -> ( ( F e. ran S -> ( ran ( F ` v ) i^i V ) = U_ x e. ( ran v i^i V ) ( ran ( F ` <" x "> ) i^i V ) ) <-> ( F e. ran S -> ( ran ( F ` ( y ++ <" z "> ) ) i^i V ) = U_ x e. ( ran ( y ++ <" z "> ) i^i V ) ( ran ( F ` <" x "> ) i^i V ) ) ) )
41 fveq2 
 |-  ( v = X -> ( F ` v ) = ( F ` X ) )
42 41 rneqd 
 |-  ( v = X -> ran ( F ` v ) = ran ( F ` X ) )
43 42 ineq1d 
 |-  ( v = X -> ( ran ( F ` v ) i^i V ) = ( ran ( F ` X ) i^i V ) )
44 rneq 
 |-  ( v = X -> ran v = ran X )
45 44 ineq1d 
 |-  ( v = X -> ( ran v i^i V ) = ( ran X i^i V ) )
46 45 iuneq1d 
 |-  ( v = X -> U_ x e. ( ran v i^i V ) ( ran ( F ` <" x "> ) i^i V ) = U_ x e. ( ran X i^i V ) ( ran ( F ` <" x "> ) i^i V ) )
47 43 46 eqeq12d 
 |-  ( v = X -> ( ( ran ( F ` v ) i^i V ) = U_ x e. ( ran v i^i V ) ( ran ( F ` <" x "> ) i^i V ) <-> ( ran ( F ` X ) i^i V ) = U_ x e. ( ran X i^i V ) ( ran ( F ` <" x "> ) i^i V ) ) )
48 47 imbi2d 
 |-  ( v = X -> ( ( F e. ran S -> ( ran ( F ` v ) i^i V ) = U_ x e. ( ran v i^i V ) ( ran ( F ` <" x "> ) i^i V ) ) <-> ( F e. ran S -> ( ran ( F ` X ) i^i V ) = U_ x e. ( ran X i^i V ) ( ran ( F ` <" x "> ) i^i V ) ) ) )
49 1 mrsub0 
 |-  ( F e. ran S -> ( F ` (/) ) = (/) )
50 49 rneqd 
 |-  ( F e. ran S -> ran ( F ` (/) ) = ran (/) )
51 50 15 eqtrdi 
 |-  ( F e. ran S -> ran ( F ` (/) ) = (/) )
52 51 ineq1d 
 |-  ( F e. ran S -> ( ran ( F ` (/) ) i^i V ) = ( (/) i^i V ) )
53 52 18 eqtrdi 
 |-  ( F e. ran S -> ( ran ( F ` (/) ) i^i V ) = (/) )
54 uneq1 
 |-  ( ( ran ( F ` y ) i^i V ) = U_ x e. ( ran y i^i V ) ( ran ( F ` <" x "> ) i^i V ) -> ( ( ran ( F ` y ) i^i V ) u. ( ran ( F ` <" z "> ) i^i V ) ) = ( U_ x e. ( ran y i^i V ) ( ran ( F ` <" x "> ) i^i V ) u. ( ran ( F ` <" z "> ) i^i V ) ) )
55 simpl 
 |-  ( ( F e. ran S /\ ( y e. Word ( ( mCN ` T ) u. V ) /\ z e. ( ( mCN ` T ) u. V ) ) ) -> F e. ran S )
56 simprl 
 |-  ( ( F e. ran S /\ ( y e. Word ( ( mCN ` T ) u. V ) /\ z e. ( ( mCN ` T ) u. V ) ) ) -> y e. Word ( ( mCN ` T ) u. V ) )
57 9 adantr 
 |-  ( ( F e. ran S /\ ( y e. Word ( ( mCN ` T ) u. V ) /\ z e. ( ( mCN ` T ) u. V ) ) ) -> R = Word ( ( mCN ` T ) u. V ) )
58 56 57 eleqtrrd 
 |-  ( ( F e. ran S /\ ( y e. Word ( ( mCN ` T ) u. V ) /\ z e. ( ( mCN ` T ) u. V ) ) ) -> y e. R )
59 simprr 
 |-  ( ( F e. ran S /\ ( y e. Word ( ( mCN ` T ) u. V ) /\ z e. ( ( mCN ` T ) u. V ) ) ) -> z e. ( ( mCN ` T ) u. V ) )
60 59 s1cld 
 |-  ( ( F e. ran S /\ ( y e. Word ( ( mCN ` T ) u. V ) /\ z e. ( ( mCN ` T ) u. V ) ) ) -> <" z "> e. Word ( ( mCN ` T ) u. V ) )
61 60 57 eleqtrrd 
 |-  ( ( F e. ran S /\ ( y e. Word ( ( mCN ` T ) u. V ) /\ z e. ( ( mCN ` T ) u. V ) ) ) -> <" z "> e. R )
62 1 3 mrsubccat 
 |-  ( ( F e. ran S /\ y e. R /\ <" z "> e. R ) -> ( F ` ( y ++ <" z "> ) ) = ( ( F ` y ) ++ ( F ` <" z "> ) ) )
63 55 58 61 62 syl3anc 
 |-  ( ( F e. ran S /\ ( y e. Word ( ( mCN ` T ) u. V ) /\ z e. ( ( mCN ` T ) u. V ) ) ) -> ( F ` ( y ++ <" z "> ) ) = ( ( F ` y ) ++ ( F ` <" z "> ) ) )
64 63 rneqd 
 |-  ( ( F e. ran S /\ ( y e. Word ( ( mCN ` T ) u. V ) /\ z e. ( ( mCN ` T ) u. V ) ) ) -> ran ( F ` ( y ++ <" z "> ) ) = ran ( ( F ` y ) ++ ( F ` <" z "> ) ) )
65 1 3 mrsubf 
 |-  ( F e. ran S -> F : R --> R )
66 65 adantr 
 |-  ( ( F e. ran S /\ ( y e. Word ( ( mCN ` T ) u. V ) /\ z e. ( ( mCN ` T ) u. V ) ) ) -> F : R --> R )
67 66 58 ffvelrnd 
 |-  ( ( F e. ran S /\ ( y e. Word ( ( mCN ` T ) u. V ) /\ z e. ( ( mCN ` T ) u. V ) ) ) -> ( F ` y ) e. R )
68 67 57 eleqtrd 
 |-  ( ( F e. ran S /\ ( y e. Word ( ( mCN ` T ) u. V ) /\ z e. ( ( mCN ` T ) u. V ) ) ) -> ( F ` y ) e. Word ( ( mCN ` T ) u. V ) )
69 66 61 ffvelrnd 
 |-  ( ( F e. ran S /\ ( y e. Word ( ( mCN ` T ) u. V ) /\ z e. ( ( mCN ` T ) u. V ) ) ) -> ( F ` <" z "> ) e. R )
70 69 57 eleqtrd 
 |-  ( ( F e. ran S /\ ( y e. Word ( ( mCN ` T ) u. V ) /\ z e. ( ( mCN ` T ) u. V ) ) ) -> ( F ` <" z "> ) e. Word ( ( mCN ` T ) u. V ) )
71 ccatrn 
 |-  ( ( ( F ` y ) e. Word ( ( mCN ` T ) u. V ) /\ ( F ` <" z "> ) e. Word ( ( mCN ` T ) u. V ) ) -> ran ( ( F ` y ) ++ ( F ` <" z "> ) ) = ( ran ( F ` y ) u. ran ( F ` <" z "> ) ) )
72 68 70 71 syl2anc 
 |-  ( ( F e. ran S /\ ( y e. Word ( ( mCN ` T ) u. V ) /\ z e. ( ( mCN ` T ) u. V ) ) ) -> ran ( ( F ` y ) ++ ( F ` <" z "> ) ) = ( ran ( F ` y ) u. ran ( F ` <" z "> ) ) )
73 64 72 eqtrd 
 |-  ( ( F e. ran S /\ ( y e. Word ( ( mCN ` T ) u. V ) /\ z e. ( ( mCN ` T ) u. V ) ) ) -> ran ( F ` ( y ++ <" z "> ) ) = ( ran ( F ` y ) u. ran ( F ` <" z "> ) ) )
74 73 ineq1d 
 |-  ( ( F e. ran S /\ ( y e. Word ( ( mCN ` T ) u. V ) /\ z e. ( ( mCN ` T ) u. V ) ) ) -> ( ran ( F ` ( y ++ <" z "> ) ) i^i V ) = ( ( ran ( F ` y ) u. ran ( F ` <" z "> ) ) i^i V ) )
75 indir 
 |-  ( ( ran ( F ` y ) u. ran ( F ` <" z "> ) ) i^i V ) = ( ( ran ( F ` y ) i^i V ) u. ( ran ( F ` <" z "> ) i^i V ) )
76 74 75 eqtrdi 
 |-  ( ( F e. ran S /\ ( y e. Word ( ( mCN ` T ) u. V ) /\ z e. ( ( mCN ` T ) u. V ) ) ) -> ( ran ( F ` ( y ++ <" z "> ) ) i^i V ) = ( ( ran ( F ` y ) i^i V ) u. ( ran ( F ` <" z "> ) i^i V ) ) )
77 ccatrn 
 |-  ( ( y e. Word ( ( mCN ` T ) u. V ) /\ <" z "> e. Word ( ( mCN ` T ) u. V ) ) -> ran ( y ++ <" z "> ) = ( ran y u. ran <" z "> ) )
78 56 60 77 syl2anc 
 |-  ( ( F e. ran S /\ ( y e. Word ( ( mCN ` T ) u. V ) /\ z e. ( ( mCN ` T ) u. V ) ) ) -> ran ( y ++ <" z "> ) = ( ran y u. ran <" z "> ) )
79 s1rn 
 |-  ( z e. ( ( mCN ` T ) u. V ) -> ran <" z "> = { z } )
80 79 ad2antll 
 |-  ( ( F e. ran S /\ ( y e. Word ( ( mCN ` T ) u. V ) /\ z e. ( ( mCN ` T ) u. V ) ) ) -> ran <" z "> = { z } )
81 80 uneq2d 
 |-  ( ( F e. ran S /\ ( y e. Word ( ( mCN ` T ) u. V ) /\ z e. ( ( mCN ` T ) u. V ) ) ) -> ( ran y u. ran <" z "> ) = ( ran y u. { z } ) )
82 78 81 eqtrd 
 |-  ( ( F e. ran S /\ ( y e. Word ( ( mCN ` T ) u. V ) /\ z e. ( ( mCN ` T ) u. V ) ) ) -> ran ( y ++ <" z "> ) = ( ran y u. { z } ) )
83 82 ineq1d 
 |-  ( ( F e. ran S /\ ( y e. Word ( ( mCN ` T ) u. V ) /\ z e. ( ( mCN ` T ) u. V ) ) ) -> ( ran ( y ++ <" z "> ) i^i V ) = ( ( ran y u. { z } ) i^i V ) )
84 indir 
 |-  ( ( ran y u. { z } ) i^i V ) = ( ( ran y i^i V ) u. ( { z } i^i V ) )
85 83 84 eqtrdi 
 |-  ( ( F e. ran S /\ ( y e. Word ( ( mCN ` T ) u. V ) /\ z e. ( ( mCN ` T ) u. V ) ) ) -> ( ran ( y ++ <" z "> ) i^i V ) = ( ( ran y i^i V ) u. ( { z } i^i V ) ) )
86 85 iuneq1d 
 |-  ( ( F e. ran S /\ ( y e. Word ( ( mCN ` T ) u. V ) /\ z e. ( ( mCN ` T ) u. V ) ) ) -> U_ x e. ( ran ( y ++ <" z "> ) i^i V ) ( ran ( F ` <" x "> ) i^i V ) = U_ x e. ( ( ran y i^i V ) u. ( { z } i^i V ) ) ( ran ( F ` <" x "> ) i^i V ) )
87 iunxun 
 |-  U_ x e. ( ( ran y i^i V ) u. ( { z } i^i V ) ) ( ran ( F ` <" x "> ) i^i V ) = ( U_ x e. ( ran y i^i V ) ( ran ( F ` <" x "> ) i^i V ) u. U_ x e. ( { z } i^i V ) ( ran ( F ` <" x "> ) i^i V ) )
88 86 87 eqtrdi 
 |-  ( ( F e. ran S /\ ( y e. Word ( ( mCN ` T ) u. V ) /\ z e. ( ( mCN ` T ) u. V ) ) ) -> U_ x e. ( ran ( y ++ <" z "> ) i^i V ) ( ran ( F ` <" x "> ) i^i V ) = ( U_ x e. ( ran y i^i V ) ( ran ( F ` <" x "> ) i^i V ) u. U_ x e. ( { z } i^i V ) ( ran ( F ` <" x "> ) i^i V ) ) )
89 simpr 
 |-  ( ( ( F e. ran S /\ ( y e. Word ( ( mCN ` T ) u. V ) /\ z e. ( ( mCN ` T ) u. V ) ) ) /\ z e. V ) -> z e. V )
90 89 snssd 
 |-  ( ( ( F e. ran S /\ ( y e. Word ( ( mCN ` T ) u. V ) /\ z e. ( ( mCN ` T ) u. V ) ) ) /\ z e. V ) -> { z } C_ V )
91 df-ss 
 |-  ( { z } C_ V <-> ( { z } i^i V ) = { z } )
92 90 91 sylib 
 |-  ( ( ( F e. ran S /\ ( y e. Word ( ( mCN ` T ) u. V ) /\ z e. ( ( mCN ` T ) u. V ) ) ) /\ z e. V ) -> ( { z } i^i V ) = { z } )
93 92 iuneq1d 
 |-  ( ( ( F e. ran S /\ ( y e. Word ( ( mCN ` T ) u. V ) /\ z e. ( ( mCN ` T ) u. V ) ) ) /\ z e. V ) -> U_ x e. ( { z } i^i V ) ( ran ( F ` <" x "> ) i^i V ) = U_ x e. { z } ( ran ( F ` <" x "> ) i^i V ) )
94 vex 
 |-  z e. _V
95 s1eq 
 |-  ( x = z -> <" x "> = <" z "> )
96 95 fveq2d 
 |-  ( x = z -> ( F ` <" x "> ) = ( F ` <" z "> ) )
97 96 rneqd 
 |-  ( x = z -> ran ( F ` <" x "> ) = ran ( F ` <" z "> ) )
98 97 ineq1d 
 |-  ( x = z -> ( ran ( F ` <" x "> ) i^i V ) = ( ran ( F ` <" z "> ) i^i V ) )
99 94 98 iunxsn 
 |-  U_ x e. { z } ( ran ( F ` <" x "> ) i^i V ) = ( ran ( F ` <" z "> ) i^i V )
100 93 99 eqtrdi 
 |-  ( ( ( F e. ran S /\ ( y e. Word ( ( mCN ` T ) u. V ) /\ z e. ( ( mCN ` T ) u. V ) ) ) /\ z e. V ) -> U_ x e. ( { z } i^i V ) ( ran ( F ` <" x "> ) i^i V ) = ( ran ( F ` <" z "> ) i^i V ) )
101 incom 
 |-  ( { z } i^i V ) = ( V i^i { z } )
102 simpr 
 |-  ( ( ( F e. ran S /\ ( y e. Word ( ( mCN ` T ) u. V ) /\ z e. ( ( mCN ` T ) u. V ) ) ) /\ -. z e. V ) -> -. z e. V )
103 disjsn 
 |-  ( ( V i^i { z } ) = (/) <-> -. z e. V )
104 102 103 sylibr 
 |-  ( ( ( F e. ran S /\ ( y e. Word ( ( mCN ` T ) u. V ) /\ z e. ( ( mCN ` T ) u. V ) ) ) /\ -. z e. V ) -> ( V i^i { z } ) = (/) )
105 101 104 syl5eq 
 |-  ( ( ( F e. ran S /\ ( y e. Word ( ( mCN ` T ) u. V ) /\ z e. ( ( mCN ` T ) u. V ) ) ) /\ -. z e. V ) -> ( { z } i^i V ) = (/) )
106 105 iuneq1d 
 |-  ( ( ( F e. ran S /\ ( y e. Word ( ( mCN ` T ) u. V ) /\ z e. ( ( mCN ` T ) u. V ) ) ) /\ -. z e. V ) -> U_ x e. ( { z } i^i V ) ( ran ( F ` <" x "> ) i^i V ) = U_ x e. (/) ( ran ( F ` <" x "> ) i^i V ) )
107 55 adantr 
 |-  ( ( ( F e. ran S /\ ( y e. Word ( ( mCN ` T ) u. V ) /\ z e. ( ( mCN ` T ) u. V ) ) ) /\ -. z e. V ) -> F e. ran S )
108 eldif 
 |-  ( z e. ( ( ( mCN ` T ) u. V ) \ V ) <-> ( z e. ( ( mCN ` T ) u. V ) /\ -. z e. V ) )
109 108 biimpri 
 |-  ( ( z e. ( ( mCN ` T ) u. V ) /\ -. z e. V ) -> z e. ( ( ( mCN ` T ) u. V ) \ V ) )
110 59 109 sylan 
 |-  ( ( ( F e. ran S /\ ( y e. Word ( ( mCN ` T ) u. V ) /\ z e. ( ( mCN ` T ) u. V ) ) ) /\ -. z e. V ) -> z e. ( ( ( mCN ` T ) u. V ) \ V ) )
111 difun2 
 |-  ( ( ( mCN ` T ) u. V ) \ V ) = ( ( mCN ` T ) \ V )
112 110 111 eleqtrdi 
 |-  ( ( ( F e. ran S /\ ( y e. Word ( ( mCN ` T ) u. V ) /\ z e. ( ( mCN ` T ) u. V ) ) ) /\ -. z e. V ) -> z e. ( ( mCN ` T ) \ V ) )
113 1 3 2 7 mrsubcn 
 |-  ( ( F e. ran S /\ z e. ( ( mCN ` T ) \ V ) ) -> ( F ` <" z "> ) = <" z "> )
114 107 112 113 syl2anc 
 |-  ( ( ( F e. ran S /\ ( y e. Word ( ( mCN ` T ) u. V ) /\ z e. ( ( mCN ` T ) u. V ) ) ) /\ -. z e. V ) -> ( F ` <" z "> ) = <" z "> )
115 114 rneqd 
 |-  ( ( ( F e. ran S /\ ( y e. Word ( ( mCN ` T ) u. V ) /\ z e. ( ( mCN ` T ) u. V ) ) ) /\ -. z e. V ) -> ran ( F ` <" z "> ) = ran <" z "> )
116 80 adantr 
 |-  ( ( ( F e. ran S /\ ( y e. Word ( ( mCN ` T ) u. V ) /\ z e. ( ( mCN ` T ) u. V ) ) ) /\ -. z e. V ) -> ran <" z "> = { z } )
117 115 116 eqtrd 
 |-  ( ( ( F e. ran S /\ ( y e. Word ( ( mCN ` T ) u. V ) /\ z e. ( ( mCN ` T ) u. V ) ) ) /\ -. z e. V ) -> ran ( F ` <" z "> ) = { z } )
118 117 ineq1d 
 |-  ( ( ( F e. ran S /\ ( y e. Word ( ( mCN ` T ) u. V ) /\ z e. ( ( mCN ` T ) u. V ) ) ) /\ -. z e. V ) -> ( ran ( F ` <" z "> ) i^i V ) = ( { z } i^i V ) )
119 118 105 eqtrd 
 |-  ( ( ( F e. ran S /\ ( y e. Word ( ( mCN ` T ) u. V ) /\ z e. ( ( mCN ` T ) u. V ) ) ) /\ -. z e. V ) -> ( ran ( F ` <" z "> ) i^i V ) = (/) )
120 21 106 119 3eqtr4a 
 |-  ( ( ( F e. ran S /\ ( y e. Word ( ( mCN ` T ) u. V ) /\ z e. ( ( mCN ` T ) u. V ) ) ) /\ -. z e. V ) -> U_ x e. ( { z } i^i V ) ( ran ( F ` <" x "> ) i^i V ) = ( ran ( F ` <" z "> ) i^i V ) )
121 100 120 pm2.61dan 
 |-  ( ( F e. ran S /\ ( y e. Word ( ( mCN ` T ) u. V ) /\ z e. ( ( mCN ` T ) u. V ) ) ) -> U_ x e. ( { z } i^i V ) ( ran ( F ` <" x "> ) i^i V ) = ( ran ( F ` <" z "> ) i^i V ) )
122 121 uneq2d 
 |-  ( ( F e. ran S /\ ( y e. Word ( ( mCN ` T ) u. V ) /\ z e. ( ( mCN ` T ) u. V ) ) ) -> ( U_ x e. ( ran y i^i V ) ( ran ( F ` <" x "> ) i^i V ) u. U_ x e. ( { z } i^i V ) ( ran ( F ` <" x "> ) i^i V ) ) = ( U_ x e. ( ran y i^i V ) ( ran ( F ` <" x "> ) i^i V ) u. ( ran ( F ` <" z "> ) i^i V ) ) )
123 88 122 eqtrd 
 |-  ( ( F e. ran S /\ ( y e. Word ( ( mCN ` T ) u. V ) /\ z e. ( ( mCN ` T ) u. V ) ) ) -> U_ x e. ( ran ( y ++ <" z "> ) i^i V ) ( ran ( F ` <" x "> ) i^i V ) = ( U_ x e. ( ran y i^i V ) ( ran ( F ` <" x "> ) i^i V ) u. ( ran ( F ` <" z "> ) i^i V ) ) )
124 76 123 eqeq12d 
 |-  ( ( F e. ran S /\ ( y e. Word ( ( mCN ` T ) u. V ) /\ z e. ( ( mCN ` T ) u. V ) ) ) -> ( ( ran ( F ` ( y ++ <" z "> ) ) i^i V ) = U_ x e. ( ran ( y ++ <" z "> ) i^i V ) ( ran ( F ` <" x "> ) i^i V ) <-> ( ( ran ( F ` y ) i^i V ) u. ( ran ( F ` <" z "> ) i^i V ) ) = ( U_ x e. ( ran y i^i V ) ( ran ( F ` <" x "> ) i^i V ) u. ( ran ( F ` <" z "> ) i^i V ) ) ) )
125 54 124 syl5ibr 
 |-  ( ( F e. ran S /\ ( y e. Word ( ( mCN ` T ) u. V ) /\ z e. ( ( mCN ` T ) u. V ) ) ) -> ( ( ran ( F ` y ) i^i V ) = U_ x e. ( ran y i^i V ) ( ran ( F ` <" x "> ) i^i V ) -> ( ran ( F ` ( y ++ <" z "> ) ) i^i V ) = U_ x e. ( ran ( y ++ <" z "> ) i^i V ) ( ran ( F ` <" x "> ) i^i V ) ) )
126 125 expcom 
 |-  ( ( y e. Word ( ( mCN ` T ) u. V ) /\ z e. ( ( mCN ` T ) u. V ) ) -> ( F e. ran S -> ( ( ran ( F ` y ) i^i V ) = U_ x e. ( ran y i^i V ) ( ran ( F ` <" x "> ) i^i V ) -> ( ran ( F ` ( y ++ <" z "> ) ) i^i V ) = U_ x e. ( ran ( y ++ <" z "> ) i^i V ) ( ran ( F ` <" x "> ) i^i V ) ) ) )
127 126 a2d 
 |-  ( ( y e. Word ( ( mCN ` T ) u. V ) /\ z e. ( ( mCN ` T ) u. V ) ) -> ( ( F e. ran S -> ( ran ( F ` y ) i^i V ) = U_ x e. ( ran y i^i V ) ( ran ( F ` <" x "> ) i^i V ) ) -> ( F e. ran S -> ( ran ( F ` ( y ++ <" z "> ) ) i^i V ) = U_ x e. ( ran ( y ++ <" z "> ) i^i V ) ( ran ( F ` <" x "> ) i^i V ) ) ) )
128 24 32 40 48 53 127 wrdind 
 |-  ( X e. Word ( ( mCN ` T ) u. V ) -> ( F e. ran S -> ( ran ( F ` X ) i^i V ) = U_ x e. ( ran X i^i V ) ( ran ( F ` <" x "> ) i^i V ) ) )
129 128 com12 
 |-  ( F e. ran S -> ( X e. Word ( ( mCN ` T ) u. V ) -> ( ran ( F ` X ) i^i V ) = U_ x e. ( ran X i^i V ) ( ran ( F ` <" x "> ) i^i V ) ) )
130 10 129 sylbid 
 |-  ( F e. ran S -> ( X e. R -> ( ran ( F ` X ) i^i V ) = U_ x e. ( ran X i^i V ) ( ran ( F ` <" x "> ) i^i V ) ) )
131 130 imp 
 |-  ( ( F e. ran S /\ X e. R ) -> ( ran ( F ` X ) i^i V ) = U_ x e. ( ran X i^i V ) ( ran ( F ` <" x "> ) i^i V ) )