Step | Hyp | Ref
| Expression |
1 | | simp3 1063 |
. . . . 5
⊢ ((𝐹:𝐴⟶𝑅 ∧ 𝐴 ⊆ 𝑉 ∧ 𝑋 ∈ (𝐶 ∪ 𝑉)) → 𝑋 ∈ (𝐶 ∪ 𝑉)) |
2 | 1 | s1cld 13383 |
. . . 4
⊢ ((𝐹:𝐴⟶𝑅 ∧ 𝐴 ⊆ 𝑉 ∧ 𝑋 ∈ (𝐶 ∪ 𝑉)) → 〈“𝑋”〉 ∈ Word (𝐶 ∪ 𝑉)) |
3 | | elun 3753 |
. . . . . . 7
⊢ (𝑋 ∈ (𝐶 ∪ 𝑉) ↔ (𝑋 ∈ 𝐶 ∨ 𝑋 ∈ 𝑉)) |
4 | | elfvex 6221 |
. . . . . . . . 9
⊢ (𝑋 ∈ (mCN‘𝑇) → 𝑇 ∈ V) |
5 | | mrsubffval.c |
. . . . . . . . 9
⊢ 𝐶 = (mCN‘𝑇) |
6 | 4, 5 | eleq2s 2719 |
. . . . . . . 8
⊢ (𝑋 ∈ 𝐶 → 𝑇 ∈ V) |
7 | | elfvex 6221 |
. . . . . . . . 9
⊢ (𝑋 ∈ (mVR‘𝑇) → 𝑇 ∈ V) |
8 | | mrsubffval.v |
. . . . . . . . 9
⊢ 𝑉 = (mVR‘𝑇) |
9 | 7, 8 | eleq2s 2719 |
. . . . . . . 8
⊢ (𝑋 ∈ 𝑉 → 𝑇 ∈ V) |
10 | 6, 9 | jaoi 394 |
. . . . . . 7
⊢ ((𝑋 ∈ 𝐶 ∨ 𝑋 ∈ 𝑉) → 𝑇 ∈ V) |
11 | 3, 10 | sylbi 207 |
. . . . . 6
⊢ (𝑋 ∈ (𝐶 ∪ 𝑉) → 𝑇 ∈ V) |
12 | 11 | 3ad2ant3 1084 |
. . . . 5
⊢ ((𝐹:𝐴⟶𝑅 ∧ 𝐴 ⊆ 𝑉 ∧ 𝑋 ∈ (𝐶 ∪ 𝑉)) → 𝑇 ∈ V) |
13 | | mrsubffval.r |
. . . . . 6
⊢ 𝑅 = (mREx‘𝑇) |
14 | 5, 8, 13 | mrexval 31398 |
. . . . 5
⊢ (𝑇 ∈ V → 𝑅 = Word (𝐶 ∪ 𝑉)) |
15 | 12, 14 | syl 17 |
. . . 4
⊢ ((𝐹:𝐴⟶𝑅 ∧ 𝐴 ⊆ 𝑉 ∧ 𝑋 ∈ (𝐶 ∪ 𝑉)) → 𝑅 = Word (𝐶 ∪ 𝑉)) |
16 | 2, 15 | eleqtrrd 2704 |
. . 3
⊢ ((𝐹:𝐴⟶𝑅 ∧ 𝐴 ⊆ 𝑉 ∧ 𝑋 ∈ (𝐶 ∪ 𝑉)) → 〈“𝑋”〉 ∈ 𝑅) |
17 | | mrsubffval.s |
. . . 4
⊢ 𝑆 = (mRSubst‘𝑇) |
18 | | eqid 2622 |
. . . 4
⊢
(freeMnd‘(𝐶
∪ 𝑉)) =
(freeMnd‘(𝐶 ∪
𝑉)) |
19 | 5, 8, 13, 17, 18 | mrsubval 31406 |
. . 3
⊢ ((𝐹:𝐴⟶𝑅 ∧ 𝐴 ⊆ 𝑉 ∧ 〈“𝑋”〉 ∈ 𝑅) → ((𝑆‘𝐹)‘〈“𝑋”〉) = ((freeMnd‘(𝐶 ∪ 𝑉)) Σg ((𝑣 ∈ (𝐶 ∪ 𝑉) ↦ if(𝑣 ∈ 𝐴, (𝐹‘𝑣), 〈“𝑣”〉)) ∘ 〈“𝑋”〉))) |
20 | 16, 19 | syld3an3 1371 |
. 2
⊢ ((𝐹:𝐴⟶𝑅 ∧ 𝐴 ⊆ 𝑉 ∧ 𝑋 ∈ (𝐶 ∪ 𝑉)) → ((𝑆‘𝐹)‘〈“𝑋”〉) = ((freeMnd‘(𝐶 ∪ 𝑉)) Σg ((𝑣 ∈ (𝐶 ∪ 𝑉) ↦ if(𝑣 ∈ 𝐴, (𝐹‘𝑣), 〈“𝑣”〉)) ∘ 〈“𝑋”〉))) |
21 | | simpl1 1064 |
. . . . . . . . 9
⊢ (((𝐹:𝐴⟶𝑅 ∧ 𝐴 ⊆ 𝑉 ∧ 𝑋 ∈ (𝐶 ∪ 𝑉)) ∧ 𝑣 ∈ (𝐶 ∪ 𝑉)) → 𝐹:𝐴⟶𝑅) |
22 | 21 | ffvelrnda 6359 |
. . . . . . . 8
⊢ ((((𝐹:𝐴⟶𝑅 ∧ 𝐴 ⊆ 𝑉 ∧ 𝑋 ∈ (𝐶 ∪ 𝑉)) ∧ 𝑣 ∈ (𝐶 ∪ 𝑉)) ∧ 𝑣 ∈ 𝐴) → (𝐹‘𝑣) ∈ 𝑅) |
23 | 15 | ad2antrr 762 |
. . . . . . . 8
⊢ ((((𝐹:𝐴⟶𝑅 ∧ 𝐴 ⊆ 𝑉 ∧ 𝑋 ∈ (𝐶 ∪ 𝑉)) ∧ 𝑣 ∈ (𝐶 ∪ 𝑉)) ∧ 𝑣 ∈ 𝐴) → 𝑅 = Word (𝐶 ∪ 𝑉)) |
24 | 22, 23 | eleqtrd 2703 |
. . . . . . 7
⊢ ((((𝐹:𝐴⟶𝑅 ∧ 𝐴 ⊆ 𝑉 ∧ 𝑋 ∈ (𝐶 ∪ 𝑉)) ∧ 𝑣 ∈ (𝐶 ∪ 𝑉)) ∧ 𝑣 ∈ 𝐴) → (𝐹‘𝑣) ∈ Word (𝐶 ∪ 𝑉)) |
25 | | simplr 792 |
. . . . . . . 8
⊢ ((((𝐹:𝐴⟶𝑅 ∧ 𝐴 ⊆ 𝑉 ∧ 𝑋 ∈ (𝐶 ∪ 𝑉)) ∧ 𝑣 ∈ (𝐶 ∪ 𝑉)) ∧ ¬ 𝑣 ∈ 𝐴) → 𝑣 ∈ (𝐶 ∪ 𝑉)) |
26 | 25 | s1cld 13383 |
. . . . . . 7
⊢ ((((𝐹:𝐴⟶𝑅 ∧ 𝐴 ⊆ 𝑉 ∧ 𝑋 ∈ (𝐶 ∪ 𝑉)) ∧ 𝑣 ∈ (𝐶 ∪ 𝑉)) ∧ ¬ 𝑣 ∈ 𝐴) → 〈“𝑣”〉 ∈ Word (𝐶 ∪ 𝑉)) |
27 | 24, 26 | ifclda 4120 |
. . . . . 6
⊢ (((𝐹:𝐴⟶𝑅 ∧ 𝐴 ⊆ 𝑉 ∧ 𝑋 ∈ (𝐶 ∪ 𝑉)) ∧ 𝑣 ∈ (𝐶 ∪ 𝑉)) → if(𝑣 ∈ 𝐴, (𝐹‘𝑣), 〈“𝑣”〉) ∈ Word (𝐶 ∪ 𝑉)) |
28 | | eqid 2622 |
. . . . . 6
⊢ (𝑣 ∈ (𝐶 ∪ 𝑉) ↦ if(𝑣 ∈ 𝐴, (𝐹‘𝑣), 〈“𝑣”〉)) = (𝑣 ∈ (𝐶 ∪ 𝑉) ↦ if(𝑣 ∈ 𝐴, (𝐹‘𝑣), 〈“𝑣”〉)) |
29 | 27, 28 | fmptd 6385 |
. . . . 5
⊢ ((𝐹:𝐴⟶𝑅 ∧ 𝐴 ⊆ 𝑉 ∧ 𝑋 ∈ (𝐶 ∪ 𝑉)) → (𝑣 ∈ (𝐶 ∪ 𝑉) ↦ if(𝑣 ∈ 𝐴, (𝐹‘𝑣), 〈“𝑣”〉)):(𝐶 ∪ 𝑉)⟶Word (𝐶 ∪ 𝑉)) |
30 | | s1co 13579 |
. . . . 5
⊢ ((𝑋 ∈ (𝐶 ∪ 𝑉) ∧ (𝑣 ∈ (𝐶 ∪ 𝑉) ↦ if(𝑣 ∈ 𝐴, (𝐹‘𝑣), 〈“𝑣”〉)):(𝐶 ∪ 𝑉)⟶Word (𝐶 ∪ 𝑉)) → ((𝑣 ∈ (𝐶 ∪ 𝑉) ↦ if(𝑣 ∈ 𝐴, (𝐹‘𝑣), 〈“𝑣”〉)) ∘ 〈“𝑋”〉) =
〈“((𝑣 ∈
(𝐶 ∪ 𝑉) ↦ if(𝑣 ∈ 𝐴, (𝐹‘𝑣), 〈“𝑣”〉))‘𝑋)”〉) |
31 | 1, 29, 30 | syl2anc 693 |
. . . 4
⊢ ((𝐹:𝐴⟶𝑅 ∧ 𝐴 ⊆ 𝑉 ∧ 𝑋 ∈ (𝐶 ∪ 𝑉)) → ((𝑣 ∈ (𝐶 ∪ 𝑉) ↦ if(𝑣 ∈ 𝐴, (𝐹‘𝑣), 〈“𝑣”〉)) ∘ 〈“𝑋”〉) =
〈“((𝑣 ∈
(𝐶 ∪ 𝑉) ↦ if(𝑣 ∈ 𝐴, (𝐹‘𝑣), 〈“𝑣”〉))‘𝑋)”〉) |
32 | | eleq1 2689 |
. . . . . . . 8
⊢ (𝑣 = 𝑋 → (𝑣 ∈ 𝐴 ↔ 𝑋 ∈ 𝐴)) |
33 | | fveq2 6191 |
. . . . . . . 8
⊢ (𝑣 = 𝑋 → (𝐹‘𝑣) = (𝐹‘𝑋)) |
34 | | s1eq 13380 |
. . . . . . . 8
⊢ (𝑣 = 𝑋 → 〈“𝑣”〉 = 〈“𝑋”〉) |
35 | 32, 33, 34 | ifbieq12d 4113 |
. . . . . . 7
⊢ (𝑣 = 𝑋 → if(𝑣 ∈ 𝐴, (𝐹‘𝑣), 〈“𝑣”〉) = if(𝑋 ∈ 𝐴, (𝐹‘𝑋), 〈“𝑋”〉)) |
36 | | fvex 6201 |
. . . . . . . 8
⊢ (𝐹‘𝑋) ∈ V |
37 | | s1cli 13384 |
. . . . . . . . 9
⊢
〈“𝑋”〉 ∈ Word V |
38 | 37 | elexi 3213 |
. . . . . . . 8
⊢
〈“𝑋”〉 ∈ V |
39 | 36, 38 | ifex 4156 |
. . . . . . 7
⊢ if(𝑋 ∈ 𝐴, (𝐹‘𝑋), 〈“𝑋”〉) ∈ V |
40 | 35, 28, 39 | fvmpt 6282 |
. . . . . 6
⊢ (𝑋 ∈ (𝐶 ∪ 𝑉) → ((𝑣 ∈ (𝐶 ∪ 𝑉) ↦ if(𝑣 ∈ 𝐴, (𝐹‘𝑣), 〈“𝑣”〉))‘𝑋) = if(𝑋 ∈ 𝐴, (𝐹‘𝑋), 〈“𝑋”〉)) |
41 | 40 | 3ad2ant3 1084 |
. . . . 5
⊢ ((𝐹:𝐴⟶𝑅 ∧ 𝐴 ⊆ 𝑉 ∧ 𝑋 ∈ (𝐶 ∪ 𝑉)) → ((𝑣 ∈ (𝐶 ∪ 𝑉) ↦ if(𝑣 ∈ 𝐴, (𝐹‘𝑣), 〈“𝑣”〉))‘𝑋) = if(𝑋 ∈ 𝐴, (𝐹‘𝑋), 〈“𝑋”〉)) |
42 | 41 | s1eqd 13381 |
. . . 4
⊢ ((𝐹:𝐴⟶𝑅 ∧ 𝐴 ⊆ 𝑉 ∧ 𝑋 ∈ (𝐶 ∪ 𝑉)) → 〈“((𝑣 ∈ (𝐶 ∪ 𝑉) ↦ if(𝑣 ∈ 𝐴, (𝐹‘𝑣), 〈“𝑣”〉))‘𝑋)”〉 = 〈“if(𝑋 ∈ 𝐴, (𝐹‘𝑋), 〈“𝑋”〉)”〉) |
43 | 31, 42 | eqtrd 2656 |
. . 3
⊢ ((𝐹:𝐴⟶𝑅 ∧ 𝐴 ⊆ 𝑉 ∧ 𝑋 ∈ (𝐶 ∪ 𝑉)) → ((𝑣 ∈ (𝐶 ∪ 𝑉) ↦ if(𝑣 ∈ 𝐴, (𝐹‘𝑣), 〈“𝑣”〉)) ∘ 〈“𝑋”〉) =
〈“if(𝑋 ∈
𝐴, (𝐹‘𝑋), 〈“𝑋”〉)”〉) |
44 | 43 | oveq2d 6666 |
. 2
⊢ ((𝐹:𝐴⟶𝑅 ∧ 𝐴 ⊆ 𝑉 ∧ 𝑋 ∈ (𝐶 ∪ 𝑉)) → ((freeMnd‘(𝐶 ∪ 𝑉)) Σg ((𝑣 ∈ (𝐶 ∪ 𝑉) ↦ if(𝑣 ∈ 𝐴, (𝐹‘𝑣), 〈“𝑣”〉)) ∘ 〈“𝑋”〉)) =
((freeMnd‘(𝐶 ∪
𝑉))
Σg 〈“if(𝑋 ∈ 𝐴, (𝐹‘𝑋), 〈“𝑋”〉)”〉)) |
45 | 29, 1 | ffvelrnd 6360 |
. . . 4
⊢ ((𝐹:𝐴⟶𝑅 ∧ 𝐴 ⊆ 𝑉 ∧ 𝑋 ∈ (𝐶 ∪ 𝑉)) → ((𝑣 ∈ (𝐶 ∪ 𝑉) ↦ if(𝑣 ∈ 𝐴, (𝐹‘𝑣), 〈“𝑣”〉))‘𝑋) ∈ Word (𝐶 ∪ 𝑉)) |
46 | 41, 45 | eqeltrrd 2702 |
. . 3
⊢ ((𝐹:𝐴⟶𝑅 ∧ 𝐴 ⊆ 𝑉 ∧ 𝑋 ∈ (𝐶 ∪ 𝑉)) → if(𝑋 ∈ 𝐴, (𝐹‘𝑋), 〈“𝑋”〉) ∈ Word (𝐶 ∪ 𝑉)) |
47 | | fvex 6201 |
. . . . . . . 8
⊢
(mCN‘𝑇) ∈
V |
48 | 5, 47 | eqeltri 2697 |
. . . . . . 7
⊢ 𝐶 ∈ V |
49 | | fvex 6201 |
. . . . . . . 8
⊢
(mVR‘𝑇) ∈
V |
50 | 8, 49 | eqeltri 2697 |
. . . . . . 7
⊢ 𝑉 ∈ V |
51 | 48, 50 | unex 6956 |
. . . . . 6
⊢ (𝐶 ∪ 𝑉) ∈ V |
52 | | eqid 2622 |
. . . . . . 7
⊢
(Base‘(freeMnd‘(𝐶 ∪ 𝑉))) = (Base‘(freeMnd‘(𝐶 ∪ 𝑉))) |
53 | 18, 52 | frmdbas 17389 |
. . . . . 6
⊢ ((𝐶 ∪ 𝑉) ∈ V →
(Base‘(freeMnd‘(𝐶 ∪ 𝑉))) = Word (𝐶 ∪ 𝑉)) |
54 | 51, 53 | ax-mp 5 |
. . . . 5
⊢
(Base‘(freeMnd‘(𝐶 ∪ 𝑉))) = Word (𝐶 ∪ 𝑉) |
55 | 54 | eqcomi 2631 |
. . . 4
⊢ Word
(𝐶 ∪ 𝑉) = (Base‘(freeMnd‘(𝐶 ∪ 𝑉))) |
56 | 55 | gsumws1 17376 |
. . 3
⊢ (if(𝑋 ∈ 𝐴, (𝐹‘𝑋), 〈“𝑋”〉) ∈ Word (𝐶 ∪ 𝑉) → ((freeMnd‘(𝐶 ∪ 𝑉)) Σg
〈“if(𝑋 ∈
𝐴, (𝐹‘𝑋), 〈“𝑋”〉)”〉) = if(𝑋 ∈ 𝐴, (𝐹‘𝑋), 〈“𝑋”〉)) |
57 | 46, 56 | syl 17 |
. 2
⊢ ((𝐹:𝐴⟶𝑅 ∧ 𝐴 ⊆ 𝑉 ∧ 𝑋 ∈ (𝐶 ∪ 𝑉)) → ((freeMnd‘(𝐶 ∪ 𝑉)) Σg
〈“if(𝑋 ∈
𝐴, (𝐹‘𝑋), 〈“𝑋”〉)”〉) = if(𝑋 ∈ 𝐴, (𝐹‘𝑋), 〈“𝑋”〉)) |
58 | 20, 44, 57 | 3eqtrd 2660 |
1
⊢ ((𝐹:𝐴⟶𝑅 ∧ 𝐴 ⊆ 𝑉 ∧ 𝑋 ∈ (𝐶 ∪ 𝑉)) → ((𝑆‘𝐹)‘〈“𝑋”〉) = if(𝑋 ∈ 𝐴, (𝐹‘𝑋), 〈“𝑋”〉)) |