Step | Hyp | Ref
| Expression |
1 | | simprl 770 |
. . . . . 6
โข (((๐ โ Fin โง ๐
โ Ring) โง (๐ โ ๐ต โง ๐ โ ๐ต)) โ ๐ โ ๐ต) |
2 | | scmatscmide.1 |
. . . . . . . 8
โข 1 =
(1rโ๐ด) |
3 | | scmatscmide.a |
. . . . . . . . 9
โข ๐ด = (๐ Mat ๐
) |
4 | | eqid 2733 |
. . . . . . . . 9
โข
(Baseโ๐ด) =
(Baseโ๐ด) |
5 | | scmatscmide.0 |
. . . . . . . . 9
โข 0 =
(0gโ๐
) |
6 | | eqid 2733 |
. . . . . . . . 9
โข (๐ DMat ๐
) = (๐ DMat ๐
) |
7 | 3, 4, 5, 6 | dmatid 21867 |
. . . . . . . 8
โข ((๐ โ Fin โง ๐
โ Ring) โ
(1rโ๐ด)
โ (๐ DMat ๐
)) |
8 | 2, 7 | eqeltrid 2838 |
. . . . . . 7
โข ((๐ โ Fin โง ๐
โ Ring) โ 1 โ (๐ DMat ๐
)) |
9 | 8 | adantr 482 |
. . . . . 6
โข (((๐ โ Fin โง ๐
โ Ring) โง (๐ โ ๐ต โง ๐ โ ๐ต)) โ 1 โ (๐ DMat ๐
)) |
10 | 1, 9 | jca 513 |
. . . . 5
โข (((๐ โ Fin โง ๐
โ Ring) โง (๐ โ ๐ต โง ๐ โ ๐ต)) โ (๐ โ ๐ต โง 1 โ (๐ DMat ๐
))) |
11 | | scmatscmide.b |
. . . . . 6
โข ๐ต = (Baseโ๐
) |
12 | | scmatscmide.m |
. . . . . 6
โข โ = (
ยท๐ โ๐ด) |
13 | 11, 3, 4, 12, 6 | dmatscmcl 21875 |
. . . . 5
โข (((๐ โ Fin โง ๐
โ Ring) โง (๐ โ ๐ต โง 1 โ (๐ DMat ๐
))) โ (๐ โ 1 ) โ (๐ DMat ๐
)) |
14 | 10, 13 | syldan 592 |
. . . 4
โข (((๐ โ Fin โง ๐
โ Ring) โง (๐ โ ๐ต โง ๐ โ ๐ต)) โ (๐ โ 1 ) โ (๐ DMat ๐
)) |
15 | | simprr 772 |
. . . . . 6
โข (((๐ โ Fin โง ๐
โ Ring) โง (๐ โ ๐ต โง ๐ โ ๐ต)) โ ๐ โ ๐ต) |
16 | 15, 9 | jca 513 |
. . . . 5
โข (((๐ โ Fin โง ๐
โ Ring) โง (๐ โ ๐ต โง ๐ โ ๐ต)) โ (๐ โ ๐ต โง 1 โ (๐ DMat ๐
))) |
17 | 11, 3, 4, 12, 6 | dmatscmcl 21875 |
. . . . 5
โข (((๐ โ Fin โง ๐
โ Ring) โง (๐ โ ๐ต โง 1 โ (๐ DMat ๐
))) โ (๐ โ 1 ) โ (๐ DMat ๐
)) |
18 | 16, 17 | syldan 592 |
. . . 4
โข (((๐ โ Fin โง ๐
โ Ring) โง (๐ โ ๐ต โง ๐ โ ๐ต)) โ (๐ โ 1 ) โ (๐ DMat ๐
)) |
19 | 14, 18 | jca 513 |
. . 3
โข (((๐ โ Fin โง ๐
โ Ring) โง (๐ โ ๐ต โง ๐ โ ๐ต)) โ ((๐ โ 1 ) โ (๐ DMat ๐
) โง (๐ โ 1 ) โ (๐ DMat ๐
))) |
20 | | scmatscmiddistr.m |
. . . . 5
โข ร =
(.rโ๐ด) |
21 | 20 | oveqi 7374 |
. . . 4
โข ((๐ โ 1 ) ร (๐ โ 1 )) = ((๐ โ 1
)(.rโ๐ด)(๐ โ 1 )) |
22 | 3, 4, 5, 6 | dmatmul 21869 |
. . . 4
โข (((๐ โ Fin โง ๐
โ Ring) โง ((๐ โ 1 ) โ (๐ DMat ๐
) โง (๐ โ 1 ) โ (๐ DMat ๐
))) โ ((๐ โ 1
)(.rโ๐ด)(๐ โ 1 )) = (๐ โ ๐, ๐ โ ๐ โฆ if(๐ = ๐, ((๐(๐ โ 1 )๐)(.rโ๐
)(๐(๐ โ 1 )๐)), 0 ))) |
23 | 21, 22 | eqtrid 2785 |
. . 3
โข (((๐ โ Fin โง ๐
โ Ring) โง ((๐ โ 1 ) โ (๐ DMat ๐
) โง (๐ โ 1 ) โ (๐ DMat ๐
))) โ ((๐ โ 1 ) ร (๐ โ 1 )) = (๐ โ ๐, ๐ โ ๐ โฆ if(๐ = ๐, ((๐(๐ โ 1 )๐)(.rโ๐
)(๐(๐ โ 1 )๐)), 0 ))) |
24 | 19, 23 | syldan 592 |
. 2
โข (((๐ โ Fin โง ๐
โ Ring) โง (๐ โ ๐ต โง ๐ โ ๐ต)) โ ((๐ โ 1 ) ร (๐ โ 1 )) = (๐ โ ๐, ๐ โ ๐ โฆ if(๐ = ๐, ((๐(๐ โ 1 )๐)(.rโ๐
)(๐(๐ โ 1 )๐)), 0 ))) |
25 | | simpll 766 |
. . . . . . . . 9
โข (((๐ โ Fin โง ๐
โ Ring) โง (๐ โ ๐ต โง ๐ โ ๐ต)) โ ๐ โ Fin) |
26 | | simplr 768 |
. . . . . . . . 9
โข (((๐ โ Fin โง ๐
โ Ring) โง (๐ โ ๐ต โง ๐ โ ๐ต)) โ ๐
โ Ring) |
27 | 25, 26, 1 | 3jca 1129 |
. . . . . . . 8
โข (((๐ โ Fin โง ๐
โ Ring) โง (๐ โ ๐ต โง ๐ โ ๐ต)) โ (๐ โ Fin โง ๐
โ Ring โง ๐ โ ๐ต)) |
28 | 27 | 3ad2ant1 1134 |
. . . . . . 7
โข ((((๐ โ Fin โง ๐
โ Ring) โง (๐ โ ๐ต โง ๐ โ ๐ต)) โง ๐ โ ๐ โง ๐ โ ๐) โ (๐ โ Fin โง ๐
โ Ring โง ๐ โ ๐ต)) |
29 | | 3simpc 1151 |
. . . . . . 7
โข ((((๐ โ Fin โง ๐
โ Ring) โง (๐ โ ๐ต โง ๐ โ ๐ต)) โง ๐ โ ๐ โง ๐ โ ๐) โ (๐ โ ๐ โง ๐ โ ๐)) |
30 | 3, 11, 5, 2, 12 | scmatscmide 21879 |
. . . . . . 7
โข (((๐ โ Fin โง ๐
โ Ring โง ๐ โ ๐ต) โง (๐ โ ๐ โง ๐ โ ๐)) โ (๐(๐ โ 1 )๐) = if(๐ = ๐, ๐, 0 )) |
31 | 28, 29, 30 | syl2anc 585 |
. . . . . 6
โข ((((๐ โ Fin โง ๐
โ Ring) โง (๐ โ ๐ต โง ๐ โ ๐ต)) โง ๐ โ ๐ โง ๐ โ ๐) โ (๐(๐ โ 1 )๐) = if(๐ = ๐, ๐, 0 )) |
32 | 25, 26, 15 | 3jca 1129 |
. . . . . . . 8
โข (((๐ โ Fin โง ๐
โ Ring) โง (๐ โ ๐ต โง ๐ โ ๐ต)) โ (๐ โ Fin โง ๐
โ Ring โง ๐ โ ๐ต)) |
33 | 32 | 3ad2ant1 1134 |
. . . . . . 7
โข ((((๐ โ Fin โง ๐
โ Ring) โง (๐ โ ๐ต โง ๐ โ ๐ต)) โง ๐ โ ๐ โง ๐ โ ๐) โ (๐ โ Fin โง ๐
โ Ring โง ๐ โ ๐ต)) |
34 | 3, 11, 5, 2, 12 | scmatscmide 21879 |
. . . . . . 7
โข (((๐ โ Fin โง ๐
โ Ring โง ๐ โ ๐ต) โง (๐ โ ๐ โง ๐ โ ๐)) โ (๐(๐ โ 1 )๐) = if(๐ = ๐, ๐, 0 )) |
35 | 33, 29, 34 | syl2anc 585 |
. . . . . 6
โข ((((๐ โ Fin โง ๐
โ Ring) โง (๐ โ ๐ต โง ๐ โ ๐ต)) โง ๐ โ ๐ โง ๐ โ ๐) โ (๐(๐ โ 1 )๐) = if(๐ = ๐, ๐, 0 )) |
36 | 31, 35 | oveq12d 7379 |
. . . . 5
โข ((((๐ โ Fin โง ๐
โ Ring) โง (๐ โ ๐ต โง ๐ โ ๐ต)) โง ๐ โ ๐ โง ๐ โ ๐) โ ((๐(๐ โ 1 )๐)(.rโ๐
)(๐(๐ โ 1 )๐)) = (if(๐ = ๐, ๐, 0
)(.rโ๐
)if(๐ = ๐, ๐, 0 ))) |
37 | 36 | ifeq1d 4509 |
. . . 4
โข ((((๐ โ Fin โง ๐
โ Ring) โง (๐ โ ๐ต โง ๐ โ ๐ต)) โง ๐ โ ๐ โง ๐ โ ๐) โ if(๐ = ๐, ((๐(๐ โ 1 )๐)(.rโ๐
)(๐(๐ โ 1 )๐)), 0 ) = if(๐ = ๐, (if(๐ = ๐, ๐, 0
)(.rโ๐
)if(๐ = ๐, ๐, 0 )), 0 )) |
38 | 37 | mpoeq3dva 7438 |
. . 3
โข (((๐ โ Fin โง ๐
โ Ring) โง (๐ โ ๐ต โง ๐ โ ๐ต)) โ (๐ โ ๐, ๐ โ ๐ โฆ if(๐ = ๐, ((๐(๐ โ 1 )๐)(.rโ๐
)(๐(๐ โ 1 )๐)), 0 )) = (๐ โ ๐, ๐ โ ๐ โฆ if(๐ = ๐, (if(๐ = ๐, ๐, 0
)(.rโ๐
)if(๐ = ๐, ๐, 0 )), 0 ))) |
39 | | iftrue 4496 |
. . . . . . . 8
โข (๐ = ๐ โ if(๐ = ๐, ๐, 0 ) = ๐) |
40 | | iftrue 4496 |
. . . . . . . 8
โข (๐ = ๐ โ if(๐ = ๐, ๐, 0 ) = ๐) |
41 | 39, 40 | oveq12d 7379 |
. . . . . . 7
โข (๐ = ๐ โ (if(๐ = ๐, ๐, 0
)(.rโ๐
)if(๐ = ๐, ๐, 0 )) = (๐(.rโ๐
)๐)) |
42 | 41 | adantl 483 |
. . . . . 6
โข
(((((๐ โ Fin
โง ๐
โ Ring) โง
(๐ โ ๐ต โง ๐ โ ๐ต)) โง ๐ โ ๐ โง ๐ โ ๐) โง ๐ = ๐) โ (if(๐ = ๐, ๐, 0
)(.rโ๐
)if(๐ = ๐, ๐, 0 )) = (๐(.rโ๐
)๐)) |
43 | 42 | ifeq1da 4521 |
. . . . 5
โข ((((๐ โ Fin โง ๐
โ Ring) โง (๐ โ ๐ต โง ๐ โ ๐ต)) โง ๐ โ ๐ โง ๐ โ ๐) โ if(๐ = ๐, (if(๐ = ๐, ๐, 0
)(.rโ๐
)if(๐ = ๐, ๐, 0 )), 0 ) = if(๐ = ๐, (๐(.rโ๐
)๐), 0 )) |
44 | 43 | mpoeq3dva 7438 |
. . . 4
โข (((๐ โ Fin โง ๐
โ Ring) โง (๐ โ ๐ต โง ๐ โ ๐ต)) โ (๐ โ ๐, ๐ โ ๐ โฆ if(๐ = ๐, (if(๐ = ๐, ๐, 0
)(.rโ๐
)if(๐ = ๐, ๐, 0 )), 0 )) = (๐ โ ๐, ๐ โ ๐ โฆ if(๐ = ๐, (๐(.rโ๐
)๐), 0 ))) |
45 | | eqidd 2734 |
. . . . . . . 8
โข ((((๐ โ Fin โง ๐
โ Ring) โง (๐ โ ๐ต โง ๐ โ ๐ต)) โง (๐ฅ โ ๐ โง ๐ฆ โ ๐)) โ (๐ โ ๐, ๐ โ ๐ โฆ if(๐ = ๐, (๐(.rโ๐
)๐), 0 )) = (๐ โ ๐, ๐ โ ๐ โฆ if(๐ = ๐, (๐(.rโ๐
)๐), 0 ))) |
46 | | eqeq12 2750 |
. . . . . . . . . 10
โข ((๐ = ๐ฅ โง ๐ = ๐ฆ) โ (๐ = ๐ โ ๐ฅ = ๐ฆ)) |
47 | | scmatscmiddistr.t |
. . . . . . . . . . . . 13
โข ยท =
(.rโ๐
) |
48 | 47 | eqcomi 2742 |
. . . . . . . . . . . 12
โข
(.rโ๐
) = ยท |
49 | 48 | oveqi 7374 |
. . . . . . . . . . 11
โข (๐(.rโ๐
)๐) = (๐ ยท ๐) |
50 | 49 | a1i 11 |
. . . . . . . . . 10
โข ((๐ = ๐ฅ โง ๐ = ๐ฆ) โ (๐(.rโ๐
)๐) = (๐ ยท ๐)) |
51 | 46, 50 | ifbieq1d 4514 |
. . . . . . . . 9
โข ((๐ = ๐ฅ โง ๐ = ๐ฆ) โ if(๐ = ๐, (๐(.rโ๐
)๐), 0 ) = if(๐ฅ = ๐ฆ, (๐ ยท ๐), 0 )) |
52 | 51 | adantl 483 |
. . . . . . . 8
โข
(((((๐ โ Fin
โง ๐
โ Ring) โง
(๐ โ ๐ต โง ๐ โ ๐ต)) โง (๐ฅ โ ๐ โง ๐ฆ โ ๐)) โง (๐ = ๐ฅ โง ๐ = ๐ฆ)) โ if(๐ = ๐, (๐(.rโ๐
)๐), 0 ) = if(๐ฅ = ๐ฆ, (๐ ยท ๐), 0 )) |
53 | | simprl 770 |
. . . . . . . 8
โข ((((๐ โ Fin โง ๐
โ Ring) โง (๐ โ ๐ต โง ๐ โ ๐ต)) โง (๐ฅ โ ๐ โง ๐ฆ โ ๐)) โ ๐ฅ โ ๐) |
54 | | simprr 772 |
. . . . . . . 8
โข ((((๐ โ Fin โง ๐
โ Ring) โง (๐ โ ๐ต โง ๐ โ ๐ต)) โง (๐ฅ โ ๐ โง ๐ฆ โ ๐)) โ ๐ฆ โ ๐) |
55 | | ovex 7394 |
. . . . . . . . . 10
โข (๐ ยท ๐) โ V |
56 | 5 | fvexi 6860 |
. . . . . . . . . 10
โข 0 โ
V |
57 | 55, 56 | ifex 4540 |
. . . . . . . . 9
โข if(๐ฅ = ๐ฆ, (๐ ยท ๐), 0 ) โ
V |
58 | 57 | a1i 11 |
. . . . . . . 8
โข ((((๐ โ Fin โง ๐
โ Ring) โง (๐ โ ๐ต โง ๐ โ ๐ต)) โง (๐ฅ โ ๐ โง ๐ฆ โ ๐)) โ if(๐ฅ = ๐ฆ, (๐ ยท ๐), 0 ) โ
V) |
59 | 45, 52, 53, 54, 58 | ovmpod 7511 |
. . . . . . 7
โข ((((๐ โ Fin โง ๐
โ Ring) โง (๐ โ ๐ต โง ๐ โ ๐ต)) โง (๐ฅ โ ๐ โง ๐ฆ โ ๐)) โ (๐ฅ(๐ โ ๐, ๐ โ ๐ โฆ if(๐ = ๐, (๐(.rโ๐
)๐), 0 ))๐ฆ) = if(๐ฅ = ๐ฆ, (๐ ยท ๐), 0 )) |
60 | 26, 1, 15 | 3jca 1129 |
. . . . . . . . . 10
โข (((๐ โ Fin โง ๐
โ Ring) โง (๐ โ ๐ต โง ๐ โ ๐ต)) โ (๐
โ Ring โง ๐ โ ๐ต โง ๐ โ ๐ต)) |
61 | 11, 47 | ringcl 19989 |
. . . . . . . . . 10
โข ((๐
โ Ring โง ๐ โ ๐ต โง ๐ โ ๐ต) โ (๐ ยท ๐) โ ๐ต) |
62 | 60, 61 | syl 17 |
. . . . . . . . 9
โข (((๐ โ Fin โง ๐
โ Ring) โง (๐ โ ๐ต โง ๐ โ ๐ต)) โ (๐ ยท ๐) โ ๐ต) |
63 | 25, 26, 62 | 3jca 1129 |
. . . . . . . 8
โข (((๐ โ Fin โง ๐
โ Ring) โง (๐ โ ๐ต โง ๐ โ ๐ต)) โ (๐ โ Fin โง ๐
โ Ring โง (๐ ยท ๐) โ ๐ต)) |
64 | 3, 11, 5, 2, 12 | scmatscmide 21879 |
. . . . . . . 8
โข (((๐ โ Fin โง ๐
โ Ring โง (๐ ยท ๐) โ ๐ต) โง (๐ฅ โ ๐ โง ๐ฆ โ ๐)) โ (๐ฅ((๐ ยท ๐) โ 1 )๐ฆ) = if(๐ฅ = ๐ฆ, (๐ ยท ๐), 0 )) |
65 | 63, 64 | sylan 581 |
. . . . . . 7
โข ((((๐ โ Fin โง ๐
โ Ring) โง (๐ โ ๐ต โง ๐ โ ๐ต)) โง (๐ฅ โ ๐ โง ๐ฆ โ ๐)) โ (๐ฅ((๐ ยท ๐) โ 1 )๐ฆ) = if(๐ฅ = ๐ฆ, (๐ ยท ๐), 0 )) |
66 | 59, 65 | eqtr4d 2776 |
. . . . . 6
โข ((((๐ โ Fin โง ๐
โ Ring) โง (๐ โ ๐ต โง ๐ โ ๐ต)) โง (๐ฅ โ ๐ โง ๐ฆ โ ๐)) โ (๐ฅ(๐ โ ๐, ๐ โ ๐ โฆ if(๐ = ๐, (๐(.rโ๐
)๐), 0 ))๐ฆ) = (๐ฅ((๐ ยท ๐) โ 1 )๐ฆ)) |
67 | 66 | ralrimivva 3194 |
. . . . 5
โข (((๐ โ Fin โง ๐
โ Ring) โง (๐ โ ๐ต โง ๐ โ ๐ต)) โ โ๐ฅ โ ๐ โ๐ฆ โ ๐ (๐ฅ(๐ โ ๐, ๐ โ ๐ โฆ if(๐ = ๐, (๐(.rโ๐
)๐), 0 ))๐ฆ) = (๐ฅ((๐ ยท ๐) โ 1 )๐ฆ)) |
68 | | eqid 2733 |
. . . . . . . . . . 11
โข
(.rโ๐
) = (.rโ๐
) |
69 | 11, 68 | ringcl 19989 |
. . . . . . . . . 10
โข ((๐
โ Ring โง ๐ โ ๐ต โง ๐ โ ๐ต) โ (๐(.rโ๐
)๐) โ ๐ต) |
70 | 60, 69 | syl 17 |
. . . . . . . . 9
โข (((๐ โ Fin โง ๐
โ Ring) โง (๐ โ ๐ต โง ๐ โ ๐ต)) โ (๐(.rโ๐
)๐) โ ๐ต) |
71 | 11, 5 | ring0cl 19998 |
. . . . . . . . . . 11
โข (๐
โ Ring โ 0 โ ๐ต) |
72 | 71 | adantl 483 |
. . . . . . . . . 10
โข ((๐ โ Fin โง ๐
โ Ring) โ 0 โ ๐ต) |
73 | 72 | adantr 482 |
. . . . . . . . 9
โข (((๐ โ Fin โง ๐
โ Ring) โง (๐ โ ๐ต โง ๐ โ ๐ต)) โ 0 โ ๐ต) |
74 | 70, 73 | ifcld 4536 |
. . . . . . . 8
โข (((๐ โ Fin โง ๐
โ Ring) โง (๐ โ ๐ต โง ๐ โ ๐ต)) โ if(๐ = ๐, (๐(.rโ๐
)๐), 0 ) โ ๐ต) |
75 | 74 | 3ad2ant1 1134 |
. . . . . . 7
โข ((((๐ โ Fin โง ๐
โ Ring) โง (๐ โ ๐ต โง ๐ โ ๐ต)) โง ๐ โ ๐ โง ๐ โ ๐) โ if(๐ = ๐, (๐(.rโ๐
)๐), 0 ) โ ๐ต) |
76 | 3, 11, 4, 25, 26, 75 | matbas2d 21795 |
. . . . . 6
โข (((๐ โ Fin โง ๐
โ Ring) โง (๐ โ ๐ต โง ๐ โ ๐ต)) โ (๐ โ ๐, ๐ โ ๐ โฆ if(๐ = ๐, (๐(.rโ๐
)๐), 0 )) โ
(Baseโ๐ด)) |
77 | 3 | matring 21815 |
. . . . . . . . . 10
โข ((๐ โ Fin โง ๐
โ Ring) โ ๐ด โ Ring) |
78 | 4, 2 | ringidcl 19997 |
. . . . . . . . . 10
โข (๐ด โ Ring โ 1 โ
(Baseโ๐ด)) |
79 | 77, 78 | syl 17 |
. . . . . . . . 9
โข ((๐ โ Fin โง ๐
โ Ring) โ 1 โ
(Baseโ๐ด)) |
80 | 79 | adantr 482 |
. . . . . . . 8
โข (((๐ โ Fin โง ๐
โ Ring) โง (๐ โ ๐ต โง ๐ โ ๐ต)) โ 1 โ (Baseโ๐ด)) |
81 | 62, 80 | jca 513 |
. . . . . . 7
โข (((๐ โ Fin โง ๐
โ Ring) โง (๐ โ ๐ต โง ๐ โ ๐ต)) โ ((๐ ยท ๐) โ ๐ต โง 1 โ (Baseโ๐ด))) |
82 | 11, 3, 4, 12 | matvscl 21803 |
. . . . . . 7
โข (((๐ โ Fin โง ๐
โ Ring) โง ((๐ ยท ๐) โ ๐ต โง 1 โ (Baseโ๐ด))) โ ((๐ ยท ๐) โ 1 ) โ (Baseโ๐ด)) |
83 | 81, 82 | syldan 592 |
. . . . . 6
โข (((๐ โ Fin โง ๐
โ Ring) โง (๐ โ ๐ต โง ๐ โ ๐ต)) โ ((๐ ยท ๐) โ 1 ) โ (Baseโ๐ด)) |
84 | 3, 4 | eqmat 21796 |
. . . . . 6
โข (((๐ โ ๐, ๐ โ ๐ โฆ if(๐ = ๐, (๐(.rโ๐
)๐), 0 )) โ
(Baseโ๐ด) โง
((๐ ยท ๐) โ 1 ) โ (Baseโ๐ด)) โ ((๐ โ ๐, ๐ โ ๐ โฆ if(๐ = ๐, (๐(.rโ๐
)๐), 0 )) = ((๐ ยท ๐) โ 1 ) โ โ๐ฅ โ ๐ โ๐ฆ โ ๐ (๐ฅ(๐ โ ๐, ๐ โ ๐ โฆ if(๐ = ๐, (๐(.rโ๐
)๐), 0 ))๐ฆ) = (๐ฅ((๐ ยท ๐) โ 1 )๐ฆ))) |
85 | 76, 83, 84 | syl2anc 585 |
. . . . 5
โข (((๐ โ Fin โง ๐
โ Ring) โง (๐ โ ๐ต โง ๐ โ ๐ต)) โ ((๐ โ ๐, ๐ โ ๐ โฆ if(๐ = ๐, (๐(.rโ๐
)๐), 0 )) = ((๐ ยท ๐) โ 1 ) โ โ๐ฅ โ ๐ โ๐ฆ โ ๐ (๐ฅ(๐ โ ๐, ๐ โ ๐ โฆ if(๐ = ๐, (๐(.rโ๐
)๐), 0 ))๐ฆ) = (๐ฅ((๐ ยท ๐) โ 1 )๐ฆ))) |
86 | 67, 85 | mpbird 257 |
. . . 4
โข (((๐ โ Fin โง ๐
โ Ring) โง (๐ โ ๐ต โง ๐ โ ๐ต)) โ (๐ โ ๐, ๐ โ ๐ โฆ if(๐ = ๐, (๐(.rโ๐
)๐), 0 )) = ((๐ ยท ๐) โ 1 )) |
87 | 44, 86 | eqtrd 2773 |
. . 3
โข (((๐ โ Fin โง ๐
โ Ring) โง (๐ โ ๐ต โง ๐ โ ๐ต)) โ (๐ โ ๐, ๐ โ ๐ โฆ if(๐ = ๐, (if(๐ = ๐, ๐, 0
)(.rโ๐
)if(๐ = ๐, ๐, 0 )), 0 )) = ((๐ ยท ๐) โ 1 )) |
88 | 38, 87 | eqtrd 2773 |
. 2
โข (((๐ โ Fin โง ๐
โ Ring) โง (๐ โ ๐ต โง ๐ โ ๐ต)) โ (๐ โ ๐, ๐ โ ๐ โฆ if(๐ = ๐, ((๐(๐ โ 1 )๐)(.rโ๐
)(๐(๐ โ 1 )๐)), 0 )) = ((๐ ยท ๐) โ 1 )) |
89 | 24, 88 | eqtrd 2773 |
1
โข (((๐ โ Fin โง ๐
โ Ring) โง (๐ โ ๐ต โง ๐ โ ๐ต)) โ ((๐ โ 1 ) ร (๐ โ 1 )) = ((๐ ยท ๐) โ 1 )) |