Step | Hyp | Ref
| Expression |
1 | | scmatrhmval.k |
. . . 4
โข ๐พ = (Baseโ๐
) |
2 | | scmatrhmval.a |
. . . 4
โข ๐ด = (๐ Mat ๐
) |
3 | | scmatrhmval.o |
. . . 4
โข 1 =
(1rโ๐ด) |
4 | | scmatrhmval.t |
. . . 4
โข โ = (
ยท๐ โ๐ด) |
5 | | scmatrhmval.f |
. . . 4
โข ๐น = (๐ฅ โ ๐พ โฆ (๐ฅ โ 1 )) |
6 | | scmatrhmval.c |
. . . 4
โข ๐ถ = (๐ ScMat ๐
) |
7 | 1, 2, 3, 4, 5, 6 | scmatf 22022 |
. . 3
โข ((๐ โ Fin โง ๐
โ Ring) โ ๐น:๐พโถ๐ถ) |
8 | 7 | 3adant2 1131 |
. 2
โข ((๐ โ Fin โง ๐ โ โ
โง ๐
โ Ring) โ ๐น:๐พโถ๐ถ) |
9 | | simpr 485 |
. . . . . . 7
โข ((๐ โ Fin โง ๐
โ Ring) โ ๐
โ Ring) |
10 | | simpl 483 |
. . . . . . 7
โข ((๐ฆ โ ๐พ โง ๐ง โ ๐พ) โ ๐ฆ โ ๐พ) |
11 | 1, 2, 3, 4, 5 | scmatrhmval 22020 |
. . . . . . 7
โข ((๐
โ Ring โง ๐ฆ โ ๐พ) โ (๐นโ๐ฆ) = (๐ฆ โ 1 )) |
12 | 9, 10, 11 | syl2an 596 |
. . . . . 6
โข (((๐ โ Fin โง ๐
โ Ring) โง (๐ฆ โ ๐พ โง ๐ง โ ๐พ)) โ (๐นโ๐ฆ) = (๐ฆ โ 1 )) |
13 | | simpr 485 |
. . . . . . 7
โข ((๐ฆ โ ๐พ โง ๐ง โ ๐พ) โ ๐ง โ ๐พ) |
14 | 1, 2, 3, 4, 5 | scmatrhmval 22020 |
. . . . . . 7
โข ((๐
โ Ring โง ๐ง โ ๐พ) โ (๐นโ๐ง) = (๐ง โ 1 )) |
15 | 9, 13, 14 | syl2an 596 |
. . . . . 6
โข (((๐ โ Fin โง ๐
โ Ring) โง (๐ฆ โ ๐พ โง ๐ง โ ๐พ)) โ (๐นโ๐ง) = (๐ง โ 1 )) |
16 | 12, 15 | eqeq12d 2748 |
. . . . 5
โข (((๐ โ Fin โง ๐
โ Ring) โง (๐ฆ โ ๐พ โง ๐ง โ ๐พ)) โ ((๐นโ๐ฆ) = (๐นโ๐ง) โ (๐ฆ โ 1 ) = (๐ง โ 1 ))) |
17 | 16 | 3adantl2 1167 |
. . . 4
โข (((๐ โ Fin โง ๐ โ โ
โง ๐
โ Ring) โง (๐ฆ โ ๐พ โง ๐ง โ ๐พ)) โ ((๐นโ๐ฆ) = (๐นโ๐ง) โ (๐ฆ โ 1 ) = (๐ง โ 1 ))) |
18 | 2 | matring 21936 |
. . . . . . . . . . 11
โข ((๐ โ Fin โง ๐
โ Ring) โ ๐ด โ Ring) |
19 | | eqid 2732 |
. . . . . . . . . . . 12
โข
(Baseโ๐ด) =
(Baseโ๐ด) |
20 | 19, 3 | ringidcl 20076 |
. . . . . . . . . . 11
โข (๐ด โ Ring โ 1 โ
(Baseโ๐ด)) |
21 | 18, 20 | syl 17 |
. . . . . . . . . 10
โข ((๐ โ Fin โง ๐
โ Ring) โ 1 โ
(Baseโ๐ด)) |
22 | 21, 10 | anim12ci 614 |
. . . . . . . . 9
โข (((๐ โ Fin โง ๐
โ Ring) โง (๐ฆ โ ๐พ โง ๐ง โ ๐พ)) โ (๐ฆ โ ๐พ โง 1 โ (Baseโ๐ด))) |
23 | 1, 2, 19, 4 | matvscl 21924 |
. . . . . . . . 9
โข (((๐ โ Fin โง ๐
โ Ring) โง (๐ฆ โ ๐พ โง 1 โ (Baseโ๐ด))) โ (๐ฆ โ 1 ) โ (Baseโ๐ด)) |
24 | 22, 23 | syldan 591 |
. . . . . . . 8
โข (((๐ โ Fin โง ๐
โ Ring) โง (๐ฆ โ ๐พ โง ๐ง โ ๐พ)) โ (๐ฆ โ 1 ) โ (Baseโ๐ด)) |
25 | 21, 13 | anim12ci 614 |
. . . . . . . . 9
โข (((๐ โ Fin โง ๐
โ Ring) โง (๐ฆ โ ๐พ โง ๐ง โ ๐พ)) โ (๐ง โ ๐พ โง 1 โ (Baseโ๐ด))) |
26 | 1, 2, 19, 4 | matvscl 21924 |
. . . . . . . . 9
โข (((๐ โ Fin โง ๐
โ Ring) โง (๐ง โ ๐พ โง 1 โ (Baseโ๐ด))) โ (๐ง โ 1 ) โ (Baseโ๐ด)) |
27 | 25, 26 | syldan 591 |
. . . . . . . 8
โข (((๐ โ Fin โง ๐
โ Ring) โง (๐ฆ โ ๐พ โง ๐ง โ ๐พ)) โ (๐ง โ 1 ) โ (Baseโ๐ด)) |
28 | 24, 27 | jca 512 |
. . . . . . 7
โข (((๐ โ Fin โง ๐
โ Ring) โง (๐ฆ โ ๐พ โง ๐ง โ ๐พ)) โ ((๐ฆ โ 1 ) โ (Baseโ๐ด) โง (๐ง โ 1 ) โ (Baseโ๐ด))) |
29 | 28 | 3adantl2 1167 |
. . . . . 6
โข (((๐ โ Fin โง ๐ โ โ
โง ๐
โ Ring) โง (๐ฆ โ ๐พ โง ๐ง โ ๐พ)) โ ((๐ฆ โ 1 ) โ (Baseโ๐ด) โง (๐ง โ 1 ) โ (Baseโ๐ด))) |
30 | 2, 19 | eqmat 21917 |
. . . . . 6
โข (((๐ฆ โ 1 ) โ (Baseโ๐ด) โง (๐ง โ 1 ) โ (Baseโ๐ด)) โ ((๐ฆ โ 1 ) = (๐ง โ 1 ) โ โ๐ โ ๐ โ๐ โ ๐ (๐(๐ฆ โ 1 )๐) = (๐(๐ง โ 1 )๐))) |
31 | 29, 30 | syl 17 |
. . . . 5
โข (((๐ โ Fin โง ๐ โ โ
โง ๐
โ Ring) โง (๐ฆ โ ๐พ โง ๐ง โ ๐พ)) โ ((๐ฆ โ 1 ) = (๐ง โ 1 ) โ โ๐ โ ๐ โ๐ โ ๐ (๐(๐ฆ โ 1 )๐) = (๐(๐ง โ 1 )๐))) |
32 | | difsnid 4812 |
. . . . . . . . . . . 12
โข (๐ โ ๐ โ ((๐ โ {๐}) โช {๐}) = ๐) |
33 | 32 | eqcomd 2738 |
. . . . . . . . . . 11
โข (๐ โ ๐ โ ๐ = ((๐ โ {๐}) โช {๐})) |
34 | 33 | adantl 482 |
. . . . . . . . . 10
โข ((((๐ โ Fin โง ๐
โ Ring) โง (๐ฆ โ ๐พ โง ๐ง โ ๐พ)) โง ๐ โ ๐) โ ๐ = ((๐ โ {๐}) โช {๐})) |
35 | 34 | raleqdv 3325 |
. . . . . . . . 9
โข ((((๐ โ Fin โง ๐
โ Ring) โง (๐ฆ โ ๐พ โง ๐ง โ ๐พ)) โง ๐ โ ๐) โ (โ๐ โ ๐ (๐(๐ฆ โ 1 )๐) = (๐(๐ง โ 1 )๐) โ โ๐ โ ((๐ โ {๐}) โช {๐})(๐(๐ฆ โ 1 )๐) = (๐(๐ง โ 1 )๐))) |
36 | | oveq2 7413 |
. . . . . . . . . . . 12
โข (๐ = ๐ โ (๐(๐ฆ โ 1 )๐) = (๐(๐ฆ โ 1 )๐)) |
37 | | oveq2 7413 |
. . . . . . . . . . . 12
โข (๐ = ๐ โ (๐(๐ง โ 1 )๐) = (๐(๐ง โ 1 )๐)) |
38 | 36, 37 | eqeq12d 2748 |
. . . . . . . . . . 11
โข (๐ = ๐ โ ((๐(๐ฆ โ 1 )๐) = (๐(๐ง โ 1 )๐) โ (๐(๐ฆ โ 1 )๐) = (๐(๐ง โ 1 )๐))) |
39 | 38 | ralunsn 4893 |
. . . . . . . . . 10
โข (๐ โ ๐ โ (โ๐ โ ((๐ โ {๐}) โช {๐})(๐(๐ฆ โ 1 )๐) = (๐(๐ง โ 1 )๐) โ (โ๐ โ (๐ โ {๐})(๐(๐ฆ โ 1 )๐) = (๐(๐ง โ 1 )๐) โง (๐(๐ฆ โ 1 )๐) = (๐(๐ง โ 1 )๐)))) |
40 | 39 | adantl 482 |
. . . . . . . . 9
โข ((((๐ โ Fin โง ๐
โ Ring) โง (๐ฆ โ ๐พ โง ๐ง โ ๐พ)) โง ๐ โ ๐) โ (โ๐ โ ((๐ โ {๐}) โช {๐})(๐(๐ฆ โ 1 )๐) = (๐(๐ง โ 1 )๐) โ (โ๐ โ (๐ โ {๐})(๐(๐ฆ โ 1 )๐) = (๐(๐ง โ 1 )๐) โง (๐(๐ฆ โ 1 )๐) = (๐(๐ง โ 1 )๐)))) |
41 | 10 | anim2i 617 |
. . . . . . . . . . . . . 14
โข (((๐ โ Fin โง ๐
โ Ring) โง (๐ฆ โ ๐พ โง ๐ง โ ๐พ)) โ ((๐ โ Fin โง ๐
โ Ring) โง ๐ฆ โ ๐พ)) |
42 | | df-3an 1089 |
. . . . . . . . . . . . . 14
โข ((๐ โ Fin โง ๐
โ Ring โง ๐ฆ โ ๐พ) โ ((๐ โ Fin โง ๐
โ Ring) โง ๐ฆ โ ๐พ)) |
43 | 41, 42 | sylibr 233 |
. . . . . . . . . . . . 13
โข (((๐ โ Fin โง ๐
โ Ring) โง (๐ฆ โ ๐พ โง ๐ง โ ๐พ)) โ (๐ โ Fin โง ๐
โ Ring โง ๐ฆ โ ๐พ)) |
44 | | id 22 |
. . . . . . . . . . . . . 14
โข (๐ โ ๐ โ ๐ โ ๐) |
45 | 44, 44 | jca 512 |
. . . . . . . . . . . . 13
โข (๐ โ ๐ โ (๐ โ ๐ โง ๐ โ ๐)) |
46 | | eqid 2732 |
. . . . . . . . . . . . . 14
โข
(0gโ๐
) = (0gโ๐
) |
47 | 2, 1, 46, 3, 4 | scmatscmide 22000 |
. . . . . . . . . . . . 13
โข (((๐ โ Fin โง ๐
โ Ring โง ๐ฆ โ ๐พ) โง (๐ โ ๐ โง ๐ โ ๐)) โ (๐(๐ฆ โ 1 )๐) = if(๐ = ๐, ๐ฆ, (0gโ๐
))) |
48 | 43, 45, 47 | syl2an 596 |
. . . . . . . . . . . 12
โข ((((๐ โ Fin โง ๐
โ Ring) โง (๐ฆ โ ๐พ โง ๐ง โ ๐พ)) โง ๐ โ ๐) โ (๐(๐ฆ โ 1 )๐) = if(๐ = ๐, ๐ฆ, (0gโ๐
))) |
49 | | eqid 2732 |
. . . . . . . . . . . . 13
โข ๐ = ๐ |
50 | 49 | iftruei 4534 |
. . . . . . . . . . . 12
โข if(๐ = ๐, ๐ฆ, (0gโ๐
)) = ๐ฆ |
51 | 48, 50 | eqtrdi 2788 |
. . . . . . . . . . 11
โข ((((๐ โ Fin โง ๐
โ Ring) โง (๐ฆ โ ๐พ โง ๐ง โ ๐พ)) โง ๐ โ ๐) โ (๐(๐ฆ โ 1 )๐) = ๐ฆ) |
52 | 13 | anim2i 617 |
. . . . . . . . . . . . . 14
โข (((๐ โ Fin โง ๐
โ Ring) โง (๐ฆ โ ๐พ โง ๐ง โ ๐พ)) โ ((๐ โ Fin โง ๐
โ Ring) โง ๐ง โ ๐พ)) |
53 | | df-3an 1089 |
. . . . . . . . . . . . . 14
โข ((๐ โ Fin โง ๐
โ Ring โง ๐ง โ ๐พ) โ ((๐ โ Fin โง ๐
โ Ring) โง ๐ง โ ๐พ)) |
54 | 52, 53 | sylibr 233 |
. . . . . . . . . . . . 13
โข (((๐ โ Fin โง ๐
โ Ring) โง (๐ฆ โ ๐พ โง ๐ง โ ๐พ)) โ (๐ โ Fin โง ๐
โ Ring โง ๐ง โ ๐พ)) |
55 | 2, 1, 46, 3, 4 | scmatscmide 22000 |
. . . . . . . . . . . . 13
โข (((๐ โ Fin โง ๐
โ Ring โง ๐ง โ ๐พ) โง (๐ โ ๐ โง ๐ โ ๐)) โ (๐(๐ง โ 1 )๐) = if(๐ = ๐, ๐ง, (0gโ๐
))) |
56 | 54, 45, 55 | syl2an 596 |
. . . . . . . . . . . 12
โข ((((๐ โ Fin โง ๐
โ Ring) โง (๐ฆ โ ๐พ โง ๐ง โ ๐พ)) โง ๐ โ ๐) โ (๐(๐ง โ 1 )๐) = if(๐ = ๐, ๐ง, (0gโ๐
))) |
57 | 49 | iftruei 4534 |
. . . . . . . . . . . 12
โข if(๐ = ๐, ๐ง, (0gโ๐
)) = ๐ง |
58 | 56, 57 | eqtrdi 2788 |
. . . . . . . . . . 11
โข ((((๐ โ Fin โง ๐
โ Ring) โง (๐ฆ โ ๐พ โง ๐ง โ ๐พ)) โง ๐ โ ๐) โ (๐(๐ง โ 1 )๐) = ๐ง) |
59 | 51, 58 | eqeq12d 2748 |
. . . . . . . . . 10
โข ((((๐ โ Fin โง ๐
โ Ring) โง (๐ฆ โ ๐พ โง ๐ง โ ๐พ)) โง ๐ โ ๐) โ ((๐(๐ฆ โ 1 )๐) = (๐(๐ง โ 1 )๐) โ ๐ฆ = ๐ง)) |
60 | 59 | anbi2d 629 |
. . . . . . . . 9
โข ((((๐ โ Fin โง ๐
โ Ring) โง (๐ฆ โ ๐พ โง ๐ง โ ๐พ)) โง ๐ โ ๐) โ ((โ๐ โ (๐ โ {๐})(๐(๐ฆ โ 1 )๐) = (๐(๐ง โ 1 )๐) โง (๐(๐ฆ โ 1 )๐) = (๐(๐ง โ 1 )๐)) โ (โ๐ โ (๐ โ {๐})(๐(๐ฆ โ 1 )๐) = (๐(๐ง โ 1 )๐) โง ๐ฆ = ๐ง))) |
61 | 35, 40, 60 | 3bitrd 304 |
. . . . . . . 8
โข ((((๐ โ Fin โง ๐
โ Ring) โง (๐ฆ โ ๐พ โง ๐ง โ ๐พ)) โง ๐ โ ๐) โ (โ๐ โ ๐ (๐(๐ฆ โ 1 )๐) = (๐(๐ง โ 1 )๐) โ (โ๐ โ (๐ โ {๐})(๐(๐ฆ โ 1 )๐) = (๐(๐ง โ 1 )๐) โง ๐ฆ = ๐ง))) |
62 | 61 | ralbidva 3175 |
. . . . . . 7
โข (((๐ โ Fin โง ๐
โ Ring) โง (๐ฆ โ ๐พ โง ๐ง โ ๐พ)) โ (โ๐ โ ๐ โ๐ โ ๐ (๐(๐ฆ โ 1 )๐) = (๐(๐ง โ 1 )๐) โ โ๐ โ ๐ (โ๐ โ (๐ โ {๐})(๐(๐ฆ โ 1 )๐) = (๐(๐ง โ 1 )๐) โง ๐ฆ = ๐ง))) |
63 | 62 | 3adantl2 1167 |
. . . . . 6
โข (((๐ โ Fin โง ๐ โ โ
โง ๐
โ Ring) โง (๐ฆ โ ๐พ โง ๐ง โ ๐พ)) โ (โ๐ โ ๐ โ๐ โ ๐ (๐(๐ฆ โ 1 )๐) = (๐(๐ง โ 1 )๐) โ โ๐ โ ๐ (โ๐ โ (๐ โ {๐})(๐(๐ฆ โ 1 )๐) = (๐(๐ง โ 1 )๐) โง ๐ฆ = ๐ง))) |
64 | | r19.26 3111 |
. . . . . . . 8
โข
(โ๐ โ
๐ (โ๐ โ (๐ โ {๐})(๐(๐ฆ โ 1 )๐) = (๐(๐ง โ 1 )๐) โง ๐ฆ = ๐ง) โ (โ๐ โ ๐ โ๐ โ (๐ โ {๐})(๐(๐ฆ โ 1 )๐) = (๐(๐ง โ 1 )๐) โง โ๐ โ ๐ ๐ฆ = ๐ง)) |
65 | | rspn0 4351 |
. . . . . . . . . . 11
โข (๐ โ โ
โ
(โ๐ โ ๐ ๐ฆ = ๐ง โ ๐ฆ = ๐ง)) |
66 | 65 | 3ad2ant2 1134 |
. . . . . . . . . 10
โข ((๐ โ Fin โง ๐ โ โ
โง ๐
โ Ring) โ
(โ๐ โ ๐ ๐ฆ = ๐ง โ ๐ฆ = ๐ง)) |
67 | 66 | adantr 481 |
. . . . . . . . 9
โข (((๐ โ Fin โง ๐ โ โ
โง ๐
โ Ring) โง (๐ฆ โ ๐พ โง ๐ง โ ๐พ)) โ (โ๐ โ ๐ ๐ฆ = ๐ง โ ๐ฆ = ๐ง)) |
68 | 67 | com12 32 |
. . . . . . . 8
โข
(โ๐ โ
๐ ๐ฆ = ๐ง โ (((๐ โ Fin โง ๐ โ โ
โง ๐
โ Ring) โง (๐ฆ โ ๐พ โง ๐ง โ ๐พ)) โ ๐ฆ = ๐ง)) |
69 | 64, 68 | simplbiim 505 |
. . . . . . 7
โข
(โ๐ โ
๐ (โ๐ โ (๐ โ {๐})(๐(๐ฆ โ 1 )๐) = (๐(๐ง โ 1 )๐) โง ๐ฆ = ๐ง) โ (((๐ โ Fin โง ๐ โ โ
โง ๐
โ Ring) โง (๐ฆ โ ๐พ โง ๐ง โ ๐พ)) โ ๐ฆ = ๐ง)) |
70 | 69 | com12 32 |
. . . . . 6
โข (((๐ โ Fin โง ๐ โ โ
โง ๐
โ Ring) โง (๐ฆ โ ๐พ โง ๐ง โ ๐พ)) โ (โ๐ โ ๐ (โ๐ โ (๐ โ {๐})(๐(๐ฆ โ 1 )๐) = (๐(๐ง โ 1 )๐) โง ๐ฆ = ๐ง) โ ๐ฆ = ๐ง)) |
71 | 63, 70 | sylbid 239 |
. . . . 5
โข (((๐ โ Fin โง ๐ โ โ
โง ๐
โ Ring) โง (๐ฆ โ ๐พ โง ๐ง โ ๐พ)) โ (โ๐ โ ๐ โ๐ โ ๐ (๐(๐ฆ โ 1 )๐) = (๐(๐ง โ 1 )๐) โ ๐ฆ = ๐ง)) |
72 | 31, 71 | sylbid 239 |
. . . 4
โข (((๐ โ Fin โง ๐ โ โ
โง ๐
โ Ring) โง (๐ฆ โ ๐พ โง ๐ง โ ๐พ)) โ ((๐ฆ โ 1 ) = (๐ง โ 1 ) โ ๐ฆ = ๐ง)) |
73 | 17, 72 | sylbid 239 |
. . 3
โข (((๐ โ Fin โง ๐ โ โ
โง ๐
โ Ring) โง (๐ฆ โ ๐พ โง ๐ง โ ๐พ)) โ ((๐นโ๐ฆ) = (๐นโ๐ง) โ ๐ฆ = ๐ง)) |
74 | 73 | ralrimivva 3200 |
. 2
โข ((๐ โ Fin โง ๐ โ โ
โง ๐
โ Ring) โ
โ๐ฆ โ ๐พ โ๐ง โ ๐พ ((๐นโ๐ฆ) = (๐นโ๐ง) โ ๐ฆ = ๐ง)) |
75 | | dff13 7250 |
. 2
โข (๐น:๐พโ1-1โ๐ถ โ (๐น:๐พโถ๐ถ โง โ๐ฆ โ ๐พ โ๐ง โ ๐พ ((๐นโ๐ฆ) = (๐นโ๐ง) โ ๐ฆ = ๐ง))) |
76 | 8, 74, 75 | sylanbrc 583 |
1
โข ((๐ โ Fin โง ๐ โ โ
โง ๐
โ Ring) โ ๐น:๐พโ1-1โ๐ถ) |