Step | Hyp | Ref
| Expression |
1 | | elrgspn.r |
. 2
⊢ (𝜑 → 𝑅 ∈ Ring) |
2 | | elrgspn.b |
. . 3
⊢ 𝐵 = (Base‘𝑅) |
3 | | elrgspn.m |
. . 3
⊢ 𝑀 = (mulGrp‘𝑅) |
4 | | elrgspn.x |
. . 3
⊢ · =
(.g‘𝑅) |
5 | | elrgspn.n |
. . 3
⊢ 𝑁 = (RingSpan‘𝑅) |
6 | | elrgspn.f |
. . 3
⊢ 𝐹 = {𝑓 ∈ (ℤ ↑m Word
𝐴) ∣ 𝑓 finSupp 0} |
7 | | elrgspn.a |
. . 3
⊢ (𝜑 → 𝐴 ⊆ 𝐵) |
8 | | elrgspnlem1.1 |
. . 3
⊢ 𝑆 = ran (𝑔 ∈ 𝐹 ↦ (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑔‘𝑤) · (𝑀 Σg 𝑤))))) |
9 | 2, 3, 4, 5, 6, 1, 7, 8 | elrgspnlem1 33231 |
. 2
⊢ (𝜑 → 𝑆 ∈ (SubGrp‘𝑅)) |
10 | | eqeq2 2746 |
. . . . . . 7
⊢
((1r‘𝑅) = if(𝑤 = ∅, (1r‘𝑅), (0g‘𝑅)) → ((((𝑣 ∈ Word 𝐴 ↦ if(𝑣 = ∅, 1, 0))‘𝑤) · (𝑀 Σg 𝑤)) = (1r‘𝑅) ↔ (((𝑣 ∈ Word 𝐴 ↦ if(𝑣 = ∅, 1, 0))‘𝑤) · (𝑀 Σg 𝑤)) = if(𝑤 = ∅, (1r‘𝑅), (0g‘𝑅)))) |
11 | | eqeq2 2746 |
. . . . . . 7
⊢
((0g‘𝑅) = if(𝑤 = ∅, (1r‘𝑅), (0g‘𝑅)) → ((((𝑣 ∈ Word 𝐴 ↦ if(𝑣 = ∅, 1, 0))‘𝑤) · (𝑀 Σg 𝑤)) = (0g‘𝑅) ↔ (((𝑣 ∈ Word 𝐴 ↦ if(𝑣 = ∅, 1, 0))‘𝑤) · (𝑀 Σg 𝑤)) = if(𝑤 = ∅, (1r‘𝑅), (0g‘𝑅)))) |
12 | | simpr 484 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑤 ∈ Word 𝐴) ∧ 𝑤 = ∅) → 𝑤 = ∅) |
13 | 12 | fveq2d 6910 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑤 ∈ Word 𝐴) ∧ 𝑤 = ∅) → ((𝑣 ∈ Word 𝐴 ↦ if(𝑣 = ∅, 1, 0))‘𝑤) = ((𝑣 ∈ Word 𝐴 ↦ if(𝑣 = ∅, 1,
0))‘∅)) |
14 | | eqid 2734 |
. . . . . . . . . . . 12
⊢ (𝑣 ∈ Word 𝐴 ↦ if(𝑣 = ∅, 1, 0)) = (𝑣 ∈ Word 𝐴 ↦ if(𝑣 = ∅, 1, 0)) |
15 | | simpr 484 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑣 = ∅) → 𝑣 = ∅) |
16 | 15 | iftrued 4538 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑣 = ∅) → if(𝑣 = ∅, 1, 0) = 1) |
17 | | wrd0 14573 |
. . . . . . . . . . . . 13
⊢ ∅
∈ Word 𝐴 |
18 | 17 | a1i 11 |
. . . . . . . . . . . 12
⊢ (𝜑 → ∅ ∈ Word 𝐴) |
19 | | 1zzd 12645 |
. . . . . . . . . . . 12
⊢ (𝜑 → 1 ∈
ℤ) |
20 | 14, 16, 18, 19 | fvmptd2 7023 |
. . . . . . . . . . 11
⊢ (𝜑 → ((𝑣 ∈ Word 𝐴 ↦ if(𝑣 = ∅, 1, 0))‘∅) =
1) |
21 | 20 | ad2antrr 726 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑤 ∈ Word 𝐴) ∧ 𝑤 = ∅) → ((𝑣 ∈ Word 𝐴 ↦ if(𝑣 = ∅, 1, 0))‘∅) =
1) |
22 | 13, 21 | eqtrd 2774 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑤 ∈ Word 𝐴) ∧ 𝑤 = ∅) → ((𝑣 ∈ Word 𝐴 ↦ if(𝑣 = ∅, 1, 0))‘𝑤) = 1) |
23 | 12 | oveq2d 7446 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑤 ∈ Word 𝐴) ∧ 𝑤 = ∅) → (𝑀 Σg 𝑤) = (𝑀 Σg
∅)) |
24 | | eqid 2734 |
. . . . . . . . . . . 12
⊢
(1r‘𝑅) = (1r‘𝑅) |
25 | 3, 24 | ringidval 20200 |
. . . . . . . . . . 11
⊢
(1r‘𝑅) = (0g‘𝑀) |
26 | 25 | gsum0 18709 |
. . . . . . . . . 10
⊢ (𝑀 Σg
∅) = (1r‘𝑅) |
27 | 23, 26 | eqtrdi 2790 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑤 ∈ Word 𝐴) ∧ 𝑤 = ∅) → (𝑀 Σg 𝑤) = (1r‘𝑅)) |
28 | 22, 27 | oveq12d 7448 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑤 ∈ Word 𝐴) ∧ 𝑤 = ∅) → (((𝑣 ∈ Word 𝐴 ↦ if(𝑣 = ∅, 1, 0))‘𝑤) · (𝑀 Σg 𝑤)) = (1 ·
(1r‘𝑅))) |
29 | 2, 24 | ringidcl 20279 |
. . . . . . . . . . 11
⊢ (𝑅 ∈ Ring →
(1r‘𝑅)
∈ 𝐵) |
30 | 1, 29 | syl 17 |
. . . . . . . . . 10
⊢ (𝜑 → (1r‘𝑅) ∈ 𝐵) |
31 | 2, 4 | mulg1 19111 |
. . . . . . . . . 10
⊢
((1r‘𝑅) ∈ 𝐵 → (1 ·
(1r‘𝑅)) =
(1r‘𝑅)) |
32 | 30, 31 | syl 17 |
. . . . . . . . 9
⊢ (𝜑 → (1 ·
(1r‘𝑅)) =
(1r‘𝑅)) |
33 | 32 | ad2antrr 726 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑤 ∈ Word 𝐴) ∧ 𝑤 = ∅) → (1 ·
(1r‘𝑅)) =
(1r‘𝑅)) |
34 | 28, 33 | eqtrd 2774 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑤 ∈ Word 𝐴) ∧ 𝑤 = ∅) → (((𝑣 ∈ Word 𝐴 ↦ if(𝑣 = ∅, 1, 0))‘𝑤) · (𝑀 Σg 𝑤)) = (1r‘𝑅)) |
35 | | eqeq1 2738 |
. . . . . . . . . . . . . 14
⊢ (𝑣 = 𝑤 → (𝑣 = ∅ ↔ 𝑤 = ∅)) |
36 | 35 | notbid 318 |
. . . . . . . . . . . . 13
⊢ (𝑣 = 𝑤 → (¬ 𝑣 = ∅ ↔ ¬ 𝑤 = ∅)) |
37 | 36 | biimparc 479 |
. . . . . . . . . . . 12
⊢ ((¬
𝑤 = ∅ ∧ 𝑣 = 𝑤) → ¬ 𝑣 = ∅) |
38 | 37 | adantll 714 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑤 ∈ Word 𝐴) ∧ ¬ 𝑤 = ∅) ∧ 𝑣 = 𝑤) → ¬ 𝑣 = ∅) |
39 | 38 | iffalsed 4541 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑤 ∈ Word 𝐴) ∧ ¬ 𝑤 = ∅) ∧ 𝑣 = 𝑤) → if(𝑣 = ∅, 1, 0) = 0) |
40 | | simplr 769 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑤 ∈ Word 𝐴) ∧ ¬ 𝑤 = ∅) → 𝑤 ∈ Word 𝐴) |
41 | | 0zd 12622 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑤 ∈ Word 𝐴) ∧ ¬ 𝑤 = ∅) → 0 ∈
ℤ) |
42 | 14, 39, 40, 41 | fvmptd2 7023 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑤 ∈ Word 𝐴) ∧ ¬ 𝑤 = ∅) → ((𝑣 ∈ Word 𝐴 ↦ if(𝑣 = ∅, 1, 0))‘𝑤) = 0) |
43 | 42 | oveq1d 7445 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑤 ∈ Word 𝐴) ∧ ¬ 𝑤 = ∅) → (((𝑣 ∈ Word 𝐴 ↦ if(𝑣 = ∅, 1, 0))‘𝑤) · (𝑀 Σg 𝑤)) = (0 · (𝑀 Σg 𝑤))) |
44 | 3 | ringmgp 20256 |
. . . . . . . . . . . 12
⊢ (𝑅 ∈ Ring → 𝑀 ∈ Mnd) |
45 | 1, 44 | syl 17 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝑀 ∈ Mnd) |
46 | | sswrd 14556 |
. . . . . . . . . . . . 13
⊢ (𝐴 ⊆ 𝐵 → Word 𝐴 ⊆ Word 𝐵) |
47 | 7, 46 | syl 17 |
. . . . . . . . . . . 12
⊢ (𝜑 → Word 𝐴 ⊆ Word 𝐵) |
48 | 47 | sselda 3994 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑤 ∈ Word 𝐴) → 𝑤 ∈ Word 𝐵) |
49 | 3, 2 | mgpbas 20157 |
. . . . . . . . . . . 12
⊢ 𝐵 = (Base‘𝑀) |
50 | 49 | gsumwcl 18864 |
. . . . . . . . . . 11
⊢ ((𝑀 ∈ Mnd ∧ 𝑤 ∈ Word 𝐵) → (𝑀 Σg 𝑤) ∈ 𝐵) |
51 | 45, 48, 50 | syl2an2r 685 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑤 ∈ Word 𝐴) → (𝑀 Σg 𝑤) ∈ 𝐵) |
52 | | eqid 2734 |
. . . . . . . . . . 11
⊢
(0g‘𝑅) = (0g‘𝑅) |
53 | 2, 52, 4 | mulg0 19104 |
. . . . . . . . . 10
⊢ ((𝑀 Σg
𝑤) ∈ 𝐵 → (0 · (𝑀 Σg 𝑤)) = (0g‘𝑅)) |
54 | 51, 53 | syl 17 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑤 ∈ Word 𝐴) → (0 · (𝑀 Σg 𝑤)) = (0g‘𝑅)) |
55 | 54 | adantr 480 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑤 ∈ Word 𝐴) ∧ ¬ 𝑤 = ∅) → (0 · (𝑀 Σg 𝑤)) = (0g‘𝑅)) |
56 | 43, 55 | eqtrd 2774 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑤 ∈ Word 𝐴) ∧ ¬ 𝑤 = ∅) → (((𝑣 ∈ Word 𝐴 ↦ if(𝑣 = ∅, 1, 0))‘𝑤) · (𝑀 Σg 𝑤)) = (0g‘𝑅)) |
57 | 10, 11, 34, 56 | ifbothda 4568 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑤 ∈ Word 𝐴) → (((𝑣 ∈ Word 𝐴 ↦ if(𝑣 = ∅, 1, 0))‘𝑤) · (𝑀 Σg 𝑤)) = if(𝑤 = ∅, (1r‘𝑅), (0g‘𝑅))) |
58 | 57 | mpteq2dva 5247 |
. . . . 5
⊢ (𝜑 → (𝑤 ∈ Word 𝐴 ↦ (((𝑣 ∈ Word 𝐴 ↦ if(𝑣 = ∅, 1, 0))‘𝑤) · (𝑀 Σg 𝑤))) = (𝑤 ∈ Word 𝐴 ↦ if(𝑤 = ∅, (1r‘𝑅), (0g‘𝑅)))) |
59 | 58 | oveq2d 7446 |
. . . 4
⊢ (𝜑 → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ (((𝑣 ∈ Word 𝐴 ↦ if(𝑣 = ∅, 1, 0))‘𝑤) · (𝑀 Σg 𝑤)))) = (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ if(𝑤 = ∅, (1r‘𝑅), (0g‘𝑅))))) |
60 | 1 | ringcmnd 20297 |
. . . . . 6
⊢ (𝜑 → 𝑅 ∈ CMnd) |
61 | 60 | cmnmndd 19836 |
. . . . 5
⊢ (𝜑 → 𝑅 ∈ Mnd) |
62 | 2 | fvexi 6920 |
. . . . . . . 8
⊢ 𝐵 ∈ V |
63 | 62 | a1i 11 |
. . . . . . 7
⊢ (𝜑 → 𝐵 ∈ V) |
64 | 63, 7 | ssexd 5329 |
. . . . . 6
⊢ (𝜑 → 𝐴 ∈ V) |
65 | | wrdexg 14558 |
. . . . . 6
⊢ (𝐴 ∈ V → Word 𝐴 ∈ V) |
66 | 64, 65 | syl 17 |
. . . . 5
⊢ (𝜑 → Word 𝐴 ∈ V) |
67 | | eqid 2734 |
. . . . 5
⊢ (𝑤 ∈ Word 𝐴 ↦ if(𝑤 = ∅, (1r‘𝑅), (0g‘𝑅))) = (𝑤 ∈ Word 𝐴 ↦ if(𝑤 = ∅, (1r‘𝑅), (0g‘𝑅))) |
68 | 30, 2 | eleqtrdi 2848 |
. . . . 5
⊢ (𝜑 → (1r‘𝑅) ∈ (Base‘𝑅)) |
69 | 52, 61, 66, 18, 67, 68 | gsummptif1n0 19998 |
. . . 4
⊢ (𝜑 → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ if(𝑤 = ∅, (1r‘𝑅), (0g‘𝑅)))) =
(1r‘𝑅)) |
70 | 59, 69 | eqtrd 2774 |
. . 3
⊢ (𝜑 → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ (((𝑣 ∈ Word 𝐴 ↦ if(𝑣 = ∅, 1, 0))‘𝑤) · (𝑀 Σg 𝑤)))) =
(1r‘𝑅)) |
71 | | eqid 2734 |
. . . . 5
⊢ (𝑔 ∈ 𝐹 ↦ (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑔‘𝑤) · (𝑀 Σg 𝑤))))) = (𝑔 ∈ 𝐹 ↦ (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑔‘𝑤) · (𝑀 Σg 𝑤))))) |
72 | | fveq1 6905 |
. . . . . . . . . 10
⊢ (𝑔 = (𝑣 ∈ Word 𝐴 ↦ if(𝑣 = ∅, 1, 0)) → (𝑔‘𝑤) = ((𝑣 ∈ Word 𝐴 ↦ if(𝑣 = ∅, 1, 0))‘𝑤)) |
73 | 72 | oveq1d 7445 |
. . . . . . . . 9
⊢ (𝑔 = (𝑣 ∈ Word 𝐴 ↦ if(𝑣 = ∅, 1, 0)) → ((𝑔‘𝑤) · (𝑀 Σg 𝑤)) = (((𝑣 ∈ Word 𝐴 ↦ if(𝑣 = ∅, 1, 0))‘𝑤) · (𝑀 Σg 𝑤))) |
74 | 73 | mpteq2dv 5249 |
. . . . . . . 8
⊢ (𝑔 = (𝑣 ∈ Word 𝐴 ↦ if(𝑣 = ∅, 1, 0)) → (𝑤 ∈ Word 𝐴 ↦ ((𝑔‘𝑤) · (𝑀 Σg 𝑤))) = (𝑤 ∈ Word 𝐴 ↦ (((𝑣 ∈ Word 𝐴 ↦ if(𝑣 = ∅, 1, 0))‘𝑤) · (𝑀 Σg 𝑤)))) |
75 | 74 | oveq2d 7446 |
. . . . . . 7
⊢ (𝑔 = (𝑣 ∈ Word 𝐴 ↦ if(𝑣 = ∅, 1, 0)) → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑔‘𝑤) · (𝑀 Σg 𝑤)))) = (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ (((𝑣 ∈ Word 𝐴 ↦ if(𝑣 = ∅, 1, 0))‘𝑤) · (𝑀 Σg 𝑤))))) |
76 | 75 | eqeq2d 2745 |
. . . . . 6
⊢ (𝑔 = (𝑣 ∈ Word 𝐴 ↦ if(𝑣 = ∅, 1, 0)) → ((𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ (((𝑣 ∈ Word 𝐴 ↦ if(𝑣 = ∅, 1, 0))‘𝑤) · (𝑀 Σg 𝑤)))) = (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑔‘𝑤) · (𝑀 Σg 𝑤)))) ↔ (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ (((𝑣 ∈ Word 𝐴 ↦ if(𝑣 = ∅, 1, 0))‘𝑤) · (𝑀 Σg 𝑤)))) = (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ (((𝑣 ∈ Word 𝐴 ↦ if(𝑣 = ∅, 1, 0))‘𝑤) · (𝑀 Σg 𝑤)))))) |
77 | | breq1 5150 |
. . . . . . . 8
⊢ (𝑓 = (𝑣 ∈ Word 𝐴 ↦ if(𝑣 = ∅, 1, 0)) → (𝑓 finSupp 0 ↔ (𝑣 ∈ Word 𝐴 ↦ if(𝑣 = ∅, 1, 0)) finSupp
0)) |
78 | | zex 12619 |
. . . . . . . . . 10
⊢ ℤ
∈ V |
79 | 78 | a1i 11 |
. . . . . . . . 9
⊢ (𝜑 → ℤ ∈
V) |
80 | | 1zzd 12645 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑣 ∈ Word 𝐴) ∧ 𝑣 = ∅) → 1 ∈
ℤ) |
81 | | 0zd 12622 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑣 ∈ Word 𝐴) ∧ ¬ 𝑣 = ∅) → 0 ∈
ℤ) |
82 | 80, 81 | ifclda 4565 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑣 ∈ Word 𝐴) → if(𝑣 = ∅, 1, 0) ∈
ℤ) |
83 | 82 | fmpttd 7134 |
. . . . . . . . 9
⊢ (𝜑 → (𝑣 ∈ Word 𝐴 ↦ if(𝑣 = ∅, 1, 0)):Word 𝐴⟶ℤ) |
84 | 79, 66, 83 | elmapdd 8879 |
. . . . . . . 8
⊢ (𝜑 → (𝑣 ∈ Word 𝐴 ↦ if(𝑣 = ∅, 1, 0)) ∈ (ℤ
↑m Word 𝐴)) |
85 | 66 | mptexd 7243 |
. . . . . . . . 9
⊢ (𝜑 → (𝑣 ∈ Word 𝐴 ↦ if(𝑣 = ∅, 1, 0)) ∈ V) |
86 | 83 | ffund 6740 |
. . . . . . . . 9
⊢ (𝜑 → Fun (𝑣 ∈ Word 𝐴 ↦ if(𝑣 = ∅, 1, 0))) |
87 | | 0zd 12622 |
. . . . . . . . 9
⊢ (𝜑 → 0 ∈
ℤ) |
88 | | snfi 9081 |
. . . . . . . . . 10
⊢ {∅}
∈ Fin |
89 | 88 | a1i 11 |
. . . . . . . . 9
⊢ (𝜑 → {∅} ∈
Fin) |
90 | | eldifsni 4794 |
. . . . . . . . . . . . 13
⊢ (𝑣 ∈ (Word 𝐴 ∖ {∅}) → 𝑣 ≠ ∅) |
91 | 90 | adantl 481 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑣 ∈ (Word 𝐴 ∖ {∅})) → 𝑣 ≠ ∅) |
92 | 91 | neneqd 2942 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑣 ∈ (Word 𝐴 ∖ {∅})) → ¬ 𝑣 = ∅) |
93 | 92 | iffalsed 4541 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑣 ∈ (Word 𝐴 ∖ {∅})) → if(𝑣 = ∅, 1, 0) =
0) |
94 | 93, 66 | suppss2 8223 |
. . . . . . . . 9
⊢ (𝜑 → ((𝑣 ∈ Word 𝐴 ↦ if(𝑣 = ∅, 1, 0)) supp 0) ⊆
{∅}) |
95 | | 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) |
96 | 85, 86, 87, 89, 94, 95 | syl32anc 1377 |
. . . . . . . 8
⊢ (𝜑 → (𝑣 ∈ Word 𝐴 ↦ if(𝑣 = ∅, 1, 0)) finSupp
0) |
97 | 77, 84, 96 | elrabd 3696 |
. . . . . . 7
⊢ (𝜑 → (𝑣 ∈ Word 𝐴 ↦ if(𝑣 = ∅, 1, 0)) ∈ {𝑓 ∈ (ℤ ↑m Word
𝐴) ∣ 𝑓 finSupp 0}) |
98 | 97, 6 | eleqtrrdi 2849 |
. . . . . 6
⊢ (𝜑 → (𝑣 ∈ Word 𝐴 ↦ if(𝑣 = ∅, 1, 0)) ∈ 𝐹) |
99 | | eqidd 2735 |
. . . . . 6
⊢ (𝜑 → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ (((𝑣 ∈ Word 𝐴 ↦ if(𝑣 = ∅, 1, 0))‘𝑤) · (𝑀 Σg 𝑤)))) = (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ (((𝑣 ∈ Word 𝐴 ↦ if(𝑣 = ∅, 1, 0))‘𝑤) · (𝑀 Σg 𝑤))))) |
100 | 76, 98, 99 | rspcedvdw 3624 |
. . . . 5
⊢ (𝜑 → ∃𝑔 ∈ 𝐹 (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ (((𝑣 ∈ Word 𝐴 ↦ if(𝑣 = ∅, 1, 0))‘𝑤) · (𝑀 Σg 𝑤)))) = (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑔‘𝑤) · (𝑀 Σg 𝑤))))) |
101 | | ovexd 7465 |
. . . . 5
⊢ (𝜑 → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ (((𝑣 ∈ Word 𝐴 ↦ if(𝑣 = ∅, 1, 0))‘𝑤) · (𝑀 Σg 𝑤)))) ∈ V) |
102 | 71, 100, 101 | elrnmptd 5976 |
. . . 4
⊢ (𝜑 → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ (((𝑣 ∈ Word 𝐴 ↦ if(𝑣 = ∅, 1, 0))‘𝑤) · (𝑀 Σg 𝑤)))) ∈ ran (𝑔 ∈ 𝐹 ↦ (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑔‘𝑤) · (𝑀 Σg 𝑤)))))) |
103 | 102, 8 | eleqtrrdi 2849 |
. . 3
⊢ (𝜑 → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ (((𝑣 ∈ Word 𝐴 ↦ if(𝑣 = ∅, 1, 0))‘𝑤) · (𝑀 Σg 𝑤)))) ∈ 𝑆) |
104 | 70, 103 | eqeltrrd 2839 |
. 2
⊢ (𝜑 → (1r‘𝑅) ∈ 𝑆) |
105 | | simpllr 776 |
. . . . . . . 8
⊢
(((((((𝜑 ∧ 𝑥 ∈ 𝑆) ∧ 𝑦 ∈ 𝑆) ∧ 𝑔 ∈ 𝐹) ∧ 𝑥 = (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑔‘𝑤) · (𝑀 Σg 𝑤))))) ∧ 𝑖 ∈ 𝐹) ∧ 𝑦 = (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑖‘𝑤) · (𝑀 Σg 𝑤))))) → 𝑥 = (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑔‘𝑤) · (𝑀 Σg 𝑤))))) |
106 | | simpr 484 |
. . . . . . . 8
⊢
(((((((𝜑 ∧ 𝑥 ∈ 𝑆) ∧ 𝑦 ∈ 𝑆) ∧ 𝑔 ∈ 𝐹) ∧ 𝑥 = (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑔‘𝑤) · (𝑀 Σg 𝑤))))) ∧ 𝑖 ∈ 𝐹) ∧ 𝑦 = (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑖‘𝑤) · (𝑀 Σg 𝑤))))) → 𝑦 = (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑖‘𝑤) · (𝑀 Σg 𝑤))))) |
107 | 105, 106 | oveq12d 7448 |
. . . . . . 7
⊢
(((((((𝜑 ∧ 𝑥 ∈ 𝑆) ∧ 𝑦 ∈ 𝑆) ∧ 𝑔 ∈ 𝐹) ∧ 𝑥 = (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑔‘𝑤) · (𝑀 Σg 𝑤))))) ∧ 𝑖 ∈ 𝐹) ∧ 𝑦 = (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑖‘𝑤) · (𝑀 Σg 𝑤))))) → (𝑥(.r‘𝑅)𝑦) = ((𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑔‘𝑤) · (𝑀 Σg 𝑤))))(.r‘𝑅)(𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑖‘𝑤) · (𝑀 Σg 𝑤)))))) |
108 | | eqid 2734 |
. . . . . . . . . . . . . 14
⊢
(.r‘𝑅) = (.r‘𝑅) |
109 | 66 | ad2antrr 726 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) → Word 𝐴 ∈ V) |
110 | 1 | ad2antrr 726 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) → 𝑅 ∈ Ring) |
111 | 1 | ringgrpd 20259 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → 𝑅 ∈ Grp) |
112 | 111 | ad2antrr 726 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑤 ∈ Word 𝐴) → 𝑅 ∈ Grp) |
113 | 6 | ssrab3 4091 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ 𝐹 ⊆ (ℤ
↑m Word 𝐴) |
114 | 113 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝜑 → 𝐹 ⊆ (ℤ ↑m Word
𝐴)) |
115 | 114 | sselda 3994 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝜑 ∧ 𝑔 ∈ 𝐹) → 𝑔 ∈ (ℤ ↑m Word
𝐴)) |
116 | 79, 66 | elmapd 8878 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝜑 → (𝑔 ∈ (ℤ ↑m Word
𝐴) ↔ 𝑔:Word 𝐴⟶ℤ)) |
117 | 116 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝜑 ∧ 𝑔 ∈ 𝐹) → (𝑔 ∈ (ℤ ↑m Word
𝐴) ↔ 𝑔:Word 𝐴⟶ℤ)) |
118 | 115, 117 | mpbid 232 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ 𝑔 ∈ 𝐹) → 𝑔:Word 𝐴⟶ℤ) |
119 | 118 | ffvelcdmda 7103 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑤 ∈ Word 𝐴) → (𝑔‘𝑤) ∈ ℤ) |
120 | 51 | adantlr 715 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑤 ∈ Word 𝐴) → (𝑀 Σg 𝑤) ∈ 𝐵) |
121 | 2, 4, 112, 119, 120 | mulgcld 19126 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑤 ∈ Word 𝐴) → ((𝑔‘𝑤) · (𝑀 Σg 𝑤)) ∈ 𝐵) |
122 | 121 | adantlr 715 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑤 ∈ Word 𝐴) → ((𝑔‘𝑤) · (𝑀 Σg 𝑤)) ∈ 𝐵) |
123 | 122 | ralrimiva 3143 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) → ∀𝑤 ∈ Word 𝐴((𝑔‘𝑤) · (𝑀 Σg 𝑤)) ∈ 𝐵) |
124 | | fveq2 6906 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑢 = 𝑤 → (𝑔‘𝑢) = (𝑔‘𝑤)) |
125 | | oveq2 7438 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑢 = 𝑤 → (𝑀 Σg 𝑢) = (𝑀 Σg 𝑤)) |
126 | 124, 125 | oveq12d 7448 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑢 = 𝑤 → ((𝑔‘𝑢) · (𝑀 Σg 𝑢)) = ((𝑔‘𝑤) · (𝑀 Σg 𝑤))) |
127 | 126 | eleq1d 2823 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑢 = 𝑤 → (((𝑔‘𝑢) · (𝑀 Σg 𝑢)) ∈ 𝐵 ↔ ((𝑔‘𝑤) · (𝑀 Σg 𝑤)) ∈ 𝐵)) |
128 | 127 | cbvralvw 3234 |
. . . . . . . . . . . . . . . 16
⊢
(∀𝑢 ∈
Word 𝐴((𝑔‘𝑢) · (𝑀 Σg 𝑢)) ∈ 𝐵 ↔ ∀𝑤 ∈ Word 𝐴((𝑔‘𝑤) · (𝑀 Σg 𝑤)) ∈ 𝐵) |
129 | 123, 128 | sylibr 234 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) → ∀𝑢 ∈ Word 𝐴((𝑔‘𝑢) · (𝑀 Σg 𝑢)) ∈ 𝐵) |
130 | 129 | r19.21bi 3248 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑢 ∈ Word 𝐴) → ((𝑔‘𝑢) · (𝑀 Σg 𝑢)) ∈ 𝐵) |
131 | 111 | ad2antrr 726 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝑖 ∈ 𝐹) ∧ 𝑤 ∈ Word 𝐴) → 𝑅 ∈ Grp) |
132 | | breq1 5150 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑓 = 𝑖 → (𝑓 finSupp 0 ↔ 𝑖 finSupp 0)) |
133 | 132, 6 | elrab2 3697 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑖 ∈ 𝐹 ↔ (𝑖 ∈ (ℤ ↑m Word
𝐴) ∧ 𝑖 finSupp 0)) |
134 | 133 | simplbi 497 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑖 ∈ 𝐹 → 𝑖 ∈ (ℤ ↑m Word
𝐴)) |
135 | 134 | adantl 481 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝜑 ∧ 𝑖 ∈ 𝐹) → 𝑖 ∈ (ℤ ↑m Word
𝐴)) |
136 | 79, 66 | elmapd 8878 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝜑 → (𝑖 ∈ (ℤ ↑m Word
𝐴) ↔ 𝑖:Word 𝐴⟶ℤ)) |
137 | 136 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝜑 ∧ 𝑖 ∈ 𝐹) → (𝑖 ∈ (ℤ ↑m Word
𝐴) ↔ 𝑖:Word 𝐴⟶ℤ)) |
138 | 135, 137 | mpbid 232 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ 𝑖 ∈ 𝐹) → 𝑖:Word 𝐴⟶ℤ) |
139 | 138 | ffvelcdmda 7103 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝑖 ∈ 𝐹) ∧ 𝑤 ∈ Word 𝐴) → (𝑖‘𝑤) ∈ ℤ) |
140 | 51 | adantlr 715 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝑖 ∈ 𝐹) ∧ 𝑤 ∈ Word 𝐴) → (𝑀 Σg 𝑤) ∈ 𝐵) |
141 | 2, 4, 131, 139, 140 | mulgcld 19126 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑖 ∈ 𝐹) ∧ 𝑤 ∈ Word 𝐴) → ((𝑖‘𝑤) · (𝑀 Σg 𝑤)) ∈ 𝐵) |
142 | 141 | adantllr 719 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑤 ∈ Word 𝐴) → ((𝑖‘𝑤) · (𝑀 Σg 𝑤)) ∈ 𝐵) |
143 | 142 | ralrimiva 3143 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) → ∀𝑤 ∈ Word 𝐴((𝑖‘𝑤) · (𝑀 Σg 𝑤)) ∈ 𝐵) |
144 | | fveq2 6906 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑣 = 𝑤 → (𝑖‘𝑣) = (𝑖‘𝑤)) |
145 | | oveq2 7438 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑣 = 𝑤 → (𝑀 Σg 𝑣) = (𝑀 Σg 𝑤)) |
146 | 144, 145 | oveq12d 7448 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑣 = 𝑤 → ((𝑖‘𝑣) · (𝑀 Σg 𝑣)) = ((𝑖‘𝑤) · (𝑀 Σg 𝑤))) |
147 | 146 | eleq1d 2823 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑣 = 𝑤 → (((𝑖‘𝑣) · (𝑀 Σg 𝑣)) ∈ 𝐵 ↔ ((𝑖‘𝑤) · (𝑀 Σg 𝑤)) ∈ 𝐵)) |
148 | 147 | cbvralvw 3234 |
. . . . . . . . . . . . . . . 16
⊢
(∀𝑣 ∈
Word 𝐴((𝑖‘𝑣) · (𝑀 Σg 𝑣)) ∈ 𝐵 ↔ ∀𝑤 ∈ Word 𝐴((𝑖‘𝑤) · (𝑀 Σg 𝑤)) ∈ 𝐵) |
149 | 143, 148 | sylibr 234 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) → ∀𝑣 ∈ Word 𝐴((𝑖‘𝑣) · (𝑀 Σg 𝑣)) ∈ 𝐵) |
150 | 149 | r19.21bi 3248 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑣 ∈ Word 𝐴) → ((𝑖‘𝑣) · (𝑀 Σg 𝑣)) ∈ 𝐵) |
151 | 126 | cbvmptv 5260 |
. . . . . . . . . . . . . . 15
⊢ (𝑢 ∈ Word 𝐴 ↦ ((𝑔‘𝑢) · (𝑀 Σg 𝑢))) = (𝑤 ∈ Word 𝐴 ↦ ((𝑔‘𝑤) · (𝑀 Σg 𝑤))) |
152 | | fvexd 6921 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑔 ∈ 𝐹) → (0g‘𝑅) ∈ V) |
153 | | 0zd 12622 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑔 ∈ 𝐹) → 0 ∈ ℤ) |
154 | 66 | adantr 480 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑔 ∈ 𝐹) → Word 𝐴 ∈ V) |
155 | | ssidd 4018 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑔 ∈ 𝐹) → Word 𝐴 ⊆ Word 𝐴) |
156 | | breq1 5150 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑓 = 𝑔 → (𝑓 finSupp 0 ↔ 𝑔 finSupp 0)) |
157 | 156, 6 | elrab2 3697 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑔 ∈ 𝐹 ↔ (𝑔 ∈ (ℤ ↑m Word
𝐴) ∧ 𝑔 finSupp 0)) |
158 | 157 | simprbi 496 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑔 ∈ 𝐹 → 𝑔 finSupp 0) |
159 | 158 | adantl 481 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑔 ∈ 𝐹) → 𝑔 finSupp 0) |
160 | 2, 52, 4 | mulg0 19104 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑦 ∈ 𝐵 → (0 · 𝑦) = (0g‘𝑅)) |
161 | 160 | adantl 481 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑦 ∈ 𝐵) → (0 · 𝑦) = (0g‘𝑅)) |
162 | 152, 153,
154, 155, 120, 118, 159, 161 | fisuppov1 32697 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑔 ∈ 𝐹) → (𝑤 ∈ Word 𝐴 ↦ ((𝑔‘𝑤) · (𝑀 Σg 𝑤))) finSupp
(0g‘𝑅)) |
163 | 162 | adantr 480 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) → (𝑤 ∈ Word 𝐴 ↦ ((𝑔‘𝑤) · (𝑀 Σg 𝑤))) finSupp
(0g‘𝑅)) |
164 | 151, 163 | eqbrtrid 5182 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) → (𝑢 ∈ Word 𝐴 ↦ ((𝑔‘𝑢) · (𝑀 Σg 𝑢))) finSupp
(0g‘𝑅)) |
165 | 146 | cbvmptv 5260 |
. . . . . . . . . . . . . . 15
⊢ (𝑣 ∈ Word 𝐴 ↦ ((𝑖‘𝑣) · (𝑀 Σg 𝑣))) = (𝑤 ∈ Word 𝐴 ↦ ((𝑖‘𝑤) · (𝑀 Σg 𝑤))) |
166 | 162 | ralrimiva 3143 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → ∀𝑔 ∈ 𝐹 (𝑤 ∈ Word 𝐴 ↦ ((𝑔‘𝑤) · (𝑀 Σg 𝑤))) finSupp
(0g‘𝑅)) |
167 | | fveq1 6905 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑔 = 𝑖 → (𝑔‘𝑤) = (𝑖‘𝑤)) |
168 | 167 | oveq1d 7445 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑔 = 𝑖 → ((𝑔‘𝑤) · (𝑀 Σg 𝑤)) = ((𝑖‘𝑤) · (𝑀 Σg 𝑤))) |
169 | 168 | mpteq2dv 5249 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑔 = 𝑖 → (𝑤 ∈ Word 𝐴 ↦ ((𝑔‘𝑤) · (𝑀 Σg 𝑤))) = (𝑤 ∈ Word 𝐴 ↦ ((𝑖‘𝑤) · (𝑀 Σg 𝑤)))) |
170 | 169 | breq1d 5157 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑔 = 𝑖 → ((𝑤 ∈ Word 𝐴 ↦ ((𝑔‘𝑤) · (𝑀 Σg 𝑤))) finSupp
(0g‘𝑅)
↔ (𝑤 ∈ Word 𝐴 ↦ ((𝑖‘𝑤) · (𝑀 Σg 𝑤))) finSupp
(0g‘𝑅))) |
171 | 170 | cbvralvw 3234 |
. . . . . . . . . . . . . . . . . 18
⊢
(∀𝑔 ∈
𝐹 (𝑤 ∈ Word 𝐴 ↦ ((𝑔‘𝑤) · (𝑀 Σg 𝑤))) finSupp
(0g‘𝑅)
↔ ∀𝑖 ∈
𝐹 (𝑤 ∈ Word 𝐴 ↦ ((𝑖‘𝑤) · (𝑀 Σg 𝑤))) finSupp
(0g‘𝑅)) |
172 | 166, 171 | sylib 218 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → ∀𝑖 ∈ 𝐹 (𝑤 ∈ Word 𝐴 ↦ ((𝑖‘𝑤) · (𝑀 Σg 𝑤))) finSupp
(0g‘𝑅)) |
173 | 172 | r19.21bi 3248 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑖 ∈ 𝐹) → (𝑤 ∈ Word 𝐴 ↦ ((𝑖‘𝑤) · (𝑀 Σg 𝑤))) finSupp
(0g‘𝑅)) |
174 | 173 | adantlr 715 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) → (𝑤 ∈ Word 𝐴 ↦ ((𝑖‘𝑤) · (𝑀 Σg 𝑤))) finSupp
(0g‘𝑅)) |
175 | 165, 174 | eqbrtrid 5182 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) → (𝑣 ∈ Word 𝐴 ↦ ((𝑖‘𝑣) · (𝑀 Σg 𝑣))) finSupp
(0g‘𝑅)) |
176 | 2, 108, 52, 109, 109, 110, 130, 150, 164, 175 | gsumdixp 20332 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) → ((𝑅 Σg (𝑢 ∈ Word 𝐴 ↦ ((𝑔‘𝑢) · (𝑀 Σg 𝑢))))(.r‘𝑅)(𝑅 Σg (𝑣 ∈ Word 𝐴 ↦ ((𝑖‘𝑣) · (𝑀 Σg 𝑣))))) = (𝑅 Σg (𝑢 ∈ Word 𝐴, 𝑣 ∈ Word 𝐴 ↦ (((𝑔‘𝑢) · (𝑀 Σg 𝑢))(.r‘𝑅)((𝑖‘𝑣) · (𝑀 Σg 𝑣)))))) |
177 | 151 | oveq2i 7441 |
. . . . . . . . . . . . . . 15
⊢ (𝑅 Σg
(𝑢 ∈ Word 𝐴 ↦ ((𝑔‘𝑢) · (𝑀 Σg 𝑢)))) = (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑔‘𝑤) · (𝑀 Σg 𝑤)))) |
178 | 165 | oveq2i 7441 |
. . . . . . . . . . . . . . 15
⊢ (𝑅 Σg
(𝑣 ∈ Word 𝐴 ↦ ((𝑖‘𝑣) · (𝑀 Σg 𝑣)))) = (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑖‘𝑤) · (𝑀 Σg 𝑤)))) |
179 | 177, 178 | oveq12i 7442 |
. . . . . . . . . . . . . 14
⊢ ((𝑅 Σg
(𝑢 ∈ Word 𝐴 ↦ ((𝑔‘𝑢) · (𝑀 Σg 𝑢))))(.r‘𝑅)(𝑅 Σg (𝑣 ∈ Word 𝐴 ↦ ((𝑖‘𝑣) · (𝑀 Σg 𝑣))))) = ((𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑔‘𝑤) · (𝑀 Σg 𝑤))))(.r‘𝑅)(𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑖‘𝑤) · (𝑀 Σg 𝑤))))) |
180 | 179 | a1i 11 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) → ((𝑅 Σg (𝑢 ∈ Word 𝐴 ↦ ((𝑔‘𝑢) · (𝑀 Σg 𝑢))))(.r‘𝑅)(𝑅 Σg (𝑣 ∈ Word 𝐴 ↦ ((𝑖‘𝑣) · (𝑀 Σg 𝑣))))) = ((𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑔‘𝑤) · (𝑀 Σg 𝑤))))(.r‘𝑅)(𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑖‘𝑤) · (𝑀 Σg 𝑤)))))) |
181 | 110 | ad2antrr 726 |
. . . . . . . . . . . . . . . . . . 19
⊢
(((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑤 ∈ Word 𝐴) ∧ 𝑓 ∈ Word 𝐴) → 𝑅 ∈ Ring) |
182 | 122 | adantr 480 |
. . . . . . . . . . . . . . . . . . 19
⊢
(((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑤 ∈ Word 𝐴) ∧ 𝑓 ∈ Word 𝐴) → ((𝑔‘𝑤) · (𝑀 Σg 𝑤)) ∈ 𝐵) |
183 | 111 | ad4antr 732 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑤 ∈ Word 𝐴) ∧ 𝑓 ∈ Word 𝐴) → 𝑅 ∈ Grp) |
184 | 138 | adantlr 715 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) → 𝑖:Word 𝐴⟶ℤ) |
185 | 184 | ffvelcdmda 7103 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑓 ∈ Word 𝐴) → (𝑖‘𝑓) ∈ ℤ) |
186 | 185 | adantlr 715 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑤 ∈ Word 𝐴) ∧ 𝑓 ∈ Word 𝐴) → (𝑖‘𝑓) ∈ ℤ) |
187 | 45 | ad4antr 732 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
(((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑤 ∈ Word 𝐴) ∧ 𝑓 ∈ Word 𝐴) → 𝑀 ∈ Mnd) |
188 | 47 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝜑 ∧ 𝑔 ∈ 𝐹) → Word 𝐴 ⊆ Word 𝐵) |
189 | 188 | ad2antrr 726 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑤 ∈ Word 𝐴) → Word 𝐴 ⊆ Word 𝐵) |
190 | 189 | sselda 3994 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
(((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑤 ∈ Word 𝐴) ∧ 𝑓 ∈ Word 𝐴) → 𝑓 ∈ Word 𝐵) |
191 | 49 | gsumwcl 18864 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑀 ∈ Mnd ∧ 𝑓 ∈ Word 𝐵) → (𝑀 Σg 𝑓) ∈ 𝐵) |
192 | 187, 190,
191 | syl2anc 584 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑤 ∈ Word 𝐴) ∧ 𝑓 ∈ Word 𝐴) → (𝑀 Σg 𝑓) ∈ 𝐵) |
193 | 2, 4, 183, 186, 192 | mulgcld 19126 |
. . . . . . . . . . . . . . . . . . 19
⊢
(((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑤 ∈ Word 𝐴) ∧ 𝑓 ∈ Word 𝐴) → ((𝑖‘𝑓) · (𝑀 Σg 𝑓)) ∈ 𝐵) |
194 | 2, 108, 181, 182, 193 | ringcld 20276 |
. . . . . . . . . . . . . . . . . 18
⊢
(((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑤 ∈ Word 𝐴) ∧ 𝑓 ∈ Word 𝐴) → (((𝑔‘𝑤) · (𝑀 Σg 𝑤))(.r‘𝑅)((𝑖‘𝑓) · (𝑀 Σg 𝑓))) ∈ 𝐵) |
195 | 194 | anasss 466 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ (𝑤 ∈ Word 𝐴 ∧ 𝑓 ∈ Word 𝐴)) → (((𝑔‘𝑤) · (𝑀 Σg 𝑤))(.r‘𝑅)((𝑖‘𝑓) · (𝑀 Σg 𝑓))) ∈ 𝐵) |
196 | 195 | ralrimivva 3199 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) → ∀𝑤 ∈ Word 𝐴∀𝑓 ∈ Word 𝐴(((𝑔‘𝑤) · (𝑀 Σg 𝑤))(.r‘𝑅)((𝑖‘𝑓) · (𝑀 Σg 𝑓))) ∈ 𝐵) |
197 | | eqid 2734 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑤 ∈ Word 𝐴, 𝑓 ∈ Word 𝐴 ↦ (((𝑔‘𝑤) · (𝑀 Σg 𝑤))(.r‘𝑅)((𝑖‘𝑓) · (𝑀 Σg 𝑓)))) = (𝑤 ∈ Word 𝐴, 𝑓 ∈ Word 𝐴 ↦ (((𝑔‘𝑤) · (𝑀 Σg 𝑤))(.r‘𝑅)((𝑖‘𝑓) · (𝑀 Σg 𝑓)))) |
198 | 197 | fmpo 8091 |
. . . . . . . . . . . . . . . 16
⊢
(∀𝑤 ∈
Word 𝐴∀𝑓 ∈ Word 𝐴(((𝑔‘𝑤) · (𝑀 Σg 𝑤))(.r‘𝑅)((𝑖‘𝑓) · (𝑀 Σg 𝑓))) ∈ 𝐵 ↔ (𝑤 ∈ Word 𝐴, 𝑓 ∈ Word 𝐴 ↦ (((𝑔‘𝑤) · (𝑀 Σg 𝑤))(.r‘𝑅)((𝑖‘𝑓) · (𝑀 Σg 𝑓)))):(Word 𝐴 × Word 𝐴)⟶𝐵) |
199 | 196, 198 | sylib 218 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) → (𝑤 ∈ Word 𝐴, 𝑓 ∈ Word 𝐴 ↦ (((𝑔‘𝑤) · (𝑀 Σg 𝑤))(.r‘𝑅)((𝑖‘𝑓) · (𝑀 Σg 𝑓)))):(Word 𝐴 × Word 𝐴)⟶𝐵) |
200 | | vex 3481 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ 𝑤 ∈ V |
201 | | vex 3481 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ 𝑓 ∈ V |
202 | 200, 201 | op1std 8022 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑎 = 〈𝑤, 𝑓〉 → (1st ‘𝑎) = 𝑤) |
203 | 202 | fveq2d 6910 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑎 = 〈𝑤, 𝑓〉 → (𝑔‘(1st ‘𝑎)) = (𝑔‘𝑤)) |
204 | 202 | oveq2d 7446 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑎 = 〈𝑤, 𝑓〉 → (𝑀 Σg (1st
‘𝑎)) = (𝑀 Σg
𝑤)) |
205 | 203, 204 | oveq12d 7448 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑎 = 〈𝑤, 𝑓〉 → ((𝑔‘(1st ‘𝑎)) · (𝑀 Σg (1st
‘𝑎))) = ((𝑔‘𝑤) · (𝑀 Σg 𝑤))) |
206 | 200, 201 | op2ndd 8023 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑎 = 〈𝑤, 𝑓〉 → (2nd ‘𝑎) = 𝑓) |
207 | 206 | fveq2d 6910 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑎 = 〈𝑤, 𝑓〉 → (𝑖‘(2nd ‘𝑎)) = (𝑖‘𝑓)) |
208 | 206 | oveq2d 7446 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑎 = 〈𝑤, 𝑓〉 → (𝑀 Σg (2nd
‘𝑎)) = (𝑀 Σg
𝑓)) |
209 | 207, 208 | oveq12d 7448 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑎 = 〈𝑤, 𝑓〉 → ((𝑖‘(2nd ‘𝑎)) · (𝑀 Σg (2nd
‘𝑎))) = ((𝑖‘𝑓) · (𝑀 Σg 𝑓))) |
210 | 205, 209 | oveq12d 7448 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑎 = 〈𝑤, 𝑓〉 → (((𝑔‘(1st ‘𝑎)) · (𝑀 Σg (1st
‘𝑎)))(.r‘𝑅)((𝑖‘(2nd ‘𝑎)) · (𝑀 Σg (2nd
‘𝑎)))) = (((𝑔‘𝑤) · (𝑀 Σg 𝑤))(.r‘𝑅)((𝑖‘𝑓) · (𝑀 Σg 𝑓)))) |
211 | 210 | mpompt 7546 |
. . . . . . . . . . . . . . . 16
⊢ (𝑎 ∈ (Word 𝐴 × Word 𝐴) ↦ (((𝑔‘(1st ‘𝑎)) · (𝑀 Σg (1st
‘𝑎)))(.r‘𝑅)((𝑖‘(2nd ‘𝑎)) · (𝑀 Σg (2nd
‘𝑎))))) = (𝑤 ∈ Word 𝐴, 𝑓 ∈ Word 𝐴 ↦ (((𝑔‘𝑤) · (𝑀 Σg 𝑤))(.r‘𝑅)((𝑖‘𝑓) · (𝑀 Σg 𝑓)))) |
212 | 66, 66 | xpexd 7769 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → (Word 𝐴 × Word 𝐴) ∈ V) |
213 | 212 | ad2antrr 726 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) → (Word 𝐴 × Word 𝐴) ∈ V) |
214 | 213 | mptexd 7243 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) → (𝑎 ∈ (Word 𝐴 × Word 𝐴) ↦ (((𝑔‘(1st ‘𝑎)) · (𝑀 Σg (1st
‘𝑎)))(.r‘𝑅)((𝑖‘(2nd ‘𝑎)) · (𝑀 Σg (2nd
‘𝑎))))) ∈
V) |
215 | | fvexd 6921 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) → (0g‘𝑅) ∈ V) |
216 | 110 | adantr 480 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑎 ∈ (Word 𝐴 × Word 𝐴)) → 𝑅 ∈ Ring) |
217 | 111 | ad3antrrr 730 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑎 ∈ (Word 𝐴 × Word 𝐴)) → 𝑅 ∈ Grp) |
218 | 118 | ad2antrr 726 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑎 ∈ (Word 𝐴 × Word 𝐴)) → 𝑔:Word 𝐴⟶ℤ) |
219 | | xp1st 8044 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑎 ∈ (Word 𝐴 × Word 𝐴) → (1st ‘𝑎) ∈ Word 𝐴) |
220 | 219 | adantl 481 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑎 ∈ (Word 𝐴 × Word 𝐴)) → (1st ‘𝑎) ∈ Word 𝐴) |
221 | 218, 220 | ffvelcdmd 7104 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑎 ∈ (Word 𝐴 × Word 𝐴)) → (𝑔‘(1st ‘𝑎)) ∈
ℤ) |
222 | 216, 44 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑎 ∈ (Word 𝐴 × Word 𝐴)) → 𝑀 ∈ Mnd) |
223 | 188 | ad2antrr 726 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑎 ∈ (Word 𝐴 × Word 𝐴)) → Word 𝐴 ⊆ Word 𝐵) |
224 | 223, 220 | sseldd 3995 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑎 ∈ (Word 𝐴 × Word 𝐴)) → (1st ‘𝑎) ∈ Word 𝐵) |
225 | 49 | gsumwcl 18864 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑀 ∈ Mnd ∧
(1st ‘𝑎)
∈ Word 𝐵) →
(𝑀
Σg (1st ‘𝑎)) ∈ 𝐵) |
226 | 222, 224,
225 | syl2anc 584 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑎 ∈ (Word 𝐴 × Word 𝐴)) → (𝑀 Σg (1st
‘𝑎)) ∈ 𝐵) |
227 | 2, 4, 217, 221, 226 | mulgcld 19126 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑎 ∈ (Word 𝐴 × Word 𝐴)) → ((𝑔‘(1st ‘𝑎)) · (𝑀 Σg (1st
‘𝑎))) ∈ 𝐵) |
228 | 184 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑎 ∈ (Word 𝐴 × Word 𝐴)) → 𝑖:Word 𝐴⟶ℤ) |
229 | | xp2nd 8045 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑎 ∈ (Word 𝐴 × Word 𝐴) → (2nd ‘𝑎) ∈ Word 𝐴) |
230 | 229 | adantl 481 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑎 ∈ (Word 𝐴 × Word 𝐴)) → (2nd ‘𝑎) ∈ Word 𝐴) |
231 | 228, 230 | ffvelcdmd 7104 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑎 ∈ (Word 𝐴 × Word 𝐴)) → (𝑖‘(2nd ‘𝑎)) ∈
ℤ) |
232 | 223, 230 | sseldd 3995 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑎 ∈ (Word 𝐴 × Word 𝐴)) → (2nd ‘𝑎) ∈ Word 𝐵) |
233 | 49 | gsumwcl 18864 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑀 ∈ Mnd ∧
(2nd ‘𝑎)
∈ Word 𝐵) →
(𝑀
Σg (2nd ‘𝑎)) ∈ 𝐵) |
234 | 222, 232,
233 | syl2anc 584 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑎 ∈ (Word 𝐴 × Word 𝐴)) → (𝑀 Σg (2nd
‘𝑎)) ∈ 𝐵) |
235 | 2, 4, 217, 231, 234 | mulgcld 19126 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑎 ∈ (Word 𝐴 × Word 𝐴)) → ((𝑖‘(2nd ‘𝑎)) · (𝑀 Σg (2nd
‘𝑎))) ∈ 𝐵) |
236 | 2, 108, 216, 227, 235 | ringcld 20276 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑎 ∈ (Word 𝐴 × Word 𝐴)) → (((𝑔‘(1st ‘𝑎)) · (𝑀 Σg (1st
‘𝑎)))(.r‘𝑅)((𝑖‘(2nd ‘𝑎)) · (𝑀 Σg (2nd
‘𝑎)))) ∈ 𝐵) |
237 | 236 | fmpttd 7134 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) → (𝑎 ∈ (Word 𝐴 × Word 𝐴) ↦ (((𝑔‘(1st ‘𝑎)) · (𝑀 Σg (1st
‘𝑎)))(.r‘𝑅)((𝑖‘(2nd ‘𝑎)) · (𝑀 Σg (2nd
‘𝑎))))):(Word 𝐴 × Word 𝐴)⟶𝐵) |
238 | 237 | ffund 6740 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) → Fun (𝑎 ∈ (Word 𝐴 × Word 𝐴) ↦ (((𝑔‘(1st ‘𝑎)) · (𝑀 Σg (1st
‘𝑎)))(.r‘𝑅)((𝑖‘(2nd ‘𝑎)) · (𝑀 Σg (2nd
‘𝑎)))))) |
239 | 159 | fsuppimpd 9406 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑔 ∈ 𝐹) → (𝑔 supp 0) ∈ Fin) |
240 | 133 | simprbi 496 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑖 ∈ 𝐹 → 𝑖 finSupp 0) |
241 | 240 | adantl 481 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) → 𝑖 finSupp 0) |
242 | 241 | fsuppimpd 9406 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) → (𝑖 supp 0) ∈ Fin) |
243 | | xpfi 9355 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝑔 supp 0) ∈ Fin ∧ (𝑖 supp 0) ∈ Fin) →
((𝑔 supp 0) × (𝑖 supp 0)) ∈
Fin) |
244 | 239, 242,
243 | syl2an2r 685 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) → ((𝑔 supp 0) × (𝑖 supp 0)) ∈ Fin) |
245 | 118 | ffnd 6737 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝜑 ∧ 𝑔 ∈ 𝐹) → 𝑔 Fn Word 𝐴) |
246 | 245 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) → 𝑔 Fn Word 𝐴) |
247 | 246 | ad2antrr 726 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢
(((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑎 ∈ ((Word 𝐴 × Word 𝐴) ∖ ((𝑔 supp 0) × (𝑖 supp 0)))) ∧ 𝑎 ∈ ((Word 𝐴 ∖ (𝑔 supp 0)) × Word 𝐴)) → 𝑔 Fn Word 𝐴) |
248 | 109 | ad2antrr 726 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢
(((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑎 ∈ ((Word 𝐴 × Word 𝐴) ∖ ((𝑔 supp 0) × (𝑖 supp 0)))) ∧ 𝑎 ∈ ((Word 𝐴 ∖ (𝑔 supp 0)) × Word 𝐴)) → Word 𝐴 ∈ V) |
249 | | 0zd 12622 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢
(((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑎 ∈ ((Word 𝐴 × Word 𝐴) ∖ ((𝑔 supp 0) × (𝑖 supp 0)))) ∧ 𝑎 ∈ ((Word 𝐴 ∖ (𝑔 supp 0)) × Word 𝐴)) → 0 ∈ ℤ) |
250 | | xp1st 8044 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑎 ∈ ((Word 𝐴 ∖ (𝑔 supp 0)) × Word 𝐴) → (1st ‘𝑎) ∈ (Word 𝐴 ∖ (𝑔 supp 0))) |
251 | 250 | adantl 481 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢
(((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑎 ∈ ((Word 𝐴 × Word 𝐴) ∖ ((𝑔 supp 0) × (𝑖 supp 0)))) ∧ 𝑎 ∈ ((Word 𝐴 ∖ (𝑔 supp 0)) × Word 𝐴)) → (1st ‘𝑎) ∈ (Word 𝐴 ∖ (𝑔 supp 0))) |
252 | 247, 248,
249, 251 | fvdifsupp 8194 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
(((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑎 ∈ ((Word 𝐴 × Word 𝐴) ∖ ((𝑔 supp 0) × (𝑖 supp 0)))) ∧ 𝑎 ∈ ((Word 𝐴 ∖ (𝑔 supp 0)) × Word 𝐴)) → (𝑔‘(1st ‘𝑎)) = 0) |
253 | 252 | oveq1d 7445 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
(((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑎 ∈ ((Word 𝐴 × Word 𝐴) ∖ ((𝑔 supp 0) × (𝑖 supp 0)))) ∧ 𝑎 ∈ ((Word 𝐴 ∖ (𝑔 supp 0)) × Word 𝐴)) → ((𝑔‘(1st ‘𝑎)) · (𝑀 Σg (1st
‘𝑎))) = (0 · (𝑀 Σg
(1st ‘𝑎)))) |
254 | 45 | ad4antr 732 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢
(((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑎 ∈ ((Word 𝐴 × Word 𝐴) ∖ ((𝑔 supp 0) × (𝑖 supp 0)))) ∧ 𝑎 ∈ ((Word 𝐴 ∖ (𝑔 supp 0)) × Word 𝐴)) → 𝑀 ∈ Mnd) |
255 | 188 | ad3antrrr 730 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢
(((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑎 ∈ ((Word 𝐴 × Word 𝐴) ∖ ((𝑔 supp 0) × (𝑖 supp 0)))) ∧ 𝑎 ∈ ((Word 𝐴 ∖ (𝑔 supp 0)) × Word 𝐴)) → Word 𝐴 ⊆ Word 𝐵) |
256 | 251 | eldifad 3974 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢
(((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑎 ∈ ((Word 𝐴 × Word 𝐴) ∖ ((𝑔 supp 0) × (𝑖 supp 0)))) ∧ 𝑎 ∈ ((Word 𝐴 ∖ (𝑔 supp 0)) × Word 𝐴)) → (1st ‘𝑎) ∈ Word 𝐴) |
257 | 255, 256 | sseldd 3995 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢
(((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑎 ∈ ((Word 𝐴 × Word 𝐴) ∖ ((𝑔 supp 0) × (𝑖 supp 0)))) ∧ 𝑎 ∈ ((Word 𝐴 ∖ (𝑔 supp 0)) × Word 𝐴)) → (1st ‘𝑎) ∈ Word 𝐵) |
258 | 254, 257,
225 | syl2anc 584 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
(((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑎 ∈ ((Word 𝐴 × Word 𝐴) ∖ ((𝑔 supp 0) × (𝑖 supp 0)))) ∧ 𝑎 ∈ ((Word 𝐴 ∖ (𝑔 supp 0)) × Word 𝐴)) → (𝑀 Σg (1st
‘𝑎)) ∈ 𝐵) |
259 | 2, 52, 4 | mulg0 19104 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝑀 Σg
(1st ‘𝑎))
∈ 𝐵 → (0 · (𝑀 Σg
(1st ‘𝑎)))
= (0g‘𝑅)) |
260 | 258, 259 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
(((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑎 ∈ ((Word 𝐴 × Word 𝐴) ∖ ((𝑔 supp 0) × (𝑖 supp 0)))) ∧ 𝑎 ∈ ((Word 𝐴 ∖ (𝑔 supp 0)) × Word 𝐴)) → (0 · (𝑀 Σg (1st
‘𝑎))) =
(0g‘𝑅)) |
261 | 253, 260 | eqtrd 2774 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
(((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑎 ∈ ((Word 𝐴 × Word 𝐴) ∖ ((𝑔 supp 0) × (𝑖 supp 0)))) ∧ 𝑎 ∈ ((Word 𝐴 ∖ (𝑔 supp 0)) × Word 𝐴)) → ((𝑔‘(1st ‘𝑎)) · (𝑀 Σg (1st
‘𝑎))) =
(0g‘𝑅)) |
262 | 261 | oveq1d 7445 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
(((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑎 ∈ ((Word 𝐴 × Word 𝐴) ∖ ((𝑔 supp 0) × (𝑖 supp 0)))) ∧ 𝑎 ∈ ((Word 𝐴 ∖ (𝑔 supp 0)) × Word 𝐴)) → (((𝑔‘(1st ‘𝑎)) · (𝑀 Σg (1st
‘𝑎)))(.r‘𝑅)((𝑖‘(2nd ‘𝑎)) · (𝑀 Σg (2nd
‘𝑎)))) =
((0g‘𝑅)(.r‘𝑅)((𝑖‘(2nd ‘𝑎)) · (𝑀 Σg (2nd
‘𝑎))))) |
263 | 110 | ad2antrr 726 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
(((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑎 ∈ ((Word 𝐴 × Word 𝐴) ∖ ((𝑔 supp 0) × (𝑖 supp 0)))) ∧ 𝑎 ∈ ((Word 𝐴 ∖ (𝑔 supp 0)) × Word 𝐴)) → 𝑅 ∈ Ring) |
264 | 111 | ad4antr 732 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
(((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑎 ∈ ((Word 𝐴 × Word 𝐴) ∖ ((𝑔 supp 0) × (𝑖 supp 0)))) ∧ 𝑎 ∈ ((Word 𝐴 ∖ (𝑔 supp 0)) × Word 𝐴)) → 𝑅 ∈ Grp) |
265 | 184 | ad2antrr 726 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
(((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑎 ∈ ((Word 𝐴 × Word 𝐴) ∖ ((𝑔 supp 0) × (𝑖 supp 0)))) ∧ 𝑎 ∈ ((Word 𝐴 ∖ (𝑔 supp 0)) × Word 𝐴)) → 𝑖:Word 𝐴⟶ℤ) |
266 | | xp2nd 8045 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑎 ∈ ((Word 𝐴 ∖ (𝑔 supp 0)) × Word 𝐴) → (2nd ‘𝑎) ∈ Word 𝐴) |
267 | 266 | adantl 481 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
(((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑎 ∈ ((Word 𝐴 × Word 𝐴) ∖ ((𝑔 supp 0) × (𝑖 supp 0)))) ∧ 𝑎 ∈ ((Word 𝐴 ∖ (𝑔 supp 0)) × Word 𝐴)) → (2nd ‘𝑎) ∈ Word 𝐴) |
268 | 265, 267 | ffvelcdmd 7104 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
(((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑎 ∈ ((Word 𝐴 × Word 𝐴) ∖ ((𝑔 supp 0) × (𝑖 supp 0)))) ∧ 𝑎 ∈ ((Word 𝐴 ∖ (𝑔 supp 0)) × Word 𝐴)) → (𝑖‘(2nd ‘𝑎)) ∈
ℤ) |
269 | 255, 267 | sseldd 3995 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
(((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑎 ∈ ((Word 𝐴 × Word 𝐴) ∖ ((𝑔 supp 0) × (𝑖 supp 0)))) ∧ 𝑎 ∈ ((Word 𝐴 ∖ (𝑔 supp 0)) × Word 𝐴)) → (2nd ‘𝑎) ∈ Word 𝐵) |
270 | 254, 269,
233 | syl2anc 584 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
(((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑎 ∈ ((Word 𝐴 × Word 𝐴) ∖ ((𝑔 supp 0) × (𝑖 supp 0)))) ∧ 𝑎 ∈ ((Word 𝐴 ∖ (𝑔 supp 0)) × Word 𝐴)) → (𝑀 Σg (2nd
‘𝑎)) ∈ 𝐵) |
271 | 2, 4, 264, 268, 270 | mulgcld 19126 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
(((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑎 ∈ ((Word 𝐴 × Word 𝐴) ∖ ((𝑔 supp 0) × (𝑖 supp 0)))) ∧ 𝑎 ∈ ((Word 𝐴 ∖ (𝑔 supp 0)) × Word 𝐴)) → ((𝑖‘(2nd ‘𝑎)) · (𝑀 Σg (2nd
‘𝑎))) ∈ 𝐵) |
272 | 2, 108, 52, 263, 271 | ringlzd 20308 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
(((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑎 ∈ ((Word 𝐴 × Word 𝐴) ∖ ((𝑔 supp 0) × (𝑖 supp 0)))) ∧ 𝑎 ∈ ((Word 𝐴 ∖ (𝑔 supp 0)) × Word 𝐴)) → ((0g‘𝑅)(.r‘𝑅)((𝑖‘(2nd ‘𝑎)) · (𝑀 Σg (2nd
‘𝑎)))) =
(0g‘𝑅)) |
273 | 262, 272 | eqtrd 2774 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑎 ∈ ((Word 𝐴 × Word 𝐴) ∖ ((𝑔 supp 0) × (𝑖 supp 0)))) ∧ 𝑎 ∈ ((Word 𝐴 ∖ (𝑔 supp 0)) × Word 𝐴)) → (((𝑔‘(1st ‘𝑎)) · (𝑀 Σg (1st
‘𝑎)))(.r‘𝑅)((𝑖‘(2nd ‘𝑎)) · (𝑀 Σg (2nd
‘𝑎)))) =
(0g‘𝑅)) |
274 | 138 | ffnd 6737 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝜑 ∧ 𝑖 ∈ 𝐹) → 𝑖 Fn Word 𝐴) |
275 | 274 | adantlr 715 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) → 𝑖 Fn Word 𝐴) |
276 | 275 | ad2antrr 726 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢
(((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑎 ∈ ((Word 𝐴 × Word 𝐴) ∖ ((𝑔 supp 0) × (𝑖 supp 0)))) ∧ 𝑎 ∈ (Word 𝐴 × (Word 𝐴 ∖ (𝑖 supp 0)))) → 𝑖 Fn Word 𝐴) |
277 | 109 | ad2antrr 726 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢
(((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑎 ∈ ((Word 𝐴 × Word 𝐴) ∖ ((𝑔 supp 0) × (𝑖 supp 0)))) ∧ 𝑎 ∈ (Word 𝐴 × (Word 𝐴 ∖ (𝑖 supp 0)))) → Word 𝐴 ∈ V) |
278 | | 0zd 12622 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢
(((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑎 ∈ ((Word 𝐴 × Word 𝐴) ∖ ((𝑔 supp 0) × (𝑖 supp 0)))) ∧ 𝑎 ∈ (Word 𝐴 × (Word 𝐴 ∖ (𝑖 supp 0)))) → 0 ∈
ℤ) |
279 | | xp2nd 8045 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑎 ∈ (Word 𝐴 × (Word 𝐴 ∖ (𝑖 supp 0))) → (2nd
‘𝑎) ∈ (Word
𝐴 ∖ (𝑖 supp 0))) |
280 | 279 | adantl 481 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢
(((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑎 ∈ ((Word 𝐴 × Word 𝐴) ∖ ((𝑔 supp 0) × (𝑖 supp 0)))) ∧ 𝑎 ∈ (Word 𝐴 × (Word 𝐴 ∖ (𝑖 supp 0)))) → (2nd
‘𝑎) ∈ (Word
𝐴 ∖ (𝑖 supp 0))) |
281 | 276, 277,
278, 280 | fvdifsupp 8194 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
(((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑎 ∈ ((Word 𝐴 × Word 𝐴) ∖ ((𝑔 supp 0) × (𝑖 supp 0)))) ∧ 𝑎 ∈ (Word 𝐴 × (Word 𝐴 ∖ (𝑖 supp 0)))) → (𝑖‘(2nd ‘𝑎)) = 0) |
282 | 281 | oveq1d 7445 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
(((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑎 ∈ ((Word 𝐴 × Word 𝐴) ∖ ((𝑔 supp 0) × (𝑖 supp 0)))) ∧ 𝑎 ∈ (Word 𝐴 × (Word 𝐴 ∖ (𝑖 supp 0)))) → ((𝑖‘(2nd ‘𝑎)) · (𝑀 Σg (2nd
‘𝑎))) = (0 · (𝑀 Σg
(2nd ‘𝑎)))) |
283 | 45 | ad4antr 732 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢
(((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑎 ∈ ((Word 𝐴 × Word 𝐴) ∖ ((𝑔 supp 0) × (𝑖 supp 0)))) ∧ 𝑎 ∈ (Word 𝐴 × (Word 𝐴 ∖ (𝑖 supp 0)))) → 𝑀 ∈ Mnd) |
284 | 188 | ad3antrrr 730 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢
(((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑎 ∈ ((Word 𝐴 × Word 𝐴) ∖ ((𝑔 supp 0) × (𝑖 supp 0)))) ∧ 𝑎 ∈ (Word 𝐴 × (Word 𝐴 ∖ (𝑖 supp 0)))) → Word 𝐴 ⊆ Word 𝐵) |
285 | 280 | eldifad 3974 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢
(((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑎 ∈ ((Word 𝐴 × Word 𝐴) ∖ ((𝑔 supp 0) × (𝑖 supp 0)))) ∧ 𝑎 ∈ (Word 𝐴 × (Word 𝐴 ∖ (𝑖 supp 0)))) → (2nd
‘𝑎) ∈ Word 𝐴) |
286 | 284, 285 | sseldd 3995 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢
(((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑎 ∈ ((Word 𝐴 × Word 𝐴) ∖ ((𝑔 supp 0) × (𝑖 supp 0)))) ∧ 𝑎 ∈ (Word 𝐴 × (Word 𝐴 ∖ (𝑖 supp 0)))) → (2nd
‘𝑎) ∈ Word 𝐵) |
287 | 283, 286,
233 | syl2anc 584 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
(((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑎 ∈ ((Word 𝐴 × Word 𝐴) ∖ ((𝑔 supp 0) × (𝑖 supp 0)))) ∧ 𝑎 ∈ (Word 𝐴 × (Word 𝐴 ∖ (𝑖 supp 0)))) → (𝑀 Σg (2nd
‘𝑎)) ∈ 𝐵) |
288 | 2, 52, 4 | mulg0 19104 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝑀 Σg
(2nd ‘𝑎))
∈ 𝐵 → (0 · (𝑀 Σg
(2nd ‘𝑎)))
= (0g‘𝑅)) |
289 | 287, 288 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
(((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑎 ∈ ((Word 𝐴 × Word 𝐴) ∖ ((𝑔 supp 0) × (𝑖 supp 0)))) ∧ 𝑎 ∈ (Word 𝐴 × (Word 𝐴 ∖ (𝑖 supp 0)))) → (0 · (𝑀 Σg (2nd
‘𝑎))) =
(0g‘𝑅)) |
290 | 282, 289 | eqtrd 2774 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
(((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑎 ∈ ((Word 𝐴 × Word 𝐴) ∖ ((𝑔 supp 0) × (𝑖 supp 0)))) ∧ 𝑎 ∈ (Word 𝐴 × (Word 𝐴 ∖ (𝑖 supp 0)))) → ((𝑖‘(2nd ‘𝑎)) · (𝑀 Σg (2nd
‘𝑎))) =
(0g‘𝑅)) |
291 | 290 | oveq2d 7446 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
(((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑎 ∈ ((Word 𝐴 × Word 𝐴) ∖ ((𝑔 supp 0) × (𝑖 supp 0)))) ∧ 𝑎 ∈ (Word 𝐴 × (Word 𝐴 ∖ (𝑖 supp 0)))) → (((𝑔‘(1st ‘𝑎)) · (𝑀 Σg (1st
‘𝑎)))(.r‘𝑅)((𝑖‘(2nd ‘𝑎)) · (𝑀 Σg (2nd
‘𝑎)))) = (((𝑔‘(1st
‘𝑎)) · (𝑀 Σg
(1st ‘𝑎)))(.r‘𝑅)(0g‘𝑅))) |
292 | 110 | ad2antrr 726 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
(((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑎 ∈ ((Word 𝐴 × Word 𝐴) ∖ ((𝑔 supp 0) × (𝑖 supp 0)))) ∧ 𝑎 ∈ (Word 𝐴 × (Word 𝐴 ∖ (𝑖 supp 0)))) → 𝑅 ∈ Ring) |
293 | 111 | ad4antr 732 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
(((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑎 ∈ ((Word 𝐴 × Word 𝐴) ∖ ((𝑔 supp 0) × (𝑖 supp 0)))) ∧ 𝑎 ∈ (Word 𝐴 × (Word 𝐴 ∖ (𝑖 supp 0)))) → 𝑅 ∈ Grp) |
294 | 118 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) → 𝑔:Word 𝐴⟶ℤ) |
295 | 294 | ad2antrr 726 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
(((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑎 ∈ ((Word 𝐴 × Word 𝐴) ∖ ((𝑔 supp 0) × (𝑖 supp 0)))) ∧ 𝑎 ∈ (Word 𝐴 × (Word 𝐴 ∖ (𝑖 supp 0)))) → 𝑔:Word 𝐴⟶ℤ) |
296 | | xp1st 8044 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑎 ∈ (Word 𝐴 × (Word 𝐴 ∖ (𝑖 supp 0))) → (1st
‘𝑎) ∈ Word 𝐴) |
297 | 296 | adantl 481 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
(((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑎 ∈ ((Word 𝐴 × Word 𝐴) ∖ ((𝑔 supp 0) × (𝑖 supp 0)))) ∧ 𝑎 ∈ (Word 𝐴 × (Word 𝐴 ∖ (𝑖 supp 0)))) → (1st
‘𝑎) ∈ Word 𝐴) |
298 | 295, 297 | ffvelcdmd 7104 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
(((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑎 ∈ ((Word 𝐴 × Word 𝐴) ∖ ((𝑔 supp 0) × (𝑖 supp 0)))) ∧ 𝑎 ∈ (Word 𝐴 × (Word 𝐴 ∖ (𝑖 supp 0)))) → (𝑔‘(1st ‘𝑎)) ∈
ℤ) |
299 | 284, 297 | sseldd 3995 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
(((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑎 ∈ ((Word 𝐴 × Word 𝐴) ∖ ((𝑔 supp 0) × (𝑖 supp 0)))) ∧ 𝑎 ∈ (Word 𝐴 × (Word 𝐴 ∖ (𝑖 supp 0)))) → (1st
‘𝑎) ∈ Word 𝐵) |
300 | 283, 299,
225 | syl2anc 584 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
(((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑎 ∈ ((Word 𝐴 × Word 𝐴) ∖ ((𝑔 supp 0) × (𝑖 supp 0)))) ∧ 𝑎 ∈ (Word 𝐴 × (Word 𝐴 ∖ (𝑖 supp 0)))) → (𝑀 Σg (1st
‘𝑎)) ∈ 𝐵) |
301 | 2, 4, 293, 298, 300 | mulgcld 19126 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
(((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑎 ∈ ((Word 𝐴 × Word 𝐴) ∖ ((𝑔 supp 0) × (𝑖 supp 0)))) ∧ 𝑎 ∈ (Word 𝐴 × (Word 𝐴 ∖ (𝑖 supp 0)))) → ((𝑔‘(1st ‘𝑎)) · (𝑀 Σg (1st
‘𝑎))) ∈ 𝐵) |
302 | 2, 108, 52, 292, 301 | ringrzd 20309 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
(((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑎 ∈ ((Word 𝐴 × Word 𝐴) ∖ ((𝑔 supp 0) × (𝑖 supp 0)))) ∧ 𝑎 ∈ (Word 𝐴 × (Word 𝐴 ∖ (𝑖 supp 0)))) → (((𝑔‘(1st ‘𝑎)) · (𝑀 Σg (1st
‘𝑎)))(.r‘𝑅)(0g‘𝑅)) = (0g‘𝑅)) |
303 | 291, 302 | eqtrd 2774 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑎 ∈ ((Word 𝐴 × Word 𝐴) ∖ ((𝑔 supp 0) × (𝑖 supp 0)))) ∧ 𝑎 ∈ (Word 𝐴 × (Word 𝐴 ∖ (𝑖 supp 0)))) → (((𝑔‘(1st ‘𝑎)) · (𝑀 Σg (1st
‘𝑎)))(.r‘𝑅)((𝑖‘(2nd ‘𝑎)) · (𝑀 Σg (2nd
‘𝑎)))) =
(0g‘𝑅)) |
304 | | simpr 484 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑎 ∈ ((Word 𝐴 × Word 𝐴) ∖ ((𝑔 supp 0) × (𝑖 supp 0)))) → 𝑎 ∈ ((Word 𝐴 × Word 𝐴) ∖ ((𝑔 supp 0) × (𝑖 supp 0)))) |
305 | | difxp 6185 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((Word
𝐴 × Word 𝐴) ∖ ((𝑔 supp 0) × (𝑖 supp 0))) = (((Word 𝐴 ∖ (𝑔 supp 0)) × Word 𝐴) ∪ (Word 𝐴 × (Word 𝐴 ∖ (𝑖 supp 0)))) |
306 | 304, 305 | eleqtrdi 2848 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑎 ∈ ((Word 𝐴 × Word 𝐴) ∖ ((𝑔 supp 0) × (𝑖 supp 0)))) → 𝑎 ∈ (((Word 𝐴 ∖ (𝑔 supp 0)) × Word 𝐴) ∪ (Word 𝐴 × (Word 𝐴 ∖ (𝑖 supp 0))))) |
307 | | elun 4162 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑎 ∈ (((Word 𝐴 ∖ (𝑔 supp 0)) × Word 𝐴) ∪ (Word 𝐴 × (Word 𝐴 ∖ (𝑖 supp 0)))) ↔ (𝑎 ∈ ((Word 𝐴 ∖ (𝑔 supp 0)) × Word 𝐴) ∨ 𝑎 ∈ (Word 𝐴 × (Word 𝐴 ∖ (𝑖 supp 0))))) |
308 | 306, 307 | sylib 218 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑎 ∈ ((Word 𝐴 × Word 𝐴) ∖ ((𝑔 supp 0) × (𝑖 supp 0)))) → (𝑎 ∈ ((Word 𝐴 ∖ (𝑔 supp 0)) × Word 𝐴) ∨ 𝑎 ∈ (Word 𝐴 × (Word 𝐴 ∖ (𝑖 supp 0))))) |
309 | 273, 303,
308 | mpjaodan 960 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑎 ∈ ((Word 𝐴 × Word 𝐴) ∖ ((𝑔 supp 0) × (𝑖 supp 0)))) → (((𝑔‘(1st ‘𝑎)) · (𝑀 Σg (1st
‘𝑎)))(.r‘𝑅)((𝑖‘(2nd ‘𝑎)) · (𝑀 Σg (2nd
‘𝑎)))) =
(0g‘𝑅)) |
310 | 309, 213 | suppss2 8223 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) → ((𝑎 ∈ (Word 𝐴 × Word 𝐴) ↦ (((𝑔‘(1st ‘𝑎)) · (𝑀 Σg (1st
‘𝑎)))(.r‘𝑅)((𝑖‘(2nd ‘𝑎)) · (𝑀 Σg (2nd
‘𝑎))))) supp
(0g‘𝑅))
⊆ ((𝑔 supp 0) ×
(𝑖 supp
0))) |
311 | 244, 310 | ssfid 9298 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) → ((𝑎 ∈ (Word 𝐴 × Word 𝐴) ↦ (((𝑔‘(1st ‘𝑎)) · (𝑀 Σg (1st
‘𝑎)))(.r‘𝑅)((𝑖‘(2nd ‘𝑎)) · (𝑀 Σg (2nd
‘𝑎))))) supp
(0g‘𝑅))
∈ Fin) |
312 | 214, 215,
238, 311 | isfsuppd 9403 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) → (𝑎 ∈ (Word 𝐴 × Word 𝐴) ↦ (((𝑔‘(1st ‘𝑎)) · (𝑀 Σg (1st
‘𝑎)))(.r‘𝑅)((𝑖‘(2nd ‘𝑎)) · (𝑀 Σg (2nd
‘𝑎))))) finSupp
(0g‘𝑅)) |
313 | 211, 312 | eqbrtrrid 5183 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) → (𝑤 ∈ Word 𝐴, 𝑓 ∈ Word 𝐴 ↦ (((𝑔‘𝑤) · (𝑀 Σg 𝑤))(.r‘𝑅)((𝑖‘𝑓) · (𝑀 Σg 𝑓)))) finSupp
(0g‘𝑅)) |
314 | 60 | ad2antrr 726 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) → 𝑅 ∈ CMnd) |
315 | 7 | ad2antrr 726 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) → 𝐴 ⊆ 𝐵) |
316 | 2, 52, 199, 313, 314, 315 | gsumwrd2dccat 33052 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) → (𝑅 Σg (𝑤 ∈ Word 𝐴, 𝑓 ∈ Word 𝐴 ↦ (((𝑔‘𝑤) · (𝑀 Σg 𝑤))(.r‘𝑅)((𝑖‘𝑓) · (𝑀 Σg 𝑓))))) = (𝑅 Σg (𝑣 ∈ Word 𝐴 ↦ (𝑅 Σg (𝑗 ∈
(0...(♯‘𝑣))
↦ ((𝑤 ∈ Word
𝐴, 𝑓 ∈ Word 𝐴 ↦ (((𝑔‘𝑤) · (𝑀 Σg 𝑤))(.r‘𝑅)((𝑖‘𝑓) · (𝑀 Σg 𝑓))))‘〈(𝑣 prefix 𝑗), (𝑣 substr 〈𝑗, (♯‘𝑣)〉)〉)))))) |
317 | 126 | oveq1d 7445 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑢 = 𝑤 → (((𝑔‘𝑢) · (𝑀 Σg 𝑢))(.r‘𝑅)((𝑖‘𝑣) · (𝑀 Σg 𝑣))) = (((𝑔‘𝑤) · (𝑀 Σg 𝑤))(.r‘𝑅)((𝑖‘𝑣) · (𝑀 Σg 𝑣)))) |
318 | | fveq2 6906 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑣 = 𝑓 → (𝑖‘𝑣) = (𝑖‘𝑓)) |
319 | | oveq2 7438 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑣 = 𝑓 → (𝑀 Σg 𝑣) = (𝑀 Σg 𝑓)) |
320 | 318, 319 | oveq12d 7448 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑣 = 𝑓 → ((𝑖‘𝑣) · (𝑀 Σg 𝑣)) = ((𝑖‘𝑓) · (𝑀 Σg 𝑓))) |
321 | 320 | oveq2d 7446 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑣 = 𝑓 → (((𝑔‘𝑤) · (𝑀 Σg 𝑤))(.r‘𝑅)((𝑖‘𝑣) · (𝑀 Σg 𝑣))) = (((𝑔‘𝑤) · (𝑀 Σg 𝑤))(.r‘𝑅)((𝑖‘𝑓) · (𝑀 Σg 𝑓)))) |
322 | 317, 321 | cbvmpov 7527 |
. . . . . . . . . . . . . . . 16
⊢ (𝑢 ∈ Word 𝐴, 𝑣 ∈ Word 𝐴 ↦ (((𝑔‘𝑢) · (𝑀 Σg 𝑢))(.r‘𝑅)((𝑖‘𝑣) · (𝑀 Σg 𝑣)))) = (𝑤 ∈ Word 𝐴, 𝑓 ∈ Word 𝐴 ↦ (((𝑔‘𝑤) · (𝑀 Σg 𝑤))(.r‘𝑅)((𝑖‘𝑓) · (𝑀 Σg 𝑓)))) |
323 | 322 | oveq2i 7441 |
. . . . . . . . . . . . . . 15
⊢ (𝑅 Σg
(𝑢 ∈ Word 𝐴, 𝑣 ∈ Word 𝐴 ↦ (((𝑔‘𝑢) · (𝑀 Σg 𝑢))(.r‘𝑅)((𝑖‘𝑣) · (𝑀 Σg 𝑣))))) = (𝑅 Σg (𝑤 ∈ Word 𝐴, 𝑓 ∈ Word 𝐴 ↦ (((𝑔‘𝑤) · (𝑀 Σg 𝑤))(.r‘𝑅)((𝑖‘𝑓) · (𝑀 Σg 𝑓))))) |
324 | 323 | a1i 11 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) → (𝑅 Σg (𝑢 ∈ Word 𝐴, 𝑣 ∈ Word 𝐴 ↦ (((𝑔‘𝑢) · (𝑀 Σg 𝑢))(.r‘𝑅)((𝑖‘𝑣) · (𝑀 Σg 𝑣))))) = (𝑅 Σg (𝑤 ∈ Word 𝐴, 𝑓 ∈ Word 𝐴 ↦ (((𝑔‘𝑤) · (𝑀 Σg 𝑤))(.r‘𝑅)((𝑖‘𝑓) · (𝑀 Σg 𝑓)))))) |
325 | | pfxcctswrd 14744 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑣 ∈ Word 𝐴 ∧ 𝑗 ∈ (0...(♯‘𝑣))) → ((𝑣 prefix 𝑗) ++ (𝑣 substr 〈𝑗, (♯‘𝑣)〉)) = 𝑣) |
326 | 325 | adantll 714 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
(((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑣 ∈ Word 𝐴) ∧ 𝑗 ∈ (0...(♯‘𝑣))) → ((𝑣 prefix 𝑗) ++ (𝑣 substr 〈𝑗, (♯‘𝑣)〉)) = 𝑣) |
327 | 326 | oveq2d 7446 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑣 ∈ Word 𝐴) ∧ 𝑗 ∈ (0...(♯‘𝑣))) → (𝑀 Σg ((𝑣 prefix 𝑗) ++ (𝑣 substr 〈𝑗, (♯‘𝑣)〉))) = (𝑀 Σg 𝑣)) |
328 | 327 | oveq2d 7446 |
. . . . . . . . . . . . . . . . . . 19
⊢
(((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑣 ∈ Word 𝐴) ∧ 𝑗 ∈ (0...(♯‘𝑣))) → (((𝑔‘(𝑣 prefix 𝑗)) · (𝑖‘(𝑣 substr 〈𝑗, (♯‘𝑣)〉))) · (𝑀 Σg ((𝑣 prefix 𝑗) ++ (𝑣 substr 〈𝑗, (♯‘𝑣)〉)))) = (((𝑔‘(𝑣 prefix 𝑗)) · (𝑖‘(𝑣 substr 〈𝑗, (♯‘𝑣)〉))) · (𝑀 Σg 𝑣))) |
329 | 328 | mpteq2dva 5247 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑣 ∈ Word 𝐴) → (𝑗 ∈ (0...(♯‘𝑣)) ↦ (((𝑔‘(𝑣 prefix 𝑗)) · (𝑖‘(𝑣 substr 〈𝑗, (♯‘𝑣)〉))) · (𝑀 Σg ((𝑣 prefix 𝑗) ++ (𝑣 substr 〈𝑗, (♯‘𝑣)〉))))) = (𝑗 ∈ (0...(♯‘𝑣)) ↦ (((𝑔‘(𝑣 prefix 𝑗)) · (𝑖‘(𝑣 substr 〈𝑗, (♯‘𝑣)〉))) · (𝑀 Σg 𝑣)))) |
330 | 329 | oveq2d 7446 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑣 ∈ Word 𝐴) → (𝑅 Σg (𝑗 ∈
(0...(♯‘𝑣))
↦ (((𝑔‘(𝑣 prefix 𝑗)) · (𝑖‘(𝑣 substr 〈𝑗, (♯‘𝑣)〉))) · (𝑀 Σg ((𝑣 prefix 𝑗) ++ (𝑣 substr 〈𝑗, (♯‘𝑣)〉)))))) = (𝑅 Σg (𝑗 ∈
(0...(♯‘𝑣))
↦ (((𝑔‘(𝑣 prefix 𝑗)) · (𝑖‘(𝑣 substr 〈𝑗, (♯‘𝑣)〉))) · (𝑀 Σg 𝑣))))) |
331 | | df-ov 7433 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑣 prefix 𝑗)(𝑤 ∈ Word 𝐴, 𝑓 ∈ Word 𝐴 ↦ (((𝑔‘𝑤) · (𝑀 Σg 𝑤))(.r‘𝑅)((𝑖‘𝑓) · (𝑀 Σg 𝑓))))(𝑣 substr 〈𝑗, (♯‘𝑣)〉)) = ((𝑤 ∈ Word 𝐴, 𝑓 ∈ Word 𝐴 ↦ (((𝑔‘𝑤) · (𝑀 Σg 𝑤))(.r‘𝑅)((𝑖‘𝑓) · (𝑀 Σg 𝑓))))‘〈(𝑣 prefix 𝑗), (𝑣 substr 〈𝑗, (♯‘𝑣)〉)〉) |
332 | 188 | sselda 3994 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ (((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑤 ∈ Word 𝐴) → 𝑤 ∈ Word 𝐵) |
333 | 332 | ad4ant13 751 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢
(((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑤 ∈ Word 𝐴) ∧ 𝑓 ∈ Word 𝐴) → 𝑤 ∈ Word 𝐵) |
334 | 187, 333,
50 | syl2anc 584 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢
(((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑤 ∈ Word 𝐴) ∧ 𝑓 ∈ Word 𝐴) → (𝑀 Σg 𝑤) ∈ 𝐵) |
335 | 2, 4, 108 | mulgass3 20369 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ ((𝑅 ∈ Ring ∧ ((𝑖‘𝑓) ∈ ℤ ∧ (𝑀 Σg 𝑤) ∈ 𝐵 ∧ (𝑀 Σg 𝑓) ∈ 𝐵)) → ((𝑀 Σg 𝑤)(.r‘𝑅)((𝑖‘𝑓) · (𝑀 Σg 𝑓))) = ((𝑖‘𝑓) · ((𝑀 Σg 𝑤)(.r‘𝑅)(𝑀 Σg 𝑓)))) |
336 | 181, 186,
334, 192, 335 | syl13anc 1371 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢
(((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑤 ∈ Word 𝐴) ∧ 𝑓 ∈ Word 𝐴) → ((𝑀 Σg 𝑤)(.r‘𝑅)((𝑖‘𝑓) · (𝑀 Σg 𝑓))) = ((𝑖‘𝑓) · ((𝑀 Σg 𝑤)(.r‘𝑅)(𝑀 Σg 𝑓)))) |
337 | 336 | oveq2d 7446 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢
(((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑤 ∈ Word 𝐴) ∧ 𝑓 ∈ Word 𝐴) → ((𝑔‘𝑤) · ((𝑀 Σg 𝑤)(.r‘𝑅)((𝑖‘𝑓) · (𝑀 Σg 𝑓)))) = ((𝑔‘𝑤) · ((𝑖‘𝑓) · ((𝑀 Σg 𝑤)(.r‘𝑅)(𝑀 Σg 𝑓))))) |
338 | 119 | ad4ant13 751 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢
(((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑤 ∈ Word 𝐴) ∧ 𝑓 ∈ Word 𝐴) → (𝑔‘𝑤) ∈ ℤ) |
339 | 2, 4, 108 | mulgass2 20322 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((𝑅 ∈ Ring ∧ ((𝑔‘𝑤) ∈ ℤ ∧ (𝑀 Σg 𝑤) ∈ 𝐵 ∧ ((𝑖‘𝑓) · (𝑀 Σg 𝑓)) ∈ 𝐵)) → (((𝑔‘𝑤) · (𝑀 Σg 𝑤))(.r‘𝑅)((𝑖‘𝑓) · (𝑀 Σg 𝑓))) = ((𝑔‘𝑤) · ((𝑀 Σg 𝑤)(.r‘𝑅)((𝑖‘𝑓) · (𝑀 Σg 𝑓))))) |
340 | 181, 338,
334, 193, 339 | syl13anc 1371 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢
(((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑤 ∈ Word 𝐴) ∧ 𝑓 ∈ Word 𝐴) → (((𝑔‘𝑤) · (𝑀 Σg 𝑤))(.r‘𝑅)((𝑖‘𝑓) · (𝑀 Σg 𝑓))) = ((𝑔‘𝑤) · ((𝑀 Σg 𝑤)(.r‘𝑅)((𝑖‘𝑓) · (𝑀 Σg 𝑓))))) |
341 | 2, 108, 181, 334, 192 | ringcld 20276 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢
(((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑤 ∈ Word 𝐴) ∧ 𝑓 ∈ Word 𝐴) → ((𝑀 Σg 𝑤)(.r‘𝑅)(𝑀 Σg 𝑓)) ∈ 𝐵) |
342 | 2, 4 | mulgass 19141 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((𝑅 ∈ Grp ∧ ((𝑔‘𝑤) ∈ ℤ ∧ (𝑖‘𝑓) ∈ ℤ ∧ ((𝑀 Σg 𝑤)(.r‘𝑅)(𝑀 Σg 𝑓)) ∈ 𝐵)) → (((𝑔‘𝑤) · (𝑖‘𝑓)) · ((𝑀 Σg 𝑤)(.r‘𝑅)(𝑀 Σg 𝑓))) = ((𝑔‘𝑤) · ((𝑖‘𝑓) · ((𝑀 Σg 𝑤)(.r‘𝑅)(𝑀 Σg 𝑓))))) |
343 | 183, 338,
186, 341, 342 | syl13anc 1371 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢
(((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑤 ∈ Word 𝐴) ∧ 𝑓 ∈ Word 𝐴) → (((𝑔‘𝑤) · (𝑖‘𝑓)) · ((𝑀 Σg 𝑤)(.r‘𝑅)(𝑀 Σg 𝑓))) = ((𝑔‘𝑤) · ((𝑖‘𝑓) · ((𝑀 Σg 𝑤)(.r‘𝑅)(𝑀 Σg 𝑓))))) |
344 | 337, 340,
343 | 3eqtr4d 2784 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢
(((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑤 ∈ Word 𝐴) ∧ 𝑓 ∈ Word 𝐴) → (((𝑔‘𝑤) · (𝑀 Σg 𝑤))(.r‘𝑅)((𝑖‘𝑓) · (𝑀 Σg 𝑓))) = (((𝑔‘𝑤) · (𝑖‘𝑓)) · ((𝑀 Σg 𝑤)(.r‘𝑅)(𝑀 Σg 𝑓)))) |
345 | 3, 108 | mgpplusg 20155 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢
(.r‘𝑅) = (+g‘𝑀) |
346 | 49, 345 | gsumccat 18866 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((𝑀 ∈ Mnd ∧ 𝑤 ∈ Word 𝐵 ∧ 𝑓 ∈ Word 𝐵) → (𝑀 Σg (𝑤 ++ 𝑓)) = ((𝑀 Σg 𝑤)(.r‘𝑅)(𝑀 Σg 𝑓))) |
347 | 187, 333,
190, 346 | syl3anc 1370 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢
(((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑤 ∈ Word 𝐴) ∧ 𝑓 ∈ Word 𝐴) → (𝑀 Σg (𝑤 ++ 𝑓)) = ((𝑀 Σg 𝑤)(.r‘𝑅)(𝑀 Σg 𝑓))) |
348 | 347 | oveq2d 7446 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢
(((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑤 ∈ Word 𝐴) ∧ 𝑓 ∈ Word 𝐴) → (((𝑔‘𝑤) · (𝑖‘𝑓)) · (𝑀 Σg (𝑤 ++ 𝑓))) = (((𝑔‘𝑤) · (𝑖‘𝑓)) · ((𝑀 Σg 𝑤)(.r‘𝑅)(𝑀 Σg 𝑓)))) |
349 | 344, 348 | eqtr4d 2777 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢
(((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑤 ∈ Word 𝐴) ∧ 𝑓 ∈ Word 𝐴) → (((𝑔‘𝑤) · (𝑀 Σg 𝑤))(.r‘𝑅)((𝑖‘𝑓) · (𝑀 Σg 𝑓))) = (((𝑔‘𝑤) · (𝑖‘𝑓)) · (𝑀 Σg (𝑤 ++ 𝑓)))) |
350 | 349 | adantllr 719 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
((((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑣 ∈ Word 𝐴) ∧ 𝑤 ∈ Word 𝐴) ∧ 𝑓 ∈ Word 𝐴) → (((𝑔‘𝑤) · (𝑀 Σg 𝑤))(.r‘𝑅)((𝑖‘𝑓) · (𝑀 Σg 𝑓))) = (((𝑔‘𝑤) · (𝑖‘𝑓)) · (𝑀 Σg (𝑤 ++ 𝑓)))) |
351 | 350 | adantllr 719 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
(((((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑣 ∈ Word 𝐴) ∧ 𝑗 ∈ (0...(♯‘𝑣))) ∧ 𝑤 ∈ Word 𝐴) ∧ 𝑓 ∈ Word 𝐴) → (((𝑔‘𝑤) · (𝑀 Σg 𝑤))(.r‘𝑅)((𝑖‘𝑓) · (𝑀 Σg 𝑓))) = (((𝑔‘𝑤) · (𝑖‘𝑓)) · (𝑀 Σg (𝑤 ++ 𝑓)))) |
352 | 351 | 3impa 1109 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
((((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑣 ∈ Word 𝐴) ∧ 𝑗 ∈ (0...(♯‘𝑣))) ∧ 𝑤 ∈ Word 𝐴 ∧ 𝑓 ∈ Word 𝐴) → (((𝑔‘𝑤) · (𝑀 Σg 𝑤))(.r‘𝑅)((𝑖‘𝑓) · (𝑀 Σg 𝑓))) = (((𝑔‘𝑤) · (𝑖‘𝑓)) · (𝑀 Σg (𝑤 ++ 𝑓)))) |
353 | 352 | mpoeq3dva 7509 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
(((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑣 ∈ Word 𝐴) ∧ 𝑗 ∈ (0...(♯‘𝑣))) → (𝑤 ∈ Word 𝐴, 𝑓 ∈ Word 𝐴 ↦ (((𝑔‘𝑤) · (𝑀 Σg 𝑤))(.r‘𝑅)((𝑖‘𝑓) · (𝑀 Σg 𝑓)))) = (𝑤 ∈ Word 𝐴, 𝑓 ∈ Word 𝐴 ↦ (((𝑔‘𝑤) · (𝑖‘𝑓)) · (𝑀 Σg (𝑤 ++ 𝑓))))) |
354 | | fveq2 6906 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑤 = (𝑣 prefix 𝑗) → (𝑔‘𝑤) = (𝑔‘(𝑣 prefix 𝑗))) |
355 | | fveq2 6906 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑓 = (𝑣 substr 〈𝑗, (♯‘𝑣)〉) → (𝑖‘𝑓) = (𝑖‘(𝑣 substr 〈𝑗, (♯‘𝑣)〉))) |
356 | 354, 355 | oveqan12d 7449 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝑤 = (𝑣 prefix 𝑗) ∧ 𝑓 = (𝑣 substr 〈𝑗, (♯‘𝑣)〉)) → ((𝑔‘𝑤) · (𝑖‘𝑓)) = ((𝑔‘(𝑣 prefix 𝑗)) · (𝑖‘(𝑣 substr 〈𝑗, (♯‘𝑣)〉)))) |
357 | | oveq12 7439 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝑤 = (𝑣 prefix 𝑗) ∧ 𝑓 = (𝑣 substr 〈𝑗, (♯‘𝑣)〉)) → (𝑤 ++ 𝑓) = ((𝑣 prefix 𝑗) ++ (𝑣 substr 〈𝑗, (♯‘𝑣)〉))) |
358 | 357 | oveq2d 7446 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝑤 = (𝑣 prefix 𝑗) ∧ 𝑓 = (𝑣 substr 〈𝑗, (♯‘𝑣)〉)) → (𝑀 Σg (𝑤 ++ 𝑓)) = (𝑀 Σg ((𝑣 prefix 𝑗) ++ (𝑣 substr 〈𝑗, (♯‘𝑣)〉)))) |
359 | 356, 358 | oveq12d 7448 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑤 = (𝑣 prefix 𝑗) ∧ 𝑓 = (𝑣 substr 〈𝑗, (♯‘𝑣)〉)) → (((𝑔‘𝑤) · (𝑖‘𝑓)) · (𝑀 Σg (𝑤 ++ 𝑓))) = (((𝑔‘(𝑣 prefix 𝑗)) · (𝑖‘(𝑣 substr 〈𝑗, (♯‘𝑣)〉))) · (𝑀 Σg ((𝑣 prefix 𝑗) ++ (𝑣 substr 〈𝑗, (♯‘𝑣)〉))))) |
360 | 359 | adantl 481 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
((((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑣 ∈ Word 𝐴) ∧ 𝑗 ∈ (0...(♯‘𝑣))) ∧ (𝑤 = (𝑣 prefix 𝑗) ∧ 𝑓 = (𝑣 substr 〈𝑗, (♯‘𝑣)〉))) → (((𝑔‘𝑤) · (𝑖‘𝑓)) · (𝑀 Σg (𝑤 ++ 𝑓))) = (((𝑔‘(𝑣 prefix 𝑗)) · (𝑖‘(𝑣 substr 〈𝑗, (♯‘𝑣)〉))) · (𝑀 Σg ((𝑣 prefix 𝑗) ++ (𝑣 substr 〈𝑗, (♯‘𝑣)〉))))) |
361 | | pfxcl 14711 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑣 ∈ Word 𝐴 → (𝑣 prefix 𝑗) ∈ Word 𝐴) |
362 | 361 | ad2antlr 727 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
(((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑣 ∈ Word 𝐴) ∧ 𝑗 ∈ (0...(♯‘𝑣))) → (𝑣 prefix 𝑗) ∈ Word 𝐴) |
363 | | swrdcl 14679 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑣 ∈ Word 𝐴 → (𝑣 substr 〈𝑗, (♯‘𝑣)〉) ∈ Word 𝐴) |
364 | 363 | ad2antlr 727 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
(((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑣 ∈ Word 𝐴) ∧ 𝑗 ∈ (0...(♯‘𝑣))) → (𝑣 substr 〈𝑗, (♯‘𝑣)〉) ∈ Word 𝐴) |
365 | | ovexd 7465 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
(((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑣 ∈ Word 𝐴) ∧ 𝑗 ∈ (0...(♯‘𝑣))) → (((𝑔‘(𝑣 prefix 𝑗)) · (𝑖‘(𝑣 substr 〈𝑗, (♯‘𝑣)〉))) · (𝑀 Σg ((𝑣 prefix 𝑗) ++ (𝑣 substr 〈𝑗, (♯‘𝑣)〉)))) ∈ V) |
366 | 353, 360,
362, 364, 365 | ovmpod 7584 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑣 ∈ Word 𝐴) ∧ 𝑗 ∈ (0...(♯‘𝑣))) → ((𝑣 prefix 𝑗)(𝑤 ∈ Word 𝐴, 𝑓 ∈ Word 𝐴 ↦ (((𝑔‘𝑤) · (𝑀 Σg 𝑤))(.r‘𝑅)((𝑖‘𝑓) · (𝑀 Σg 𝑓))))(𝑣 substr 〈𝑗, (♯‘𝑣)〉)) = (((𝑔‘(𝑣 prefix 𝑗)) · (𝑖‘(𝑣 substr 〈𝑗, (♯‘𝑣)〉))) · (𝑀 Σg ((𝑣 prefix 𝑗) ++ (𝑣 substr 〈𝑗, (♯‘𝑣)〉))))) |
367 | 331, 366 | eqtr3id 2788 |
. . . . . . . . . . . . . . . . . . 19
⊢
(((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑣 ∈ Word 𝐴) ∧ 𝑗 ∈ (0...(♯‘𝑣))) → ((𝑤 ∈ Word 𝐴, 𝑓 ∈ Word 𝐴 ↦ (((𝑔‘𝑤) · (𝑀 Σg 𝑤))(.r‘𝑅)((𝑖‘𝑓) · (𝑀 Σg 𝑓))))‘〈(𝑣 prefix 𝑗), (𝑣 substr 〈𝑗, (♯‘𝑣)〉)〉) = (((𝑔‘(𝑣 prefix 𝑗)) · (𝑖‘(𝑣 substr 〈𝑗, (♯‘𝑣)〉))) · (𝑀 Σg ((𝑣 prefix 𝑗) ++ (𝑣 substr 〈𝑗, (♯‘𝑣)〉))))) |
368 | 367 | mpteq2dva 5247 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑣 ∈ Word 𝐴) → (𝑗 ∈ (0...(♯‘𝑣)) ↦ ((𝑤 ∈ Word 𝐴, 𝑓 ∈ Word 𝐴 ↦ (((𝑔‘𝑤) · (𝑀 Σg 𝑤))(.r‘𝑅)((𝑖‘𝑓) · (𝑀 Σg 𝑓))))‘〈(𝑣 prefix 𝑗), (𝑣 substr 〈𝑗, (♯‘𝑣)〉)〉)) = (𝑗 ∈ (0...(♯‘𝑣)) ↦ (((𝑔‘(𝑣 prefix 𝑗)) · (𝑖‘(𝑣 substr 〈𝑗, (♯‘𝑣)〉))) · (𝑀 Σg ((𝑣 prefix 𝑗) ++ (𝑣 substr 〈𝑗, (♯‘𝑣)〉)))))) |
369 | 368 | oveq2d 7446 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑣 ∈ Word 𝐴) → (𝑅 Σg (𝑗 ∈
(0...(♯‘𝑣))
↦ ((𝑤 ∈ Word
𝐴, 𝑓 ∈ Word 𝐴 ↦ (((𝑔‘𝑤) · (𝑀 Σg 𝑤))(.r‘𝑅)((𝑖‘𝑓) · (𝑀 Σg 𝑓))))‘〈(𝑣 prefix 𝑗), (𝑣 substr 〈𝑗, (♯‘𝑣)〉)〉))) = (𝑅 Σg (𝑗 ∈
(0...(♯‘𝑣))
↦ (((𝑔‘(𝑣 prefix 𝑗)) · (𝑖‘(𝑣 substr 〈𝑗, (♯‘𝑣)〉))) · (𝑀 Σg ((𝑣 prefix 𝑗) ++ (𝑣 substr 〈𝑗, (♯‘𝑣)〉))))))) |
370 | | eqid 2734 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑡 ∈ Word 𝐴 ↦ Σ𝑗 ∈ (0...(♯‘𝑡))((𝑔‘(𝑡 prefix 𝑗)) · (𝑖‘(𝑡 substr 〈𝑗, (♯‘𝑡)〉)))) = (𝑡 ∈ Word 𝐴 ↦ Σ𝑗 ∈ (0...(♯‘𝑡))((𝑔‘(𝑡 prefix 𝑗)) · (𝑖‘(𝑡 substr 〈𝑗, (♯‘𝑡)〉)))) |
371 | | fveq2 6906 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑡 = 𝑣 → (♯‘𝑡) = (♯‘𝑣)) |
372 | 371 | oveq2d 7446 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑡 = 𝑣 → (0...(♯‘𝑡)) = (0...(♯‘𝑣))) |
373 | | fvoveq1 7453 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑡 = 𝑣 → (𝑔‘(𝑡 prefix 𝑗)) = (𝑔‘(𝑣 prefix 𝑗))) |
374 | | id 22 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑡 = 𝑣 → 𝑡 = 𝑣) |
375 | 371 | opeq2d 4884 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑡 = 𝑣 → 〈𝑗, (♯‘𝑡)〉 = 〈𝑗, (♯‘𝑣)〉) |
376 | 374, 375 | oveq12d 7448 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑡 = 𝑣 → (𝑡 substr 〈𝑗, (♯‘𝑡)〉) = (𝑣 substr 〈𝑗, (♯‘𝑣)〉)) |
377 | 376 | fveq2d 6910 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑡 = 𝑣 → (𝑖‘(𝑡 substr 〈𝑗, (♯‘𝑡)〉)) = (𝑖‘(𝑣 substr 〈𝑗, (♯‘𝑣)〉))) |
378 | 373, 377 | oveq12d 7448 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑡 = 𝑣 → ((𝑔‘(𝑡 prefix 𝑗)) · (𝑖‘(𝑡 substr 〈𝑗, (♯‘𝑡)〉))) = ((𝑔‘(𝑣 prefix 𝑗)) · (𝑖‘(𝑣 substr 〈𝑗, (♯‘𝑣)〉)))) |
379 | 378 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑡 = 𝑣 ∧ 𝑗 ∈ (0...(♯‘𝑡))) → ((𝑔‘(𝑡 prefix 𝑗)) · (𝑖‘(𝑡 substr 〈𝑗, (♯‘𝑡)〉))) = ((𝑔‘(𝑣 prefix 𝑗)) · (𝑖‘(𝑣 substr 〈𝑗, (♯‘𝑣)〉)))) |
380 | 372, 379 | sumeq12dv 15738 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑡 = 𝑣 → Σ𝑗 ∈ (0...(♯‘𝑡))((𝑔‘(𝑡 prefix 𝑗)) · (𝑖‘(𝑡 substr 〈𝑗, (♯‘𝑡)〉))) = Σ𝑗 ∈ (0...(♯‘𝑣))((𝑔‘(𝑣 prefix 𝑗)) · (𝑖‘(𝑣 substr 〈𝑗, (♯‘𝑣)〉)))) |
381 | | simpr 484 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑣 ∈ Word 𝐴) → 𝑣 ∈ Word 𝐴) |
382 | | fzfid 14010 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑣 ∈ Word 𝐴) → (0...(♯‘𝑣)) ∈ Fin) |
383 | 294 | ad2antrr 726 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
(((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑣 ∈ Word 𝐴) ∧ 𝑗 ∈ (0...(♯‘𝑣))) → 𝑔:Word 𝐴⟶ℤ) |
384 | 383, 362 | ffvelcdmd 7104 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
(((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑣 ∈ Word 𝐴) ∧ 𝑗 ∈ (0...(♯‘𝑣))) → (𝑔‘(𝑣 prefix 𝑗)) ∈ ℤ) |
385 | 184 | ad2antrr 726 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
(((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑣 ∈ Word 𝐴) ∧ 𝑗 ∈ (0...(♯‘𝑣))) → 𝑖:Word 𝐴⟶ℤ) |
386 | 385, 364 | ffvelcdmd 7104 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
(((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑣 ∈ Word 𝐴) ∧ 𝑗 ∈ (0...(♯‘𝑣))) → (𝑖‘(𝑣 substr 〈𝑗, (♯‘𝑣)〉)) ∈ ℤ) |
387 | 384, 386 | zmulcld 12725 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
(((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑣 ∈ Word 𝐴) ∧ 𝑗 ∈ (0...(♯‘𝑣))) → ((𝑔‘(𝑣 prefix 𝑗)) · (𝑖‘(𝑣 substr 〈𝑗, (♯‘𝑣)〉))) ∈ ℤ) |
388 | 387 | zcnd 12720 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
(((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑣 ∈ Word 𝐴) ∧ 𝑗 ∈ (0...(♯‘𝑣))) → ((𝑔‘(𝑣 prefix 𝑗)) · (𝑖‘(𝑣 substr 〈𝑗, (♯‘𝑣)〉))) ∈ ℂ) |
389 | 382, 388 | fsumcl 15765 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑣 ∈ Word 𝐴) → Σ𝑗 ∈ (0...(♯‘𝑣))((𝑔‘(𝑣 prefix 𝑗)) · (𝑖‘(𝑣 substr 〈𝑗, (♯‘𝑣)〉))) ∈ ℂ) |
390 | 370, 380,
381, 389 | fvmptd3 7038 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑣 ∈ Word 𝐴) → ((𝑡 ∈ Word 𝐴 ↦ Σ𝑗 ∈ (0...(♯‘𝑡))((𝑔‘(𝑡 prefix 𝑗)) · (𝑖‘(𝑡 substr 〈𝑗, (♯‘𝑡)〉))))‘𝑣) = Σ𝑗 ∈ (0...(♯‘𝑣))((𝑔‘(𝑣 prefix 𝑗)) · (𝑖‘(𝑣 substr 〈𝑗, (♯‘𝑣)〉)))) |
391 | 390 | oveq1d 7445 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑣 ∈ Word 𝐴) → (((𝑡 ∈ Word 𝐴 ↦ Σ𝑗 ∈ (0...(♯‘𝑡))((𝑔‘(𝑡 prefix 𝑗)) · (𝑖‘(𝑡 substr 〈𝑗, (♯‘𝑡)〉))))‘𝑣) · (𝑀 Σg 𝑣)) = (Σ𝑗 ∈ (0...(♯‘𝑣))((𝑔‘(𝑣 prefix 𝑗)) · (𝑖‘(𝑣 substr 〈𝑗, (♯‘𝑣)〉))) · (𝑀 Σg 𝑣))) |
392 | 111 | ad3antrrr 730 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑣 ∈ Word 𝐴) → 𝑅 ∈ Grp) |
393 | 45 | ad3antrrr 730 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑣 ∈ Word 𝐴) → 𝑀 ∈ Mnd) |
394 | 315, 46 | syl 17 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) → Word 𝐴 ⊆ Word 𝐵) |
395 | 394 | sselda 3994 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑣 ∈ Word 𝐴) → 𝑣 ∈ Word 𝐵) |
396 | 49 | gsumwcl 18864 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑀 ∈ Mnd ∧ 𝑣 ∈ Word 𝐵) → (𝑀 Σg 𝑣) ∈ 𝐵) |
397 | 393, 395,
396 | syl2anc 584 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑣 ∈ Word 𝐴) → (𝑀 Σg 𝑣) ∈ 𝐵) |
398 | 2, 4, 392, 382, 397, 387 | gsummulgc2 33045 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑣 ∈ Word 𝐴) → (𝑅 Σg (𝑗 ∈
(0...(♯‘𝑣))
↦ (((𝑔‘(𝑣 prefix 𝑗)) · (𝑖‘(𝑣 substr 〈𝑗, (♯‘𝑣)〉))) · (𝑀 Σg 𝑣)))) = (Σ𝑗 ∈
(0...(♯‘𝑣))((𝑔‘(𝑣 prefix 𝑗)) · (𝑖‘(𝑣 substr 〈𝑗, (♯‘𝑣)〉))) · (𝑀 Σg 𝑣))) |
399 | 391, 398 | eqtr4d 2777 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑣 ∈ Word 𝐴) → (((𝑡 ∈ Word 𝐴 ↦ Σ𝑗 ∈ (0...(♯‘𝑡))((𝑔‘(𝑡 prefix 𝑗)) · (𝑖‘(𝑡 substr 〈𝑗, (♯‘𝑡)〉))))‘𝑣) · (𝑀 Σg 𝑣)) = (𝑅 Σg (𝑗 ∈
(0...(♯‘𝑣))
↦ (((𝑔‘(𝑣 prefix 𝑗)) · (𝑖‘(𝑣 substr 〈𝑗, (♯‘𝑣)〉))) · (𝑀 Σg 𝑣))))) |
400 | 330, 369,
399 | 3eqtr4rd 2785 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑣 ∈ Word 𝐴) → (((𝑡 ∈ Word 𝐴 ↦ Σ𝑗 ∈ (0...(♯‘𝑡))((𝑔‘(𝑡 prefix 𝑗)) · (𝑖‘(𝑡 substr 〈𝑗, (♯‘𝑡)〉))))‘𝑣) · (𝑀 Σg 𝑣)) = (𝑅 Σg (𝑗 ∈
(0...(♯‘𝑣))
↦ ((𝑤 ∈ Word
𝐴, 𝑓 ∈ Word 𝐴 ↦ (((𝑔‘𝑤) · (𝑀 Σg 𝑤))(.r‘𝑅)((𝑖‘𝑓) · (𝑀 Σg 𝑓))))‘〈(𝑣 prefix 𝑗), (𝑣 substr 〈𝑗, (♯‘𝑣)〉)〉)))) |
401 | 400 | mpteq2dva 5247 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) → (𝑣 ∈ Word 𝐴 ↦ (((𝑡 ∈ Word 𝐴 ↦ Σ𝑗 ∈ (0...(♯‘𝑡))((𝑔‘(𝑡 prefix 𝑗)) · (𝑖‘(𝑡 substr 〈𝑗, (♯‘𝑡)〉))))‘𝑣) · (𝑀 Σg 𝑣))) = (𝑣 ∈ Word 𝐴 ↦ (𝑅 Σg (𝑗 ∈
(0...(♯‘𝑣))
↦ ((𝑤 ∈ Word
𝐴, 𝑓 ∈ Word 𝐴 ↦ (((𝑔‘𝑤) · (𝑀 Σg 𝑤))(.r‘𝑅)((𝑖‘𝑓) · (𝑀 Σg 𝑓))))‘〈(𝑣 prefix 𝑗), (𝑣 substr 〈𝑗, (♯‘𝑣)〉)〉))))) |
402 | 401 | oveq2d 7446 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) → (𝑅 Σg (𝑣 ∈ Word 𝐴 ↦ (((𝑡 ∈ Word 𝐴 ↦ Σ𝑗 ∈ (0...(♯‘𝑡))((𝑔‘(𝑡 prefix 𝑗)) · (𝑖‘(𝑡 substr 〈𝑗, (♯‘𝑡)〉))))‘𝑣) · (𝑀 Σg 𝑣)))) = (𝑅 Σg (𝑣 ∈ Word 𝐴 ↦ (𝑅 Σg (𝑗 ∈
(0...(♯‘𝑣))
↦ ((𝑤 ∈ Word
𝐴, 𝑓 ∈ Word 𝐴 ↦ (((𝑔‘𝑤) · (𝑀 Σg 𝑤))(.r‘𝑅)((𝑖‘𝑓) · (𝑀 Σg 𝑓))))‘〈(𝑣 prefix 𝑗), (𝑣 substr 〈𝑗, (♯‘𝑣)〉)〉)))))) |
403 | 316, 324,
402 | 3eqtr4d 2784 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) → (𝑅 Σg (𝑢 ∈ Word 𝐴, 𝑣 ∈ Word 𝐴 ↦ (((𝑔‘𝑢) · (𝑀 Σg 𝑢))(.r‘𝑅)((𝑖‘𝑣) · (𝑀 Σg 𝑣))))) = (𝑅 Σg (𝑣 ∈ Word 𝐴 ↦ (((𝑡 ∈ Word 𝐴 ↦ Σ𝑗 ∈ (0...(♯‘𝑡))((𝑔‘(𝑡 prefix 𝑗)) · (𝑖‘(𝑡 substr 〈𝑗, (♯‘𝑡)〉))))‘𝑣) · (𝑀 Σg 𝑣))))) |
404 | 176, 180,
403 | 3eqtr3d 2782 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) → ((𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑔‘𝑤) · (𝑀 Σg 𝑤))))(.r‘𝑅)(𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑖‘𝑤) · (𝑀 Σg 𝑤))))) = (𝑅 Σg (𝑣 ∈ Word 𝐴 ↦ (((𝑡 ∈ Word 𝐴 ↦ Σ𝑗 ∈ (0...(♯‘𝑡))((𝑔‘(𝑡 prefix 𝑗)) · (𝑖‘(𝑡 substr 〈𝑗, (♯‘𝑡)〉))))‘𝑣) · (𝑀 Σg 𝑣))))) |
405 | | fveq1 6905 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑔 = ℎ → (𝑔‘𝑤) = (ℎ‘𝑤)) |
406 | 405 | oveq1d 7445 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑔 = ℎ → ((𝑔‘𝑤) · (𝑀 Σg 𝑤)) = ((ℎ‘𝑤) · (𝑀 Σg 𝑤))) |
407 | 406 | mpteq2dv 5249 |
. . . . . . . . . . . . . . . 16
⊢ (𝑔 = ℎ → (𝑤 ∈ Word 𝐴 ↦ ((𝑔‘𝑤) · (𝑀 Σg 𝑤))) = (𝑤 ∈ Word 𝐴 ↦ ((ℎ‘𝑤) · (𝑀 Σg 𝑤)))) |
408 | 407 | oveq2d 7446 |
. . . . . . . . . . . . . . 15
⊢ (𝑔 = ℎ → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑔‘𝑤) · (𝑀 Σg 𝑤)))) = (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((ℎ‘𝑤) · (𝑀 Σg 𝑤))))) |
409 | 408 | cbvmptv 5260 |
. . . . . . . . . . . . . 14
⊢ (𝑔 ∈ 𝐹 ↦ (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑔‘𝑤) · (𝑀 Σg 𝑤))))) = (ℎ ∈ 𝐹 ↦ (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((ℎ‘𝑤) · (𝑀 Σg 𝑤))))) |
410 | | fveq1 6905 |
. . . . . . . . . . . . . . . . . . 19
⊢ (ℎ = (𝑡 ∈ Word 𝐴 ↦ Σ𝑗 ∈ (0...(♯‘𝑡))((𝑔‘(𝑡 prefix 𝑗)) · (𝑖‘(𝑡 substr 〈𝑗, (♯‘𝑡)〉)))) → (ℎ‘𝑤) = ((𝑡 ∈ Word 𝐴 ↦ Σ𝑗 ∈ (0...(♯‘𝑡))((𝑔‘(𝑡 prefix 𝑗)) · (𝑖‘(𝑡 substr 〈𝑗, (♯‘𝑡)〉))))‘𝑤)) |
411 | 410 | oveq1d 7445 |
. . . . . . . . . . . . . . . . . 18
⊢ (ℎ = (𝑡 ∈ Word 𝐴 ↦ Σ𝑗 ∈ (0...(♯‘𝑡))((𝑔‘(𝑡 prefix 𝑗)) · (𝑖‘(𝑡 substr 〈𝑗, (♯‘𝑡)〉)))) → ((ℎ‘𝑤) · (𝑀 Σg 𝑤)) = (((𝑡 ∈ Word 𝐴 ↦ Σ𝑗 ∈ (0...(♯‘𝑡))((𝑔‘(𝑡 prefix 𝑗)) · (𝑖‘(𝑡 substr 〈𝑗, (♯‘𝑡)〉))))‘𝑤) · (𝑀 Σg 𝑤))) |
412 | 411 | mpteq2dv 5249 |
. . . . . . . . . . . . . . . . 17
⊢ (ℎ = (𝑡 ∈ Word 𝐴 ↦ Σ𝑗 ∈ (0...(♯‘𝑡))((𝑔‘(𝑡 prefix 𝑗)) · (𝑖‘(𝑡 substr 〈𝑗, (♯‘𝑡)〉)))) → (𝑤 ∈ Word 𝐴 ↦ ((ℎ‘𝑤) · (𝑀 Σg 𝑤))) = (𝑤 ∈ Word 𝐴 ↦ (((𝑡 ∈ Word 𝐴 ↦ Σ𝑗 ∈ (0...(♯‘𝑡))((𝑔‘(𝑡 prefix 𝑗)) · (𝑖‘(𝑡 substr 〈𝑗, (♯‘𝑡)〉))))‘𝑤) · (𝑀 Σg 𝑤)))) |
413 | 412 | oveq2d 7446 |
. . . . . . . . . . . . . . . 16
⊢ (ℎ = (𝑡 ∈ Word 𝐴 ↦ Σ𝑗 ∈ (0...(♯‘𝑡))((𝑔‘(𝑡 prefix 𝑗)) · (𝑖‘(𝑡 substr 〈𝑗, (♯‘𝑡)〉)))) → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((ℎ‘𝑤) · (𝑀 Σg 𝑤)))) = (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ (((𝑡 ∈ Word 𝐴 ↦ Σ𝑗 ∈ (0...(♯‘𝑡))((𝑔‘(𝑡 prefix 𝑗)) · (𝑖‘(𝑡 substr 〈𝑗, (♯‘𝑡)〉))))‘𝑤) · (𝑀 Σg 𝑤))))) |
414 | 413 | eqeq2d 2745 |
. . . . . . . . . . . . . . 15
⊢ (ℎ = (𝑡 ∈ Word 𝐴 ↦ Σ𝑗 ∈ (0...(♯‘𝑡))((𝑔‘(𝑡 prefix 𝑗)) · (𝑖‘(𝑡 substr 〈𝑗, (♯‘𝑡)〉)))) → ((𝑅 Σg (𝑣 ∈ Word 𝐴 ↦ (((𝑡 ∈ Word 𝐴 ↦ Σ𝑗 ∈ (0...(♯‘𝑡))((𝑔‘(𝑡 prefix 𝑗)) · (𝑖‘(𝑡 substr 〈𝑗, (♯‘𝑡)〉))))‘𝑣) · (𝑀 Σg 𝑣)))) = (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((ℎ‘𝑤) · (𝑀 Σg 𝑤)))) ↔ (𝑅 Σg (𝑣 ∈ Word 𝐴 ↦ (((𝑡 ∈ Word 𝐴 ↦ Σ𝑗 ∈ (0...(♯‘𝑡))((𝑔‘(𝑡 prefix 𝑗)) · (𝑖‘(𝑡 substr 〈𝑗, (♯‘𝑡)〉))))‘𝑣) · (𝑀 Σg 𝑣)))) = (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ (((𝑡 ∈ Word 𝐴 ↦ Σ𝑗 ∈ (0...(♯‘𝑡))((𝑔‘(𝑡 prefix 𝑗)) · (𝑖‘(𝑡 substr 〈𝑗, (♯‘𝑡)〉))))‘𝑤) · (𝑀 Σg 𝑤)))))) |
415 | | breq1 5150 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑓 = (𝑡 ∈ Word 𝐴 ↦ Σ𝑗 ∈ (0...(♯‘𝑡))((𝑔‘(𝑡 prefix 𝑗)) · (𝑖‘(𝑡 substr 〈𝑗, (♯‘𝑡)〉)))) → (𝑓 finSupp 0 ↔ (𝑡 ∈ Word 𝐴 ↦ Σ𝑗 ∈ (0...(♯‘𝑡))((𝑔‘(𝑡 prefix 𝑗)) · (𝑖‘(𝑡 substr 〈𝑗, (♯‘𝑡)〉)))) finSupp 0)) |
416 | 78 | a1i 11 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) → ℤ ∈ V) |
417 | | fzfid 14010 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑡 ∈ Word 𝐴) → (0...(♯‘𝑡)) ∈ Fin) |
418 | 294 | ad2antrr 726 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
(((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑡 ∈ Word 𝐴) ∧ 𝑗 ∈ (0...(♯‘𝑡))) → 𝑔:Word 𝐴⟶ℤ) |
419 | | pfxcl 14711 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑡 ∈ Word 𝐴 → (𝑡 prefix 𝑗) ∈ Word 𝐴) |
420 | 419 | ad2antlr 727 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
(((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑡 ∈ Word 𝐴) ∧ 𝑗 ∈ (0...(♯‘𝑡))) → (𝑡 prefix 𝑗) ∈ Word 𝐴) |
421 | 418, 420 | ffvelcdmd 7104 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
(((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑡 ∈ Word 𝐴) ∧ 𝑗 ∈ (0...(♯‘𝑡))) → (𝑔‘(𝑡 prefix 𝑗)) ∈ ℤ) |
422 | 184 | ad2antrr 726 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
(((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑡 ∈ Word 𝐴) ∧ 𝑗 ∈ (0...(♯‘𝑡))) → 𝑖:Word 𝐴⟶ℤ) |
423 | | swrdcl 14679 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑡 ∈ Word 𝐴 → (𝑡 substr 〈𝑗, (♯‘𝑡)〉) ∈ Word 𝐴) |
424 | 423 | ad2antlr 727 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
(((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑡 ∈ Word 𝐴) ∧ 𝑗 ∈ (0...(♯‘𝑡))) → (𝑡 substr 〈𝑗, (♯‘𝑡)〉) ∈ Word 𝐴) |
425 | 422, 424 | ffvelcdmd 7104 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
(((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑡 ∈ Word 𝐴) ∧ 𝑗 ∈ (0...(♯‘𝑡))) → (𝑖‘(𝑡 substr 〈𝑗, (♯‘𝑡)〉)) ∈ ℤ) |
426 | 421, 425 | zmulcld 12725 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑡 ∈ Word 𝐴) ∧ 𝑗 ∈ (0...(♯‘𝑡))) → ((𝑔‘(𝑡 prefix 𝑗)) · (𝑖‘(𝑡 substr 〈𝑗, (♯‘𝑡)〉))) ∈ ℤ) |
427 | 417, 426 | fsumzcl 15767 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑡 ∈ Word 𝐴) → Σ𝑗 ∈ (0...(♯‘𝑡))((𝑔‘(𝑡 prefix 𝑗)) · (𝑖‘(𝑡 substr 〈𝑗, (♯‘𝑡)〉))) ∈ ℤ) |
428 | 427 | fmpttd 7134 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) → (𝑡 ∈ Word 𝐴 ↦ Σ𝑗 ∈ (0...(♯‘𝑡))((𝑔‘(𝑡 prefix 𝑗)) · (𝑖‘(𝑡 substr 〈𝑗, (♯‘𝑡)〉)))):Word 𝐴⟶ℤ) |
429 | 416, 109,
428 | elmapdd 8879 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) → (𝑡 ∈ Word 𝐴 ↦ Σ𝑗 ∈ (0...(♯‘𝑡))((𝑔‘(𝑡 prefix 𝑗)) · (𝑖‘(𝑡 substr 〈𝑗, (♯‘𝑡)〉)))) ∈ (ℤ
↑m Word 𝐴)) |
430 | | 0zd 12622 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) → 0 ∈ ℤ) |
431 | 428 | ffund 6740 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) → Fun (𝑡 ∈ Word 𝐴 ↦ Σ𝑗 ∈ (0...(♯‘𝑡))((𝑔‘(𝑡 prefix 𝑗)) · (𝑖‘(𝑡 substr 〈𝑗, (♯‘𝑡)〉))))) |
432 | | ccatfn 14606 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ++ Fn (V
× V) |
433 | | fnfun 6668 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ( ++ Fn
(V × V) → Fun ++ ) |
434 | 432, 433 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . . 20
⊢ Fun
++ |
435 | | imafi 9350 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((Fun ++
∧ ((𝑔 supp 0) ×
(𝑖 supp 0)) ∈ Fin)
→ ( ++ “ ((𝑔
supp 0) × (𝑖 supp
0))) ∈ Fin) |
436 | 434, 244,
435 | sylancr 587 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) → ( ++ “ ((𝑔 supp 0) × (𝑖 supp 0))) ∈ Fin) |
437 | | fveq2 6906 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑡 = 𝑤 → (♯‘𝑡) = (♯‘𝑤)) |
438 | 437 | oveq2d 7446 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑡 = 𝑤 → (0...(♯‘𝑡)) = (0...(♯‘𝑤))) |
439 | | fvoveq1 7453 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑡 = 𝑤 → (𝑔‘(𝑡 prefix 𝑗)) = (𝑔‘(𝑤 prefix 𝑗))) |
440 | | id 22 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝑡 = 𝑤 → 𝑡 = 𝑤) |
441 | 437 | opeq2d 4884 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝑡 = 𝑤 → 〈𝑗, (♯‘𝑡)〉 = 〈𝑗, (♯‘𝑤)〉) |
442 | 440, 441 | oveq12d 7448 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑡 = 𝑤 → (𝑡 substr 〈𝑗, (♯‘𝑡)〉) = (𝑤 substr 〈𝑗, (♯‘𝑤)〉)) |
443 | 442 | fveq2d 6910 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑡 = 𝑤 → (𝑖‘(𝑡 substr 〈𝑗, (♯‘𝑡)〉)) = (𝑖‘(𝑤 substr 〈𝑗, (♯‘𝑤)〉))) |
444 | 439, 443 | oveq12d 7448 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑡 = 𝑤 → ((𝑔‘(𝑡 prefix 𝑗)) · (𝑖‘(𝑡 substr 〈𝑗, (♯‘𝑡)〉))) = ((𝑔‘(𝑤 prefix 𝑗)) · (𝑖‘(𝑤 substr 〈𝑗, (♯‘𝑤)〉)))) |
445 | 444 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝑡 = 𝑤 ∧ 𝑗 ∈ (0...(♯‘𝑡))) → ((𝑔‘(𝑡 prefix 𝑗)) · (𝑖‘(𝑡 substr 〈𝑗, (♯‘𝑡)〉))) = ((𝑔‘(𝑤 prefix 𝑗)) · (𝑖‘(𝑤 substr 〈𝑗, (♯‘𝑤)〉)))) |
446 | 438, 445 | sumeq12dv 15738 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑡 = 𝑤 → Σ𝑗 ∈ (0...(♯‘𝑡))((𝑔‘(𝑡 prefix 𝑗)) · (𝑖‘(𝑡 substr 〈𝑗, (♯‘𝑡)〉))) = Σ𝑗 ∈ (0...(♯‘𝑤))((𝑔‘(𝑤 prefix 𝑗)) · (𝑖‘(𝑤 substr 〈𝑗, (♯‘𝑤)〉)))) |
447 | | oveq1 7437 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ (𝑢 = (𝑤 prefix 𝑗) → (𝑢 ++ 𝑣) = ((𝑤 prefix 𝑗) ++ 𝑣)) |
448 | 447 | eqeq2d 2745 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ (𝑢 = (𝑤 prefix 𝑗) → (𝑤 = (𝑢 ++ 𝑣) ↔ 𝑤 = ((𝑤 prefix 𝑗) ++ 𝑣))) |
449 | | oveq2 7438 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ (𝑣 = (𝑤 substr 〈𝑗, (♯‘𝑤)〉) → ((𝑤 prefix 𝑗) ++ 𝑣) = ((𝑤 prefix 𝑗) ++ (𝑤 substr 〈𝑗, (♯‘𝑤)〉))) |
450 | 449 | eqeq2d 2745 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ (𝑣 = (𝑤 substr 〈𝑗, (♯‘𝑤)〉) → (𝑤 = ((𝑤 prefix 𝑗) ++ 𝑣) ↔ 𝑤 = ((𝑤 prefix 𝑗) ++ (𝑤 substr 〈𝑗, (♯‘𝑤)〉)))) |
451 | 246 | ad4antr 732 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢
(((((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑤 ∈ (Word 𝐴 ∖ ( ++ “ ((𝑔 supp 0) × (𝑖 supp 0))))) ∧ 𝑗 ∈ (0...(♯‘𝑤))) ∧ (𝑔‘(𝑤 prefix 𝑗)) ≠ 0) ∧ (𝑖‘(𝑤 substr 〈𝑗, (♯‘𝑤)〉)) ≠ 0) → 𝑔 Fn Word 𝐴) |
452 | 109 | ad4antr 732 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢
(((((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑤 ∈ (Word 𝐴 ∖ ( ++ “ ((𝑔 supp 0) × (𝑖 supp 0))))) ∧ 𝑗 ∈ (0...(♯‘𝑤))) ∧ (𝑔‘(𝑤 prefix 𝑗)) ≠ 0) ∧ (𝑖‘(𝑤 substr 〈𝑗, (♯‘𝑤)〉)) ≠ 0) → Word 𝐴 ∈ V) |
453 | | 0zd 12622 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢
(((((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑤 ∈ (Word 𝐴 ∖ ( ++ “ ((𝑔 supp 0) × (𝑖 supp 0))))) ∧ 𝑗 ∈ (0...(♯‘𝑤))) ∧ (𝑔‘(𝑤 prefix 𝑗)) ≠ 0) ∧ (𝑖‘(𝑤 substr 〈𝑗, (♯‘𝑤)〉)) ≠ 0) → 0 ∈
ℤ) |
454 | | simpr 484 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
⊢ ((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑤 ∈ (Word 𝐴 ∖ ( ++ “ ((𝑔 supp 0) × (𝑖 supp 0))))) → 𝑤 ∈ (Word 𝐴 ∖ ( ++ “ ((𝑔 supp 0) × (𝑖 supp 0))))) |
455 | 454 | eldifad 3974 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢ ((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑤 ∈ (Word 𝐴 ∖ ( ++ “ ((𝑔 supp 0) × (𝑖 supp 0))))) → 𝑤 ∈ Word 𝐴) |
456 | 455 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢
(((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑤 ∈ (Word 𝐴 ∖ ( ++ “ ((𝑔 supp 0) × (𝑖 supp 0))))) ∧ 𝑗 ∈ (0...(♯‘𝑤))) → 𝑤 ∈ Word 𝐴) |
457 | | pfxcl 14711 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ (𝑤 ∈ Word 𝐴 → (𝑤 prefix 𝑗) ∈ Word 𝐴) |
458 | 456, 457 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢
(((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑤 ∈ (Word 𝐴 ∖ ( ++ “ ((𝑔 supp 0) × (𝑖 supp 0))))) ∧ 𝑗 ∈ (0...(♯‘𝑤))) → (𝑤 prefix 𝑗) ∈ Word 𝐴) |
459 | 458 | ad2antrr 726 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢
(((((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑤 ∈ (Word 𝐴 ∖ ( ++ “ ((𝑔 supp 0) × (𝑖 supp 0))))) ∧ 𝑗 ∈ (0...(♯‘𝑤))) ∧ (𝑔‘(𝑤 prefix 𝑗)) ≠ 0) ∧ (𝑖‘(𝑤 substr 〈𝑗, (♯‘𝑤)〉)) ≠ 0) → (𝑤 prefix 𝑗) ∈ Word 𝐴) |
460 | | simplr 769 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢
(((((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑤 ∈ (Word 𝐴 ∖ ( ++ “ ((𝑔 supp 0) × (𝑖 supp 0))))) ∧ 𝑗 ∈ (0...(♯‘𝑤))) ∧ (𝑔‘(𝑤 prefix 𝑗)) ≠ 0) ∧ (𝑖‘(𝑤 substr 〈𝑗, (♯‘𝑤)〉)) ≠ 0) → (𝑔‘(𝑤 prefix 𝑗)) ≠ 0) |
461 | 451, 452,
453, 459, 460 | elsuppfnd 32696 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢
(((((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑤 ∈ (Word 𝐴 ∖ ( ++ “ ((𝑔 supp 0) × (𝑖 supp 0))))) ∧ 𝑗 ∈ (0...(♯‘𝑤))) ∧ (𝑔‘(𝑤 prefix 𝑗)) ≠ 0) ∧ (𝑖‘(𝑤 substr 〈𝑗, (♯‘𝑤)〉)) ≠ 0) → (𝑤 prefix 𝑗) ∈ (𝑔 supp 0)) |
462 | 275 | ad4antr 732 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢
(((((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑤 ∈ (Word 𝐴 ∖ ( ++ “ ((𝑔 supp 0) × (𝑖 supp 0))))) ∧ 𝑗 ∈ (0...(♯‘𝑤))) ∧ (𝑔‘(𝑤 prefix 𝑗)) ≠ 0) ∧ (𝑖‘(𝑤 substr 〈𝑗, (♯‘𝑤)〉)) ≠ 0) → 𝑖 Fn Word 𝐴) |
463 | | swrdcl 14679 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ (𝑤 ∈ Word 𝐴 → (𝑤 substr 〈𝑗, (♯‘𝑤)〉) ∈ Word 𝐴) |
464 | 456, 463 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢
(((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑤 ∈ (Word 𝐴 ∖ ( ++ “ ((𝑔 supp 0) × (𝑖 supp 0))))) ∧ 𝑗 ∈ (0...(♯‘𝑤))) → (𝑤 substr 〈𝑗, (♯‘𝑤)〉) ∈ Word 𝐴) |
465 | 464 | ad2antrr 726 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢
(((((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑤 ∈ (Word 𝐴 ∖ ( ++ “ ((𝑔 supp 0) × (𝑖 supp 0))))) ∧ 𝑗 ∈ (0...(♯‘𝑤))) ∧ (𝑔‘(𝑤 prefix 𝑗)) ≠ 0) ∧ (𝑖‘(𝑤 substr 〈𝑗, (♯‘𝑤)〉)) ≠ 0) → (𝑤 substr 〈𝑗, (♯‘𝑤)〉) ∈ Word 𝐴) |
466 | | simpr 484 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢
(((((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑤 ∈ (Word 𝐴 ∖ ( ++ “ ((𝑔 supp 0) × (𝑖 supp 0))))) ∧ 𝑗 ∈ (0...(♯‘𝑤))) ∧ (𝑔‘(𝑤 prefix 𝑗)) ≠ 0) ∧ (𝑖‘(𝑤 substr 〈𝑗, (♯‘𝑤)〉)) ≠ 0) → (𝑖‘(𝑤 substr 〈𝑗, (♯‘𝑤)〉)) ≠ 0) |
467 | 462, 452,
453, 465, 466 | elsuppfnd 32696 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢
(((((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑤 ∈ (Word 𝐴 ∖ ( ++ “ ((𝑔 supp 0) × (𝑖 supp 0))))) ∧ 𝑗 ∈ (0...(♯‘𝑤))) ∧ (𝑔‘(𝑤 prefix 𝑗)) ≠ 0) ∧ (𝑖‘(𝑤 substr 〈𝑗, (♯‘𝑤)〉)) ≠ 0) → (𝑤 substr 〈𝑗, (♯‘𝑤)〉) ∈ (𝑖 supp 0)) |
468 | 456 | ad2antrr 726 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢
(((((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑤 ∈ (Word 𝐴 ∖ ( ++ “ ((𝑔 supp 0) × (𝑖 supp 0))))) ∧ 𝑗 ∈ (0...(♯‘𝑤))) ∧ (𝑔‘(𝑤 prefix 𝑗)) ≠ 0) ∧ (𝑖‘(𝑤 substr 〈𝑗, (♯‘𝑤)〉)) ≠ 0) → 𝑤 ∈ Word 𝐴) |
469 | | simpllr 776 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢
(((((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑤 ∈ (Word 𝐴 ∖ ( ++ “ ((𝑔 supp 0) × (𝑖 supp 0))))) ∧ 𝑗 ∈ (0...(♯‘𝑤))) ∧ (𝑔‘(𝑤 prefix 𝑗)) ≠ 0) ∧ (𝑖‘(𝑤 substr 〈𝑗, (♯‘𝑤)〉)) ≠ 0) → 𝑗 ∈ (0...(♯‘𝑤))) |
470 | | pfxcctswrd 14744 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ ((𝑤 ∈ Word 𝐴 ∧ 𝑗 ∈ (0...(♯‘𝑤))) → ((𝑤 prefix 𝑗) ++ (𝑤 substr 〈𝑗, (♯‘𝑤)〉)) = 𝑤) |
471 | 468, 469,
470 | syl2anc 584 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢
(((((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑤 ∈ (Word 𝐴 ∖ ( ++ “ ((𝑔 supp 0) × (𝑖 supp 0))))) ∧ 𝑗 ∈ (0...(♯‘𝑤))) ∧ (𝑔‘(𝑤 prefix 𝑗)) ≠ 0) ∧ (𝑖‘(𝑤 substr 〈𝑗, (♯‘𝑤)〉)) ≠ 0) → ((𝑤 prefix 𝑗) ++ (𝑤 substr 〈𝑗, (♯‘𝑤)〉)) = 𝑤) |
472 | 471 | eqcomd 2740 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢
(((((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑤 ∈ (Word 𝐴 ∖ ( ++ “ ((𝑔 supp 0) × (𝑖 supp 0))))) ∧ 𝑗 ∈ (0...(♯‘𝑤))) ∧ (𝑔‘(𝑤 prefix 𝑗)) ≠ 0) ∧ (𝑖‘(𝑤 substr 〈𝑗, (♯‘𝑤)〉)) ≠ 0) → 𝑤 = ((𝑤 prefix 𝑗) ++ (𝑤 substr 〈𝑗, (♯‘𝑤)〉))) |
473 | 448, 450,
461, 467, 472 | 2rspcedvdw 3635 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢
(((((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑤 ∈ (Word 𝐴 ∖ ( ++ “ ((𝑔 supp 0) × (𝑖 supp 0))))) ∧ 𝑗 ∈ (0...(♯‘𝑤))) ∧ (𝑔‘(𝑤 prefix 𝑗)) ≠ 0) ∧ (𝑖‘(𝑤 substr 〈𝑗, (♯‘𝑤)〉)) ≠ 0) → ∃𝑢 ∈ (𝑔 supp 0)∃𝑣 ∈ (𝑖 supp 0)𝑤 = (𝑢 ++ 𝑣)) |
474 | | fnov 7563 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ ( ++ Fn
(V × V) ↔ ++ = (𝑢 ∈ V, 𝑣 ∈ V ↦ (𝑢 ++ 𝑣))) |
475 | 432, 474 | mpbi 230 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ ++ =
(𝑢 ∈ V, 𝑣 ∈ V ↦ (𝑢 ++ 𝑣)) |
476 | 200 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ (⊤
→ 𝑤 ∈
V) |
477 | | ssv 4019 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ (𝑔 supp 0) ⊆
V |
478 | 477 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ (⊤
→ (𝑔 supp 0) ⊆
V) |
479 | | ssv 4019 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ (𝑖 supp 0) ⊆
V |
480 | 479 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ (⊤
→ (𝑖 supp 0) ⊆
V) |
481 | 475, 476,
478, 480 | elimampo 7569 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ (⊤
→ (𝑤 ∈ ( ++
“ ((𝑔 supp 0) ×
(𝑖 supp 0))) ↔
∃𝑢 ∈ (𝑔 supp 0)∃𝑣 ∈ (𝑖 supp 0)𝑤 = (𝑢 ++ 𝑣))) |
482 | 481 | mptru 1543 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (𝑤 ∈ ( ++ “ ((𝑔 supp 0) × (𝑖 supp 0))) ↔ ∃𝑢 ∈ (𝑔 supp 0)∃𝑣 ∈ (𝑖 supp 0)𝑤 = (𝑢 ++ 𝑣)) |
483 | 473, 482 | sylibr 234 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢
(((((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑤 ∈ (Word 𝐴 ∖ ( ++ “ ((𝑔 supp 0) × (𝑖 supp 0))))) ∧ 𝑗 ∈ (0...(♯‘𝑤))) ∧ (𝑔‘(𝑤 prefix 𝑗)) ≠ 0) ∧ (𝑖‘(𝑤 substr 〈𝑗, (♯‘𝑤)〉)) ≠ 0) → 𝑤 ∈ ( ++ “ ((𝑔 supp 0) × (𝑖 supp 0)))) |
484 | 483 | anasss 466 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢
((((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑤 ∈ (Word 𝐴 ∖ ( ++ “ ((𝑔 supp 0) × (𝑖 supp 0))))) ∧ 𝑗 ∈ (0...(♯‘𝑤))) ∧ ((𝑔‘(𝑤 prefix 𝑗)) ≠ 0 ∧ (𝑖‘(𝑤 substr 〈𝑗, (♯‘𝑤)〉)) ≠ 0)) → 𝑤 ∈ ( ++ “ ((𝑔 supp 0) × (𝑖 supp 0)))) |
485 | 454 | ad3antrrr 730 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢
(((((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑤 ∈ (Word 𝐴 ∖ ( ++ “ ((𝑔 supp 0) × (𝑖 supp 0))))) ∧ 𝑗 ∈ (0...(♯‘𝑤))) ∧ (𝑔‘(𝑤 prefix 𝑗)) ≠ 0) ∧ (𝑖‘(𝑤 substr 〈𝑗, (♯‘𝑤)〉)) ≠ 0) → 𝑤 ∈ (Word 𝐴 ∖ ( ++ “ ((𝑔 supp 0) × (𝑖 supp 0))))) |
486 | 485 | eldifbd 3975 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢
(((((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑤 ∈ (Word 𝐴 ∖ ( ++ “ ((𝑔 supp 0) × (𝑖 supp 0))))) ∧ 𝑗 ∈ (0...(♯‘𝑤))) ∧ (𝑔‘(𝑤 prefix 𝑗)) ≠ 0) ∧ (𝑖‘(𝑤 substr 〈𝑗, (♯‘𝑤)〉)) ≠ 0) → ¬ 𝑤 ∈ ( ++ “ ((𝑔 supp 0) × (𝑖 supp 0)))) |
487 | 486 | anasss 466 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢
((((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑤 ∈ (Word 𝐴 ∖ ( ++ “ ((𝑔 supp 0) × (𝑖 supp 0))))) ∧ 𝑗 ∈ (0...(♯‘𝑤))) ∧ ((𝑔‘(𝑤 prefix 𝑗)) ≠ 0 ∧ (𝑖‘(𝑤 substr 〈𝑗, (♯‘𝑤)〉)) ≠ 0)) → ¬ 𝑤 ∈ ( ++ “ ((𝑔 supp 0) × (𝑖 supp 0)))) |
488 | 484, 487 | pm2.65da 817 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢
(((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑤 ∈ (Word 𝐴 ∖ ( ++ “ ((𝑔 supp 0) × (𝑖 supp 0))))) ∧ 𝑗 ∈ (0...(♯‘𝑤))) → ¬ ((𝑔‘(𝑤 prefix 𝑗)) ≠ 0 ∧ (𝑖‘(𝑤 substr 〈𝑗, (♯‘𝑤)〉)) ≠ 0)) |
489 | | df-ne 2938 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ ((𝑔‘(𝑤 prefix 𝑗)) ≠ 0 ↔ ¬ (𝑔‘(𝑤 prefix 𝑗)) = 0) |
490 | | df-ne 2938 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ ((𝑖‘(𝑤 substr 〈𝑗, (♯‘𝑤)〉)) ≠ 0 ↔ ¬ (𝑖‘(𝑤 substr 〈𝑗, (♯‘𝑤)〉)) = 0) |
491 | 489, 490 | anbi12i 628 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (((𝑔‘(𝑤 prefix 𝑗)) ≠ 0 ∧ (𝑖‘(𝑤 substr 〈𝑗, (♯‘𝑤)〉)) ≠ 0) ↔ (¬ (𝑔‘(𝑤 prefix 𝑗)) = 0 ∧ ¬ (𝑖‘(𝑤 substr 〈𝑗, (♯‘𝑤)〉)) = 0)) |
492 | 491 | notbii 320 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (¬
((𝑔‘(𝑤 prefix 𝑗)) ≠ 0 ∧ (𝑖‘(𝑤 substr 〈𝑗, (♯‘𝑤)〉)) ≠ 0) ↔ ¬ (¬ (𝑔‘(𝑤 prefix 𝑗)) = 0 ∧ ¬ (𝑖‘(𝑤 substr 〈𝑗, (♯‘𝑤)〉)) = 0)) |
493 | | pm4.57 992 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (¬
(¬ (𝑔‘(𝑤 prefix 𝑗)) = 0 ∧ ¬ (𝑖‘(𝑤 substr 〈𝑗, (♯‘𝑤)〉)) = 0) ↔ ((𝑔‘(𝑤 prefix 𝑗)) = 0 ∨ (𝑖‘(𝑤 substr 〈𝑗, (♯‘𝑤)〉)) = 0)) |
494 | 492, 493 | bitr2i 276 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (((𝑔‘(𝑤 prefix 𝑗)) = 0 ∨ (𝑖‘(𝑤 substr 〈𝑗, (♯‘𝑤)〉)) = 0) ↔ ¬ ((𝑔‘(𝑤 prefix 𝑗)) ≠ 0 ∧ (𝑖‘(𝑤 substr 〈𝑗, (♯‘𝑤)〉)) ≠ 0)) |
495 | 488, 494 | sylibr 234 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢
(((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑤 ∈ (Word 𝐴 ∖ ( ++ “ ((𝑔 supp 0) × (𝑖 supp 0))))) ∧ 𝑗 ∈ (0...(♯‘𝑤))) → ((𝑔‘(𝑤 prefix 𝑗)) = 0 ∨ (𝑖‘(𝑤 substr 〈𝑗, (♯‘𝑤)〉)) = 0)) |
496 | 294 | ad2antrr 726 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢
(((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑤 ∈ (Word 𝐴 ∖ ( ++ “ ((𝑔 supp 0) × (𝑖 supp 0))))) ∧ 𝑗 ∈ (0...(♯‘𝑤))) → 𝑔:Word 𝐴⟶ℤ) |
497 | 496, 458 | ffvelcdmd 7104 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢
(((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑤 ∈ (Word 𝐴 ∖ ( ++ “ ((𝑔 supp 0) × (𝑖 supp 0))))) ∧ 𝑗 ∈ (0...(♯‘𝑤))) → (𝑔‘(𝑤 prefix 𝑗)) ∈ ℤ) |
498 | 497 | zcnd 12720 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢
(((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑤 ∈ (Word 𝐴 ∖ ( ++ “ ((𝑔 supp 0) × (𝑖 supp 0))))) ∧ 𝑗 ∈ (0...(♯‘𝑤))) → (𝑔‘(𝑤 prefix 𝑗)) ∈ ℂ) |
499 | 184 | ad2antrr 726 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢
(((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑤 ∈ (Word 𝐴 ∖ ( ++ “ ((𝑔 supp 0) × (𝑖 supp 0))))) ∧ 𝑗 ∈ (0...(♯‘𝑤))) → 𝑖:Word 𝐴⟶ℤ) |
500 | 499, 464 | ffvelcdmd 7104 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢
(((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑤 ∈ (Word 𝐴 ∖ ( ++ “ ((𝑔 supp 0) × (𝑖 supp 0))))) ∧ 𝑗 ∈ (0...(♯‘𝑤))) → (𝑖‘(𝑤 substr 〈𝑗, (♯‘𝑤)〉)) ∈ ℤ) |
501 | 500 | zcnd 12720 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢
(((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑤 ∈ (Word 𝐴 ∖ ( ++ “ ((𝑔 supp 0) × (𝑖 supp 0))))) ∧ 𝑗 ∈ (0...(♯‘𝑤))) → (𝑖‘(𝑤 substr 〈𝑗, (♯‘𝑤)〉)) ∈ ℂ) |
502 | 498, 501 | mul0ord 11910 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢
(((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑤 ∈ (Word 𝐴 ∖ ( ++ “ ((𝑔 supp 0) × (𝑖 supp 0))))) ∧ 𝑗 ∈ (0...(♯‘𝑤))) → (((𝑔‘(𝑤 prefix 𝑗)) · (𝑖‘(𝑤 substr 〈𝑗, (♯‘𝑤)〉))) = 0 ↔ ((𝑔‘(𝑤 prefix 𝑗)) = 0 ∨ (𝑖‘(𝑤 substr 〈𝑗, (♯‘𝑤)〉)) = 0))) |
503 | 495, 502 | mpbird 257 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
(((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑤 ∈ (Word 𝐴 ∖ ( ++ “ ((𝑔 supp 0) × (𝑖 supp 0))))) ∧ 𝑗 ∈ (0...(♯‘𝑤))) → ((𝑔‘(𝑤 prefix 𝑗)) · (𝑖‘(𝑤 substr 〈𝑗, (♯‘𝑤)〉))) = 0) |
504 | 503 | sumeq2dv 15734 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑤 ∈ (Word 𝐴 ∖ ( ++ “ ((𝑔 supp 0) × (𝑖 supp 0))))) → Σ𝑗 ∈ (0...(♯‘𝑤))((𝑔‘(𝑤 prefix 𝑗)) · (𝑖‘(𝑤 substr 〈𝑗, (♯‘𝑤)〉))) = Σ𝑗 ∈ (0...(♯‘𝑤))0) |
505 | | fzssuz 13601 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
(0...(♯‘𝑤)) ⊆
(ℤ≥‘0) |
506 | | sumz 15754 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢
(((0...(♯‘𝑤)) ⊆ (ℤ≥‘0)
∨ (0...(♯‘𝑤)) ∈ Fin) → Σ𝑗 ∈
(0...(♯‘𝑤))0 =
0) |
507 | 506 | orcs 875 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
((0...(♯‘𝑤)) ⊆ (ℤ≥‘0)
→ Σ𝑗 ∈
(0...(♯‘𝑤))0 =
0) |
508 | 505, 507 | mp1i 13 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑤 ∈ (Word 𝐴 ∖ ( ++ “ ((𝑔 supp 0) × (𝑖 supp 0))))) → Σ𝑗 ∈ (0...(♯‘𝑤))0 = 0) |
509 | 504, 508 | eqtrd 2774 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑤 ∈ (Word 𝐴 ∖ ( ++ “ ((𝑔 supp 0) × (𝑖 supp 0))))) → Σ𝑗 ∈ (0...(♯‘𝑤))((𝑔‘(𝑤 prefix 𝑗)) · (𝑖‘(𝑤 substr 〈𝑗, (♯‘𝑤)〉))) = 0) |
510 | 446, 509 | sylan9eqr 2796 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
(((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑤 ∈ (Word 𝐴 ∖ ( ++ “ ((𝑔 supp 0) × (𝑖 supp 0))))) ∧ 𝑡 = 𝑤) → Σ𝑗 ∈ (0...(♯‘𝑡))((𝑔‘(𝑡 prefix 𝑗)) · (𝑖‘(𝑡 substr 〈𝑗, (♯‘𝑡)〉))) = 0) |
511 | | 0zd 12622 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑤 ∈ (Word 𝐴 ∖ ( ++ “ ((𝑔 supp 0) × (𝑖 supp 0))))) → 0 ∈
ℤ) |
512 | 370, 510,
455, 511 | fvmptd2 7023 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑤 ∈ (Word 𝐴 ∖ ( ++ “ ((𝑔 supp 0) × (𝑖 supp 0))))) → ((𝑡 ∈ Word 𝐴 ↦ Σ𝑗 ∈ (0...(♯‘𝑡))((𝑔‘(𝑡 prefix 𝑗)) · (𝑖‘(𝑡 substr 〈𝑗, (♯‘𝑡)〉))))‘𝑤) = 0) |
513 | 428, 512 | suppss 8217 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) → ((𝑡 ∈ Word 𝐴 ↦ Σ𝑗 ∈ (0...(♯‘𝑡))((𝑔‘(𝑡 prefix 𝑗)) · (𝑖‘(𝑡 substr 〈𝑗, (♯‘𝑡)〉)))) supp 0) ⊆ ( ++ “
((𝑔 supp 0) × (𝑖 supp 0)))) |
514 | 436, 513 | ssfid 9298 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) → ((𝑡 ∈ Word 𝐴 ↦ Σ𝑗 ∈ (0...(♯‘𝑡))((𝑔‘(𝑡 prefix 𝑗)) · (𝑖‘(𝑡 substr 〈𝑗, (♯‘𝑡)〉)))) supp 0) ∈
Fin) |
515 | 429, 430,
431, 514 | isfsuppd 9403 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) → (𝑡 ∈ Word 𝐴 ↦ Σ𝑗 ∈ (0...(♯‘𝑡))((𝑔‘(𝑡 prefix 𝑗)) · (𝑖‘(𝑡 substr 〈𝑗, (♯‘𝑡)〉)))) finSupp 0) |
516 | 415, 429,
515 | elrabd 3696 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) → (𝑡 ∈ Word 𝐴 ↦ Σ𝑗 ∈ (0...(♯‘𝑡))((𝑔‘(𝑡 prefix 𝑗)) · (𝑖‘(𝑡 substr 〈𝑗, (♯‘𝑡)〉)))) ∈ {𝑓 ∈ (ℤ ↑m Word
𝐴) ∣ 𝑓 finSupp 0}) |
517 | 516, 6 | eleqtrrdi 2849 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) → (𝑡 ∈ Word 𝐴 ↦ Σ𝑗 ∈ (0...(♯‘𝑡))((𝑔‘(𝑡 prefix 𝑗)) · (𝑖‘(𝑡 substr 〈𝑗, (♯‘𝑡)〉)))) ∈ 𝐹) |
518 | | fveq2 6906 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑣 = 𝑤 → ((𝑡 ∈ Word 𝐴 ↦ Σ𝑗 ∈ (0...(♯‘𝑡))((𝑔‘(𝑡 prefix 𝑗)) · (𝑖‘(𝑡 substr 〈𝑗, (♯‘𝑡)〉))))‘𝑣) = ((𝑡 ∈ Word 𝐴 ↦ Σ𝑗 ∈ (0...(♯‘𝑡))((𝑔‘(𝑡 prefix 𝑗)) · (𝑖‘(𝑡 substr 〈𝑗, (♯‘𝑡)〉))))‘𝑤)) |
519 | 518, 145 | oveq12d 7448 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑣 = 𝑤 → (((𝑡 ∈ Word 𝐴 ↦ Σ𝑗 ∈ (0...(♯‘𝑡))((𝑔‘(𝑡 prefix 𝑗)) · (𝑖‘(𝑡 substr 〈𝑗, (♯‘𝑡)〉))))‘𝑣) · (𝑀 Σg 𝑣)) = (((𝑡 ∈ Word 𝐴 ↦ Σ𝑗 ∈ (0...(♯‘𝑡))((𝑔‘(𝑡 prefix 𝑗)) · (𝑖‘(𝑡 substr 〈𝑗, (♯‘𝑡)〉))))‘𝑤) · (𝑀 Σg 𝑤))) |
520 | 519 | cbvmptv 5260 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑣 ∈ Word 𝐴 ↦ (((𝑡 ∈ Word 𝐴 ↦ Σ𝑗 ∈ (0...(♯‘𝑡))((𝑔‘(𝑡 prefix 𝑗)) · (𝑖‘(𝑡 substr 〈𝑗, (♯‘𝑡)〉))))‘𝑣) · (𝑀 Σg 𝑣))) = (𝑤 ∈ Word 𝐴 ↦ (((𝑡 ∈ Word 𝐴 ↦ Σ𝑗 ∈ (0...(♯‘𝑡))((𝑔‘(𝑡 prefix 𝑗)) · (𝑖‘(𝑡 substr 〈𝑗, (♯‘𝑡)〉))))‘𝑤) · (𝑀 Σg 𝑤))) |
521 | 520 | oveq2i 7441 |
. . . . . . . . . . . . . . . 16
⊢ (𝑅 Σg
(𝑣 ∈ Word 𝐴 ↦ (((𝑡 ∈ Word 𝐴 ↦ Σ𝑗 ∈ (0...(♯‘𝑡))((𝑔‘(𝑡 prefix 𝑗)) · (𝑖‘(𝑡 substr 〈𝑗, (♯‘𝑡)〉))))‘𝑣) · (𝑀 Σg 𝑣)))) = (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ (((𝑡 ∈ Word 𝐴 ↦ Σ𝑗 ∈ (0...(♯‘𝑡))((𝑔‘(𝑡 prefix 𝑗)) · (𝑖‘(𝑡 substr 〈𝑗, (♯‘𝑡)〉))))‘𝑤) · (𝑀 Σg 𝑤)))) |
522 | 521 | a1i 11 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) → (𝑅 Σg (𝑣 ∈ Word 𝐴 ↦ (((𝑡 ∈ Word 𝐴 ↦ Σ𝑗 ∈ (0...(♯‘𝑡))((𝑔‘(𝑡 prefix 𝑗)) · (𝑖‘(𝑡 substr 〈𝑗, (♯‘𝑡)〉))))‘𝑣) · (𝑀 Σg 𝑣)))) = (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ (((𝑡 ∈ Word 𝐴 ↦ Σ𝑗 ∈ (0...(♯‘𝑡))((𝑔‘(𝑡 prefix 𝑗)) · (𝑖‘(𝑡 substr 〈𝑗, (♯‘𝑡)〉))))‘𝑤) · (𝑀 Σg 𝑤))))) |
523 | 414, 517,
522 | rspcedvdw 3624 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) → ∃ℎ ∈ 𝐹 (𝑅 Σg (𝑣 ∈ Word 𝐴 ↦ (((𝑡 ∈ Word 𝐴 ↦ Σ𝑗 ∈ (0...(♯‘𝑡))((𝑔‘(𝑡 prefix 𝑗)) · (𝑖‘(𝑡 substr 〈𝑗, (♯‘𝑡)〉))))‘𝑣) · (𝑀 Σg 𝑣)))) = (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((ℎ‘𝑤) · (𝑀 Σg 𝑤))))) |
524 | | ovexd 7465 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) → (𝑅 Σg (𝑣 ∈ Word 𝐴 ↦ (((𝑡 ∈ Word 𝐴 ↦ Σ𝑗 ∈ (0...(♯‘𝑡))((𝑔‘(𝑡 prefix 𝑗)) · (𝑖‘(𝑡 substr 〈𝑗, (♯‘𝑡)〉))))‘𝑣) · (𝑀 Σg 𝑣)))) ∈ V) |
525 | 409, 523,
524 | elrnmptd 5976 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) → (𝑅 Σg (𝑣 ∈ Word 𝐴 ↦ (((𝑡 ∈ Word 𝐴 ↦ Σ𝑗 ∈ (0...(♯‘𝑡))((𝑔‘(𝑡 prefix 𝑗)) · (𝑖‘(𝑡 substr 〈𝑗, (♯‘𝑡)〉))))‘𝑣) · (𝑀 Σg 𝑣)))) ∈ ran (𝑔 ∈ 𝐹 ↦ (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑔‘𝑤) · (𝑀 Σg 𝑤)))))) |
526 | 525, 8 | eleqtrrdi 2849 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) → (𝑅 Σg (𝑣 ∈ Word 𝐴 ↦ (((𝑡 ∈ Word 𝐴 ↦ Σ𝑗 ∈ (0...(♯‘𝑡))((𝑔‘(𝑡 prefix 𝑗)) · (𝑖‘(𝑡 substr 〈𝑗, (♯‘𝑡)〉))))‘𝑣) · (𝑀 Σg 𝑣)))) ∈ 𝑆) |
527 | 404, 526 | eqeltrd 2838 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) → ((𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑔‘𝑤) · (𝑀 Σg 𝑤))))(.r‘𝑅)(𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑖‘𝑤) · (𝑀 Σg 𝑤))))) ∈ 𝑆) |
528 | 527 | adantllr 719 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑥 ∈ 𝑆) ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) → ((𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑔‘𝑤) · (𝑀 Σg 𝑤))))(.r‘𝑅)(𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑖‘𝑤) · (𝑀 Σg 𝑤))))) ∈ 𝑆) |
529 | 528 | adantllr 719 |
. . . . . . . . 9
⊢
(((((𝜑 ∧ 𝑥 ∈ 𝑆) ∧ 𝑦 ∈ 𝑆) ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) → ((𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑔‘𝑤) · (𝑀 Σg 𝑤))))(.r‘𝑅)(𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑖‘𝑤) · (𝑀 Σg 𝑤))))) ∈ 𝑆) |
530 | 529 | adantlr 715 |
. . . . . . . 8
⊢
((((((𝜑 ∧ 𝑥 ∈ 𝑆) ∧ 𝑦 ∈ 𝑆) ∧ 𝑔 ∈ 𝐹) ∧ 𝑥 = (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑔‘𝑤) · (𝑀 Σg 𝑤))))) ∧ 𝑖 ∈ 𝐹) → ((𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑔‘𝑤) · (𝑀 Σg 𝑤))))(.r‘𝑅)(𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑖‘𝑤) · (𝑀 Σg 𝑤))))) ∈ 𝑆) |
531 | 530 | adantr 480 |
. . . . . . 7
⊢
(((((((𝜑 ∧ 𝑥 ∈ 𝑆) ∧ 𝑦 ∈ 𝑆) ∧ 𝑔 ∈ 𝐹) ∧ 𝑥 = (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑔‘𝑤) · (𝑀 Σg 𝑤))))) ∧ 𝑖 ∈ 𝐹) ∧ 𝑦 = (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑖‘𝑤) · (𝑀 Σg 𝑤))))) → ((𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑔‘𝑤) · (𝑀 Σg 𝑤))))(.r‘𝑅)(𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑖‘𝑤) · (𝑀 Σg 𝑤))))) ∈ 𝑆) |
532 | 107, 531 | eqeltrd 2838 |
. . . . . 6
⊢
(((((((𝜑 ∧ 𝑥 ∈ 𝑆) ∧ 𝑦 ∈ 𝑆) ∧ 𝑔 ∈ 𝐹) ∧ 𝑥 = (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑔‘𝑤) · (𝑀 Σg 𝑤))))) ∧ 𝑖 ∈ 𝐹) ∧ 𝑦 = (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑖‘𝑤) · (𝑀 Σg 𝑤))))) → (𝑥(.r‘𝑅)𝑦) ∈ 𝑆) |
533 | 8 | eleq2i 2830 |
. . . . . . . . 9
⊢ (𝑦 ∈ 𝑆 ↔ 𝑦 ∈ ran (𝑔 ∈ 𝐹 ↦ (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑔‘𝑤) · (𝑀 Σg 𝑤)))))) |
534 | 169 | oveq2d 7446 |
. . . . . . . . . . . 12
⊢ (𝑔 = 𝑖 → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑔‘𝑤) · (𝑀 Σg 𝑤)))) = (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑖‘𝑤) · (𝑀 Σg 𝑤))))) |
535 | 534 | cbvmptv 5260 |
. . . . . . . . . . 11
⊢ (𝑔 ∈ 𝐹 ↦ (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑔‘𝑤) · (𝑀 Σg 𝑤))))) = (𝑖 ∈ 𝐹 ↦ (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑖‘𝑤) · (𝑀 Σg 𝑤))))) |
536 | 535 | elrnmpt 5971 |
. . . . . . . . . 10
⊢ (𝑦 ∈ V → (𝑦 ∈ ran (𝑔 ∈ 𝐹 ↦ (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑔‘𝑤) · (𝑀 Σg 𝑤))))) ↔ ∃𝑖 ∈ 𝐹 𝑦 = (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑖‘𝑤) · (𝑀 Σg 𝑤)))))) |
537 | 536 | elv 3482 |
. . . . . . . . 9
⊢ (𝑦 ∈ ran (𝑔 ∈ 𝐹 ↦ (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑔‘𝑤) · (𝑀 Σg 𝑤))))) ↔ ∃𝑖 ∈ 𝐹 𝑦 = (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑖‘𝑤) · (𝑀 Σg 𝑤))))) |
538 | 533, 537 | sylbb 219 |
. . . . . . . 8
⊢ (𝑦 ∈ 𝑆 → ∃𝑖 ∈ 𝐹 𝑦 = (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑖‘𝑤) · (𝑀 Σg 𝑤))))) |
539 | 538 | adantl 481 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑥 ∈ 𝑆) ∧ 𝑦 ∈ 𝑆) → ∃𝑖 ∈ 𝐹 𝑦 = (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑖‘𝑤) · (𝑀 Σg 𝑤))))) |
540 | 539 | ad2antrr 726 |
. . . . . 6
⊢
(((((𝜑 ∧ 𝑥 ∈ 𝑆) ∧ 𝑦 ∈ 𝑆) ∧ 𝑔 ∈ 𝐹) ∧ 𝑥 = (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑔‘𝑤) · (𝑀 Σg 𝑤))))) → ∃𝑖 ∈ 𝐹 𝑦 = (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑖‘𝑤) · (𝑀 Σg 𝑤))))) |
541 | 532, 540 | r19.29a 3159 |
. . . . 5
⊢
(((((𝜑 ∧ 𝑥 ∈ 𝑆) ∧ 𝑦 ∈ 𝑆) ∧ 𝑔 ∈ 𝐹) ∧ 𝑥 = (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑔‘𝑤) · (𝑀 Σg 𝑤))))) → (𝑥(.r‘𝑅)𝑦) ∈ 𝑆) |
542 | 8 | eleq2i 2830 |
. . . . . . 7
⊢ (𝑥 ∈ 𝑆 ↔ 𝑥 ∈ ran (𝑔 ∈ 𝐹 ↦ (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑔‘𝑤) · (𝑀 Σg 𝑤)))))) |
543 | 71 | elrnmpt 5971 |
. . . . . . . 8
⊢ (𝑥 ∈ V → (𝑥 ∈ ran (𝑔 ∈ 𝐹 ↦ (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑔‘𝑤) · (𝑀 Σg 𝑤))))) ↔ ∃𝑔 ∈ 𝐹 𝑥 = (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑔‘𝑤) · (𝑀 Σg 𝑤)))))) |
544 | 543 | elv 3482 |
. . . . . . 7
⊢ (𝑥 ∈ ran (𝑔 ∈ 𝐹 ↦ (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑔‘𝑤) · (𝑀 Σg 𝑤))))) ↔ ∃𝑔 ∈ 𝐹 𝑥 = (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑔‘𝑤) · (𝑀 Σg 𝑤))))) |
545 | 542, 544 | sylbb 219 |
. . . . . 6
⊢ (𝑥 ∈ 𝑆 → ∃𝑔 ∈ 𝐹 𝑥 = (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑔‘𝑤) · (𝑀 Σg 𝑤))))) |
546 | 545 | ad2antlr 727 |
. . . . 5
⊢ (((𝜑 ∧ 𝑥 ∈ 𝑆) ∧ 𝑦 ∈ 𝑆) → ∃𝑔 ∈ 𝐹 𝑥 = (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑔‘𝑤) · (𝑀 Σg 𝑤))))) |
547 | 541, 546 | r19.29a 3159 |
. . . 4
⊢ (((𝜑 ∧ 𝑥 ∈ 𝑆) ∧ 𝑦 ∈ 𝑆) → (𝑥(.r‘𝑅)𝑦) ∈ 𝑆) |
548 | 547 | anasss 466 |
. . 3
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆)) → (𝑥(.r‘𝑅)𝑦) ∈ 𝑆) |
549 | 548 | ralrimivva 3199 |
. 2
⊢ (𝜑 → ∀𝑥 ∈ 𝑆 ∀𝑦 ∈ 𝑆 (𝑥(.r‘𝑅)𝑦) ∈ 𝑆) |
550 | 2, 24, 108 | issubrg2 20608 |
. . 3
⊢ (𝑅 ∈ Ring → (𝑆 ∈ (SubRing‘𝑅) ↔ (𝑆 ∈ (SubGrp‘𝑅) ∧ (1r‘𝑅) ∈ 𝑆 ∧ ∀𝑥 ∈ 𝑆 ∀𝑦 ∈ 𝑆 (𝑥(.r‘𝑅)𝑦) ∈ 𝑆))) |
551 | 550 | biimpar 477 |
. 2
⊢ ((𝑅 ∈ Ring ∧ (𝑆 ∈ (SubGrp‘𝑅) ∧
(1r‘𝑅)
∈ 𝑆 ∧
∀𝑥 ∈ 𝑆 ∀𝑦 ∈ 𝑆 (𝑥(.r‘𝑅)𝑦) ∈ 𝑆)) → 𝑆 ∈ (SubRing‘𝑅)) |
552 | 1, 9, 104, 549, 551 | syl13anc 1371 |
1
⊢ (𝜑 → 𝑆 ∈ (SubRing‘𝑅)) |