Metamath Proof Explorer

Theorem mrsubccat

Description: Substitution distributes over concatenation. (Contributed by Mario Carneiro, 18-Jul-2016)

Ref Expression
Hypotheses mrsubccat.s ⊢S=mRSubst⁡T
mrsubccat.r ⊢R=mREx⁡T
Assertion mrsubccat ⊢F∈ran⁡S∧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 n0i ⊢F∈ran⁡S→¬ran⁡S=∅
4 1 rnfvprc ⊢¬T∈V→ran⁡S=∅
5 3 4 nsyl2 ⊢F∈ran⁡S→T∈V
6 eqid ⊢mVR⁡T=mVR⁡T
7 6 2 1 mrsubff ⊢T∈V→S:R↑𝑝𝑚mVR⁡T⟶RR
8 ffun ⊢S:R↑𝑝𝑚mVR⁡T⟶RR→Fun⁡S
9 5 7 8 3syl ⊢F∈ran⁡S→Fun⁡S
10 6 2 1 mrsubrn ⊢ran⁡S=SRmVR⁡T
11 10 eleq2i ⊢F∈ran⁡S↔F∈SRmVR⁡T
12 11 biimpi ⊢F∈ran⁡S→F∈SRmVR⁡T
13 fvelima ⊢Fun⁡S∧F∈SRmVR⁡T→∃f∈RmVR⁡TS⁡f=F
14 9 12 13 syl2anc ⊢F∈ran⁡S→∃f∈RmVR⁡TS⁡f=F
15 simprl ⊢f∈RmVR⁡T∧X∈R∧Y∈R→X∈R
16 elfvex ⊢X∈mREx⁡T→T∈V
17 16 2 eleq2s ⊢X∈R→T∈V
18 eqid ⊢mCN⁡T=mCN⁡T
19 18 6 2 mrexval ⊢T∈V→R=WordmCN⁡T∪mVR⁡T
20 15 17 19 3syl ⊢f∈RmVR⁡T∧X∈R∧Y∈R→R=WordmCN⁡T∪mVR⁡T
21 15 20 eleqtrd ⊢f∈RmVR⁡T∧X∈R∧Y∈R→X∈WordmCN⁡T∪mVR⁡T
22 simprr ⊢f∈RmVR⁡T∧X∈R∧Y∈R→Y∈R
23 22 20 eleqtrd ⊢f∈RmVR⁡T∧X∈R∧Y∈R→Y∈WordmCN⁡T∪mVR⁡T
24 elmapi ⊢f∈RmVR⁡T→f:mVR⁡T⟶R
25 24 adantr ⊢f∈RmVR⁡T∧X∈R∧Y∈R→f:mVR⁡T⟶R
26 25 adantr ⊢f∈RmVR⁡T∧X∈R∧Y∈R∧v∈mCN⁡T∪mVR⁡T→f:mVR⁡T⟶R
27 26 ffvelcdmda ⊢f∈RmVR⁡T∧X∈R∧Y∈R∧v∈mCN⁡T∪mVR⁡T∧v∈mVR⁡T→f⁡v∈R
28 20 ad2antrr ⊢f∈RmVR⁡T∧X∈R∧Y∈R∧v∈mCN⁡T∪mVR⁡T∧v∈mVR⁡T→R=WordmCN⁡T∪mVR⁡T
29 27 28 eleqtrd ⊢f∈RmVR⁡T∧X∈R∧Y∈R∧v∈mCN⁡T∪mVR⁡T∧v∈mVR⁡T→f⁡v∈WordmCN⁡T∪mVR⁡T
30 simplr ⊢f∈RmVR⁡T∧X∈R∧Y∈R∧v∈mCN⁡T∪mVR⁡T∧¬v∈mVR⁡T→v∈mCN⁡T∪mVR⁡T
31 30 s1cld ⊢f∈RmVR⁡T∧X∈R∧Y∈R∧v∈mCN⁡T∪mVR⁡T∧¬v∈mVR⁡T→⟨“v”⟩∈WordmCN⁡T∪mVR⁡T
32 29 31 ifclda ⊢f∈RmVR⁡T∧X∈R∧Y∈R∧v∈mCN⁡T∪mVR⁡T→ifv∈mVR⁡Tf⁡v⟨“v”⟩∈WordmCN⁡T∪mVR⁡T
33 32 fmpttd ⊢f∈RmVR⁡T∧X∈R∧Y∈R→v∈mCN⁡T∪mVR⁡T⟼ifv∈mVR⁡Tf⁡v⟨“v”⟩:mCN⁡T∪mVR⁡T⟶WordmCN⁡T∪mVR⁡T
34 ccatco ⊢X∈WordmCN⁡T∪mVR⁡T∧Y∈WordmCN⁡T∪mVR⁡T∧v∈mCN⁡T∪mVR⁡T⟼ifv∈mVR⁡Tf⁡v⟨“v”⟩:mCN⁡T∪mVR⁡T⟶WordmCN⁡T∪mVR⁡T→v∈mCN⁡T∪mVR⁡T⟼ifv∈mVR⁡Tf⁡v⟨“v”⟩∘X++Y=v∈mCN⁡T∪mVR⁡T⟼ifv∈mVR⁡Tf⁡v⟨“v”⟩∘X++v∈mCN⁡T∪mVR⁡T⟼ifv∈mVR⁡Tf⁡v⟨“v”⟩∘Y
35 21 23 33 34 syl3anc ⊢f∈RmVR⁡T∧X∈R∧Y∈R→v∈mCN⁡T∪mVR⁡T⟼ifv∈mVR⁡Tf⁡v⟨“v”⟩∘X++Y=v∈mCN⁡T∪mVR⁡T⟼ifv∈mVR⁡Tf⁡v⟨“v”⟩∘X++v∈mCN⁡T∪mVR⁡T⟼ifv∈mVR⁡Tf⁡v⟨“v”⟩∘Y
36 35 oveq2d ⊢f∈RmVR⁡T∧X∈R∧Y∈R→∑freeMnd⁡mCN⁡T∪mVR⁡Tv∈mCN⁡T∪mVR⁡T⟼ifv∈mVR⁡Tf⁡v⟨“v”⟩∘X++Y=∑freeMnd⁡mCN⁡T∪mVR⁡Tv∈mCN⁡T∪mVR⁡T⟼ifv∈mVR⁡Tf⁡v⟨“v”⟩∘X++v∈mCN⁡T∪mVR⁡T⟼ifv∈mVR⁡Tf⁡v⟨“v”⟩∘Y
37 fvex ⊢mCN⁡T∈V
38 fvex ⊢mVR⁡T∈V
39 37 38 unex ⊢mCN⁡T∪mVR⁡T∈V
40 eqid ⊢freeMnd⁡mCN⁡T∪mVR⁡T=freeMnd⁡mCN⁡T∪mVR⁡T
41 40 frmdmnd ⊢mCN⁡T∪mVR⁡T∈V→freeMnd⁡mCN⁡T∪mVR⁡T∈Mnd
42 39 41 mp1i ⊢f∈RmVR⁡T∧X∈R∧Y∈R→freeMnd⁡mCN⁡T∪mVR⁡T∈Mnd
43 wrdco ⊢X∈WordmCN⁡T∪mVR⁡T∧v∈mCN⁡T∪mVR⁡T⟼ifv∈mVR⁡Tf⁡v⟨“v”⟩:mCN⁡T∪mVR⁡T⟶WordmCN⁡T∪mVR⁡T→v∈mCN⁡T∪mVR⁡T⟼ifv∈mVR⁡Tf⁡v⟨“v”⟩∘X∈WordWordmCN⁡T∪mVR⁡T
44 21 33 43 syl2anc ⊢f∈RmVR⁡T∧X∈R∧Y∈R→v∈mCN⁡T∪mVR⁡T⟼ifv∈mVR⁡Tf⁡v⟨“v”⟩∘X∈WordWordmCN⁡T∪mVR⁡T
45 wrdco ⊢Y∈WordmCN⁡T∪mVR⁡T∧v∈mCN⁡T∪mVR⁡T⟼ifv∈mVR⁡Tf⁡v⟨“v”⟩:mCN⁡T∪mVR⁡T⟶WordmCN⁡T∪mVR⁡T→v∈mCN⁡T∪mVR⁡T⟼ifv∈mVR⁡Tf⁡v⟨“v”⟩∘Y∈WordWordmCN⁡T∪mVR⁡T
46 23 33 45 syl2anc ⊢f∈RmVR⁡T∧X∈R∧Y∈R→v∈mCN⁡T∪mVR⁡T⟼ifv∈mVR⁡Tf⁡v⟨“v”⟩∘Y∈WordWordmCN⁡T∪mVR⁡T
47 eqid ⊢BasefreeMnd⁡mCN⁡T∪mVR⁡T=BasefreeMnd⁡mCN⁡T∪mVR⁡T
48 40 47 frmdbas ⊢mCN⁡T∪mVR⁡T∈V→BasefreeMnd⁡mCN⁡T∪mVR⁡T=WordmCN⁡T∪mVR⁡T
49 39 48 ax-mp ⊢BasefreeMnd⁡mCN⁡T∪mVR⁡T=WordmCN⁡T∪mVR⁡T
50 49 eqcomi ⊢WordmCN⁡T∪mVR⁡T=BasefreeMnd⁡mCN⁡T∪mVR⁡T
51 eqid ⊢+freeMnd⁡mCN⁡T∪mVR⁡T=+freeMnd⁡mCN⁡T∪mVR⁡T
52 50 51 gsumccat ⊢freeMnd⁡mCN⁡T∪mVR⁡T∈Mnd∧v∈mCN⁡T∪mVR⁡T⟼ifv∈mVR⁡Tf⁡v⟨“v”⟩∘X∈WordWordmCN⁡T∪mVR⁡T∧v∈mCN⁡T∪mVR⁡T⟼ifv∈mVR⁡Tf⁡v⟨“v”⟩∘Y∈WordWordmCN⁡T∪mVR⁡T→∑freeMnd⁡mCN⁡T∪mVR⁡Tv∈mCN⁡T∪mVR⁡T⟼ifv∈mVR⁡Tf⁡v⟨“v”⟩∘X++v∈mCN⁡T∪mVR⁡T⟼ifv∈mVR⁡Tf⁡v⟨“v”⟩∘Y=∑freeMnd⁡mCN⁡T∪mVR⁡Tv∈mCN⁡T∪mVR⁡T⟼ifv∈mVR⁡Tf⁡v⟨“v”⟩∘X+freeMnd⁡mCN⁡T∪mVR⁡T∑freeMnd⁡mCN⁡T∪mVR⁡Tv∈mCN⁡T∪mVR⁡T⟼ifv∈mVR⁡Tf⁡v⟨“v”⟩∘Y
53 42 44 46 52 syl3anc ⊢f∈RmVR⁡T∧X∈R∧Y∈R→∑freeMnd⁡mCN⁡T∪mVR⁡Tv∈mCN⁡T∪mVR⁡T⟼ifv∈mVR⁡Tf⁡v⟨“v”⟩∘X++v∈mCN⁡T∪mVR⁡T⟼ifv∈mVR⁡Tf⁡v⟨“v”⟩∘Y=∑freeMnd⁡mCN⁡T∪mVR⁡Tv∈mCN⁡T∪mVR⁡T⟼ifv∈mVR⁡Tf⁡v⟨“v”⟩∘X+freeMnd⁡mCN⁡T∪mVR⁡T∑freeMnd⁡mCN⁡T∪mVR⁡Tv∈mCN⁡T∪mVR⁡T⟼ifv∈mVR⁡Tf⁡v⟨“v”⟩∘Y
54 50 gsumwcl ⊢freeMnd⁡mCN⁡T∪mVR⁡T∈Mnd∧v∈mCN⁡T∪mVR⁡T⟼ifv∈mVR⁡Tf⁡v⟨“v”⟩∘X∈WordWordmCN⁡T∪mVR⁡T→∑freeMnd⁡mCN⁡T∪mVR⁡Tv∈mCN⁡T∪mVR⁡T⟼ifv∈mVR⁡Tf⁡v⟨“v”⟩∘X∈WordmCN⁡T∪mVR⁡T
55 42 44 54 syl2anc ⊢f∈RmVR⁡T∧X∈R∧Y∈R→∑freeMnd⁡mCN⁡T∪mVR⁡Tv∈mCN⁡T∪mVR⁡T⟼ifv∈mVR⁡Tf⁡v⟨“v”⟩∘X∈WordmCN⁡T∪mVR⁡T
56 50 gsumwcl ⊢freeMnd⁡mCN⁡T∪mVR⁡T∈Mnd∧v∈mCN⁡T∪mVR⁡T⟼ifv∈mVR⁡Tf⁡v⟨“v”⟩∘Y∈WordWordmCN⁡T∪mVR⁡T→∑freeMnd⁡mCN⁡T∪mVR⁡Tv∈mCN⁡T∪mVR⁡T⟼ifv∈mVR⁡Tf⁡v⟨“v”⟩∘Y∈WordmCN⁡T∪mVR⁡T
57 42 46 56 syl2anc ⊢f∈RmVR⁡T∧X∈R∧Y∈R→∑freeMnd⁡mCN⁡T∪mVR⁡Tv∈mCN⁡T∪mVR⁡T⟼ifv∈mVR⁡Tf⁡v⟨“v”⟩∘Y∈WordmCN⁡T∪mVR⁡T
58 40 50 51 frmdadd ⊢∑freeMnd⁡mCN⁡T∪mVR⁡Tv∈mCN⁡T∪mVR⁡T⟼ifv∈mVR⁡Tf⁡v⟨“v”⟩∘X∈WordmCN⁡T∪mVR⁡T∧∑freeMnd⁡mCN⁡T∪mVR⁡Tv∈mCN⁡T∪mVR⁡T⟼ifv∈mVR⁡Tf⁡v⟨“v”⟩∘Y∈WordmCN⁡T∪mVR⁡T→∑freeMnd⁡mCN⁡T∪mVR⁡Tv∈mCN⁡T∪mVR⁡T⟼ifv∈mVR⁡Tf⁡v⟨“v”⟩∘X+freeMnd⁡mCN⁡T∪mVR⁡T∑freeMnd⁡mCN⁡T∪mVR⁡Tv∈mCN⁡T∪mVR⁡T⟼ifv∈mVR⁡Tf⁡v⟨“v”⟩∘Y=∑freeMnd⁡mCN⁡T∪mVR⁡Tv∈mCN⁡T∪mVR⁡T⟼ifv∈mVR⁡Tf⁡v⟨“v”⟩∘X++∑freeMnd⁡mCN⁡T∪mVR⁡Tv∈mCN⁡T∪mVR⁡T⟼ifv∈mVR⁡Tf⁡v⟨“v”⟩∘Y
59 55 57 58 syl2anc ⊢f∈RmVR⁡T∧X∈R∧Y∈R→∑freeMnd⁡mCN⁡T∪mVR⁡Tv∈mCN⁡T∪mVR⁡T⟼ifv∈mVR⁡Tf⁡v⟨“v”⟩∘X+freeMnd⁡mCN⁡T∪mVR⁡T∑freeMnd⁡mCN⁡T∪mVR⁡Tv∈mCN⁡T∪mVR⁡T⟼ifv∈mVR⁡Tf⁡v⟨“v”⟩∘Y=∑freeMnd⁡mCN⁡T∪mVR⁡Tv∈mCN⁡T∪mVR⁡T⟼ifv∈mVR⁡Tf⁡v⟨“v”⟩∘X++∑freeMnd⁡mCN⁡T∪mVR⁡Tv∈mCN⁡T∪mVR⁡T⟼ifv∈mVR⁡Tf⁡v⟨“v”⟩∘Y
60 36 53 59 3eqtrd ⊢f∈RmVR⁡T∧X∈R∧Y∈R→∑freeMnd⁡mCN⁡T∪mVR⁡Tv∈mCN⁡T∪mVR⁡T⟼ifv∈mVR⁡Tf⁡v⟨“v”⟩∘X++Y=∑freeMnd⁡mCN⁡T∪mVR⁡Tv∈mCN⁡T∪mVR⁡T⟼ifv∈mVR⁡Tf⁡v⟨“v”⟩∘X++∑freeMnd⁡mCN⁡T∪mVR⁡Tv∈mCN⁡T∪mVR⁡T⟼ifv∈mVR⁡Tf⁡v⟨“v”⟩∘Y
61 ssidd ⊢f∈RmVR⁡T∧X∈R∧Y∈R→mVR⁡T⊆mVR⁡T
62 ccatcl ⊢X∈WordmCN⁡T∪mVR⁡T∧Y∈WordmCN⁡T∪mVR⁡T→X++Y∈WordmCN⁡T∪mVR⁡T
63 21 23 62 syl2anc ⊢f∈RmVR⁡T∧X∈R∧Y∈R→X++Y∈WordmCN⁡T∪mVR⁡T
64 63 20 eleqtrrd ⊢f∈RmVR⁡T∧X∈R∧Y∈R→X++Y∈R
65 18 6 2 1 40 mrsubval ⊢f:mVR⁡T⟶R∧mVR⁡T⊆mVR⁡T∧X++Y∈R→S⁡f⁡X++Y=∑freeMnd⁡mCN⁡T∪mVR⁡Tv∈mCN⁡T∪mVR⁡T⟼ifv∈mVR⁡Tf⁡v⟨“v”⟩∘X++Y
66 25 61 64 65 syl3anc ⊢f∈RmVR⁡T∧X∈R∧Y∈R→S⁡f⁡X++Y=∑freeMnd⁡mCN⁡T∪mVR⁡Tv∈mCN⁡T∪mVR⁡T⟼ifv∈mVR⁡Tf⁡v⟨“v”⟩∘X++Y
67 18 6 2 1 40 mrsubval ⊢f:mVR⁡T⟶R∧mVR⁡T⊆mVR⁡T∧X∈R→S⁡f⁡X=∑freeMnd⁡mCN⁡T∪mVR⁡Tv∈mCN⁡T∪mVR⁡T⟼ifv∈mVR⁡Tf⁡v⟨“v”⟩∘X
68 25 61 15 67 syl3anc ⊢f∈RmVR⁡T∧X∈R∧Y∈R→S⁡f⁡X=∑freeMnd⁡mCN⁡T∪mVR⁡Tv∈mCN⁡T∪mVR⁡T⟼ifv∈mVR⁡Tf⁡v⟨“v”⟩∘X
69 18 6 2 1 40 mrsubval ⊢f:mVR⁡T⟶R∧mVR⁡T⊆mVR⁡T∧Y∈R→S⁡f⁡Y=∑freeMnd⁡mCN⁡T∪mVR⁡Tv∈mCN⁡T∪mVR⁡T⟼ifv∈mVR⁡Tf⁡v⟨“v”⟩∘Y
70 25 61 22 69 syl3anc ⊢f∈RmVR⁡T∧X∈R∧Y∈R→S⁡f⁡Y=∑freeMnd⁡mCN⁡T∪mVR⁡Tv∈mCN⁡T∪mVR⁡T⟼ifv∈mVR⁡Tf⁡v⟨“v”⟩∘Y
71 68 70 oveq12d ⊢f∈RmVR⁡T∧X∈R∧Y∈R→S⁡f⁡X++S⁡f⁡Y=∑freeMnd⁡mCN⁡T∪mVR⁡Tv∈mCN⁡T∪mVR⁡T⟼ifv∈mVR⁡Tf⁡v⟨“v”⟩∘X++∑freeMnd⁡mCN⁡T∪mVR⁡Tv∈mCN⁡T∪mVR⁡T⟼ifv∈mVR⁡Tf⁡v⟨“v”⟩∘Y
72 60 66 71 3eqtr4d ⊢f∈RmVR⁡T∧X∈R∧Y∈R→S⁡f⁡X++Y=S⁡f⁡X++S⁡f⁡Y
73 fveq1 ⊢S⁡f=F→S⁡f⁡X++Y=F⁡X++Y
74 fveq1 ⊢S⁡f=F→S⁡f⁡X=F⁡X
75 fveq1 ⊢S⁡f=F→S⁡f⁡Y=F⁡Y
76 74 75 oveq12d ⊢S⁡f=F→S⁡f⁡X++S⁡f⁡Y=F⁡X++F⁡Y
77 73 76 eqeq12d ⊢S⁡f=F→S⁡f⁡X++Y=S⁡f⁡X++S⁡f⁡Y↔F⁡X++Y=F⁡X++F⁡Y
78 72 77 syl5ibcom ⊢f∈RmVR⁡T∧X∈R∧Y∈R→S⁡f=F→F⁡X++Y=F⁡X++F⁡Y
79 78 ex ⊢f∈RmVR⁡T→X∈R∧Y∈R→S⁡f=F→F⁡X++Y=F⁡X++F⁡Y
80 79 com23 ⊢f∈RmVR⁡T→S⁡f=F→X∈R∧Y∈R→F⁡X++Y=F⁡X++F⁡Y
81 80 rexlimiv ⊢∃f∈RmVR⁡TS⁡f=F→X∈R∧Y∈R→F⁡X++Y=F⁡X++F⁡Y
82 14 81 syl ⊢F∈ran⁡S→X∈R∧Y∈R→F⁡X++Y=F⁡X++F⁡Y
83 82 3impib ⊢F∈ran⁡S∧X∈R∧Y∈R→F⁡X++Y=F⁡X++F⁡Y