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 2623 |
. 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 18880 |
. . . . . . 7
⊢ ((𝑊 ∈ LMod ∧ 𝑘 ∈ 𝐾 ∧ 𝑋 ∈ 𝑉) → (𝑘 · 𝑋) ∈ 𝑉) |
13 | 12 | 3expa 1265 |
. . . . . 6
⊢ (((𝑊 ∈ LMod ∧ 𝑘 ∈ 𝐾) ∧ 𝑋 ∈ 𝑉) → (𝑘 · 𝑋) ∈ 𝑉) |
14 | 13 | an32s 846 |
. . . . 5
⊢ (((𝑊 ∈ LMod ∧ 𝑋 ∈ 𝑉) ∧ 𝑘 ∈ 𝐾) → (𝑘 · 𝑋) ∈ 𝑉) |
15 | | eleq1a 2696 |
. . . . 5
⊢ ((𝑘 · 𝑋) ∈ 𝑉 → (𝑣 = (𝑘 · 𝑋) → 𝑣 ∈ 𝑉)) |
16 | 14, 15 | syl 17 |
. . . 4
⊢ (((𝑊 ∈ LMod ∧ 𝑋 ∈ 𝑉) ∧ 𝑘 ∈ 𝐾) → (𝑣 = (𝑘 · 𝑋) → 𝑣 ∈ 𝑉)) |
17 | 16 | rexlimdva 3031 |
. . 3
⊢ ((𝑊 ∈ LMod ∧ 𝑋 ∈ 𝑉) → (∃𝑘 ∈ 𝐾 𝑣 = (𝑘 · 𝑋) → 𝑣 ∈ 𝑉)) |
18 | 17 | abssdv 3676 |
. 2
⊢ ((𝑊 ∈ LMod ∧ 𝑋 ∈ 𝑉) → {𝑣 ∣ ∃𝑘 ∈ 𝐾 𝑣 = (𝑘 · 𝑋)} ⊆ 𝑉) |
19 | | eqid 2622 |
. . . . 5
⊢
(0g‘𝐹) = (0g‘𝐹) |
20 | 1, 3, 19 | lmod0cl 18889 |
. . . 4
⊢ (𝑊 ∈ LMod →
(0g‘𝐹)
∈ 𝐾) |
21 | 20 | adantr 481 |
. . 3
⊢ ((𝑊 ∈ LMod ∧ 𝑋 ∈ 𝑉) → (0g‘𝐹) ∈ 𝐾) |
22 | | nfcv 2764 |
. . . 4
⊢
Ⅎ𝑘(0g‘𝐹) |
23 | | nfre1 3005 |
. . . . . 6
⊢
Ⅎ𝑘∃𝑘 ∈ 𝐾 𝑣 = (𝑘 · 𝑋) |
24 | 23 | nfab 2769 |
. . . . 5
⊢
Ⅎ𝑘{𝑣 ∣ ∃𝑘 ∈ 𝐾 𝑣 = (𝑘 · 𝑋)} |
25 | | nfcv 2764 |
. . . . 5
⊢
Ⅎ𝑘∅ |
26 | 24, 25 | nfne 2894 |
. . . 4
⊢
Ⅎ𝑘{𝑣 ∣ ∃𝑘 ∈ 𝐾 𝑣 = (𝑘 · 𝑋)} ≠ ∅ |
27 | | biidd 252 |
. . . 4
⊢ (𝑘 = (0g‘𝐹) → ({𝑣 ∣ ∃𝑘 ∈ 𝐾 𝑣 = (𝑘 · 𝑋)} ≠ ∅ ↔ {𝑣 ∣ ∃𝑘 ∈ 𝐾 𝑣 = (𝑘 · 𝑋)} ≠ ∅)) |
28 | | ovex 6678 |
. . . . . 6
⊢ (𝑘 · 𝑋) ∈ V |
29 | 28 | elabrex 6501 |
. . . . 5
⊢ (𝑘 ∈ 𝐾 → (𝑘 · 𝑋) ∈ {𝑣 ∣ ∃𝑘 ∈ 𝐾 𝑣 = (𝑘 · 𝑋)}) |
30 | | ne0i 3921 |
. . . . 5
⊢ ((𝑘 · 𝑋) ∈ {𝑣 ∣ ∃𝑘 ∈ 𝐾 𝑣 = (𝑘 · 𝑋)} → {𝑣 ∣ ∃𝑘 ∈ 𝐾 𝑣 = (𝑘 · 𝑋)} ≠ ∅) |
31 | 29, 30 | syl 17 |
. . . 4
⊢ (𝑘 ∈ 𝐾 → {𝑣 ∣ ∃𝑘 ∈ 𝐾 𝑣 = (𝑘 · 𝑋)} ≠ ∅) |
32 | 22, 26, 27, 31 | vtoclgaf 3271 |
. . 3
⊢
((0g‘𝐹) ∈ 𝐾 → {𝑣 ∣ ∃𝑘 ∈ 𝐾 𝑣 = (𝑘 · 𝑋)} ≠ ∅) |
33 | 21, 32 | syl 17 |
. 2
⊢ ((𝑊 ∈ LMod ∧ 𝑋 ∈ 𝑉) → {𝑣 ∣ ∃𝑘 ∈ 𝐾 𝑣 = (𝑘 · 𝑋)} ≠ ∅) |
34 | | vex 3203 |
. . . . . . . . . . 11
⊢ 𝑎 ∈ V |
35 | | eqeq1 2626 |
. . . . . . . . . . . 12
⊢ (𝑣 = 𝑎 → (𝑣 = (𝑘 · 𝑋) ↔ 𝑎 = (𝑘 · 𝑋))) |
36 | 35 | rexbidv 3052 |
. . . . . . . . . . 11
⊢ (𝑣 = 𝑎 → (∃𝑘 ∈ 𝐾 𝑣 = (𝑘 · 𝑋) ↔ ∃𝑘 ∈ 𝐾 𝑎 = (𝑘 · 𝑋))) |
37 | 34, 36 | elab 3350 |
. . . . . . . . . 10
⊢ (𝑎 ∈ {𝑣 ∣ ∃𝑘 ∈ 𝐾 𝑣 = (𝑘 · 𝑋)} ↔ ∃𝑘 ∈ 𝐾 𝑎 = (𝑘 · 𝑋)) |
38 | | oveq1 6657 |
. . . . . . . . . . . 12
⊢ (𝑘 = 𝑦 → (𝑘 · 𝑋) = (𝑦 · 𝑋)) |
39 | 38 | eqeq2d 2632 |
. . . . . . . . . . 11
⊢ (𝑘 = 𝑦 → (𝑎 = (𝑘 · 𝑋) ↔ 𝑎 = (𝑦 · 𝑋))) |
40 | 39 | cbvrexv 3172 |
. . . . . . . . . 10
⊢
(∃𝑘 ∈
𝐾 𝑎 = (𝑘 · 𝑋) ↔ ∃𝑦 ∈ 𝐾 𝑎 = (𝑦 · 𝑋)) |
41 | 37, 40 | bitri 264 |
. . . . . . . . 9
⊢ (𝑎 ∈ {𝑣 ∣ ∃𝑘 ∈ 𝐾 𝑣 = (𝑘 · 𝑋)} ↔ ∃𝑦 ∈ 𝐾 𝑎 = (𝑦 · 𝑋)) |
42 | | vex 3203 |
. . . . . . . . . . 11
⊢ 𝑏 ∈ V |
43 | | eqeq1 2626 |
. . . . . . . . . . . 12
⊢ (𝑣 = 𝑏 → (𝑣 = (𝑘 · 𝑋) ↔ 𝑏 = (𝑘 · 𝑋))) |
44 | 43 | rexbidv 3052 |
. . . . . . . . . . 11
⊢ (𝑣 = 𝑏 → (∃𝑘 ∈ 𝐾 𝑣 = (𝑘 · 𝑋) ↔ ∃𝑘 ∈ 𝐾 𝑏 = (𝑘 · 𝑋))) |
45 | 42, 44 | elab 3350 |
. . . . . . . . . 10
⊢ (𝑏 ∈ {𝑣 ∣ ∃𝑘 ∈ 𝐾 𝑣 = (𝑘 · 𝑋)} ↔ ∃𝑘 ∈ 𝐾 𝑏 = (𝑘 · 𝑋)) |
46 | | oveq1 6657 |
. . . . . . . . . . . 12
⊢ (𝑘 = 𝑧 → (𝑘 · 𝑋) = (𝑧 · 𝑋)) |
47 | 46 | eqeq2d 2632 |
. . . . . . . . . . 11
⊢ (𝑘 = 𝑧 → (𝑏 = (𝑘 · 𝑋) ↔ 𝑏 = (𝑧 · 𝑋))) |
48 | 47 | cbvrexv 3172 |
. . . . . . . . . 10
⊢
(∃𝑘 ∈
𝐾 𝑏 = (𝑘 · 𝑋) ↔ ∃𝑧 ∈ 𝐾 𝑏 = (𝑧 · 𝑋)) |
49 | 45, 48 | bitri 264 |
. . . . . . . . 9
⊢ (𝑏 ∈ {𝑣 ∣ ∃𝑘 ∈ 𝐾 𝑣 = (𝑘 · 𝑋)} ↔ ∃𝑧 ∈ 𝐾 𝑏 = (𝑧 · 𝑋)) |
50 | 41, 49 | anbi12i 733 |
. . . . . . . 8
⊢ ((𝑎 ∈ {𝑣 ∣ ∃𝑘 ∈ 𝐾 𝑣 = (𝑘 · 𝑋)} ∧ 𝑏 ∈ {𝑣 ∣ ∃𝑘 ∈ 𝐾 𝑣 = (𝑘 · 𝑋)}) ↔ (∃𝑦 ∈ 𝐾 𝑎 = (𝑦 · 𝑋) ∧ ∃𝑧 ∈ 𝐾 𝑏 = (𝑧 · 𝑋))) |
51 | | reeanv 3107 |
. . . . . . . 8
⊢
(∃𝑦 ∈
𝐾 ∃𝑧 ∈ 𝐾 (𝑎 = (𝑦 · 𝑋) ∧ 𝑏 = (𝑧 · 𝑋)) ↔ (∃𝑦 ∈ 𝐾 𝑎 = (𝑦 · 𝑋) ∧ ∃𝑧 ∈ 𝐾 𝑏 = (𝑧 · 𝑋))) |
52 | 50, 51 | bitr4i 267 |
. . . . . . 7
⊢ ((𝑎 ∈ {𝑣 ∣ ∃𝑘 ∈ 𝐾 𝑣 = (𝑘 · 𝑋)} ∧ 𝑏 ∈ {𝑣 ∣ ∃𝑘 ∈ 𝐾 𝑣 = (𝑘 · 𝑋)}) ↔ ∃𝑦 ∈ 𝐾 ∃𝑧 ∈ 𝐾 (𝑎 = (𝑦 · 𝑋) ∧ 𝑏 = (𝑧 · 𝑋))) |
53 | | simpll 790 |
. . . . . . . . . . . . 13
⊢ (((𝑊 ∈ LMod ∧ 𝑋 ∈ 𝑉) ∧ ((𝑦 ∈ 𝐾 ∧ 𝑧 ∈ 𝐾) ∧ 𝑥 ∈ 𝐾)) → 𝑊 ∈ LMod) |
54 | | simprr 796 |
. . . . . . . . . . . . . 14
⊢ (((𝑊 ∈ LMod ∧ 𝑋 ∈ 𝑉) ∧ ((𝑦 ∈ 𝐾 ∧ 𝑧 ∈ 𝐾) ∧ 𝑥 ∈ 𝐾)) → 𝑥 ∈ 𝐾) |
55 | | simprll 802 |
. . . . . . . . . . . . . 14
⊢ (((𝑊 ∈ LMod ∧ 𝑋 ∈ 𝑉) ∧ ((𝑦 ∈ 𝐾 ∧ 𝑧 ∈ 𝐾) ∧ 𝑥 ∈ 𝐾)) → 𝑦 ∈ 𝐾) |
56 | | eqid 2622 |
. . . . . . . . . . . . . . 15
⊢
(.r‘𝐹) = (.r‘𝐹) |
57 | 1, 3, 56 | lmodmcl 18875 |
. . . . . . . . . . . . . 14
⊢ ((𝑊 ∈ LMod ∧ 𝑥 ∈ 𝐾 ∧ 𝑦 ∈ 𝐾) → (𝑥(.r‘𝐹)𝑦) ∈ 𝐾) |
58 | 53, 54, 55, 57 | syl3anc 1326 |
. . . . . . . . . . . . 13
⊢ (((𝑊 ∈ LMod ∧ 𝑋 ∈ 𝑉) ∧ ((𝑦 ∈ 𝐾 ∧ 𝑧 ∈ 𝐾) ∧ 𝑥 ∈ 𝐾)) → (𝑥(.r‘𝐹)𝑦) ∈ 𝐾) |
59 | | simprlr 803 |
. . . . . . . . . . . . 13
⊢ (((𝑊 ∈ LMod ∧ 𝑋 ∈ 𝑉) ∧ ((𝑦 ∈ 𝐾 ∧ 𝑧 ∈ 𝐾) ∧ 𝑥 ∈ 𝐾)) → 𝑧 ∈ 𝐾) |
60 | | eqid 2622 |
. . . . . . . . . . . . . 14
⊢
(+g‘𝐹) = (+g‘𝐹) |
61 | 1, 3, 60 | lmodacl 18874 |
. . . . . . . . . . . . 13
⊢ ((𝑊 ∈ LMod ∧ (𝑥(.r‘𝐹)𝑦) ∈ 𝐾 ∧ 𝑧 ∈ 𝐾) → ((𝑥(.r‘𝐹)𝑦)(+g‘𝐹)𝑧) ∈ 𝐾) |
62 | 53, 58, 59, 61 | syl3anc 1326 |
. . . . . . . . . . . 12
⊢ (((𝑊 ∈ LMod ∧ 𝑋 ∈ 𝑉) ∧ ((𝑦 ∈ 𝐾 ∧ 𝑧 ∈ 𝐾) ∧ 𝑥 ∈ 𝐾)) → ((𝑥(.r‘𝐹)𝑦)(+g‘𝐹)𝑧) ∈ 𝐾) |
63 | | simplr 792 |
. . . . . . . . . . . . . 14
⊢ (((𝑊 ∈ LMod ∧ 𝑋 ∈ 𝑉) ∧ ((𝑦 ∈ 𝐾 ∧ 𝑧 ∈ 𝐾) ∧ 𝑥 ∈ 𝐾)) → 𝑋 ∈ 𝑉) |
64 | | eqid 2622 |
. . . . . . . . . . . . . . 15
⊢
(+g‘𝑊) = (+g‘𝑊) |
65 | 5, 64, 1, 8, 3, 60 | lmodvsdir 18887 |
. . . . . . . . . . . . . 14
⊢ ((𝑊 ∈ LMod ∧ ((𝑥(.r‘𝐹)𝑦) ∈ 𝐾 ∧ 𝑧 ∈ 𝐾 ∧ 𝑋 ∈ 𝑉)) → (((𝑥(.r‘𝐹)𝑦)(+g‘𝐹)𝑧) · 𝑋) = (((𝑥(.r‘𝐹)𝑦) · 𝑋)(+g‘𝑊)(𝑧 · 𝑋))) |
66 | 53, 58, 59, 63, 65 | syl13anc 1328 |
. . . . . . . . . . . . 13
⊢ (((𝑊 ∈ LMod ∧ 𝑋 ∈ 𝑉) ∧ ((𝑦 ∈ 𝐾 ∧ 𝑧 ∈ 𝐾) ∧ 𝑥 ∈ 𝐾)) → (((𝑥(.r‘𝐹)𝑦)(+g‘𝐹)𝑧) · 𝑋) = (((𝑥(.r‘𝐹)𝑦) · 𝑋)(+g‘𝑊)(𝑧 · 𝑋))) |
67 | 5, 1, 8, 3, 56 | lmodvsass 18888 |
. . . . . . . . . . . . . . 15
⊢ ((𝑊 ∈ LMod ∧ (𝑥 ∈ 𝐾 ∧ 𝑦 ∈ 𝐾 ∧ 𝑋 ∈ 𝑉)) → ((𝑥(.r‘𝐹)𝑦) · 𝑋) = (𝑥 · (𝑦 · 𝑋))) |
68 | 53, 54, 55, 63, 67 | syl13anc 1328 |
. . . . . . . . . . . . . 14
⊢ (((𝑊 ∈ LMod ∧ 𝑋 ∈ 𝑉) ∧ ((𝑦 ∈ 𝐾 ∧ 𝑧 ∈ 𝐾) ∧ 𝑥 ∈ 𝐾)) → ((𝑥(.r‘𝐹)𝑦) · 𝑋) = (𝑥 · (𝑦 · 𝑋))) |
69 | 68 | oveq1d 6665 |
. . . . . . . . . . . . 13
⊢ (((𝑊 ∈ LMod ∧ 𝑋 ∈ 𝑉) ∧ ((𝑦 ∈ 𝐾 ∧ 𝑧 ∈ 𝐾) ∧ 𝑥 ∈ 𝐾)) → (((𝑥(.r‘𝐹)𝑦) · 𝑋)(+g‘𝑊)(𝑧 · 𝑋)) = ((𝑥 · (𝑦 · 𝑋))(+g‘𝑊)(𝑧 · 𝑋))) |
70 | 66, 69 | eqtr2d 2657 |
. . . . . . . . . . . 12
⊢ (((𝑊 ∈ LMod ∧ 𝑋 ∈ 𝑉) ∧ ((𝑦 ∈ 𝐾 ∧ 𝑧 ∈ 𝐾) ∧ 𝑥 ∈ 𝐾)) → ((𝑥 · (𝑦 · 𝑋))(+g‘𝑊)(𝑧 · 𝑋)) = (((𝑥(.r‘𝐹)𝑦)(+g‘𝐹)𝑧) · 𝑋)) |
71 | | oveq1 6657 |
. . . . . . . . . . . . . 14
⊢ (𝑘 = ((𝑥(.r‘𝐹)𝑦)(+g‘𝐹)𝑧) → (𝑘 · 𝑋) = (((𝑥(.r‘𝐹)𝑦)(+g‘𝐹)𝑧) · 𝑋)) |
72 | 71 | eqeq2d 2632 |
. . . . . . . . . . . . 13
⊢ (𝑘 = ((𝑥(.r‘𝐹)𝑦)(+g‘𝐹)𝑧) → (((𝑥 · (𝑦 · 𝑋))(+g‘𝑊)(𝑧 · 𝑋)) = (𝑘 · 𝑋) ↔ ((𝑥 · (𝑦 · 𝑋))(+g‘𝑊)(𝑧 · 𝑋)) = (((𝑥(.r‘𝐹)𝑦)(+g‘𝐹)𝑧) · 𝑋))) |
73 | 72 | rspcev 3309 |
. . . . . . . . . . . 12
⊢ ((((𝑥(.r‘𝐹)𝑦)(+g‘𝐹)𝑧) ∈ 𝐾 ∧ ((𝑥 · (𝑦 · 𝑋))(+g‘𝑊)(𝑧 · 𝑋)) = (((𝑥(.r‘𝐹)𝑦)(+g‘𝐹)𝑧) · 𝑋)) → ∃𝑘 ∈ 𝐾 ((𝑥 · (𝑦 · 𝑋))(+g‘𝑊)(𝑧 · 𝑋)) = (𝑘 · 𝑋)) |
74 | 62, 70, 73 | syl2anc 693 |
. . . . . . . . . . 11
⊢ (((𝑊 ∈ LMod ∧ 𝑋 ∈ 𝑉) ∧ ((𝑦 ∈ 𝐾 ∧ 𝑧 ∈ 𝐾) ∧ 𝑥 ∈ 𝐾)) → ∃𝑘 ∈ 𝐾 ((𝑥 · (𝑦 · 𝑋))(+g‘𝑊)(𝑧 · 𝑋)) = (𝑘 · 𝑋)) |
75 | | oveq2 6658 |
. . . . . . . . . . . . . 14
⊢ (𝑎 = (𝑦 · 𝑋) → (𝑥 · 𝑎) = (𝑥 · (𝑦 · 𝑋))) |
76 | | oveq12 6659 |
. . . . . . . . . . . . . 14
⊢ (((𝑥 · 𝑎) = (𝑥 · (𝑦 · 𝑋)) ∧ 𝑏 = (𝑧 · 𝑋)) → ((𝑥 · 𝑎)(+g‘𝑊)𝑏) = ((𝑥 · (𝑦 · 𝑋))(+g‘𝑊)(𝑧 · 𝑋))) |
77 | 75, 76 | sylan 488 |
. . . . . . . . . . . . 13
⊢ ((𝑎 = (𝑦 · 𝑋) ∧ 𝑏 = (𝑧 · 𝑋)) → ((𝑥 · 𝑎)(+g‘𝑊)𝑏) = ((𝑥 · (𝑦 · 𝑋))(+g‘𝑊)(𝑧 · 𝑋))) |
78 | 77 | eqeq1d 2624 |
. . . . . . . . . . . 12
⊢ ((𝑎 = (𝑦 · 𝑋) ∧ 𝑏 = (𝑧 · 𝑋)) → (((𝑥 · 𝑎)(+g‘𝑊)𝑏) = (𝑘 · 𝑋) ↔ ((𝑥 · (𝑦 · 𝑋))(+g‘𝑊)(𝑧 · 𝑋)) = (𝑘 · 𝑋))) |
79 | 78 | rexbidv 3052 |
. . . . . . . . . . 11
⊢ ((𝑎 = (𝑦 · 𝑋) ∧ 𝑏 = (𝑧 · 𝑋)) → (∃𝑘 ∈ 𝐾 ((𝑥 · 𝑎)(+g‘𝑊)𝑏) = (𝑘 · 𝑋) ↔ ∃𝑘 ∈ 𝐾 ((𝑥 · (𝑦 · 𝑋))(+g‘𝑊)(𝑧 · 𝑋)) = (𝑘 · 𝑋))) |
80 | 74, 79 | syl5ibrcom 237 |
. . . . . . . . . 10
⊢ (((𝑊 ∈ LMod ∧ 𝑋 ∈ 𝑉) ∧ ((𝑦 ∈ 𝐾 ∧ 𝑧 ∈ 𝐾) ∧ 𝑥 ∈ 𝐾)) → ((𝑎 = (𝑦 · 𝑋) ∧ 𝑏 = (𝑧 · 𝑋)) → ∃𝑘 ∈ 𝐾 ((𝑥 · 𝑎)(+g‘𝑊)𝑏) = (𝑘 · 𝑋))) |
81 | 80 | expr 643 |
. . . . . . . . 9
⊢ (((𝑊 ∈ LMod ∧ 𝑋 ∈ 𝑉) ∧ (𝑦 ∈ 𝐾 ∧ 𝑧 ∈ 𝐾)) → (𝑥 ∈ 𝐾 → ((𝑎 = (𝑦 · 𝑋) ∧ 𝑏 = (𝑧 · 𝑋)) → ∃𝑘 ∈ 𝐾 ((𝑥 · 𝑎)(+g‘𝑊)𝑏) = (𝑘 · 𝑋)))) |
82 | 81 | com23 86 |
. . . . . . . 8
⊢ (((𝑊 ∈ LMod ∧ 𝑋 ∈ 𝑉) ∧ (𝑦 ∈ 𝐾 ∧ 𝑧 ∈ 𝐾)) → ((𝑎 = (𝑦 · 𝑋) ∧ 𝑏 = (𝑧 · 𝑋)) → (𝑥 ∈ 𝐾 → ∃𝑘 ∈ 𝐾 ((𝑥 · 𝑎)(+g‘𝑊)𝑏) = (𝑘 · 𝑋)))) |
83 | 82 | rexlimdvva 3038 |
. . . . . . 7
⊢ ((𝑊 ∈ LMod ∧ 𝑋 ∈ 𝑉) → (∃𝑦 ∈ 𝐾 ∃𝑧 ∈ 𝐾 (𝑎 = (𝑦 · 𝑋) ∧ 𝑏 = (𝑧 · 𝑋)) → (𝑥 ∈ 𝐾 → ∃𝑘 ∈ 𝐾 ((𝑥 · 𝑎)(+g‘𝑊)𝑏) = (𝑘 · 𝑋)))) |
84 | 52, 83 | syl5bi 232 |
. . . . . 6
⊢ ((𝑊 ∈ LMod ∧ 𝑋 ∈ 𝑉) → ((𝑎 ∈ {𝑣 ∣ ∃𝑘 ∈ 𝐾 𝑣 = (𝑘 · 𝑋)} ∧ 𝑏 ∈ {𝑣 ∣ ∃𝑘 ∈ 𝐾 𝑣 = (𝑘 · 𝑋)}) → (𝑥 ∈ 𝐾 → ∃𝑘 ∈ 𝐾 ((𝑥 · 𝑎)(+g‘𝑊)𝑏) = (𝑘 · 𝑋)))) |
85 | 84 | expcomd 454 |
. . . . 5
⊢ ((𝑊 ∈ LMod ∧ 𝑋 ∈ 𝑉) → (𝑏 ∈ {𝑣 ∣ ∃𝑘 ∈ 𝐾 𝑣 = (𝑘 · 𝑋)} → (𝑎 ∈ {𝑣 ∣ ∃𝑘 ∈ 𝐾 𝑣 = (𝑘 · 𝑋)} → (𝑥 ∈ 𝐾 → ∃𝑘 ∈ 𝐾 ((𝑥 · 𝑎)(+g‘𝑊)𝑏) = (𝑘 · 𝑋))))) |
86 | 85 | com24 95 |
. . . 4
⊢ ((𝑊 ∈ LMod ∧ 𝑋 ∈ 𝑉) → (𝑥 ∈ 𝐾 → (𝑎 ∈ {𝑣 ∣ ∃𝑘 ∈ 𝐾 𝑣 = (𝑘 · 𝑋)} → (𝑏 ∈ {𝑣 ∣ ∃𝑘 ∈ 𝐾 𝑣 = (𝑘 · 𝑋)} → ∃𝑘 ∈ 𝐾 ((𝑥 · 𝑎)(+g‘𝑊)𝑏) = (𝑘 · 𝑋))))) |
87 | 86 | 3imp2 1282 |
. . 3
⊢ (((𝑊 ∈ LMod ∧ 𝑋 ∈ 𝑉) ∧ (𝑥 ∈ 𝐾 ∧ 𝑎 ∈ {𝑣 ∣ ∃𝑘 ∈ 𝐾 𝑣 = (𝑘 · 𝑋)} ∧ 𝑏 ∈ {𝑣 ∣ ∃𝑘 ∈ 𝐾 𝑣 = (𝑘 · 𝑋)})) → ∃𝑘 ∈ 𝐾 ((𝑥 · 𝑎)(+g‘𝑊)𝑏) = (𝑘 · 𝑋)) |
88 | | ovex 6678 |
. . . 4
⊢ ((𝑥 · 𝑎)(+g‘𝑊)𝑏) ∈ V |
89 | | eqeq1 2626 |
. . . . 5
⊢ (𝑣 = ((𝑥 · 𝑎)(+g‘𝑊)𝑏) → (𝑣 = (𝑘 · 𝑋) ↔ ((𝑥 · 𝑎)(+g‘𝑊)𝑏) = (𝑘 · 𝑋))) |
90 | 89 | rexbidv 3052 |
. . . 4
⊢ (𝑣 = ((𝑥 · 𝑎)(+g‘𝑊)𝑏) → (∃𝑘 ∈ 𝐾 𝑣 = (𝑘 · 𝑋) ↔ ∃𝑘 ∈ 𝐾 ((𝑥 · 𝑎)(+g‘𝑊)𝑏) = (𝑘 · 𝑋))) |
91 | 88, 90 | elab 3350 |
. . 3
⊢ (((𝑥 · 𝑎)(+g‘𝑊)𝑏) ∈ {𝑣 ∣ ∃𝑘 ∈ 𝐾 𝑣 = (𝑘 · 𝑋)} ↔ ∃𝑘 ∈ 𝐾 ((𝑥 · 𝑎)(+g‘𝑊)𝑏) = (𝑘 · 𝑋)) |
92 | 87, 91 | sylibr 224 |
. 2
⊢ (((𝑊 ∈ LMod ∧ 𝑋 ∈ 𝑉) ∧ (𝑥 ∈ 𝐾 ∧ 𝑎 ∈ {𝑣 ∣ ∃𝑘 ∈ 𝐾 𝑣 = (𝑘 · 𝑋)} ∧ 𝑏 ∈ {𝑣 ∣ ∃𝑘 ∈ 𝐾 𝑣 = (𝑘 · 𝑋)})) → ((𝑥 · 𝑎)(+g‘𝑊)𝑏) ∈ {𝑣 ∣ ∃𝑘 ∈ 𝐾 𝑣 = (𝑘 · 𝑋)}) |
93 | 2, 4, 6, 7, 9, 11,
18, 33, 92 | islssd 18936 |
1
⊢ ((𝑊 ∈ LMod ∧ 𝑋 ∈ 𝑉) → {𝑣 ∣ ∃𝑘 ∈ 𝐾 𝑣 = (𝑘 · 𝑋)} ∈ 𝑆) |