Step | Hyp | Ref
| Expression |
1 | | prjspnfv01.f |
. . . 4
โข ๐น = (๐ โ ๐ต โฆ if((๐โ0) = 0 , ๐, ((๐ผโ(๐โ0)) ยท ๐))) |
2 | | fveq1 6891 |
. . . . . 6
โข (๐ = ๐ โ (๐โ0) = (๐โ0)) |
3 | 2 | eqeq1d 2727 |
. . . . 5
โข (๐ = ๐ โ ((๐โ0) = 0 โ (๐โ0) = 0 )) |
4 | | id 22 |
. . . . 5
โข (๐ = ๐ โ ๐ = ๐) |
5 | 2 | fveq2d 6896 |
. . . . . 6
โข (๐ = ๐ โ (๐ผโ(๐โ0)) = (๐ผโ(๐โ0))) |
6 | 5, 4 | oveq12d 7434 |
. . . . 5
โข (๐ = ๐ โ ((๐ผโ(๐โ0)) ยท ๐) = ((๐ผโ(๐โ0)) ยท ๐)) |
7 | 3, 4, 6 | ifbieq12d 4552 |
. . . 4
โข (๐ = ๐ โ if((๐โ0) = 0 , ๐, ((๐ผโ(๐โ0)) ยท ๐)) = if((๐โ0) = 0 , ๐, ((๐ผโ(๐โ0)) ยท ๐))) |
8 | | prjspnfv01.x |
. . . 4
โข (๐ โ ๐ โ ๐ต) |
9 | | ovexd 7451 |
. . . . 5
โข (๐ โ ((๐ผโ(๐โ0)) ยท ๐) โ V) |
10 | 8, 9 | ifexd 4572 |
. . . 4
โข (๐ โ if((๐โ0) = 0 , ๐, ((๐ผโ(๐โ0)) ยท ๐)) โ V) |
11 | 1, 7, 8, 10 | fvmptd3 7023 |
. . 3
โข (๐ โ (๐นโ๐) = if((๐โ0) = 0 , ๐, ((๐ผโ(๐โ0)) ยท ๐))) |
12 | 11 | fveq1d 6894 |
. 2
โข (๐ โ ((๐นโ๐)โ0) = (if((๐โ0) = 0 , ๐, ((๐ผโ(๐โ0)) ยท ๐))โ0)) |
13 | | iffv 6909 |
. . 3
โข
(if((๐โ0) =
0 , ๐, ((๐ผโ(๐โ0)) ยท ๐))โ0) = if((๐โ0) = 0 , (๐โ0), (((๐ผโ(๐โ0)) ยท ๐)โ0)) |
14 | 13 | a1i 11 |
. 2
โข (๐ โ (if((๐โ0) = 0 , ๐, ((๐ผโ(๐โ0)) ยท ๐))โ0) = if((๐โ0) = 0 , (๐โ0), (((๐ผโ(๐โ0)) ยท ๐)โ0))) |
15 | | simpr 483 |
. . 3
โข ((๐ โง (๐โ0) = 0 ) โ (๐โ0) = 0 ) |
16 | | prjspnfv01.w |
. . . . 5
โข ๐ = (๐พ freeLMod (0...๐)) |
17 | | eqid 2725 |
. . . . 5
โข
(Baseโ๐) =
(Baseโ๐) |
18 | | eqid 2725 |
. . . . 5
โข
(Baseโ๐พ) =
(Baseโ๐พ) |
19 | | ovexd 7451 |
. . . . 5
โข ((๐ โง ยฌ (๐โ0) = 0 ) โ (0...๐) โ V) |
20 | | prjspnfv01.k |
. . . . . 6
โข (๐ โ ๐พ โ DivRing) |
21 | | ovexd 7451 |
. . . . . . . 8
โข (๐ โ (0...๐) โ V) |
22 | | prjspnfv01.b |
. . . . . . . . . 10
โข ๐ต = ((Baseโ๐) โ
{(0gโ๐)}) |
23 | 8, 22 | eleqtrdi 2835 |
. . . . . . . . 9
โข (๐ โ ๐ โ ((Baseโ๐) โ {(0gโ๐)})) |
24 | 23 | eldifad 3951 |
. . . . . . . 8
โข (๐ โ ๐ โ (Baseโ๐)) |
25 | 16, 18, 17 | frlmbasf 21698 |
. . . . . . . 8
โข
(((0...๐) โ V
โง ๐ โ
(Baseโ๐)) โ
๐:(0...๐)โถ(Baseโ๐พ)) |
26 | 21, 24, 25 | syl2anc 582 |
. . . . . . 7
โข (๐ โ ๐:(0...๐)โถ(Baseโ๐พ)) |
27 | | prjspnfv01.n |
. . . . . . . 8
โข (๐ โ ๐ โ
โ0) |
28 | | 0elfz 13630 |
. . . . . . . 8
โข (๐ โ โ0
โ 0 โ (0...๐)) |
29 | 27, 28 | syl 17 |
. . . . . . 7
โข (๐ โ 0 โ (0...๐)) |
30 | 26, 29 | ffvelcdmd 7090 |
. . . . . 6
โข (๐ โ (๐โ0) โ (Baseโ๐พ)) |
31 | | neqne 2938 |
. . . . . 6
โข (ยฌ
(๐โ0) = 0 โ (๐โ0) โ 0
) |
32 | | prjspnfv01.0 |
. . . . . . 7
โข 0 =
(0gโ๐พ) |
33 | | prjspnfv01.i |
. . . . . . 7
โข ๐ผ = (invrโ๐พ) |
34 | 18, 32, 33 | drnginvrcl 20650 |
. . . . . 6
โข ((๐พ โ DivRing โง (๐โ0) โ
(Baseโ๐พ) โง (๐โ0) โ 0 ) โ
(๐ผโ(๐โ0)) โ (Baseโ๐พ)) |
35 | 20, 30, 31, 34 | syl2an3an 1419 |
. . . . 5
โข ((๐ โง ยฌ (๐โ0) = 0 ) โ (๐ผโ(๐โ0)) โ (Baseโ๐พ)) |
36 | 24 | adantr 479 |
. . . . 5
โข ((๐ โง ยฌ (๐โ0) = 0 ) โ ๐ โ (Baseโ๐)) |
37 | 29 | adantr 479 |
. . . . 5
โข ((๐ โง ยฌ (๐โ0) = 0 ) โ 0 โ
(0...๐)) |
38 | | prjspnfv01.t |
. . . . 5
โข ยท = (
ยท๐ โ๐) |
39 | | eqid 2725 |
. . . . 5
โข
(.rโ๐พ) = (.rโ๐พ) |
40 | 16, 17, 18, 19, 35, 36, 37, 38, 39 | frlmvscaval 21706 |
. . . 4
โข ((๐ โง ยฌ (๐โ0) = 0 ) โ (((๐ผโ(๐โ0)) ยท ๐)โ0) = ((๐ผโ(๐โ0))(.rโ๐พ)(๐โ0))) |
41 | | prjspnfv01.1 |
. . . . . 6
โข 1 =
(1rโ๐พ) |
42 | 18, 32, 39, 41, 33 | drnginvrl 20653 |
. . . . 5
โข ((๐พ โ DivRing โง (๐โ0) โ
(Baseโ๐พ) โง (๐โ0) โ 0 ) โ
((๐ผโ(๐โ0))(.rโ๐พ)(๐โ0)) = 1 ) |
43 | 20, 30, 31, 42 | syl2an3an 1419 |
. . . 4
โข ((๐ โง ยฌ (๐โ0) = 0 ) โ ((๐ผโ(๐โ0))(.rโ๐พ)(๐โ0)) = 1 ) |
44 | 40, 43 | eqtrd 2765 |
. . 3
โข ((๐ โง ยฌ (๐โ0) = 0 ) โ (((๐ผโ(๐โ0)) ยท ๐)โ0) = 1 ) |
45 | 15, 44 | ifeq12da 4557 |
. 2
โข (๐ โ if((๐โ0) = 0 , (๐โ0), (((๐ผโ(๐โ0)) ยท ๐)โ0)) = if((๐โ0) = 0 , 0 , 1 )) |
46 | 12, 14, 45 | 3eqtrd 2769 |
1
โข (๐ โ ((๐นโ๐)โ0) = if((๐โ0) = 0 , 0 , 1 )) |