| Step |
Hyp |
Ref |
Expression |
| 1 |
|
mrsubccat.s |
⊢ 𝑆 = ( mRSubst ‘ 𝑇 ) |
| 2 |
|
mrsubccat.r |
⊢ 𝑅 = ( mREx ‘ 𝑇 ) |
| 3 |
|
n0i |
⊢ ( 𝐹 ∈ ran 𝑆 → ¬ ran 𝑆 = ∅ ) |
| 4 |
1
|
rnfvprc |
⊢ ( ¬ 𝑇 ∈ V → ran 𝑆 = ∅ ) |
| 5 |
3 4
|
nsyl2 |
⊢ ( 𝐹 ∈ ran 𝑆 → 𝑇 ∈ V ) |
| 6 |
|
eqid |
⊢ ( mVR ‘ 𝑇 ) = ( mVR ‘ 𝑇 ) |
| 7 |
6 2 1
|
mrsubff |
⊢ ( 𝑇 ∈ V → 𝑆 : ( 𝑅 ↑pm ( mVR ‘ 𝑇 ) ) ⟶ ( 𝑅 ↑m 𝑅 ) ) |
| 8 |
|
ffun |
⊢ ( 𝑆 : ( 𝑅 ↑pm ( mVR ‘ 𝑇 ) ) ⟶ ( 𝑅 ↑m 𝑅 ) → Fun 𝑆 ) |
| 9 |
5 7 8
|
3syl |
⊢ ( 𝐹 ∈ ran 𝑆 → Fun 𝑆 ) |
| 10 |
6 2 1
|
mrsubrn |
⊢ ran 𝑆 = ( 𝑆 “ ( 𝑅 ↑m ( mVR ‘ 𝑇 ) ) ) |
| 11 |
10
|
eleq2i |
⊢ ( 𝐹 ∈ ran 𝑆 ↔ 𝐹 ∈ ( 𝑆 “ ( 𝑅 ↑m ( mVR ‘ 𝑇 ) ) ) ) |
| 12 |
11
|
biimpi |
⊢ ( 𝐹 ∈ ran 𝑆 → 𝐹 ∈ ( 𝑆 “ ( 𝑅 ↑m ( mVR ‘ 𝑇 ) ) ) ) |
| 13 |
|
fvelima |
⊢ ( ( Fun 𝑆 ∧ 𝐹 ∈ ( 𝑆 “ ( 𝑅 ↑m ( mVR ‘ 𝑇 ) ) ) ) → ∃ 𝑓 ∈ ( 𝑅 ↑m ( mVR ‘ 𝑇 ) ) ( 𝑆 ‘ 𝑓 ) = 𝐹 ) |
| 14 |
9 12 13
|
syl2anc |
⊢ ( 𝐹 ∈ ran 𝑆 → ∃ 𝑓 ∈ ( 𝑅 ↑m ( mVR ‘ 𝑇 ) ) ( 𝑆 ‘ 𝑓 ) = 𝐹 ) |
| 15 |
|
simprl |
⊢ ( ( 𝑓 ∈ ( 𝑅 ↑m ( mVR ‘ 𝑇 ) ) ∧ ( 𝑋 ∈ 𝑅 ∧ 𝑌 ∈ 𝑅 ) ) → 𝑋 ∈ 𝑅 ) |
| 16 |
|
elfvex |
⊢ ( 𝑋 ∈ ( mREx ‘ 𝑇 ) → 𝑇 ∈ V ) |
| 17 |
16 2
|
eleq2s |
⊢ ( 𝑋 ∈ 𝑅 → 𝑇 ∈ V ) |
| 18 |
|
eqid |
⊢ ( mCN ‘ 𝑇 ) = ( mCN ‘ 𝑇 ) |
| 19 |
18 6 2
|
mrexval |
⊢ ( 𝑇 ∈ V → 𝑅 = Word ( ( mCN ‘ 𝑇 ) ∪ ( mVR ‘ 𝑇 ) ) ) |
| 20 |
15 17 19
|
3syl |
⊢ ( ( 𝑓 ∈ ( 𝑅 ↑m ( mVR ‘ 𝑇 ) ) ∧ ( 𝑋 ∈ 𝑅 ∧ 𝑌 ∈ 𝑅 ) ) → 𝑅 = Word ( ( mCN ‘ 𝑇 ) ∪ ( mVR ‘ 𝑇 ) ) ) |
| 21 |
15 20
|
eleqtrd |
⊢ ( ( 𝑓 ∈ ( 𝑅 ↑m ( mVR ‘ 𝑇 ) ) ∧ ( 𝑋 ∈ 𝑅 ∧ 𝑌 ∈ 𝑅 ) ) → 𝑋 ∈ Word ( ( mCN ‘ 𝑇 ) ∪ ( mVR ‘ 𝑇 ) ) ) |
| 22 |
|
simprr |
⊢ ( ( 𝑓 ∈ ( 𝑅 ↑m ( mVR ‘ 𝑇 ) ) ∧ ( 𝑋 ∈ 𝑅 ∧ 𝑌 ∈ 𝑅 ) ) → 𝑌 ∈ 𝑅 ) |
| 23 |
22 20
|
eleqtrd |
⊢ ( ( 𝑓 ∈ ( 𝑅 ↑m ( mVR ‘ 𝑇 ) ) ∧ ( 𝑋 ∈ 𝑅 ∧ 𝑌 ∈ 𝑅 ) ) → 𝑌 ∈ Word ( ( mCN ‘ 𝑇 ) ∪ ( mVR ‘ 𝑇 ) ) ) |
| 24 |
|
elmapi |
⊢ ( 𝑓 ∈ ( 𝑅 ↑m ( mVR ‘ 𝑇 ) ) → 𝑓 : ( mVR ‘ 𝑇 ) ⟶ 𝑅 ) |
| 25 |
24
|
adantr |
⊢ ( ( 𝑓 ∈ ( 𝑅 ↑m ( mVR ‘ 𝑇 ) ) ∧ ( 𝑋 ∈ 𝑅 ∧ 𝑌 ∈ 𝑅 ) ) → 𝑓 : ( mVR ‘ 𝑇 ) ⟶ 𝑅 ) |
| 26 |
25
|
adantr |
⊢ ( ( ( 𝑓 ∈ ( 𝑅 ↑m ( mVR ‘ 𝑇 ) ) ∧ ( 𝑋 ∈ 𝑅 ∧ 𝑌 ∈ 𝑅 ) ) ∧ 𝑣 ∈ ( ( mCN ‘ 𝑇 ) ∪ ( mVR ‘ 𝑇 ) ) ) → 𝑓 : ( mVR ‘ 𝑇 ) ⟶ 𝑅 ) |
| 27 |
26
|
ffvelrnda |
⊢ ( ( ( ( 𝑓 ∈ ( 𝑅 ↑m ( mVR ‘ 𝑇 ) ) ∧ ( 𝑋 ∈ 𝑅 ∧ 𝑌 ∈ 𝑅 ) ) ∧ 𝑣 ∈ ( ( mCN ‘ 𝑇 ) ∪ ( mVR ‘ 𝑇 ) ) ) ∧ 𝑣 ∈ ( mVR ‘ 𝑇 ) ) → ( 𝑓 ‘ 𝑣 ) ∈ 𝑅 ) |
| 28 |
20
|
ad2antrr |
⊢ ( ( ( ( 𝑓 ∈ ( 𝑅 ↑m ( mVR ‘ 𝑇 ) ) ∧ ( 𝑋 ∈ 𝑅 ∧ 𝑌 ∈ 𝑅 ) ) ∧ 𝑣 ∈ ( ( mCN ‘ 𝑇 ) ∪ ( mVR ‘ 𝑇 ) ) ) ∧ 𝑣 ∈ ( mVR ‘ 𝑇 ) ) → 𝑅 = Word ( ( mCN ‘ 𝑇 ) ∪ ( mVR ‘ 𝑇 ) ) ) |
| 29 |
27 28
|
eleqtrd |
⊢ ( ( ( ( 𝑓 ∈ ( 𝑅 ↑m ( mVR ‘ 𝑇 ) ) ∧ ( 𝑋 ∈ 𝑅 ∧ 𝑌 ∈ 𝑅 ) ) ∧ 𝑣 ∈ ( ( mCN ‘ 𝑇 ) ∪ ( mVR ‘ 𝑇 ) ) ) ∧ 𝑣 ∈ ( mVR ‘ 𝑇 ) ) → ( 𝑓 ‘ 𝑣 ) ∈ Word ( ( mCN ‘ 𝑇 ) ∪ ( mVR ‘ 𝑇 ) ) ) |
| 30 |
|
simplr |
⊢ ( ( ( ( 𝑓 ∈ ( 𝑅 ↑m ( mVR ‘ 𝑇 ) ) ∧ ( 𝑋 ∈ 𝑅 ∧ 𝑌 ∈ 𝑅 ) ) ∧ 𝑣 ∈ ( ( mCN ‘ 𝑇 ) ∪ ( mVR ‘ 𝑇 ) ) ) ∧ ¬ 𝑣 ∈ ( mVR ‘ 𝑇 ) ) → 𝑣 ∈ ( ( mCN ‘ 𝑇 ) ∪ ( mVR ‘ 𝑇 ) ) ) |
| 31 |
30
|
s1cld |
⊢ ( ( ( ( 𝑓 ∈ ( 𝑅 ↑m ( mVR ‘ 𝑇 ) ) ∧ ( 𝑋 ∈ 𝑅 ∧ 𝑌 ∈ 𝑅 ) ) ∧ 𝑣 ∈ ( ( mCN ‘ 𝑇 ) ∪ ( mVR ‘ 𝑇 ) ) ) ∧ ¬ 𝑣 ∈ ( mVR ‘ 𝑇 ) ) → ⟨“ 𝑣 ”⟩ ∈ Word ( ( mCN ‘ 𝑇 ) ∪ ( mVR ‘ 𝑇 ) ) ) |
| 32 |
29 31
|
ifclda |
⊢ ( ( ( 𝑓 ∈ ( 𝑅 ↑m ( mVR ‘ 𝑇 ) ) ∧ ( 𝑋 ∈ 𝑅 ∧ 𝑌 ∈ 𝑅 ) ) ∧ 𝑣 ∈ ( ( mCN ‘ 𝑇 ) ∪ ( mVR ‘ 𝑇 ) ) ) → if ( 𝑣 ∈ ( mVR ‘ 𝑇 ) , ( 𝑓 ‘ 𝑣 ) , ⟨“ 𝑣 ”⟩ ) ∈ Word ( ( mCN ‘ 𝑇 ) ∪ ( mVR ‘ 𝑇 ) ) ) |
| 33 |
32
|
fmpttd |
⊢ ( ( 𝑓 ∈ ( 𝑅 ↑m ( mVR ‘ 𝑇 ) ) ∧ ( 𝑋 ∈ 𝑅 ∧ 𝑌 ∈ 𝑅 ) ) → ( 𝑣 ∈ ( ( mCN ‘ 𝑇 ) ∪ ( mVR ‘ 𝑇 ) ) ↦ if ( 𝑣 ∈ ( mVR ‘ 𝑇 ) , ( 𝑓 ‘ 𝑣 ) , ⟨“ 𝑣 ”⟩ ) ) : ( ( mCN ‘ 𝑇 ) ∪ ( mVR ‘ 𝑇 ) ) ⟶ Word ( ( mCN ‘ 𝑇 ) ∪ ( mVR ‘ 𝑇 ) ) ) |
| 34 |
|
ccatco |
⊢ ( ( 𝑋 ∈ 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 ‘ 𝑇 ) , ( 𝑓 ‘ 𝑣 ) , ⟨“ 𝑣 ”⟩ ) ) ∘ 𝑌 ) ) ) |
| 35 |
21 23 33 34
|
syl3anc |
⊢ ( ( 𝑓 ∈ ( 𝑅 ↑m ( mVR ‘ 𝑇 ) ) ∧ ( 𝑋 ∈ 𝑅 ∧ 𝑌 ∈ 𝑅 ) ) → ( ( 𝑣 ∈ ( ( mCN ‘ 𝑇 ) ∪ ( mVR ‘ 𝑇 ) ) ↦ if ( 𝑣 ∈ ( mVR ‘ 𝑇 ) , ( 𝑓 ‘ 𝑣 ) , ⟨“ 𝑣 ”⟩ ) ) ∘ ( 𝑋 ++ 𝑌 ) ) = ( ( ( 𝑣 ∈ ( ( mCN ‘ 𝑇 ) ∪ ( mVR ‘ 𝑇 ) ) ↦ if ( 𝑣 ∈ ( mVR ‘ 𝑇 ) , ( 𝑓 ‘ 𝑣 ) , ⟨“ 𝑣 ”⟩ ) ) ∘ 𝑋 ) ++ ( ( 𝑣 ∈ ( ( mCN ‘ 𝑇 ) ∪ ( mVR ‘ 𝑇 ) ) ↦ if ( 𝑣 ∈ ( mVR ‘ 𝑇 ) , ( 𝑓 ‘ 𝑣 ) , ⟨“ 𝑣 ”⟩ ) ) ∘ 𝑌 ) ) ) |
| 36 |
35
|
oveq2d |
⊢ ( ( 𝑓 ∈ ( 𝑅 ↑m ( mVR ‘ 𝑇 ) ) ∧ ( 𝑋 ∈ 𝑅 ∧ 𝑌 ∈ 𝑅 ) ) → ( ( freeMnd ‘ ( ( mCN ‘ 𝑇 ) ∪ ( mVR ‘ 𝑇 ) ) ) Σg ( ( 𝑣 ∈ ( ( mCN ‘ 𝑇 ) ∪ ( mVR ‘ 𝑇 ) ) ↦ if ( 𝑣 ∈ ( mVR ‘ 𝑇 ) , ( 𝑓 ‘ 𝑣 ) , ⟨“ 𝑣 ”⟩ ) ) ∘ ( 𝑋 ++ 𝑌 ) ) ) = ( ( freeMnd ‘ ( ( mCN ‘ 𝑇 ) ∪ ( mVR ‘ 𝑇 ) ) ) Σg ( ( ( 𝑣 ∈ ( ( mCN ‘ 𝑇 ) ∪ ( mVR ‘ 𝑇 ) ) ↦ if ( 𝑣 ∈ ( mVR ‘ 𝑇 ) , ( 𝑓 ‘ 𝑣 ) , ⟨“ 𝑣 ”⟩ ) ) ∘ 𝑋 ) ++ ( ( 𝑣 ∈ ( ( mCN ‘ 𝑇 ) ∪ ( mVR ‘ 𝑇 ) ) ↦ if ( 𝑣 ∈ ( mVR ‘ 𝑇 ) , ( 𝑓 ‘ 𝑣 ) , ⟨“ 𝑣 ”⟩ ) ) ∘ 𝑌 ) ) ) ) |
| 37 |
|
fvex |
⊢ ( mCN ‘ 𝑇 ) ∈ V |
| 38 |
|
fvex |
⊢ ( mVR ‘ 𝑇 ) ∈ V |
| 39 |
37 38
|
unex |
⊢ ( ( mCN ‘ 𝑇 ) ∪ ( mVR ‘ 𝑇 ) ) ∈ V |
| 40 |
|
eqid |
⊢ ( freeMnd ‘ ( ( mCN ‘ 𝑇 ) ∪ ( mVR ‘ 𝑇 ) ) ) = ( freeMnd ‘ ( ( mCN ‘ 𝑇 ) ∪ ( mVR ‘ 𝑇 ) ) ) |
| 41 |
40
|
frmdmnd |
⊢ ( ( ( mCN ‘ 𝑇 ) ∪ ( mVR ‘ 𝑇 ) ) ∈ V → ( freeMnd ‘ ( ( mCN ‘ 𝑇 ) ∪ ( mVR ‘ 𝑇 ) ) ) ∈ Mnd ) |
| 42 |
39 41
|
mp1i |
⊢ ( ( 𝑓 ∈ ( 𝑅 ↑m ( mVR ‘ 𝑇 ) ) ∧ ( 𝑋 ∈ 𝑅 ∧ 𝑌 ∈ 𝑅 ) ) → ( freeMnd ‘ ( ( mCN ‘ 𝑇 ) ∪ ( mVR ‘ 𝑇 ) ) ) ∈ Mnd ) |
| 43 |
|
wrdco |
⊢ ( ( 𝑋 ∈ Word ( ( mCN ‘ 𝑇 ) ∪ ( mVR ‘ 𝑇 ) ) ∧ ( 𝑣 ∈ ( ( mCN ‘ 𝑇 ) ∪ ( mVR ‘ 𝑇 ) ) ↦ if ( 𝑣 ∈ ( mVR ‘ 𝑇 ) , ( 𝑓 ‘ 𝑣 ) , ⟨“ 𝑣 ”⟩ ) ) : ( ( mCN ‘ 𝑇 ) ∪ ( mVR ‘ 𝑇 ) ) ⟶ Word ( ( mCN ‘ 𝑇 ) ∪ ( mVR ‘ 𝑇 ) ) ) → ( ( 𝑣 ∈ ( ( mCN ‘ 𝑇 ) ∪ ( mVR ‘ 𝑇 ) ) ↦ if ( 𝑣 ∈ ( mVR ‘ 𝑇 ) , ( 𝑓 ‘ 𝑣 ) , ⟨“ 𝑣 ”⟩ ) ) ∘ 𝑋 ) ∈ Word Word ( ( mCN ‘ 𝑇 ) ∪ ( mVR ‘ 𝑇 ) ) ) |
| 44 |
21 33 43
|
syl2anc |
⊢ ( ( 𝑓 ∈ ( 𝑅 ↑m ( mVR ‘ 𝑇 ) ) ∧ ( 𝑋 ∈ 𝑅 ∧ 𝑌 ∈ 𝑅 ) ) → ( ( 𝑣 ∈ ( ( mCN ‘ 𝑇 ) ∪ ( mVR ‘ 𝑇 ) ) ↦ if ( 𝑣 ∈ ( mVR ‘ 𝑇 ) , ( 𝑓 ‘ 𝑣 ) , ⟨“ 𝑣 ”⟩ ) ) ∘ 𝑋 ) ∈ Word Word ( ( mCN ‘ 𝑇 ) ∪ ( mVR ‘ 𝑇 ) ) ) |
| 45 |
|
wrdco |
⊢ ( ( 𝑌 ∈ Word ( ( mCN ‘ 𝑇 ) ∪ ( mVR ‘ 𝑇 ) ) ∧ ( 𝑣 ∈ ( ( mCN ‘ 𝑇 ) ∪ ( mVR ‘ 𝑇 ) ) ↦ if ( 𝑣 ∈ ( mVR ‘ 𝑇 ) , ( 𝑓 ‘ 𝑣 ) , ⟨“ 𝑣 ”⟩ ) ) : ( ( mCN ‘ 𝑇 ) ∪ ( mVR ‘ 𝑇 ) ) ⟶ Word ( ( mCN ‘ 𝑇 ) ∪ ( mVR ‘ 𝑇 ) ) ) → ( ( 𝑣 ∈ ( ( mCN ‘ 𝑇 ) ∪ ( mVR ‘ 𝑇 ) ) ↦ if ( 𝑣 ∈ ( mVR ‘ 𝑇 ) , ( 𝑓 ‘ 𝑣 ) , ⟨“ 𝑣 ”⟩ ) ) ∘ 𝑌 ) ∈ Word Word ( ( mCN ‘ 𝑇 ) ∪ ( mVR ‘ 𝑇 ) ) ) |
| 46 |
23 33 45
|
syl2anc |
⊢ ( ( 𝑓 ∈ ( 𝑅 ↑m ( mVR ‘ 𝑇 ) ) ∧ ( 𝑋 ∈ 𝑅 ∧ 𝑌 ∈ 𝑅 ) ) → ( ( 𝑣 ∈ ( ( mCN ‘ 𝑇 ) ∪ ( mVR ‘ 𝑇 ) ) ↦ if ( 𝑣 ∈ ( mVR ‘ 𝑇 ) , ( 𝑓 ‘ 𝑣 ) , ⟨“ 𝑣 ”⟩ ) ) ∘ 𝑌 ) ∈ Word Word ( ( mCN ‘ 𝑇 ) ∪ ( mVR ‘ 𝑇 ) ) ) |
| 47 |
|
eqid |
⊢ ( Base ‘ ( freeMnd ‘ ( ( mCN ‘ 𝑇 ) ∪ ( mVR ‘ 𝑇 ) ) ) ) = ( Base ‘ ( freeMnd ‘ ( ( mCN ‘ 𝑇 ) ∪ ( mVR ‘ 𝑇 ) ) ) ) |
| 48 |
40 47
|
frmdbas |
⊢ ( ( ( mCN ‘ 𝑇 ) ∪ ( mVR ‘ 𝑇 ) ) ∈ V → ( Base ‘ ( freeMnd ‘ ( ( mCN ‘ 𝑇 ) ∪ ( mVR ‘ 𝑇 ) ) ) ) = Word ( ( mCN ‘ 𝑇 ) ∪ ( mVR ‘ 𝑇 ) ) ) |
| 49 |
39 48
|
ax-mp |
⊢ ( Base ‘ ( freeMnd ‘ ( ( mCN ‘ 𝑇 ) ∪ ( mVR ‘ 𝑇 ) ) ) ) = Word ( ( mCN ‘ 𝑇 ) ∪ ( mVR ‘ 𝑇 ) ) |
| 50 |
49
|
eqcomi |
⊢ Word ( ( mCN ‘ 𝑇 ) ∪ ( mVR ‘ 𝑇 ) ) = ( Base ‘ ( freeMnd ‘ ( ( mCN ‘ 𝑇 ) ∪ ( mVR ‘ 𝑇 ) ) ) ) |
| 51 |
|
eqid |
⊢ ( +g ‘ ( freeMnd ‘ ( ( mCN ‘ 𝑇 ) ∪ ( mVR ‘ 𝑇 ) ) ) ) = ( +g ‘ ( freeMnd ‘ ( ( mCN ‘ 𝑇 ) ∪ ( mVR ‘ 𝑇 ) ) ) ) |
| 52 |
50 51
|
gsumccat |
⊢ ( ( ( 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 ‘ 𝑇 ) , ( 𝑓 ‘ 𝑣 ) , ⟨“ 𝑣 ”⟩ ) ) ∘ 𝑌 ) ) ) ) |
| 53 |
42 44 46 52
|
syl3anc |
⊢ ( ( 𝑓 ∈ ( 𝑅 ↑m ( 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 ‘ 𝑇 ) , ( 𝑓 ‘ 𝑣 ) , ⟨“ 𝑣 ”⟩ ) ) ∘ 𝑌 ) ) ) ) |
| 54 |
50
|
gsumwcl |
⊢ ( ( ( freeMnd ‘ ( ( mCN ‘ 𝑇 ) ∪ ( mVR ‘ 𝑇 ) ) ) ∈ Mnd ∧ ( ( 𝑣 ∈ ( ( mCN ‘ 𝑇 ) ∪ ( mVR ‘ 𝑇 ) ) ↦ if ( 𝑣 ∈ ( mVR ‘ 𝑇 ) , ( 𝑓 ‘ 𝑣 ) , ⟨“ 𝑣 ”⟩ ) ) ∘ 𝑋 ) ∈ Word Word ( ( mCN ‘ 𝑇 ) ∪ ( mVR ‘ 𝑇 ) ) ) → ( ( freeMnd ‘ ( ( mCN ‘ 𝑇 ) ∪ ( mVR ‘ 𝑇 ) ) ) Σg ( ( 𝑣 ∈ ( ( mCN ‘ 𝑇 ) ∪ ( mVR ‘ 𝑇 ) ) ↦ if ( 𝑣 ∈ ( mVR ‘ 𝑇 ) , ( 𝑓 ‘ 𝑣 ) , ⟨“ 𝑣 ”⟩ ) ) ∘ 𝑋 ) ) ∈ Word ( ( mCN ‘ 𝑇 ) ∪ ( mVR ‘ 𝑇 ) ) ) |
| 55 |
42 44 54
|
syl2anc |
⊢ ( ( 𝑓 ∈ ( 𝑅 ↑m ( mVR ‘ 𝑇 ) ) ∧ ( 𝑋 ∈ 𝑅 ∧ 𝑌 ∈ 𝑅 ) ) → ( ( freeMnd ‘ ( ( mCN ‘ 𝑇 ) ∪ ( mVR ‘ 𝑇 ) ) ) Σg ( ( 𝑣 ∈ ( ( mCN ‘ 𝑇 ) ∪ ( mVR ‘ 𝑇 ) ) ↦ if ( 𝑣 ∈ ( mVR ‘ 𝑇 ) , ( 𝑓 ‘ 𝑣 ) , ⟨“ 𝑣 ”⟩ ) ) ∘ 𝑋 ) ) ∈ Word ( ( mCN ‘ 𝑇 ) ∪ ( mVR ‘ 𝑇 ) ) ) |
| 56 |
50
|
gsumwcl |
⊢ ( ( ( freeMnd ‘ ( ( mCN ‘ 𝑇 ) ∪ ( mVR ‘ 𝑇 ) ) ) ∈ Mnd ∧ ( ( 𝑣 ∈ ( ( mCN ‘ 𝑇 ) ∪ ( mVR ‘ 𝑇 ) ) ↦ if ( 𝑣 ∈ ( mVR ‘ 𝑇 ) , ( 𝑓 ‘ 𝑣 ) , ⟨“ 𝑣 ”⟩ ) ) ∘ 𝑌 ) ∈ Word Word ( ( mCN ‘ 𝑇 ) ∪ ( mVR ‘ 𝑇 ) ) ) → ( ( freeMnd ‘ ( ( mCN ‘ 𝑇 ) ∪ ( mVR ‘ 𝑇 ) ) ) Σg ( ( 𝑣 ∈ ( ( mCN ‘ 𝑇 ) ∪ ( mVR ‘ 𝑇 ) ) ↦ if ( 𝑣 ∈ ( mVR ‘ 𝑇 ) , ( 𝑓 ‘ 𝑣 ) , ⟨“ 𝑣 ”⟩ ) ) ∘ 𝑌 ) ) ∈ Word ( ( mCN ‘ 𝑇 ) ∪ ( mVR ‘ 𝑇 ) ) ) |
| 57 |
42 46 56
|
syl2anc |
⊢ ( ( 𝑓 ∈ ( 𝑅 ↑m ( mVR ‘ 𝑇 ) ) ∧ ( 𝑋 ∈ 𝑅 ∧ 𝑌 ∈ 𝑅 ) ) → ( ( freeMnd ‘ ( ( mCN ‘ 𝑇 ) ∪ ( mVR ‘ 𝑇 ) ) ) Σg ( ( 𝑣 ∈ ( ( mCN ‘ 𝑇 ) ∪ ( mVR ‘ 𝑇 ) ) ↦ if ( 𝑣 ∈ ( mVR ‘ 𝑇 ) , ( 𝑓 ‘ 𝑣 ) , ⟨“ 𝑣 ”⟩ ) ) ∘ 𝑌 ) ) ∈ Word ( ( mCN ‘ 𝑇 ) ∪ ( mVR ‘ 𝑇 ) ) ) |
| 58 |
40 50 51
|
frmdadd |
⊢ ( ( ( ( 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 ‘ 𝑇 ) , ( 𝑓 ‘ 𝑣 ) , ⟨“ 𝑣 ”⟩ ) ) ∘ 𝑌 ) ) ) ) |
| 59 |
55 57 58
|
syl2anc |
⊢ ( ( 𝑓 ∈ ( 𝑅 ↑m ( 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 ‘ 𝑇 ) , ( 𝑓 ‘ 𝑣 ) , ⟨“ 𝑣 ”⟩ ) ) ∘ 𝑌 ) ) ) ) |
| 60 |
36 53 59
|
3eqtrd |
⊢ ( ( 𝑓 ∈ ( 𝑅 ↑m ( 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 |
⊢ ( ( 𝑓 ∈ ( 𝑅 ↑m ( mVR ‘ 𝑇 ) ) ∧ ( 𝑋 ∈ 𝑅 ∧ 𝑌 ∈ 𝑅 ) ) → ( mVR ‘ 𝑇 ) ⊆ ( mVR ‘ 𝑇 ) ) |
| 62 |
|
ccatcl |
⊢ ( ( 𝑋 ∈ Word ( ( mCN ‘ 𝑇 ) ∪ ( mVR ‘ 𝑇 ) ) ∧ 𝑌 ∈ Word ( ( mCN ‘ 𝑇 ) ∪ ( mVR ‘ 𝑇 ) ) ) → ( 𝑋 ++ 𝑌 ) ∈ Word ( ( mCN ‘ 𝑇 ) ∪ ( mVR ‘ 𝑇 ) ) ) |
| 63 |
21 23 62
|
syl2anc |
⊢ ( ( 𝑓 ∈ ( 𝑅 ↑m ( mVR ‘ 𝑇 ) ) ∧ ( 𝑋 ∈ 𝑅 ∧ 𝑌 ∈ 𝑅 ) ) → ( 𝑋 ++ 𝑌 ) ∈ Word ( ( mCN ‘ 𝑇 ) ∪ ( mVR ‘ 𝑇 ) ) ) |
| 64 |
63 20
|
eleqtrrd |
⊢ ( ( 𝑓 ∈ ( 𝑅 ↑m ( mVR ‘ 𝑇 ) ) ∧ ( 𝑋 ∈ 𝑅 ∧ 𝑌 ∈ 𝑅 ) ) → ( 𝑋 ++ 𝑌 ) ∈ 𝑅 ) |
| 65 |
18 6 2 1 40
|
mrsubval |
⊢ ( ( 𝑓 : ( mVR ‘ 𝑇 ) ⟶ 𝑅 ∧ ( mVR ‘ 𝑇 ) ⊆ ( mVR ‘ 𝑇 ) ∧ ( 𝑋 ++ 𝑌 ) ∈ 𝑅 ) → ( ( 𝑆 ‘ 𝑓 ) ‘ ( 𝑋 ++ 𝑌 ) ) = ( ( freeMnd ‘ ( ( mCN ‘ 𝑇 ) ∪ ( mVR ‘ 𝑇 ) ) ) Σg ( ( 𝑣 ∈ ( ( mCN ‘ 𝑇 ) ∪ ( mVR ‘ 𝑇 ) ) ↦ if ( 𝑣 ∈ ( mVR ‘ 𝑇 ) , ( 𝑓 ‘ 𝑣 ) , ⟨“ 𝑣 ”⟩ ) ) ∘ ( 𝑋 ++ 𝑌 ) ) ) ) |
| 66 |
25 61 64 65
|
syl3anc |
⊢ ( ( 𝑓 ∈ ( 𝑅 ↑m ( mVR ‘ 𝑇 ) ) ∧ ( 𝑋 ∈ 𝑅 ∧ 𝑌 ∈ 𝑅 ) ) → ( ( 𝑆 ‘ 𝑓 ) ‘ ( 𝑋 ++ 𝑌 ) ) = ( ( freeMnd ‘ ( ( mCN ‘ 𝑇 ) ∪ ( mVR ‘ 𝑇 ) ) ) Σg ( ( 𝑣 ∈ ( ( mCN ‘ 𝑇 ) ∪ ( mVR ‘ 𝑇 ) ) ↦ if ( 𝑣 ∈ ( mVR ‘ 𝑇 ) , ( 𝑓 ‘ 𝑣 ) , ⟨“ 𝑣 ”⟩ ) ) ∘ ( 𝑋 ++ 𝑌 ) ) ) ) |
| 67 |
18 6 2 1 40
|
mrsubval |
⊢ ( ( 𝑓 : ( mVR ‘ 𝑇 ) ⟶ 𝑅 ∧ ( mVR ‘ 𝑇 ) ⊆ ( mVR ‘ 𝑇 ) ∧ 𝑋 ∈ 𝑅 ) → ( ( 𝑆 ‘ 𝑓 ) ‘ 𝑋 ) = ( ( freeMnd ‘ ( ( mCN ‘ 𝑇 ) ∪ ( mVR ‘ 𝑇 ) ) ) Σg ( ( 𝑣 ∈ ( ( mCN ‘ 𝑇 ) ∪ ( mVR ‘ 𝑇 ) ) ↦ if ( 𝑣 ∈ ( mVR ‘ 𝑇 ) , ( 𝑓 ‘ 𝑣 ) , ⟨“ 𝑣 ”⟩ ) ) ∘ 𝑋 ) ) ) |
| 68 |
25 61 15 67
|
syl3anc |
⊢ ( ( 𝑓 ∈ ( 𝑅 ↑m ( mVR ‘ 𝑇 ) ) ∧ ( 𝑋 ∈ 𝑅 ∧ 𝑌 ∈ 𝑅 ) ) → ( ( 𝑆 ‘ 𝑓 ) ‘ 𝑋 ) = ( ( freeMnd ‘ ( ( mCN ‘ 𝑇 ) ∪ ( mVR ‘ 𝑇 ) ) ) Σg ( ( 𝑣 ∈ ( ( mCN ‘ 𝑇 ) ∪ ( mVR ‘ 𝑇 ) ) ↦ if ( 𝑣 ∈ ( mVR ‘ 𝑇 ) , ( 𝑓 ‘ 𝑣 ) , ⟨“ 𝑣 ”⟩ ) ) ∘ 𝑋 ) ) ) |
| 69 |
18 6 2 1 40
|
mrsubval |
⊢ ( ( 𝑓 : ( mVR ‘ 𝑇 ) ⟶ 𝑅 ∧ ( mVR ‘ 𝑇 ) ⊆ ( mVR ‘ 𝑇 ) ∧ 𝑌 ∈ 𝑅 ) → ( ( 𝑆 ‘ 𝑓 ) ‘ 𝑌 ) = ( ( freeMnd ‘ ( ( mCN ‘ 𝑇 ) ∪ ( mVR ‘ 𝑇 ) ) ) Σg ( ( 𝑣 ∈ ( ( mCN ‘ 𝑇 ) ∪ ( mVR ‘ 𝑇 ) ) ↦ if ( 𝑣 ∈ ( mVR ‘ 𝑇 ) , ( 𝑓 ‘ 𝑣 ) , ⟨“ 𝑣 ”⟩ ) ) ∘ 𝑌 ) ) ) |
| 70 |
25 61 22 69
|
syl3anc |
⊢ ( ( 𝑓 ∈ ( 𝑅 ↑m ( mVR ‘ 𝑇 ) ) ∧ ( 𝑋 ∈ 𝑅 ∧ 𝑌 ∈ 𝑅 ) ) → ( ( 𝑆 ‘ 𝑓 ) ‘ 𝑌 ) = ( ( freeMnd ‘ ( ( mCN ‘ 𝑇 ) ∪ ( mVR ‘ 𝑇 ) ) ) Σg ( ( 𝑣 ∈ ( ( mCN ‘ 𝑇 ) ∪ ( mVR ‘ 𝑇 ) ) ↦ if ( 𝑣 ∈ ( mVR ‘ 𝑇 ) , ( 𝑓 ‘ 𝑣 ) , ⟨“ 𝑣 ”⟩ ) ) ∘ 𝑌 ) ) ) |
| 71 |
68 70
|
oveq12d |
⊢ ( ( 𝑓 ∈ ( 𝑅 ↑m ( mVR ‘ 𝑇 ) ) ∧ ( 𝑋 ∈ 𝑅 ∧ 𝑌 ∈ 𝑅 ) ) → ( ( ( 𝑆 ‘ 𝑓 ) ‘ 𝑋 ) ++ ( ( 𝑆 ‘ 𝑓 ) ‘ 𝑌 ) ) = ( ( ( freeMnd ‘ ( ( mCN ‘ 𝑇 ) ∪ ( mVR ‘ 𝑇 ) ) ) Σg ( ( 𝑣 ∈ ( ( mCN ‘ 𝑇 ) ∪ ( mVR ‘ 𝑇 ) ) ↦ if ( 𝑣 ∈ ( mVR ‘ 𝑇 ) , ( 𝑓 ‘ 𝑣 ) , ⟨“ 𝑣 ”⟩ ) ) ∘ 𝑋 ) ) ++ ( ( freeMnd ‘ ( ( mCN ‘ 𝑇 ) ∪ ( mVR ‘ 𝑇 ) ) ) Σg ( ( 𝑣 ∈ ( ( mCN ‘ 𝑇 ) ∪ ( mVR ‘ 𝑇 ) ) ↦ if ( 𝑣 ∈ ( mVR ‘ 𝑇 ) , ( 𝑓 ‘ 𝑣 ) , ⟨“ 𝑣 ”⟩ ) ) ∘ 𝑌 ) ) ) ) |
| 72 |
60 66 71
|
3eqtr4d |
⊢ ( ( 𝑓 ∈ ( 𝑅 ↑m ( mVR ‘ 𝑇 ) ) ∧ ( 𝑋 ∈ 𝑅 ∧ 𝑌 ∈ 𝑅 ) ) → ( ( 𝑆 ‘ 𝑓 ) ‘ ( 𝑋 ++ 𝑌 ) ) = ( ( ( 𝑆 ‘ 𝑓 ) ‘ 𝑋 ) ++ ( ( 𝑆 ‘ 𝑓 ) ‘ 𝑌 ) ) ) |
| 73 |
|
fveq1 |
⊢ ( ( 𝑆 ‘ 𝑓 ) = 𝐹 → ( ( 𝑆 ‘ 𝑓 ) ‘ ( 𝑋 ++ 𝑌 ) ) = ( 𝐹 ‘ ( 𝑋 ++ 𝑌 ) ) ) |
| 74 |
|
fveq1 |
⊢ ( ( 𝑆 ‘ 𝑓 ) = 𝐹 → ( ( 𝑆 ‘ 𝑓 ) ‘ 𝑋 ) = ( 𝐹 ‘ 𝑋 ) ) |
| 75 |
|
fveq1 |
⊢ ( ( 𝑆 ‘ 𝑓 ) = 𝐹 → ( ( 𝑆 ‘ 𝑓 ) ‘ 𝑌 ) = ( 𝐹 ‘ 𝑌 ) ) |
| 76 |
74 75
|
oveq12d |
⊢ ( ( 𝑆 ‘ 𝑓 ) = 𝐹 → ( ( ( 𝑆 ‘ 𝑓 ) ‘ 𝑋 ) ++ ( ( 𝑆 ‘ 𝑓 ) ‘ 𝑌 ) ) = ( ( 𝐹 ‘ 𝑋 ) ++ ( 𝐹 ‘ 𝑌 ) ) ) |
| 77 |
73 76
|
eqeq12d |
⊢ ( ( 𝑆 ‘ 𝑓 ) = 𝐹 → ( ( ( 𝑆 ‘ 𝑓 ) ‘ ( 𝑋 ++ 𝑌 ) ) = ( ( ( 𝑆 ‘ 𝑓 ) ‘ 𝑋 ) ++ ( ( 𝑆 ‘ 𝑓 ) ‘ 𝑌 ) ) ↔ ( 𝐹 ‘ ( 𝑋 ++ 𝑌 ) ) = ( ( 𝐹 ‘ 𝑋 ) ++ ( 𝐹 ‘ 𝑌 ) ) ) ) |
| 78 |
72 77
|
syl5ibcom |
⊢ ( ( 𝑓 ∈ ( 𝑅 ↑m ( mVR ‘ 𝑇 ) ) ∧ ( 𝑋 ∈ 𝑅 ∧ 𝑌 ∈ 𝑅 ) ) → ( ( 𝑆 ‘ 𝑓 ) = 𝐹 → ( 𝐹 ‘ ( 𝑋 ++ 𝑌 ) ) = ( ( 𝐹 ‘ 𝑋 ) ++ ( 𝐹 ‘ 𝑌 ) ) ) ) |
| 79 |
78
|
ex |
⊢ ( 𝑓 ∈ ( 𝑅 ↑m ( mVR ‘ 𝑇 ) ) → ( ( 𝑋 ∈ 𝑅 ∧ 𝑌 ∈ 𝑅 ) → ( ( 𝑆 ‘ 𝑓 ) = 𝐹 → ( 𝐹 ‘ ( 𝑋 ++ 𝑌 ) ) = ( ( 𝐹 ‘ 𝑋 ) ++ ( 𝐹 ‘ 𝑌 ) ) ) ) ) |
| 80 |
79
|
com23 |
⊢ ( 𝑓 ∈ ( 𝑅 ↑m ( mVR ‘ 𝑇 ) ) → ( ( 𝑆 ‘ 𝑓 ) = 𝐹 → ( ( 𝑋 ∈ 𝑅 ∧ 𝑌 ∈ 𝑅 ) → ( 𝐹 ‘ ( 𝑋 ++ 𝑌 ) ) = ( ( 𝐹 ‘ 𝑋 ) ++ ( 𝐹 ‘ 𝑌 ) ) ) ) ) |
| 81 |
80
|
rexlimiv |
⊢ ( ∃ 𝑓 ∈ ( 𝑅 ↑m ( mVR ‘ 𝑇 ) ) ( 𝑆 ‘ 𝑓 ) = 𝐹 → ( ( 𝑋 ∈ 𝑅 ∧ 𝑌 ∈ 𝑅 ) → ( 𝐹 ‘ ( 𝑋 ++ 𝑌 ) ) = ( ( 𝐹 ‘ 𝑋 ) ++ ( 𝐹 ‘ 𝑌 ) ) ) ) |
| 82 |
14 81
|
syl |
⊢ ( 𝐹 ∈ ran 𝑆 → ( ( 𝑋 ∈ 𝑅 ∧ 𝑌 ∈ 𝑅 ) → ( 𝐹 ‘ ( 𝑋 ++ 𝑌 ) ) = ( ( 𝐹 ‘ 𝑋 ) ++ ( 𝐹 ‘ 𝑌 ) ) ) ) |
| 83 |
82
|
3impib |
⊢ ( ( 𝐹 ∈ ran 𝑆 ∧ 𝑋 ∈ 𝑅 ∧ 𝑌 ∈ 𝑅 ) → ( 𝐹 ‘ ( 𝑋 ++ 𝑌 ) ) = ( ( 𝐹 ‘ 𝑋 ) ++ ( 𝐹 ‘ 𝑌 ) ) ) |