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 } ) ¬ ( 𝑦 · 𝑥 ) ∈ ( 𝑁 ‘ ( 𝐵 ∖ { 𝑥 } ) ) ) ) ) |