| Step | Hyp | Ref
| Expression |
| 1 | | eqid 2737 |
. . . . 5
⊢ (𝑔 ∈ 𝐹 ↦ (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑔‘𝑤) · (𝑀 Σg 𝑤))))) = (𝑔 ∈ 𝐹 ↦ (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑔‘𝑤) · (𝑀 Σg 𝑤))))) |
| 2 | | fveq1 6905 |
. . . . . . . . . 10
⊢ (𝑔 = (𝑣 ∈ Word 𝐴 ↦ if(𝑣 = 〈“𝑥”〉, 1, 0)) → (𝑔‘𝑤) = ((𝑣 ∈ Word 𝐴 ↦ if(𝑣 = 〈“𝑥”〉, 1, 0))‘𝑤)) |
| 3 | 2 | oveq1d 7446 |
. . . . . . . . 9
⊢ (𝑔 = (𝑣 ∈ Word 𝐴 ↦ if(𝑣 = 〈“𝑥”〉, 1, 0)) → ((𝑔‘𝑤) · (𝑀 Σg 𝑤)) = (((𝑣 ∈ Word 𝐴 ↦ if(𝑣 = 〈“𝑥”〉, 1, 0))‘𝑤) · (𝑀 Σg 𝑤))) |
| 4 | 3 | mpteq2dv 5244 |
. . . . . . . 8
⊢ (𝑔 = (𝑣 ∈ Word 𝐴 ↦ if(𝑣 = 〈“𝑥”〉, 1, 0)) → (𝑤 ∈ Word 𝐴 ↦ ((𝑔‘𝑤) · (𝑀 Σg 𝑤))) = (𝑤 ∈ Word 𝐴 ↦ (((𝑣 ∈ Word 𝐴 ↦ if(𝑣 = 〈“𝑥”〉, 1, 0))‘𝑤) · (𝑀 Σg 𝑤)))) |
| 5 | 4 | oveq2d 7447 |
. . . . . . 7
⊢ (𝑔 = (𝑣 ∈ Word 𝐴 ↦ if(𝑣 = 〈“𝑥”〉, 1, 0)) → (𝑅 Σg
(𝑤 ∈ Word 𝐴 ↦ ((𝑔‘𝑤) · (𝑀 Σg 𝑤)))) = (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ (((𝑣 ∈ Word 𝐴 ↦ if(𝑣 = 〈“𝑥”〉, 1, 0))‘𝑤) · (𝑀 Σg 𝑤))))) |
| 6 | 5 | eqeq2d 2748 |
. . . . . 6
⊢ (𝑔 = (𝑣 ∈ Word 𝐴 ↦ if(𝑣 = 〈“𝑥”〉, 1, 0)) → (𝑥 = (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑔‘𝑤) · (𝑀 Σg 𝑤)))) ↔ 𝑥 = (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ (((𝑣 ∈ Word 𝐴 ↦ if(𝑣 = 〈“𝑥”〉, 1, 0))‘𝑤) · (𝑀 Σg 𝑤)))))) |
| 7 | | breq1 5146 |
. . . . . . . 8
⊢ (𝑓 = (𝑣 ∈ Word 𝐴 ↦ if(𝑣 = 〈“𝑥”〉, 1, 0)) → (𝑓 finSupp 0 ↔ (𝑣 ∈ Word 𝐴 ↦ if(𝑣 = 〈“𝑥”〉, 1, 0)) finSupp
0)) |
| 8 | | zex 12622 |
. . . . . . . . . 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 5324 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐴 ∈ V) |
| 15 | | wrdexg 14562 |
. . . . . . . . . . 11
⊢ (𝐴 ∈ V → Word 𝐴 ∈ V) |
| 16 | 14, 15 | syl 17 |
. . . . . . . . . 10
⊢ (𝜑 → Word 𝐴 ∈ V) |
| 17 | 16 | adantr 480 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → Word 𝐴 ∈ V) |
| 18 | | 1zzd 12648 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑣 ∈ Word 𝐴) ∧ 𝑣 = 〈“𝑥”〉) → 1 ∈
ℤ) |
| 19 | | 0zd 12625 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑣 ∈ Word 𝐴) ∧ ¬ 𝑣 = 〈“𝑥”〉) → 0 ∈
ℤ) |
| 20 | 18, 19 | ifclda 4561 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑣 ∈ Word 𝐴) → if(𝑣 = 〈“𝑥”〉, 1, 0) ∈
ℤ) |
| 21 | 20 | fmpttd 7135 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝑣 ∈ Word 𝐴 ↦ if(𝑣 = 〈“𝑥”〉, 1, 0)):Word 𝐴⟶ℤ) |
| 22 | 9, 17, 21 | elmapdd 8881 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝑣 ∈ Word 𝐴 ↦ if(𝑣 = 〈“𝑥”〉, 1, 0)) ∈ (ℤ
↑m Word 𝐴)) |
| 23 | 22 | elexd 3504 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝑣 ∈ Word 𝐴 ↦ if(𝑣 = 〈“𝑥”〉, 1, 0)) ∈
V) |
| 24 | 21 | ffund 6740 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → Fun (𝑣 ∈ Word 𝐴 ↦ if(𝑣 = 〈“𝑥”〉, 1, 0))) |
| 25 | | 0zd 12625 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 0 ∈ ℤ) |
| 26 | | snfi 9083 |
. . . . . . . . . 10
⊢
{〈“𝑥”〉} ∈ Fin |
| 27 | 26 | a1i 11 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → {〈“𝑥”〉} ∈ Fin) |
| 28 | | eldifsni 4790 |
. . . . . . . . . . . . 13
⊢ (𝑣 ∈ (Word 𝐴 ∖ {〈“𝑥”〉}) → 𝑣 ≠ 〈“𝑥”〉) |
| 29 | 28 | adantl 481 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑣 ∈ (Word 𝐴 ∖ {〈“𝑥”〉})) → 𝑣 ≠ 〈“𝑥”〉) |
| 30 | 29 | neneqd 2945 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑣 ∈ (Word 𝐴 ∖ {〈“𝑥”〉})) → ¬ 𝑣 = 〈“𝑥”〉) |
| 31 | 30 | iffalsed 4536 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑣 ∈ (Word 𝐴 ∖ {〈“𝑥”〉})) → if(𝑣 = 〈“𝑥”〉, 1, 0) = 0) |
| 32 | 31, 17 | suppss2 8225 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ((𝑣 ∈ Word 𝐴 ↦ if(𝑣 = 〈“𝑥”〉, 1, 0)) supp 0) ⊆
{〈“𝑥”〉}) |
| 33 | | suppssfifsupp 9420 |
. . . . . . . . 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 1380 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝑣 ∈ Word 𝐴 ↦ if(𝑣 = 〈“𝑥”〉, 1, 0)) finSupp
0) |
| 35 | 7, 22, 34 | elrabd 3694 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝑣 ∈ Word 𝐴 ↦ if(𝑣 = 〈“𝑥”〉, 1, 0)) ∈ {𝑓 ∈ (ℤ
↑m Word 𝐴)
∣ 𝑓 finSupp
0}) |
| 36 | | elrgspn.f |
. . . . . . 7
⊢ 𝐹 = {𝑓 ∈ (ℤ ↑m Word
𝐴) ∣ 𝑓 finSupp 0} |
| 37 | 35, 36 | eleqtrrdi 2852 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝑣 ∈ Word 𝐴 ↦ if(𝑣 = 〈“𝑥”〉, 1, 0)) ∈ 𝐹) |
| 38 | | eqeq2 2749 |
. . . . . . . . . 10
⊢ (𝑥 = if(𝑤 = 〈“𝑥”〉, 𝑥, (0g‘𝑅)) → ((((𝑣 ∈ Word 𝐴 ↦ if(𝑣 = 〈“𝑥”〉, 1, 0))‘𝑤) · (𝑀 Σg 𝑤)) = 𝑥 ↔ (((𝑣 ∈ Word 𝐴 ↦ if(𝑣 = 〈“𝑥”〉, 1, 0))‘𝑤) · (𝑀 Σg 𝑤)) = if(𝑤 = 〈“𝑥”〉, 𝑥, (0g‘𝑅)))) |
| 39 | | eqeq2 2749 |
. . . . . . . . . 10
⊢
((0g‘𝑅) = if(𝑤 = 〈“𝑥”〉, 𝑥, (0g‘𝑅)) → ((((𝑣 ∈ Word 𝐴 ↦ if(𝑣 = 〈“𝑥”〉, 1, 0))‘𝑤) · (𝑀 Σg 𝑤)) = (0g‘𝑅) ↔ (((𝑣 ∈ Word 𝐴 ↦ if(𝑣 = 〈“𝑥”〉, 1, 0))‘𝑤) · (𝑀 Σg 𝑤)) = if(𝑤 = 〈“𝑥”〉, 𝑥, (0g‘𝑅)))) |
| 40 | | eqid 2737 |
. . . . . . . . . . . . 13
⊢ (𝑣 ∈ Word 𝐴 ↦ if(𝑣 = 〈“𝑥”〉, 1, 0)) = (𝑣 ∈ Word 𝐴 ↦ if(𝑣 = 〈“𝑥”〉, 1, 0)) |
| 41 | | simpr 484 |
. . . . . . . . . . . . . . 15
⊢
(((((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑤 ∈ Word 𝐴) ∧ 𝑤 = 〈“𝑥”〉) ∧ 𝑣 = 𝑤) → 𝑣 = 𝑤) |
| 42 | | simplr 769 |
. . . . . . . . . . . . . . 15
⊢
(((((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑤 ∈ Word 𝐴) ∧ 𝑤 = 〈“𝑥”〉) ∧ 𝑣 = 𝑤) → 𝑤 = 〈“𝑥”〉) |
| 43 | 41, 42 | eqtrd 2777 |
. . . . . . . . . . . . . 14
⊢
(((((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑤 ∈ Word 𝐴) ∧ 𝑤 = 〈“𝑥”〉) ∧ 𝑣 = 𝑤) → 𝑣 = 〈“𝑥”〉) |
| 44 | 43 | iftrued 4533 |
. . . . . . . . . . . . 13
⊢
(((((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑤 ∈ Word 𝐴) ∧ 𝑤 = 〈“𝑥”〉) ∧ 𝑣 = 𝑤) → if(𝑣 = 〈“𝑥”〉, 1, 0) = 1) |
| 45 | | simplr 769 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑤 ∈ Word 𝐴) ∧ 𝑤 = 〈“𝑥”〉) → 𝑤 ∈ Word 𝐴) |
| 46 | | 1zzd 12648 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑤 ∈ Word 𝐴) ∧ 𝑤 = 〈“𝑥”〉) → 1 ∈
ℤ) |
| 47 | 40, 44, 45, 46 | fvmptd2 7024 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑤 ∈ Word 𝐴) ∧ 𝑤 = 〈“𝑥”〉) → ((𝑣 ∈ Word 𝐴 ↦ if(𝑣 = 〈“𝑥”〉, 1, 0))‘𝑤) = 1) |
| 48 | | simpr 484 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑤 ∈ Word 𝐴) ∧ 𝑤 = 〈“𝑥”〉) → 𝑤 = 〈“𝑥”〉) |
| 49 | 48 | oveq2d 7447 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑤 ∈ Word 𝐴) ∧ 𝑤 = 〈“𝑥”〉) → (𝑀 Σg 𝑤) = (𝑀 Σg
〈“𝑥”〉)) |
| 50 | 13 | sselda 3983 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝑥 ∈ 𝐵) |
| 51 | 50 | ad2antrr 726 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑤 ∈ Word 𝐴) ∧ 𝑤 = 〈“𝑥”〉) → 𝑥 ∈ 𝐵) |
| 52 | | elrgspn.m |
. . . . . . . . . . . . . . . 16
⊢ 𝑀 = (mulGrp‘𝑅) |
| 53 | 52, 10 | mgpbas 20142 |
. . . . . . . . . . . . . . 15
⊢ 𝐵 = (Base‘𝑀) |
| 54 | 53 | gsumws1 18851 |
. . . . . . . . . . . . . 14
⊢ (𝑥 ∈ 𝐵 → (𝑀 Σg
〈“𝑥”〉) = 𝑥) |
| 55 | 51, 54 | syl 17 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑤 ∈ Word 𝐴) ∧ 𝑤 = 〈“𝑥”〉) → (𝑀 Σg
〈“𝑥”〉) = 𝑥) |
| 56 | 49, 55 | eqtrd 2777 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑤 ∈ Word 𝐴) ∧ 𝑤 = 〈“𝑥”〉) → (𝑀 Σg 𝑤) = 𝑥) |
| 57 | 47, 56 | oveq12d 7449 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑤 ∈ Word 𝐴) ∧ 𝑤 = 〈“𝑥”〉) → (((𝑣 ∈ Word 𝐴 ↦ if(𝑣 = 〈“𝑥”〉, 1, 0))‘𝑤) · (𝑀 Σg 𝑤)) = (1 · 𝑥)) |
| 58 | | elrgspn.x |
. . . . . . . . . . . . 13
⊢ · =
(.g‘𝑅) |
| 59 | 10, 58 | mulg1 19099 |
. . . . . . . . . . . 12
⊢ (𝑥 ∈ 𝐵 → (1 · 𝑥) = 𝑥) |
| 60 | 51, 59 | syl 17 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑤 ∈ Word 𝐴) ∧ 𝑤 = 〈“𝑥”〉) → (1 · 𝑥) = 𝑥) |
| 61 | 57, 60 | eqtrd 2777 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑤 ∈ Word 𝐴) ∧ 𝑤 = 〈“𝑥”〉) → (((𝑣 ∈ Word 𝐴 ↦ if(𝑣 = 〈“𝑥”〉, 1, 0))‘𝑤) · (𝑀 Σg 𝑤)) = 𝑥) |
| 62 | | eqeq1 2741 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑣 = 𝑤 → (𝑣 = 〈“𝑥”〉 ↔ 𝑤 = 〈“𝑥”〉)) |
| 63 | 62 | notbid 318 |
. . . . . . . . . . . . . . . 16
⊢ (𝑣 = 𝑤 → (¬ 𝑣 = 〈“𝑥”〉 ↔ ¬ 𝑤 = 〈“𝑥”〉)) |
| 64 | 63 | biimparc 479 |
. . . . . . . . . . . . . . 15
⊢ ((¬
𝑤 = 〈“𝑥”〉 ∧ 𝑣 = 𝑤) → ¬ 𝑣 = 〈“𝑥”〉) |
| 65 | 64 | adantll 714 |
. . . . . . . . . . . . . 14
⊢
(((((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑤 ∈ Word 𝐴) ∧ ¬ 𝑤 = 〈“𝑥”〉) ∧ 𝑣 = 𝑤) → ¬ 𝑣 = 〈“𝑥”〉) |
| 66 | 65 | iffalsed 4536 |
. . . . . . . . . . . . 13
⊢
(((((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑤 ∈ Word 𝐴) ∧ ¬ 𝑤 = 〈“𝑥”〉) ∧ 𝑣 = 𝑤) → if(𝑣 = 〈“𝑥”〉, 1, 0) = 0) |
| 67 | | simplr 769 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑤 ∈ Word 𝐴) ∧ ¬ 𝑤 = 〈“𝑥”〉) → 𝑤 ∈ Word 𝐴) |
| 68 | | 0zd 12625 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑤 ∈ Word 𝐴) ∧ ¬ 𝑤 = 〈“𝑥”〉) → 0 ∈
ℤ) |
| 69 | 40, 66, 67, 68 | fvmptd2 7024 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑤 ∈ Word 𝐴) ∧ ¬ 𝑤 = 〈“𝑥”〉) → ((𝑣 ∈ Word 𝐴 ↦ if(𝑣 = 〈“𝑥”〉, 1, 0))‘𝑤) = 0) |
| 70 | 69 | oveq1d 7446 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑤 ∈ Word 𝐴) ∧ ¬ 𝑤 = 〈“𝑥”〉) → (((𝑣 ∈ Word 𝐴 ↦ if(𝑣 = 〈“𝑥”〉, 1, 0))‘𝑤) · (𝑀 Σg 𝑤)) = (0 · (𝑀 Σg 𝑤))) |
| 71 | | elrgspn.r |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → 𝑅 ∈ Ring) |
| 72 | 52 | ringmgp 20236 |
. . . . . . . . . . . . . . 15
⊢ (𝑅 ∈ Ring → 𝑀 ∈ Mnd) |
| 73 | 71, 72 | syl 17 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 𝑀 ∈ Mnd) |
| 74 | 73 | ad3antrrr 730 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑤 ∈ Word 𝐴) ∧ ¬ 𝑤 = 〈“𝑥”〉) → 𝑀 ∈ Mnd) |
| 75 | | sswrd 14560 |
. . . . . . . . . . . . . . . . 17
⊢ (𝐴 ⊆ 𝐵 → Word 𝐴 ⊆ Word 𝐵) |
| 76 | 13, 75 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → Word 𝐴 ⊆ Word 𝐵) |
| 77 | 76 | adantr 480 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → Word 𝐴 ⊆ Word 𝐵) |
| 78 | 77 | sselda 3983 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑤 ∈ Word 𝐴) → 𝑤 ∈ Word 𝐵) |
| 79 | 78 | adantr 480 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑤 ∈ Word 𝐴) ∧ ¬ 𝑤 = 〈“𝑥”〉) → 𝑤 ∈ Word 𝐵) |
| 80 | 53 | gsumwcl 18852 |
. . . . . . . . . . . . 13
⊢ ((𝑀 ∈ Mnd ∧ 𝑤 ∈ Word 𝐵) → (𝑀 Σg 𝑤) ∈ 𝐵) |
| 81 | 74, 79, 80 | syl2anc 584 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑤 ∈ Word 𝐴) ∧ ¬ 𝑤 = 〈“𝑥”〉) → (𝑀 Σg 𝑤) ∈ 𝐵) |
| 82 | | eqid 2737 |
. . . . . . . . . . . . 13
⊢
(0g‘𝑅) = (0g‘𝑅) |
| 83 | 10, 82, 58 | mulg0 19092 |
. . . . . . . . . . . 12
⊢ ((𝑀 Σg
𝑤) ∈ 𝐵 → (0 · (𝑀 Σg 𝑤)) = (0g‘𝑅)) |
| 84 | 81, 83 | syl 17 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑤 ∈ Word 𝐴) ∧ ¬ 𝑤 = 〈“𝑥”〉) → (0 · (𝑀 Σg 𝑤)) = (0g‘𝑅)) |
| 85 | 70, 84 | eqtrd 2777 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑤 ∈ Word 𝐴) ∧ ¬ 𝑤 = 〈“𝑥”〉) → (((𝑣 ∈ Word 𝐴 ↦ if(𝑣 = 〈“𝑥”〉, 1, 0))‘𝑤) · (𝑀 Σg 𝑤)) = (0g‘𝑅)) |
| 86 | 38, 39, 61, 85 | ifbothda 4564 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑤 ∈ Word 𝐴) → (((𝑣 ∈ Word 𝐴 ↦ if(𝑣 = 〈“𝑥”〉, 1, 0))‘𝑤) · (𝑀 Σg 𝑤)) = if(𝑤 = 〈“𝑥”〉, 𝑥, (0g‘𝑅))) |
| 87 | 86 | mpteq2dva 5242 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝑤 ∈ Word 𝐴 ↦ (((𝑣 ∈ Word 𝐴 ↦ if(𝑣 = 〈“𝑥”〉, 1, 0))‘𝑤) · (𝑀 Σg 𝑤))) = (𝑤 ∈ Word 𝐴 ↦ if(𝑤 = 〈“𝑥”〉, 𝑥, (0g‘𝑅)))) |
| 88 | 87 | oveq2d 7447 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ (((𝑣 ∈ Word 𝐴 ↦ if(𝑣 = 〈“𝑥”〉, 1, 0))‘𝑤) · (𝑀 Σg 𝑤)))) = (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ if(𝑤 = 〈“𝑥”〉, 𝑥, (0g‘𝑅))))) |
| 89 | | ringmnd 20240 |
. . . . . . . . . 10
⊢ (𝑅 ∈ Ring → 𝑅 ∈ Mnd) |
| 90 | 71, 89 | syl 17 |
. . . . . . . . 9
⊢ (𝜑 → 𝑅 ∈ Mnd) |
| 91 | 90 | adantr 480 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝑅 ∈ Mnd) |
| 92 | | simpr 484 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝑥 ∈ 𝐴) |
| 93 | 92 | s1cld 14641 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 〈“𝑥”〉 ∈ Word 𝐴) |
| 94 | | eqid 2737 |
. . . . . . . 8
⊢ (𝑤 ∈ Word 𝐴 ↦ if(𝑤 = 〈“𝑥”〉, 𝑥, (0g‘𝑅))) = (𝑤 ∈ Word 𝐴 ↦ if(𝑤 = 〈“𝑥”〉, 𝑥, (0g‘𝑅))) |
| 95 | 13, 10 | sseqtrdi 4024 |
. . . . . . . . 9
⊢ (𝜑 → 𝐴 ⊆ (Base‘𝑅)) |
| 96 | 95 | sselda 3983 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝑥 ∈ (Base‘𝑅)) |
| 97 | 82, 91, 17, 93, 94, 96 | gsummptif1n0 19984 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ if(𝑤 = 〈“𝑥”〉, 𝑥, (0g‘𝑅)))) = 𝑥) |
| 98 | 88, 97 | eqtr2d 2778 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝑥 = (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ (((𝑣 ∈ Word 𝐴 ↦ if(𝑣 = 〈“𝑥”〉, 1, 0))‘𝑤) · (𝑀 Σg 𝑤))))) |
| 99 | 6, 37, 98 | rspcedvdw 3625 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ∃𝑔 ∈ 𝐹 𝑥 = (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑔‘𝑤) · (𝑀 Σg 𝑤))))) |
| 100 | 1, 99, 92 | elrnmptd 5974 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝑥 ∈ ran (𝑔 ∈ 𝐹 ↦ (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑔‘𝑤) · (𝑀 Σg 𝑤)))))) |
| 101 | | elrgspnlem1.1 |
. . . 4
⊢ 𝑆 = ran (𝑔 ∈ 𝐹 ↦ (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑔‘𝑤) · (𝑀 Σg 𝑤))))) |
| 102 | 100, 101 | eleqtrrdi 2852 |
. . 3
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝑥 ∈ 𝑆) |
| 103 | 102 | ex 412 |
. 2
⊢ (𝜑 → (𝑥 ∈ 𝐴 → 𝑥 ∈ 𝑆)) |
| 104 | 103 | ssrdv 3989 |
1
⊢ (𝜑 → 𝐴 ⊆ 𝑆) |