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 ”⟩ = if X A F 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 ”⟩ Word C 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 = Word C V
16 14 15 syl F : A R A V X C V R = Word C 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 V v C V if v A F v ⟨“ v ”⟩ ⟨“ X ”⟩
20 17 19 syld3an3 F : A R A V X C V S F ⟨“ X ”⟩ = freeMnd C V v C V if v A F v ⟨“ v ”⟩ ⟨“ X ”⟩
21 simpl1 F : A R A V X C V v C V F : A R
22 21 ffvelrnda 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 = Word C V
24 22 23 eleqtrd F : A R A V X C V v C V v A F v Word C 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 ”⟩ Word C V
27 24 26 ifclda F : A R A V X C V v C V if v A F v ⟨“ v ”⟩ Word C V
28 27 fmpttd F : A R A V X C V v C V if v A F v ⟨“ v ”⟩ : C V Word C V
29 s1co X C V v C V if v A F v ⟨“ v ”⟩ : C V Word C V v C V if v A F v ⟨“ v ”⟩ ⟨“ X ”⟩ = ⟨“ v C V if v A F v ⟨“ v ”⟩ X ”⟩
30 5 28 29 syl2anc F : A R A V X C V v C V if v A F v ⟨“ v ”⟩ ⟨“ X ”⟩ = ⟨“ v C V if v A F 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 if v A F v ⟨“ v ”⟩ = if X A F X ⟨“ X ”⟩
35 eqid v C V if v A F v ⟨“ v ”⟩ = v C V if v A F v ⟨“ v ”⟩
36 fvex F X V
37 s1cli ⟨“ X ”⟩ Word V
38 37 elexi ⟨“ X ”⟩ V
39 36 38 ifex if X A F X ⟨“ X ”⟩ V
40 34 35 39 fvmpt X C V v C V if v A F v ⟨“ v ”⟩ X = if X A F X ⟨“ X ”⟩
41 40 3ad2ant3 F : A R A V X C V v C V if v A F v ⟨“ v ”⟩ X = if X A F X ⟨“ X ”⟩
42 41 s1eqd F : A R A V X C V ⟨“ v C V if v A F v ⟨“ v ”⟩ X ”⟩ = ⟨“ if X A F X ⟨“ X ”⟩ ”⟩
43 30 42 eqtrd F : A R A V X C V v C V if v A F v ⟨“ v ”⟩ ⟨“ X ”⟩ = ⟨“ if X A F X ⟨“ X ”⟩ ”⟩
44 43 oveq2d F : A R A V X C V freeMnd C V v C V if v A F v ⟨“ v ”⟩ ⟨“ X ”⟩ = freeMnd C V ⟨“ if X A F X ⟨“ X ”⟩ ”⟩
45 28 5 ffvelrnd F : A R A V X C V v C V if v A F v ⟨“ v ”⟩ X Word C V
46 41 45 eqeltrrd F : A R A V X C V if X A F X ⟨“ X ”⟩ Word C V
47 1 fvexi C V
48 2 fvexi V V
49 47 48 unex C V V
50 eqid Base freeMnd C V = Base freeMnd C V
51 18 50 frmdbas C V V Base freeMnd C V = Word C V
52 49 51 ax-mp Base freeMnd C V = Word C V
53 52 eqcomi Word C V = Base freeMnd C V
54 53 gsumws1 if X A F X ⟨“ X ”⟩ Word C V freeMnd C V ⟨“ if X A F X ⟨“ X ”⟩ ”⟩ = if X A F X ⟨“ X ”⟩
55 46 54 syl F : A R A V X C V freeMnd C V ⟨“ if X A F X ⟨“ X ”⟩ ”⟩ = if X A F X ⟨“ X ”⟩
56 20 44 55 3eqtrd F : A R A V X C V S F ⟨“ X ”⟩ = if X A F X ⟨“ X ”⟩