Metamath Proof Explorer

Theorem islinds4

Description: A set is independent in a vector space iff it is a subset of some basis. This is an axiom of choice equivalent. (Contributed by Stefan O'Rear, 24-Feb-2015)

Ref Expression
Hypothesis islinds4.j 
|- J = ( LBasis ` W )
Assertion islinds4 
|- ( W e. LVec -> ( Y e. ( LIndS ` W ) <-> E. b e. J Y C_ b ) )

Proof

Step Hyp Ref Expression
1 islinds4.j 
 |-  J = ( LBasis ` W )
2 simpl 
 |-  ( ( W e. LVec /\ Y e. ( LIndS ` W ) ) -> W e. LVec )
3 eqid 
 |-  ( Base ` W ) = ( Base ` W )
4 3 linds1 
 |-  ( Y e. ( LIndS ` W ) -> Y C_ ( Base ` W ) )
5 4 adantl 
 |-  ( ( W e. LVec /\ Y e. ( LIndS ` W ) ) -> Y C_ ( Base ` W ) )
6 lveclmod 
 |-  ( W e. LVec -> W e. LMod )
7 6 ad2antrr 
 |-  ( ( ( W e. LVec /\ Y e. ( LIndS ` W ) ) /\ x e. Y ) -> W e. LMod )
8 eqid 
 |-  ( Scalar ` W ) = ( Scalar ` W )
9 8 lvecdrng 
 |-  ( W e. LVec -> ( Scalar ` W ) e. DivRing )
10 drngnzr 
 |-  ( ( Scalar ` W ) e. DivRing -> ( Scalar ` W ) e. NzRing )
11 9 10 syl 
 |-  ( W e. LVec -> ( Scalar ` W ) e. NzRing )
12 11 ad2antrr 
 |-  ( ( ( W e. LVec /\ Y e. ( LIndS ` W ) ) /\ x e. Y ) -> ( Scalar ` W ) e. NzRing )
13 simplr 
 |-  ( ( ( W e. LVec /\ Y e. ( LIndS ` W ) ) /\ x e. Y ) -> Y e. ( LIndS ` W ) )
14 simpr 
 |-  ( ( ( W e. LVec /\ Y e. ( LIndS ` W ) ) /\ x e. Y ) -> x e. Y )
15 eqid 
 |-  ( LSpan ` W ) = ( LSpan ` W )
16 15 8 lindsind2 
 |-  ( ( ( W e. LMod /\ ( Scalar ` W ) e. NzRing ) /\ Y e. ( LIndS ` W ) /\ x e. Y ) -> -. x e. ( ( LSpan ` W ) ` ( Y \ { x } ) ) )
17 7 12 13 14 16 syl211anc 
 |-  ( ( ( W e. LVec /\ Y e. ( LIndS ` W ) ) /\ x e. Y ) -> -. x e. ( ( LSpan ` W ) ` ( Y \ { x } ) ) )
18 17 ralrimiva 
 |-  ( ( W e. LVec /\ Y e. ( LIndS ` W ) ) -> A. x e. Y -. x e. ( ( LSpan ` W ) ` ( Y \ { x } ) ) )
19 1 3 15 lbsext 
 |-  ( ( W e. LVec /\ Y C_ ( Base ` W ) /\ A. x e. Y -. x e. ( ( LSpan ` W ) ` ( Y \ { x } ) ) ) -> E. b e. J Y C_ b )
20 2 5 18 19 syl3anc 
 |-  ( ( W e. LVec /\ Y e. ( LIndS ` W ) ) -> E. b e. J Y C_ b )
21 20 ex 
 |-  ( W e. LVec -> ( Y e. ( LIndS ` W ) -> E. b e. J Y C_ b ) )
22 6 ad2antrr 
 |-  ( ( ( W e. LVec /\ b e. J ) /\ Y C_ b ) -> W e. LMod )
23 1 lbslinds 
 |-  J C_ ( LIndS ` W )
24 23 sseli 
 |-  ( b e. J -> b e. ( LIndS ` W ) )
25 24 ad2antlr 
 |-  ( ( ( W e. LVec /\ b e. J ) /\ Y C_ b ) -> b e. ( LIndS ` W ) )
26 simpr 
 |-  ( ( ( W e. LVec /\ b e. J ) /\ Y C_ b ) -> Y C_ b )
27 lindsss 
 |-  ( ( W e. LMod /\ b e. ( LIndS ` W ) /\ Y C_ b ) -> Y e. ( LIndS ` W ) )
28 22 25 26 27 syl3anc 
 |-  ( ( ( W e. LVec /\ b e. J ) /\ Y C_ b ) -> Y e. ( LIndS ` W ) )
29 28 rexlimdva2 
 |-  ( W e. LVec -> ( E. b e. J Y C_ b -> Y e. ( LIndS ` W ) ) )
30 21 29 impbid 
 |-  ( W e. LVec -> ( Y e. ( LIndS ` W ) <-> E. b e. J Y C_ b ) )