Metamath Proof Explorer

Theorem islbs4

Description: A basis is an independent spanning set. This could have been used as alternative definition of a basis: LBasis = ( w e. _V |-> { b e. ~P ( Basew ) | ( ( ( LSpanw ) ` `b ) = ( Basew ) /\ b e. ( LIndSw ) ) } ) . (Contributed by Stefan O'Rear, 24-Feb-2015)

Ref Expression
Hypotheses islbs4.b 
|- B = ( Base ` W )
islbs4.j 
|- J = ( LBasis ` W )
islbs4.k 
|- K = ( LSpan ` W )
Assertion islbs4 
|- ( X e. J <-> ( X e. ( LIndS ` W ) /\ ( K ` X ) = B ) )

Proof

Step Hyp Ref Expression
1 islbs4.b 
 |-  B = ( Base ` W )
2 islbs4.j 
 |-  J = ( LBasis ` W )
3 islbs4.k 
 |-  K = ( LSpan ` W )
4 elfvex 
 |-  ( X e. ( LBasis ` W ) -> W e. _V )
5 4 2 eleq2s 
 |-  ( X e. J -> W e. _V )
6 elfvex 
 |-  ( X e. ( LIndS ` W ) -> W e. _V )
7 6 adantr 
 |-  ( ( X e. ( LIndS ` W ) /\ ( K ` X ) = B ) -> W e. _V )
8 eqid 
 |-  ( Scalar ` W ) = ( Scalar ` W )
9 eqid 
 |-  ( .s ` W ) = ( .s ` W )
10 eqid 
 |-  ( Base ` ( Scalar ` W ) ) = ( Base ` ( Scalar ` W ) )
11 eqid 
 |-  ( 0g ` ( Scalar ` W ) ) = ( 0g ` ( Scalar ` W ) )
12 1 8 9 10 2 3 11 islbs 
 |-  ( W e. _V -> ( X e. J <-> ( X C_ B /\ ( K ` X ) = B /\ A. x e. X A. k e. ( ( Base ` ( Scalar ` W ) ) \ { ( 0g ` ( Scalar ` W ) ) } ) -. ( k ( .s ` W ) x ) e. ( K ` ( X \ { x } ) ) ) ) )
13 3anan32 
 |-  ( ( X C_ B /\ ( K ` X ) = B /\ A. x e. X A. k e. ( ( Base ` ( Scalar ` W ) ) \ { ( 0g ` ( Scalar ` W ) ) } ) -. ( k ( .s ` W ) x ) e. ( K ` ( X \ { x } ) ) ) <-> ( ( X C_ B /\ A. x e. X A. k e. ( ( Base ` ( Scalar ` W ) ) \ { ( 0g ` ( Scalar ` W ) ) } ) -. ( k ( .s ` W ) x ) e. ( K ` ( X \ { x } ) ) ) /\ ( K ` X ) = B ) )
14 1 9 3 8 10 11 islinds2 
 |-  ( W e. _V -> ( X e. ( LIndS ` W ) <-> ( X C_ B /\ A. x e. X A. k e. ( ( Base ` ( Scalar ` W ) ) \ { ( 0g ` ( Scalar ` W ) ) } ) -. ( k ( .s ` W ) x ) e. ( K ` ( X \ { x } ) ) ) ) )
15 14 anbi1d 
 |-  ( W e. _V -> ( ( X e. ( LIndS ` W ) /\ ( K ` X ) = B ) <-> ( ( X C_ B /\ A. x e. X A. k e. ( ( Base ` ( Scalar ` W ) ) \ { ( 0g ` ( Scalar ` W ) ) } ) -. ( k ( .s ` W ) x ) e. ( K ` ( X \ { x } ) ) ) /\ ( K ` X ) = B ) ) )
16 13 15 bitr4id 
 |-  ( W e. _V -> ( ( X C_ B /\ ( K ` X ) = B /\ A. x e. X A. k e. ( ( Base ` ( Scalar ` W ) ) \ { ( 0g ` ( Scalar ` W ) ) } ) -. ( k ( .s ` W ) x ) e. ( K ` ( X \ { x } ) ) ) <-> ( X e. ( LIndS ` W ) /\ ( K ` X ) = B ) ) )
17 12 16 bitrd 
 |-  ( W e. _V -> ( X e. J <-> ( X e. ( LIndS ` W ) /\ ( K ` X ) = B ) ) )
18 5 7 17 pm5.21nii 
 |-  ( X e. J <-> ( X e. ( LIndS ` W ) /\ ( K ` X ) = B ) )