Step | Hyp | Ref
| Expression |
1 | | snex 5392 |
. . . . 5
โข {๐พ} โ V |
2 | 1 | a1i 11 |
. . . 4
โข ((๐ โ ๐ต โง ๐พ โ ๐ โง ๐ โ (Baseโ๐
)) โ {๐พ} โ V) |
3 | | smadiadet.a |
. . . . . . 7
โข ๐ด = (๐ Mat ๐
) |
4 | | smadiadet.b |
. . . . . . 7
โข ๐ต = (Baseโ๐ด) |
5 | 3, 4 | matrcl 21782 |
. . . . . 6
โข (๐ โ ๐ต โ (๐ โ Fin โง ๐
โ V)) |
6 | | elex 3465 |
. . . . . . 7
โข (๐ โ Fin โ ๐ โ V) |
7 | 6 | adantr 482 |
. . . . . 6
โข ((๐ โ Fin โง ๐
โ V) โ ๐ โ V) |
8 | 5, 7 | syl 17 |
. . . . 5
โข (๐ โ ๐ต โ ๐ โ V) |
9 | 8 | 3ad2ant1 1134 |
. . . 4
โข ((๐ โ ๐ต โง ๐พ โ ๐ โง ๐ โ (Baseโ๐
)) โ ๐ โ V) |
10 | | simp13 1206 |
. . . 4
โข (((๐ โ ๐ต โง ๐พ โ ๐ โง ๐ โ (Baseโ๐
)) โง ๐ โ {๐พ} โง ๐ โ ๐) โ ๐ โ (Baseโ๐
)) |
11 | | smadiadet.r |
. . . . . 6
โข ๐
โ CRing |
12 | | crngring 19984 |
. . . . . 6
โข (๐
โ CRing โ ๐
โ Ring) |
13 | 11, 12 | mp1i 13 |
. . . . 5
โข (((๐ โ ๐ต โง ๐พ โ ๐ โง ๐ โ (Baseโ๐
)) โง ๐ โ {๐พ} โง ๐ โ ๐) โ ๐
โ Ring) |
14 | | eqid 2733 |
. . . . . . 7
โข
(Baseโ๐
) =
(Baseโ๐
) |
15 | | eqid 2733 |
. . . . . . 7
โข
(1rโ๐
) = (1rโ๐
) |
16 | 14, 15 | ringidcl 19997 |
. . . . . 6
โข (๐
โ Ring โ
(1rโ๐
)
โ (Baseโ๐
)) |
17 | | eqid 2733 |
. . . . . . 7
โข
(0gโ๐
) = (0gโ๐
) |
18 | 14, 17 | ring0cl 19998 |
. . . . . 6
โข (๐
โ Ring โ
(0gโ๐
)
โ (Baseโ๐
)) |
19 | 16, 18 | ifcld 4536 |
. . . . 5
โข (๐
โ Ring โ if(๐ = ๐พ, (1rโ๐
), (0gโ๐
)) โ (Baseโ๐
)) |
20 | 13, 19 | syl 17 |
. . . 4
โข (((๐ โ ๐ต โง ๐พ โ ๐ โง ๐ โ (Baseโ๐
)) โง ๐ โ {๐พ} โง ๐ โ ๐) โ if(๐ = ๐พ, (1rโ๐
), (0gโ๐
)) โ (Baseโ๐
)) |
21 | | fconstmpo 7477 |
. . . . 5
โข (({๐พ} ร ๐) ร {๐}) = (๐ โ {๐พ}, ๐ โ ๐ โฆ ๐) |
22 | 21 | a1i 11 |
. . . 4
โข ((๐ โ ๐ต โง ๐พ โ ๐ โง ๐ โ (Baseโ๐
)) โ (({๐พ} ร ๐) ร {๐}) = (๐ โ {๐พ}, ๐ โ ๐ โฆ ๐)) |
23 | | eqidd 2734 |
. . . 4
โข ((๐ โ ๐ต โง ๐พ โ ๐ โง ๐ โ (Baseโ๐
)) โ (๐ โ {๐พ}, ๐ โ ๐ โฆ if(๐ = ๐พ, (1rโ๐
), (0gโ๐
))) = (๐ โ {๐พ}, ๐ โ ๐ โฆ if(๐ = ๐พ, (1rโ๐
), (0gโ๐
)))) |
24 | 2, 9, 10, 20, 22, 23 | offval22 8024 |
. . 3
โข ((๐ โ ๐ต โง ๐พ โ ๐ โง ๐ โ (Baseโ๐
)) โ ((({๐พ} ร ๐) ร {๐}) โf ยท (๐ โ {๐พ}, ๐ โ ๐ โฆ if(๐ = ๐พ, (1rโ๐
), (0gโ๐
)))) = (๐ โ {๐พ}, ๐ โ ๐ โฆ (๐ ยท if(๐ = ๐พ, (1rโ๐
), (0gโ๐
))))) |
25 | 11, 12 | mp1i 13 |
. . . . . . . . . 10
โข (๐ โ (Baseโ๐
) โ ๐
โ Ring) |
26 | | smadiadetg.x |
. . . . . . . . . . 11
โข ยท =
(.rโ๐
) |
27 | 14, 26, 15 | ringridm 20001 |
. . . . . . . . . 10
โข ((๐
โ Ring โง ๐ โ (Baseโ๐
)) โ (๐ ยท
(1rโ๐
)) =
๐) |
28 | 25, 27 | mpancom 687 |
. . . . . . . . 9
โข (๐ โ (Baseโ๐
) โ (๐ ยท
(1rโ๐
)) =
๐) |
29 | 28 | 3ad2ant3 1136 |
. . . . . . . 8
โข ((๐ โ ๐ต โง ๐พ โ ๐ โง ๐ โ (Baseโ๐
)) โ (๐ ยท
(1rโ๐
)) =
๐) |
30 | 29 | ad2antrl 727 |
. . . . . . 7
โข ((๐ = ๐พ โง ((๐ โ ๐ต โง ๐พ โ ๐ โง ๐ โ (Baseโ๐
)) โง ๐ โ ๐)) โ (๐ ยท
(1rโ๐
)) =
๐) |
31 | | iftrue 4496 |
. . . . . . . . 9
โข (๐ = ๐พ โ if(๐ = ๐พ, (1rโ๐
), (0gโ๐
)) = (1rโ๐
)) |
32 | 31 | adantr 482 |
. . . . . . . 8
โข ((๐ = ๐พ โง ((๐ โ ๐ต โง ๐พ โ ๐ โง ๐ โ (Baseโ๐
)) โง ๐ โ ๐)) โ if(๐ = ๐พ, (1rโ๐
), (0gโ๐
)) = (1rโ๐
)) |
33 | 32 | oveq2d 7377 |
. . . . . . 7
โข ((๐ = ๐พ โง ((๐ โ ๐ต โง ๐พ โ ๐ โง ๐ โ (Baseโ๐
)) โง ๐ โ ๐)) โ (๐ ยท if(๐ = ๐พ, (1rโ๐
), (0gโ๐
))) = (๐ ยท
(1rโ๐
))) |
34 | | iftrue 4496 |
. . . . . . . 8
โข (๐ = ๐พ โ if(๐ = ๐พ, ๐, (0gโ๐
)) = ๐) |
35 | 34 | adantr 482 |
. . . . . . 7
โข ((๐ = ๐พ โง ((๐ โ ๐ต โง ๐พ โ ๐ โง ๐ โ (Baseโ๐
)) โง ๐ โ ๐)) โ if(๐ = ๐พ, ๐, (0gโ๐
)) = ๐) |
36 | 30, 33, 35 | 3eqtr4d 2783 |
. . . . . 6
โข ((๐ = ๐พ โง ((๐ โ ๐ต โง ๐พ โ ๐ โง ๐ โ (Baseโ๐
)) โง ๐ โ ๐)) โ (๐ ยท if(๐ = ๐พ, (1rโ๐
), (0gโ๐
))) = if(๐ = ๐พ, ๐, (0gโ๐
))) |
37 | 14, 26, 17 | ringrz 20020 |
. . . . . . . . . 10
โข ((๐
โ Ring โง ๐ โ (Baseโ๐
)) โ (๐ ยท
(0gโ๐
)) =
(0gโ๐
)) |
38 | 25, 37 | mpancom 687 |
. . . . . . . . 9
โข (๐ โ (Baseโ๐
) โ (๐ ยท
(0gโ๐
)) =
(0gโ๐
)) |
39 | 38 | 3ad2ant3 1136 |
. . . . . . . 8
โข ((๐ โ ๐ต โง ๐พ โ ๐ โง ๐ โ (Baseโ๐
)) โ (๐ ยท
(0gโ๐
)) =
(0gโ๐
)) |
40 | 39 | ad2antrl 727 |
. . . . . . 7
โข ((ยฌ
๐ = ๐พ โง ((๐ โ ๐ต โง ๐พ โ ๐ โง ๐ โ (Baseโ๐
)) โง ๐ โ ๐)) โ (๐ ยท
(0gโ๐
)) =
(0gโ๐
)) |
41 | | iffalse 4499 |
. . . . . . . . 9
โข (ยฌ
๐ = ๐พ โ if(๐ = ๐พ, (1rโ๐
), (0gโ๐
)) = (0gโ๐
)) |
42 | 41 | oveq2d 7377 |
. . . . . . . 8
โข (ยฌ
๐ = ๐พ โ (๐ ยท if(๐ = ๐พ, (1rโ๐
), (0gโ๐
))) = (๐ ยท
(0gโ๐
))) |
43 | 42 | adantr 482 |
. . . . . . 7
โข ((ยฌ
๐ = ๐พ โง ((๐ โ ๐ต โง ๐พ โ ๐ โง ๐ โ (Baseโ๐
)) โง ๐ โ ๐)) โ (๐ ยท if(๐ = ๐พ, (1rโ๐
), (0gโ๐
))) = (๐ ยท
(0gโ๐
))) |
44 | | iffalse 4499 |
. . . . . . . 8
โข (ยฌ
๐ = ๐พ โ if(๐ = ๐พ, ๐, (0gโ๐
)) = (0gโ๐
)) |
45 | 44 | adantr 482 |
. . . . . . 7
โข ((ยฌ
๐ = ๐พ โง ((๐ โ ๐ต โง ๐พ โ ๐ โง ๐ โ (Baseโ๐
)) โง ๐ โ ๐)) โ if(๐ = ๐พ, ๐, (0gโ๐
)) = (0gโ๐
)) |
46 | 40, 43, 45 | 3eqtr4d 2783 |
. . . . . 6
โข ((ยฌ
๐ = ๐พ โง ((๐ โ ๐ต โง ๐พ โ ๐ โง ๐ โ (Baseโ๐
)) โง ๐ โ ๐)) โ (๐ ยท if(๐ = ๐พ, (1rโ๐
), (0gโ๐
))) = if(๐ = ๐พ, ๐, (0gโ๐
))) |
47 | 36, 46 | pm2.61ian 811 |
. . . . 5
โข (((๐ โ ๐ต โง ๐พ โ ๐ โง ๐ โ (Baseโ๐
)) โง ๐ โ ๐) โ (๐ ยท if(๐ = ๐พ, (1rโ๐
), (0gโ๐
))) = if(๐ = ๐พ, ๐, (0gโ๐
))) |
48 | 47 | 3adant2 1132 |
. . . 4
โข (((๐ โ ๐ต โง ๐พ โ ๐ โง ๐ โ (Baseโ๐
)) โง ๐ โ {๐พ} โง ๐ โ ๐) โ (๐ ยท if(๐ = ๐พ, (1rโ๐
), (0gโ๐
))) = if(๐ = ๐พ, ๐, (0gโ๐
))) |
49 | 48 | mpoeq3dva 7438 |
. . 3
โข ((๐ โ ๐ต โง ๐พ โ ๐ โง ๐ โ (Baseโ๐
)) โ (๐ โ {๐พ}, ๐ โ ๐ โฆ (๐ ยท if(๐ = ๐พ, (1rโ๐
), (0gโ๐
)))) = (๐ โ {๐พ}, ๐ โ ๐ โฆ if(๐ = ๐พ, ๐, (0gโ๐
)))) |
50 | 24, 49 | eqtrd 2773 |
. 2
โข ((๐ โ ๐ต โง ๐พ โ ๐ โง ๐ โ (Baseโ๐
)) โ ((({๐พ} ร ๐) ร {๐}) โf ยท (๐ โ {๐พ}, ๐ โ ๐ โฆ if(๐ = ๐พ, (1rโ๐
), (0gโ๐
)))) = (๐ โ {๐พ}, ๐ โ ๐ โฆ if(๐ = ๐พ, ๐, (0gโ๐
)))) |
51 | | simp2 1138 |
. . . . . 6
โข ((๐ โ ๐ต โง ๐พ โ ๐ โง ๐ โ (Baseโ๐
)) โ ๐พ โ ๐) |
52 | | eqid 2733 |
. . . . . . 7
โข (๐ minMatR1 ๐
) = (๐ minMatR1 ๐
) |
53 | 3, 4, 52, 15, 17 | minmar1val 22020 |
. . . . . 6
โข ((๐ โ ๐ต โง ๐พ โ ๐ โง ๐พ โ ๐) โ (๐พ((๐ minMatR1 ๐
)โ๐)๐พ) = (๐ โ ๐, ๐ โ ๐ โฆ if(๐ = ๐พ, if(๐ = ๐พ, (1rโ๐
), (0gโ๐
)), (๐๐๐)))) |
54 | 51, 53 | syld3an3 1410 |
. . . . 5
โข ((๐ โ ๐ต โง ๐พ โ ๐ โง ๐ โ (Baseโ๐
)) โ (๐พ((๐ minMatR1 ๐
)โ๐)๐พ) = (๐ โ ๐, ๐ โ ๐ โฆ if(๐ = ๐พ, if(๐ = ๐พ, (1rโ๐
), (0gโ๐
)), (๐๐๐)))) |
55 | 54 | reseq1d 5940 |
. . . 4
โข ((๐ โ ๐ต โง ๐พ โ ๐ โง ๐ โ (Baseโ๐
)) โ ((๐พ((๐ minMatR1 ๐
)โ๐)๐พ) โพ ({๐พ} ร ๐)) = ((๐ โ ๐, ๐ โ ๐ โฆ if(๐ = ๐พ, if(๐ = ๐พ, (1rโ๐
), (0gโ๐
)), (๐๐๐))) โพ ({๐พ} ร ๐))) |
56 | | snssi 4772 |
. . . . . 6
โข (๐พ โ ๐ โ {๐พ} โ ๐) |
57 | 56 | 3ad2ant2 1135 |
. . . . 5
โข ((๐ โ ๐ต โง ๐พ โ ๐ โง ๐ โ (Baseโ๐
)) โ {๐พ} โ ๐) |
58 | | ssid 3970 |
. . . . 5
โข ๐ โ ๐ |
59 | | resmpo 7480 |
. . . . 5
โข (({๐พ} โ ๐ โง ๐ โ ๐) โ ((๐ โ ๐, ๐ โ ๐ โฆ if(๐ = ๐พ, if(๐ = ๐พ, (1rโ๐
), (0gโ๐
)), (๐๐๐))) โพ ({๐พ} ร ๐)) = (๐ โ {๐พ}, ๐ โ ๐ โฆ if(๐ = ๐พ, if(๐ = ๐พ, (1rโ๐
), (0gโ๐
)), (๐๐๐)))) |
60 | 57, 58, 59 | sylancl 587 |
. . . 4
โข ((๐ โ ๐ต โง ๐พ โ ๐ โง ๐ โ (Baseโ๐
)) โ ((๐ โ ๐, ๐ โ ๐ โฆ if(๐ = ๐พ, if(๐ = ๐พ, (1rโ๐
), (0gโ๐
)), (๐๐๐))) โพ ({๐พ} ร ๐)) = (๐ โ {๐พ}, ๐ โ ๐ โฆ if(๐ = ๐พ, if(๐ = ๐พ, (1rโ๐
), (0gโ๐
)), (๐๐๐)))) |
61 | | mposnif 7476 |
. . . . 5
โข (๐ โ {๐พ}, ๐ โ ๐ โฆ if(๐ = ๐พ, if(๐ = ๐พ, (1rโ๐
), (0gโ๐
)), (๐๐๐))) = (๐ โ {๐พ}, ๐ โ ๐ โฆ if(๐ = ๐พ, (1rโ๐
), (0gโ๐
))) |
62 | 61 | a1i 11 |
. . . 4
โข ((๐ โ ๐ต โง ๐พ โ ๐ โง ๐ โ (Baseโ๐
)) โ (๐ โ {๐พ}, ๐ โ ๐ โฆ if(๐ = ๐พ, if(๐ = ๐พ, (1rโ๐
), (0gโ๐
)), (๐๐๐))) = (๐ โ {๐พ}, ๐ โ ๐ โฆ if(๐ = ๐พ, (1rโ๐
), (0gโ๐
)))) |
63 | 55, 60, 62 | 3eqtrd 2777 |
. . 3
โข ((๐ โ ๐ต โง ๐พ โ ๐ โง ๐ โ (Baseโ๐
)) โ ((๐พ((๐ minMatR1 ๐
)โ๐)๐พ) โพ ({๐พ} ร ๐)) = (๐ โ {๐พ}, ๐ โ ๐ โฆ if(๐ = ๐พ, (1rโ๐
), (0gโ๐
)))) |
64 | 63 | oveq2d 7377 |
. 2
โข ((๐ โ ๐ต โง ๐พ โ ๐ โง ๐ โ (Baseโ๐
)) โ ((({๐พ} ร ๐) ร {๐}) โf ยท ((๐พ((๐ minMatR1 ๐
)โ๐)๐พ) โพ ({๐พ} ร ๐))) = ((({๐พ} ร ๐) ร {๐}) โf ยท (๐ โ {๐พ}, ๐ โ ๐ โฆ if(๐ = ๐พ, (1rโ๐
), (0gโ๐
))))) |
65 | | 3simpb 1150 |
. . . . 5
โข ((๐ โ ๐ต โง ๐พ โ ๐ โง ๐ โ (Baseโ๐
)) โ (๐ โ ๐ต โง ๐ โ (Baseโ๐
))) |
66 | | eqid 2733 |
. . . . . 6
โข (๐ matRRep ๐
) = (๐ matRRep ๐
) |
67 | 3, 4, 66, 17 | marrepval 21934 |
. . . . 5
โข (((๐ โ ๐ต โง ๐ โ (Baseโ๐
)) โง (๐พ โ ๐ โง ๐พ โ ๐)) โ (๐พ(๐(๐ matRRep ๐
)๐)๐พ) = (๐ โ ๐, ๐ โ ๐ โฆ if(๐ = ๐พ, if(๐ = ๐พ, ๐, (0gโ๐
)), (๐๐๐)))) |
68 | 65, 51, 51, 67 | syl12anc 836 |
. . . 4
โข ((๐ โ ๐ต โง ๐พ โ ๐ โง ๐ โ (Baseโ๐
)) โ (๐พ(๐(๐ matRRep ๐
)๐)๐พ) = (๐ โ ๐, ๐ โ ๐ โฆ if(๐ = ๐พ, if(๐ = ๐พ, ๐, (0gโ๐
)), (๐๐๐)))) |
69 | 68 | reseq1d 5940 |
. . 3
โข ((๐ โ ๐ต โง ๐พ โ ๐ โง ๐ โ (Baseโ๐
)) โ ((๐พ(๐(๐ matRRep ๐
)๐)๐พ) โพ ({๐พ} ร ๐)) = ((๐ โ ๐, ๐ โ ๐ โฆ if(๐ = ๐พ, if(๐ = ๐พ, ๐, (0gโ๐
)), (๐๐๐))) โพ ({๐พ} ร ๐))) |
70 | | resmpo 7480 |
. . . 4
โข (({๐พ} โ ๐ โง ๐ โ ๐) โ ((๐ โ ๐, ๐ โ ๐ โฆ if(๐ = ๐พ, if(๐ = ๐พ, ๐, (0gโ๐
)), (๐๐๐))) โพ ({๐พ} ร ๐)) = (๐ โ {๐พ}, ๐ โ ๐ โฆ if(๐ = ๐พ, if(๐ = ๐พ, ๐, (0gโ๐
)), (๐๐๐)))) |
71 | 57, 58, 70 | sylancl 587 |
. . 3
โข ((๐ โ ๐ต โง ๐พ โ ๐ โง ๐ โ (Baseโ๐
)) โ ((๐ โ ๐, ๐ โ ๐ โฆ if(๐ = ๐พ, if(๐ = ๐พ, ๐, (0gโ๐
)), (๐๐๐))) โพ ({๐พ} ร ๐)) = (๐ โ {๐พ}, ๐ โ ๐ โฆ if(๐ = ๐พ, if(๐ = ๐พ, ๐, (0gโ๐
)), (๐๐๐)))) |
72 | | mposnif 7476 |
. . . 4
โข (๐ โ {๐พ}, ๐ โ ๐ โฆ if(๐ = ๐พ, if(๐ = ๐พ, ๐, (0gโ๐
)), (๐๐๐))) = (๐ โ {๐พ}, ๐ โ ๐ โฆ if(๐ = ๐พ, ๐, (0gโ๐
))) |
73 | 72 | a1i 11 |
. . 3
โข ((๐ โ ๐ต โง ๐พ โ ๐ โง ๐ โ (Baseโ๐
)) โ (๐ โ {๐พ}, ๐ โ ๐ โฆ if(๐ = ๐พ, if(๐ = ๐พ, ๐, (0gโ๐
)), (๐๐๐))) = (๐ โ {๐พ}, ๐ โ ๐ โฆ if(๐ = ๐พ, ๐, (0gโ๐
)))) |
74 | 69, 71, 73 | 3eqtrd 2777 |
. 2
โข ((๐ โ ๐ต โง ๐พ โ ๐ โง ๐ โ (Baseโ๐
)) โ ((๐พ(๐(๐ matRRep ๐
)๐)๐พ) โพ ({๐พ} ร ๐)) = (๐ โ {๐พ}, ๐ โ ๐ โฆ if(๐ = ๐พ, ๐, (0gโ๐
)))) |
75 | 50, 64, 74 | 3eqtr4rd 2784 |
1
โข ((๐ โ ๐ต โง ๐พ โ ๐ โง ๐ โ (Baseโ๐
)) โ ((๐พ(๐(๐ matRRep ๐
)๐)๐พ) โพ ({๐พ} ร ๐)) = ((({๐พ} ร ๐) ร {๐}) โf ยท ((๐พ((๐ minMatR1 ๐
)โ๐)๐พ) โพ ({๐พ} ร ๐)))) |