Step | Hyp | Ref
| Expression |
1 | | srgpcomp.r |
. . . . 5
โข (๐ โ ๐
โ SRing) |
2 | | srgpcomppsc.c |
. . . . 5
โข (๐ โ ๐ถ โ
โ0) |
3 | | srgpcomp.g |
. . . . . . . . 9
โข ๐บ = (mulGrpโ๐
) |
4 | 3 | srgmgp 13156 |
. . . . . . . 8
โข (๐
โ SRing โ ๐บ โ Mnd) |
5 | 1, 4 | syl 14 |
. . . . . . 7
โข (๐ โ ๐บ โ Mnd) |
6 | | srgpcompp.n |
. . . . . . 7
โข (๐ โ ๐ โ
โ0) |
7 | | srgpcomp.a |
. . . . . . . 8
โข (๐ โ ๐ด โ ๐) |
8 | | srgpcomp.s |
. . . . . . . . . 10
โข ๐ = (Baseโ๐
) |
9 | 3, 8 | mgpbasg 13141 |
. . . . . . . . 9
โข (๐
โ SRing โ ๐ = (Baseโ๐บ)) |
10 | 1, 9 | syl 14 |
. . . . . . . 8
โข (๐ โ ๐ = (Baseโ๐บ)) |
11 | 7, 10 | eleqtrd 2256 |
. . . . . . 7
โข (๐ โ ๐ด โ (Baseโ๐บ)) |
12 | | eqid 2177 |
. . . . . . . 8
โข
(Baseโ๐บ) =
(Baseโ๐บ) |
13 | | srgpcomp.e |
. . . . . . . 8
โข โ =
(.gโ๐บ) |
14 | 12, 13 | mulgnn0cl 13004 |
. . . . . . 7
โข ((๐บ โ Mnd โง ๐ โ โ0
โง ๐ด โ
(Baseโ๐บ)) โ
(๐ โ ๐ด) โ (Baseโ๐บ)) |
15 | 5, 6, 11, 14 | syl3anc 1238 |
. . . . . 6
โข (๐ โ (๐ โ ๐ด) โ (Baseโ๐บ)) |
16 | 15, 10 | eleqtrrd 2257 |
. . . . 5
โข (๐ โ (๐ โ ๐ด) โ ๐) |
17 | | srgpcomp.k |
. . . . . . 7
โข (๐ โ ๐พ โ
โ0) |
18 | | srgpcomp.b |
. . . . . . . 8
โข (๐ โ ๐ต โ ๐) |
19 | 18, 10 | eleqtrd 2256 |
. . . . . . 7
โข (๐ โ ๐ต โ (Baseโ๐บ)) |
20 | 12, 13 | mulgnn0cl 13004 |
. . . . . . 7
โข ((๐บ โ Mnd โง ๐พ โ โ0
โง ๐ต โ
(Baseโ๐บ)) โ
(๐พ โ ๐ต) โ (Baseโ๐บ)) |
21 | 5, 17, 19, 20 | syl3anc 1238 |
. . . . . 6
โข (๐ โ (๐พ โ ๐ต) โ (Baseโ๐บ)) |
22 | 21, 10 | eleqtrrd 2257 |
. . . . 5
โข (๐ โ (๐พ โ ๐ต) โ ๐) |
23 | | srgpcomppsc.t |
. . . . . . 7
โข ยท =
(.gโ๐
) |
24 | | srgpcomp.m |
. . . . . . 7
โข ร =
(.rโ๐
) |
25 | 8, 23, 24 | srgmulgass 13177 |
. . . . . 6
โข ((๐
โ SRing โง (๐ถ โ โ0
โง (๐ โ ๐ด) โ ๐ โง (๐พ โ ๐ต) โ ๐)) โ ((๐ถ ยท (๐ โ ๐ด)) ร (๐พ โ ๐ต)) = (๐ถ ยท ((๐ โ ๐ด) ร (๐พ โ ๐ต)))) |
26 | 25 | eqcomd 2183 |
. . . . 5
โข ((๐
โ SRing โง (๐ถ โ โ0
โง (๐ โ ๐ด) โ ๐ โง (๐พ โ ๐ต) โ ๐)) โ (๐ถ ยท ((๐ โ ๐ด) ร (๐พ โ ๐ต))) = ((๐ถ ยท (๐ โ ๐ด)) ร (๐พ โ ๐ต))) |
27 | 1, 2, 16, 22, 26 | syl13anc 1240 |
. . . 4
โข (๐ โ (๐ถ ยท ((๐ โ ๐ด) ร (๐พ โ ๐ต))) = ((๐ถ ยท (๐ โ ๐ด)) ร (๐พ โ ๐ต))) |
28 | 27 | oveq1d 5892 |
. . 3
โข (๐ โ ((๐ถ ยท ((๐ โ ๐ด) ร (๐พ โ ๐ต))) ร ๐ด) = (((๐ถ ยท (๐ โ ๐ด)) ร (๐พ โ ๐ต)) ร ๐ด)) |
29 | | srgmnd 13155 |
. . . . . 6
โข (๐
โ SRing โ ๐
โ Mnd) |
30 | 1, 29 | syl 14 |
. . . . 5
โข (๐ โ ๐
โ Mnd) |
31 | 8, 23 | mulgnn0cl 13004 |
. . . . 5
โข ((๐
โ Mnd โง ๐ถ โ โ0
โง (๐ โ ๐ด) โ ๐) โ (๐ถ ยท (๐ โ ๐ด)) โ ๐) |
32 | 30, 2, 16, 31 | syl3anc 1238 |
. . . 4
โข (๐ โ (๐ถ ยท (๐ โ ๐ด)) โ ๐) |
33 | 8, 24 | srgass 13159 |
. . . 4
โข ((๐
โ SRing โง ((๐ถ ยท (๐ โ ๐ด)) โ ๐ โง (๐พ โ ๐ต) โ ๐ โง ๐ด โ ๐)) โ (((๐ถ ยท (๐ โ ๐ด)) ร (๐พ โ ๐ต)) ร ๐ด) = ((๐ถ ยท (๐ โ ๐ด)) ร ((๐พ โ ๐ต) ร ๐ด))) |
34 | 1, 32, 22, 7, 33 | syl13anc 1240 |
. . 3
โข (๐ โ (((๐ถ ยท (๐ โ ๐ด)) ร (๐พ โ ๐ต)) ร ๐ด) = ((๐ถ ยท (๐ โ ๐ด)) ร ((๐พ โ ๐ต) ร ๐ด))) |
35 | 28, 34 | eqtrd 2210 |
. 2
โข (๐ โ ((๐ถ ยท ((๐ โ ๐ด) ร (๐พ โ ๐ต))) ร ๐ด) = ((๐ถ ยท (๐ โ ๐ด)) ร ((๐พ โ ๐ต) ร ๐ด))) |
36 | 8, 24 | srgcl 13158 |
. . . . 5
โข ((๐
โ SRing โง (๐พ โ ๐ต) โ ๐ โง ๐ด โ ๐) โ ((๐พ โ ๐ต) ร ๐ด) โ ๐) |
37 | 1, 22, 7, 36 | syl3anc 1238 |
. . . 4
โข (๐ โ ((๐พ โ ๐ต) ร ๐ด) โ ๐) |
38 | 8, 23, 24 | srgmulgass 13177 |
. . . 4
โข ((๐
โ SRing โง (๐ถ โ โ0
โง (๐ โ ๐ด) โ ๐ โง ((๐พ โ ๐ต) ร ๐ด) โ ๐)) โ ((๐ถ ยท (๐ โ ๐ด)) ร ((๐พ โ ๐ต) ร ๐ด)) = (๐ถ ยท ((๐ โ ๐ด) ร ((๐พ โ ๐ต) ร ๐ด)))) |
39 | 1, 2, 16, 37, 38 | syl13anc 1240 |
. . 3
โข (๐ โ ((๐ถ ยท (๐ โ ๐ด)) ร ((๐พ โ ๐ต) ร ๐ด)) = (๐ถ ยท ((๐ โ ๐ด) ร ((๐พ โ ๐ต) ร ๐ด)))) |
40 | 8, 24 | srgass 13159 |
. . . . . 6
โข ((๐
โ SRing โง ((๐ โ ๐ด) โ ๐ โง (๐พ โ ๐ต) โ ๐ โง ๐ด โ ๐)) โ (((๐ โ ๐ด) ร (๐พ โ ๐ต)) ร ๐ด) = ((๐ โ ๐ด) ร ((๐พ โ ๐ต) ร ๐ด))) |
41 | 1, 16, 22, 7, 40 | syl13anc 1240 |
. . . . 5
โข (๐ โ (((๐ โ ๐ด) ร (๐พ โ ๐ต)) ร ๐ด) = ((๐ โ ๐ด) ร ((๐พ โ ๐ต) ร ๐ด))) |
42 | 41 | eqcomd 2183 |
. . . 4
โข (๐ โ ((๐ โ ๐ด) ร ((๐พ โ ๐ต) ร ๐ด)) = (((๐ โ ๐ด) ร (๐พ โ ๐ต)) ร ๐ด)) |
43 | 42 | oveq2d 5893 |
. . 3
โข (๐ โ (๐ถ ยท ((๐ โ ๐ด) ร ((๐พ โ ๐ต) ร ๐ด))) = (๐ถ ยท (((๐ โ ๐ด) ร (๐พ โ ๐ต)) ร ๐ด))) |
44 | 39, 43 | eqtrd 2210 |
. 2
โข (๐ โ ((๐ถ ยท (๐ โ ๐ด)) ร ((๐พ โ ๐ต) ร ๐ด)) = (๐ถ ยท (((๐ โ ๐ด) ร (๐พ โ ๐ต)) ร ๐ด))) |
45 | | srgpcomp.c |
. . . 4
โข (๐ โ (๐ด ร ๐ต) = (๐ต ร ๐ด)) |
46 | 8, 24, 3, 13, 1, 7,
18, 17, 45, 6 | srgpcompp 13179 |
. . 3
โข (๐ โ (((๐ โ ๐ด) ร (๐พ โ ๐ต)) ร ๐ด) = (((๐ + 1) โ ๐ด) ร (๐พ โ ๐ต))) |
47 | 46 | oveq2d 5893 |
. 2
โข (๐ โ (๐ถ ยท (((๐ โ ๐ด) ร (๐พ โ ๐ต)) ร ๐ด)) = (๐ถ ยท (((๐ + 1) โ ๐ด) ร (๐พ โ ๐ต)))) |
48 | 35, 44, 47 | 3eqtrd 2214 |
1
โข (๐ โ ((๐ถ ยท ((๐ โ ๐ด) ร (๐พ โ ๐ต))) ร ๐ด) = (๐ถ ยท (((๐ + 1) โ ๐ด) ร (๐พ โ ๐ต)))) |