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 ⊢ 𝐵 = ( Base ‘ 𝑊 )
islbs4.j ⊢ 𝐽 = ( LBasis ‘ 𝑊 )
islbs4.k ⊢ 𝐾 = ( LSpan ‘ 𝑊 )
Assertion islbs4 ( 𝑋 ∈ 𝐽 ↔ ( 𝑋 ∈ ( LIndS ‘ 𝑊 ) ∧ ( 𝐾 ‘ 𝑋 ) = 𝐵 ) )

Proof

Step Hyp Ref Expression
1 islbs4.b ⊢ 𝐵 = ( Base ‘ 𝑊 )
2 islbs4.j ⊢ 𝐽 = ( LBasis ‘ 𝑊 )
3 islbs4.k ⊢ 𝐾 = ( LSpan ‘ 𝑊 )
4 elfvex ⊢ ( 𝑋 ∈ ( LBasis ‘ 𝑊 ) → 𝑊 ∈ V )
5 4 2 eleq2s ⊢ ( 𝑋 ∈ 𝐽 → 𝑊 ∈ V )
6 elfvex ⊢ ( 𝑋 ∈ ( LIndS ‘ 𝑊 ) → 𝑊 ∈ V )
7 6 adantr ⊢ ( ( 𝑋 ∈ ( LIndS ‘ 𝑊 ) ∧ ( 𝐾 ‘ 𝑋 ) = 𝐵 ) → 𝑊 ∈ V )
8 eqid ⊢ ( Scalar ‘ 𝑊 ) = ( Scalar ‘ 𝑊 )
9 eqid ⊢ ( ·𝑠 ‘ 𝑊 ) = ( ·𝑠 ‘ 𝑊 )
10 eqid ⊢ ( Base ‘ ( Scalar ‘ 𝑊 ) ) = ( Base ‘ ( Scalar ‘ 𝑊 ) )
11 eqid ⊢ ( 0g ‘ ( Scalar ‘ 𝑊 ) ) = ( 0g ‘ ( Scalar ‘ 𝑊 ) )
12 1 8 9 10 2 3 11 islbs ⊢ ( 𝑊 ∈ V → ( 𝑋 ∈ 𝐽 ↔ ( 𝑋 ⊆ 𝐵 ∧ ( 𝐾 ‘ 𝑋 ) = 𝐵 ∧ ∀ 𝑥 ∈ 𝑋 ∀ 𝑘 ∈ ( ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∖ { ( 0g ‘ ( Scalar ‘ 𝑊 ) ) } ) ¬ ( 𝑘 ( ·𝑠 ‘ 𝑊 ) 𝑥 ) ∈ ( 𝐾 ‘ ( 𝑋 ∖ { 𝑥 } ) ) ) ) )
13 3anan32 ⊢ ( ( 𝑋 ⊆ 𝐵 ∧ ( 𝐾 ‘ 𝑋 ) = 𝐵 ∧ ∀ 𝑥 ∈ 𝑋 ∀ 𝑘 ∈ ( ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∖ { ( 0g ‘ ( Scalar ‘ 𝑊 ) ) } ) ¬ ( 𝑘 ( ·𝑠 ‘ 𝑊 ) 𝑥 ) ∈ ( 𝐾 ‘ ( 𝑋 ∖ { 𝑥 } ) ) ) ↔ ( ( 𝑋 ⊆ 𝐵 ∧ ∀ 𝑥 ∈ 𝑋 ∀ 𝑘 ∈ ( ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∖ { ( 0g ‘ ( Scalar ‘ 𝑊 ) ) } ) ¬ ( 𝑘 ( ·𝑠 ‘ 𝑊 ) 𝑥 ) ∈ ( 𝐾 ‘ ( 𝑋 ∖ { 𝑥 } ) ) ) ∧ ( 𝐾 ‘ 𝑋 ) = 𝐵 ) )
14 1 9 3 8 10 11 islinds2 ⊢ ( 𝑊 ∈ V → ( 𝑋 ∈ ( LIndS ‘ 𝑊 ) ↔ ( 𝑋 ⊆ 𝐵 ∧ ∀ 𝑥 ∈ 𝑋 ∀ 𝑘 ∈ ( ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∖ { ( 0g ‘ ( Scalar ‘ 𝑊 ) ) } ) ¬ ( 𝑘 ( ·𝑠 ‘ 𝑊 ) 𝑥 ) ∈ ( 𝐾 ‘ ( 𝑋 ∖ { 𝑥 } ) ) ) ) )
15 14 anbi1d ⊢ ( 𝑊 ∈ V → ( ( 𝑋 ∈ ( LIndS ‘ 𝑊 ) ∧ ( 𝐾 ‘ 𝑋 ) = 𝐵 ) ↔ ( ( 𝑋 ⊆ 𝐵 ∧ ∀ 𝑥 ∈ 𝑋 ∀ 𝑘 ∈ ( ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∖ { ( 0g ‘ ( Scalar ‘ 𝑊 ) ) } ) ¬ ( 𝑘 ( ·𝑠 ‘ 𝑊 ) 𝑥 ) ∈ ( 𝐾 ‘ ( 𝑋 ∖ { 𝑥 } ) ) ) ∧ ( 𝐾 ‘ 𝑋 ) = 𝐵 ) ) )
16 13 15 bitr4id ⊢ ( 𝑊 ∈ V → ( ( 𝑋 ⊆ 𝐵 ∧ ( 𝐾 ‘ 𝑋 ) = 𝐵 ∧ ∀ 𝑥 ∈ 𝑋 ∀ 𝑘 ∈ ( ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∖ { ( 0g ‘ ( Scalar ‘ 𝑊 ) ) } ) ¬ ( 𝑘 ( ·𝑠 ‘ 𝑊 ) 𝑥 ) ∈ ( 𝐾 ‘ ( 𝑋 ∖ { 𝑥 } ) ) ) ↔ ( 𝑋 ∈ ( LIndS ‘ 𝑊 ) ∧ ( 𝐾 ‘ 𝑋 ) = 𝐵 ) ) )
17 12 16 bitrd ⊢ ( 𝑊 ∈ V → ( 𝑋 ∈ 𝐽 ↔ ( 𝑋 ∈ ( LIndS ‘ 𝑊 ) ∧ ( 𝐾 ‘ 𝑋 ) = 𝐵 ) ) )
18 5 7 17 pm5.21nii ⊢ ( 𝑋 ∈ 𝐽 ↔ ( 𝑋 ∈ ( LIndS ‘ 𝑊 ) ∧ ( 𝐾 ‘ 𝑋 ) = 𝐵 ) )