Step | Hyp | Ref
| Expression |
1 | | crngring 19983 |
. . 3
β’ (π
β CRing β π
β Ring) |
2 | | simpll 766 |
. . . 4
β’ (((π β Fin β§ π
β Ring) β§ (π β πΎ β§ πΏ β β0)) β π β Fin) |
3 | | simplr 768 |
. . . 4
β’ (((π β Fin β§ π
β Ring) β§ (π β πΎ β§ πΏ β β0)) β π
β Ring) |
4 | | monmat2matmon.a |
. . . . 5
β’ π΄ = (π Mat π
) |
5 | | monmat2matmon.k |
. . . . 5
β’ πΎ = (Baseβπ΄) |
6 | | monmat2matmon.t |
. . . . 5
β’ π = (π matToPolyMat π
) |
7 | | monmat2matmon.p |
. . . . 5
β’ π = (Poly1βπ
) |
8 | | monmat2matmon.c |
. . . . 5
β’ πΆ = (π Mat π) |
9 | | monmat2matmon.b |
. . . . 5
β’ π΅ = (BaseβπΆ) |
10 | | monmat2matmon.m2 |
. . . . 5
β’ Β· = (
Β·π βπΆ) |
11 | | monmat2matmon.e2 |
. . . . 5
β’ πΈ =
(.gβ(mulGrpβπ)) |
12 | | monmat2matmon.y |
. . . . 5
β’ π = (var1βπ
) |
13 | 4, 5, 6, 7, 8, 9, 10, 11, 12 | mat2pmatscmxcl 22105 |
. . . 4
β’ (((π β Fin β§ π
β Ring) β§ (π β πΎ β§ πΏ β β0)) β ((πΏπΈπ) Β· (πβπ)) β π΅) |
14 | | monmat2matmon.m1 |
. . . . 5
β’ β = (
Β·π βπ) |
15 | | monmat2matmon.e1 |
. . . . 5
β’ β =
(.gβ(mulGrpβπ)) |
16 | | monmat2matmon.x |
. . . . 5
β’ π = (var1βπ΄) |
17 | | monmat2matmon.q |
. . . . 5
β’ π = (Poly1βπ΄) |
18 | | monmat2matmon.i |
. . . . 5
β’ πΌ = (π pMatToMatPoly π
) |
19 | 7, 8, 9, 14, 15, 16, 4, 17, 18 | pm2mpfval 22161 |
. . . 4
β’ ((π β Fin β§ π
β Ring β§ ((πΏπΈπ) Β· (πβπ)) β π΅) β (πΌβ((πΏπΈπ) Β· (πβπ))) = (π Ξ£g (π β β0
β¦ ((((πΏπΈπ) Β· (πβπ)) decompPMat π) β (π β π))))) |
20 | 2, 3, 13, 19 | syl3anc 1372 |
. . 3
β’ (((π β Fin β§ π
β Ring) β§ (π β πΎ β§ πΏ β β0)) β (πΌβ((πΏπΈπ) Β· (πβπ))) = (π Ξ£g (π β β0
β¦ ((((πΏπΈπ) Β· (πβπ)) decompPMat π) β (π β π))))) |
21 | 1, 20 | sylanl2 680 |
. 2
β’ (((π β Fin β§ π
β CRing) β§ (π β πΎ β§ πΏ β β0)) β (πΌβ((πΏπΈπ) Β· (πβπ))) = (π Ξ£g (π β β0
β¦ ((((πΏπΈπ) Β· (πβπ)) decompPMat π) β (π β π))))) |
22 | | simpll 766 |
. . . . . . . 8
β’ ((((π β Fin β§ π
β CRing) β§ (π β πΎ β§ πΏ β β0)) β§ π β β0)
β (π β Fin β§
π
β
CRing)) |
23 | | simpr 486 |
. . . . . . . . . 10
β’ (((π β Fin β§ π
β CRing) β§ (π β πΎ β§ πΏ β β0)) β (π β πΎ β§ πΏ β
β0)) |
24 | 23 | anim1i 616 |
. . . . . . . . 9
β’ ((((π β Fin β§ π
β CRing) β§ (π β πΎ β§ πΏ β β0)) β§ π β β0)
β ((π β πΎ β§ πΏ β β0) β§ π β
β0)) |
25 | | df-3an 1090 |
. . . . . . . . 9
β’ ((π β πΎ β§ πΏ β β0 β§ π β β0)
β ((π β πΎ β§ πΏ β β0) β§ π β
β0)) |
26 | 24, 25 | sylibr 233 |
. . . . . . . 8
β’ ((((π β Fin β§ π
β CRing) β§ (π β πΎ β§ πΏ β β0)) β§ π β β0)
β (π β πΎ β§ πΏ β β0 β§ π β
β0)) |
27 | | eqid 2737 |
. . . . . . . . 9
β’
(0gβπ΄) = (0gβπ΄) |
28 | 7, 8, 4, 5, 27, 11, 12, 10, 6 | monmatcollpw 22144 |
. . . . . . . 8
β’ (((π β Fin β§ π
β CRing) β§ (π β πΎ β§ πΏ β β0 β§ π β β0))
β (((πΏπΈπ) Β· (πβπ)) decompPMat π) = if(π = πΏ, π, (0gβπ΄))) |
29 | 22, 26, 28 | syl2anc 585 |
. . . . . . 7
β’ ((((π β Fin β§ π
β CRing) β§ (π β πΎ β§ πΏ β β0)) β§ π β β0)
β (((πΏπΈπ) Β· (πβπ)) decompPMat π) = if(π = πΏ, π, (0gβπ΄))) |
30 | 29 | oveq1d 7377 |
. . . . . 6
β’ ((((π β Fin β§ π
β CRing) β§ (π β πΎ β§ πΏ β β0)) β§ π β β0)
β ((((πΏπΈπ) Β· (πβπ)) decompPMat π) β (π β π)) = (if(π = πΏ, π, (0gβπ΄)) β (π β π))) |
31 | 1 | a1i 11 |
. . . . . . . . . 10
β’ (π β β0
β (π
β CRing
β π
β
Ring)) |
32 | 31 | anim2d 613 |
. . . . . . . . 9
β’ (π β β0
β ((π β Fin β§
π
β CRing) β
(π β Fin β§ π
β Ring))) |
33 | 32 | anim1d 612 |
. . . . . . . 8
β’ (π β β0
β (((π β Fin
β§ π
β CRing) β§
(π β πΎ β§ πΏ β β0)) β ((π β Fin β§ π
β Ring) β§ (π β πΎ β§ πΏ β
β0)))) |
34 | 33 | imdistanri 571 |
. . . . . . 7
β’ ((((π β Fin β§ π
β CRing) β§ (π β πΎ β§ πΏ β β0)) β§ π β β0)
β (((π β Fin
β§ π
β Ring) β§
(π β πΎ β§ πΏ β β0)) β§ π β
β0)) |
35 | | ovif 7459 |
. . . . . . . 8
β’ (if(π = πΏ, π, (0gβπ΄)) β (π β π)) = if(π = πΏ, (π β (π β π)), ((0gβπ΄) β (π β π))) |
36 | 4 | matring 21808 |
. . . . . . . . . . . . . 14
β’ ((π β Fin β§ π
β Ring) β π΄ β Ring) |
37 | 17 | ply1sca 21640 |
. . . . . . . . . . . . . 14
β’ (π΄ β Ring β π΄ = (Scalarβπ)) |
38 | 36, 37 | syl 17 |
. . . . . . . . . . . . 13
β’ ((π β Fin β§ π
β Ring) β π΄ = (Scalarβπ)) |
39 | 38 | ad2antrr 725 |
. . . . . . . . . . . 12
β’ ((((π β Fin β§ π
β Ring) β§ (π β πΎ β§ πΏ β β0)) β§ π β β0)
β π΄ =
(Scalarβπ)) |
40 | 39 | fveq2d 6851 |
. . . . . . . . . . 11
β’ ((((π β Fin β§ π
β Ring) β§ (π β πΎ β§ πΏ β β0)) β§ π β β0)
β (0gβπ΄) = (0gβ(Scalarβπ))) |
41 | 40 | oveq1d 7377 |
. . . . . . . . . 10
β’ ((((π β Fin β§ π
β Ring) β§ (π β πΎ β§ πΏ β β0)) β§ π β β0)
β ((0gβπ΄) β (π β π)) =
((0gβ(Scalarβπ)) β (π β π))) |
42 | 17 | ply1lmod 21639 |
. . . . . . . . . . . . 13
β’ (π΄ β Ring β π β LMod) |
43 | 36, 42 | syl 17 |
. . . . . . . . . . . 12
β’ ((π β Fin β§ π
β Ring) β π β LMod) |
44 | 43 | ad2antrr 725 |
. . . . . . . . . . 11
β’ ((((π β Fin β§ π
β Ring) β§ (π β πΎ β§ πΏ β β0)) β§ π β β0)
β π β
LMod) |
45 | | eqid 2737 |
. . . . . . . . . . . . 13
β’
(mulGrpβπ) =
(mulGrpβπ) |
46 | | eqid 2737 |
. . . . . . . . . . . . 13
β’
(Baseβπ) =
(Baseβπ) |
47 | 45, 46 | mgpbas 19909 |
. . . . . . . . . . . 12
β’
(Baseβπ) =
(Baseβ(mulGrpβπ)) |
48 | 17 | ply1ring 21635 |
. . . . . . . . . . . . . . 15
β’ (π΄ β Ring β π β Ring) |
49 | 36, 48 | syl 17 |
. . . . . . . . . . . . . 14
β’ ((π β Fin β§ π
β Ring) β π β Ring) |
50 | 45 | ringmgp 19977 |
. . . . . . . . . . . . . 14
β’ (π β Ring β
(mulGrpβπ) β
Mnd) |
51 | 49, 50 | syl 17 |
. . . . . . . . . . . . 13
β’ ((π β Fin β§ π
β Ring) β
(mulGrpβπ) β
Mnd) |
52 | 51 | ad2antrr 725 |
. . . . . . . . . . . 12
β’ ((((π β Fin β§ π
β Ring) β§ (π β πΎ β§ πΏ β β0)) β§ π β β0)
β (mulGrpβπ)
β Mnd) |
53 | | simpr 486 |
. . . . . . . . . . . 12
β’ ((((π β Fin β§ π
β Ring) β§ (π β πΎ β§ πΏ β β0)) β§ π β β0)
β π β
β0) |
54 | 16, 17, 46 | vr1cl 21604 |
. . . . . . . . . . . . . 14
β’ (π΄ β Ring β π β (Baseβπ)) |
55 | 36, 54 | syl 17 |
. . . . . . . . . . . . 13
β’ ((π β Fin β§ π
β Ring) β π β (Baseβπ)) |
56 | 55 | ad2antrr 725 |
. . . . . . . . . . . 12
β’ ((((π β Fin β§ π
β Ring) β§ (π β πΎ β§ πΏ β β0)) β§ π β β0)
β π β
(Baseβπ)) |
57 | 47, 15, 52, 53, 56 | mulgnn0cld 18904 |
. . . . . . . . . . 11
β’ ((((π β Fin β§ π
β Ring) β§ (π β πΎ β§ πΏ β β0)) β§ π β β0)
β (π β π) β (Baseβπ)) |
58 | | eqid 2737 |
. . . . . . . . . . . 12
β’
(Scalarβπ) =
(Scalarβπ) |
59 | | eqid 2737 |
. . . . . . . . . . . 12
β’
(0gβ(Scalarβπ)) =
(0gβ(Scalarβπ)) |
60 | | eqid 2737 |
. . . . . . . . . . . 12
β’
(0gβπ) = (0gβπ) |
61 | 46, 58, 14, 59, 60 | lmod0vs 20371 |
. . . . . . . . . . 11
β’ ((π β LMod β§ (π β π) β (Baseβπ)) β
((0gβ(Scalarβπ)) β (π β π)) = (0gβπ)) |
62 | 44, 57, 61 | syl2anc 585 |
. . . . . . . . . 10
β’ ((((π β Fin β§ π
β Ring) β§ (π β πΎ β§ πΏ β β0)) β§ π β β0)
β ((0gβ(Scalarβπ)) β (π β π)) = (0gβπ)) |
63 | 41, 62 | eqtrd 2777 |
. . . . . . . . 9
β’ ((((π β Fin β§ π
β Ring) β§ (π β πΎ β§ πΏ β β0)) β§ π β β0)
β ((0gβπ΄) β (π β π)) = (0gβπ)) |
64 | 63 | ifeq2d 4511 |
. . . . . . . 8
β’ ((((π β Fin β§ π
β Ring) β§ (π β πΎ β§ πΏ β β0)) β§ π β β0)
β if(π = πΏ, (π β (π β π)), ((0gβπ΄) β (π β π))) = if(π = πΏ, (π β (π β π)), (0gβπ))) |
65 | 35, 64 | eqtrid 2789 |
. . . . . . 7
β’ ((((π β Fin β§ π
β Ring) β§ (π β πΎ β§ πΏ β β0)) β§ π β β0)
β (if(π = πΏ, π, (0gβπ΄)) β (π β π)) = if(π = πΏ, (π β (π β π)), (0gβπ))) |
66 | 34, 65 | syl 17 |
. . . . . 6
β’ ((((π β Fin β§ π
β CRing) β§ (π β πΎ β§ πΏ β β0)) β§ π β β0)
β (if(π = πΏ, π, (0gβπ΄)) β (π β π)) = if(π = πΏ, (π β (π β π)), (0gβπ))) |
67 | 30, 66 | eqtrd 2777 |
. . . . 5
β’ ((((π β Fin β§ π
β CRing) β§ (π β πΎ β§ πΏ β β0)) β§ π β β0)
β ((((πΏπΈπ) Β· (πβπ)) decompPMat π) β (π β π)) = if(π = πΏ, (π β (π β π)), (0gβπ))) |
68 | 67 | mpteq2dva 5210 |
. . . 4
β’ (((π β Fin β§ π
β CRing) β§ (π β πΎ β§ πΏ β β0)) β (π β β0
β¦ ((((πΏπΈπ) Β· (πβπ)) decompPMat π) β (π β π))) = (π β β0 β¦ if(π = πΏ, (π β (π β π)), (0gβπ)))) |
69 | 68 | oveq2d 7378 |
. . 3
β’ (((π β Fin β§ π
β CRing) β§ (π β πΎ β§ πΏ β β0)) β (π Ξ£g
(π β
β0 β¦ ((((πΏπΈπ) Β· (πβπ)) decompPMat π) β (π β π)))) = (π Ξ£g (π β β0
β¦ if(π = πΏ, (π β (π β π)), (0gβπ))))) |
70 | | ringmnd 19981 |
. . . . . . 7
β’ (π β Ring β π β Mnd) |
71 | 49, 70 | syl 17 |
. . . . . 6
β’ ((π β Fin β§ π
β Ring) β π β Mnd) |
72 | 71 | adantr 482 |
. . . . 5
β’ (((π β Fin β§ π
β Ring) β§ (π β πΎ β§ πΏ β β0)) β π β Mnd) |
73 | | nn0ex 12426 |
. . . . . 6
β’
β0 β V |
74 | 73 | a1i 11 |
. . . . 5
β’ (((π β Fin β§ π
β Ring) β§ (π β πΎ β§ πΏ β β0)) β
β0 β V) |
75 | | simprr 772 |
. . . . 5
β’ (((π β Fin β§ π
β Ring) β§ (π β πΎ β§ πΏ β β0)) β πΏ β
β0) |
76 | | eqid 2737 |
. . . . 5
β’ (π β β0
β¦ if(π = πΏ, (π β (π β π)), (0gβπ))) = (π β β0 β¦ if(π = πΏ, (π β (π β π)), (0gβπ))) |
77 | 38 | fveq2d 6851 |
. . . . . . . . . . . . 13
β’ ((π β Fin β§ π
β Ring) β
(Baseβπ΄) =
(Baseβ(Scalarβπ))) |
78 | 5, 77 | eqtrid 2789 |
. . . . . . . . . . . 12
β’ ((π β Fin β§ π
β Ring) β πΎ =
(Baseβ(Scalarβπ))) |
79 | 78 | eleq2d 2824 |
. . . . . . . . . . 11
β’ ((π β Fin β§ π
β Ring) β (π β πΎ β π β (Baseβ(Scalarβπ)))) |
80 | 79 | biimpcd 249 |
. . . . . . . . . 10
β’ (π β πΎ β ((π β Fin β§ π
β Ring) β π β (Baseβ(Scalarβπ)))) |
81 | 80 | adantr 482 |
. . . . . . . . 9
β’ ((π β πΎ β§ πΏ β β0) β ((π β Fin β§ π
β Ring) β π β
(Baseβ(Scalarβπ)))) |
82 | 81 | impcom 409 |
. . . . . . . 8
β’ (((π β Fin β§ π
β Ring) β§ (π β πΎ β§ πΏ β β0)) β π β
(Baseβ(Scalarβπ))) |
83 | 82 | adantr 482 |
. . . . . . 7
β’ ((((π β Fin β§ π
β Ring) β§ (π β πΎ β§ πΏ β β0)) β§ π β β0)
β π β
(Baseβ(Scalarβπ))) |
84 | | eqid 2737 |
. . . . . . . 8
β’
(Baseβ(Scalarβπ)) = (Baseβ(Scalarβπ)) |
85 | 46, 58, 14, 84 | lmodvscl 20355 |
. . . . . . 7
β’ ((π β LMod β§ π β
(Baseβ(Scalarβπ)) β§ (π β π) β (Baseβπ)) β (π β (π β π)) β (Baseβπ)) |
86 | 44, 83, 57, 85 | syl3anc 1372 |
. . . . . 6
β’ ((((π β Fin β§ π
β Ring) β§ (π β πΎ β§ πΏ β β0)) β§ π β β0)
β (π β (π β π)) β (Baseβπ)) |
87 | 86 | ralrimiva 3144 |
. . . . 5
β’ (((π β Fin β§ π
β Ring) β§ (π β πΎ β§ πΏ β β0)) β
βπ β
β0 (π
β
(π β π)) β (Baseβπ)) |
88 | 60, 72, 74, 75, 76, 87 | gsummpt1n0 19749 |
. . . 4
β’ (((π β Fin β§ π
β Ring) β§ (π β πΎ β§ πΏ β β0)) β (π Ξ£g
(π β
β0 β¦ if(π = πΏ, (π β (π β π)), (0gβπ)))) = β¦πΏ / πβ¦(π β (π β π))) |
89 | 1, 88 | sylanl2 680 |
. . 3
β’ (((π β Fin β§ π
β CRing) β§ (π β πΎ β§ πΏ β β0)) β (π Ξ£g
(π β
β0 β¦ if(π = πΏ, (π β (π β π)), (0gβπ)))) = β¦πΏ / πβ¦(π β (π β π))) |
90 | 69, 89 | eqtrd 2777 |
. 2
β’ (((π β Fin β§ π
β CRing) β§ (π β πΎ β§ πΏ β β0)) β (π Ξ£g
(π β
β0 β¦ ((((πΏπΈπ) Β· (πβπ)) decompPMat π) β (π β π)))) = β¦πΏ / πβ¦(π β (π β π))) |
91 | | csbov2g 7408 |
. . . 4
β’ (πΏ β β0
β β¦πΏ /
πβ¦(π β (π β π)) = (π β
β¦πΏ / πβ¦(π β π))) |
92 | | csbov1g 7407 |
. . . . . 6
β’ (πΏ β β0
β β¦πΏ /
πβ¦(π β π) = (β¦πΏ / πβ¦π β π)) |
93 | | csbvarg 4396 |
. . . . . . 7
β’ (πΏ β β0
β β¦πΏ /
πβ¦π = πΏ) |
94 | 93 | oveq1d 7377 |
. . . . . 6
β’ (πΏ β β0
β (β¦πΏ /
πβ¦π β π) = (πΏ β π)) |
95 | 92, 94 | eqtrd 2777 |
. . . . 5
β’ (πΏ β β0
β β¦πΏ /
πβ¦(π β π) = (πΏ β π)) |
96 | 95 | oveq2d 7378 |
. . . 4
β’ (πΏ β β0
β (π β
β¦πΏ / πβ¦(π β π)) = (π β (πΏ β π))) |
97 | 91, 96 | eqtrd 2777 |
. . 3
β’ (πΏ β β0
β β¦πΏ /
πβ¦(π β (π β π)) = (π β (πΏ β π))) |
98 | 97 | ad2antll 728 |
. 2
β’ (((π β Fin β§ π
β CRing) β§ (π β πΎ β§ πΏ β β0)) β
β¦πΏ / πβ¦(π β (π β π)) = (π β (πΏ β π))) |
99 | 21, 90, 98 | 3eqtrd 2781 |
1
β’ (((π β Fin β§ π
β CRing) β§ (π β πΎ β§ πΏ β β0)) β (πΌβ((πΏπΈπ) Β· (πβπ))) = (π β (πΏ β π))) |