Metamath Proof Explorer

Theorem islbs

Description: The predicate " B is a basis for the left module or vector space W ". A subset of the base set is a basis if zero is not in the set, it spans the set, and no nonzero multiple of an element of the basis is in the span of the rest of the family. (Contributed by Mario Carneiro, 24-Jun-2014) (Revised by Mario Carneiro, 14-Jan-2015)

Ref Expression
Hypotheses islbs.v 
|- V = ( Base ` W )
islbs.f 
|- F = ( Scalar ` W )
islbs.s 
|- .x. = ( .s ` W )
islbs.k 
|- K = ( Base ` F )
islbs.j 
|- J = ( LBasis ` W )
islbs.n 
|- N = ( LSpan ` W )
islbs.z 
|- .0. = ( 0g ` F )
Assertion islbs 
|- ( W e. X -> ( B e. J <-> ( B C_ V /\ ( N ` B ) = V /\ A. x e. B A. y e. ( K \ { .0. } ) -. ( y .x. x ) e. ( N ` ( B \ { x } ) ) ) ) )

Proof

Step Hyp Ref Expression
1 islbs.v 
 |-  V = ( Base ` W )
2 islbs.f 
 |-  F = ( Scalar ` W )
3 islbs.s 
 |-  .x. = ( .s ` W )
4 islbs.k 
 |-  K = ( Base ` F )
5 islbs.j 
 |-  J = ( LBasis ` W )
6 islbs.n 
 |-  N = ( LSpan ` W )
7 islbs.z 
 |-  .0. = ( 0g ` F )
8 elex 
 |-  ( W e. X -> W e. _V )
9 fveq2 
 |-  ( w = W -> ( Base ` w ) = ( Base ` W ) )
10 9 1 eqtr4di 
 |-  ( w = W -> ( Base ` w ) = V )
11 10 pweqd 
 |-  ( w = W -> ~P ( Base ` w ) = ~P V )
12 fvexd 
 |-  ( w = W -> ( LSpan ` w ) e. _V )
13 fveq2 
 |-  ( w = W -> ( LSpan ` w ) = ( LSpan ` W ) )
14 13 6 eqtr4di 
 |-  ( w = W -> ( LSpan ` w ) = N )
15 fvexd 
 |-  ( ( w = W /\ n = N ) -> ( Scalar ` w ) e. _V )
16 fveq2 
 |-  ( w = W -> ( Scalar ` w ) = ( Scalar ` W ) )
17 16 adantr 
 |-  ( ( w = W /\ n = N ) -> ( Scalar ` w ) = ( Scalar ` W ) )
18 17 2 eqtr4di 
 |-  ( ( w = W /\ n = N ) -> ( Scalar ` w ) = F )
19 simplr 
 |-  ( ( ( w = W /\ n = N ) /\ f = F ) -> n = N )
20 19 fveq1d 
 |-  ( ( ( w = W /\ n = N ) /\ f = F ) -> ( n ` b ) = ( N ` b ) )
21 10 ad2antrr 
 |-  ( ( ( w = W /\ n = N ) /\ f = F ) -> ( Base ` w ) = V )
22 20 21 eqeq12d 
 |-  ( ( ( w = W /\ n = N ) /\ f = F ) -> ( ( n ` b ) = ( Base ` w ) <-> ( N ` b ) = V ) )
23 simpr 
 |-  ( ( ( w = W /\ n = N ) /\ f = F ) -> f = F )
24 23 fveq2d 
 |-  ( ( ( w = W /\ n = N ) /\ f = F ) -> ( Base ` f ) = ( Base ` F ) )
25 24 4 eqtr4di 
 |-  ( ( ( w = W /\ n = N ) /\ f = F ) -> ( Base ` f ) = K )
26 23 fveq2d 
 |-  ( ( ( w = W /\ n = N ) /\ f = F ) -> ( 0g ` f ) = ( 0g ` F ) )
27 26 7 eqtr4di 
 |-  ( ( ( w = W /\ n = N ) /\ f = F ) -> ( 0g ` f ) = .0. )
