Step |
Hyp |
Ref |
Expression |
1 |
|
frlmlbs.f |
โข ๐น = ( ๐
freeLMod ๐ผ ) |
2 |
|
frlmlbs.u |
โข ๐ = ( ๐
unitVec ๐ผ ) |
3 |
|
frlmlbs.j |
โข ๐ฝ = ( LBasis โ ๐น ) |
4 |
|
eqid |
โข ( Base โ ๐น ) = ( Base โ ๐น ) |
5 |
2 1 4
|
uvcff |
โข ( ( ๐
โ Ring โง ๐ผ โ ๐ ) โ ๐ : ๐ผ โถ ( Base โ ๐น ) ) |
6 |
5
|
frnd |
โข ( ( ๐
โ Ring โง ๐ผ โ ๐ ) โ ran ๐ โ ( Base โ ๐น ) ) |
7 |
|
suppssdm |
โข ( ๐ supp ( 0g โ ๐
) ) โ dom ๐ |
8 |
|
eqid |
โข ( Base โ ๐
) = ( Base โ ๐
) |
9 |
1 8 4
|
frlmbasf |
โข ( ( ๐ผ โ ๐ โง ๐ โ ( Base โ ๐น ) ) โ ๐ : ๐ผ โถ ( Base โ ๐
) ) |
10 |
9
|
adantll |
โข ( ( ( ๐
โ Ring โง ๐ผ โ ๐ ) โง ๐ โ ( Base โ ๐น ) ) โ ๐ : ๐ผ โถ ( Base โ ๐
) ) |
11 |
7 10
|
fssdm |
โข ( ( ( ๐
โ Ring โง ๐ผ โ ๐ ) โง ๐ โ ( Base โ ๐น ) ) โ ( ๐ supp ( 0g โ ๐
) ) โ ๐ผ ) |
12 |
11
|
ralrimiva |
โข ( ( ๐
โ Ring โง ๐ผ โ ๐ ) โ โ ๐ โ ( Base โ ๐น ) ( ๐ supp ( 0g โ ๐
) ) โ ๐ผ ) |
13 |
|
rabid2 |
โข ( ( Base โ ๐น ) = { ๐ โ ( Base โ ๐น ) โฃ ( ๐ supp ( 0g โ ๐
) ) โ ๐ผ } โ โ ๐ โ ( Base โ ๐น ) ( ๐ supp ( 0g โ ๐
) ) โ ๐ผ ) |
14 |
12 13
|
sylibr |
โข ( ( ๐
โ Ring โง ๐ผ โ ๐ ) โ ( Base โ ๐น ) = { ๐ โ ( Base โ ๐น ) โฃ ( ๐ supp ( 0g โ ๐
) ) โ ๐ผ } ) |
15 |
|
ssid |
โข ๐ผ โ ๐ผ |
16 |
|
eqid |
โข ( LSpan โ ๐น ) = ( LSpan โ ๐น ) |
17 |
|
eqid |
โข ( 0g โ ๐
) = ( 0g โ ๐
) |
18 |
|
eqid |
โข { ๐ โ ( Base โ ๐น ) โฃ ( ๐ supp ( 0g โ ๐
) ) โ ๐ผ } = { ๐ โ ( Base โ ๐น ) โฃ ( ๐ supp ( 0g โ ๐
) ) โ ๐ผ } |
19 |
1 2 16 4 17 18
|
frlmsslsp |
โข ( ( ๐
โ Ring โง ๐ผ โ ๐ โง ๐ผ โ ๐ผ ) โ ( ( LSpan โ ๐น ) โ ( ๐ โ ๐ผ ) ) = { ๐ โ ( Base โ ๐น ) โฃ ( ๐ supp ( 0g โ ๐
) ) โ ๐ผ } ) |
20 |
15 19
|
mp3an3 |
โข ( ( ๐
โ Ring โง ๐ผ โ ๐ ) โ ( ( LSpan โ ๐น ) โ ( ๐ โ ๐ผ ) ) = { ๐ โ ( Base โ ๐น ) โฃ ( ๐ supp ( 0g โ ๐
) ) โ ๐ผ } ) |
21 |
|
ffn |
โข ( ๐ : ๐ผ โถ ( Base โ ๐น ) โ ๐ Fn ๐ผ ) |
22 |
|
fnima |
โข ( ๐ Fn ๐ผ โ ( ๐ โ ๐ผ ) = ran ๐ ) |
23 |
5 21 22
|
3syl |
โข ( ( ๐
โ Ring โง ๐ผ โ ๐ ) โ ( ๐ โ ๐ผ ) = ran ๐ ) |
24 |
23
|
fveq2d |
โข ( ( ๐
โ Ring โง ๐ผ โ ๐ ) โ ( ( LSpan โ ๐น ) โ ( ๐ โ ๐ผ ) ) = ( ( LSpan โ ๐น ) โ ran ๐ ) ) |
25 |
14 20 24
|
3eqtr2rd |
โข ( ( ๐
โ Ring โง ๐ผ โ ๐ ) โ ( ( LSpan โ ๐น ) โ ran ๐ ) = ( Base โ ๐น ) ) |
26 |
|
eqid |
โข ( ยท๐ โ ๐น ) = ( ยท๐ โ ๐น ) |
27 |
|
eqid |
โข { ๐ โ ( Base โ ๐น ) โฃ ( ๐ supp ( 0g โ ๐
) ) โ ( ๐ผ โ { ๐ } ) } = { ๐ โ ( Base โ ๐น ) โฃ ( ๐ supp ( 0g โ ๐
) ) โ ( ๐ผ โ { ๐ } ) } |
28 |
|
simpll |
โข ( ( ( ๐
โ Ring โง ๐ผ โ ๐ ) โง ( ๐ โ ๐ผ โง ๐ โ ( ( Base โ ( Scalar โ ๐น ) ) โ { ( 0g โ ( Scalar โ ๐น ) ) } ) ) ) โ ๐
โ Ring ) |
29 |
|
simplr |
โข ( ( ( ๐
โ Ring โง ๐ผ โ ๐ ) โง ( ๐ โ ๐ผ โง ๐ โ ( ( Base โ ( Scalar โ ๐น ) ) โ { ( 0g โ ( Scalar โ ๐น ) ) } ) ) ) โ ๐ผ โ ๐ ) |
30 |
|
difssd |
โข ( ( ( ๐
โ Ring โง ๐ผ โ ๐ ) โง ( ๐ โ ๐ผ โง ๐ โ ( ( Base โ ( Scalar โ ๐น ) ) โ { ( 0g โ ( Scalar โ ๐น ) ) } ) ) ) โ ( ๐ผ โ { ๐ } ) โ ๐ผ ) |
31 |
|
vsnid |
โข ๐ โ { ๐ } |
32 |
|
snssi |
โข ( ๐ โ ๐ผ โ { ๐ } โ ๐ผ ) |
33 |
32
|
ad2antrl |
โข ( ( ( ๐
โ Ring โง ๐ผ โ ๐ ) โง ( ๐ โ ๐ผ โง ๐ โ ( ( Base โ ( Scalar โ ๐น ) ) โ { ( 0g โ ( Scalar โ ๐น ) ) } ) ) ) โ { ๐ } โ ๐ผ ) |
34 |
|
dfss4 |
โข ( { ๐ } โ ๐ผ โ ( ๐ผ โ ( ๐ผ โ { ๐ } ) ) = { ๐ } ) |
35 |
33 34
|
sylib |
โข ( ( ( ๐
โ Ring โง ๐ผ โ ๐ ) โง ( ๐ โ ๐ผ โง ๐ โ ( ( Base โ ( Scalar โ ๐น ) ) โ { ( 0g โ ( Scalar โ ๐น ) ) } ) ) ) โ ( ๐ผ โ ( ๐ผ โ { ๐ } ) ) = { ๐ } ) |
36 |
31 35
|
eleqtrrid |
โข ( ( ( ๐
โ Ring โง ๐ผ โ ๐ ) โง ( ๐ โ ๐ผ โง ๐ โ ( ( Base โ ( Scalar โ ๐น ) ) โ { ( 0g โ ( Scalar โ ๐น ) ) } ) ) ) โ ๐ โ ( ๐ผ โ ( ๐ผ โ { ๐ } ) ) ) |
37 |
1
|
frlmsca |
โข ( ( ๐
โ Ring โง ๐ผ โ ๐ ) โ ๐
= ( Scalar โ ๐น ) ) |
38 |
37
|
fveq2d |
โข ( ( ๐
โ Ring โง ๐ผ โ ๐ ) โ ( Base โ ๐
) = ( Base โ ( Scalar โ ๐น ) ) ) |
39 |
37
|
fveq2d |
โข ( ( ๐
โ Ring โง ๐ผ โ ๐ ) โ ( 0g โ ๐
) = ( 0g โ ( Scalar โ ๐น ) ) ) |
40 |
39
|
sneqd |
โข ( ( ๐
โ Ring โง ๐ผ โ ๐ ) โ { ( 0g โ ๐
) } = { ( 0g โ ( Scalar โ ๐น ) ) } ) |
41 |
38 40
|
difeq12d |
โข ( ( ๐
โ Ring โง ๐ผ โ ๐ ) โ ( ( Base โ ๐
) โ { ( 0g โ ๐
) } ) = ( ( Base โ ( Scalar โ ๐น ) ) โ { ( 0g โ ( Scalar โ ๐น ) ) } ) ) |
42 |
41
|
eleq2d |
โข ( ( ๐
โ Ring โง ๐ผ โ ๐ ) โ ( ๐ โ ( ( Base โ ๐
) โ { ( 0g โ ๐
) } ) โ ๐ โ ( ( Base โ ( Scalar โ ๐น ) ) โ { ( 0g โ ( Scalar โ ๐น ) ) } ) ) ) |
43 |
42
|
biimpar |
โข ( ( ( ๐
โ Ring โง ๐ผ โ ๐ ) โง ๐ โ ( ( Base โ ( Scalar โ ๐น ) ) โ { ( 0g โ ( Scalar โ ๐น ) ) } ) ) โ ๐ โ ( ( Base โ ๐
) โ { ( 0g โ ๐
) } ) ) |
44 |
43
|
adantrl |
โข ( ( ( ๐
โ Ring โง ๐ผ โ ๐ ) โง ( ๐ โ ๐ผ โง ๐ โ ( ( Base โ ( Scalar โ ๐น ) ) โ { ( 0g โ ( Scalar โ ๐น ) ) } ) ) ) โ ๐ โ ( ( Base โ ๐
) โ { ( 0g โ ๐
) } ) ) |
45 |
1 2 4 8 26 17 27 28 29 30 36 44
|
frlmssuvc2 |
โข ( ( ( ๐
โ Ring โง ๐ผ โ ๐ ) โง ( ๐ โ ๐ผ โง ๐ โ ( ( Base โ ( Scalar โ ๐น ) ) โ { ( 0g โ ( Scalar โ ๐น ) ) } ) ) ) โ ยฌ ( ๐ ( ยท๐ โ ๐น ) ( ๐ โ ๐ ) ) โ { ๐ โ ( Base โ ๐น ) โฃ ( ๐ supp ( 0g โ ๐
) ) โ ( ๐ผ โ { ๐ } ) } ) |
46 |
17 8
|
ringelnzr |
โข ( ( ๐
โ Ring โง ๐ โ ( ( Base โ ๐
) โ { ( 0g โ ๐
) } ) ) โ ๐
โ NzRing ) |
47 |
28 44 46
|
syl2anc |
โข ( ( ( ๐
โ Ring โง ๐ผ โ ๐ ) โง ( ๐ โ ๐ผ โง ๐ โ ( ( Base โ ( Scalar โ ๐น ) ) โ { ( 0g โ ( Scalar โ ๐น ) ) } ) ) ) โ ๐
โ NzRing ) |
48 |
2 1 4
|
uvcf1 |
โข ( ( ๐
โ NzRing โง ๐ผ โ ๐ ) โ ๐ : ๐ผ โ1-1โ ( Base โ ๐น ) ) |
49 |
47 29 48
|
syl2anc |
โข ( ( ( ๐
โ Ring โง ๐ผ โ ๐ ) โง ( ๐ โ ๐ผ โง ๐ โ ( ( Base โ ( Scalar โ ๐น ) ) โ { ( 0g โ ( Scalar โ ๐น ) ) } ) ) ) โ ๐ : ๐ผ โ1-1โ ( Base โ ๐น ) ) |
50 |
|
df-f1 |
โข ( ๐ : ๐ผ โ1-1โ ( Base โ ๐น ) โ ( ๐ : ๐ผ โถ ( Base โ ๐น ) โง Fun โก ๐ ) ) |
51 |
50
|
simprbi |
โข ( ๐ : ๐ผ โ1-1โ ( Base โ ๐น ) โ Fun โก ๐ ) |
52 |
|
imadif |
โข ( Fun โก ๐ โ ( ๐ โ ( ๐ผ โ { ๐ } ) ) = ( ( ๐ โ ๐ผ ) โ ( ๐ โ { ๐ } ) ) ) |
53 |
49 51 52
|
3syl |
โข ( ( ( ๐
โ Ring โง ๐ผ โ ๐ ) โง ( ๐ โ ๐ผ โง ๐ โ ( ( Base โ ( Scalar โ ๐น ) ) โ { ( 0g โ ( Scalar โ ๐น ) ) } ) ) ) โ ( ๐ โ ( ๐ผ โ { ๐ } ) ) = ( ( ๐ โ ๐ผ ) โ ( ๐ โ { ๐ } ) ) ) |
54 |
|
f1fn |
โข ( ๐ : ๐ผ โ1-1โ ( Base โ ๐น ) โ ๐ Fn ๐ผ ) |
55 |
49 54 22
|
3syl |
โข ( ( ( ๐
โ Ring โง ๐ผ โ ๐ ) โง ( ๐ โ ๐ผ โง ๐ โ ( ( Base โ ( Scalar โ ๐น ) ) โ { ( 0g โ ( Scalar โ ๐น ) ) } ) ) ) โ ( ๐ โ ๐ผ ) = ran ๐ ) |
56 |
49 54
|
syl |
โข ( ( ( ๐
โ Ring โง ๐ผ โ ๐ ) โง ( ๐ โ ๐ผ โง ๐ โ ( ( Base โ ( Scalar โ ๐น ) ) โ { ( 0g โ ( Scalar โ ๐น ) ) } ) ) ) โ ๐ Fn ๐ผ ) |
57 |
|
simprl |
โข ( ( ( ๐
โ Ring โง ๐ผ โ ๐ ) โง ( ๐ โ ๐ผ โง ๐ โ ( ( Base โ ( Scalar โ ๐น ) ) โ { ( 0g โ ( Scalar โ ๐น ) ) } ) ) ) โ ๐ โ ๐ผ ) |
58 |
|
fnsnfv |
โข ( ( ๐ Fn ๐ผ โง ๐ โ ๐ผ ) โ { ( ๐ โ ๐ ) } = ( ๐ โ { ๐ } ) ) |
59 |
56 57 58
|
syl2anc |
โข ( ( ( ๐
โ Ring โง ๐ผ โ ๐ ) โง ( ๐ โ ๐ผ โง ๐ โ ( ( Base โ ( Scalar โ ๐น ) ) โ { ( 0g โ ( Scalar โ ๐น ) ) } ) ) ) โ { ( ๐ โ ๐ ) } = ( ๐ โ { ๐ } ) ) |
60 |
59
|
eqcomd |
โข ( ( ( ๐
โ Ring โง ๐ผ โ ๐ ) โง ( ๐ โ ๐ผ โง ๐ โ ( ( Base โ ( Scalar โ ๐น ) ) โ { ( 0g โ ( Scalar โ ๐น ) ) } ) ) ) โ ( ๐ โ { ๐ } ) = { ( ๐ โ ๐ ) } ) |
61 |
55 60
|
difeq12d |
โข ( ( ( ๐
โ Ring โง ๐ผ โ ๐ ) โง ( ๐ โ ๐ผ โง ๐ โ ( ( Base โ ( Scalar โ ๐น ) ) โ { ( 0g โ ( Scalar โ ๐น ) ) } ) ) ) โ ( ( ๐ โ ๐ผ ) โ ( ๐ โ { ๐ } ) ) = ( ran ๐ โ { ( ๐ โ ๐ ) } ) ) |
62 |
53 61
|
eqtr2d |
โข ( ( ( ๐
โ Ring โง ๐ผ โ ๐ ) โง ( ๐ โ ๐ผ โง ๐ โ ( ( Base โ ( Scalar โ ๐น ) ) โ { ( 0g โ ( Scalar โ ๐น ) ) } ) ) ) โ ( ran ๐ โ { ( ๐ โ ๐ ) } ) = ( ๐ โ ( ๐ผ โ { ๐ } ) ) ) |
63 |
62
|
fveq2d |
โข ( ( ( ๐
โ Ring โง ๐ผ โ ๐ ) โง ( ๐ โ ๐ผ โง ๐ โ ( ( Base โ ( Scalar โ ๐น ) ) โ { ( 0g โ ( Scalar โ ๐น ) ) } ) ) ) โ ( ( LSpan โ ๐น ) โ ( ran ๐ โ { ( ๐ โ ๐ ) } ) ) = ( ( LSpan โ ๐น ) โ ( ๐ โ ( ๐ผ โ { ๐ } ) ) ) ) |
64 |
1 2 16 4 17 27
|
frlmsslsp |
โข ( ( ๐
โ Ring โง ๐ผ โ ๐ โง ( ๐ผ โ { ๐ } ) โ ๐ผ ) โ ( ( LSpan โ ๐น ) โ ( ๐ โ ( ๐ผ โ { ๐ } ) ) ) = { ๐ โ ( Base โ ๐น ) โฃ ( ๐ supp ( 0g โ ๐
) ) โ ( ๐ผ โ { ๐ } ) } ) |
65 |
28 29 30 64
|
syl3anc |
โข ( ( ( ๐
โ Ring โง ๐ผ โ ๐ ) โง ( ๐ โ ๐ผ โง ๐ โ ( ( Base โ ( Scalar โ ๐น ) ) โ { ( 0g โ ( Scalar โ ๐น ) ) } ) ) ) โ ( ( LSpan โ ๐น ) โ ( ๐ โ ( ๐ผ โ { ๐ } ) ) ) = { ๐ โ ( Base โ ๐น ) โฃ ( ๐ supp ( 0g โ ๐
) ) โ ( ๐ผ โ { ๐ } ) } ) |
66 |
63 65
|
eqtrd |
โข ( ( ( ๐
โ Ring โง ๐ผ โ ๐ ) โง ( ๐ โ ๐ผ โง ๐ โ ( ( Base โ ( Scalar โ ๐น ) ) โ { ( 0g โ ( Scalar โ ๐น ) ) } ) ) ) โ ( ( LSpan โ ๐น ) โ ( ran ๐ โ { ( ๐ โ ๐ ) } ) ) = { ๐ โ ( Base โ ๐น ) โฃ ( ๐ supp ( 0g โ ๐
) ) โ ( ๐ผ โ { ๐ } ) } ) |
67 |
45 66
|
neleqtrrd |
โข ( ( ( ๐
โ Ring โง ๐ผ โ ๐ ) โง ( ๐ โ ๐ผ โง ๐ โ ( ( Base โ ( Scalar โ ๐น ) ) โ { ( 0g โ ( Scalar โ ๐น ) ) } ) ) ) โ ยฌ ( ๐ ( ยท๐ โ ๐น ) ( ๐ โ ๐ ) ) โ ( ( LSpan โ ๐น ) โ ( ran ๐ โ { ( ๐ โ ๐ ) } ) ) ) |
68 |
67
|
ralrimivva |
โข ( ( ๐
โ Ring โง ๐ผ โ ๐ ) โ โ ๐ โ ๐ผ โ ๐ โ ( ( Base โ ( Scalar โ ๐น ) ) โ { ( 0g โ ( Scalar โ ๐น ) ) } ) ยฌ ( ๐ ( ยท๐ โ ๐น ) ( ๐ โ ๐ ) ) โ ( ( LSpan โ ๐น ) โ ( ran ๐ โ { ( ๐ โ ๐ ) } ) ) ) |
69 |
|
oveq2 |
โข ( ๐ = ( ๐ โ ๐ ) โ ( ๐ ( ยท๐ โ ๐น ) ๐ ) = ( ๐ ( ยท๐ โ ๐น ) ( ๐ โ ๐ ) ) ) |
70 |
|
sneq |
โข ( ๐ = ( ๐ โ ๐ ) โ { ๐ } = { ( ๐ โ ๐ ) } ) |
71 |
70
|
difeq2d |
โข ( ๐ = ( ๐ โ ๐ ) โ ( ran ๐ โ { ๐ } ) = ( ran ๐ โ { ( ๐ โ ๐ ) } ) ) |
72 |
71
|
fveq2d |
โข ( ๐ = ( ๐ โ ๐ ) โ ( ( LSpan โ ๐น ) โ ( ran ๐ โ { ๐ } ) ) = ( ( LSpan โ ๐น ) โ ( ran ๐ โ { ( ๐ โ ๐ ) } ) ) ) |
73 |
69 72
|
eleq12d |
โข ( ๐ = ( ๐ โ ๐ ) โ ( ( ๐ ( ยท๐ โ ๐น ) ๐ ) โ ( ( LSpan โ ๐น ) โ ( ran ๐ โ { ๐ } ) ) โ ( ๐ ( ยท๐ โ ๐น ) ( ๐ โ ๐ ) ) โ ( ( LSpan โ ๐น ) โ ( ran ๐ โ { ( ๐ โ ๐ ) } ) ) ) ) |
74 |
73
|
notbid |
โข ( ๐ = ( ๐ โ ๐ ) โ ( ยฌ ( ๐ ( ยท๐ โ ๐น ) ๐ ) โ ( ( LSpan โ ๐น ) โ ( ran ๐ โ { ๐ } ) ) โ ยฌ ( ๐ ( ยท๐ โ ๐น ) ( ๐ โ ๐ ) ) โ ( ( LSpan โ ๐น ) โ ( ran ๐ โ { ( ๐ โ ๐ ) } ) ) ) ) |
75 |
74
|
ralbidv |
โข ( ๐ = ( ๐ โ ๐ ) โ ( โ ๐ โ ( ( Base โ ( Scalar โ ๐น ) ) โ { ( 0g โ ( Scalar โ ๐น ) ) } ) ยฌ ( ๐ ( ยท๐ โ ๐น ) ๐ ) โ ( ( LSpan โ ๐น ) โ ( ran ๐ โ { ๐ } ) ) โ โ ๐ โ ( ( Base โ ( Scalar โ ๐น ) ) โ { ( 0g โ ( Scalar โ ๐น ) ) } ) ยฌ ( ๐ ( ยท๐ โ ๐น ) ( ๐ โ ๐ ) ) โ ( ( LSpan โ ๐น ) โ ( ran ๐ โ { ( ๐ โ ๐ ) } ) ) ) ) |
76 |
75
|
ralrn |
โข ( ๐ Fn ๐ผ โ ( โ ๐ โ ran ๐ โ ๐ โ ( ( Base โ ( Scalar โ ๐น ) ) โ { ( 0g โ ( Scalar โ ๐น ) ) } ) ยฌ ( ๐ ( ยท๐ โ ๐น ) ๐ ) โ ( ( LSpan โ ๐น ) โ ( ran ๐ โ { ๐ } ) ) โ โ ๐ โ ๐ผ โ ๐ โ ( ( Base โ ( Scalar โ ๐น ) ) โ { ( 0g โ ( Scalar โ ๐น ) ) } ) ยฌ ( ๐ ( ยท๐ โ ๐น ) ( ๐ โ ๐ ) ) โ ( ( LSpan โ ๐น ) โ ( ran ๐ โ { ( ๐ โ ๐ ) } ) ) ) ) |
77 |
5 21 76
|
3syl |
โข ( ( ๐
โ Ring โง ๐ผ โ ๐ ) โ ( โ ๐ โ ran ๐ โ ๐ โ ( ( Base โ ( Scalar โ ๐น ) ) โ { ( 0g โ ( Scalar โ ๐น ) ) } ) ยฌ ( ๐ ( ยท๐ โ ๐น ) ๐ ) โ ( ( LSpan โ ๐น ) โ ( ran ๐ โ { ๐ } ) ) โ โ ๐ โ ๐ผ โ ๐ โ ( ( Base โ ( Scalar โ ๐น ) ) โ { ( 0g โ ( Scalar โ ๐น ) ) } ) ยฌ ( ๐ ( ยท๐ โ ๐น ) ( ๐ โ ๐ ) ) โ ( ( LSpan โ ๐น ) โ ( ran ๐ โ { ( ๐ โ ๐ ) } ) ) ) ) |
78 |
68 77
|
mpbird |
โข ( ( ๐
โ Ring โง ๐ผ โ ๐ ) โ โ ๐ โ ran ๐ โ ๐ โ ( ( Base โ ( Scalar โ ๐น ) ) โ { ( 0g โ ( Scalar โ ๐น ) ) } ) ยฌ ( ๐ ( ยท๐ โ ๐น ) ๐ ) โ ( ( LSpan โ ๐น ) โ ( ran ๐ โ { ๐ } ) ) ) |
79 |
1
|
ovexi |
โข ๐น โ V |
80 |
|
eqid |
โข ( Scalar โ ๐น ) = ( Scalar โ ๐น ) |
81 |
|
eqid |
โข ( Base โ ( Scalar โ ๐น ) ) = ( Base โ ( Scalar โ ๐น ) ) |
82 |
|
eqid |
โข ( 0g โ ( Scalar โ ๐น ) ) = ( 0g โ ( Scalar โ ๐น ) ) |
83 |
4 80 26 81 3 16 82
|
islbs |
โข ( ๐น โ V โ ( ran ๐ โ ๐ฝ โ ( ran ๐ โ ( Base โ ๐น ) โง ( ( LSpan โ ๐น ) โ ran ๐ ) = ( Base โ ๐น ) โง โ ๐ โ ran ๐ โ ๐ โ ( ( Base โ ( Scalar โ ๐น ) ) โ { ( 0g โ ( Scalar โ ๐น ) ) } ) ยฌ ( ๐ ( ยท๐ โ ๐น ) ๐ ) โ ( ( LSpan โ ๐น ) โ ( ran ๐ โ { ๐ } ) ) ) ) ) |
84 |
79 83
|
ax-mp |
โข ( ran ๐ โ ๐ฝ โ ( ran ๐ โ ( Base โ ๐น ) โง ( ( LSpan โ ๐น ) โ ran ๐ ) = ( Base โ ๐น ) โง โ ๐ โ ran ๐ โ ๐ โ ( ( Base โ ( Scalar โ ๐น ) ) โ { ( 0g โ ( Scalar โ ๐น ) ) } ) ยฌ ( ๐ ( ยท๐ โ ๐น ) ๐ ) โ ( ( LSpan โ ๐น ) โ ( ran ๐ โ { ๐ } ) ) ) ) |
85 |
6 25 78 84
|
syl3anbrc |
โข ( ( ๐
โ Ring โง ๐ผ โ ๐ ) โ ran ๐ โ ๐ฝ ) |