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	lspsnel5	⊢ ( ( ( 𝑊 ∈ LVec ∧ ( 𝐵 ⊆ 𝑉 ∧ ( 𝑁 ‘ 𝐵 ) = 𝑉 ∧ ∀ 𝑥 ∈ 𝐵 ¬ 𝑥 ∈ ( 𝑁 ‘ ( 𝐵 ∖ { 𝑥 } ) ) ) ) ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ ( ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∖ { ( 0g ‘ ( Scalar ‘ 𝑊 ) ) } ) ) ) → ( ( 𝑧 ( ·𝑠 ‘ 𝑊 ) 𝑦 ) ∈ ( 𝑁 ‘ ( 𝐵 ∖ { 𝑦 } ) ) ↔ ( 𝑁 ‘ { ( 𝑧 ( ·𝑠 ‘ 𝑊 ) 𝑦 ) } ) ⊆ ( 𝑁 ‘ ( 𝐵 ∖ { 𝑦 } ) ) ) )
53	1 43 3 45 48 37	lspsnel5	⊢ ( ( ( 𝑊 ∈ 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 → ( 𝐵 ∈ 𝐽 ↔ ( 𝐵 ⊆ 𝑉 ∧ ( 𝑁 ‘ 𝐵 ) = 𝑉 ∧ ∀ 𝑥 ∈ 𝐵 ¬ 𝑥 ∈ ( 𝑁 ‘ ( 𝐵 ∖ { 𝑥 } ) ) ) ) )