| Step | Hyp | Ref
| Expression |
| 1 | | lss1d.f |
. . 3
⊢ 𝐹 = (Scalar‘𝑊) |
| 2 | 1 | a1i 11 |
. 2
⊢ ((𝑊 ∈ LMod ∧ 𝑋 ∈ 𝑉) → 𝐹 = (Scalar‘𝑊)) |
| 3 | | lss1d.k |
. . 3
⊢ 𝐾 = (Base‘𝐹) |
| 4 | 3 | a1i 11 |
. 2
⊢ ((𝑊 ∈ LMod ∧ 𝑋 ∈ 𝑉) → 𝐾 = (Base‘𝐹)) |
| 5 | | lss1d.v |
. . 3
⊢ 𝑉 = (Base‘𝑊) |
| 6 | 5 | a1i 11 |
. 2
⊢ ((𝑊 ∈ LMod ∧ 𝑋 ∈ 𝑉) → 𝑉 = (Base‘𝑊)) |
| 7 | | eqidd 2738 |
. 2
⊢ ((𝑊 ∈ LMod ∧ 𝑋 ∈ 𝑉) → (+g‘𝑊) = (+g‘𝑊)) |
| 8 | | lss1d.t |
. . 3
⊢ · = (
·𝑠 ‘𝑊) |
| 9 | 8 | a1i 11 |
. 2
⊢ ((𝑊 ∈ LMod ∧ 𝑋 ∈ 𝑉) → · = (
·𝑠 ‘𝑊)) |
| 10 | | lss1d.s |
. . 3
⊢ 𝑆 = (LSubSp‘𝑊) |
| 11 | 10 | a1i 11 |
. 2
⊢ ((𝑊 ∈ LMod ∧ 𝑋 ∈ 𝑉) → 𝑆 = (LSubSp‘𝑊)) |
| 12 | 5, 1, 8, 3 | lmodvscl 20876 |
. . . . . . 7
⊢ ((𝑊 ∈ LMod ∧ 𝑘 ∈ 𝐾 ∧ 𝑋 ∈ 𝑉) → (𝑘 · 𝑋) ∈ 𝑉) |
| 13 | 12 | 3expa 1119 |
. . . . . 6
⊢ (((𝑊 ∈ LMod ∧ 𝑘 ∈ 𝐾) ∧ 𝑋 ∈ 𝑉) → (𝑘 · 𝑋) ∈ 𝑉) |
| 14 | 13 | an32s 652 |
. . . . 5
⊢ (((𝑊 ∈ LMod ∧ 𝑋 ∈ 𝑉) ∧ 𝑘 ∈ 𝐾) → (𝑘 · 𝑋) ∈ 𝑉) |
| 15 | | eleq1a 2836 |
. . . . 5
⊢ ((𝑘 · 𝑋) ∈ 𝑉 → (𝑣 = (𝑘 · 𝑋) → 𝑣 ∈ 𝑉)) |
| 16 | 14, 15 | syl 17 |
. . . 4
⊢ (((𝑊 ∈ LMod ∧ 𝑋 ∈ 𝑉) ∧ 𝑘 ∈ 𝐾) → (𝑣 = (𝑘 · 𝑋) → 𝑣 ∈ 𝑉)) |
| 17 | 16 | rexlimdva 3155 |
. . 3
⊢ ((𝑊 ∈ LMod ∧ 𝑋 ∈ 𝑉) → (∃𝑘 ∈ 𝐾 𝑣 = (𝑘 · 𝑋) → 𝑣 ∈ 𝑉)) |
| 18 | 17 | abssdv 4068 |
. 2
⊢ ((𝑊 ∈ LMod ∧ 𝑋 ∈ 𝑉) → {𝑣 ∣ ∃𝑘 ∈ 𝐾 𝑣 = (𝑘 · 𝑋)} ⊆ 𝑉) |
| 19 | | eqid 2737 |
. . . . 5
⊢
(0g‘𝐹) = (0g‘𝐹) |
| 20 | 1, 3, 19 | lmod0cl 20886 |
. . . 4
⊢ (𝑊 ∈ LMod →
(0g‘𝐹)
∈ 𝐾) |
| 21 | 20 | adantr 480 |
. . 3
⊢ ((𝑊 ∈ LMod ∧ 𝑋 ∈ 𝑉) → (0g‘𝐹) ∈ 𝐾) |
| 22 | | nfcv 2905 |
. . . 4
⊢
Ⅎ𝑘(0g‘𝐹) |
| 23 | | nfre1 3285 |
. . . . . 6
⊢
Ⅎ𝑘∃𝑘 ∈ 𝐾 𝑣 = (𝑘 · 𝑋) |
| 24 | 23 | nfab 2911 |
. . . . 5
⊢
Ⅎ𝑘{𝑣 ∣ ∃𝑘 ∈ 𝐾 𝑣 = (𝑘 · 𝑋)} |
| 25 | | nfcv 2905 |
. . . . 5
⊢
Ⅎ𝑘∅ |
| 26 | 24, 25 | nfne 3043 |
. . . 4
⊢
Ⅎ𝑘{𝑣 ∣ ∃𝑘 ∈ 𝐾 𝑣 = (𝑘 · 𝑋)} ≠ ∅ |
| 27 | | biidd 262 |
. . . 4
⊢ (𝑘 = (0g‘𝐹) → ({𝑣 ∣ ∃𝑘 ∈ 𝐾 𝑣 = (𝑘 · 𝑋)} ≠ ∅ ↔ {𝑣 ∣ ∃𝑘 ∈ 𝐾 𝑣 = (𝑘 · 𝑋)} ≠ ∅)) |
| 28 | | ovex 7464 |
. . . . . 6
⊢ (𝑘 · 𝑋) ∈ V |
| 29 | 28 | elabrex 7262 |
. . . . 5
⊢ (𝑘 ∈ 𝐾 → (𝑘 · 𝑋) ∈ {𝑣 ∣ ∃𝑘 ∈ 𝐾 𝑣 = (𝑘 · 𝑋)}) |
| 30 | 29 | ne0d 4342 |
. . . 4
⊢ (𝑘 ∈ 𝐾 → {𝑣 ∣ ∃𝑘 ∈ 𝐾 𝑣 = (𝑘 · 𝑋)} ≠ ∅) |
| 31 | 22, 26, 27, 30 | vtoclgaf 3576 |
. . 3
⊢
((0g‘𝐹) ∈ 𝐾 → {𝑣 ∣ ∃𝑘 ∈ 𝐾 𝑣 = (𝑘 · 𝑋)} ≠ ∅) |
| 32 | 21, 31 | syl 17 |
. 2
⊢ ((𝑊 ∈ LMod ∧ 𝑋 ∈ 𝑉) → {𝑣 ∣ ∃𝑘 ∈ 𝐾 𝑣 = (𝑘 · 𝑋)} ≠ ∅) |
| 33 | | vex 3484 |
. . . . . . . . . . 11
⊢ 𝑎 ∈ V |
| 34 | | eqeq1 2741 |
. . . . . . . . . . . 12
⊢ (𝑣 = 𝑎 → (𝑣 = (𝑘 · 𝑋) ↔ 𝑎 = (𝑘 · 𝑋))) |
| 35 | 34 | rexbidv 3179 |
. . . . . . . . . . 11
⊢ (𝑣 = 𝑎 → (∃𝑘 ∈ 𝐾 𝑣 = (𝑘 · 𝑋) ↔ ∃𝑘 ∈ 𝐾 𝑎 = (𝑘 · 𝑋))) |
| 36 | 33, 35 | elab 3679 |
. . . . . . . . . 10
⊢ (𝑎 ∈ {𝑣 ∣ ∃𝑘 ∈ 𝐾 𝑣 = (𝑘 · 𝑋)} ↔ ∃𝑘 ∈ 𝐾 𝑎 = (𝑘 · 𝑋)) |
| 37 | | oveq1 7438 |
. . . . . . . . . . . 12
⊢ (𝑘 = 𝑦 → (𝑘 · 𝑋) = (𝑦 · 𝑋)) |
| 38 | 37 | eqeq2d 2748 |
. . . . . . . . . . 11
⊢ (𝑘 = 𝑦 → (𝑎 = (𝑘 · 𝑋) ↔ 𝑎 = (𝑦 · 𝑋))) |
| 39 | 38 | cbvrexvw 3238 |
. . . . . . . . . 10
⊢
(∃𝑘 ∈
𝐾 𝑎 = (𝑘 · 𝑋) ↔ ∃𝑦 ∈ 𝐾 𝑎 = (𝑦 · 𝑋)) |
| 40 | 36, 39 | bitri 275 |
. . . . . . . . 9
⊢ (𝑎 ∈ {𝑣 ∣ ∃𝑘 ∈ 𝐾 𝑣 = (𝑘 · 𝑋)} ↔ ∃𝑦 ∈ 𝐾 𝑎 = (𝑦 · 𝑋)) |
| 41 | | vex 3484 |
. . . . . . . . . . 11
⊢ 𝑏 ∈ V |
| 42 | | eqeq1 2741 |
. . . . . . . . . . . 12
⊢ (𝑣 = 𝑏 → (𝑣 = (𝑘 · 𝑋) ↔ 𝑏 = (𝑘 · 𝑋))) |
| 43 | 42 | rexbidv 3179 |
. . . . . . . . . . 11
⊢ (𝑣 = 𝑏 → (∃𝑘 ∈ 𝐾 𝑣 = (𝑘 · 𝑋) ↔ ∃𝑘 ∈ 𝐾 𝑏 = (𝑘 · 𝑋))) |
| 44 | 41, 43 | elab 3679 |
. . . . . . . . . 10
⊢ (𝑏 ∈ {𝑣 ∣ ∃𝑘 ∈ 𝐾 𝑣 = (𝑘 · 𝑋)} ↔ ∃𝑘 ∈ 𝐾 𝑏 = (𝑘 · 𝑋)) |
| 45 | | oveq1 7438 |
. . . . . . . . . . . 12
⊢ (𝑘 = 𝑧 → (𝑘 · 𝑋) = (𝑧 · 𝑋)) |
| 46 | 45 | eqeq2d 2748 |
. . . . . . . . . . 11
⊢ (𝑘 = 𝑧 → (𝑏 = (𝑘 · 𝑋) ↔ 𝑏 = (𝑧 · 𝑋))) |
| 47 | 46 | cbvrexvw 3238 |
. . . . . . . . . 10
⊢
(∃𝑘 ∈
𝐾 𝑏 = (𝑘 · 𝑋) ↔ ∃𝑧 ∈ 𝐾 𝑏 = (𝑧 · 𝑋)) |
| 48 | 44, 47 | bitri 275 |
. . . . . . . . 9
⊢ (𝑏 ∈ {𝑣 ∣ ∃𝑘 ∈ 𝐾 𝑣 = (𝑘 · 𝑋)} ↔ ∃𝑧 ∈ 𝐾 𝑏 = (𝑧 · 𝑋)) |
| 49 | 40, 48 | anbi12i 628 |
. . . . . . . 8
⊢ ((𝑎 ∈ {𝑣 ∣ ∃𝑘 ∈ 𝐾 𝑣 = (𝑘 · 𝑋)} ∧ 𝑏 ∈ {𝑣 ∣ ∃𝑘 ∈ 𝐾 𝑣 = (𝑘 · 𝑋)}) ↔ (∃𝑦 ∈ 𝐾 𝑎 = (𝑦 · 𝑋) ∧ ∃𝑧 ∈ 𝐾 𝑏 = (𝑧 · 𝑋))) |
| 50 | | reeanv 3229 |
. . . . . . . 8
⊢
(∃𝑦 ∈
𝐾 ∃𝑧 ∈ 𝐾 (𝑎 = (𝑦 · 𝑋) ∧ 𝑏 = (𝑧 · 𝑋)) ↔ (∃𝑦 ∈ 𝐾 𝑎 = (𝑦 · 𝑋) ∧ ∃𝑧 ∈ 𝐾 𝑏 = (𝑧 · 𝑋))) |
| 51 | 49, 50 | bitr4i 278 |
. . . . . . 7
⊢ ((𝑎 ∈ {𝑣 ∣ ∃𝑘 ∈ 𝐾 𝑣 = (𝑘 · 𝑋)} ∧ 𝑏 ∈ {𝑣 ∣ ∃𝑘 ∈ 𝐾 𝑣 = (𝑘 · 𝑋)}) ↔ ∃𝑦 ∈ 𝐾 ∃𝑧 ∈ 𝐾 (𝑎 = (𝑦 · 𝑋) ∧ 𝑏 = (𝑧 · 𝑋))) |
| 52 | | simpll 767 |
. . . . . . . . . . . . 13
⊢ (((𝑊 ∈ LMod ∧ 𝑋 ∈ 𝑉) ∧ ((𝑦 ∈ 𝐾 ∧ 𝑧 ∈ 𝐾) ∧ 𝑥 ∈ 𝐾)) → 𝑊 ∈ LMod) |
| 53 | | simprr 773 |
. . . . . . . . . . . . . 14
⊢ (((𝑊 ∈ LMod ∧ 𝑋 ∈ 𝑉) ∧ ((𝑦 ∈ 𝐾 ∧ 𝑧 ∈ 𝐾) ∧ 𝑥 ∈ 𝐾)) → 𝑥 ∈ 𝐾) |
| 54 | | simprll 779 |
. . . . . . . . . . . . . 14
⊢ (((𝑊 ∈ LMod ∧ 𝑋 ∈ 𝑉) ∧ ((𝑦 ∈ 𝐾 ∧ 𝑧 ∈ 𝐾) ∧ 𝑥 ∈ 𝐾)) → 𝑦 ∈ 𝐾) |
| 55 | | eqid 2737 |
. . . . . . . . . . . . . . 15
⊢
(.r‘𝐹) = (.r‘𝐹) |
| 56 | 1, 3, 55 | lmodmcl 20871 |
. . . . . . . . . . . . . 14
⊢ ((𝑊 ∈ LMod ∧ 𝑥 ∈ 𝐾 ∧ 𝑦 ∈ 𝐾) → (𝑥(.r‘𝐹)𝑦) ∈ 𝐾) |
| 57 | 52, 53, 54, 56 | syl3anc 1373 |
. . . . . . . . . . . . 13
⊢ (((𝑊 ∈ LMod ∧ 𝑋 ∈ 𝑉) ∧ ((𝑦 ∈ 𝐾 ∧ 𝑧 ∈ 𝐾) ∧ 𝑥 ∈ 𝐾)) → (𝑥(.r‘𝐹)𝑦) ∈ 𝐾) |
| 58 | | simprlr 780 |
. . . . . . . . . . . . 13
⊢ (((𝑊 ∈ LMod ∧ 𝑋 ∈ 𝑉) ∧ ((𝑦 ∈ 𝐾 ∧ 𝑧 ∈ 𝐾) ∧ 𝑥 ∈ 𝐾)) → 𝑧 ∈ 𝐾) |
| 59 | | eqid 2737 |
. . . . . . . . . . . . . 14
⊢
(+g‘𝐹) = (+g‘𝐹) |
| 60 | 1, 3, 59 | lmodacl 20870 |
. . . . . . . . . . . . 13
⊢ ((𝑊 ∈ LMod ∧ (𝑥(.r‘𝐹)𝑦) ∈ 𝐾 ∧ 𝑧 ∈ 𝐾) → ((𝑥(.r‘𝐹)𝑦)(+g‘𝐹)𝑧) ∈ 𝐾) |
| 61 | 52, 57, 58, 60 | syl3anc 1373 |
. . . . . . . . . . . 12
⊢ (((𝑊 ∈ LMod ∧ 𝑋 ∈ 𝑉) ∧ ((𝑦 ∈ 𝐾 ∧ 𝑧 ∈ 𝐾) ∧ 𝑥 ∈ 𝐾)) → ((𝑥(.r‘𝐹)𝑦)(+g‘𝐹)𝑧) ∈ 𝐾) |
| 62 | | simplr 769 |
. . . . . . . . . . . . . 14
⊢ (((𝑊 ∈ LMod ∧ 𝑋 ∈ 𝑉) ∧ ((𝑦 ∈ 𝐾 ∧ 𝑧 ∈ 𝐾) ∧ 𝑥 ∈ 𝐾)) → 𝑋 ∈ 𝑉) |
| 63 | | eqid 2737 |
. . . . . . . . . . . . . . 15
⊢
(+g‘𝑊) = (+g‘𝑊) |
| 64 | 5, 63, 1, 8, 3, 59 | lmodvsdir 20884 |
. . . . . . . . . . . . . 14
⊢ ((𝑊 ∈ LMod ∧ ((𝑥(.r‘𝐹)𝑦) ∈ 𝐾 ∧ 𝑧 ∈ 𝐾 ∧ 𝑋 ∈ 𝑉)) → (((𝑥(.r‘𝐹)𝑦)(+g‘𝐹)𝑧) · 𝑋) = (((𝑥(.r‘𝐹)𝑦) · 𝑋)(+g‘𝑊)(𝑧 · 𝑋))) |
| 65 | 52, 57, 58, 62, 64 | syl13anc 1374 |
. . . . . . . . . . . . 13
⊢ (((𝑊 ∈ LMod ∧ 𝑋 ∈ 𝑉) ∧ ((𝑦 ∈ 𝐾 ∧ 𝑧 ∈ 𝐾) ∧ 𝑥 ∈ 𝐾)) → (((𝑥(.r‘𝐹)𝑦)(+g‘𝐹)𝑧) · 𝑋) = (((𝑥(.r‘𝐹)𝑦) · 𝑋)(+g‘𝑊)(𝑧 · 𝑋))) |
| 66 | 5, 1, 8, 3, 55 | lmodvsass 20885 |
. . . . . . . . . . . . . . 15
⊢ ((𝑊 ∈ LMod ∧ (𝑥 ∈ 𝐾 ∧ 𝑦 ∈ 𝐾 ∧ 𝑋 ∈ 𝑉)) → ((𝑥(.r‘𝐹)𝑦) · 𝑋) = (𝑥 · (𝑦 · 𝑋))) |
| 67 | 52, 53, 54, 62, 66 | syl13anc 1374 |
. . . . . . . . . . . . . 14
⊢ (((𝑊 ∈ LMod ∧ 𝑋 ∈ 𝑉) ∧ ((𝑦 ∈ 𝐾 ∧ 𝑧 ∈ 𝐾) ∧ 𝑥 ∈ 𝐾)) → ((𝑥(.r‘𝐹)𝑦) · 𝑋) = (𝑥 · (𝑦 · 𝑋))) |
| 68 | 67 | oveq1d 7446 |
. . . . . . . . . . . . 13
⊢ (((𝑊 ∈ LMod ∧ 𝑋 ∈ 𝑉) ∧ ((𝑦 ∈ 𝐾 ∧ 𝑧 ∈ 𝐾) ∧ 𝑥 ∈ 𝐾)) → (((𝑥(.r‘𝐹)𝑦) · 𝑋)(+g‘𝑊)(𝑧 · 𝑋)) = ((𝑥 · (𝑦 · 𝑋))(+g‘𝑊)(𝑧 · 𝑋))) |
| 69 | 65, 68 | eqtr2d 2778 |
. . . . . . . . . . . 12
⊢ (((𝑊 ∈ LMod ∧ 𝑋 ∈ 𝑉) ∧ ((𝑦 ∈ 𝐾 ∧ 𝑧 ∈ 𝐾) ∧ 𝑥 ∈ 𝐾)) → ((𝑥 · (𝑦 · 𝑋))(+g‘𝑊)(𝑧 · 𝑋)) = (((𝑥(.r‘𝐹)𝑦)(+g‘𝐹)𝑧) · 𝑋)) |
| 70 | | oveq1 7438 |
. . . . . . . . . . . . 13
⊢ (𝑘 = ((𝑥(.r‘𝐹)𝑦)(+g‘𝐹)𝑧) → (𝑘 · 𝑋) = (((𝑥(.r‘𝐹)𝑦)(+g‘𝐹)𝑧) · 𝑋)) |
| 71 | 70 | rspceeqv 3645 |
. . . . . . . . . . . 12
⊢ ((((𝑥(.r‘𝐹)𝑦)(+g‘𝐹)𝑧) ∈ 𝐾 ∧ ((𝑥 · (𝑦 · 𝑋))(+g‘𝑊)(𝑧 · 𝑋)) = (((𝑥(.r‘𝐹)𝑦)(+g‘𝐹)𝑧) · 𝑋)) → ∃𝑘 ∈ 𝐾 ((𝑥 · (𝑦 · 𝑋))(+g‘𝑊)(𝑧 · 𝑋)) = (𝑘 · 𝑋)) |
| 72 | 61, 69, 71 | syl2anc 584 |
. . . . . . . . . . 11
⊢ (((𝑊 ∈ LMod ∧ 𝑋 ∈ 𝑉) ∧ ((𝑦 ∈ 𝐾 ∧ 𝑧 ∈ 𝐾) ∧ 𝑥 ∈ 𝐾)) → ∃𝑘 ∈ 𝐾 ((𝑥 · (𝑦 · 𝑋))(+g‘𝑊)(𝑧 · 𝑋)) = (𝑘 · 𝑋)) |
| 73 | | oveq2 7439 |
. . . . . . . . . . . . . 14
⊢ (𝑎 = (𝑦 · 𝑋) → (𝑥 · 𝑎) = (𝑥 · (𝑦 · 𝑋))) |
| 74 | | oveq12 7440 |
. . . . . . . . . . . . . 14
⊢ (((𝑥 · 𝑎) = (𝑥 · (𝑦 · 𝑋)) ∧ 𝑏 = (𝑧 · 𝑋)) → ((𝑥 · 𝑎)(+g‘𝑊)𝑏) = ((𝑥 · (𝑦 · 𝑋))(+g‘𝑊)(𝑧 · 𝑋))) |
| 75 | 73, 74 | sylan 580 |
. . . . . . . . . . . . 13
⊢ ((𝑎 = (𝑦 · 𝑋) ∧ 𝑏 = (𝑧 · 𝑋)) → ((𝑥 · 𝑎)(+g‘𝑊)𝑏) = ((𝑥 · (𝑦 · 𝑋))(+g‘𝑊)(𝑧 · 𝑋))) |
| 76 | 75 | eqeq1d 2739 |
. . . . . . . . . . . 12
⊢ ((𝑎 = (𝑦 · 𝑋) ∧ 𝑏 = (𝑧 · 𝑋)) → (((𝑥 · 𝑎)(+g‘𝑊)𝑏) = (𝑘 · 𝑋) ↔ ((𝑥 · (𝑦 · 𝑋))(+g‘𝑊)(𝑧 · 𝑋)) = (𝑘 · 𝑋))) |
| 77 | 76 | rexbidv 3179 |
. . . . . . . . . . 11
⊢ ((𝑎 = (𝑦 · 𝑋) ∧ 𝑏 = (𝑧 · 𝑋)) → (∃𝑘 ∈ 𝐾 ((𝑥 · 𝑎)(+g‘𝑊)𝑏) = (𝑘 · 𝑋) ↔ ∃𝑘 ∈ 𝐾 ((𝑥 · (𝑦 · 𝑋))(+g‘𝑊)(𝑧 · 𝑋)) = (𝑘 · 𝑋))) |
| 78 | 72, 77 | syl5ibrcom 247 |
. . . . . . . . . 10
⊢ (((𝑊 ∈ LMod ∧ 𝑋 ∈ 𝑉) ∧ ((𝑦 ∈ 𝐾 ∧ 𝑧 ∈ 𝐾) ∧ 𝑥 ∈ 𝐾)) → ((𝑎 = (𝑦 · 𝑋) ∧ 𝑏 = (𝑧 · 𝑋)) → ∃𝑘 ∈ 𝐾 ((𝑥 · 𝑎)(+g‘𝑊)𝑏) = (𝑘 · 𝑋))) |
| 79 | 78 | expr 456 |
. . . . . . . . 9
⊢ (((𝑊 ∈ LMod ∧ 𝑋 ∈ 𝑉) ∧ (𝑦 ∈ 𝐾 ∧ 𝑧 ∈ 𝐾)) → (𝑥 ∈ 𝐾 → ((𝑎 = (𝑦 · 𝑋) ∧ 𝑏 = (𝑧 · 𝑋)) → ∃𝑘 ∈ 𝐾 ((𝑥 · 𝑎)(+g‘𝑊)𝑏) = (𝑘 · 𝑋)))) |
| 80 | 79 | com23 86 |
. . . . . . . 8
⊢ (((𝑊 ∈ LMod ∧ 𝑋 ∈ 𝑉) ∧ (𝑦 ∈ 𝐾 ∧ 𝑧 ∈ 𝐾)) → ((𝑎 = (𝑦 · 𝑋) ∧ 𝑏 = (𝑧 · 𝑋)) → (𝑥 ∈ 𝐾 → ∃𝑘 ∈ 𝐾 ((𝑥 · 𝑎)(+g‘𝑊)𝑏) = (𝑘 · 𝑋)))) |
| 81 | 80 | rexlimdvva 3213 |
. . . . . . 7
⊢ ((𝑊 ∈ LMod ∧ 𝑋 ∈ 𝑉) → (∃𝑦 ∈ 𝐾 ∃𝑧 ∈ 𝐾 (𝑎 = (𝑦 · 𝑋) ∧ 𝑏 = (𝑧 · 𝑋)) → (𝑥 ∈ 𝐾 → ∃𝑘 ∈ 𝐾 ((𝑥 · 𝑎)(+g‘𝑊)𝑏) = (𝑘 · 𝑋)))) |
| 82 | 51, 81 | biimtrid 242 |
. . . . . 6
⊢ ((𝑊 ∈ LMod ∧ 𝑋 ∈ 𝑉) → ((𝑎 ∈ {𝑣 ∣ ∃𝑘 ∈ 𝐾 𝑣 = (𝑘 · 𝑋)} ∧ 𝑏 ∈ {𝑣 ∣ ∃𝑘 ∈ 𝐾 𝑣 = (𝑘 · 𝑋)}) → (𝑥 ∈ 𝐾 → ∃𝑘 ∈ 𝐾 ((𝑥 · 𝑎)(+g‘𝑊)𝑏) = (𝑘 · 𝑋)))) |
| 83 | 82 | expcomd 416 |
. . . . 5
⊢ ((𝑊 ∈ LMod ∧ 𝑋 ∈ 𝑉) → (𝑏 ∈ {𝑣 ∣ ∃𝑘 ∈ 𝐾 𝑣 = (𝑘 · 𝑋)} → (𝑎 ∈ {𝑣 ∣ ∃𝑘 ∈ 𝐾 𝑣 = (𝑘 · 𝑋)} → (𝑥 ∈ 𝐾 → ∃𝑘 ∈ 𝐾 ((𝑥 · 𝑎)(+g‘𝑊)𝑏) = (𝑘 · 𝑋))))) |
| 84 | 83 | com24 95 |
. . . 4
⊢ ((𝑊 ∈ LMod ∧ 𝑋 ∈ 𝑉) → (𝑥 ∈ 𝐾 → (𝑎 ∈ {𝑣 ∣ ∃𝑘 ∈ 𝐾 𝑣 = (𝑘 · 𝑋)} → (𝑏 ∈ {𝑣 ∣ ∃𝑘 ∈ 𝐾 𝑣 = (𝑘 · 𝑋)} → ∃𝑘 ∈ 𝐾 ((𝑥 · 𝑎)(+g‘𝑊)𝑏) = (𝑘 · 𝑋))))) |
| 85 | 84 | 3imp2 1350 |
. . 3
⊢ (((𝑊 ∈ LMod ∧ 𝑋 ∈ 𝑉) ∧ (𝑥 ∈ 𝐾 ∧ 𝑎 ∈ {𝑣 ∣ ∃𝑘 ∈ 𝐾 𝑣 = (𝑘 · 𝑋)} ∧ 𝑏 ∈ {𝑣 ∣ ∃𝑘 ∈ 𝐾 𝑣 = (𝑘 · 𝑋)})) → ∃𝑘 ∈ 𝐾 ((𝑥 · 𝑎)(+g‘𝑊)𝑏) = (𝑘 · 𝑋)) |
| 86 | | ovex 7464 |
. . . 4
⊢ ((𝑥 · 𝑎)(+g‘𝑊)𝑏) ∈ V |
| 87 | | eqeq1 2741 |
. . . . 5
⊢ (𝑣 = ((𝑥 · 𝑎)(+g‘𝑊)𝑏) → (𝑣 = (𝑘 · 𝑋) ↔ ((𝑥 · 𝑎)(+g‘𝑊)𝑏) = (𝑘 · 𝑋))) |
| 88 | 87 | rexbidv 3179 |
. . . 4
⊢ (𝑣 = ((𝑥 · 𝑎)(+g‘𝑊)𝑏) → (∃𝑘 ∈ 𝐾 𝑣 = (𝑘 · 𝑋) ↔ ∃𝑘 ∈ 𝐾 ((𝑥 · 𝑎)(+g‘𝑊)𝑏) = (𝑘 · 𝑋))) |
| 89 | 86, 88 | elab 3679 |
. . 3
⊢ (((𝑥 · 𝑎)(+g‘𝑊)𝑏) ∈ {𝑣 ∣ ∃𝑘 ∈ 𝐾 𝑣 = (𝑘 · 𝑋)} ↔ ∃𝑘 ∈ 𝐾 ((𝑥 · 𝑎)(+g‘𝑊)𝑏) = (𝑘 · 𝑋)) |
| 90 | 85, 89 | sylibr 234 |
. 2
⊢ (((𝑊 ∈ LMod ∧ 𝑋 ∈ 𝑉) ∧ (𝑥 ∈ 𝐾 ∧ 𝑎 ∈ {𝑣 ∣ ∃𝑘 ∈ 𝐾 𝑣 = (𝑘 · 𝑋)} ∧ 𝑏 ∈ {𝑣 ∣ ∃𝑘 ∈ 𝐾 𝑣 = (𝑘 · 𝑋)})) → ((𝑥 · 𝑎)(+g‘𝑊)𝑏) ∈ {𝑣 ∣ ∃𝑘 ∈ 𝐾 𝑣 = (𝑘 · 𝑋)}) |
| 91 | 2, 4, 6, 7, 9, 11,
18, 32, 90 | islssd 20933 |
1
⊢ ((𝑊 ∈ LMod ∧ 𝑋 ∈ 𝑉) → {𝑣 ∣ ∃𝑘 ∈ 𝐾 𝑣 = (𝑘 · 𝑋)} ∈ 𝑆) |