Metamath Proof Explorer


Theorem elmrsubrn

Description: Characterization of the substitutions as functions from expressions to expressions that distribute under concatenation and map constants to themselves. (The constant part uses ( C \ V ) because we don't know that C and V are disjoint until we get to ismfs .) (Contributed by Mario Carneiro, 18-Jul-2016)

Ref Expression
Hypotheses mrsubccat.s S = mRSubst T
mrsubccat.r R = mREx T
mrsubcn.v V = mVR T
mrsubcn.c C = mCN T
Assertion elmrsubrn T W F ran S F : R R c C V F ⟨“ c ”⟩ = ⟨“ c ”⟩ x R y R F x ++ y = F x ++ F y

Proof

Step Hyp Ref Expression
1 mrsubccat.s S = mRSubst T
2 mrsubccat.r R = mREx T
3 mrsubcn.v V = mVR T
4 mrsubcn.c C = mCN T
5 1 2 mrsubf F ran S F : R R
6 1 2 3 4 mrsubcn F ran S c C V F ⟨“ c ”⟩ = ⟨“ c ”⟩
7 6 ralrimiva F ran S c C V F ⟨“ c ”⟩ = ⟨“ c ”⟩
8 1 2 mrsubccat F ran S x R y R F x ++ y = F x ++ F y
9 8 3expb F ran S x R y R F x ++ y = F x ++ F y
10 9 ralrimivva F ran S x R y R F x ++ y = F x ++ F y
11 5 7 10 3jca F ran S F : R R c C V F ⟨“ c ”⟩ = ⟨“ c ”⟩ x R y R F x ++ y = F x ++ F y
12 4 3 2 mrexval T W R = Word C V
13 12 adantr T W F : R R c C V F ⟨“ c ”⟩ = ⟨“ c ”⟩ x R y R F x ++ y = F x ++ F y R = Word C V
14 s1eq w = v ⟨“ w ”⟩ = ⟨“ v ”⟩
15 14 fveq2d w = v F ⟨“ w ”⟩ = F ⟨“ v ”⟩
16 eqid w V F ⟨“ w ”⟩ = w V F ⟨“ w ”⟩
17 fvex F ⟨“ v ”⟩ V
18 15 16 17 fvmpt v V w V F ⟨“ w ”⟩ v = F ⟨“ v ”⟩
19 18 adantl T W F : R R c C V F ⟨“ c ”⟩ = ⟨“ c ”⟩ x R y R F x ++ y = F x ++ F y v C V v V w V F ⟨“ w ”⟩ v = F ⟨“ v ”⟩
20 difun2 C V V = C V
21 20 eleq2i v C V V v C V
22 eldif v C V V v C V ¬ v V
23 21 22 bitr3i v C V v C V ¬ v V
24 simpr2 T W F : R R c C V F ⟨“ c ”⟩ = ⟨“ c ”⟩ x R y R F x ++ y = F x ++ F y c C V F ⟨“ c ”⟩ = ⟨“ c ”⟩
25 s1eq c = v ⟨“ c ”⟩ = ⟨“ v ”⟩
26 25 fveq2d c = v F ⟨“ c ”⟩ = F ⟨“ v ”⟩
27 26 25 eqeq12d c = v F ⟨“ c ”⟩ = ⟨“ c ”⟩ F ⟨“ v ”⟩ = ⟨“ v ”⟩
28 27 rspccva c C V F ⟨“ c ”⟩ = ⟨“ c ”⟩ v C V F ⟨“ v ”⟩ = ⟨“ v ”⟩
29 24 28 sylan T W F : R R c C V F ⟨“ c ”⟩ = ⟨“ c ”⟩ x R y R F x ++ y = F x ++ F y v C V F ⟨“ v ”⟩ = ⟨“ v ”⟩
30 23 29 sylan2br T W F : R R c C V F ⟨“ c ”⟩ = ⟨“ c ”⟩ x R y R F x ++ y = F x ++ F y v C V ¬ v V F ⟨“ v ”⟩ = ⟨“ v ”⟩
31 30 anassrs T W F : R R c C V F ⟨“ c ”⟩ = ⟨“ c ”⟩ x R y R F x ++ y = F x ++ F y v C V ¬ v V F ⟨“ v ”⟩ = ⟨“ v ”⟩
32 31 eqcomd T W F : R R c C V F ⟨“ c ”⟩ = ⟨“ c ”⟩ x R y R F x ++ y = F x ++ F y v C V ¬ v V ⟨“ v ”⟩ = F ⟨“ v ”⟩
33 19 32 ifeqda T W F : R R c C V F ⟨“ c ”⟩ = ⟨“ c ”⟩ x R y R F x ++ y = F x ++ F y v C V if v V w V F ⟨“ w ”⟩ v ⟨“ v ”⟩ = F ⟨“ v ”⟩
34 33 mpteq2dva T W F : R R c C V F ⟨“ c ”⟩ = ⟨“ c ”⟩ x R y R F x ++ y = F x ++ F y v C V if v V w V F ⟨“ w ”⟩ v ⟨“ v ”⟩ = v C V F ⟨“ v ”⟩
35 34 coeq1d T W F : R R c C V F ⟨“ c ”⟩ = ⟨“ c ”⟩ x R y R F x ++ y = F x ++ F y v C V if v V w V F ⟨“ w ”⟩ v ⟨“ v ”⟩ r = v C V F ⟨“ v ”⟩ r
36 35 oveq2d T W F : R R c C V F ⟨“ c ”⟩ = ⟨“ c ”⟩ x R y R F x ++ y = F x ++ F y freeMnd C V v C V if v V w V F ⟨“ w ”⟩ v ⟨“ v ”⟩ r = freeMnd C V v C V F ⟨“ v ”⟩ r
37 13 36 mpteq12dv T W F : R R c C V F ⟨“ c ”⟩ = ⟨“ c ”⟩ x R y R F x ++ y = F x ++ F y r R freeMnd C V v C V if v V w V F ⟨“ w ”⟩ v ⟨“ v ”⟩ r = r Word C V freeMnd C V v C V F ⟨“ v ”⟩ r
38 elun2 v V v C V
39 simplr1 T W F : R R c C V F ⟨“ c ”⟩ = ⟨“ c ”⟩ x R y R F x ++ y = F x ++ F y v C V F : R R
40 simpr T W F : R R c C V F ⟨“ c ”⟩ = ⟨“ c ”⟩ x R y R F x ++ y = F x ++ F y v C V v C V
41 40 s1cld T W F : R R c C V F ⟨“ c ”⟩ = ⟨“ c ”⟩ x R y R F x ++ y = F x ++ F y v C V ⟨“ v ”⟩ Word C V
42 12 ad2antrr T W F : R R c C V F ⟨“ c ”⟩ = ⟨“ c ”⟩ x R y R F x ++ y = F x ++ F y v C V R = Word C V
43 41 42 eleqtrrd T W F : R R c C V F ⟨“ c ”⟩ = ⟨“ c ”⟩ x R y R F x ++ y = F x ++ F y v C V ⟨“ v ”⟩ R
44 39 43 ffvelrnd T W F : R R c C V F ⟨“ c ”⟩ = ⟨“ c ”⟩ x R y R F x ++ y = F x ++ F y v C V F ⟨“ v ”⟩ R
45 38 44 sylan2 T W F : R R c C V F ⟨“ c ”⟩ = ⟨“ c ”⟩ x R y R F x ++ y = F x ++ F y v V F ⟨“ v ”⟩ R
46 15 cbvmptv w V F ⟨“ w ”⟩ = v V F ⟨“ v ”⟩
47 45 46 fmptd T W F : R R c C V F ⟨“ c ”⟩ = ⟨“ c ”⟩ x R y R F x ++ y = F x ++ F y w V F ⟨“ w ”⟩ : V R
48 ssid V V
49 eqid freeMnd C V = freeMnd C V
50 4 3 2 1 49 mrsubfval w V F ⟨“ w ”⟩ : V R V V S w V F ⟨“ w ”⟩ = r R freeMnd C V v C V if v V w V F ⟨“ w ”⟩ v ⟨“ v ”⟩ r
51 47 48 50 sylancl T W F : R R c C V F ⟨“ c ”⟩ = ⟨“ c ”⟩ x R y R F x ++ y = F x ++ F y S w V F ⟨“ w ”⟩ = r R freeMnd C V v C V if v V w V F ⟨“ w ”⟩ v ⟨“ v ”⟩ r
52 4 fvexi C V
53 3 fvexi V V
54 52 53 unex C V V
55 49 frmdmnd C V V freeMnd C V Mnd
56 54 55 ax-mp freeMnd C V Mnd
57 56 a1i T W F : R R c C V F ⟨“ c ”⟩ = ⟨“ c ”⟩ x R y R F x ++ y = F x ++ F y freeMnd C V Mnd
58 54 a1i T W F : R R c C V F ⟨“ c ”⟩ = ⟨“ c ”⟩ x R y R F x ++ y = F x ++ F y C V V
59 44 42 eleqtrd T W F : R R c C V F ⟨“ c ”⟩ = ⟨“ c ”⟩ x R y R F x ++ y = F x ++ F y v C V F ⟨“ v ”⟩ Word C V
60 59 fmpttd T W F : R R c C V F ⟨“ c ”⟩ = ⟨“ c ”⟩ x R y R F x ++ y = F x ++ F y v C V F ⟨“ v ”⟩ : C V Word C V
61 simpr1 T W F : R R c C V F ⟨“ c ”⟩ = ⟨“ c ”⟩ x R y R F x ++ y = F x ++ F y F : R R
62 13 13 feq23d T W F : R R c C V F ⟨“ c ”⟩ = ⟨“ c ”⟩ x R y R F x ++ y = F x ++ F y F : R R F : Word C V Word C V
63 61 62 mpbid T W F : R R c C V F ⟨“ c ”⟩ = ⟨“ c ”⟩ x R y R F x ++ y = F x ++ F y F : Word C V Word C V
64 simpr3 T W F : R R c C V F ⟨“ c ”⟩ = ⟨“ c ”⟩ x R y R F x ++ y = F x ++ F y x R y R F x ++ y = F x ++ F y
65 simprl T W F : R R x R y R x R
66 12 adantr T W F : R R R = Word C V
67 66 adantr T W F : R R x R y R R = Word C V
68 65 67 eleqtrd T W F : R R x R y R x Word C V
69 simprr T W F : R R x R y R y R
70 69 67 eleqtrd T W F : R R x R y R y Word C V
71 eqid Base freeMnd C V = Base freeMnd C V
72 49 71 frmdbas C V V Base freeMnd C V = Word C V
73 54 72 ax-mp Base freeMnd C V = Word C V
74 73 eqcomi Word C V = Base freeMnd C V
75 eqid + freeMnd C V = + freeMnd C V
76 49 74 75 frmdadd x Word C V y Word C V x + freeMnd C V y = x ++ y
77 68 70 76 syl2anc T W F : R R x R y R x + freeMnd C V y = x ++ y
78 77 fveq2d T W F : R R x R y R F x + freeMnd C V y = F x ++ y
79 ffvelrn F : R R x R F x R
80 79 ad2ant2lr T W F : R R x R y R F x R
81 80 67 eleqtrd T W F : R R x R y R F x Word C V
82 ffvelrn F : R R y R F y R
83 82 ad2ant2l T W F : R R x R y R F y R
84 83 67 eleqtrd T W F : R R x R y R F y Word C V
85 49 74 75 frmdadd F x Word C V F y Word C V F x + freeMnd C V F y = F x ++ F y
86 81 84 85 syl2anc T W F : R R x R y R F x + freeMnd C V F y = F x ++ F y
87 78 86 eqeq12d T W F : R R x R y R F x + freeMnd C V y = F x + freeMnd C V F y F x ++ y = F x ++ F y
88 87 2ralbidva T W F : R R x R y R F x + freeMnd C V y = F x + freeMnd C V F y x R y R F x ++ y = F x ++ F y
89 66 raleqdv T W F : R R y R F x + freeMnd C V y = F x + freeMnd C V F y y Word C V F x + freeMnd C V y = F x + freeMnd C V F y
90 66 89 raleqbidv T W F : R R x R y R F x + freeMnd C V y = F x + freeMnd C V F y x Word C V y Word C V F x + freeMnd C V y = F x + freeMnd C V F y
91 88 90 bitr3d T W F : R R x R y R F x ++ y = F x ++ F y x Word C V y Word C V F x + freeMnd C V y = F x + freeMnd C V F y
92 91 3ad2antr1 T W F : R R c C V F ⟨“ c ”⟩ = ⟨“ c ”⟩ x R y R F x ++ y = F x ++ F y x R y R F x ++ y = F x ++ F y x Word C V y Word C V F x + freeMnd C V y = F x + freeMnd C V F y
93 64 92 mpbid T W F : R R c C V F ⟨“ c ”⟩ = ⟨“ c ”⟩ x R y R F x ++ y = F x ++ F y x Word C V y Word C V F x + freeMnd C V y = F x + freeMnd C V F y
94 wrd0 Word C V
95 ffvelrn F : Word C V Word C V Word C V F Word C V
96 63 94 95 sylancl T W F : R R c C V F ⟨“ c ”⟩ = ⟨“ c ”⟩ x R y R F x ++ y = F x ++ F y F Word C V
97 lencl F Word C V F 0
98 96 97 syl T W F : R R c C V F ⟨“ c ”⟩ = ⟨“ c ”⟩ x R y R F x ++ y = F x ++ F y F 0
99 98 nn0cnd T W F : R R c C V F ⟨“ c ”⟩ = ⟨“ c ”⟩ x R y R F x ++ y = F x ++ F y F
100 0cnd T W F : R R c C V F ⟨“ c ”⟩ = ⟨“ c ”⟩ x R y R F x ++ y = F x ++ F y 0
101 99 addid1d T W F : R R c C V F ⟨“ c ”⟩ = ⟨“ c ”⟩ x R y R F x ++ y = F x ++ F y F + 0 = F
102 94 13 eleqtrrid T W F : R R c C V F ⟨“ c ”⟩ = ⟨“ c ”⟩ x R y R F x ++ y = F x ++ F y R
103 fvoveq1 x = F x ++ y = F ++ y
104 fveq2 x = F x = F
105 104 oveq1d x = F x ++ F y = F ++ F y
106 103 105 eqeq12d x = F x ++ y = F x ++ F y F ++ y = F ++ F y
107 oveq2 y = ++ y = ++
108 ccatidid ++ =
109 107 108 syl6eq y = ++ y =
110 109 fveq2d y = F ++ y = F
111 fveq2 y = F y = F
112 111 oveq2d y = F ++ F y = F ++ F
113 110 112 eqeq12d y = F ++ y = F ++ F y F = F ++ F
114 106 113 rspc2va R R x R y R F x ++ y = F x ++ F y F = F ++ F
115 102 102 64 114 syl21anc T W F : R R c C V F ⟨“ c ”⟩ = ⟨“ c ”⟩ x R y R F x ++ y = F x ++ F y F = F ++ F
116 115 fveq2d T W F : R R c C V F ⟨“ c ”⟩ = ⟨“ c ”⟩ x R y R F x ++ y = F x ++ F y F = F ++ F
117 ccatlen F Word C V F Word C V F ++ F = F + F
118 96 96 117 syl2anc T W F : R R c C V F ⟨“ c ”⟩ = ⟨“ c ”⟩ x R y R F x ++ y = F x ++ F y F ++ F = F + F
119 101 116 118 3eqtrrd T W F : R R c C V F ⟨“ c ”⟩ = ⟨“ c ”⟩ x R y R F x ++ y = F x ++ F y F + F = F + 0
120 99 99 100 119 addcanad T W F : R R c C V F ⟨“ c ”⟩ = ⟨“ c ”⟩ x R y R F x ++ y = F x ++ F y F = 0
121 fvex F V
122 hasheq0 F V F = 0 F =
123 121 122 ax-mp F = 0 F =
124 120 123 sylib T W F : R R c C V F ⟨“ c ”⟩ = ⟨“ c ”⟩ x R y R F x ++ y = F x ++ F y F =
125 56 56 pm3.2i freeMnd C V Mnd freeMnd C V Mnd
126 49 frmd0 = 0 freeMnd C V
127 74 74 75 75 126 126 ismhm F freeMnd C V MndHom freeMnd C V freeMnd C V Mnd freeMnd C V Mnd F : Word C V Word C V x Word C V y Word C V F x + freeMnd C V y = F x + freeMnd C V F y F =
128 125 127 mpbiran F freeMnd C V MndHom freeMnd C V F : Word C V Word C V x Word C V y Word C V F x + freeMnd C V y = F x + freeMnd C V F y F =
129 63 93 124 128 syl3anbrc T W F : R R c C V F ⟨“ c ”⟩ = ⟨“ c ”⟩ x R y R F x ++ y = F x ++ F y F freeMnd C V MndHom freeMnd C V
130 eqid var FMnd C V = var FMnd C V
131 130 vrmdf C V V var FMnd C V : C V Word C V
132 54 131 ax-mp var FMnd C V : C V Word C V
133 fcompt F : Word C V Word C V var FMnd C V : C V Word C V F var FMnd C V = v C V F var FMnd C V v
134 63 132 133 sylancl T W F : R R c C V F ⟨“ c ”⟩ = ⟨“ c ”⟩ x R y R F x ++ y = F x ++ F y F var FMnd C V = v C V F var FMnd C V v
135 130 vrmdval C V V v C V var FMnd C V v = ⟨“ v ”⟩
136 54 135 mpan v C V var FMnd C V v = ⟨“ v ”⟩
137 136 fveq2d v C V F var FMnd C V v = F ⟨“ v ”⟩
138 137 mpteq2ia v C V F var FMnd C V v = v C V F ⟨“ v ”⟩
139 134 138 syl6eq T W F : R R c C V F ⟨“ c ”⟩ = ⟨“ c ”⟩ x R y R F x ++ y = F x ++ F y F var FMnd C V = v C V F ⟨“ v ”⟩
140 49 74 130 frmdup3lem freeMnd C V Mnd C V V v C V F ⟨“ v ”⟩ : C V Word C V F freeMnd C V MndHom freeMnd C V F var FMnd C V = v C V F ⟨“ v ”⟩ F = r Word C V freeMnd C V v C V F ⟨“ v ”⟩ r
141 57 58 60 129 139 140 syl32anc T W F : R R c C V F ⟨“ c ”⟩ = ⟨“ c ”⟩ x R y R F x ++ y = F x ++ F y F = r Word C V freeMnd C V v C V F ⟨“ v ”⟩ r
142 37 51 141 3eqtr4rd T W F : R R c C V F ⟨“ c ”⟩ = ⟨“ c ”⟩ x R y R F x ++ y = F x ++ F y F = S w V F ⟨“ w ”⟩
143 3 2 1 mrsubff T W S : R 𝑝𝑚 V R R
144 143 ffnd T W S Fn R 𝑝𝑚 V
145 144 adantr T W F : R R c C V F ⟨“ c ”⟩ = ⟨“ c ”⟩ x R y R F x ++ y = F x ++ F y S Fn R 𝑝𝑚 V
146 2 fvexi R V
147 elpm2r R V V V w V F ⟨“ w ”⟩ : V R V V w V F ⟨“ w ”⟩ R 𝑝𝑚 V
148 146 53 147 mpanl12 w V F ⟨“ w ”⟩ : V R V V w V F ⟨“ w ”⟩ R 𝑝𝑚 V
149 47 48 148 sylancl T W F : R R c C V F ⟨“ c ”⟩ = ⟨“ c ”⟩ x R y R F x ++ y = F x ++ F y w V F ⟨“ w ”⟩ R 𝑝𝑚 V
150 fnfvelrn S Fn R 𝑝𝑚 V w V F ⟨“ w ”⟩ R 𝑝𝑚 V S w V F ⟨“ w ”⟩ ran S
151 145 149 150 syl2anc T W F : R R c C V F ⟨“ c ”⟩ = ⟨“ c ”⟩ x R y R F x ++ y = F x ++ F y S w V F ⟨“ w ”⟩ ran S
152 142 151 eqeltrd T W F : R R c C V F ⟨“ c ”⟩ = ⟨“ c ”⟩ x R y R F x ++ y = F x ++ F y F ran S
153 152 ex T W F : R R c C V F ⟨“ c ”⟩ = ⟨“ c ”⟩ x R y R F x ++ y = F x ++ F y F ran S
154 11 153 impbid2 T W F ran S F : R R c C V F ⟨“ c ”⟩ = ⟨“ c ”⟩ x R y R F x ++ y = F x ++ F y