| 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 33246 |
. 2
⊢ (𝜑 → 𝑆 ∈ (SubGrp‘𝑅)) |
| 10 | | eqeq2 2749 |
. . . . . . 7
⊢
((1r‘𝑅) = if(𝑤 = ∅, (1r‘𝑅), (0g‘𝑅)) → ((((𝑣 ∈ Word 𝐴 ↦ if(𝑣 = ∅, 1, 0))‘𝑤) · (𝑀 Σg 𝑤)) = (1r‘𝑅) ↔ (((𝑣 ∈ Word 𝐴 ↦ if(𝑣 = ∅, 1, 0))‘𝑤) · (𝑀 Σg 𝑤)) = if(𝑤 = ∅, (1r‘𝑅), (0g‘𝑅)))) |
| 11 | | eqeq2 2749 |
. . . . . . 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 2737 |
. . . . . . . . . . . 12
⊢ (𝑣 ∈ Word 𝐴 ↦ if(𝑣 = ∅, 1, 0)) = (𝑣 ∈ Word 𝐴 ↦ if(𝑣 = ∅, 1, 0)) |
| 15 | | simpr 484 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑣 = ∅) → 𝑣 = ∅) |
| 16 | 15 | iftrued 4533 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑣 = ∅) → if(𝑣 = ∅, 1, 0) = 1) |
| 17 | | wrd0 14577 |
. . . . . . . . . . . . 13
⊢ ∅
∈ Word 𝐴 |
| 18 | 17 | a1i 11 |
. . . . . . . . . . . 12
⊢ (𝜑 → ∅ ∈ Word 𝐴) |
| 19 | | 1zzd 12648 |
. . . . . . . . . . . 12
⊢ (𝜑 → 1 ∈
ℤ) |
| 20 | 14, 16, 18, 19 | fvmptd2 7024 |
. . . . . . . . . . 11
⊢ (𝜑 → ((𝑣 ∈ Word 𝐴 ↦ if(𝑣 = ∅, 1, 0))‘∅) =
1) |
| 21 | 20 | ad2antrr 726 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑤 ∈ Word 𝐴) ∧ 𝑤 = ∅) → ((𝑣 ∈ Word 𝐴 ↦ if(𝑣 = ∅, 1, 0))‘∅) =
1) |
| 22 | 13, 21 | eqtrd 2777 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑤 ∈ Word 𝐴) ∧ 𝑤 = ∅) → ((𝑣 ∈ Word 𝐴 ↦ if(𝑣 = ∅, 1, 0))‘𝑤) = 1) |
| 23 | 12 | oveq2d 7447 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑤 ∈ Word 𝐴) ∧ 𝑤 = ∅) → (𝑀 Σg 𝑤) = (𝑀 Σg
∅)) |
| 24 | | eqid 2737 |
. . . . . . . . . . . 12
⊢
(1r‘𝑅) = (1r‘𝑅) |
| 25 | 3, 24 | ringidval 20180 |
. . . . . . . . . . 11
⊢
(1r‘𝑅) = (0g‘𝑀) |
| 26 | 25 | gsum0 18697 |
. . . . . . . . . 10
⊢ (𝑀 Σg
∅) = (1r‘𝑅) |
| 27 | 23, 26 | eqtrdi 2793 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑤 ∈ Word 𝐴) ∧ 𝑤 = ∅) → (𝑀 Σg 𝑤) = (1r‘𝑅)) |
| 28 | 22, 27 | oveq12d 7449 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑤 ∈ Word 𝐴) ∧ 𝑤 = ∅) → (((𝑣 ∈ Word 𝐴 ↦ if(𝑣 = ∅, 1, 0))‘𝑤) · (𝑀 Σg 𝑤)) = (1 ·
(1r‘𝑅))) |
| 29 | 2, 24 | ringidcl 20262 |
. . . . . . . . . . 11
⊢ (𝑅 ∈ Ring →
(1r‘𝑅)
∈ 𝐵) |
| 30 | 1, 29 | syl 17 |
. . . . . . . . . 10
⊢ (𝜑 → (1r‘𝑅) ∈ 𝐵) |
| 31 | 2, 4 | mulg1 19099 |
. . . . . . . . . 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 2777 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑤 ∈ Word 𝐴) ∧ 𝑤 = ∅) → (((𝑣 ∈ Word 𝐴 ↦ if(𝑣 = ∅, 1, 0))‘𝑤) · (𝑀 Σg 𝑤)) = (1r‘𝑅)) |
| 35 | | eqeq1 2741 |
. . . . . . . . . . . . . 14
⊢ (𝑣 = 𝑤 → (𝑣 = ∅ ↔ 𝑤 = ∅)) |
| 36 | 35 | notbid 318 |
. . . . . . . . . . . . 13
⊢ (𝑣 = 𝑤 → (¬ 𝑣 = ∅ ↔ ¬ 𝑤 = ∅)) |
| 37 | 36 | biimparc 479 |
. . . . . . . . . . . 12
⊢ ((¬
𝑤 = ∅ ∧ 𝑣 = 𝑤) → ¬ 𝑣 = ∅) |
| 38 | 37 | adantll 714 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑤 ∈ Word 𝐴) ∧ ¬ 𝑤 = ∅) ∧ 𝑣 = 𝑤) → ¬ 𝑣 = ∅) |
| 39 | 38 | iffalsed 4536 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑤 ∈ Word 𝐴) ∧ ¬ 𝑤 = ∅) ∧ 𝑣 = 𝑤) → if(𝑣 = ∅, 1, 0) = 0) |
| 40 | | simplr 769 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑤 ∈ Word 𝐴) ∧ ¬ 𝑤 = ∅) → 𝑤 ∈ Word 𝐴) |
| 41 | | 0zd 12625 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑤 ∈ Word 𝐴) ∧ ¬ 𝑤 = ∅) → 0 ∈
ℤ) |
| 42 | 14, 39, 40, 41 | fvmptd2 7024 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑤 ∈ Word 𝐴) ∧ ¬ 𝑤 = ∅) → ((𝑣 ∈ Word 𝐴 ↦ if(𝑣 = ∅, 1, 0))‘𝑤) = 0) |
| 43 | 42 | oveq1d 7446 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑤 ∈ Word 𝐴) ∧ ¬ 𝑤 = ∅) → (((𝑣 ∈ Word 𝐴 ↦ if(𝑣 = ∅, 1, 0))‘𝑤) · (𝑀 Σg 𝑤)) = (0 · (𝑀 Σg 𝑤))) |
| 44 | 3 | ringmgp 20236 |
. . . . . . . . . . . 12
⊢ (𝑅 ∈ Ring → 𝑀 ∈ Mnd) |
| 45 | 1, 44 | syl 17 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝑀 ∈ Mnd) |
| 46 | | sswrd 14560 |
. . . . . . . . . . . . 13
⊢ (𝐴 ⊆ 𝐵 → Word 𝐴 ⊆ Word 𝐵) |
| 47 | 7, 46 | syl 17 |
. . . . . . . . . . . 12
⊢ (𝜑 → Word 𝐴 ⊆ Word 𝐵) |
| 48 | 47 | sselda 3983 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑤 ∈ Word 𝐴) → 𝑤 ∈ Word 𝐵) |
| 49 | 3, 2 | mgpbas 20142 |
. . . . . . . . . . . 12
⊢ 𝐵 = (Base‘𝑀) |
| 50 | 49 | gsumwcl 18852 |
. . . . . . . . . . 11
⊢ ((𝑀 ∈ Mnd ∧ 𝑤 ∈ Word 𝐵) → (𝑀 Σg 𝑤) ∈ 𝐵) |
| 51 | 45, 48, 50 | syl2an2r 685 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑤 ∈ Word 𝐴) → (𝑀 Σg 𝑤) ∈ 𝐵) |
| 52 | | eqid 2737 |
. . . . . . . . . . 11
⊢
(0g‘𝑅) = (0g‘𝑅) |
| 53 | 2, 52, 4 | mulg0 19092 |
. . . . . . . . . 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 2777 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑤 ∈ Word 𝐴) ∧ ¬ 𝑤 = ∅) → (((𝑣 ∈ Word 𝐴 ↦ if(𝑣 = ∅, 1, 0))‘𝑤) · (𝑀 Σg 𝑤)) = (0g‘𝑅)) |
| 57 | 10, 11, 34, 56 | ifbothda 4564 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑤 ∈ Word 𝐴) → (((𝑣 ∈ Word 𝐴 ↦ if(𝑣 = ∅, 1, 0))‘𝑤) · (𝑀 Σg 𝑤)) = if(𝑤 = ∅, (1r‘𝑅), (0g‘𝑅))) |
| 58 | 57 | mpteq2dva 5242 |
. . . . 5
⊢ (𝜑 → (𝑤 ∈ Word 𝐴 ↦ (((𝑣 ∈ Word 𝐴 ↦ if(𝑣 = ∅, 1, 0))‘𝑤) · (𝑀 Σg 𝑤))) = (𝑤 ∈ Word 𝐴 ↦ if(𝑤 = ∅, (1r‘𝑅), (0g‘𝑅)))) |
| 59 | 58 | oveq2d 7447 |
. . . 4
⊢ (𝜑 → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ (((𝑣 ∈ Word 𝐴 ↦ if(𝑣 = ∅, 1, 0))‘𝑤) · (𝑀 Σg 𝑤)))) = (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ if(𝑤 = ∅, (1r‘𝑅), (0g‘𝑅))))) |
| 60 | 1 | ringcmnd 20281 |
. . . . . 6
⊢ (𝜑 → 𝑅 ∈ CMnd) |
| 61 | 60 | cmnmndd 19822 |
. . . . 5
⊢ (𝜑 → 𝑅 ∈ Mnd) |
| 62 | 2 | fvexi 6920 |
. . . . . . . 8
⊢ 𝐵 ∈ V |
| 63 | 62 | a1i 11 |
. . . . . . 7
⊢ (𝜑 → 𝐵 ∈ V) |
| 64 | 63, 7 | ssexd 5324 |
. . . . . 6
⊢ (𝜑 → 𝐴 ∈ V) |
| 65 | | wrdexg 14562 |
. . . . . 6
⊢ (𝐴 ∈ V → Word 𝐴 ∈ V) |
| 66 | 64, 65 | syl 17 |
. . . . 5
⊢ (𝜑 → Word 𝐴 ∈ V) |
| 67 | | eqid 2737 |
. . . . 5
⊢ (𝑤 ∈ Word 𝐴 ↦ if(𝑤 = ∅, (1r‘𝑅), (0g‘𝑅))) = (𝑤 ∈ Word 𝐴 ↦ if(𝑤 = ∅, (1r‘𝑅), (0g‘𝑅))) |
| 68 | 30, 2 | eleqtrdi 2851 |
. . . . 5
⊢ (𝜑 → (1r‘𝑅) ∈ (Base‘𝑅)) |
| 69 | 52, 61, 66, 18, 67, 68 | gsummptif1n0 19984 |
. . . 4
⊢ (𝜑 → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ if(𝑤 = ∅, (1r‘𝑅), (0g‘𝑅)))) =
(1r‘𝑅)) |
| 70 | 59, 69 | eqtrd 2777 |
. . 3
⊢ (𝜑 → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ (((𝑣 ∈ Word 𝐴 ↦ if(𝑣 = ∅, 1, 0))‘𝑤) · (𝑀 Σg 𝑤)))) =
(1r‘𝑅)) |
| 71 | | eqid 2737 |
. . . . 5
⊢ (𝑔 ∈ 𝐹 ↦ (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑔‘𝑤) · (𝑀 Σg 𝑤))))) = (𝑔 ∈ 𝐹 ↦ (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑔‘𝑤) · (𝑀 Σg 𝑤))))) |
| 72 | | fveq1 6905 |
. . . . . . . . . 10
⊢ (𝑔 = (𝑣 ∈ Word 𝐴 ↦ if(𝑣 = ∅, 1, 0)) → (𝑔‘𝑤) = ((𝑣 ∈ Word 𝐴 ↦ if(𝑣 = ∅, 1, 0))‘𝑤)) |
| 73 | 72 | oveq1d 7446 |
. . . . . . . . 9
⊢ (𝑔 = (𝑣 ∈ Word 𝐴 ↦ if(𝑣 = ∅, 1, 0)) → ((𝑔‘𝑤) · (𝑀 Σg 𝑤)) = (((𝑣 ∈ Word 𝐴 ↦ if(𝑣 = ∅, 1, 0))‘𝑤) · (𝑀 Σg 𝑤))) |
| 74 | 73 | mpteq2dv 5244 |
. . . . . . . 8
⊢ (𝑔 = (𝑣 ∈ Word 𝐴 ↦ if(𝑣 = ∅, 1, 0)) → (𝑤 ∈ Word 𝐴 ↦ ((𝑔‘𝑤) · (𝑀 Σg 𝑤))) = (𝑤 ∈ Word 𝐴 ↦ (((𝑣 ∈ Word 𝐴 ↦ if(𝑣 = ∅, 1, 0))‘𝑤) · (𝑀 Σg 𝑤)))) |
| 75 | 74 | oveq2d 7447 |
. . . . . . 7
⊢ (𝑔 = (𝑣 ∈ Word 𝐴 ↦ if(𝑣 = ∅, 1, 0)) → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑔‘𝑤) · (𝑀 Σg 𝑤)))) = (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ (((𝑣 ∈ Word 𝐴 ↦ if(𝑣 = ∅, 1, 0))‘𝑤) · (𝑀 Σg 𝑤))))) |
| 76 | 75 | eqeq2d 2748 |
. . . . . 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 5146 |
. . . . . . . 8
⊢ (𝑓 = (𝑣 ∈ Word 𝐴 ↦ if(𝑣 = ∅, 1, 0)) → (𝑓 finSupp 0 ↔ (𝑣 ∈ Word 𝐴 ↦ if(𝑣 = ∅, 1, 0)) finSupp
0)) |
| 78 | | zex 12622 |
. . . . . . . . . 10
⊢ ℤ
∈ V |
| 79 | 78 | a1i 11 |
. . . . . . . . 9
⊢ (𝜑 → ℤ ∈
V) |
| 80 | | 1zzd 12648 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑣 ∈ Word 𝐴) ∧ 𝑣 = ∅) → 1 ∈
ℤ) |
| 81 | | 0zd 12625 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑣 ∈ Word 𝐴) ∧ ¬ 𝑣 = ∅) → 0 ∈
ℤ) |
| 82 | 80, 81 | ifclda 4561 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑣 ∈ Word 𝐴) → if(𝑣 = ∅, 1, 0) ∈
ℤ) |
| 83 | 82 | fmpttd 7135 |
. . . . . . . . 9
⊢ (𝜑 → (𝑣 ∈ Word 𝐴 ↦ if(𝑣 = ∅, 1, 0)):Word 𝐴⟶ℤ) |
| 84 | 79, 66, 83 | elmapdd 8881 |
. . . . . . . 8
⊢ (𝜑 → (𝑣 ∈ Word 𝐴 ↦ if(𝑣 = ∅, 1, 0)) ∈ (ℤ
↑m Word 𝐴)) |
| 85 | 66 | mptexd 7244 |
. . . . . . . . 9
⊢ (𝜑 → (𝑣 ∈ Word 𝐴 ↦ if(𝑣 = ∅, 1, 0)) ∈ V) |
| 86 | 83 | ffund 6740 |
. . . . . . . . 9
⊢ (𝜑 → Fun (𝑣 ∈ Word 𝐴 ↦ if(𝑣 = ∅, 1, 0))) |
| 87 | | 0zd 12625 |
. . . . . . . . 9
⊢ (𝜑 → 0 ∈
ℤ) |
| 88 | | snfi 9083 |
. . . . . . . . . 10
⊢ {∅}
∈ Fin |
| 89 | 88 | a1i 11 |
. . . . . . . . 9
⊢ (𝜑 → {∅} ∈
Fin) |
| 90 | | eldifsni 4790 |
. . . . . . . . . . . . 13
⊢ (𝑣 ∈ (Word 𝐴 ∖ {∅}) → 𝑣 ≠ ∅) |
| 91 | 90 | adantl 481 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑣 ∈ (Word 𝐴 ∖ {∅})) → 𝑣 ≠ ∅) |
| 92 | 91 | neneqd 2945 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑣 ∈ (Word 𝐴 ∖ {∅})) → ¬ 𝑣 = ∅) |
| 93 | 92 | iffalsed 4536 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑣 ∈ (Word 𝐴 ∖ {∅})) → if(𝑣 = ∅, 1, 0) =
0) |
| 94 | 93, 66 | suppss2 8225 |
. . . . . . . . 9
⊢ (𝜑 → ((𝑣 ∈ Word 𝐴 ↦ if(𝑣 = ∅, 1, 0)) supp 0) ⊆
{∅}) |
| 95 | | suppssfifsupp 9420 |
. . . . . . . . 9
⊢ ((((𝑣 ∈ Word 𝐴 ↦ if(𝑣 = ∅, 1, 0)) ∈ V ∧ Fun (𝑣 ∈ Word 𝐴 ↦ if(𝑣 = ∅, 1, 0)) ∧ 0 ∈ ℤ)
∧ ({∅} ∈ Fin ∧ ((𝑣 ∈ Word 𝐴 ↦ if(𝑣 = ∅, 1, 0)) supp 0) ⊆
{∅})) → (𝑣
∈ Word 𝐴 ↦
if(𝑣 = ∅, 1, 0))
finSupp 0) |
| 96 | 85, 86, 87, 89, 94, 95 | syl32anc 1380 |
. . . . . . . 8
⊢ (𝜑 → (𝑣 ∈ Word 𝐴 ↦ if(𝑣 = ∅, 1, 0)) finSupp
0) |
| 97 | 77, 84, 96 | elrabd 3694 |
. . . . . . 7
⊢ (𝜑 → (𝑣 ∈ Word 𝐴 ↦ if(𝑣 = ∅, 1, 0)) ∈ {𝑓 ∈ (ℤ ↑m Word
𝐴) ∣ 𝑓 finSupp 0}) |
| 98 | 97, 6 | eleqtrrdi 2852 |
. . . . . 6
⊢ (𝜑 → (𝑣 ∈ Word 𝐴 ↦ if(𝑣 = ∅, 1, 0)) ∈ 𝐹) |
| 99 | | eqidd 2738 |
. . . . . 6
⊢ (𝜑 → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ (((𝑣 ∈ Word 𝐴 ↦ if(𝑣 = ∅, 1, 0))‘𝑤) · (𝑀 Σg 𝑤)))) = (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ (((𝑣 ∈ Word 𝐴 ↦ if(𝑣 = ∅, 1, 0))‘𝑤) · (𝑀 Σg 𝑤))))) |
| 100 | 76, 98, 99 | rspcedvdw 3625 |
. . . . 5
⊢ (𝜑 → ∃𝑔 ∈ 𝐹 (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ (((𝑣 ∈ Word 𝐴 ↦ if(𝑣 = ∅, 1, 0))‘𝑤) · (𝑀 Σg 𝑤)))) = (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑔‘𝑤) · (𝑀 Σg 𝑤))))) |
| 101 | | ovexd 7466 |
. . . . 5
⊢ (𝜑 → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ (((𝑣 ∈ Word 𝐴 ↦ if(𝑣 = ∅, 1, 0))‘𝑤) · (𝑀 Σg 𝑤)))) ∈ V) |
| 102 | 71, 100, 101 | elrnmptd 5974 |
. . . 4
⊢ (𝜑 → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ (((𝑣 ∈ Word 𝐴 ↦ if(𝑣 = ∅, 1, 0))‘𝑤) · (𝑀 Σg 𝑤)))) ∈ ran (𝑔 ∈ 𝐹 ↦ (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑔‘𝑤) · (𝑀 Σg 𝑤)))))) |
| 103 | 102, 8 | eleqtrrdi 2852 |
. . 3
⊢ (𝜑 → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ (((𝑣 ∈ Word 𝐴 ↦ if(𝑣 = ∅, 1, 0))‘𝑤) · (𝑀 Σg 𝑤)))) ∈ 𝑆) |
| 104 | 70, 103 | eqeltrrd 2842 |
. 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 7449 |
. . . . . . 7
⊢
(((((((𝜑 ∧ 𝑥 ∈ 𝑆) ∧ 𝑦 ∈ 𝑆) ∧ 𝑔 ∈ 𝐹) ∧ 𝑥 = (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑔‘𝑤) · (𝑀 Σg 𝑤))))) ∧ 𝑖 ∈ 𝐹) ∧ 𝑦 = (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑖‘𝑤) · (𝑀 Σg 𝑤))))) → (𝑥(.r‘𝑅)𝑦) = ((𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑔‘𝑤) · (𝑀 Σg 𝑤))))(.r‘𝑅)(𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑖‘𝑤) · (𝑀 Σg 𝑤)))))) |
| 108 | | eqid 2737 |
. . . . . . . . . . . . . 14
⊢
(.r‘𝑅) = (.r‘𝑅) |
| 109 | 66 | ad2antrr 726 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) → Word 𝐴 ∈ V) |
| 110 | 1 | ad2antrr 726 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) → 𝑅 ∈ Ring) |
| 111 | 1 | ringgrpd 20239 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → 𝑅 ∈ Grp) |
| 112 | 111 | ad2antrr 726 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑤 ∈ Word 𝐴) → 𝑅 ∈ Grp) |
| 113 | 6 | ssrab3 4082 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ 𝐹 ⊆ (ℤ
↑m Word 𝐴) |
| 114 | 113 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝜑 → 𝐹 ⊆ (ℤ ↑m Word
𝐴)) |
| 115 | 114 | sselda 3983 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝜑 ∧ 𝑔 ∈ 𝐹) → 𝑔 ∈ (ℤ ↑m Word
𝐴)) |
| 116 | 79, 66 | elmapd 8880 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝜑 → (𝑔 ∈ (ℤ ↑m Word
𝐴) ↔ 𝑔:Word 𝐴⟶ℤ)) |
| 117 | 116 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝜑 ∧ 𝑔 ∈ 𝐹) → (𝑔 ∈ (ℤ ↑m Word
𝐴) ↔ 𝑔:Word 𝐴⟶ℤ)) |
| 118 | 115, 117 | mpbid 232 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ 𝑔 ∈ 𝐹) → 𝑔:Word 𝐴⟶ℤ) |
| 119 | 118 | ffvelcdmda 7104 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑤 ∈ Word 𝐴) → (𝑔‘𝑤) ∈ ℤ) |
| 120 | 51 | adantlr 715 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑤 ∈ Word 𝐴) → (𝑀 Σg 𝑤) ∈ 𝐵) |
| 121 | 2, 4, 112, 119, 120 | mulgcld 19114 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑤 ∈ Word 𝐴) → ((𝑔‘𝑤) · (𝑀 Σg 𝑤)) ∈ 𝐵) |
| 122 | 121 | adantlr 715 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑤 ∈ Word 𝐴) → ((𝑔‘𝑤) · (𝑀 Σg 𝑤)) ∈ 𝐵) |
| 123 | 122 | ralrimiva 3146 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) → ∀𝑤 ∈ Word 𝐴((𝑔‘𝑤) · (𝑀 Σg 𝑤)) ∈ 𝐵) |
| 124 | | fveq2 6906 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑢 = 𝑤 → (𝑔‘𝑢) = (𝑔‘𝑤)) |
| 125 | | oveq2 7439 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑢 = 𝑤 → (𝑀 Σg 𝑢) = (𝑀 Σg 𝑤)) |
| 126 | 124, 125 | oveq12d 7449 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑢 = 𝑤 → ((𝑔‘𝑢) · (𝑀 Σg 𝑢)) = ((𝑔‘𝑤) · (𝑀 Σg 𝑤))) |
| 127 | 126 | eleq1d 2826 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑢 = 𝑤 → (((𝑔‘𝑢) · (𝑀 Σg 𝑢)) ∈ 𝐵 ↔ ((𝑔‘𝑤) · (𝑀 Σg 𝑤)) ∈ 𝐵)) |
| 128 | 127 | cbvralvw 3237 |
. . . . . . . . . . . . . . . 16
⊢
(∀𝑢 ∈
Word 𝐴((𝑔‘𝑢) · (𝑀 Σg 𝑢)) ∈ 𝐵 ↔ ∀𝑤 ∈ Word 𝐴((𝑔‘𝑤) · (𝑀 Σg 𝑤)) ∈ 𝐵) |
| 129 | 123, 128 | sylibr 234 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) → ∀𝑢 ∈ Word 𝐴((𝑔‘𝑢) · (𝑀 Σg 𝑢)) ∈ 𝐵) |
| 130 | 129 | r19.21bi 3251 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑢 ∈ Word 𝐴) → ((𝑔‘𝑢) · (𝑀 Σg 𝑢)) ∈ 𝐵) |
| 131 | 111 | ad2antrr 726 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝑖 ∈ 𝐹) ∧ 𝑤 ∈ Word 𝐴) → 𝑅 ∈ Grp) |
| 132 | | breq1 5146 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑓 = 𝑖 → (𝑓 finSupp 0 ↔ 𝑖 finSupp 0)) |
| 133 | 132, 6 | elrab2 3695 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑖 ∈ 𝐹 ↔ (𝑖 ∈ (ℤ ↑m Word
𝐴) ∧ 𝑖 finSupp 0)) |
| 134 | 133 | simplbi 497 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑖 ∈ 𝐹 → 𝑖 ∈ (ℤ ↑m Word
𝐴)) |
| 135 | 134 | adantl 481 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝜑 ∧ 𝑖 ∈ 𝐹) → 𝑖 ∈ (ℤ ↑m Word
𝐴)) |
| 136 | 79, 66 | elmapd 8880 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝜑 → (𝑖 ∈ (ℤ ↑m Word
𝐴) ↔ 𝑖:Word 𝐴⟶ℤ)) |
| 137 | 136 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝜑 ∧ 𝑖 ∈ 𝐹) → (𝑖 ∈ (ℤ ↑m Word
𝐴) ↔ 𝑖:Word 𝐴⟶ℤ)) |
| 138 | 135, 137 | mpbid 232 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ 𝑖 ∈ 𝐹) → 𝑖:Word 𝐴⟶ℤ) |
| 139 | 138 | ffvelcdmda 7104 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝑖 ∈ 𝐹) ∧ 𝑤 ∈ Word 𝐴) → (𝑖‘𝑤) ∈ ℤ) |
| 140 | 51 | adantlr 715 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝑖 ∈ 𝐹) ∧ 𝑤 ∈ Word 𝐴) → (𝑀 Σg 𝑤) ∈ 𝐵) |
| 141 | 2, 4, 131, 139, 140 | mulgcld 19114 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑖 ∈ 𝐹) ∧ 𝑤 ∈ Word 𝐴) → ((𝑖‘𝑤) · (𝑀 Σg 𝑤)) ∈ 𝐵) |
| 142 | 141 | adantllr 719 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑤 ∈ Word 𝐴) → ((𝑖‘𝑤) · (𝑀 Σg 𝑤)) ∈ 𝐵) |
| 143 | 142 | ralrimiva 3146 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) → ∀𝑤 ∈ Word 𝐴((𝑖‘𝑤) · (𝑀 Σg 𝑤)) ∈ 𝐵) |
| 144 | | fveq2 6906 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑣 = 𝑤 → (𝑖‘𝑣) = (𝑖‘𝑤)) |
| 145 | | oveq2 7439 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑣 = 𝑤 → (𝑀 Σg 𝑣) = (𝑀 Σg 𝑤)) |
| 146 | 144, 145 | oveq12d 7449 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑣 = 𝑤 → ((𝑖‘𝑣) · (𝑀 Σg 𝑣)) = ((𝑖‘𝑤) · (𝑀 Σg 𝑤))) |
| 147 | 146 | eleq1d 2826 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑣 = 𝑤 → (((𝑖‘𝑣) · (𝑀 Σg 𝑣)) ∈ 𝐵 ↔ ((𝑖‘𝑤) · (𝑀 Σg 𝑤)) ∈ 𝐵)) |
| 148 | 147 | cbvralvw 3237 |
. . . . . . . . . . . . . . . 16
⊢
(∀𝑣 ∈
Word 𝐴((𝑖‘𝑣) · (𝑀 Σg 𝑣)) ∈ 𝐵 ↔ ∀𝑤 ∈ Word 𝐴((𝑖‘𝑤) · (𝑀 Σg 𝑤)) ∈ 𝐵) |
| 149 | 143, 148 | sylibr 234 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) → ∀𝑣 ∈ Word 𝐴((𝑖‘𝑣) · (𝑀 Σg 𝑣)) ∈ 𝐵) |
| 150 | 149 | r19.21bi 3251 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑣 ∈ Word 𝐴) → ((𝑖‘𝑣) · (𝑀 Σg 𝑣)) ∈ 𝐵) |
| 151 | 126 | cbvmptv 5255 |
. . . . . . . . . . . . . . 15
⊢ (𝑢 ∈ Word 𝐴 ↦ ((𝑔‘𝑢) · (𝑀 Σg 𝑢))) = (𝑤 ∈ Word 𝐴 ↦ ((𝑔‘𝑤) · (𝑀 Σg 𝑤))) |
| 152 | | fvexd 6921 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑔 ∈ 𝐹) → (0g‘𝑅) ∈ V) |
| 153 | | 0zd 12625 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑔 ∈ 𝐹) → 0 ∈ ℤ) |
| 154 | 66 | adantr 480 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑔 ∈ 𝐹) → Word 𝐴 ∈ V) |
| 155 | | ssidd 4007 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑔 ∈ 𝐹) → Word 𝐴 ⊆ Word 𝐴) |
| 156 | | breq1 5146 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑓 = 𝑔 → (𝑓 finSupp 0 ↔ 𝑔 finSupp 0)) |
| 157 | 156, 6 | elrab2 3695 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑔 ∈ 𝐹 ↔ (𝑔 ∈ (ℤ ↑m Word
𝐴) ∧ 𝑔 finSupp 0)) |
| 158 | 157 | simprbi 496 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑔 ∈ 𝐹 → 𝑔 finSupp 0) |
| 159 | 158 | adantl 481 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑔 ∈ 𝐹) → 𝑔 finSupp 0) |
| 160 | 2, 52, 4 | mulg0 19092 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑦 ∈ 𝐵 → (0 · 𝑦) = (0g‘𝑅)) |
| 161 | 160 | adantl 481 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑦 ∈ 𝐵) → (0 · 𝑦) = (0g‘𝑅)) |
| 162 | 152, 153,
154, 155, 120, 118, 159, 161 | fisuppov1 32692 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑔 ∈ 𝐹) → (𝑤 ∈ Word 𝐴 ↦ ((𝑔‘𝑤) · (𝑀 Σg 𝑤))) finSupp
(0g‘𝑅)) |
| 163 | 162 | adantr 480 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) → (𝑤 ∈ Word 𝐴 ↦ ((𝑔‘𝑤) · (𝑀 Σg 𝑤))) finSupp
(0g‘𝑅)) |
| 164 | 151, 163 | eqbrtrid 5178 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) → (𝑢 ∈ Word 𝐴 ↦ ((𝑔‘𝑢) · (𝑀 Σg 𝑢))) finSupp
(0g‘𝑅)) |
| 165 | 146 | cbvmptv 5255 |
. . . . . . . . . . . . . . 15
⊢ (𝑣 ∈ Word 𝐴 ↦ ((𝑖‘𝑣) · (𝑀 Σg 𝑣))) = (𝑤 ∈ Word 𝐴 ↦ ((𝑖‘𝑤) · (𝑀 Σg 𝑤))) |
| 166 | 162 | ralrimiva 3146 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → ∀𝑔 ∈ 𝐹 (𝑤 ∈ Word 𝐴 ↦ ((𝑔‘𝑤) · (𝑀 Σg 𝑤))) finSupp
(0g‘𝑅)) |
| 167 | | fveq1 6905 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑔 = 𝑖 → (𝑔‘𝑤) = (𝑖‘𝑤)) |
| 168 | 167 | oveq1d 7446 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑔 = 𝑖 → ((𝑔‘𝑤) · (𝑀 Σg 𝑤)) = ((𝑖‘𝑤) · (𝑀 Σg 𝑤))) |
| 169 | 168 | mpteq2dv 5244 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑔 = 𝑖 → (𝑤 ∈ Word 𝐴 ↦ ((𝑔‘𝑤) · (𝑀 Σg 𝑤))) = (𝑤 ∈ Word 𝐴 ↦ ((𝑖‘𝑤) · (𝑀 Σg 𝑤)))) |
| 170 | 169 | breq1d 5153 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑔 = 𝑖 → ((𝑤 ∈ Word 𝐴 ↦ ((𝑔‘𝑤) · (𝑀 Σg 𝑤))) finSupp
(0g‘𝑅)
↔ (𝑤 ∈ Word 𝐴 ↦ ((𝑖‘𝑤) · (𝑀 Σg 𝑤))) finSupp
(0g‘𝑅))) |
| 171 | 170 | cbvralvw 3237 |
. . . . . . . . . . . . . . . . . 18
⊢
(∀𝑔 ∈
𝐹 (𝑤 ∈ Word 𝐴 ↦ ((𝑔‘𝑤) · (𝑀 Σg 𝑤))) finSupp
(0g‘𝑅)
↔ ∀𝑖 ∈
𝐹 (𝑤 ∈ Word 𝐴 ↦ ((𝑖‘𝑤) · (𝑀 Σg 𝑤))) finSupp
(0g‘𝑅)) |
| 172 | 166, 171 | sylib 218 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → ∀𝑖 ∈ 𝐹 (𝑤 ∈ Word 𝐴 ↦ ((𝑖‘𝑤) · (𝑀 Σg 𝑤))) finSupp
(0g‘𝑅)) |
| 173 | 172 | r19.21bi 3251 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑖 ∈ 𝐹) → (𝑤 ∈ Word 𝐴 ↦ ((𝑖‘𝑤) · (𝑀 Σg 𝑤))) finSupp
(0g‘𝑅)) |
| 174 | 173 | adantlr 715 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) → (𝑤 ∈ Word 𝐴 ↦ ((𝑖‘𝑤) · (𝑀 Σg 𝑤))) finSupp
(0g‘𝑅)) |
| 175 | 165, 174 | eqbrtrid 5178 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) → (𝑣 ∈ Word 𝐴 ↦ ((𝑖‘𝑣) · (𝑀 Σg 𝑣))) finSupp
(0g‘𝑅)) |
| 176 | 2, 108, 52, 109, 109, 110, 130, 150, 164, 175 | gsumdixp 20316 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) → ((𝑅 Σg (𝑢 ∈ Word 𝐴 ↦ ((𝑔‘𝑢) · (𝑀 Σg 𝑢))))(.r‘𝑅)(𝑅 Σg (𝑣 ∈ Word 𝐴 ↦ ((𝑖‘𝑣) · (𝑀 Σg 𝑣))))) = (𝑅 Σg (𝑢 ∈ Word 𝐴, 𝑣 ∈ Word 𝐴 ↦ (((𝑔‘𝑢) · (𝑀 Σg 𝑢))(.r‘𝑅)((𝑖‘𝑣) · (𝑀 Σg 𝑣)))))) |
| 177 | 151 | oveq2i 7442 |
. . . . . . . . . . . . . . 15
⊢ (𝑅 Σg
(𝑢 ∈ Word 𝐴 ↦ ((𝑔‘𝑢) · (𝑀 Σg 𝑢)))) = (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑔‘𝑤) · (𝑀 Σg 𝑤)))) |
| 178 | 165 | oveq2i 7442 |
. . . . . . . . . . . . . . 15
⊢ (𝑅 Σg
(𝑣 ∈ Word 𝐴 ↦ ((𝑖‘𝑣) · (𝑀 Σg 𝑣)))) = (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑖‘𝑤) · (𝑀 Σg 𝑤)))) |
| 179 | 177, 178 | oveq12i 7443 |
. . . . . . . . . . . . . 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 7104 |
. . . . . . . . . . . . . . . . . . . . 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 3983 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
(((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑤 ∈ Word 𝐴) ∧ 𝑓 ∈ Word 𝐴) → 𝑓 ∈ Word 𝐵) |
| 191 | 49 | gsumwcl 18852 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑀 ∈ Mnd ∧ 𝑓 ∈ Word 𝐵) → (𝑀 Σg 𝑓) ∈ 𝐵) |
| 192 | 187, 190,
191 | syl2anc 584 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑤 ∈ Word 𝐴) ∧ 𝑓 ∈ Word 𝐴) → (𝑀 Σg 𝑓) ∈ 𝐵) |
| 193 | 2, 4, 183, 186, 192 | mulgcld 19114 |
. . . . . . . . . . . . . . . . . . 19
⊢
(((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑤 ∈ Word 𝐴) ∧ 𝑓 ∈ Word 𝐴) → ((𝑖‘𝑓) · (𝑀 Σg 𝑓)) ∈ 𝐵) |
| 194 | 2, 108, 181, 182, 193 | ringcld 20257 |
. . . . . . . . . . . . . . . . . 18
⊢
(((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑤 ∈ Word 𝐴) ∧ 𝑓 ∈ Word 𝐴) → (((𝑔‘𝑤) · (𝑀 Σg 𝑤))(.r‘𝑅)((𝑖‘𝑓) · (𝑀 Σg 𝑓))) ∈ 𝐵) |
| 195 | 194 | anasss 466 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ (𝑤 ∈ Word 𝐴 ∧ 𝑓 ∈ Word 𝐴)) → (((𝑔‘𝑤) · (𝑀 Σg 𝑤))(.r‘𝑅)((𝑖‘𝑓) · (𝑀 Σg 𝑓))) ∈ 𝐵) |
| 196 | 195 | ralrimivva 3202 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) → ∀𝑤 ∈ Word 𝐴∀𝑓 ∈ Word 𝐴(((𝑔‘𝑤) · (𝑀 Σg 𝑤))(.r‘𝑅)((𝑖‘𝑓) · (𝑀 Σg 𝑓))) ∈ 𝐵) |
| 197 | | eqid 2737 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑤 ∈ Word 𝐴, 𝑓 ∈ Word 𝐴 ↦ (((𝑔‘𝑤) · (𝑀 Σg 𝑤))(.r‘𝑅)((𝑖‘𝑓) · (𝑀 Σg 𝑓)))) = (𝑤 ∈ Word 𝐴, 𝑓 ∈ Word 𝐴 ↦ (((𝑔‘𝑤) · (𝑀 Σg 𝑤))(.r‘𝑅)((𝑖‘𝑓) · (𝑀 Σg 𝑓)))) |
| 198 | 197 | fmpo 8093 |
. . . . . . . . . . . . . . . 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 3484 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ 𝑤 ∈ V |
| 201 | | vex 3484 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ 𝑓 ∈ V |
| 202 | 200, 201 | op1std 8024 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑎 = 〈𝑤, 𝑓〉 → (1st ‘𝑎) = 𝑤) |
| 203 | 202 | fveq2d 6910 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑎 = 〈𝑤, 𝑓〉 → (𝑔‘(1st ‘𝑎)) = (𝑔‘𝑤)) |
| 204 | 202 | oveq2d 7447 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑎 = 〈𝑤, 𝑓〉 → (𝑀 Σg (1st
‘𝑎)) = (𝑀 Σg
𝑤)) |
| 205 | 203, 204 | oveq12d 7449 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑎 = 〈𝑤, 𝑓〉 → ((𝑔‘(1st ‘𝑎)) · (𝑀 Σg (1st
‘𝑎))) = ((𝑔‘𝑤) · (𝑀 Σg 𝑤))) |
| 206 | 200, 201 | op2ndd 8025 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑎 = 〈𝑤, 𝑓〉 → (2nd ‘𝑎) = 𝑓) |
| 207 | 206 | fveq2d 6910 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑎 = 〈𝑤, 𝑓〉 → (𝑖‘(2nd ‘𝑎)) = (𝑖‘𝑓)) |
| 208 | 206 | oveq2d 7447 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑎 = 〈𝑤, 𝑓〉 → (𝑀 Σg (2nd
‘𝑎)) = (𝑀 Σg
𝑓)) |
| 209 | 207, 208 | oveq12d 7449 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑎 = 〈𝑤, 𝑓〉 → ((𝑖‘(2nd ‘𝑎)) · (𝑀 Σg (2nd
‘𝑎))) = ((𝑖‘𝑓) · (𝑀 Σg 𝑓))) |
| 210 | 205, 209 | oveq12d 7449 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑎 = 〈𝑤, 𝑓〉 → (((𝑔‘(1st ‘𝑎)) · (𝑀 Σg (1st
‘𝑎)))(.r‘𝑅)((𝑖‘(2nd ‘𝑎)) · (𝑀 Σg (2nd
‘𝑎)))) = (((𝑔‘𝑤) · (𝑀 Σg 𝑤))(.r‘𝑅)((𝑖‘𝑓) · (𝑀 Σg 𝑓)))) |
| 211 | 210 | mpompt 7547 |
. . . . . . . . . . . . . . . 16
⊢ (𝑎 ∈ (Word 𝐴 × Word 𝐴) ↦ (((𝑔‘(1st ‘𝑎)) · (𝑀 Σg (1st
‘𝑎)))(.r‘𝑅)((𝑖‘(2nd ‘𝑎)) · (𝑀 Σg (2nd
‘𝑎))))) = (𝑤 ∈ Word 𝐴, 𝑓 ∈ Word 𝐴 ↦ (((𝑔‘𝑤) · (𝑀 Σg 𝑤))(.r‘𝑅)((𝑖‘𝑓) · (𝑀 Σg 𝑓)))) |
| 212 | 66, 66 | xpexd 7771 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → (Word 𝐴 × Word 𝐴) ∈ V) |
| 213 | 212 | ad2antrr 726 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) → (Word 𝐴 × Word 𝐴) ∈ V) |
| 214 | 213 | mptexd 7244 |
. . . . . . . . . . . . . . . . 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 8046 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑎 ∈ (Word 𝐴 × Word 𝐴) → (1st ‘𝑎) ∈ Word 𝐴) |
| 220 | 219 | adantl 481 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑎 ∈ (Word 𝐴 × Word 𝐴)) → (1st ‘𝑎) ∈ Word 𝐴) |
| 221 | 218, 220 | ffvelcdmd 7105 |
. . . . . . . . . . . . . . . . . . . . 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 3984 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑎 ∈ (Word 𝐴 × Word 𝐴)) → (1st ‘𝑎) ∈ Word 𝐵) |
| 225 | 49 | gsumwcl 18852 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑀 ∈ Mnd ∧
(1st ‘𝑎)
∈ Word 𝐵) →
(𝑀
Σg (1st ‘𝑎)) ∈ 𝐵) |
| 226 | 222, 224,
225 | syl2anc 584 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑎 ∈ (Word 𝐴 × Word 𝐴)) → (𝑀 Σg (1st
‘𝑎)) ∈ 𝐵) |
| 227 | 2, 4, 217, 221, 226 | mulgcld 19114 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑎 ∈ (Word 𝐴 × Word 𝐴)) → ((𝑔‘(1st ‘𝑎)) · (𝑀 Σg (1st
‘𝑎))) ∈ 𝐵) |
| 228 | 184 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑎 ∈ (Word 𝐴 × Word 𝐴)) → 𝑖:Word 𝐴⟶ℤ) |
| 229 | | xp2nd 8047 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑎 ∈ (Word 𝐴 × Word 𝐴) → (2nd ‘𝑎) ∈ Word 𝐴) |
| 230 | 229 | adantl 481 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑎 ∈ (Word 𝐴 × Word 𝐴)) → (2nd ‘𝑎) ∈ Word 𝐴) |
| 231 | 228, 230 | ffvelcdmd 7105 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑎 ∈ (Word 𝐴 × Word 𝐴)) → (𝑖‘(2nd ‘𝑎)) ∈
ℤ) |
| 232 | 223, 230 | sseldd 3984 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑎 ∈ (Word 𝐴 × Word 𝐴)) → (2nd ‘𝑎) ∈ Word 𝐵) |
| 233 | 49 | gsumwcl 18852 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑀 ∈ Mnd ∧
(2nd ‘𝑎)
∈ Word 𝐵) →
(𝑀
Σg (2nd ‘𝑎)) ∈ 𝐵) |
| 234 | 222, 232,
233 | syl2anc 584 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑎 ∈ (Word 𝐴 × Word 𝐴)) → (𝑀 Σg (2nd
‘𝑎)) ∈ 𝐵) |
| 235 | 2, 4, 217, 231, 234 | mulgcld 19114 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑎 ∈ (Word 𝐴 × Word 𝐴)) → ((𝑖‘(2nd ‘𝑎)) · (𝑀 Σg (2nd
‘𝑎))) ∈ 𝐵) |
| 236 | 2, 108, 216, 227, 235 | ringcld 20257 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑎 ∈ (Word 𝐴 × Word 𝐴)) → (((𝑔‘(1st ‘𝑎)) · (𝑀 Σg (1st
‘𝑎)))(.r‘𝑅)((𝑖‘(2nd ‘𝑎)) · (𝑀 Σg (2nd
‘𝑎)))) ∈ 𝐵) |
| 237 | 236 | fmpttd 7135 |
. . . . . . . . . . . . . . . . . 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 9409 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑔 ∈ 𝐹) → (𝑔 supp 0) ∈ Fin) |
| 240 | 133 | simprbi 496 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑖 ∈ 𝐹 → 𝑖 finSupp 0) |
| 241 | 240 | adantl 481 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) → 𝑖 finSupp 0) |
| 242 | 241 | fsuppimpd 9409 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) → (𝑖 supp 0) ∈ Fin) |
| 243 | | xpfi 9358 |
. . . . . . . . . . . . . . . . . . 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 12625 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢
(((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑎 ∈ ((Word 𝐴 × Word 𝐴) ∖ ((𝑔 supp 0) × (𝑖 supp 0)))) ∧ 𝑎 ∈ ((Word 𝐴 ∖ (𝑔 supp 0)) × Word 𝐴)) → 0 ∈ ℤ) |
| 250 | | xp1st 8046 |
. . . . . . . . . . . . . . . . . . . . . . . . . 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 8196 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
(((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑎 ∈ ((Word 𝐴 × Word 𝐴) ∖ ((𝑔 supp 0) × (𝑖 supp 0)))) ∧ 𝑎 ∈ ((Word 𝐴 ∖ (𝑔 supp 0)) × Word 𝐴)) → (𝑔‘(1st ‘𝑎)) = 0) |
| 253 | 252 | oveq1d 7446 |
. . . . . . . . . . . . . . . . . . . . . . 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 3963 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢
(((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑎 ∈ ((Word 𝐴 × Word 𝐴) ∖ ((𝑔 supp 0) × (𝑖 supp 0)))) ∧ 𝑎 ∈ ((Word 𝐴 ∖ (𝑔 supp 0)) × Word 𝐴)) → (1st ‘𝑎) ∈ Word 𝐴) |
| 257 | 255, 256 | sseldd 3984 |
. . . . . . . . . . . . . . . . . . . . . . . . 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 19092 |
. . . . . . . . . . . . . . . . . . . . . . . 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 2777 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
(((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑎 ∈ ((Word 𝐴 × Word 𝐴) ∖ ((𝑔 supp 0) × (𝑖 supp 0)))) ∧ 𝑎 ∈ ((Word 𝐴 ∖ (𝑔 supp 0)) × Word 𝐴)) → ((𝑔‘(1st ‘𝑎)) · (𝑀 Σg (1st
‘𝑎))) =
(0g‘𝑅)) |
| 262 | 261 | oveq1d 7446 |
. . . . . . . . . . . . . . . . . . . . 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 8047 |
. . . . . . . . . . . . . . . . . . . . . . . . 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 7105 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
(((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑎 ∈ ((Word 𝐴 × Word 𝐴) ∖ ((𝑔 supp 0) × (𝑖 supp 0)))) ∧ 𝑎 ∈ ((Word 𝐴 ∖ (𝑔 supp 0)) × Word 𝐴)) → (𝑖‘(2nd ‘𝑎)) ∈
ℤ) |
| 269 | 255, 267 | sseldd 3984 |
. . . . . . . . . . . . . . . . . . . . . . . 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 19114 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
(((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑎 ∈ ((Word 𝐴 × Word 𝐴) ∖ ((𝑔 supp 0) × (𝑖 supp 0)))) ∧ 𝑎 ∈ ((Word 𝐴 ∖ (𝑔 supp 0)) × Word 𝐴)) → ((𝑖‘(2nd ‘𝑎)) · (𝑀 Σg (2nd
‘𝑎))) ∈ 𝐵) |
| 272 | 2, 108, 52, 263, 271 | ringlzd 20292 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
(((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑎 ∈ ((Word 𝐴 × Word 𝐴) ∖ ((𝑔 supp 0) × (𝑖 supp 0)))) ∧ 𝑎 ∈ ((Word 𝐴 ∖ (𝑔 supp 0)) × Word 𝐴)) → ((0g‘𝑅)(.r‘𝑅)((𝑖‘(2nd ‘𝑎)) · (𝑀 Σg (2nd
‘𝑎)))) =
(0g‘𝑅)) |
| 273 | 262, 272 | eqtrd 2777 |
. . . . . . . . . . . . . . . . . . . 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 12625 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢
(((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑎 ∈ ((Word 𝐴 × Word 𝐴) ∖ ((𝑔 supp 0) × (𝑖 supp 0)))) ∧ 𝑎 ∈ (Word 𝐴 × (Word 𝐴 ∖ (𝑖 supp 0)))) → 0 ∈
ℤ) |
| 279 | | xp2nd 8047 |
. . . . . . . . . . . . . . . . . . . . . . . . . 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 8196 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
(((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑎 ∈ ((Word 𝐴 × Word 𝐴) ∖ ((𝑔 supp 0) × (𝑖 supp 0)))) ∧ 𝑎 ∈ (Word 𝐴 × (Word 𝐴 ∖ (𝑖 supp 0)))) → (𝑖‘(2nd ‘𝑎)) = 0) |
| 282 | 281 | oveq1d 7446 |
. . . . . . . . . . . . . . . . . . . . . . 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 3963 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢
(((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑎 ∈ ((Word 𝐴 × Word 𝐴) ∖ ((𝑔 supp 0) × (𝑖 supp 0)))) ∧ 𝑎 ∈ (Word 𝐴 × (Word 𝐴 ∖ (𝑖 supp 0)))) → (2nd
‘𝑎) ∈ Word 𝐴) |
| 286 | 284, 285 | sseldd 3984 |
. . . . . . . . . . . . . . . . . . . . . . . . 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 19092 |
. . . . . . . . . . . . . . . . . . . . . . . 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 2777 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
(((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑎 ∈ ((Word 𝐴 × Word 𝐴) ∖ ((𝑔 supp 0) × (𝑖 supp 0)))) ∧ 𝑎 ∈ (Word 𝐴 × (Word 𝐴 ∖ (𝑖 supp 0)))) → ((𝑖‘(2nd ‘𝑎)) · (𝑀 Σg (2nd
‘𝑎))) =
(0g‘𝑅)) |
| 291 | 290 | oveq2d 7447 |
. . . . . . . . . . . . . . . . . . . . 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 8046 |
. . . . . . . . . . . . . . . . . . . . . . . . 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 7105 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
(((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑎 ∈ ((Word 𝐴 × Word 𝐴) ∖ ((𝑔 supp 0) × (𝑖 supp 0)))) ∧ 𝑎 ∈ (Word 𝐴 × (Word 𝐴 ∖ (𝑖 supp 0)))) → (𝑔‘(1st ‘𝑎)) ∈
ℤ) |
| 299 | 284, 297 | sseldd 3984 |
. . . . . . . . . . . . . . . . . . . . . . . 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 19114 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
(((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑎 ∈ ((Word 𝐴 × Word 𝐴) ∖ ((𝑔 supp 0) × (𝑖 supp 0)))) ∧ 𝑎 ∈ (Word 𝐴 × (Word 𝐴 ∖ (𝑖 supp 0)))) → ((𝑔‘(1st ‘𝑎)) · (𝑀 Σg (1st
‘𝑎))) ∈ 𝐵) |
| 302 | 2, 108, 52, 292, 301 | ringrzd 20293 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
(((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑎 ∈ ((Word 𝐴 × Word 𝐴) ∖ ((𝑔 supp 0) × (𝑖 supp 0)))) ∧ 𝑎 ∈ (Word 𝐴 × (Word 𝐴 ∖ (𝑖 supp 0)))) → (((𝑔‘(1st ‘𝑎)) · (𝑀 Σg (1st
‘𝑎)))(.r‘𝑅)(0g‘𝑅)) = (0g‘𝑅)) |
| 303 | 291, 302 | eqtrd 2777 |
. . . . . . . . . . . . . . . . . . . 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 6184 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((Word
𝐴 × Word 𝐴) ∖ ((𝑔 supp 0) × (𝑖 supp 0))) = (((Word 𝐴 ∖ (𝑔 supp 0)) × Word 𝐴) ∪ (Word 𝐴 × (Word 𝐴 ∖ (𝑖 supp 0)))) |
| 306 | 304, 305 | eleqtrdi 2851 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑎 ∈ ((Word 𝐴 × Word 𝐴) ∖ ((𝑔 supp 0) × (𝑖 supp 0)))) → 𝑎 ∈ (((Word 𝐴 ∖ (𝑔 supp 0)) × Word 𝐴) ∪ (Word 𝐴 × (Word 𝐴 ∖ (𝑖 supp 0))))) |
| 307 | | elun 4153 |
. . . . . . . . . . . . . . . . . . . . 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 961 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑎 ∈ ((Word 𝐴 × Word 𝐴) ∖ ((𝑔 supp 0) × (𝑖 supp 0)))) → (((𝑔‘(1st ‘𝑎)) · (𝑀 Σg (1st
‘𝑎)))(.r‘𝑅)((𝑖‘(2nd ‘𝑎)) · (𝑀 Σg (2nd
‘𝑎)))) =
(0g‘𝑅)) |
| 310 | 309, 213 | suppss2 8225 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) → ((𝑎 ∈ (Word 𝐴 × Word 𝐴) ↦ (((𝑔‘(1st ‘𝑎)) · (𝑀 Σg (1st
‘𝑎)))(.r‘𝑅)((𝑖‘(2nd ‘𝑎)) · (𝑀 Σg (2nd
‘𝑎))))) supp
(0g‘𝑅))
⊆ ((𝑔 supp 0) ×
(𝑖 supp
0))) |
| 311 | 244, 310 | ssfid 9301 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) → ((𝑎 ∈ (Word 𝐴 × Word 𝐴) ↦ (((𝑔‘(1st ‘𝑎)) · (𝑀 Σg (1st
‘𝑎)))(.r‘𝑅)((𝑖‘(2nd ‘𝑎)) · (𝑀 Σg (2nd
‘𝑎))))) supp
(0g‘𝑅))
∈ Fin) |
| 312 | 214, 215,
238, 311 | isfsuppd 9406 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) → (𝑎 ∈ (Word 𝐴 × Word 𝐴) ↦ (((𝑔‘(1st ‘𝑎)) · (𝑀 Σg (1st
‘𝑎)))(.r‘𝑅)((𝑖‘(2nd ‘𝑎)) · (𝑀 Σg (2nd
‘𝑎))))) finSupp
(0g‘𝑅)) |
| 313 | 211, 312 | eqbrtrrid 5179 |
. . . . . . . . . . . . . . 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 33070 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) → (𝑅 Σg (𝑤 ∈ Word 𝐴, 𝑓 ∈ Word 𝐴 ↦ (((𝑔‘𝑤) · (𝑀 Σg 𝑤))(.r‘𝑅)((𝑖‘𝑓) · (𝑀 Σg 𝑓))))) = (𝑅 Σg (𝑣 ∈ Word 𝐴 ↦ (𝑅 Σg (𝑗 ∈
(0...(♯‘𝑣))
↦ ((𝑤 ∈ Word
𝐴, 𝑓 ∈ Word 𝐴 ↦ (((𝑔‘𝑤) · (𝑀 Σg 𝑤))(.r‘𝑅)((𝑖‘𝑓) · (𝑀 Σg 𝑓))))‘〈(𝑣 prefix 𝑗), (𝑣 substr 〈𝑗, (♯‘𝑣)〉)〉)))))) |
| 317 | 126 | oveq1d 7446 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑢 = 𝑤 → (((𝑔‘𝑢) · (𝑀 Σg 𝑢))(.r‘𝑅)((𝑖‘𝑣) · (𝑀 Σg 𝑣))) = (((𝑔‘𝑤) · (𝑀 Σg 𝑤))(.r‘𝑅)((𝑖‘𝑣) · (𝑀 Σg 𝑣)))) |
| 318 | | fveq2 6906 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑣 = 𝑓 → (𝑖‘𝑣) = (𝑖‘𝑓)) |
| 319 | | oveq2 7439 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑣 = 𝑓 → (𝑀 Σg 𝑣) = (𝑀 Σg 𝑓)) |
| 320 | 318, 319 | oveq12d 7449 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑣 = 𝑓 → ((𝑖‘𝑣) · (𝑀 Σg 𝑣)) = ((𝑖‘𝑓) · (𝑀 Σg 𝑓))) |
| 321 | 320 | oveq2d 7447 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑣 = 𝑓 → (((𝑔‘𝑤) · (𝑀 Σg 𝑤))(.r‘𝑅)((𝑖‘𝑣) · (𝑀 Σg 𝑣))) = (((𝑔‘𝑤) · (𝑀 Σg 𝑤))(.r‘𝑅)((𝑖‘𝑓) · (𝑀 Σg 𝑓)))) |
| 322 | 317, 321 | cbvmpov 7528 |
. . . . . . . . . . . . . . . 16
⊢ (𝑢 ∈ Word 𝐴, 𝑣 ∈ Word 𝐴 ↦ (((𝑔‘𝑢) · (𝑀 Σg 𝑢))(.r‘𝑅)((𝑖‘𝑣) · (𝑀 Σg 𝑣)))) = (𝑤 ∈ Word 𝐴, 𝑓 ∈ Word 𝐴 ↦ (((𝑔‘𝑤) · (𝑀 Σg 𝑤))(.r‘𝑅)((𝑖‘𝑓) · (𝑀 Σg 𝑓)))) |
| 323 | 322 | oveq2i 7442 |
. . . . . . . . . . . . . . 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 14748 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑣 ∈ Word 𝐴 ∧ 𝑗 ∈ (0...(♯‘𝑣))) → ((𝑣 prefix 𝑗) ++ (𝑣 substr 〈𝑗, (♯‘𝑣)〉)) = 𝑣) |
| 326 | 325 | adantll 714 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
(((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑣 ∈ Word 𝐴) ∧ 𝑗 ∈ (0...(♯‘𝑣))) → ((𝑣 prefix 𝑗) ++ (𝑣 substr 〈𝑗, (♯‘𝑣)〉)) = 𝑣) |
| 327 | 326 | oveq2d 7447 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑣 ∈ Word 𝐴) ∧ 𝑗 ∈ (0...(♯‘𝑣))) → (𝑀 Σg ((𝑣 prefix 𝑗) ++ (𝑣 substr 〈𝑗, (♯‘𝑣)〉))) = (𝑀 Σg 𝑣)) |
| 328 | 327 | oveq2d 7447 |
. . . . . . . . . . . . . . . . . . 19
⊢
(((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑣 ∈ Word 𝐴) ∧ 𝑗 ∈ (0...(♯‘𝑣))) → (((𝑔‘(𝑣 prefix 𝑗)) · (𝑖‘(𝑣 substr 〈𝑗, (♯‘𝑣)〉))) · (𝑀 Σg ((𝑣 prefix 𝑗) ++ (𝑣 substr 〈𝑗, (♯‘𝑣)〉)))) = (((𝑔‘(𝑣 prefix 𝑗)) · (𝑖‘(𝑣 substr 〈𝑗, (♯‘𝑣)〉))) · (𝑀 Σg 𝑣))) |
| 329 | 328 | mpteq2dva 5242 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑣 ∈ Word 𝐴) → (𝑗 ∈ (0...(♯‘𝑣)) ↦ (((𝑔‘(𝑣 prefix 𝑗)) · (𝑖‘(𝑣 substr 〈𝑗, (♯‘𝑣)〉))) · (𝑀 Σg ((𝑣 prefix 𝑗) ++ (𝑣 substr 〈𝑗, (♯‘𝑣)〉))))) = (𝑗 ∈ (0...(♯‘𝑣)) ↦ (((𝑔‘(𝑣 prefix 𝑗)) · (𝑖‘(𝑣 substr 〈𝑗, (♯‘𝑣)〉))) · (𝑀 Σg 𝑣)))) |
| 330 | 329 | oveq2d 7447 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑣 ∈ Word 𝐴) → (𝑅 Σg (𝑗 ∈
(0...(♯‘𝑣))
↦ (((𝑔‘(𝑣 prefix 𝑗)) · (𝑖‘(𝑣 substr 〈𝑗, (♯‘𝑣)〉))) · (𝑀 Σg ((𝑣 prefix 𝑗) ++ (𝑣 substr 〈𝑗, (♯‘𝑣)〉)))))) = (𝑅 Σg (𝑗 ∈
(0...(♯‘𝑣))
↦ (((𝑔‘(𝑣 prefix 𝑗)) · (𝑖‘(𝑣 substr 〈𝑗, (♯‘𝑣)〉))) · (𝑀 Σg 𝑣))))) |
| 331 | | df-ov 7434 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑣 prefix 𝑗)(𝑤 ∈ Word 𝐴, 𝑓 ∈ Word 𝐴 ↦ (((𝑔‘𝑤) · (𝑀 Σg 𝑤))(.r‘𝑅)((𝑖‘𝑓) · (𝑀 Σg 𝑓))))(𝑣 substr 〈𝑗, (♯‘𝑣)〉)) = ((𝑤 ∈ Word 𝐴, 𝑓 ∈ Word 𝐴 ↦ (((𝑔‘𝑤) · (𝑀 Σg 𝑤))(.r‘𝑅)((𝑖‘𝑓) · (𝑀 Σg 𝑓))))‘〈(𝑣 prefix 𝑗), (𝑣 substr 〈𝑗, (♯‘𝑣)〉)〉) |
| 332 | 188 | sselda 3983 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
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 20353 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ ((𝑅 ∈ Ring ∧ ((𝑖‘𝑓) ∈ ℤ ∧ (𝑀 Σg 𝑤) ∈ 𝐵 ∧ (𝑀 Σg 𝑓) ∈ 𝐵)) → ((𝑀 Σg 𝑤)(.r‘𝑅)((𝑖‘𝑓) · (𝑀 Σg 𝑓))) = ((𝑖‘𝑓) · ((𝑀 Σg 𝑤)(.r‘𝑅)(𝑀 Σg 𝑓)))) |
| 336 | 181, 186,
334, 192, 335 | syl13anc 1374 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢
(((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑤 ∈ Word 𝐴) ∧ 𝑓 ∈ Word 𝐴) → ((𝑀 Σg 𝑤)(.r‘𝑅)((𝑖‘𝑓) · (𝑀 Σg 𝑓))) = ((𝑖‘𝑓) · ((𝑀 Σg 𝑤)(.r‘𝑅)(𝑀 Σg 𝑓)))) |
| 337 | 336 | oveq2d 7447 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢
(((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑤 ∈ Word 𝐴) ∧ 𝑓 ∈ Word 𝐴) → ((𝑔‘𝑤) · ((𝑀 Σg 𝑤)(.r‘𝑅)((𝑖‘𝑓) · (𝑀 Σg 𝑓)))) = ((𝑔‘𝑤) · ((𝑖‘𝑓) · ((𝑀 Σg 𝑤)(.r‘𝑅)(𝑀 Σg 𝑓))))) |
| 338 | 119 | ad4ant13 751 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢
(((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑤 ∈ Word 𝐴) ∧ 𝑓 ∈ Word 𝐴) → (𝑔‘𝑤) ∈ ℤ) |
| 339 | 2, 4, 108 | mulgass2 20306 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((𝑅 ∈ Ring ∧ ((𝑔‘𝑤) ∈ ℤ ∧ (𝑀 Σg 𝑤) ∈ 𝐵 ∧ ((𝑖‘𝑓) · (𝑀 Σg 𝑓)) ∈ 𝐵)) → (((𝑔‘𝑤) · (𝑀 Σg 𝑤))(.r‘𝑅)((𝑖‘𝑓) · (𝑀 Σg 𝑓))) = ((𝑔‘𝑤) · ((𝑀 Σg 𝑤)(.r‘𝑅)((𝑖‘𝑓) · (𝑀 Σg 𝑓))))) |
| 340 | 181, 338,
334, 193, 339 | syl13anc 1374 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢
(((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑤 ∈ Word 𝐴) ∧ 𝑓 ∈ Word 𝐴) → (((𝑔‘𝑤) · (𝑀 Σg 𝑤))(.r‘𝑅)((𝑖‘𝑓) · (𝑀 Σg 𝑓))) = ((𝑔‘𝑤) · ((𝑀 Σg 𝑤)(.r‘𝑅)((𝑖‘𝑓) · (𝑀 Σg 𝑓))))) |
| 341 | 2, 108, 181, 334, 192 | ringcld 20257 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢
(((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑤 ∈ Word 𝐴) ∧ 𝑓 ∈ Word 𝐴) → ((𝑀 Σg 𝑤)(.r‘𝑅)(𝑀 Σg 𝑓)) ∈ 𝐵) |
| 342 | 2, 4 | mulgass 19129 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((𝑅 ∈ Grp ∧ ((𝑔‘𝑤) ∈ ℤ ∧ (𝑖‘𝑓) ∈ ℤ ∧ ((𝑀 Σg 𝑤)(.r‘𝑅)(𝑀 Σg 𝑓)) ∈ 𝐵)) → (((𝑔‘𝑤) · (𝑖‘𝑓)) · ((𝑀 Σg 𝑤)(.r‘𝑅)(𝑀 Σg 𝑓))) = ((𝑔‘𝑤) · ((𝑖‘𝑓) · ((𝑀 Σg 𝑤)(.r‘𝑅)(𝑀 Σg 𝑓))))) |
| 343 | 183, 338,
186, 341, 342 | syl13anc 1374 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢
(((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑤 ∈ Word 𝐴) ∧ 𝑓 ∈ Word 𝐴) → (((𝑔‘𝑤) · (𝑖‘𝑓)) · ((𝑀 Σg 𝑤)(.r‘𝑅)(𝑀 Σg 𝑓))) = ((𝑔‘𝑤) · ((𝑖‘𝑓) · ((𝑀 Σg 𝑤)(.r‘𝑅)(𝑀 Σg 𝑓))))) |
| 344 | 337, 340,
343 | 3eqtr4d 2787 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢
(((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑤 ∈ Word 𝐴) ∧ 𝑓 ∈ Word 𝐴) → (((𝑔‘𝑤) · (𝑀 Σg 𝑤))(.r‘𝑅)((𝑖‘𝑓) · (𝑀 Σg 𝑓))) = (((𝑔‘𝑤) · (𝑖‘𝑓)) · ((𝑀 Σg 𝑤)(.r‘𝑅)(𝑀 Σg 𝑓)))) |
| 345 | 3, 108 | mgpplusg 20141 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢
(.r‘𝑅) = (+g‘𝑀) |
| 346 | 49, 345 | gsumccat 18854 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((𝑀 ∈ Mnd ∧ 𝑤 ∈ Word 𝐵 ∧ 𝑓 ∈ Word 𝐵) → (𝑀 Σg (𝑤 ++ 𝑓)) = ((𝑀 Σg 𝑤)(.r‘𝑅)(𝑀 Σg 𝑓))) |
| 347 | 187, 333,
190, 346 | syl3anc 1373 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢
(((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑤 ∈ Word 𝐴) ∧ 𝑓 ∈ Word 𝐴) → (𝑀 Σg (𝑤 ++ 𝑓)) = ((𝑀 Σg 𝑤)(.r‘𝑅)(𝑀 Σg 𝑓))) |
| 348 | 347 | oveq2d 7447 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢
(((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑤 ∈ Word 𝐴) ∧ 𝑓 ∈ Word 𝐴) → (((𝑔‘𝑤) · (𝑖‘𝑓)) · (𝑀 Σg (𝑤 ++ 𝑓))) = (((𝑔‘𝑤) · (𝑖‘𝑓)) · ((𝑀 Σg 𝑤)(.r‘𝑅)(𝑀 Σg 𝑓)))) |
| 349 | 344, 348 | eqtr4d 2780 |
. . . . . . . . . . . . . . . . . . . . . . . . 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 1110 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
((((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑣 ∈ Word 𝐴) ∧ 𝑗 ∈ (0...(♯‘𝑣))) ∧ 𝑤 ∈ Word 𝐴 ∧ 𝑓 ∈ Word 𝐴) → (((𝑔‘𝑤) · (𝑀 Σg 𝑤))(.r‘𝑅)((𝑖‘𝑓) · (𝑀 Σg 𝑓))) = (((𝑔‘𝑤) · (𝑖‘𝑓)) · (𝑀 Σg (𝑤 ++ 𝑓)))) |
| 353 | 352 | mpoeq3dva 7510 |
. . . . . . . . . . . . . . . . . . . . 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 7450 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝑤 = (𝑣 prefix 𝑗) ∧ 𝑓 = (𝑣 substr 〈𝑗, (♯‘𝑣)〉)) → ((𝑔‘𝑤) · (𝑖‘𝑓)) = ((𝑔‘(𝑣 prefix 𝑗)) · (𝑖‘(𝑣 substr 〈𝑗, (♯‘𝑣)〉)))) |
| 357 | | oveq12 7440 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝑤 = (𝑣 prefix 𝑗) ∧ 𝑓 = (𝑣 substr 〈𝑗, (♯‘𝑣)〉)) → (𝑤 ++ 𝑓) = ((𝑣 prefix 𝑗) ++ (𝑣 substr 〈𝑗, (♯‘𝑣)〉))) |
| 358 | 357 | oveq2d 7447 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝑤 = (𝑣 prefix 𝑗) ∧ 𝑓 = (𝑣 substr 〈𝑗, (♯‘𝑣)〉)) → (𝑀 Σg (𝑤 ++ 𝑓)) = (𝑀 Σg ((𝑣 prefix 𝑗) ++ (𝑣 substr 〈𝑗, (♯‘𝑣)〉)))) |
| 359 | 356, 358 | oveq12d 7449 |
. . . . . . . . . . . . . . . . . . . . . 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 14715 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑣 ∈ Word 𝐴 → (𝑣 prefix 𝑗) ∈ Word 𝐴) |
| 362 | 361 | ad2antlr 727 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
(((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑣 ∈ Word 𝐴) ∧ 𝑗 ∈ (0...(♯‘𝑣))) → (𝑣 prefix 𝑗) ∈ Word 𝐴) |
| 363 | | swrdcl 14683 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑣 ∈ Word 𝐴 → (𝑣 substr 〈𝑗, (♯‘𝑣)〉) ∈ Word 𝐴) |
| 364 | 363 | ad2antlr 727 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
(((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑣 ∈ Word 𝐴) ∧ 𝑗 ∈ (0...(♯‘𝑣))) → (𝑣 substr 〈𝑗, (♯‘𝑣)〉) ∈ Word 𝐴) |
| 365 | | ovexd 7466 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
(((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑣 ∈ Word 𝐴) ∧ 𝑗 ∈ (0...(♯‘𝑣))) → (((𝑔‘(𝑣 prefix 𝑗)) · (𝑖‘(𝑣 substr 〈𝑗, (♯‘𝑣)〉))) · (𝑀 Σg ((𝑣 prefix 𝑗) ++ (𝑣 substr 〈𝑗, (♯‘𝑣)〉)))) ∈ V) |
| 366 | 353, 360,
362, 364, 365 | ovmpod 7585 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑣 ∈ Word 𝐴) ∧ 𝑗 ∈ (0...(♯‘𝑣))) → ((𝑣 prefix 𝑗)(𝑤 ∈ Word 𝐴, 𝑓 ∈ Word 𝐴 ↦ (((𝑔‘𝑤) · (𝑀 Σg 𝑤))(.r‘𝑅)((𝑖‘𝑓) · (𝑀 Σg 𝑓))))(𝑣 substr 〈𝑗, (♯‘𝑣)〉)) = (((𝑔‘(𝑣 prefix 𝑗)) · (𝑖‘(𝑣 substr 〈𝑗, (♯‘𝑣)〉))) · (𝑀 Σg ((𝑣 prefix 𝑗) ++ (𝑣 substr 〈𝑗, (♯‘𝑣)〉))))) |
| 367 | 331, 366 | eqtr3id 2791 |
. . . . . . . . . . . . . . . . . . 19
⊢
(((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑣 ∈ Word 𝐴) ∧ 𝑗 ∈ (0...(♯‘𝑣))) → ((𝑤 ∈ Word 𝐴, 𝑓 ∈ Word 𝐴 ↦ (((𝑔‘𝑤) · (𝑀 Σg 𝑤))(.r‘𝑅)((𝑖‘𝑓) · (𝑀 Σg 𝑓))))‘〈(𝑣 prefix 𝑗), (𝑣 substr 〈𝑗, (♯‘𝑣)〉)〉) = (((𝑔‘(𝑣 prefix 𝑗)) · (𝑖‘(𝑣 substr 〈𝑗, (♯‘𝑣)〉))) · (𝑀 Σg ((𝑣 prefix 𝑗) ++ (𝑣 substr 〈𝑗, (♯‘𝑣)〉))))) |
| 368 | 367 | mpteq2dva 5242 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑣 ∈ Word 𝐴) → (𝑗 ∈ (0...(♯‘𝑣)) ↦ ((𝑤 ∈ Word 𝐴, 𝑓 ∈ Word 𝐴 ↦ (((𝑔‘𝑤) · (𝑀 Σg 𝑤))(.r‘𝑅)((𝑖‘𝑓) · (𝑀 Σg 𝑓))))‘〈(𝑣 prefix 𝑗), (𝑣 substr 〈𝑗, (♯‘𝑣)〉)〉)) = (𝑗 ∈ (0...(♯‘𝑣)) ↦ (((𝑔‘(𝑣 prefix 𝑗)) · (𝑖‘(𝑣 substr 〈𝑗, (♯‘𝑣)〉))) · (𝑀 Σg ((𝑣 prefix 𝑗) ++ (𝑣 substr 〈𝑗, (♯‘𝑣)〉)))))) |
| 369 | 368 | oveq2d 7447 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑣 ∈ Word 𝐴) → (𝑅 Σg (𝑗 ∈
(0...(♯‘𝑣))
↦ ((𝑤 ∈ Word
𝐴, 𝑓 ∈ Word 𝐴 ↦ (((𝑔‘𝑤) · (𝑀 Σg 𝑤))(.r‘𝑅)((𝑖‘𝑓) · (𝑀 Σg 𝑓))))‘〈(𝑣 prefix 𝑗), (𝑣 substr 〈𝑗, (♯‘𝑣)〉)〉))) = (𝑅 Σg (𝑗 ∈
(0...(♯‘𝑣))
↦ (((𝑔‘(𝑣 prefix 𝑗)) · (𝑖‘(𝑣 substr 〈𝑗, (♯‘𝑣)〉))) · (𝑀 Σg ((𝑣 prefix 𝑗) ++ (𝑣 substr 〈𝑗, (♯‘𝑣)〉))))))) |
| 370 | | eqid 2737 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑡 ∈ Word 𝐴 ↦ Σ𝑗 ∈ (0...(♯‘𝑡))((𝑔‘(𝑡 prefix 𝑗)) · (𝑖‘(𝑡 substr 〈𝑗, (♯‘𝑡)〉)))) = (𝑡 ∈ Word 𝐴 ↦ Σ𝑗 ∈ (0...(♯‘𝑡))((𝑔‘(𝑡 prefix 𝑗)) · (𝑖‘(𝑡 substr 〈𝑗, (♯‘𝑡)〉)))) |
| 371 | | fveq2 6906 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑡 = 𝑣 → (♯‘𝑡) = (♯‘𝑣)) |
| 372 | 371 | oveq2d 7447 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑡 = 𝑣 → (0...(♯‘𝑡)) = (0...(♯‘𝑣))) |
| 373 | | fvoveq1 7454 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑡 = 𝑣 → (𝑔‘(𝑡 prefix 𝑗)) = (𝑔‘(𝑣 prefix 𝑗))) |
| 374 | | id 22 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑡 = 𝑣 → 𝑡 = 𝑣) |
| 375 | 371 | opeq2d 4880 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑡 = 𝑣 → 〈𝑗, (♯‘𝑡)〉 = 〈𝑗, (♯‘𝑣)〉) |
| 376 | 374, 375 | oveq12d 7449 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑡 = 𝑣 → (𝑡 substr 〈𝑗, (♯‘𝑡)〉) = (𝑣 substr 〈𝑗, (♯‘𝑣)〉)) |
| 377 | 376 | fveq2d 6910 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑡 = 𝑣 → (𝑖‘(𝑡 substr 〈𝑗, (♯‘𝑡)〉)) = (𝑖‘(𝑣 substr 〈𝑗, (♯‘𝑣)〉))) |
| 378 | 373, 377 | oveq12d 7449 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑡 = 𝑣 → ((𝑔‘(𝑡 prefix 𝑗)) · (𝑖‘(𝑡 substr 〈𝑗, (♯‘𝑡)〉))) = ((𝑔‘(𝑣 prefix 𝑗)) · (𝑖‘(𝑣 substr 〈𝑗, (♯‘𝑣)〉)))) |
| 379 | 378 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑡 = 𝑣 ∧ 𝑗 ∈ (0...(♯‘𝑡))) → ((𝑔‘(𝑡 prefix 𝑗)) · (𝑖‘(𝑡 substr 〈𝑗, (♯‘𝑡)〉))) = ((𝑔‘(𝑣 prefix 𝑗)) · (𝑖‘(𝑣 substr 〈𝑗, (♯‘𝑣)〉)))) |
| 380 | 372, 379 | sumeq12dv 15742 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑡 = 𝑣 → Σ𝑗 ∈ (0...(♯‘𝑡))((𝑔‘(𝑡 prefix 𝑗)) · (𝑖‘(𝑡 substr 〈𝑗, (♯‘𝑡)〉))) = Σ𝑗 ∈ (0...(♯‘𝑣))((𝑔‘(𝑣 prefix 𝑗)) · (𝑖‘(𝑣 substr 〈𝑗, (♯‘𝑣)〉)))) |
| 381 | | simpr 484 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑣 ∈ Word 𝐴) → 𝑣 ∈ Word 𝐴) |
| 382 | | fzfid 14014 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑣 ∈ Word 𝐴) → (0...(♯‘𝑣)) ∈ Fin) |
| 383 | 294 | ad2antrr 726 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
(((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑣 ∈ Word 𝐴) ∧ 𝑗 ∈ (0...(♯‘𝑣))) → 𝑔:Word 𝐴⟶ℤ) |
| 384 | 383, 362 | ffvelcdmd 7105 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
(((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑣 ∈ Word 𝐴) ∧ 𝑗 ∈ (0...(♯‘𝑣))) → (𝑔‘(𝑣 prefix 𝑗)) ∈ ℤ) |
| 385 | 184 | ad2antrr 726 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
(((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑣 ∈ Word 𝐴) ∧ 𝑗 ∈ (0...(♯‘𝑣))) → 𝑖:Word 𝐴⟶ℤ) |
| 386 | 385, 364 | ffvelcdmd 7105 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
(((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑣 ∈ Word 𝐴) ∧ 𝑗 ∈ (0...(♯‘𝑣))) → (𝑖‘(𝑣 substr 〈𝑗, (♯‘𝑣)〉)) ∈ ℤ) |
| 387 | 384, 386 | zmulcld 12728 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
(((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑣 ∈ Word 𝐴) ∧ 𝑗 ∈ (0...(♯‘𝑣))) → ((𝑔‘(𝑣 prefix 𝑗)) · (𝑖‘(𝑣 substr 〈𝑗, (♯‘𝑣)〉))) ∈ ℤ) |
| 388 | 387 | zcnd 12723 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
(((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑣 ∈ Word 𝐴) ∧ 𝑗 ∈ (0...(♯‘𝑣))) → ((𝑔‘(𝑣 prefix 𝑗)) · (𝑖‘(𝑣 substr 〈𝑗, (♯‘𝑣)〉))) ∈ ℂ) |
| 389 | 382, 388 | fsumcl 15769 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑣 ∈ Word 𝐴) → Σ𝑗 ∈ (0...(♯‘𝑣))((𝑔‘(𝑣 prefix 𝑗)) · (𝑖‘(𝑣 substr 〈𝑗, (♯‘𝑣)〉))) ∈ ℂ) |
| 390 | 370, 380,
381, 389 | fvmptd3 7039 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑣 ∈ Word 𝐴) → ((𝑡 ∈ Word 𝐴 ↦ Σ𝑗 ∈ (0...(♯‘𝑡))((𝑔‘(𝑡 prefix 𝑗)) · (𝑖‘(𝑡 substr 〈𝑗, (♯‘𝑡)〉))))‘𝑣) = Σ𝑗 ∈ (0...(♯‘𝑣))((𝑔‘(𝑣 prefix 𝑗)) · (𝑖‘(𝑣 substr 〈𝑗, (♯‘𝑣)〉)))) |
| 391 | 390 | oveq1d 7446 |
. . . . . . . . . . . . . . . . . 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 3983 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑣 ∈ Word 𝐴) → 𝑣 ∈ Word 𝐵) |
| 396 | 49 | gsumwcl 18852 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑀 ∈ Mnd ∧ 𝑣 ∈ Word 𝐵) → (𝑀 Σg 𝑣) ∈ 𝐵) |
| 397 | 393, 395,
396 | syl2anc 584 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑣 ∈ Word 𝐴) → (𝑀 Σg 𝑣) ∈ 𝐵) |
| 398 | 2, 4, 392, 382, 397, 387 | gsummulgc2 33063 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑣 ∈ Word 𝐴) → (𝑅 Σg (𝑗 ∈
(0...(♯‘𝑣))
↦ (((𝑔‘(𝑣 prefix 𝑗)) · (𝑖‘(𝑣 substr 〈𝑗, (♯‘𝑣)〉))) · (𝑀 Σg 𝑣)))) = (Σ𝑗 ∈
(0...(♯‘𝑣))((𝑔‘(𝑣 prefix 𝑗)) · (𝑖‘(𝑣 substr 〈𝑗, (♯‘𝑣)〉))) · (𝑀 Σg 𝑣))) |
| 399 | 391, 398 | eqtr4d 2780 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑣 ∈ Word 𝐴) → (((𝑡 ∈ Word 𝐴 ↦ Σ𝑗 ∈ (0...(♯‘𝑡))((𝑔‘(𝑡 prefix 𝑗)) · (𝑖‘(𝑡 substr 〈𝑗, (♯‘𝑡)〉))))‘𝑣) · (𝑀 Σg 𝑣)) = (𝑅 Σg (𝑗 ∈
(0...(♯‘𝑣))
↦ (((𝑔‘(𝑣 prefix 𝑗)) · (𝑖‘(𝑣 substr 〈𝑗, (♯‘𝑣)〉))) · (𝑀 Σg 𝑣))))) |
| 400 | 330, 369,
399 | 3eqtr4rd 2788 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑣 ∈ Word 𝐴) → (((𝑡 ∈ Word 𝐴 ↦ Σ𝑗 ∈ (0...(♯‘𝑡))((𝑔‘(𝑡 prefix 𝑗)) · (𝑖‘(𝑡 substr 〈𝑗, (♯‘𝑡)〉))))‘𝑣) · (𝑀 Σg 𝑣)) = (𝑅 Σg (𝑗 ∈
(0...(♯‘𝑣))
↦ ((𝑤 ∈ Word
𝐴, 𝑓 ∈ Word 𝐴 ↦ (((𝑔‘𝑤) · (𝑀 Σg 𝑤))(.r‘𝑅)((𝑖‘𝑓) · (𝑀 Σg 𝑓))))‘〈(𝑣 prefix 𝑗), (𝑣 substr 〈𝑗, (♯‘𝑣)〉)〉)))) |
| 401 | 400 | mpteq2dva 5242 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) → (𝑣 ∈ Word 𝐴 ↦ (((𝑡 ∈ Word 𝐴 ↦ Σ𝑗 ∈ (0...(♯‘𝑡))((𝑔‘(𝑡 prefix 𝑗)) · (𝑖‘(𝑡 substr 〈𝑗, (♯‘𝑡)〉))))‘𝑣) · (𝑀 Σg 𝑣))) = (𝑣 ∈ Word 𝐴 ↦ (𝑅 Σg (𝑗 ∈
(0...(♯‘𝑣))
↦ ((𝑤 ∈ Word
𝐴, 𝑓 ∈ Word 𝐴 ↦ (((𝑔‘𝑤) · (𝑀 Σg 𝑤))(.r‘𝑅)((𝑖‘𝑓) · (𝑀 Σg 𝑓))))‘〈(𝑣 prefix 𝑗), (𝑣 substr 〈𝑗, (♯‘𝑣)〉)〉))))) |
| 402 | 401 | oveq2d 7447 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) → (𝑅 Σg (𝑣 ∈ Word 𝐴 ↦ (((𝑡 ∈ Word 𝐴 ↦ Σ𝑗 ∈ (0...(♯‘𝑡))((𝑔‘(𝑡 prefix 𝑗)) · (𝑖‘(𝑡 substr 〈𝑗, (♯‘𝑡)〉))))‘𝑣) · (𝑀 Σg 𝑣)))) = (𝑅 Σg (𝑣 ∈ Word 𝐴 ↦ (𝑅 Σg (𝑗 ∈
(0...(♯‘𝑣))
↦ ((𝑤 ∈ Word
𝐴, 𝑓 ∈ Word 𝐴 ↦ (((𝑔‘𝑤) · (𝑀 Σg 𝑤))(.r‘𝑅)((𝑖‘𝑓) · (𝑀 Σg 𝑓))))‘〈(𝑣 prefix 𝑗), (𝑣 substr 〈𝑗, (♯‘𝑣)〉)〉)))))) |
| 403 | 316, 324,
402 | 3eqtr4d 2787 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) → (𝑅 Σg (𝑢 ∈ Word 𝐴, 𝑣 ∈ Word 𝐴 ↦ (((𝑔‘𝑢) · (𝑀 Σg 𝑢))(.r‘𝑅)((𝑖‘𝑣) · (𝑀 Σg 𝑣))))) = (𝑅 Σg (𝑣 ∈ Word 𝐴 ↦ (((𝑡 ∈ Word 𝐴 ↦ Σ𝑗 ∈ (0...(♯‘𝑡))((𝑔‘(𝑡 prefix 𝑗)) · (𝑖‘(𝑡 substr 〈𝑗, (♯‘𝑡)〉))))‘𝑣) · (𝑀 Σg 𝑣))))) |
| 404 | 176, 180,
403 | 3eqtr3d 2785 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) → ((𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑔‘𝑤) · (𝑀 Σg 𝑤))))(.r‘𝑅)(𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑖‘𝑤) · (𝑀 Σg 𝑤))))) = (𝑅 Σg (𝑣 ∈ Word 𝐴 ↦ (((𝑡 ∈ Word 𝐴 ↦ Σ𝑗 ∈ (0...(♯‘𝑡))((𝑔‘(𝑡 prefix 𝑗)) · (𝑖‘(𝑡 substr 〈𝑗, (♯‘𝑡)〉))))‘𝑣) · (𝑀 Σg 𝑣))))) |
| 405 | | fveq1 6905 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑔 = ℎ → (𝑔‘𝑤) = (ℎ‘𝑤)) |
| 406 | 405 | oveq1d 7446 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑔 = ℎ → ((𝑔‘𝑤) · (𝑀 Σg 𝑤)) = ((ℎ‘𝑤) · (𝑀 Σg 𝑤))) |
| 407 | 406 | mpteq2dv 5244 |
. . . . . . . . . . . . . . . 16
⊢ (𝑔 = ℎ → (𝑤 ∈ Word 𝐴 ↦ ((𝑔‘𝑤) · (𝑀 Σg 𝑤))) = (𝑤 ∈ Word 𝐴 ↦ ((ℎ‘𝑤) · (𝑀 Σg 𝑤)))) |
| 408 | 407 | oveq2d 7447 |
. . . . . . . . . . . . . . 15
⊢ (𝑔 = ℎ → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑔‘𝑤) · (𝑀 Σg 𝑤)))) = (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((ℎ‘𝑤) · (𝑀 Σg 𝑤))))) |
| 409 | 408 | cbvmptv 5255 |
. . . . . . . . . . . . . 14
⊢ (𝑔 ∈ 𝐹 ↦ (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑔‘𝑤) · (𝑀 Σg 𝑤))))) = (ℎ ∈ 𝐹 ↦ (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((ℎ‘𝑤) · (𝑀 Σg 𝑤))))) |
| 410 | | fveq1 6905 |
. . . . . . . . . . . . . . . . . . 19
⊢ (ℎ = (𝑡 ∈ Word 𝐴 ↦ Σ𝑗 ∈ (0...(♯‘𝑡))((𝑔‘(𝑡 prefix 𝑗)) · (𝑖‘(𝑡 substr 〈𝑗, (♯‘𝑡)〉)))) → (ℎ‘𝑤) = ((𝑡 ∈ Word 𝐴 ↦ Σ𝑗 ∈ (0...(♯‘𝑡))((𝑔‘(𝑡 prefix 𝑗)) · (𝑖‘(𝑡 substr 〈𝑗, (♯‘𝑡)〉))))‘𝑤)) |
| 411 | 410 | oveq1d 7446 |
. . . . . . . . . . . . . . . . . 18
⊢ (ℎ = (𝑡 ∈ Word 𝐴 ↦ Σ𝑗 ∈ (0...(♯‘𝑡))((𝑔‘(𝑡 prefix 𝑗)) · (𝑖‘(𝑡 substr 〈𝑗, (♯‘𝑡)〉)))) → ((ℎ‘𝑤) · (𝑀 Σg 𝑤)) = (((𝑡 ∈ Word 𝐴 ↦ Σ𝑗 ∈ (0...(♯‘𝑡))((𝑔‘(𝑡 prefix 𝑗)) · (𝑖‘(𝑡 substr 〈𝑗, (♯‘𝑡)〉))))‘𝑤) · (𝑀 Σg 𝑤))) |
| 412 | 411 | mpteq2dv 5244 |
. . . . . . . . . . . . . . . . 17
⊢ (ℎ = (𝑡 ∈ Word 𝐴 ↦ Σ𝑗 ∈ (0...(♯‘𝑡))((𝑔‘(𝑡 prefix 𝑗)) · (𝑖‘(𝑡 substr 〈𝑗, (♯‘𝑡)〉)))) → (𝑤 ∈ Word 𝐴 ↦ ((ℎ‘𝑤) · (𝑀 Σg 𝑤))) = (𝑤 ∈ Word 𝐴 ↦ (((𝑡 ∈ Word 𝐴 ↦ Σ𝑗 ∈ (0...(♯‘𝑡))((𝑔‘(𝑡 prefix 𝑗)) · (𝑖‘(𝑡 substr 〈𝑗, (♯‘𝑡)〉))))‘𝑤) · (𝑀 Σg 𝑤)))) |
| 413 | 412 | oveq2d 7447 |
. . . . . . . . . . . . . . . 16
⊢ (ℎ = (𝑡 ∈ Word 𝐴 ↦ Σ𝑗 ∈ (0...(♯‘𝑡))((𝑔‘(𝑡 prefix 𝑗)) · (𝑖‘(𝑡 substr 〈𝑗, (♯‘𝑡)〉)))) → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((ℎ‘𝑤) · (𝑀 Σg 𝑤)))) = (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ (((𝑡 ∈ Word 𝐴 ↦ Σ𝑗 ∈ (0...(♯‘𝑡))((𝑔‘(𝑡 prefix 𝑗)) · (𝑖‘(𝑡 substr 〈𝑗, (♯‘𝑡)〉))))‘𝑤) · (𝑀 Σg 𝑤))))) |
| 414 | 413 | eqeq2d 2748 |
. . . . . . . . . . . . . . 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 5146 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑓 = (𝑡 ∈ Word 𝐴 ↦ Σ𝑗 ∈ (0...(♯‘𝑡))((𝑔‘(𝑡 prefix 𝑗)) · (𝑖‘(𝑡 substr 〈𝑗, (♯‘𝑡)〉)))) → (𝑓 finSupp 0 ↔ (𝑡 ∈ Word 𝐴 ↦ Σ𝑗 ∈ (0...(♯‘𝑡))((𝑔‘(𝑡 prefix 𝑗)) · (𝑖‘(𝑡 substr 〈𝑗, (♯‘𝑡)〉)))) finSupp 0)) |
| 416 | 78 | a1i 11 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) → ℤ ∈ V) |
| 417 | | fzfid 14014 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑡 ∈ Word 𝐴) → (0...(♯‘𝑡)) ∈ Fin) |
| 418 | 294 | ad2antrr 726 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
(((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑡 ∈ Word 𝐴) ∧ 𝑗 ∈ (0...(♯‘𝑡))) → 𝑔:Word 𝐴⟶ℤ) |
| 419 | | pfxcl 14715 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑡 ∈ Word 𝐴 → (𝑡 prefix 𝑗) ∈ Word 𝐴) |
| 420 | 419 | ad2antlr 727 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
(((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑡 ∈ Word 𝐴) ∧ 𝑗 ∈ (0...(♯‘𝑡))) → (𝑡 prefix 𝑗) ∈ Word 𝐴) |
| 421 | 418, 420 | ffvelcdmd 7105 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
(((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑡 ∈ Word 𝐴) ∧ 𝑗 ∈ (0...(♯‘𝑡))) → (𝑔‘(𝑡 prefix 𝑗)) ∈ ℤ) |
| 422 | 184 | ad2antrr 726 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
(((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑡 ∈ Word 𝐴) ∧ 𝑗 ∈ (0...(♯‘𝑡))) → 𝑖:Word 𝐴⟶ℤ) |
| 423 | | swrdcl 14683 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑡 ∈ Word 𝐴 → (𝑡 substr 〈𝑗, (♯‘𝑡)〉) ∈ Word 𝐴) |
| 424 | 423 | ad2antlr 727 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
(((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑡 ∈ Word 𝐴) ∧ 𝑗 ∈ (0...(♯‘𝑡))) → (𝑡 substr 〈𝑗, (♯‘𝑡)〉) ∈ Word 𝐴) |
| 425 | 422, 424 | ffvelcdmd 7105 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
(((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑡 ∈ Word 𝐴) ∧ 𝑗 ∈ (0...(♯‘𝑡))) → (𝑖‘(𝑡 substr 〈𝑗, (♯‘𝑡)〉)) ∈ ℤ) |
| 426 | 421, 425 | zmulcld 12728 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑡 ∈ Word 𝐴) ∧ 𝑗 ∈ (0...(♯‘𝑡))) → ((𝑔‘(𝑡 prefix 𝑗)) · (𝑖‘(𝑡 substr 〈𝑗, (♯‘𝑡)〉))) ∈ ℤ) |
| 427 | 417, 426 | fsumzcl 15771 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑡 ∈ Word 𝐴) → Σ𝑗 ∈ (0...(♯‘𝑡))((𝑔‘(𝑡 prefix 𝑗)) · (𝑖‘(𝑡 substr 〈𝑗, (♯‘𝑡)〉))) ∈ ℤ) |
| 428 | 427 | fmpttd 7135 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) → (𝑡 ∈ Word 𝐴 ↦ Σ𝑗 ∈ (0...(♯‘𝑡))((𝑔‘(𝑡 prefix 𝑗)) · (𝑖‘(𝑡 substr 〈𝑗, (♯‘𝑡)〉)))):Word 𝐴⟶ℤ) |
| 429 | 416, 109,
428 | elmapdd 8881 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) → (𝑡 ∈ Word 𝐴 ↦ Σ𝑗 ∈ (0...(♯‘𝑡))((𝑔‘(𝑡 prefix 𝑗)) · (𝑖‘(𝑡 substr 〈𝑗, (♯‘𝑡)〉)))) ∈ (ℤ
↑m Word 𝐴)) |
| 430 | | 0zd 12625 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) → 0 ∈ ℤ) |
| 431 | 428 | ffund 6740 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) → Fun (𝑡 ∈ Word 𝐴 ↦ Σ𝑗 ∈ (0...(♯‘𝑡))((𝑔‘(𝑡 prefix 𝑗)) · (𝑖‘(𝑡 substr 〈𝑗, (♯‘𝑡)〉))))) |
| 432 | | ccatfn 14610 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ++ Fn (V
× V) |
| 433 | | fnfun 6668 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ( ++ Fn
(V × V) → Fun ++ ) |
| 434 | 432, 433 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . . 20
⊢ Fun
++ |
| 435 | | imafi 9353 |
. . . . . . . . . . . . . . . . . . . 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 7447 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑡 = 𝑤 → (0...(♯‘𝑡)) = (0...(♯‘𝑤))) |
| 439 | | fvoveq1 7454 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑡 = 𝑤 → (𝑔‘(𝑡 prefix 𝑗)) = (𝑔‘(𝑤 prefix 𝑗))) |
| 440 | | id 22 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝑡 = 𝑤 → 𝑡 = 𝑤) |
| 441 | 437 | opeq2d 4880 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝑡 = 𝑤 → 〈𝑗, (♯‘𝑡)〉 = 〈𝑗, (♯‘𝑤)〉) |
| 442 | 440, 441 | oveq12d 7449 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑡 = 𝑤 → (𝑡 substr 〈𝑗, (♯‘𝑡)〉) = (𝑤 substr 〈𝑗, (♯‘𝑤)〉)) |
| 443 | 442 | fveq2d 6910 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑡 = 𝑤 → (𝑖‘(𝑡 substr 〈𝑗, (♯‘𝑡)〉)) = (𝑖‘(𝑤 substr 〈𝑗, (♯‘𝑤)〉))) |
| 444 | 439, 443 | oveq12d 7449 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑡 = 𝑤 → ((𝑔‘(𝑡 prefix 𝑗)) · (𝑖‘(𝑡 substr 〈𝑗, (♯‘𝑡)〉))) = ((𝑔‘(𝑤 prefix 𝑗)) · (𝑖‘(𝑤 substr 〈𝑗, (♯‘𝑤)〉)))) |
| 445 | 444 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝑡 = 𝑤 ∧ 𝑗 ∈ (0...(♯‘𝑡))) → ((𝑔‘(𝑡 prefix 𝑗)) · (𝑖‘(𝑡 substr 〈𝑗, (♯‘𝑡)〉))) = ((𝑔‘(𝑤 prefix 𝑗)) · (𝑖‘(𝑤 substr 〈𝑗, (♯‘𝑤)〉)))) |
| 446 | 438, 445 | sumeq12dv 15742 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑡 = 𝑤 → Σ𝑗 ∈ (0...(♯‘𝑡))((𝑔‘(𝑡 prefix 𝑗)) · (𝑖‘(𝑡 substr 〈𝑗, (♯‘𝑡)〉))) = Σ𝑗 ∈ (0...(♯‘𝑤))((𝑔‘(𝑤 prefix 𝑗)) · (𝑖‘(𝑤 substr 〈𝑗, (♯‘𝑤)〉)))) |
| 447 | | oveq1 7438 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ (𝑢 = (𝑤 prefix 𝑗) → (𝑢 ++ 𝑣) = ((𝑤 prefix 𝑗) ++ 𝑣)) |
| 448 | 447 | eqeq2d 2748 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ (𝑢 = (𝑤 prefix 𝑗) → (𝑤 = (𝑢 ++ 𝑣) ↔ 𝑤 = ((𝑤 prefix 𝑗) ++ 𝑣))) |
| 449 | | oveq2 7439 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ (𝑣 = (𝑤 substr 〈𝑗, (♯‘𝑤)〉) → ((𝑤 prefix 𝑗) ++ 𝑣) = ((𝑤 prefix 𝑗) ++ (𝑤 substr 〈𝑗, (♯‘𝑤)〉))) |
| 450 | 449 | eqeq2d 2748 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
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 12625 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
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 3963 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢ ((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑤 ∈ (Word 𝐴 ∖ ( ++ “ ((𝑔 supp 0) × (𝑖 supp 0))))) → 𝑤 ∈ Word 𝐴) |
| 456 | 455 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢
(((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑤 ∈ (Word 𝐴 ∖ ( ++ “ ((𝑔 supp 0) × (𝑖 supp 0))))) ∧ 𝑗 ∈ (0...(♯‘𝑤))) → 𝑤 ∈ Word 𝐴) |
| 457 | | pfxcl 14715 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
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 32691 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
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 14683 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
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 32691 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
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 14748 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
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 2743 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢
(((((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑤 ∈ (Word 𝐴 ∖ ( ++ “ ((𝑔 supp 0) × (𝑖 supp 0))))) ∧ 𝑗 ∈ (0...(♯‘𝑤))) ∧ (𝑔‘(𝑤 prefix 𝑗)) ≠ 0) ∧ (𝑖‘(𝑤 substr 〈𝑗, (♯‘𝑤)〉)) ≠ 0) → 𝑤 = ((𝑤 prefix 𝑗) ++ (𝑤 substr 〈𝑗, (♯‘𝑤)〉))) |
| 473 | 448, 450,
461, 467, 472 | 2rspcedvdw 3636 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢
(((((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑤 ∈ (Word 𝐴 ∖ ( ++ “ ((𝑔 supp 0) × (𝑖 supp 0))))) ∧ 𝑗 ∈ (0...(♯‘𝑤))) ∧ (𝑔‘(𝑤 prefix 𝑗)) ≠ 0) ∧ (𝑖‘(𝑤 substr 〈𝑗, (♯‘𝑤)〉)) ≠ 0) → ∃𝑢 ∈ (𝑔 supp 0)∃𝑣 ∈ (𝑖 supp 0)𝑤 = (𝑢 ++ 𝑣)) |
| 474 | | fnov 7564 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ ( ++ Fn
(V × V) ↔ ++ = (𝑢 ∈ V, 𝑣 ∈ V ↦ (𝑢 ++ 𝑣))) |
| 475 | 432, 474 | mpbi 230 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ ++ =
(𝑢 ∈ V, 𝑣 ∈ V ↦ (𝑢 ++ 𝑣)) |
| 476 | 200 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ (⊤
→ 𝑤 ∈
V) |
| 477 | | ssv 4008 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ (𝑔 supp 0) ⊆
V |
| 478 | 477 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ (⊤
→ (𝑔 supp 0) ⊆
V) |
| 479 | | ssv 4008 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ (𝑖 supp 0) ⊆
V |
| 480 | 479 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ (⊤
→ (𝑖 supp 0) ⊆
V) |
| 481 | 475, 476,
478, 480 | elimampo 7570 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ (⊤
→ (𝑤 ∈ ( ++
“ ((𝑔 supp 0) ×
(𝑖 supp 0))) ↔
∃𝑢 ∈ (𝑔 supp 0)∃𝑣 ∈ (𝑖 supp 0)𝑤 = (𝑢 ++ 𝑣))) |
| 482 | 481 | mptru 1547 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 3964 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 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 2941 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ ((𝑔‘(𝑤 prefix 𝑗)) ≠ 0 ↔ ¬ (𝑔‘(𝑤 prefix 𝑗)) = 0) |
| 490 | | df-ne 2941 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 993 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 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 7105 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢
(((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑤 ∈ (Word 𝐴 ∖ ( ++ “ ((𝑔 supp 0) × (𝑖 supp 0))))) ∧ 𝑗 ∈ (0...(♯‘𝑤))) → (𝑔‘(𝑤 prefix 𝑗)) ∈ ℤ) |
| 498 | 497 | zcnd 12723 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢
(((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑤 ∈ (Word 𝐴 ∖ ( ++ “ ((𝑔 supp 0) × (𝑖 supp 0))))) ∧ 𝑗 ∈ (0...(♯‘𝑤))) → (𝑔‘(𝑤 prefix 𝑗)) ∈ ℂ) |
| 499 | 184 | ad2antrr 726 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢
(((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑤 ∈ (Word 𝐴 ∖ ( ++ “ ((𝑔 supp 0) × (𝑖 supp 0))))) ∧ 𝑗 ∈ (0...(♯‘𝑤))) → 𝑖:Word 𝐴⟶ℤ) |
| 500 | 499, 464 | ffvelcdmd 7105 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢
(((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑤 ∈ (Word 𝐴 ∖ ( ++ “ ((𝑔 supp 0) × (𝑖 supp 0))))) ∧ 𝑗 ∈ (0...(♯‘𝑤))) → (𝑖‘(𝑤 substr 〈𝑗, (♯‘𝑤)〉)) ∈ ℤ) |
| 501 | 500 | zcnd 12723 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢
(((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑤 ∈ (Word 𝐴 ∖ ( ++ “ ((𝑔 supp 0) × (𝑖 supp 0))))) ∧ 𝑗 ∈ (0...(♯‘𝑤))) → (𝑖‘(𝑤 substr 〈𝑗, (♯‘𝑤)〉)) ∈ ℂ) |
| 502 | 498, 501 | mul0ord 11913 |
. . . . . . . . . . . . . . . . . . . . . . . . 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 15738 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑤 ∈ (Word 𝐴 ∖ ( ++ “ ((𝑔 supp 0) × (𝑖 supp 0))))) → Σ𝑗 ∈ (0...(♯‘𝑤))((𝑔‘(𝑤 prefix 𝑗)) · (𝑖‘(𝑤 substr 〈𝑗, (♯‘𝑤)〉))) = Σ𝑗 ∈ (0...(♯‘𝑤))0) |
| 505 | | fzssuz 13605 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
(0...(♯‘𝑤)) ⊆
(ℤ≥‘0) |
| 506 | | sumz 15758 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢
(((0...(♯‘𝑤)) ⊆ (ℤ≥‘0)
∨ (0...(♯‘𝑤)) ∈ Fin) → Σ𝑗 ∈
(0...(♯‘𝑤))0 =
0) |
| 507 | 506 | orcs 876 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
((0...(♯‘𝑤)) ⊆ (ℤ≥‘0)
→ Σ𝑗 ∈
(0...(♯‘𝑤))0 =
0) |
| 508 | 505, 507 | mp1i 13 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑤 ∈ (Word 𝐴 ∖ ( ++ “ ((𝑔 supp 0) × (𝑖 supp 0))))) → Σ𝑗 ∈ (0...(♯‘𝑤))0 = 0) |
| 509 | 504, 508 | eqtrd 2777 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑤 ∈ (Word 𝐴 ∖ ( ++ “ ((𝑔 supp 0) × (𝑖 supp 0))))) → Σ𝑗 ∈ (0...(♯‘𝑤))((𝑔‘(𝑤 prefix 𝑗)) · (𝑖‘(𝑤 substr 〈𝑗, (♯‘𝑤)〉))) = 0) |
| 510 | 446, 509 | sylan9eqr 2799 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
(((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑤 ∈ (Word 𝐴 ∖ ( ++ “ ((𝑔 supp 0) × (𝑖 supp 0))))) ∧ 𝑡 = 𝑤) → Σ𝑗 ∈ (0...(♯‘𝑡))((𝑔‘(𝑡 prefix 𝑗)) · (𝑖‘(𝑡 substr 〈𝑗, (♯‘𝑡)〉))) = 0) |
| 511 | | 0zd 12625 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑤 ∈ (Word 𝐴 ∖ ( ++ “ ((𝑔 supp 0) × (𝑖 supp 0))))) → 0 ∈
ℤ) |
| 512 | 370, 510,
455, 511 | fvmptd2 7024 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) ∧ 𝑤 ∈ (Word 𝐴 ∖ ( ++ “ ((𝑔 supp 0) × (𝑖 supp 0))))) → ((𝑡 ∈ Word 𝐴 ↦ Σ𝑗 ∈ (0...(♯‘𝑡))((𝑔‘(𝑡 prefix 𝑗)) · (𝑖‘(𝑡 substr 〈𝑗, (♯‘𝑡)〉))))‘𝑤) = 0) |
| 513 | 428, 512 | suppss 8219 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) → ((𝑡 ∈ Word 𝐴 ↦ Σ𝑗 ∈ (0...(♯‘𝑡))((𝑔‘(𝑡 prefix 𝑗)) · (𝑖‘(𝑡 substr 〈𝑗, (♯‘𝑡)〉)))) supp 0) ⊆ ( ++ “
((𝑔 supp 0) × (𝑖 supp 0)))) |
| 514 | 436, 513 | ssfid 9301 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) → ((𝑡 ∈ Word 𝐴 ↦ Σ𝑗 ∈ (0...(♯‘𝑡))((𝑔‘(𝑡 prefix 𝑗)) · (𝑖‘(𝑡 substr 〈𝑗, (♯‘𝑡)〉)))) supp 0) ∈
Fin) |
| 515 | 429, 430,
431, 514 | isfsuppd 9406 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) → (𝑡 ∈ Word 𝐴 ↦ Σ𝑗 ∈ (0...(♯‘𝑡))((𝑔‘(𝑡 prefix 𝑗)) · (𝑖‘(𝑡 substr 〈𝑗, (♯‘𝑡)〉)))) finSupp 0) |
| 516 | 415, 429,
515 | elrabd 3694 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) → (𝑡 ∈ Word 𝐴 ↦ Σ𝑗 ∈ (0...(♯‘𝑡))((𝑔‘(𝑡 prefix 𝑗)) · (𝑖‘(𝑡 substr 〈𝑗, (♯‘𝑡)〉)))) ∈ {𝑓 ∈ (ℤ ↑m Word
𝐴) ∣ 𝑓 finSupp 0}) |
| 517 | 516, 6 | eleqtrrdi 2852 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) → (𝑡 ∈ Word 𝐴 ↦ Σ𝑗 ∈ (0...(♯‘𝑡))((𝑔‘(𝑡 prefix 𝑗)) · (𝑖‘(𝑡 substr 〈𝑗, (♯‘𝑡)〉)))) ∈ 𝐹) |
| 518 | | fveq2 6906 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑣 = 𝑤 → ((𝑡 ∈ Word 𝐴 ↦ Σ𝑗 ∈ (0...(♯‘𝑡))((𝑔‘(𝑡 prefix 𝑗)) · (𝑖‘(𝑡 substr 〈𝑗, (♯‘𝑡)〉))))‘𝑣) = ((𝑡 ∈ Word 𝐴 ↦ Σ𝑗 ∈ (0...(♯‘𝑡))((𝑔‘(𝑡 prefix 𝑗)) · (𝑖‘(𝑡 substr 〈𝑗, (♯‘𝑡)〉))))‘𝑤)) |
| 519 | 518, 145 | oveq12d 7449 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑣 = 𝑤 → (((𝑡 ∈ Word 𝐴 ↦ Σ𝑗 ∈ (0...(♯‘𝑡))((𝑔‘(𝑡 prefix 𝑗)) · (𝑖‘(𝑡 substr 〈𝑗, (♯‘𝑡)〉))))‘𝑣) · (𝑀 Σg 𝑣)) = (((𝑡 ∈ Word 𝐴 ↦ Σ𝑗 ∈ (0...(♯‘𝑡))((𝑔‘(𝑡 prefix 𝑗)) · (𝑖‘(𝑡 substr 〈𝑗, (♯‘𝑡)〉))))‘𝑤) · (𝑀 Σg 𝑤))) |
| 520 | 519 | cbvmptv 5255 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑣 ∈ Word 𝐴 ↦ (((𝑡 ∈ Word 𝐴 ↦ Σ𝑗 ∈ (0...(♯‘𝑡))((𝑔‘(𝑡 prefix 𝑗)) · (𝑖‘(𝑡 substr 〈𝑗, (♯‘𝑡)〉))))‘𝑣) · (𝑀 Σg 𝑣))) = (𝑤 ∈ Word 𝐴 ↦ (((𝑡 ∈ Word 𝐴 ↦ Σ𝑗 ∈ (0...(♯‘𝑡))((𝑔‘(𝑡 prefix 𝑗)) · (𝑖‘(𝑡 substr 〈𝑗, (♯‘𝑡)〉))))‘𝑤) · (𝑀 Σg 𝑤))) |
| 521 | 520 | oveq2i 7442 |
. . . . . . . . . . . . . . . 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 3625 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) → ∃ℎ ∈ 𝐹 (𝑅 Σg (𝑣 ∈ Word 𝐴 ↦ (((𝑡 ∈ Word 𝐴 ↦ Σ𝑗 ∈ (0...(♯‘𝑡))((𝑔‘(𝑡 prefix 𝑗)) · (𝑖‘(𝑡 substr 〈𝑗, (♯‘𝑡)〉))))‘𝑣) · (𝑀 Σg 𝑣)))) = (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((ℎ‘𝑤) · (𝑀 Σg 𝑤))))) |
| 524 | | ovexd 7466 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) → (𝑅 Σg (𝑣 ∈ Word 𝐴 ↦ (((𝑡 ∈ Word 𝐴 ↦ Σ𝑗 ∈ (0...(♯‘𝑡))((𝑔‘(𝑡 prefix 𝑗)) · (𝑖‘(𝑡 substr 〈𝑗, (♯‘𝑡)〉))))‘𝑣) · (𝑀 Σg 𝑣)))) ∈ V) |
| 525 | 409, 523,
524 | elrnmptd 5974 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) → (𝑅 Σg (𝑣 ∈ Word 𝐴 ↦ (((𝑡 ∈ Word 𝐴 ↦ Σ𝑗 ∈ (0...(♯‘𝑡))((𝑔‘(𝑡 prefix 𝑗)) · (𝑖‘(𝑡 substr 〈𝑗, (♯‘𝑡)〉))))‘𝑣) · (𝑀 Σg 𝑣)))) ∈ ran (𝑔 ∈ 𝐹 ↦ (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑔‘𝑤) · (𝑀 Σg 𝑤)))))) |
| 526 | 525, 8 | eleqtrrdi 2852 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑖 ∈ 𝐹) → (𝑅 Σg (𝑣 ∈ Word 𝐴 ↦ (((𝑡 ∈ Word 𝐴 ↦ Σ𝑗 ∈ (0...(♯‘𝑡))((𝑔‘(𝑡 prefix 𝑗)) · (𝑖‘(𝑡 substr 〈𝑗, (♯‘𝑡)〉))))‘𝑣) · (𝑀 Σg 𝑣)))) ∈ 𝑆) |
| 527 | 404, 526 | eqeltrd 2841 |
. . . . . . . . . . 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 2841 |
. . . . . 6
⊢
(((((((𝜑 ∧ 𝑥 ∈ 𝑆) ∧ 𝑦 ∈ 𝑆) ∧ 𝑔 ∈ 𝐹) ∧ 𝑥 = (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑔‘𝑤) · (𝑀 Σg 𝑤))))) ∧ 𝑖 ∈ 𝐹) ∧ 𝑦 = (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑖‘𝑤) · (𝑀 Σg 𝑤))))) → (𝑥(.r‘𝑅)𝑦) ∈ 𝑆) |
| 533 | 8 | eleq2i 2833 |
. . . . . . . . 9
⊢ (𝑦 ∈ 𝑆 ↔ 𝑦 ∈ ran (𝑔 ∈ 𝐹 ↦ (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑔‘𝑤) · (𝑀 Σg 𝑤)))))) |
| 534 | 169 | oveq2d 7447 |
. . . . . . . . . . . 12
⊢ (𝑔 = 𝑖 → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑔‘𝑤) · (𝑀 Σg 𝑤)))) = (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑖‘𝑤) · (𝑀 Σg 𝑤))))) |
| 535 | 534 | cbvmptv 5255 |
. . . . . . . . . . 11
⊢ (𝑔 ∈ 𝐹 ↦ (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑔‘𝑤) · (𝑀 Σg 𝑤))))) = (𝑖 ∈ 𝐹 ↦ (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑖‘𝑤) · (𝑀 Σg 𝑤))))) |
| 536 | 535 | elrnmpt 5969 |
. . . . . . . . . 10
⊢ (𝑦 ∈ V → (𝑦 ∈ ran (𝑔 ∈ 𝐹 ↦ (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑔‘𝑤) · (𝑀 Σg 𝑤))))) ↔ ∃𝑖 ∈ 𝐹 𝑦 = (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑖‘𝑤) · (𝑀 Σg 𝑤)))))) |
| 537 | 536 | elv 3485 |
. . . . . . . . 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 3162 |
. . . . 5
⊢
(((((𝜑 ∧ 𝑥 ∈ 𝑆) ∧ 𝑦 ∈ 𝑆) ∧ 𝑔 ∈ 𝐹) ∧ 𝑥 = (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑔‘𝑤) · (𝑀 Σg 𝑤))))) → (𝑥(.r‘𝑅)𝑦) ∈ 𝑆) |
| 542 | 8 | eleq2i 2833 |
. . . . . . 7
⊢ (𝑥 ∈ 𝑆 ↔ 𝑥 ∈ ran (𝑔 ∈ 𝐹 ↦ (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑔‘𝑤) · (𝑀 Σg 𝑤)))))) |
| 543 | 71 | elrnmpt 5969 |
. . . . . . . 8
⊢ (𝑥 ∈ V → (𝑥 ∈ ran (𝑔 ∈ 𝐹 ↦ (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑔‘𝑤) · (𝑀 Σg 𝑤))))) ↔ ∃𝑔 ∈ 𝐹 𝑥 = (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑔‘𝑤) · (𝑀 Σg 𝑤)))))) |
| 544 | 543 | elv 3485 |
. . . . . . 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 3162 |
. . . 4
⊢ (((𝜑 ∧ 𝑥 ∈ 𝑆) ∧ 𝑦 ∈ 𝑆) → (𝑥(.r‘𝑅)𝑦) ∈ 𝑆) |
| 548 | 547 | anasss 466 |
. . 3
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆)) → (𝑥(.r‘𝑅)𝑦) ∈ 𝑆) |
| 549 | 548 | ralrimivva 3202 |
. 2
⊢ (𝜑 → ∀𝑥 ∈ 𝑆 ∀𝑦 ∈ 𝑆 (𝑥(.r‘𝑅)𝑦) ∈ 𝑆) |
| 550 | 2, 24, 108 | issubrg2 20592 |
. . 3
⊢ (𝑅 ∈ Ring → (𝑆 ∈ (SubRing‘𝑅) ↔ (𝑆 ∈ (SubGrp‘𝑅) ∧ (1r‘𝑅) ∈ 𝑆 ∧ ∀𝑥 ∈ 𝑆 ∀𝑦 ∈ 𝑆 (𝑥(.r‘𝑅)𝑦) ∈ 𝑆))) |
| 551 | 550 | biimpar 477 |
. 2
⊢ ((𝑅 ∈ Ring ∧ (𝑆 ∈ (SubGrp‘𝑅) ∧
(1r‘𝑅)
∈ 𝑆 ∧
∀𝑥 ∈ 𝑆 ∀𝑦 ∈ 𝑆 (𝑥(.r‘𝑅)𝑦) ∈ 𝑆)) → 𝑆 ∈ (SubRing‘𝑅)) |
| 552 | 1, 9, 104, 549, 551 | syl13anc 1374 |
1
⊢ (𝜑 → 𝑆 ∈ (SubRing‘𝑅)) |