Step | Hyp | Ref
| Expression |
1 | | mrsubco.s |
. . . . 5
β’ π = (mRSubstβπ) |
2 | | eqid 2733 |
. . . . 5
β’
(mRExβπ) =
(mRExβπ) |
3 | 1, 2 | mrsubf 34175 |
. . . 4
β’ (πΉ β ran π β πΉ:(mRExβπ)βΆ(mRExβπ)) |
4 | 3 | adantr 482 |
. . 3
β’ ((πΉ β ran π β§ πΊ β ran π) β πΉ:(mRExβπ)βΆ(mRExβπ)) |
5 | 1, 2 | mrsubf 34175 |
. . . 4
β’ (πΊ β ran π β πΊ:(mRExβπ)βΆ(mRExβπ)) |
6 | 5 | adantl 483 |
. . 3
β’ ((πΉ β ran π β§ πΊ β ran π) β πΊ:(mRExβπ)βΆ(mRExβπ)) |
7 | | fco 6696 |
. . 3
β’ ((πΉ:(mRExβπ)βΆ(mRExβπ) β§ πΊ:(mRExβπ)βΆ(mRExβπ)) β (πΉ β πΊ):(mRExβπ)βΆ(mRExβπ)) |
8 | 4, 6, 7 | syl2anc 585 |
. 2
β’ ((πΉ β ran π β§ πΊ β ran π) β (πΉ β πΊ):(mRExβπ)βΆ(mRExβπ)) |
9 | 6 | adantr 482 |
. . . . 5
β’ (((πΉ β ran π β§ πΊ β ran π) β§ π β ((mCNβπ) β (mVRβπ))) β πΊ:(mRExβπ)βΆ(mRExβπ)) |
10 | | eldifi 4090 |
. . . . . . . . 9
β’ (π β ((mCNβπ) β (mVRβπ)) β π β (mCNβπ)) |
11 | | elun1 4140 |
. . . . . . . . 9
β’ (π β (mCNβπ) β π β ((mCNβπ) βͺ (mVRβπ))) |
12 | 10, 11 | syl 17 |
. . . . . . . 8
β’ (π β ((mCNβπ) β (mVRβπ)) β π β ((mCNβπ) βͺ (mVRβπ))) |
13 | 12 | adantl 483 |
. . . . . . 7
β’ (((πΉ β ran π β§ πΊ β ran π) β§ π β ((mCNβπ) β (mVRβπ))) β π β ((mCNβπ) βͺ (mVRβπ))) |
14 | 13 | s1cld 14500 |
. . . . . 6
β’ (((πΉ β ran π β§ πΊ β ran π) β§ π β ((mCNβπ) β (mVRβπ))) β β¨βπββ© β Word ((mCNβπ) βͺ (mVRβπ))) |
15 | | n0i 4297 |
. . . . . . . . . 10
β’ (πΉ β ran π β Β¬ ran π = β
) |
16 | 1 | rnfvprc 6840 |
. . . . . . . . . 10
β’ (Β¬
π β V β ran π = β
) |
17 | 15, 16 | nsyl2 141 |
. . . . . . . . 9
β’ (πΉ β ran π β π β V) |
18 | 17 | adantr 482 |
. . . . . . . 8
β’ ((πΉ β ran π β§ πΊ β ran π) β π β V) |
19 | 18 | adantr 482 |
. . . . . . 7
β’ (((πΉ β ran π β§ πΊ β ran π) β§ π β ((mCNβπ) β (mVRβπ))) β π β V) |
20 | | eqid 2733 |
. . . . . . . 8
β’
(mCNβπ) =
(mCNβπ) |
21 | | eqid 2733 |
. . . . . . . 8
β’
(mVRβπ) =
(mVRβπ) |
22 | 20, 21, 2 | mrexval 34159 |
. . . . . . 7
β’ (π β V β
(mRExβπ) = Word
((mCNβπ) βͺ
(mVRβπ))) |
23 | 19, 22 | syl 17 |
. . . . . 6
β’ (((πΉ β ran π β§ πΊ β ran π) β§ π β ((mCNβπ) β (mVRβπ))) β (mRExβπ) = Word ((mCNβπ) βͺ (mVRβπ))) |
24 | 14, 23 | eleqtrrd 2837 |
. . . . 5
β’ (((πΉ β ran π β§ πΊ β ran π) β§ π β ((mCNβπ) β (mVRβπ))) β β¨βπββ© β (mRExβπ)) |
25 | | fvco3 6944 |
. . . . 5
β’ ((πΊ:(mRExβπ)βΆ(mRExβπ) β§ β¨βπββ© β (mRExβπ)) β ((πΉ β πΊ)ββ¨βπββ©) = (πΉβ(πΊββ¨βπββ©))) |
26 | 9, 24, 25 | syl2anc 585 |
. . . 4
β’ (((πΉ β ran π β§ πΊ β ran π) β§ π β ((mCNβπ) β (mVRβπ))) β ((πΉ β πΊ)ββ¨βπββ©) = (πΉβ(πΊββ¨βπββ©))) |
27 | 1, 2, 21, 20 | mrsubcn 34177 |
. . . . . 6
β’ ((πΊ β ran π β§ π β ((mCNβπ) β (mVRβπ))) β (πΊββ¨βπββ©) = β¨βπββ©) |
28 | 27 | adantll 713 |
. . . . 5
β’ (((πΉ β ran π β§ πΊ β ran π) β§ π β ((mCNβπ) β (mVRβπ))) β (πΊββ¨βπββ©) = β¨βπββ©) |
29 | 28 | fveq2d 6850 |
. . . 4
β’ (((πΉ β ran π β§ πΊ β ran π) β§ π β ((mCNβπ) β (mVRβπ))) β (πΉβ(πΊββ¨βπββ©)) = (πΉββ¨βπββ©)) |
30 | 1, 2, 21, 20 | mrsubcn 34177 |
. . . . 5
β’ ((πΉ β ran π β§ π β ((mCNβπ) β (mVRβπ))) β (πΉββ¨βπββ©) = β¨βπββ©) |
31 | 30 | adantlr 714 |
. . . 4
β’ (((πΉ β ran π β§ πΊ β ran π) β§ π β ((mCNβπ) β (mVRβπ))) β (πΉββ¨βπββ©) = β¨βπββ©) |
32 | 26, 29, 31 | 3eqtrd 2777 |
. . 3
β’ (((πΉ β ran π β§ πΊ β ran π) β§ π β ((mCNβπ) β (mVRβπ))) β ((πΉ β πΊ)ββ¨βπββ©) = β¨βπββ©) |
33 | 32 | ralrimiva 3140 |
. 2
β’ ((πΉ β ran π β§ πΊ β ran π) β βπ β ((mCNβπ) β (mVRβπ))((πΉ β πΊ)ββ¨βπββ©) = β¨βπββ©) |
34 | 1, 2 | mrsubccat 34176 |
. . . . . . . 8
β’ ((πΊ β ran π β§ π₯ β (mRExβπ) β§ π¦ β (mRExβπ)) β (πΊβ(π₯ ++ π¦)) = ((πΊβπ₯) ++ (πΊβπ¦))) |
35 | 34 | 3expb 1121 |
. . . . . . 7
β’ ((πΊ β ran π β§ (π₯ β (mRExβπ) β§ π¦ β (mRExβπ))) β (πΊβ(π₯ ++ π¦)) = ((πΊβπ₯) ++ (πΊβπ¦))) |
36 | 35 | adantll 713 |
. . . . . 6
β’ (((πΉ β ran π β§ πΊ β ran π) β§ (π₯ β (mRExβπ) β§ π¦ β (mRExβπ))) β (πΊβ(π₯ ++ π¦)) = ((πΊβπ₯) ++ (πΊβπ¦))) |
37 | 36 | fveq2d 6850 |
. . . . 5
β’ (((πΉ β ran π β§ πΊ β ran π) β§ (π₯ β (mRExβπ) β§ π¦ β (mRExβπ))) β (πΉβ(πΊβ(π₯ ++ π¦))) = (πΉβ((πΊβπ₯) ++ (πΊβπ¦)))) |
38 | | simpll 766 |
. . . . . 6
β’ (((πΉ β ran π β§ πΊ β ran π) β§ (π₯ β (mRExβπ) β§ π¦ β (mRExβπ))) β πΉ β ran π) |
39 | 6 | adantr 482 |
. . . . . . 7
β’ (((πΉ β ran π β§ πΊ β ran π) β§ (π₯ β (mRExβπ) β§ π¦ β (mRExβπ))) β πΊ:(mRExβπ)βΆ(mRExβπ)) |
40 | | simprl 770 |
. . . . . . 7
β’ (((πΉ β ran π β§ πΊ β ran π) β§ (π₯ β (mRExβπ) β§ π¦ β (mRExβπ))) β π₯ β (mRExβπ)) |
41 | 39, 40 | ffvelcdmd 7040 |
. . . . . 6
β’ (((πΉ β ran π β§ πΊ β ran π) β§ (π₯ β (mRExβπ) β§ π¦ β (mRExβπ))) β (πΊβπ₯) β (mRExβπ)) |
42 | | simprr 772 |
. . . . . . 7
β’ (((πΉ β ran π β§ πΊ β ran π) β§ (π₯ β (mRExβπ) β§ π¦ β (mRExβπ))) β π¦ β (mRExβπ)) |
43 | 39, 42 | ffvelcdmd 7040 |
. . . . . 6
β’ (((πΉ β ran π β§ πΊ β ran π) β§ (π₯ β (mRExβπ) β§ π¦ β (mRExβπ))) β (πΊβπ¦) β (mRExβπ)) |
44 | 1, 2 | mrsubccat 34176 |
. . . . . 6
β’ ((πΉ β ran π β§ (πΊβπ₯) β (mRExβπ) β§ (πΊβπ¦) β (mRExβπ)) β (πΉβ((πΊβπ₯) ++ (πΊβπ¦))) = ((πΉβ(πΊβπ₯)) ++ (πΉβ(πΊβπ¦)))) |
45 | 38, 41, 43, 44 | syl3anc 1372 |
. . . . 5
β’ (((πΉ β ran π β§ πΊ β ran π) β§ (π₯ β (mRExβπ) β§ π¦ β (mRExβπ))) β (πΉβ((πΊβπ₯) ++ (πΊβπ¦))) = ((πΉβ(πΊβπ₯)) ++ (πΉβ(πΊβπ¦)))) |
46 | 37, 45 | eqtrd 2773 |
. . . 4
β’ (((πΉ β ran π β§ πΊ β ran π) β§ (π₯ β (mRExβπ) β§ π¦ β (mRExβπ))) β (πΉβ(πΊβ(π₯ ++ π¦))) = ((πΉβ(πΊβπ₯)) ++ (πΉβ(πΊβπ¦)))) |
47 | 18, 22 | syl 17 |
. . . . . . . . 9
β’ ((πΉ β ran π β§ πΊ β ran π) β (mRExβπ) = Word ((mCNβπ) βͺ (mVRβπ))) |
48 | 47 | adantr 482 |
. . . . . . . 8
β’ (((πΉ β ran π β§ πΊ β ran π) β§ (π₯ β (mRExβπ) β§ π¦ β (mRExβπ))) β (mRExβπ) = Word ((mCNβπ) βͺ (mVRβπ))) |
49 | 40, 48 | eleqtrd 2836 |
. . . . . . 7
β’ (((πΉ β ran π β§ πΊ β ran π) β§ (π₯ β (mRExβπ) β§ π¦ β (mRExβπ))) β π₯ β Word ((mCNβπ) βͺ (mVRβπ))) |
50 | 42, 48 | eleqtrd 2836 |
. . . . . . 7
β’ (((πΉ β ran π β§ πΊ β ran π) β§ (π₯ β (mRExβπ) β§ π¦ β (mRExβπ))) β π¦ β Word ((mCNβπ) βͺ (mVRβπ))) |
51 | | ccatcl 14471 |
. . . . . . 7
β’ ((π₯ β Word ((mCNβπ) βͺ (mVRβπ)) β§ π¦ β Word ((mCNβπ) βͺ (mVRβπ))) β (π₯ ++ π¦) β Word ((mCNβπ) βͺ (mVRβπ))) |
52 | 49, 50, 51 | syl2anc 585 |
. . . . . 6
β’ (((πΉ β ran π β§ πΊ β ran π) β§ (π₯ β (mRExβπ) β§ π¦ β (mRExβπ))) β (π₯ ++ π¦) β Word ((mCNβπ) βͺ (mVRβπ))) |
53 | 52, 48 | eleqtrrd 2837 |
. . . . 5
β’ (((πΉ β ran π β§ πΊ β ran π) β§ (π₯ β (mRExβπ) β§ π¦ β (mRExβπ))) β (π₯ ++ π¦) β (mRExβπ)) |
54 | | fvco3 6944 |
. . . . 5
β’ ((πΊ:(mRExβπ)βΆ(mRExβπ) β§ (π₯ ++ π¦) β (mRExβπ)) β ((πΉ β πΊ)β(π₯ ++ π¦)) = (πΉβ(πΊβ(π₯ ++ π¦)))) |
55 | 39, 53, 54 | syl2anc 585 |
. . . 4
β’ (((πΉ β ran π β§ πΊ β ran π) β§ (π₯ β (mRExβπ) β§ π¦ β (mRExβπ))) β ((πΉ β πΊ)β(π₯ ++ π¦)) = (πΉβ(πΊβ(π₯ ++ π¦)))) |
56 | | fvco3 6944 |
. . . . . 6
β’ ((πΊ:(mRExβπ)βΆ(mRExβπ) β§ π₯ β (mRExβπ)) β ((πΉ β πΊ)βπ₯) = (πΉβ(πΊβπ₯))) |
57 | 39, 40, 56 | syl2anc 585 |
. . . . 5
β’ (((πΉ β ran π β§ πΊ β ran π) β§ (π₯ β (mRExβπ) β§ π¦ β (mRExβπ))) β ((πΉ β πΊ)βπ₯) = (πΉβ(πΊβπ₯))) |
58 | | fvco3 6944 |
. . . . . 6
β’ ((πΊ:(mRExβπ)βΆ(mRExβπ) β§ π¦ β (mRExβπ)) β ((πΉ β πΊ)βπ¦) = (πΉβ(πΊβπ¦))) |
59 | 39, 42, 58 | syl2anc 585 |
. . . . 5
β’ (((πΉ β ran π β§ πΊ β ran π) β§ (π₯ β (mRExβπ) β§ π¦ β (mRExβπ))) β ((πΉ β πΊ)βπ¦) = (πΉβ(πΊβπ¦))) |
60 | 57, 59 | oveq12d 7379 |
. . . 4
β’ (((πΉ β ran π β§ πΊ β ran π) β§ (π₯ β (mRExβπ) β§ π¦ β (mRExβπ))) β (((πΉ β πΊ)βπ₯) ++ ((πΉ β πΊ)βπ¦)) = ((πΉβ(πΊβπ₯)) ++ (πΉβ(πΊβπ¦)))) |
61 | 46, 55, 60 | 3eqtr4d 2783 |
. . 3
β’ (((πΉ β ran π β§ πΊ β ran π) β§ (π₯ β (mRExβπ) β§ π¦ β (mRExβπ))) β ((πΉ β πΊ)β(π₯ ++ π¦)) = (((πΉ β πΊ)βπ₯) ++ ((πΉ β πΊ)βπ¦))) |
62 | 61 | ralrimivva 3194 |
. 2
β’ ((πΉ β ran π β§ πΊ β ran π) β βπ₯ β (mRExβπ)βπ¦ β (mRExβπ)((πΉ β πΊ)β(π₯ ++ π¦)) = (((πΉ β πΊ)βπ₯) ++ ((πΉ β πΊ)βπ¦))) |
63 | 1, 2, 21, 20 | elmrsubrn 34178 |
. . 3
β’ (π β V β ((πΉ β πΊ) β ran π β ((πΉ β πΊ):(mRExβπ)βΆ(mRExβπ) β§ βπ β ((mCNβπ) β (mVRβπ))((πΉ β πΊ)ββ¨βπββ©) = β¨βπββ© β§
βπ₯ β
(mRExβπ)βπ¦ β (mRExβπ)((πΉ β πΊ)β(π₯ ++ π¦)) = (((πΉ β πΊ)βπ₯) ++ ((πΉ β πΊ)βπ¦))))) |
64 | 18, 63 | syl 17 |
. 2
β’ ((πΉ β ran π β§ πΊ β ran π) β ((πΉ β πΊ) β ran π β ((πΉ β πΊ):(mRExβπ)βΆ(mRExβπ) β§ βπ β ((mCNβπ) β (mVRβπ))((πΉ β πΊ)ββ¨βπββ©) = β¨βπββ© β§
βπ₯ β
(mRExβπ)βπ¦ β (mRExβπ)((πΉ β πΊ)β(π₯ ++ π¦)) = (((πΉ β πΊ)βπ₯) ++ ((πΉ β πΊ)βπ¦))))) |
65 | 8, 33, 62, 64 | mpbir3and 1343 |
1
β’ ((πΉ β ran π β§ πΊ β ran π) β (πΉ β πΊ) β ran π) |