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

Theorem mrsubfval 34330
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 34329 . . . . 5 (𝑇 ∈ V → 𝑆 = (𝑓 ∈ (𝑅pm 𝑉) ↦ (𝑒𝑅 ↦ (𝐺 Σg ((𝑣 ∈ (𝐶𝑉) ↦ if(𝑣 ∈ dom 𝑓, (𝑓𝑣), ⟨“𝑣”⟩)) ∘ 𝑒)))))
76adantr 481 . . . 4 ((𝑇 ∈ V ∧ (𝐹:𝐴𝑅𝐴𝑉)) → 𝑆 = (𝑓 ∈ (𝑅pm 𝑉) ↦ (𝑒𝑅 ↦ (𝐺 Σg ((𝑣 ∈ (𝐶𝑉) ↦ if(𝑣 ∈ dom 𝑓, (𝑓𝑣), ⟨“𝑣”⟩)) ∘ 𝑒)))))
8 dmeq 5895 . . . . . . . . . . 11 (𝑓 = 𝐹 → dom 𝑓 = dom 𝐹)
9 fdm 6713 . . . . . . . . . . . 12 (𝐹:𝐴𝑅 → dom 𝐹 = 𝐴)
109ad2antrl 726 . . . . . . . . . . 11 ((𝑇 ∈ V ∧ (𝐹:𝐴𝑅𝐴𝑉)) → dom 𝐹 = 𝐴)
118, 10sylan9eqr 2793 . . . . . . . . . 10 (((𝑇 ∈ V ∧ (𝐹:𝐴𝑅𝐴𝑉)) ∧ 𝑓 = 𝐹) → dom 𝑓 = 𝐴)
1211eleq2d 2818 . . . . . . . . 9 (((𝑇 ∈ V ∧ (𝐹:𝐴𝑅𝐴𝑉)) ∧ 𝑓 = 𝐹) → (𝑣 ∈ dom 𝑓𝑣𝐴))
13 simpr 485 . . . . . . . . . 10 (((𝑇 ∈ V ∧ (𝐹:𝐴𝑅𝐴𝑉)) ∧ 𝑓 = 𝐹) → 𝑓 = 𝐹)
1413fveq1d 6880 . . . . . . . . 9 (((𝑇 ∈ V ∧ (𝐹:𝐴𝑅𝐴𝑉)) ∧ 𝑓 = 𝐹) → (𝑓𝑣) = (𝐹𝑣))
1512, 14ifbieq1d 4546 . . . . . . . 8 (((𝑇 ∈ V ∧ (𝐹:𝐴𝑅𝐴𝑉)) ∧ 𝑓 = 𝐹) → if(𝑣 ∈ dom 𝑓, (𝑓𝑣), ⟨“𝑣”⟩) = if(𝑣𝐴, (𝐹𝑣), ⟨“𝑣”⟩))
1615mpteq2dv 5243 . . . . . . 7 (((𝑇 ∈ V ∧ (𝐹:𝐴𝑅𝐴𝑉)) ∧ 𝑓 = 𝐹) → (𝑣 ∈ (𝐶𝑉) ↦ if(𝑣 ∈ dom 𝑓, (𝑓𝑣), ⟨“𝑣”⟩)) = (𝑣 ∈ (𝐶𝑉) ↦ if(𝑣𝐴, (𝐹𝑣), ⟨“𝑣”⟩)))
1716coeq1d 5853 . . . . . 6 (((𝑇 ∈ V ∧ (𝐹:𝐴𝑅𝐴𝑉)) ∧ 𝑓 = 𝐹) → ((𝑣 ∈ (𝐶𝑉) ↦ if(𝑣 ∈ dom 𝑓, (𝑓𝑣), ⟨“𝑣”⟩)) ∘ 𝑒) = ((𝑣 ∈ (𝐶𝑉) ↦ if(𝑣𝐴, (𝐹𝑣), ⟨“𝑣”⟩)) ∘ 𝑒))
1817oveq2d 7409 . . . . 5 (((𝑇 ∈ V ∧ (𝐹:𝐴𝑅𝐴𝑉)) ∧ 𝑓 = 𝐹) → (𝐺 Σg ((𝑣 ∈ (𝐶𝑉) ↦ if(𝑣 ∈ dom 𝑓, (𝑓𝑣), ⟨“𝑣”⟩)) ∘ 𝑒)) = (𝐺 Σg ((𝑣 ∈ (𝐶𝑉) ↦ if(𝑣𝐴, (𝐹𝑣), ⟨“𝑣”⟩)) ∘ 𝑒)))
1918mpteq2dv 5243 . . . 4 (((𝑇 ∈ V ∧ (𝐹:𝐴𝑅𝐴𝑉)) ∧ 𝑓 = 𝐹) → (𝑒𝑅 ↦ (𝐺 Σg ((𝑣 ∈ (𝐶𝑉) ↦ if(𝑣 ∈ dom 𝑓, (𝑓𝑣), ⟨“𝑣”⟩)) ∘ 𝑒))) = (𝑒𝑅 ↦ (𝐺 Σg ((𝑣 ∈ (𝐶𝑉) ↦ if(𝑣𝐴, (𝐹𝑣), ⟨“𝑣”⟩)) ∘ 𝑒))))
203fvexi 6892 . . . . . 6 𝑅 ∈ V
2120a1i 11 . . . . 5 ((𝑇 ∈ V ∧ (𝐹:𝐴𝑅𝐴𝑉)) → 𝑅 ∈ V)
222fvexi 6892 . . . . . 6 𝑉 ∈ V
2322a1i 11 . . . . 5 ((𝑇 ∈ V ∧ (𝐹:𝐴𝑅𝐴𝑉)) → 𝑉 ∈ V)
24 simprl 769 . . . . 5 ((𝑇 ∈ V ∧ (𝐹:𝐴𝑅𝐴𝑉)) → 𝐹:𝐴𝑅)
25 simprr 771 . . . . 5 ((𝑇 ∈ V ∧ (𝐹:𝐴𝑅𝐴𝑉)) → 𝐴𝑉)
26 elpm2r 8822 . . . . 5 (((𝑅 ∈ V ∧ 𝑉 ∈ V) ∧ (𝐹:𝐴𝑅𝐴𝑉)) → 𝐹 ∈ (𝑅pm 𝑉))
2721, 23, 24, 25, 26syl22anc 837 . . . 4 ((𝑇 ∈ V ∧ (𝐹:𝐴𝑅𝐴𝑉)) → 𝐹 ∈ (𝑅pm 𝑉))
2820mptex 7209 . . . . 5 (𝑒𝑅 ↦ (𝐺 Σg ((𝑣 ∈ (𝐶𝑉) ↦ if(𝑣𝐴, (𝐹𝑣), ⟨“𝑣”⟩)) ∘ 𝑒))) ∈ V
2928a1i 11 . . . 4 ((𝑇 ∈ V ∧ (𝐹:𝐴𝑅𝐴𝑉)) → (𝑒𝑅 ↦ (𝐺 Σg ((𝑣 ∈ (𝐶𝑉) ↦ if(𝑣𝐴, (𝐹𝑣), ⟨“𝑣”⟩)) ∘ 𝑒))) ∈ V)
307, 19, 27, 29fvmptd 6991 . . 3 ((𝑇 ∈ V ∧ (𝐹:𝐴𝑅𝐴𝑉)) → (𝑆𝐹) = (𝑒𝑅 ↦ (𝐺 Σg ((𝑣 ∈ (𝐶𝑉) ↦ if(𝑣𝐴, (𝐹𝑣), ⟨“𝑣”⟩)) ∘ 𝑒))))
3130ex 413 . 2 (𝑇 ∈ V → ((𝐹:𝐴𝑅𝐴𝑉) → (𝑆𝐹) = (𝑒𝑅 ↦ (𝐺 Σg ((𝑣 ∈ (𝐶𝑉) ↦ if(𝑣𝐴, (𝐹𝑣), ⟨“𝑣”⟩)) ∘ 𝑒)))))
32 0fv 6922 . . . 4 (∅‘𝐹) = ∅
33 fvprc 6870 . . . . . 6 𝑇 ∈ V → (mRSubst‘𝑇) = ∅)
344, 33eqtrid 2783 . . . . 5 𝑇 ∈ V → 𝑆 = ∅)
3534fveq1d 6880 . . . 4 𝑇 ∈ V → (𝑆𝐹) = (∅‘𝐹))
36 fvprc 6870 . . . . . . 7 𝑇 ∈ V → (mREx‘𝑇) = ∅)
373, 36eqtrid 2783 . . . . . 6 𝑇 ∈ V → 𝑅 = ∅)
3837mpteq1d 5236 . . . . 5 𝑇 ∈ V → (𝑒𝑅 ↦ (𝐺 Σg ((𝑣 ∈ (𝐶𝑉) ↦ if(𝑣𝐴, (𝐹𝑣), ⟨“𝑣”⟩)) ∘ 𝑒))) = (𝑒 ∈ ∅ ↦ (𝐺 Σg ((𝑣 ∈ (𝐶𝑉) ↦ if(𝑣𝐴, (𝐹𝑣), ⟨“𝑣”⟩)) ∘ 𝑒))))
39 mpt0 6679 . . . . 5 (𝑒 ∈ ∅ ↦ (𝐺 Σg ((𝑣 ∈ (𝐶𝑉) ↦ if(𝑣𝐴, (𝐹𝑣), ⟨“𝑣”⟩)) ∘ 𝑒))) = ∅
4038, 39eqtrdi 2787 . . . 4 𝑇 ∈ V → (𝑒𝑅 ↦ (𝐺 Σg ((𝑣 ∈ (𝐶𝑉) ↦ if(𝑣𝐴, (𝐹𝑣), ⟨“𝑣”⟩)) ∘ 𝑒))) = ∅)
4132, 35, 403eqtr4a 2797 . . 3 𝑇 ∈ V → (𝑆𝐹) = (𝑒𝑅 ↦ (𝐺 Σg ((𝑣 ∈ (𝐶𝑉) ↦ if(𝑣𝐴, (𝐹𝑣), ⟨“𝑣”⟩)) ∘ 𝑒))))
4241a1d 25 . 2 𝑇 ∈ V → ((𝐹:𝐴𝑅𝐴𝑉) → (𝑆𝐹) = (𝑒𝑅 ↦ (𝐺 Σg ((𝑣 ∈ (𝐶𝑉) ↦ if(𝑣𝐴, (𝐹𝑣), ⟨“𝑣”⟩)) ∘ 𝑒)))))
4331, 42pm2.61i 182 1 ((𝐹:𝐴𝑅𝐴𝑉) → (𝑆𝐹) = (𝑒𝑅 ↦ (𝐺 Σg ((𝑣 ∈ (𝐶𝑉) ↦ if(𝑣𝐴, (𝐹𝑣), ⟨“𝑣”⟩)) ∘ 𝑒))))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wa 396   = wceq 1541  wcel 2106  Vcvv 3473  cun 3942  wss 3944  c0 4318  ifcif 4522  cmpt 5224  dom cdm 5669  ccom 5673  wf 6528  cfv 6532  (class class class)co 7393  pm cpm 8804  ⟨“cs1 14527   Σg cgsu 17368  freeMndcfrmd 18703  mCNcmcn 34282  mVRcmvar 34283  mRExcmrex 34288  mRSubstcmrsub 34292
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2702  ax-rep 5278  ax-sep 5292  ax-nul 5299  ax-pow 5356  ax-pr 5420  ax-un 7708
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2533  df-eu 2562  df-clab 2709  df-cleq 2723  df-clel 2809  df-nfc 2884  df-ne 2940  df-ral 3061  df-rex 3070  df-reu 3376  df-rab 3432  df-v 3475  df-sbc 3774  df-csb 3890  df-dif 3947  df-un 3949  df-in 3951  df-ss 3961  df-nul 4319  df-if 4523  df-pw 4598  df-sn 4623  df-pr 4625  df-op 4629  df-uni 4902  df-iun 4992  df-br 5142  df-opab 5204  df-mpt 5225  df-id 5567  df-xp 5675  df-rel 5676  df-cnv 5677  df-co 5678  df-dm 5679  df-rn 5680  df-res 5681  df-ima 5682  df-iota 6484  df-fun 6534  df-fn 6535  df-f 6536  df-f1 6537  df-fo 6538  df-f1o 6539  df-fv 6540  df-ov 7396  df-oprab 7397  df-mpo 7398  df-pm 8806  df-mrsub 34312
This theorem is referenced by:  mrsubval  34331  mrsubrn  34335  elmrsubrn  34342
  Copyright terms: Public domain W3C validator