Step | Hyp | Ref
| Expression |
1 | | eqid 2734 |
. . . . 5
⊢ (𝑔 ∈ 𝐹 ↦ (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑔‘𝑤) · (𝑀 Σg 𝑤))))) = (𝑔 ∈ 𝐹 ↦ (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑔‘𝑤) · (𝑀 Σg 𝑤))))) |
2 | | fveq1 6905 |
. . . . . . . . . 10
⊢ (𝑔 = (𝑣 ∈ Word 𝐴 ↦ if(𝑣 = 〈“𝑥”〉, 1, 0)) → (𝑔‘𝑤) = ((𝑣 ∈ Word 𝐴 ↦ if(𝑣 = 〈“𝑥”〉, 1, 0))‘𝑤)) |
3 | 2 | oveq1d 7445 |
. . . . . . . . 9
⊢ (𝑔 = (𝑣 ∈ Word 𝐴 ↦ if(𝑣 = 〈“𝑥”〉, 1, 0)) → ((𝑔‘𝑤) · (𝑀 Σg 𝑤)) = (((𝑣 ∈ Word 𝐴 ↦ if(𝑣 = 〈“𝑥”〉, 1, 0))‘𝑤) · (𝑀 Σg 𝑤))) |
4 | 3 | mpteq2dv 5249 |
. . . . . . . 8
⊢ (𝑔 = (𝑣 ∈ Word 𝐴 ↦ if(𝑣 = 〈“𝑥”〉, 1, 0)) → (𝑤 ∈ Word 𝐴 ↦ ((𝑔‘𝑤) · (𝑀 Σg 𝑤))) = (𝑤 ∈ Word 𝐴 ↦ (((𝑣 ∈ Word 𝐴 ↦ if(𝑣 = 〈“𝑥”〉, 1, 0))‘𝑤) · (𝑀 Σg 𝑤)))) |
5 | 4 | oveq2d 7446 |
. . . . . . 7
⊢ (𝑔 = (𝑣 ∈ Word 𝐴 ↦ if(𝑣 = 〈“𝑥”〉, 1, 0)) → (𝑅 Σg
(𝑤 ∈ Word 𝐴 ↦ ((𝑔‘𝑤) · (𝑀 Σg 𝑤)))) = (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ (((𝑣 ∈ Word 𝐴 ↦ if(𝑣 = 〈“𝑥”〉, 1, 0))‘𝑤) · (𝑀 Σg 𝑤))))) |
6 | 5 | eqeq2d 2745 |
. . . . . 6
⊢ (𝑔 = (𝑣 ∈ Word 𝐴 ↦ if(𝑣 = 〈“𝑥”〉, 1, 0)) → (𝑥 = (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑔‘𝑤) · (𝑀 Σg 𝑤)))) ↔ 𝑥 = (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ (((𝑣 ∈ Word 𝐴 ↦ if(𝑣 = 〈“𝑥”〉, 1, 0))‘𝑤) · (𝑀 Σg 𝑤)))))) |
7 | | breq1 5150 |
. . . . . . . 8
⊢ (𝑓 = (𝑣 ∈ Word 𝐴 ↦ if(𝑣 = 〈“𝑥”〉, 1, 0)) → (𝑓 finSupp 0 ↔ (𝑣 ∈ Word 𝐴 ↦ if(𝑣 = 〈“𝑥”〉, 1, 0)) finSupp
0)) |
8 | | zex 12619 |
. . . . . . . . . 10
⊢ ℤ
∈ V |
9 | 8 | a1i 11 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ℤ ∈ V) |
10 | | elrgspn.b |
. . . . . . . . . . . . . 14
⊢ 𝐵 = (Base‘𝑅) |
11 | 10 | fvexi 6920 |
. . . . . . . . . . . . 13
⊢ 𝐵 ∈ V |
12 | 11 | a1i 11 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝐵 ∈ V) |
13 | | elrgspn.a |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝐴 ⊆ 𝐵) |
14 | 12, 13 | ssexd 5329 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐴 ∈ V) |
15 | | wrdexg 14558 |
. . . . . . . . . . 11
⊢ (𝐴 ∈ V → Word 𝐴 ∈ V) |
16 | 14, 15 | syl 17 |
. . . . . . . . . 10
⊢ (𝜑 → Word 𝐴 ∈ V) |
17 | 16 | adantr 480 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → Word 𝐴 ∈ V) |
18 | | 1zzd 12645 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑣 ∈ Word 𝐴) ∧ 𝑣 = 〈“𝑥”〉) → 1 ∈
ℤ) |
19 | | 0zd 12622 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑣 ∈ Word 𝐴) ∧ ¬ 𝑣 = 〈“𝑥”〉) → 0 ∈
ℤ) |
20 | 18, 19 | ifclda 4565 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑣 ∈ Word 𝐴) → if(𝑣 = 〈“𝑥”〉, 1, 0) ∈
ℤ) |
21 | 20 | fmpttd 7134 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝑣 ∈ Word 𝐴 ↦ if(𝑣 = 〈“𝑥”〉, 1, 0)):Word 𝐴⟶ℤ) |
22 | 9, 17, 21 | elmapdd 8879 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝑣 ∈ Word 𝐴 ↦ if(𝑣 = 〈“𝑥”〉, 1, 0)) ∈ (ℤ
↑m Word 𝐴)) |
23 | 22 | elexd 3501 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝑣 ∈ Word 𝐴 ↦ if(𝑣 = 〈“𝑥”〉, 1, 0)) ∈
V) |
24 | 21 | ffund 6740 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → Fun (𝑣 ∈ Word 𝐴 ↦ if(𝑣 = 〈“𝑥”〉, 1, 0))) |
25 | | 0zd 12622 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 0 ∈ ℤ) |
26 | | snfi 9081 |
. . . . . . . . . 10
⊢
{〈“𝑥”〉} ∈ Fin |
27 | 26 | a1i 11 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → {〈“𝑥”〉} ∈ Fin) |
28 | | eldifsni 4794 |
. . . . . . . . . . . . 13
⊢ (𝑣 ∈ (Word 𝐴 ∖ {〈“𝑥”〉}) → 𝑣 ≠ 〈“𝑥”〉) |
29 | 28 | adantl 481 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑣 ∈ (Word 𝐴 ∖ {〈“𝑥”〉})) → 𝑣 ≠ 〈“𝑥”〉) |
30 | 29 | neneqd 2942 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑣 ∈ (Word 𝐴 ∖ {〈“𝑥”〉})) → ¬ 𝑣 = 〈“𝑥”〉) |
31 | 30 | iffalsed 4541 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑣 ∈ (Word 𝐴 ∖ {〈“𝑥”〉})) → if(𝑣 = 〈“𝑥”〉, 1, 0) = 0) |
32 | 31, 17 | suppss2 8223 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ((𝑣 ∈ Word 𝐴 ↦ if(𝑣 = 〈“𝑥”〉, 1, 0)) supp 0) ⊆
{〈“𝑥”〉}) |
33 | | suppssfifsupp 9417 |
. . . . . . . . 9
⊢ ((((𝑣 ∈ Word 𝐴 ↦ if(𝑣 = 〈“𝑥”〉, 1, 0)) ∈ V ∧ Fun
(𝑣 ∈ Word 𝐴 ↦ if(𝑣 = 〈“𝑥”〉, 1, 0)) ∧ 0 ∈ ℤ)
∧ ({〈“𝑥”〉} ∈ Fin ∧ ((𝑣 ∈ Word 𝐴 ↦ if(𝑣 = 〈“𝑥”〉, 1, 0)) supp 0) ⊆
{〈“𝑥”〉})) → (𝑣 ∈ Word 𝐴 ↦ if(𝑣 = 〈“𝑥”〉, 1, 0)) finSupp
0) |
34 | 23, 24, 25, 27, 32, 33 | syl32anc 1377 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝑣 ∈ Word 𝐴 ↦ if(𝑣 = 〈“𝑥”〉, 1, 0)) finSupp
0) |
35 | 7, 22, 34 | elrabd 3696 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝑣 ∈ Word 𝐴 ↦ if(𝑣 = 〈“𝑥”〉, 1, 0)) ∈ {𝑓 ∈ (ℤ
↑m Word 𝐴)
∣ 𝑓 finSupp
0}) |
36 | | elrgspn.f |
. . . . . . 7
⊢ 𝐹 = {𝑓 ∈ (ℤ ↑m Word
𝐴) ∣ 𝑓 finSupp 0} |
37 | 35, 36 | eleqtrrdi 2849 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝑣 ∈ Word 𝐴 ↦ if(𝑣 = 〈“𝑥”〉, 1, 0)) ∈ 𝐹) |
38 | | eqeq2 2746 |
. . . . . . . . . 10
⊢ (𝑥 = if(𝑤 = 〈“𝑥”〉, 𝑥, (0g‘𝑅)) → ((((𝑣 ∈ Word 𝐴 ↦ if(𝑣 = 〈“𝑥”〉, 1, 0))‘𝑤) · (𝑀 Σg 𝑤)) = 𝑥 ↔ (((𝑣 ∈ Word 𝐴 ↦ if(𝑣 = 〈“𝑥”〉, 1, 0))‘𝑤) · (𝑀 Σg 𝑤)) = if(𝑤 = 〈“𝑥”〉, 𝑥, (0g‘𝑅)))) |
39 | | eqeq2 2746 |
. . . . . . . . . 10
⊢
((0g‘𝑅) = if(𝑤 = 〈“𝑥”〉, 𝑥, (0g‘𝑅)) → ((((𝑣 ∈ Word 𝐴 ↦ if(𝑣 = 〈“𝑥”〉, 1, 0))‘𝑤) · (𝑀 Σg 𝑤)) = (0g‘𝑅) ↔ (((𝑣 ∈ Word 𝐴 ↦ if(𝑣 = 〈“𝑥”〉, 1, 0))‘𝑤) · (𝑀 Σg 𝑤)) = if(𝑤 = 〈“𝑥”〉, 𝑥, (0g‘𝑅)))) |
40 | | eqid 2734 |
. . . . . . . . . . . . 13
⊢ (𝑣 ∈ Word 𝐴 ↦ if(𝑣 = 〈“𝑥”〉, 1, 0)) = (𝑣 ∈ Word 𝐴 ↦ if(𝑣 = 〈“𝑥”〉, 1, 0)) |
41 | | simpr 484 |
. . . . . . . . . . . . . . 15
⊢
(((((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑤 ∈ Word 𝐴) ∧ 𝑤 = 〈“𝑥”〉) ∧ 𝑣 = 𝑤) → 𝑣 = 𝑤) |
42 | | simplr 769 |
. . . . . . . . . . . . . . 15
⊢
(((((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑤 ∈ Word 𝐴) ∧ 𝑤 = 〈“𝑥”〉) ∧ 𝑣 = 𝑤) → 𝑤 = 〈“𝑥”〉) |
43 | 41, 42 | eqtrd 2774 |
. . . . . . . . . . . . . 14
⊢
(((((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑤 ∈ Word 𝐴) ∧ 𝑤 = 〈“𝑥”〉) ∧ 𝑣 = 𝑤) → 𝑣 = 〈“𝑥”〉) |
44 | 43 | iftrued 4538 |
. . . . . . . . . . . . 13
⊢
(((((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑤 ∈ Word 𝐴) ∧ 𝑤 = 〈“𝑥”〉) ∧ 𝑣 = 𝑤) → if(𝑣 = 〈“𝑥”〉, 1, 0) = 1) |
45 | | simplr 769 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑤 ∈ Word 𝐴) ∧ 𝑤 = 〈“𝑥”〉) → 𝑤 ∈ Word 𝐴) |
46 | | 1zzd 12645 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑤 ∈ Word 𝐴) ∧ 𝑤 = 〈“𝑥”〉) → 1 ∈
ℤ) |
47 | 40, 44, 45, 46 | fvmptd2 7023 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑤 ∈ Word 𝐴) ∧ 𝑤 = 〈“𝑥”〉) → ((𝑣 ∈ Word 𝐴 ↦ if(𝑣 = 〈“𝑥”〉, 1, 0))‘𝑤) = 1) |
48 | | simpr 484 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑤 ∈ Word 𝐴) ∧ 𝑤 = 〈“𝑥”〉) → 𝑤 = 〈“𝑥”〉) |
49 | 48 | oveq2d 7446 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑤 ∈ Word 𝐴) ∧ 𝑤 = 〈“𝑥”〉) → (𝑀 Σg 𝑤) = (𝑀 Σg
〈“𝑥”〉)) |
50 | 13 | sselda 3994 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝑥 ∈ 𝐵) |
51 | 50 | ad2antrr 726 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑤 ∈ Word 𝐴) ∧ 𝑤 = 〈“𝑥”〉) → 𝑥 ∈ 𝐵) |
52 | | elrgspn.m |
. . . . . . . . . . . . . . . 16
⊢ 𝑀 = (mulGrp‘𝑅) |
53 | 52, 10 | mgpbas 20157 |
. . . . . . . . . . . . . . 15
⊢ 𝐵 = (Base‘𝑀) |
54 | 53 | gsumws1 18863 |
. . . . . . . . . . . . . 14
⊢ (𝑥 ∈ 𝐵 → (𝑀 Σg
〈“𝑥”〉) = 𝑥) |
55 | 51, 54 | syl 17 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑤 ∈ Word 𝐴) ∧ 𝑤 = 〈“𝑥”〉) → (𝑀 Σg
〈“𝑥”〉) = 𝑥) |
56 | 49, 55 | eqtrd 2774 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑤 ∈ Word 𝐴) ∧ 𝑤 = 〈“𝑥”〉) → (𝑀 Σg 𝑤) = 𝑥) |
57 | 47, 56 | oveq12d 7448 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑤 ∈ Word 𝐴) ∧ 𝑤 = 〈“𝑥”〉) → (((𝑣 ∈ Word 𝐴 ↦ if(𝑣 = 〈“𝑥”〉, 1, 0))‘𝑤) · (𝑀 Σg 𝑤)) = (1 · 𝑥)) |
58 | | elrgspn.x |
. . . . . . . . . . . . 13
⊢ · =
(.g‘𝑅) |
59 | 10, 58 | mulg1 19111 |
. . . . . . . . . . . 12
⊢ (𝑥 ∈ 𝐵 → (1 · 𝑥) = 𝑥) |
60 | 51, 59 | syl 17 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑤 ∈ Word 𝐴) ∧ 𝑤 = 〈“𝑥”〉) → (1 · 𝑥) = 𝑥) |
61 | 57, 60 | eqtrd 2774 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑤 ∈ Word 𝐴) ∧ 𝑤 = 〈“𝑥”〉) → (((𝑣 ∈ Word 𝐴 ↦ if(𝑣 = 〈“𝑥”〉, 1, 0))‘𝑤) · (𝑀 Σg 𝑤)) = 𝑥) |
62 | | eqeq1 2738 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑣 = 𝑤 → (𝑣 = 〈“𝑥”〉 ↔ 𝑤 = 〈“𝑥”〉)) |
63 | 62 | notbid 318 |
. . . . . . . . . . . . . . . 16
⊢ (𝑣 = 𝑤 → (¬ 𝑣 = 〈“𝑥”〉 ↔ ¬ 𝑤 = 〈“𝑥”〉)) |
64 | 63 | biimparc 479 |
. . . . . . . . . . . . . . 15
⊢ ((¬
𝑤 = 〈“𝑥”〉 ∧ 𝑣 = 𝑤) → ¬ 𝑣 = 〈“𝑥”〉) |
65 | 64 | adantll 714 |
. . . . . . . . . . . . . 14
⊢
(((((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑤 ∈ Word 𝐴) ∧ ¬ 𝑤 = 〈“𝑥”〉) ∧ 𝑣 = 𝑤) → ¬ 𝑣 = 〈“𝑥”〉) |
66 | 65 | iffalsed 4541 |
. . . . . . . . . . . . 13
⊢
(((((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑤 ∈ Word 𝐴) ∧ ¬ 𝑤 = 〈“𝑥”〉) ∧ 𝑣 = 𝑤) → if(𝑣 = 〈“𝑥”〉, 1, 0) = 0) |
67 | | simplr 769 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑤 ∈ Word 𝐴) ∧ ¬ 𝑤 = 〈“𝑥”〉) → 𝑤 ∈ Word 𝐴) |
68 | | 0zd 12622 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑤 ∈ Word 𝐴) ∧ ¬ 𝑤 = 〈“𝑥”〉) → 0 ∈
ℤ) |
69 | 40, 66, 67, 68 | fvmptd2 7023 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑤 ∈ Word 𝐴) ∧ ¬ 𝑤 = 〈“𝑥”〉) → ((𝑣 ∈ Word 𝐴 ↦ if(𝑣 = 〈“𝑥”〉, 1, 0))‘𝑤) = 0) |
70 | 69 | oveq1d 7445 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑤 ∈ Word 𝐴) ∧ ¬ 𝑤 = 〈“𝑥”〉) → (((𝑣 ∈ Word 𝐴 ↦ if(𝑣 = 〈“𝑥”〉, 1, 0))‘𝑤) · (𝑀 Σg 𝑤)) = (0 · (𝑀 Σg 𝑤))) |
71 | | elrgspn.r |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → 𝑅 ∈ Ring) |
72 | 52 | ringmgp 20256 |
. . . . . . . . . . . . . . 15
⊢ (𝑅 ∈ Ring → 𝑀 ∈ Mnd) |
73 | 71, 72 | syl 17 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 𝑀 ∈ Mnd) |
74 | 73 | ad3antrrr 730 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑤 ∈ Word 𝐴) ∧ ¬ 𝑤 = 〈“𝑥”〉) → 𝑀 ∈ Mnd) |
75 | | sswrd 14556 |
. . . . . . . . . . . . . . . . 17
⊢ (𝐴 ⊆ 𝐵 → Word 𝐴 ⊆ Word 𝐵) |
76 | 13, 75 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → Word 𝐴 ⊆ Word 𝐵) |
77 | 76 | adantr 480 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → Word 𝐴 ⊆ Word 𝐵) |
78 | 77 | sselda 3994 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑤 ∈ Word 𝐴) → 𝑤 ∈ Word 𝐵) |
79 | 78 | adantr 480 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑤 ∈ Word 𝐴) ∧ ¬ 𝑤 = 〈“𝑥”〉) → 𝑤 ∈ Word 𝐵) |
80 | 53 | gsumwcl 18864 |
. . . . . . . . . . . . 13
⊢ ((𝑀 ∈ Mnd ∧ 𝑤 ∈ Word 𝐵) → (𝑀 Σg 𝑤) ∈ 𝐵) |
81 | 74, 79, 80 | syl2anc 584 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑤 ∈ Word 𝐴) ∧ ¬ 𝑤 = 〈“𝑥”〉) → (𝑀 Σg 𝑤) ∈ 𝐵) |
82 | | eqid 2734 |
. . . . . . . . . . . . 13
⊢
(0g‘𝑅) = (0g‘𝑅) |
83 | 10, 82, 58 | mulg0 19104 |
. . . . . . . . . . . 12
⊢ ((𝑀 Σg
𝑤) ∈ 𝐵 → (0 · (𝑀 Σg 𝑤)) = (0g‘𝑅)) |
84 | 81, 83 | syl 17 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑤 ∈ Word 𝐴) ∧ ¬ 𝑤 = 〈“𝑥”〉) → (0 · (𝑀 Σg 𝑤)) = (0g‘𝑅)) |
85 | 70, 84 | eqtrd 2774 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑤 ∈ Word 𝐴) ∧ ¬ 𝑤 = 〈“𝑥”〉) → (((𝑣 ∈ Word 𝐴 ↦ if(𝑣 = 〈“𝑥”〉, 1, 0))‘𝑤) · (𝑀 Σg 𝑤)) = (0g‘𝑅)) |
86 | 38, 39, 61, 85 | ifbothda 4568 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑤 ∈ Word 𝐴) → (((𝑣 ∈ Word 𝐴 ↦ if(𝑣 = 〈“𝑥”〉, 1, 0))‘𝑤) · (𝑀 Σg 𝑤)) = if(𝑤 = 〈“𝑥”〉, 𝑥, (0g‘𝑅))) |
87 | 86 | mpteq2dva 5247 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝑤 ∈ Word 𝐴 ↦ (((𝑣 ∈ Word 𝐴 ↦ if(𝑣 = 〈“𝑥”〉, 1, 0))‘𝑤) · (𝑀 Σg 𝑤))) = (𝑤 ∈ Word 𝐴 ↦ if(𝑤 = 〈“𝑥”〉, 𝑥, (0g‘𝑅)))) |
88 | 87 | oveq2d 7446 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ (((𝑣 ∈ Word 𝐴 ↦ if(𝑣 = 〈“𝑥”〉, 1, 0))‘𝑤) · (𝑀 Σg 𝑤)))) = (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ if(𝑤 = 〈“𝑥”〉, 𝑥, (0g‘𝑅))))) |
89 | | ringmnd 20260 |
. . . . . . . . . 10
⊢ (𝑅 ∈ Ring → 𝑅 ∈ Mnd) |
90 | 71, 89 | syl 17 |
. . . . . . . . 9
⊢ (𝜑 → 𝑅 ∈ Mnd) |
91 | 90 | adantr 480 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝑅 ∈ Mnd) |
92 | | simpr 484 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝑥 ∈ 𝐴) |
93 | 92 | s1cld 14637 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 〈“𝑥”〉 ∈ Word 𝐴) |
94 | | eqid 2734 |
. . . . . . . 8
⊢ (𝑤 ∈ Word 𝐴 ↦ if(𝑤 = 〈“𝑥”〉, 𝑥, (0g‘𝑅))) = (𝑤 ∈ Word 𝐴 ↦ if(𝑤 = 〈“𝑥”〉, 𝑥, (0g‘𝑅))) |
95 | 13, 10 | sseqtrdi 4045 |
. . . . . . . . 9
⊢ (𝜑 → 𝐴 ⊆ (Base‘𝑅)) |
96 | 95 | sselda 3994 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝑥 ∈ (Base‘𝑅)) |
97 | 82, 91, 17, 93, 94, 96 | gsummptif1n0 19998 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ if(𝑤 = 〈“𝑥”〉, 𝑥, (0g‘𝑅)))) = 𝑥) |
98 | 88, 97 | eqtr2d 2775 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝑥 = (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ (((𝑣 ∈ Word 𝐴 ↦ if(𝑣 = 〈“𝑥”〉, 1, 0))‘𝑤) · (𝑀 Σg 𝑤))))) |
99 | 6, 37, 98 | rspcedvdw 3624 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ∃𝑔 ∈ 𝐹 𝑥 = (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑔‘𝑤) · (𝑀 Σg 𝑤))))) |
100 | 1, 99, 92 | elrnmptd 5976 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝑥 ∈ ran (𝑔 ∈ 𝐹 ↦ (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑔‘𝑤) · (𝑀 Σg 𝑤)))))) |
101 | | elrgspnlem1.1 |
. . . 4
⊢ 𝑆 = ran (𝑔 ∈ 𝐹 ↦ (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑔‘𝑤) · (𝑀 Σg 𝑤))))) |
102 | 100, 101 | eleqtrrdi 2849 |
. . 3
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝑥 ∈ 𝑆) |
103 | 102 | ex 412 |
. 2
⊢ (𝜑 → (𝑥 ∈ 𝐴 → 𝑥 ∈ 𝑆)) |
104 | 103 | ssrdv 4000 |
1
⊢ (𝜑 → 𝐴 ⊆ 𝑆) |