Step | Hyp | Ref
| Expression |
1 | | lspsolv.w |
. . . . 5
⊢ (𝜑 → 𝑊 ∈ LMod) |
2 | | lspsolv.q |
. . . . . . 7
⊢ 𝑄 = {𝑧 ∈ 𝑉 ∣ ∃𝑟 ∈ 𝐵 (𝑧 + (𝑟 · 𝑌)) ∈ (𝑁‘𝐴)} |
3 | 2 | ssrab3 4060 |
. . . . . 6
⊢ 𝑄 ⊆ 𝑉 |
4 | 3 | a1i 11 |
. . . . 5
⊢ (𝜑 → 𝑄 ⊆ 𝑉) |
5 | | lspsolv.ss |
. . . . . . . 8
⊢ (𝜑 → 𝐴 ⊆ 𝑉) |
6 | 1 | adantr 483 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑧 ∈ 𝐴) → 𝑊 ∈ LMod) |
7 | | lspsolv.f |
. . . . . . . . . . 11
⊢ 𝐹 = (Scalar‘𝑊) |
8 | | lspsolv.b |
. . . . . . . . . . 11
⊢ 𝐵 = (Base‘𝐹) |
9 | | eqid 2824 |
. . . . . . . . . . 11
⊢
(0g‘𝐹) = (0g‘𝐹) |
10 | 7, 8, 9 | lmod0cl 19663 |
. . . . . . . . . 10
⊢ (𝑊 ∈ LMod →
(0g‘𝐹)
∈ 𝐵) |
11 | 6, 10 | syl 17 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑧 ∈ 𝐴) → (0g‘𝐹) ∈ 𝐵) |
12 | | lspsolv.y |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 𝑌 ∈ 𝑉) |
13 | | lspsolv.v |
. . . . . . . . . . . . . . 15
⊢ 𝑉 = (Base‘𝑊) |
14 | | lspsolv.t |
. . . . . . . . . . . . . . 15
⊢ · = (
·𝑠 ‘𝑊) |
15 | | eqid 2824 |
. . . . . . . . . . . . . . 15
⊢
(0g‘𝑊) = (0g‘𝑊) |
16 | 13, 7, 14, 9, 15 | lmod0vs 19670 |
. . . . . . . . . . . . . 14
⊢ ((𝑊 ∈ LMod ∧ 𝑌 ∈ 𝑉) → ((0g‘𝐹) · 𝑌) = (0g‘𝑊)) |
17 | 1, 12, 16 | syl2anc 586 |
. . . . . . . . . . . . 13
⊢ (𝜑 →
((0g‘𝐹)
·
𝑌) =
(0g‘𝑊)) |
18 | 17 | adantr 483 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑧 ∈ 𝐴) → ((0g‘𝐹) · 𝑌) = (0g‘𝑊)) |
19 | 18 | oveq2d 7175 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑧 ∈ 𝐴) → (𝑧 +
((0g‘𝐹)
·
𝑌)) = (𝑧 + (0g‘𝑊))) |
20 | 5 | sselda 3970 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑧 ∈ 𝐴) → 𝑧 ∈ 𝑉) |
21 | | lspsolv.p |
. . . . . . . . . . . . 13
⊢ + =
(+g‘𝑊) |
22 | 13, 21, 15 | lmod0vrid 19668 |
. . . . . . . . . . . 12
⊢ ((𝑊 ∈ LMod ∧ 𝑧 ∈ 𝑉) → (𝑧 + (0g‘𝑊)) = 𝑧) |
23 | 6, 20, 22 | syl2anc 586 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑧 ∈ 𝐴) → (𝑧 + (0g‘𝑊)) = 𝑧) |
24 | 19, 23 | eqtrd 2859 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑧 ∈ 𝐴) → (𝑧 +
((0g‘𝐹)
·
𝑌)) = 𝑧) |
25 | | lspsolv.n |
. . . . . . . . . . . . 13
⊢ 𝑁 = (LSpan‘𝑊) |
26 | 13, 25 | lspssid 19760 |
. . . . . . . . . . . 12
⊢ ((𝑊 ∈ LMod ∧ 𝐴 ⊆ 𝑉) → 𝐴 ⊆ (𝑁‘𝐴)) |
27 | 1, 5, 26 | syl2anc 586 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐴 ⊆ (𝑁‘𝐴)) |
28 | 27 | sselda 3970 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑧 ∈ 𝐴) → 𝑧 ∈ (𝑁‘𝐴)) |
29 | 24, 28 | eqeltrd 2916 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑧 ∈ 𝐴) → (𝑧 +
((0g‘𝐹)
·
𝑌)) ∈ (𝑁‘𝐴)) |
30 | | oveq1 7166 |
. . . . . . . . . . . 12
⊢ (𝑟 = (0g‘𝐹) → (𝑟 · 𝑌) = ((0g‘𝐹) · 𝑌)) |
31 | 30 | oveq2d 7175 |
. . . . . . . . . . 11
⊢ (𝑟 = (0g‘𝐹) → (𝑧 + (𝑟 · 𝑌)) = (𝑧 +
((0g‘𝐹)
·
𝑌))) |
32 | 31 | eleq1d 2900 |
. . . . . . . . . 10
⊢ (𝑟 = (0g‘𝐹) → ((𝑧 + (𝑟 · 𝑌)) ∈ (𝑁‘𝐴) ↔ (𝑧 +
((0g‘𝐹)
·
𝑌)) ∈ (𝑁‘𝐴))) |
33 | 32 | rspcev 3626 |
. . . . . . . . 9
⊢
(((0g‘𝐹) ∈ 𝐵 ∧ (𝑧 +
((0g‘𝐹)
·
𝑌)) ∈ (𝑁‘𝐴)) → ∃𝑟 ∈ 𝐵 (𝑧 + (𝑟 · 𝑌)) ∈ (𝑁‘𝐴)) |
34 | 11, 29, 33 | syl2anc 586 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑧 ∈ 𝐴) → ∃𝑟 ∈ 𝐵 (𝑧 + (𝑟 · 𝑌)) ∈ (𝑁‘𝐴)) |
35 | 5, 34 | ssrabdv 4053 |
. . . . . . 7
⊢ (𝜑 → 𝐴 ⊆ {𝑧 ∈ 𝑉 ∣ ∃𝑟 ∈ 𝐵 (𝑧 + (𝑟 · 𝑌)) ∈ (𝑁‘𝐴)}) |
36 | 35, 2 | sseqtrrdi 4021 |
. . . . . 6
⊢ (𝜑 → 𝐴 ⊆ 𝑄) |
37 | 7 | lmodfgrp 19646 |
. . . . . . . . . . 11
⊢ (𝑊 ∈ LMod → 𝐹 ∈ Grp) |
38 | 1, 37 | syl 17 |
. . . . . . . . . 10
⊢ (𝜑 → 𝐹 ∈ Grp) |
39 | | eqid 2824 |
. . . . . . . . . . . 12
⊢
(1r‘𝐹) = (1r‘𝐹) |
40 | 7, 8, 39 | lmod1cl 19664 |
. . . . . . . . . . 11
⊢ (𝑊 ∈ LMod →
(1r‘𝐹)
∈ 𝐵) |
41 | 1, 40 | syl 17 |
. . . . . . . . . 10
⊢ (𝜑 → (1r‘𝐹) ∈ 𝐵) |
42 | | eqid 2824 |
. . . . . . . . . . 11
⊢
(invg‘𝐹) = (invg‘𝐹) |
43 | 8, 42 | grpinvcl 18154 |
. . . . . . . . . 10
⊢ ((𝐹 ∈ Grp ∧
(1r‘𝐹)
∈ 𝐵) →
((invg‘𝐹)‘(1r‘𝐹)) ∈ 𝐵) |
44 | 38, 41, 43 | syl2anc 586 |
. . . . . . . . 9
⊢ (𝜑 →
((invg‘𝐹)‘(1r‘𝐹)) ∈ 𝐵) |
45 | | eqid 2824 |
. . . . . . . . . . . . . 14
⊢
(invg‘𝑊) = (invg‘𝑊) |
46 | 13, 45, 7, 14, 39, 42 | lmodvneg1 19680 |
. . . . . . . . . . . . 13
⊢ ((𝑊 ∈ LMod ∧ 𝑌 ∈ 𝑉) → (((invg‘𝐹)‘(1r‘𝐹)) · 𝑌) = ((invg‘𝑊)‘𝑌)) |
47 | 1, 12, 46 | syl2anc 586 |
. . . . . . . . . . . 12
⊢ (𝜑 →
(((invg‘𝐹)‘(1r‘𝐹)) · 𝑌) = ((invg‘𝑊)‘𝑌)) |
48 | 47 | oveq2d 7175 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝑌 +
(((invg‘𝐹)‘(1r‘𝐹)) · 𝑌)) = (𝑌 +
((invg‘𝑊)‘𝑌))) |
49 | | lmodgrp 19644 |
. . . . . . . . . . . . 13
⊢ (𝑊 ∈ LMod → 𝑊 ∈ Grp) |
50 | 1, 49 | syl 17 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝑊 ∈ Grp) |
51 | 13, 21, 15, 45 | grprinv 18156 |
. . . . . . . . . . . 12
⊢ ((𝑊 ∈ Grp ∧ 𝑌 ∈ 𝑉) → (𝑌 +
((invg‘𝑊)‘𝑌)) = (0g‘𝑊)) |
52 | 50, 12, 51 | syl2anc 586 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝑌 +
((invg‘𝑊)‘𝑌)) = (0g‘𝑊)) |
53 | 48, 52 | eqtrd 2859 |
. . . . . . . . . 10
⊢ (𝜑 → (𝑌 +
(((invg‘𝐹)‘(1r‘𝐹)) · 𝑌)) = (0g‘𝑊)) |
54 | | lspsolv.s |
. . . . . . . . . . . . 13
⊢ 𝑆 = (LSubSp‘𝑊) |
55 | 13, 54, 25 | lspcl 19751 |
. . . . . . . . . . . 12
⊢ ((𝑊 ∈ LMod ∧ 𝐴 ⊆ 𝑉) → (𝑁‘𝐴) ∈ 𝑆) |
56 | 1, 5, 55 | syl2anc 586 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝑁‘𝐴) ∈ 𝑆) |
57 | 15, 54 | lss0cl 19721 |
. . . . . . . . . . 11
⊢ ((𝑊 ∈ LMod ∧ (𝑁‘𝐴) ∈ 𝑆) → (0g‘𝑊) ∈ (𝑁‘𝐴)) |
58 | 1, 56, 57 | syl2anc 586 |
. . . . . . . . . 10
⊢ (𝜑 → (0g‘𝑊) ∈ (𝑁‘𝐴)) |
59 | 53, 58 | eqeltrd 2916 |
. . . . . . . . 9
⊢ (𝜑 → (𝑌 +
(((invg‘𝐹)‘(1r‘𝐹)) · 𝑌)) ∈ (𝑁‘𝐴)) |
60 | | oveq1 7166 |
. . . . . . . . . . . 12
⊢ (𝑟 = ((invg‘𝐹)‘(1r‘𝐹)) → (𝑟 · 𝑌) = (((invg‘𝐹)‘(1r‘𝐹)) · 𝑌)) |
61 | 60 | oveq2d 7175 |
. . . . . . . . . . 11
⊢ (𝑟 = ((invg‘𝐹)‘(1r‘𝐹)) → (𝑌 + (𝑟 · 𝑌)) = (𝑌 +
(((invg‘𝐹)‘(1r‘𝐹)) · 𝑌))) |
62 | 61 | eleq1d 2900 |
. . . . . . . . . 10
⊢ (𝑟 = ((invg‘𝐹)‘(1r‘𝐹)) → ((𝑌 + (𝑟 · 𝑌)) ∈ (𝑁‘𝐴) ↔ (𝑌 +
(((invg‘𝐹)‘(1r‘𝐹)) · 𝑌)) ∈ (𝑁‘𝐴))) |
63 | 62 | rspcev 3626 |
. . . . . . . . 9
⊢
((((invg‘𝐹)‘(1r‘𝐹)) ∈ 𝐵 ∧ (𝑌 +
(((invg‘𝐹)‘(1r‘𝐹)) · 𝑌)) ∈ (𝑁‘𝐴)) → ∃𝑟 ∈ 𝐵 (𝑌 + (𝑟 · 𝑌)) ∈ (𝑁‘𝐴)) |
64 | 44, 59, 63 | syl2anc 586 |
. . . . . . . 8
⊢ (𝜑 → ∃𝑟 ∈ 𝐵 (𝑌 + (𝑟 · 𝑌)) ∈ (𝑁‘𝐴)) |
65 | | oveq1 7166 |
. . . . . . . . . . 11
⊢ (𝑧 = 𝑌 → (𝑧 + (𝑟 · 𝑌)) = (𝑌 + (𝑟 · 𝑌))) |
66 | 65 | eleq1d 2900 |
. . . . . . . . . 10
⊢ (𝑧 = 𝑌 → ((𝑧 + (𝑟 · 𝑌)) ∈ (𝑁‘𝐴) ↔ (𝑌 + (𝑟 · 𝑌)) ∈ (𝑁‘𝐴))) |
67 | 66 | rexbidv 3300 |
. . . . . . . . 9
⊢ (𝑧 = 𝑌 → (∃𝑟 ∈ 𝐵 (𝑧 + (𝑟 · 𝑌)) ∈ (𝑁‘𝐴) ↔ ∃𝑟 ∈ 𝐵 (𝑌 + (𝑟 · 𝑌)) ∈ (𝑁‘𝐴))) |
68 | 67, 2 | elrab2 3686 |
. . . . . . . 8
⊢ (𝑌 ∈ 𝑄 ↔ (𝑌 ∈ 𝑉 ∧ ∃𝑟 ∈ 𝐵 (𝑌 + (𝑟 · 𝑌)) ∈ (𝑁‘𝐴))) |
69 | 12, 64, 68 | sylanbrc 585 |
. . . . . . 7
⊢ (𝜑 → 𝑌 ∈ 𝑄) |
70 | 69 | snssd 4745 |
. . . . . 6
⊢ (𝜑 → {𝑌} ⊆ 𝑄) |
71 | 36, 70 | unssd 4165 |
. . . . 5
⊢ (𝜑 → (𝐴 ∪ {𝑌}) ⊆ 𝑄) |
72 | 13, 25 | lspss 19759 |
. . . . 5
⊢ ((𝑊 ∈ LMod ∧ 𝑄 ⊆ 𝑉 ∧ (𝐴 ∪ {𝑌}) ⊆ 𝑄) → (𝑁‘(𝐴 ∪ {𝑌})) ⊆ (𝑁‘𝑄)) |
73 | 1, 4, 71, 72 | syl3anc 1367 |
. . . 4
⊢ (𝜑 → (𝑁‘(𝐴 ∪ {𝑌})) ⊆ (𝑁‘𝑄)) |
74 | 7 | a1i 11 |
. . . . . 6
⊢ (𝜑 → 𝐹 = (Scalar‘𝑊)) |
75 | 8 | a1i 11 |
. . . . . 6
⊢ (𝜑 → 𝐵 = (Base‘𝐹)) |
76 | 13 | a1i 11 |
. . . . . 6
⊢ (𝜑 → 𝑉 = (Base‘𝑊)) |
77 | 21 | a1i 11 |
. . . . . 6
⊢ (𝜑 → + =
(+g‘𝑊)) |
78 | 14 | a1i 11 |
. . . . . 6
⊢ (𝜑 → · = (
·𝑠 ‘𝑊)) |
79 | 54 | a1i 11 |
. . . . . 6
⊢ (𝜑 → 𝑆 = (LSubSp‘𝑊)) |
80 | 69 | ne0d 4304 |
. . . . . 6
⊢ (𝜑 → 𝑄 ≠ ∅) |
81 | | oveq1 7166 |
. . . . . . . . . . . . . . 15
⊢ (𝑧 = 𝑥 → (𝑧 + (𝑟 · 𝑌)) = (𝑥 + (𝑟 · 𝑌))) |
82 | 81 | eleq1d 2900 |
. . . . . . . . . . . . . 14
⊢ (𝑧 = 𝑥 → ((𝑧 + (𝑟 · 𝑌)) ∈ (𝑁‘𝐴) ↔ (𝑥 + (𝑟 · 𝑌)) ∈ (𝑁‘𝐴))) |
83 | 82 | rexbidv 3300 |
. . . . . . . . . . . . 13
⊢ (𝑧 = 𝑥 → (∃𝑟 ∈ 𝐵 (𝑧 + (𝑟 · 𝑌)) ∈ (𝑁‘𝐴) ↔ ∃𝑟 ∈ 𝐵 (𝑥 + (𝑟 · 𝑌)) ∈ (𝑁‘𝐴))) |
84 | | oveq1 7166 |
. . . . . . . . . . . . . . . 16
⊢ (𝑟 = 𝑠 → (𝑟 · 𝑌) = (𝑠 · 𝑌)) |
85 | 84 | oveq2d 7175 |
. . . . . . . . . . . . . . 15
⊢ (𝑟 = 𝑠 → (𝑥 + (𝑟 · 𝑌)) = (𝑥 + (𝑠 · 𝑌))) |
86 | 85 | eleq1d 2900 |
. . . . . . . . . . . . . 14
⊢ (𝑟 = 𝑠 → ((𝑥 + (𝑟 · 𝑌)) ∈ (𝑁‘𝐴) ↔ (𝑥 + (𝑠 · 𝑌)) ∈ (𝑁‘𝐴))) |
87 | 86 | cbvrexvw 3453 |
. . . . . . . . . . . . 13
⊢
(∃𝑟 ∈
𝐵 (𝑥 + (𝑟 · 𝑌)) ∈ (𝑁‘𝐴) ↔ ∃𝑠 ∈ 𝐵 (𝑥 + (𝑠 · 𝑌)) ∈ (𝑁‘𝐴)) |
88 | 83, 87 | syl6bb 289 |
. . . . . . . . . . . 12
⊢ (𝑧 = 𝑥 → (∃𝑟 ∈ 𝐵 (𝑧 + (𝑟 · 𝑌)) ∈ (𝑁‘𝐴) ↔ ∃𝑠 ∈ 𝐵 (𝑥 + (𝑠 · 𝑌)) ∈ (𝑁‘𝐴))) |
89 | 88, 2 | elrab2 3686 |
. . . . . . . . . . 11
⊢ (𝑥 ∈ 𝑄 ↔ (𝑥 ∈ 𝑉 ∧ ∃𝑠 ∈ 𝐵 (𝑥 + (𝑠 · 𝑌)) ∈ (𝑁‘𝐴))) |
90 | | oveq1 7166 |
. . . . . . . . . . . . . . 15
⊢ (𝑧 = 𝑦 → (𝑧 + (𝑟 · 𝑌)) = (𝑦 + (𝑟 · 𝑌))) |
91 | 90 | eleq1d 2900 |
. . . . . . . . . . . . . 14
⊢ (𝑧 = 𝑦 → ((𝑧 + (𝑟 · 𝑌)) ∈ (𝑁‘𝐴) ↔ (𝑦 + (𝑟 · 𝑌)) ∈ (𝑁‘𝐴))) |
92 | 91 | rexbidv 3300 |
. . . . . . . . . . . . 13
⊢ (𝑧 = 𝑦 → (∃𝑟 ∈ 𝐵 (𝑧 + (𝑟 · 𝑌)) ∈ (𝑁‘𝐴) ↔ ∃𝑟 ∈ 𝐵 (𝑦 + (𝑟 · 𝑌)) ∈ (𝑁‘𝐴))) |
93 | | oveq1 7166 |
. . . . . . . . . . . . . . . 16
⊢ (𝑟 = 𝑡 → (𝑟 · 𝑌) = (𝑡 · 𝑌)) |
94 | 93 | oveq2d 7175 |
. . . . . . . . . . . . . . 15
⊢ (𝑟 = 𝑡 → (𝑦 + (𝑟 · 𝑌)) = (𝑦 + (𝑡 · 𝑌))) |
95 | 94 | eleq1d 2900 |
. . . . . . . . . . . . . 14
⊢ (𝑟 = 𝑡 → ((𝑦 + (𝑟 · 𝑌)) ∈ (𝑁‘𝐴) ↔ (𝑦 + (𝑡 · 𝑌)) ∈ (𝑁‘𝐴))) |
96 | 95 | cbvrexvw 3453 |
. . . . . . . . . . . . 13
⊢
(∃𝑟 ∈
𝐵 (𝑦 + (𝑟 · 𝑌)) ∈ (𝑁‘𝐴) ↔ ∃𝑡 ∈ 𝐵 (𝑦 + (𝑡 · 𝑌)) ∈ (𝑁‘𝐴)) |
97 | 92, 96 | syl6bb 289 |
. . . . . . . . . . . 12
⊢ (𝑧 = 𝑦 → (∃𝑟 ∈ 𝐵 (𝑧 + (𝑟 · 𝑌)) ∈ (𝑁‘𝐴) ↔ ∃𝑡 ∈ 𝐵 (𝑦 + (𝑡 · 𝑌)) ∈ (𝑁‘𝐴))) |
98 | 97, 2 | elrab2 3686 |
. . . . . . . . . . 11
⊢ (𝑦 ∈ 𝑄 ↔ (𝑦 ∈ 𝑉 ∧ ∃𝑡 ∈ 𝐵 (𝑦 + (𝑡 · 𝑌)) ∈ (𝑁‘𝐴))) |
99 | 89, 98 | anbi12i 628 |
. . . . . . . . . 10
⊢ ((𝑥 ∈ 𝑄 ∧ 𝑦 ∈ 𝑄) ↔ ((𝑥 ∈ 𝑉 ∧ ∃𝑠 ∈ 𝐵 (𝑥 + (𝑠 · 𝑌)) ∈ (𝑁‘𝐴)) ∧ (𝑦 ∈ 𝑉 ∧ ∃𝑡 ∈ 𝐵 (𝑦 + (𝑡 · 𝑌)) ∈ (𝑁‘𝐴)))) |
100 | | an4 654 |
. . . . . . . . . 10
⊢ (((𝑥 ∈ 𝑉 ∧ ∃𝑠 ∈ 𝐵 (𝑥 + (𝑠 · 𝑌)) ∈ (𝑁‘𝐴)) ∧ (𝑦 ∈ 𝑉 ∧ ∃𝑡 ∈ 𝐵 (𝑦 + (𝑡 · 𝑌)) ∈ (𝑁‘𝐴))) ↔ ((𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉) ∧ (∃𝑠 ∈ 𝐵 (𝑥 + (𝑠 · 𝑌)) ∈ (𝑁‘𝐴) ∧ ∃𝑡 ∈ 𝐵 (𝑦 + (𝑡 · 𝑌)) ∈ (𝑁‘𝐴)))) |
101 | 99, 100 | bitri 277 |
. . . . . . . . 9
⊢ ((𝑥 ∈ 𝑄 ∧ 𝑦 ∈ 𝑄) ↔ ((𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉) ∧ (∃𝑠 ∈ 𝐵 (𝑥 + (𝑠 · 𝑌)) ∈ (𝑁‘𝐴) ∧ ∃𝑡 ∈ 𝐵 (𝑦 + (𝑡 · 𝑌)) ∈ (𝑁‘𝐴)))) |
102 | | reeanv 3370 |
. . . . . . . . . . 11
⊢
(∃𝑠 ∈
𝐵 ∃𝑡 ∈ 𝐵 ((𝑥 + (𝑠 · 𝑌)) ∈ (𝑁‘𝐴) ∧ (𝑦 + (𝑡 · 𝑌)) ∈ (𝑁‘𝐴)) ↔ (∃𝑠 ∈ 𝐵 (𝑥 + (𝑠 · 𝑌)) ∈ (𝑁‘𝐴) ∧ ∃𝑡 ∈ 𝐵 (𝑦 + (𝑡 · 𝑌)) ∈ (𝑁‘𝐴))) |
103 | | simp1ll 1232 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝜑 ∧ 𝑎 ∈ 𝐵) ∧ (𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉)) ∧ (𝑠 ∈ 𝐵 ∧ 𝑡 ∈ 𝐵) ∧ ((𝑥 + (𝑠 · 𝑌)) ∈ (𝑁‘𝐴) ∧ (𝑦 + (𝑡 · 𝑌)) ∈ (𝑁‘𝐴))) → 𝜑) |
104 | 103, 1 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ 𝑎 ∈ 𝐵) ∧ (𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉)) ∧ (𝑠 ∈ 𝐵 ∧ 𝑡 ∈ 𝐵) ∧ ((𝑥 + (𝑠 · 𝑌)) ∈ (𝑁‘𝐴) ∧ (𝑦 + (𝑡 · 𝑌)) ∈ (𝑁‘𝐴))) → 𝑊 ∈ LMod) |
105 | | simp1lr 1233 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝜑 ∧ 𝑎 ∈ 𝐵) ∧ (𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉)) ∧ (𝑠 ∈ 𝐵 ∧ 𝑡 ∈ 𝐵) ∧ ((𝑥 + (𝑠 · 𝑌)) ∈ (𝑁‘𝐴) ∧ (𝑦 + (𝑡 · 𝑌)) ∈ (𝑁‘𝐴))) → 𝑎 ∈ 𝐵) |
106 | | simp1rl 1234 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝜑 ∧ 𝑎 ∈ 𝐵) ∧ (𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉)) ∧ (𝑠 ∈ 𝐵 ∧ 𝑡 ∈ 𝐵) ∧ ((𝑥 + (𝑠 · 𝑌)) ∈ (𝑁‘𝐴) ∧ (𝑦 + (𝑡 · 𝑌)) ∈ (𝑁‘𝐴))) → 𝑥 ∈ 𝑉) |
107 | 13, 7, 14, 8 | lmodvscl 19654 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑊 ∈ LMod ∧ 𝑎 ∈ 𝐵 ∧ 𝑥 ∈ 𝑉) → (𝑎 · 𝑥) ∈ 𝑉) |
108 | 104, 105,
106, 107 | syl3anc 1367 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ 𝑎 ∈ 𝐵) ∧ (𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉)) ∧ (𝑠 ∈ 𝐵 ∧ 𝑡 ∈ 𝐵) ∧ ((𝑥 + (𝑠 · 𝑌)) ∈ (𝑁‘𝐴) ∧ (𝑦 + (𝑡 · 𝑌)) ∈ (𝑁‘𝐴))) → (𝑎 · 𝑥) ∈ 𝑉) |
109 | | simp1rr 1235 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ 𝑎 ∈ 𝐵) ∧ (𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉)) ∧ (𝑠 ∈ 𝐵 ∧ 𝑡 ∈ 𝐵) ∧ ((𝑥 + (𝑠 · 𝑌)) ∈ (𝑁‘𝐴) ∧ (𝑦 + (𝑡 · 𝑌)) ∈ (𝑁‘𝐴))) → 𝑦 ∈ 𝑉) |
110 | 13, 21 | lmodvacl 19651 |
. . . . . . . . . . . . . . 15
⊢ ((𝑊 ∈ LMod ∧ (𝑎 · 𝑥) ∈ 𝑉 ∧ 𝑦 ∈ 𝑉) → ((𝑎 · 𝑥) + 𝑦) ∈ 𝑉) |
111 | 104, 108,
109, 110 | syl3anc 1367 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ 𝑎 ∈ 𝐵) ∧ (𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉)) ∧ (𝑠 ∈ 𝐵 ∧ 𝑡 ∈ 𝐵) ∧ ((𝑥 + (𝑠 · 𝑌)) ∈ (𝑁‘𝐴) ∧ (𝑦 + (𝑡 · 𝑌)) ∈ (𝑁‘𝐴))) → ((𝑎 · 𝑥) + 𝑦) ∈ 𝑉) |
112 | | simp2l 1195 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝜑 ∧ 𝑎 ∈ 𝐵) ∧ (𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉)) ∧ (𝑠 ∈ 𝐵 ∧ 𝑡 ∈ 𝐵) ∧ ((𝑥 + (𝑠 · 𝑌)) ∈ (𝑁‘𝐴) ∧ (𝑦 + (𝑡 · 𝑌)) ∈ (𝑁‘𝐴))) → 𝑠 ∈ 𝐵) |
113 | | eqid 2824 |
. . . . . . . . . . . . . . . . . 18
⊢
(.r‘𝐹) = (.r‘𝐹) |
114 | 7, 8, 113 | lmodmcl 19649 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑊 ∈ LMod ∧ 𝑎 ∈ 𝐵 ∧ 𝑠 ∈ 𝐵) → (𝑎(.r‘𝐹)𝑠) ∈ 𝐵) |
115 | 104, 105,
112, 114 | syl3anc 1367 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝜑 ∧ 𝑎 ∈ 𝐵) ∧ (𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉)) ∧ (𝑠 ∈ 𝐵 ∧ 𝑡 ∈ 𝐵) ∧ ((𝑥 + (𝑠 · 𝑌)) ∈ (𝑁‘𝐴) ∧ (𝑦 + (𝑡 · 𝑌)) ∈ (𝑁‘𝐴))) → (𝑎(.r‘𝐹)𝑠) ∈ 𝐵) |
116 | | simp2r 1196 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝜑 ∧ 𝑎 ∈ 𝐵) ∧ (𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉)) ∧ (𝑠 ∈ 𝐵 ∧ 𝑡 ∈ 𝐵) ∧ ((𝑥 + (𝑠 · 𝑌)) ∈ (𝑁‘𝐴) ∧ (𝑦 + (𝑡 · 𝑌)) ∈ (𝑁‘𝐴))) → 𝑡 ∈ 𝐵) |
117 | | eqid 2824 |
. . . . . . . . . . . . . . . . 17
⊢
(+g‘𝐹) = (+g‘𝐹) |
118 | 7, 8, 117 | lmodacl 19648 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑊 ∈ LMod ∧ (𝑎(.r‘𝐹)𝑠) ∈ 𝐵 ∧ 𝑡 ∈ 𝐵) → ((𝑎(.r‘𝐹)𝑠)(+g‘𝐹)𝑡) ∈ 𝐵) |
119 | 104, 115,
116, 118 | syl3anc 1367 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ 𝑎 ∈ 𝐵) ∧ (𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉)) ∧ (𝑠 ∈ 𝐵 ∧ 𝑡 ∈ 𝐵) ∧ ((𝑥 + (𝑠 · 𝑌)) ∈ (𝑁‘𝐴) ∧ (𝑦 + (𝑡 · 𝑌)) ∈ (𝑁‘𝐴))) → ((𝑎(.r‘𝐹)𝑠)(+g‘𝐹)𝑡) ∈ 𝐵) |
120 | 103, 12 | syl 17 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝜑 ∧ 𝑎 ∈ 𝐵) ∧ (𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉)) ∧ (𝑠 ∈ 𝐵 ∧ 𝑡 ∈ 𝐵) ∧ ((𝑥 + (𝑠 · 𝑌)) ∈ (𝑁‘𝐴) ∧ (𝑦 + (𝑡 · 𝑌)) ∈ (𝑁‘𝐴))) → 𝑌 ∈ 𝑉) |
121 | 13, 7, 14, 8 | lmodvscl 19654 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑊 ∈ LMod ∧ 𝑠 ∈ 𝐵 ∧ 𝑌 ∈ 𝑉) → (𝑠 · 𝑌) ∈ 𝑉) |
122 | 104, 112,
120, 121 | syl3anc 1367 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝜑 ∧ 𝑎 ∈ 𝐵) ∧ (𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉)) ∧ (𝑠 ∈ 𝐵 ∧ 𝑡 ∈ 𝐵) ∧ ((𝑥 + (𝑠 · 𝑌)) ∈ (𝑁‘𝐴) ∧ (𝑦 + (𝑡 · 𝑌)) ∈ (𝑁‘𝐴))) → (𝑠 · 𝑌) ∈ 𝑉) |
123 | 13, 7, 14, 8 | lmodvscl 19654 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑊 ∈ LMod ∧ 𝑎 ∈ 𝐵 ∧ (𝑠 · 𝑌) ∈ 𝑉) → (𝑎 · (𝑠 · 𝑌)) ∈ 𝑉) |
124 | 104, 105,
122, 123 | syl3anc 1367 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝜑 ∧ 𝑎 ∈ 𝐵) ∧ (𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉)) ∧ (𝑠 ∈ 𝐵 ∧ 𝑡 ∈ 𝐵) ∧ ((𝑥 + (𝑠 · 𝑌)) ∈ (𝑁‘𝐴) ∧ (𝑦 + (𝑡 · 𝑌)) ∈ (𝑁‘𝐴))) → (𝑎 · (𝑠 · 𝑌)) ∈ 𝑉) |
125 | 13, 7, 14, 8 | lmodvscl 19654 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑊 ∈ LMod ∧ 𝑡 ∈ 𝐵 ∧ 𝑌 ∈ 𝑉) → (𝑡 · 𝑌) ∈ 𝑉) |
126 | 104, 116,
120, 125 | syl3anc 1367 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝜑 ∧ 𝑎 ∈ 𝐵) ∧ (𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉)) ∧ (𝑠 ∈ 𝐵 ∧ 𝑡 ∈ 𝐵) ∧ ((𝑥 + (𝑠 · 𝑌)) ∈ (𝑁‘𝐴) ∧ (𝑦 + (𝑡 · 𝑌)) ∈ (𝑁‘𝐴))) → (𝑡 · 𝑌) ∈ 𝑉) |
127 | 13, 21 | lmod4 19687 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑊 ∈ LMod ∧ ((𝑎 · 𝑥) ∈ 𝑉 ∧ 𝑦 ∈ 𝑉) ∧ ((𝑎 · (𝑠 · 𝑌)) ∈ 𝑉 ∧ (𝑡 · 𝑌) ∈ 𝑉)) → (((𝑎 · 𝑥) + 𝑦) + ((𝑎 · (𝑠 · 𝑌)) + (𝑡 · 𝑌))) = (((𝑎 · 𝑥) + (𝑎 · (𝑠 · 𝑌))) + (𝑦 + (𝑡 · 𝑌)))) |
128 | 104, 108,
109, 124, 126, 127 | syl122anc 1375 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝜑 ∧ 𝑎 ∈ 𝐵) ∧ (𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉)) ∧ (𝑠 ∈ 𝐵 ∧ 𝑡 ∈ 𝐵) ∧ ((𝑥 + (𝑠 · 𝑌)) ∈ (𝑁‘𝐴) ∧ (𝑦 + (𝑡 · 𝑌)) ∈ (𝑁‘𝐴))) → (((𝑎 · 𝑥) + 𝑦) + ((𝑎 · (𝑠 · 𝑌)) + (𝑡 · 𝑌))) = (((𝑎 · 𝑥) + (𝑎 · (𝑠 · 𝑌))) + (𝑦 + (𝑡 · 𝑌)))) |
129 | 13, 21, 7, 14, 8, 117 | lmodvsdir 19661 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑊 ∈ LMod ∧ ((𝑎(.r‘𝐹)𝑠) ∈ 𝐵 ∧ 𝑡 ∈ 𝐵 ∧ 𝑌 ∈ 𝑉)) → (((𝑎(.r‘𝐹)𝑠)(+g‘𝐹)𝑡) · 𝑌) = (((𝑎(.r‘𝐹)𝑠) · 𝑌) + (𝑡 · 𝑌))) |
130 | 104, 115,
116, 120, 129 | syl13anc 1368 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝜑 ∧ 𝑎 ∈ 𝐵) ∧ (𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉)) ∧ (𝑠 ∈ 𝐵 ∧ 𝑡 ∈ 𝐵) ∧ ((𝑥 + (𝑠 · 𝑌)) ∈ (𝑁‘𝐴) ∧ (𝑦 + (𝑡 · 𝑌)) ∈ (𝑁‘𝐴))) → (((𝑎(.r‘𝐹)𝑠)(+g‘𝐹)𝑡) · 𝑌) = (((𝑎(.r‘𝐹)𝑠) · 𝑌) + (𝑡 · 𝑌))) |
131 | 13, 7, 14, 8, 113 | lmodvsass 19662 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑊 ∈ LMod ∧ (𝑎 ∈ 𝐵 ∧ 𝑠 ∈ 𝐵 ∧ 𝑌 ∈ 𝑉)) → ((𝑎(.r‘𝐹)𝑠) · 𝑌) = (𝑎 · (𝑠 · 𝑌))) |
132 | 104, 105,
112, 120, 131 | syl13anc 1368 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝜑 ∧ 𝑎 ∈ 𝐵) ∧ (𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉)) ∧ (𝑠 ∈ 𝐵 ∧ 𝑡 ∈ 𝐵) ∧ ((𝑥 + (𝑠 · 𝑌)) ∈ (𝑁‘𝐴) ∧ (𝑦 + (𝑡 · 𝑌)) ∈ (𝑁‘𝐴))) → ((𝑎(.r‘𝐹)𝑠) · 𝑌) = (𝑎 · (𝑠 · 𝑌))) |
133 | 132 | oveq1d 7174 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝜑 ∧ 𝑎 ∈ 𝐵) ∧ (𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉)) ∧ (𝑠 ∈ 𝐵 ∧ 𝑡 ∈ 𝐵) ∧ ((𝑥 + (𝑠 · 𝑌)) ∈ (𝑁‘𝐴) ∧ (𝑦 + (𝑡 · 𝑌)) ∈ (𝑁‘𝐴))) → (((𝑎(.r‘𝐹)𝑠) · 𝑌) + (𝑡 · 𝑌)) = ((𝑎 · (𝑠 · 𝑌)) + (𝑡 · 𝑌))) |
134 | 130, 133 | eqtrd 2859 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝜑 ∧ 𝑎 ∈ 𝐵) ∧ (𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉)) ∧ (𝑠 ∈ 𝐵 ∧ 𝑡 ∈ 𝐵) ∧ ((𝑥 + (𝑠 · 𝑌)) ∈ (𝑁‘𝐴) ∧ (𝑦 + (𝑡 · 𝑌)) ∈ (𝑁‘𝐴))) → (((𝑎(.r‘𝐹)𝑠)(+g‘𝐹)𝑡) · 𝑌) = ((𝑎 · (𝑠 · 𝑌)) + (𝑡 · 𝑌))) |
135 | 134 | oveq2d 7175 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝜑 ∧ 𝑎 ∈ 𝐵) ∧ (𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉)) ∧ (𝑠 ∈ 𝐵 ∧ 𝑡 ∈ 𝐵) ∧ ((𝑥 + (𝑠 · 𝑌)) ∈ (𝑁‘𝐴) ∧ (𝑦 + (𝑡 · 𝑌)) ∈ (𝑁‘𝐴))) → (((𝑎 · 𝑥) + 𝑦) + (((𝑎(.r‘𝐹)𝑠)(+g‘𝐹)𝑡) · 𝑌)) = (((𝑎 · 𝑥) + 𝑦) + ((𝑎 · (𝑠 · 𝑌)) + (𝑡 · 𝑌)))) |
136 | 13, 21, 7, 14, 8 | lmodvsdi 19660 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑊 ∈ LMod ∧ (𝑎 ∈ 𝐵 ∧ 𝑥 ∈ 𝑉 ∧ (𝑠 · 𝑌) ∈ 𝑉)) → (𝑎 · (𝑥 + (𝑠 · 𝑌))) = ((𝑎 · 𝑥) + (𝑎 · (𝑠 · 𝑌)))) |
137 | 104, 105,
106, 122, 136 | syl13anc 1368 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝜑 ∧ 𝑎 ∈ 𝐵) ∧ (𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉)) ∧ (𝑠 ∈ 𝐵 ∧ 𝑡 ∈ 𝐵) ∧ ((𝑥 + (𝑠 · 𝑌)) ∈ (𝑁‘𝐴) ∧ (𝑦 + (𝑡 · 𝑌)) ∈ (𝑁‘𝐴))) → (𝑎 · (𝑥 + (𝑠 · 𝑌))) = ((𝑎 · 𝑥) + (𝑎 · (𝑠 · 𝑌)))) |
138 | 137 | oveq1d 7174 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝜑 ∧ 𝑎 ∈ 𝐵) ∧ (𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉)) ∧ (𝑠 ∈ 𝐵 ∧ 𝑡 ∈ 𝐵) ∧ ((𝑥 + (𝑠 · 𝑌)) ∈ (𝑁‘𝐴) ∧ (𝑦 + (𝑡 · 𝑌)) ∈ (𝑁‘𝐴))) → ((𝑎 · (𝑥 + (𝑠 · 𝑌))) + (𝑦 + (𝑡 · 𝑌))) = (((𝑎 · 𝑥) + (𝑎 · (𝑠 · 𝑌))) + (𝑦 + (𝑡 · 𝑌)))) |
139 | 128, 135,
138 | 3eqtr4d 2869 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝜑 ∧ 𝑎 ∈ 𝐵) ∧ (𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉)) ∧ (𝑠 ∈ 𝐵 ∧ 𝑡 ∈ 𝐵) ∧ ((𝑥 + (𝑠 · 𝑌)) ∈ (𝑁‘𝐴) ∧ (𝑦 + (𝑡 · 𝑌)) ∈ (𝑁‘𝐴))) → (((𝑎 · 𝑥) + 𝑦) + (((𝑎(.r‘𝐹)𝑠)(+g‘𝐹)𝑡) · 𝑌)) = ((𝑎 · (𝑥 + (𝑠 · 𝑌))) + (𝑦 + (𝑡 · 𝑌)))) |
140 | 103, 56 | syl 17 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝜑 ∧ 𝑎 ∈ 𝐵) ∧ (𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉)) ∧ (𝑠 ∈ 𝐵 ∧ 𝑡 ∈ 𝐵) ∧ ((𝑥 + (𝑠 · 𝑌)) ∈ (𝑁‘𝐴) ∧ (𝑦 + (𝑡 · 𝑌)) ∈ (𝑁‘𝐴))) → (𝑁‘𝐴) ∈ 𝑆) |
141 | | simp3l 1197 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝜑 ∧ 𝑎 ∈ 𝐵) ∧ (𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉)) ∧ (𝑠 ∈ 𝐵 ∧ 𝑡 ∈ 𝐵) ∧ ((𝑥 + (𝑠 · 𝑌)) ∈ (𝑁‘𝐴) ∧ (𝑦 + (𝑡 · 𝑌)) ∈ (𝑁‘𝐴))) → (𝑥 + (𝑠 · 𝑌)) ∈ (𝑁‘𝐴)) |
142 | | simp3r 1198 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝜑 ∧ 𝑎 ∈ 𝐵) ∧ (𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉)) ∧ (𝑠 ∈ 𝐵 ∧ 𝑡 ∈ 𝐵) ∧ ((𝑥 + (𝑠 · 𝑌)) ∈ (𝑁‘𝐴) ∧ (𝑦 + (𝑡 · 𝑌)) ∈ (𝑁‘𝐴))) → (𝑦 + (𝑡 · 𝑌)) ∈ (𝑁‘𝐴)) |
143 | 7, 8, 21, 14, 54 | lsscl 19717 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑁‘𝐴) ∈ 𝑆 ∧ (𝑎 ∈ 𝐵 ∧ (𝑥 + (𝑠 · 𝑌)) ∈ (𝑁‘𝐴) ∧ (𝑦 + (𝑡 · 𝑌)) ∈ (𝑁‘𝐴))) → ((𝑎 · (𝑥 + (𝑠 · 𝑌))) + (𝑦 + (𝑡 · 𝑌))) ∈ (𝑁‘𝐴)) |
144 | 140, 105,
141, 142, 143 | syl13anc 1368 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝜑 ∧ 𝑎 ∈ 𝐵) ∧ (𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉)) ∧ (𝑠 ∈ 𝐵 ∧ 𝑡 ∈ 𝐵) ∧ ((𝑥 + (𝑠 · 𝑌)) ∈ (𝑁‘𝐴) ∧ (𝑦 + (𝑡 · 𝑌)) ∈ (𝑁‘𝐴))) → ((𝑎 · (𝑥 + (𝑠 · 𝑌))) + (𝑦 + (𝑡 · 𝑌))) ∈ (𝑁‘𝐴)) |
145 | 139, 144 | eqeltrd 2916 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ 𝑎 ∈ 𝐵) ∧ (𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉)) ∧ (𝑠 ∈ 𝐵 ∧ 𝑡 ∈ 𝐵) ∧ ((𝑥 + (𝑠 · 𝑌)) ∈ (𝑁‘𝐴) ∧ (𝑦 + (𝑡 · 𝑌)) ∈ (𝑁‘𝐴))) → (((𝑎 · 𝑥) + 𝑦) + (((𝑎(.r‘𝐹)𝑠)(+g‘𝐹)𝑡) · 𝑌)) ∈ (𝑁‘𝐴)) |
146 | | oveq1 7166 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑟 = ((𝑎(.r‘𝐹)𝑠)(+g‘𝐹)𝑡) → (𝑟 · 𝑌) = (((𝑎(.r‘𝐹)𝑠)(+g‘𝐹)𝑡) · 𝑌)) |
147 | 146 | oveq2d 7175 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑟 = ((𝑎(.r‘𝐹)𝑠)(+g‘𝐹)𝑡) → (((𝑎 · 𝑥) + 𝑦) + (𝑟 · 𝑌)) = (((𝑎 · 𝑥) + 𝑦) + (((𝑎(.r‘𝐹)𝑠)(+g‘𝐹)𝑡) · 𝑌))) |
148 | 147 | eleq1d 2900 |
. . . . . . . . . . . . . . . 16
⊢ (𝑟 = ((𝑎(.r‘𝐹)𝑠)(+g‘𝐹)𝑡) → ((((𝑎 · 𝑥) + 𝑦) + (𝑟 · 𝑌)) ∈ (𝑁‘𝐴) ↔ (((𝑎 · 𝑥) + 𝑦) + (((𝑎(.r‘𝐹)𝑠)(+g‘𝐹)𝑡) · 𝑌)) ∈ (𝑁‘𝐴))) |
149 | 148 | rspcev 3626 |
. . . . . . . . . . . . . . 15
⊢ ((((𝑎(.r‘𝐹)𝑠)(+g‘𝐹)𝑡) ∈ 𝐵 ∧ (((𝑎 · 𝑥) + 𝑦) + (((𝑎(.r‘𝐹)𝑠)(+g‘𝐹)𝑡) · 𝑌)) ∈ (𝑁‘𝐴)) → ∃𝑟 ∈ 𝐵 (((𝑎 · 𝑥) + 𝑦) + (𝑟 · 𝑌)) ∈ (𝑁‘𝐴)) |
150 | 119, 145,
149 | syl2anc 586 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ 𝑎 ∈ 𝐵) ∧ (𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉)) ∧ (𝑠 ∈ 𝐵 ∧ 𝑡 ∈ 𝐵) ∧ ((𝑥 + (𝑠 · 𝑌)) ∈ (𝑁‘𝐴) ∧ (𝑦 + (𝑡 · 𝑌)) ∈ (𝑁‘𝐴))) → ∃𝑟 ∈ 𝐵 (((𝑎 · 𝑥) + 𝑦) + (𝑟 · 𝑌)) ∈ (𝑁‘𝐴)) |
151 | | oveq1 7166 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑧 = ((𝑎 · 𝑥) + 𝑦) → (𝑧 + (𝑟 · 𝑌)) = (((𝑎 · 𝑥) + 𝑦) + (𝑟 · 𝑌))) |
152 | 151 | eleq1d 2900 |
. . . . . . . . . . . . . . . 16
⊢ (𝑧 = ((𝑎 · 𝑥) + 𝑦) → ((𝑧 + (𝑟 · 𝑌)) ∈ (𝑁‘𝐴) ↔ (((𝑎 · 𝑥) + 𝑦) + (𝑟 · 𝑌)) ∈ (𝑁‘𝐴))) |
153 | 152 | rexbidv 3300 |
. . . . . . . . . . . . . . 15
⊢ (𝑧 = ((𝑎 · 𝑥) + 𝑦) → (∃𝑟 ∈ 𝐵 (𝑧 + (𝑟 · 𝑌)) ∈ (𝑁‘𝐴) ↔ ∃𝑟 ∈ 𝐵 (((𝑎 · 𝑥) + 𝑦) + (𝑟 · 𝑌)) ∈ (𝑁‘𝐴))) |
154 | 153, 2 | elrab2 3686 |
. . . . . . . . . . . . . 14
⊢ (((𝑎 · 𝑥) + 𝑦) ∈ 𝑄 ↔ (((𝑎 · 𝑥) + 𝑦) ∈ 𝑉 ∧ ∃𝑟 ∈ 𝐵 (((𝑎 · 𝑥) + 𝑦) + (𝑟 · 𝑌)) ∈ (𝑁‘𝐴))) |
155 | 111, 150,
154 | sylanbrc 585 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝑎 ∈ 𝐵) ∧ (𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉)) ∧ (𝑠 ∈ 𝐵 ∧ 𝑡 ∈ 𝐵) ∧ ((𝑥 + (𝑠 · 𝑌)) ∈ (𝑁‘𝐴) ∧ (𝑦 + (𝑡 · 𝑌)) ∈ (𝑁‘𝐴))) → ((𝑎 · 𝑥) + 𝑦) ∈ 𝑄) |
156 | 155 | 3exp 1115 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑎 ∈ 𝐵) ∧ (𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉)) → ((𝑠 ∈ 𝐵 ∧ 𝑡 ∈ 𝐵) → (((𝑥 + (𝑠 · 𝑌)) ∈ (𝑁‘𝐴) ∧ (𝑦 + (𝑡 · 𝑌)) ∈ (𝑁‘𝐴)) → ((𝑎 · 𝑥) + 𝑦) ∈ 𝑄))) |
157 | 156 | rexlimdvv 3296 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑎 ∈ 𝐵) ∧ (𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉)) → (∃𝑠 ∈ 𝐵 ∃𝑡 ∈ 𝐵 ((𝑥 + (𝑠 · 𝑌)) ∈ (𝑁‘𝐴) ∧ (𝑦 + (𝑡 · 𝑌)) ∈ (𝑁‘𝐴)) → ((𝑎 · 𝑥) + 𝑦) ∈ 𝑄)) |
158 | 102, 157 | syl5bir 245 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑎 ∈ 𝐵) ∧ (𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉)) → ((∃𝑠 ∈ 𝐵 (𝑥 + (𝑠 · 𝑌)) ∈ (𝑁‘𝐴) ∧ ∃𝑡 ∈ 𝐵 (𝑦 + (𝑡 · 𝑌)) ∈ (𝑁‘𝐴)) → ((𝑎 · 𝑥) + 𝑦) ∈ 𝑄)) |
159 | 158 | expimpd 456 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑎 ∈ 𝐵) → (((𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉) ∧ (∃𝑠 ∈ 𝐵 (𝑥 + (𝑠 · 𝑌)) ∈ (𝑁‘𝐴) ∧ ∃𝑡 ∈ 𝐵 (𝑦 + (𝑡 · 𝑌)) ∈ (𝑁‘𝐴))) → ((𝑎 · 𝑥) + 𝑦) ∈ 𝑄)) |
160 | 101, 159 | syl5bi 244 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑎 ∈ 𝐵) → ((𝑥 ∈ 𝑄 ∧ 𝑦 ∈ 𝑄) → ((𝑎 · 𝑥) + 𝑦) ∈ 𝑄)) |
161 | 160 | exp4b 433 |
. . . . . . 7
⊢ (𝜑 → (𝑎 ∈ 𝐵 → (𝑥 ∈ 𝑄 → (𝑦 ∈ 𝑄 → ((𝑎 · 𝑥) + 𝑦) ∈ 𝑄)))) |
162 | 161 | 3imp2 1345 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑎 ∈ 𝐵 ∧ 𝑥 ∈ 𝑄 ∧ 𝑦 ∈ 𝑄)) → ((𝑎 · 𝑥) + 𝑦) ∈ 𝑄) |
163 | 74, 75, 76, 77, 78, 79, 4, 80, 162 | islssd 19710 |
. . . . 5
⊢ (𝜑 → 𝑄 ∈ 𝑆) |
164 | 54, 25 | lspid 19757 |
. . . . 5
⊢ ((𝑊 ∈ LMod ∧ 𝑄 ∈ 𝑆) → (𝑁‘𝑄) = 𝑄) |
165 | 1, 163, 164 | syl2anc 586 |
. . . 4
⊢ (𝜑 → (𝑁‘𝑄) = 𝑄) |
166 | 73, 165 | sseqtrd 4010 |
. . 3
⊢ (𝜑 → (𝑁‘(𝐴 ∪ {𝑌})) ⊆ 𝑄) |
167 | | lspsolv.x |
. . 3
⊢ (𝜑 → 𝑋 ∈ (𝑁‘(𝐴 ∪ {𝑌}))) |
168 | 166, 167 | sseldd 3971 |
. 2
⊢ (𝜑 → 𝑋 ∈ 𝑄) |
169 | | oveq1 7166 |
. . . . . 6
⊢ (𝑧 = 𝑋 → (𝑧 + (𝑟 · 𝑌)) = (𝑋 + (𝑟 · 𝑌))) |
170 | 169 | eleq1d 2900 |
. . . . 5
⊢ (𝑧 = 𝑋 → ((𝑧 + (𝑟 · 𝑌)) ∈ (𝑁‘𝐴) ↔ (𝑋 + (𝑟 · 𝑌)) ∈ (𝑁‘𝐴))) |
171 | 170 | rexbidv 3300 |
. . . 4
⊢ (𝑧 = 𝑋 → (∃𝑟 ∈ 𝐵 (𝑧 + (𝑟 · 𝑌)) ∈ (𝑁‘𝐴) ↔ ∃𝑟 ∈ 𝐵 (𝑋 + (𝑟 · 𝑌)) ∈ (𝑁‘𝐴))) |
172 | 171, 2 | elrab2 3686 |
. . 3
⊢ (𝑋 ∈ 𝑄 ↔ (𝑋 ∈ 𝑉 ∧ ∃𝑟 ∈ 𝐵 (𝑋 + (𝑟 · 𝑌)) ∈ (𝑁‘𝐴))) |
173 | 172 | simprbi 499 |
. 2
⊢ (𝑋 ∈ 𝑄 → ∃𝑟 ∈ 𝐵 (𝑋 + (𝑟 · 𝑌)) ∈ (𝑁‘𝐴)) |
174 | 168, 173 | syl 17 |
1
⊢ (𝜑 → ∃𝑟 ∈ 𝐵 (𝑋 + (𝑟 · 𝑌)) ∈ (𝑁‘𝐴)) |