Step | Hyp | Ref
| Expression |
1 | | eqidd 2734 |
. 2
β’ (π β (Baseβπ) = (Baseβπ)) |
2 | | eqidd 2734 |
. 2
β’ (π β (+gβπ) = (+gβπ)) |
3 | | prdsmndd.y |
. . . 4
β’ π = (πXsπ
) |
4 | | eqid 2733 |
. . . 4
β’
(Baseβπ) =
(Baseβπ) |
5 | | eqid 2733 |
. . . 4
β’
(+gβπ) = (+gβπ) |
6 | | prdsmndd.s |
. . . . . 6
β’ (π β π β π) |
7 | 6 | elexd 3495 |
. . . . 5
β’ (π β π β V) |
8 | 7 | adantr 482 |
. . . 4
β’ ((π β§ (π β (Baseβπ) β§ π β (Baseβπ))) β π β V) |
9 | | prdsmndd.i |
. . . . . 6
β’ (π β πΌ β π) |
10 | 9 | elexd 3495 |
. . . . 5
β’ (π β πΌ β V) |
11 | 10 | adantr 482 |
. . . 4
β’ ((π β§ (π β (Baseβπ) β§ π β (Baseβπ))) β πΌ β V) |
12 | | prdsmndd.r |
. . . . 5
β’ (π β π
:πΌβΆMnd) |
13 | 12 | adantr 482 |
. . . 4
β’ ((π β§ (π β (Baseβπ) β§ π β (Baseβπ))) β π
:πΌβΆMnd) |
14 | | simprl 770 |
. . . 4
β’ ((π β§ (π β (Baseβπ) β§ π β (Baseβπ))) β π β (Baseβπ)) |
15 | | simprr 772 |
. . . 4
β’ ((π β§ (π β (Baseβπ) β§ π β (Baseβπ))) β π β (Baseβπ)) |
16 | 3, 4, 5, 8, 11, 13, 14, 15 | prdsplusgcl 18656 |
. . 3
β’ ((π β§ (π β (Baseβπ) β§ π β (Baseβπ))) β (π(+gβπ)π) β (Baseβπ)) |
17 | 16 | 3impb 1116 |
. 2
β’ ((π β§ π β (Baseβπ) β§ π β (Baseβπ)) β (π(+gβπ)π) β (Baseβπ)) |
18 | 12 | ffvelcdmda 7087 |
. . . . . . 7
β’ ((π β§ π¦ β πΌ) β (π
βπ¦) β Mnd) |
19 | 18 | adantlr 714 |
. . . . . 6
β’ (((π β§ (π β (Baseβπ) β§ π β (Baseβπ) β§ π β (Baseβπ))) β§ π¦ β πΌ) β (π
βπ¦) β Mnd) |
20 | 7 | ad2antrr 725 |
. . . . . . 7
β’ (((π β§ (π β (Baseβπ) β§ π β (Baseβπ) β§ π β (Baseβπ))) β§ π¦ β πΌ) β π β V) |
21 | 10 | ad2antrr 725 |
. . . . . . 7
β’ (((π β§ (π β (Baseβπ) β§ π β (Baseβπ) β§ π β (Baseβπ))) β§ π¦ β πΌ) β πΌ β V) |
22 | 12 | ffnd 6719 |
. . . . . . . 8
β’ (π β π
Fn πΌ) |
23 | 22 | ad2antrr 725 |
. . . . . . 7
β’ (((π β§ (π β (Baseβπ) β§ π β (Baseβπ) β§ π β (Baseβπ))) β§ π¦ β πΌ) β π
Fn πΌ) |
24 | | simplr1 1216 |
. . . . . . 7
β’ (((π β§ (π β (Baseβπ) β§ π β (Baseβπ) β§ π β (Baseβπ))) β§ π¦ β πΌ) β π β (Baseβπ)) |
25 | | simpr 486 |
. . . . . . 7
β’ (((π β§ (π β (Baseβπ) β§ π β (Baseβπ) β§ π β (Baseβπ))) β§ π¦ β πΌ) β π¦ β πΌ) |
26 | 3, 4, 20, 21, 23, 24, 25 | prdsbasprj 17418 |
. . . . . 6
β’ (((π β§ (π β (Baseβπ) β§ π β (Baseβπ) β§ π β (Baseβπ))) β§ π¦ β πΌ) β (πβπ¦) β (Baseβ(π
βπ¦))) |
27 | | simplr2 1217 |
. . . . . . 7
β’ (((π β§ (π β (Baseβπ) β§ π β (Baseβπ) β§ π β (Baseβπ))) β§ π¦ β πΌ) β π β (Baseβπ)) |
28 | 3, 4, 20, 21, 23, 27, 25 | prdsbasprj 17418 |
. . . . . 6
β’ (((π β§ (π β (Baseβπ) β§ π β (Baseβπ) β§ π β (Baseβπ))) β§ π¦ β πΌ) β (πβπ¦) β (Baseβ(π
βπ¦))) |
29 | | simplr3 1218 |
. . . . . . 7
β’ (((π β§ (π β (Baseβπ) β§ π β (Baseβπ) β§ π β (Baseβπ))) β§ π¦ β πΌ) β π β (Baseβπ)) |
30 | 3, 4, 20, 21, 23, 29, 25 | prdsbasprj 17418 |
. . . . . 6
β’ (((π β§ (π β (Baseβπ) β§ π β (Baseβπ) β§ π β (Baseβπ))) β§ π¦ β πΌ) β (πβπ¦) β (Baseβ(π
βπ¦))) |
31 | | eqid 2733 |
. . . . . . 7
β’
(Baseβ(π
βπ¦)) = (Baseβ(π
βπ¦)) |
32 | | eqid 2733 |
. . . . . . 7
β’
(+gβ(π
βπ¦)) = (+gβ(π
βπ¦)) |
33 | 31, 32 | mndass 18634 |
. . . . . 6
β’ (((π
βπ¦) β Mnd β§ ((πβπ¦) β (Baseβ(π
βπ¦)) β§ (πβπ¦) β (Baseβ(π
βπ¦)) β§ (πβπ¦) β (Baseβ(π
βπ¦)))) β (((πβπ¦)(+gβ(π
βπ¦))(πβπ¦))(+gβ(π
βπ¦))(πβπ¦)) = ((πβπ¦)(+gβ(π
βπ¦))((πβπ¦)(+gβ(π
βπ¦))(πβπ¦)))) |
34 | 19, 26, 28, 30, 33 | syl13anc 1373 |
. . . . 5
β’ (((π β§ (π β (Baseβπ) β§ π β (Baseβπ) β§ π β (Baseβπ))) β§ π¦ β πΌ) β (((πβπ¦)(+gβ(π
βπ¦))(πβπ¦))(+gβ(π
βπ¦))(πβπ¦)) = ((πβπ¦)(+gβ(π
βπ¦))((πβπ¦)(+gβ(π
βπ¦))(πβπ¦)))) |
35 | 3, 4, 20, 21, 23, 24, 27, 5, 25 | prdsplusgfval 17420 |
. . . . . 6
β’ (((π β§ (π β (Baseβπ) β§ π β (Baseβπ) β§ π β (Baseβπ))) β§ π¦ β πΌ) β ((π(+gβπ)π)βπ¦) = ((πβπ¦)(+gβ(π
βπ¦))(πβπ¦))) |
36 | 35 | oveq1d 7424 |
. . . . 5
β’ (((π β§ (π β (Baseβπ) β§ π β (Baseβπ) β§ π β (Baseβπ))) β§ π¦ β πΌ) β (((π(+gβπ)π)βπ¦)(+gβ(π
βπ¦))(πβπ¦)) = (((πβπ¦)(+gβ(π
βπ¦))(πβπ¦))(+gβ(π
βπ¦))(πβπ¦))) |
37 | 3, 4, 20, 21, 23, 27, 29, 5, 25 | prdsplusgfval 17420 |
. . . . . 6
β’ (((π β§ (π β (Baseβπ) β§ π β (Baseβπ) β§ π β (Baseβπ))) β§ π¦ β πΌ) β ((π(+gβπ)π)βπ¦) = ((πβπ¦)(+gβ(π
βπ¦))(πβπ¦))) |
38 | 37 | oveq2d 7425 |
. . . . 5
β’ (((π β§ (π β (Baseβπ) β§ π β (Baseβπ) β§ π β (Baseβπ))) β§ π¦ β πΌ) β ((πβπ¦)(+gβ(π
βπ¦))((π(+gβπ)π)βπ¦)) = ((πβπ¦)(+gβ(π
βπ¦))((πβπ¦)(+gβ(π
βπ¦))(πβπ¦)))) |
39 | 34, 36, 38 | 3eqtr4d 2783 |
. . . 4
β’ (((π β§ (π β (Baseβπ) β§ π β (Baseβπ) β§ π β (Baseβπ))) β§ π¦ β πΌ) β (((π(+gβπ)π)βπ¦)(+gβ(π
βπ¦))(πβπ¦)) = ((πβπ¦)(+gβ(π
βπ¦))((π(+gβπ)π)βπ¦))) |
40 | 39 | mpteq2dva 5249 |
. . 3
β’ ((π β§ (π β (Baseβπ) β§ π β (Baseβπ) β§ π β (Baseβπ))) β (π¦ β πΌ β¦ (((π(+gβπ)π)βπ¦)(+gβ(π
βπ¦))(πβπ¦))) = (π¦ β πΌ β¦ ((πβπ¦)(+gβ(π
βπ¦))((π(+gβπ)π)βπ¦)))) |
41 | 7 | adantr 482 |
. . . 4
β’ ((π β§ (π β (Baseβπ) β§ π β (Baseβπ) β§ π β (Baseβπ))) β π β V) |
42 | 10 | adantr 482 |
. . . 4
β’ ((π β§ (π β (Baseβπ) β§ π β (Baseβπ) β§ π β (Baseβπ))) β πΌ β V) |
43 | 22 | adantr 482 |
. . . 4
β’ ((π β§ (π β (Baseβπ) β§ π β (Baseβπ) β§ π β (Baseβπ))) β π
Fn πΌ) |
44 | 16 | 3adantr3 1172 |
. . . 4
β’ ((π β§ (π β (Baseβπ) β§ π β (Baseβπ) β§ π β (Baseβπ))) β (π(+gβπ)π) β (Baseβπ)) |
45 | | simpr3 1197 |
. . . 4
β’ ((π β§ (π β (Baseβπ) β§ π β (Baseβπ) β§ π β (Baseβπ))) β π β (Baseβπ)) |
46 | 3, 4, 41, 42, 43, 44, 45, 5 | prdsplusgval 17419 |
. . 3
β’ ((π β§ (π β (Baseβπ) β§ π β (Baseβπ) β§ π β (Baseβπ))) β ((π(+gβπ)π)(+gβπ)π) = (π¦ β πΌ β¦ (((π(+gβπ)π)βπ¦)(+gβ(π
βπ¦))(πβπ¦)))) |
47 | | simpr1 1195 |
. . . 4
β’ ((π β§ (π β (Baseβπ) β§ π β (Baseβπ) β§ π β (Baseβπ))) β π β (Baseβπ)) |
48 | 12 | adantr 482 |
. . . . 5
β’ ((π β§ (π β (Baseβπ) β§ π β (Baseβπ) β§ π β (Baseβπ))) β π
:πΌβΆMnd) |
49 | | simpr2 1196 |
. . . . 5
β’ ((π β§ (π β (Baseβπ) β§ π β (Baseβπ) β§ π β (Baseβπ))) β π β (Baseβπ)) |
50 | 3, 4, 5, 41, 42, 48, 49, 45 | prdsplusgcl 18656 |
. . . 4
β’ ((π β§ (π β (Baseβπ) β§ π β (Baseβπ) β§ π β (Baseβπ))) β (π(+gβπ)π) β (Baseβπ)) |
51 | 3, 4, 41, 42, 43, 47, 50, 5 | prdsplusgval 17419 |
. . 3
β’ ((π β§ (π β (Baseβπ) β§ π β (Baseβπ) β§ π β (Baseβπ))) β (π(+gβπ)(π(+gβπ)π)) = (π¦ β πΌ β¦ ((πβπ¦)(+gβ(π
βπ¦))((π(+gβπ)π)βπ¦)))) |
52 | 40, 46, 51 | 3eqtr4d 2783 |
. 2
β’ ((π β§ (π β (Baseβπ) β§ π β (Baseβπ) β§ π β (Baseβπ))) β ((π(+gβπ)π)(+gβπ)π) = (π(+gβπ)(π(+gβπ)π))) |
53 | | eqid 2733 |
. . . 4
β’
(0g β π
) = (0g β π
) |
54 | 3, 4, 5, 7, 10, 12, 53 | prdsidlem 18657 |
. . 3
β’ (π β ((0g β
π
) β (Baseβπ) β§ βπ β (Baseβπ)(((0g β π
)(+gβπ)π) = π β§ (π(+gβπ)(0g β π
)) = π))) |
55 | 54 | simpld 496 |
. 2
β’ (π β (0g β
π
) β (Baseβπ)) |
56 | 54 | simprd 497 |
. . . 4
β’ (π β βπ β (Baseβπ)(((0g β π
)(+gβπ)π) = π β§ (π(+gβπ)(0g β π
)) = π)) |
57 | 56 | r19.21bi 3249 |
. . 3
β’ ((π β§ π β (Baseβπ)) β (((0g β π
)(+gβπ)π) = π β§ (π(+gβπ)(0g β π
)) = π)) |
58 | 57 | simpld 496 |
. 2
β’ ((π β§ π β (Baseβπ)) β ((0g β π
)(+gβπ)π) = π) |
59 | 57 | simprd 497 |
. 2
β’ ((π β§ π β (Baseβπ)) β (π(+gβπ)(0g β π
)) = π) |
60 | 1, 2, 17, 52, 55, 58, 59 | ismndd 18647 |
1
β’ (π β π β Mnd) |