| Step | Hyp | Ref
| Expression |
| 1 | | elrgspn.r |
. . 3
⊢ (𝜑 → 𝑅 ∈ Ring) |
| 2 | 1 | ringgrpd 20239 |
. 2
⊢ (𝜑 → 𝑅 ∈ Grp) |
| 3 | | simpr 484 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 𝑥 ∈ 𝑆) ∧ 𝑔 ∈ 𝐹) ∧ 𝑥 = (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑔‘𝑤) · (𝑀 Σg 𝑤))))) → 𝑥 = (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑔‘𝑤) · (𝑀 Σg 𝑤))))) |
| 4 | | elrgspn.b |
. . . . . . . . . 10
⊢ 𝐵 = (Base‘𝑅) |
| 5 | | eqid 2737 |
. . . . . . . . . 10
⊢
(0g‘𝑅) = (0g‘𝑅) |
| 6 | 1 | ringcmnd 20281 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝑅 ∈ CMnd) |
| 7 | 6 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑔 ∈ 𝐹) → 𝑅 ∈ CMnd) |
| 8 | 4 | fvexi 6920 |
. . . . . . . . . . . . . 14
⊢ 𝐵 ∈ V |
| 9 | 8 | a1i 11 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝐵 ∈ V) |
| 10 | | elrgspn.a |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝐴 ⊆ 𝐵) |
| 11 | 9, 10 | ssexd 5324 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝐴 ∈ V) |
| 12 | | wrdexg 14562 |
. . . . . . . . . . . 12
⊢ (𝐴 ∈ V → Word 𝐴 ∈ V) |
| 13 | 11, 12 | syl 17 |
. . . . . . . . . . 11
⊢ (𝜑 → Word 𝐴 ∈ V) |
| 14 | 13 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑔 ∈ 𝐹) → Word 𝐴 ∈ V) |
| 15 | | elrgspn.x |
. . . . . . . . . . . 12
⊢ · =
(.g‘𝑅) |
| 16 | 2 | ad2antrr 726 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑤 ∈ Word 𝐴) → 𝑅 ∈ Grp) |
| 17 | | elrgspn.f |
. . . . . . . . . . . . . . . . 17
⊢ 𝐹 = {𝑓 ∈ (ℤ ↑m Word
𝐴) ∣ 𝑓 finSupp 0} |
| 18 | 17 | ssrab3 4082 |
. . . . . . . . . . . . . . . 16
⊢ 𝐹 ⊆ (ℤ
↑m Word 𝐴) |
| 19 | 18 | a1i 11 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → 𝐹 ⊆ (ℤ ↑m Word
𝐴)) |
| 20 | 19 | sselda 3983 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑔 ∈ 𝐹) → 𝑔 ∈ (ℤ ↑m Word
𝐴)) |
| 21 | | zex 12622 |
. . . . . . . . . . . . . . . . 17
⊢ ℤ
∈ V |
| 22 | 21 | a1i 11 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → ℤ ∈
V) |
| 23 | 22, 13 | elmapd 8880 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (𝑔 ∈ (ℤ ↑m Word
𝐴) ↔ 𝑔:Word 𝐴⟶ℤ)) |
| 24 | 23 | adantr 480 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑔 ∈ 𝐹) → (𝑔 ∈ (ℤ ↑m Word
𝐴) ↔ 𝑔:Word 𝐴⟶ℤ)) |
| 25 | 20, 24 | mpbid 232 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑔 ∈ 𝐹) → 𝑔:Word 𝐴⟶ℤ) |
| 26 | 25 | ffvelcdmda 7104 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑤 ∈ Word 𝐴) → (𝑔‘𝑤) ∈ ℤ) |
| 27 | | elrgspn.m |
. . . . . . . . . . . . . . . 16
⊢ 𝑀 = (mulGrp‘𝑅) |
| 28 | 27 | ringmgp 20236 |
. . . . . . . . . . . . . . 15
⊢ (𝑅 ∈ Ring → 𝑀 ∈ Mnd) |
| 29 | 1, 28 | syl 17 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 𝑀 ∈ Mnd) |
| 30 | | sswrd 14560 |
. . . . . . . . . . . . . . . 16
⊢ (𝐴 ⊆ 𝐵 → Word 𝐴 ⊆ Word 𝐵) |
| 31 | 10, 30 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → Word 𝐴 ⊆ Word 𝐵) |
| 32 | 31 | sselda 3983 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑤 ∈ Word 𝐴) → 𝑤 ∈ Word 𝐵) |
| 33 | 27, 4 | mgpbas 20142 |
. . . . . . . . . . . . . . 15
⊢ 𝐵 = (Base‘𝑀) |
| 34 | 33 | gsumwcl 18852 |
. . . . . . . . . . . . . 14
⊢ ((𝑀 ∈ Mnd ∧ 𝑤 ∈ Word 𝐵) → (𝑀 Σg 𝑤) ∈ 𝐵) |
| 35 | 29, 32, 34 | syl2an2r 685 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑤 ∈ Word 𝐴) → (𝑀 Σg 𝑤) ∈ 𝐵) |
| 36 | 35 | adantlr 715 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑤 ∈ Word 𝐴) → (𝑀 Σg 𝑤) ∈ 𝐵) |
| 37 | 4, 15, 16, 26, 36 | mulgcld 19114 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑤 ∈ Word 𝐴) → ((𝑔‘𝑤) · (𝑀 Σg 𝑤)) ∈ 𝐵) |
| 38 | 37 | fmpttd 7135 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑔 ∈ 𝐹) → (𝑤 ∈ Word 𝐴 ↦ ((𝑔‘𝑤) · (𝑀 Σg 𝑤))):Word 𝐴⟶𝐵) |
| 39 | | fvexd 6921 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑔 ∈ 𝐹) → (0g‘𝑅) ∈ V) |
| 40 | | 0zd 12625 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑔 ∈ 𝐹) → 0 ∈ ℤ) |
| 41 | | ssidd 4007 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑔 ∈ 𝐹) → Word 𝐴 ⊆ Word 𝐴) |
| 42 | | breq1 5146 |
. . . . . . . . . . . . . 14
⊢ (𝑓 = 𝑔 → (𝑓 finSupp 0 ↔ 𝑔 finSupp 0)) |
| 43 | 42, 17 | elrab2 3695 |
. . . . . . . . . . . . 13
⊢ (𝑔 ∈ 𝐹 ↔ (𝑔 ∈ (ℤ ↑m Word
𝐴) ∧ 𝑔 finSupp 0)) |
| 44 | 43 | simprbi 496 |
. . . . . . . . . . . 12
⊢ (𝑔 ∈ 𝐹 → 𝑔 finSupp 0) |
| 45 | 44 | adantl 481 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑔 ∈ 𝐹) → 𝑔 finSupp 0) |
| 46 | 4, 5, 15 | mulg0 19092 |
. . . . . . . . . . . 12
⊢ (𝑦 ∈ 𝐵 → (0 · 𝑦) = (0g‘𝑅)) |
| 47 | 46 | adantl 481 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑦 ∈ 𝐵) → (0 · 𝑦) = (0g‘𝑅)) |
| 48 | 39, 40, 14, 41, 36, 25, 45, 47 | fisuppov1 32692 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑔 ∈ 𝐹) → (𝑤 ∈ Word 𝐴 ↦ ((𝑔‘𝑤) · (𝑀 Σg 𝑤))) finSupp
(0g‘𝑅)) |
| 49 | 4, 5, 7, 14, 38, 48 | gsumcl 19933 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑔 ∈ 𝐹) → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑔‘𝑤) · (𝑀 Σg 𝑤)))) ∈ 𝐵) |
| 50 | 49 | ad4ant13 751 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 𝑥 ∈ 𝑆) ∧ 𝑔 ∈ 𝐹) ∧ 𝑥 = (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑔‘𝑤) · (𝑀 Σg 𝑤))))) → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑔‘𝑤) · (𝑀 Σg 𝑤)))) ∈ 𝐵) |
| 51 | 3, 50 | eqeltrd 2841 |
. . . . . . 7
⊢ ((((𝜑 ∧ 𝑥 ∈ 𝑆) ∧ 𝑔 ∈ 𝐹) ∧ 𝑥 = (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑔‘𝑤) · (𝑀 Σg 𝑤))))) → 𝑥 ∈ 𝐵) |
| 52 | | elrgspnlem1.1 |
. . . . . . . . . 10
⊢ 𝑆 = ran (𝑔 ∈ 𝐹 ↦ (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑔‘𝑤) · (𝑀 Σg 𝑤))))) |
| 53 | 52 | eleq2i 2833 |
. . . . . . . . 9
⊢ (𝑥 ∈ 𝑆 ↔ 𝑥 ∈ ran (𝑔 ∈ 𝐹 ↦ (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑔‘𝑤) · (𝑀 Σg 𝑤)))))) |
| 54 | | eqid 2737 |
. . . . . . . . . . 11
⊢ (𝑔 ∈ 𝐹 ↦ (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑔‘𝑤) · (𝑀 Σg 𝑤))))) = (𝑔 ∈ 𝐹 ↦ (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑔‘𝑤) · (𝑀 Σg 𝑤))))) |
| 55 | 54 | elrnmpt 5969 |
. . . . . . . . . 10
⊢ (𝑥 ∈ V → (𝑥 ∈ ran (𝑔 ∈ 𝐹 ↦ (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑔‘𝑤) · (𝑀 Σg 𝑤))))) ↔ ∃𝑔 ∈ 𝐹 𝑥 = (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑔‘𝑤) · (𝑀 Σg 𝑤)))))) |
| 56 | 55 | elv 3485 |
. . . . . . . . 9
⊢ (𝑥 ∈ ran (𝑔 ∈ 𝐹 ↦ (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑔‘𝑤) · (𝑀 Σg 𝑤))))) ↔ ∃𝑔 ∈ 𝐹 𝑥 = (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑔‘𝑤) · (𝑀 Σg 𝑤))))) |
| 57 | 53, 56 | sylbb 219 |
. . . . . . . 8
⊢ (𝑥 ∈ 𝑆 → ∃𝑔 ∈ 𝐹 𝑥 = (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑔‘𝑤) · (𝑀 Σg 𝑤))))) |
| 58 | 57 | adantl 481 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → ∃𝑔 ∈ 𝐹 𝑥 = (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑔‘𝑤) · (𝑀 Σg 𝑤))))) |
| 59 | 51, 58 | r19.29a 3162 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → 𝑥 ∈ 𝐵) |
| 60 | 59, 4 | eleqtrdi 2851 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → 𝑥 ∈ (Base‘𝑅)) |
| 61 | 60 | ex 412 |
. . . 4
⊢ (𝜑 → (𝑥 ∈ 𝑆 → 𝑥 ∈ (Base‘𝑅))) |
| 62 | 61 | ssrdv 3989 |
. . 3
⊢ (𝜑 → 𝑆 ⊆ (Base‘𝑅)) |
| 63 | 62, 4 | sseqtrrdi 4025 |
. 2
⊢ (𝜑 → 𝑆 ⊆ 𝐵) |
| 64 | | breq1 5146 |
. . . . . . . 8
⊢ (𝑓 = (Word 𝐴 × {0}) → (𝑓 finSupp 0 ↔ (Word 𝐴 × {0}) finSupp 0)) |
| 65 | | 0z 12624 |
. . . . . . . . . . 11
⊢ 0 ∈
ℤ |
| 66 | 65 | fconst6 6798 |
. . . . . . . . . 10
⊢ (Word
𝐴 × {0}):Word 𝐴⟶ℤ |
| 67 | 66 | a1i 11 |
. . . . . . . . 9
⊢ (𝜑 → (Word 𝐴 × {0}):Word 𝐴⟶ℤ) |
| 68 | 22, 13, 67 | elmapdd 8881 |
. . . . . . . 8
⊢ (𝜑 → (Word 𝐴 × {0}) ∈ (ℤ
↑m Word 𝐴)) |
| 69 | | c0ex 11255 |
. . . . . . . . . 10
⊢ 0 ∈
V |
| 70 | 69 | a1i 11 |
. . . . . . . . 9
⊢ (𝜑 → 0 ∈
V) |
| 71 | 13, 70 | fczfsuppd 9426 |
. . . . . . . 8
⊢ (𝜑 → (Word 𝐴 × {0}) finSupp 0) |
| 72 | 64, 68, 71 | elrabd 3694 |
. . . . . . 7
⊢ (𝜑 → (Word 𝐴 × {0}) ∈ {𝑓 ∈ (ℤ ↑m Word
𝐴) ∣ 𝑓 finSupp 0}) |
| 73 | 72, 17 | eleqtrrdi 2852 |
. . . . . 6
⊢ (𝜑 → (Word 𝐴 × {0}) ∈ 𝐹) |
| 74 | | simplr 769 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑔 = (Word 𝐴 × {0})) ∧ 𝑤 ∈ Word 𝐴) → 𝑔 = (Word 𝐴 × {0})) |
| 75 | 74 | fveq1d 6908 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑔 = (Word 𝐴 × {0})) ∧ 𝑤 ∈ Word 𝐴) → (𝑔‘𝑤) = ((Word 𝐴 × {0})‘𝑤)) |
| 76 | 69 | fconst 6794 |
. . . . . . . . . . . . . . 15
⊢ (Word
𝐴 × {0}):Word 𝐴⟶{0} |
| 77 | 76 | a1i 11 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑔 = (Word 𝐴 × {0})) ∧ 𝑤 ∈ Word 𝐴) → (Word 𝐴 × {0}):Word 𝐴⟶{0}) |
| 78 | | simpr 484 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑔 = (Word 𝐴 × {0})) ∧ 𝑤 ∈ Word 𝐴) → 𝑤 ∈ Word 𝐴) |
| 79 | | fvconst 7184 |
. . . . . . . . . . . . . 14
⊢ (((Word
𝐴 × {0}):Word 𝐴⟶{0} ∧ 𝑤 ∈ Word 𝐴) → ((Word 𝐴 × {0})‘𝑤) = 0) |
| 80 | 77, 78, 79 | syl2anc 584 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑔 = (Word 𝐴 × {0})) ∧ 𝑤 ∈ Word 𝐴) → ((Word 𝐴 × {0})‘𝑤) = 0) |
| 81 | 75, 80 | eqtrd 2777 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑔 = (Word 𝐴 × {0})) ∧ 𝑤 ∈ Word 𝐴) → (𝑔‘𝑤) = 0) |
| 82 | 81 | oveq1d 7446 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑔 = (Word 𝐴 × {0})) ∧ 𝑤 ∈ Word 𝐴) → ((𝑔‘𝑤) · (𝑀 Σg 𝑤)) = (0 · (𝑀 Σg 𝑤))) |
| 83 | 35 | adantlr 715 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑔 = (Word 𝐴 × {0})) ∧ 𝑤 ∈ Word 𝐴) → (𝑀 Σg 𝑤) ∈ 𝐵) |
| 84 | 4, 5, 15 | mulg0 19092 |
. . . . . . . . . . . 12
⊢ ((𝑀 Σg
𝑤) ∈ 𝐵 → (0 · (𝑀 Σg 𝑤)) = (0g‘𝑅)) |
| 85 | 83, 84 | syl 17 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑔 = (Word 𝐴 × {0})) ∧ 𝑤 ∈ Word 𝐴) → (0 · (𝑀 Σg 𝑤)) = (0g‘𝑅)) |
| 86 | 82, 85 | eqtrd 2777 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑔 = (Word 𝐴 × {0})) ∧ 𝑤 ∈ Word 𝐴) → ((𝑔‘𝑤) · (𝑀 Σg 𝑤)) = (0g‘𝑅)) |
| 87 | 86 | mpteq2dva 5242 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑔 = (Word 𝐴 × {0})) → (𝑤 ∈ Word 𝐴 ↦ ((𝑔‘𝑤) · (𝑀 Σg 𝑤))) = (𝑤 ∈ Word 𝐴 ↦ (0g‘𝑅))) |
| 88 | 87 | oveq2d 7447 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑔 = (Word 𝐴 × {0})) → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑔‘𝑤) · (𝑀 Σg 𝑤)))) = (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ (0g‘𝑅)))) |
| 89 | 6 | cmnmndd 19822 |
. . . . . . . . . 10
⊢ (𝜑 → 𝑅 ∈ Mnd) |
| 90 | 5 | gsumz 18849 |
. . . . . . . . . 10
⊢ ((𝑅 ∈ Mnd ∧ Word 𝐴 ∈ V) → (𝑅 Σg
(𝑤 ∈ Word 𝐴 ↦
(0g‘𝑅))) =
(0g‘𝑅)) |
| 91 | 89, 13, 90 | syl2anc 584 |
. . . . . . . . 9
⊢ (𝜑 → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ (0g‘𝑅))) = (0g‘𝑅)) |
| 92 | 91 | adantr 480 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑔 = (Word 𝐴 × {0})) → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ (0g‘𝑅))) = (0g‘𝑅)) |
| 93 | 88, 92 | eqtrd 2777 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑔 = (Word 𝐴 × {0})) → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑔‘𝑤) · (𝑀 Σg 𝑤)))) =
(0g‘𝑅)) |
| 94 | 93 | eqeq2d 2748 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑔 = (Word 𝐴 × {0})) →
((0g‘𝑅) =
(𝑅
Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑔‘𝑤) · (𝑀 Σg 𝑤)))) ↔
(0g‘𝑅) =
(0g‘𝑅))) |
| 95 | | eqidd 2738 |
. . . . . 6
⊢ (𝜑 → (0g‘𝑅) = (0g‘𝑅)) |
| 96 | 73, 94, 95 | rspcedvd 3624 |
. . . . 5
⊢ (𝜑 → ∃𝑔 ∈ 𝐹 (0g‘𝑅) = (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑔‘𝑤) · (𝑀 Σg 𝑤))))) |
| 97 | | fvexd 6921 |
. . . . 5
⊢ (𝜑 → (0g‘𝑅) ∈ V) |
| 98 | 54, 96, 97 | elrnmptd 5974 |
. . . 4
⊢ (𝜑 → (0g‘𝑅) ∈ ran (𝑔 ∈ 𝐹 ↦ (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑔‘𝑤) · (𝑀 Σg 𝑤)))))) |
| 99 | 98, 52 | eleqtrrdi 2852 |
. . 3
⊢ (𝜑 → (0g‘𝑅) ∈ 𝑆) |
| 100 | 99 | ne0d 4342 |
. 2
⊢ (𝜑 → 𝑆 ≠ ∅) |
| 101 | | simpllr 776 |
. . . . . . . . 9
⊢
(((((((𝜑 ∧ 𝑥 ∈ 𝑆) ∧ 𝑦 ∈ 𝑆) ∧ 𝑔 ∈ 𝐹) ∧ 𝑥 = (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑔‘𝑤) · (𝑀 Σg 𝑤))))) ∧ 𝑖 ∈ 𝐹) ∧ 𝑦 = (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑖‘𝑤) · (𝑀 Σg 𝑤))))) → 𝑥 = (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑔‘𝑤) · (𝑀 Σg 𝑤))))) |
| 102 | | simpr 484 |
. . . . . . . . 9
⊢
(((((((𝜑 ∧ 𝑥 ∈ 𝑆) ∧ 𝑦 ∈ 𝑆) ∧ 𝑔 ∈ 𝐹) ∧ 𝑥 = (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑔‘𝑤) · (𝑀 Σg 𝑤))))) ∧ 𝑖 ∈ 𝐹) ∧ 𝑦 = (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑖‘𝑤) · (𝑀 Σg 𝑤))))) → 𝑦 = (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑖‘𝑤) · (𝑀 Σg 𝑤))))) |
| 103 | 101, 102 | oveq12d 7449 |
. . . . . . . 8
⊢
(((((((𝜑 ∧ 𝑥 ∈ 𝑆) ∧ 𝑦 ∈ 𝑆) ∧ 𝑔 ∈ 𝐹) ∧ 𝑥 = (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑔‘𝑤) · (𝑀 Σg 𝑤))))) ∧ 𝑖 ∈ 𝐹) ∧ 𝑦 = (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑖‘𝑤) · (𝑀 Σg 𝑤))))) → (𝑥(+g‘𝑅)𝑦) = ((𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑔‘𝑤) · (𝑀 Σg 𝑤))))(+g‘𝑅)(𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑖‘𝑤) · (𝑀 Σg 𝑤)))))) |
| 104 | | eqid 2737 |
. . . . . . . . . . . . . 14
⊢
(+g‘𝑅) = (+g‘𝑅) |
| 105 | 7 | adantr 480 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) → 𝑅 ∈ CMnd) |
| 106 | 14 | adantr 480 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) → Word 𝐴 ∈ V) |
| 107 | 37 | adantlr 715 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑤 ∈ Word 𝐴) → ((𝑔‘𝑤) · (𝑀 Σg 𝑤)) ∈ 𝐵) |
| 108 | 2 | ad2antrr 726 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑖 ∈ 𝐹) ∧ 𝑤 ∈ Word 𝐴) → 𝑅 ∈ Grp) |
| 109 | | breq1 5146 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑓 = 𝑖 → (𝑓 finSupp 0 ↔ 𝑖 finSupp 0)) |
| 110 | 109, 17 | elrab2 3695 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑖 ∈ 𝐹 ↔ (𝑖 ∈ (ℤ ↑m Word
𝐴) ∧ 𝑖 finSupp 0)) |
| 111 | 110 | simplbi 497 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑖 ∈ 𝐹 → 𝑖 ∈ (ℤ ↑m Word
𝐴)) |
| 112 | 111 | adantl 481 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑖 ∈ 𝐹) → 𝑖 ∈ (ℤ ↑m Word
𝐴)) |
| 113 | 22, 13 | elmapd 8880 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → (𝑖 ∈ (ℤ ↑m Word
𝐴) ↔ 𝑖:Word 𝐴⟶ℤ)) |
| 114 | 113 | adantr 480 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑖 ∈ 𝐹) → (𝑖 ∈ (ℤ ↑m Word
𝐴) ↔ 𝑖:Word 𝐴⟶ℤ)) |
| 115 | 112, 114 | mpbid 232 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑖 ∈ 𝐹) → 𝑖:Word 𝐴⟶ℤ) |
| 116 | 115 | ffvelcdmda 7104 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑖 ∈ 𝐹) ∧ 𝑤 ∈ Word 𝐴) → (𝑖‘𝑤) ∈ ℤ) |
| 117 | 35 | adantlr 715 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑖 ∈ 𝐹) ∧ 𝑤 ∈ Word 𝐴) → (𝑀 Σg 𝑤) ∈ 𝐵) |
| 118 | 4, 15, 108, 116, 117 | mulgcld 19114 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑖 ∈ 𝐹) ∧ 𝑤 ∈ Word 𝐴) → ((𝑖‘𝑤) · (𝑀 Σg 𝑤)) ∈ 𝐵) |
| 119 | 118 | adantllr 719 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑤 ∈ Word 𝐴) → ((𝑖‘𝑤) · (𝑀 Σg 𝑤)) ∈ 𝐵) |
| 120 | | eqidd 2738 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) → (𝑤 ∈ Word 𝐴 ↦ ((𝑔‘𝑤) · (𝑀 Σg 𝑤))) = (𝑤 ∈ Word 𝐴 ↦ ((𝑔‘𝑤) · (𝑀 Σg 𝑤)))) |
| 121 | | eqidd 2738 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) → (𝑤 ∈ Word 𝐴 ↦ ((𝑖‘𝑤) · (𝑀 Σg 𝑤))) = (𝑤 ∈ Word 𝐴 ↦ ((𝑖‘𝑤) · (𝑀 Σg 𝑤)))) |
| 122 | 48 | adantr 480 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) → (𝑤 ∈ Word 𝐴 ↦ ((𝑔‘𝑤) · (𝑀 Σg 𝑤))) finSupp
(0g‘𝑅)) |
| 123 | 48 | ralrimiva 3146 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → ∀𝑔 ∈ 𝐹 (𝑤 ∈ Word 𝐴 ↦ ((𝑔‘𝑤) · (𝑀 Σg 𝑤))) finSupp
(0g‘𝑅)) |
| 124 | | fveq1 6905 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑔 = 𝑖 → (𝑔‘𝑤) = (𝑖‘𝑤)) |
| 125 | 124 | oveq1d 7446 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑔 = 𝑖 → ((𝑔‘𝑤) · (𝑀 Σg 𝑤)) = ((𝑖‘𝑤) · (𝑀 Σg 𝑤))) |
| 126 | 125 | mpteq2dv 5244 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑔 = 𝑖 → (𝑤 ∈ Word 𝐴 ↦ ((𝑔‘𝑤) · (𝑀 Σg 𝑤))) = (𝑤 ∈ Word 𝐴 ↦ ((𝑖‘𝑤) · (𝑀 Σg 𝑤)))) |
| 127 | 126 | breq1d 5153 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑔 = 𝑖 → ((𝑤 ∈ Word 𝐴 ↦ ((𝑔‘𝑤) · (𝑀 Σg 𝑤))) finSupp
(0g‘𝑅)
↔ (𝑤 ∈ Word 𝐴 ↦ ((𝑖‘𝑤) · (𝑀 Σg 𝑤))) finSupp
(0g‘𝑅))) |
| 128 | 127 | cbvralvw 3237 |
. . . . . . . . . . . . . . . . 17
⊢
(∀𝑔 ∈
𝐹 (𝑤 ∈ Word 𝐴 ↦ ((𝑔‘𝑤) · (𝑀 Σg 𝑤))) finSupp
(0g‘𝑅)
↔ ∀𝑖 ∈
𝐹 (𝑤 ∈ Word 𝐴 ↦ ((𝑖‘𝑤) · (𝑀 Σg 𝑤))) finSupp
(0g‘𝑅)) |
| 129 | 123, 128 | sylib 218 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → ∀𝑖 ∈ 𝐹 (𝑤 ∈ Word 𝐴 ↦ ((𝑖‘𝑤) · (𝑀 Σg 𝑤))) finSupp
(0g‘𝑅)) |
| 130 | 129 | r19.21bi 3251 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑖 ∈ 𝐹) → (𝑤 ∈ Word 𝐴 ↦ ((𝑖‘𝑤) · (𝑀 Σg 𝑤))) finSupp
(0g‘𝑅)) |
| 131 | 130 | adantlr 715 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) → (𝑤 ∈ Word 𝐴 ↦ ((𝑖‘𝑤) · (𝑀 Σg 𝑤))) finSupp
(0g‘𝑅)) |
| 132 | 4, 5, 104, 105, 106, 107, 119, 120, 121, 122, 131 | gsummptfsadd 19942 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ (((𝑔‘𝑤) · (𝑀 Σg 𝑤))(+g‘𝑅)((𝑖‘𝑤) · (𝑀 Σg 𝑤))))) = ((𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑔‘𝑤) · (𝑀 Σg 𝑤))))(+g‘𝑅)(𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑖‘𝑤) · (𝑀 Σg 𝑤)))))) |
| 133 | 25 | ffnd 6737 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑔 ∈ 𝐹) → 𝑔 Fn Word 𝐴) |
| 134 | 133 | adantr 480 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) → 𝑔 Fn Word 𝐴) |
| 135 | 115 | ffnd 6737 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑖 ∈ 𝐹) → 𝑖 Fn Word 𝐴) |
| 136 | 135 | adantlr 715 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) → 𝑖 Fn Word 𝐴) |
| 137 | | inidm 4227 |
. . . . . . . . . . . . . . . . . 18
⊢ (Word
𝐴 ∩ Word 𝐴) = Word 𝐴 |
| 138 | | eqidd 2738 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑤 ∈ Word 𝐴) → (𝑔‘𝑤) = (𝑔‘𝑤)) |
| 139 | | eqidd 2738 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑤 ∈ Word 𝐴) → (𝑖‘𝑤) = (𝑖‘𝑤)) |
| 140 | 134, 136,
106, 106, 137, 138, 139 | ofval 7708 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑤 ∈ Word 𝐴) → ((𝑔 ∘f + 𝑖)‘𝑤) = ((𝑔‘𝑤) + (𝑖‘𝑤))) |
| 141 | 140 | oveq1d 7446 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑤 ∈ Word 𝐴) → (((𝑔 ∘f + 𝑖)‘𝑤) · (𝑀 Σg 𝑤)) = (((𝑔‘𝑤) + (𝑖‘𝑤)) · (𝑀 Σg 𝑤))) |
| 142 | 16 | adantlr 715 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑤 ∈ Word 𝐴) → 𝑅 ∈ Grp) |
| 143 | 26 | adantlr 715 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑤 ∈ Word 𝐴) → (𝑔‘𝑤) ∈ ℤ) |
| 144 | 116 | adantllr 719 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑤 ∈ Word 𝐴) → (𝑖‘𝑤) ∈ ℤ) |
| 145 | 36 | adantlr 715 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑤 ∈ Word 𝐴) → (𝑀 Σg 𝑤) ∈ 𝐵) |
| 146 | 4, 15, 104 | mulgdir 19124 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑅 ∈ Grp ∧ ((𝑔‘𝑤) ∈ ℤ ∧ (𝑖‘𝑤) ∈ ℤ ∧ (𝑀 Σg 𝑤) ∈ 𝐵)) → (((𝑔‘𝑤) + (𝑖‘𝑤)) · (𝑀 Σg 𝑤)) = (((𝑔‘𝑤) · (𝑀 Σg 𝑤))(+g‘𝑅)((𝑖‘𝑤) · (𝑀 Σg 𝑤)))) |
| 147 | 142, 143,
144, 145, 146 | syl13anc 1374 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑤 ∈ Word 𝐴) → (((𝑔‘𝑤) + (𝑖‘𝑤)) · (𝑀 Σg 𝑤)) = (((𝑔‘𝑤) · (𝑀 Σg 𝑤))(+g‘𝑅)((𝑖‘𝑤) · (𝑀 Σg 𝑤)))) |
| 148 | 141, 147 | eqtr2d 2778 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑤 ∈ Word 𝐴) → (((𝑔‘𝑤) · (𝑀 Σg 𝑤))(+g‘𝑅)((𝑖‘𝑤) · (𝑀 Σg 𝑤))) = (((𝑔 ∘f + 𝑖)‘𝑤) · (𝑀 Σg 𝑤))) |
| 149 | 148 | mpteq2dva 5242 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) → (𝑤 ∈ Word 𝐴 ↦ (((𝑔‘𝑤) · (𝑀 Σg 𝑤))(+g‘𝑅)((𝑖‘𝑤) · (𝑀 Σg 𝑤)))) = (𝑤 ∈ Word 𝐴 ↦ (((𝑔 ∘f + 𝑖)‘𝑤) · (𝑀 Σg 𝑤)))) |
| 150 | 149 | oveq2d 7447 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ (((𝑔‘𝑤) · (𝑀 Σg 𝑤))(+g‘𝑅)((𝑖‘𝑤) · (𝑀 Σg 𝑤))))) = (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ (((𝑔 ∘f + 𝑖)‘𝑤) · (𝑀 Σg 𝑤))))) |
| 151 | 132, 150 | eqtr3d 2779 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) → ((𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑔‘𝑤) · (𝑀 Σg 𝑤))))(+g‘𝑅)(𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑖‘𝑤) · (𝑀 Σg 𝑤))))) = (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ (((𝑔 ∘f + 𝑖)‘𝑤) · (𝑀 Σg 𝑤))))) |
| 152 | | fveq1 6905 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑔 = ℎ → (𝑔‘𝑤) = (ℎ‘𝑤)) |
| 153 | 152 | oveq1d 7446 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑔 = ℎ → ((𝑔‘𝑤) · (𝑀 Σg 𝑤)) = ((ℎ‘𝑤) · (𝑀 Σg 𝑤))) |
| 154 | 153 | mpteq2dv 5244 |
. . . . . . . . . . . . . . . 16
⊢ (𝑔 = ℎ → (𝑤 ∈ Word 𝐴 ↦ ((𝑔‘𝑤) · (𝑀 Σg 𝑤))) = (𝑤 ∈ Word 𝐴 ↦ ((ℎ‘𝑤) · (𝑀 Σg 𝑤)))) |
| 155 | 154 | oveq2d 7447 |
. . . . . . . . . . . . . . 15
⊢ (𝑔 = ℎ → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑔‘𝑤) · (𝑀 Σg 𝑤)))) = (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((ℎ‘𝑤) · (𝑀 Σg 𝑤))))) |
| 156 | 155 | cbvmptv 5255 |
. . . . . . . . . . . . . 14
⊢ (𝑔 ∈ 𝐹 ↦ (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑔‘𝑤) · (𝑀 Σg 𝑤))))) = (ℎ ∈ 𝐹 ↦ (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((ℎ‘𝑤) · (𝑀 Σg 𝑤))))) |
| 157 | | fveq1 6905 |
. . . . . . . . . . . . . . . . . . 19
⊢ (ℎ = (𝑔 ∘f + 𝑖) → (ℎ‘𝑤) = ((𝑔 ∘f + 𝑖)‘𝑤)) |
| 158 | 157 | oveq1d 7446 |
. . . . . . . . . . . . . . . . . 18
⊢ (ℎ = (𝑔 ∘f + 𝑖) → ((ℎ‘𝑤) · (𝑀 Σg 𝑤)) = (((𝑔 ∘f + 𝑖)‘𝑤) · (𝑀 Σg 𝑤))) |
| 159 | 158 | mpteq2dv 5244 |
. . . . . . . . . . . . . . . . 17
⊢ (ℎ = (𝑔 ∘f + 𝑖) → (𝑤 ∈ Word 𝐴 ↦ ((ℎ‘𝑤) · (𝑀 Σg 𝑤))) = (𝑤 ∈ Word 𝐴 ↦ (((𝑔 ∘f + 𝑖)‘𝑤) · (𝑀 Σg 𝑤)))) |
| 160 | 159 | oveq2d 7447 |
. . . . . . . . . . . . . . . 16
⊢ (ℎ = (𝑔 ∘f + 𝑖) → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((ℎ‘𝑤) · (𝑀 Σg 𝑤)))) = (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ (((𝑔 ∘f + 𝑖)‘𝑤) · (𝑀 Σg 𝑤))))) |
| 161 | 160 | eqeq2d 2748 |
. . . . . . . . . . . . . . 15
⊢ (ℎ = (𝑔 ∘f + 𝑖) → ((𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ (((𝑔 ∘f + 𝑖)‘𝑤) · (𝑀 Σg 𝑤)))) = (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((ℎ‘𝑤) · (𝑀 Σg 𝑤)))) ↔ (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ (((𝑔 ∘f + 𝑖)‘𝑤) · (𝑀 Σg 𝑤)))) = (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ (((𝑔 ∘f + 𝑖)‘𝑤) · (𝑀 Σg 𝑤)))))) |
| 162 | | breq1 5146 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑓 = (𝑔 ∘f + 𝑖) → (𝑓 finSupp 0 ↔ (𝑔 ∘f + 𝑖) finSupp 0)) |
| 163 | 21 | a1i 11 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) → ℤ ∈ V) |
| 164 | | zaddcl 12657 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ) → (𝑥 + 𝑦) ∈ ℤ) |
| 165 | 164 | adantl 481 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ (𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ)) → (𝑥 + 𝑦) ∈ ℤ) |
| 166 | 25 | adantr 480 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) → 𝑔:Word 𝐴⟶ℤ) |
| 167 | 115 | adantlr 715 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) → 𝑖:Word 𝐴⟶ℤ) |
| 168 | 165, 166,
167, 106, 106, 137 | off 7715 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) → (𝑔 ∘f + 𝑖):Word 𝐴⟶ℤ) |
| 169 | 163, 106,
168 | elmapdd 8881 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) → (𝑔 ∘f + 𝑖) ∈ (ℤ ↑m Word
𝐴)) |
| 170 | | zringring 21460 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
ℤring ∈ Ring |
| 171 | | ringmnd 20240 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
(ℤring ∈ Ring → ℤring ∈
Mnd) |
| 172 | 170, 171 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . . 20
⊢
ℤring ∈ Mnd |
| 173 | 172 | a1i 11 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) → ℤring ∈
Mnd) |
| 174 | 20 | adantr 480 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) → 𝑔 ∈ (ℤ ↑m Word
𝐴)) |
| 175 | 111 | adantl 481 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) → 𝑖 ∈ (ℤ ↑m Word
𝐴)) |
| 176 | 45 | adantr 480 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) → 𝑔 finSupp 0) |
| 177 | | zring0 21469 |
. . . . . . . . . . . . . . . . . . . 20
⊢ 0 =
(0g‘ℤring) |
| 178 | 176, 177 | breqtrdi 5184 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) → 𝑔 finSupp
(0g‘ℤring)) |
| 179 | 110 | simprbi 496 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑖 ∈ 𝐹 → 𝑖 finSupp 0) |
| 180 | 179 | adantl 481 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) → 𝑖 finSupp 0) |
| 181 | 180, 177 | breqtrdi 5184 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) → 𝑖 finSupp
(0g‘ℤring)) |
| 182 | | zringbas 21464 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ℤ =
(Base‘ℤring) |
| 183 | 182 | mndpfsupp 18780 |
. . . . . . . . . . . . . . . . . . 19
⊢
(((ℤring ∈ Mnd ∧ Word 𝐴 ∈ V) ∧ (𝑔 ∈ (ℤ ↑m Word
𝐴) ∧ 𝑖 ∈ (ℤ ↑m Word
𝐴)) ∧ (𝑔 finSupp
(0g‘ℤring) ∧ 𝑖 finSupp
(0g‘ℤring))) → (𝑔 ∘f
(+g‘ℤring)𝑖) finSupp
(0g‘ℤring)) |
| 184 | 173, 106,
174, 175, 178, 181, 183 | syl222anc 1388 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) → (𝑔 ∘f
(+g‘ℤring)𝑖) finSupp
(0g‘ℤring)) |
| 185 | | zringplusg 21465 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ + =
(+g‘ℤring) |
| 186 | 185 | a1i 11 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) → + =
(+g‘ℤring)) |
| 187 | 186 | ofeqd 7699 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) → ∘f + =
∘f
(+g‘ℤring)) |
| 188 | 187 | oveqd 7448 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) → (𝑔 ∘f + 𝑖) = (𝑔 ∘f
(+g‘ℤring)𝑖)) |
| 189 | 177 | a1i 11 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) → 0 =
(0g‘ℤring)) |
| 190 | 184, 188,
189 | 3brtr4d 5175 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) → (𝑔 ∘f + 𝑖) finSupp 0) |
| 191 | 162, 169,
190 | elrabd 3694 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) → (𝑔 ∘f + 𝑖) ∈ {𝑓 ∈ (ℤ ↑m Word
𝐴) ∣ 𝑓 finSupp 0}) |
| 192 | 191, 17 | eleqtrrdi 2852 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) → (𝑔 ∘f + 𝑖) ∈ 𝐹) |
| 193 | | eqidd 2738 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ (((𝑔 ∘f + 𝑖)‘𝑤) · (𝑀 Σg 𝑤)))) = (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ (((𝑔 ∘f + 𝑖)‘𝑤) · (𝑀 Σg 𝑤))))) |
| 194 | 161, 192,
193 | rspcedvdw 3625 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) → ∃ℎ ∈ 𝐹 (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ (((𝑔 ∘f + 𝑖)‘𝑤) · (𝑀 Σg 𝑤)))) = (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((ℎ‘𝑤) · (𝑀 Σg 𝑤))))) |
| 195 | | ovexd 7466 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ (((𝑔 ∘f + 𝑖)‘𝑤) · (𝑀 Σg 𝑤)))) ∈ V) |
| 196 | 156, 194,
195 | elrnmptd 5974 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ (((𝑔 ∘f + 𝑖)‘𝑤) · (𝑀 Σg 𝑤)))) ∈ ran (𝑔 ∈ 𝐹 ↦ (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑔‘𝑤) · (𝑀 Σg 𝑤)))))) |
| 197 | 196, 52 | eleqtrrdi 2852 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ (((𝑔 ∘f + 𝑖)‘𝑤) · (𝑀 Σg 𝑤)))) ∈ 𝑆) |
| 198 | 151, 197 | eqeltrd 2841 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) → ((𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑔‘𝑤) · (𝑀 Σg 𝑤))))(+g‘𝑅)(𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑖‘𝑤) · (𝑀 Σg 𝑤))))) ∈ 𝑆) |
| 199 | 198 | adantllr 719 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑥 ∈ 𝑆) ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) → ((𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑔‘𝑤) · (𝑀 Σg 𝑤))))(+g‘𝑅)(𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑖‘𝑤) · (𝑀 Σg 𝑤))))) ∈ 𝑆) |
| 200 | 199 | adantllr 719 |
. . . . . . . . 9
⊢
(((((𝜑 ∧ 𝑥 ∈ 𝑆) ∧ 𝑦 ∈ 𝑆) ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) → ((𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑔‘𝑤) · (𝑀 Σg 𝑤))))(+g‘𝑅)(𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑖‘𝑤) · (𝑀 Σg 𝑤))))) ∈ 𝑆) |
| 201 | 200 | ad4ant13 751 |
. . . . . . . 8
⊢
(((((((𝜑 ∧ 𝑥 ∈ 𝑆) ∧ 𝑦 ∈ 𝑆) ∧ 𝑔 ∈ 𝐹) ∧ 𝑥 = (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑔‘𝑤) · (𝑀 Σg 𝑤))))) ∧ 𝑖 ∈ 𝐹) ∧ 𝑦 = (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑖‘𝑤) · (𝑀 Σg 𝑤))))) → ((𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑔‘𝑤) · (𝑀 Σg 𝑤))))(+g‘𝑅)(𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑖‘𝑤) · (𝑀 Σg 𝑤))))) ∈ 𝑆) |
| 202 | 103, 201 | eqeltrd 2841 |
. . . . . . 7
⊢
(((((((𝜑 ∧ 𝑥 ∈ 𝑆) ∧ 𝑦 ∈ 𝑆) ∧ 𝑔 ∈ 𝐹) ∧ 𝑥 = (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑔‘𝑤) · (𝑀 Σg 𝑤))))) ∧ 𝑖 ∈ 𝐹) ∧ 𝑦 = (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑖‘𝑤) · (𝑀 Σg 𝑤))))) → (𝑥(+g‘𝑅)𝑦) ∈ 𝑆) |
| 203 | 52 | eleq2i 2833 |
. . . . . . . . . 10
⊢ (𝑦 ∈ 𝑆 ↔ 𝑦 ∈ ran (𝑔 ∈ 𝐹 ↦ (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑔‘𝑤) · (𝑀 Σg 𝑤)))))) |
| 204 | 126 | oveq2d 7447 |
. . . . . . . . . . . . 13
⊢ (𝑔 = 𝑖 → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑔‘𝑤) · (𝑀 Σg 𝑤)))) = (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑖‘𝑤) · (𝑀 Σg 𝑤))))) |
| 205 | 204 | cbvmptv 5255 |
. . . . . . . . . . . 12
⊢ (𝑔 ∈ 𝐹 ↦ (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑔‘𝑤) · (𝑀 Σg 𝑤))))) = (𝑖 ∈ 𝐹 ↦ (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑖‘𝑤) · (𝑀 Σg 𝑤))))) |
| 206 | 205 | elrnmpt 5969 |
. . . . . . . . . . 11
⊢ (𝑦 ∈ V → (𝑦 ∈ ran (𝑔 ∈ 𝐹 ↦ (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑔‘𝑤) · (𝑀 Σg 𝑤))))) ↔ ∃𝑖 ∈ 𝐹 𝑦 = (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑖‘𝑤) · (𝑀 Σg 𝑤)))))) |
| 207 | 206 | elv 3485 |
. . . . . . . . . 10
⊢ (𝑦 ∈ ran (𝑔 ∈ 𝐹 ↦ (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑔‘𝑤) · (𝑀 Σg 𝑤))))) ↔ ∃𝑖 ∈ 𝐹 𝑦 = (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑖‘𝑤) · (𝑀 Σg 𝑤))))) |
| 208 | 203, 207 | sylbb 219 |
. . . . . . . . 9
⊢ (𝑦 ∈ 𝑆 → ∃𝑖 ∈ 𝐹 𝑦 = (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑖‘𝑤) · (𝑀 Σg 𝑤))))) |
| 209 | 208 | adantl 481 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑥 ∈ 𝑆) ∧ 𝑦 ∈ 𝑆) → ∃𝑖 ∈ 𝐹 𝑦 = (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑖‘𝑤) · (𝑀 Σg 𝑤))))) |
| 210 | 209 | ad2antrr 726 |
. . . . . . 7
⊢
(((((𝜑 ∧ 𝑥 ∈ 𝑆) ∧ 𝑦 ∈ 𝑆) ∧ 𝑔 ∈ 𝐹) ∧ 𝑥 = (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑔‘𝑤) · (𝑀 Σg 𝑤))))) → ∃𝑖 ∈ 𝐹 𝑦 = (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑖‘𝑤) · (𝑀 Σg 𝑤))))) |
| 211 | 202, 210 | r19.29a 3162 |
. . . . . 6
⊢
(((((𝜑 ∧ 𝑥 ∈ 𝑆) ∧ 𝑦 ∈ 𝑆) ∧ 𝑔 ∈ 𝐹) ∧ 𝑥 = (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑔‘𝑤) · (𝑀 Σg 𝑤))))) → (𝑥(+g‘𝑅)𝑦) ∈ 𝑆) |
| 212 | 58 | adantr 480 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑥 ∈ 𝑆) ∧ 𝑦 ∈ 𝑆) → ∃𝑔 ∈ 𝐹 𝑥 = (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑔‘𝑤) · (𝑀 Σg 𝑤))))) |
| 213 | 211, 212 | r19.29a 3162 |
. . . . 5
⊢ (((𝜑 ∧ 𝑥 ∈ 𝑆) ∧ 𝑦 ∈ 𝑆) → (𝑥(+g‘𝑅)𝑦) ∈ 𝑆) |
| 214 | 213 | ralrimiva 3146 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → ∀𝑦 ∈ 𝑆 (𝑥(+g‘𝑅)𝑦) ∈ 𝑆) |
| 215 | 2 | ad3antrrr 730 |
. . . . . . 7
⊢ ((((𝜑 ∧ 𝑥 ∈ 𝑆) ∧ 𝑔 ∈ 𝐹) ∧ 𝑥 = (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑔‘𝑤) · (𝑀 Σg 𝑤))))) → 𝑅 ∈ Grp) |
| 216 | 26 | znegcld 12724 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑤 ∈ Word 𝐴) → -(𝑔‘𝑤) ∈ ℤ) |
| 217 | 4, 15, 16, 216, 36 | mulgcld 19114 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑤 ∈ Word 𝐴) → (-(𝑔‘𝑤) · (𝑀 Σg 𝑤)) ∈ 𝐵) |
| 218 | 217 | fmpttd 7135 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑔 ∈ 𝐹) → (𝑤 ∈ Word 𝐴 ↦ (-(𝑔‘𝑤) · (𝑀 Σg 𝑤))):Word 𝐴⟶𝐵) |
| 219 | 25 | adantr 480 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑤 ∈ Word 𝐴) → 𝑔:Word 𝐴⟶ℤ) |
| 220 | | simpr 484 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑤 ∈ Word 𝐴) → 𝑤 ∈ Word 𝐴) |
| 221 | 219, 220 | fvco3d 7009 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑤 ∈ Word 𝐴) → (((𝑧 ∈ ℤ ↦ -𝑧) ∘ 𝑔)‘𝑤) = ((𝑧 ∈ ℤ ↦ -𝑧)‘(𝑔‘𝑤))) |
| 222 | | eqid 2737 |
. . . . . . . . . . . . . 14
⊢ (𝑧 ∈ ℤ ↦ -𝑧) = (𝑧 ∈ ℤ ↦ -𝑧) |
| 223 | | negeq 11500 |
. . . . . . . . . . . . . 14
⊢ (𝑧 = (𝑔‘𝑤) → -𝑧 = -(𝑔‘𝑤)) |
| 224 | 222, 223,
26, 216 | fvmptd3 7039 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑤 ∈ Word 𝐴) → ((𝑧 ∈ ℤ ↦ -𝑧)‘(𝑔‘𝑤)) = -(𝑔‘𝑤)) |
| 225 | 221, 224 | eqtrd 2777 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑤 ∈ Word 𝐴) → (((𝑧 ∈ ℤ ↦ -𝑧) ∘ 𝑔)‘𝑤) = -(𝑔‘𝑤)) |
| 226 | 225 | oveq1d 7446 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑤 ∈ Word 𝐴) → ((((𝑧 ∈ ℤ ↦ -𝑧) ∘ 𝑔)‘𝑤) · (𝑀 Σg 𝑤)) = (-(𝑔‘𝑤) · (𝑀 Σg 𝑤))) |
| 227 | 226 | mpteq2dva 5242 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑔 ∈ 𝐹) → (𝑤 ∈ Word 𝐴 ↦ ((((𝑧 ∈ ℤ ↦ -𝑧) ∘ 𝑔)‘𝑤) · (𝑀 Σg 𝑤))) = (𝑤 ∈ Word 𝐴 ↦ (-(𝑔‘𝑤) · (𝑀 Σg 𝑤)))) |
| 228 | | simpr 484 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑧 ∈ ℤ) → 𝑧 ∈ ℤ) |
| 229 | 228 | znegcld 12724 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑧 ∈ ℤ) → -𝑧 ∈ ℤ) |
| 230 | 229 | fmpttd 7135 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝑧 ∈ ℤ ↦ -𝑧):ℤ⟶ℤ) |
| 231 | 230 | adantr 480 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑔 ∈ 𝐹) → (𝑧 ∈ ℤ ↦ -𝑧):ℤ⟶ℤ) |
| 232 | 231, 25 | fcod 6761 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑔 ∈ 𝐹) → ((𝑧 ∈ ℤ ↦ -𝑧) ∘ 𝑔):Word 𝐴⟶ℤ) |
| 233 | 21 | a1i 11 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑔 ∈ 𝐹) → ℤ ∈ V) |
| 234 | | negeq 11500 |
. . . . . . . . . . . . . . 15
⊢ (𝑧 = 0 → -𝑧 = -0) |
| 235 | | neg0 11555 |
. . . . . . . . . . . . . . 15
⊢ -0 =
0 |
| 236 | 234, 235 | eqtrdi 2793 |
. . . . . . . . . . . . . 14
⊢ (𝑧 = 0 → -𝑧 = 0) |
| 237 | | 0zd 12625 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 0 ∈
ℤ) |
| 238 | 222, 236,
237, 237 | fvmptd3 7039 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ((𝑧 ∈ ℤ ↦ -𝑧)‘0) = 0) |
| 239 | 238 | adantr 480 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑔 ∈ 𝐹) → ((𝑧 ∈ ℤ ↦ -𝑧)‘0) = 0) |
| 240 | 40, 25, 231, 14, 233, 45, 239 | fsuppco2 9443 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑔 ∈ 𝐹) → ((𝑧 ∈ ℤ ↦ -𝑧) ∘ 𝑔) finSupp 0) |
| 241 | 39, 40, 14, 41, 36, 232, 240, 47 | fisuppov1 32692 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑔 ∈ 𝐹) → (𝑤 ∈ Word 𝐴 ↦ ((((𝑧 ∈ ℤ ↦ -𝑧) ∘ 𝑔)‘𝑤) · (𝑀 Σg 𝑤))) finSupp
(0g‘𝑅)) |
| 242 | 227, 241 | eqbrtrrd 5167 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑔 ∈ 𝐹) → (𝑤 ∈ Word 𝐴 ↦ (-(𝑔‘𝑤) · (𝑀 Σg 𝑤))) finSupp
(0g‘𝑅)) |
| 243 | 4, 5, 7, 14, 218, 242 | gsumcl 19933 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑔 ∈ 𝐹) → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ (-(𝑔‘𝑤) · (𝑀 Σg 𝑤)))) ∈ 𝐵) |
| 244 | 243 | ad4ant13 751 |
. . . . . . 7
⊢ ((((𝜑 ∧ 𝑥 ∈ 𝑆) ∧ 𝑔 ∈ 𝐹) ∧ 𝑥 = (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑔‘𝑤) · (𝑀 Σg 𝑤))))) → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ (-(𝑔‘𝑤) · (𝑀 Σg 𝑤)))) ∈ 𝐵) |
| 245 | 3 | oveq1d 7446 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 𝑥 ∈ 𝑆) ∧ 𝑔 ∈ 𝐹) ∧ 𝑥 = (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑔‘𝑤) · (𝑀 Σg 𝑤))))) → (𝑥(+g‘𝑅)(𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ (-(𝑔‘𝑤) · (𝑀 Σg 𝑤))))) = ((𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑔‘𝑤) · (𝑀 Σg 𝑤))))(+g‘𝑅)(𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ (-(𝑔‘𝑤) · (𝑀 Σg 𝑤)))))) |
| 246 | | eqidd 2738 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑔 ∈ 𝐹) → (𝑤 ∈ Word 𝐴 ↦ ((𝑔‘𝑤) · (𝑀 Σg 𝑤))) = (𝑤 ∈ Word 𝐴 ↦ ((𝑔‘𝑤) · (𝑀 Σg 𝑤)))) |
| 247 | | eqidd 2738 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑔 ∈ 𝐹) → (𝑤 ∈ Word 𝐴 ↦ (-(𝑔‘𝑤) · (𝑀 Σg 𝑤))) = (𝑤 ∈ Word 𝐴 ↦ (-(𝑔‘𝑤) · (𝑀 Σg 𝑤)))) |
| 248 | 4, 5, 104, 7, 14, 37, 217, 246, 247, 48, 242 | gsummptfsadd 19942 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑔 ∈ 𝐹) → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ (((𝑔‘𝑤) · (𝑀 Σg 𝑤))(+g‘𝑅)(-(𝑔‘𝑤) · (𝑀 Σg 𝑤))))) = ((𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑔‘𝑤) · (𝑀 Σg 𝑤))))(+g‘𝑅)(𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ (-(𝑔‘𝑤) · (𝑀 Σg 𝑤)))))) |
| 249 | 248 | ad4ant13 751 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 𝑥 ∈ 𝑆) ∧ 𝑔 ∈ 𝐹) ∧ 𝑥 = (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑔‘𝑤) · (𝑀 Σg 𝑤))))) → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ (((𝑔‘𝑤) · (𝑀 Σg 𝑤))(+g‘𝑅)(-(𝑔‘𝑤) · (𝑀 Σg 𝑤))))) = ((𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑔‘𝑤) · (𝑀 Σg 𝑤))))(+g‘𝑅)(𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ (-(𝑔‘𝑤) · (𝑀 Σg 𝑤)))))) |
| 250 | 26 | zcnd 12723 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑤 ∈ Word 𝐴) → (𝑔‘𝑤) ∈ ℂ) |
| 251 | 250 | negidd 11610 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑤 ∈ Word 𝐴) → ((𝑔‘𝑤) + -(𝑔‘𝑤)) = 0) |
| 252 | 251 | oveq1d 7446 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑤 ∈ Word 𝐴) → (((𝑔‘𝑤) + -(𝑔‘𝑤)) · (𝑀 Σg 𝑤)) = (0 · (𝑀 Σg 𝑤))) |
| 253 | 4, 15, 104 | mulgdir 19124 |
. . . . . . . . . . . . . 14
⊢ ((𝑅 ∈ Grp ∧ ((𝑔‘𝑤) ∈ ℤ ∧ -(𝑔‘𝑤) ∈ ℤ ∧ (𝑀 Σg 𝑤) ∈ 𝐵)) → (((𝑔‘𝑤) + -(𝑔‘𝑤)) · (𝑀 Σg 𝑤)) = (((𝑔‘𝑤) · (𝑀 Σg 𝑤))(+g‘𝑅)(-(𝑔‘𝑤) · (𝑀 Σg 𝑤)))) |
| 254 | 16, 26, 216, 36, 253 | syl13anc 1374 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑤 ∈ Word 𝐴) → (((𝑔‘𝑤) + -(𝑔‘𝑤)) · (𝑀 Σg 𝑤)) = (((𝑔‘𝑤) · (𝑀 Σg 𝑤))(+g‘𝑅)(-(𝑔‘𝑤) · (𝑀 Σg 𝑤)))) |
| 255 | 36, 84 | syl 17 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑤 ∈ Word 𝐴) → (0 · (𝑀 Σg 𝑤)) = (0g‘𝑅)) |
| 256 | 252, 254,
255 | 3eqtr3d 2785 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑤 ∈ Word 𝐴) → (((𝑔‘𝑤) · (𝑀 Σg 𝑤))(+g‘𝑅)(-(𝑔‘𝑤) · (𝑀 Σg 𝑤))) = (0g‘𝑅)) |
| 257 | 256 | mpteq2dva 5242 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑔 ∈ 𝐹) → (𝑤 ∈ Word 𝐴 ↦ (((𝑔‘𝑤) · (𝑀 Σg 𝑤))(+g‘𝑅)(-(𝑔‘𝑤) · (𝑀 Σg 𝑤)))) = (𝑤 ∈ Word 𝐴 ↦ (0g‘𝑅))) |
| 258 | 257 | oveq2d 7447 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑔 ∈ 𝐹) → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ (((𝑔‘𝑤) · (𝑀 Σg 𝑤))(+g‘𝑅)(-(𝑔‘𝑤) · (𝑀 Σg 𝑤))))) = (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ (0g‘𝑅)))) |
| 259 | 91 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑔 ∈ 𝐹) → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ (0g‘𝑅))) = (0g‘𝑅)) |
| 260 | 258, 259 | eqtrd 2777 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑔 ∈ 𝐹) → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ (((𝑔‘𝑤) · (𝑀 Σg 𝑤))(+g‘𝑅)(-(𝑔‘𝑤) · (𝑀 Σg 𝑤))))) =
(0g‘𝑅)) |
| 261 | 260 | ad4ant13 751 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 𝑥 ∈ 𝑆) ∧ 𝑔 ∈ 𝐹) ∧ 𝑥 = (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑔‘𝑤) · (𝑀 Σg 𝑤))))) → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ (((𝑔‘𝑤) · (𝑀 Σg 𝑤))(+g‘𝑅)(-(𝑔‘𝑤) · (𝑀 Σg 𝑤))))) =
(0g‘𝑅)) |
| 262 | 245, 249,
261 | 3eqtr2d 2783 |
. . . . . . 7
⊢ ((((𝜑 ∧ 𝑥 ∈ 𝑆) ∧ 𝑔 ∈ 𝐹) ∧ 𝑥 = (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑔‘𝑤) · (𝑀 Σg 𝑤))))) → (𝑥(+g‘𝑅)(𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ (-(𝑔‘𝑤) · (𝑀 Σg 𝑤))))) =
(0g‘𝑅)) |
| 263 | | eqid 2737 |
. . . . . . . . 9
⊢
(invg‘𝑅) = (invg‘𝑅) |
| 264 | 4, 104, 5, 263 | grpinvid1 19009 |
. . . . . . . 8
⊢ ((𝑅 ∈ Grp ∧ 𝑥 ∈ 𝐵 ∧ (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ (-(𝑔‘𝑤) · (𝑀 Σg 𝑤)))) ∈ 𝐵) → (((invg‘𝑅)‘𝑥) = (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ (-(𝑔‘𝑤) · (𝑀 Σg 𝑤)))) ↔ (𝑥(+g‘𝑅)(𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ (-(𝑔‘𝑤) · (𝑀 Σg 𝑤))))) =
(0g‘𝑅))) |
| 265 | 264 | biimpar 477 |
. . . . . . 7
⊢ (((𝑅 ∈ Grp ∧ 𝑥 ∈ 𝐵 ∧ (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ (-(𝑔‘𝑤) · (𝑀 Σg 𝑤)))) ∈ 𝐵) ∧ (𝑥(+g‘𝑅)(𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ (-(𝑔‘𝑤) · (𝑀 Σg 𝑤))))) =
(0g‘𝑅))
→ ((invg‘𝑅)‘𝑥) = (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ (-(𝑔‘𝑤) · (𝑀 Σg 𝑤))))) |
| 266 | 215, 51, 244, 262, 265 | syl31anc 1375 |
. . . . . 6
⊢ ((((𝜑 ∧ 𝑥 ∈ 𝑆) ∧ 𝑔 ∈ 𝐹) ∧ 𝑥 = (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑔‘𝑤) · (𝑀 Σg 𝑤))))) →
((invg‘𝑅)‘𝑥) = (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ (-(𝑔‘𝑤) · (𝑀 Σg 𝑤))))) |
| 267 | | fveq1 6905 |
. . . . . . . . . . . . . 14
⊢ (ℎ = (𝑣 ∈ Word 𝐴 ↦ -(𝑔‘𝑣)) → (ℎ‘𝑤) = ((𝑣 ∈ Word 𝐴 ↦ -(𝑔‘𝑣))‘𝑤)) |
| 268 | 267 | oveq1d 7446 |
. . . . . . . . . . . . 13
⊢ (ℎ = (𝑣 ∈ Word 𝐴 ↦ -(𝑔‘𝑣)) → ((ℎ‘𝑤) · (𝑀 Σg 𝑤)) = (((𝑣 ∈ Word 𝐴 ↦ -(𝑔‘𝑣))‘𝑤) · (𝑀 Σg 𝑤))) |
| 269 | 268 | mpteq2dv 5244 |
. . . . . . . . . . . 12
⊢ (ℎ = (𝑣 ∈ Word 𝐴 ↦ -(𝑔‘𝑣)) → (𝑤 ∈ Word 𝐴 ↦ ((ℎ‘𝑤) · (𝑀 Σg 𝑤))) = (𝑤 ∈ Word 𝐴 ↦ (((𝑣 ∈ Word 𝐴 ↦ -(𝑔‘𝑣))‘𝑤) · (𝑀 Σg 𝑤)))) |
| 270 | 269 | oveq2d 7447 |
. . . . . . . . . . 11
⊢ (ℎ = (𝑣 ∈ Word 𝐴 ↦ -(𝑔‘𝑣)) → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((ℎ‘𝑤) · (𝑀 Σg 𝑤)))) = (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ (((𝑣 ∈ Word 𝐴 ↦ -(𝑔‘𝑣))‘𝑤) · (𝑀 Σg 𝑤))))) |
| 271 | 270 | eqeq2d 2748 |
. . . . . . . . . 10
⊢ (ℎ = (𝑣 ∈ Word 𝐴 ↦ -(𝑔‘𝑣)) → ((𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ (-(𝑔‘𝑤) · (𝑀 Σg 𝑤)))) = (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((ℎ‘𝑤) · (𝑀 Σg 𝑤)))) ↔ (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ (-(𝑔‘𝑤) · (𝑀 Σg 𝑤)))) = (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ (((𝑣 ∈ Word 𝐴 ↦ -(𝑔‘𝑣))‘𝑤) · (𝑀 Σg 𝑤)))))) |
| 272 | | breq1 5146 |
. . . . . . . . . . . 12
⊢ (𝑓 = (𝑣 ∈ Word 𝐴 ↦ -(𝑔‘𝑣)) → (𝑓 finSupp 0 ↔ (𝑣 ∈ Word 𝐴 ↦ -(𝑔‘𝑣)) finSupp 0)) |
| 273 | 25 | ffvelcdmda 7104 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑣 ∈ Word 𝐴) → (𝑔‘𝑣) ∈ ℤ) |
| 274 | 273 | znegcld 12724 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑣 ∈ Word 𝐴) → -(𝑔‘𝑣) ∈ ℤ) |
| 275 | 274 | fmpttd 7135 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑔 ∈ 𝐹) → (𝑣 ∈ Word 𝐴 ↦ -(𝑔‘𝑣)):Word 𝐴⟶ℤ) |
| 276 | 233, 14, 275 | elmapdd 8881 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑔 ∈ 𝐹) → (𝑣 ∈ Word 𝐴 ↦ -(𝑔‘𝑣)) ∈ (ℤ ↑m Word
𝐴)) |
| 277 | 275 | ffund 6740 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑔 ∈ 𝐹) → Fun (𝑣 ∈ Word 𝐴 ↦ -(𝑔‘𝑣))) |
| 278 | 133 | adantr 480 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑣 ∈ (Word 𝐴 ∖ (𝑔 supp 0))) → 𝑔 Fn Word 𝐴) |
| 279 | 14 | adantr 480 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑣 ∈ (Word 𝐴 ∖ (𝑔 supp 0))) → Word 𝐴 ∈ V) |
| 280 | | 0zd 12625 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑣 ∈ (Word 𝐴 ∖ (𝑔 supp 0))) → 0 ∈
ℤ) |
| 281 | | simpr 484 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑣 ∈ (Word 𝐴 ∖ (𝑔 supp 0))) → 𝑣 ∈ (Word 𝐴 ∖ (𝑔 supp 0))) |
| 282 | 278, 279,
280, 281 | fvdifsupp 8196 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑣 ∈ (Word 𝐴 ∖ (𝑔 supp 0))) → (𝑔‘𝑣) = 0) |
| 283 | 282 | negeqd 11502 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑣 ∈ (Word 𝐴 ∖ (𝑔 supp 0))) → -(𝑔‘𝑣) = -0) |
| 284 | 283, 235 | eqtrdi 2793 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑣 ∈ (Word 𝐴 ∖ (𝑔 supp 0))) → -(𝑔‘𝑣) = 0) |
| 285 | 284, 14 | suppss2 8225 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑔 ∈ 𝐹) → ((𝑣 ∈ Word 𝐴 ↦ -(𝑔‘𝑣)) supp 0) ⊆ (𝑔 supp 0)) |
| 286 | 276, 40, 277, 45, 285 | fsuppsssuppgd 9422 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑔 ∈ 𝐹) → (𝑣 ∈ Word 𝐴 ↦ -(𝑔‘𝑣)) finSupp 0) |
| 287 | 272, 276,
286 | elrabd 3694 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑔 ∈ 𝐹) → (𝑣 ∈ Word 𝐴 ↦ -(𝑔‘𝑣)) ∈ {𝑓 ∈ (ℤ ↑m Word
𝐴) ∣ 𝑓 finSupp 0}) |
| 288 | 287, 17 | eleqtrrdi 2852 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑔 ∈ 𝐹) → (𝑣 ∈ Word 𝐴 ↦ -(𝑔‘𝑣)) ∈ 𝐹) |
| 289 | | eqid 2737 |
. . . . . . . . . . . . . . 15
⊢ (𝑣 ∈ Word 𝐴 ↦ -(𝑔‘𝑣)) = (𝑣 ∈ Word 𝐴 ↦ -(𝑔‘𝑣)) |
| 290 | | fveq2 6906 |
. . . . . . . . . . . . . . . 16
⊢ (𝑣 = 𝑤 → (𝑔‘𝑣) = (𝑔‘𝑤)) |
| 291 | 290 | negeqd 11502 |
. . . . . . . . . . . . . . 15
⊢ (𝑣 = 𝑤 → -(𝑔‘𝑣) = -(𝑔‘𝑤)) |
| 292 | 289, 291,
220, 216 | fvmptd3 7039 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑤 ∈ Word 𝐴) → ((𝑣 ∈ Word 𝐴 ↦ -(𝑔‘𝑣))‘𝑤) = -(𝑔‘𝑤)) |
| 293 | 292 | eqcomd 2743 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑤 ∈ Word 𝐴) → -(𝑔‘𝑤) = ((𝑣 ∈ Word 𝐴 ↦ -(𝑔‘𝑣))‘𝑤)) |
| 294 | 293 | oveq1d 7446 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑤 ∈ Word 𝐴) → (-(𝑔‘𝑤) · (𝑀 Σg 𝑤)) = (((𝑣 ∈ Word 𝐴 ↦ -(𝑔‘𝑣))‘𝑤) · (𝑀 Σg 𝑤))) |
| 295 | 294 | mpteq2dva 5242 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑔 ∈ 𝐹) → (𝑤 ∈ Word 𝐴 ↦ (-(𝑔‘𝑤) · (𝑀 Σg 𝑤))) = (𝑤 ∈ Word 𝐴 ↦ (((𝑣 ∈ Word 𝐴 ↦ -(𝑔‘𝑣))‘𝑤) · (𝑀 Σg 𝑤)))) |
| 296 | 295 | oveq2d 7447 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑔 ∈ 𝐹) → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ (-(𝑔‘𝑤) · (𝑀 Σg 𝑤)))) = (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ (((𝑣 ∈ Word 𝐴 ↦ -(𝑔‘𝑣))‘𝑤) · (𝑀 Σg 𝑤))))) |
| 297 | 271, 288,
296 | rspcedvdw 3625 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑔 ∈ 𝐹) → ∃ℎ ∈ 𝐹 (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ (-(𝑔‘𝑤) · (𝑀 Σg 𝑤)))) = (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((ℎ‘𝑤) · (𝑀 Σg 𝑤))))) |
| 298 | 156, 297,
243 | elrnmptd 5974 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑔 ∈ 𝐹) → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ (-(𝑔‘𝑤) · (𝑀 Σg 𝑤)))) ∈ ran (𝑔 ∈ 𝐹 ↦ (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑔‘𝑤) · (𝑀 Σg 𝑤)))))) |
| 299 | 298, 52 | eleqtrrdi 2852 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑔 ∈ 𝐹) → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ (-(𝑔‘𝑤) · (𝑀 Σg 𝑤)))) ∈ 𝑆) |
| 300 | 299 | ad4ant13 751 |
. . . . . 6
⊢ ((((𝜑 ∧ 𝑥 ∈ 𝑆) ∧ 𝑔 ∈ 𝐹) ∧ 𝑥 = (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑔‘𝑤) · (𝑀 Σg 𝑤))))) → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ (-(𝑔‘𝑤) · (𝑀 Σg 𝑤)))) ∈ 𝑆) |
| 301 | 266, 300 | eqeltrd 2841 |
. . . . 5
⊢ ((((𝜑 ∧ 𝑥 ∈ 𝑆) ∧ 𝑔 ∈ 𝐹) ∧ 𝑥 = (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑔‘𝑤) · (𝑀 Σg 𝑤))))) →
((invg‘𝑅)‘𝑥) ∈ 𝑆) |
| 302 | 301, 58 | r19.29a 3162 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → ((invg‘𝑅)‘𝑥) ∈ 𝑆) |
| 303 | 214, 302 | jca 511 |
. . 3
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → (∀𝑦 ∈ 𝑆 (𝑥(+g‘𝑅)𝑦) ∈ 𝑆 ∧ ((invg‘𝑅)‘𝑥) ∈ 𝑆)) |
| 304 | 303 | ralrimiva 3146 |
. 2
⊢ (𝜑 → ∀𝑥 ∈ 𝑆 (∀𝑦 ∈ 𝑆 (𝑥(+g‘𝑅)𝑦) ∈ 𝑆 ∧ ((invg‘𝑅)‘𝑥) ∈ 𝑆)) |
| 305 | 4, 104, 263 | issubg2 19159 |
. . 3
⊢ (𝑅 ∈ Grp → (𝑆 ∈ (SubGrp‘𝑅) ↔ (𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅ ∧ ∀𝑥 ∈ 𝑆 (∀𝑦 ∈ 𝑆 (𝑥(+g‘𝑅)𝑦) ∈ 𝑆 ∧ ((invg‘𝑅)‘𝑥) ∈ 𝑆)))) |
| 306 | 305 | biimpar 477 |
. 2
⊢ ((𝑅 ∈ Grp ∧ (𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅ ∧ ∀𝑥 ∈ 𝑆 (∀𝑦 ∈ 𝑆 (𝑥(+g‘𝑅)𝑦) ∈ 𝑆 ∧ ((invg‘𝑅)‘𝑥) ∈ 𝑆))) → 𝑆 ∈ (SubGrp‘𝑅)) |
| 307 | 2, 63, 100, 304, 306 | syl13anc 1374 |
1
⊢ (𝜑 → 𝑆 ∈ (SubGrp‘𝑅)) |