Step |
Hyp |
Ref |
Expression |
1 |
|
islbs.v |
โข ๐ = ( Base โ ๐ ) |
2 |
|
islbs.f |
โข ๐น = ( Scalar โ ๐ ) |
3 |
|
islbs.s |
โข ยท = ( ยท๐ โ ๐ ) |
4 |
|
islbs.k |
โข ๐พ = ( Base โ ๐น ) |
5 |
|
islbs.j |
โข ๐ฝ = ( LBasis โ ๐ ) |
6 |
|
islbs.n |
โข ๐ = ( LSpan โ ๐ ) |
7 |
|
islbs.z |
โข 0 = ( 0g โ ๐น ) |
8 |
|
elex |
โข ( ๐ โ ๐ โ ๐ โ V ) |
9 |
|
fveq2 |
โข ( ๐ค = ๐ โ ( Base โ ๐ค ) = ( Base โ ๐ ) ) |
10 |
9 1
|
eqtr4di |
โข ( ๐ค = ๐ โ ( Base โ ๐ค ) = ๐ ) |
11 |
10
|
pweqd |
โข ( ๐ค = ๐ โ ๐ซ ( Base โ ๐ค ) = ๐ซ ๐ ) |
12 |
|
fvexd |
โข ( ๐ค = ๐ โ ( LSpan โ ๐ค ) โ V ) |
13 |
|
fveq2 |
โข ( ๐ค = ๐ โ ( LSpan โ ๐ค ) = ( LSpan โ ๐ ) ) |
14 |
13 6
|
eqtr4di |
โข ( ๐ค = ๐ โ ( LSpan โ ๐ค ) = ๐ ) |
15 |
|
fvexd |
โข ( ( ๐ค = ๐ โง ๐ = ๐ ) โ ( Scalar โ ๐ค ) โ V ) |
16 |
|
fveq2 |
โข ( ๐ค = ๐ โ ( Scalar โ ๐ค ) = ( Scalar โ ๐ ) ) |
17 |
16
|
adantr |
โข ( ( ๐ค = ๐ โง ๐ = ๐ ) โ ( Scalar โ ๐ค ) = ( Scalar โ ๐ ) ) |
18 |
17 2
|
eqtr4di |
โข ( ( ๐ค = ๐ โง ๐ = ๐ ) โ ( Scalar โ ๐ค ) = ๐น ) |
19 |
|
simplr |
โข ( ( ( ๐ค = ๐ โง ๐ = ๐ ) โง ๐ = ๐น ) โ ๐ = ๐ ) |
20 |
19
|
fveq1d |
โข ( ( ( ๐ค = ๐ โง ๐ = ๐ ) โง ๐ = ๐น ) โ ( ๐ โ ๐ ) = ( ๐ โ ๐ ) ) |
21 |
10
|
ad2antrr |
โข ( ( ( ๐ค = ๐ โง ๐ = ๐ ) โง ๐ = ๐น ) โ ( Base โ ๐ค ) = ๐ ) |
22 |
20 21
|
eqeq12d |
โข ( ( ( ๐ค = ๐ โง ๐ = ๐ ) โง ๐ = ๐น ) โ ( ( ๐ โ ๐ ) = ( Base โ ๐ค ) โ ( ๐ โ ๐ ) = ๐ ) ) |
23 |
|
simpr |
โข ( ( ( ๐ค = ๐ โง ๐ = ๐ ) โง ๐ = ๐น ) โ ๐ = ๐น ) |
24 |
23
|
fveq2d |
โข ( ( ( ๐ค = ๐ โง ๐ = ๐ ) โง ๐ = ๐น ) โ ( Base โ ๐ ) = ( Base โ ๐น ) ) |
25 |
24 4
|
eqtr4di |
โข ( ( ( ๐ค = ๐ โง ๐ = ๐ ) โง ๐ = ๐น ) โ ( Base โ ๐ ) = ๐พ ) |
26 |
23
|
fveq2d |
โข ( ( ( ๐ค = ๐ โง ๐ = ๐ ) โง ๐ = ๐น ) โ ( 0g โ ๐ ) = ( 0g โ ๐น ) ) |
27 |
26 7
|
eqtr4di |
โข ( ( ( ๐ค = ๐ โง ๐ = ๐ ) โง ๐ = ๐น ) โ ( 0g โ ๐ ) = 0 ) |
28 |
27
|
sneqd |
โข ( ( ( ๐ค = ๐ โง ๐ = ๐ ) โง ๐ = ๐น ) โ { ( 0g โ ๐ ) } = { 0 } ) |
29 |
25 28
|
difeq12d |
โข ( ( ( ๐ค = ๐ โง ๐ = ๐ ) โง ๐ = ๐น ) โ ( ( Base โ ๐ ) โ { ( 0g โ ๐ ) } ) = ( ๐พ โ { 0 } ) ) |
30 |
|
fveq2 |
โข ( ๐ค = ๐ โ ( ยท๐ โ ๐ค ) = ( ยท๐ โ ๐ ) ) |
31 |
30 3
|
eqtr4di |
โข ( ๐ค = ๐ โ ( ยท๐ โ ๐ค ) = ยท ) |
32 |
31
|
ad2antrr |
โข ( ( ( ๐ค = ๐ โง ๐ = ๐ ) โง ๐ = ๐น ) โ ( ยท๐ โ ๐ค ) = ยท ) |
33 |
32
|
oveqd |
โข ( ( ( ๐ค = ๐ โง ๐ = ๐ ) โง ๐ = ๐น ) โ ( ๐ฆ ( ยท๐ โ ๐ค ) ๐ฅ ) = ( ๐ฆ ยท ๐ฅ ) ) |
34 |
19
|
fveq1d |
โข ( ( ( ๐ค = ๐ โง ๐ = ๐ ) โง ๐ = ๐น ) โ ( ๐ โ ( ๐ โ { ๐ฅ } ) ) = ( ๐ โ ( ๐ โ { ๐ฅ } ) ) ) |
35 |
33 34
|
eleq12d |
โข ( ( ( ๐ค = ๐ โง ๐ = ๐ ) โง ๐ = ๐น ) โ ( ( ๐ฆ ( ยท๐ โ ๐ค ) ๐ฅ ) โ ( ๐ โ ( ๐ โ { ๐ฅ } ) ) โ ( ๐ฆ ยท ๐ฅ ) โ ( ๐ โ ( ๐ โ { ๐ฅ } ) ) ) ) |
36 |
35
|
notbid |
โข ( ( ( ๐ค = ๐ โง ๐ = ๐ ) โง ๐ = ๐น ) โ ( ยฌ ( ๐ฆ ( ยท๐ โ ๐ค ) ๐ฅ ) โ ( ๐ โ ( ๐ โ { ๐ฅ } ) ) โ ยฌ ( ๐ฆ ยท ๐ฅ ) โ ( ๐ โ ( ๐ โ { ๐ฅ } ) ) ) ) |
37 |
29 36
|
raleqbidv |
โข ( ( ( ๐ค = ๐ โง ๐ = ๐ ) โง ๐ = ๐น ) โ ( โ ๐ฆ โ ( ( Base โ ๐ ) โ { ( 0g โ ๐ ) } ) ยฌ ( ๐ฆ ( ยท๐ โ ๐ค ) ๐ฅ ) โ ( ๐ โ ( ๐ โ { ๐ฅ } ) ) โ โ ๐ฆ โ ( ๐พ โ { 0 } ) ยฌ ( ๐ฆ ยท ๐ฅ ) โ ( ๐ โ ( ๐ โ { ๐ฅ } ) ) ) ) |
38 |
37
|
ralbidv |
โข ( ( ( ๐ค = ๐ โง ๐ = ๐ ) โง ๐ = ๐น ) โ ( โ ๐ฅ โ ๐ โ ๐ฆ โ ( ( Base โ ๐ ) โ { ( 0g โ ๐ ) } ) ยฌ ( ๐ฆ ( ยท๐ โ ๐ค ) ๐ฅ ) โ ( ๐ โ ( ๐ โ { ๐ฅ } ) ) โ โ ๐ฅ โ ๐ โ ๐ฆ โ ( ๐พ โ { 0 } ) ยฌ ( ๐ฆ ยท ๐ฅ ) โ ( ๐ โ ( ๐ โ { ๐ฅ } ) ) ) ) |
39 |
22 38
|
anbi12d |
โข ( ( ( ๐ค = ๐ โง ๐ = ๐ ) โง ๐ = ๐น ) โ ( ( ( ๐ โ ๐ ) = ( Base โ ๐ค ) โง โ ๐ฅ โ ๐ โ ๐ฆ โ ( ( Base โ ๐ ) โ { ( 0g โ ๐ ) } ) ยฌ ( ๐ฆ ( ยท๐ โ ๐ค ) ๐ฅ ) โ ( ๐ โ ( ๐ โ { ๐ฅ } ) ) ) โ ( ( ๐ โ ๐ ) = ๐ โง โ ๐ฅ โ ๐ โ ๐ฆ โ ( ๐พ โ { 0 } ) ยฌ ( ๐ฆ ยท ๐ฅ ) โ ( ๐ โ ( ๐ โ { ๐ฅ } ) ) ) ) ) |
40 |
15 18 39
|
sbcied2 |
โข ( ( ๐ค = ๐ โง ๐ = ๐ ) โ ( [ ( Scalar โ ๐ค ) / ๐ ] ( ( ๐ โ ๐ ) = ( Base โ ๐ค ) โง โ ๐ฅ โ ๐ โ ๐ฆ โ ( ( Base โ ๐ ) โ { ( 0g โ ๐ ) } ) ยฌ ( ๐ฆ ( ยท๐ โ ๐ค ) ๐ฅ ) โ ( ๐ โ ( ๐ โ { ๐ฅ } ) ) ) โ ( ( ๐ โ ๐ ) = ๐ โง โ ๐ฅ โ ๐ โ ๐ฆ โ ( ๐พ โ { 0 } ) ยฌ ( ๐ฆ ยท ๐ฅ ) โ ( ๐ โ ( ๐ โ { ๐ฅ } ) ) ) ) ) |
41 |
12 14 40
|
sbcied2 |
โข ( ๐ค = ๐ โ ( [ ( LSpan โ ๐ค ) / ๐ ] [ ( Scalar โ ๐ค ) / ๐ ] ( ( ๐ โ ๐ ) = ( Base โ ๐ค ) โง โ ๐ฅ โ ๐ โ ๐ฆ โ ( ( Base โ ๐ ) โ { ( 0g โ ๐ ) } ) ยฌ ( ๐ฆ ( ยท๐ โ ๐ค ) ๐ฅ ) โ ( ๐ โ ( ๐ โ { ๐ฅ } ) ) ) โ ( ( ๐ โ ๐ ) = ๐ โง โ ๐ฅ โ ๐ โ ๐ฆ โ ( ๐พ โ { 0 } ) ยฌ ( ๐ฆ ยท ๐ฅ ) โ ( ๐ โ ( ๐ โ { ๐ฅ } ) ) ) ) ) |
42 |
11 41
|
rabeqbidv |
โข ( ๐ค = ๐ โ { ๐ โ ๐ซ ( Base โ ๐ค ) โฃ [ ( LSpan โ ๐ค ) / ๐ ] [ ( Scalar โ ๐ค ) / ๐ ] ( ( ๐ โ ๐ ) = ( Base โ ๐ค ) โง โ ๐ฅ โ ๐ โ ๐ฆ โ ( ( Base โ ๐ ) โ { ( 0g โ ๐ ) } ) ยฌ ( ๐ฆ ( ยท๐ โ ๐ค ) ๐ฅ ) โ ( ๐ โ ( ๐ โ { ๐ฅ } ) ) ) } = { ๐ โ ๐ซ ๐ โฃ ( ( ๐ โ ๐ ) = ๐ โง โ ๐ฅ โ ๐ โ ๐ฆ โ ( ๐พ โ { 0 } ) ยฌ ( ๐ฆ ยท ๐ฅ ) โ ( ๐ โ ( ๐ โ { ๐ฅ } ) ) ) } ) |
43 |
|
df-lbs |
โข LBasis = ( ๐ค โ V โฆ { ๐ โ ๐ซ ( Base โ ๐ค ) โฃ [ ( LSpan โ ๐ค ) / ๐ ] [ ( Scalar โ ๐ค ) / ๐ ] ( ( ๐ โ ๐ ) = ( Base โ ๐ค ) โง โ ๐ฅ โ ๐ โ ๐ฆ โ ( ( Base โ ๐ ) โ { ( 0g โ ๐ ) } ) ยฌ ( ๐ฆ ( ยท๐ โ ๐ค ) ๐ฅ ) โ ( ๐ โ ( ๐ โ { ๐ฅ } ) ) ) } ) |
44 |
1
|
fvexi |
โข ๐ โ V |
45 |
44
|
pwex |
โข ๐ซ ๐ โ V |
46 |
45
|
rabex |
โข { ๐ โ ๐ซ ๐ โฃ ( ( ๐ โ ๐ ) = ๐ โง โ ๐ฅ โ ๐ โ ๐ฆ โ ( ๐พ โ { 0 } ) ยฌ ( ๐ฆ ยท ๐ฅ ) โ ( ๐ โ ( ๐ โ { ๐ฅ } ) ) ) } โ V |
47 |
42 43 46
|
fvmpt |
โข ( ๐ โ V โ ( LBasis โ ๐ ) = { ๐ โ ๐ซ ๐ โฃ ( ( ๐ โ ๐ ) = ๐ โง โ ๐ฅ โ ๐ โ ๐ฆ โ ( ๐พ โ { 0 } ) ยฌ ( ๐ฆ ยท ๐ฅ ) โ ( ๐ โ ( ๐ โ { ๐ฅ } ) ) ) } ) |
48 |
5 47
|
eqtrid |
โข ( ๐ โ V โ ๐ฝ = { ๐ โ ๐ซ ๐ โฃ ( ( ๐ โ ๐ ) = ๐ โง โ ๐ฅ โ ๐ โ ๐ฆ โ ( ๐พ โ { 0 } ) ยฌ ( ๐ฆ ยท ๐ฅ ) โ ( ๐ โ ( ๐ โ { ๐ฅ } ) ) ) } ) |
49 |
8 48
|
syl |
โข ( ๐ โ ๐ โ ๐ฝ = { ๐ โ ๐ซ ๐ โฃ ( ( ๐ โ ๐ ) = ๐ โง โ ๐ฅ โ ๐ โ ๐ฆ โ ( ๐พ โ { 0 } ) ยฌ ( ๐ฆ ยท ๐ฅ ) โ ( ๐ โ ( ๐ โ { ๐ฅ } ) ) ) } ) |
50 |
49
|
eleq2d |
โข ( ๐ โ ๐ โ ( ๐ต โ ๐ฝ โ ๐ต โ { ๐ โ ๐ซ ๐ โฃ ( ( ๐ โ ๐ ) = ๐ โง โ ๐ฅ โ ๐ โ ๐ฆ โ ( ๐พ โ { 0 } ) ยฌ ( ๐ฆ ยท ๐ฅ ) โ ( ๐ โ ( ๐ โ { ๐ฅ } ) ) ) } ) ) |
51 |
44
|
elpw2 |
โข ( ๐ต โ ๐ซ ๐ โ ๐ต โ ๐ ) |
52 |
51
|
anbi1i |
โข ( ( ๐ต โ ๐ซ ๐ โง ( ( ๐ โ ๐ต ) = ๐ โง โ ๐ฅ โ ๐ต โ ๐ฆ โ ( ๐พ โ { 0 } ) ยฌ ( ๐ฆ ยท ๐ฅ ) โ ( ๐ โ ( ๐ต โ { ๐ฅ } ) ) ) ) โ ( ๐ต โ ๐ โง ( ( ๐ โ ๐ต ) = ๐ โง โ ๐ฅ โ ๐ต โ ๐ฆ โ ( ๐พ โ { 0 } ) ยฌ ( ๐ฆ ยท ๐ฅ ) โ ( ๐ โ ( ๐ต โ { ๐ฅ } ) ) ) ) ) |
53 |
|
fveqeq2 |
โข ( ๐ = ๐ต โ ( ( ๐ โ ๐ ) = ๐ โ ( ๐ โ ๐ต ) = ๐ ) ) |
54 |
|
difeq1 |
โข ( ๐ = ๐ต โ ( ๐ โ { ๐ฅ } ) = ( ๐ต โ { ๐ฅ } ) ) |
55 |
54
|
fveq2d |
โข ( ๐ = ๐ต โ ( ๐ โ ( ๐ โ { ๐ฅ } ) ) = ( ๐ โ ( ๐ต โ { ๐ฅ } ) ) ) |
56 |
55
|
eleq2d |
โข ( ๐ = ๐ต โ ( ( ๐ฆ ยท ๐ฅ ) โ ( ๐ โ ( ๐ โ { ๐ฅ } ) ) โ ( ๐ฆ ยท ๐ฅ ) โ ( ๐ โ ( ๐ต โ { ๐ฅ } ) ) ) ) |
57 |
56
|
notbid |
โข ( ๐ = ๐ต โ ( ยฌ ( ๐ฆ ยท ๐ฅ ) โ ( ๐ โ ( ๐ โ { ๐ฅ } ) ) โ ยฌ ( ๐ฆ ยท ๐ฅ ) โ ( ๐ โ ( ๐ต โ { ๐ฅ } ) ) ) ) |
58 |
57
|
ralbidv |
โข ( ๐ = ๐ต โ ( โ ๐ฆ โ ( ๐พ โ { 0 } ) ยฌ ( ๐ฆ ยท ๐ฅ ) โ ( ๐ โ ( ๐ โ { ๐ฅ } ) ) โ โ ๐ฆ โ ( ๐พ โ { 0 } ) ยฌ ( ๐ฆ ยท ๐ฅ ) โ ( ๐ โ ( ๐ต โ { ๐ฅ } ) ) ) ) |
59 |
58
|
raleqbi1dv |
โข ( ๐ = ๐ต โ ( โ ๐ฅ โ ๐ โ ๐ฆ โ ( ๐พ โ { 0 } ) ยฌ ( ๐ฆ ยท ๐ฅ ) โ ( ๐ โ ( ๐ โ { ๐ฅ } ) ) โ โ ๐ฅ โ ๐ต โ ๐ฆ โ ( ๐พ โ { 0 } ) ยฌ ( ๐ฆ ยท ๐ฅ ) โ ( ๐ โ ( ๐ต โ { ๐ฅ } ) ) ) ) |
60 |
53 59
|
anbi12d |
โข ( ๐ = ๐ต โ ( ( ( ๐ โ ๐ ) = ๐ โง โ ๐ฅ โ ๐ โ ๐ฆ โ ( ๐พ โ { 0 } ) ยฌ ( ๐ฆ ยท ๐ฅ ) โ ( ๐ โ ( ๐ โ { ๐ฅ } ) ) ) โ ( ( ๐ โ ๐ต ) = ๐ โง โ ๐ฅ โ ๐ต โ ๐ฆ โ ( ๐พ โ { 0 } ) ยฌ ( ๐ฆ ยท ๐ฅ ) โ ( ๐ โ ( ๐ต โ { ๐ฅ } ) ) ) ) ) |
61 |
60
|
elrab |
โข ( ๐ต โ { ๐ โ ๐ซ ๐ โฃ ( ( ๐ โ ๐ ) = ๐ โง โ ๐ฅ โ ๐ โ ๐ฆ โ ( ๐พ โ { 0 } ) ยฌ ( ๐ฆ ยท ๐ฅ ) โ ( ๐ โ ( ๐ โ { ๐ฅ } ) ) ) } โ ( ๐ต โ ๐ซ ๐ โง ( ( ๐ โ ๐ต ) = ๐ โง โ ๐ฅ โ ๐ต โ ๐ฆ โ ( ๐พ โ { 0 } ) ยฌ ( ๐ฆ ยท ๐ฅ ) โ ( ๐ โ ( ๐ต โ { ๐ฅ } ) ) ) ) ) |
62 |
|
3anass |
โข ( ( ๐ต โ ๐ โง ( ๐ โ ๐ต ) = ๐ โง โ ๐ฅ โ ๐ต โ ๐ฆ โ ( ๐พ โ { 0 } ) ยฌ ( ๐ฆ ยท ๐ฅ ) โ ( ๐ โ ( ๐ต โ { ๐ฅ } ) ) ) โ ( ๐ต โ ๐ โง ( ( ๐ โ ๐ต ) = ๐ โง โ ๐ฅ โ ๐ต โ ๐ฆ โ ( ๐พ โ { 0 } ) ยฌ ( ๐ฆ ยท ๐ฅ ) โ ( ๐ โ ( ๐ต โ { ๐ฅ } ) ) ) ) ) |
63 |
52 61 62
|
3bitr4i |
โข ( ๐ต โ { ๐ โ ๐ซ ๐ โฃ ( ( ๐ โ ๐ ) = ๐ โง โ ๐ฅ โ ๐ โ ๐ฆ โ ( ๐พ โ { 0 } ) ยฌ ( ๐ฆ ยท ๐ฅ ) โ ( ๐ โ ( ๐ โ { ๐ฅ } ) ) ) } โ ( ๐ต โ ๐ โง ( ๐ โ ๐ต ) = ๐ โง โ ๐ฅ โ ๐ต โ ๐ฆ โ ( ๐พ โ { 0 } ) ยฌ ( ๐ฆ ยท ๐ฅ ) โ ( ๐ โ ( ๐ต โ { ๐ฅ } ) ) ) ) |
64 |
50 63
|
bitrdi |
โข ( ๐ โ ๐ โ ( ๐ต โ ๐ฝ โ ( ๐ต โ ๐ โง ( ๐ โ ๐ต ) = ๐ โง โ ๐ฅ โ ๐ต โ ๐ฆ โ ( ๐พ โ { 0 } ) ยฌ ( ๐ฆ ยท ๐ฅ ) โ ( ๐ โ ( ๐ต โ { ๐ฅ } ) ) ) ) ) |