Metamath Proof Explorer

Theorem mrsubcv

Description: The value of a substituted singleton. (Contributed by Mario Carneiro, 18-Jul-2016)

Ref Expression
Hypotheses mrsubffval.c ⊢C=mCN⁡T
mrsubffval.v ⊢V=mVR⁡T
mrsubffval.r ⊢R=mREx⁡T
mrsubffval.s ⊢S=mRSubst⁡T
Assertion mrsubcv ⊢F:A⟶R∧A⊆V∧X∈C∪V→S⁡F⁡⟨“X”⟩=ifX∈AF⁡X⟨“X”⟩

Proof

Step Hyp Ref Expression
1 mrsubffval.c ⊢C=mCN⁡T
2 mrsubffval.v ⊢V=mVR⁡T
3 mrsubffval.r ⊢R=mREx⁡T
4 mrsubffval.s ⊢S=mRSubst⁡T
5 simp3 ⊢F:A⟶R∧A⊆V∧X∈C∪V→X∈C∪V
6 5 s1cld ⊢F:A⟶R∧A⊆V∧X∈C∪V→⟨“X”⟩∈WordC∪V
7 elun ⊢X∈C∪V↔X∈C∨X∈V
8 elfvex ⊢X∈mCN⁡T→T∈V
9 8 1 eleq2s ⊢X∈C→T∈V
10 elfvex ⊢X∈mVR⁡T→T∈V
11 10 2 eleq2s ⊢X∈V→T∈V
12 9 11 jaoi ⊢X∈C∨X∈V→T∈V
13 7 12 sylbi ⊢X∈C∪V→T∈V
14 13 3ad2ant3 ⊢F:A⟶R∧A⊆V∧X∈C∪V→T∈V
15 1 2 3 mrexval ⊢T∈V→R=WordC∪V
16 14 15 syl ⊢F:A⟶R∧A⊆V∧X∈C∪V→R=WordC∪V
17 6 16 eleqtrrd ⊢F:A⟶R∧A⊆V∧X∈C∪V→⟨“X”⟩∈R
18 eqid ⊢freeMnd⁡C∪V=freeMnd⁡C∪V
19 1 2 3 4 18 mrsubval ⊢F:A⟶R∧A⊆V∧⟨“X”⟩∈R→S⁡F⁡⟨“X”⟩=∑freeMnd⁡C∪Vv∈C∪V⟼ifv∈AF⁡v⟨“v”⟩∘⟨“X”⟩
20 17 19 syld3an3 ⊢F:A⟶R∧A⊆V∧X∈C∪V→S⁡F⁡⟨“X”⟩=∑freeMnd⁡C∪Vv∈C∪V⟼ifv∈AF⁡v⟨“v”⟩∘⟨“X”⟩
21 simpl1 ⊢F:A⟶R∧A⊆V∧X∈C∪V∧v∈C∪V→F:A⟶R
22 21 ffvelcdmda ⊢F:A⟶R∧A⊆V∧X∈C∪V∧v∈C∪V∧v∈A→F⁡v∈R
23 16 ad2antrr ⊢F:A⟶R∧A⊆V∧X∈C∪V∧v∈C∪V∧v∈A→R=WordC∪V
24 22 23 eleqtrd ⊢F:A⟶R∧A⊆V∧X∈C∪V∧v∈C∪V∧v∈A→F⁡v∈WordC∪V
25 simplr ⊢F:A⟶R∧A⊆V∧X∈C∪V∧v∈C∪V∧¬v∈A→v∈C∪V
26 25 s1cld ⊢F:A⟶R∧A⊆V∧X∈C∪V∧v∈C∪V∧¬v∈A→⟨“v”⟩∈WordC∪V
27 24 26 ifclda ⊢F:A⟶R∧A⊆V∧X∈C∪V∧v∈C∪V→ifv∈AF⁡v⟨“v”⟩∈WordC∪V
28 27 fmpttd ⊢F:A⟶R∧A⊆V∧X∈C∪V→v∈C∪V⟼ifv∈AF⁡v⟨“v”⟩:C∪V⟶WordC∪V
29 s1co ⊢X∈C∪V∧v∈C∪V⟼ifv∈AF⁡v⟨“v”⟩:C∪V⟶WordC∪V→v∈C∪V⟼ifv∈AF⁡v⟨“v”⟩∘⟨“X”⟩=⟨“v∈C∪V⟼ifv∈AF⁡v⟨“v”⟩⁡X”⟩
30 5 28 29 syl2anc ⊢F:A⟶R∧A⊆V∧X∈C∪V→v∈C∪V⟼ifv∈AF⁡v⟨“v”⟩∘⟨“X”⟩=⟨“v∈C∪V⟼ifv∈AF⁡v⟨“v”⟩⁡X”⟩
31 eleq1 ⊢v=X→v∈A↔X∈A
32 fveq2 ⊢v=X→F⁡v=F⁡X
33 s1eq ⊢v=X→⟨“v”⟩=⟨“X”⟩
34 31 32 33 ifbieq12d ⊢v=X→ifv∈AF⁡v⟨“v”⟩=ifX∈AF⁡X⟨“X”⟩
35 eqid ⊢v∈C∪V⟼ifv∈AF⁡v⟨“v”⟩=v∈C∪V⟼ifv∈AF⁡v⟨“v”⟩
36 fvex ⊢F⁡X∈V
37 s1cli ⊢⟨“X”⟩∈WordV
38 37 elexi ⊢⟨“X”⟩∈V
39 36 38 ifex ⊢ifX∈AF⁡X⟨“X”⟩∈V
40 34 35 39 fvmpt ⊢X∈C∪V→v∈C∪V⟼ifv∈AF⁡v⟨“v”⟩⁡X=ifX∈AF⁡X⟨“X”⟩
41 40 3ad2ant3 ⊢F:A⟶R∧A⊆V∧X∈C∪V→v∈C∪V⟼ifv∈AF⁡v⟨“v”⟩⁡X=ifX∈AF⁡X⟨“X”⟩
42 41 s1eqd ⊢F:A⟶R∧A⊆V∧X∈C∪V→⟨“v∈C∪V⟼ifv∈AF⁡v⟨“v”⟩⁡X”⟩=⟨“ifX∈AF⁡X⟨“X”⟩”⟩
43 30 42 eqtrd ⊢F:A⟶R∧A⊆V∧X∈C∪V→v∈C∪V⟼ifv∈AF⁡v⟨“v”⟩∘⟨“X”⟩=⟨“ifX∈AF⁡X⟨“X”⟩”⟩
44 43 oveq2d ⊢F:A⟶R∧A⊆V∧X∈C∪V→∑freeMnd⁡C∪Vv∈C∪V⟼ifv∈AF⁡v⟨“v”⟩∘⟨“X”⟩=∑freeMnd⁡C∪V⟨“ifX∈AF⁡X⟨“X”⟩”⟩
45 28 5 ffvelcdmd ⊢F:A⟶R∧A⊆V∧X∈C∪V→v∈C∪V⟼ifv∈AF⁡v⟨“v”⟩⁡X∈WordC∪V
46 41 45 eqeltrrd ⊢F:A⟶R∧A⊆V∧X∈C∪V→ifX∈AF⁡X⟨“X”⟩∈WordC∪V
47 1 fvexi ⊢C∈V
48 2 fvexi ⊢V∈V
49 47 48 unex ⊢C∪V∈V
50 eqid ⊢BasefreeMnd⁡C∪V=BasefreeMnd⁡C∪V
51 18 50 frmdbas ⊢C∪V∈V→BasefreeMnd⁡C∪V=WordC∪V
52 49 51 ax-mp ⊢BasefreeMnd⁡C∪V=WordC∪V
53 52 eqcomi ⊢WordC∪V=BasefreeMnd⁡C∪V
54 53 gsumws1 ⊢ifX∈AF⁡X⟨“X”⟩∈WordC∪V→∑freeMnd⁡C∪V⟨“ifX∈AF⁡X⟨“X”⟩”⟩=ifX∈AF⁡X⟨“X”⟩
55 46 54 syl ⊢F:A⟶R∧A⊆V∧X∈C∪V→∑freeMnd⁡C∪V⟨“ifX∈AF⁡X⟨“X”⟩”⟩=ifX∈AF⁡X⟨“X”⟩
56 20 44 55 3eqtrd ⊢F:A⟶R∧A⊆V∧X∈C∪V→S⁡F⁡⟨“X”⟩=ifX∈AF⁡X⟨“X”⟩