Users' Mathboxes Mathbox for Mario Carneiro < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  mrsubccat Structured version   Visualization version   GIF version

Theorem mrsubccat 32018
Description: Substitution distributes over concatenation. (Contributed by Mario Carneiro, 18-Jul-2016.)
Hypotheses
Ref Expression
mrsubccat.s 𝑆 = (mRSubst‘𝑇)
mrsubccat.r 𝑅 = (mREx‘𝑇)
Assertion
Ref Expression
mrsubccat ((𝐹 ∈ ran 𝑆𝑋𝑅𝑌𝑅) → (𝐹‘(𝑋 ++ 𝑌)) = ((𝐹𝑋) ++ (𝐹𝑌)))

Proof of Theorem mrsubccat
Dummy variables 𝑓 𝑣 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 n0i 4148 . . . . . 6 (𝐹 ∈ ran 𝑆 → ¬ ran 𝑆 = ∅)
2 mrsubccat.s . . . . . . 7 𝑆 = (mRSubst‘𝑇)
32rnfvprc 6442 . . . . . 6 𝑇 ∈ V → ran 𝑆 = ∅)
41, 3nsyl2 145 . . . . 5 (𝐹 ∈ ran 𝑆𝑇 ∈ V)
5 eqid 2778 . . . . . 6 (mVR‘𝑇) = (mVR‘𝑇)
6 mrsubccat.r . . . . . 6 𝑅 = (mREx‘𝑇)
75, 6, 2mrsubff 32012 . . . . 5 (𝑇 ∈ V → 𝑆:(𝑅pm (mVR‘𝑇))⟶(𝑅𝑚 𝑅))
8 ffun 6296 . . . . 5 (𝑆:(𝑅pm (mVR‘𝑇))⟶(𝑅𝑚 𝑅) → Fun 𝑆)
94, 7, 83syl 18 . . . 4 (𝐹 ∈ ran 𝑆 → Fun 𝑆)
105, 6, 2mrsubrn 32013 . . . . . 6 ran 𝑆 = (𝑆 “ (𝑅𝑚 (mVR‘𝑇)))
1110eleq2i 2851 . . . . 5 (𝐹 ∈ ran 𝑆𝐹 ∈ (𝑆 “ (𝑅𝑚 (mVR‘𝑇))))
1211biimpi 208 . . . 4 (𝐹 ∈ ran 𝑆𝐹 ∈ (𝑆 “ (𝑅𝑚 (mVR‘𝑇))))
13 fvelima 6510 . . . 4 ((Fun 𝑆𝐹 ∈ (𝑆 “ (𝑅𝑚 (mVR‘𝑇)))) → ∃𝑓 ∈ (𝑅𝑚 (mVR‘𝑇))(𝑆𝑓) = 𝐹)
149, 12, 13syl2anc 579 . . 3 (𝐹 ∈ ran 𝑆 → ∃𝑓 ∈ (𝑅𝑚 (mVR‘𝑇))(𝑆𝑓) = 𝐹)
15 simprl 761 . . . . . . . . . . . 12 ((𝑓 ∈ (𝑅𝑚 (mVR‘𝑇)) ∧ (𝑋𝑅𝑌𝑅)) → 𝑋𝑅)
16 elfvex 6482 . . . . . . . . . . . . . 14 (𝑋 ∈ (mREx‘𝑇) → 𝑇 ∈ V)
1716, 6eleq2s 2877 . . . . . . . . . . . . 13 (𝑋𝑅𝑇 ∈ V)
18 eqid 2778 . . . . . . . . . . . . . 14 (mCN‘𝑇) = (mCN‘𝑇)
1918, 5, 6mrexval 32001 . . . . . . . . . . . . 13 (𝑇 ∈ V → 𝑅 = Word ((mCN‘𝑇) ∪ (mVR‘𝑇)))
2015, 17, 193syl 18 . . . . . . . . . . . 12 ((𝑓 ∈ (𝑅𝑚 (mVR‘𝑇)) ∧ (𝑋𝑅𝑌𝑅)) → 𝑅 = Word ((mCN‘𝑇) ∪ (mVR‘𝑇)))
2115, 20eleqtrd 2861 . . . . . . . . . . 11 ((𝑓 ∈ (𝑅𝑚 (mVR‘𝑇)) ∧ (𝑋𝑅𝑌𝑅)) → 𝑋 ∈ Word ((mCN‘𝑇) ∪ (mVR‘𝑇)))
22 simprr 763 . . . . . . . . . . . 12 ((𝑓 ∈ (𝑅𝑚 (mVR‘𝑇)) ∧ (𝑋𝑅𝑌𝑅)) → 𝑌𝑅)
2322, 20eleqtrd 2861 . . . . . . . . . . 11 ((𝑓 ∈ (𝑅𝑚 (mVR‘𝑇)) ∧ (𝑋𝑅𝑌𝑅)) → 𝑌 ∈ Word ((mCN‘𝑇) ∪ (mVR‘𝑇)))
24 elmapi 8164 . . . . . . . . . . . . . . . . 17 (𝑓 ∈ (𝑅𝑚 (mVR‘𝑇)) → 𝑓:(mVR‘𝑇)⟶𝑅)
2524adantr 474 . . . . . . . . . . . . . . . 16 ((𝑓 ∈ (𝑅𝑚 (mVR‘𝑇)) ∧ (𝑋𝑅𝑌𝑅)) → 𝑓:(mVR‘𝑇)⟶𝑅)
2625adantr 474 . . . . . . . . . . . . . . 15 (((𝑓 ∈ (𝑅𝑚 (mVR‘𝑇)) ∧ (𝑋𝑅𝑌𝑅)) ∧ 𝑣 ∈ ((mCN‘𝑇) ∪ (mVR‘𝑇))) → 𝑓:(mVR‘𝑇)⟶𝑅)
2726ffvelrnda 6625 . . . . . . . . . . . . . 14 ((((𝑓 ∈ (𝑅𝑚 (mVR‘𝑇)) ∧ (𝑋𝑅𝑌𝑅)) ∧ 𝑣 ∈ ((mCN‘𝑇) ∪ (mVR‘𝑇))) ∧ 𝑣 ∈ (mVR‘𝑇)) → (𝑓𝑣) ∈ 𝑅)
2820ad2antrr 716 . . . . . . . . . . . . . 14 ((((𝑓 ∈ (𝑅𝑚 (mVR‘𝑇)) ∧ (𝑋𝑅𝑌𝑅)) ∧ 𝑣 ∈ ((mCN‘𝑇) ∪ (mVR‘𝑇))) ∧ 𝑣 ∈ (mVR‘𝑇)) → 𝑅 = Word ((mCN‘𝑇) ∪ (mVR‘𝑇)))
2927, 28eleqtrd 2861 . . . . . . . . . . . . 13 ((((𝑓 ∈ (𝑅𝑚 (mVR‘𝑇)) ∧ (𝑋𝑅𝑌𝑅)) ∧ 𝑣 ∈ ((mCN‘𝑇) ∪ (mVR‘𝑇))) ∧ 𝑣 ∈ (mVR‘𝑇)) → (𝑓𝑣) ∈ Word ((mCN‘𝑇) ∪ (mVR‘𝑇)))
30 simplr 759 . . . . . . . . . . . . . 14 ((((𝑓 ∈ (𝑅𝑚 (mVR‘𝑇)) ∧ (𝑋𝑅𝑌𝑅)) ∧ 𝑣 ∈ ((mCN‘𝑇) ∪ (mVR‘𝑇))) ∧ ¬ 𝑣 ∈ (mVR‘𝑇)) → 𝑣 ∈ ((mCN‘𝑇) ∪ (mVR‘𝑇)))
3130s1cld 13697 . . . . . . . . . . . . 13 ((((𝑓 ∈ (𝑅𝑚 (mVR‘𝑇)) ∧ (𝑋𝑅𝑌𝑅)) ∧ 𝑣 ∈ ((mCN‘𝑇) ∪ (mVR‘𝑇))) ∧ ¬ 𝑣 ∈ (mVR‘𝑇)) → ⟨“𝑣”⟩ ∈ Word ((mCN‘𝑇) ∪ (mVR‘𝑇)))
3229, 31ifclda 4341 . . . . . . . . . . . 12 (((𝑓 ∈ (𝑅𝑚 (mVR‘𝑇)) ∧ (𝑋𝑅𝑌𝑅)) ∧ 𝑣 ∈ ((mCN‘𝑇) ∪ (mVR‘𝑇))) → if(𝑣 ∈ (mVR‘𝑇), (𝑓𝑣), ⟨“𝑣”⟩) ∈ Word ((mCN‘𝑇) ∪ (mVR‘𝑇)))
3332fmpttd 6651 . . . . . . . . . . 11 ((𝑓 ∈ (𝑅𝑚 (mVR‘𝑇)) ∧ (𝑋𝑅𝑌𝑅)) → (𝑣 ∈ ((mCN‘𝑇) ∪ (mVR‘𝑇)) ↦ if(𝑣 ∈ (mVR‘𝑇), (𝑓𝑣), ⟨“𝑣”⟩)):((mCN‘𝑇) ∪ (mVR‘𝑇))⟶Word ((mCN‘𝑇) ∪ (mVR‘𝑇)))
34 ccatco 13990 . . . . . . . . . . 11 ((𝑋 ∈ Word ((mCN‘𝑇) ∪ (mVR‘𝑇)) ∧ 𝑌 ∈ Word ((mCN‘𝑇) ∪ (mVR‘𝑇)) ∧ (𝑣 ∈ ((mCN‘𝑇) ∪ (mVR‘𝑇)) ↦ if(𝑣 ∈ (mVR‘𝑇), (𝑓𝑣), ⟨“𝑣”⟩)):((mCN‘𝑇) ∪ (mVR‘𝑇))⟶Word ((mCN‘𝑇) ∪ (mVR‘𝑇))) → ((𝑣 ∈ ((mCN‘𝑇) ∪ (mVR‘𝑇)) ↦ if(𝑣 ∈ (mVR‘𝑇), (𝑓𝑣), ⟨“𝑣”⟩)) ∘ (𝑋 ++ 𝑌)) = (((𝑣 ∈ ((mCN‘𝑇) ∪ (mVR‘𝑇)) ↦ if(𝑣 ∈ (mVR‘𝑇), (𝑓𝑣), ⟨“𝑣”⟩)) ∘ 𝑋) ++ ((𝑣 ∈ ((mCN‘𝑇) ∪ (mVR‘𝑇)) ↦ if(𝑣 ∈ (mVR‘𝑇), (𝑓𝑣), ⟨“𝑣”⟩)) ∘ 𝑌)))
3521, 23, 33, 34syl3anc 1439 . . . . . . . . . 10 ((𝑓 ∈ (𝑅𝑚 (mVR‘𝑇)) ∧ (𝑋𝑅𝑌𝑅)) → ((𝑣 ∈ ((mCN‘𝑇) ∪ (mVR‘𝑇)) ↦ if(𝑣 ∈ (mVR‘𝑇), (𝑓𝑣), ⟨“𝑣”⟩)) ∘ (𝑋 ++ 𝑌)) = (((𝑣 ∈ ((mCN‘𝑇) ∪ (mVR‘𝑇)) ↦ if(𝑣 ∈ (mVR‘𝑇), (𝑓𝑣), ⟨“𝑣”⟩)) ∘ 𝑋) ++ ((𝑣 ∈ ((mCN‘𝑇) ∪ (mVR‘𝑇)) ↦ if(𝑣 ∈ (mVR‘𝑇), (𝑓𝑣), ⟨“𝑣”⟩)) ∘ 𝑌)))
3635oveq2d 6940 . . . . . . . . 9 ((𝑓 ∈ (𝑅𝑚 (mVR‘𝑇)) ∧ (𝑋𝑅𝑌𝑅)) → ((freeMnd‘((mCN‘𝑇) ∪ (mVR‘𝑇))) Σg ((𝑣 ∈ ((mCN‘𝑇) ∪ (mVR‘𝑇)) ↦ if(𝑣 ∈ (mVR‘𝑇), (𝑓𝑣), ⟨“𝑣”⟩)) ∘ (𝑋 ++ 𝑌))) = ((freeMnd‘((mCN‘𝑇) ∪ (mVR‘𝑇))) Σg (((𝑣 ∈ ((mCN‘𝑇) ∪ (mVR‘𝑇)) ↦ if(𝑣 ∈ (mVR‘𝑇), (𝑓𝑣), ⟨“𝑣”⟩)) ∘ 𝑋) ++ ((𝑣 ∈ ((mCN‘𝑇) ∪ (mVR‘𝑇)) ↦ if(𝑣 ∈ (mVR‘𝑇), (𝑓𝑣), ⟨“𝑣”⟩)) ∘ 𝑌))))
37 fvex 6461 . . . . . . . . . . . 12 (mCN‘𝑇) ∈ V
38 fvex 6461 . . . . . . . . . . . 12 (mVR‘𝑇) ∈ V
3937, 38unex 7235 . . . . . . . . . . 11 ((mCN‘𝑇) ∪ (mVR‘𝑇)) ∈ V
40 eqid 2778 . . . . . . . . . . . 12 (freeMnd‘((mCN‘𝑇) ∪ (mVR‘𝑇))) = (freeMnd‘((mCN‘𝑇) ∪ (mVR‘𝑇)))
4140frmdmnd 17787 . . . . . . . . . . 11 (((mCN‘𝑇) ∪ (mVR‘𝑇)) ∈ V → (freeMnd‘((mCN‘𝑇) ∪ (mVR‘𝑇))) ∈ Mnd)
4239, 41mp1i 13 . . . . . . . . . 10 ((𝑓 ∈ (𝑅𝑚 (mVR‘𝑇)) ∧ (𝑋𝑅𝑌𝑅)) → (freeMnd‘((mCN‘𝑇) ∪ (mVR‘𝑇))) ∈ Mnd)
43 wrdco 13986 . . . . . . . . . . 11 ((𝑋 ∈ Word ((mCN‘𝑇) ∪ (mVR‘𝑇)) ∧ (𝑣 ∈ ((mCN‘𝑇) ∪ (mVR‘𝑇)) ↦ if(𝑣 ∈ (mVR‘𝑇), (𝑓𝑣), ⟨“𝑣”⟩)):((mCN‘𝑇) ∪ (mVR‘𝑇))⟶Word ((mCN‘𝑇) ∪ (mVR‘𝑇))) → ((𝑣 ∈ ((mCN‘𝑇) ∪ (mVR‘𝑇)) ↦ if(𝑣 ∈ (mVR‘𝑇), (𝑓𝑣), ⟨“𝑣”⟩)) ∘ 𝑋) ∈ Word Word ((mCN‘𝑇) ∪ (mVR‘𝑇)))
4421, 33, 43syl2anc 579 . . . . . . . . . 10 ((𝑓 ∈ (𝑅𝑚 (mVR‘𝑇)) ∧ (𝑋𝑅𝑌𝑅)) → ((𝑣 ∈ ((mCN‘𝑇) ∪ (mVR‘𝑇)) ↦ if(𝑣 ∈ (mVR‘𝑇), (𝑓𝑣), ⟨“𝑣”⟩)) ∘ 𝑋) ∈ Word Word ((mCN‘𝑇) ∪ (mVR‘𝑇)))
45 wrdco 13986 . . . . . . . . . . 11 ((𝑌 ∈ Word ((mCN‘𝑇) ∪ (mVR‘𝑇)) ∧ (𝑣 ∈ ((mCN‘𝑇) ∪ (mVR‘𝑇)) ↦ if(𝑣 ∈ (mVR‘𝑇), (𝑓𝑣), ⟨“𝑣”⟩)):((mCN‘𝑇) ∪ (mVR‘𝑇))⟶Word ((mCN‘𝑇) ∪ (mVR‘𝑇))) → ((𝑣 ∈ ((mCN‘𝑇) ∪ (mVR‘𝑇)) ↦ if(𝑣 ∈ (mVR‘𝑇), (𝑓𝑣), ⟨“𝑣”⟩)) ∘ 𝑌) ∈ Word Word ((mCN‘𝑇) ∪ (mVR‘𝑇)))
4623, 33, 45syl2anc 579 . . . . . . . . . 10 ((𝑓 ∈ (𝑅𝑚 (mVR‘𝑇)) ∧ (𝑋𝑅𝑌𝑅)) → ((𝑣 ∈ ((mCN‘𝑇) ∪ (mVR‘𝑇)) ↦ if(𝑣 ∈ (mVR‘𝑇), (𝑓𝑣), ⟨“𝑣”⟩)) ∘ 𝑌) ∈ Word Word ((mCN‘𝑇) ∪ (mVR‘𝑇)))
47 eqid 2778 . . . . . . . . . . . . . 14 (Base‘(freeMnd‘((mCN‘𝑇) ∪ (mVR‘𝑇)))) = (Base‘(freeMnd‘((mCN‘𝑇) ∪ (mVR‘𝑇))))
4840, 47frmdbas 17780 . . . . . . . . . . . . 13 (((mCN‘𝑇) ∪ (mVR‘𝑇)) ∈ V → (Base‘(freeMnd‘((mCN‘𝑇) ∪ (mVR‘𝑇)))) = Word ((mCN‘𝑇) ∪ (mVR‘𝑇)))
4939, 48ax-mp 5 . . . . . . . . . . . 12 (Base‘(freeMnd‘((mCN‘𝑇) ∪ (mVR‘𝑇)))) = Word ((mCN‘𝑇) ∪ (mVR‘𝑇))
5049eqcomi 2787 . . . . . . . . . . 11 Word ((mCN‘𝑇) ∪ (mVR‘𝑇)) = (Base‘(freeMnd‘((mCN‘𝑇) ∪ (mVR‘𝑇))))
51 eqid 2778 . . . . . . . . . . 11 (+g‘(freeMnd‘((mCN‘𝑇) ∪ (mVR‘𝑇)))) = (+g‘(freeMnd‘((mCN‘𝑇) ∪ (mVR‘𝑇))))
5250, 51gsumccat 17768 . . . . . . . . . 10 (((freeMnd‘((mCN‘𝑇) ∪ (mVR‘𝑇))) ∈ Mnd ∧ ((𝑣 ∈ ((mCN‘𝑇) ∪ (mVR‘𝑇)) ↦ if(𝑣 ∈ (mVR‘𝑇), (𝑓𝑣), ⟨“𝑣”⟩)) ∘ 𝑋) ∈ Word Word ((mCN‘𝑇) ∪ (mVR‘𝑇)) ∧ ((𝑣 ∈ ((mCN‘𝑇) ∪ (mVR‘𝑇)) ↦ if(𝑣 ∈ (mVR‘𝑇), (𝑓𝑣), ⟨“𝑣”⟩)) ∘ 𝑌) ∈ Word Word ((mCN‘𝑇) ∪ (mVR‘𝑇))) → ((freeMnd‘((mCN‘𝑇) ∪ (mVR‘𝑇))) Σg (((𝑣 ∈ ((mCN‘𝑇) ∪ (mVR‘𝑇)) ↦ if(𝑣 ∈ (mVR‘𝑇), (𝑓𝑣), ⟨“𝑣”⟩)) ∘ 𝑋) ++ ((𝑣 ∈ ((mCN‘𝑇) ∪ (mVR‘𝑇)) ↦ if(𝑣 ∈ (mVR‘𝑇), (𝑓𝑣), ⟨“𝑣”⟩)) ∘ 𝑌))) = (((freeMnd‘((mCN‘𝑇) ∪ (mVR‘𝑇))) Σg ((𝑣 ∈ ((mCN‘𝑇) ∪ (mVR‘𝑇)) ↦ if(𝑣 ∈ (mVR‘𝑇), (𝑓𝑣), ⟨“𝑣”⟩)) ∘ 𝑋))(+g‘(freeMnd‘((mCN‘𝑇) ∪ (mVR‘𝑇))))((freeMnd‘((mCN‘𝑇) ∪ (mVR‘𝑇))) Σg ((𝑣 ∈ ((mCN‘𝑇) ∪ (mVR‘𝑇)) ↦ if(𝑣 ∈ (mVR‘𝑇), (𝑓𝑣), ⟨“𝑣”⟩)) ∘ 𝑌))))
5342, 44, 46, 52syl3anc 1439 . . . . . . . . 9 ((𝑓 ∈ (𝑅𝑚 (mVR‘𝑇)) ∧ (𝑋𝑅𝑌𝑅)) → ((freeMnd‘((mCN‘𝑇) ∪ (mVR‘𝑇))) Σg (((𝑣 ∈ ((mCN‘𝑇) ∪ (mVR‘𝑇)) ↦ if(𝑣 ∈ (mVR‘𝑇), (𝑓𝑣), ⟨“𝑣”⟩)) ∘ 𝑋) ++ ((𝑣 ∈ ((mCN‘𝑇) ∪ (mVR‘𝑇)) ↦ if(𝑣 ∈ (mVR‘𝑇), (𝑓𝑣), ⟨“𝑣”⟩)) ∘ 𝑌))) = (((freeMnd‘((mCN‘𝑇) ∪ (mVR‘𝑇))) Σg ((𝑣 ∈ ((mCN‘𝑇) ∪ (mVR‘𝑇)) ↦ if(𝑣 ∈ (mVR‘𝑇), (𝑓𝑣), ⟨“𝑣”⟩)) ∘ 𝑋))(+g‘(freeMnd‘((mCN‘𝑇) ∪ (mVR‘𝑇))))((freeMnd‘((mCN‘𝑇) ∪ (mVR‘𝑇))) Σg ((𝑣 ∈ ((mCN‘𝑇) ∪ (mVR‘𝑇)) ↦ if(𝑣 ∈ (mVR‘𝑇), (𝑓𝑣), ⟨“𝑣”⟩)) ∘ 𝑌))))
5450gsumwcl 17767 . . . . . . . . . . 11 (((freeMnd‘((mCN‘𝑇) ∪ (mVR‘𝑇))) ∈ Mnd ∧ ((𝑣 ∈ ((mCN‘𝑇) ∪ (mVR‘𝑇)) ↦ if(𝑣 ∈ (mVR‘𝑇), (𝑓𝑣), ⟨“𝑣”⟩)) ∘ 𝑋) ∈ Word Word ((mCN‘𝑇) ∪ (mVR‘𝑇))) → ((freeMnd‘((mCN‘𝑇) ∪ (mVR‘𝑇))) Σg ((𝑣 ∈ ((mCN‘𝑇) ∪ (mVR‘𝑇)) ↦ if(𝑣 ∈ (mVR‘𝑇), (𝑓𝑣), ⟨“𝑣”⟩)) ∘ 𝑋)) ∈ Word ((mCN‘𝑇) ∪ (mVR‘𝑇)))
5542, 44, 54syl2anc 579 . . . . . . . . . 10 ((𝑓 ∈ (𝑅𝑚 (mVR‘𝑇)) ∧ (𝑋𝑅𝑌𝑅)) → ((freeMnd‘((mCN‘𝑇) ∪ (mVR‘𝑇))) Σg ((𝑣 ∈ ((mCN‘𝑇) ∪ (mVR‘𝑇)) ↦ if(𝑣 ∈ (mVR‘𝑇), (𝑓𝑣), ⟨“𝑣”⟩)) ∘ 𝑋)) ∈ Word ((mCN‘𝑇) ∪ (mVR‘𝑇)))
5650gsumwcl 17767 . . . . . . . . . . 11 (((freeMnd‘((mCN‘𝑇) ∪ (mVR‘𝑇))) ∈ Mnd ∧ ((𝑣 ∈ ((mCN‘𝑇) ∪ (mVR‘𝑇)) ↦ if(𝑣 ∈ (mVR‘𝑇), (𝑓𝑣), ⟨“𝑣”⟩)) ∘ 𝑌) ∈ Word Word ((mCN‘𝑇) ∪ (mVR‘𝑇))) → ((freeMnd‘((mCN‘𝑇) ∪ (mVR‘𝑇))) Σg ((𝑣 ∈ ((mCN‘𝑇) ∪ (mVR‘𝑇)) ↦ if(𝑣 ∈ (mVR‘𝑇), (𝑓𝑣), ⟨“𝑣”⟩)) ∘ 𝑌)) ∈ Word ((mCN‘𝑇) ∪ (mVR‘𝑇)))
5742, 46, 56syl2anc 579 . . . . . . . . . 10 ((𝑓 ∈ (𝑅𝑚 (mVR‘𝑇)) ∧ (𝑋𝑅𝑌𝑅)) → ((freeMnd‘((mCN‘𝑇) ∪ (mVR‘𝑇))) Σg ((𝑣 ∈ ((mCN‘𝑇) ∪ (mVR‘𝑇)) ↦ if(𝑣 ∈ (mVR‘𝑇), (𝑓𝑣), ⟨“𝑣”⟩)) ∘ 𝑌)) ∈ Word ((mCN‘𝑇) ∪ (mVR‘𝑇)))
5840, 50, 51frmdadd 17783 . . . . . . . . . 10 ((((freeMnd‘((mCN‘𝑇) ∪ (mVR‘𝑇))) Σg ((𝑣 ∈ ((mCN‘𝑇) ∪ (mVR‘𝑇)) ↦ if(𝑣 ∈ (mVR‘𝑇), (𝑓𝑣), ⟨“𝑣”⟩)) ∘ 𝑋)) ∈ Word ((mCN‘𝑇) ∪ (mVR‘𝑇)) ∧ ((freeMnd‘((mCN‘𝑇) ∪ (mVR‘𝑇))) Σg ((𝑣 ∈ ((mCN‘𝑇) ∪ (mVR‘𝑇)) ↦ if(𝑣 ∈ (mVR‘𝑇), (𝑓𝑣), ⟨“𝑣”⟩)) ∘ 𝑌)) ∈ Word ((mCN‘𝑇) ∪ (mVR‘𝑇))) → (((freeMnd‘((mCN‘𝑇) ∪ (mVR‘𝑇))) Σg ((𝑣 ∈ ((mCN‘𝑇) ∪ (mVR‘𝑇)) ↦ if(𝑣 ∈ (mVR‘𝑇), (𝑓𝑣), ⟨“𝑣”⟩)) ∘ 𝑋))(+g‘(freeMnd‘((mCN‘𝑇) ∪ (mVR‘𝑇))))((freeMnd‘((mCN‘𝑇) ∪ (mVR‘𝑇))) Σg ((𝑣 ∈ ((mCN‘𝑇) ∪ (mVR‘𝑇)) ↦ if(𝑣 ∈ (mVR‘𝑇), (𝑓𝑣), ⟨“𝑣”⟩)) ∘ 𝑌))) = (((freeMnd‘((mCN‘𝑇) ∪ (mVR‘𝑇))) Σg ((𝑣 ∈ ((mCN‘𝑇) ∪ (mVR‘𝑇)) ↦ if(𝑣 ∈ (mVR‘𝑇), (𝑓𝑣), ⟨“𝑣”⟩)) ∘ 𝑋)) ++ ((freeMnd‘((mCN‘𝑇) ∪ (mVR‘𝑇))) Σg ((𝑣 ∈ ((mCN‘𝑇) ∪ (mVR‘𝑇)) ↦ if(𝑣 ∈ (mVR‘𝑇), (𝑓𝑣), ⟨“𝑣”⟩)) ∘ 𝑌))))
5955, 57, 58syl2anc 579 . . . . . . . . 9 ((𝑓 ∈ (𝑅𝑚 (mVR‘𝑇)) ∧ (𝑋𝑅𝑌𝑅)) → (((freeMnd‘((mCN‘𝑇) ∪ (mVR‘𝑇))) Σg ((𝑣 ∈ ((mCN‘𝑇) ∪ (mVR‘𝑇)) ↦ if(𝑣 ∈ (mVR‘𝑇), (𝑓𝑣), ⟨“𝑣”⟩)) ∘ 𝑋))(+g‘(freeMnd‘((mCN‘𝑇) ∪ (mVR‘𝑇))))((freeMnd‘((mCN‘𝑇) ∪ (mVR‘𝑇))) Σg ((𝑣 ∈ ((mCN‘𝑇) ∪ (mVR‘𝑇)) ↦ if(𝑣 ∈ (mVR‘𝑇), (𝑓𝑣), ⟨“𝑣”⟩)) ∘ 𝑌))) = (((freeMnd‘((mCN‘𝑇) ∪ (mVR‘𝑇))) Σg ((𝑣 ∈ ((mCN‘𝑇) ∪ (mVR‘𝑇)) ↦ if(𝑣 ∈ (mVR‘𝑇), (𝑓𝑣), ⟨“𝑣”⟩)) ∘ 𝑋)) ++ ((freeMnd‘((mCN‘𝑇) ∪ (mVR‘𝑇))) Σg ((𝑣 ∈ ((mCN‘𝑇) ∪ (mVR‘𝑇)) ↦ if(𝑣 ∈ (mVR‘𝑇), (𝑓𝑣), ⟨“𝑣”⟩)) ∘ 𝑌))))
6036, 53, 593eqtrd 2818 . . . . . . . 8 ((𝑓 ∈ (𝑅𝑚 (mVR‘𝑇)) ∧ (𝑋𝑅𝑌𝑅)) → ((freeMnd‘((mCN‘𝑇) ∪ (mVR‘𝑇))) Σg ((𝑣 ∈ ((mCN‘𝑇) ∪ (mVR‘𝑇)) ↦ if(𝑣 ∈ (mVR‘𝑇), (𝑓𝑣), ⟨“𝑣”⟩)) ∘ (𝑋 ++ 𝑌))) = (((freeMnd‘((mCN‘𝑇) ∪ (mVR‘𝑇))) Σg ((𝑣 ∈ ((mCN‘𝑇) ∪ (mVR‘𝑇)) ↦ if(𝑣 ∈ (mVR‘𝑇), (𝑓𝑣), ⟨“𝑣”⟩)) ∘ 𝑋)) ++ ((freeMnd‘((mCN‘𝑇) ∪ (mVR‘𝑇))) Σg ((𝑣 ∈ ((mCN‘𝑇) ∪ (mVR‘𝑇)) ↦ if(𝑣 ∈ (mVR‘𝑇), (𝑓𝑣), ⟨“𝑣”⟩)) ∘ 𝑌))))
61 ssidd 3843 . . . . . . . . 9 ((𝑓 ∈ (𝑅𝑚 (mVR‘𝑇)) ∧ (𝑋𝑅𝑌𝑅)) → (mVR‘𝑇) ⊆ (mVR‘𝑇))
62 ccatcl 13668 . . . . . . . . . . 11 ((𝑋 ∈ Word ((mCN‘𝑇) ∪ (mVR‘𝑇)) ∧ 𝑌 ∈ Word ((mCN‘𝑇) ∪ (mVR‘𝑇))) → (𝑋 ++ 𝑌) ∈ Word ((mCN‘𝑇) ∪ (mVR‘𝑇)))
6321, 23, 62syl2anc 579 . . . . . . . . . 10 ((𝑓 ∈ (𝑅𝑚 (mVR‘𝑇)) ∧ (𝑋𝑅𝑌𝑅)) → (𝑋 ++ 𝑌) ∈ Word ((mCN‘𝑇) ∪ (mVR‘𝑇)))
6463, 20eleqtrrd 2862 . . . . . . . . 9 ((𝑓 ∈ (𝑅𝑚 (mVR‘𝑇)) ∧ (𝑋𝑅𝑌𝑅)) → (𝑋 ++ 𝑌) ∈ 𝑅)
6518, 5, 6, 2, 40mrsubval 32009 . . . . . . . . 9 ((𝑓:(mVR‘𝑇)⟶𝑅 ∧ (mVR‘𝑇) ⊆ (mVR‘𝑇) ∧ (𝑋 ++ 𝑌) ∈ 𝑅) → ((𝑆𝑓)‘(𝑋 ++ 𝑌)) = ((freeMnd‘((mCN‘𝑇) ∪ (mVR‘𝑇))) Σg ((𝑣 ∈ ((mCN‘𝑇) ∪ (mVR‘𝑇)) ↦ if(𝑣 ∈ (mVR‘𝑇), (𝑓𝑣), ⟨“𝑣”⟩)) ∘ (𝑋 ++ 𝑌))))
6625, 61, 64, 65syl3anc 1439 . . . . . . . 8 ((𝑓 ∈ (𝑅𝑚 (mVR‘𝑇)) ∧ (𝑋𝑅𝑌𝑅)) → ((𝑆𝑓)‘(𝑋 ++ 𝑌)) = ((freeMnd‘((mCN‘𝑇) ∪ (mVR‘𝑇))) Σg ((𝑣 ∈ ((mCN‘𝑇) ∪ (mVR‘𝑇)) ↦ if(𝑣 ∈ (mVR‘𝑇), (𝑓𝑣), ⟨“𝑣”⟩)) ∘ (𝑋 ++ 𝑌))))
6718, 5, 6, 2, 40mrsubval 32009 . . . . . . . . . 10 ((𝑓:(mVR‘𝑇)⟶𝑅 ∧ (mVR‘𝑇) ⊆ (mVR‘𝑇) ∧ 𝑋𝑅) → ((𝑆𝑓)‘𝑋) = ((freeMnd‘((mCN‘𝑇) ∪ (mVR‘𝑇))) Σg ((𝑣 ∈ ((mCN‘𝑇) ∪ (mVR‘𝑇)) ↦ if(𝑣 ∈ (mVR‘𝑇), (𝑓𝑣), ⟨“𝑣”⟩)) ∘ 𝑋)))
6825, 61, 15, 67syl3anc 1439 . . . . . . . . 9 ((𝑓 ∈ (𝑅𝑚 (mVR‘𝑇)) ∧ (𝑋𝑅𝑌𝑅)) → ((𝑆𝑓)‘𝑋) = ((freeMnd‘((mCN‘𝑇) ∪ (mVR‘𝑇))) Σg ((𝑣 ∈ ((mCN‘𝑇) ∪ (mVR‘𝑇)) ↦ if(𝑣 ∈ (mVR‘𝑇), (𝑓𝑣), ⟨“𝑣”⟩)) ∘ 𝑋)))
6918, 5, 6, 2, 40mrsubval 32009 . . . . . . . . . 10 ((𝑓:(mVR‘𝑇)⟶𝑅 ∧ (mVR‘𝑇) ⊆ (mVR‘𝑇) ∧ 𝑌𝑅) → ((𝑆𝑓)‘𝑌) = ((freeMnd‘((mCN‘𝑇) ∪ (mVR‘𝑇))) Σg ((𝑣 ∈ ((mCN‘𝑇) ∪ (mVR‘𝑇)) ↦ if(𝑣 ∈ (mVR‘𝑇), (𝑓𝑣), ⟨“𝑣”⟩)) ∘ 𝑌)))
7025, 61, 22, 69syl3anc 1439 . . . . . . . . 9 ((𝑓 ∈ (𝑅𝑚 (mVR‘𝑇)) ∧ (𝑋𝑅𝑌𝑅)) → ((𝑆𝑓)‘𝑌) = ((freeMnd‘((mCN‘𝑇) ∪ (mVR‘𝑇))) Σg ((𝑣 ∈ ((mCN‘𝑇) ∪ (mVR‘𝑇)) ↦ if(𝑣 ∈ (mVR‘𝑇), (𝑓𝑣), ⟨“𝑣”⟩)) ∘ 𝑌)))
7168, 70oveq12d 6942 . . . . . . . 8 ((𝑓 ∈ (𝑅𝑚 (mVR‘𝑇)) ∧ (𝑋𝑅𝑌𝑅)) → (((𝑆𝑓)‘𝑋) ++ ((𝑆𝑓)‘𝑌)) = (((freeMnd‘((mCN‘𝑇) ∪ (mVR‘𝑇))) Σg ((𝑣 ∈ ((mCN‘𝑇) ∪ (mVR‘𝑇)) ↦ if(𝑣 ∈ (mVR‘𝑇), (𝑓𝑣), ⟨“𝑣”⟩)) ∘ 𝑋)) ++ ((freeMnd‘((mCN‘𝑇) ∪ (mVR‘𝑇))) Σg ((𝑣 ∈ ((mCN‘𝑇) ∪ (mVR‘𝑇)) ↦ if(𝑣 ∈ (mVR‘𝑇), (𝑓𝑣), ⟨“𝑣”⟩)) ∘ 𝑌))))
7260, 66, 713eqtr4d 2824 . . . . . . 7 ((𝑓 ∈ (𝑅𝑚 (mVR‘𝑇)) ∧ (𝑋𝑅𝑌𝑅)) → ((𝑆𝑓)‘(𝑋 ++ 𝑌)) = (((𝑆𝑓)‘𝑋) ++ ((𝑆𝑓)‘𝑌)))
73 fveq1 6447 . . . . . . . 8 ((𝑆𝑓) = 𝐹 → ((𝑆𝑓)‘(𝑋 ++ 𝑌)) = (𝐹‘(𝑋 ++ 𝑌)))
74 fveq1 6447 . . . . . . . . 9 ((𝑆𝑓) = 𝐹 → ((𝑆𝑓)‘𝑋) = (𝐹𝑋))
75 fveq1 6447 . . . . . . . . 9 ((𝑆𝑓) = 𝐹 → ((𝑆𝑓)‘𝑌) = (𝐹𝑌))
7674, 75oveq12d 6942 . . . . . . . 8 ((𝑆𝑓) = 𝐹 → (((𝑆𝑓)‘𝑋) ++ ((𝑆𝑓)‘𝑌)) = ((𝐹𝑋) ++ (𝐹𝑌)))
7773, 76eqeq12d 2793 . . . . . . 7 ((𝑆𝑓) = 𝐹 → (((𝑆𝑓)‘(𝑋 ++ 𝑌)) = (((𝑆𝑓)‘𝑋) ++ ((𝑆𝑓)‘𝑌)) ↔ (𝐹‘(𝑋 ++ 𝑌)) = ((𝐹𝑋) ++ (𝐹𝑌))))
7872, 77syl5ibcom 237 . . . . . 6 ((𝑓 ∈ (𝑅𝑚 (mVR‘𝑇)) ∧ (𝑋𝑅𝑌𝑅)) → ((𝑆𝑓) = 𝐹 → (𝐹‘(𝑋 ++ 𝑌)) = ((𝐹𝑋) ++ (𝐹𝑌))))
7978ex 403 . . . . 5 (𝑓 ∈ (𝑅𝑚 (mVR‘𝑇)) → ((𝑋𝑅𝑌𝑅) → ((𝑆𝑓) = 𝐹 → (𝐹‘(𝑋 ++ 𝑌)) = ((𝐹𝑋) ++ (𝐹𝑌)))))
8079com23 86 . . . 4 (𝑓 ∈ (𝑅𝑚 (mVR‘𝑇)) → ((𝑆𝑓) = 𝐹 → ((𝑋𝑅𝑌𝑅) → (𝐹‘(𝑋 ++ 𝑌)) = ((𝐹𝑋) ++ (𝐹𝑌)))))
8180rexlimiv 3209 . . 3 (∃𝑓 ∈ (𝑅𝑚 (mVR‘𝑇))(𝑆𝑓) = 𝐹 → ((𝑋𝑅𝑌𝑅) → (𝐹‘(𝑋 ++ 𝑌)) = ((𝐹𝑋) ++ (𝐹𝑌))))
8214, 81syl 17 . 2 (𝐹 ∈ ran 𝑆 → ((𝑋𝑅𝑌𝑅) → (𝐹‘(𝑋 ++ 𝑌)) = ((𝐹𝑋) ++ (𝐹𝑌))))
83823impib 1105 1 ((𝐹 ∈ ran 𝑆𝑋𝑅𝑌𝑅) → (𝐹‘(𝑋 ++ 𝑌)) = ((𝐹𝑋) ++ (𝐹𝑌)))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wa 386  w3a 1071   = wceq 1601  wcel 2107  wrex 3091  Vcvv 3398  cun 3790  wss 3792  c0 4141  ifcif 4307  cmpt 4967  ran crn 5358  cima 5360  ccom 5361  Fun wfun 6131  wf 6133  cfv 6137  (class class class)co 6924  𝑚 cmap 8142  pm cpm 8143  Word cword 13603   ++ cconcat 13664  ⟨“cs1 13689  Basecbs 16259  +gcplusg 16342   Σg cgsu 16491  Mndcmnd 17684  freeMndcfrmd 17775  mCNcmcn 31960  mVRcmvar 31961  mRExcmrex 31966  mRSubstcmrsub 31970
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1839  ax-4 1853  ax-5 1953  ax-6 2021  ax-7 2055  ax-8 2109  ax-9 2116  ax-10 2135  ax-11 2150  ax-12 2163  ax-13 2334  ax-ext 2754  ax-rep 5008  ax-sep 5019  ax-nul 5027  ax-pow 5079  ax-pr 5140  ax-un 7228  ax-cnex 10330  ax-resscn 10331  ax-1cn 10332  ax-icn 10333  ax-addcl 10334  ax-addrcl 10335  ax-mulcl 10336  ax-mulrcl 10337  ax-mulcom 10338  ax-addass 10339  ax-mulass 10340  ax-distr 10341  ax-i2m1 10342  ax-1ne0 10343  ax-1rid 10344  ax-rnegex 10345  ax-rrecex 10346  ax-cnre 10347  ax-pre-lttri 10348  ax-pre-lttrn 10349  ax-pre-ltadd 10350  ax-pre-mulgt0 10351
This theorem depends on definitions:  df-bi 199  df-an 387  df-or 837  df-3or 1072  df-3an 1073  df-tru 1605  df-ex 1824  df-nf 1828  df-sb 2012  df-mo 2551  df-eu 2587  df-clab 2764  df-cleq 2770  df-clel 2774  df-nfc 2921  df-ne 2970  df-nel 3076  df-ral 3095  df-rex 3096  df-reu 3097  df-rmo 3098  df-rab 3099  df-v 3400  df-sbc 3653  df-csb 3752  df-dif 3795  df-un 3797  df-in 3799  df-ss 3806  df-pss 3808  df-nul 4142  df-if 4308  df-pw 4381  df-sn 4399  df-pr 4401  df-tp 4403  df-op 4405  df-uni 4674  df-int 4713  df-iun 4757  df-br 4889  df-opab 4951  df-mpt 4968  df-tr 4990  df-id 5263  df-eprel 5268  df-po 5276  df-so 5277  df-fr 5316  df-we 5318  df-xp 5363  df-rel 5364  df-cnv 5365  df-co 5366  df-dm 5367  df-rn 5368  df-res 5369  df-ima 5370  df-pred 5935  df-ord 5981  df-on 5982  df-lim 5983  df-suc 5984  df-iota 6101  df-fun 6139  df-fn 6140  df-f 6141  df-f1 6142  df-fo 6143  df-f1o 6144  df-fv 6145  df-riota 6885  df-ov 6927  df-oprab 6928  df-mpt2 6929  df-om 7346  df-1st 7447  df-2nd 7448  df-wrecs 7691  df-recs 7753  df-rdg 7791  df-1o 7845  df-oadd 7849  df-er 8028  df-map 8144  df-pm 8145  df-en 8244  df-dom 8245  df-sdom 8246  df-fin 8247  df-card 9100  df-pnf 10415  df-mnf 10416  df-xr 10417  df-ltxr 10418  df-le 10419  df-sub 10610  df-neg 10611  df-nn 11379  df-2 11442  df-n0 11647  df-z 11733  df-uz 11997  df-fz 12648  df-fzo 12789  df-seq 13124  df-hash 13440  df-word 13604  df-concat 13665  df-s1 13690  df-struct 16261  df-ndx 16262  df-slot 16263  df-base 16265  df-sets 16266  df-ress 16267  df-plusg 16355  df-0g 16492  df-gsum 16493  df-mgm 17632  df-sgrp 17674  df-mnd 17685  df-submnd 17726  df-frmd 17777  df-mrex 31986  df-mrsub 31990
This theorem is referenced by:  elmrsubrn  32020  mrsubco  32021  mrsubvrs  32022
  Copyright terms: Public domain W3C validator