28 27 sneqd 
 |-  ( ( ( w = W /\ n = N ) /\ f = F ) -> { ( 0g ` f ) } = { .0. } )
29 25 28 difeq12d 
 |-  ( ( ( w = W /\ n = N ) /\ f = F ) -> ( ( Base ` f ) \ { ( 0g ` f ) } ) = ( K \ { .0. } ) )
30 fveq2 
 |-  ( w = W -> ( .s ` w ) = ( .s ` W ) )
31 30 3 eqtr4di 
 |-  ( w = W -> ( .s ` w ) = .x. )
32 31 ad2antrr 
 |-  ( ( ( w = W /\ n = N ) /\ f = F ) -> ( .s ` w ) = .x. )
33 32 oveqd 
 |-  ( ( ( w = W /\ n = N ) /\ f = F ) -> ( y ( .s ` w ) x ) = ( y .x. x ) )
34 19 fveq1d 
 |-  ( ( ( w = W /\ n = N ) /\ f = F ) -> ( n ` ( b \ { x } ) ) = ( N ` ( b \ { x } ) ) )
35 33 34 eleq12d 
 |-  ( ( ( w = W /\ n = N ) /\ f = F ) -> ( ( y ( .s ` w ) x ) e. ( n ` ( b \ { x } ) ) <-> ( y .x. x ) e. ( N ` ( b \ { x } ) ) ) )
36 35 notbid 
 |-  ( ( ( w = W /\ n = N ) /\ f = F ) -> ( -. ( y ( .s ` w ) x ) e. ( n ` ( b \ { x } ) ) <-> -. ( y .x. x ) e. ( N ` ( b \ { x } ) ) ) )
37 29 36 raleqbidv 
 |-  ( ( ( w = W /\ n = N ) /\ f = F ) -> ( A. y e. ( ( Base ` f ) \ { ( 0g ` f ) } ) -. ( y ( .s ` w ) x ) e. ( n ` ( b \ { x } ) ) <-> A. y e. ( K \ { .0. } ) -. ( y .x. x ) e. ( N ` ( b \ { x } ) ) ) )
38 37 ralbidv 
 |-  ( ( ( w = W /\ n = N ) /\ f = F ) -> ( A. x e. b A. y e. ( ( Base ` f ) \ { ( 0g ` f ) } ) -. ( y ( .s ` w ) x ) e. ( n ` ( b \ { x } ) ) <-> A. x e. b A. y e. ( K \ { .0. } ) -. ( y .x. x ) e. ( N ` ( b \ { x } ) ) ) )
39 22 38 anbi12d 
 |-  ( ( ( w = W /\ n = N ) /\ f = F ) -> ( ( ( n ` b ) = ( Base ` w ) /\ A. x e. b A. y e. ( ( Base ` f ) \ { ( 0g ` f ) } ) -. ( y ( .s ` w ) x ) e. ( n ` ( b \ { x } ) ) ) <-> ( ( N ` b ) = V /\ A. x e. b A. y e. ( K \ { .0. } ) -. ( y .x. x ) e. ( N ` ( b \ { x } ) ) ) ) )
40 15 18 39 sbcied2 
 |-  ( ( w = W /\ n = N ) -> ( [. ( Scalar ` w ) / f ]. ( ( n ` b ) = ( Base ` w ) /\ A. x e. b A. y e. ( ( Base ` f ) \ { ( 0g ` f ) } ) -. ( y ( .s ` w ) x ) e. ( n ` ( b \ { x } ) ) ) <-> ( ( N ` b ) = V /\ A. x e. b A. y e. ( K \ { .0. } ) -. ( y .x. x ) e. ( N ` ( b \ { x } ) ) ) ) )
41 12 14 40 sbcied2 
 |-  ( w = W -> ( [. ( LSpan ` w ) / n ]. [. ( Scalar ` w ) / f ]. ( ( n ` b ) = ( Base ` w ) /\ A. x e. b A. y e. ( ( Base ` f ) \ { ( 0g ` f ) } ) -. ( y ( .s ` w ) x ) e. ( n ` ( b \ { x } ) ) ) <-> ( ( N ` b ) = V /\ A. x e. b A. y e. ( K \ { .0. } ) -. ( y .x. x ) e. ( N ` ( b \ { x } ) ) ) ) )
42 11 41 rabeqbidv 
 |-  ( w = W -> { b e. ~P ( Base ` w ) | [. ( LSpan ` w ) / n ]. [. ( Scalar ` w ) / f ]. ( ( n ` b ) = ( Base ` w ) /\ A. x e. b A. y e. ( ( Base ` f ) \ { ( 0g ` f ) } ) -. ( y ( .s ` w ) x ) e. ( n ` ( b \ { x } ) ) ) } = { b e. ~P V | ( ( N ` b ) = V /\ A. x e. b A. y e. ( K \ { .0. } ) -. ( y .x. x ) e. ( N ` ( b \ { x } ) ) ) } )
43 df-lbs 
 |-  LBasis = ( w e. _V |-> { b e. ~P ( Base ` w ) | [. ( LSpan ` w ) / n ]. [. ( Scalar ` w ) / f ]. ( ( n ` b ) = ( Base ` w ) /\ A. x e. b A. y e. ( ( Base ` f ) \ { ( 0g ` f ) } ) -. ( y ( .s ` w ) x ) e. ( n ` ( b \ { x } ) ) ) } )
44 1 fvexi 
 |-  V e. _V
45 44 pwex 
 |-  ~P V e. _V
46 45 rabex 
 |-  { b e. ~P V | ( ( N ` b ) = V /\ A. x e. b A. y e. ( K \ { .0. } ) -. ( y .x. x ) e. ( N ` ( b \ { x } ) ) ) } e. _V
47 42 43 46 fvmpt 
 |-  ( W e. _V -> ( LBasis ` W ) = { b e. ~P V | ( ( N ` b ) = V /\ A. x e. b A. y e. ( K \ { .0. } ) -. ( y .x. x ) e. ( N ` ( b \ { x } ) ) ) } )
48 5 47 eqtrid 
 |-  ( W e. _V -> J = { b e. ~P V | ( ( N ` b ) = V /\ A. x e. b A. y e. ( K \ { .0. } ) -. ( y .x. x ) e. ( N ` ( b \ { x } ) ) ) } )
49 8 48 syl 
 |-  ( W e. X -> J = { b e. ~P V | ( ( N ` b ) = V /\ A. x e. b A. y e. ( K \ { .0. } ) -. ( y .x. x ) e. ( N ` ( b \ { x } ) ) ) } )
50 49 eleq2d 
 |-  ( W e. X -> ( B e. J <-> B e. { b e. ~P V | ( ( N ` b ) = V /\ A. x e. b A. y e. ( K \ { .0. } ) -. ( y .x. x ) e. ( N ` ( b \ { x } ) ) ) } ) )
51 44 elpw2 
 |-  ( B e. ~P V <-> B C_ V )
52 51 anbi1i 
 |-  ( ( B e. ~P V /\ ( ( N ` B ) = V /\ A. x e. B A. y e. ( K \ { .0. } ) -. ( y .x. x ) e. ( N ` ( B \ { x } ) ) ) ) <-> ( B C_ V /\ ( ( N ` B ) = V /\ A. x e. B A. y e. ( K \ { .0. } ) -. ( y .x. x ) e. ( N ` ( B \ { x } ) ) ) ) )
53 fveqeq2 
 |-  ( b = B -> ( ( N ` b ) = V <-> ( N ` B ) = V ) )
54 difeq1 
 |-  ( b = B -> ( b \ { x } ) = ( B \ { x } ) )
55 54 fveq2d 
 |-  ( b = B -> ( N ` ( b \ { x } ) ) = ( N ` ( B \ { x } ) ) )
56 55 eleq2d 
 |-  ( b = B -> ( ( y .x. x ) e. ( N ` ( b \ { x } ) ) <-> ( y .x. x ) e. ( N ` ( B \ { x } ) ) ) )
57 56 notbid 
 |-  ( b = B -> ( -. ( y .x. x ) e. ( N ` ( b \ { x } ) ) <-> -. ( y .x. x ) e. ( N ` ( B \ { x } ) ) ) )
58 57 ralbidv 
 |-  ( b = B -> ( A. y e. ( K \ { .0. } ) -. ( y .x. x ) e. ( N ` ( b \ { x } ) ) <-> A. y e. ( K \ { .0. } ) -. ( y .x. x ) e. ( N ` ( B \ { x } ) ) ) )
59 58 raleqbi1dv 
 |-  ( b = B -> ( A. x e. b A. y e. ( K \ { .0. } ) -. ( y .x. x ) e. ( N ` ( b \ { x } ) ) <-> A. x e. B A. y e. ( K \ { .0. } ) -. ( y .x. x ) e. ( N ` ( B \ { x } ) ) ) )
60 53 59 anbi12d 
 |-  ( b = B -> ( ( ( N ` b ) = V /\ A. x e. b A. y e. ( K \ { .0. } ) -. ( y .x. x ) e. ( N ` ( b \ { x } ) ) ) <-> ( ( N ` B ) = V /\ A. x e. B A. y e. ( K \ { .0. } ) -. ( y .x. x ) e. ( N ` ( B \ { x } ) ) ) ) )
61 60 elrab 
 |-  ( B e. { b e. ~P V | ( ( N ` b ) = V /\ A. x e. b A. y e. ( K \ { .0. } ) -. ( y .x. x ) e. ( N ` ( b \ { x } ) ) ) } <-> ( B e. ~P V /\ ( ( N ` B ) = V /\ A. x e. B A. y e. ( K \ { .0. } ) -. ( y .x. x ) e. ( N ` ( B \ { x } ) ) ) ) )
62 3anass 
 |-  ( ( B C_ V /\ ( N ` B ) = V /\ A. x e. B A. y e. ( K \ { .0. } ) -. ( y .x. x ) e. ( N ` ( B \ { x } ) ) ) <-> ( B C_ V /\ ( ( N ` B ) = V /\ A. x e. B A. y e. ( K \ { .0. } ) -. ( y .x. x ) e. ( N ` ( B \ { x } ) ) ) ) )
63 52 61 62 3bitr4i 
 |-  ( B e. { b e. ~P V | ( ( N ` b ) = V /\ A. x e. b A. y e. ( K \ { .0. } ) -. ( y .x. x ) e. ( N ` ( b \ { x } ) ) ) } <-> ( B C_ V /\ ( N ` B ) = V /\ A. x e. B A. y e. ( K \ { .0. } ) -. ( y .x. x ) e. ( N ` ( B \ { x } ) ) ) )
64 50 63 bitrdi 
 |-  ( W e. X -> ( B e. J <-> ( B C_ V /\ ( N ` B ) = V /\ A. x e. B A. y e. ( K \ { .0. } ) -. ( y .x. x ) e. ( N ` ( B \ { x } ) ) ) ) )