Step | Hyp | Ref
| Expression |
1 | | simpr 486 |
. 2
โข ((๐พ โ DivRing โง ๐ โ ๐ต) โ ๐ โ ๐ต) |
2 | | 0prjspnrel.b |
. . . 4
โข ๐ต = ((Baseโ๐) โ
{(0gโ๐)}) |
3 | | 0prjspnrel.w |
. . . 4
โข ๐ = (๐พ freeLMod (0...0)) |
4 | | 0prjspnrel.1 |
. . . 4
โข 1 = ((๐พ unitVec
(0...0))โ0) |
5 | 2, 3, 4 | 0prjspnlem 41008 |
. . 3
โข (๐พ โ DivRing โ 1 โ ๐ต) |
6 | 5 | adantr 482 |
. 2
โข ((๐พ โ DivRing โง ๐ โ ๐ต) โ 1 โ ๐ต) |
7 | | ovexd 7396 |
. . . . . 6
โข ((๐พ โ DivRing โง ๐ โ ๐ต) โ (0...0) โ V) |
8 | | difss 4095 |
. . . . . . . . 9
โข
((Baseโ๐)
โ {(0gโ๐)}) โ (Baseโ๐) |
9 | 2, 8 | eqsstri 3982 |
. . . . . . . 8
โข ๐ต โ (Baseโ๐) |
10 | 9 | sseli 3944 |
. . . . . . 7
โข (๐ โ ๐ต โ ๐ โ (Baseโ๐)) |
11 | 10 | adantl 483 |
. . . . . 6
โข ((๐พ โ DivRing โง ๐ โ ๐ต) โ ๐ โ (Baseโ๐)) |
12 | | eqid 2733 |
. . . . . . 7
โข
(Baseโ๐พ) =
(Baseโ๐พ) |
13 | | eqid 2733 |
. . . . . . 7
โข
(Baseโ๐) =
(Baseโ๐) |
14 | 3, 12, 13 | frlmbasf 21189 |
. . . . . 6
โข (((0...0)
โ V โง ๐ โ
(Baseโ๐)) โ
๐:(0...0)โถ(Baseโ๐พ)) |
15 | 7, 11, 14 | syl2anc 585 |
. . . . 5
โข ((๐พ โ DivRing โง ๐ โ ๐ต) โ ๐:(0...0)โถ(Baseโ๐พ)) |
16 | | c0ex 11157 |
. . . . . . . 8
โข 0 โ
V |
17 | 16 | snid 4626 |
. . . . . . 7
โข 0 โ
{0} |
18 | | fz0sn 13550 |
. . . . . . 7
โข (0...0) =
{0} |
19 | 17, 18 | eleqtrri 2833 |
. . . . . 6
โข 0 โ
(0...0) |
20 | 19 | a1i 11 |
. . . . 5
โข ((๐พ โ DivRing โง ๐ โ ๐ต) โ 0 โ (0...0)) |
21 | 15, 20 | ffvelcdmd 7040 |
. . . 4
โข ((๐พ โ DivRing โง ๐ โ ๐ต) โ (๐โ0) โ (Baseโ๐พ)) |
22 | | sneq 4600 |
. . . . . . 7
โข (๐ = (๐โ0) โ {๐} = {(๐โ0)}) |
23 | 22 | xpeq2d 5667 |
. . . . . 6
โข (๐ = (๐โ0) โ ((0...0) ร {๐}) = ((0...0) ร {(๐โ0)})) |
24 | 23 | eqeq2d 2744 |
. . . . 5
โข (๐ = (๐โ0) โ (๐ = ((0...0) ร {๐}) โ ๐ = ((0...0) ร {(๐โ0)}))) |
25 | 24 | adantl 483 |
. . . 4
โข (((๐พ โ DivRing โง ๐ โ ๐ต) โง ๐ = (๐โ0)) โ (๐ = ((0...0) ร {๐}) โ ๐ = ((0...0) ร {(๐โ0)}))) |
26 | 3, 12, 13 | frlmbasmap 21188 |
. . . . . 6
โข (((0...0)
โ V โง ๐ โ
(Baseโ๐)) โ
๐ โ ((Baseโ๐พ) โm
(0...0))) |
27 | 7, 11, 26 | syl2anc 585 |
. . . . 5
โข ((๐พ โ DivRing โง ๐ โ ๐ต) โ ๐ โ ((Baseโ๐พ) โm
(0...0))) |
28 | | fvex 6859 |
. . . . . 6
โข
(Baseโ๐พ)
โ V |
29 | 18, 28, 16 | mapsnconst 8836 |
. . . . 5
โข (๐ โ ((Baseโ๐พ) โm (0...0))
โ ๐ = ((0...0) ร
{(๐โ0)})) |
30 | 27, 29 | syl 17 |
. . . 4
โข ((๐พ โ DivRing โง ๐ โ ๐ต) โ ๐ = ((0...0) ร {(๐โ0)})) |
31 | 21, 25, 30 | rspcedvd 3585 |
. . 3
โข ((๐พ โ DivRing โง ๐ โ ๐ต) โ โ๐ โ (Baseโ๐พ)๐ = ((0...0) ร {๐})) |
32 | | simprl 770 |
. . . . 5
โข (((๐พ โ DivRing โง ๐ โ ๐ต) โง (๐ โ (Baseโ๐พ) โง ๐ = ((0...0) ร {๐}))) โ ๐ โ (Baseโ๐พ)) |
33 | | 0prjspnrel.s |
. . . . 5
โข ๐ = (Baseโ๐พ) |
34 | 32, 33 | eleqtrrdi 2845 |
. . . 4
โข (((๐พ โ DivRing โง ๐ โ ๐ต) โง (๐ โ (Baseโ๐พ) โง ๐ = ((0...0) ร {๐}))) โ ๐ โ ๐) |
35 | | oveq1 7368 |
. . . . . 6
โข (๐ = ๐ โ (๐ ยท 1 ) = (๐ ยท 1 )) |
36 | 35 | eqeq2d 2744 |
. . . . 5
โข (๐ = ๐ โ (๐ = (๐ ยท 1 ) โ ๐ = (๐ ยท 1 ))) |
37 | 36 | adantl 483 |
. . . 4
โข ((((๐พ โ DivRing โง ๐ โ ๐ต) โง (๐ โ (Baseโ๐พ) โง ๐ = ((0...0) ร {๐}))) โง ๐ = ๐) โ (๐ = (๐ ยท 1 ) โ ๐ = (๐ ยท 1 ))) |
38 | | ovexd 7396 |
. . . . . . . . 9
โข (((๐พ โ DivRing โง ๐ โ ๐ต) โง ๐ โ (Baseโ๐พ)) โ (0...0) โ V) |
39 | | simpr 486 |
. . . . . . . . 9
โข (((๐พ โ DivRing โง ๐ โ ๐ต) โง ๐ โ (Baseโ๐พ)) โ ๐ โ (Baseโ๐พ)) |
40 | 5 | ad2antrr 725 |
. . . . . . . . . 10
โข (((๐พ โ DivRing โง ๐ โ ๐ต) โง ๐ โ (Baseโ๐พ)) โ 1 โ ๐ต) |
41 | 9, 40 | sselid 3946 |
. . . . . . . . 9
โข (((๐พ โ DivRing โง ๐ โ ๐ต) โง ๐ โ (Baseโ๐พ)) โ 1 โ (Baseโ๐)) |
42 | | 0prjspnrel.x |
. . . . . . . . 9
โข ยท = (
ยท๐ โ๐) |
43 | | eqid 2733 |
. . . . . . . . 9
โข
(.rโ๐พ) = (.rโ๐พ) |
44 | 3, 13, 12, 38, 39, 41, 42, 43 | frlmvscafval 21195 |
. . . . . . . 8
โข (((๐พ โ DivRing โง ๐ โ ๐ต) โง ๐ โ (Baseโ๐พ)) โ (๐ ยท 1 ) = (((0...0) ร
{๐}) โf
(.rโ๐พ)
1
)) |
45 | 3, 12, 13 | frlmbasf 21189 |
. . . . . . . . . . 11
โข (((0...0)
โ V โง 1 โ (Baseโ๐)) โ 1
:(0...0)โถ(Baseโ๐พ)) |
46 | 38, 41, 45 | syl2anc 585 |
. . . . . . . . . 10
โข (((๐พ โ DivRing โง ๐ โ ๐ต) โง ๐ โ (Baseโ๐พ)) โ 1
:(0...0)โถ(Baseโ๐พ)) |
47 | | drngring 20226 |
. . . . . . . . . . . . . 14
โข (๐พ โ DivRing โ ๐พ โ Ring) |
48 | | eqid 2733 |
. . . . . . . . . . . . . . 15
โข
(1rโ๐พ) = (1rโ๐พ) |
49 | 12, 48 | ringidcl 19997 |
. . . . . . . . . . . . . 14
โข (๐พ โ Ring โ
(1rโ๐พ)
โ (Baseโ๐พ)) |
50 | 47, 49 | syl 17 |
. . . . . . . . . . . . 13
โข (๐พ โ DivRing โ
(1rโ๐พ)
โ (Baseโ๐พ)) |
51 | 50 | ad2antrr 725 |
. . . . . . . . . . . 12
โข (((๐พ โ DivRing โง ๐ โ ๐ต) โง ๐ โ (Baseโ๐พ)) โ (1rโ๐พ) โ (Baseโ๐พ)) |
52 | 51 | snssd 4773 |
. . . . . . . . . . 11
โข (((๐พ โ DivRing โง ๐ โ ๐ต) โง ๐ โ (Baseโ๐พ)) โ {(1rโ๐พ)} โ (Baseโ๐พ)) |
53 | 4 | a1i 11 |
. . . . . . . . . . . . . . 15
โข (๐ โ (0...0) โ 1 = ((๐พ unitVec
(0...0))โ0)) |
54 | | elfz1eq 13461 |
. . . . . . . . . . . . . . 15
โข (๐ โ (0...0) โ ๐ = 0) |
55 | 53, 54 | fveq12d 6853 |
. . . . . . . . . . . . . 14
โข (๐ โ (0...0) โ ( 1 โ๐) = (((๐พ unitVec
(0...0))โ0)โ0)) |
56 | 55 | adantl 483 |
. . . . . . . . . . . . 13
โข ((((๐พ โ DivRing โง ๐ โ ๐ต) โง ๐ โ (Baseโ๐พ)) โง ๐ โ (0...0)) โ ( 1 โ๐) = (((๐พ unitVec
(0...0))โ0)โ0)) |
57 | | eqid 2733 |
. . . . . . . . . . . . . . 15
โข (๐พ unitVec (0...0)) = (๐พ unitVec
(0...0)) |
58 | | simplll 774 |
. . . . . . . . . . . . . . 15
โข ((((๐พ โ DivRing โง ๐ โ ๐ต) โง ๐ โ (Baseโ๐พ)) โง ๐ โ (0...0)) โ ๐พ โ DivRing) |
59 | | ovexd 7396 |
. . . . . . . . . . . . . . 15
โข ((((๐พ โ DivRing โง ๐ โ ๐ต) โง ๐ โ (Baseโ๐พ)) โง ๐ โ (0...0)) โ (0...0) โ
V) |
60 | 19 | a1i 11 |
. . . . . . . . . . . . . . 15
โข ((((๐พ โ DivRing โง ๐ โ ๐ต) โง ๐ โ (Baseโ๐พ)) โง ๐ โ (0...0)) โ 0 โ
(0...0)) |
61 | 57, 58, 59, 60, 48 | uvcvv1 21218 |
. . . . . . . . . . . . . 14
โข ((((๐พ โ DivRing โง ๐ โ ๐ต) โง ๐ โ (Baseโ๐พ)) โง ๐ โ (0...0)) โ (((๐พ unitVec (0...0))โ0)โ0) =
(1rโ๐พ)) |
62 | | fvex 6859 |
. . . . . . . . . . . . . . 15
โข (((๐พ unitVec
(0...0))โ0)โ0) โ V |
63 | 62 | elsn 4605 |
. . . . . . . . . . . . . 14
โข ((((๐พ unitVec
(0...0))โ0)โ0) โ {(1rโ๐พ)} โ (((๐พ unitVec (0...0))โ0)โ0) =
(1rโ๐พ)) |
64 | 61, 63 | sylibr 233 |
. . . . . . . . . . . . 13
โข ((((๐พ โ DivRing โง ๐ โ ๐ต) โง ๐ โ (Baseโ๐พ)) โง ๐ โ (0...0)) โ (((๐พ unitVec (0...0))โ0)โ0) โ
{(1rโ๐พ)}) |
65 | 56, 64 | eqeltrd 2834 |
. . . . . . . . . . . 12
โข ((((๐พ โ DivRing โง ๐ โ ๐ต) โง ๐ โ (Baseโ๐พ)) โง ๐ โ (0...0)) โ ( 1 โ๐) โ {(1rโ๐พ)}) |
66 | 65 | ralrimiva 3140 |
. . . . . . . . . . 11
โข (((๐พ โ DivRing โง ๐ โ ๐ต) โง ๐ โ (Baseโ๐พ)) โ โ๐ โ (0...0)( 1 โ๐) โ {(1rโ๐พ)}) |
67 | | fcdmssb 7073 |
. . . . . . . . . . 11
โข
(({(1rโ๐พ)} โ (Baseโ๐พ) โง โ๐ โ (0...0)( 1 โ๐) โ {(1rโ๐พ)}) โ ( 1
:(0...0)โถ(Baseโ๐พ) โ 1
:(0...0)โถ{(1rโ๐พ)})) |
68 | 52, 66, 67 | syl2anc 585 |
. . . . . . . . . 10
โข (((๐พ โ DivRing โง ๐ โ ๐ต) โง ๐ โ (Baseโ๐พ)) โ ( 1
:(0...0)โถ(Baseโ๐พ) โ 1
:(0...0)โถ{(1rโ๐พ)})) |
69 | 46, 68 | mpbid 231 |
. . . . . . . . 9
โข (((๐พ โ DivRing โง ๐ โ ๐ต) โง ๐ โ (Baseโ๐พ)) โ 1
:(0...0)โถ{(1rโ๐พ)}) |
70 | | vex 3451 |
. . . . . . . . . 10
โข ๐ โ V |
71 | 70 | a1i 11 |
. . . . . . . . 9
โข (((๐พ โ DivRing โง ๐ โ ๐ต) โง ๐ โ (Baseโ๐พ)) โ ๐ โ V) |
72 | | elsni 4607 |
. . . . . . . . . . 11
โข (๐ โ
{(1rโ๐พ)}
โ ๐ =
(1rโ๐พ)) |
73 | 72 | oveq2d 7377 |
. . . . . . . . . 10
โข (๐ โ
{(1rโ๐พ)}
โ (๐(.rโ๐พ)๐) = (๐(.rโ๐พ)(1rโ๐พ))) |
74 | 47 | ad2antrr 725 |
. . . . . . . . . . 11
โข (((๐พ โ DivRing โง ๐ โ ๐ต) โง ๐ โ (Baseโ๐พ)) โ ๐พ โ Ring) |
75 | 12, 43, 48 | ringridm 20001 |
. . . . . . . . . . 11
โข ((๐พ โ Ring โง ๐ โ (Baseโ๐พ)) โ (๐(.rโ๐พ)(1rโ๐พ)) = ๐) |
76 | 74, 39, 75 | syl2anc 585 |
. . . . . . . . . 10
โข (((๐พ โ DivRing โง ๐ โ ๐ต) โง ๐ โ (Baseโ๐พ)) โ (๐(.rโ๐พ)(1rโ๐พ)) = ๐) |
77 | 73, 76 | sylan9eqr 2795 |
. . . . . . . . 9
โข ((((๐พ โ DivRing โง ๐ โ ๐ต) โง ๐ โ (Baseโ๐พ)) โง ๐ โ {(1rโ๐พ)}) โ (๐(.rโ๐พ)๐) = ๐) |
78 | 38, 69, 71, 71, 77 | caofid2 7655 |
. . . . . . . 8
โข (((๐พ โ DivRing โง ๐ โ ๐ต) โง ๐ โ (Baseโ๐พ)) โ (((0...0) ร {๐}) โf
(.rโ๐พ)
1 ) =
((0...0) ร {๐})) |
79 | 44, 78 | eqtrd 2773 |
. . . . . . 7
โข (((๐พ โ DivRing โง ๐ โ ๐ต) โง ๐ โ (Baseโ๐พ)) โ (๐ ยท 1 ) = ((0...0) ร
{๐})) |
80 | 79 | eqeq2d 2744 |
. . . . . 6
โข (((๐พ โ DivRing โง ๐ โ ๐ต) โง ๐ โ (Baseโ๐พ)) โ (๐ = (๐ ยท 1 ) โ ๐ = ((0...0) ร {๐}))) |
81 | 80 | biimprd 248 |
. . . . 5
โข (((๐พ โ DivRing โง ๐ โ ๐ต) โง ๐ โ (Baseโ๐พ)) โ (๐ = ((0...0) ร {๐}) โ ๐ = (๐ ยท 1 ))) |
82 | 81 | impr 456 |
. . . 4
โข (((๐พ โ DivRing โง ๐ โ ๐ต) โง (๐ โ (Baseโ๐พ) โง ๐ = ((0...0) ร {๐}))) โ ๐ = (๐ ยท 1 )) |
83 | 34, 37, 82 | rspcedvd 3585 |
. . 3
โข (((๐พ โ DivRing โง ๐ โ ๐ต) โง (๐ โ (Baseโ๐พ) โง ๐ = ((0...0) ร {๐}))) โ โ๐ โ ๐ ๐ = (๐ ยท 1 )) |
84 | 31, 83 | rexlimddv 3155 |
. 2
โข ((๐พ โ DivRing โง ๐ โ ๐ต) โ โ๐ โ ๐ ๐ = (๐ ยท 1 )) |
85 | | 0prjspnrel.e |
. . 3
โข โผ =
{โจ๐ฅ, ๐ฆโฉ โฃ ((๐ฅ โ ๐ต โง ๐ฆ โ ๐ต) โง โ๐ โ ๐ ๐ฅ = (๐ ยท ๐ฆ))} |
86 | 85 | prjsprel 40989 |
. 2
โข (๐ โผ 1 โ ((๐ โ ๐ต โง 1 โ ๐ต) โง โ๐ โ ๐ ๐ = (๐ ยท 1 ))) |
87 | 1, 6, 84, 86 | syl21anbrc 1345 |
1
โข ((๐พ โ DivRing โง ๐ โ ๐ต) โ ๐ โผ 1 ) |