Metamath Proof Explorer

Theorem islinds3

Description: A subset is linearly independent iff it is a basis of its span. (Contributed by Stefan O'Rear, 25-Feb-2015)

Ref Expression
Hypotheses islinds3.b 
|- B = ( Base ` W )
islinds3.k 
|- K = ( LSpan ` W )
islinds3.x 
|- X = ( W |`s ( K ` Y ) )
islinds3.j 
|- J = ( LBasis ` X )
Assertion islinds3 
|- ( W e. LMod -> ( Y e. ( LIndS ` W ) <-> Y e. J ) )

Proof

Step Hyp Ref Expression
1 islinds3.b 
 |-  B = ( Base ` W )
2 islinds3.k 
 |-  K = ( LSpan ` W )
3 islinds3.x 
 |-  X = ( W |`s ( K ` Y ) )
4 islinds3.j 
 |-  J = ( LBasis ` X )
5 1 linds1 
 |-  ( Y e. ( LIndS ` W ) -> Y C_ B )
6 5 a1i 
 |-  ( W e. LMod -> ( Y e. ( LIndS ` W ) -> Y C_ B ) )
7 eqid 
 |-  ( Base ` X ) = ( Base ` X )
8 7 linds1 
 |-  ( Y e. ( LIndS ` X ) -> Y C_ ( Base ` X ) )
9 3 1 ressbasss 
 |-  ( Base ` X ) C_ B
10 8 9 sstrdi 
 |-  ( Y e. ( LIndS ` X ) -> Y C_ B )
11 10 adantr 
 |-  ( ( Y e. ( LIndS ` X ) /\ ( ( LSpan ` X ) ` Y ) = ( Base ` X ) ) -> Y C_ B )
12 11 a1i 
 |-  ( W e. LMod -> ( ( Y e. ( LIndS ` X ) /\ ( ( LSpan ` X ) ` Y ) = ( Base ` X ) ) -> Y C_ B ) )
13 simpl 
 |-  ( ( W e. LMod /\ Y C_ B ) -> W e. LMod )
14 eqid 
 |-  ( LSubSp ` W ) = ( LSubSp ` W )
15 1 14 2 lspcl 
 |-  ( ( W e. LMod /\ Y C_ B ) -> ( K ` Y ) e. ( LSubSp ` W ) )
16 1 2 lspssid 
 |-  ( ( W e. LMod /\ Y C_ B ) -> Y C_ ( K ` Y ) )
17 eqid 
 |-  ( LSpan ` X ) = ( LSpan ` X )
18 3 2 17 14 lsslsp 
 |-  ( ( W e. LMod /\ ( K ` Y ) e. ( LSubSp ` W ) /\ Y C_ ( K ` Y ) ) -> ( K ` Y ) = ( ( LSpan ` X ) ` Y ) )
19 13 15 16 18 syl3anc 
 |-  ( ( W e. LMod /\ Y C_ B ) -> ( K ` Y ) = ( ( LSpan ` X ) ` Y ) )
20 1 2 lspssv 
 |-  ( ( W e. LMod /\ Y C_ B ) -> ( K ` Y ) C_ B )
21 3 1 ressbas2 
 |-  ( ( K ` Y ) C_ B -> ( K ` Y ) = ( Base ` X ) )
22 20 21 syl 
 |-  ( ( W e. LMod /\ Y C_ B ) -> ( K ` Y ) = ( Base ` X ) )
23 19 22 eqtr3d 
 |-  ( ( W e. LMod /\ Y C_ B ) -> ( ( LSpan ` X ) ` Y ) = ( Base ` X ) )
24 23 biantrud 
 |-  ( ( W e. LMod /\ Y C_ B ) -> ( Y e. ( LIndS ` W ) <-> ( Y e. ( LIndS ` W ) /\ ( ( LSpan ` X ) ` Y ) = ( Base ` X ) ) ) )
25 14 3 lsslinds 
 |-  ( ( W e. LMod /\ ( K ` Y ) e. ( LSubSp ` W ) /\ Y C_ ( K ` Y ) ) -> ( Y e. ( LIndS ` X ) <-> Y e. ( LIndS ` W ) ) )
26 13 15 16 25 syl3anc 
 |-  ( ( W e. LMod /\ Y C_ B ) -> ( Y e. ( LIndS ` X ) <-> Y e. ( LIndS ` W ) ) )
27 26 bicomd 
 |-  ( ( W e. LMod /\ Y C_ B ) -> ( Y e. ( LIndS ` W ) <-> Y e. ( LIndS ` X ) ) )
28 27 anbi1d 
 |-  ( ( W e. LMod /\ Y C_ B ) -> ( ( Y e. ( LIndS ` W ) /\ ( ( LSpan ` X ) ` Y ) = ( Base ` X ) ) <-> ( Y e. ( LIndS ` X ) /\ ( ( LSpan ` X ) ` Y ) = ( Base ` X ) ) ) )
29 24 28 bitrd 
 |-  ( ( W e. LMod /\ Y C_ B ) -> ( Y e. ( LIndS ` W ) <-> ( Y e. ( LIndS ` X ) /\ ( ( LSpan ` X ) ` Y ) = ( Base ` X ) ) ) )
30 29 ex 
 |-  ( W e. LMod -> ( Y C_ B -> ( Y e. ( LIndS ` W ) <-> ( Y e. ( LIndS ` X ) /\ ( ( LSpan ` X ) ` Y ) = ( Base ` X ) ) ) ) )
31 6 12 30 pm5.21ndd 
 |-  ( W e. LMod -> ( Y e. ( LIndS ` W ) <-> ( Y e. ( LIndS ` X ) /\ ( ( LSpan ` X ) ` Y ) = ( Base ` X ) ) ) )
32 7 4 17 islbs4 
 |-  ( Y e. J <-> ( Y e. ( LIndS ` X ) /\ ( ( LSpan ` X ) ` Y ) = ( Base ` X ) ) )
33 31 32 bitr4di 
 |-  ( W e. LMod -> ( Y e. ( LIndS ` W ) <-> Y e. J ) )