Step | Hyp | Ref
| Expression |
1 | | prdspjmhm.y |
. . 3
β’ π = (πXsπ
) |
2 | | prdspjmhm.i |
. . 3
β’ (π β πΌ β π) |
3 | | prdspjmhm.s |
. . 3
β’ (π β π β π) |
4 | | prdspjmhm.r |
. . 3
β’ (π β π
:πΌβΆMnd) |
5 | 1, 2, 3, 4 | prdsmndd 18594 |
. 2
β’ (π β π β Mnd) |
6 | | prdspjmhm.a |
. . 3
β’ (π β π΄ β πΌ) |
7 | 4, 6 | ffvelcdmd 7037 |
. 2
β’ (π β (π
βπ΄) β Mnd) |
8 | | prdspjmhm.b |
. . . . 5
β’ π΅ = (Baseβπ) |
9 | 3 | adantr 482 |
. . . . 5
β’ ((π β§ π₯ β π΅) β π β π) |
10 | 2 | adantr 482 |
. . . . 5
β’ ((π β§ π₯ β π΅) β πΌ β π) |
11 | 4 | ffnd 6670 |
. . . . . 6
β’ (π β π
Fn πΌ) |
12 | 11 | adantr 482 |
. . . . 5
β’ ((π β§ π₯ β π΅) β π
Fn πΌ) |
13 | | simpr 486 |
. . . . 5
β’ ((π β§ π₯ β π΅) β π₯ β π΅) |
14 | 6 | adantr 482 |
. . . . 5
β’ ((π β§ π₯ β π΅) β π΄ β πΌ) |
15 | 1, 8, 9, 10, 12, 13, 14 | prdsbasprj 17359 |
. . . 4
β’ ((π β§ π₯ β π΅) β (π₯βπ΄) β (Baseβ(π
βπ΄))) |
16 | 15 | fmpttd 7064 |
. . 3
β’ (π β (π₯ β π΅ β¦ (π₯βπ΄)):π΅βΆ(Baseβ(π
βπ΄))) |
17 | 3 | adantr 482 |
. . . . . 6
β’ ((π β§ (π¦ β π΅ β§ π§ β π΅)) β π β π) |
18 | 2 | adantr 482 |
. . . . . 6
β’ ((π β§ (π¦ β π΅ β§ π§ β π΅)) β πΌ β π) |
19 | 11 | adantr 482 |
. . . . . 6
β’ ((π β§ (π¦ β π΅ β§ π§ β π΅)) β π
Fn πΌ) |
20 | | simprl 770 |
. . . . . 6
β’ ((π β§ (π¦ β π΅ β§ π§ β π΅)) β π¦ β π΅) |
21 | | simprr 772 |
. . . . . 6
β’ ((π β§ (π¦ β π΅ β§ π§ β π΅)) β π§ β π΅) |
22 | | eqid 2733 |
. . . . . 6
β’
(+gβπ) = (+gβπ) |
23 | 6 | adantr 482 |
. . . . . 6
β’ ((π β§ (π¦ β π΅ β§ π§ β π΅)) β π΄ β πΌ) |
24 | 1, 8, 17, 18, 19, 20, 21, 22, 23 | prdsplusgfval 17361 |
. . . . 5
β’ ((π β§ (π¦ β π΅ β§ π§ β π΅)) β ((π¦(+gβπ)π§)βπ΄) = ((π¦βπ΄)(+gβ(π
βπ΄))(π§βπ΄))) |
25 | 8, 22 | mndcl 18569 |
. . . . . . . 8
β’ ((π β Mnd β§ π¦ β π΅ β§ π§ β π΅) β (π¦(+gβπ)π§) β π΅) |
26 | 25 | 3expb 1121 |
. . . . . . 7
β’ ((π β Mnd β§ (π¦ β π΅ β§ π§ β π΅)) β (π¦(+gβπ)π§) β π΅) |
27 | 5, 26 | sylan 581 |
. . . . . 6
β’ ((π β§ (π¦ β π΅ β§ π§ β π΅)) β (π¦(+gβπ)π§) β π΅) |
28 | | fveq1 6842 |
. . . . . . 7
β’ (π₯ = (π¦(+gβπ)π§) β (π₯βπ΄) = ((π¦(+gβπ)π§)βπ΄)) |
29 | | eqid 2733 |
. . . . . . 7
β’ (π₯ β π΅ β¦ (π₯βπ΄)) = (π₯ β π΅ β¦ (π₯βπ΄)) |
30 | | fvex 6856 |
. . . . . . 7
β’ ((π¦(+gβπ)π§)βπ΄) β V |
31 | 28, 29, 30 | fvmpt 6949 |
. . . . . 6
β’ ((π¦(+gβπ)π§) β π΅ β ((π₯ β π΅ β¦ (π₯βπ΄))β(π¦(+gβπ)π§)) = ((π¦(+gβπ)π§)βπ΄)) |
32 | 27, 31 | syl 17 |
. . . . 5
β’ ((π β§ (π¦ β π΅ β§ π§ β π΅)) β ((π₯ β π΅ β¦ (π₯βπ΄))β(π¦(+gβπ)π§)) = ((π¦(+gβπ)π§)βπ΄)) |
33 | | fveq1 6842 |
. . . . . . . 8
β’ (π₯ = π¦ β (π₯βπ΄) = (π¦βπ΄)) |
34 | | fvex 6856 |
. . . . . . . 8
β’ (π¦βπ΄) β V |
35 | 33, 29, 34 | fvmpt 6949 |
. . . . . . 7
β’ (π¦ β π΅ β ((π₯ β π΅ β¦ (π₯βπ΄))βπ¦) = (π¦βπ΄)) |
36 | | fveq1 6842 |
. . . . . . . 8
β’ (π₯ = π§ β (π₯βπ΄) = (π§βπ΄)) |
37 | | fvex 6856 |
. . . . . . . 8
β’ (π§βπ΄) β V |
38 | 36, 29, 37 | fvmpt 6949 |
. . . . . . 7
β’ (π§ β π΅ β ((π₯ β π΅ β¦ (π₯βπ΄))βπ§) = (π§βπ΄)) |
39 | 35, 38 | oveqan12d 7377 |
. . . . . 6
β’ ((π¦ β π΅ β§ π§ β π΅) β (((π₯ β π΅ β¦ (π₯βπ΄))βπ¦)(+gβ(π
βπ΄))((π₯ β π΅ β¦ (π₯βπ΄))βπ§)) = ((π¦βπ΄)(+gβ(π
βπ΄))(π§βπ΄))) |
40 | 39 | adantl 483 |
. . . . 5
β’ ((π β§ (π¦ β π΅ β§ π§ β π΅)) β (((π₯ β π΅ β¦ (π₯βπ΄))βπ¦)(+gβ(π
βπ΄))((π₯ β π΅ β¦ (π₯βπ΄))βπ§)) = ((π¦βπ΄)(+gβ(π
βπ΄))(π§βπ΄))) |
41 | 24, 32, 40 | 3eqtr4d 2783 |
. . . 4
β’ ((π β§ (π¦ β π΅ β§ π§ β π΅)) β ((π₯ β π΅ β¦ (π₯βπ΄))β(π¦(+gβπ)π§)) = (((π₯ β π΅ β¦ (π₯βπ΄))βπ¦)(+gβ(π
βπ΄))((π₯ β π΅ β¦ (π₯βπ΄))βπ§))) |
42 | 41 | ralrimivva 3194 |
. . 3
β’ (π β βπ¦ β π΅ βπ§ β π΅ ((π₯ β π΅ β¦ (π₯βπ΄))β(π¦(+gβπ)π§)) = (((π₯ β π΅ β¦ (π₯βπ΄))βπ¦)(+gβ(π
βπ΄))((π₯ β π΅ β¦ (π₯βπ΄))βπ§))) |
43 | | eqid 2733 |
. . . . . 6
β’
(0gβπ) = (0gβπ) |
44 | 8, 43 | mndidcl 18576 |
. . . . 5
β’ (π β Mnd β
(0gβπ)
β π΅) |
45 | | fveq1 6842 |
. . . . . 6
β’ (π₯ = (0gβπ) β (π₯βπ΄) = ((0gβπ)βπ΄)) |
46 | | fvex 6856 |
. . . . . 6
β’
((0gβπ)βπ΄) β V |
47 | 45, 29, 46 | fvmpt 6949 |
. . . . 5
β’
((0gβπ) β π΅ β ((π₯ β π΅ β¦ (π₯βπ΄))β(0gβπ)) = ((0gβπ)βπ΄)) |
48 | 5, 44, 47 | 3syl 18 |
. . . 4
β’ (π β ((π₯ β π΅ β¦ (π₯βπ΄))β(0gβπ)) = ((0gβπ)βπ΄)) |
49 | 1, 2, 3, 4 | prds0g 18595 |
. . . . 5
β’ (π β (0g β
π
) =
(0gβπ)) |
50 | 49 | fveq1d 6845 |
. . . 4
β’ (π β ((0g β
π
)βπ΄) = ((0gβπ)βπ΄)) |
51 | | fvco3 6941 |
. . . . 5
β’ ((π
:πΌβΆMnd β§ π΄ β πΌ) β ((0g β π
)βπ΄) = (0gβ(π
βπ΄))) |
52 | 4, 6, 51 | syl2anc 585 |
. . . 4
β’ (π β ((0g β
π
)βπ΄) = (0gβ(π
βπ΄))) |
53 | 48, 50, 52 | 3eqtr2d 2779 |
. . 3
β’ (π β ((π₯ β π΅ β¦ (π₯βπ΄))β(0gβπ)) = (0gβ(π
βπ΄))) |
54 | 16, 42, 53 | 3jca 1129 |
. 2
β’ (π β ((π₯ β π΅ β¦ (π₯βπ΄)):π΅βΆ(Baseβ(π
βπ΄)) β§ βπ¦ β π΅ βπ§ β π΅ ((π₯ β π΅ β¦ (π₯βπ΄))β(π¦(+gβπ)π§)) = (((π₯ β π΅ β¦ (π₯βπ΄))βπ¦)(+gβ(π
βπ΄))((π₯ β π΅ β¦ (π₯βπ΄))βπ§)) β§ ((π₯ β π΅ β¦ (π₯βπ΄))β(0gβπ)) = (0gβ(π
βπ΄)))) |
55 | | eqid 2733 |
. . 3
β’
(Baseβ(π
βπ΄)) = (Baseβ(π
βπ΄)) |
56 | | eqid 2733 |
. . 3
β’
(+gβ(π
βπ΄)) = (+gβ(π
βπ΄)) |
57 | | eqid 2733 |
. . 3
β’
(0gβ(π
βπ΄)) = (0gβ(π
βπ΄)) |
58 | 8, 55, 22, 56, 43, 57 | ismhm 18608 |
. 2
β’ ((π₯ β π΅ β¦ (π₯βπ΄)) β (π MndHom (π
βπ΄)) β ((π β Mnd β§ (π
βπ΄) β Mnd) β§ ((π₯ β π΅ β¦ (π₯βπ΄)):π΅βΆ(Baseβ(π
βπ΄)) β§ βπ¦ β π΅ βπ§ β π΅ ((π₯ β π΅ β¦ (π₯βπ΄))β(π¦(+gβπ)π§)) = (((π₯ β π΅ β¦ (π₯βπ΄))βπ¦)(+gβ(π
βπ΄))((π₯ β π΅ β¦ (π₯βπ΄))βπ§)) β§ ((π₯ β π΅ β¦ (π₯βπ΄))β(0gβπ)) = (0gβ(π
βπ΄))))) |
59 | 5, 7, 54, 58 | syl21anbrc 1345 |
1
β’ (π β (π₯ β π΅ β¦ (π₯βπ΄)) β (π MndHom (π
βπ΄))) |