Step | Hyp | Ref
| Expression |
1 | | elex 3185 |
. . . 4
⊢ (𝑊 ∈ 𝑋 → 𝑊 ∈ V) |
2 | | islbs.j |
. . . . 5
⊢ 𝐽 = (LBasis‘𝑊) |
3 | | fveq2 6103 |
. . . . . . . . 9
⊢ (𝑤 = 𝑊 → (Base‘𝑤) = (Base‘𝑊)) |
4 | | islbs.v |
. . . . . . . . 9
⊢ 𝑉 = (Base‘𝑊) |
5 | 3, 4 | syl6eqr 2662 |
. . . . . . . 8
⊢ (𝑤 = 𝑊 → (Base‘𝑤) = 𝑉) |
6 | 5 | pweqd 4113 |
. . . . . . 7
⊢ (𝑤 = 𝑊 → 𝒫 (Base‘𝑤) = 𝒫 𝑉) |
7 | | fvex 6113 |
. . . . . . . . 9
⊢
(LSpan‘𝑤)
∈ V |
8 | 7 | a1i 11 |
. . . . . . . 8
⊢ (𝑤 = 𝑊 → (LSpan‘𝑤) ∈ V) |
9 | | fveq2 6103 |
. . . . . . . . 9
⊢ (𝑤 = 𝑊 → (LSpan‘𝑤) = (LSpan‘𝑊)) |
10 | | islbs.n |
. . . . . . . . 9
⊢ 𝑁 = (LSpan‘𝑊) |
11 | 9, 10 | syl6eqr 2662 |
. . . . . . . 8
⊢ (𝑤 = 𝑊 → (LSpan‘𝑤) = 𝑁) |
12 | | fvex 6113 |
. . . . . . . . . 10
⊢
(Scalar‘𝑤)
∈ V |
13 | 12 | a1i 11 |
. . . . . . . . 9
⊢ ((𝑤 = 𝑊 ∧ 𝑛 = 𝑁) → (Scalar‘𝑤) ∈ V) |
14 | | fveq2 6103 |
. . . . . . . . . . 11
⊢ (𝑤 = 𝑊 → (Scalar‘𝑤) = (Scalar‘𝑊)) |
15 | 14 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝑤 = 𝑊 ∧ 𝑛 = 𝑁) → (Scalar‘𝑤) = (Scalar‘𝑊)) |
16 | | islbs.f |
. . . . . . . . . 10
⊢ 𝐹 = (Scalar‘𝑊) |
17 | 15, 16 | syl6eqr 2662 |
. . . . . . . . 9
⊢ ((𝑤 = 𝑊 ∧ 𝑛 = 𝑁) → (Scalar‘𝑤) = 𝐹) |
18 | | simplr 788 |
. . . . . . . . . . . 12
⊢ (((𝑤 = 𝑊 ∧ 𝑛 = 𝑁) ∧ 𝑓 = 𝐹) → 𝑛 = 𝑁) |
19 | 18 | fveq1d 6105 |
. . . . . . . . . . 11
⊢ (((𝑤 = 𝑊 ∧ 𝑛 = 𝑁) ∧ 𝑓 = 𝐹) → (𝑛‘𝑏) = (𝑁‘𝑏)) |
20 | 5 | ad2antrr 758 |
. . . . . . . . . . 11
⊢ (((𝑤 = 𝑊 ∧ 𝑛 = 𝑁) ∧ 𝑓 = 𝐹) → (Base‘𝑤) = 𝑉) |
21 | 19, 20 | eqeq12d 2625 |
. . . . . . . . . 10
⊢ (((𝑤 = 𝑊 ∧ 𝑛 = 𝑁) ∧ 𝑓 = 𝐹) → ((𝑛‘𝑏) = (Base‘𝑤) ↔ (𝑁‘𝑏) = 𝑉)) |
22 | | simpr 476 |
. . . . . . . . . . . . . . 15
⊢ (((𝑤 = 𝑊 ∧ 𝑛 = 𝑁) ∧ 𝑓 = 𝐹) → 𝑓 = 𝐹) |
23 | 22 | fveq2d 6107 |
. . . . . . . . . . . . . 14
⊢ (((𝑤 = 𝑊 ∧ 𝑛 = 𝑁) ∧ 𝑓 = 𝐹) → (Base‘𝑓) = (Base‘𝐹)) |
24 | | islbs.k |
. . . . . . . . . . . . . 14
⊢ 𝐾 = (Base‘𝐹) |
25 | 23, 24 | syl6eqr 2662 |
. . . . . . . . . . . . 13
⊢ (((𝑤 = 𝑊 ∧ 𝑛 = 𝑁) ∧ 𝑓 = 𝐹) → (Base‘𝑓) = 𝐾) |
26 | 22 | fveq2d 6107 |
. . . . . . . . . . . . . . 15
⊢ (((𝑤 = 𝑊 ∧ 𝑛 = 𝑁) ∧ 𝑓 = 𝐹) → (0g‘𝑓) = (0g‘𝐹)) |
27 | | islbs.z |
. . . . . . . . . . . . . . 15
⊢ 0 =
(0g‘𝐹) |
28 | 26, 27 | syl6eqr 2662 |
. . . . . . . . . . . . . 14
⊢ (((𝑤 = 𝑊 ∧ 𝑛 = 𝑁) ∧ 𝑓 = 𝐹) → (0g‘𝑓) = 0 ) |
29 | 28 | sneqd 4137 |
. . . . . . . . . . . . 13
⊢ (((𝑤 = 𝑊 ∧ 𝑛 = 𝑁) ∧ 𝑓 = 𝐹) → {(0g‘𝑓)} = { 0 }) |
30 | 25, 29 | difeq12d 3691 |
. . . . . . . . . . . 12
⊢ (((𝑤 = 𝑊 ∧ 𝑛 = 𝑁) ∧ 𝑓 = 𝐹) → ((Base‘𝑓) ∖ {(0g‘𝑓)}) = (𝐾 ∖ { 0 })) |
31 | | fveq2 6103 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑤 = 𝑊 → (
·𝑠 ‘𝑤) = ( ·𝑠
‘𝑊)) |
32 | | islbs.s |
. . . . . . . . . . . . . . . . 17
⊢ · = (
·𝑠 ‘𝑊) |
33 | 31, 32 | syl6eqr 2662 |
. . . . . . . . . . . . . . . 16
⊢ (𝑤 = 𝑊 → (
·𝑠 ‘𝑤) = · ) |
34 | 33 | ad2antrr 758 |
. . . . . . . . . . . . . . 15
⊢ (((𝑤 = 𝑊 ∧ 𝑛 = 𝑁) ∧ 𝑓 = 𝐹) → (
·𝑠 ‘𝑤) = · ) |
35 | 34 | oveqd 6566 |
. . . . . . . . . . . . . 14
⊢ (((𝑤 = 𝑊 ∧ 𝑛 = 𝑁) ∧ 𝑓 = 𝐹) → (𝑦( ·𝑠
‘𝑤)𝑥) = (𝑦 · 𝑥)) |
36 | 18 | fveq1d 6105 |
. . . . . . . . . . . . . 14
⊢ (((𝑤 = 𝑊 ∧ 𝑛 = 𝑁) ∧ 𝑓 = 𝐹) → (𝑛‘(𝑏 ∖ {𝑥})) = (𝑁‘(𝑏 ∖ {𝑥}))) |
37 | 35, 36 | eleq12d 2682 |
. . . . . . . . . . . . 13
⊢ (((𝑤 = 𝑊 ∧ 𝑛 = 𝑁) ∧ 𝑓 = 𝐹) → ((𝑦( ·𝑠
‘𝑤)𝑥) ∈ (𝑛‘(𝑏 ∖ {𝑥})) ↔ (𝑦 · 𝑥) ∈ (𝑁‘(𝑏 ∖ {𝑥})))) |
38 | 37 | notbid 307 |
. . . . . . . . . . . 12
⊢ (((𝑤 = 𝑊 ∧ 𝑛 = 𝑁) ∧ 𝑓 = 𝐹) → (¬ (𝑦( ·𝑠
‘𝑤)𝑥) ∈ (𝑛‘(𝑏 ∖ {𝑥})) ↔ ¬ (𝑦 · 𝑥) ∈ (𝑁‘(𝑏 ∖ {𝑥})))) |
39 | 30, 38 | raleqbidv 3129 |
. . . . . . . . . . 11
⊢ (((𝑤 = 𝑊 ∧ 𝑛 = 𝑁) ∧ 𝑓 = 𝐹) → (∀𝑦 ∈ ((Base‘𝑓) ∖ {(0g‘𝑓)}) ¬ (𝑦( ·𝑠
‘𝑤)𝑥) ∈ (𝑛‘(𝑏 ∖ {𝑥})) ↔ ∀𝑦 ∈ (𝐾 ∖ { 0 }) ¬ (𝑦 · 𝑥) ∈ (𝑁‘(𝑏 ∖ {𝑥})))) |
40 | 39 | ralbidv 2969 |
. . . . . . . . . 10
⊢ (((𝑤 = 𝑊 ∧ 𝑛 = 𝑁) ∧ 𝑓 = 𝐹) → (∀𝑥 ∈ 𝑏 ∀𝑦 ∈ ((Base‘𝑓) ∖ {(0g‘𝑓)}) ¬ (𝑦( ·𝑠
‘𝑤)𝑥) ∈ (𝑛‘(𝑏 ∖ {𝑥})) ↔ ∀𝑥 ∈ 𝑏 ∀𝑦 ∈ (𝐾 ∖ { 0 }) ¬ (𝑦 · 𝑥) ∈ (𝑁‘(𝑏 ∖ {𝑥})))) |
41 | 21, 40 | anbi12d 743 |
. . . . . . . . 9
⊢ (((𝑤 = 𝑊 ∧ 𝑛 = 𝑁) ∧ 𝑓 = 𝐹) → (((𝑛‘𝑏) = (Base‘𝑤) ∧ ∀𝑥 ∈ 𝑏 ∀𝑦 ∈ ((Base‘𝑓) ∖ {(0g‘𝑓)}) ¬ (𝑦( ·𝑠
‘𝑤)𝑥) ∈ (𝑛‘(𝑏 ∖ {𝑥}))) ↔ ((𝑁‘𝑏) = 𝑉 ∧ ∀𝑥 ∈ 𝑏 ∀𝑦 ∈ (𝐾 ∖ { 0 }) ¬ (𝑦 · 𝑥) ∈ (𝑁‘(𝑏 ∖ {𝑥}))))) |
42 | 13, 17, 41 | sbcied2 3440 |
. . . . . . . 8
⊢ ((𝑤 = 𝑊 ∧ 𝑛 = 𝑁) → ([(Scalar‘𝑤) / 𝑓]((𝑛‘𝑏) = (Base‘𝑤) ∧ ∀𝑥 ∈ 𝑏 ∀𝑦 ∈ ((Base‘𝑓) ∖ {(0g‘𝑓)}) ¬ (𝑦( ·𝑠
‘𝑤)𝑥) ∈ (𝑛‘(𝑏 ∖ {𝑥}))) ↔ ((𝑁‘𝑏) = 𝑉 ∧ ∀𝑥 ∈ 𝑏 ∀𝑦 ∈ (𝐾 ∖ { 0 }) ¬ (𝑦 · 𝑥) ∈ (𝑁‘(𝑏 ∖ {𝑥}))))) |
43 | 8, 11, 42 | sbcied2 3440 |
. . . . . . 7
⊢ (𝑤 = 𝑊 → ([(LSpan‘𝑤) / 𝑛][(Scalar‘𝑤) / 𝑓]((𝑛‘𝑏) = (Base‘𝑤) ∧ ∀𝑥 ∈ 𝑏 ∀𝑦 ∈ ((Base‘𝑓) ∖ {(0g‘𝑓)}) ¬ (𝑦( ·𝑠
‘𝑤)𝑥) ∈ (𝑛‘(𝑏 ∖ {𝑥}))) ↔ ((𝑁‘𝑏) = 𝑉 ∧ ∀𝑥 ∈ 𝑏 ∀𝑦 ∈ (𝐾 ∖ { 0 }) ¬ (𝑦 · 𝑥) ∈ (𝑁‘(𝑏 ∖ {𝑥}))))) |
44 | 6, 43 | rabeqbidv 3168 |
. . . . . 6
⊢ (𝑤 = 𝑊 → {𝑏 ∈ 𝒫 (Base‘𝑤) ∣
[(LSpan‘𝑤) /
𝑛][(Scalar‘𝑤) / 𝑓]((𝑛‘𝑏) = (Base‘𝑤) ∧ ∀𝑥 ∈ 𝑏 ∀𝑦 ∈ ((Base‘𝑓) ∖ {(0g‘𝑓)}) ¬ (𝑦( ·𝑠
‘𝑤)𝑥) ∈ (𝑛‘(𝑏 ∖ {𝑥})))} = {𝑏 ∈ 𝒫 𝑉 ∣ ((𝑁‘𝑏) = 𝑉 ∧ ∀𝑥 ∈ 𝑏 ∀𝑦 ∈ (𝐾 ∖ { 0 }) ¬ (𝑦 · 𝑥) ∈ (𝑁‘(𝑏 ∖ {𝑥})))}) |
45 | | df-lbs 18896 |
. . . . . 6
⊢ LBasis =
(𝑤 ∈ V ↦ {𝑏 ∈ 𝒫
(Base‘𝑤) ∣
[(LSpan‘𝑤) /
𝑛][(Scalar‘𝑤) / 𝑓]((𝑛‘𝑏) = (Base‘𝑤) ∧ ∀𝑥 ∈ 𝑏 ∀𝑦 ∈ ((Base‘𝑓) ∖ {(0g‘𝑓)}) ¬ (𝑦( ·𝑠
‘𝑤)𝑥) ∈ (𝑛‘(𝑏 ∖ {𝑥})))}) |
46 | | fvex 6113 |
. . . . . . . . 9
⊢
(Base‘𝑊)
∈ V |
47 | 4, 46 | eqeltri 2684 |
. . . . . . . 8
⊢ 𝑉 ∈ V |
48 | 47 | pwex 4774 |
. . . . . . 7
⊢ 𝒫
𝑉 ∈ V |
49 | 48 | rabex 4740 |
. . . . . 6
⊢ {𝑏 ∈ 𝒫 𝑉 ∣ ((𝑁‘𝑏) = 𝑉 ∧ ∀𝑥 ∈ 𝑏 ∀𝑦 ∈ (𝐾 ∖ { 0 }) ¬ (𝑦 · 𝑥) ∈ (𝑁‘(𝑏 ∖ {𝑥})))} ∈ V |
50 | 44, 45, 49 | fvmpt 6191 |
. . . . 5
⊢ (𝑊 ∈ V →
(LBasis‘𝑊) = {𝑏 ∈ 𝒫 𝑉 ∣ ((𝑁‘𝑏) = 𝑉 ∧ ∀𝑥 ∈ 𝑏 ∀𝑦 ∈ (𝐾 ∖ { 0 }) ¬ (𝑦 · 𝑥) ∈ (𝑁‘(𝑏 ∖ {𝑥})))}) |
51 | 2, 50 | syl5eq 2656 |
. . . 4
⊢ (𝑊 ∈ V → 𝐽 = {𝑏 ∈ 𝒫 𝑉 ∣ ((𝑁‘𝑏) = 𝑉 ∧ ∀𝑥 ∈ 𝑏 ∀𝑦 ∈ (𝐾 ∖ { 0 }) ¬ (𝑦 · 𝑥) ∈ (𝑁‘(𝑏 ∖ {𝑥})))}) |
52 | 1, 51 | syl 17 |
. . 3
⊢ (𝑊 ∈ 𝑋 → 𝐽 = {𝑏 ∈ 𝒫 𝑉 ∣ ((𝑁‘𝑏) = 𝑉 ∧ ∀𝑥 ∈ 𝑏 ∀𝑦 ∈ (𝐾 ∖ { 0 }) ¬ (𝑦 · 𝑥) ∈ (𝑁‘(𝑏 ∖ {𝑥})))}) |
53 | 52 | eleq2d 2673 |
. 2
⊢ (𝑊 ∈ 𝑋 → (𝐵 ∈ 𝐽 ↔ 𝐵 ∈ {𝑏 ∈ 𝒫 𝑉 ∣ ((𝑁‘𝑏) = 𝑉 ∧ ∀𝑥 ∈ 𝑏 ∀𝑦 ∈ (𝐾 ∖ { 0 }) ¬ (𝑦 · 𝑥) ∈ (𝑁‘(𝑏 ∖ {𝑥})))})) |
54 | 47 | elpw2 4755 |
. . . 4
⊢ (𝐵 ∈ 𝒫 𝑉 ↔ 𝐵 ⊆ 𝑉) |
55 | 54 | anbi1i 727 |
. . 3
⊢ ((𝐵 ∈ 𝒫 𝑉 ∧ ((𝑁‘𝐵) = 𝑉 ∧ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ (𝐾 ∖ { 0 }) ¬ (𝑦 · 𝑥) ∈ (𝑁‘(𝐵 ∖ {𝑥})))) ↔ (𝐵 ⊆ 𝑉 ∧ ((𝑁‘𝐵) = 𝑉 ∧ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ (𝐾 ∖ { 0 }) ¬ (𝑦 · 𝑥) ∈ (𝑁‘(𝐵 ∖ {𝑥}))))) |
56 | | fveq2 6103 |
. . . . . 6
⊢ (𝑏 = 𝐵 → (𝑁‘𝑏) = (𝑁‘𝐵)) |
57 | 56 | eqeq1d 2612 |
. . . . 5
⊢ (𝑏 = 𝐵 → ((𝑁‘𝑏) = 𝑉 ↔ (𝑁‘𝐵) = 𝑉)) |
58 | | difeq1 3683 |
. . . . . . . . . 10
⊢ (𝑏 = 𝐵 → (𝑏 ∖ {𝑥}) = (𝐵 ∖ {𝑥})) |
59 | 58 | fveq2d 6107 |
. . . . . . . . 9
⊢ (𝑏 = 𝐵 → (𝑁‘(𝑏 ∖ {𝑥})) = (𝑁‘(𝐵 ∖ {𝑥}))) |
60 | 59 | eleq2d 2673 |
. . . . . . . 8
⊢ (𝑏 = 𝐵 → ((𝑦 · 𝑥) ∈ (𝑁‘(𝑏 ∖ {𝑥})) ↔ (𝑦 · 𝑥) ∈ (𝑁‘(𝐵 ∖ {𝑥})))) |
61 | 60 | notbid 307 |
. . . . . . 7
⊢ (𝑏 = 𝐵 → (¬ (𝑦 · 𝑥) ∈ (𝑁‘(𝑏 ∖ {𝑥})) ↔ ¬ (𝑦 · 𝑥) ∈ (𝑁‘(𝐵 ∖ {𝑥})))) |
62 | 61 | ralbidv 2969 |
. . . . . 6
⊢ (𝑏 = 𝐵 → (∀𝑦 ∈ (𝐾 ∖ { 0 }) ¬ (𝑦 · 𝑥) ∈ (𝑁‘(𝑏 ∖ {𝑥})) ↔ ∀𝑦 ∈ (𝐾 ∖ { 0 }) ¬ (𝑦 · 𝑥) ∈ (𝑁‘(𝐵 ∖ {𝑥})))) |
63 | 62 | raleqbi1dv 3123 |
. . . . 5
⊢ (𝑏 = 𝐵 → (∀𝑥 ∈ 𝑏 ∀𝑦 ∈ (𝐾 ∖ { 0 }) ¬ (𝑦 · 𝑥) ∈ (𝑁‘(𝑏 ∖ {𝑥})) ↔ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ (𝐾 ∖ { 0 }) ¬ (𝑦 · 𝑥) ∈ (𝑁‘(𝐵 ∖ {𝑥})))) |
64 | 57, 63 | anbi12d 743 |
. . . 4
⊢ (𝑏 = 𝐵 → (((𝑁‘𝑏) = 𝑉 ∧ ∀𝑥 ∈ 𝑏 ∀𝑦 ∈ (𝐾 ∖ { 0 }) ¬ (𝑦 · 𝑥) ∈ (𝑁‘(𝑏 ∖ {𝑥}))) ↔ ((𝑁‘𝐵) = 𝑉 ∧ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ (𝐾 ∖ { 0 }) ¬ (𝑦 · 𝑥) ∈ (𝑁‘(𝐵 ∖ {𝑥}))))) |
65 | 64 | elrab 3331 |
. . 3
⊢ (𝐵 ∈ {𝑏 ∈ 𝒫 𝑉 ∣ ((𝑁‘𝑏) = 𝑉 ∧ ∀𝑥 ∈ 𝑏 ∀𝑦 ∈ (𝐾 ∖ { 0 }) ¬ (𝑦 · 𝑥) ∈ (𝑁‘(𝑏 ∖ {𝑥})))} ↔ (𝐵 ∈ 𝒫 𝑉 ∧ ((𝑁‘𝐵) = 𝑉 ∧ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ (𝐾 ∖ { 0 }) ¬ (𝑦 · 𝑥) ∈ (𝑁‘(𝐵 ∖ {𝑥}))))) |
66 | | 3anass 1035 |
. . 3
⊢ ((𝐵 ⊆ 𝑉 ∧ (𝑁‘𝐵) = 𝑉 ∧ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ (𝐾 ∖ { 0 }) ¬ (𝑦 · 𝑥) ∈ (𝑁‘(𝐵 ∖ {𝑥}))) ↔ (𝐵 ⊆ 𝑉 ∧ ((𝑁‘𝐵) = 𝑉 ∧ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ (𝐾 ∖ { 0 }) ¬ (𝑦 · 𝑥) ∈ (𝑁‘(𝐵 ∖ {𝑥}))))) |
67 | 55, 65, 66 | 3bitr4i 291 |
. 2
⊢ (𝐵 ∈ {𝑏 ∈ 𝒫 𝑉 ∣ ((𝑁‘𝑏) = 𝑉 ∧ ∀𝑥 ∈ 𝑏 ∀𝑦 ∈ (𝐾 ∖ { 0 }) ¬ (𝑦 · 𝑥) ∈ (𝑁‘(𝑏 ∖ {𝑥})))} ↔ (𝐵 ⊆ 𝑉 ∧ (𝑁‘𝐵) = 𝑉 ∧ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ (𝐾 ∖ { 0 }) ¬ (𝑦 · 𝑥) ∈ (𝑁‘(𝐵 ∖ {𝑥})))) |
68 | 53, 67 | syl6bb 275 |
1
⊢ (𝑊 ∈ 𝑋 → (𝐵 ∈ 𝐽 ↔ (𝐵 ⊆ 𝑉 ∧ (𝑁‘𝐵) = 𝑉 ∧ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ (𝐾 ∖ { 0 }) ¬ (𝑦 · 𝑥) ∈ (𝑁‘(𝐵 ∖ {𝑥}))))) |