| Step | Hyp | Ref
| Expression |
| 1 | | elex 3501 |
. . . 4
⊢ (𝑊 ∈ 𝑋 → 𝑊 ∈ V) |
| 2 | | islbs.j |
. . . . 5
⊢ 𝐽 = (LBasis‘𝑊) |
| 3 | | fveq2 6906 |
. . . . . . . . 9
⊢ (𝑤 = 𝑊 → (Base‘𝑤) = (Base‘𝑊)) |
| 4 | | islbs.v |
. . . . . . . . 9
⊢ 𝑉 = (Base‘𝑊) |
| 5 | 3, 4 | eqtr4di 2795 |
. . . . . . . 8
⊢ (𝑤 = 𝑊 → (Base‘𝑤) = 𝑉) |
| 6 | 5 | pweqd 4617 |
. . . . . . 7
⊢ (𝑤 = 𝑊 → 𝒫 (Base‘𝑤) = 𝒫 𝑉) |
| 7 | | fvexd 6921 |
. . . . . . . 8
⊢ (𝑤 = 𝑊 → (LSpan‘𝑤) ∈ V) |
| 8 | | fveq2 6906 |
. . . . . . . . 9
⊢ (𝑤 = 𝑊 → (LSpan‘𝑤) = (LSpan‘𝑊)) |
| 9 | | islbs.n |
. . . . . . . . 9
⊢ 𝑁 = (LSpan‘𝑊) |
| 10 | 8, 9 | eqtr4di 2795 |
. . . . . . . 8
⊢ (𝑤 = 𝑊 → (LSpan‘𝑤) = 𝑁) |
| 11 | | fvexd 6921 |
. . . . . . . . 9
⊢ ((𝑤 = 𝑊 ∧ 𝑛 = 𝑁) → (Scalar‘𝑤) ∈ V) |
| 12 | | fveq2 6906 |
. . . . . . . . . . 11
⊢ (𝑤 = 𝑊 → (Scalar‘𝑤) = (Scalar‘𝑊)) |
| 13 | 12 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝑤 = 𝑊 ∧ 𝑛 = 𝑁) → (Scalar‘𝑤) = (Scalar‘𝑊)) |
| 14 | | islbs.f |
. . . . . . . . . 10
⊢ 𝐹 = (Scalar‘𝑊) |
| 15 | 13, 14 | eqtr4di 2795 |
. . . . . . . . 9
⊢ ((𝑤 = 𝑊 ∧ 𝑛 = 𝑁) → (Scalar‘𝑤) = 𝐹) |
| 16 | | simplr 769 |
. . . . . . . . . . . 12
⊢ (((𝑤 = 𝑊 ∧ 𝑛 = 𝑁) ∧ 𝑓 = 𝐹) → 𝑛 = 𝑁) |
| 17 | 16 | fveq1d 6908 |
. . . . . . . . . . 11
⊢ (((𝑤 = 𝑊 ∧ 𝑛 = 𝑁) ∧ 𝑓 = 𝐹) → (𝑛‘𝑏) = (𝑁‘𝑏)) |
| 18 | 5 | ad2antrr 726 |
. . . . . . . . . . 11
⊢ (((𝑤 = 𝑊 ∧ 𝑛 = 𝑁) ∧ 𝑓 = 𝐹) → (Base‘𝑤) = 𝑉) |
| 19 | 17, 18 | eqeq12d 2753 |
. . . . . . . . . 10
⊢ (((𝑤 = 𝑊 ∧ 𝑛 = 𝑁) ∧ 𝑓 = 𝐹) → ((𝑛‘𝑏) = (Base‘𝑤) ↔ (𝑁‘𝑏) = 𝑉)) |
| 20 | | simpr 484 |
. . . . . . . . . . . . . . 15
⊢ (((𝑤 = 𝑊 ∧ 𝑛 = 𝑁) ∧ 𝑓 = 𝐹) → 𝑓 = 𝐹) |
| 21 | 20 | fveq2d 6910 |
. . . . . . . . . . . . . 14
⊢ (((𝑤 = 𝑊 ∧ 𝑛 = 𝑁) ∧ 𝑓 = 𝐹) → (Base‘𝑓) = (Base‘𝐹)) |
| 22 | | islbs.k |
. . . . . . . . . . . . . 14
⊢ 𝐾 = (Base‘𝐹) |
| 23 | 21, 22 | eqtr4di 2795 |
. . . . . . . . . . . . 13
⊢ (((𝑤 = 𝑊 ∧ 𝑛 = 𝑁) ∧ 𝑓 = 𝐹) → (Base‘𝑓) = 𝐾) |
| 24 | 20 | fveq2d 6910 |
. . . . . . . . . . . . . . 15
⊢ (((𝑤 = 𝑊 ∧ 𝑛 = 𝑁) ∧ 𝑓 = 𝐹) → (0g‘𝑓) = (0g‘𝐹)) |
| 25 | | islbs.z |
. . . . . . . . . . . . . . 15
⊢ 0 =
(0g‘𝐹) |
| 26 | 24, 25 | eqtr4di 2795 |
. . . . . . . . . . . . . 14
⊢ (((𝑤 = 𝑊 ∧ 𝑛 = 𝑁) ∧ 𝑓 = 𝐹) → (0g‘𝑓) = 0 ) |
| 27 | 26 | sneqd 4638 |
. . . . . . . . . . . . 13
⊢ (((𝑤 = 𝑊 ∧ 𝑛 = 𝑁) ∧ 𝑓 = 𝐹) → {(0g‘𝑓)} = { 0 }) |
| 28 | 23, 27 | difeq12d 4127 |
. . . . . . . . . . . 12
⊢ (((𝑤 = 𝑊 ∧ 𝑛 = 𝑁) ∧ 𝑓 = 𝐹) → ((Base‘𝑓) ∖ {(0g‘𝑓)}) = (𝐾 ∖ { 0 })) |
| 29 | | fveq2 6906 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑤 = 𝑊 → (
·𝑠 ‘𝑤) = ( ·𝑠
‘𝑊)) |
| 30 | | islbs.s |
. . . . . . . . . . . . . . . . 17
⊢ · = (
·𝑠 ‘𝑊) |
| 31 | 29, 30 | eqtr4di 2795 |
. . . . . . . . . . . . . . . 16
⊢ (𝑤 = 𝑊 → (
·𝑠 ‘𝑤) = · ) |
| 32 | 31 | ad2antrr 726 |
. . . . . . . . . . . . . . 15
⊢ (((𝑤 = 𝑊 ∧ 𝑛 = 𝑁) ∧ 𝑓 = 𝐹) → (
·𝑠 ‘𝑤) = · ) |
| 33 | 32 | oveqd 7448 |
. . . . . . . . . . . . . 14
⊢ (((𝑤 = 𝑊 ∧ 𝑛 = 𝑁) ∧ 𝑓 = 𝐹) → (𝑦( ·𝑠
‘𝑤)𝑥) = (𝑦 · 𝑥)) |
| 34 | 16 | fveq1d 6908 |
. . . . . . . . . . . . . 14
⊢ (((𝑤 = 𝑊 ∧ 𝑛 = 𝑁) ∧ 𝑓 = 𝐹) → (𝑛‘(𝑏 ∖ {𝑥})) = (𝑁‘(𝑏 ∖ {𝑥}))) |
| 35 | 33, 34 | eleq12d 2835 |
. . . . . . . . . . . . 13
⊢ (((𝑤 = 𝑊 ∧ 𝑛 = 𝑁) ∧ 𝑓 = 𝐹) → ((𝑦( ·𝑠
‘𝑤)𝑥) ∈ (𝑛‘(𝑏 ∖ {𝑥})) ↔ (𝑦 · 𝑥) ∈ (𝑁‘(𝑏 ∖ {𝑥})))) |
| 36 | 35 | notbid 318 |
. . . . . . . . . . . 12
⊢ (((𝑤 = 𝑊 ∧ 𝑛 = 𝑁) ∧ 𝑓 = 𝐹) → (¬ (𝑦( ·𝑠
‘𝑤)𝑥) ∈ (𝑛‘(𝑏 ∖ {𝑥})) ↔ ¬ (𝑦 · 𝑥) ∈ (𝑁‘(𝑏 ∖ {𝑥})))) |
| 37 | 28, 36 | raleqbidv 3346 |
. . . . . . . . . . 11
⊢ (((𝑤 = 𝑊 ∧ 𝑛 = 𝑁) ∧ 𝑓 = 𝐹) → (∀𝑦 ∈ ((Base‘𝑓) ∖ {(0g‘𝑓)}) ¬ (𝑦( ·𝑠
‘𝑤)𝑥) ∈ (𝑛‘(𝑏 ∖ {𝑥})) ↔ ∀𝑦 ∈ (𝐾 ∖ { 0 }) ¬ (𝑦 · 𝑥) ∈ (𝑁‘(𝑏 ∖ {𝑥})))) |
| 38 | 37 | ralbidv 3178 |
. . . . . . . . . 10
⊢ (((𝑤 = 𝑊 ∧ 𝑛 = 𝑁) ∧ 𝑓 = 𝐹) → (∀𝑥 ∈ 𝑏 ∀𝑦 ∈ ((Base‘𝑓) ∖ {(0g‘𝑓)}) ¬ (𝑦( ·𝑠
‘𝑤)𝑥) ∈ (𝑛‘(𝑏 ∖ {𝑥})) ↔ ∀𝑥 ∈ 𝑏 ∀𝑦 ∈ (𝐾 ∖ { 0 }) ¬ (𝑦 · 𝑥) ∈ (𝑁‘(𝑏 ∖ {𝑥})))) |
| 39 | 19, 38 | anbi12d 632 |
. . . . . . . . 9
⊢ (((𝑤 = 𝑊 ∧ 𝑛 = 𝑁) ∧ 𝑓 = 𝐹) → (((𝑛‘𝑏) = (Base‘𝑤) ∧ ∀𝑥 ∈ 𝑏 ∀𝑦 ∈ ((Base‘𝑓) ∖ {(0g‘𝑓)}) ¬ (𝑦( ·𝑠
‘𝑤)𝑥) ∈ (𝑛‘(𝑏 ∖ {𝑥}))) ↔ ((𝑁‘𝑏) = 𝑉 ∧ ∀𝑥 ∈ 𝑏 ∀𝑦 ∈ (𝐾 ∖ { 0 }) ¬ (𝑦 · 𝑥) ∈ (𝑁‘(𝑏 ∖ {𝑥}))))) |
| 40 | 11, 15, 39 | sbcied2 3833 |
. . . . . . . 8
⊢ ((𝑤 = 𝑊 ∧ 𝑛 = 𝑁) → ([(Scalar‘𝑤) / 𝑓]((𝑛‘𝑏) = (Base‘𝑤) ∧ ∀𝑥 ∈ 𝑏 ∀𝑦 ∈ ((Base‘𝑓) ∖ {(0g‘𝑓)}) ¬ (𝑦( ·𝑠
‘𝑤)𝑥) ∈ (𝑛‘(𝑏 ∖ {𝑥}))) ↔ ((𝑁‘𝑏) = 𝑉 ∧ ∀𝑥 ∈ 𝑏 ∀𝑦 ∈ (𝐾 ∖ { 0 }) ¬ (𝑦 · 𝑥) ∈ (𝑁‘(𝑏 ∖ {𝑥}))))) |
| 41 | 7, 10, 40 | sbcied2 3833 |
. . . . . . 7
⊢ (𝑤 = 𝑊 → ([(LSpan‘𝑤) / 𝑛][(Scalar‘𝑤) / 𝑓]((𝑛‘𝑏) = (Base‘𝑤) ∧ ∀𝑥 ∈ 𝑏 ∀𝑦 ∈ ((Base‘𝑓) ∖ {(0g‘𝑓)}) ¬ (𝑦( ·𝑠
‘𝑤)𝑥) ∈ (𝑛‘(𝑏 ∖ {𝑥}))) ↔ ((𝑁‘𝑏) = 𝑉 ∧ ∀𝑥 ∈ 𝑏 ∀𝑦 ∈ (𝐾 ∖ { 0 }) ¬ (𝑦 · 𝑥) ∈ (𝑁‘(𝑏 ∖ {𝑥}))))) |
| 42 | 6, 41 | rabeqbidv 3455 |
. . . . . 6
⊢ (𝑤 = 𝑊 → {𝑏 ∈ 𝒫 (Base‘𝑤) ∣
[(LSpan‘𝑤) /
𝑛][(Scalar‘𝑤) / 𝑓]((𝑛‘𝑏) = (Base‘𝑤) ∧ ∀𝑥 ∈ 𝑏 ∀𝑦 ∈ ((Base‘𝑓) ∖ {(0g‘𝑓)}) ¬ (𝑦( ·𝑠
‘𝑤)𝑥) ∈ (𝑛‘(𝑏 ∖ {𝑥})))} = {𝑏 ∈ 𝒫 𝑉 ∣ ((𝑁‘𝑏) = 𝑉 ∧ ∀𝑥 ∈ 𝑏 ∀𝑦 ∈ (𝐾 ∖ { 0 }) ¬ (𝑦 · 𝑥) ∈ (𝑁‘(𝑏 ∖ {𝑥})))}) |
| 43 | | df-lbs 21074 |
. . . . . 6
⊢ LBasis =
(𝑤 ∈ V ↦ {𝑏 ∈ 𝒫
(Base‘𝑤) ∣
[(LSpan‘𝑤) /
𝑛][(Scalar‘𝑤) / 𝑓]((𝑛‘𝑏) = (Base‘𝑤) ∧ ∀𝑥 ∈ 𝑏 ∀𝑦 ∈ ((Base‘𝑓) ∖ {(0g‘𝑓)}) ¬ (𝑦( ·𝑠
‘𝑤)𝑥) ∈ (𝑛‘(𝑏 ∖ {𝑥})))}) |
| 44 | 4 | fvexi 6920 |
. . . . . . . 8
⊢ 𝑉 ∈ V |
| 45 | 44 | pwex 5380 |
. . . . . . 7
⊢ 𝒫
𝑉 ∈ V |
| 46 | 45 | rabex 5339 |
. . . . . 6
⊢ {𝑏 ∈ 𝒫 𝑉 ∣ ((𝑁‘𝑏) = 𝑉 ∧ ∀𝑥 ∈ 𝑏 ∀𝑦 ∈ (𝐾 ∖ { 0 }) ¬ (𝑦 · 𝑥) ∈ (𝑁‘(𝑏 ∖ {𝑥})))} ∈ V |
| 47 | 42, 43, 46 | fvmpt 7016 |
. . . . 5
⊢ (𝑊 ∈ V →
(LBasis‘𝑊) = {𝑏 ∈ 𝒫 𝑉 ∣ ((𝑁‘𝑏) = 𝑉 ∧ ∀𝑥 ∈ 𝑏 ∀𝑦 ∈ (𝐾 ∖ { 0 }) ¬ (𝑦 · 𝑥) ∈ (𝑁‘(𝑏 ∖ {𝑥})))}) |
| 48 | 2, 47 | eqtrid 2789 |
. . . 4
⊢ (𝑊 ∈ V → 𝐽 = {𝑏 ∈ 𝒫 𝑉 ∣ ((𝑁‘𝑏) = 𝑉 ∧ ∀𝑥 ∈ 𝑏 ∀𝑦 ∈ (𝐾 ∖ { 0 }) ¬ (𝑦 · 𝑥) ∈ (𝑁‘(𝑏 ∖ {𝑥})))}) |
| 49 | 1, 48 | syl 17 |
. . 3
⊢ (𝑊 ∈ 𝑋 → 𝐽 = {𝑏 ∈ 𝒫 𝑉 ∣ ((𝑁‘𝑏) = 𝑉 ∧ ∀𝑥 ∈ 𝑏 ∀𝑦 ∈ (𝐾 ∖ { 0 }) ¬ (𝑦 · 𝑥) ∈ (𝑁‘(𝑏 ∖ {𝑥})))}) |
| 50 | 49 | eleq2d 2827 |
. 2
⊢ (𝑊 ∈ 𝑋 → (𝐵 ∈ 𝐽 ↔ 𝐵 ∈ {𝑏 ∈ 𝒫 𝑉 ∣ ((𝑁‘𝑏) = 𝑉 ∧ ∀𝑥 ∈ 𝑏 ∀𝑦 ∈ (𝐾 ∖ { 0 }) ¬ (𝑦 · 𝑥) ∈ (𝑁‘(𝑏 ∖ {𝑥})))})) |
| 51 | 44 | elpw2 5334 |
. . . 4
⊢ (𝐵 ∈ 𝒫 𝑉 ↔ 𝐵 ⊆ 𝑉) |
| 52 | 51 | anbi1i 624 |
. . 3
⊢ ((𝐵 ∈ 𝒫 𝑉 ∧ ((𝑁‘𝐵) = 𝑉 ∧ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ (𝐾 ∖ { 0 }) ¬ (𝑦 · 𝑥) ∈ (𝑁‘(𝐵 ∖ {𝑥})))) ↔ (𝐵 ⊆ 𝑉 ∧ ((𝑁‘𝐵) = 𝑉 ∧ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ (𝐾 ∖ { 0 }) ¬ (𝑦 · 𝑥) ∈ (𝑁‘(𝐵 ∖ {𝑥}))))) |
| 53 | | fveqeq2 6915 |
. . . . 5
⊢ (𝑏 = 𝐵 → ((𝑁‘𝑏) = 𝑉 ↔ (𝑁‘𝐵) = 𝑉)) |
| 54 | | difeq1 4119 |
. . . . . . . . . 10
⊢ (𝑏 = 𝐵 → (𝑏 ∖ {𝑥}) = (𝐵 ∖ {𝑥})) |
| 55 | 54 | fveq2d 6910 |
. . . . . . . . 9
⊢ (𝑏 = 𝐵 → (𝑁‘(𝑏 ∖ {𝑥})) = (𝑁‘(𝐵 ∖ {𝑥}))) |
| 56 | 55 | eleq2d 2827 |
. . . . . . . 8
⊢ (𝑏 = 𝐵 → ((𝑦 · 𝑥) ∈ (𝑁‘(𝑏 ∖ {𝑥})) ↔ (𝑦 · 𝑥) ∈ (𝑁‘(𝐵 ∖ {𝑥})))) |
| 57 | 56 | notbid 318 |
. . . . . . 7
⊢ (𝑏 = 𝐵 → (¬ (𝑦 · 𝑥) ∈ (𝑁‘(𝑏 ∖ {𝑥})) ↔ ¬ (𝑦 · 𝑥) ∈ (𝑁‘(𝐵 ∖ {𝑥})))) |
| 58 | 57 | ralbidv 3178 |
. . . . . 6
⊢ (𝑏 = 𝐵 → (∀𝑦 ∈ (𝐾 ∖ { 0 }) ¬ (𝑦 · 𝑥) ∈ (𝑁‘(𝑏 ∖ {𝑥})) ↔ ∀𝑦 ∈ (𝐾 ∖ { 0 }) ¬ (𝑦 · 𝑥) ∈ (𝑁‘(𝐵 ∖ {𝑥})))) |
| 59 | 58 | raleqbi1dv 3338 |
. . . . 5
⊢ (𝑏 = 𝐵 → (∀𝑥 ∈ 𝑏 ∀𝑦 ∈ (𝐾 ∖ { 0 }) ¬ (𝑦 · 𝑥) ∈ (𝑁‘(𝑏 ∖ {𝑥})) ↔ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ (𝐾 ∖ { 0 }) ¬ (𝑦 · 𝑥) ∈ (𝑁‘(𝐵 ∖ {𝑥})))) |
| 60 | 53, 59 | anbi12d 632 |
. . . 4
⊢ (𝑏 = 𝐵 → (((𝑁‘𝑏) = 𝑉 ∧ ∀𝑥 ∈ 𝑏 ∀𝑦 ∈ (𝐾 ∖ { 0 }) ¬ (𝑦 · 𝑥) ∈ (𝑁‘(𝑏 ∖ {𝑥}))) ↔ ((𝑁‘𝐵) = 𝑉 ∧ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ (𝐾 ∖ { 0 }) ¬ (𝑦 · 𝑥) ∈ (𝑁‘(𝐵 ∖ {𝑥}))))) |
| 61 | 60 | elrab 3692 |
. . 3
⊢ (𝐵 ∈ {𝑏 ∈ 𝒫 𝑉 ∣ ((𝑁‘𝑏) = 𝑉 ∧ ∀𝑥 ∈ 𝑏 ∀𝑦 ∈ (𝐾 ∖ { 0 }) ¬ (𝑦 · 𝑥) ∈ (𝑁‘(𝑏 ∖ {𝑥})))} ↔ (𝐵 ∈ 𝒫 𝑉 ∧ ((𝑁‘𝐵) = 𝑉 ∧ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ (𝐾 ∖ { 0 }) ¬ (𝑦 · 𝑥) ∈ (𝑁‘(𝐵 ∖ {𝑥}))))) |
| 62 | | 3anass 1095 |
. . 3
⊢ ((𝐵 ⊆ 𝑉 ∧ (𝑁‘𝐵) = 𝑉 ∧ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ (𝐾 ∖ { 0 }) ¬ (𝑦 · 𝑥) ∈ (𝑁‘(𝐵 ∖ {𝑥}))) ↔ (𝐵 ⊆ 𝑉 ∧ ((𝑁‘𝐵) = 𝑉 ∧ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ (𝐾 ∖ { 0 }) ¬ (𝑦 · 𝑥) ∈ (𝑁‘(𝐵 ∖ {𝑥}))))) |
| 63 | 52, 61, 62 | 3bitr4i 303 |
. 2
⊢ (𝐵 ∈ {𝑏 ∈ 𝒫 𝑉 ∣ ((𝑁‘𝑏) = 𝑉 ∧ ∀𝑥 ∈ 𝑏 ∀𝑦 ∈ (𝐾 ∖ { 0 }) ¬ (𝑦 · 𝑥) ∈ (𝑁‘(𝑏 ∖ {𝑥})))} ↔ (𝐵 ⊆ 𝑉 ∧ (𝑁‘𝐵) = 𝑉 ∧ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ (𝐾 ∖ { 0 }) ¬ (𝑦 · 𝑥) ∈ (𝑁‘(𝐵 ∖ {𝑥})))) |
| 64 | 50, 63 | bitrdi 287 |
1
⊢ (𝑊 ∈ 𝑋 → (𝐵 ∈ 𝐽 ↔ (𝐵 ⊆ 𝑉 ∧ (𝑁‘𝐵) = 𝑉 ∧ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ (𝐾 ∖ { 0 }) ¬ (𝑦 · 𝑥) ∈ (𝑁‘(𝐵 ∖ {𝑥}))))) |