Step | Hyp | Ref
| Expression |
1 | | fconst6g 6781 |
. . . . 5
β’ (π β β0
β (1o Γ {π}):1oβΆβ0) |
2 | | nn0ex 12478 |
. . . . . 6
β’
β0 β V |
3 | | 1on 8478 |
. . . . . . 7
β’
1o β On |
4 | 3 | elexi 3494 |
. . . . . 6
β’
1o β V |
5 | 2, 4 | elmap 8865 |
. . . . 5
β’
((1o Γ {π}) β (β0
βm 1o) β (1o Γ {π}):1oβΆβ0) |
6 | 1, 5 | sylibr 233 |
. . . 4
β’ (π β β0
β (1o Γ {π}) β (β0
βm 1o)) |
7 | 6 | adantl 483 |
. . 3
β’ (((π
β Ring β§ πΉ β π΅ β§ πΊ β π΅) β§ π β β0) β
(1o Γ {π})
β (β0 βm 1o)) |
8 | | eqidd 2734 |
. . 3
β’ ((π
β Ring β§ πΉ β π΅ β§ πΊ β π΅) β (π β β0 β¦
(1o Γ {π})) = (π β β0 β¦
(1o Γ {π}))) |
9 | | eqid 2733 |
. . . 4
β’
(1o mPwSer π
) = (1o mPwSer π
) |
10 | | coe1mul2.s |
. . . . 5
β’ π =
(PwSer1βπ
) |
11 | | coe1mul2.b |
. . . . 5
β’ π΅ = (Baseβπ) |
12 | 10, 11, 9 | psr1bas2 21714 |
. . . 4
β’ π΅ = (Baseβ(1o
mPwSer π
)) |
13 | | coe1mul2.u |
. . . 4
β’ Β· =
(.rβπ
) |
14 | | coe1mul2.t |
. . . . 5
β’ β =
(.rβπ) |
15 | 10, 9, 14 | psr1mulr 21746 |
. . . 4
β’ β =
(.rβ(1o mPwSer π
)) |
16 | | psr1baslem 21709 |
. . . 4
β’
(β0 βm 1o) = {π β (β0
βm 1o) β£ (β‘π β β) β
Fin} |
17 | | simp2 1138 |
. . . 4
β’ ((π
β Ring β§ πΉ β π΅ β§ πΊ β π΅) β πΉ β π΅) |
18 | | simp3 1139 |
. . . 4
β’ ((π
β Ring β§ πΉ β π΅ β§ πΊ β π΅) β πΊ β π΅) |
19 | 9, 12, 13, 15, 16, 17, 18 | psrmulfval 21504 |
. . 3
β’ ((π
β Ring β§ πΉ β π΅ β§ πΊ β π΅) β (πΉ β πΊ) = (π β (β0
βm 1o) β¦ (π
Ξ£g (π β {π β (β0
βm 1o) β£ π βr β€ π} β¦ ((πΉβπ) Β· (πΊβ(π βf β π))))))) |
20 | | breq2 5153 |
. . . . . 6
β’ (π = (1o Γ {π}) β (π βr β€ π β π βr β€ (1o
Γ {π}))) |
21 | 20 | rabbidv 3441 |
. . . . 5
β’ (π = (1o Γ {π}) β {π β (β0
βm 1o) β£ π βr β€ π} = {π β (β0
βm 1o) β£ π βr β€ (1o
Γ {π})}) |
22 | | fvoveq1 7432 |
. . . . . 6
β’ (π = (1o Γ {π}) β (πΊβ(π βf β π)) = (πΊβ((1o Γ {π}) βf β
π))) |
23 | 22 | oveq2d 7425 |
. . . . 5
β’ (π = (1o Γ {π}) β ((πΉβπ) Β· (πΊβ(π βf β π))) = ((πΉβπ) Β· (πΊβ((1o Γ {π}) βf β
π)))) |
24 | 21, 23 | mpteq12dv 5240 |
. . . 4
β’ (π = (1o Γ {π}) β (π β {π β (β0
βm 1o) β£ π βr β€ π} β¦ ((πΉβπ) Β· (πΊβ(π βf β π)))) = (π β {π β (β0
βm 1o) β£ π βr β€ (1o
Γ {π})} β¦
((πΉβπ) Β· (πΊβ((1o Γ {π}) βf β
π))))) |
25 | 24 | oveq2d 7425 |
. . 3
β’ (π = (1o Γ {π}) β (π
Ξ£g (π β {π β (β0
βm 1o) β£ π βr β€ π} β¦ ((πΉβπ) Β· (πΊβ(π βf β π))))) = (π
Ξ£g (π β {π β (β0
βm 1o) β£ π βr β€ (1o
Γ {π})} β¦
((πΉβπ) Β· (πΊβ((1o Γ {π}) βf β
π)))))) |
26 | 7, 8, 19, 25 | fmptco 7127 |
. 2
β’ ((π
β Ring β§ πΉ β π΅ β§ πΊ β π΅) β ((πΉ β πΊ) β (π β β0 β¦
(1o Γ {π}))) = (π β β0 β¦ (π
Ξ£g
(π β {π β (β0
βm 1o) β£ π βr β€ (1o
Γ {π})} β¦
((πΉβπ) Β· (πΊβ((1o Γ {π}) βf β
π))))))) |
27 | 10 | psr1ring 21769 |
. . . 4
β’ (π
β Ring β π β Ring) |
28 | 11, 14 | ringcl 20073 |
. . . 4
β’ ((π β Ring β§ πΉ β π΅ β§ πΊ β π΅) β (πΉ β πΊ) β π΅) |
29 | 27, 28 | syl3an1 1164 |
. . 3
β’ ((π
β Ring β§ πΉ β π΅ β§ πΊ β π΅) β (πΉ β πΊ) β π΅) |
30 | | eqid 2733 |
. . . 4
β’
(coe1β(πΉ β πΊ)) = (coe1β(πΉ β πΊ)) |
31 | | eqid 2733 |
. . . 4
β’ (π β β0
β¦ (1o Γ {π})) = (π β β0 β¦
(1o Γ {π})) |
32 | 30, 11, 10, 31 | coe1fval3 21732 |
. . 3
β’ ((πΉ β πΊ) β π΅ β (coe1β(πΉ β πΊ)) = ((πΉ β πΊ) β (π β β0 β¦
(1o Γ {π})))) |
33 | 29, 32 | syl 17 |
. 2
β’ ((π
β Ring β§ πΉ β π΅ β§ πΊ β π΅) β (coe1β(πΉ β πΊ)) = ((πΉ β πΊ) β (π β β0 β¦
(1o Γ {π})))) |
34 | | eqid 2733 |
. . . . 5
β’
(Baseβπ
) =
(Baseβπ
) |
35 | | eqid 2733 |
. . . . 5
β’
(0gβπ
) = (0gβπ
) |
36 | | simpl1 1192 |
. . . . . 6
β’ (((π
β Ring β§ πΉ β π΅ β§ πΊ β π΅) β§ π β β0) β π
β Ring) |
37 | | ringcmn 20099 |
. . . . . 6
β’ (π
β Ring β π
β CMnd) |
38 | 36, 37 | syl 17 |
. . . . 5
β’ (((π
β Ring β§ πΉ β π΅ β§ πΊ β π΅) β§ π β β0) β π
β CMnd) |
39 | | fzfi 13937 |
. . . . . 6
β’
(0...π) β
Fin |
40 | 39 | a1i 11 |
. . . . 5
β’ (((π
β Ring β§ πΉ β π΅ β§ πΊ β π΅) β§ π β β0) β
(0...π) β
Fin) |
41 | | simpll1 1213 |
. . . . . . 7
β’ ((((π
β Ring β§ πΉ β π΅ β§ πΊ β π΅) β§ π β β0) β§ π₯ β (0...π)) β π
β Ring) |
42 | | simpll2 1214 |
. . . . . . . . 9
β’ ((((π
β Ring β§ πΉ β π΅ β§ πΊ β π΅) β§ π β β0) β§ π₯ β (0...π)) β πΉ β π΅) |
43 | | eqid 2733 |
. . . . . . . . . 10
β’
(coe1βπΉ) = (coe1βπΉ) |
44 | 43, 11, 10, 34 | coe1f2 21733 |
. . . . . . . . 9
β’ (πΉ β π΅ β (coe1βπΉ):β0βΆ(Baseβπ
)) |
45 | 42, 44 | syl 17 |
. . . . . . . 8
β’ ((((π
β Ring β§ πΉ β π΅ β§ πΊ β π΅) β§ π β β0) β§ π₯ β (0...π)) β (coe1βπΉ):β0βΆ(Baseβπ
)) |
46 | | elfznn0 13594 |
. . . . . . . . 9
β’ (π₯ β (0...π) β π₯ β β0) |
47 | 46 | adantl 483 |
. . . . . . . 8
β’ ((((π
β Ring β§ πΉ β π΅ β§ πΊ β π΅) β§ π β β0) β§ π₯ β (0...π)) β π₯ β β0) |
48 | 45, 47 | ffvelcdmd 7088 |
. . . . . . 7
β’ ((((π
β Ring β§ πΉ β π΅ β§ πΊ β π΅) β§ π β β0) β§ π₯ β (0...π)) β ((coe1βπΉ)βπ₯) β (Baseβπ
)) |
49 | | simpll3 1215 |
. . . . . . . . 9
β’ ((((π
β Ring β§ πΉ β π΅ β§ πΊ β π΅) β§ π β β0) β§ π₯ β (0...π)) β πΊ β π΅) |
50 | | eqid 2733 |
. . . . . . . . . 10
β’
(coe1βπΊ) = (coe1βπΊ) |
51 | 50, 11, 10, 34 | coe1f2 21733 |
. . . . . . . . 9
β’ (πΊ β π΅ β (coe1βπΊ):β0βΆ(Baseβπ
)) |
52 | 49, 51 | syl 17 |
. . . . . . . 8
β’ ((((π
β Ring β§ πΉ β π΅ β§ πΊ β π΅) β§ π β β0) β§ π₯ β (0...π)) β (coe1βπΊ):β0βΆ(Baseβπ
)) |
53 | | fznn0sub 13533 |
. . . . . . . . 9
β’ (π₯ β (0...π) β (π β π₯) β
β0) |
54 | 53 | adantl 483 |
. . . . . . . 8
β’ ((((π
β Ring β§ πΉ β π΅ β§ πΊ β π΅) β§ π β β0) β§ π₯ β (0...π)) β (π β π₯) β
β0) |
55 | 52, 54 | ffvelcdmd 7088 |
. . . . . . 7
β’ ((((π
β Ring β§ πΉ β π΅ β§ πΊ β π΅) β§ π β β0) β§ π₯ β (0...π)) β ((coe1βπΊ)β(π β π₯)) β (Baseβπ
)) |
56 | 34, 13 | ringcl 20073 |
. . . . . . 7
β’ ((π
β Ring β§
((coe1βπΉ)βπ₯) β (Baseβπ
) β§ ((coe1βπΊ)β(π β π₯)) β (Baseβπ
)) β (((coe1βπΉ)βπ₯) Β·
((coe1βπΊ)β(π β π₯))) β (Baseβπ
)) |
57 | 41, 48, 55, 56 | syl3anc 1372 |
. . . . . 6
β’ ((((π
β Ring β§ πΉ β π΅ β§ πΊ β π΅) β§ π β β0) β§ π₯ β (0...π)) β (((coe1βπΉ)βπ₯) Β·
((coe1βπΊ)β(π β π₯))) β (Baseβπ
)) |
58 | 57 | fmpttd 7115 |
. . . . 5
β’ (((π
β Ring β§ πΉ β π΅ β§ πΊ β π΅) β§ π β β0) β (π₯ β (0...π) β¦ (((coe1βπΉ)βπ₯) Β·
((coe1βπΊ)β(π β π₯)))):(0...π)βΆ(Baseβπ
)) |
59 | 39 | elexi 3494 |
. . . . . . . . 9
β’
(0...π) β
V |
60 | 59 | mptex 7225 |
. . . . . . . 8
β’ (π₯ β (0...π) β¦ (((coe1βπΉ)βπ₯) Β·
((coe1βπΊ)β(π β π₯)))) β V |
61 | | funmpt 6587 |
. . . . . . . 8
β’ Fun
(π₯ β (0...π) β¦
(((coe1βπΉ)βπ₯) Β·
((coe1βπΊ)β(π β π₯)))) |
62 | | fvex 6905 |
. . . . . . . 8
β’
(0gβπ
) β V |
63 | 60, 61, 62 | 3pm3.2i 1340 |
. . . . . . 7
β’ ((π₯ β (0...π) β¦ (((coe1βπΉ)βπ₯) Β·
((coe1βπΊ)β(π β π₯)))) β V β§ Fun (π₯ β (0...π) β¦ (((coe1βπΉ)βπ₯) Β·
((coe1βπΊ)β(π β π₯)))) β§ (0gβπ
) β V) |
64 | | suppssdm 8162 |
. . . . . . . . 9
β’ ((π₯ β (0...π) β¦ (((coe1βπΉ)βπ₯) Β·
((coe1βπΊ)β(π β π₯)))) supp (0gβπ
)) β dom (π₯ β (0...π) β¦ (((coe1βπΉ)βπ₯) Β·
((coe1βπΊ)β(π β π₯)))) |
65 | | eqid 2733 |
. . . . . . . . . 10
β’ (π₯ β (0...π) β¦ (((coe1βπΉ)βπ₯) Β·
((coe1βπΊ)β(π β π₯)))) = (π₯ β (0...π) β¦ (((coe1βπΉ)βπ₯) Β·
((coe1βπΊ)β(π β π₯)))) |
66 | 65 | dmmptss 6241 |
. . . . . . . . 9
β’ dom
(π₯ β (0...π) β¦
(((coe1βπΉ)βπ₯) Β·
((coe1βπΊ)β(π β π₯)))) β (0...π) |
67 | 64, 66 | sstri 3992 |
. . . . . . . 8
β’ ((π₯ β (0...π) β¦ (((coe1βπΉ)βπ₯) Β·
((coe1βπΊ)β(π β π₯)))) supp (0gβπ
)) β (0...π) |
68 | 39, 67 | pm3.2i 472 |
. . . . . . 7
β’
((0...π) β Fin
β§ ((π₯ β (0...π) β¦
(((coe1βπΉ)βπ₯) Β·
((coe1βπΊ)β(π β π₯)))) supp (0gβπ
)) β (0...π)) |
69 | | suppssfifsupp 9378 |
. . . . . . 7
β’ ((((π₯ β (0...π) β¦ (((coe1βπΉ)βπ₯) Β·
((coe1βπΊ)β(π β π₯)))) β V β§ Fun (π₯ β (0...π) β¦ (((coe1βπΉ)βπ₯) Β·
((coe1βπΊ)β(π β π₯)))) β§ (0gβπ
) β V) β§ ((0...π) β Fin β§ ((π₯ β (0...π) β¦ (((coe1βπΉ)βπ₯) Β·
((coe1βπΊ)β(π β π₯)))) supp (0gβπ
)) β (0...π))) β (π₯ β (0...π) β¦ (((coe1βπΉ)βπ₯) Β·
((coe1βπΊ)β(π β π₯)))) finSupp (0gβπ
)) |
70 | 63, 68, 69 | mp2an 691 |
. . . . . 6
β’ (π₯ β (0...π) β¦ (((coe1βπΉ)βπ₯) Β·
((coe1βπΊ)β(π β π₯)))) finSupp (0gβπ
) |
71 | 70 | a1i 11 |
. . . . 5
β’ (((π
β Ring β§ πΉ β π΅ β§ πΊ β π΅) β§ π β β0) β (π₯ β (0...π) β¦ (((coe1βπΉ)βπ₯) Β·
((coe1βπΊ)β(π β π₯)))) finSupp (0gβπ
)) |
72 | | eqid 2733 |
. . . . . . 7
β’ {π β (β0
βm 1o) β£ π βr β€ (1o
Γ {π})} = {π β (β0
βm 1o) β£ π βr β€ (1o
Γ {π})} |
73 | 72 | coe1mul2lem2 21790 |
. . . . . 6
β’ (π β β0
β (π β {π β (β0
βm 1o) β£ π βr β€ (1o
Γ {π})} β¦
(πββ
)):{π β (β0
βm 1o) β£ π βr β€ (1o
Γ {π})}β1-1-ontoβ(0...π)) |
74 | 73 | adantl 483 |
. . . . 5
β’ (((π
β Ring β§ πΉ β π΅ β§ πΊ β π΅) β§ π β β0) β (π β {π β (β0
βm 1o) β£ π βr β€ (1o
Γ {π})} β¦
(πββ
)):{π β (β0
βm 1o) β£ π βr β€ (1o
Γ {π})}β1-1-ontoβ(0...π)) |
75 | 34, 35, 38, 40, 58, 71, 74 | gsumf1o 19784 |
. . . 4
β’ (((π
β Ring β§ πΉ β π΅ β§ πΊ β π΅) β§ π β β0) β (π
Ξ£g
(π₯ β (0...π) β¦
(((coe1βπΉ)βπ₯) Β·
((coe1βπΊ)β(π β π₯))))) = (π
Ξ£g ((π₯ β (0...π) β¦ (((coe1βπΉ)βπ₯) Β·
((coe1βπΊ)β(π β π₯)))) β (π β {π β (β0
βm 1o) β£ π βr β€ (1o
Γ {π})} β¦
(πββ
))))) |
76 | | breq1 5152 |
. . . . . . . . . . 11
β’ (π = π β (π βr β€ (1o
Γ {π}) β π βr β€
(1o Γ {π}))) |
77 | 76 | elrab 3684 |
. . . . . . . . . 10
β’ (π β {π β (β0
βm 1o) β£ π βr β€ (1o
Γ {π})} β (π β (β0
βm 1o) β§ π βr β€ (1o
Γ {π}))) |
78 | 77 | simprbi 498 |
. . . . . . . . 9
β’ (π β {π β (β0
βm 1o) β£ π βr β€ (1o
Γ {π})} β π βr β€
(1o Γ {π})) |
79 | 78 | adantl 483 |
. . . . . . . 8
β’ ((((π
β Ring β§ πΉ β π΅ β§ πΊ β π΅) β§ π β β0) β§ π β {π β (β0
βm 1o) β£ π βr β€ (1o
Γ {π})}) β π βr β€
(1o Γ {π})) |
80 | | simplr 768 |
. . . . . . . . 9
β’ ((((π
β Ring β§ πΉ β π΅ β§ πΊ β π΅) β§ π β β0) β§ π β {π β (β0
βm 1o) β£ π βr β€ (1o
Γ {π})}) β π β
β0) |
81 | | elrabi 3678 |
. . . . . . . . . 10
β’ (π β {π β (β0
βm 1o) β£ π βr β€ (1o
Γ {π})} β π β (β0
βm 1o)) |
82 | 81 | adantl 483 |
. . . . . . . . 9
β’ ((((π
β Ring β§ πΉ β π΅ β§ πΊ β π΅) β§ π β β0) β§ π β {π β (β0
βm 1o) β£ π βr β€ (1o
Γ {π})}) β π β (β0
βm 1o)) |
83 | | coe1mul2lem1 21789 |
. . . . . . . . 9
β’ ((π β β0
β§ π β
(β0 βm 1o)) β (π βr β€
(1o Γ {π})
β (πββ
)
β (0...π))) |
84 | 80, 82, 83 | syl2anc 585 |
. . . . . . . 8
β’ ((((π
β Ring β§ πΉ β π΅ β§ πΊ β π΅) β§ π β β0) β§ π β {π β (β0
βm 1o) β£ π βr β€ (1o
Γ {π})}) β
(π βr β€
(1o Γ {π})
β (πββ
)
β (0...π))) |
85 | 79, 84 | mpbid 231 |
. . . . . . 7
β’ ((((π
β Ring β§ πΉ β π΅ β§ πΊ β π΅) β§ π β β0) β§ π β {π β (β0
βm 1o) β£ π βr β€ (1o
Γ {π})}) β
(πββ
) β
(0...π)) |
86 | | eqidd 2734 |
. . . . . . 7
β’ (((π
β Ring β§ πΉ β π΅ β§ πΊ β π΅) β§ π β β0) β (π β {π β (β0
βm 1o) β£ π βr β€ (1o
Γ {π})} β¦
(πββ
)) = (π β {π β (β0
βm 1o) β£ π βr β€ (1o
Γ {π})} β¦
(πββ
))) |
87 | | eqidd 2734 |
. . . . . . 7
β’ (((π
β Ring β§ πΉ β π΅ β§ πΊ β π΅) β§ π β β0) β (π₯ β (0...π) β¦ (((coe1βπΉ)βπ₯) Β·
((coe1βπΊ)β(π β π₯)))) = (π₯ β (0...π) β¦ (((coe1βπΉ)βπ₯) Β·
((coe1βπΊ)β(π β π₯))))) |
88 | | fveq2 6892 |
. . . . . . . 8
β’ (π₯ = (πββ
) β
((coe1βπΉ)βπ₯) = ((coe1βπΉ)β(πββ
))) |
89 | | oveq2 7417 |
. . . . . . . . 9
β’ (π₯ = (πββ
) β (π β π₯) = (π β (πββ
))) |
90 | 89 | fveq2d 6896 |
. . . . . . . 8
β’ (π₯ = (πββ
) β
((coe1βπΊ)β(π β π₯)) = ((coe1βπΊ)β(π β (πββ
)))) |
91 | 88, 90 | oveq12d 7427 |
. . . . . . 7
β’ (π₯ = (πββ
) β
(((coe1βπΉ)βπ₯) Β·
((coe1βπΊ)β(π β π₯))) = (((coe1βπΉ)β(πββ
)) Β·
((coe1βπΊ)β(π β (πββ
))))) |
92 | 85, 86, 87, 91 | fmptco 7127 |
. . . . . 6
β’ (((π
β Ring β§ πΉ β π΅ β§ πΊ β π΅) β§ π β β0) β ((π₯ β (0...π) β¦ (((coe1βπΉ)βπ₯) Β·
((coe1βπΊ)β(π β π₯)))) β (π β {π β (β0
βm 1o) β£ π βr β€ (1o
Γ {π})} β¦
(πββ
))) =
(π β {π β (β0
βm 1o) β£ π βr β€ (1o
Γ {π})} β¦
(((coe1βπΉ)β(πββ
)) Β·
((coe1βπΊ)β(π β (πββ
)))))) |
93 | | simpll2 1214 |
. . . . . . . . 9
β’ ((((π
β Ring β§ πΉ β π΅ β§ πΊ β π΅) β§ π β β0) β§ π β {π β (β0
βm 1o) β£ π βr β€ (1o
Γ {π})}) β πΉ β π΅) |
94 | 43 | fvcoe1 21731 |
. . . . . . . . 9
β’ ((πΉ β π΅ β§ π β (β0
βm 1o)) β (πΉβπ) = ((coe1βπΉ)β(πββ
))) |
95 | 93, 82, 94 | syl2anc 585 |
. . . . . . . 8
β’ ((((π
β Ring β§ πΉ β π΅ β§ πΊ β π΅) β§ π β β0) β§ π β {π β (β0
βm 1o) β£ π βr β€ (1o
Γ {π})}) β
(πΉβπ) = ((coe1βπΉ)β(πββ
))) |
96 | | df1o2 8473 |
. . . . . . . . . . . . . 14
β’
1o = {β
} |
97 | | 0ex 5308 |
. . . . . . . . . . . . . 14
β’ β
β V |
98 | 96, 2, 97 | mapsnconst 8886 |
. . . . . . . . . . . . 13
β’ (π β (β0
βm 1o) β π = (1o Γ {(πββ
)})) |
99 | 82, 98 | syl 17 |
. . . . . . . . . . . 12
β’ ((((π
β Ring β§ πΉ β π΅ β§ πΊ β π΅) β§ π β β0) β§ π β {π β (β0
βm 1o) β£ π βr β€ (1o
Γ {π})}) β π = (1o Γ
{(πββ
)})) |
100 | 99 | oveq2d 7425 |
. . . . . . . . . . 11
β’ ((((π
β Ring β§ πΉ β π΅ β§ πΊ β π΅) β§ π β β0) β§ π β {π β (β0
βm 1o) β£ π βr β€ (1o
Γ {π})}) β
((1o Γ {π}) βf β π) = ((1o Γ
{π}) βf
β (1o Γ {(πββ
)}))) |
101 | 3 | a1i 11 |
. . . . . . . . . . . 12
β’ ((((π
β Ring β§ πΉ β π΅ β§ πΊ β π΅) β§ π β β0) β§ π β {π β (β0
βm 1o) β£ π βr β€ (1o
Γ {π})}) β
1o β On) |
102 | | vex 3479 |
. . . . . . . . . . . . 13
β’ π β V |
103 | 102 | a1i 11 |
. . . . . . . . . . . 12
β’ ((((π
β Ring β§ πΉ β π΅ β§ πΊ β π΅) β§ π β β0) β§ π β {π β (β0
βm 1o) β£ π βr β€ (1o
Γ {π})}) β π β V) |
104 | | fvexd 6907 |
. . . . . . . . . . . 12
β’ ((((π
β Ring β§ πΉ β π΅ β§ πΊ β π΅) β§ π β β0) β§ π β {π β (β0
βm 1o) β£ π βr β€ (1o
Γ {π})}) β
(πββ
) β
V) |
105 | 101, 103,
104 | ofc12 7698 |
. . . . . . . . . . 11
β’ ((((π
β Ring β§ πΉ β π΅ β§ πΊ β π΅) β§ π β β0) β§ π β {π β (β0
βm 1o) β£ π βr β€ (1o
Γ {π})}) β
((1o Γ {π}) βf β (1o
Γ {(πββ
)})) = (1o Γ
{(π β (πββ
))})) |
106 | 100, 105 | eqtrd 2773 |
. . . . . . . . . 10
β’ ((((π
β Ring β§ πΉ β π΅ β§ πΊ β π΅) β§ π β β0) β§ π β {π β (β0
βm 1o) β£ π βr β€ (1o
Γ {π})}) β
((1o Γ {π}) βf β π) = (1o Γ
{(π β (πββ
))})) |
107 | 106 | fveq2d 6896 |
. . . . . . . . 9
β’ ((((π
β Ring β§ πΉ β π΅ β§ πΊ β π΅) β§ π β β0) β§ π β {π β (β0
βm 1o) β£ π βr β€ (1o
Γ {π})}) β
(πΊβ((1o
Γ {π})
βf β π)) = (πΊβ(1o Γ {(π β (πββ
))}))) |
108 | | simpll3 1215 |
. . . . . . . . . 10
β’ ((((π
β Ring β§ πΉ β π΅ β§ πΊ β π΅) β§ π β β0) β§ π β {π β (β0
βm 1o) β£ π βr β€ (1o
Γ {π})}) β πΊ β π΅) |
109 | | fznn0sub 13533 |
. . . . . . . . . . 11
β’ ((πββ
) β
(0...π) β (π β (πββ
)) β
β0) |
110 | 85, 109 | syl 17 |
. . . . . . . . . 10
β’ ((((π
β Ring β§ πΉ β π΅ β§ πΊ β π΅) β§ π β β0) β§ π β {π β (β0
βm 1o) β£ π βr β€ (1o
Γ {π})}) β
(π β (πββ
)) β
β0) |
111 | 50 | coe1fv 21730 |
. . . . . . . . . 10
β’ ((πΊ β π΅ β§ (π β (πββ
)) β β0)
β ((coe1βπΊ)β(π β (πββ
))) = (πΊβ(1o Γ {(π β (πββ
))}))) |
112 | 108, 110,
111 | syl2anc 585 |
. . . . . . . . 9
β’ ((((π
β Ring β§ πΉ β π΅ β§ πΊ β π΅) β§ π β β0) β§ π β {π β (β0
βm 1o) β£ π βr β€ (1o
Γ {π})}) β
((coe1βπΊ)β(π β (πββ
))) = (πΊβ(1o Γ {(π β (πββ
))}))) |
113 | 107, 112 | eqtr4d 2776 |
. . . . . . . 8
β’ ((((π
β Ring β§ πΉ β π΅ β§ πΊ β π΅) β§ π β β0) β§ π β {π β (β0
βm 1o) β£ π βr β€ (1o
Γ {π})}) β
(πΊβ((1o
Γ {π})
βf β π)) = ((coe1βπΊ)β(π β (πββ
)))) |
114 | 95, 113 | oveq12d 7427 |
. . . . . . 7
β’ ((((π
β Ring β§ πΉ β π΅ β§ πΊ β π΅) β§ π β β0) β§ π β {π β (β0
βm 1o) β£ π βr β€ (1o
Γ {π})}) β
((πΉβπ) Β· (πΊβ((1o Γ {π}) βf β
π))) =
(((coe1βπΉ)β(πββ
)) Β·
((coe1βπΊ)β(π β (πββ
))))) |
115 | 114 | mpteq2dva 5249 |
. . . . . 6
β’ (((π
β Ring β§ πΉ β π΅ β§ πΊ β π΅) β§ π β β0) β (π β {π β (β0
βm 1o) β£ π βr β€ (1o
Γ {π})} β¦
((πΉβπ) Β· (πΊβ((1o Γ {π}) βf β
π)))) = (π β {π β (β0
βm 1o) β£ π βr β€ (1o
Γ {π})} β¦
(((coe1βπΉ)β(πββ
)) Β·
((coe1βπΊ)β(π β (πββ
)))))) |
116 | 92, 115 | eqtr4d 2776 |
. . . . 5
β’ (((π
β Ring β§ πΉ β π΅ β§ πΊ β π΅) β§ π β β0) β ((π₯ β (0...π) β¦ (((coe1βπΉ)βπ₯) Β·
((coe1βπΊ)β(π β π₯)))) β (π β {π β (β0
βm 1o) β£ π βr β€ (1o
Γ {π})} β¦
(πββ
))) =
(π β {π β (β0
βm 1o) β£ π βr β€ (1o
Γ {π})} β¦
((πΉβπ) Β· (πΊβ((1o Γ {π}) βf β
π))))) |
117 | 116 | oveq2d 7425 |
. . . 4
β’ (((π
β Ring β§ πΉ β π΅ β§ πΊ β π΅) β§ π β β0) β (π
Ξ£g
((π₯ β (0...π) β¦
(((coe1βπΉ)βπ₯) Β·
((coe1βπΊ)β(π β π₯)))) β (π β {π β (β0
βm 1o) β£ π βr β€ (1o
Γ {π})} β¦
(πββ
)))) =
(π
Ξ£g (π β {π β (β0
βm 1o) β£ π βr β€ (1o
Γ {π})} β¦
((πΉβπ) Β· (πΊβ((1o Γ {π}) βf β
π)))))) |
118 | 75, 117 | eqtrd 2773 |
. . 3
β’ (((π
β Ring β§ πΉ β π΅ β§ πΊ β π΅) β§ π β β0) β (π
Ξ£g
(π₯ β (0...π) β¦
(((coe1βπΉ)βπ₯) Β·
((coe1βπΊ)β(π β π₯))))) = (π
Ξ£g (π β {π β (β0
βm 1o) β£ π βr β€ (1o
Γ {π})} β¦
((πΉβπ) Β· (πΊβ((1o Γ {π}) βf β
π)))))) |
119 | 118 | mpteq2dva 5249 |
. 2
β’ ((π
β Ring β§ πΉ β π΅ β§ πΊ β π΅) β (π β β0 β¦ (π
Ξ£g
(π₯ β (0...π) β¦
(((coe1βπΉ)βπ₯) Β·
((coe1βπΊ)β(π β π₯)))))) = (π β β0 β¦ (π
Ξ£g
(π β {π β (β0
βm 1o) β£ π βr β€ (1o
Γ {π})} β¦
((πΉβπ) Β· (πΊβ((1o Γ {π}) βf β
π))))))) |
120 | 26, 33, 119 | 3eqtr4d 2783 |
1
β’ ((π
β Ring β§ πΉ β π΅ β§ πΊ β π΅) β (coe1β(πΉ β πΊ)) = (π β β0 β¦ (π
Ξ£g
(π₯ β (0...π) β¦
(((coe1βπΉ)βπ₯) Β·
((coe1βπΊ)β(π β π₯))))))) |