Step | Hyp | Ref
| Expression |
1 | | mrsubccat.s |
. . . 4
β’ π = (mRSubstβπ) |
2 | | mrsubccat.r |
. . . 4
β’ π
= (mRExβπ) |
3 | 1, 2 | mrsubf 34497 |
. . 3
β’ (πΉ β ran π β πΉ:π
βΆπ
) |
4 | | mrsubcn.v |
. . . . 5
β’ π = (mVRβπ) |
5 | | mrsubcn.c |
. . . . 5
β’ πΆ = (mCNβπ) |
6 | 1, 2, 4, 5 | mrsubcn 34499 |
. . . 4
β’ ((πΉ β ran π β§ π β (πΆ β π)) β (πΉββ¨βπββ©) = β¨βπββ©) |
7 | 6 | ralrimiva 3147 |
. . 3
β’ (πΉ β ran π β βπ β (πΆ β π)(πΉββ¨βπββ©) = β¨βπββ©) |
8 | 1, 2 | mrsubccat 34498 |
. . . . 5
β’ ((πΉ β ran π β§ π₯ β π
β§ π¦ β π
) β (πΉβ(π₯ ++ π¦)) = ((πΉβπ₯) ++ (πΉβπ¦))) |
9 | 8 | 3expb 1121 |
. . . 4
β’ ((πΉ β ran π β§ (π₯ β π
β§ π¦ β π
)) β (πΉβ(π₯ ++ π¦)) = ((πΉβπ₯) ++ (πΉβπ¦))) |
10 | 9 | ralrimivva 3201 |
. . 3
β’ (πΉ β ran π β βπ₯ β π
βπ¦ β π
(πΉβ(π₯ ++ π¦)) = ((πΉβπ₯) ++ (πΉβπ¦))) |
11 | 3, 7, 10 | 3jca 1129 |
. 2
β’ (πΉ β ran π β (πΉ:π
βΆπ
β§ βπ β (πΆ β π)(πΉββ¨βπββ©) = β¨βπββ© β§
βπ₯ β π
βπ¦ β π
(πΉβ(π₯ ++ π¦)) = ((πΉβπ₯) ++ (πΉβπ¦)))) |
12 | 5, 4, 2 | mrexval 34481 |
. . . . . . 7
β’ (π β π β π
= Word (πΆ βͺ π)) |
13 | 12 | adantr 482 |
. . . . . 6
β’ ((π β π β§ (πΉ:π
βΆπ
β§ βπ β (πΆ β π)(πΉββ¨βπββ©) = β¨βπββ© β§
βπ₯ β π
βπ¦ β π
(πΉβ(π₯ ++ π¦)) = ((πΉβπ₯) ++ (πΉβπ¦)))) β π
= Word (πΆ βͺ π)) |
14 | | s1eq 14547 |
. . . . . . . . . . . . 13
β’ (π€ = π£ β β¨βπ€ββ© = β¨βπ£ββ©) |
15 | 14 | fveq2d 6893 |
. . . . . . . . . . . 12
β’ (π€ = π£ β (πΉββ¨βπ€ββ©) = (πΉββ¨βπ£ββ©)) |
16 | | eqid 2733 |
. . . . . . . . . . . 12
β’ (π€ β π β¦ (πΉββ¨βπ€ββ©)) = (π€ β π β¦ (πΉββ¨βπ€ββ©)) |
17 | | fvex 6902 |
. . . . . . . . . . . 12
β’ (πΉββ¨βπ£ββ©) β
V |
18 | 15, 16, 17 | fvmpt 6996 |
. . . . . . . . . . 11
β’ (π£ β π β ((π€ β π β¦ (πΉββ¨βπ€ββ©))βπ£) = (πΉββ¨βπ£ββ©)) |
19 | 18 | adantl 483 |
. . . . . . . . . 10
β’ ((((π β π β§ (πΉ:π
βΆπ
β§ βπ β (πΆ β π)(πΉββ¨βπββ©) = β¨βπββ© β§
βπ₯ β π
βπ¦ β π
(πΉβ(π₯ ++ π¦)) = ((πΉβπ₯) ++ (πΉβπ¦)))) β§ π£ β (πΆ βͺ π)) β§ π£ β π) β ((π€ β π β¦ (πΉββ¨βπ€ββ©))βπ£) = (πΉββ¨βπ£ββ©)) |
20 | | difun2 4480 |
. . . . . . . . . . . . . . 15
β’ ((πΆ βͺ π) β π) = (πΆ β π) |
21 | 20 | eleq2i 2826 |
. . . . . . . . . . . . . 14
β’ (π£ β ((πΆ βͺ π) β π) β π£ β (πΆ β π)) |
22 | | eldif 3958 |
. . . . . . . . . . . . . 14
β’ (π£ β ((πΆ βͺ π) β π) β (π£ β (πΆ βͺ π) β§ Β¬ π£ β π)) |
23 | 21, 22 | bitr3i 277 |
. . . . . . . . . . . . 13
β’ (π£ β (πΆ β π) β (π£ β (πΆ βͺ π) β§ Β¬ π£ β π)) |
24 | | simpr2 1196 |
. . . . . . . . . . . . . 14
β’ ((π β π β§ (πΉ:π
βΆπ
β§ βπ β (πΆ β π)(πΉββ¨βπββ©) = β¨βπββ© β§
βπ₯ β π
βπ¦ β π
(πΉβ(π₯ ++ π¦)) = ((πΉβπ₯) ++ (πΉβπ¦)))) β βπ β (πΆ β π)(πΉββ¨βπββ©) = β¨βπββ©) |
25 | | s1eq 14547 |
. . . . . . . . . . . . . . . . 17
β’ (π = π£ β β¨βπββ© = β¨βπ£ββ©) |
26 | 25 | fveq2d 6893 |
. . . . . . . . . . . . . . . 16
β’ (π = π£ β (πΉββ¨βπββ©) = (πΉββ¨βπ£ββ©)) |
27 | 26, 25 | eqeq12d 2749 |
. . . . . . . . . . . . . . 15
β’ (π = π£ β ((πΉββ¨βπββ©) = β¨βπββ© β (πΉββ¨βπ£ββ©) =
β¨βπ£ββ©)) |
28 | 27 | rspccva 3612 |
. . . . . . . . . . . . . 14
β’
((βπ β
(πΆ β π)(πΉββ¨βπββ©) = β¨βπββ© β§ π£ β (πΆ β π)) β (πΉββ¨βπ£ββ©) = β¨βπ£ββ©) |
29 | 24, 28 | sylan 581 |
. . . . . . . . . . . . 13
β’ (((π β π β§ (πΉ:π
βΆπ
β§ βπ β (πΆ β π)(πΉββ¨βπββ©) = β¨βπββ© β§
βπ₯ β π
βπ¦ β π
(πΉβ(π₯ ++ π¦)) = ((πΉβπ₯) ++ (πΉβπ¦)))) β§ π£ β (πΆ β π)) β (πΉββ¨βπ£ββ©) = β¨βπ£ββ©) |
30 | 23, 29 | sylan2br 596 |
. . . . . . . . . . . 12
β’ (((π β π β§ (πΉ:π
βΆπ
β§ βπ β (πΆ β π)(πΉββ¨βπββ©) = β¨βπββ© β§
βπ₯ β π
βπ¦ β π
(πΉβ(π₯ ++ π¦)) = ((πΉβπ₯) ++ (πΉβπ¦)))) β§ (π£ β (πΆ βͺ π) β§ Β¬ π£ β π)) β (πΉββ¨βπ£ββ©) = β¨βπ£ββ©) |
31 | 30 | anassrs 469 |
. . . . . . . . . . 11
β’ ((((π β π β§ (πΉ:π
βΆπ
β§ βπ β (πΆ β π)(πΉββ¨βπββ©) = β¨βπββ© β§
βπ₯ β π
βπ¦ β π
(πΉβ(π₯ ++ π¦)) = ((πΉβπ₯) ++ (πΉβπ¦)))) β§ π£ β (πΆ βͺ π)) β§ Β¬ π£ β π) β (πΉββ¨βπ£ββ©) = β¨βπ£ββ©) |
32 | 31 | eqcomd 2739 |
. . . . . . . . . 10
β’ ((((π β π β§ (πΉ:π
βΆπ
β§ βπ β (πΆ β π)(πΉββ¨βπββ©) = β¨βπββ© β§
βπ₯ β π
βπ¦ β π
(πΉβ(π₯ ++ π¦)) = ((πΉβπ₯) ++ (πΉβπ¦)))) β§ π£ β (πΆ βͺ π)) β§ Β¬ π£ β π) β β¨βπ£ββ© = (πΉββ¨βπ£ββ©)) |
33 | 19, 32 | ifeqda 4564 |
. . . . . . . . 9
β’ (((π β π β§ (πΉ:π
βΆπ
β§ βπ β (πΆ β π)(πΉββ¨βπββ©) = β¨βπββ© β§
βπ₯ β π
βπ¦ β π
(πΉβ(π₯ ++ π¦)) = ((πΉβπ₯) ++ (πΉβπ¦)))) β§ π£ β (πΆ βͺ π)) β if(π£ β π, ((π€ β π β¦ (πΉββ¨βπ€ββ©))βπ£), β¨βπ£ββ©) = (πΉββ¨βπ£ββ©)) |
34 | 33 | mpteq2dva 5248 |
. . . . . . . 8
β’ ((π β π β§ (πΉ:π
βΆπ
β§ βπ β (πΆ β π)(πΉββ¨βπββ©) = β¨βπββ© β§
βπ₯ β π
βπ¦ β π
(πΉβ(π₯ ++ π¦)) = ((πΉβπ₯) ++ (πΉβπ¦)))) β (π£ β (πΆ βͺ π) β¦ if(π£ β π, ((π€ β π β¦ (πΉββ¨βπ€ββ©))βπ£), β¨βπ£ββ©)) = (π£ β (πΆ βͺ π) β¦ (πΉββ¨βπ£ββ©))) |
35 | 34 | coeq1d 5860 |
. . . . . . 7
β’ ((π β π β§ (πΉ:π
βΆπ
β§ βπ β (πΆ β π)(πΉββ¨βπββ©) = β¨βπββ© β§
βπ₯ β π
βπ¦ β π
(πΉβ(π₯ ++ π¦)) = ((πΉβπ₯) ++ (πΉβπ¦)))) β ((π£ β (πΆ βͺ π) β¦ if(π£ β π, ((π€ β π β¦ (πΉββ¨βπ€ββ©))βπ£), β¨βπ£ββ©)) β π) = ((π£ β (πΆ βͺ π) β¦ (πΉββ¨βπ£ββ©)) β π)) |
36 | 35 | oveq2d 7422 |
. . . . . 6
β’ ((π β π β§ (πΉ:π
βΆπ
β§ βπ β (πΆ β π)(πΉββ¨βπββ©) = β¨βπββ© β§
βπ₯ β π
βπ¦ β π
(πΉβ(π₯ ++ π¦)) = ((πΉβπ₯) ++ (πΉβπ¦)))) β ((freeMndβ(πΆ βͺ π)) Ξ£g ((π£ β (πΆ βͺ π) β¦ if(π£ β π, ((π€ β π β¦ (πΉββ¨βπ€ββ©))βπ£), β¨βπ£ββ©)) β π)) = ((freeMndβ(πΆ βͺ π)) Ξ£g ((π£ β (πΆ βͺ π) β¦ (πΉββ¨βπ£ββ©)) β π))) |
37 | 13, 36 | mpteq12dv 5239 |
. . . . 5
β’ ((π β π β§ (πΉ:π
βΆπ
β§ βπ β (πΆ β π)(πΉββ¨βπββ©) = β¨βπββ© β§
βπ₯ β π
βπ¦ β π
(πΉβ(π₯ ++ π¦)) = ((πΉβπ₯) ++ (πΉβπ¦)))) β (π β π
β¦ ((freeMndβ(πΆ βͺ π)) Ξ£g ((π£ β (πΆ βͺ π) β¦ if(π£ β π, ((π€ β π β¦ (πΉββ¨βπ€ββ©))βπ£), β¨βπ£ββ©)) β π))) = (π β Word (πΆ βͺ π) β¦ ((freeMndβ(πΆ βͺ π)) Ξ£g ((π£ β (πΆ βͺ π) β¦ (πΉββ¨βπ£ββ©)) β π)))) |
38 | | elun2 4177 |
. . . . . . . 8
β’ (π£ β π β π£ β (πΆ βͺ π)) |
39 | | simplr1 1216 |
. . . . . . . . 9
β’ (((π β π β§ (πΉ:π
βΆπ
β§ βπ β (πΆ β π)(πΉββ¨βπββ©) = β¨βπββ© β§
βπ₯ β π
βπ¦ β π
(πΉβ(π₯ ++ π¦)) = ((πΉβπ₯) ++ (πΉβπ¦)))) β§ π£ β (πΆ βͺ π)) β πΉ:π
βΆπ
) |
40 | | simpr 486 |
. . . . . . . . . . 11
β’ (((π β π β§ (πΉ:π
βΆπ
β§ βπ β (πΆ β π)(πΉββ¨βπββ©) = β¨βπββ© β§
βπ₯ β π
βπ¦ β π
(πΉβ(π₯ ++ π¦)) = ((πΉβπ₯) ++ (πΉβπ¦)))) β§ π£ β (πΆ βͺ π)) β π£ β (πΆ βͺ π)) |
41 | 40 | s1cld 14550 |
. . . . . . . . . 10
β’ (((π β π β§ (πΉ:π
βΆπ
β§ βπ β (πΆ β π)(πΉββ¨βπββ©) = β¨βπββ© β§
βπ₯ β π
βπ¦ β π
(πΉβ(π₯ ++ π¦)) = ((πΉβπ₯) ++ (πΉβπ¦)))) β§ π£ β (πΆ βͺ π)) β β¨βπ£ββ© β Word (πΆ βͺ π)) |
42 | 12 | ad2antrr 725 |
. . . . . . . . . 10
β’ (((π β π β§ (πΉ:π
βΆπ
β§ βπ β (πΆ β π)(πΉββ¨βπββ©) = β¨βπββ© β§
βπ₯ β π
βπ¦ β π
(πΉβ(π₯ ++ π¦)) = ((πΉβπ₯) ++ (πΉβπ¦)))) β§ π£ β (πΆ βͺ π)) β π
= Word (πΆ βͺ π)) |
43 | 41, 42 | eleqtrrd 2837 |
. . . . . . . . 9
β’ (((π β π β§ (πΉ:π
βΆπ
β§ βπ β (πΆ β π)(πΉββ¨βπββ©) = β¨βπββ© β§
βπ₯ β π
βπ¦ β π
(πΉβ(π₯ ++ π¦)) = ((πΉβπ₯) ++ (πΉβπ¦)))) β§ π£ β (πΆ βͺ π)) β β¨βπ£ββ© β π
) |
44 | 39, 43 | ffvelcdmd 7085 |
. . . . . . . 8
β’ (((π β π β§ (πΉ:π
βΆπ
β§ βπ β (πΆ β π)(πΉββ¨βπββ©) = β¨βπββ© β§
βπ₯ β π
βπ¦ β π
(πΉβ(π₯ ++ π¦)) = ((πΉβπ₯) ++ (πΉβπ¦)))) β§ π£ β (πΆ βͺ π)) β (πΉββ¨βπ£ββ©) β π
) |
45 | 38, 44 | sylan2 594 |
. . . . . . 7
β’ (((π β π β§ (πΉ:π
βΆπ
β§ βπ β (πΆ β π)(πΉββ¨βπββ©) = β¨βπββ© β§
βπ₯ β π
βπ¦ β π
(πΉβ(π₯ ++ π¦)) = ((πΉβπ₯) ++ (πΉβπ¦)))) β§ π£ β π) β (πΉββ¨βπ£ββ©) β π
) |
46 | 15 | cbvmptv 5261 |
. . . . . . 7
β’ (π€ β π β¦ (πΉββ¨βπ€ββ©)) = (π£ β π β¦ (πΉββ¨βπ£ββ©)) |
47 | 45, 46 | fmptd 7111 |
. . . . . 6
β’ ((π β π β§ (πΉ:π
βΆπ
β§ βπ β (πΆ β π)(πΉββ¨βπββ©) = β¨βπββ© β§
βπ₯ β π
βπ¦ β π
(πΉβ(π₯ ++ π¦)) = ((πΉβπ₯) ++ (πΉβπ¦)))) β (π€ β π β¦ (πΉββ¨βπ€ββ©)):πβΆπ
) |
48 | | ssid 4004 |
. . . . . 6
β’ π β π |
49 | | eqid 2733 |
. . . . . . 7
β’
(freeMndβ(πΆ
βͺ π)) =
(freeMndβ(πΆ βͺ
π)) |
50 | 5, 4, 2, 1, 49 | mrsubfval 34488 |
. . . . . 6
β’ (((π€ β π β¦ (πΉββ¨βπ€ββ©)):πβΆπ
β§ π β π) β (πβ(π€ β π β¦ (πΉββ¨βπ€ββ©))) = (π β π
β¦ ((freeMndβ(πΆ βͺ π)) Ξ£g ((π£ β (πΆ βͺ π) β¦ if(π£ β π, ((π€ β π β¦ (πΉββ¨βπ€ββ©))βπ£), β¨βπ£ββ©)) β π)))) |
51 | 47, 48, 50 | sylancl 587 |
. . . . 5
β’ ((π β π β§ (πΉ:π
βΆπ
β§ βπ β (πΆ β π)(πΉββ¨βπββ©) = β¨βπββ© β§
βπ₯ β π
βπ¦ β π
(πΉβ(π₯ ++ π¦)) = ((πΉβπ₯) ++ (πΉβπ¦)))) β (πβ(π€ β π β¦ (πΉββ¨βπ€ββ©))) = (π β π
β¦ ((freeMndβ(πΆ βͺ π)) Ξ£g ((π£ β (πΆ βͺ π) β¦ if(π£ β π, ((π€ β π β¦ (πΉββ¨βπ€ββ©))βπ£), β¨βπ£ββ©)) β π)))) |
52 | 5 | fvexi 6903 |
. . . . . . . . 9
β’ πΆ β V |
53 | 4 | fvexi 6903 |
. . . . . . . . 9
β’ π β V |
54 | 52, 53 | unex 7730 |
. . . . . . . 8
β’ (πΆ βͺ π) β V |
55 | 49 | frmdmnd 18737 |
. . . . . . . 8
β’ ((πΆ βͺ π) β V β (freeMndβ(πΆ βͺ π)) β Mnd) |
56 | 54, 55 | ax-mp 5 |
. . . . . . 7
β’
(freeMndβ(πΆ
βͺ π)) β
Mnd |
57 | 56 | a1i 11 |
. . . . . 6
β’ ((π β π β§ (πΉ:π
βΆπ
β§ βπ β (πΆ β π)(πΉββ¨βπββ©) = β¨βπββ© β§
βπ₯ β π
βπ¦ β π
(πΉβ(π₯ ++ π¦)) = ((πΉβπ₯) ++ (πΉβπ¦)))) β (freeMndβ(πΆ βͺ π)) β Mnd) |
58 | 54 | a1i 11 |
. . . . . 6
β’ ((π β π β§ (πΉ:π
βΆπ
β§ βπ β (πΆ β π)(πΉββ¨βπββ©) = β¨βπββ© β§
βπ₯ β π
βπ¦ β π
(πΉβ(π₯ ++ π¦)) = ((πΉβπ₯) ++ (πΉβπ¦)))) β (πΆ βͺ π) β V) |
59 | 44, 42 | eleqtrd 2836 |
. . . . . . 7
β’ (((π β π β§ (πΉ:π
βΆπ
β§ βπ β (πΆ β π)(πΉββ¨βπββ©) = β¨βπββ© β§
βπ₯ β π
βπ¦ β π
(πΉβ(π₯ ++ π¦)) = ((πΉβπ₯) ++ (πΉβπ¦)))) β§ π£ β (πΆ βͺ π)) β (πΉββ¨βπ£ββ©) β Word (πΆ βͺ π)) |
60 | 59 | fmpttd 7112 |
. . . . . 6
β’ ((π β π β§ (πΉ:π
βΆπ
β§ βπ β (πΆ β π)(πΉββ¨βπββ©) = β¨βπββ© β§
βπ₯ β π
βπ¦ β π
(πΉβ(π₯ ++ π¦)) = ((πΉβπ₯) ++ (πΉβπ¦)))) β (π£ β (πΆ βͺ π) β¦ (πΉββ¨βπ£ββ©)):(πΆ βͺ π)βΆWord (πΆ βͺ π)) |
61 | | simpr1 1195 |
. . . . . . . 8
β’ ((π β π β§ (πΉ:π
βΆπ
β§ βπ β (πΆ β π)(πΉββ¨βπββ©) = β¨βπββ© β§
βπ₯ β π
βπ¦ β π
(πΉβ(π₯ ++ π¦)) = ((πΉβπ₯) ++ (πΉβπ¦)))) β πΉ:π
βΆπ
) |
62 | 13, 13 | feq23d 6710 |
. . . . . . . 8
β’ ((π β π β§ (πΉ:π
βΆπ
β§ βπ β (πΆ β π)(πΉββ¨βπββ©) = β¨βπββ© β§
βπ₯ β π
βπ¦ β π
(πΉβ(π₯ ++ π¦)) = ((πΉβπ₯) ++ (πΉβπ¦)))) β (πΉ:π
βΆπ
β πΉ:Word (πΆ βͺ π)βΆWord (πΆ βͺ π))) |
63 | 61, 62 | mpbid 231 |
. . . . . . 7
β’ ((π β π β§ (πΉ:π
βΆπ
β§ βπ β (πΆ β π)(πΉββ¨βπββ©) = β¨βπββ© β§
βπ₯ β π
βπ¦ β π
(πΉβ(π₯ ++ π¦)) = ((πΉβπ₯) ++ (πΉβπ¦)))) β πΉ:Word (πΆ βͺ π)βΆWord (πΆ βͺ π)) |
64 | | simpr3 1197 |
. . . . . . . 8
β’ ((π β π β§ (πΉ:π
βΆπ
β§ βπ β (πΆ β π)(πΉββ¨βπββ©) = β¨βπββ© β§
βπ₯ β π
βπ¦ β π
(πΉβ(π₯ ++ π¦)) = ((πΉβπ₯) ++ (πΉβπ¦)))) β βπ₯ β π
βπ¦ β π
(πΉβ(π₯ ++ π¦)) = ((πΉβπ₯) ++ (πΉβπ¦))) |
65 | | simprl 770 |
. . . . . . . . . . . . . . 15
β’ (((π β π β§ πΉ:π
βΆπ
) β§ (π₯ β π
β§ π¦ β π
)) β π₯ β π
) |
66 | 12 | adantr 482 |
. . . . . . . . . . . . . . . 16
β’ ((π β π β§ πΉ:π
βΆπ
) β π
= Word (πΆ βͺ π)) |
67 | 66 | adantr 482 |
. . . . . . . . . . . . . . 15
β’ (((π β π β§ πΉ:π
βΆπ
) β§ (π₯ β π
β§ π¦ β π
)) β π
= Word (πΆ βͺ π)) |
68 | 65, 67 | eleqtrd 2836 |
. . . . . . . . . . . . . 14
β’ (((π β π β§ πΉ:π
βΆπ
) β§ (π₯ β π
β§ π¦ β π
)) β π₯ β Word (πΆ βͺ π)) |
69 | | simprr 772 |
. . . . . . . . . . . . . . 15
β’ (((π β π β§ πΉ:π
βΆπ
) β§ (π₯ β π
β§ π¦ β π
)) β π¦ β π
) |
70 | 69, 67 | eleqtrd 2836 |
. . . . . . . . . . . . . 14
β’ (((π β π β§ πΉ:π
βΆπ
) β§ (π₯ β π
β§ π¦ β π
)) β π¦ β Word (πΆ βͺ π)) |
71 | | eqid 2733 |
. . . . . . . . . . . . . . . . . 18
β’
(Baseβ(freeMndβ(πΆ βͺ π))) = (Baseβ(freeMndβ(πΆ βͺ π))) |
72 | 49, 71 | frmdbas 18730 |
. . . . . . . . . . . . . . . . 17
β’ ((πΆ βͺ π) β V β
(Baseβ(freeMndβ(πΆ βͺ π))) = Word (πΆ βͺ π)) |
73 | 54, 72 | ax-mp 5 |
. . . . . . . . . . . . . . . 16
β’
(Baseβ(freeMndβ(πΆ βͺ π))) = Word (πΆ βͺ π) |
74 | 73 | eqcomi 2742 |
. . . . . . . . . . . . . . 15
β’ Word
(πΆ βͺ π) = (Baseβ(freeMndβ(πΆ βͺ π))) |
75 | | eqid 2733 |
. . . . . . . . . . . . . . 15
β’
(+gβ(freeMndβ(πΆ βͺ π))) =
(+gβ(freeMndβ(πΆ βͺ π))) |
76 | 49, 74, 75 | frmdadd 18733 |
. . . . . . . . . . . . . 14
β’ ((π₯ β Word (πΆ βͺ π) β§ π¦ β Word (πΆ βͺ π)) β (π₯(+gβ(freeMndβ(πΆ βͺ π)))π¦) = (π₯ ++ π¦)) |
77 | 68, 70, 76 | syl2anc 585 |
. . . . . . . . . . . . 13
β’ (((π β π β§ πΉ:π
βΆπ
) β§ (π₯ β π
β§ π¦ β π
)) β (π₯(+gβ(freeMndβ(πΆ βͺ π)))π¦) = (π₯ ++ π¦)) |
78 | 77 | fveq2d 6893 |
. . . . . . . . . . . 12
β’ (((π β π β§ πΉ:π
βΆπ
) β§ (π₯ β π
β§ π¦ β π
)) β (πΉβ(π₯(+gβ(freeMndβ(πΆ βͺ π)))π¦)) = (πΉβ(π₯ ++ π¦))) |
79 | | ffvelcdm 7081 |
. . . . . . . . . . . . . . 15
β’ ((πΉ:π
βΆπ
β§ π₯ β π
) β (πΉβπ₯) β π
) |
80 | 79 | ad2ant2lr 747 |
. . . . . . . . . . . . . 14
β’ (((π β π β§ πΉ:π
βΆπ
) β§ (π₯ β π
β§ π¦ β π
)) β (πΉβπ₯) β π
) |
81 | 80, 67 | eleqtrd 2836 |
. . . . . . . . . . . . 13
β’ (((π β π β§ πΉ:π
βΆπ
) β§ (π₯ β π
β§ π¦ β π
)) β (πΉβπ₯) β Word (πΆ βͺ π)) |
82 | | ffvelcdm 7081 |
. . . . . . . . . . . . . . 15
β’ ((πΉ:π
βΆπ
β§ π¦ β π
) β (πΉβπ¦) β π
) |
83 | 82 | ad2ant2l 745 |
. . . . . . . . . . . . . 14
β’ (((π β π β§ πΉ:π
βΆπ
) β§ (π₯ β π
β§ π¦ β π
)) β (πΉβπ¦) β π
) |
84 | 83, 67 | eleqtrd 2836 |
. . . . . . . . . . . . 13
β’ (((π β π β§ πΉ:π
βΆπ
) β§ (π₯ β π
β§ π¦ β π
)) β (πΉβπ¦) β Word (πΆ βͺ π)) |
85 | 49, 74, 75 | frmdadd 18733 |
. . . . . . . . . . . . 13
β’ (((πΉβπ₯) β Word (πΆ βͺ π) β§ (πΉβπ¦) β Word (πΆ βͺ π)) β ((πΉβπ₯)(+gβ(freeMndβ(πΆ βͺ π)))(πΉβπ¦)) = ((πΉβπ₯) ++ (πΉβπ¦))) |
86 | 81, 84, 85 | syl2anc 585 |
. . . . . . . . . . . 12
β’ (((π β π β§ πΉ:π
βΆπ
) β§ (π₯ β π
β§ π¦ β π
)) β ((πΉβπ₯)(+gβ(freeMndβ(πΆ βͺ π)))(πΉβπ¦)) = ((πΉβπ₯) ++ (πΉβπ¦))) |
87 | 78, 86 | eqeq12d 2749 |
. . . . . . . . . . 11
β’ (((π β π β§ πΉ:π
βΆπ
) β§ (π₯ β π
β§ π¦ β π
)) β ((πΉβ(π₯(+gβ(freeMndβ(πΆ βͺ π)))π¦)) = ((πΉβπ₯)(+gβ(freeMndβ(πΆ βͺ π)))(πΉβπ¦)) β (πΉβ(π₯ ++ π¦)) = ((πΉβπ₯) ++ (πΉβπ¦)))) |
88 | 87 | 2ralbidva 3217 |
. . . . . . . . . 10
β’ ((π β π β§ πΉ:π
βΆπ
) β (βπ₯ β π
βπ¦ β π
(πΉβ(π₯(+gβ(freeMndβ(πΆ βͺ π)))π¦)) = ((πΉβπ₯)(+gβ(freeMndβ(πΆ βͺ π)))(πΉβπ¦)) β βπ₯ β π
βπ¦ β π
(πΉβ(π₯ ++ π¦)) = ((πΉβπ₯) ++ (πΉβπ¦)))) |
89 | 66 | raleqdv 3326 |
. . . . . . . . . . 11
β’ ((π β π β§ πΉ:π
βΆπ
) β (βπ¦ β π
(πΉβ(π₯(+gβ(freeMndβ(πΆ βͺ π)))π¦)) = ((πΉβπ₯)(+gβ(freeMndβ(πΆ βͺ π)))(πΉβπ¦)) β βπ¦ β Word (πΆ βͺ π)(πΉβ(π₯(+gβ(freeMndβ(πΆ βͺ π)))π¦)) = ((πΉβπ₯)(+gβ(freeMndβ(πΆ βͺ π)))(πΉβπ¦)))) |
90 | 66, 89 | raleqbidv 3343 |
. . . . . . . . . 10
β’ ((π β π β§ πΉ:π
βΆπ
) β (βπ₯ β π
βπ¦ β π
(πΉβ(π₯(+gβ(freeMndβ(πΆ βͺ π)))π¦)) = ((πΉβπ₯)(+gβ(freeMndβ(πΆ βͺ π)))(πΉβπ¦)) β βπ₯ β Word (πΆ βͺ π)βπ¦ β Word (πΆ βͺ π)(πΉβ(π₯(+gβ(freeMndβ(πΆ βͺ π)))π¦)) = ((πΉβπ₯)(+gβ(freeMndβ(πΆ βͺ π)))(πΉβπ¦)))) |
91 | 88, 90 | bitr3d 281 |
. . . . . . . . 9
β’ ((π β π β§ πΉ:π
βΆπ
) β (βπ₯ β π
βπ¦ β π
(πΉβ(π₯ ++ π¦)) = ((πΉβπ₯) ++ (πΉβπ¦)) β βπ₯ β Word (πΆ βͺ π)βπ¦ β Word (πΆ βͺ π)(πΉβ(π₯(+gβ(freeMndβ(πΆ βͺ π)))π¦)) = ((πΉβπ₯)(+gβ(freeMndβ(πΆ βͺ π)))(πΉβπ¦)))) |
92 | 91 | 3ad2antr1 1189 |
. . . . . . . 8
β’ ((π β π β§ (πΉ:π
βΆπ
β§ βπ β (πΆ β π)(πΉββ¨βπββ©) = β¨βπββ© β§
βπ₯ β π
βπ¦ β π
(πΉβ(π₯ ++ π¦)) = ((πΉβπ₯) ++ (πΉβπ¦)))) β (βπ₯ β π
βπ¦ β π
(πΉβ(π₯ ++ π¦)) = ((πΉβπ₯) ++ (πΉβπ¦)) β βπ₯ β Word (πΆ βͺ π)βπ¦ β Word (πΆ βͺ π)(πΉβ(π₯(+gβ(freeMndβ(πΆ βͺ π)))π¦)) = ((πΉβπ₯)(+gβ(freeMndβ(πΆ βͺ π)))(πΉβπ¦)))) |
93 | 64, 92 | mpbid 231 |
. . . . . . 7
β’ ((π β π β§ (πΉ:π
βΆπ
β§ βπ β (πΆ β π)(πΉββ¨βπββ©) = β¨βπββ© β§
βπ₯ β π
βπ¦ β π
(πΉβ(π₯ ++ π¦)) = ((πΉβπ₯) ++ (πΉβπ¦)))) β βπ₯ β Word (πΆ βͺ π)βπ¦ β Word (πΆ βͺ π)(πΉβ(π₯(+gβ(freeMndβ(πΆ βͺ π)))π¦)) = ((πΉβπ₯)(+gβ(freeMndβ(πΆ βͺ π)))(πΉβπ¦))) |
94 | | wrd0 14486 |
. . . . . . . . . . . 12
β’ β
β Word (πΆ βͺ π) |
95 | | ffvelcdm 7081 |
. . . . . . . . . . . 12
β’ ((πΉ:Word (πΆ βͺ π)βΆWord (πΆ βͺ π) β§ β
β Word (πΆ βͺ π)) β (πΉββ
) β Word (πΆ βͺ π)) |
96 | 63, 94, 95 | sylancl 587 |
. . . . . . . . . . 11
β’ ((π β π β§ (πΉ:π
βΆπ
β§ βπ β (πΆ β π)(πΉββ¨βπββ©) = β¨βπββ© β§
βπ₯ β π
βπ¦ β π
(πΉβ(π₯ ++ π¦)) = ((πΉβπ₯) ++ (πΉβπ¦)))) β (πΉββ
) β Word (πΆ βͺ π)) |
97 | | lencl 14480 |
. . . . . . . . . . 11
β’ ((πΉββ
) β Word
(πΆ βͺ π) β (β―β(πΉββ
)) β
β0) |
98 | 96, 97 | syl 17 |
. . . . . . . . . 10
β’ ((π β π β§ (πΉ:π
βΆπ
β§ βπ β (πΆ β π)(πΉββ¨βπββ©) = β¨βπββ© β§
βπ₯ β π
βπ¦ β π
(πΉβ(π₯ ++ π¦)) = ((πΉβπ₯) ++ (πΉβπ¦)))) β (β―β(πΉββ
)) β
β0) |
99 | 98 | nn0cnd 12531 |
. . . . . . . . 9
β’ ((π β π β§ (πΉ:π
βΆπ
β§ βπ β (πΆ β π)(πΉββ¨βπββ©) = β¨βπββ© β§
βπ₯ β π
βπ¦ β π
(πΉβ(π₯ ++ π¦)) = ((πΉβπ₯) ++ (πΉβπ¦)))) β (β―β(πΉββ
)) β
β) |
100 | | 0cnd 11204 |
. . . . . . . . 9
β’ ((π β π β§ (πΉ:π
βΆπ
β§ βπ β (πΆ β π)(πΉββ¨βπββ©) = β¨βπββ© β§
βπ₯ β π
βπ¦ β π
(πΉβ(π₯ ++ π¦)) = ((πΉβπ₯) ++ (πΉβπ¦)))) β 0 β
β) |
101 | 99 | addridd 11411 |
. . . . . . . . . 10
β’ ((π β π β§ (πΉ:π
βΆπ
β§ βπ β (πΆ β π)(πΉββ¨βπββ©) = β¨βπββ© β§
βπ₯ β π
βπ¦ β π
(πΉβ(π₯ ++ π¦)) = ((πΉβπ₯) ++ (πΉβπ¦)))) β ((β―β(πΉββ
)) + 0) =
(β―β(πΉββ
))) |
102 | 94, 13 | eleqtrrid 2841 |
. . . . . . . . . . . 12
β’ ((π β π β§ (πΉ:π
βΆπ
β§ βπ β (πΆ β π)(πΉββ¨βπββ©) = β¨βπββ© β§
βπ₯ β π
βπ¦ β π
(πΉβ(π₯ ++ π¦)) = ((πΉβπ₯) ++ (πΉβπ¦)))) β β
β π
) |
103 | | fvoveq1 7429 |
. . . . . . . . . . . . . 14
β’ (π₯ = β
β (πΉβ(π₯ ++ π¦)) = (πΉβ(β
++ π¦))) |
104 | | fveq2 6889 |
. . . . . . . . . . . . . . 15
β’ (π₯ = β
β (πΉβπ₯) = (πΉββ
)) |
105 | 104 | oveq1d 7421 |
. . . . . . . . . . . . . 14
β’ (π₯ = β
β ((πΉβπ₯) ++ (πΉβπ¦)) = ((πΉββ
) ++ (πΉβπ¦))) |
106 | 103, 105 | eqeq12d 2749 |
. . . . . . . . . . . . 13
β’ (π₯ = β
β ((πΉβ(π₯ ++ π¦)) = ((πΉβπ₯) ++ (πΉβπ¦)) β (πΉβ(β
++ π¦)) = ((πΉββ
) ++ (πΉβπ¦)))) |
107 | | oveq2 7414 |
. . . . . . . . . . . . . . . 16
β’ (π¦ = β
β (β
++
π¦) = (β
++
β
)) |
108 | | ccatidid 14537 |
. . . . . . . . . . . . . . . 16
β’ (β
++ β
) = β
|
109 | 107, 108 | eqtrdi 2789 |
. . . . . . . . . . . . . . 15
β’ (π¦ = β
β (β
++
π¦) =
β
) |
110 | 109 | fveq2d 6893 |
. . . . . . . . . . . . . 14
β’ (π¦ = β
β (πΉβ(β
++ π¦)) = (πΉββ
)) |
111 | | fveq2 6889 |
. . . . . . . . . . . . . . 15
β’ (π¦ = β
β (πΉβπ¦) = (πΉββ
)) |
112 | 111 | oveq2d 7422 |
. . . . . . . . . . . . . 14
β’ (π¦ = β
β ((πΉββ
) ++ (πΉβπ¦)) = ((πΉββ
) ++ (πΉββ
))) |
113 | 110, 112 | eqeq12d 2749 |
. . . . . . . . . . . . 13
β’ (π¦ = β
β ((πΉβ(β
++ π¦)) = ((πΉββ
) ++ (πΉβπ¦)) β (πΉββ
) = ((πΉββ
) ++ (πΉββ
)))) |
114 | 106, 113 | rspc2va 3623 |
. . . . . . . . . . . 12
β’
(((β
β π
β§ β
β π
)
β§ βπ₯ β
π
βπ¦ β π
(πΉβ(π₯ ++ π¦)) = ((πΉβπ₯) ++ (πΉβπ¦))) β (πΉββ
) = ((πΉββ
) ++ (πΉββ
))) |
115 | 102, 102,
64, 114 | syl21anc 837 |
. . . . . . . . . . 11
β’ ((π β π β§ (πΉ:π
βΆπ
β§ βπ β (πΆ β π)(πΉββ¨βπββ©) = β¨βπββ© β§
βπ₯ β π
βπ¦ β π
(πΉβ(π₯ ++ π¦)) = ((πΉβπ₯) ++ (πΉβπ¦)))) β (πΉββ
) = ((πΉββ
) ++ (πΉββ
))) |
116 | 115 | fveq2d 6893 |
. . . . . . . . . 10
β’ ((π β π β§ (πΉ:π
βΆπ
β§ βπ β (πΆ β π)(πΉββ¨βπββ©) = β¨βπββ© β§
βπ₯ β π
βπ¦ β π
(πΉβ(π₯ ++ π¦)) = ((πΉβπ₯) ++ (πΉβπ¦)))) β (β―β(πΉββ
)) = (β―β((πΉββ
) ++ (πΉββ
)))) |
117 | | ccatlen 14522 |
. . . . . . . . . . 11
β’ (((πΉββ
) β Word
(πΆ βͺ π) β§ (πΉββ
) β Word (πΆ βͺ π)) β (β―β((πΉββ
) ++ (πΉββ
))) = ((β―β(πΉββ
)) +
(β―β(πΉββ
)))) |
118 | 96, 96, 117 | syl2anc 585 |
. . . . . . . . . 10
β’ ((π β π β§ (πΉ:π
βΆπ
β§ βπ β (πΆ β π)(πΉββ¨βπββ©) = β¨βπββ© β§
βπ₯ β π
βπ¦ β π
(πΉβ(π₯ ++ π¦)) = ((πΉβπ₯) ++ (πΉβπ¦)))) β (β―β((πΉββ
) ++ (πΉββ
))) =
((β―β(πΉββ
)) + (β―β(πΉββ
)))) |
119 | 101, 116,
118 | 3eqtrrd 2778 |
. . . . . . . . 9
β’ ((π β π β§ (πΉ:π
βΆπ
β§ βπ β (πΆ β π)(πΉββ¨βπββ©) = β¨βπββ© β§
βπ₯ β π
βπ¦ β π
(πΉβ(π₯ ++ π¦)) = ((πΉβπ₯) ++ (πΉβπ¦)))) β ((β―β(πΉββ
)) +
(β―β(πΉββ
))) = ((β―β(πΉββ
)) +
0)) |
120 | 99, 99, 100, 119 | addcanad 11416 |
. . . . . . . 8
β’ ((π β π β§ (πΉ:π
βΆπ
β§ βπ β (πΆ β π)(πΉββ¨βπββ©) = β¨βπββ© β§
βπ₯ β π
βπ¦ β π
(πΉβ(π₯ ++ π¦)) = ((πΉβπ₯) ++ (πΉβπ¦)))) β (β―β(πΉββ
)) = 0) |
121 | | fvex 6902 |
. . . . . . . . 9
β’ (πΉββ
) β
V |
122 | | hasheq0 14320 |
. . . . . . . . 9
β’ ((πΉββ
) β V β
((β―β(πΉββ
)) = 0 β (πΉββ
) =
β
)) |
123 | 121, 122 | ax-mp 5 |
. . . . . . . 8
β’
((β―β(πΉββ
)) = 0 β (πΉββ
) =
β
) |
124 | 120, 123 | sylib 217 |
. . . . . . 7
β’ ((π β π β§ (πΉ:π
βΆπ
β§ βπ β (πΆ β π)(πΉββ¨βπββ©) = β¨βπββ© β§
βπ₯ β π
βπ¦ β π
(πΉβ(π₯ ++ π¦)) = ((πΉβπ₯) ++ (πΉβπ¦)))) β (πΉββ
) = β
) |
125 | 56, 56 | pm3.2i 472 |
. . . . . . . 8
β’
((freeMndβ(πΆ
βͺ π)) β Mnd β§
(freeMndβ(πΆ βͺ
π)) β
Mnd) |
126 | 49 | frmd0 18738 |
. . . . . . . . 9
β’ β
=
(0gβ(freeMndβ(πΆ βͺ π))) |
127 | 74, 74, 75, 75, 126, 126 | ismhm 18670 |
. . . . . . . 8
β’ (πΉ β ((freeMndβ(πΆ βͺ π)) MndHom (freeMndβ(πΆ βͺ π))) β (((freeMndβ(πΆ βͺ π)) β Mnd β§ (freeMndβ(πΆ βͺ π)) β Mnd) β§ (πΉ:Word (πΆ βͺ π)βΆWord (πΆ βͺ π) β§ βπ₯ β Word (πΆ βͺ π)βπ¦ β Word (πΆ βͺ π)(πΉβ(π₯(+gβ(freeMndβ(πΆ βͺ π)))π¦)) = ((πΉβπ₯)(+gβ(freeMndβ(πΆ βͺ π)))(πΉβπ¦)) β§ (πΉββ
) =
β
))) |
128 | 125, 127 | mpbiran 708 |
. . . . . . 7
β’ (πΉ β ((freeMndβ(πΆ βͺ π)) MndHom (freeMndβ(πΆ βͺ π))) β (πΉ:Word (πΆ βͺ π)βΆWord (πΆ βͺ π) β§ βπ₯ β Word (πΆ βͺ π)βπ¦ β Word (πΆ βͺ π)(πΉβ(π₯(+gβ(freeMndβ(πΆ βͺ π)))π¦)) = ((πΉβπ₯)(+gβ(freeMndβ(πΆ βͺ π)))(πΉβπ¦)) β§ (πΉββ
) = β
)) |
129 | 63, 93, 124, 128 | syl3anbrc 1344 |
. . . . . 6
β’ ((π β π β§ (πΉ:π
βΆπ
β§ βπ β (πΆ β π)(πΉββ¨βπββ©) = β¨βπββ© β§
βπ₯ β π
βπ¦ β π
(πΉβ(π₯ ++ π¦)) = ((πΉβπ₯) ++ (πΉβπ¦)))) β πΉ β ((freeMndβ(πΆ βͺ π)) MndHom (freeMndβ(πΆ βͺ π)))) |
130 | | eqid 2733 |
. . . . . . . . . 10
β’
(varFMndβ(πΆ βͺ π)) = (varFMndβ(πΆ βͺ π)) |
131 | 130 | vrmdf 18736 |
. . . . . . . . 9
β’ ((πΆ βͺ π) β V β
(varFMndβ(πΆ βͺ π)):(πΆ βͺ π)βΆWord (πΆ βͺ π)) |
132 | 54, 131 | ax-mp 5 |
. . . . . . . 8
β’
(varFMndβ(πΆ βͺ π)):(πΆ βͺ π)βΆWord (πΆ βͺ π) |
133 | | fcompt 7128 |
. . . . . . . 8
β’ ((πΉ:Word (πΆ βͺ π)βΆWord (πΆ βͺ π) β§
(varFMndβ(πΆ βͺ π)):(πΆ βͺ π)βΆWord (πΆ βͺ π)) β (πΉ β
(varFMndβ(πΆ βͺ π))) = (π£ β (πΆ βͺ π) β¦ (πΉβ((varFMndβ(πΆ βͺ π))βπ£)))) |
134 | 63, 132, 133 | sylancl 587 |
. . . . . . 7
β’ ((π β π β§ (πΉ:π
βΆπ
β§ βπ β (πΆ β π)(πΉββ¨βπββ©) = β¨βπββ© β§
βπ₯ β π
βπ¦ β π
(πΉβ(π₯ ++ π¦)) = ((πΉβπ₯) ++ (πΉβπ¦)))) β (πΉ β
(varFMndβ(πΆ βͺ π))) = (π£ β (πΆ βͺ π) β¦ (πΉβ((varFMndβ(πΆ βͺ π))βπ£)))) |
135 | 130 | vrmdval 18735 |
. . . . . . . . . 10
β’ (((πΆ βͺ π) β V β§ π£ β (πΆ βͺ π)) β
((varFMndβ(πΆ βͺ π))βπ£) = β¨βπ£ββ©) |
136 | 54, 135 | mpan 689 |
. . . . . . . . 9
β’ (π£ β (πΆ βͺ π) β
((varFMndβ(πΆ βͺ π))βπ£) = β¨βπ£ββ©) |
137 | 136 | fveq2d 6893 |
. . . . . . . 8
β’ (π£ β (πΆ βͺ π) β (πΉβ((varFMndβ(πΆ βͺ π))βπ£)) = (πΉββ¨βπ£ββ©)) |
138 | 137 | mpteq2ia 5251 |
. . . . . . 7
β’ (π£ β (πΆ βͺ π) β¦ (πΉβ((varFMndβ(πΆ βͺ π))βπ£))) = (π£ β (πΆ βͺ π) β¦ (πΉββ¨βπ£ββ©)) |
139 | 134, 138 | eqtrdi 2789 |
. . . . . 6
β’ ((π β π β§ (πΉ:π
βΆπ
β§ βπ β (πΆ β π)(πΉββ¨βπββ©) = β¨βπββ© β§
βπ₯ β π
βπ¦ β π
(πΉβ(π₯ ++ π¦)) = ((πΉβπ₯) ++ (πΉβπ¦)))) β (πΉ β
(varFMndβ(πΆ βͺ π))) = (π£ β (πΆ βͺ π) β¦ (πΉββ¨βπ£ββ©))) |
140 | 49, 74, 130 | frmdup3lem 18744 |
. . . . . 6
β’
((((freeMndβ(πΆ
βͺ π)) β Mnd β§
(πΆ βͺ π) β V β§ (π£ β (πΆ βͺ π) β¦ (πΉββ¨βπ£ββ©)):(πΆ βͺ π)βΆWord (πΆ βͺ π)) β§ (πΉ β ((freeMndβ(πΆ βͺ π)) MndHom (freeMndβ(πΆ βͺ π))) β§ (πΉ β
(varFMndβ(πΆ βͺ π))) = (π£ β (πΆ βͺ π) β¦ (πΉββ¨βπ£ββ©)))) β πΉ = (π β Word (πΆ βͺ π) β¦ ((freeMndβ(πΆ βͺ π)) Ξ£g ((π£ β (πΆ βͺ π) β¦ (πΉββ¨βπ£ββ©)) β π)))) |
141 | 57, 58, 60, 129, 139, 140 | syl32anc 1379 |
. . . . 5
β’ ((π β π β§ (πΉ:π
βΆπ
β§ βπ β (πΆ β π)(πΉββ¨βπββ©) = β¨βπββ© β§
βπ₯ β π
βπ¦ β π
(πΉβ(π₯ ++ π¦)) = ((πΉβπ₯) ++ (πΉβπ¦)))) β πΉ = (π β Word (πΆ βͺ π) β¦ ((freeMndβ(πΆ βͺ π)) Ξ£g ((π£ β (πΆ βͺ π) β¦ (πΉββ¨βπ£ββ©)) β π)))) |
142 | 37, 51, 141 | 3eqtr4rd 2784 |
. . . 4
β’ ((π β π β§ (πΉ:π
βΆπ
β§ βπ β (πΆ β π)(πΉββ¨βπββ©) = β¨βπββ© β§
βπ₯ β π
βπ¦ β π
(πΉβ(π₯ ++ π¦)) = ((πΉβπ₯) ++ (πΉβπ¦)))) β πΉ = (πβ(π€ β π β¦ (πΉββ¨βπ€ββ©)))) |
143 | 4, 2, 1 | mrsubff 34492 |
. . . . . . 7
β’ (π β π β π:(π
βpm π)βΆ(π
βm π
)) |
144 | 143 | ffnd 6716 |
. . . . . 6
β’ (π β π β π Fn (π
βpm π)) |
145 | 144 | adantr 482 |
. . . . 5
β’ ((π β π β§ (πΉ:π
βΆπ
β§ βπ β (πΆ β π)(πΉββ¨βπββ©) = β¨βπββ© β§
βπ₯ β π
βπ¦ β π
(πΉβ(π₯ ++ π¦)) = ((πΉβπ₯) ++ (πΉβπ¦)))) β π Fn (π
βpm π)) |
146 | 2 | fvexi 6903 |
. . . . . . 7
β’ π
β V |
147 | | elpm2r 8836 |
. . . . . . 7
β’ (((π
β V β§ π β V) β§ ((π€ β π β¦ (πΉββ¨βπ€ββ©)):πβΆπ
β§ π β π)) β (π€ β π β¦ (πΉββ¨βπ€ββ©)) β (π
βpm π)) |
148 | 146, 53, 147 | mpanl12 701 |
. . . . . 6
β’ (((π€ β π β¦ (πΉββ¨βπ€ββ©)):πβΆπ
β§ π β π) β (π€ β π β¦ (πΉββ¨βπ€ββ©)) β (π
βpm π)) |
149 | 47, 48, 148 | sylancl 587 |
. . . . 5
β’ ((π β π β§ (πΉ:π
βΆπ
β§ βπ β (πΆ β π)(πΉββ¨βπββ©) = β¨βπββ© β§
βπ₯ β π
βπ¦ β π
(πΉβ(π₯ ++ π¦)) = ((πΉβπ₯) ++ (πΉβπ¦)))) β (π€ β π β¦ (πΉββ¨βπ€ββ©)) β (π
βpm π)) |
150 | | fnfvelrn 7080 |
. . . . 5
β’ ((π Fn (π
βpm π) β§ (π€ β π β¦ (πΉββ¨βπ€ββ©)) β (π
βpm π)) β (πβ(π€ β π β¦ (πΉββ¨βπ€ββ©))) β ran π) |
151 | 145, 149,
150 | syl2anc 585 |
. . . 4
β’ ((π β π β§ (πΉ:π
βΆπ
β§ βπ β (πΆ β π)(πΉββ¨βπββ©) = β¨βπββ© β§
βπ₯ β π
βπ¦ β π
(πΉβ(π₯ ++ π¦)) = ((πΉβπ₯) ++ (πΉβπ¦)))) β (πβ(π€ β π β¦ (πΉββ¨βπ€ββ©))) β ran π) |
152 | 142, 151 | eqeltrd 2834 |
. . 3
β’ ((π β π β§ (πΉ:π
βΆπ
β§ βπ β (πΆ β π)(πΉββ¨βπββ©) = β¨βπββ© β§
βπ₯ β π
βπ¦ β π
(πΉβ(π₯ ++ π¦)) = ((πΉβπ₯) ++ (πΉβπ¦)))) β πΉ β ran π) |
153 | 152 | ex 414 |
. 2
β’ (π β π β ((πΉ:π
βΆπ
β§ βπ β (πΆ β π)(πΉββ¨βπββ©) = β¨βπββ© β§
βπ₯ β π
βπ¦ β π
(πΉβ(π₯ ++ π¦)) = ((πΉβπ₯) ++ (πΉβπ¦))) β πΉ β ran π)) |
154 | 11, 153 | impbid2 225 |
1
β’ (π β π β (πΉ β ran π β (πΉ:π
βΆπ
β§ βπ β (πΆ β π)(πΉββ¨βπββ©) = β¨βπββ© β§
βπ₯ β π
βπ¦ β π
(πΉβ(π₯ ++ π¦)) = ((πΉβπ₯) ++ (πΉβπ¦))))) |