| Step | Hyp | Ref
| Expression |
| 1 | | lshpkrlem.w |
. . . . 5
⊢ (𝜑 → 𝑊 ∈ LVec) |
| 2 | | lveclmod 21105 |
. . . . 5
⊢ (𝑊 ∈ LVec → 𝑊 ∈ LMod) |
| 3 | 1, 2 | syl 17 |
. . . 4
⊢ (𝜑 → 𝑊 ∈ LMod) |
| 4 | | lshpkrlem.d |
. . . . 5
⊢ 𝐷 = (Scalar‘𝑊) |
| 5 | 4 | lmodfgrp 20867 |
. . . 4
⊢ (𝑊 ∈ LMod → 𝐷 ∈ Grp) |
| 6 | | lshpkrlem.k |
. . . . 5
⊢ 𝐾 = (Base‘𝐷) |
| 7 | | lshpkrlem.o |
. . . . 5
⊢ 0 =
(0g‘𝐷) |
| 8 | 6, 7 | grpidcl 18983 |
. . . 4
⊢ (𝐷 ∈ Grp → 0 ∈ 𝐾) |
| 9 | 3, 5, 8 | 3syl 18 |
. . 3
⊢ (𝜑 → 0 ∈ 𝐾) |
| 10 | | lshpkrlem.v |
. . . 4
⊢ 𝑉 = (Base‘𝑊) |
| 11 | | lshpkrlem.a |
. . . 4
⊢ + =
(+g‘𝑊) |
| 12 | | lshpkrlem.n |
. . . 4
⊢ 𝑁 = (LSpan‘𝑊) |
| 13 | | lshpkrlem.p |
. . . 4
⊢ ⊕ =
(LSSum‘𝑊) |
| 14 | | lshpkrlem.h |
. . . 4
⊢ 𝐻 = (LSHyp‘𝑊) |
| 15 | | lshpkrlem.u |
. . . 4
⊢ (𝜑 → 𝑈 ∈ 𝐻) |
| 16 | | lshpkrlem.z |
. . . 4
⊢ (𝜑 → 𝑍 ∈ 𝑉) |
| 17 | | lshpkrlem.x |
. . . 4
⊢ (𝜑 → 𝑋 ∈ 𝑉) |
| 18 | | lshpkrlem.e |
. . . 4
⊢ (𝜑 → (𝑈 ⊕ (𝑁‘{𝑍})) = 𝑉) |
| 19 | | lshpkrlem.t |
. . . 4
⊢ · = (
·𝑠 ‘𝑊) |
| 20 | 10, 11, 12, 13, 14, 1, 15, 16, 17, 18, 4, 6, 19 | lshpsmreu 39110 |
. . 3
⊢ (𝜑 → ∃!𝑘 ∈ 𝐾 ∃𝑏 ∈ 𝑈 𝑋 = (𝑏 + (𝑘 · 𝑍))) |
| 21 | | oveq1 7438 |
. . . . . . 7
⊢ (𝑘 = 0 → (𝑘 · 𝑍) = ( 0 · 𝑍)) |
| 22 | 21 | oveq2d 7447 |
. . . . . 6
⊢ (𝑘 = 0 → (𝑏 + (𝑘 · 𝑍)) = (𝑏 + ( 0 · 𝑍))) |
| 23 | 22 | eqeq2d 2748 |
. . . . 5
⊢ (𝑘 = 0 → (𝑋 = (𝑏 + (𝑘 · 𝑍)) ↔ 𝑋 = (𝑏 + ( 0 · 𝑍)))) |
| 24 | 23 | rexbidv 3179 |
. . . 4
⊢ (𝑘 = 0 → (∃𝑏 ∈ 𝑈 𝑋 = (𝑏 + (𝑘 · 𝑍)) ↔ ∃𝑏 ∈ 𝑈 𝑋 = (𝑏 + ( 0 · 𝑍)))) |
| 25 | 24 | riota2 7413 |
. . 3
⊢ (( 0 ∈ 𝐾 ∧ ∃!𝑘 ∈ 𝐾 ∃𝑏 ∈ 𝑈 𝑋 = (𝑏 + (𝑘 · 𝑍))) → (∃𝑏 ∈ 𝑈 𝑋 = (𝑏 + ( 0 · 𝑍)) ↔ (℩𝑘 ∈ 𝐾 ∃𝑏 ∈ 𝑈 𝑋 = (𝑏 + (𝑘 · 𝑍))) = 0 )) |
| 26 | 9, 20, 25 | syl2anc 584 |
. 2
⊢ (𝜑 → (∃𝑏 ∈ 𝑈 𝑋 = (𝑏 + ( 0 · 𝑍)) ↔ (℩𝑘 ∈ 𝐾 ∃𝑏 ∈ 𝑈 𝑋 = (𝑏 + (𝑘 · 𝑍))) = 0 )) |
| 27 | | simpr 484 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑋 ∈ 𝑈) → 𝑋 ∈ 𝑈) |
| 28 | | eqidd 2738 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑋 ∈ 𝑈) → 𝑋 = 𝑋) |
| 29 | | eqeq2 2749 |
. . . . . . 7
⊢ (𝑏 = 𝑋 → (𝑋 = 𝑏 ↔ 𝑋 = 𝑋)) |
| 30 | 29 | rspcev 3622 |
. . . . . 6
⊢ ((𝑋 ∈ 𝑈 ∧ 𝑋 = 𝑋) → ∃𝑏 ∈ 𝑈 𝑋 = 𝑏) |
| 31 | 27, 28, 30 | syl2anc 584 |
. . . . 5
⊢ ((𝜑 ∧ 𝑋 ∈ 𝑈) → ∃𝑏 ∈ 𝑈 𝑋 = 𝑏) |
| 32 | 31 | ex 412 |
. . . 4
⊢ (𝜑 → (𝑋 ∈ 𝑈 → ∃𝑏 ∈ 𝑈 𝑋 = 𝑏)) |
| 33 | | eleq1a 2836 |
. . . . . 6
⊢ (𝑏 ∈ 𝑈 → (𝑋 = 𝑏 → 𝑋 ∈ 𝑈)) |
| 34 | 33 | a1i 11 |
. . . . 5
⊢ (𝜑 → (𝑏 ∈ 𝑈 → (𝑋 = 𝑏 → 𝑋 ∈ 𝑈))) |
| 35 | 34 | rexlimdv 3153 |
. . . 4
⊢ (𝜑 → (∃𝑏 ∈ 𝑈 𝑋 = 𝑏 → 𝑋 ∈ 𝑈)) |
| 36 | 32, 35 | impbid 212 |
. . 3
⊢ (𝜑 → (𝑋 ∈ 𝑈 ↔ ∃𝑏 ∈ 𝑈 𝑋 = 𝑏)) |
| 37 | | eqid 2737 |
. . . . . . . . . . 11
⊢
(0g‘𝑊) = (0g‘𝑊) |
| 38 | 10, 4, 19, 7, 37 | lmod0vs 20893 |
. . . . . . . . . 10
⊢ ((𝑊 ∈ LMod ∧ 𝑍 ∈ 𝑉) → ( 0 · 𝑍) = (0g‘𝑊)) |
| 39 | 3, 16, 38 | syl2anc 584 |
. . . . . . . . 9
⊢ (𝜑 → ( 0 · 𝑍) = (0g‘𝑊)) |
| 40 | 39 | adantr 480 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑏 ∈ 𝑈) → ( 0 · 𝑍) = (0g‘𝑊)) |
| 41 | 40 | oveq2d 7447 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑏 ∈ 𝑈) → (𝑏 + ( 0 · 𝑍)) = (𝑏 + (0g‘𝑊))) |
| 42 | 1 | adantr 480 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑏 ∈ 𝑈) → 𝑊 ∈ LVec) |
| 43 | 42, 2 | syl 17 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑏 ∈ 𝑈) → 𝑊 ∈ LMod) |
| 44 | | eqid 2737 |
. . . . . . . . . 10
⊢
(LSubSp‘𝑊) =
(LSubSp‘𝑊) |
| 45 | 44, 14, 3, 15 | lshplss 38982 |
. . . . . . . . 9
⊢ (𝜑 → 𝑈 ∈ (LSubSp‘𝑊)) |
| 46 | 10, 44 | lssel 20935 |
. . . . . . . . 9
⊢ ((𝑈 ∈ (LSubSp‘𝑊) ∧ 𝑏 ∈ 𝑈) → 𝑏 ∈ 𝑉) |
| 47 | 45, 46 | sylan 580 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑏 ∈ 𝑈) → 𝑏 ∈ 𝑉) |
| 48 | 10, 11, 37 | lmod0vrid 20891 |
. . . . . . . 8
⊢ ((𝑊 ∈ LMod ∧ 𝑏 ∈ 𝑉) → (𝑏 + (0g‘𝑊)) = 𝑏) |
| 49 | 43, 47, 48 | syl2anc 584 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑏 ∈ 𝑈) → (𝑏 + (0g‘𝑊)) = 𝑏) |
| 50 | 41, 49 | eqtrd 2777 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑏 ∈ 𝑈) → (𝑏 + ( 0 · 𝑍)) = 𝑏) |
| 51 | 50 | eqeq2d 2748 |
. . . . 5
⊢ ((𝜑 ∧ 𝑏 ∈ 𝑈) → (𝑋 = (𝑏 + ( 0 · 𝑍)) ↔ 𝑋 = 𝑏)) |
| 52 | 51 | bicomd 223 |
. . . 4
⊢ ((𝜑 ∧ 𝑏 ∈ 𝑈) → (𝑋 = 𝑏 ↔ 𝑋 = (𝑏 + ( 0 · 𝑍)))) |
| 53 | 52 | rexbidva 3177 |
. . 3
⊢ (𝜑 → (∃𝑏 ∈ 𝑈 𝑋 = 𝑏 ↔ ∃𝑏 ∈ 𝑈 𝑋 = (𝑏 + ( 0 · 𝑍)))) |
| 54 | 36, 53 | bitrd 279 |
. 2
⊢ (𝜑 → (𝑋 ∈ 𝑈 ↔ ∃𝑏 ∈ 𝑈 𝑋 = (𝑏 + ( 0 · 𝑍)))) |
| 55 | | eqeq1 2741 |
. . . . . . . 8
⊢ (𝑥 = 𝑋 → (𝑥 = (𝑦 + (𝑘 · 𝑍)) ↔ 𝑋 = (𝑦 + (𝑘 · 𝑍)))) |
| 56 | 55 | rexbidv 3179 |
. . . . . . 7
⊢ (𝑥 = 𝑋 → (∃𝑦 ∈ 𝑈 𝑥 = (𝑦 + (𝑘 · 𝑍)) ↔ ∃𝑦 ∈ 𝑈 𝑋 = (𝑦 + (𝑘 · 𝑍)))) |
| 57 | 56 | riotabidv 7390 |
. . . . . 6
⊢ (𝑥 = 𝑋 → (℩𝑘 ∈ 𝐾 ∃𝑦 ∈ 𝑈 𝑥 = (𝑦 + (𝑘 · 𝑍))) = (℩𝑘 ∈ 𝐾 ∃𝑦 ∈ 𝑈 𝑋 = (𝑦 + (𝑘 · 𝑍)))) |
| 58 | | lshpkrlem.g |
. . . . . 6
⊢ 𝐺 = (𝑥 ∈ 𝑉 ↦ (℩𝑘 ∈ 𝐾 ∃𝑦 ∈ 𝑈 𝑥 = (𝑦 + (𝑘 · 𝑍)))) |
| 59 | | riotaex 7392 |
. . . . . 6
⊢
(℩𝑘
∈ 𝐾 ∃𝑦 ∈ 𝑈 𝑋 = (𝑦 + (𝑘 · 𝑍))) ∈ V |
| 60 | 57, 58, 59 | fvmpt 7016 |
. . . . 5
⊢ (𝑋 ∈ 𝑉 → (𝐺‘𝑋) = (℩𝑘 ∈ 𝐾 ∃𝑦 ∈ 𝑈 𝑋 = (𝑦 + (𝑘 · 𝑍)))) |
| 61 | | oveq1 7438 |
. . . . . . . . 9
⊢ (𝑦 = 𝑏 → (𝑦 + (𝑘 · 𝑍)) = (𝑏 + (𝑘 · 𝑍))) |
| 62 | 61 | eqeq2d 2748 |
. . . . . . . 8
⊢ (𝑦 = 𝑏 → (𝑋 = (𝑦 + (𝑘 · 𝑍)) ↔ 𝑋 = (𝑏 + (𝑘 · 𝑍)))) |
| 63 | 62 | cbvrexvw 3238 |
. . . . . . 7
⊢
(∃𝑦 ∈
𝑈 𝑋 = (𝑦 + (𝑘 · 𝑍)) ↔ ∃𝑏 ∈ 𝑈 𝑋 = (𝑏 + (𝑘 · 𝑍))) |
| 64 | 63 | a1i 11 |
. . . . . 6
⊢ (𝑘 ∈ 𝐾 → (∃𝑦 ∈ 𝑈 𝑋 = (𝑦 + (𝑘 · 𝑍)) ↔ ∃𝑏 ∈ 𝑈 𝑋 = (𝑏 + (𝑘 · 𝑍)))) |
| 65 | 64 | riotabiia 7408 |
. . . . 5
⊢
(℩𝑘
∈ 𝐾 ∃𝑦 ∈ 𝑈 𝑋 = (𝑦 + (𝑘 · 𝑍))) = (℩𝑘 ∈ 𝐾 ∃𝑏 ∈ 𝑈 𝑋 = (𝑏 + (𝑘 · 𝑍))) |
| 66 | 60, 65 | eqtrdi 2793 |
. . . 4
⊢ (𝑋 ∈ 𝑉 → (𝐺‘𝑋) = (℩𝑘 ∈ 𝐾 ∃𝑏 ∈ 𝑈 𝑋 = (𝑏 + (𝑘 · 𝑍)))) |
| 67 | 17, 66 | syl 17 |
. . 3
⊢ (𝜑 → (𝐺‘𝑋) = (℩𝑘 ∈ 𝐾 ∃𝑏 ∈ 𝑈 𝑋 = (𝑏 + (𝑘 · 𝑍)))) |
| 68 | 67 | eqeq1d 2739 |
. 2
⊢ (𝜑 → ((𝐺‘𝑋) = 0 ↔
(℩𝑘 ∈
𝐾 ∃𝑏 ∈ 𝑈 𝑋 = (𝑏 + (𝑘 · 𝑍))) = 0 )) |
| 69 | 26, 54, 68 | 3bitr4d 311 |
1
⊢ (𝜑 → (𝑋 ∈ 𝑈 ↔ (𝐺‘𝑋) = 0 )) |