Metamath Proof Explorer

Theorem islbs3

Description: An equivalent formulation of the basis predicate: a subset is a basis iff it is a minimal spanning set. (Contributed by Mario Carneiro, 25-Jun-2014)

Ref Expression
Hypotheses islbs2.v ⊢ 𝑉 = ( Base ‘ 𝑊 )
islbs2.j ⊢ 𝐽 = ( LBasis ‘ 𝑊 )
islbs2.n ⊢ 𝑁 = ( LSpan ‘ 𝑊 )
Assertion islbs3 ( 𝑊 ∈ 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 8 3ad2ant1 ⊢ ( ( 𝑊 ∈ LVec ∧ 𝐵 ∈ 𝐽 ∧ 𝑠 ⊊ 𝐵 ) → 𝑊 ∈ LMod )
10 pssss ⊢ ( 𝑠 ⊊ 𝐵 → 𝑠 ⊆ 𝐵 )
11 10 4 sylan9ssr ⊢ ( ( 𝐵 ∈ 𝐽 ∧ 𝑠 ⊊ 𝐵 ) → 𝑠 ⊆ 𝑉 )
12 11 3adant1 ⊢ ( ( 𝑊 ∈ LVec ∧ 𝐵 ∈ 𝐽 ∧ 𝑠 ⊊ 𝐵 ) → 𝑠 ⊆ 𝑉 )
13 1 3 lspssv ⊢ ( ( 𝑊 ∈ LMod ∧ 𝑠 ⊆ 𝑉 ) → ( 𝑁 ‘ 𝑠 ) ⊆ 𝑉 )
14 9 12 13 syl2anc ⊢ ( ( 𝑊 ∈ LVec ∧ 𝐵 ∈ 𝐽 ∧ 𝑠 ⊊ 𝐵 ) → ( 𝑁 ‘ 𝑠 ) ⊆ 𝑉 )
15 eqid ⊢ ( Scalar ‘ 𝑊 ) = ( Scalar ‘ 𝑊 )
16 15 lvecdrng ⊢ ( 𝑊 ∈ LVec → ( Scalar ‘ 𝑊 ) ∈ DivRing )
17 eqid ⊢ ( 0g ‘ ( Scalar ‘ 𝑊 ) ) = ( 0g ‘ ( Scalar ‘ 𝑊 ) )
18 eqid ⊢ ( 1r ‘ ( Scalar ‘ 𝑊 ) ) = ( 1r ‘ ( Scalar ‘ 𝑊 ) )
19 17 18 drngunz ⊢ ( ( Scalar ‘ 𝑊 ) ∈ DivRing → ( 1r ‘ ( Scalar ‘ 𝑊 ) ) ≠ ( 0g ‘ ( Scalar ‘ 𝑊 ) ) )
20 16 19 syl ⊢ ( 𝑊 ∈ LVec → ( 1r ‘ ( Scalar ‘ 𝑊 ) ) ≠ ( 0g ‘ ( Scalar ‘ 𝑊 ) ) )
21 8 20 jca ⊢ ( 𝑊 ∈ LVec → ( 𝑊 ∈ LMod ∧ ( 1r ‘ ( Scalar ‘ 𝑊 ) ) ≠ ( 0g ‘ ( Scalar ‘ 𝑊 ) ) ) )
22 2 3 15 18 17 1 lbspss ⊢ ( ( ( 𝑊 ∈ LMod ∧ ( 1r ‘ ( Scalar ‘ 𝑊 ) ) ≠ ( 0g ‘ ( Scalar ‘ 𝑊 ) ) ) ∧ 𝐵 ∈ 𝐽 ∧ 𝑠 ⊊ 𝐵 ) → ( 𝑁 ‘ 𝑠 ) ≠ 𝑉 )
23 21 22 syl3an1 ⊢ ( ( 𝑊 ∈ LVec ∧ 𝐵 ∈ 𝐽 ∧ 𝑠 ⊊ 𝐵 ) → ( 𝑁 ‘ 𝑠 ) ≠ 𝑉 )
24 df-pss ⊢ ( ( 𝑁 ‘ 𝑠 ) ⊊ 𝑉 ↔ ( ( 𝑁 ‘ 𝑠 ) ⊆ 𝑉 ∧ ( 𝑁 ‘ 𝑠 ) ≠ 𝑉 ) )
25 14 23 24 sylanbrc ⊢ ( ( 𝑊 ∈ LVec ∧ 𝐵 ∈ 𝐽 ∧ 𝑠 ⊊ 𝐵 ) → ( 𝑁 ‘ 𝑠 ) ⊊ 𝑉 )
26 25 3expia ⊢ ( ( 𝑊 ∈ LVec ∧ 𝐵 ∈ 𝐽 ) → ( 𝑠 ⊊ 𝐵 → ( 𝑁 ‘ 𝑠 ) ⊊ 𝑉 ) )
27 26 alrimiv ⊢ ( ( 𝑊 ∈ LVec ∧ 𝐵 ∈ 𝐽 ) → ∀ 𝑠 ( 𝑠 ⊊ 𝐵 → ( 𝑁 ‘ 𝑠 ) ⊊ 𝑉 ) )
28 5 7 27 3jca ⊢ ( ( 𝑊 ∈ LVec ∧ 𝐵 ∈ 𝐽 ) → ( 𝐵 ⊆ 𝑉 ∧ ( 𝑁 ‘ 𝐵 ) = 𝑉 ∧ ∀ 𝑠 ( 𝑠 ⊊ 𝐵 → ( 𝑁 ‘ 𝑠 ) ⊊ 𝑉 ) ) )
29 simpr1 ⊢ ( ( 𝑊 ∈ LVec ∧ ( 𝐵 ⊆ 𝑉 ∧ ( 𝑁 ‘ 𝐵 ) = 𝑉 ∧ ∀ 𝑠 ( 𝑠 ⊊ 𝐵 → ( 𝑁 ‘ 𝑠 ) ⊊ 𝑉 ) ) ) → 𝐵 ⊆ 𝑉 )
30 simpr2 ⊢ ( ( 𝑊 ∈ LVec ∧ ( 𝐵 ⊆ 𝑉 ∧ ( 𝑁 ‘ 𝐵 ) = 𝑉 ∧ ∀ 𝑠 ( 𝑠 ⊊ 𝐵 → ( 𝑁 ‘ 𝑠 ) ⊊ 𝑉 ) ) ) → ( 𝑁 ‘ 𝐵 ) = 𝑉 )
31 simplr1 ⊢ ( ( ( 𝑊 ∈ LVec ∧ ( 𝐵 ⊆ 𝑉 ∧ ( 𝑁 ‘ 𝐵 ) = 𝑉 ∧ ∀ 𝑠 ( 𝑠 ⊊ 𝐵 → ( 𝑁 ‘ 𝑠 ) ⊊ 𝑉 ) ) ) ∧ 𝑥 ∈ 𝐵 ) → 𝐵 ⊆ 𝑉 )
32 31 ssdifssd ⊢ ( ( ( 𝑊 ∈ LVec ∧ ( 𝐵 ⊆ 𝑉 ∧ ( 𝑁 ‘ 𝐵 ) = 𝑉 ∧ ∀ 𝑠 ( 𝑠 ⊊ 𝐵 → ( 𝑁 ‘ 𝑠 ) ⊊ 𝑉 ) ) ) ∧ 𝑥 ∈ 𝐵 ) → ( 𝐵 ∖ { 𝑥 } ) ⊆ 𝑉 )
33 1 fvexi ⊢ 𝑉 ∈ V
34 ssexg ⊢ ( ( ( 𝐵 ∖ { 𝑥 } ) ⊆ 𝑉 ∧ 𝑉 ∈ V ) → ( 𝐵 ∖ { 𝑥 } ) ∈ V )
35 32 33 34 sylancl ⊢ ( ( ( 𝑊 ∈ LVec ∧ ( 𝐵 ⊆ 𝑉 ∧ ( 𝑁 ‘ 𝐵 ) = 𝑉 ∧ ∀ 𝑠 ( 𝑠 ⊊ 𝐵 → ( 𝑁 ‘ 𝑠 ) ⊊ 𝑉 ) ) ) ∧ 𝑥 ∈ 𝐵 ) → ( 𝐵 ∖ { 𝑥 } ) ∈ V )
36 simplr3 ⊢ ( ( ( 𝑊 ∈ LVec ∧ ( 𝐵 ⊆ 𝑉 ∧ ( 𝑁 ‘ 𝐵 ) = 𝑉 ∧ ∀ 𝑠 ( 𝑠 ⊊ 𝐵 → ( 𝑁 ‘ 𝑠 ) ⊊ 𝑉 ) ) ) ∧ 𝑥 ∈ 𝐵 ) → ∀ 𝑠 ( 𝑠 ⊊ 𝐵 → ( 𝑁 ‘ 𝑠 ) ⊊ 𝑉 ) )
37 difssd ⊢ ( ( ( 𝑊 ∈ LVec ∧ ( 𝐵 ⊆ 𝑉 ∧ ( 𝑁 ‘ 𝐵 ) = 𝑉 ∧ ∀ 𝑠 ( 𝑠 ⊊ 𝐵 → ( 𝑁 ‘ 𝑠 ) ⊊ 𝑉 ) ) ) ∧ 𝑥 ∈ 𝐵 ) → ( 𝐵 ∖ { 𝑥 } ) ⊆ 𝐵 )
38 simpr ⊢ ( ( ( 𝑊 ∈ LVec ∧ ( 𝐵 ⊆ 𝑉 ∧ ( 𝑁 ‘ 𝐵 ) = 𝑉 ∧ ∀ 𝑠 ( 𝑠 ⊊ 𝐵 → ( 𝑁 ‘ 𝑠 ) ⊊ 𝑉 ) ) ) ∧ 𝑥 ∈ 𝐵 ) → 𝑥 ∈ 𝐵 )
39 neldifsn ⊢ ¬ 𝑥 ∈ ( 𝐵 ∖ { 𝑥 } )
40 nelne1 ⊢ ( ( 𝑥 ∈ 𝐵 ∧ ¬ 𝑥 ∈ ( 𝐵 ∖ { 𝑥 } ) ) → 𝐵 ≠ ( 𝐵 ∖ { 𝑥 } ) )
41 38 39 40 sylancl ⊢ ( ( ( 𝑊 ∈ LVec ∧ ( 𝐵 ⊆ 𝑉 ∧ ( 𝑁 ‘ 𝐵 ) = 𝑉 ∧ ∀ 𝑠 ( 𝑠 ⊊ 𝐵 → ( 𝑁 ‘ 𝑠 ) ⊊ 𝑉 ) ) ) ∧ 𝑥 ∈ 𝐵 ) → 𝐵 ≠ ( 𝐵 ∖ { 𝑥 } ) )
42 41 necomd ⊢ ( ( ( 𝑊 ∈ LVec ∧ ( 𝐵 ⊆ 𝑉 ∧ ( 𝑁 ‘ 𝐵 ) = 𝑉 ∧ ∀ 𝑠 ( 𝑠 ⊊ 𝐵 → ( 𝑁 ‘ 𝑠 ) ⊊ 𝑉 ) ) ) ∧ 𝑥 ∈ 𝐵 ) → ( 𝐵 ∖ { 𝑥 } ) ≠ 𝐵 )
43 df-pss ⊢ ( ( 𝐵 ∖ { 𝑥 } ) ⊊ 𝐵 ↔ ( ( 𝐵 ∖ { 𝑥 } ) ⊆ 𝐵 ∧ ( 𝐵 ∖ { 𝑥 } ) ≠ 𝐵 ) )
44 37 42 43 sylanbrc ⊢ ( ( ( 𝑊 ∈ LVec ∧ ( 𝐵 ⊆ 𝑉 ∧ ( 𝑁 ‘ 𝐵 ) = 𝑉 ∧ ∀ 𝑠 ( 𝑠 ⊊ 𝐵 → ( 𝑁 ‘ 𝑠 ) ⊊ 𝑉 ) ) ) ∧ 𝑥 ∈ 𝐵 ) → ( 𝐵 ∖ { 𝑥 } ) ⊊ 𝐵 )
45 psseq1 ⊢ ( 𝑠 = ( 𝐵 ∖ { 𝑥 } ) → ( 𝑠 ⊊ 𝐵 ↔ ( 𝐵 ∖ { 𝑥 } ) ⊊ 𝐵 ) )
46 fveq2 ⊢ ( 𝑠 = ( 𝐵 ∖ { 𝑥 } ) → ( 𝑁 ‘ 𝑠 ) = ( 𝑁 ‘ ( 𝐵 ∖ { 𝑥 } ) ) )
47 46 psseq1d ⊢ ( 𝑠 = ( 𝐵 ∖ { 𝑥 } ) → ( ( 𝑁 ‘ 𝑠 ) ⊊ 𝑉 ↔ ( 𝑁 ‘ ( 𝐵 ∖ { 𝑥 } ) ) ⊊ 𝑉 ) )
48 45 47 imbi12d ⊢ ( 𝑠 = ( 𝐵 ∖ { 𝑥 } ) → ( ( 𝑠 ⊊ 𝐵 → ( 𝑁 ‘ 𝑠 ) ⊊ 𝑉 ) ↔ ( ( 𝐵 ∖ { 𝑥 } ) ⊊ 𝐵 → ( 𝑁 ‘ ( 𝐵 ∖ { 𝑥 } ) ) ⊊ 𝑉 ) ) )
49 48 spcgv ⊢ ( ( 𝐵 ∖ { 𝑥 } ) ∈ V → ( ∀ 𝑠 ( 𝑠 ⊊ 𝐵 → ( 𝑁 ‘ 𝑠 ) ⊊ 𝑉 ) → ( ( 𝐵 ∖ { 𝑥 } ) ⊊ 𝐵 → ( 𝑁 ‘ ( 𝐵 ∖ { 𝑥 } ) ) ⊊ 𝑉 ) ) )
50 35 36 44 49 syl3c ⊢ ( ( ( 𝑊 ∈ LVec ∧ ( 𝐵 ⊆ 𝑉 ∧ ( 𝑁 ‘ 𝐵 ) = 𝑉 ∧ ∀ 𝑠 ( 𝑠 ⊊ 𝐵 → ( 𝑁 ‘ 𝑠 ) ⊊ 𝑉 ) ) ) ∧ 𝑥 ∈ 𝐵 ) → ( 𝑁 ‘ ( 𝐵 ∖ { 𝑥 } ) ) ⊊ 𝑉 )
51 dfpss3 ⊢ ( ( 𝑁 ‘ ( 𝐵 ∖ { 𝑥 } ) ) ⊊ 𝑉 ↔ ( ( 𝑁 ‘ ( 𝐵 ∖ { 𝑥 } ) ) ⊆ 𝑉 ∧ ¬ 𝑉 ⊆ ( 𝑁 ‘ ( 𝐵 ∖ { 𝑥 } ) ) ) )
52 51 simprbi ⊢ ( ( 𝑁 ‘ ( 𝐵 ∖ { 𝑥 } ) ) ⊊ 𝑉 → ¬ 𝑉 ⊆ ( 𝑁 ‘ ( 𝐵 ∖ { 𝑥 } ) ) )
53 50 52 syl ⊢ ( ( ( 𝑊 ∈ LVec ∧ ( 𝐵 ⊆ 𝑉 ∧ ( 𝑁 ‘ 𝐵 ) = 𝑉 ∧ ∀ 𝑠 ( 𝑠 ⊊ 𝐵 → ( 𝑁 ‘ 𝑠 ) ⊊ 𝑉 ) ) ) ∧ 𝑥 ∈ 𝐵 ) → ¬ 𝑉 ⊆ ( 𝑁 ‘ ( 𝐵 ∖ { 𝑥 } ) ) )
54 simplr2 ⊢ ( ( ( 𝑊 ∈ LVec ∧ ( 𝐵 ⊆ 𝑉 ∧ ( 𝑁 ‘ 𝐵 ) = 𝑉 ∧ ∀ 𝑠 ( 𝑠 ⊊ 𝐵 → ( 𝑁 ‘ 𝑠 ) ⊊ 𝑉 ) ) ) ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑥 ∈ ( 𝑁 ‘ ( 𝐵 ∖ { 𝑥 } ) ) ) ) → ( 𝑁 ‘ 𝐵 ) = 𝑉 )
55 8 ad2antrr ⊢ ( ( ( 𝑊 ∈ LVec ∧ ( 𝐵 ⊆ 𝑉 ∧ ( 𝑁 ‘ 𝐵 ) = 𝑉 ∧ ∀ 𝑠 ( 𝑠 ⊊ 𝐵 → ( 𝑁 ‘ 𝑠 ) ⊊ 𝑉 ) ) ) ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑥 ∈ ( 𝑁 ‘ ( 𝐵 ∖ { 𝑥 } ) ) ) ) → 𝑊 ∈ LMod )
56 32 adantrr ⊢ ( ( ( 𝑊 ∈ LVec ∧ ( 𝐵 ⊆ 𝑉 ∧ ( 𝑁 ‘ 𝐵 ) = 𝑉 ∧ ∀ 𝑠 ( 𝑠 ⊊ 𝐵 → ( 𝑁 ‘ 𝑠 ) ⊊ 𝑉 ) ) ) ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑥 ∈ ( 𝑁 ‘ ( 𝐵 ∖ { 𝑥 } ) ) ) ) → ( 𝐵 ∖ { 𝑥 } ) ⊆ 𝑉 )
57 eqid ⊢ ( LSubSp ‘ 𝑊 ) = ( LSubSp ‘ 𝑊 )
58 1 57 3 lspcl ⊢ ( ( 𝑊 ∈ LMod ∧ ( 𝐵 ∖ { 𝑥 } ) ⊆ 𝑉 ) → ( 𝑁 ‘ ( 𝐵 ∖ { 𝑥 } ) ) ∈ ( LSubSp ‘ 𝑊 ) )
59 55 56 58 syl2anc ⊢ ( ( ( 𝑊 ∈ LVec ∧ ( 𝐵 ⊆ 𝑉 ∧ ( 𝑁 ‘ 𝐵 ) = 𝑉 ∧ ∀ 𝑠 ( 𝑠 ⊊ 𝐵 → ( 𝑁 ‘ 𝑠 ) ⊊ 𝑉 ) ) ) ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑥 ∈ ( 𝑁 ‘ ( 𝐵 ∖ { 𝑥 } ) ) ) ) → ( 𝑁 ‘ ( 𝐵 ∖ { 𝑥 } ) ) ∈ ( LSubSp ‘ 𝑊 ) )
60 ssun1 ⊢ 𝐵 ⊆ ( 𝐵 ∪ { 𝑥 } )
61 undif1 ⊢ ( ( 𝐵 ∖ { 𝑥 } ) ∪ { 𝑥 } ) = ( 𝐵 ∪ { 𝑥 } )
62 60 61 sseqtrri ⊢ 𝐵 ⊆ ( ( 𝐵 ∖ { 𝑥 } ) ∪ { 𝑥 } )
63 1 3 lspssid ⊢ ( ( 𝑊 ∈ LMod ∧ ( 𝐵 ∖ { 𝑥 } ) ⊆ 𝑉 ) → ( 𝐵 ∖ { 𝑥 } ) ⊆ ( 𝑁 ‘ ( 𝐵 ∖ { 𝑥 } ) ) )
64 55 56 63 syl2anc ⊢ ( ( ( 𝑊 ∈ LVec ∧ ( 𝐵 ⊆ 𝑉 ∧ ( 𝑁 ‘ 𝐵 ) = 𝑉 ∧ ∀ 𝑠 ( 𝑠 ⊊ 𝐵 → ( 𝑁 ‘ 𝑠 ) ⊊ 𝑉 ) ) ) ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑥 ∈ ( 𝑁 ‘ ( 𝐵 ∖ { 𝑥 } ) ) ) ) → ( 𝐵 ∖ { 𝑥 } ) ⊆ ( 𝑁 ‘ ( 𝐵 ∖ { 𝑥 } ) ) )
65 simprr ⊢ ( ( ( 𝑊 ∈ LVec ∧ ( 𝐵 ⊆ 𝑉 ∧ ( 𝑁 ‘ 𝐵 ) = 𝑉 ∧ ∀ 𝑠 ( 𝑠 ⊊ 𝐵 → ( 𝑁 ‘ 𝑠 ) ⊊ 𝑉 ) ) ) ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑥 ∈ ( 𝑁 ‘ ( 𝐵 ∖ { 𝑥 } ) ) ) ) → 𝑥 ∈ ( 𝑁 ‘ ( 𝐵 ∖ { 𝑥 } ) ) )
66 65 snssd ⊢ ( ( ( 𝑊 ∈ LVec ∧ ( 𝐵 ⊆ 𝑉 ∧ ( 𝑁 ‘ 𝐵 ) = 𝑉 ∧ ∀ 𝑠 ( 𝑠 ⊊ 𝐵 → ( 𝑁 ‘ 𝑠 ) ⊊ 𝑉 ) ) ) ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑥 ∈ ( 𝑁 ‘ ( 𝐵 ∖ { 𝑥 } ) ) ) ) → { 𝑥 } ⊆ ( 𝑁 ‘ ( 𝐵 ∖ { 𝑥 } ) ) )
67 64 66 unssd ⊢ ( ( ( 𝑊 ∈ LVec ∧ ( 𝐵 ⊆ 𝑉 ∧ ( 𝑁 ‘ 𝐵 ) = 𝑉 ∧ ∀ 𝑠 ( 𝑠 ⊊ 𝐵 → ( 𝑁 ‘ 𝑠 ) ⊊ 𝑉 ) ) ) ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑥 ∈ ( 𝑁 ‘ ( 𝐵 ∖ { 𝑥 } ) ) ) ) → ( ( 𝐵 ∖ { 𝑥 } ) ∪ { 𝑥 } ) ⊆ ( 𝑁 ‘ ( 𝐵 ∖ { 𝑥 } ) ) )
68 62 67 sstrid ⊢ ( ( ( 𝑊 ∈ LVec ∧ ( 𝐵 ⊆ 𝑉 ∧ ( 𝑁 ‘ 𝐵 ) = 𝑉 ∧ ∀ 𝑠 ( 𝑠 ⊊ 𝐵 → ( 𝑁 ‘ 𝑠 ) ⊊ 𝑉 ) ) ) ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑥 ∈ ( 𝑁 ‘ ( 𝐵 ∖ { 𝑥 } ) ) ) ) → 𝐵 ⊆ ( 𝑁 ‘ ( 𝐵 ∖ { 𝑥 } ) ) )
69 57 3 lspssp ⊢ ( ( 𝑊 ∈ LMod ∧ ( 𝑁 ‘ ( 𝐵 ∖ { 𝑥 } ) ) ∈ ( LSubSp ‘ 𝑊 ) ∧ 𝐵 ⊆ ( 𝑁 ‘ ( 𝐵 ∖ { 𝑥 } ) ) ) → ( 𝑁 ‘ 𝐵 ) ⊆ ( 𝑁 ‘ ( 𝐵 ∖ { 𝑥 } ) ) )
70 55 59 68 69 syl3anc ⊢ ( ( ( 𝑊 ∈ LVec ∧ ( 𝐵 ⊆ 𝑉 ∧ ( 𝑁 ‘ 𝐵 ) = 𝑉 ∧ ∀ 𝑠 ( 𝑠 ⊊ 𝐵 → ( 𝑁 ‘ 𝑠 ) ⊊ 𝑉 ) ) ) ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑥 ∈ ( 𝑁 ‘ ( 𝐵 ∖ { 𝑥 } ) ) ) ) → ( 𝑁 ‘ 𝐵 ) ⊆ ( 𝑁 ‘ ( 𝐵 ∖ { 𝑥 } ) ) )
71 54 70 eqsstrrd ⊢ ( ( ( 𝑊 ∈ LVec ∧ ( 𝐵 ⊆ 𝑉 ∧ ( 𝑁 ‘ 𝐵 ) = 𝑉 ∧ ∀ 𝑠 ( 𝑠 ⊊ 𝐵 → ( 𝑁 ‘ 𝑠 ) ⊊ 𝑉 ) ) ) ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑥 ∈ ( 𝑁 ‘ ( 𝐵 ∖ { 𝑥 } ) ) ) ) → 𝑉 ⊆ ( 𝑁 ‘ ( 𝐵 ∖ { 𝑥 } ) ) )
72 71 expr ⊢ ( ( ( 𝑊 ∈ LVec ∧ ( 𝐵 ⊆ 𝑉 ∧ ( 𝑁 ‘ 𝐵 ) = 𝑉 ∧ ∀ 𝑠 ( 𝑠 ⊊ 𝐵 → ( 𝑁 ‘ 𝑠 ) ⊊ 𝑉 ) ) ) ∧ 𝑥 ∈ 𝐵 ) → ( 𝑥 ∈ ( 𝑁 ‘ ( 𝐵 ∖ { 𝑥 } ) ) → 𝑉 ⊆ ( 𝑁 ‘ ( 𝐵 ∖ { 𝑥 } ) ) ) )
73 53 72 mtod ⊢ ( ( ( 𝑊 ∈ LVec ∧ ( 𝐵 ⊆ 𝑉 ∧ ( 𝑁 ‘ 𝐵 ) = 𝑉 ∧ ∀ 𝑠 ( 𝑠 ⊊ 𝐵 → ( 𝑁 ‘ 𝑠 ) ⊊ 𝑉 ) ) ) ∧ 𝑥 ∈ 𝐵 ) → ¬ 𝑥 ∈ ( 𝑁 ‘ ( 𝐵 ∖ { 𝑥 } ) ) )
74 73 ralrimiva ⊢ ( ( 𝑊 ∈ LVec ∧ ( 𝐵 ⊆ 𝑉 ∧ ( 𝑁 ‘ 𝐵 ) = 𝑉 ∧ ∀ 𝑠 ( 𝑠 ⊊ 𝐵 → ( 𝑁 ‘ 𝑠 ) ⊊ 𝑉 ) ) ) → ∀ 𝑥 ∈ 𝐵 ¬ 𝑥 ∈ ( 𝑁 ‘ ( 𝐵 ∖ { 𝑥 } ) ) )
75 1 2 3 islbs2 ⊢ ( 𝑊 ∈ LVec → ( 𝐵 ∈ 𝐽 ↔ ( 𝐵 ⊆ 𝑉 ∧ ( 𝑁 ‘ 𝐵 ) = 𝑉 ∧ ∀ 𝑥 ∈ 𝐵 ¬ 𝑥 ∈ ( 𝑁 ‘ ( 𝐵 ∖ { 𝑥 } ) ) ) ) )
76 75 adantr ⊢ ( ( 𝑊 ∈ LVec ∧ ( 𝐵 ⊆ 𝑉 ∧ ( 𝑁 ‘ 𝐵 ) = 𝑉 ∧ ∀ 𝑠 ( 𝑠 ⊊ 𝐵 → ( 𝑁 ‘ 𝑠 ) ⊊ 𝑉 ) ) ) → ( 𝐵 ∈ 𝐽 ↔ ( 𝐵 ⊆ 𝑉 ∧ ( 𝑁 ‘ 𝐵 ) = 𝑉 ∧ ∀ 𝑥 ∈ 𝐵 ¬ 𝑥 ∈ ( 𝑁 ‘ ( 𝐵 ∖ { 𝑥 } ) ) ) ) )
77 29 30 74 76 mpbir3and ⊢ ( ( 𝑊 ∈ LVec ∧ ( 𝐵 ⊆ 𝑉 ∧ ( 𝑁 ‘ 𝐵 ) = 𝑉 ∧ ∀ 𝑠 ( 𝑠 ⊊ 𝐵 → ( 𝑁 ‘ 𝑠 ) ⊊ 𝑉 ) ) ) → 𝐵 ∈ 𝐽 )
78 28 77 impbida ⊢ ( 𝑊 ∈ LVec → ( 𝐵 ∈ 𝐽 ↔ ( 𝐵 ⊆ 𝑉 ∧ ( 𝑁 ‘ 𝐵 ) = 𝑉 ∧ ∀ 𝑠 ( 𝑠 ⊊ 𝐵 → ( 𝑁 ‘ 𝑠 ) ⊊ 𝑉 ) ) ) )