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 J X 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 LBasis W W V
5 4 2 eleq2s X J W V
6 elfvex X LIndS W W V
7 6 adantr X LIndS W K X = B W V
8 eqid Scalar W = Scalar W
9 eqid W = W
10 eqid Base Scalar W = Base Scalar W
11 eqid 0 Scalar W = 0 Scalar W
12 1 8 9 10 2 3 11 islbs W V X J X B K X = B x X k Base Scalar W 0 Scalar W ¬ k W x K X x
13 3anan32 X B K X = B x X k Base Scalar W 0 Scalar W ¬ k W x K X x X B x X k Base Scalar W 0 Scalar W ¬ k W x K X x K X = B
14 1 9 3 8 10 11 islinds2 W V X LIndS W X B x X k Base Scalar W 0 Scalar W ¬ k W x K X x
15 14 anbi1d W V X LIndS W K X = B X B x X k Base Scalar W 0 Scalar W ¬ k W x K X x K X = B
16 13 15 bitr4id W V X B K X = B x X k Base Scalar W 0 Scalar W ¬ k W x K X x X LIndS W K X = B
17 12 16 bitrd W V X J X LIndS W K X = B
18 5 7 17 pm5.21nii X J X LIndS W K X = B