Step |
Hyp |
Ref |
Expression |
1 |
|
0prjspnrel.e |
|- .~ = { <. x , y >. | ( ( x e. B /\ y e. B ) /\ E. l e. S x = ( l .x. y ) ) } |
2 |
|
0prjspnrel.b |
|- B = ( ( Base ` W ) \ { ( 0g ` W ) } ) |
3 |
|
0prjspnrel.x |
|- .x. = ( .s ` W ) |
4 |
|
0prjspnrel.s |
|- S = ( Base ` K ) |
5 |
|
0prjspnrel.w |
|- W = ( K freeLMod ( 0 ... 0 ) ) |
6 |
|
0prjspnrel.1 |
|- .1. = ( ( K unitVec ( 0 ... 0 ) ) ` 0 ) |
7 |
|
simpr |
|- ( ( K e. DivRing /\ X e. B ) -> X e. B ) |
8 |
2 5 6
|
0prjspnlem |
|- ( K e. DivRing -> .1. e. B ) |
9 |
8
|
adantr |
|- ( ( K e. DivRing /\ X e. B ) -> .1. e. B ) |
10 |
|
ovexd |
|- ( ( K e. DivRing /\ X e. B ) -> ( 0 ... 0 ) e. _V ) |
11 |
|
difss |
|- ( ( Base ` W ) \ { ( 0g ` W ) } ) C_ ( Base ` W ) |
12 |
2 11
|
eqsstri |
|- B C_ ( Base ` W ) |
13 |
12
|
sseli |
|- ( X e. B -> X e. ( Base ` W ) ) |
14 |
13
|
adantl |
|- ( ( K e. DivRing /\ X e. B ) -> X e. ( Base ` W ) ) |
15 |
|
eqid |
|- ( Base ` K ) = ( Base ` K ) |
16 |
|
eqid |
|- ( Base ` W ) = ( Base ` W ) |
17 |
5 15 16
|
frlmbasf |
|- ( ( ( 0 ... 0 ) e. _V /\ X e. ( Base ` W ) ) -> X : ( 0 ... 0 ) --> ( Base ` K ) ) |
18 |
10 14 17
|
syl2anc |
|- ( ( K e. DivRing /\ X e. B ) -> X : ( 0 ... 0 ) --> ( Base ` K ) ) |
19 |
|
c0ex |
|- 0 e. _V |
20 |
19
|
snid |
|- 0 e. { 0 } |
21 |
|
fz0sn |
|- ( 0 ... 0 ) = { 0 } |
22 |
20 21
|
eleqtrri |
|- 0 e. ( 0 ... 0 ) |
23 |
22
|
a1i |
|- ( ( K e. DivRing /\ X e. B ) -> 0 e. ( 0 ... 0 ) ) |
24 |
18 23
|
ffvelrnd |
|- ( ( K e. DivRing /\ X e. B ) -> ( X ` 0 ) e. ( Base ` K ) ) |
25 |
|
sneq |
|- ( n = ( X ` 0 ) -> { n } = { ( X ` 0 ) } ) |
26 |
25
|
xpeq2d |
|- ( n = ( X ` 0 ) -> ( ( 0 ... 0 ) X. { n } ) = ( ( 0 ... 0 ) X. { ( X ` 0 ) } ) ) |
27 |
26
|
eqeq2d |
|- ( n = ( X ` 0 ) -> ( X = ( ( 0 ... 0 ) X. { n } ) <-> X = ( ( 0 ... 0 ) X. { ( X ` 0 ) } ) ) ) |
28 |
27
|
adantl |
|- ( ( ( K e. DivRing /\ X e. B ) /\ n = ( X ` 0 ) ) -> ( X = ( ( 0 ... 0 ) X. { n } ) <-> X = ( ( 0 ... 0 ) X. { ( X ` 0 ) } ) ) ) |
29 |
5 15 16
|
frlmbasmap |
|- ( ( ( 0 ... 0 ) e. _V /\ X e. ( Base ` W ) ) -> X e. ( ( Base ` K ) ^m ( 0 ... 0 ) ) ) |
30 |
10 14 29
|
syl2anc |
|- ( ( K e. DivRing /\ X e. B ) -> X e. ( ( Base ` K ) ^m ( 0 ... 0 ) ) ) |
31 |
|
fvex |
|- ( Base ` K ) e. _V |
32 |
21 31 19
|
mapsnconst |
|- ( X e. ( ( Base ` K ) ^m ( 0 ... 0 ) ) -> X = ( ( 0 ... 0 ) X. { ( X ` 0 ) } ) ) |
33 |
30 32
|
syl |
|- ( ( K e. DivRing /\ X e. B ) -> X = ( ( 0 ... 0 ) X. { ( X ` 0 ) } ) ) |
34 |
24 28 33
|
rspcedvd |
|- ( ( K e. DivRing /\ X e. B ) -> E. n e. ( Base ` K ) X = ( ( 0 ... 0 ) X. { n } ) ) |
35 |
|
simprl |
|- ( ( ( K e. DivRing /\ X e. B ) /\ ( n e. ( Base ` K ) /\ X = ( ( 0 ... 0 ) X. { n } ) ) ) -> n e. ( Base ` K ) ) |
36 |
35 4
|
eleqtrrdi |
|- ( ( ( K e. DivRing /\ X e. B ) /\ ( n e. ( Base ` K ) /\ X = ( ( 0 ... 0 ) X. { n } ) ) ) -> n e. S ) |
37 |
|
oveq1 |
|- ( m = n -> ( m .x. .1. ) = ( n .x. .1. ) ) |
38 |
37
|
eqeq2d |
|- ( m = n -> ( X = ( m .x. .1. ) <-> X = ( n .x. .1. ) ) ) |
39 |
38
|
adantl |
|- ( ( ( ( K e. DivRing /\ X e. B ) /\ ( n e. ( Base ` K ) /\ X = ( ( 0 ... 0 ) X. { n } ) ) ) /\ m = n ) -> ( X = ( m .x. .1. ) <-> X = ( n .x. .1. ) ) ) |
40 |
|
ovexd |
|- ( ( ( K e. DivRing /\ X e. B ) /\ n e. ( Base ` K ) ) -> ( 0 ... 0 ) e. _V ) |
41 |
|
simpr |
|- ( ( ( K e. DivRing /\ X e. B ) /\ n e. ( Base ` K ) ) -> n e. ( Base ` K ) ) |
42 |
8
|
ad2antrr |
|- ( ( ( K e. DivRing /\ X e. B ) /\ n e. ( Base ` K ) ) -> .1. e. B ) |
43 |
12 42
|
sselid |
|- ( ( ( K e. DivRing /\ X e. B ) /\ n e. ( Base ` K ) ) -> .1. e. ( Base ` W ) ) |
44 |
|
eqid |
|- ( .r ` K ) = ( .r ` K ) |
45 |
5 16 15 40 41 43 3 44
|
frlmvscafval |
|- ( ( ( K e. DivRing /\ X e. B ) /\ n e. ( Base ` K ) ) -> ( n .x. .1. ) = ( ( ( 0 ... 0 ) X. { n } ) oF ( .r ` K ) .1. ) ) |
46 |
5 15 16
|
frlmbasf |
|- ( ( ( 0 ... 0 ) e. _V /\ .1. e. ( Base ` W ) ) -> .1. : ( 0 ... 0 ) --> ( Base ` K ) ) |
47 |
40 43 46
|
syl2anc |
|- ( ( ( K e. DivRing /\ X e. B ) /\ n e. ( Base ` K ) ) -> .1. : ( 0 ... 0 ) --> ( Base ` K ) ) |
48 |
|
drngring |
|- ( K e. DivRing -> K e. Ring ) |
49 |
|
eqid |
|- ( 1r ` K ) = ( 1r ` K ) |
50 |
15 49
|
ringidcl |
|- ( K e. Ring -> ( 1r ` K ) e. ( Base ` K ) ) |
51 |
48 50
|
syl |
|- ( K e. DivRing -> ( 1r ` K ) e. ( Base ` K ) ) |
52 |
51
|
ad2antrr |
|- ( ( ( K e. DivRing /\ X e. B ) /\ n e. ( Base ` K ) ) -> ( 1r ` K ) e. ( Base ` K ) ) |
53 |
52
|
snssd |
|- ( ( ( K e. DivRing /\ X e. B ) /\ n e. ( Base ` K ) ) -> { ( 1r ` K ) } C_ ( Base ` K ) ) |
54 |
6
|
a1i |
|- ( d e. ( 0 ... 0 ) -> .1. = ( ( K unitVec ( 0 ... 0 ) ) ` 0 ) ) |
55 |
|
elfz1eq |
|- ( d e. ( 0 ... 0 ) -> d = 0 ) |
56 |
54 55
|
fveq12d |
|- ( d e. ( 0 ... 0 ) -> ( .1. ` d ) = ( ( ( K unitVec ( 0 ... 0 ) ) ` 0 ) ` 0 ) ) |
57 |
56
|
adantl |
|- ( ( ( ( K e. DivRing /\ X e. B ) /\ n e. ( Base ` K ) ) /\ d e. ( 0 ... 0 ) ) -> ( .1. ` d ) = ( ( ( K unitVec ( 0 ... 0 ) ) ` 0 ) ` 0 ) ) |
58 |
|
eqid |
|- ( K unitVec ( 0 ... 0 ) ) = ( K unitVec ( 0 ... 0 ) ) |
59 |
|
simplll |
|- ( ( ( ( K e. DivRing /\ X e. B ) /\ n e. ( Base ` K ) ) /\ d e. ( 0 ... 0 ) ) -> K e. DivRing ) |
60 |
|
ovexd |
|- ( ( ( ( K e. DivRing /\ X e. B ) /\ n e. ( Base ` K ) ) /\ d e. ( 0 ... 0 ) ) -> ( 0 ... 0 ) e. _V ) |
61 |
22
|
a1i |
|- ( ( ( ( K e. DivRing /\ X e. B ) /\ n e. ( Base ` K ) ) /\ d e. ( 0 ... 0 ) ) -> 0 e. ( 0 ... 0 ) ) |
62 |
58 59 60 61 49
|
uvcvv1 |
|- ( ( ( ( K e. DivRing /\ X e. B ) /\ n e. ( Base ` K ) ) /\ d e. ( 0 ... 0 ) ) -> ( ( ( K unitVec ( 0 ... 0 ) ) ` 0 ) ` 0 ) = ( 1r ` K ) ) |
63 |
|
fvex |
|- ( ( ( K unitVec ( 0 ... 0 ) ) ` 0 ) ` 0 ) e. _V |
64 |
63
|
elsn |
|- ( ( ( ( K unitVec ( 0 ... 0 ) ) ` 0 ) ` 0 ) e. { ( 1r ` K ) } <-> ( ( ( K unitVec ( 0 ... 0 ) ) ` 0 ) ` 0 ) = ( 1r ` K ) ) |
65 |
62 64
|
sylibr |
|- ( ( ( ( K e. DivRing /\ X e. B ) /\ n e. ( Base ` K ) ) /\ d e. ( 0 ... 0 ) ) -> ( ( ( K unitVec ( 0 ... 0 ) ) ` 0 ) ` 0 ) e. { ( 1r ` K ) } ) |
66 |
57 65
|
eqeltrd |
|- ( ( ( ( K e. DivRing /\ X e. B ) /\ n e. ( Base ` K ) ) /\ d e. ( 0 ... 0 ) ) -> ( .1. ` d ) e. { ( 1r ` K ) } ) |
67 |
66
|
ralrimiva |
|- ( ( ( K e. DivRing /\ X e. B ) /\ n e. ( Base ` K ) ) -> A. d e. ( 0 ... 0 ) ( .1. ` d ) e. { ( 1r ` K ) } ) |
68 |
|
frnssb |
|- ( ( { ( 1r ` K ) } C_ ( Base ` K ) /\ A. d e. ( 0 ... 0 ) ( .1. ` d ) e. { ( 1r ` K ) } ) -> ( .1. : ( 0 ... 0 ) --> ( Base ` K ) <-> .1. : ( 0 ... 0 ) --> { ( 1r ` K ) } ) ) |
69 |
53 67 68
|
syl2anc |
|- ( ( ( K e. DivRing /\ X e. B ) /\ n e. ( Base ` K ) ) -> ( .1. : ( 0 ... 0 ) --> ( Base ` K ) <-> .1. : ( 0 ... 0 ) --> { ( 1r ` K ) } ) ) |
70 |
47 69
|
mpbid |
|- ( ( ( K e. DivRing /\ X e. B ) /\ n e. ( Base ` K ) ) -> .1. : ( 0 ... 0 ) --> { ( 1r ` K ) } ) |
71 |
|
vex |
|- n e. _V |
72 |
71
|
a1i |
|- ( ( ( K e. DivRing /\ X e. B ) /\ n e. ( Base ` K ) ) -> n e. _V ) |
73 |
|
elsni |
|- ( c e. { ( 1r ` K ) } -> c = ( 1r ` K ) ) |
74 |
73
|
oveq2d |
|- ( c e. { ( 1r ` K ) } -> ( n ( .r ` K ) c ) = ( n ( .r ` K ) ( 1r ` K ) ) ) |
75 |
48
|
ad2antrr |
|- ( ( ( K e. DivRing /\ X e. B ) /\ n e. ( Base ` K ) ) -> K e. Ring ) |
76 |
15 44 49
|
ringridm |
|- ( ( K e. Ring /\ n e. ( Base ` K ) ) -> ( n ( .r ` K ) ( 1r ` K ) ) = n ) |
77 |
75 41 76
|
syl2anc |
|- ( ( ( K e. DivRing /\ X e. B ) /\ n e. ( Base ` K ) ) -> ( n ( .r ` K ) ( 1r ` K ) ) = n ) |
78 |
74 77
|
sylan9eqr |
|- ( ( ( ( K e. DivRing /\ X e. B ) /\ n e. ( Base ` K ) ) /\ c e. { ( 1r ` K ) } ) -> ( n ( .r ` K ) c ) = n ) |
79 |
40 70 72 72 78
|
caofid2 |
|- ( ( ( K e. DivRing /\ X e. B ) /\ n e. ( Base ` K ) ) -> ( ( ( 0 ... 0 ) X. { n } ) oF ( .r ` K ) .1. ) = ( ( 0 ... 0 ) X. { n } ) ) |
80 |
45 79
|
eqtrd |
|- ( ( ( K e. DivRing /\ X e. B ) /\ n e. ( Base ` K ) ) -> ( n .x. .1. ) = ( ( 0 ... 0 ) X. { n } ) ) |
81 |
80
|
eqeq2d |
|- ( ( ( K e. DivRing /\ X e. B ) /\ n e. ( Base ` K ) ) -> ( X = ( n .x. .1. ) <-> X = ( ( 0 ... 0 ) X. { n } ) ) ) |
82 |
81
|
biimprd |
|- ( ( ( K e. DivRing /\ X e. B ) /\ n e. ( Base ` K ) ) -> ( X = ( ( 0 ... 0 ) X. { n } ) -> X = ( n .x. .1. ) ) ) |
83 |
82
|
impr |
|- ( ( ( K e. DivRing /\ X e. B ) /\ ( n e. ( Base ` K ) /\ X = ( ( 0 ... 0 ) X. { n } ) ) ) -> X = ( n .x. .1. ) ) |
84 |
36 39 83
|
rspcedvd |
|- ( ( ( K e. DivRing /\ X e. B ) /\ ( n e. ( Base ` K ) /\ X = ( ( 0 ... 0 ) X. { n } ) ) ) -> E. m e. S X = ( m .x. .1. ) ) |
85 |
34 84
|
rexlimddv |
|- ( ( K e. DivRing /\ X e. B ) -> E. m e. S X = ( m .x. .1. ) ) |
86 |
1
|
prjsprel |
|- ( X .~ .1. <-> ( ( X e. B /\ .1. e. B ) /\ E. m e. S X = ( m .x. .1. ) ) ) |
87 |
7 9 85 86
|
syl21anbrc |
|- ( ( K e. DivRing /\ X e. B ) -> X .~ .1. ) |