Metamath Proof Explorer

Theorem islbs2

Description: An equivalent formulation of the basis predicate in a vector space: a subset is a basis iff no element is in the span of the rest of the set. (Contributed by Mario Carneiro, 14-Jan-2015)

Ref Expression
Hypotheses islbs2.v ⊢ 𝑉 = ( Base ‘ 𝑊 )
islbs2.j ⊢ 𝐽 = ( LBasis ‘ 𝑊 )
islbs2.n ⊢ 𝑁 = ( LSpan ‘ 𝑊 )
Assertion islbs2 ( 𝑊 ∈ LVec → ( 𝐵 ∈ 𝐽 ↔ ( 𝐵 ⊆ 𝑉 ∧ ( 𝑁 ‘ 𝐵 ) = 𝑉 ∧ ∀ 𝑥 ∈ 𝐵 ¬ 𝑥 ∈ ( 𝑁 ‘ ( 𝐵 ∖ { 𝑥 } ) ) ) ) )

Proof

Step Hyp Ref Expression
1 islbs2.v ⊢ 𝑉 = ( Base ‘ 𝑊 )
2 islbs2.j ⊢ 𝐽 = ( LBasis ‘ 𝑊 )
3 islbs2.n ⊢ 𝑁 = ( LSpan ‘ 𝑊 )
4 1 2 lbsss ⊢ ( 𝐵 ∈ 𝐽 → 𝐵 ⊆ 𝑉 )
5 4 adantl ⊢ ( ( 𝑊 ∈ LVec ∧ 𝐵 ∈ 𝐽 ) → 𝐵 ⊆ 𝑉 )
6 1 2 3 lbssp ⊢ ( 𝐵 ∈ 𝐽 → ( 𝑁 ‘ 𝐵 ) = 𝑉 )
7 6 adantl ⊢ ( ( 𝑊 ∈ LVec ∧ 𝐵 ∈ 𝐽 ) → ( 𝑁 ‘ 𝐵 ) = 𝑉 )
8 lveclmod ⊢ ( 𝑊 ∈ LVec → 𝑊 ∈ LMod )
9 eqid ⊢ ( Scalar ‘ 𝑊 ) = ( Scalar ‘ 𝑊 )
10 9 lvecdrng ⊢ ( 𝑊 ∈ LVec → ( Scalar ‘ 𝑊 ) ∈ DivRing )
11 eqid ⊢ ( 0g ‘ ( Scalar ‘ 𝑊 ) ) = ( 0g ‘ ( Scalar ‘ 𝑊 ) )
12 eqid ⊢ ( 1r ‘ ( Scalar ‘ 𝑊 ) ) = ( 1r ‘ ( Scalar ‘ 𝑊 ) )
13 11 12 drngunz ⊢ ( ( Scalar ‘ 𝑊 ) ∈ DivRing → ( 1r ‘ ( Scalar ‘ 𝑊 ) ) ≠ ( 0g ‘ ( Scalar ‘ 𝑊 ) ) )
14 10 13 syl ⊢ ( 𝑊 ∈ LVec → ( 1r ‘ ( Scalar ‘ 𝑊 ) ) ≠ ( 0g ‘ ( Scalar ‘ 𝑊 ) ) )
15 8 14 jca ⊢ ( 𝑊 ∈ LVec → ( 𝑊 ∈ LMod ∧ ( 1r ‘ ( Scalar ‘ 𝑊 ) ) ≠ ( 0g ‘ ( Scalar ‘ 𝑊 ) ) ) )
16 2 3 9 12 11 lbsind2 ⊢ ( ( ( 𝑊 ∈ LMod ∧ ( 1r ‘ ( Scalar ‘ 𝑊 ) ) ≠ ( 0g ‘ ( Scalar ‘ 𝑊 ) ) ) ∧ 𝐵 ∈ 𝐽 ∧ 𝑥 ∈ 𝐵 ) → ¬ 𝑥 ∈ ( 𝑁 ‘ ( 𝐵 ∖ { 𝑥 } ) ) )
17 15 16 syl3an1 ⊢ ( ( 𝑊 ∈ LVec ∧ 𝐵 ∈ 𝐽 ∧ 𝑥 ∈ 𝐵 ) → ¬ 𝑥 ∈ ( 𝑁 ‘ ( 𝐵 ∖ { 𝑥 } ) ) )
18 17 3expa ⊢ ( ( ( 𝑊 ∈ LVec ∧ 𝐵 ∈ 𝐽 ) ∧ 𝑥 ∈ 𝐵 ) → ¬ 𝑥 ∈ ( 𝑁 ‘ ( 𝐵 ∖ { 𝑥 } ) ) )
19 18 ralrimiva ⊢ ( ( 𝑊 ∈ LVec ∧ 𝐵 ∈ 𝐽 ) → ∀ 𝑥 ∈ 𝐵 ¬ 𝑥 ∈ ( 𝑁 ‘ ( 𝐵 ∖ { 𝑥 } ) ) )
20 5 7 19 3jca ⊢ ( ( 𝑊 ∈ LVec ∧ 𝐵 ∈ 𝐽 ) → ( 𝐵 ⊆ 𝑉 ∧ ( 𝑁 ‘ 𝐵 ) = 𝑉 ∧ ∀ 𝑥 ∈ 𝐵 ¬ 𝑥 ∈ ( 𝑁 ‘ ( 𝐵 ∖ { 𝑥 } ) ) ) )
21 simpr1 ⊢ ( ( 𝑊 ∈ LVec ∧ ( 𝐵 ⊆ 𝑉 ∧ ( 𝑁 ‘ 𝐵 ) = 𝑉 ∧ ∀ 𝑥 ∈ 𝐵 ¬ 𝑥 ∈ ( 𝑁 ‘ ( 𝐵 ∖ { 𝑥 } ) ) ) ) → 𝐵 ⊆ 𝑉 )
22 simpr2 ⊢ ( ( 𝑊 ∈ LVec ∧ ( 𝐵 ⊆ 𝑉 ∧ ( 𝑁 ‘ 𝐵 ) = 𝑉 ∧ ∀ 𝑥 ∈ 𝐵 ¬ 𝑥 ∈ ( 𝑁 ‘ ( 𝐵 ∖ { 𝑥 } ) ) ) ) → ( 𝑁 ‘ 𝐵 ) = 𝑉 )
23 id ⊢ ( 𝑥 = 𝑦 → 𝑥 = 𝑦 )
24 sneq ⊢ ( 𝑥 = 𝑦 → { 𝑥 } = { 𝑦 } )
25 24 difeq2d ⊢ ( 𝑥 = 𝑦 → ( 𝐵 ∖ { 𝑥 } ) = ( 𝐵 ∖ { 𝑦 } ) )
26 25 fveq2d ⊢ ( 𝑥 = 𝑦 → ( 𝑁 ‘ ( 𝐵 ∖ { 𝑥 } ) ) = ( 𝑁 ‘ ( 𝐵 ∖ { 𝑦 } ) ) )
27 23 26 eleq12d ⊢ ( 𝑥 = 𝑦 → ( 𝑥 ∈ ( 𝑁 ‘ ( 𝐵 ∖ { 𝑥 } ) ) ↔ 𝑦 ∈ ( 𝑁 ‘ ( 𝐵 ∖ { 𝑦 } ) ) ) )
28 27 notbid ⊢ ( 𝑥 = 𝑦 → ( ¬ 𝑥 ∈ ( 𝑁 ‘ ( 𝐵 ∖ { 𝑥 } ) ) ↔ ¬ 𝑦 ∈ ( 𝑁 ‘ ( 𝐵 ∖ { 𝑦 } ) ) ) )
29 simplr3 ⊢ ( ( ( 𝑊 ∈ LVec ∧ ( 𝐵 ⊆ 𝑉 ∧ ( 𝑁 ‘ 𝐵 ) = 𝑉 ∧ ∀ 𝑥 ∈ 𝐵 ¬ 𝑥 ∈ ( 𝑁 ‘ ( 𝐵 ∖ { 𝑥 } ) ) ) ) ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ ( ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∖ { ( 0g ‘ ( Scalar ‘ 𝑊 ) ) } ) ) ) → ∀ 𝑥 ∈ 𝐵 ¬ 𝑥 ∈ ( 𝑁 ‘ ( 𝐵 ∖ { 𝑥 } ) ) )
30 simprl ⊢ ( ( ( 𝑊 ∈ LVec ∧ ( 𝐵 ⊆ 𝑉 ∧ ( 𝑁 ‘ 𝐵 ) = 𝑉 ∧ ∀ 𝑥 ∈ 𝐵 ¬ 𝑥 ∈ ( 𝑁 ‘ ( 𝐵 ∖ { 𝑥 } ) ) ) ) ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ ( ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∖ { ( 0g ‘ ( Scalar ‘ 𝑊 ) ) } ) ) ) → 𝑦 ∈ 𝐵 )
31 28 29 30 rspcdva ⊢ ( ( ( 𝑊 ∈ LVec ∧ ( 𝐵 ⊆ 𝑉 ∧ ( 𝑁 ‘ 𝐵 ) = 𝑉 ∧ ∀ 𝑥 ∈ 𝐵 ¬ 𝑥 ∈ ( 𝑁 ‘ ( 𝐵 ∖ { 𝑥 } ) ) ) ) ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ ( ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∖ { ( 0g ‘ ( Scalar ‘ 𝑊 ) ) } ) ) ) → ¬ 𝑦 ∈ ( 𝑁 ‘ ( 𝐵 ∖ { 𝑦 } ) ) )
32 simpll ⊢ ( ( ( 𝑊 ∈ LVec ∧ ( 𝐵 ⊆ 𝑉 ∧ ( 𝑁 ‘ 𝐵 ) = 𝑉 ∧ ∀ 𝑥 ∈ 𝐵 ¬ 𝑥 ∈ ( 𝑁 ‘ ( 𝐵 ∖ { 𝑥 } ) ) ) ) ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ ( ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∖ { ( 0g ‘ ( Scalar ‘ 𝑊 ) ) } ) ) ) → 𝑊 ∈ LVec )
33 simprr ⊢ ( ( ( 𝑊 ∈ LVec ∧ ( 𝐵 ⊆ 𝑉 ∧ ( 𝑁 ‘ 𝐵 ) = 𝑉 ∧ ∀ 𝑥 ∈ 𝐵 ¬ 𝑥 ∈ ( 𝑁 ‘ ( 𝐵 ∖ { 𝑥 } ) ) ) ) ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ ( ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∖ { ( 0g ‘ ( Scalar ‘ 𝑊 ) ) } ) ) ) → 𝑧 ∈ ( ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∖ { ( 0g ‘ ( Scalar ‘ 𝑊 ) ) } ) )
34 eldifsn ⊢ ( 𝑧 ∈ ( ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∖ { ( 0g ‘ ( Scalar ‘ 𝑊 ) ) } ) ↔ ( 𝑧 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∧ 𝑧 ≠ ( 0g ‘ ( Scalar ‘ 𝑊 ) ) ) )
35 33 34 sylib ⊢ ( ( ( 𝑊 ∈ LVec ∧ ( 𝐵 ⊆ 𝑉 ∧ ( 𝑁 ‘ 𝐵 ) = 𝑉 ∧ ∀ 𝑥 ∈ 𝐵 ¬ 𝑥 ∈ ( 𝑁 ‘ ( 𝐵 ∖ { 𝑥 } ) ) ) ) ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ ( ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∖ { ( 0g ‘ ( Scalar ‘ 𝑊 ) ) } ) ) ) → ( 𝑧 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∧ 𝑧 ≠ ( 0g ‘ ( Scalar ‘ 𝑊 ) ) ) )
36 21 adantr ⊢ ( ( ( 𝑊 ∈ LVec ∧ ( 𝐵 ⊆ 𝑉 ∧ ( 𝑁 ‘ 𝐵 ) = 𝑉 ∧ ∀ 𝑥 ∈ 𝐵 ¬ 𝑥 ∈ ( 𝑁 ‘ ( 𝐵 ∖ { 𝑥 } ) ) ) ) ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ ( ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∖ { ( 0g ‘ ( Scalar ‘ 𝑊 ) ) } ) ) ) → 𝐵 ⊆ 𝑉 )
37 36 30 sseldd ⊢ ( ( ( 𝑊 ∈ LVec ∧ ( 𝐵 ⊆ 𝑉 ∧ ( 𝑁 ‘ 𝐵 ) = 𝑉 ∧ ∀ 𝑥 ∈ 𝐵 ¬ 𝑥 ∈ ( 𝑁 ‘ ( 𝐵 ∖ { 𝑥 } ) ) ) ) ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ ( ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∖ { ( 0g ‘ ( Scalar ‘ 𝑊 ) ) } ) ) ) → 𝑦 ∈ 𝑉 )
38 eqid ⊢ ( ·𝑠 ‘ 𝑊 ) = ( ·𝑠 ‘ 𝑊 )
39 eqid ⊢ ( Base ‘ ( Scalar ‘ 𝑊 ) ) = ( Base ‘ ( Scalar ‘ 𝑊 ) )
40 1 9 38 39 11 3 lspsnvs ⊢ ( ( 𝑊 ∈ LVec ∧ ( 𝑧 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∧ 𝑧 ≠ ( 0g ‘ ( Scalar ‘ 𝑊 ) ) ) ∧ 𝑦 ∈ 𝑉 ) → ( 𝑁 ‘ { ( 𝑧 ( ·𝑠 ‘ 𝑊 ) 𝑦 ) } ) = ( 𝑁 ‘ { 𝑦 } ) )
41 32 35 37 40 syl3anc ⊢ ( ( ( 𝑊 ∈ LVec ∧ ( 𝐵 ⊆ 𝑉 ∧ ( 𝑁 ‘ 𝐵 ) = 𝑉 ∧ ∀ 𝑥 ∈ 𝐵 ¬ 𝑥 ∈ ( 𝑁 ‘ ( 𝐵 ∖ { 𝑥 } ) ) ) ) ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ ( ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∖ { ( 0g ‘ ( Scalar ‘ 𝑊 ) ) } ) ) ) → ( 𝑁 ‘ { ( 𝑧 ( ·𝑠 ‘ 𝑊 ) 𝑦 ) } ) = ( 𝑁 ‘ { 𝑦 } ) )
42 41 sseq1d ⊢ ( ( ( 𝑊 ∈ LVec ∧ ( 𝐵 ⊆ 𝑉 ∧ ( 𝑁 ‘ 𝐵 ) = 𝑉 ∧ ∀ 𝑥 ∈ 𝐵 ¬ 𝑥 ∈ ( 𝑁 ‘ ( 𝐵 ∖ { 𝑥 } ) ) ) ) ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ ( ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∖ { ( 0g ‘ ( Scalar ‘ 𝑊 ) ) } ) ) ) → ( ( 𝑁 ‘ { ( 𝑧 ( ·𝑠 ‘ 𝑊 ) 𝑦 ) } ) ⊆ ( 𝑁 ‘ ( 𝐵 ∖ { 𝑦 } ) ) ↔ ( 𝑁 ‘ { 𝑦 } ) ⊆ ( 𝑁 ‘ ( 𝐵 ∖ { 𝑦 } ) ) ) )
43 eqid ⊢ ( LSubSp ‘ 𝑊 ) = ( LSubSp ‘ 𝑊 )
44 8 adantr ⊢ ( ( 𝑊 ∈ LVec ∧ ( 𝐵 ⊆ 𝑉 ∧ ( 𝑁 ‘ 𝐵 ) = 𝑉 ∧ ∀ 𝑥 ∈ 𝐵 ¬ 𝑥 ∈ ( 𝑁 ‘ ( 𝐵 ∖ { 𝑥 } ) ) ) ) → 𝑊 ∈ LMod )
45 44 adantr ⊢ ( ( ( 𝑊 ∈ LVec ∧ ( 𝐵 ⊆ 𝑉 ∧ ( 𝑁 ‘ 𝐵 ) = 𝑉 ∧ ∀ 𝑥 ∈ 𝐵 ¬ 𝑥 ∈ ( 𝑁 ‘ ( 𝐵 ∖ { 𝑥 } ) ) ) ) ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ ( ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∖ { ( 0g ‘ ( Scalar ‘ 𝑊 ) ) } ) ) ) → 𝑊 ∈ LMod )
46 36 ssdifssd ⊢ ( ( ( 𝑊 ∈ LVec ∧ ( 𝐵 ⊆ 𝑉 ∧ ( 𝑁 ‘ 𝐵 ) = 𝑉 ∧ ∀ 𝑥 ∈ 𝐵 ¬ 𝑥 ∈ ( 𝑁 ‘ ( 𝐵 ∖ { 𝑥 } ) ) ) ) ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ ( ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∖ { ( 0g ‘ ( Scalar ‘ 𝑊 ) ) } ) ) ) → ( 𝐵 ∖ { 𝑦 } ) ⊆ 𝑉 )
47 1 43 3 lspcl ⊢ ( ( 𝑊 ∈ LMod ∧ ( 𝐵 ∖ { 𝑦 } ) ⊆ 𝑉 ) → ( 𝑁 ‘ ( 𝐵 ∖ { 𝑦 } ) ) ∈ ( LSubSp ‘ 𝑊 ) )
48 45 46 47 syl2anc ⊢ ( ( ( 𝑊 ∈ LVec ∧ ( 𝐵 ⊆ 𝑉 ∧ ( 𝑁 ‘ 𝐵 ) = 𝑉 ∧ ∀ 𝑥 ∈ 𝐵 ¬ 𝑥 ∈ ( 𝑁 ‘ ( 𝐵 ∖ { 𝑥 } ) ) ) ) ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ ( ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∖ { ( 0g ‘ ( Scalar ‘ 𝑊 ) ) } ) ) ) → ( 𝑁 ‘ ( 𝐵 ∖ { 𝑦 } ) ) ∈ ( LSubSp ‘ 𝑊 ) )
49 35 simpld ⊢ ( ( ( 𝑊 ∈ LVec ∧ ( 𝐵 ⊆ 𝑉 ∧ ( 𝑁 ‘ 𝐵 ) = 𝑉 ∧ ∀ 𝑥 ∈ 𝐵 ¬ 𝑥 ∈ ( 𝑁 ‘ ( 𝐵 ∖ { 𝑥 } ) ) ) ) ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ ( ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∖ { ( 0g ‘ ( Scalar ‘ 𝑊 ) ) } ) ) ) → 𝑧 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) )
50 1 9 38 39 lmodvscl ⊢ ( ( 𝑊 ∈ LMod ∧ 𝑧 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∧ 𝑦 ∈ 𝑉 ) → ( 𝑧 ( ·𝑠 ‘ 𝑊 ) 𝑦 ) ∈ 𝑉 )
51 45 49 37 50 syl3anc ⊢ ( ( ( 𝑊 ∈ LVec ∧ ( 𝐵 ⊆ 𝑉 ∧ ( 𝑁 ‘ 𝐵 ) = 𝑉 ∧ ∀ 𝑥 ∈ 𝐵 ¬ 𝑥 ∈ ( 𝑁 ‘ ( 𝐵 ∖ { 𝑥 } ) ) ) ) ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ ( ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∖ { ( 0g ‘ ( Scalar ‘ 𝑊 ) ) } ) ) ) → ( 𝑧 ( ·𝑠 ‘ 𝑊 ) 𝑦 ) ∈ 𝑉 )
52 1 43 3 45 48 51 ellspsn5b ⊢ ( ( ( 𝑊 ∈ LVec ∧ ( 𝐵 ⊆ 𝑉 ∧ ( 𝑁 ‘ 𝐵 ) = 𝑉 ∧ ∀ 𝑥 ∈ 𝐵 ¬ 𝑥 ∈ ( 𝑁 ‘ ( 𝐵 ∖ { 𝑥 } ) ) ) ) ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ ( ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∖ { ( 0g ‘ ( Scalar ‘ 𝑊 ) ) } ) ) ) → ( ( 𝑧 ( ·𝑠 ‘ 𝑊 ) 𝑦 ) ∈ ( 𝑁 ‘ ( 𝐵 ∖ { 𝑦 } ) ) ↔ ( 𝑁 ‘ { ( 𝑧 ( ·𝑠 ‘ 𝑊 ) 𝑦 ) } ) ⊆ ( 𝑁 ‘ ( 𝐵 ∖ { 𝑦 } ) ) ) )
53 1 43 3 45 48 37 ellspsn5b ⊢ ( ( ( 𝑊 ∈ LVec ∧ ( 𝐵 ⊆ 𝑉 ∧ ( 𝑁 ‘ 𝐵 ) = 𝑉 ∧ ∀ 𝑥 ∈ 𝐵 ¬ 𝑥 ∈ ( 𝑁 ‘ ( 𝐵 ∖ { 𝑥 } ) ) ) ) ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ ( ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∖ { ( 0g ‘ ( Scalar ‘ 𝑊 ) ) } ) ) ) → ( 𝑦 ∈ ( 𝑁 ‘ ( 𝐵 ∖ { 𝑦 } ) ) ↔ ( 𝑁 ‘ { 𝑦 } ) ⊆ ( 𝑁 ‘ ( 𝐵 ∖ { 𝑦 } ) ) ) )
54 42 52 53 3bitr4d ⊢ ( ( ( 𝑊 ∈ LVec ∧ ( 𝐵 ⊆ 𝑉 ∧ ( 𝑁 ‘ 𝐵 ) = 𝑉 ∧ ∀ 𝑥 ∈ 𝐵 ¬ 𝑥 ∈ ( 𝑁 ‘ ( 𝐵 ∖ { 𝑥 } ) ) ) ) ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ ( ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∖ { ( 0g ‘ ( Scalar ‘ 𝑊 ) ) } ) ) ) → ( ( 𝑧 ( ·𝑠 ‘ 𝑊 ) 𝑦 ) ∈ ( 𝑁 ‘ ( 𝐵 ∖ { 𝑦 } ) ) ↔ 𝑦 ∈ ( 𝑁 ‘ ( 𝐵 ∖ { 𝑦 } ) ) ) )
55 31 54 mtbird ⊢ ( ( ( 𝑊 ∈ LVec ∧ ( 𝐵 ⊆ 𝑉 ∧ ( 𝑁 ‘ 𝐵 ) = 𝑉 ∧ ∀ 𝑥 ∈ 𝐵 ¬ 𝑥 ∈ ( 𝑁 ‘ ( 𝐵 ∖ { 𝑥 } ) ) ) ) ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ ( ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∖ { ( 0g ‘ ( Scalar ‘ 𝑊 ) ) } ) ) ) → ¬ ( 𝑧 ( ·𝑠 ‘ 𝑊 ) 𝑦 ) ∈ ( 𝑁 ‘ ( 𝐵 ∖ { 𝑦 } ) ) )
56 55 ralrimivva ⊢ ( ( 𝑊 ∈ LVec ∧ ( 𝐵 ⊆ 𝑉 ∧ ( 𝑁 ‘ 𝐵 ) = 𝑉 ∧ ∀ 𝑥 ∈ 𝐵 ¬ 𝑥 ∈ ( 𝑁 ‘ ( 𝐵 ∖ { 𝑥 } ) ) ) ) → ∀ 𝑦 ∈ 𝐵 ∀ 𝑧 ∈ ( ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∖ { ( 0g ‘ ( Scalar ‘ 𝑊 ) ) } ) ¬ ( 𝑧 ( ·𝑠 ‘ 𝑊 ) 𝑦 ) ∈ ( 𝑁 ‘ ( 𝐵 ∖ { 𝑦 } ) ) )
57 1 9 38 39 2 3 11 islbs ⊢ ( 𝑊 ∈ LVec → ( 𝐵 ∈ 𝐽 ↔ ( 𝐵 ⊆ 𝑉 ∧ ( 𝑁 ‘ 𝐵 ) = 𝑉 ∧ ∀ 𝑦 ∈ 𝐵 ∀ 𝑧 ∈ ( ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∖ { ( 0g ‘ ( Scalar ‘ 𝑊 ) ) } ) ¬ ( 𝑧 ( ·𝑠 ‘ 𝑊 ) 𝑦 ) ∈ ( 𝑁 ‘ ( 𝐵 ∖ { 𝑦 } ) ) ) ) )
58 57 adantr ⊢ ( ( 𝑊 ∈ LVec ∧ ( 𝐵 ⊆ 𝑉 ∧ ( 𝑁 ‘ 𝐵 ) = 𝑉 ∧ ∀ 𝑥 ∈ 𝐵 ¬ 𝑥 ∈ ( 𝑁 ‘ ( 𝐵 ∖ { 𝑥 } ) ) ) ) → ( 𝐵 ∈ 𝐽 ↔ ( 𝐵 ⊆ 𝑉 ∧ ( 𝑁 ‘ 𝐵 ) = 𝑉 ∧ ∀ 𝑦 ∈ 𝐵 ∀ 𝑧 ∈ ( ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∖ { ( 0g ‘ ( Scalar ‘ 𝑊 ) ) } ) ¬ ( 𝑧 ( ·𝑠 ‘ 𝑊 ) 𝑦 ) ∈ ( 𝑁 ‘ ( 𝐵 ∖ { 𝑦 } ) ) ) ) )
59 21 22 56 58 mpbir3and ⊢ ( ( 𝑊 ∈ LVec ∧ ( 𝐵 ⊆ 𝑉 ∧ ( 𝑁 ‘ 𝐵 ) = 𝑉 ∧ ∀ 𝑥 ∈ 𝐵 ¬ 𝑥 ∈ ( 𝑁 ‘ ( 𝐵 ∖ { 𝑥 } ) ) ) ) → 𝐵 ∈ 𝐽 )
60 20 59 impbida ⊢ ( 𝑊 ∈ LVec → ( 𝐵 ∈ 𝐽 ↔ ( 𝐵 ⊆ 𝑉 ∧ ( 𝑁 ‘ 𝐵 ) = 𝑉 ∧ ∀ 𝑥 ∈ 𝐵 ¬ 𝑥 ∈ ( 𝑁 ‘ ( 𝐵 ∖ { 𝑥 } ) ) ) ) )