Step | Hyp | Ref
| Expression |
1 | | elrgspn.r |
. . 3
⊢ (𝜑 → 𝑅 ∈ Ring) |
2 | 1 | ringgrpd 20259 |
. 2
⊢ (𝜑 → 𝑅 ∈ Grp) |
3 | | simpr 484 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 𝑥 ∈ 𝑆) ∧ 𝑔 ∈ 𝐹) ∧ 𝑥 = (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑔‘𝑤) · (𝑀 Σg 𝑤))))) → 𝑥 = (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑔‘𝑤) · (𝑀 Σg 𝑤))))) |
4 | | elrgspn.b |
. . . . . . . . . 10
⊢ 𝐵 = (Base‘𝑅) |
5 | | eqid 2734 |
. . . . . . . . . 10
⊢
(0g‘𝑅) = (0g‘𝑅) |
6 | 1 | ringcmnd 20297 |
. . . . . . . . . . 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 5329 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝐴 ∈ V) |
12 | | wrdexg 14558 |
. . . . . . . . . . . 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 4091 |
. . . . . . . . . . . . . . . 16
⊢ 𝐹 ⊆ (ℤ
↑m Word 𝐴) |
19 | 18 | a1i 11 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → 𝐹 ⊆ (ℤ ↑m Word
𝐴)) |
20 | 19 | sselda 3994 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑔 ∈ 𝐹) → 𝑔 ∈ (ℤ ↑m Word
𝐴)) |
21 | | zex 12619 |
. . . . . . . . . . . . . . . . 17
⊢ ℤ
∈ V |
22 | 21 | a1i 11 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → ℤ ∈
V) |
23 | 22, 13 | elmapd 8878 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (𝑔 ∈ (ℤ ↑m Word
𝐴) ↔ 𝑔:Word 𝐴⟶ℤ)) |
24 | 23 | adantr 480 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑔 ∈ 𝐹) → (𝑔 ∈ (ℤ ↑m Word
𝐴) ↔ 𝑔:Word 𝐴⟶ℤ)) |
25 | 20, 24 | mpbid 232 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑔 ∈ 𝐹) → 𝑔:Word 𝐴⟶ℤ) |
26 | 25 | ffvelcdmda 7103 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑤 ∈ Word 𝐴) → (𝑔‘𝑤) ∈ ℤ) |
27 | | elrgspn.m |
. . . . . . . . . . . . . . . 16
⊢ 𝑀 = (mulGrp‘𝑅) |
28 | 27 | ringmgp 20256 |
. . . . . . . . . . . . . . 15
⊢ (𝑅 ∈ Ring → 𝑀 ∈ Mnd) |
29 | 1, 28 | syl 17 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 𝑀 ∈ Mnd) |
30 | | sswrd 14556 |
. . . . . . . . . . . . . . . 16
⊢ (𝐴 ⊆ 𝐵 → Word 𝐴 ⊆ Word 𝐵) |
31 | 10, 30 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → Word 𝐴 ⊆ Word 𝐵) |
32 | 31 | sselda 3994 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑤 ∈ Word 𝐴) → 𝑤 ∈ Word 𝐵) |
33 | 27, 4 | mgpbas 20157 |
. . . . . . . . . . . . . . 15
⊢ 𝐵 = (Base‘𝑀) |
34 | 33 | gsumwcl 18864 |
. . . . . . . . . . . . . 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 19126 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑤 ∈ Word 𝐴) → ((𝑔‘𝑤) · (𝑀 Σg 𝑤)) ∈ 𝐵) |
38 | 37 | fmpttd 7134 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑔 ∈ 𝐹) → (𝑤 ∈ Word 𝐴 ↦ ((𝑔‘𝑤) · (𝑀 Σg 𝑤))):Word 𝐴⟶𝐵) |
39 | | fvexd 6921 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑔 ∈ 𝐹) → (0g‘𝑅) ∈ V) |
40 | | 0zd 12622 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑔 ∈ 𝐹) → 0 ∈ ℤ) |
41 | | ssidd 4018 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑔 ∈ 𝐹) → Word 𝐴 ⊆ Word 𝐴) |
42 | | breq1 5150 |
. . . . . . . . . . . . . 14
⊢ (𝑓 = 𝑔 → (𝑓 finSupp 0 ↔ 𝑔 finSupp 0)) |
43 | 42, 17 | elrab2 3697 |
. . . . . . . . . . . . 13
⊢ (𝑔 ∈ 𝐹 ↔ (𝑔 ∈ (ℤ ↑m Word
𝐴) ∧ 𝑔 finSupp 0)) |
44 | 43 | simprbi 496 |
. . . . . . . . . . . 12
⊢ (𝑔 ∈ 𝐹 → 𝑔 finSupp 0) |
45 | 44 | adantl 481 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑔 ∈ 𝐹) → 𝑔 finSupp 0) |
46 | 4, 5, 15 | mulg0 19104 |
. . . . . . . . . . . 12
⊢ (𝑦 ∈ 𝐵 → (0 · 𝑦) = (0g‘𝑅)) |
47 | 46 | adantl 481 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑦 ∈ 𝐵) → (0 · 𝑦) = (0g‘𝑅)) |
48 | 39, 40, 14, 41, 36, 25, 45, 47 | fisuppov1 32697 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑔 ∈ 𝐹) → (𝑤 ∈ Word 𝐴 ↦ ((𝑔‘𝑤) · (𝑀 Σg 𝑤))) finSupp
(0g‘𝑅)) |
49 | 4, 5, 7, 14, 38, 48 | gsumcl 19947 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑔 ∈ 𝐹) → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑔‘𝑤) · (𝑀 Σg 𝑤)))) ∈ 𝐵) |
50 | 49 | ad4ant13 751 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 𝑥 ∈ 𝑆) ∧ 𝑔 ∈ 𝐹) ∧ 𝑥 = (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑔‘𝑤) · (𝑀 Σg 𝑤))))) → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑔‘𝑤) · (𝑀 Σg 𝑤)))) ∈ 𝐵) |
51 | 3, 50 | eqeltrd 2838 |
. . . . . . 7
⊢ ((((𝜑 ∧ 𝑥 ∈ 𝑆) ∧ 𝑔 ∈ 𝐹) ∧ 𝑥 = (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑔‘𝑤) · (𝑀 Σg 𝑤))))) → 𝑥 ∈ 𝐵) |
52 | | elrgspnlem1.1 |
. . . . . . . . . 10
⊢ 𝑆 = ran (𝑔 ∈ 𝐹 ↦ (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑔‘𝑤) · (𝑀 Σg 𝑤))))) |
53 | 52 | eleq2i 2830 |
. . . . . . . . 9
⊢ (𝑥 ∈ 𝑆 ↔ 𝑥 ∈ ran (𝑔 ∈ 𝐹 ↦ (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑔‘𝑤) · (𝑀 Σg 𝑤)))))) |
54 | | eqid 2734 |
. . . . . . . . . . 11
⊢ (𝑔 ∈ 𝐹 ↦ (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑔‘𝑤) · (𝑀 Σg 𝑤))))) = (𝑔 ∈ 𝐹 ↦ (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑔‘𝑤) · (𝑀 Σg 𝑤))))) |
55 | 54 | elrnmpt 5971 |
. . . . . . . . . 10
⊢ (𝑥 ∈ V → (𝑥 ∈ ran (𝑔 ∈ 𝐹 ↦ (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑔‘𝑤) · (𝑀 Σg 𝑤))))) ↔ ∃𝑔 ∈ 𝐹 𝑥 = (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑔‘𝑤) · (𝑀 Σg 𝑤)))))) |
56 | 55 | elv 3482 |
. . . . . . . . 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 3159 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → 𝑥 ∈ 𝐵) |
60 | 59, 4 | eleqtrdi 2848 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → 𝑥 ∈ (Base‘𝑅)) |
61 | 60 | ex 412 |
. . . 4
⊢ (𝜑 → (𝑥 ∈ 𝑆 → 𝑥 ∈ (Base‘𝑅))) |
62 | 61 | ssrdv 4000 |
. . 3
⊢ (𝜑 → 𝑆 ⊆ (Base‘𝑅)) |
63 | 62, 4 | sseqtrrdi 4046 |
. 2
⊢ (𝜑 → 𝑆 ⊆ 𝐵) |
64 | | breq1 5150 |
. . . . . . . 8
⊢ (𝑓 = (Word 𝐴 × {0}) → (𝑓 finSupp 0 ↔ (Word 𝐴 × {0}) finSupp 0)) |
65 | | 0z 12621 |
. . . . . . . . . . 11
⊢ 0 ∈
ℤ |
66 | 65 | fconst6 6798 |
. . . . . . . . . 10
⊢ (Word
𝐴 × {0}):Word 𝐴⟶ℤ |
67 | 66 | a1i 11 |
. . . . . . . . 9
⊢ (𝜑 → (Word 𝐴 × {0}):Word 𝐴⟶ℤ) |
68 | 22, 13, 67 | elmapdd 8879 |
. . . . . . . 8
⊢ (𝜑 → (Word 𝐴 × {0}) ∈ (ℤ
↑m Word 𝐴)) |
69 | | c0ex 11252 |
. . . . . . . . . 10
⊢ 0 ∈
V |
70 | 69 | a1i 11 |
. . . . . . . . 9
⊢ (𝜑 → 0 ∈
V) |
71 | 13, 70 | fczfsuppd 9423 |
. . . . . . . 8
⊢ (𝜑 → (Word 𝐴 × {0}) finSupp 0) |
72 | 64, 68, 71 | elrabd 3696 |
. . . . . . 7
⊢ (𝜑 → (Word 𝐴 × {0}) ∈ {𝑓 ∈ (ℤ ↑m Word
𝐴) ∣ 𝑓 finSupp 0}) |
73 | 72, 17 | eleqtrrdi 2849 |
. . . . . 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 7183 |
. . . . . . . . . . . . . 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 2774 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑔 = (Word 𝐴 × {0})) ∧ 𝑤 ∈ Word 𝐴) → (𝑔‘𝑤) = 0) |
82 | 81 | oveq1d 7445 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑔 = (Word 𝐴 × {0})) ∧ 𝑤 ∈ Word 𝐴) → ((𝑔‘𝑤) · (𝑀 Σg 𝑤)) = (0 · (𝑀 Σg 𝑤))) |
83 | 35 | adantlr 715 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑔 = (Word 𝐴 × {0})) ∧ 𝑤 ∈ Word 𝐴) → (𝑀 Σg 𝑤) ∈ 𝐵) |
84 | 4, 5, 15 | mulg0 19104 |
. . . . . . . . . . . 12
⊢ ((𝑀 Σg
𝑤) ∈ 𝐵 → (0 · (𝑀 Σg 𝑤)) = (0g‘𝑅)) |
85 | 83, 84 | syl 17 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑔 = (Word 𝐴 × {0})) ∧ 𝑤 ∈ Word 𝐴) → (0 · (𝑀 Σg 𝑤)) = (0g‘𝑅)) |
86 | 82, 85 | eqtrd 2774 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑔 = (Word 𝐴 × {0})) ∧ 𝑤 ∈ Word 𝐴) → ((𝑔‘𝑤) · (𝑀 Σg 𝑤)) = (0g‘𝑅)) |
87 | 86 | mpteq2dva 5247 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑔 = (Word 𝐴 × {0})) → (𝑤 ∈ Word 𝐴 ↦ ((𝑔‘𝑤) · (𝑀 Σg 𝑤))) = (𝑤 ∈ Word 𝐴 ↦ (0g‘𝑅))) |
88 | 87 | oveq2d 7446 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑔 = (Word 𝐴 × {0})) → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑔‘𝑤) · (𝑀 Σg 𝑤)))) = (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ (0g‘𝑅)))) |
89 | 6 | cmnmndd 19836 |
. . . . . . . . . 10
⊢ (𝜑 → 𝑅 ∈ Mnd) |
90 | 5 | gsumz 18861 |
. . . . . . . . . 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 2774 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑔 = (Word 𝐴 × {0})) → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑔‘𝑤) · (𝑀 Σg 𝑤)))) =
(0g‘𝑅)) |
94 | 93 | eqeq2d 2745 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑔 = (Word 𝐴 × {0})) →
((0g‘𝑅) =
(𝑅
Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑔‘𝑤) · (𝑀 Σg 𝑤)))) ↔
(0g‘𝑅) =
(0g‘𝑅))) |
95 | | eqidd 2735 |
. . . . . 6
⊢ (𝜑 → (0g‘𝑅) = (0g‘𝑅)) |
96 | 73, 94, 95 | rspcedvd 3623 |
. . . . 5
⊢ (𝜑 → ∃𝑔 ∈ 𝐹 (0g‘𝑅) = (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑔‘𝑤) · (𝑀 Σg 𝑤))))) |
97 | | fvexd 6921 |
. . . . 5
⊢ (𝜑 → (0g‘𝑅) ∈ V) |
98 | 54, 96, 97 | elrnmptd 5976 |
. . . 4
⊢ (𝜑 → (0g‘𝑅) ∈ ran (𝑔 ∈ 𝐹 ↦ (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑔‘𝑤) · (𝑀 Σg 𝑤)))))) |
99 | 98, 52 | eleqtrrdi 2849 |
. . 3
⊢ (𝜑 → (0g‘𝑅) ∈ 𝑆) |
100 | 99 | ne0d 4347 |
. 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 7448 |
. . . . . . . 8
⊢
(((((((𝜑 ∧ 𝑥 ∈ 𝑆) ∧ 𝑦 ∈ 𝑆) ∧ 𝑔 ∈ 𝐹) ∧ 𝑥 = (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑔‘𝑤) · (𝑀 Σg 𝑤))))) ∧ 𝑖 ∈ 𝐹) ∧ 𝑦 = (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑖‘𝑤) · (𝑀 Σg 𝑤))))) → (𝑥(+g‘𝑅)𝑦) = ((𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑔‘𝑤) · (𝑀 Σg 𝑤))))(+g‘𝑅)(𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑖‘𝑤) · (𝑀 Σg 𝑤)))))) |
104 | | eqid 2734 |
. . . . . . . . . . . . . 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 5150 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑓 = 𝑖 → (𝑓 finSupp 0 ↔ 𝑖 finSupp 0)) |
110 | 109, 17 | elrab2 3697 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑖 ∈ 𝐹 ↔ (𝑖 ∈ (ℤ ↑m Word
𝐴) ∧ 𝑖 finSupp 0)) |
111 | 110 | simplbi 497 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑖 ∈ 𝐹 → 𝑖 ∈ (ℤ ↑m Word
𝐴)) |
112 | 111 | adantl 481 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑖 ∈ 𝐹) → 𝑖 ∈ (ℤ ↑m Word
𝐴)) |
113 | 22, 13 | elmapd 8878 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → (𝑖 ∈ (ℤ ↑m Word
𝐴) ↔ 𝑖:Word 𝐴⟶ℤ)) |
114 | 113 | adantr 480 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑖 ∈ 𝐹) → (𝑖 ∈ (ℤ ↑m Word
𝐴) ↔ 𝑖:Word 𝐴⟶ℤ)) |
115 | 112, 114 | mpbid 232 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑖 ∈ 𝐹) → 𝑖:Word 𝐴⟶ℤ) |
116 | 115 | ffvelcdmda 7103 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑖 ∈ 𝐹) ∧ 𝑤 ∈ Word 𝐴) → (𝑖‘𝑤) ∈ ℤ) |
117 | 35 | adantlr 715 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑖 ∈ 𝐹) ∧ 𝑤 ∈ Word 𝐴) → (𝑀 Σg 𝑤) ∈ 𝐵) |
118 | 4, 15, 108, 116, 117 | mulgcld 19126 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑖 ∈ 𝐹) ∧ 𝑤 ∈ Word 𝐴) → ((𝑖‘𝑤) · (𝑀 Σg 𝑤)) ∈ 𝐵) |
119 | 118 | adantllr 719 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑤 ∈ Word 𝐴) → ((𝑖‘𝑤) · (𝑀 Σg 𝑤)) ∈ 𝐵) |
120 | | eqidd 2735 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) → (𝑤 ∈ Word 𝐴 ↦ ((𝑔‘𝑤) · (𝑀 Σg 𝑤))) = (𝑤 ∈ Word 𝐴 ↦ ((𝑔‘𝑤) · (𝑀 Σg 𝑤)))) |
121 | | eqidd 2735 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) → (𝑤 ∈ Word 𝐴 ↦ ((𝑖‘𝑤) · (𝑀 Σg 𝑤))) = (𝑤 ∈ Word 𝐴 ↦ ((𝑖‘𝑤) · (𝑀 Σg 𝑤)))) |
122 | 48 | adantr 480 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) → (𝑤 ∈ Word 𝐴 ↦ ((𝑔‘𝑤) · (𝑀 Σg 𝑤))) finSupp
(0g‘𝑅)) |
123 | 48 | ralrimiva 3143 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → ∀𝑔 ∈ 𝐹 (𝑤 ∈ Word 𝐴 ↦ ((𝑔‘𝑤) · (𝑀 Σg 𝑤))) finSupp
(0g‘𝑅)) |
124 | | fveq1 6905 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑔 = 𝑖 → (𝑔‘𝑤) = (𝑖‘𝑤)) |
125 | 124 | oveq1d 7445 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑔 = 𝑖 → ((𝑔‘𝑤) · (𝑀 Σg 𝑤)) = ((𝑖‘𝑤) · (𝑀 Σg 𝑤))) |
126 | 125 | mpteq2dv 5249 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑔 = 𝑖 → (𝑤 ∈ Word 𝐴 ↦ ((𝑔‘𝑤) · (𝑀 Σg 𝑤))) = (𝑤 ∈ Word 𝐴 ↦ ((𝑖‘𝑤) · (𝑀 Σg 𝑤)))) |
127 | 126 | breq1d 5157 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑔 = 𝑖 → ((𝑤 ∈ Word 𝐴 ↦ ((𝑔‘𝑤) · (𝑀 Σg 𝑤))) finSupp
(0g‘𝑅)
↔ (𝑤 ∈ Word 𝐴 ↦ ((𝑖‘𝑤) · (𝑀 Σg 𝑤))) finSupp
(0g‘𝑅))) |
128 | 127 | cbvralvw 3234 |
. . . . . . . . . . . . . . . . 17
⊢
(∀𝑔 ∈
𝐹 (𝑤 ∈ Word 𝐴 ↦ ((𝑔‘𝑤) · (𝑀 Σg 𝑤))) finSupp
(0g‘𝑅)
↔ ∀𝑖 ∈
𝐹 (𝑤 ∈ Word 𝐴 ↦ ((𝑖‘𝑤) · (𝑀 Σg 𝑤))) finSupp
(0g‘𝑅)) |
129 | 123, 128 | sylib 218 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → ∀𝑖 ∈ 𝐹 (𝑤 ∈ Word 𝐴 ↦ ((𝑖‘𝑤) · (𝑀 Σg 𝑤))) finSupp
(0g‘𝑅)) |
130 | 129 | r19.21bi 3248 |
. . . . . . . . . . . . . . 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 19956 |
. . . . . . . . . . . . 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 4234 |
. . . . . . . . . . . . . . . . . 18
⊢ (Word
𝐴 ∩ Word 𝐴) = Word 𝐴 |
138 | | eqidd 2735 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑤 ∈ Word 𝐴) → (𝑔‘𝑤) = (𝑔‘𝑤)) |
139 | | eqidd 2735 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑤 ∈ Word 𝐴) → (𝑖‘𝑤) = (𝑖‘𝑤)) |
140 | 134, 136,
106, 106, 137, 138, 139 | ofval 7707 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑤 ∈ Word 𝐴) → ((𝑔 ∘f + 𝑖)‘𝑤) = ((𝑔‘𝑤) + (𝑖‘𝑤))) |
141 | 140 | oveq1d 7445 |
. . . . . . . . . . . . . . . 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 19136 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑅 ∈ Grp ∧ ((𝑔‘𝑤) ∈ ℤ ∧ (𝑖‘𝑤) ∈ ℤ ∧ (𝑀 Σg 𝑤) ∈ 𝐵)) → (((𝑔‘𝑤) + (𝑖‘𝑤)) · (𝑀 Σg 𝑤)) = (((𝑔‘𝑤) · (𝑀 Σg 𝑤))(+g‘𝑅)((𝑖‘𝑤) · (𝑀 Σg 𝑤)))) |
147 | 142, 143,
144, 145, 146 | syl13anc 1371 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑤 ∈ Word 𝐴) → (((𝑔‘𝑤) + (𝑖‘𝑤)) · (𝑀 Σg 𝑤)) = (((𝑔‘𝑤) · (𝑀 Σg 𝑤))(+g‘𝑅)((𝑖‘𝑤) · (𝑀 Σg 𝑤)))) |
148 | 141, 147 | eqtr2d 2775 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑤 ∈ Word 𝐴) → (((𝑔‘𝑤) · (𝑀 Σg 𝑤))(+g‘𝑅)((𝑖‘𝑤) · (𝑀 Σg 𝑤))) = (((𝑔 ∘f + 𝑖)‘𝑤) · (𝑀 Σg 𝑤))) |
149 | 148 | mpteq2dva 5247 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) → (𝑤 ∈ Word 𝐴 ↦ (((𝑔‘𝑤) · (𝑀 Σg 𝑤))(+g‘𝑅)((𝑖‘𝑤) · (𝑀 Σg 𝑤)))) = (𝑤 ∈ Word 𝐴 ↦ (((𝑔 ∘f + 𝑖)‘𝑤) · (𝑀 Σg 𝑤)))) |
150 | 149 | oveq2d 7446 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ (((𝑔‘𝑤) · (𝑀 Σg 𝑤))(+g‘𝑅)((𝑖‘𝑤) · (𝑀 Σg 𝑤))))) = (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ (((𝑔 ∘f + 𝑖)‘𝑤) · (𝑀 Σg 𝑤))))) |
151 | 132, 150 | eqtr3d 2776 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) → ((𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑔‘𝑤) · (𝑀 Σg 𝑤))))(+g‘𝑅)(𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑖‘𝑤) · (𝑀 Σg 𝑤))))) = (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ (((𝑔 ∘f + 𝑖)‘𝑤) · (𝑀 Σg 𝑤))))) |
152 | | fveq1 6905 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑔 = ℎ → (𝑔‘𝑤) = (ℎ‘𝑤)) |
153 | 152 | oveq1d 7445 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑔 = ℎ → ((𝑔‘𝑤) · (𝑀 Σg 𝑤)) = ((ℎ‘𝑤) · (𝑀 Σg 𝑤))) |
154 | 153 | mpteq2dv 5249 |
. . . . . . . . . . . . . . . 16
⊢ (𝑔 = ℎ → (𝑤 ∈ Word 𝐴 ↦ ((𝑔‘𝑤) · (𝑀 Σg 𝑤))) = (𝑤 ∈ Word 𝐴 ↦ ((ℎ‘𝑤) · (𝑀 Σg 𝑤)))) |
155 | 154 | oveq2d 7446 |
. . . . . . . . . . . . . . 15
⊢ (𝑔 = ℎ → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑔‘𝑤) · (𝑀 Σg 𝑤)))) = (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((ℎ‘𝑤) · (𝑀 Σg 𝑤))))) |
156 | 155 | cbvmptv 5260 |
. . . . . . . . . . . . . 14
⊢ (𝑔 ∈ 𝐹 ↦ (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑔‘𝑤) · (𝑀 Σg 𝑤))))) = (ℎ ∈ 𝐹 ↦ (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((ℎ‘𝑤) · (𝑀 Σg 𝑤))))) |
157 | | fveq1 6905 |
. . . . . . . . . . . . . . . . . . 19
⊢ (ℎ = (𝑔 ∘f + 𝑖) → (ℎ‘𝑤) = ((𝑔 ∘f + 𝑖)‘𝑤)) |
158 | 157 | oveq1d 7445 |
. . . . . . . . . . . . . . . . . 18
⊢ (ℎ = (𝑔 ∘f + 𝑖) → ((ℎ‘𝑤) · (𝑀 Σg 𝑤)) = (((𝑔 ∘f + 𝑖)‘𝑤) · (𝑀 Σg 𝑤))) |
159 | 158 | mpteq2dv 5249 |
. . . . . . . . . . . . . . . . 17
⊢ (ℎ = (𝑔 ∘f + 𝑖) → (𝑤 ∈ Word 𝐴 ↦ ((ℎ‘𝑤) · (𝑀 Σg 𝑤))) = (𝑤 ∈ Word 𝐴 ↦ (((𝑔 ∘f + 𝑖)‘𝑤) · (𝑀 Σg 𝑤)))) |
160 | 159 | oveq2d 7446 |
. . . . . . . . . . . . . . . 16
⊢ (ℎ = (𝑔 ∘f + 𝑖) → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((ℎ‘𝑤) · (𝑀 Σg 𝑤)))) = (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ (((𝑔 ∘f + 𝑖)‘𝑤) · (𝑀 Σg 𝑤))))) |
161 | 160 | eqeq2d 2745 |
. . . . . . . . . . . . . . 15
⊢ (ℎ = (𝑔 ∘f + 𝑖) → ((𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ (((𝑔 ∘f + 𝑖)‘𝑤) · (𝑀 Σg 𝑤)))) = (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((ℎ‘𝑤) · (𝑀 Σg 𝑤)))) ↔ (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ (((𝑔 ∘f + 𝑖)‘𝑤) · (𝑀 Σg 𝑤)))) = (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ (((𝑔 ∘f + 𝑖)‘𝑤) · (𝑀 Σg 𝑤)))))) |
162 | | breq1 5150 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑓 = (𝑔 ∘f + 𝑖) → (𝑓 finSupp 0 ↔ (𝑔 ∘f + 𝑖) finSupp 0)) |
163 | 21 | a1i 11 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) → ℤ ∈ V) |
164 | | zaddcl 12654 |
. . . . . . . . . . . . . . . . . . . 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 7714 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) → (𝑔 ∘f + 𝑖):Word 𝐴⟶ℤ) |
169 | 163, 106,
168 | elmapdd 8879 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) → (𝑔 ∘f + 𝑖) ∈ (ℤ ↑m Word
𝐴)) |
170 | | zringring 21477 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
ℤring ∈ Ring |
171 | | ringmnd 20260 |
. . . . . . . . . . . . . . . . . . . . 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 21486 |
. . . . . . . . . . . . . . . . . . . 20
⊢ 0 =
(0g‘ℤring) |
178 | 176, 177 | breqtrdi 5188 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) → 𝑔 finSupp
(0g‘ℤring)) |
179 | 110 | simprbi 496 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑖 ∈ 𝐹 → 𝑖 finSupp 0) |
180 | 179 | adantl 481 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) → 𝑖 finSupp 0) |
181 | 180, 177 | breqtrdi 5188 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) → 𝑖 finSupp
(0g‘ℤring)) |
182 | | zringbas 21481 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ℤ =
(Base‘ℤring) |
183 | 182 | mndpfsupp 18792 |
. . . . . . . . . . . . . . . . . . 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 1385 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) → (𝑔 ∘f
(+g‘ℤring)𝑖) finSupp
(0g‘ℤring)) |
185 | | zringplusg 21482 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ + =
(+g‘ℤring) |
186 | 185 | a1i 11 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) → + =
(+g‘ℤring)) |
187 | 186 | ofeqd 7698 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) → ∘f + =
∘f
(+g‘ℤring)) |
188 | 187 | oveqd 7447 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) → (𝑔 ∘f + 𝑖) = (𝑔 ∘f
(+g‘ℤring)𝑖)) |
189 | 177 | a1i 11 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) → 0 =
(0g‘ℤring)) |
190 | 184, 188,
189 | 3brtr4d 5179 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) → (𝑔 ∘f + 𝑖) finSupp 0) |
191 | 162, 169,
190 | elrabd 3696 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) → (𝑔 ∘f + 𝑖) ∈ {𝑓 ∈ (ℤ ↑m Word
𝐴) ∣ 𝑓 finSupp 0}) |
192 | 191, 17 | eleqtrrdi 2849 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) → (𝑔 ∘f + 𝑖) ∈ 𝐹) |
193 | | eqidd 2735 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ (((𝑔 ∘f + 𝑖)‘𝑤) · (𝑀 Σg 𝑤)))) = (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ (((𝑔 ∘f + 𝑖)‘𝑤) · (𝑀 Σg 𝑤))))) |
194 | 161, 192,
193 | rspcedvdw 3624 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) → ∃ℎ ∈ 𝐹 (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ (((𝑔 ∘f + 𝑖)‘𝑤) · (𝑀 Σg 𝑤)))) = (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((ℎ‘𝑤) · (𝑀 Σg 𝑤))))) |
195 | | ovexd 7465 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ (((𝑔 ∘f + 𝑖)‘𝑤) · (𝑀 Σg 𝑤)))) ∈ V) |
196 | 156, 194,
195 | elrnmptd 5976 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ (((𝑔 ∘f + 𝑖)‘𝑤) · (𝑀 Σg 𝑤)))) ∈ ran (𝑔 ∈ 𝐹 ↦ (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑔‘𝑤) · (𝑀 Σg 𝑤)))))) |
197 | 196, 52 | eleqtrrdi 2849 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ (((𝑔 ∘f + 𝑖)‘𝑤) · (𝑀 Σg 𝑤)))) ∈ 𝑆) |
198 | 151, 197 | eqeltrd 2838 |
. . . . . . . . . . 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 2838 |
. . . . . . 7
⊢
(((((((𝜑 ∧ 𝑥 ∈ 𝑆) ∧ 𝑦 ∈ 𝑆) ∧ 𝑔 ∈ 𝐹) ∧ 𝑥 = (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑔‘𝑤) · (𝑀 Σg 𝑤))))) ∧ 𝑖 ∈ 𝐹) ∧ 𝑦 = (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑖‘𝑤) · (𝑀 Σg 𝑤))))) → (𝑥(+g‘𝑅)𝑦) ∈ 𝑆) |
203 | 52 | eleq2i 2830 |
. . . . . . . . . 10
⊢ (𝑦 ∈ 𝑆 ↔ 𝑦 ∈ ran (𝑔 ∈ 𝐹 ↦ (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑔‘𝑤) · (𝑀 Σg 𝑤)))))) |
204 | 126 | oveq2d 7446 |
. . . . . . . . . . . . 13
⊢ (𝑔 = 𝑖 → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑔‘𝑤) · (𝑀 Σg 𝑤)))) = (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑖‘𝑤) · (𝑀 Σg 𝑤))))) |
205 | 204 | cbvmptv 5260 |
. . . . . . . . . . . 12
⊢ (𝑔 ∈ 𝐹 ↦ (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑔‘𝑤) · (𝑀 Σg 𝑤))))) = (𝑖 ∈ 𝐹 ↦ (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑖‘𝑤) · (𝑀 Σg 𝑤))))) |
206 | 205 | elrnmpt 5971 |
. . . . . . . . . . 11
⊢ (𝑦 ∈ V → (𝑦 ∈ ran (𝑔 ∈ 𝐹 ↦ (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑔‘𝑤) · (𝑀 Σg 𝑤))))) ↔ ∃𝑖 ∈ 𝐹 𝑦 = (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑖‘𝑤) · (𝑀 Σg 𝑤)))))) |
207 | 206 | elv 3482 |
. . . . . . . . . 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 3159 |
. . . . . 6
⊢
(((((𝜑 ∧ 𝑥 ∈ 𝑆) ∧ 𝑦 ∈ 𝑆) ∧ 𝑔 ∈ 𝐹) ∧ 𝑥 = (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑔‘𝑤) · (𝑀 Σg 𝑤))))) → (𝑥(+g‘𝑅)𝑦) ∈ 𝑆) |
212 | 58 | adantr 480 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑥 ∈ 𝑆) ∧ 𝑦 ∈ 𝑆) → ∃𝑔 ∈ 𝐹 𝑥 = (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑔‘𝑤) · (𝑀 Σg 𝑤))))) |
213 | 211, 212 | r19.29a 3159 |
. . . . 5
⊢ (((𝜑 ∧ 𝑥 ∈ 𝑆) ∧ 𝑦 ∈ 𝑆) → (𝑥(+g‘𝑅)𝑦) ∈ 𝑆) |
214 | 213 | ralrimiva 3143 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → ∀𝑦 ∈ 𝑆 (𝑥(+g‘𝑅)𝑦) ∈ 𝑆) |
215 | 2 | ad3antrrr 730 |
. . . . . . 7
⊢ ((((𝜑 ∧ 𝑥 ∈ 𝑆) ∧ 𝑔 ∈ 𝐹) ∧ 𝑥 = (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑔‘𝑤) · (𝑀 Σg 𝑤))))) → 𝑅 ∈ Grp) |
216 | 26 | znegcld 12721 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑤 ∈ Word 𝐴) → -(𝑔‘𝑤) ∈ ℤ) |
217 | 4, 15, 16, 216, 36 | mulgcld 19126 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑤 ∈ Word 𝐴) → (-(𝑔‘𝑤) · (𝑀 Σg 𝑤)) ∈ 𝐵) |
218 | 217 | fmpttd 7134 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑔 ∈ 𝐹) → (𝑤 ∈ Word 𝐴 ↦ (-(𝑔‘𝑤) · (𝑀 Σg 𝑤))):Word 𝐴⟶𝐵) |
219 | 25 | adantr 480 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑤 ∈ Word 𝐴) → 𝑔:Word 𝐴⟶ℤ) |
220 | | simpr 484 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑤 ∈ Word 𝐴) → 𝑤 ∈ Word 𝐴) |
221 | 219, 220 | fvco3d 7008 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑤 ∈ Word 𝐴) → (((𝑧 ∈ ℤ ↦ -𝑧) ∘ 𝑔)‘𝑤) = ((𝑧 ∈ ℤ ↦ -𝑧)‘(𝑔‘𝑤))) |
222 | | eqid 2734 |
. . . . . . . . . . . . . 14
⊢ (𝑧 ∈ ℤ ↦ -𝑧) = (𝑧 ∈ ℤ ↦ -𝑧) |
223 | | negeq 11497 |
. . . . . . . . . . . . . 14
⊢ (𝑧 = (𝑔‘𝑤) → -𝑧 = -(𝑔‘𝑤)) |
224 | 222, 223,
26, 216 | fvmptd3 7038 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑤 ∈ Word 𝐴) → ((𝑧 ∈ ℤ ↦ -𝑧)‘(𝑔‘𝑤)) = -(𝑔‘𝑤)) |
225 | 221, 224 | eqtrd 2774 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑤 ∈ Word 𝐴) → (((𝑧 ∈ ℤ ↦ -𝑧) ∘ 𝑔)‘𝑤) = -(𝑔‘𝑤)) |
226 | 225 | oveq1d 7445 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑤 ∈ Word 𝐴) → ((((𝑧 ∈ ℤ ↦ -𝑧) ∘ 𝑔)‘𝑤) · (𝑀 Σg 𝑤)) = (-(𝑔‘𝑤) · (𝑀 Σg 𝑤))) |
227 | 226 | mpteq2dva 5247 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑔 ∈ 𝐹) → (𝑤 ∈ Word 𝐴 ↦ ((((𝑧 ∈ ℤ ↦ -𝑧) ∘ 𝑔)‘𝑤) · (𝑀 Σg 𝑤))) = (𝑤 ∈ Word 𝐴 ↦ (-(𝑔‘𝑤) · (𝑀 Σg 𝑤)))) |
228 | | simpr 484 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑧 ∈ ℤ) → 𝑧 ∈ ℤ) |
229 | 228 | znegcld 12721 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑧 ∈ ℤ) → -𝑧 ∈ ℤ) |
230 | 229 | fmpttd 7134 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝑧 ∈ ℤ ↦ -𝑧):ℤ⟶ℤ) |
231 | 230 | adantr 480 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑔 ∈ 𝐹) → (𝑧 ∈ ℤ ↦ -𝑧):ℤ⟶ℤ) |
232 | 231, 25 | fcod 6761 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑔 ∈ 𝐹) → ((𝑧 ∈ ℤ ↦ -𝑧) ∘ 𝑔):Word 𝐴⟶ℤ) |
233 | 21 | a1i 11 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑔 ∈ 𝐹) → ℤ ∈ V) |
234 | | negeq 11497 |
. . . . . . . . . . . . . . 15
⊢ (𝑧 = 0 → -𝑧 = -0) |
235 | | neg0 11552 |
. . . . . . . . . . . . . . 15
⊢ -0 =
0 |
236 | 234, 235 | eqtrdi 2790 |
. . . . . . . . . . . . . 14
⊢ (𝑧 = 0 → -𝑧 = 0) |
237 | | 0zd 12622 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 0 ∈
ℤ) |
238 | 222, 236,
237, 237 | fvmptd3 7038 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ((𝑧 ∈ ℤ ↦ -𝑧)‘0) = 0) |
239 | 238 | adantr 480 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑔 ∈ 𝐹) → ((𝑧 ∈ ℤ ↦ -𝑧)‘0) = 0) |
240 | 40, 25, 231, 14, 233, 45, 239 | fsuppco2 9440 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑔 ∈ 𝐹) → ((𝑧 ∈ ℤ ↦ -𝑧) ∘ 𝑔) finSupp 0) |
241 | 39, 40, 14, 41, 36, 232, 240, 47 | fisuppov1 32697 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑔 ∈ 𝐹) → (𝑤 ∈ Word 𝐴 ↦ ((((𝑧 ∈ ℤ ↦ -𝑧) ∘ 𝑔)‘𝑤) · (𝑀 Σg 𝑤))) finSupp
(0g‘𝑅)) |
242 | 227, 241 | eqbrtrrd 5171 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑔 ∈ 𝐹) → (𝑤 ∈ Word 𝐴 ↦ (-(𝑔‘𝑤) · (𝑀 Σg 𝑤))) finSupp
(0g‘𝑅)) |
243 | 4, 5, 7, 14, 218, 242 | gsumcl 19947 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑔 ∈ 𝐹) → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ (-(𝑔‘𝑤) · (𝑀 Σg 𝑤)))) ∈ 𝐵) |
244 | 243 | ad4ant13 751 |
. . . . . . 7
⊢ ((((𝜑 ∧ 𝑥 ∈ 𝑆) ∧ 𝑔 ∈ 𝐹) ∧ 𝑥 = (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑔‘𝑤) · (𝑀 Σg 𝑤))))) → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ (-(𝑔‘𝑤) · (𝑀 Σg 𝑤)))) ∈ 𝐵) |
245 | 3 | oveq1d 7445 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 𝑥 ∈ 𝑆) ∧ 𝑔 ∈ 𝐹) ∧ 𝑥 = (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑔‘𝑤) · (𝑀 Σg 𝑤))))) → (𝑥(+g‘𝑅)(𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ (-(𝑔‘𝑤) · (𝑀 Σg 𝑤))))) = ((𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑔‘𝑤) · (𝑀 Σg 𝑤))))(+g‘𝑅)(𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ (-(𝑔‘𝑤) · (𝑀 Σg 𝑤)))))) |
246 | | eqidd 2735 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑔 ∈ 𝐹) → (𝑤 ∈ Word 𝐴 ↦ ((𝑔‘𝑤) · (𝑀 Σg 𝑤))) = (𝑤 ∈ Word 𝐴 ↦ ((𝑔‘𝑤) · (𝑀 Σg 𝑤)))) |
247 | | eqidd 2735 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑔 ∈ 𝐹) → (𝑤 ∈ Word 𝐴 ↦ (-(𝑔‘𝑤) · (𝑀 Σg 𝑤))) = (𝑤 ∈ Word 𝐴 ↦ (-(𝑔‘𝑤) · (𝑀 Σg 𝑤)))) |
248 | 4, 5, 104, 7, 14, 37, 217, 246, 247, 48, 242 | gsummptfsadd 19956 |
. . . . . . . . 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 12720 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑤 ∈ Word 𝐴) → (𝑔‘𝑤) ∈ ℂ) |
251 | 250 | negidd 11607 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑤 ∈ Word 𝐴) → ((𝑔‘𝑤) + -(𝑔‘𝑤)) = 0) |
252 | 251 | oveq1d 7445 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑤 ∈ Word 𝐴) → (((𝑔‘𝑤) + -(𝑔‘𝑤)) · (𝑀 Σg 𝑤)) = (0 · (𝑀 Σg 𝑤))) |
253 | 4, 15, 104 | mulgdir 19136 |
. . . . . . . . . . . . . 14
⊢ ((𝑅 ∈ Grp ∧ ((𝑔‘𝑤) ∈ ℤ ∧ -(𝑔‘𝑤) ∈ ℤ ∧ (𝑀 Σg 𝑤) ∈ 𝐵)) → (((𝑔‘𝑤) + -(𝑔‘𝑤)) · (𝑀 Σg 𝑤)) = (((𝑔‘𝑤) · (𝑀 Σg 𝑤))(+g‘𝑅)(-(𝑔‘𝑤) · (𝑀 Σg 𝑤)))) |
254 | 16, 26, 216, 36, 253 | syl13anc 1371 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑤 ∈ Word 𝐴) → (((𝑔‘𝑤) + -(𝑔‘𝑤)) · (𝑀 Σg 𝑤)) = (((𝑔‘𝑤) · (𝑀 Σg 𝑤))(+g‘𝑅)(-(𝑔‘𝑤) · (𝑀 Σg 𝑤)))) |
255 | 36, 84 | syl 17 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑤 ∈ Word 𝐴) → (0 · (𝑀 Σg 𝑤)) = (0g‘𝑅)) |
256 | 252, 254,
255 | 3eqtr3d 2782 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑤 ∈ Word 𝐴) → (((𝑔‘𝑤) · (𝑀 Σg 𝑤))(+g‘𝑅)(-(𝑔‘𝑤) · (𝑀 Σg 𝑤))) = (0g‘𝑅)) |
257 | 256 | mpteq2dva 5247 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑔 ∈ 𝐹) → (𝑤 ∈ Word 𝐴 ↦ (((𝑔‘𝑤) · (𝑀 Σg 𝑤))(+g‘𝑅)(-(𝑔‘𝑤) · (𝑀 Σg 𝑤)))) = (𝑤 ∈ Word 𝐴 ↦ (0g‘𝑅))) |
258 | 257 | oveq2d 7446 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑔 ∈ 𝐹) → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ (((𝑔‘𝑤) · (𝑀 Σg 𝑤))(+g‘𝑅)(-(𝑔‘𝑤) · (𝑀 Σg 𝑤))))) = (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ (0g‘𝑅)))) |
259 | 91 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑔 ∈ 𝐹) → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ (0g‘𝑅))) = (0g‘𝑅)) |
260 | 258, 259 | eqtrd 2774 |
. . . . . . . . 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 2780 |
. . . . . . 7
⊢ ((((𝜑 ∧ 𝑥 ∈ 𝑆) ∧ 𝑔 ∈ 𝐹) ∧ 𝑥 = (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑔‘𝑤) · (𝑀 Σg 𝑤))))) → (𝑥(+g‘𝑅)(𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ (-(𝑔‘𝑤) · (𝑀 Σg 𝑤))))) =
(0g‘𝑅)) |
263 | | eqid 2734 |
. . . . . . . . 9
⊢
(invg‘𝑅) = (invg‘𝑅) |
264 | 4, 104, 5, 263 | grpinvid1 19021 |
. . . . . . . 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 1372 |
. . . . . 6
⊢ ((((𝜑 ∧ 𝑥 ∈ 𝑆) ∧ 𝑔 ∈ 𝐹) ∧ 𝑥 = (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑔‘𝑤) · (𝑀 Σg 𝑤))))) →
((invg‘𝑅)‘𝑥) = (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ (-(𝑔‘𝑤) · (𝑀 Σg 𝑤))))) |
267 | | fveq1 6905 |
. . . . . . . . . . . . . 14
⊢ (ℎ = (𝑣 ∈ Word 𝐴 ↦ -(𝑔‘𝑣)) → (ℎ‘𝑤) = ((𝑣 ∈ Word 𝐴 ↦ -(𝑔‘𝑣))‘𝑤)) |
268 | 267 | oveq1d 7445 |
. . . . . . . . . . . . 13
⊢ (ℎ = (𝑣 ∈ Word 𝐴 ↦ -(𝑔‘𝑣)) → ((ℎ‘𝑤) · (𝑀 Σg 𝑤)) = (((𝑣 ∈ Word 𝐴 ↦ -(𝑔‘𝑣))‘𝑤) · (𝑀 Σg 𝑤))) |
269 | 268 | mpteq2dv 5249 |
. . . . . . . . . . . 12
⊢ (ℎ = (𝑣 ∈ Word 𝐴 ↦ -(𝑔‘𝑣)) → (𝑤 ∈ Word 𝐴 ↦ ((ℎ‘𝑤) · (𝑀 Σg 𝑤))) = (𝑤 ∈ Word 𝐴 ↦ (((𝑣 ∈ Word 𝐴 ↦ -(𝑔‘𝑣))‘𝑤) · (𝑀 Σg 𝑤)))) |
270 | 269 | oveq2d 7446 |
. . . . . . . . . . 11
⊢ (ℎ = (𝑣 ∈ Word 𝐴 ↦ -(𝑔‘𝑣)) → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((ℎ‘𝑤) · (𝑀 Σg 𝑤)))) = (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ (((𝑣 ∈ Word 𝐴 ↦ -(𝑔‘𝑣))‘𝑤) · (𝑀 Σg 𝑤))))) |
271 | 270 | eqeq2d 2745 |
. . . . . . . . . 10
⊢ (ℎ = (𝑣 ∈ Word 𝐴 ↦ -(𝑔‘𝑣)) → ((𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ (-(𝑔‘𝑤) · (𝑀 Σg 𝑤)))) = (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((ℎ‘𝑤) · (𝑀 Σg 𝑤)))) ↔ (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ (-(𝑔‘𝑤) · (𝑀 Σg 𝑤)))) = (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ (((𝑣 ∈ Word 𝐴 ↦ -(𝑔‘𝑣))‘𝑤) · (𝑀 Σg 𝑤)))))) |
272 | | breq1 5150 |
. . . . . . . . . . . 12
⊢ (𝑓 = (𝑣 ∈ Word 𝐴 ↦ -(𝑔‘𝑣)) → (𝑓 finSupp 0 ↔ (𝑣 ∈ Word 𝐴 ↦ -(𝑔‘𝑣)) finSupp 0)) |
273 | 25 | ffvelcdmda 7103 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑣 ∈ Word 𝐴) → (𝑔‘𝑣) ∈ ℤ) |
274 | 273 | znegcld 12721 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑣 ∈ Word 𝐴) → -(𝑔‘𝑣) ∈ ℤ) |
275 | 274 | fmpttd 7134 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑔 ∈ 𝐹) → (𝑣 ∈ Word 𝐴 ↦ -(𝑔‘𝑣)):Word 𝐴⟶ℤ) |
276 | 233, 14, 275 | elmapdd 8879 |
. . . . . . . . . . . 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 12622 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑣 ∈ (Word 𝐴 ∖ (𝑔 supp 0))) → 0 ∈
ℤ) |
281 | | simpr 484 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑣 ∈ (Word 𝐴 ∖ (𝑔 supp 0))) → 𝑣 ∈ (Word 𝐴 ∖ (𝑔 supp 0))) |
282 | 278, 279,
280, 281 | fvdifsupp 8194 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑣 ∈ (Word 𝐴 ∖ (𝑔 supp 0))) → (𝑔‘𝑣) = 0) |
283 | 282 | negeqd 11499 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑣 ∈ (Word 𝐴 ∖ (𝑔 supp 0))) → -(𝑔‘𝑣) = -0) |
284 | 283, 235 | eqtrdi 2790 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑣 ∈ (Word 𝐴 ∖ (𝑔 supp 0))) → -(𝑔‘𝑣) = 0) |
285 | 284, 14 | suppss2 8223 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑔 ∈ 𝐹) → ((𝑣 ∈ Word 𝐴 ↦ -(𝑔‘𝑣)) supp 0) ⊆ (𝑔 supp 0)) |
286 | 276, 40, 277, 45, 285 | fsuppsssuppgd 9419 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑔 ∈ 𝐹) → (𝑣 ∈ Word 𝐴 ↦ -(𝑔‘𝑣)) finSupp 0) |
287 | 272, 276,
286 | elrabd 3696 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑔 ∈ 𝐹) → (𝑣 ∈ Word 𝐴 ↦ -(𝑔‘𝑣)) ∈ {𝑓 ∈ (ℤ ↑m Word
𝐴) ∣ 𝑓 finSupp 0}) |
288 | 287, 17 | eleqtrrdi 2849 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑔 ∈ 𝐹) → (𝑣 ∈ Word 𝐴 ↦ -(𝑔‘𝑣)) ∈ 𝐹) |
289 | | eqid 2734 |
. . . . . . . . . . . . . . 15
⊢ (𝑣 ∈ Word 𝐴 ↦ -(𝑔‘𝑣)) = (𝑣 ∈ Word 𝐴 ↦ -(𝑔‘𝑣)) |
290 | | fveq2 6906 |
. . . . . . . . . . . . . . . 16
⊢ (𝑣 = 𝑤 → (𝑔‘𝑣) = (𝑔‘𝑤)) |
291 | 290 | negeqd 11499 |
. . . . . . . . . . . . . . 15
⊢ (𝑣 = 𝑤 → -(𝑔‘𝑣) = -(𝑔‘𝑤)) |
292 | 289, 291,
220, 216 | fvmptd3 7038 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑤 ∈ Word 𝐴) → ((𝑣 ∈ Word 𝐴 ↦ -(𝑔‘𝑣))‘𝑤) = -(𝑔‘𝑤)) |
293 | 292 | eqcomd 2740 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑤 ∈ Word 𝐴) → -(𝑔‘𝑤) = ((𝑣 ∈ Word 𝐴 ↦ -(𝑔‘𝑣))‘𝑤)) |
294 | 293 | oveq1d 7445 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑤 ∈ Word 𝐴) → (-(𝑔‘𝑤) · (𝑀 Σg 𝑤)) = (((𝑣 ∈ Word 𝐴 ↦ -(𝑔‘𝑣))‘𝑤) · (𝑀 Σg 𝑤))) |
295 | 294 | mpteq2dva 5247 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑔 ∈ 𝐹) → (𝑤 ∈ Word 𝐴 ↦ (-(𝑔‘𝑤) · (𝑀 Σg 𝑤))) = (𝑤 ∈ Word 𝐴 ↦ (((𝑣 ∈ Word 𝐴 ↦ -(𝑔‘𝑣))‘𝑤) · (𝑀 Σg 𝑤)))) |
296 | 295 | oveq2d 7446 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑔 ∈ 𝐹) → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ (-(𝑔‘𝑤) · (𝑀 Σg 𝑤)))) = (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ (((𝑣 ∈ Word 𝐴 ↦ -(𝑔‘𝑣))‘𝑤) · (𝑀 Σg 𝑤))))) |
297 | 271, 288,
296 | rspcedvdw 3624 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑔 ∈ 𝐹) → ∃ℎ ∈ 𝐹 (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ (-(𝑔‘𝑤) · (𝑀 Σg 𝑤)))) = (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((ℎ‘𝑤) · (𝑀 Σg 𝑤))))) |
298 | 156, 297,
243 | elrnmptd 5976 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑔 ∈ 𝐹) → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ (-(𝑔‘𝑤) · (𝑀 Σg 𝑤)))) ∈ ran (𝑔 ∈ 𝐹 ↦ (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑔‘𝑤) · (𝑀 Σg 𝑤)))))) |
299 | 298, 52 | eleqtrrdi 2849 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑔 ∈ 𝐹) → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ (-(𝑔‘𝑤) · (𝑀 Σg 𝑤)))) ∈ 𝑆) |
300 | 299 | ad4ant13 751 |
. . . . . 6
⊢ ((((𝜑 ∧ 𝑥 ∈ 𝑆) ∧ 𝑔 ∈ 𝐹) ∧ 𝑥 = (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑔‘𝑤) · (𝑀 Σg 𝑤))))) → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ (-(𝑔‘𝑤) · (𝑀 Σg 𝑤)))) ∈ 𝑆) |
301 | 266, 300 | eqeltrd 2838 |
. . . . 5
⊢ ((((𝜑 ∧ 𝑥 ∈ 𝑆) ∧ 𝑔 ∈ 𝐹) ∧ 𝑥 = (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑔‘𝑤) · (𝑀 Σg 𝑤))))) →
((invg‘𝑅)‘𝑥) ∈ 𝑆) |
302 | 301, 58 | r19.29a 3159 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → ((invg‘𝑅)‘𝑥) ∈ 𝑆) |
303 | 214, 302 | jca 511 |
. . 3
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → (∀𝑦 ∈ 𝑆 (𝑥(+g‘𝑅)𝑦) ∈ 𝑆 ∧ ((invg‘𝑅)‘𝑥) ∈ 𝑆)) |
304 | 303 | ralrimiva 3143 |
. 2
⊢ (𝜑 → ∀𝑥 ∈ 𝑆 (∀𝑦 ∈ 𝑆 (𝑥(+g‘𝑅)𝑦) ∈ 𝑆 ∧ ((invg‘𝑅)‘𝑥) ∈ 𝑆)) |
305 | 4, 104, 263 | issubg2 19171 |
. . 3
⊢ (𝑅 ∈ Grp → (𝑆 ∈ (SubGrp‘𝑅) ↔ (𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅ ∧ ∀𝑥 ∈ 𝑆 (∀𝑦 ∈ 𝑆 (𝑥(+g‘𝑅)𝑦) ∈ 𝑆 ∧ ((invg‘𝑅)‘𝑥) ∈ 𝑆)))) |
306 | 305 | biimpar 477 |
. 2
⊢ ((𝑅 ∈ Grp ∧ (𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅ ∧ ∀𝑥 ∈ 𝑆 (∀𝑦 ∈ 𝑆 (𝑥(+g‘𝑅)𝑦) ∈ 𝑆 ∧ ((invg‘𝑅)‘𝑥) ∈ 𝑆))) → 𝑆 ∈ (SubGrp‘𝑅)) |
307 | 2, 63, 100, 304, 306 | syl13anc 1371 |
1
⊢ (𝜑 → 𝑆 ∈ (SubGrp‘𝑅)) |