Step | Hyp | Ref
| Expression |
1 | | matplusgcell.a |
. . . . 5
โข ๐ด = (๐ Mat ๐
) |
2 | | matplusgcell.b |
. . . . 5
โข ๐ต = (Baseโ๐ด) |
3 | | matvscacell.k |
. . . . 5
โข ๐พ = (Baseโ๐
) |
4 | | matvscacell.v |
. . . . 5
โข ยท = (
ยท๐ โ๐ด) |
5 | | matvscacell.t |
. . . . 5
โข ร =
(.rโ๐
) |
6 | | eqid 2732 |
. . . . 5
โข (๐ ร ๐) = (๐ ร ๐) |
7 | 1, 2, 3, 4, 5, 6 | matvsca2 21921 |
. . . 4
โข ((๐ โ ๐พ โง ๐ โ ๐ต) โ (๐ ยท ๐) = (((๐ ร ๐) ร {๐}) โf ร ๐)) |
8 | 7 | oveqd 7422 |
. . 3
โข ((๐ โ ๐พ โง ๐ โ ๐ต) โ (๐ผ(๐ ยท ๐)๐ฝ) = (๐ผ(((๐ ร ๐) ร {๐}) โf ร ๐)๐ฝ)) |
9 | 8 | 3ad2ant2 1134 |
. 2
โข ((๐
โ Ring โง (๐ โ ๐พ โง ๐ โ ๐ต) โง (๐ผ โ ๐ โง ๐ฝ โ ๐)) โ (๐ผ(๐ ยท ๐)๐ฝ) = (๐ผ(((๐ ร ๐) ร {๐}) โf ร ๐)๐ฝ)) |
10 | | df-ov 7408 |
. . 3
โข (๐ผ(((๐ ร ๐) ร {๐}) โf ร ๐)๐ฝ) = ((((๐ ร ๐) ร {๐}) โf ร ๐)โโจ๐ผ, ๐ฝโฉ) |
11 | 10 | a1i 11 |
. 2
โข ((๐
โ Ring โง (๐ โ ๐พ โง ๐ โ ๐ต) โง (๐ผ โ ๐ โง ๐ฝ โ ๐)) โ (๐ผ(((๐ ร ๐) ร {๐}) โf ร ๐)๐ฝ) = ((((๐ ร ๐) ร {๐}) โf ร ๐)โโจ๐ผ, ๐ฝโฉ)) |
12 | | opelxpi 5712 |
. . . 4
โข ((๐ผ โ ๐ โง ๐ฝ โ ๐) โ โจ๐ผ, ๐ฝโฉ โ (๐ ร ๐)) |
13 | 12 | 3ad2ant3 1135 |
. . 3
โข ((๐
โ Ring โง (๐ โ ๐พ โง ๐ โ ๐ต) โง (๐ผ โ ๐ โง ๐ฝ โ ๐)) โ โจ๐ผ, ๐ฝโฉ โ (๐ ร ๐)) |
14 | 1, 2 | matrcl 21903 |
. . . . . . . 8
โข (๐ โ ๐ต โ (๐ โ Fin โง ๐
โ V)) |
15 | 14 | simpld 495 |
. . . . . . 7
โข (๐ โ ๐ต โ ๐ โ Fin) |
16 | 15 | adantl 482 |
. . . . . 6
โข ((๐ โ ๐พ โง ๐ โ ๐ต) โ ๐ โ Fin) |
17 | 16 | 3ad2ant2 1134 |
. . . . 5
โข ((๐
โ Ring โง (๐ โ ๐พ โง ๐ โ ๐ต) โง (๐ผ โ ๐ โง ๐ฝ โ ๐)) โ ๐ โ Fin) |
18 | | xpfi 9313 |
. . . . 5
โข ((๐ โ Fin โง ๐ โ Fin) โ (๐ ร ๐) โ Fin) |
19 | 17, 17, 18 | syl2anc 584 |
. . . 4
โข ((๐
โ Ring โง (๐ โ ๐พ โง ๐ โ ๐ต) โง (๐ผ โ ๐ โง ๐ฝ โ ๐)) โ (๐ ร ๐) โ Fin) |
20 | | simp2l 1199 |
. . . 4
โข ((๐
โ Ring โง (๐ โ ๐พ โง ๐ โ ๐ต) โง (๐ผ โ ๐ โง ๐ฝ โ ๐)) โ ๐ โ ๐พ) |
21 | 2 | eleq2i 2825 |
. . . . . . . . 9
โข (๐ โ ๐ต โ ๐ โ (Baseโ๐ด)) |
22 | 21 | biimpi 215 |
. . . . . . . 8
โข (๐ โ ๐ต โ ๐ โ (Baseโ๐ด)) |
23 | 22 | adantl 482 |
. . . . . . 7
โข ((๐ โ ๐พ โง ๐ โ ๐ต) โ ๐ โ (Baseโ๐ด)) |
24 | 23 | 3ad2ant2 1134 |
. . . . . 6
โข ((๐
โ Ring โง (๐ โ ๐พ โง ๐ โ ๐ต) โง (๐ผ โ ๐ โง ๐ฝ โ ๐)) โ ๐ โ (Baseโ๐ด)) |
25 | | simp1 1136 |
. . . . . . 7
โข ((๐
โ Ring โง (๐ โ ๐พ โง ๐ โ ๐ต) โง (๐ผ โ ๐ โง ๐ฝ โ ๐)) โ ๐
โ Ring) |
26 | | eqid 2732 |
. . . . . . . 8
โข
(Baseโ๐
) =
(Baseโ๐
) |
27 | 1, 26 | matbas2 21914 |
. . . . . . 7
โข ((๐ โ Fin โง ๐
โ Ring) โ
((Baseโ๐
)
โm (๐
ร ๐)) =
(Baseโ๐ด)) |
28 | 17, 25, 27 | syl2anc 584 |
. . . . . 6
โข ((๐
โ Ring โง (๐ โ ๐พ โง ๐ โ ๐ต) โง (๐ผ โ ๐ โง ๐ฝ โ ๐)) โ ((Baseโ๐
) โm (๐ ร ๐)) = (Baseโ๐ด)) |
29 | 24, 28 | eleqtrrd 2836 |
. . . . 5
โข ((๐
โ Ring โง (๐ โ ๐พ โง ๐ โ ๐ต) โง (๐ผ โ ๐ โง ๐ฝ โ ๐)) โ ๐ โ ((Baseโ๐
) โm (๐ ร ๐))) |
30 | | elmapfn 8855 |
. . . . 5
โข (๐ โ ((Baseโ๐
) โm (๐ ร ๐)) โ ๐ Fn (๐ ร ๐)) |
31 | 29, 30 | syl 17 |
. . . 4
โข ((๐
โ Ring โง (๐ โ ๐พ โง ๐ โ ๐ต) โง (๐ผ โ ๐ โง ๐ฝ โ ๐)) โ ๐ Fn (๐ ร ๐)) |
32 | | df-ov 7408 |
. . . . . 6
โข (๐ผ๐๐ฝ) = (๐โโจ๐ผ, ๐ฝโฉ) |
33 | 32 | eqcomi 2741 |
. . . . 5
โข (๐โโจ๐ผ, ๐ฝโฉ) = (๐ผ๐๐ฝ) |
34 | 33 | a1i 11 |
. . . 4
โข (((๐
โ Ring โง (๐ โ ๐พ โง ๐ โ ๐ต) โง (๐ผ โ ๐ โง ๐ฝ โ ๐)) โง โจ๐ผ, ๐ฝโฉ โ (๐ ร ๐)) โ (๐โโจ๐ผ, ๐ฝโฉ) = (๐ผ๐๐ฝ)) |
35 | 19, 20, 31, 34 | ofc1 7692 |
. . 3
โข (((๐
โ Ring โง (๐ โ ๐พ โง ๐ โ ๐ต) โง (๐ผ โ ๐ โง ๐ฝ โ ๐)) โง โจ๐ผ, ๐ฝโฉ โ (๐ ร ๐)) โ ((((๐ ร ๐) ร {๐}) โf ร ๐)โโจ๐ผ, ๐ฝโฉ) = (๐ ร (๐ผ๐๐ฝ))) |
36 | 13, 35 | mpdan 685 |
. 2
โข ((๐
โ Ring โง (๐ โ ๐พ โง ๐ โ ๐ต) โง (๐ผ โ ๐ โง ๐ฝ โ ๐)) โ ((((๐ ร ๐) ร {๐}) โf ร ๐)โโจ๐ผ, ๐ฝโฉ) = (๐ ร (๐ผ๐๐ฝ))) |
37 | 9, 11, 36 | 3eqtrd 2776 |
1
โข ((๐
โ Ring โง (๐ โ ๐พ โง ๐ โ ๐ต) โง (๐ผ โ ๐ โง ๐ฝ โ ๐)) โ (๐ผ(๐ ยท ๐)๐ฝ) = (๐ ร (๐ผ๐๐ฝ))) |