Step | Hyp | Ref
| Expression |
1 | | simp3 1139 |
. . . . 5
β’ ((πΉ:π΄βΆπ
β§ π΄ β π β§ π β (πΆ βͺ π)) β π β (πΆ βͺ π)) |
2 | 1 | s1cld 14550 |
. . . 4
β’ ((πΉ:π΄βΆπ
β§ π΄ β π β§ π β (πΆ βͺ π)) β β¨βπββ© β Word (πΆ βͺ π)) |
3 | | elun 4148 |
. . . . . . 7
β’ (π β (πΆ βͺ π) β (π β πΆ β¨ π β π)) |
4 | | elfvex 6927 |
. . . . . . . . 9
β’ (π β (mCNβπ) β π β V) |
5 | | mrsubffval.c |
. . . . . . . . 9
β’ πΆ = (mCNβπ) |
6 | 4, 5 | eleq2s 2852 |
. . . . . . . 8
β’ (π β πΆ β π β V) |
7 | | elfvex 6927 |
. . . . . . . . 9
β’ (π β (mVRβπ) β π β V) |
8 | | mrsubffval.v |
. . . . . . . . 9
β’ π = (mVRβπ) |
9 | 7, 8 | eleq2s 2852 |
. . . . . . . 8
β’ (π β π β π β V) |
10 | 6, 9 | jaoi 856 |
. . . . . . 7
β’ ((π β πΆ β¨ π β π) β π β V) |
11 | 3, 10 | sylbi 216 |
. . . . . 6
β’ (π β (πΆ βͺ π) β π β V) |
12 | 11 | 3ad2ant3 1136 |
. . . . 5
β’ ((πΉ:π΄βΆπ
β§ π΄ β π β§ π β (πΆ βͺ π)) β π β V) |
13 | | mrsubffval.r |
. . . . . 6
β’ π
= (mRExβπ) |
14 | 5, 8, 13 | mrexval 34481 |
. . . . 5
β’ (π β V β π
= Word (πΆ βͺ π)) |
15 | 12, 14 | syl 17 |
. . . 4
β’ ((πΉ:π΄βΆπ
β§ π΄ β π β§ π β (πΆ βͺ π)) β π
= Word (πΆ βͺ π)) |
16 | 2, 15 | eleqtrrd 2837 |
. . 3
β’ ((πΉ:π΄βΆπ
β§ π΄ β π β§ π β (πΆ βͺ π)) β β¨βπββ© β π
) |
17 | | mrsubffval.s |
. . . 4
β’ π = (mRSubstβπ) |
18 | | eqid 2733 |
. . . 4
β’
(freeMndβ(πΆ
βͺ π)) =
(freeMndβ(πΆ βͺ
π)) |
19 | 5, 8, 13, 17, 18 | mrsubval 34489 |
. . 3
β’ ((πΉ:π΄βΆπ
β§ π΄ β π β§ β¨βπββ© β π
) β ((πβπΉ)ββ¨βπββ©) = ((freeMndβ(πΆ βͺ π)) Ξ£g ((π£ β (πΆ βͺ π) β¦ if(π£ β π΄, (πΉβπ£), β¨βπ£ββ©)) β β¨βπββ©))) |
20 | 16, 19 | syld3an3 1410 |
. 2
β’ ((πΉ:π΄βΆπ
β§ π΄ β π β§ π β (πΆ βͺ π)) β ((πβπΉ)ββ¨βπββ©) = ((freeMndβ(πΆ βͺ π)) Ξ£g ((π£ β (πΆ βͺ π) β¦ if(π£ β π΄, (πΉβπ£), β¨βπ£ββ©)) β β¨βπββ©))) |
21 | | simpl1 1192 |
. . . . . . . . 9
β’ (((πΉ:π΄βΆπ
β§ π΄ β π β§ π β (πΆ βͺ π)) β§ π£ β (πΆ βͺ π)) β πΉ:π΄βΆπ
) |
22 | 21 | ffvelcdmda 7084 |
. . . . . . . 8
β’ ((((πΉ:π΄βΆπ
β§ π΄ β π β§ π β (πΆ βͺ π)) β§ π£ β (πΆ βͺ π)) β§ π£ β π΄) β (πΉβπ£) β π
) |
23 | 15 | ad2antrr 725 |
. . . . . . . 8
β’ ((((πΉ:π΄βΆπ
β§ π΄ β π β§ π β (πΆ βͺ π)) β§ π£ β (πΆ βͺ π)) β§ π£ β π΄) β π
= Word (πΆ βͺ π)) |
24 | 22, 23 | eleqtrd 2836 |
. . . . . . 7
β’ ((((πΉ:π΄βΆπ
β§ π΄ β π β§ π β (πΆ βͺ π)) β§ π£ β (πΆ βͺ π)) β§ π£ β π΄) β (πΉβπ£) β Word (πΆ βͺ π)) |
25 | | simplr 768 |
. . . . . . . 8
β’ ((((πΉ:π΄βΆπ
β§ π΄ β π β§ π β (πΆ βͺ π)) β§ π£ β (πΆ βͺ π)) β§ Β¬ π£ β π΄) β π£ β (πΆ βͺ π)) |
26 | 25 | s1cld 14550 |
. . . . . . 7
β’ ((((πΉ:π΄βΆπ
β§ π΄ β π β§ π β (πΆ βͺ π)) β§ π£ β (πΆ βͺ π)) β§ Β¬ π£ β π΄) β β¨βπ£ββ© β Word (πΆ βͺ π)) |
27 | 24, 26 | ifclda 4563 |
. . . . . 6
β’ (((πΉ:π΄βΆπ
β§ π΄ β π β§ π β (πΆ βͺ π)) β§ π£ β (πΆ βͺ π)) β if(π£ β π΄, (πΉβπ£), β¨βπ£ββ©) β Word (πΆ βͺ π)) |
28 | 27 | fmpttd 7112 |
. . . . 5
β’ ((πΉ:π΄βΆπ
β§ π΄ β π β§ π β (πΆ βͺ π)) β (π£ β (πΆ βͺ π) β¦ if(π£ β π΄, (πΉβπ£), β¨βπ£ββ©)):(πΆ βͺ π)βΆWord (πΆ βͺ π)) |
29 | | s1co 14781 |
. . . . 5
β’ ((π β (πΆ βͺ π) β§ (π£ β (πΆ βͺ π) β¦ if(π£ β π΄, (πΉβπ£), β¨βπ£ββ©)):(πΆ βͺ π)βΆWord (πΆ βͺ π)) β ((π£ β (πΆ βͺ π) β¦ if(π£ β π΄, (πΉβπ£), β¨βπ£ββ©)) β β¨βπββ©) =
β¨β((π£ β
(πΆ βͺ π) β¦ if(π£ β π΄, (πΉβπ£), β¨βπ£ββ©))βπ)ββ©) |
30 | 1, 28, 29 | syl2anc 585 |
. . . 4
β’ ((πΉ:π΄βΆπ
β§ π΄ β π β§ π β (πΆ βͺ π)) β ((π£ β (πΆ βͺ π) β¦ if(π£ β π΄, (πΉβπ£), β¨βπ£ββ©)) β β¨βπββ©) =
β¨β((π£ β
(πΆ βͺ π) β¦ if(π£ β π΄, (πΉβπ£), β¨βπ£ββ©))βπ)ββ©) |
31 | | eleq1 2822 |
. . . . . . . 8
β’ (π£ = π β (π£ β π΄ β π β π΄)) |
32 | | fveq2 6889 |
. . . . . . . 8
β’ (π£ = π β (πΉβπ£) = (πΉβπ)) |
33 | | s1eq 14547 |
. . . . . . . 8
β’ (π£ = π β β¨βπ£ββ© = β¨βπββ©) |
34 | 31, 32, 33 | ifbieq12d 4556 |
. . . . . . 7
β’ (π£ = π β if(π£ β π΄, (πΉβπ£), β¨βπ£ββ©) = if(π β π΄, (πΉβπ), β¨βπββ©)) |
35 | | eqid 2733 |
. . . . . . 7
β’ (π£ β (πΆ βͺ π) β¦ if(π£ β π΄, (πΉβπ£), β¨βπ£ββ©)) = (π£ β (πΆ βͺ π) β¦ if(π£ β π΄, (πΉβπ£), β¨βπ£ββ©)) |
36 | | fvex 6902 |
. . . . . . . 8
β’ (πΉβπ) β V |
37 | | s1cli 14552 |
. . . . . . . . 9
β’
β¨βπββ© β Word V |
38 | 37 | elexi 3494 |
. . . . . . . 8
β’
β¨βπββ© β V |
39 | 36, 38 | ifex 4578 |
. . . . . . 7
β’ if(π β π΄, (πΉβπ), β¨βπββ©) β V |
40 | 34, 35, 39 | fvmpt 6996 |
. . . . . 6
β’ (π β (πΆ βͺ π) β ((π£ β (πΆ βͺ π) β¦ if(π£ β π΄, (πΉβπ£), β¨βπ£ββ©))βπ) = if(π β π΄, (πΉβπ), β¨βπββ©)) |
41 | 40 | 3ad2ant3 1136 |
. . . . 5
β’ ((πΉ:π΄βΆπ
β§ π΄ β π β§ π β (πΆ βͺ π)) β ((π£ β (πΆ βͺ π) β¦ if(π£ β π΄, (πΉβπ£), β¨βπ£ββ©))βπ) = if(π β π΄, (πΉβπ), β¨βπββ©)) |
42 | 41 | s1eqd 14548 |
. . . 4
β’ ((πΉ:π΄βΆπ
β§ π΄ β π β§ π β (πΆ βͺ π)) β β¨β((π£ β (πΆ βͺ π) β¦ if(π£ β π΄, (πΉβπ£), β¨βπ£ββ©))βπ)ββ© = β¨βif(π β π΄, (πΉβπ), β¨βπββ©)ββ©) |
43 | 30, 42 | eqtrd 2773 |
. . 3
β’ ((πΉ:π΄βΆπ
β§ π΄ β π β§ π β (πΆ βͺ π)) β ((π£ β (πΆ βͺ π) β¦ if(π£ β π΄, (πΉβπ£), β¨βπ£ββ©)) β β¨βπββ©) =
β¨βif(π β
π΄, (πΉβπ), β¨βπββ©)ββ©) |
44 | 43 | oveq2d 7422 |
. 2
β’ ((πΉ:π΄βΆπ
β§ π΄ β π β§ π β (πΆ βͺ π)) β ((freeMndβ(πΆ βͺ π)) Ξ£g ((π£ β (πΆ βͺ π) β¦ if(π£ β π΄, (πΉβπ£), β¨βπ£ββ©)) β β¨βπββ©)) =
((freeMndβ(πΆ βͺ
π))
Ξ£g β¨βif(π β π΄, (πΉβπ), β¨βπββ©)ββ©)) |
45 | 28, 1 | ffvelcdmd 7085 |
. . . 4
β’ ((πΉ:π΄βΆπ
β§ π΄ β π β§ π β (πΆ βͺ π)) β ((π£ β (πΆ βͺ π) β¦ if(π£ β π΄, (πΉβπ£), β¨βπ£ββ©))βπ) β Word (πΆ βͺ π)) |
46 | 41, 45 | eqeltrrd 2835 |
. . 3
β’ ((πΉ:π΄βΆπ
β§ π΄ β π β§ π β (πΆ βͺ π)) β if(π β π΄, (πΉβπ), β¨βπββ©) β Word (πΆ βͺ π)) |
47 | 5 | fvexi 6903 |
. . . . . . 7
β’ πΆ β V |
48 | 8 | fvexi 6903 |
. . . . . . 7
β’ π β V |
49 | 47, 48 | unex 7730 |
. . . . . 6
β’ (πΆ βͺ π) β V |
50 | | eqid 2733 |
. . . . . . 7
β’
(Baseβ(freeMndβ(πΆ βͺ π))) = (Baseβ(freeMndβ(πΆ βͺ π))) |
51 | 18, 50 | frmdbas 18730 |
. . . . . 6
β’ ((πΆ βͺ π) β V β
(Baseβ(freeMndβ(πΆ βͺ π))) = Word (πΆ βͺ π)) |
52 | 49, 51 | ax-mp 5 |
. . . . 5
β’
(Baseβ(freeMndβ(πΆ βͺ π))) = Word (πΆ βͺ π) |
53 | 52 | eqcomi 2742 |
. . . 4
β’ Word
(πΆ βͺ π) = (Baseβ(freeMndβ(πΆ βͺ π))) |
54 | 53 | gsumws1 18716 |
. . 3
β’ (if(π β π΄, (πΉβπ), β¨βπββ©) β Word (πΆ βͺ π) β ((freeMndβ(πΆ βͺ π)) Ξ£g
β¨βif(π β
π΄, (πΉβπ), β¨βπββ©)ββ©) = if(π β π΄, (πΉβπ), β¨βπββ©)) |
55 | 46, 54 | syl 17 |
. 2
β’ ((πΉ:π΄βΆπ
β§ π΄ β π β§ π β (πΆ βͺ π)) β ((freeMndβ(πΆ βͺ π)) Ξ£g
β¨βif(π β
π΄, (πΉβπ), β¨βπββ©)ββ©) = if(π β π΄, (πΉβπ), β¨βπββ©)) |
56 | 20, 44, 55 | 3eqtrd 2777 |
1
β’ ((πΉ:π΄βΆπ
β§ π΄ β π β§ π β (πΆ βͺ π)) β ((πβπΉ)ββ¨βπββ©) = if(π β π΄, (πΉβπ), β¨βπββ©)) |