Metamath Proof Explorer

Theorem islbs

Description: The predicate " B is a basis for the left module or vector space W ". A subset of the base set is a basis if zero is not in the set, it spans the set, and no nonzero multiple of an element of the basis is in the span of the rest of the family. (Contributed by Mario Carneiro, 24-Jun-2014) (Revised by Mario Carneiro, 14-Jan-2015)

Ref Expression
Hypotheses islbs.v ⊢ 𝑉 = ( Base ‘ 𝑊 )
islbs.f ⊢ 𝐹 = ( Scalar ‘ 𝑊 )
islbs.s ⊢ · = ( ·𝑠 ‘ 𝑊 )
islbs.k ⊢ 𝐾 = ( Base ‘ 𝐹 )
islbs.j ⊢ 𝐽 = ( LBasis ‘ 𝑊 )
islbs.n ⊢ 𝑁 = ( LSpan ‘ 𝑊 )
islbs.z ⊢ 0 = ( 0g ‘ 𝐹 )
Assertion islbs ( 𝑊 ∈ 𝑋 → ( 𝐵 ∈ 𝐽 ↔ ( 𝐵 ⊆ 𝑉 ∧ ( 𝑁 ‘ 𝐵 ) = 𝑉 ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ ( 𝐾 ∖ { 0 } ) ¬ ( 𝑦 · 𝑥 ) ∈ ( 𝑁 ‘ ( 𝐵 ∖ { 𝑥 } ) ) ) ) )

Proof

