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

Theorem mrsubfval 31166
 Description: The substitution of some variables for expressions in a raw expression. (Contributed by Mario Carneiro, 18-Jul-2016.)
Hypotheses
Ref Expression
mrsubffval.c 𝐶 = (mCN‘𝑇)
mrsubffval.v 𝑉 = (mVR‘𝑇)
mrsubffval.r 𝑅 = (mREx‘𝑇)
mrsubffval.s 𝑆 = (mRSubst‘𝑇)
mrsubffval.g 𝐺 = (freeMnd‘(𝐶𝑉))
Assertion
Ref Expression
mrsubfval ((𝐹:𝐴𝑅𝐴𝑉) → (𝑆𝐹) = (𝑒𝑅 ↦ (𝐺 Σg ((𝑣 ∈ (𝐶𝑉) ↦ if(𝑣𝐴, (𝐹𝑣), ⟨“𝑣”⟩)) ∘ 𝑒))))
Distinct variable groups:   𝑣,𝑒,𝐴   𝐶,𝑒,𝑣   𝑒,𝐹,𝑣   𝑅,𝑒,𝑣   𝑒,𝐺   𝑇,𝑒,𝑣   𝑒,𝑉,𝑣
Allowed substitution hints:   𝑆(𝑣,𝑒)   𝐺(𝑣)

