Step | Hyp | Ref
| Expression |
1 | | n0i 4297 |
. . 3
β’ (πΉ β ran π β Β¬ ran π = β
) |
2 | | mrsubccat.s |
. . . 4
β’ π = (mRSubstβπ) |
3 | 2 | rnfvprc 6840 |
. . 3
β’ (Β¬
π β V β ran π = β
) |
4 | 1, 3 | nsyl2 141 |
. 2
β’ (πΉ β ran π β π β V) |
5 | | eqid 2733 |
. . . . 5
β’
(mVRβπ) =
(mVRβπ) |
6 | | eqid 2733 |
. . . . 5
β’
(mRExβπ) =
(mRExβπ) |
7 | 5, 6, 2 | mrsubff 34170 |
. . . 4
β’ (π β V β π:((mRExβπ) βpm (mVRβπ))βΆ((mRExβπ) βm
(mRExβπ))) |
8 | | ffun 6675 |
. . . 4
β’ (π:((mRExβπ) βpm (mVRβπ))βΆ((mRExβπ) βm
(mRExβπ)) β Fun
π) |
9 | 4, 7, 8 | 3syl 18 |
. . 3
β’ (πΉ β ran π β Fun π) |
10 | 5, 6, 2 | mrsubrn 34171 |
. . . . 5
β’ ran π = (π β ((mRExβπ) βm (mVRβπ))) |
11 | 10 | eleq2i 2826 |
. . . 4
β’ (πΉ β ran π β πΉ β (π β ((mRExβπ) βm (mVRβπ)))) |
12 | 11 | biimpi 215 |
. . 3
β’ (πΉ β ran π β πΉ β (π β ((mRExβπ) βm (mVRβπ)))) |
13 | | fvelima 6912 |
. . 3
β’ ((Fun
π β§ πΉ β (π β ((mRExβπ) βm (mVRβπ)))) β βπ β ((mRExβπ) βm
(mVRβπ))(πβπ) = πΉ) |
14 | 9, 12, 13 | syl2anc 585 |
. 2
β’ (πΉ β ran π β βπ β ((mRExβπ) βm (mVRβπ))(πβπ) = πΉ) |
15 | | elmapi 8793 |
. . . . . . 7
β’ (π β ((mRExβπ) βm
(mVRβπ)) β π:(mVRβπ)βΆ(mRExβπ)) |
16 | 15 | adantl 483 |
. . . . . 6
β’ ((π β V β§ π β ((mRExβπ) βm
(mVRβπ))) β
π:(mVRβπ)βΆ(mRExβπ)) |
17 | | ssidd 3971 |
. . . . . 6
β’ ((π β V β§ π β ((mRExβπ) βm
(mVRβπ))) β
(mVRβπ) β
(mVRβπ)) |
18 | | wrd0 14436 |
. . . . . . 7
β’ β
β Word ((mCNβπ)
βͺ (mVRβπ)) |
19 | | eqid 2733 |
. . . . . . . . 9
β’
(mCNβπ) =
(mCNβπ) |
20 | 19, 5, 6 | mrexval 34159 |
. . . . . . . 8
β’ (π β V β
(mRExβπ) = Word
((mCNβπ) βͺ
(mVRβπ))) |
21 | 20 | adantr 482 |
. . . . . . 7
β’ ((π β V β§ π β ((mRExβπ) βm
(mVRβπ))) β
(mRExβπ) = Word
((mCNβπ) βͺ
(mVRβπ))) |
22 | 18, 21 | eleqtrrid 2841 |
. . . . . 6
β’ ((π β V β§ π β ((mRExβπ) βm
(mVRβπ))) β
β
β (mRExβπ)) |
23 | | eqid 2733 |
. . . . . . 7
β’
(freeMndβ((mCNβπ) βͺ (mVRβπ))) = (freeMndβ((mCNβπ) βͺ (mVRβπ))) |
24 | 19, 5, 6, 2, 23 | mrsubval 34167 |
. . . . . 6
β’ ((π:(mVRβπ)βΆ(mRExβπ) β§ (mVRβπ) β (mVRβπ) β§ β
β (mRExβπ)) β ((πβπ)ββ
) =
((freeMndβ((mCNβπ) βͺ (mVRβπ))) Ξ£g ((π£ β ((mCNβπ) βͺ (mVRβπ)) β¦ if(π£ β (mVRβπ), (πβπ£), β¨βπ£ββ©)) β
β
))) |
25 | 16, 17, 22, 24 | syl3anc 1372 |
. . . . 5
β’ ((π β V β§ π β ((mRExβπ) βm
(mVRβπ))) β
((πβπ)ββ
) =
((freeMndβ((mCNβπ) βͺ (mVRβπ))) Ξ£g ((π£ β ((mCNβπ) βͺ (mVRβπ)) β¦ if(π£ β (mVRβπ), (πβπ£), β¨βπ£ββ©)) β
β
))) |
26 | | co02 6216 |
. . . . . . 7
β’ ((π£ β ((mCNβπ) βͺ (mVRβπ)) β¦ if(π£ β (mVRβπ), (πβπ£), β¨βπ£ββ©)) β β
) =
β
|
27 | 26 | oveq2i 7372 |
. . . . . 6
β’
((freeMndβ((mCNβπ) βͺ (mVRβπ))) Ξ£g ((π£ β ((mCNβπ) βͺ (mVRβπ)) β¦ if(π£ β (mVRβπ), (πβπ£), β¨βπ£ββ©)) β β
)) =
((freeMndβ((mCNβπ) βͺ (mVRβπ))) Ξ£g
β
) |
28 | 23 | frmd0 18678 |
. . . . . . 7
β’ β
=
(0gβ(freeMndβ((mCNβπ) βͺ (mVRβπ)))) |
29 | 28 | gsum0 18547 |
. . . . . 6
β’
((freeMndβ((mCNβπ) βͺ (mVRβπ))) Ξ£g β
) =
β
|
30 | 27, 29 | eqtri 2761 |
. . . . 5
β’
((freeMndβ((mCNβπ) βͺ (mVRβπ))) Ξ£g ((π£ β ((mCNβπ) βͺ (mVRβπ)) β¦ if(π£ β (mVRβπ), (πβπ£), β¨βπ£ββ©)) β β
)) =
β
|
31 | 25, 30 | eqtrdi 2789 |
. . . 4
β’ ((π β V β§ π β ((mRExβπ) βm
(mVRβπ))) β
((πβπ)ββ
) =
β
) |
32 | | fveq1 6845 |
. . . . 5
β’ ((πβπ) = πΉ β ((πβπ)ββ
) = (πΉββ
)) |
33 | 32 | eqeq1d 2735 |
. . . 4
β’ ((πβπ) = πΉ β (((πβπ)ββ
) = β
β (πΉββ
) =
β
)) |
34 | 31, 33 | syl5ibcom 244 |
. . 3
β’ ((π β V β§ π β ((mRExβπ) βm
(mVRβπ))) β
((πβπ) = πΉ β (πΉββ
) = β
)) |
35 | 34 | rexlimdva 3149 |
. 2
β’ (π β V β (βπ β ((mRExβπ) βm
(mVRβπ))(πβπ) = πΉ β (πΉββ
) = β
)) |
36 | 4, 14, 35 | sylc 65 |
1
β’ (πΉ β ran π β (πΉββ
) = β
) |