Step | Hyp | Ref
| Expression |
1 | | scmatscm.k |
. . . 4
โข ๐พ = (Baseโ๐
) |
2 | | scmatscm.a |
. . . 4
โข ๐ด = (๐ Mat ๐
) |
3 | | scmatscm.b |
. . . 4
โข ๐ต = (Baseโ๐ด) |
4 | | eqid 2733 |
. . . 4
โข
(1rโ๐ด) = (1rโ๐ด) |
5 | | scmatscm.t |
. . . 4
โข โ = (
ยท๐ โ๐ด) |
6 | | scmatscm.c |
. . . 4
โข ๐ = (๐ ScMat ๐
) |
7 | 1, 2, 3, 4, 5, 6 | scmatscmid 21878 |
. . 3
โข ((๐ โ Fin โง ๐
โ Ring โง ๐ถ โ ๐) โ โ๐ โ ๐พ ๐ถ = (๐ โ
(1rโ๐ด))) |
8 | 7 | 3expa 1119 |
. 2
โข (((๐ โ Fin โง ๐
โ Ring) โง ๐ถ โ ๐) โ โ๐ โ ๐พ ๐ถ = (๐ โ
(1rโ๐ด))) |
9 | | oveq1 7368 |
. . . . . 6
โข (๐ถ = (๐ โ
(1rโ๐ด))
โ (๐ถ ร ๐) = ((๐ โ
(1rโ๐ด))
ร
๐)) |
10 | | simpr 486 |
. . . . . . . . . . . 12
โข ((๐ โ Fin โง ๐
โ Ring) โ ๐
โ Ring) |
11 | 10 | ad4antr 731 |
. . . . . . . . . . 11
โข
((((((๐ โ Fin
โง ๐
โ Ring) โง
๐ถ โ ๐) โง ๐ โ ๐พ) โง ๐ โ ๐ต) โง (๐ โ ๐ โง ๐ โ ๐)) โ ๐
โ Ring) |
12 | | simpl 484 |
. . . . . . . . . . . . . . 15
โข (((๐ โ Fin โง ๐
โ Ring) โง ๐ถ โ ๐) โ (๐ โ Fin โง ๐
โ Ring)) |
13 | 12 | adantr 482 |
. . . . . . . . . . . . . 14
โข ((((๐ โ Fin โง ๐
โ Ring) โง ๐ถ โ ๐) โง ๐ โ ๐พ) โ (๐ โ Fin โง ๐
โ Ring)) |
14 | 2 | matring 21815 |
. . . . . . . . . . . . . . . . 17
โข ((๐ โ Fin โง ๐
โ Ring) โ ๐ด โ Ring) |
15 | 3, 4 | ringidcl 19997 |
. . . . . . . . . . . . . . . . 17
โข (๐ด โ Ring โ
(1rโ๐ด)
โ ๐ต) |
16 | 14, 15 | syl 17 |
. . . . . . . . . . . . . . . 16
โข ((๐ โ Fin โง ๐
โ Ring) โ
(1rโ๐ด)
โ ๐ต) |
17 | 16 | adantr 482 |
. . . . . . . . . . . . . . 15
โข (((๐ โ Fin โง ๐
โ Ring) โง ๐ถ โ ๐) โ (1rโ๐ด) โ ๐ต) |
18 | 17 | anim1ci 617 |
. . . . . . . . . . . . . 14
โข ((((๐ โ Fin โง ๐
โ Ring) โง ๐ถ โ ๐) โง ๐ โ ๐พ) โ (๐ โ ๐พ โง (1rโ๐ด) โ ๐ต)) |
19 | 1, 2, 3, 5 | matvscl 21803 |
. . . . . . . . . . . . . 14
โข (((๐ โ Fin โง ๐
โ Ring) โง (๐ โ ๐พ โง (1rโ๐ด) โ ๐ต)) โ (๐ โ
(1rโ๐ด))
โ ๐ต) |
20 | 13, 18, 19 | syl2anc 585 |
. . . . . . . . . . . . 13
โข ((((๐ โ Fin โง ๐
โ Ring) โง ๐ถ โ ๐) โง ๐ โ ๐พ) โ (๐ โ
(1rโ๐ด))
โ ๐ต) |
21 | 20 | anim1i 616 |
. . . . . . . . . . . 12
โข
(((((๐ โ Fin
โง ๐
โ Ring) โง
๐ถ โ ๐) โง ๐ โ ๐พ) โง ๐ โ ๐ต) โ ((๐ โ
(1rโ๐ด))
โ ๐ต โง ๐ โ ๐ต)) |
22 | 21 | adantr 482 |
. . . . . . . . . . 11
โข
((((((๐ โ Fin
โง ๐
โ Ring) โง
๐ถ โ ๐) โง ๐ โ ๐พ) โง ๐ โ ๐ต) โง (๐ โ ๐ โง ๐ โ ๐)) โ ((๐ โ
(1rโ๐ด))
โ ๐ต โง ๐ โ ๐ต)) |
23 | | simpr 486 |
. . . . . . . . . . 11
โข
((((((๐ โ Fin
โง ๐
โ Ring) โง
๐ถ โ ๐) โง ๐ โ ๐พ) โง ๐ โ ๐ต) โง (๐ โ ๐ โง ๐ โ ๐)) โ (๐ โ ๐ โง ๐ โ ๐)) |
24 | | scmatscm.m |
. . . . . . . . . . . 12
โข ร =
(.rโ๐ด) |
25 | 2, 3, 24 | matmulcell 21817 |
. . . . . . . . . . 11
โข ((๐
โ Ring โง ((๐ โ
(1rโ๐ด))
โ ๐ต โง ๐ โ ๐ต) โง (๐ โ ๐ โง ๐ โ ๐)) โ (๐((๐ โ
(1rโ๐ด))
ร
๐)๐) = (๐
ฮฃg (๐ โ ๐ โฆ ((๐(๐ โ
(1rโ๐ด))๐)(.rโ๐
)(๐๐๐))))) |
26 | 11, 22, 23, 25 | syl3anc 1372 |
. . . . . . . . . 10
โข
((((((๐ โ Fin
โง ๐
โ Ring) โง
๐ถ โ ๐) โง ๐ โ ๐พ) โง ๐ โ ๐ต) โง (๐ โ ๐ โง ๐ โ ๐)) โ (๐((๐ โ
(1rโ๐ด))
ร
๐)๐) = (๐
ฮฃg (๐ โ ๐ โฆ ((๐(๐ โ
(1rโ๐ด))๐)(.rโ๐
)(๐๐๐))))) |
27 | 12 | anim1i 616 |
. . . . . . . . . . . . . . . . . 18
โข ((((๐ โ Fin โง ๐
โ Ring) โง ๐ถ โ ๐) โง ๐ โ ๐พ) โ ((๐ โ Fin โง ๐
โ Ring) โง ๐ โ ๐พ)) |
28 | | df-3an 1090 |
. . . . . . . . . . . . . . . . . 18
โข ((๐ โ Fin โง ๐
โ Ring โง ๐ โ ๐พ) โ ((๐ โ Fin โง ๐
โ Ring) โง ๐ โ ๐พ)) |
29 | 27, 28 | sylibr 233 |
. . . . . . . . . . . . . . . . 17
โข ((((๐ โ Fin โง ๐
โ Ring) โง ๐ถ โ ๐) โง ๐ โ ๐พ) โ (๐ โ Fin โง ๐
โ Ring โง ๐ โ ๐พ)) |
30 | 29 | ad3antrrr 729 |
. . . . . . . . . . . . . . . 16
โข
(((((((๐ โ Fin
โง ๐
โ Ring) โง
๐ถ โ ๐) โง ๐ โ ๐พ) โง ๐ โ ๐ต) โง (๐ โ ๐ โง ๐ โ ๐)) โง ๐ โ ๐) โ (๐ โ Fin โง ๐
โ Ring โง ๐ โ ๐พ)) |
31 | | eqid 2733 |
. . . . . . . . . . . . . . . . 17
โข
(0gโ๐
) = (0gโ๐
) |
32 | 2, 1, 5, 31 | matsc 21822 |
. . . . . . . . . . . . . . . 16
โข ((๐ โ Fin โง ๐
โ Ring โง ๐ โ ๐พ) โ (๐ โ
(1rโ๐ด)) =
(๐ฅ โ ๐, ๐ฆ โ ๐ โฆ if(๐ฅ = ๐ฆ, ๐, (0gโ๐
)))) |
33 | 30, 32 | syl 17 |
. . . . . . . . . . . . . . 15
โข
(((((((๐ โ Fin
โง ๐
โ Ring) โง
๐ถ โ ๐) โง ๐ โ ๐พ) โง ๐ โ ๐ต) โง (๐ โ ๐ โง ๐ โ ๐)) โง ๐ โ ๐) โ (๐ โ
(1rโ๐ด)) =
(๐ฅ โ ๐, ๐ฆ โ ๐ โฆ if(๐ฅ = ๐ฆ, ๐, (0gโ๐
)))) |
34 | | eqeq12 2750 |
. . . . . . . . . . . . . . . . 17
โข ((๐ฅ = ๐ โง ๐ฆ = ๐) โ (๐ฅ = ๐ฆ โ ๐ = ๐)) |
35 | 34 | ifbid 4513 |
. . . . . . . . . . . . . . . 16
โข ((๐ฅ = ๐ โง ๐ฆ = ๐) โ if(๐ฅ = ๐ฆ, ๐, (0gโ๐
)) = if(๐ = ๐, ๐, (0gโ๐
))) |
36 | 35 | adantl 483 |
. . . . . . . . . . . . . . 15
โข
((((((((๐ โ Fin
โง ๐
โ Ring) โง
๐ถ โ ๐) โง ๐ โ ๐พ) โง ๐ โ ๐ต) โง (๐ โ ๐ โง ๐ โ ๐)) โง ๐ โ ๐) โง (๐ฅ = ๐ โง ๐ฆ = ๐)) โ if(๐ฅ = ๐ฆ, ๐, (0gโ๐
)) = if(๐ = ๐, ๐, (0gโ๐
))) |
37 | | simpl 484 |
. . . . . . . . . . . . . . . . 17
โข ((๐ โ ๐ โง ๐ โ ๐) โ ๐ โ ๐) |
38 | 37 | adantl 483 |
. . . . . . . . . . . . . . . 16
โข
((((((๐ โ Fin
โง ๐
โ Ring) โง
๐ถ โ ๐) โง ๐ โ ๐พ) โง ๐ โ ๐ต) โง (๐ โ ๐ โง ๐ โ ๐)) โ ๐ โ ๐) |
39 | 38 | adantr 482 |
. . . . . . . . . . . . . . 15
โข
(((((((๐ โ Fin
โง ๐
โ Ring) โง
๐ถ โ ๐) โง ๐ โ ๐พ) โง ๐ โ ๐ต) โง (๐ โ ๐ โง ๐ โ ๐)) โง ๐ โ ๐) โ ๐ โ ๐) |
40 | | simpr 486 |
. . . . . . . . . . . . . . 15
โข
(((((((๐ โ Fin
โง ๐
โ Ring) โง
๐ถ โ ๐) โง ๐ โ ๐พ) โง ๐ โ ๐ต) โง (๐ โ ๐ โง ๐ โ ๐)) โง ๐ โ ๐) โ ๐ โ ๐) |
41 | | vex 3451 |
. . . . . . . . . . . . . . . . 17
โข ๐ โ V |
42 | | fvex 6859 |
. . . . . . . . . . . . . . . . 17
โข
(0gโ๐
) โ V |
43 | 41, 42 | ifex 4540 |
. . . . . . . . . . . . . . . 16
โข if(๐ = ๐, ๐, (0gโ๐
)) โ V |
44 | 43 | a1i 11 |
. . . . . . . . . . . . . . 15
โข
(((((((๐ โ Fin
โง ๐
โ Ring) โง
๐ถ โ ๐) โง ๐ โ ๐พ) โง ๐ โ ๐ต) โง (๐ โ ๐ โง ๐ โ ๐)) โง ๐ โ ๐) โ if(๐ = ๐, ๐, (0gโ๐
)) โ V) |
45 | 33, 36, 39, 40, 44 | ovmpod 7511 |
. . . . . . . . . . . . . 14
โข
(((((((๐ โ Fin
โง ๐
โ Ring) โง
๐ถ โ ๐) โง ๐ โ ๐พ) โง ๐ โ ๐ต) โง (๐ โ ๐ โง ๐ โ ๐)) โง ๐ โ ๐) โ (๐(๐ โ
(1rโ๐ด))๐) = if(๐ = ๐, ๐, (0gโ๐
))) |
46 | 45 | oveq1d 7376 |
. . . . . . . . . . . . 13
โข
(((((((๐ โ Fin
โง ๐
โ Ring) โง
๐ถ โ ๐) โง ๐ โ ๐พ) โง ๐ โ ๐ต) โง (๐ โ ๐ โง ๐ โ ๐)) โง ๐ โ ๐) โ ((๐(๐ โ
(1rโ๐ด))๐)(.rโ๐
)(๐๐๐)) = (if(๐ = ๐, ๐, (0gโ๐
))(.rโ๐
)(๐๐๐))) |
47 | 46 | mpteq2dva 5209 |
. . . . . . . . . . . 12
โข
((((((๐ โ Fin
โง ๐
โ Ring) โง
๐ถ โ ๐) โง ๐ โ ๐พ) โง ๐ โ ๐ต) โง (๐ โ ๐ โง ๐ โ ๐)) โ (๐ โ ๐ โฆ ((๐(๐ โ
(1rโ๐ด))๐)(.rโ๐
)(๐๐๐))) = (๐ โ ๐ โฆ (if(๐ = ๐, ๐, (0gโ๐
))(.rโ๐
)(๐๐๐)))) |
48 | 47 | oveq2d 7377 |
. . . . . . . . . . 11
โข
((((((๐ โ Fin
โง ๐
โ Ring) โง
๐ถ โ ๐) โง ๐ โ ๐พ) โง ๐ โ ๐ต) โง (๐ โ ๐ โง ๐ โ ๐)) โ (๐
ฮฃg (๐ โ ๐ โฆ ((๐(๐ โ
(1rโ๐ด))๐)(.rโ๐
)(๐๐๐)))) = (๐
ฮฃg (๐ โ ๐ โฆ (if(๐ = ๐, ๐, (0gโ๐
))(.rโ๐
)(๐๐๐))))) |
49 | | ovif 7458 |
. . . . . . . . . . . . . 14
โข (if(๐ = ๐, ๐, (0gโ๐
))(.rโ๐
)(๐๐๐)) = if(๐ = ๐, (๐(.rโ๐
)(๐๐๐)), ((0gโ๐
)(.rโ๐
)(๐๐๐))) |
50 | | simp-6r 787 |
. . . . . . . . . . . . . . . 16
โข
(((((((๐ โ Fin
โง ๐
โ Ring) โง
๐ถ โ ๐) โง ๐ โ ๐พ) โง ๐ โ ๐ต) โง (๐ โ ๐ โง ๐ โ ๐)) โง ๐ โ ๐) โ ๐
โ Ring) |
51 | | simplrr 777 |
. . . . . . . . . . . . . . . . 17
โข
(((((((๐ โ Fin
โง ๐
โ Ring) โง
๐ถ โ ๐) โง ๐ โ ๐พ) โง ๐ โ ๐ต) โง (๐ โ ๐ โง ๐ โ ๐)) โง ๐ โ ๐) โ ๐ โ ๐) |
52 | | simpr 486 |
. . . . . . . . . . . . . . . . . 18
โข
(((((๐ โ Fin
โง ๐
โ Ring) โง
๐ถ โ ๐) โง ๐ โ ๐พ) โง ๐ โ ๐ต) โ ๐ โ ๐ต) |
53 | 52 | ad2antrr 725 |
. . . . . . . . . . . . . . . . 17
โข
(((((((๐ โ Fin
โง ๐
โ Ring) โง
๐ถ โ ๐) โง ๐ โ ๐พ) โง ๐ โ ๐ต) โง (๐ โ ๐ โง ๐ โ ๐)) โง ๐ โ ๐) โ ๐ โ ๐ต) |
54 | 2, 1, 3, 40, 51, 53 | matecld 21798 |
. . . . . . . . . . . . . . . 16
โข
(((((((๐ โ Fin
โง ๐
โ Ring) โง
๐ถ โ ๐) โง ๐ โ ๐พ) โง ๐ โ ๐ต) โง (๐ โ ๐ โง ๐ โ ๐)) โง ๐ โ ๐) โ (๐๐๐) โ ๐พ) |
55 | | eqid 2733 |
. . . . . . . . . . . . . . . . 17
โข
(.rโ๐
) = (.rโ๐
) |
56 | 1, 55, 31 | ringlz 20019 |
. . . . . . . . . . . . . . . 16
โข ((๐
โ Ring โง (๐๐๐) โ ๐พ) โ ((0gโ๐
)(.rโ๐
)(๐๐๐)) = (0gโ๐
)) |
57 | 50, 54, 56 | syl2anc 585 |
. . . . . . . . . . . . . . 15
โข
(((((((๐ โ Fin
โง ๐
โ Ring) โง
๐ถ โ ๐) โง ๐ โ ๐พ) โง ๐ โ ๐ต) โง (๐ โ ๐ โง ๐ โ ๐)) โง ๐ โ ๐) โ ((0gโ๐
)(.rโ๐
)(๐๐๐)) = (0gโ๐
)) |
58 | 57 | ifeq2d 4510 |
. . . . . . . . . . . . . 14
โข
(((((((๐ โ Fin
โง ๐
โ Ring) โง
๐ถ โ ๐) โง ๐ โ ๐พ) โง ๐ โ ๐ต) โง (๐ โ ๐ โง ๐ โ ๐)) โง ๐ โ ๐) โ if(๐ = ๐, (๐(.rโ๐
)(๐๐๐)), ((0gโ๐
)(.rโ๐
)(๐๐๐))) = if(๐ = ๐, (๐(.rโ๐
)(๐๐๐)), (0gโ๐
))) |
59 | 49, 58 | eqtrid 2785 |
. . . . . . . . . . . . 13
โข
(((((((๐ โ Fin
โง ๐
โ Ring) โง
๐ถ โ ๐) โง ๐ โ ๐พ) โง ๐ โ ๐ต) โง (๐ โ ๐ โง ๐ โ ๐)) โง ๐ โ ๐) โ (if(๐ = ๐, ๐, (0gโ๐
))(.rโ๐
)(๐๐๐)) = if(๐ = ๐, (๐(.rโ๐
)(๐๐๐)), (0gโ๐
))) |
60 | 59 | mpteq2dva 5209 |
. . . . . . . . . . . 12
โข
((((((๐ โ Fin
โง ๐
โ Ring) โง
๐ถ โ ๐) โง ๐ โ ๐พ) โง ๐ โ ๐ต) โง (๐ โ ๐ โง ๐ โ ๐)) โ (๐ โ ๐ โฆ (if(๐ = ๐, ๐, (0gโ๐
))(.rโ๐
)(๐๐๐))) = (๐ โ ๐ โฆ if(๐ = ๐, (๐(.rโ๐
)(๐๐๐)), (0gโ๐
)))) |
61 | 60 | oveq2d 7377 |
. . . . . . . . . . 11
โข
((((((๐ โ Fin
โง ๐
โ Ring) โง
๐ถ โ ๐) โง ๐ โ ๐พ) โง ๐ โ ๐ต) โง (๐ โ ๐ โง ๐ โ ๐)) โ (๐
ฮฃg (๐ โ ๐ โฆ (if(๐ = ๐, ๐, (0gโ๐
))(.rโ๐
)(๐๐๐)))) = (๐
ฮฃg (๐ โ ๐ โฆ if(๐ = ๐, (๐(.rโ๐
)(๐๐๐)), (0gโ๐
))))) |
62 | | ringmnd 19982 |
. . . . . . . . . . . . . 14
โข (๐
โ Ring โ ๐
โ Mnd) |
63 | 62 | adantl 483 |
. . . . . . . . . . . . 13
โข ((๐ โ Fin โง ๐
โ Ring) โ ๐
โ Mnd) |
64 | 63 | ad4antr 731 |
. . . . . . . . . . . 12
โข
((((((๐ โ Fin
โง ๐
โ Ring) โง
๐ถ โ ๐) โง ๐ โ ๐พ) โง ๐ โ ๐ต) โง (๐ โ ๐ โง ๐ โ ๐)) โ ๐
โ Mnd) |
65 | | simpl 484 |
. . . . . . . . . . . . 13
โข ((๐ โ Fin โง ๐
โ Ring) โ ๐ โ Fin) |
66 | 65 | ad4antr 731 |
. . . . . . . . . . . 12
โข
((((((๐ โ Fin
โง ๐
โ Ring) โง
๐ถ โ ๐) โง ๐ โ ๐พ) โง ๐ โ ๐ต) โง (๐ โ ๐ โง ๐ โ ๐)) โ ๐ โ Fin) |
67 | | equcom 2022 |
. . . . . . . . . . . . . 14
โข (๐ = ๐ โ ๐ = ๐) |
68 | | ifbi 4512 |
. . . . . . . . . . . . . 14
โข ((๐ = ๐ โ ๐ = ๐) โ if(๐ = ๐, (๐(.rโ๐
)(๐๐๐)), (0gโ๐
)) = if(๐ = ๐, (๐(.rโ๐
)(๐๐๐)), (0gโ๐
))) |
69 | 67, 68 | ax-mp 5 |
. . . . . . . . . . . . 13
โข if(๐ = ๐, (๐(.rโ๐
)(๐๐๐)), (0gโ๐
)) = if(๐ = ๐, (๐(.rโ๐
)(๐๐๐)), (0gโ๐
)) |
70 | 69 | mpteq2i 5214 |
. . . . . . . . . . . 12
โข (๐ โ ๐ โฆ if(๐ = ๐, (๐(.rโ๐
)(๐๐๐)), (0gโ๐
))) = (๐ โ ๐ โฆ if(๐ = ๐, (๐(.rโ๐
)(๐๐๐)), (0gโ๐
))) |
71 | 1 | eleq2i 2826 |
. . . . . . . . . . . . . . . . 17
โข (๐ โ ๐พ โ ๐ โ (Baseโ๐
)) |
72 | 71 | biimpi 215 |
. . . . . . . . . . . . . . . 16
โข (๐ โ ๐พ โ ๐ โ (Baseโ๐
)) |
73 | 72 | adantl 483 |
. . . . . . . . . . . . . . 15
โข ((((๐ โ Fin โง ๐
โ Ring) โง ๐ถ โ ๐) โง ๐ โ ๐พ) โ ๐ โ (Baseโ๐
)) |
74 | 73 | ad3antrrr 729 |
. . . . . . . . . . . . . 14
โข
(((((((๐ โ Fin
โง ๐
โ Ring) โง
๐ถ โ ๐) โง ๐ โ ๐พ) โง ๐ โ ๐ต) โง (๐ โ ๐ โง ๐ โ ๐)) โง ๐ โ ๐) โ ๐ โ (Baseโ๐
)) |
75 | | eqid 2733 |
. . . . . . . . . . . . . . 15
โข
(Baseโ๐
) =
(Baseโ๐
) |
76 | 2, 75, 3, 40, 51, 53 | matecld 21798 |
. . . . . . . . . . . . . 14
โข
(((((((๐ โ Fin
โง ๐
โ Ring) โง
๐ถ โ ๐) โง ๐ โ ๐พ) โง ๐ โ ๐ต) โง (๐ โ ๐ โง ๐ โ ๐)) โง ๐ โ ๐) โ (๐๐๐) โ (Baseโ๐
)) |
77 | 75, 55 | ringcl 19989 |
. . . . . . . . . . . . . 14
โข ((๐
โ Ring โง ๐ โ (Baseโ๐
) โง (๐๐๐) โ (Baseโ๐
)) โ (๐(.rโ๐
)(๐๐๐)) โ (Baseโ๐
)) |
78 | 50, 74, 76, 77 | syl3anc 1372 |
. . . . . . . . . . . . 13
โข
(((((((๐ โ Fin
โง ๐
โ Ring) โง
๐ถ โ ๐) โง ๐ โ ๐พ) โง ๐ โ ๐ต) โง (๐ โ ๐ โง ๐ โ ๐)) โง ๐ โ ๐) โ (๐(.rโ๐
)(๐๐๐)) โ (Baseโ๐
)) |
79 | 78 | ralrimiva 3140 |
. . . . . . . . . . . 12
โข
((((((๐ โ Fin
โง ๐
โ Ring) โง
๐ถ โ ๐) โง ๐ โ ๐พ) โง ๐ โ ๐ต) โง (๐ โ ๐ โง ๐ โ ๐)) โ โ๐ โ ๐ (๐(.rโ๐
)(๐๐๐)) โ (Baseโ๐
)) |
80 | 31, 64, 66, 38, 70, 79 | gsummpt1n0 19750 |
. . . . . . . . . . 11
โข
((((((๐ โ Fin
โง ๐
โ Ring) โง
๐ถ โ ๐) โง ๐ โ ๐พ) โง ๐ โ ๐ต) โง (๐ โ ๐ โง ๐ โ ๐)) โ (๐
ฮฃg (๐ โ ๐ โฆ if(๐ = ๐, (๐(.rโ๐
)(๐๐๐)), (0gโ๐
)))) = โฆ๐ / ๐โฆ(๐(.rโ๐
)(๐๐๐))) |
81 | 48, 61, 80 | 3eqtrd 2777 |
. . . . . . . . . 10
โข
((((((๐ โ Fin
โง ๐
โ Ring) โง
๐ถ โ ๐) โง ๐ โ ๐พ) โง ๐ โ ๐ต) โง (๐ โ ๐ โง ๐ โ ๐)) โ (๐
ฮฃg (๐ โ ๐ โฆ ((๐(๐ โ
(1rโ๐ด))๐)(.rโ๐
)(๐๐๐)))) = โฆ๐ / ๐โฆ(๐(.rโ๐
)(๐๐๐))) |
82 | | csbov2g 7407 |
. . . . . . . . . . . . 13
โข (๐ โ ๐ โ โฆ๐ / ๐โฆ(๐(.rโ๐
)(๐๐๐)) = (๐(.rโ๐
)โฆ๐ / ๐โฆ(๐๐๐))) |
83 | | csbov1g 7406 |
. . . . . . . . . . . . . . 15
โข (๐ โ ๐ โ โฆ๐ / ๐โฆ(๐๐๐) = (โฆ๐ / ๐โฆ๐๐๐)) |
84 | | csbvarg 4395 |
. . . . . . . . . . . . . . . 16
โข (๐ โ ๐ โ โฆ๐ / ๐โฆ๐ = ๐) |
85 | 84 | oveq1d 7376 |
. . . . . . . . . . . . . . 15
โข (๐ โ ๐ โ (โฆ๐ / ๐โฆ๐๐๐) = (๐๐๐)) |
86 | 83, 85 | eqtrd 2773 |
. . . . . . . . . . . . . 14
โข (๐ โ ๐ โ โฆ๐ / ๐โฆ(๐๐๐) = (๐๐๐)) |
87 | 86 | oveq2d 7377 |
. . . . . . . . . . . . 13
โข (๐ โ ๐ โ (๐(.rโ๐
)โฆ๐ / ๐โฆ(๐๐๐)) = (๐(.rโ๐
)(๐๐๐))) |
88 | 82, 87 | eqtrd 2773 |
. . . . . . . . . . . 12
โข (๐ โ ๐ โ โฆ๐ / ๐โฆ(๐(.rโ๐
)(๐๐๐)) = (๐(.rโ๐
)(๐๐๐))) |
89 | 88 | adantr 482 |
. . . . . . . . . . 11
โข ((๐ โ ๐ โง ๐ โ ๐) โ โฆ๐ / ๐โฆ(๐(.rโ๐
)(๐๐๐)) = (๐(.rโ๐
)(๐๐๐))) |
90 | 89 | adantl 483 |
. . . . . . . . . 10
โข
((((((๐ โ Fin
โง ๐
โ Ring) โง
๐ถ โ ๐) โง ๐ โ ๐พ) โง ๐ โ ๐ต) โง (๐ โ ๐ โง ๐ โ ๐)) โ โฆ๐ / ๐โฆ(๐(.rโ๐
)(๐๐๐)) = (๐(.rโ๐
)(๐๐๐))) |
91 | 26, 81, 90 | 3eqtrd 2777 |
. . . . . . . . 9
โข
((((((๐ โ Fin
โง ๐
โ Ring) โง
๐ถ โ ๐) โง ๐ โ ๐พ) โง ๐ โ ๐ต) โง (๐ โ ๐ โง ๐ โ ๐)) โ (๐((๐ โ
(1rโ๐ด))
ร
๐)๐) = (๐(.rโ๐
)(๐๐๐))) |
92 | | simpr 486 |
. . . . . . . . . . . 12
โข ((((๐ โ Fin โง ๐
โ Ring) โง ๐ถ โ ๐) โง ๐ โ ๐พ) โ ๐ โ ๐พ) |
93 | 92 | anim1i 616 |
. . . . . . . . . . 11
โข
(((((๐ โ Fin
โง ๐
โ Ring) โง
๐ถ โ ๐) โง ๐ โ ๐พ) โง ๐ โ ๐ต) โ (๐ โ ๐พ โง ๐ โ ๐ต)) |
94 | 93 | adantr 482 |
. . . . . . . . . 10
โข
((((((๐ โ Fin
โง ๐
โ Ring) โง
๐ถ โ ๐) โง ๐ โ ๐พ) โง ๐ โ ๐ต) โง (๐ โ ๐ โง ๐ โ ๐)) โ (๐ โ ๐พ โง ๐ โ ๐ต)) |
95 | 2, 3, 1, 5, 55 | matvscacell 21808 |
. . . . . . . . . 10
โข ((๐
โ Ring โง (๐ โ ๐พ โง ๐ โ ๐ต) โง (๐ โ ๐ โง ๐ โ ๐)) โ (๐(๐ โ ๐)๐) = (๐(.rโ๐
)(๐๐๐))) |
96 | 11, 94, 23, 95 | syl3anc 1372 |
. . . . . . . . 9
โข
((((((๐ โ Fin
โง ๐
โ Ring) โง
๐ถ โ ๐) โง ๐ โ ๐พ) โง ๐ โ ๐ต) โง (๐ โ ๐ โง ๐ โ ๐)) โ (๐(๐ โ ๐)๐) = (๐(.rโ๐
)(๐๐๐))) |
97 | 91, 96 | eqtr4d 2776 |
. . . . . . . 8
โข
((((((๐ โ Fin
โง ๐
โ Ring) โง
๐ถ โ ๐) โง ๐ โ ๐พ) โง ๐ โ ๐ต) โง (๐ โ ๐ โง ๐ โ ๐)) โ (๐((๐ โ
(1rโ๐ด))
ร
๐)๐) = (๐(๐ โ ๐)๐)) |
98 | 97 | ralrimivva 3194 |
. . . . . . 7
โข
(((((๐ โ Fin
โง ๐
โ Ring) โง
๐ถ โ ๐) โง ๐ โ ๐พ) โง ๐ โ ๐ต) โ โ๐ โ ๐ โ๐ โ ๐ (๐((๐ โ
(1rโ๐ด))
ร
๐)๐) = (๐(๐ โ ๐)๐)) |
99 | 14 | ad3antrrr 729 |
. . . . . . . . 9
โข
(((((๐ โ Fin
โง ๐
โ Ring) โง
๐ถ โ ๐) โง ๐ โ ๐พ) โง ๐ โ ๐ต) โ ๐ด โ Ring) |
100 | 20 | adantr 482 |
. . . . . . . . 9
โข
(((((๐ โ Fin
โง ๐
โ Ring) โง
๐ถ โ ๐) โง ๐ โ ๐พ) โง ๐ โ ๐ต) โ (๐ โ
(1rโ๐ด))
โ ๐ต) |
101 | 3, 24 | ringcl 19989 |
. . . . . . . . 9
โข ((๐ด โ Ring โง (๐ โ
(1rโ๐ด))
โ ๐ต โง ๐ โ ๐ต) โ ((๐ โ
(1rโ๐ด))
ร
๐) โ ๐ต) |
102 | 99, 100, 52, 101 | syl3anc 1372 |
. . . . . . . 8
โข
(((((๐ โ Fin
โง ๐
โ Ring) โง
๐ถ โ ๐) โง ๐ โ ๐พ) โง ๐ โ ๐ต) โ ((๐ โ
(1rโ๐ด))
ร
๐) โ ๐ต) |
103 | 12 | ad2antrr 725 |
. . . . . . . . 9
โข
(((((๐ โ Fin
โง ๐
โ Ring) โง
๐ถ โ ๐) โง ๐ โ ๐พ) โง ๐ โ ๐ต) โ (๐ โ Fin โง ๐
โ Ring)) |
104 | 1, 2, 3, 5 | matvscl 21803 |
. . . . . . . . 9
โข (((๐ โ Fin โง ๐
โ Ring) โง (๐ โ ๐พ โง ๐ โ ๐ต)) โ (๐ โ ๐) โ ๐ต) |
105 | 103, 93, 104 | syl2anc 585 |
. . . . . . . 8
โข
(((((๐ โ Fin
โง ๐
โ Ring) โง
๐ถ โ ๐) โง ๐ โ ๐พ) โง ๐ โ ๐ต) โ (๐ โ ๐) โ ๐ต) |
106 | 2, 3 | eqmat 21796 |
. . . . . . . 8
โข ((((๐ โ
(1rโ๐ด))
ร
๐) โ ๐ต โง (๐ โ ๐) โ ๐ต) โ (((๐ โ
(1rโ๐ด))
ร
๐) = (๐ โ ๐) โ โ๐ โ ๐ โ๐ โ ๐ (๐((๐ โ
(1rโ๐ด))
ร
๐)๐) = (๐(๐ โ ๐)๐))) |
107 | 102, 105,
106 | syl2anc 585 |
. . . . . . 7
โข
(((((๐ โ Fin
โง ๐
โ Ring) โง
๐ถ โ ๐) โง ๐ โ ๐พ) โง ๐ โ ๐ต) โ (((๐ โ
(1rโ๐ด))
ร
๐) = (๐ โ ๐) โ โ๐ โ ๐ โ๐ โ ๐ (๐((๐ โ
(1rโ๐ด))
ร
๐)๐) = (๐(๐ โ ๐)๐))) |
108 | 98, 107 | mpbird 257 |
. . . . . 6
โข
(((((๐ โ Fin
โง ๐
โ Ring) โง
๐ถ โ ๐) โง ๐ โ ๐พ) โง ๐ โ ๐ต) โ ((๐ โ
(1rโ๐ด))
ร
๐) = (๐ โ ๐)) |
109 | 9, 108 | sylan9eqr 2795 |
. . . . 5
โข
((((((๐ โ Fin
โง ๐
โ Ring) โง
๐ถ โ ๐) โง ๐ โ ๐พ) โง ๐ โ ๐ต) โง ๐ถ = (๐ โ
(1rโ๐ด)))
โ (๐ถ ร ๐) = (๐ โ ๐)) |
110 | 109 | ex 414 |
. . . 4
โข
(((((๐ โ Fin
โง ๐
โ Ring) โง
๐ถ โ ๐) โง ๐ โ ๐พ) โง ๐ โ ๐ต) โ (๐ถ = (๐ โ
(1rโ๐ด))
โ (๐ถ ร ๐) = (๐ โ ๐))) |
111 | 110 | ralrimdva 3148 |
. . 3
โข ((((๐ โ Fin โง ๐
โ Ring) โง ๐ถ โ ๐) โง ๐ โ ๐พ) โ (๐ถ = (๐ โ
(1rโ๐ด))
โ โ๐ โ
๐ต (๐ถ ร ๐) = (๐ โ ๐))) |
112 | 111 | reximdva 3162 |
. 2
โข (((๐ โ Fin โง ๐
โ Ring) โง ๐ถ โ ๐) โ (โ๐ โ ๐พ ๐ถ = (๐ โ
(1rโ๐ด))
โ โ๐ โ
๐พ โ๐ โ ๐ต (๐ถ ร ๐) = (๐ โ ๐))) |
113 | 8, 112 | mpd 15 |
1
โข (((๐ โ Fin โง ๐
โ Ring) โง ๐ถ โ ๐) โ โ๐ โ ๐พ โ๐ โ ๐ต (๐ถ ร ๐) = (๐ โ ๐)) |