Proof of Theorem mrsubfval
Dummy variable 𝑓 is distinct from all other variables.
StepHypRef Expression
1 mrsubffval.c . . . . . 6 𝐶 = (mCN‘𝑇)
2 mrsubffval.v . . . . . 6 𝑉 = (mVR‘𝑇)
3 mrsubffval.r . . . . . 6 𝑅 = (mREx‘𝑇)
4 mrsubffval.s . . . . . 6 𝑆 = (mRSubst‘𝑇)
5 mrsubffval.g . . . . . 6 𝐺 = (freeMnd‘(𝐶𝑉))
61, 2, 3, 4, 5mrsubffval 31165 . . . . 5 (𝑇 ∈ V → 𝑆 = (𝑓 ∈ (𝑅pm 𝑉) ↦ (𝑒𝑅 ↦ (𝐺 Σg ((𝑣 ∈ (𝐶𝑉) ↦ if(𝑣 ∈ dom 𝑓, (𝑓𝑣), ⟨“𝑣”⟩)) ∘ 𝑒)))))
76adantr 481 . . . 4 ((𝑇 ∈ V ∧ (𝐹:𝐴𝑅𝐴𝑉)) → 𝑆 = (𝑓 ∈ (𝑅pm 𝑉) ↦ (𝑒𝑅 ↦ (𝐺 Σg ((𝑣 ∈ (𝐶𝑉) ↦ if(𝑣 ∈ dom 𝑓, (𝑓𝑣), ⟨“𝑣”⟩)) ∘ 𝑒)))))
8 dmeq 5294 . . . . . . . . . . 11 (𝑓 = 𝐹 → dom 𝑓 = dom 𝐹)
9 fdm 6018 . . . . . . . . . . . 12 (𝐹:𝐴𝑅 → dom 𝐹 = 𝐴)
109ad2antrl 763 . . . . . . . . . . 11 ((𝑇 ∈ V ∧ (𝐹:𝐴𝑅𝐴𝑉)) → dom 𝐹 = 𝐴)
118, 10sylan9eqr 2677 . . . . . . . . . 10 (((𝑇 ∈ V ∧ (𝐹:𝐴𝑅𝐴𝑉)) ∧ 𝑓 = 𝐹) → dom 𝑓 = 𝐴)
1211eleq2d 2684 . . . . . . . . 9 (((𝑇 ∈ V ∧ (𝐹:𝐴𝑅𝐴𝑉)) ∧ 𝑓 = 𝐹) → (𝑣 ∈ dom 𝑓𝑣𝐴))
13 simpr 477 . . . . . . . . . 10 (((𝑇 ∈ V ∧ (𝐹:𝐴𝑅𝐴𝑉)) ∧ 𝑓 = 𝐹) → 𝑓 = 𝐹)
1413fveq1d 6160 . . . . . . . . 9 (((𝑇 ∈ V ∧ (𝐹:𝐴𝑅𝐴𝑉)) ∧ 𝑓 = 𝐹) → (𝑓𝑣) = (𝐹𝑣))
1512, 14ifbieq1d 4087 . . . . . . . 8 (((𝑇 ∈ V ∧ (𝐹:𝐴𝑅𝐴𝑉)) ∧ 𝑓 = 𝐹) → if(𝑣 ∈ dom 𝑓, (𝑓𝑣), ⟨“𝑣”⟩) = if(𝑣𝐴, (𝐹𝑣), ⟨“𝑣”⟩))
1615mpteq2dv 4715 . . . . . . 7 (((𝑇 ∈ V ∧ (𝐹:𝐴𝑅𝐴𝑉)) ∧ 𝑓 = 𝐹) → (𝑣 ∈ (𝐶𝑉) ↦ if(𝑣 ∈ dom 𝑓, (𝑓𝑣), ⟨“𝑣”⟩)) = (𝑣 ∈ (𝐶𝑉) ↦ if(𝑣𝐴, (𝐹𝑣), ⟨“𝑣”⟩)))
1716coeq1d 5253 . . . . . 6 (((𝑇 ∈ V ∧ (𝐹:𝐴𝑅𝐴𝑉)) ∧ 𝑓 = 𝐹) → ((𝑣 ∈ (𝐶𝑉) ↦ if(𝑣 ∈ dom 𝑓, (𝑓𝑣), ⟨“𝑣”⟩)) ∘ 𝑒) = ((𝑣 ∈ (𝐶𝑉) ↦ if(𝑣𝐴, (𝐹𝑣), ⟨“𝑣”⟩)) ∘ 𝑒))
1817oveq2d 6631 . . . . 5 (((𝑇 ∈ V ∧ (𝐹:𝐴𝑅𝐴𝑉)) ∧ 𝑓 = 𝐹) → (𝐺 Σg ((𝑣 ∈ (𝐶𝑉) ↦ if(𝑣 ∈ dom 𝑓, (𝑓𝑣), ⟨“𝑣”⟩)) ∘ 𝑒)) = (𝐺 Σg ((𝑣 ∈ (𝐶𝑉) ↦ if(𝑣𝐴, (𝐹𝑣), ⟨“𝑣”⟩)) ∘ 𝑒)))
1918mpteq2dv 4715 . . . 4 (((𝑇 ∈ V ∧ (𝐹:𝐴𝑅𝐴𝑉)) ∧ 𝑓 = 𝐹) → (𝑒𝑅 ↦ (𝐺 Σg ((𝑣 ∈ (𝐶𝑉) ↦ if(𝑣 ∈ dom 𝑓, (𝑓𝑣), ⟨“𝑣”⟩)) ∘ 𝑒))) = (𝑒𝑅 ↦ (𝐺 Σg ((𝑣 ∈ (𝐶𝑉) ↦ if(𝑣𝐴, (𝐹𝑣), ⟨“𝑣”⟩)) ∘ 𝑒))))
20 fvex 6168 . . . . . . 7 (mREx‘𝑇) ∈ V
213, 20eqeltri 2694 . . . . . 6 𝑅 ∈ V
2221a1i 11 . . . . 5 ((𝑇 ∈ V ∧ (𝐹:𝐴𝑅𝐴𝑉)) → 𝑅 ∈ V)
23 fvex 6168 . . . . . . 7 (mVR‘𝑇) ∈ V
242, 23eqeltri 2694 . . . . . 6 𝑉 ∈ V
2524a1i 11 . . . . 5 ((𝑇 ∈ V ∧ (𝐹:𝐴𝑅𝐴𝑉)) → 𝑉 ∈ V)
26 simprl 793 . . . . 5 ((𝑇 ∈ V ∧ (𝐹:𝐴𝑅𝐴𝑉)) → 𝐹:𝐴𝑅)
27 simprr 795 . . . . 5 ((𝑇 ∈ V ∧ (𝐹:𝐴𝑅𝐴𝑉)) → 𝐴𝑉)
28 elpm2r 7835 . . . . 5 (((𝑅 ∈ V ∧ 𝑉 ∈ V) ∧ (𝐹:𝐴𝑅𝐴𝑉)) → 𝐹 ∈ (𝑅pm 𝑉))
2922, 25, 26, 27, 28syl22anc 1324 . . . 4 ((𝑇 ∈ V ∧ (𝐹:𝐴𝑅𝐴𝑉)) → 𝐹 ∈ (𝑅pm 𝑉))
3021mptex 6451 . . . . 5 (𝑒𝑅 ↦ (𝐺 Σg ((𝑣 ∈ (𝐶𝑉) ↦ if(𝑣𝐴, (𝐹𝑣), ⟨“𝑣”⟩)) ∘ 𝑒))) ∈ V
3130a1i 11 . . . 4 ((𝑇 ∈ V ∧ (𝐹:𝐴𝑅𝐴𝑉)) → (𝑒𝑅 ↦ (𝐺 Σg ((𝑣 ∈ (𝐶𝑉) ↦ if(𝑣𝐴, (𝐹𝑣), ⟨“𝑣”⟩)) ∘ 𝑒))) ∈ V)
327, 19, 29, 31fvmptd 6255 . . 3 ((𝑇 ∈ V ∧ (𝐹:𝐴𝑅𝐴𝑉)) → (𝑆𝐹) = (𝑒𝑅 ↦ (𝐺 Σg ((𝑣 ∈ (𝐶𝑉) ↦ if(𝑣𝐴, (𝐹𝑣), ⟨“𝑣”⟩)) ∘ 𝑒))))
3332ex 450 . 2 (𝑇 ∈ V → ((𝐹:𝐴𝑅𝐴𝑉) → (𝑆𝐹) = (𝑒𝑅 ↦ (𝐺 Σg ((𝑣 ∈ (𝐶𝑉) ↦ if(𝑣𝐴, (𝐹𝑣), ⟨“𝑣”⟩)) ∘ 𝑒)))))
34 0fv 6194 . . . 4 (∅‘𝐹) = ∅
35 fvprc 6152 . . . . . 6 𝑇 ∈ V → (mRSubst‘𝑇) = ∅)
364, 35syl5eq 2667 . . . . 5 𝑇 ∈ V → 𝑆 = ∅)
3736fveq1d 6160 . . . 4 𝑇 ∈ V → (𝑆𝐹) = (∅‘𝐹))
38 fvprc 6152 . . . . . . 7 𝑇 ∈ V → (mREx‘𝑇) = ∅)
393, 38syl5eq 2667 . . . . . 6 𝑇 ∈ V → 𝑅 = ∅)
4039mpteq1d 4708 . . . . 5 𝑇 ∈ V → (𝑒𝑅 ↦ (𝐺 Σg ((𝑣 ∈ (𝐶𝑉) ↦ if(𝑣𝐴, (𝐹𝑣), ⟨“𝑣”⟩)) ∘ 𝑒))) = (𝑒 ∈ ∅ ↦ (𝐺 Σg ((𝑣 ∈ (𝐶𝑉) ↦ if(𝑣𝐴, (𝐹𝑣), ⟨“𝑣”⟩)) ∘ 𝑒))))
41 mpt0 5988 . . . . 5 (𝑒 ∈ ∅ ↦ (𝐺 Σg ((𝑣 ∈ (𝐶𝑉) ↦ if(𝑣𝐴, (𝐹𝑣), ⟨“𝑣”⟩)) ∘ 𝑒))) = ∅
4240, 41syl6eq 2671 . . . 4 𝑇 ∈ V → (𝑒𝑅 ↦ (𝐺 Σg ((𝑣 ∈ (𝐶𝑉) ↦ if(𝑣𝐴, (𝐹𝑣), ⟨“𝑣”⟩)) ∘ 𝑒))) = ∅)
4334, 37, 423eqtr4a 2681 . . 3 𝑇 ∈ V → (𝑆𝐹) = (𝑒𝑅 ↦ (𝐺 Σg ((𝑣 ∈ (𝐶𝑉) ↦ if(𝑣𝐴, (𝐹𝑣), ⟨“𝑣”⟩)) ∘ 𝑒))))
4443a1d 25 . 2 𝑇 ∈ V → ((𝐹:𝐴𝑅𝐴𝑉) → (𝑆𝐹) = (𝑒𝑅 ↦ (𝐺 Σg ((𝑣 ∈ (𝐶𝑉) ↦ if(𝑣𝐴, (𝐹𝑣), ⟨“𝑣”⟩)) ∘ 𝑒)))))
4533, 44pm2.61i 176 1 ((𝐹:𝐴𝑅𝐴𝑉) → (𝑆𝐹) = (𝑒𝑅 ↦ (𝐺 Σg ((𝑣 ∈ (𝐶𝑉) ↦ if(𝑣𝐴, (𝐹𝑣), ⟨“𝑣”⟩)) ∘ 𝑒))))
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 384   = wceq 1480   ∈ wcel 1987  Vcvv 3190   ∪ cun 3558   ⊆ wss 3560  ∅c0 3897  ifcif 4064   ↦ cmpt 4683  dom cdm 5084   ∘ ccom 5088  ⟶wf 5853  ‘cfv 5857  (class class class)co 6615   ↑pm cpm 7818  ⟨“cs1 13249   Σg cgsu 16041  freeMndcfrmd 17324  mCNcmcn 31118  mVRcmvar 31119  mRExcmrex 31124  mRSubstcmrsub 31128 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-8 1989  ax-9 1996  ax-10 2016  ax-11 2031  ax-12 2044  ax-13 2245  ax-ext 2601  ax-rep 4741  ax-sep 4751  ax-nul 4759  ax-pow 4813  ax-pr 4877  ax-un 6914 This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3an 1038  df-tru 1483  df-ex 1702  df-nf 1707  df-sb 1878  df-eu 2473  df-mo 2474  df-clab 2608  df-cleq 2614  df-clel 2617  df-nfc 2750  df-ne 2791  df-ral 2913  df-rex 2914  df-reu 2915  df-rab 2917  df-v 3192  df-sbc 3423  df-csb 3520  df-dif 3563  df-un 3565  df-in 3567  df-ss 3574  df-nul 3898  df-if 4065  df-pw 4138  df-sn 4156  df-pr 4158  df-op 4162  df-uni 4410  df-iun 4494  df-br 4624  df-opab 4684  df-mpt 4685  df-id 4999  df-xp 5090  df-rel 5091  df-cnv 5092  df-co 5093  df-dm 5094  df-rn 5095  df-res 5096  df-ima 5097  df-iota 5820  df-fun 5859  df-fn 5860  df-f 5861  df-f1 5862  df-fo 5863  df-f1o 5864  df-fv 5865  df-ov 6618  df-oprab 6619  df-mpt2 6620  df-pm 7820  df-mrsub 31148 This theorem is referenced by:  mrsubval  31167  mrsubrn  31171  elmrsubrn  31178
 Copyright terms: Public domain W3C validator