Step Hyp Ref Expression
1 islbs.v ⊢ 𝑉 = ( Base ‘ 𝑊 )
2 islbs.f ⊢ 𝐹 = ( Scalar ‘ 𝑊 )
3 islbs.s ⊢ · = ( ·𝑠 ‘ 𝑊 )
4 islbs.k ⊢ 𝐾 = ( Base ‘ 𝐹 )
5 islbs.j ⊢ 𝐽 = ( LBasis ‘ 𝑊 )
6 islbs.n ⊢ 𝑁 = ( LSpan ‘ 𝑊 )
7 islbs.z ⊢ 0 = ( 0g ‘ 𝐹 )
8 elex ⊢ ( 𝑊 ∈ 𝑋 → 𝑊 ∈ V )
9 fveq2 ⊢ ( 𝑤 = 𝑊 → ( Base ‘ 𝑤 ) = ( Base ‘ 𝑊 ) )
10 9 1 eqtr4di ⊢ ( 𝑤 = 𝑊 → ( Base ‘ 𝑤 ) = 𝑉 )
11 10 pweqd ⊢ ( 𝑤 = 𝑊 → 𝒫 ( Base ‘ 𝑤 ) = 𝒫 𝑉 )
12 fvexd ⊢ ( 𝑤 = 𝑊 → ( LSpan ‘ 𝑤 ) ∈ V )
13 fveq2 ⊢ ( 𝑤 = 𝑊 → ( LSpan ‘ 𝑤 ) = ( LSpan ‘ 𝑊 ) )
14 13 6 eqtr4di ⊢ ( 𝑤 = 𝑊 → ( LSpan ‘ 𝑤 ) = 𝑁 )
15 fvexd ⊢ ( ( 𝑤 = 𝑊 ∧ 𝑛 = 𝑁 ) → ( Scalar ‘ 𝑤 ) ∈ V )
16 fveq2 ⊢ ( 𝑤 = 𝑊 → ( Scalar ‘ 𝑤 ) = ( Scalar ‘ 𝑊 ) )
17 16 adantr ⊢ ( ( 𝑤 = 𝑊 ∧ 𝑛 = 𝑁 ) → ( Scalar ‘ 𝑤 ) = ( Scalar ‘ 𝑊 ) )
18 17 2 eqtr4di ⊢ ( ( 𝑤 = 𝑊 ∧ 𝑛 = 𝑁 ) → ( Scalar ‘ 𝑤 ) = 𝐹 )
19 simplr ⊢ ( ( ( 𝑤 = 𝑊 ∧ 𝑛 = 𝑁 ) ∧ 𝑓 = 𝐹 ) → 𝑛 = 𝑁 )
20 19 fveq1d ⊢ ( ( ( 𝑤 = 𝑊 ∧ 𝑛 = 𝑁 ) ∧ 𝑓 = 𝐹 ) → ( 𝑛 ‘ 𝑏 ) = ( 𝑁 ‘ 𝑏 ) )
21 10 ad2antrr ⊢ ( ( ( 𝑤 = 𝑊 ∧ 𝑛 = 𝑁 ) ∧ 𝑓 = 𝐹 ) → ( Base ‘ 𝑤 ) = 𝑉 )
22 20 21 eqeq12d ⊢ ( ( ( 𝑤 = 𝑊 ∧ 𝑛 = 𝑁 ) ∧ 𝑓 = 𝐹 ) → ( ( 𝑛 ‘ 𝑏 ) = ( Base ‘ 𝑤 ) ↔ ( 𝑁 ‘ 𝑏 ) = 𝑉 ) )
23 simpr ⊢ ( ( ( 𝑤 = 𝑊 ∧ 𝑛 = 𝑁 ) ∧ 𝑓 = 𝐹 ) → 𝑓 = 𝐹 )
24 23 fveq2d ⊢ ( ( ( 𝑤 = 𝑊 ∧ 𝑛 = 𝑁 ) ∧ 𝑓 = 𝐹 ) → ( Base ‘ 𝑓 ) = ( Base ‘ 𝐹 ) )
25 24 4 eqtr4di ⊢ ( ( ( 𝑤 = 𝑊 ∧ 𝑛 = 𝑁 ) ∧ 𝑓 = 𝐹 ) → ( Base ‘ 𝑓 ) = 𝐾 )
26 23 fveq2d ⊢ ( ( ( 𝑤 = 𝑊 ∧ 𝑛 = 𝑁 ) ∧ 𝑓 = 𝐹 ) → ( 0g ‘ 𝑓 ) = ( 0g ‘ 𝐹 ) )
27 26 7 eqtr4di ⊢ ( ( ( 𝑤 = 𝑊 ∧ 𝑛 = 𝑁 ) ∧ 𝑓 = 𝐹 ) → ( 0g ‘ 𝑓 ) = 0 )
28 27 sneqd ⊢ ( ( ( 𝑤 = 𝑊 ∧ 𝑛 = 𝑁 ) ∧ 𝑓 = 𝐹 ) → { ( 0g ‘ 𝑓 ) } = { 0 } )
29 25 28 difeq12d ⊢ ( ( ( 𝑤 = 𝑊 ∧ 𝑛 = 𝑁 ) ∧ 𝑓 = 𝐹 ) → ( ( Base ‘ 𝑓 ) ∖ { ( 0g ‘ 𝑓 ) } ) = ( 𝐾 ∖ { 0 } ) )
30 fveq2 ⊢ ( 𝑤 = 𝑊 → ( ·𝑠 ‘ 𝑤 ) = ( ·𝑠 ‘ 𝑊 ) )
31 30 3 eqtr4di ⊢ ( 𝑤 = 𝑊 → ( ·𝑠 ‘ 𝑤 ) = · )
32 31 ad2antrr ⊢ ( ( ( 𝑤 = 𝑊 ∧ 𝑛 = 𝑁 ) ∧ 𝑓 = 𝐹 ) → ( ·𝑠 ‘ 𝑤 ) = · )
33 32 oveqd ⊢ ( ( ( 𝑤 = 𝑊 ∧ 𝑛 = 𝑁 ) ∧ 𝑓 = 𝐹 ) → ( 𝑦 ( ·𝑠 ‘ 𝑤 ) 𝑥 ) = ( 𝑦 · 𝑥 ) )
34 19 fveq1d ⊢ ( ( ( 𝑤 = 𝑊 ∧ 𝑛 = 𝑁 ) ∧ 𝑓 = 𝐹 ) → ( 𝑛 ‘ ( 𝑏 ∖ { 𝑥 } ) ) = ( 𝑁 ‘ ( 𝑏 ∖ { 𝑥 } ) ) )
35 33 34 eleq12d ⊢ ( ( ( 𝑤 = 𝑊 ∧ 𝑛 = 𝑁 ) ∧ 𝑓 = 𝐹 ) → ( ( 𝑦 ( ·𝑠 ‘ 𝑤 ) 𝑥 ) ∈ ( 𝑛 ‘ ( 𝑏 ∖ { 𝑥 } ) ) ↔ ( 𝑦 · 𝑥 ) ∈ ( 𝑁 ‘ ( 𝑏 ∖ { 𝑥 } ) ) ) )
36 35 notbid ⊢ ( ( ( 𝑤 = 𝑊 ∧ 𝑛 = 𝑁 ) ∧ 𝑓 = 𝐹 ) → ( ¬ ( 𝑦 ( ·𝑠 ‘ 𝑤 ) 𝑥 ) ∈ ( 𝑛 ‘ ( 𝑏 ∖ { 𝑥 } ) ) ↔ ¬ ( 𝑦 · 𝑥 ) ∈ ( 𝑁 ‘ ( 𝑏 ∖ { 𝑥 } ) ) ) )
37 29 36 raleqbidv ⊢ ( ( ( 𝑤 = 𝑊 ∧ 𝑛 = 𝑁 ) ∧ 𝑓 = 𝐹 ) → ( ∀ 𝑦 ∈ ( ( Base ‘ 𝑓 ) ∖ { ( 0g ‘ 𝑓 ) } ) ¬ ( 𝑦 ( ·𝑠 ‘ 𝑤 ) 𝑥 ) ∈ ( 𝑛 ‘ ( 𝑏 ∖ { 𝑥 } ) ) ↔ ∀ 𝑦 ∈ ( 𝐾 ∖ { 0 } ) ¬ ( 𝑦 · 𝑥 ) ∈ ( 𝑁 ‘ ( 𝑏 ∖ { 𝑥 } ) ) ) )
38 37 ralbidv ⊢ ( ( ( 𝑤 = 𝑊 ∧ 𝑛 = 𝑁 ) ∧ 𝑓 = 𝐹 ) → ( ∀ 𝑥 ∈ 𝑏 ∀ 𝑦 ∈ ( ( Base ‘ 𝑓 ) ∖ { ( 0g ‘ 𝑓 ) } ) ¬ ( 𝑦 ( ·𝑠 ‘ 𝑤 ) 𝑥 ) ∈ ( 𝑛 ‘ ( 𝑏 ∖ { 𝑥 } ) ) ↔ ∀ 𝑥 ∈ 𝑏 ∀ 𝑦 ∈ ( 𝐾 ∖ { 0 } ) ¬ ( 𝑦 · 𝑥 ) ∈ ( 𝑁 ‘ ( 𝑏 ∖ { 𝑥 } ) ) ) )
39 22 38 anbi12d ⊢ ( ( ( 𝑤 = 𝑊 ∧ 𝑛 = 𝑁 ) ∧ 𝑓 = 𝐹 ) → ( ( ( 𝑛 ‘ 𝑏 ) = ( Base ‘ 𝑤 ) ∧ ∀ 𝑥 ∈ 𝑏 ∀ 𝑦 ∈ ( ( Base ‘ 𝑓 ) ∖ { ( 0g ‘ 𝑓 ) } ) ¬ ( 𝑦 ( ·𝑠 ‘ 𝑤 ) 𝑥 ) ∈ ( 𝑛 ‘ ( 𝑏 ∖ { 𝑥 } ) ) ) ↔ ( ( 𝑁 ‘ 𝑏 ) = 𝑉 ∧ ∀ 𝑥 ∈ 𝑏 ∀ 𝑦 ∈ ( 𝐾 ∖ { 0 } ) ¬ ( 𝑦 · 𝑥 ) ∈ ( 𝑁 ‘ ( 𝑏 ∖ { 𝑥 } ) ) ) ) )
40 15 18 39 sbcied2 ⊢ ( ( 𝑤 = 𝑊 ∧ 𝑛 = 𝑁 ) → ( [ ( Scalar ‘ 𝑤 ) / 𝑓 ] ( ( 𝑛 ‘ 𝑏 ) = ( Base ‘ 𝑤 ) ∧ ∀ 𝑥 ∈ 𝑏 ∀ 𝑦 ∈ ( ( Base ‘ 𝑓 ) ∖ { ( 0g ‘ 𝑓 ) } ) ¬ ( 𝑦 ( ·𝑠 ‘ 𝑤 ) 𝑥 ) ∈ ( 𝑛 ‘ ( 𝑏 ∖ { 𝑥 } ) ) ) ↔ ( ( 𝑁 ‘ 𝑏 ) = 𝑉 ∧ ∀ 𝑥 ∈ 𝑏 ∀ 𝑦 ∈ ( 𝐾 ∖ { 0 } ) ¬ ( 𝑦 · 𝑥 ) ∈ ( 𝑁 ‘ ( 𝑏 ∖ { 𝑥 } ) ) ) ) )
41 12 14 40 sbcied2 ⊢ ( 𝑤 = 𝑊 → ( [ ( LSpan ‘ 𝑤 ) / 𝑛 ] [ ( Scalar ‘ 𝑤 ) / 𝑓 ] ( ( 𝑛 ‘ 𝑏 ) = ( Base ‘ 𝑤 ) ∧ ∀ 𝑥 ∈ 𝑏 ∀ 𝑦 ∈ ( ( Base ‘ 𝑓 ) ∖ { ( 0g ‘ 𝑓 ) } ) ¬ ( 𝑦 ( ·𝑠 ‘ 𝑤 ) 𝑥 ) ∈ ( 𝑛 ‘ ( 𝑏 ∖ { 𝑥 } ) ) ) ↔ ( ( 𝑁 ‘ 𝑏 ) = 𝑉 ∧ ∀ 𝑥 ∈ 𝑏 ∀ 𝑦 ∈ ( 𝐾 ∖ { 0 } ) ¬ ( 𝑦 · 𝑥 ) ∈ ( 𝑁 ‘ ( 𝑏 ∖ { 𝑥 } ) ) ) ) )
42 11 41 rabeqbidv ⊢ ( 𝑤 = 𝑊 → { 𝑏 ∈ 𝒫 ( Base ‘ 𝑤 ) ∣ [ ( LSpan ‘ 𝑤 ) / 𝑛 ] [ ( Scalar ‘ 𝑤 ) / 𝑓 ] ( ( 𝑛 ‘ 𝑏 ) = ( Base ‘ 𝑤 ) ∧ ∀ 𝑥 ∈ 𝑏 ∀ 𝑦 ∈ ( ( Base ‘ 𝑓 ) ∖ { ( 0g ‘ 𝑓 ) } ) ¬ ( 𝑦 ( ·𝑠 ‘ 𝑤 ) 𝑥 ) ∈ ( 𝑛 ‘ ( 𝑏 ∖ { 𝑥 } ) ) ) } = { 𝑏 ∈ 𝒫 𝑉 ∣ ( ( 𝑁 ‘ 𝑏 ) = 𝑉 ∧ ∀ 𝑥 ∈ 𝑏 ∀ 𝑦 ∈ ( 𝐾 ∖ { 0 } ) ¬ ( 𝑦 · 𝑥 ) ∈ ( 𝑁 ‘ ( 𝑏 ∖ { 𝑥 } ) ) ) } )
43 df-lbs ⊢ LBasis = ( 𝑤 ∈ V ↦ { 𝑏 ∈ 𝒫 ( Base ‘ 𝑤 ) ∣ [ ( LSpan ‘ 𝑤 ) / 𝑛 ] [ ( Scalar ‘ 𝑤 ) / 𝑓 ] ( ( 𝑛 ‘ 𝑏 ) = ( Base ‘ 𝑤 ) ∧ ∀ 𝑥 ∈ 𝑏 ∀ 𝑦 ∈ ( ( Base ‘ 𝑓 ) ∖ { ( 0g ‘ 𝑓 ) } ) ¬ ( 𝑦 ( ·𝑠 ‘ 𝑤 ) 𝑥 ) ∈ ( 𝑛 ‘ ( 𝑏 ∖ { 𝑥 } ) ) ) } )
44 1 fvexi ⊢ 𝑉 ∈ V
45 44 pwex ⊢ 𝒫 𝑉 ∈ V
46 45 rabex ⊢ { 𝑏 ∈ 𝒫 𝑉 ∣ ( ( 𝑁 ‘ 𝑏 ) = 𝑉 ∧ ∀ 𝑥 ∈ 𝑏 ∀ 𝑦 ∈ ( 𝐾 ∖ { 0 } ) ¬ ( 𝑦 · 𝑥 ) ∈ ( 𝑁 ‘ ( 𝑏 ∖ { 𝑥 } ) ) ) } ∈ V
47 42 43 46 fvmpt ⊢ ( 𝑊 ∈ V → ( LBasis ‘ 𝑊 ) = { 𝑏 ∈ 𝒫 𝑉 ∣ ( ( 𝑁 ‘ 𝑏 ) = 𝑉 ∧ ∀ 𝑥 ∈ 𝑏 ∀ 𝑦 ∈ ( 𝐾 ∖ { 0 } ) ¬ ( 𝑦 · 𝑥 ) ∈ ( 𝑁 ‘ ( 𝑏 ∖ { 𝑥 } ) ) ) } )
48 5 47 syl5eq ⊢ ( 𝑊 ∈ V → 𝐽 = { 𝑏 ∈ 𝒫 𝑉 ∣ ( ( 𝑁 ‘ 𝑏 ) = 𝑉 ∧ ∀ 𝑥 ∈ 𝑏 ∀ 𝑦 ∈ ( 𝐾 ∖ { 0 } ) ¬ ( 𝑦 · 𝑥 ) ∈ ( 𝑁 ‘ ( 𝑏 ∖ { 𝑥 } ) ) ) } )
49 8 48 syl ⊢ ( 𝑊 ∈ 𝑋 → 𝐽 = { 𝑏 ∈ 𝒫 𝑉 ∣ ( ( 𝑁 ‘ 𝑏 ) = 𝑉 ∧ ∀ 𝑥 ∈ 𝑏 ∀ 𝑦 ∈ ( 𝐾 ∖ { 0 } ) ¬ ( 𝑦 · 𝑥 ) ∈ ( 𝑁 ‘ ( 𝑏 ∖ { 𝑥 } ) ) ) } )
50 49 eleq2d ⊢ ( 𝑊 ∈ 𝑋 → ( 𝐵 ∈ 𝐽 ↔ 𝐵 ∈ { 𝑏 ∈ 𝒫 𝑉 ∣ ( ( 𝑁 ‘ 𝑏 ) = 𝑉 ∧ ∀ 𝑥 ∈ 𝑏 ∀ 𝑦 ∈ ( 𝐾 ∖ { 0 } ) ¬ ( 𝑦 · 𝑥 ) ∈ ( 𝑁 ‘ ( 𝑏 ∖ { 𝑥 } ) ) ) } ) )
51 44 elpw2 ⊢ ( 𝐵 ∈ 𝒫 𝑉 ↔ 𝐵 ⊆ 𝑉 )
52 51 anbi1i ⊢ ( ( 𝐵 ∈ 𝒫 𝑉 ∧ ( ( 𝑁 ‘ 𝐵 ) = 𝑉 ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ ( 𝐾 ∖ { 0 } ) ¬ ( 𝑦 · 𝑥 ) ∈ ( 𝑁 ‘ ( 𝐵 ∖ { 𝑥 } ) ) ) ) ↔ ( 𝐵 ⊆ 𝑉 ∧ ( ( 𝑁 ‘ 𝐵 ) = 𝑉 ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ ( 𝐾 ∖ { 0 } ) ¬ ( 𝑦 · 𝑥 ) ∈ ( 𝑁 ‘ ( 𝐵 ∖ { 𝑥 } ) ) ) ) )
53 fveqeq2 ⊢ ( 𝑏 = 𝐵 → ( ( 𝑁 ‘ 𝑏 ) = 𝑉 ↔ ( 𝑁 ‘ 𝐵 ) = 𝑉 ) )
54 difeq1 ⊢ ( 𝑏 = 𝐵 → ( 𝑏 ∖ { 𝑥 } ) = ( 𝐵 ∖ { 𝑥 } ) )
55 54 fveq2d ⊢ ( 𝑏 = 𝐵 → ( 𝑁 ‘ ( 𝑏 ∖ { 𝑥 } ) ) = ( 𝑁 ‘ ( 𝐵 ∖ { 𝑥 } ) ) )
56 55 eleq2d ⊢ ( 𝑏 = 𝐵 → ( ( 𝑦 · 𝑥 ) ∈ ( 𝑁 ‘ ( 𝑏 ∖ { 𝑥 } ) ) ↔ ( 𝑦 · 𝑥 ) ∈ ( 𝑁 ‘ ( 𝐵 ∖ { 𝑥 } ) ) ) )
57 56 notbid ⊢ ( 𝑏 = 𝐵 → ( ¬ ( 𝑦 · 𝑥 ) ∈ ( 𝑁 ‘ ( 𝑏 ∖ { 𝑥 } ) ) ↔ ¬ ( 𝑦 · 𝑥 ) ∈ ( 𝑁 ‘ ( 𝐵 ∖ { 𝑥 } ) ) ) )
58 57 ralbidv ⊢ ( 𝑏 = 𝐵 → ( ∀ 𝑦 ∈ ( 𝐾 ∖ { 0 } ) ¬ ( 𝑦 · 𝑥 ) ∈ ( 𝑁 ‘ ( 𝑏 ∖ { 𝑥 } ) ) ↔ ∀ 𝑦 ∈ ( 𝐾 ∖ { 0 } ) ¬ ( 𝑦 · 𝑥 ) ∈ ( 𝑁 ‘ ( 𝐵 ∖ { 𝑥 } ) ) ) )
59 58 raleqbi1dv ⊢ ( 𝑏 = 𝐵 → ( ∀ 𝑥 ∈ 𝑏 ∀ 𝑦 ∈ ( 𝐾 ∖ { 0 } ) ¬ ( 𝑦 · 𝑥 ) ∈ ( 𝑁 ‘ ( 𝑏 ∖ { 𝑥 } ) ) ↔ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ ( 𝐾 ∖ { 0 } ) ¬ ( 𝑦 · 𝑥 ) ∈ ( 𝑁 ‘ ( 𝐵 ∖ { 𝑥 } ) ) ) )
60 53 59 anbi12d ⊢ ( 𝑏 = 𝐵 → ( ( ( 𝑁 ‘ 𝑏 ) = 𝑉 ∧ ∀ 𝑥 ∈ 𝑏 ∀ 𝑦 ∈ ( 𝐾 ∖ { 0 } ) ¬ ( 𝑦 · 𝑥 ) ∈ ( 𝑁 ‘ ( 𝑏 ∖ { 𝑥 } ) ) ) ↔ ( ( 𝑁 ‘ 𝐵 ) = 𝑉 ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ ( 𝐾 ∖ { 0 } ) ¬ ( 𝑦 · 𝑥 ) ∈ ( 𝑁 ‘ ( 𝐵 ∖ { 𝑥 } ) ) ) ) )
61 60 elrab ⊢ ( 𝐵 ∈ { 𝑏 ∈ 𝒫 𝑉 ∣ ( ( 𝑁 ‘ 𝑏 ) = 𝑉 ∧ ∀ 𝑥 ∈ 𝑏 ∀ 𝑦 ∈ ( 𝐾 ∖ { 0 } ) ¬ ( 𝑦 · 𝑥 ) ∈ ( 𝑁 ‘ ( 𝑏 ∖ { 𝑥 } ) ) ) } ↔ ( 𝐵 ∈ 𝒫 𝑉 ∧ ( ( 𝑁 ‘ 𝐵 ) = 𝑉 ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ ( 𝐾 ∖ { 0 } ) ¬ ( 𝑦 · 𝑥 ) ∈ ( 𝑁 ‘ ( 𝐵 ∖ { 𝑥 } ) ) ) ) )
62 3anass ⊢ ( ( 𝐵 ⊆ 𝑉 ∧ ( 𝑁 ‘ 𝐵 ) = 𝑉 ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ ( 𝐾 ∖ { 0 } ) ¬ ( 𝑦 · 𝑥 ) ∈ ( 𝑁 ‘ ( 𝐵 ∖ { 𝑥 } ) ) ) ↔ ( 𝐵 ⊆ 𝑉 ∧ ( ( 𝑁 ‘ 𝐵 ) = 𝑉 ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ ( 𝐾 ∖ { 0 } ) ¬ ( 𝑦 · 𝑥 ) ∈ ( 𝑁 ‘ ( 𝐵 ∖ { 𝑥 } ) ) ) ) )
63 52 61 62 3bitr4i ⊢ ( 𝐵 ∈ { 𝑏 ∈ 𝒫 𝑉 ∣ ( ( 𝑁 ‘ 𝑏 ) = 𝑉 ∧ ∀ 𝑥 ∈ 𝑏 ∀ 𝑦 ∈ ( 𝐾 ∖ { 0 } ) ¬ ( 𝑦 · 𝑥 ) ∈ ( 𝑁 ‘ ( 𝑏 ∖ { 𝑥 } ) ) ) } ↔ ( 𝐵 ⊆ 𝑉 ∧ ( 𝑁 ‘ 𝐵 ) = 𝑉 ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ ( 𝐾 ∖ { 0 } ) ¬ ( 𝑦 · 𝑥 ) ∈ ( 𝑁 ‘ ( 𝐵 ∖ { 𝑥 } ) ) ) )
64 50 63 bitrdi ⊢ ( 𝑊 ∈ 𝑋 → ( 𝐵 ∈ 𝐽 ↔ ( 𝐵 ⊆ 𝑉 ∧ ( 𝑁 ‘ 𝐵 ) = 𝑉 ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ ( 𝐾 ∖ { 0 } ) ¬ ( 𝑦 · 𝑥 ) ∈ ( 𝑁 ‘ ( 𝐵 ∖ { 𝑥 } ) ) ) ) )