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 𝑠 K Y
islinds3.j J = LBasis X
Assertion islinds3 W LMod Y LIndS W Y J

Proof

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