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=BaseW
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=BaseW
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 ⊢BaseScalar⁡W=BaseScalar⁡W
11 eqid ⊢0Scalar⁡W=0Scalar⁡W
12 1 8 9 10 2 3 11 islbs ⊢W∈V→X∈J↔X⊆B∧K⁡X=B∧∀x∈X∀k∈BaseScalar⁡W∖0Scalar⁡W¬k⋅Wx∈K⁡X∖x
13 3anan32 ⊢X⊆B∧K⁡X=B∧∀x∈X∀k∈BaseScalar⁡W∖0Scalar⁡W¬k⋅Wx∈K⁡X∖x↔X⊆B∧∀x∈X∀k∈BaseScalar⁡W∖0Scalar⁡W¬k⋅Wx∈K⁡X∖x∧K⁡X=B
14 1 9 3 8 10 11 islinds2 ⊢W∈V→X∈LIndS⁡W↔X⊆B∧∀x∈X∀k∈BaseScalar⁡W∖0Scalar⁡W¬k⋅Wx∈K⁡X∖x
15 14 anbi1d ⊢W∈V→X∈LIndS⁡W∧K⁡X=B↔X⊆B∧∀x∈X∀k∈BaseScalar⁡W∖0Scalar⁡W¬k⋅Wx∈K⁡X∖x∧K⁡X=B
16 13 15 bitr4id ⊢W∈V→X⊆B∧K⁡X=B∧∀x∈X∀k∈BaseScalar⁡W∖0Scalar⁡W¬k⋅Wx∈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