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 ⟶ R R
8 ffun ⊢ S : R ↑ 𝑝𝑚 mVR ⁡ T ⟶ R R → Fun ⁡ S
9 5 7 8 3syl ⊢ F ∈ ran ⁡ S → Fun ⁡ S
10 6 2 1 mrsubrn ⊢ ran ⁡ S = S R mVR ⁡ T
11 10 eleq2i ⊢ F ∈ ran ⁡ S ↔ F ∈ S R mVR ⁡ T
12 11 biimpi ⊢ F ∈ ran ⁡ S → F ∈ S R mVR ⁡ T
13 fvelima ⊢ Fun ⁡ S ∧ F ∈ S R mVR ⁡ T → ∃ f ∈ R mVR ⁡ T S ⁡ f = F
14 9 12 13 syl2anc ⊢ F ∈ ran ⁡ S → ∃ f ∈ R mVR ⁡ T S ⁡ f = F
15 simprl ⊢ f ∈ R mVR ⁡ 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 = Word mCN ⁡ T ∪ mVR ⁡ T
20 15 17 19 3syl ⊢ f ∈ R mVR ⁡ T ∧ X ∈ R ∧ Y ∈ R → R = Word mCN ⁡ T ∪ mVR ⁡ T
21 15 20 eleqtrd ⊢ f ∈ R mVR ⁡ T ∧ X ∈ R ∧ Y ∈ R → X ∈ Word mCN ⁡ T ∪ mVR ⁡ T
22 simprr ⊢ f ∈ R mVR ⁡ T ∧ X ∈ R ∧ Y ∈ R → Y ∈ R
23 22 20 eleqtrd ⊢ f ∈ R mVR ⁡ T ∧ X ∈ R ∧ Y ∈ R → Y ∈ Word mCN ⁡ T ∪ mVR ⁡ T
24 elmapi ⊢ f ∈ R mVR ⁡ T → f : mVR ⁡ T ⟶ R
25 24 adantr ⊢ f ∈ R mVR ⁡ T ∧ X ∈ R ∧ Y ∈ R → f : mVR ⁡ T ⟶ R
26 25 adantr ⊢ f ∈ R mVR ⁡ T ∧ X ∈ R ∧ Y ∈ R ∧ v ∈ mCN ⁡ T ∪ mVR ⁡ T → f : mVR ⁡ T ⟶ R
27 26 ffvelcdmda ⊢ f ∈ R mVR ⁡ T ∧ X ∈ R ∧ Y ∈ R ∧ v ∈ mCN ⁡ T ∪ mVR ⁡ T ∧ v ∈ mVR ⁡ T → f ⁡ v ∈ R
28 20 ad2antrr ⊢ f ∈ R mVR ⁡ T ∧ X ∈ R ∧ Y ∈ R ∧ v ∈ mCN ⁡ T ∪ mVR ⁡ T ∧ v ∈ mVR ⁡ T → R = Word mCN ⁡ T ∪ mVR ⁡ T
29 27 28 eleqtrd ⊢ f ∈ R mVR ⁡ T ∧ X ∈ R ∧ Y ∈ R ∧ v ∈ mCN ⁡ T ∪ mVR ⁡ T ∧ v ∈ mVR ⁡ T → f ⁡ v ∈ Word mCN ⁡ T ∪ mVR ⁡ T
30 simplr ⊢ f ∈ R mVR ⁡ T ∧ X ∈ R ∧ Y ∈ R ∧ v ∈ mCN ⁡ T ∪ mVR ⁡ T ∧ ¬ v ∈ mVR ⁡ T → v ∈ mCN ⁡ T ∪ mVR ⁡ T
31 30 s1cld ⊢ f ∈ R mVR ⁡ T ∧ X ∈ R ∧ Y ∈ R ∧ v ∈ mCN ⁡ T ∪ mVR ⁡ T ∧ ¬ v ∈ mVR ⁡ T → ⟨“ v ”⟩ ∈ Word mCN ⁡ T ∪ mVR ⁡ T
32 29 31 ifclda ⊢ f ∈ R mVR ⁡ T ∧ X ∈ R ∧ Y ∈ R ∧ v ∈ mCN ⁡ T ∪ mVR ⁡ T → if v ∈ mVR ⁡ T f ⁡ v ⟨“ v ”⟩ ∈ Word mCN ⁡ T ∪ mVR ⁡ T
33 32 fmpttd ⊢ f ∈ R mVR ⁡ T ∧ X ∈ R ∧ Y ∈ R → v ∈ mCN ⁡ T ∪ mVR ⁡ T ⟼ if v ∈ mVR ⁡ T f ⁡ v ⟨“ v ”⟩ : mCN ⁡ T ∪ mVR ⁡ T ⟶ Word mCN ⁡ T ∪ mVR ⁡ T
34 ccatco ⊢ X ∈ Word mCN ⁡ T ∪ mVR ⁡ T ∧ Y ∈ Word mCN ⁡ T ∪ mVR ⁡ T ∧ v ∈ mCN ⁡ T ∪ mVR ⁡ T ⟼ if v ∈ mVR ⁡ T f ⁡ v ⟨“ v ”⟩ : mCN ⁡ T ∪ mVR ⁡ T ⟶ Word mCN ⁡ T ∪ mVR ⁡ T → v ∈ mCN ⁡ T ∪ mVR ⁡ T ⟼ if v ∈ mVR ⁡ T f ⁡ v ⟨“ v ”⟩ ∘ X ++ Y = v ∈ mCN ⁡ T ∪ mVR ⁡ T ⟼ if v ∈ mVR ⁡ T f ⁡ v ⟨“ v ”⟩ ∘ X ++ v ∈ mCN ⁡ T ∪ mVR ⁡ T ⟼ if v ∈ mVR ⁡ T f ⁡ v ⟨“ v ”⟩ ∘ Y
35 21 23 33 34 syl3anc ⊢ f ∈ R mVR ⁡ T ∧ X ∈ R ∧ Y ∈ R → v ∈ mCN ⁡ T ∪ mVR ⁡ T ⟼ if v ∈ mVR ⁡ T f ⁡ v ⟨“ v ”⟩ ∘ X ++ Y = v ∈ mCN ⁡ T ∪ mVR ⁡ T ⟼ if v ∈ mVR ⁡ T f ⁡ v ⟨“ v ”⟩ ∘ X ++ v ∈ mCN ⁡ T ∪ mVR ⁡ T ⟼ if v ∈ mVR ⁡ T f ⁡ v ⟨“ v ”⟩ ∘ Y
36 35 oveq2d ⊢ f ∈ R mVR ⁡ T ∧ X ∈ R ∧ Y ∈ R → ∑ freeMnd ⁡ mCN ⁡ T ∪ mVR ⁡ T v ∈ mCN ⁡ T ∪ mVR ⁡ T ⟼ if v ∈ mVR ⁡ T f ⁡ v ⟨“ v ”⟩ ∘ X ++ Y = ∑ freeMnd ⁡ mCN ⁡ T ∪ mVR ⁡ T v ∈ mCN ⁡ T ∪ mVR ⁡ T ⟼ if v ∈ mVR ⁡ T f ⁡ v ⟨“ v ”⟩ ∘ X ++ v ∈ mCN ⁡ T ∪ mVR ⁡ T ⟼ if v ∈ mVR ⁡ T f ⁡ 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 ∈ R mVR ⁡ T ∧ X ∈ R ∧ Y ∈ R → freeMnd ⁡ mCN ⁡ T ∪ mVR ⁡ T ∈ Mnd
43 wrdco ⊢ X ∈ Word mCN ⁡ T ∪ mVR ⁡ T ∧ v ∈ mCN ⁡ T ∪ mVR ⁡ T ⟼ if v ∈ mVR ⁡ T f ⁡ v ⟨“ v ”⟩ : mCN ⁡ T ∪ mVR ⁡ T ⟶ Word mCN ⁡ T ∪ mVR ⁡ T → v ∈ mCN ⁡ T ∪ mVR ⁡ T ⟼ if v ∈ mVR ⁡ T f ⁡ v ⟨“ v ”⟩ ∘ X ∈ Word Word mCN ⁡ T ∪ mVR ⁡ T
44 21 33 43 syl2anc ⊢ f ∈ R mVR ⁡ T ∧ X ∈ R ∧ Y ∈ R → v ∈ mCN ⁡ T ∪ mVR ⁡ T ⟼ if v ∈ mVR ⁡ T f ⁡ v ⟨“ v ”⟩ ∘ X ∈ Word Word mCN ⁡ T ∪ mVR ⁡ T
45 wrdco ⊢ Y ∈ Word mCN ⁡ T ∪ mVR ⁡ T ∧ v ∈ mCN ⁡ T ∪ mVR ⁡ T ⟼ if v ∈ mVR ⁡ T f ⁡ v ⟨“ v ”⟩ : mCN ⁡ T ∪ mVR ⁡ T ⟶ Word mCN ⁡ T ∪ mVR ⁡ T → v ∈ mCN ⁡ T ∪ mVR ⁡ T ⟼ if v ∈ mVR ⁡ T f ⁡ v ⟨“ v ”⟩ ∘ Y ∈ Word Word mCN ⁡ T ∪ mVR ⁡ T
46 23 33 45 syl2anc ⊢ f ∈ R mVR ⁡ T ∧ X ∈ R ∧ Y ∈ R → v ∈ mCN ⁡ T ∪ mVR ⁡ T ⟼ if v ∈ mVR ⁡ T f ⁡ v ⟨“ v ”⟩ ∘ Y ∈ Word Word mCN ⁡ T ∪ mVR ⁡ T
47 eqid ⊢ Base freeMnd ⁡ mCN ⁡ T ∪ mVR ⁡ T = Base freeMnd ⁡ mCN ⁡ T ∪ mVR ⁡ T
48 40 47 frmdbas ⊢ mCN ⁡ T ∪ mVR ⁡ T ∈ V → Base freeMnd ⁡ mCN ⁡ T ∪ mVR ⁡ T = Word mCN ⁡ T ∪ mVR ⁡ T
49 39 48 ax-mp ⊢ Base freeMnd ⁡ mCN ⁡ T ∪ mVR ⁡ T = Word mCN ⁡ T ∪ mVR ⁡ T
50 49 eqcomi ⊢ Word mCN ⁡ T ∪ mVR ⁡ T = Base freeMnd ⁡ 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 ⟼ if v ∈ mVR ⁡ T f ⁡ v ⟨“ v ”⟩ ∘ X ∈ Word Word mCN ⁡ T ∪ mVR ⁡ T ∧ v ∈ mCN ⁡ T ∪ mVR ⁡ T ⟼ if v ∈ mVR ⁡ T f ⁡ v ⟨“ v ”⟩ ∘ Y ∈ Word Word mCN ⁡ T ∪ mVR ⁡ T → ∑ freeMnd ⁡ mCN ⁡ T ∪ mVR ⁡ T v ∈ mCN ⁡ T ∪ mVR ⁡ T ⟼ if v ∈ mVR ⁡ T f ⁡ v ⟨“ v ”⟩ ∘ X ++ v ∈ mCN ⁡ T ∪ mVR ⁡ T ⟼ if v ∈ mVR ⁡ T f ⁡ v ⟨“ v ”⟩ ∘ Y = ∑ freeMnd ⁡ mCN ⁡ T ∪ mVR ⁡ T v ∈ mCN ⁡ T ∪ mVR ⁡ T ⟼ if v ∈ mVR ⁡ T f ⁡ v ⟨“ v ”⟩ ∘ X + freeMnd ⁡ mCN ⁡ T ∪ mVR ⁡ T ∑ freeMnd ⁡ mCN ⁡ T ∪ mVR ⁡ T v ∈ mCN ⁡ T ∪ mVR ⁡ T ⟼ if v ∈ mVR ⁡ T f ⁡ v ⟨“ v ”⟩ ∘ Y
53 42 44 46 52 syl3anc ⊢ f ∈ R mVR ⁡ T ∧ X ∈ R ∧ Y ∈ R → ∑ freeMnd ⁡ mCN ⁡ T ∪ mVR ⁡ T v ∈ mCN ⁡ T ∪ mVR ⁡ T ⟼ if v ∈ mVR ⁡ T f ⁡ v ⟨“ v ”⟩ ∘ X ++ v ∈ mCN ⁡ T ∪ mVR ⁡ T ⟼ if v ∈ mVR ⁡ T f ⁡ v ⟨“ v ”⟩ ∘ Y = ∑ freeMnd ⁡ mCN ⁡ T ∪ mVR ⁡ T v ∈ mCN ⁡ T ∪ mVR ⁡ T ⟼ if v ∈ mVR ⁡ T f ⁡ v ⟨“ v ”⟩ ∘ X + freeMnd ⁡ mCN ⁡ T ∪ mVR ⁡ T ∑ freeMnd ⁡ mCN ⁡ T ∪ mVR ⁡ T v ∈ mCN ⁡ T ∪ mVR ⁡ T ⟼ if v ∈ mVR ⁡ T f ⁡ v ⟨“ v ”⟩ ∘ Y
54 50 gsumwcl ⊢ freeMnd ⁡ mCN ⁡ T ∪ mVR ⁡ T ∈ Mnd ∧ v ∈ mCN ⁡ T ∪ mVR ⁡ T ⟼ if v ∈ mVR ⁡ T f ⁡ v ⟨“ v ”⟩ ∘ X ∈ Word Word mCN ⁡ T ∪ mVR ⁡ T → ∑ freeMnd ⁡ mCN ⁡ T ∪ mVR ⁡ T v ∈ mCN ⁡ T ∪ mVR ⁡ T ⟼ if v ∈ mVR ⁡ T f ⁡ v ⟨“ v ”⟩ ∘ X ∈ Word mCN ⁡ T ∪ mVR ⁡ T
55 42 44 54 syl2anc ⊢ f ∈ R mVR ⁡ T ∧ X ∈ R ∧ Y ∈ R → ∑ freeMnd ⁡ mCN ⁡ T ∪ mVR ⁡ T v ∈ mCN ⁡ T ∪ mVR ⁡ T ⟼ if v ∈ mVR ⁡ T f ⁡ v ⟨“ v ”⟩ ∘ X ∈ Word mCN ⁡ T ∪ mVR ⁡ T
56 50 gsumwcl ⊢ freeMnd ⁡ mCN ⁡ T ∪ mVR ⁡ T ∈ Mnd ∧ v ∈ mCN ⁡ T ∪ mVR ⁡ T ⟼ if v ∈ mVR ⁡ T f ⁡ v ⟨“ v ”⟩ ∘ Y ∈ Word Word mCN ⁡ T ∪ mVR ⁡ T → ∑ freeMnd ⁡ mCN ⁡ T ∪ mVR ⁡ T v ∈ mCN ⁡ T ∪ mVR ⁡ T ⟼ if v ∈ mVR ⁡ T f ⁡ v ⟨“ v ”⟩ ∘ Y ∈ Word mCN ⁡ T ∪ mVR ⁡ T
57 42 46 56 syl2anc ⊢ f ∈ R mVR ⁡ T ∧ X ∈ R ∧ Y ∈ R → ∑ freeMnd ⁡ mCN ⁡ T ∪ mVR ⁡ T v ∈ mCN ⁡ T ∪ mVR ⁡ T ⟼ if v ∈ mVR ⁡ T f ⁡ v ⟨“ v ”⟩ ∘ Y ∈ Word mCN ⁡ T ∪ mVR ⁡ T
58 40 50 51 frmdadd ⊢ ∑ freeMnd ⁡ mCN ⁡ T ∪ mVR ⁡ T v ∈ mCN ⁡ T ∪ mVR ⁡ T ⟼ if v ∈ mVR ⁡ T f ⁡ v ⟨“ v ”⟩ ∘ X ∈ Word mCN ⁡ T ∪ mVR ⁡ T ∧ ∑ freeMnd ⁡ mCN ⁡ T ∪ mVR ⁡ T v ∈ mCN ⁡ T ∪ mVR ⁡ T ⟼ if v ∈ mVR ⁡ T f ⁡ v ⟨“ v ”⟩ ∘ Y ∈ Word mCN ⁡ T ∪ mVR ⁡ T → ∑ freeMnd ⁡ mCN ⁡ T ∪ mVR ⁡ T v ∈ mCN ⁡ T ∪ mVR ⁡ T ⟼ if v ∈ mVR ⁡ T f ⁡ v ⟨“ v ”⟩ ∘ X + freeMnd ⁡ mCN ⁡ T ∪ mVR ⁡ T ∑ freeMnd ⁡ mCN ⁡ T ∪ mVR ⁡ T v ∈ mCN ⁡ T ∪ mVR ⁡ T ⟼ if v ∈ mVR ⁡ T f ⁡ v ⟨“ v ”⟩ ∘ Y = ∑ freeMnd ⁡ mCN ⁡ T ∪ mVR ⁡ T v ∈ mCN ⁡ T ∪ mVR ⁡ T ⟼ if v ∈ mVR ⁡ T f ⁡ v ⟨“ v ”⟩ ∘ X ++ ∑ freeMnd ⁡ mCN ⁡ T ∪ mVR ⁡ T v ∈ mCN ⁡ T ∪ mVR ⁡ T ⟼ if v ∈ mVR ⁡ T f ⁡ v ⟨“ v ”⟩ ∘ Y
59 55 57 58 syl2anc ⊢ f ∈ R mVR ⁡ T ∧ X ∈ R ∧ Y ∈ R → ∑ freeMnd ⁡ mCN ⁡ T ∪ mVR ⁡ T v ∈ mCN ⁡ T ∪ mVR ⁡ T ⟼ if v ∈ mVR ⁡ T f ⁡ v ⟨“ v ”⟩ ∘ X + freeMnd ⁡ mCN ⁡ T ∪ mVR ⁡ T ∑ freeMnd ⁡ mCN ⁡ T ∪ mVR ⁡ T v ∈ mCN ⁡ T ∪ mVR ⁡ T ⟼ if v ∈ mVR ⁡ T f ⁡ v ⟨“ v ”⟩ ∘ Y = ∑ freeMnd ⁡ mCN ⁡ T ∪ mVR ⁡ T v ∈ mCN ⁡ T ∪ mVR ⁡ T ⟼ if v ∈ mVR ⁡ T f ⁡ v ⟨“ v ”⟩ ∘ X ++ ∑ freeMnd ⁡ mCN ⁡ T ∪ mVR ⁡ T v ∈ mCN ⁡ T ∪ mVR ⁡ T ⟼ if v ∈ mVR ⁡ T f ⁡ v ⟨“ v ”⟩ ∘ Y
60 36 53 59 3eqtrd ⊢ f ∈ R mVR ⁡ T ∧ X ∈ R ∧ Y ∈ R → ∑ freeMnd ⁡ mCN ⁡ T ∪ mVR ⁡ T v ∈ mCN ⁡ T ∪ mVR ⁡ T ⟼ if v ∈ mVR ⁡ T f ⁡ v ⟨“ v ”⟩ ∘ X ++ Y = ∑ freeMnd ⁡ mCN ⁡ T ∪ mVR ⁡ T v ∈ mCN ⁡ T ∪ mVR ⁡ T ⟼ if v ∈ mVR ⁡ T f ⁡ v ⟨“ v ”⟩ ∘ X ++ ∑ freeMnd ⁡ mCN ⁡ T ∪ mVR ⁡ T v ∈ mCN ⁡ T ∪ mVR ⁡ T ⟼ if v ∈ mVR ⁡ T f ⁡ v ⟨“ v ”⟩ ∘ Y
61 ssidd ⊢ f ∈ R mVR ⁡ T ∧ X ∈ R ∧ Y ∈ R → mVR ⁡ T ⊆ mVR ⁡ T
62 ccatcl ⊢ X ∈ Word mCN ⁡ T ∪ mVR ⁡ T ∧ Y ∈ Word mCN ⁡ T ∪ mVR ⁡ T → X ++ Y ∈ Word mCN ⁡ T ∪ mVR ⁡ T
63 21 23 62 syl2anc ⊢ f ∈ R mVR ⁡ T ∧ X ∈ R ∧ Y ∈ R → X ++ Y ∈ Word mCN ⁡ T ∪ mVR ⁡ T
64 63 20 eleqtrrd ⊢ f ∈ R mVR ⁡ 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 ⁡ T v ∈ mCN ⁡ T ∪ mVR ⁡ T ⟼ if v ∈ mVR ⁡ T f ⁡ v ⟨“ v ”⟩ ∘ X ++ Y
66 25 61 64 65 syl3anc ⊢ f ∈ R mVR ⁡ T ∧ X ∈ R ∧ Y ∈ R → S ⁡ f ⁡ X ++ Y = ∑ freeMnd ⁡ mCN ⁡ T ∪ mVR ⁡ T v ∈ mCN ⁡ T ∪ mVR ⁡ T ⟼ if v ∈ mVR ⁡ T f ⁡ 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 ⁡ T v ∈ mCN ⁡ T ∪ mVR ⁡ T ⟼ if v ∈ mVR ⁡ T f ⁡ v ⟨“ v ”⟩ ∘ X
68 25 61 15 67 syl3anc ⊢ f ∈ R mVR ⁡ T ∧ X ∈ R ∧ Y ∈ R → S ⁡ f ⁡ X = ∑ freeMnd ⁡ mCN ⁡ T ∪ mVR ⁡ T v ∈ mCN ⁡ T ∪ mVR ⁡ T ⟼ if v ∈ mVR ⁡ T f ⁡ 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 ⁡ T v ∈ mCN ⁡ T ∪ mVR ⁡ T ⟼ if v ∈ mVR ⁡ T f ⁡ v ⟨“ v ”⟩ ∘ Y
70 25 61 22 69 syl3anc ⊢ f ∈ R mVR ⁡ T ∧ X ∈ R ∧ Y ∈ R → S ⁡ f ⁡ Y = ∑ freeMnd ⁡ mCN ⁡ T ∪ mVR ⁡ T v ∈ mCN ⁡ T ∪ mVR ⁡ T ⟼ if v ∈ mVR ⁡ T f ⁡ v ⟨“ v ”⟩ ∘ Y
71 68 70 oveq12d ⊢ f ∈ R mVR ⁡ T ∧ X ∈ R ∧ Y ∈ R → S ⁡ f ⁡ X ++ S ⁡ f ⁡ Y = ∑ freeMnd ⁡ mCN ⁡ T ∪ mVR ⁡ T v ∈ mCN ⁡ T ∪ mVR ⁡ T ⟼ if v ∈ mVR ⁡ T f ⁡ v ⟨“ v ”⟩ ∘ X ++ ∑ freeMnd ⁡ mCN ⁡ T ∪ mVR ⁡ T v ∈ mCN ⁡ T ∪ mVR ⁡ T ⟼ if v ∈ mVR ⁡ T f ⁡ v ⟨“ v ”⟩ ∘ Y
72 60 66 71 3eqtr4d ⊢ f ∈ R mVR ⁡ 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 ∈ R mVR ⁡ T ∧ X ∈ R ∧ Y ∈ R → S ⁡ f = F → F ⁡ X ++ Y = F ⁡ X ++ F ⁡ Y
79 78 ex ⊢ f ∈ R mVR ⁡ T → X ∈ R ∧ Y ∈ R → S ⁡ f = F → F ⁡ X ++ Y = F ⁡ X ++ F ⁡ Y
80 79 com23 ⊢ f ∈ R mVR ⁡ T → S ⁡ f = F → X ∈ R ∧ Y ∈ R → F ⁡ X ++ Y = F ⁡ X ++ F ⁡ Y
81 80 rexlimiv ⊢ ∃ f ∈ R mVR ⁡ T S ⁡ 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