Step | Hyp | Ref
| Expression |
1 | | prdsidlem.z |
. . . 4
β’ 0 =
(0g β π
) |
2 | | fvexd 6858 |
. . . . 5
β’ ((π β§ π¦ β πΌ) β (π
βπ¦) β V) |
3 | | prdsplusgcl.r |
. . . . . 6
β’ (π β π
:πΌβΆMnd) |
4 | 3 | feqmptd 6911 |
. . . . 5
β’ (π β π
= (π¦ β πΌ β¦ (π
βπ¦))) |
5 | | fn0g 18523 |
. . . . . . 7
β’
0g Fn V |
6 | 5 | a1i 11 |
. . . . . 6
β’ (π β 0g Fn
V) |
7 | | dffn5 6902 |
. . . . . 6
β’
(0g Fn V β 0g = (π₯ β V β¦ (0gβπ₯))) |
8 | 6, 7 | sylib 217 |
. . . . 5
β’ (π β 0g = (π₯ β V β¦
(0gβπ₯))) |
9 | | fveq2 6843 |
. . . . 5
β’ (π₯ = (π
βπ¦) β (0gβπ₯) = (0gβ(π
βπ¦))) |
10 | 2, 4, 8, 9 | fmptco 7076 |
. . . 4
β’ (π β (0g β
π
) = (π¦ β πΌ β¦ (0gβ(π
βπ¦)))) |
11 | 1, 10 | eqtrid 2785 |
. . 3
β’ (π β 0 = (π¦ β πΌ β¦ (0gβ(π
βπ¦)))) |
12 | 3 | ffvelcdmda 7036 |
. . . . . 6
β’ ((π β§ π¦ β πΌ) β (π
βπ¦) β Mnd) |
13 | | eqid 2733 |
. . . . . . 7
β’
(Baseβ(π
βπ¦)) = (Baseβ(π
βπ¦)) |
14 | | eqid 2733 |
. . . . . . 7
β’
(0gβ(π
βπ¦)) = (0gβ(π
βπ¦)) |
15 | 13, 14 | mndidcl 18576 |
. . . . . 6
β’ ((π
βπ¦) β Mnd β
(0gβ(π
βπ¦)) β (Baseβ(π
βπ¦))) |
16 | 12, 15 | syl 17 |
. . . . 5
β’ ((π β§ π¦ β πΌ) β (0gβ(π
βπ¦)) β (Baseβ(π
βπ¦))) |
17 | 16 | ralrimiva 3140 |
. . . 4
β’ (π β βπ¦ β πΌ (0gβ(π
βπ¦)) β (Baseβ(π
βπ¦))) |
18 | | prdsplusgcl.y |
. . . . 5
β’ π = (πXsπ
) |
19 | | prdsplusgcl.b |
. . . . 5
β’ π΅ = (Baseβπ) |
20 | | prdsplusgcl.s |
. . . . 5
β’ (π β π β π) |
21 | | prdsplusgcl.i |
. . . . 5
β’ (π β πΌ β π) |
22 | 3 | ffnd 6670 |
. . . . 5
β’ (π β π
Fn πΌ) |
23 | 18, 19, 20, 21, 22 | prdsbasmpt 17357 |
. . . 4
β’ (π β ((π¦ β πΌ β¦ (0gβ(π
βπ¦))) β π΅ β βπ¦ β πΌ (0gβ(π
βπ¦)) β (Baseβ(π
βπ¦)))) |
24 | 17, 23 | mpbird 257 |
. . 3
β’ (π β (π¦ β πΌ β¦ (0gβ(π
βπ¦))) β π΅) |
25 | 11, 24 | eqeltrd 2834 |
. 2
β’ (π β 0 β π΅) |
26 | 1 | fveq1i 6844 |
. . . . . . . . . 10
β’ ( 0 βπ¦) = ((0g β
π
)βπ¦) |
27 | | fvco2 6939 |
. . . . . . . . . . 11
β’ ((π
Fn πΌ β§ π¦ β πΌ) β ((0g β π
)βπ¦) = (0gβ(π
βπ¦))) |
28 | 22, 27 | sylan 581 |
. . . . . . . . . 10
β’ ((π β§ π¦ β πΌ) β ((0g β π
)βπ¦) = (0gβ(π
βπ¦))) |
29 | 26, 28 | eqtrid 2785 |
. . . . . . . . 9
β’ ((π β§ π¦ β πΌ) β ( 0 βπ¦) = (0gβ(π
βπ¦))) |
30 | 29 | adantlr 714 |
. . . . . . . 8
β’ (((π β§ π₯ β π΅) β§ π¦ β πΌ) β ( 0 βπ¦) = (0gβ(π
βπ¦))) |
31 | 30 | oveq1d 7373 |
. . . . . . 7
β’ (((π β§ π₯ β π΅) β§ π¦ β πΌ) β (( 0 βπ¦)(+gβ(π
βπ¦))(π₯βπ¦)) = ((0gβ(π
βπ¦))(+gβ(π
βπ¦))(π₯βπ¦))) |
32 | 3 | adantr 482 |
. . . . . . . . 9
β’ ((π β§ π₯ β π΅) β π
:πΌβΆMnd) |
33 | 32 | ffvelcdmda 7036 |
. . . . . . . 8
β’ (((π β§ π₯ β π΅) β§ π¦ β πΌ) β (π
βπ¦) β Mnd) |
34 | 20 | ad2antrr 725 |
. . . . . . . . 9
β’ (((π β§ π₯ β π΅) β§ π¦ β πΌ) β π β π) |
35 | 21 | ad2antrr 725 |
. . . . . . . . 9
β’ (((π β§ π₯ β π΅) β§ π¦ β πΌ) β πΌ β π) |
36 | 22 | ad2antrr 725 |
. . . . . . . . 9
β’ (((π β§ π₯ β π΅) β§ π¦ β πΌ) β π
Fn πΌ) |
37 | | simplr 768 |
. . . . . . . . 9
β’ (((π β§ π₯ β π΅) β§ π¦ β πΌ) β π₯ β π΅) |
38 | | simpr 486 |
. . . . . . . . 9
β’ (((π β§ π₯ β π΅) β§ π¦ β πΌ) β π¦ β πΌ) |
39 | 18, 19, 34, 35, 36, 37, 38 | prdsbasprj 17359 |
. . . . . . . 8
β’ (((π β§ π₯ β π΅) β§ π¦ β πΌ) β (π₯βπ¦) β (Baseβ(π
βπ¦))) |
40 | | eqid 2733 |
. . . . . . . . 9
β’
(+gβ(π
βπ¦)) = (+gβ(π
βπ¦)) |
41 | 13, 40, 14 | mndlid 18581 |
. . . . . . . 8
β’ (((π
βπ¦) β Mnd β§ (π₯βπ¦) β (Baseβ(π
βπ¦))) β ((0gβ(π
βπ¦))(+gβ(π
βπ¦))(π₯βπ¦)) = (π₯βπ¦)) |
42 | 33, 39, 41 | syl2anc 585 |
. . . . . . 7
β’ (((π β§ π₯ β π΅) β§ π¦ β πΌ) β ((0gβ(π
βπ¦))(+gβ(π
βπ¦))(π₯βπ¦)) = (π₯βπ¦)) |
43 | 31, 42 | eqtrd 2773 |
. . . . . 6
β’ (((π β§ π₯ β π΅) β§ π¦ β πΌ) β (( 0 βπ¦)(+gβ(π
βπ¦))(π₯βπ¦)) = (π₯βπ¦)) |
44 | 43 | mpteq2dva 5206 |
. . . . 5
β’ ((π β§ π₯ β π΅) β (π¦ β πΌ β¦ (( 0 βπ¦)(+gβ(π
βπ¦))(π₯βπ¦))) = (π¦ β πΌ β¦ (π₯βπ¦))) |
45 | 20 | adantr 482 |
. . . . . 6
β’ ((π β§ π₯ β π΅) β π β π) |
46 | 21 | adantr 482 |
. . . . . 6
β’ ((π β§ π₯ β π΅) β πΌ β π) |
47 | 22 | adantr 482 |
. . . . . 6
β’ ((π β§ π₯ β π΅) β π
Fn πΌ) |
48 | 25 | adantr 482 |
. . . . . 6
β’ ((π β§ π₯ β π΅) β 0 β π΅) |
49 | | simpr 486 |
. . . . . 6
β’ ((π β§ π₯ β π΅) β π₯ β π΅) |
50 | | prdsplusgcl.p |
. . . . . 6
β’ + =
(+gβπ) |
51 | 18, 19, 45, 46, 47, 48, 49, 50 | prdsplusgval 17360 |
. . . . 5
β’ ((π β§ π₯ β π΅) β ( 0 + π₯) = (π¦ β πΌ β¦ (( 0 βπ¦)(+gβ(π
βπ¦))(π₯βπ¦)))) |
52 | 18, 19, 45, 46, 47, 49 | prdsbasfn 17358 |
. . . . . 6
β’ ((π β§ π₯ β π΅) β π₯ Fn πΌ) |
53 | | dffn5 6902 |
. . . . . 6
β’ (π₯ Fn πΌ β π₯ = (π¦ β πΌ β¦ (π₯βπ¦))) |
54 | 52, 53 | sylib 217 |
. . . . 5
β’ ((π β§ π₯ β π΅) β π₯ = (π¦ β πΌ β¦ (π₯βπ¦))) |
55 | 44, 51, 54 | 3eqtr4d 2783 |
. . . 4
β’ ((π β§ π₯ β π΅) β ( 0 + π₯) = π₯) |
56 | 30 | oveq2d 7374 |
. . . . . . 7
β’ (((π β§ π₯ β π΅) β§ π¦ β πΌ) β ((π₯βπ¦)(+gβ(π
βπ¦))( 0 βπ¦)) = ((π₯βπ¦)(+gβ(π
βπ¦))(0gβ(π
βπ¦)))) |
57 | 13, 40, 14 | mndrid 18582 |
. . . . . . . 8
β’ (((π
βπ¦) β Mnd β§ (π₯βπ¦) β (Baseβ(π
βπ¦))) β ((π₯βπ¦)(+gβ(π
βπ¦))(0gβ(π
βπ¦))) = (π₯βπ¦)) |
58 | 33, 39, 57 | syl2anc 585 |
. . . . . . 7
β’ (((π β§ π₯ β π΅) β§ π¦ β πΌ) β ((π₯βπ¦)(+gβ(π
βπ¦))(0gβ(π
βπ¦))) = (π₯βπ¦)) |
59 | 56, 58 | eqtrd 2773 |
. . . . . 6
β’ (((π β§ π₯ β π΅) β§ π¦ β πΌ) β ((π₯βπ¦)(+gβ(π
βπ¦))( 0 βπ¦)) = (π₯βπ¦)) |
60 | 59 | mpteq2dva 5206 |
. . . . 5
β’ ((π β§ π₯ β π΅) β (π¦ β πΌ β¦ ((π₯βπ¦)(+gβ(π
βπ¦))( 0 βπ¦))) = (π¦ β πΌ β¦ (π₯βπ¦))) |
61 | 18, 19, 45, 46, 47, 49, 48, 50 | prdsplusgval 17360 |
. . . . 5
β’ ((π β§ π₯ β π΅) β (π₯ + 0 ) = (π¦ β πΌ β¦ ((π₯βπ¦)(+gβ(π
βπ¦))( 0 βπ¦)))) |
62 | 60, 61, 54 | 3eqtr4d 2783 |
. . . 4
β’ ((π β§ π₯ β π΅) β (π₯ + 0 ) = π₯) |
63 | 55, 62 | jca 513 |
. . 3
β’ ((π β§ π₯ β π΅) β (( 0 + π₯) = π₯ β§ (π₯ + 0 ) = π₯)) |
64 | 63 | ralrimiva 3140 |
. 2
β’ (π β βπ₯ β π΅ (( 0 + π₯) = π₯ β§ (π₯ + 0 ) = π₯)) |
65 | 25, 64 | jca 513 |
1
β’ (π β ( 0 β π΅ β§ βπ₯ β π΅ (( 0 + π₯) = π₯ β§ (π₯ + 0 ) = π₯))) |