Step | Hyp | Ref
| Expression |
1 | | elrgspn.r |
. . 3
⊢ (𝜑 → 𝑅 ∈ Ring) |
2 | | elrgspn.b |
. . . 4
⊢ 𝐵 = (Base‘𝑅) |
3 | 2 | a1i 11 |
. . 3
⊢ (𝜑 → 𝐵 = (Base‘𝑅)) |
4 | | elrgspn.a |
. . 3
⊢ (𝜑 → 𝐴 ⊆ 𝐵) |
5 | | elrgspn.n |
. . . 4
⊢ 𝑁 = (RingSpan‘𝑅) |
6 | 5 | a1i 11 |
. . 3
⊢ (𝜑 → 𝑁 = (RingSpan‘𝑅)) |
7 | | eqidd 2735 |
. . 3
⊢ (𝜑 → (𝑁‘𝐴) = (𝑁‘𝐴)) |
8 | 1, 3, 4, 6, 7 | rgspnval 20628 |
. 2
⊢ (𝜑 → (𝑁‘𝐴) = ∩ {𝑡 ∈ (SubRing‘𝑅) ∣ 𝐴 ⊆ 𝑡}) |
9 | | sseq2 4021 |
. . . . 5
⊢ (𝑡 = 𝑆 → (𝐴 ⊆ 𝑡 ↔ 𝐴 ⊆ 𝑆)) |
10 | | elrgspn.m |
. . . . . 6
⊢ 𝑀 = (mulGrp‘𝑅) |
11 | | elrgspn.x |
. . . . . 6
⊢ · =
(.g‘𝑅) |
12 | | elrgspn.f |
. . . . . 6
⊢ 𝐹 = {𝑓 ∈ (ℤ ↑m Word
𝐴) ∣ 𝑓 finSupp 0} |
13 | | elrgspnlem1.1 |
. . . . . 6
⊢ 𝑆 = ran (𝑔 ∈ 𝐹 ↦ (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑔‘𝑤) · (𝑀 Σg 𝑤))))) |
14 | 2, 10, 11, 5, 12, 1, 4, 13 | elrgspnlem2 33232 |
. . . . 5
⊢ (𝜑 → 𝑆 ∈ (SubRing‘𝑅)) |
15 | 2, 10, 11, 5, 12, 1, 4, 13 | elrgspnlem3 33233 |
. . . . 5
⊢ (𝜑 → 𝐴 ⊆ 𝑆) |
16 | 9, 14, 15 | elrabd 3696 |
. . . 4
⊢ (𝜑 → 𝑆 ∈ {𝑡 ∈ (SubRing‘𝑅) ∣ 𝐴 ⊆ 𝑡}) |
17 | | intss1 4967 |
. . . 4
⊢ (𝑆 ∈ {𝑡 ∈ (SubRing‘𝑅) ∣ 𝐴 ⊆ 𝑡} → ∩ {𝑡 ∈ (SubRing‘𝑅) ∣ 𝐴 ⊆ 𝑡} ⊆ 𝑆) |
18 | 16, 17 | syl 17 |
. . 3
⊢ (𝜑 → ∩ {𝑡
∈ (SubRing‘𝑅)
∣ 𝐴 ⊆ 𝑡} ⊆ 𝑆) |
19 | | simpr 484 |
. . . . . . . . . 10
⊢
((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑠 ∈ 𝑆) ∧ 𝑔 ∈ 𝐹) ∧ 𝑠 = (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑔‘𝑤) · (𝑀 Σg 𝑤))))) → 𝑠 = (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑔‘𝑤) · (𝑀 Σg 𝑤))))) |
20 | | eqidd 2735 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) → (𝑔 supp 0) = (𝑔 supp 0)) |
21 | | oveq1 7437 |
. . . . . . . . . . . . . . 15
⊢ (𝑓 = 𝑔 → (𝑓 supp 0) = (𝑔 supp 0)) |
22 | 21 | eqeq1d 2736 |
. . . . . . . . . . . . . 14
⊢ (𝑓 = 𝑔 → ((𝑓 supp 0) = (𝑔 supp 0) ↔ (𝑔 supp 0) = (𝑔 supp 0))) |
23 | | fveq1 6905 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑓 = 𝑔 → (𝑓‘𝑤) = (𝑔‘𝑤)) |
24 | 23 | oveq1d 7445 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑓 = 𝑔 → ((𝑓‘𝑤) · (𝑀 Σg 𝑤)) = ((𝑔‘𝑤) · (𝑀 Σg 𝑤))) |
25 | 24 | mpteq2dv 5249 |
. . . . . . . . . . . . . . . 16
⊢ (𝑓 = 𝑔 → (𝑤 ∈ Word 𝐴 ↦ ((𝑓‘𝑤) · (𝑀 Σg 𝑤))) = (𝑤 ∈ Word 𝐴 ↦ ((𝑔‘𝑤) · (𝑀 Σg 𝑤)))) |
26 | 25 | oveq2d 7446 |
. . . . . . . . . . . . . . 15
⊢ (𝑓 = 𝑔 → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑓‘𝑤) · (𝑀 Σg 𝑤)))) = (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑔‘𝑤) · (𝑀 Σg 𝑤))))) |
27 | 26 | eleq1d 2823 |
. . . . . . . . . . . . . 14
⊢ (𝑓 = 𝑔 → ((𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑓‘𝑤) · (𝑀 Σg 𝑤)))) ∈ 𝑡 ↔ (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑔‘𝑤) · (𝑀 Σg 𝑤)))) ∈ 𝑡)) |
28 | 22, 27 | imbi12d 344 |
. . . . . . . . . . . . 13
⊢ (𝑓 = 𝑔 → (((𝑓 supp 0) = (𝑔 supp 0) → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑓‘𝑤) · (𝑀 Σg 𝑤)))) ∈ 𝑡) ↔ ((𝑔 supp 0) = (𝑔 supp 0) → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑔‘𝑤) · (𝑀 Σg 𝑤)))) ∈ 𝑡))) |
29 | | eqeq2 2746 |
. . . . . . . . . . . . . . . 16
⊢ (𝑖 = ∅ → ((𝑓 supp 0) = 𝑖 ↔ (𝑓 supp 0) = ∅)) |
30 | 29 | imbi1d 341 |
. . . . . . . . . . . . . . 15
⊢ (𝑖 = ∅ → (((𝑓 supp 0) = 𝑖 → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑓‘𝑤) · (𝑀 Σg 𝑤)))) ∈ 𝑡) ↔ ((𝑓 supp 0) = ∅ → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑓‘𝑤) · (𝑀 Σg 𝑤)))) ∈ 𝑡))) |
31 | 30 | ralbidv 3175 |
. . . . . . . . . . . . . 14
⊢ (𝑖 = ∅ → (∀𝑓 ∈ 𝐹 ((𝑓 supp 0) = 𝑖 → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑓‘𝑤) · (𝑀 Σg 𝑤)))) ∈ 𝑡) ↔ ∀𝑓 ∈ 𝐹 ((𝑓 supp 0) = ∅ → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑓‘𝑤) · (𝑀 Σg 𝑤)))) ∈ 𝑡))) |
32 | | eqeq2 2746 |
. . . . . . . . . . . . . . . 16
⊢ (𝑖 = ℎ → ((𝑓 supp 0) = 𝑖 ↔ (𝑓 supp 0) = ℎ)) |
33 | 32 | imbi1d 341 |
. . . . . . . . . . . . . . 15
⊢ (𝑖 = ℎ → (((𝑓 supp 0) = 𝑖 → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑓‘𝑤) · (𝑀 Σg 𝑤)))) ∈ 𝑡) ↔ ((𝑓 supp 0) = ℎ → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑓‘𝑤) · (𝑀 Σg 𝑤)))) ∈ 𝑡))) |
34 | 33 | ralbidv 3175 |
. . . . . . . . . . . . . 14
⊢ (𝑖 = ℎ → (∀𝑓 ∈ 𝐹 ((𝑓 supp 0) = 𝑖 → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑓‘𝑤) · (𝑀 Σg 𝑤)))) ∈ 𝑡) ↔ ∀𝑓 ∈ 𝐹 ((𝑓 supp 0) = ℎ → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑓‘𝑤) · (𝑀 Σg 𝑤)))) ∈ 𝑡))) |
35 | | eqeq2 2746 |
. . . . . . . . . . . . . . . 16
⊢ (𝑖 = (ℎ ∪ {𝑥}) → ((𝑓 supp 0) = 𝑖 ↔ (𝑓 supp 0) = (ℎ ∪ {𝑥}))) |
36 | 35 | imbi1d 341 |
. . . . . . . . . . . . . . 15
⊢ (𝑖 = (ℎ ∪ {𝑥}) → (((𝑓 supp 0) = 𝑖 → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑓‘𝑤) · (𝑀 Σg 𝑤)))) ∈ 𝑡) ↔ ((𝑓 supp 0) = (ℎ ∪ {𝑥}) → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑓‘𝑤) · (𝑀 Σg 𝑤)))) ∈ 𝑡))) |
37 | 36 | ralbidv 3175 |
. . . . . . . . . . . . . 14
⊢ (𝑖 = (ℎ ∪ {𝑥}) → (∀𝑓 ∈ 𝐹 ((𝑓 supp 0) = 𝑖 → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑓‘𝑤) · (𝑀 Σg 𝑤)))) ∈ 𝑡) ↔ ∀𝑓 ∈ 𝐹 ((𝑓 supp 0) = (ℎ ∪ {𝑥}) → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑓‘𝑤) · (𝑀 Σg 𝑤)))) ∈ 𝑡))) |
38 | | eqeq2 2746 |
. . . . . . . . . . . . . . . 16
⊢ (𝑖 = (𝑔 supp 0) → ((𝑓 supp 0) = 𝑖 ↔ (𝑓 supp 0) = (𝑔 supp 0))) |
39 | 38 | imbi1d 341 |
. . . . . . . . . . . . . . 15
⊢ (𝑖 = (𝑔 supp 0) → (((𝑓 supp 0) = 𝑖 → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑓‘𝑤) · (𝑀 Σg 𝑤)))) ∈ 𝑡) ↔ ((𝑓 supp 0) = (𝑔 supp 0) → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑓‘𝑤) · (𝑀 Σg 𝑤)))) ∈ 𝑡))) |
40 | 39 | ralbidv 3175 |
. . . . . . . . . . . . . 14
⊢ (𝑖 = (𝑔 supp 0) → (∀𝑓 ∈ 𝐹 ((𝑓 supp 0) = 𝑖 → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑓‘𝑤) · (𝑀 Σg 𝑤)))) ∈ 𝑡) ↔ ∀𝑓 ∈ 𝐹 ((𝑓 supp 0) = (𝑔 supp 0) → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑓‘𝑤) · (𝑀 Σg 𝑤)))) ∈ 𝑡))) |
41 | | eqid 2734 |
. . . . . . . . . . . . . . . . . . 19
⊢
(0g‘𝑅) = (0g‘𝑅) |
42 | 1 | ringcmnd 20297 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → 𝑅 ∈ CMnd) |
43 | 42 | ad5antr 734 |
. . . . . . . . . . . . . . . . . . 19
⊢
((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ 𝑓 ∈ 𝐹) ∧ (𝑓 supp 0) = ∅) → 𝑅 ∈ CMnd) |
44 | 2 | fvexi 6920 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ 𝐵 ∈ V |
45 | 44 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝜑 → 𝐵 ∈ V) |
46 | 45, 4 | ssexd 5329 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝜑 → 𝐴 ∈ V) |
47 | | wrdexg 14558 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝐴 ∈ V → Word 𝐴 ∈ V) |
48 | 46, 47 | syl 17 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → Word 𝐴 ∈ V) |
49 | 48 | ad5antr 734 |
. . . . . . . . . . . . . . . . . . 19
⊢
((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ 𝑓 ∈ 𝐹) ∧ (𝑓 supp 0) = ∅) → Word 𝐴 ∈ V) |
50 | | simp-4l 783 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢
(((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ 𝑓 ∈ 𝐹) → 𝜑) |
51 | 12 | reqabi 3456 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝑓 ∈ 𝐹 ↔ (𝑓 ∈ (ℤ ↑m Word
𝐴) ∧ 𝑓 finSupp 0)) |
52 | 51 | simplbi 497 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑓 ∈ 𝐹 → 𝑓 ∈ (ℤ ↑m Word
𝐴)) |
53 | 52 | adantl 481 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢
(((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ 𝑓 ∈ 𝐹) → 𝑓 ∈ (ℤ ↑m Word
𝐴)) |
54 | | zex 12619 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ℤ
∈ V |
55 | 54 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝜑 → ℤ ∈
V) |
56 | 55, 48 | elmapd 8878 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝜑 → (𝑓 ∈ (ℤ ↑m Word
𝐴) ↔ 𝑓:Word 𝐴⟶ℤ)) |
57 | 56 | biimpa 476 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝜑 ∧ 𝑓 ∈ (ℤ ↑m Word
𝐴)) → 𝑓:Word 𝐴⟶ℤ) |
58 | 50, 53, 57 | syl2anc 584 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
(((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ 𝑓 ∈ 𝐹) → 𝑓:Word 𝐴⟶ℤ) |
59 | 58 | ffnd 6737 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
(((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ 𝑓 ∈ 𝐹) → 𝑓 Fn Word 𝐴) |
60 | 59 | ad2antrr 726 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
(((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ 𝑓 ∈ 𝐹) ∧ (𝑓 supp 0) = ∅) ∧ 𝑤 ∈ (Word 𝐴 ∖ ∅)) → 𝑓 Fn Word 𝐴) |
61 | 49 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
(((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ 𝑓 ∈ 𝐹) ∧ (𝑓 supp 0) = ∅) ∧ 𝑤 ∈ (Word 𝐴 ∖ ∅)) → Word 𝐴 ∈ V) |
62 | | 0zd 12622 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
(((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ 𝑓 ∈ 𝐹) ∧ (𝑓 supp 0) = ∅) ∧ 𝑤 ∈ (Word 𝐴 ∖ ∅)) → 0 ∈
ℤ) |
63 | | simpr 484 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
(((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ 𝑓 ∈ 𝐹) ∧ (𝑓 supp 0) = ∅) ∧ 𝑤 ∈ (Word 𝐴 ∖ ∅)) → 𝑤 ∈ (Word 𝐴 ∖ ∅)) |
64 | 63 | eldifad 3974 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
(((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ 𝑓 ∈ 𝐹) ∧ (𝑓 supp 0) = ∅) ∧ 𝑤 ∈ (Word 𝐴 ∖ ∅)) → 𝑤 ∈ Word 𝐴) |
65 | 63 | eldifbd 3975 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
(((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ 𝑓 ∈ 𝐹) ∧ (𝑓 supp 0) = ∅) ∧ 𝑤 ∈ (Word 𝐴 ∖ ∅)) → ¬ 𝑤 ∈
∅) |
66 | | simplr 769 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
(((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ 𝑓 ∈ 𝐹) ∧ (𝑓 supp 0) = ∅) ∧ 𝑤 ∈ (Word 𝐴 ∖ ∅)) → (𝑓 supp 0) =
∅) |
67 | 65, 66 | neleqtrrd 2861 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
(((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ 𝑓 ∈ 𝐹) ∧ (𝑓 supp 0) = ∅) ∧ 𝑤 ∈ (Word 𝐴 ∖ ∅)) → ¬ 𝑤 ∈ (𝑓 supp 0)) |
68 | 64, 67 | eldifd 3973 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
(((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ 𝑓 ∈ 𝐹) ∧ (𝑓 supp 0) = ∅) ∧ 𝑤 ∈ (Word 𝐴 ∖ ∅)) → 𝑤 ∈ (Word 𝐴 ∖ (𝑓 supp 0))) |
69 | 60, 61, 62, 68 | fvdifsupp 8194 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
(((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ 𝑓 ∈ 𝐹) ∧ (𝑓 supp 0) = ∅) ∧ 𝑤 ∈ (Word 𝐴 ∖ ∅)) → (𝑓‘𝑤) = 0) |
70 | 69 | oveq1d 7445 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ 𝑓 ∈ 𝐹) ∧ (𝑓 supp 0) = ∅) ∧ 𝑤 ∈ (Word 𝐴 ∖ ∅)) → ((𝑓‘𝑤) · (𝑀 Σg 𝑤)) = (0 · (𝑀 Σg 𝑤))) |
71 | 10 | ringmgp 20256 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑅 ∈ Ring → 𝑀 ∈ Mnd) |
72 | 1, 71 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝜑 → 𝑀 ∈ Mnd) |
73 | 72 | ad6antr 736 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
(((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ 𝑓 ∈ 𝐹) ∧ (𝑓 supp 0) = ∅) ∧ 𝑤 ∈ (Word 𝐴 ∖ ∅)) → 𝑀 ∈ Mnd) |
74 | | sswrd 14556 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝐴 ⊆ 𝐵 → Word 𝐴 ⊆ Word 𝐵) |
75 | 4, 74 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝜑 → Word 𝐴 ⊆ Word 𝐵) |
76 | 75 | ad6antr 736 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
(((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ 𝑓 ∈ 𝐹) ∧ (𝑓 supp 0) = ∅) ∧ 𝑤 ∈ (Word 𝐴 ∖ ∅)) → Word 𝐴 ⊆ Word 𝐵) |
77 | 76, 64 | sseldd 3995 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
(((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ 𝑓 ∈ 𝐹) ∧ (𝑓 supp 0) = ∅) ∧ 𝑤 ∈ (Word 𝐴 ∖ ∅)) → 𝑤 ∈ Word 𝐵) |
78 | 10, 2 | mgpbas 20157 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ 𝐵 = (Base‘𝑀) |
79 | 78 | gsumwcl 18864 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑀 ∈ Mnd ∧ 𝑤 ∈ Word 𝐵) → (𝑀 Σg 𝑤) ∈ 𝐵) |
80 | 73, 77, 79 | syl2anc 584 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
(((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ 𝑓 ∈ 𝐹) ∧ (𝑓 supp 0) = ∅) ∧ 𝑤 ∈ (Word 𝐴 ∖ ∅)) → (𝑀 Σg 𝑤) ∈ 𝐵) |
81 | 2, 41, 11 | mulg0 19104 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑀 Σg
𝑤) ∈ 𝐵 → (0 · (𝑀 Σg 𝑤)) = (0g‘𝑅)) |
82 | 80, 81 | syl 17 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ 𝑓 ∈ 𝐹) ∧ (𝑓 supp 0) = ∅) ∧ 𝑤 ∈ (Word 𝐴 ∖ ∅)) → (0 · (𝑀 Σg
𝑤)) =
(0g‘𝑅)) |
83 | 70, 82 | eqtrd 2774 |
. . . . . . . . . . . . . . . . . . 19
⊢
(((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ 𝑓 ∈ 𝐹) ∧ (𝑓 supp 0) = ∅) ∧ 𝑤 ∈ (Word 𝐴 ∖ ∅)) → ((𝑓‘𝑤) · (𝑀 Σg 𝑤)) = (0g‘𝑅)) |
84 | | 0fi 9080 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ∅
∈ Fin |
85 | 84 | a1i 11 |
. . . . . . . . . . . . . . . . . . 19
⊢
((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ 𝑓 ∈ 𝐹) ∧ (𝑓 supp 0) = ∅) → ∅ ∈
Fin) |
86 | 1 | ringgrpd 20259 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝜑 → 𝑅 ∈ Grp) |
87 | 86 | ad6antr 736 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ 𝑓 ∈ 𝐹) ∧ (𝑓 supp 0) = ∅) ∧ 𝑤 ∈ Word 𝐴) → 𝑅 ∈ Grp) |
88 | 58 | ad2antrr 726 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
(((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ 𝑓 ∈ 𝐹) ∧ (𝑓 supp 0) = ∅) ∧ 𝑤 ∈ Word 𝐴) → 𝑓:Word 𝐴⟶ℤ) |
89 | | simpr 484 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
(((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ 𝑓 ∈ 𝐹) ∧ (𝑓 supp 0) = ∅) ∧ 𝑤 ∈ Word 𝐴) → 𝑤 ∈ Word 𝐴) |
90 | 88, 89 | ffvelcdmd 7104 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ 𝑓 ∈ 𝐹) ∧ (𝑓 supp 0) = ∅) ∧ 𝑤 ∈ Word 𝐴) → (𝑓‘𝑤) ∈ ℤ) |
91 | 72 | ad6antr 736 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
(((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ 𝑓 ∈ 𝐹) ∧ (𝑓 supp 0) = ∅) ∧ 𝑤 ∈ Word 𝐴) → 𝑀 ∈ Mnd) |
92 | 75 | ad6antr 736 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
(((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ 𝑓 ∈ 𝐹) ∧ (𝑓 supp 0) = ∅) ∧ 𝑤 ∈ Word 𝐴) → Word 𝐴 ⊆ Word 𝐵) |
93 | 92, 89 | sseldd 3995 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
(((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ 𝑓 ∈ 𝐹) ∧ (𝑓 supp 0) = ∅) ∧ 𝑤 ∈ Word 𝐴) → 𝑤 ∈ Word 𝐵) |
94 | 91, 93, 79 | syl2anc 584 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ 𝑓 ∈ 𝐹) ∧ (𝑓 supp 0) = ∅) ∧ 𝑤 ∈ Word 𝐴) → (𝑀 Σg 𝑤) ∈ 𝐵) |
95 | 2, 11, 87, 90, 94 | mulgcld 19126 |
. . . . . . . . . . . . . . . . . . 19
⊢
(((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ 𝑓 ∈ 𝐹) ∧ (𝑓 supp 0) = ∅) ∧ 𝑤 ∈ Word 𝐴) → ((𝑓‘𝑤) · (𝑀 Σg 𝑤)) ∈ 𝐵) |
96 | | 0ss 4405 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ∅
⊆ Word 𝐴 |
97 | 96 | a1i 11 |
. . . . . . . . . . . . . . . . . . 19
⊢
((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ 𝑓 ∈ 𝐹) ∧ (𝑓 supp 0) = ∅) → ∅ ⊆
Word 𝐴) |
98 | 2, 41, 43, 49, 83, 85, 95, 97 | gsummptres2 33038 |
. . . . . . . . . . . . . . . . . 18
⊢
((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ 𝑓 ∈ 𝐹) ∧ (𝑓 supp 0) = ∅) → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑓‘𝑤) · (𝑀 Σg 𝑤)))) = (𝑅 Σg (𝑤 ∈ ∅ ↦ ((𝑓‘𝑤) · (𝑀 Σg 𝑤))))) |
99 | | mpt0 6710 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑤 ∈ ∅ ↦ ((𝑓‘𝑤) · (𝑀 Σg 𝑤))) = ∅ |
100 | 99 | a1i 11 |
. . . . . . . . . . . . . . . . . . 19
⊢
((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ 𝑓 ∈ 𝐹) ∧ (𝑓 supp 0) = ∅) → (𝑤 ∈ ∅ ↦ ((𝑓‘𝑤) · (𝑀 Σg 𝑤))) = ∅) |
101 | 100 | oveq2d 7446 |
. . . . . . . . . . . . . . . . . 18
⊢
((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ 𝑓 ∈ 𝐹) ∧ (𝑓 supp 0) = ∅) → (𝑅 Σg (𝑤 ∈ ∅ ↦ ((𝑓‘𝑤) · (𝑀 Σg 𝑤)))) = (𝑅 Σg
∅)) |
102 | 41 | gsum0 18709 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑅 Σg
∅) = (0g‘𝑅) |
103 | 102 | a1i 11 |
. . . . . . . . . . . . . . . . . 18
⊢
((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ 𝑓 ∈ 𝐹) ∧ (𝑓 supp 0) = ∅) → (𝑅 Σg ∅) =
(0g‘𝑅)) |
104 | 98, 101, 103 | 3eqtrd 2778 |
. . . . . . . . . . . . . . . . 17
⊢
((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ 𝑓 ∈ 𝐹) ∧ (𝑓 supp 0) = ∅) → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑓‘𝑤) · (𝑀 Σg 𝑤)))) =
(0g‘𝑅)) |
105 | | subrgsubg 20593 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑡 ∈ (SubRing‘𝑅) → 𝑡 ∈ (SubGrp‘𝑅)) |
106 | 41 | subg0cl 19164 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑡 ∈ (SubGrp‘𝑅) →
(0g‘𝑅)
∈ 𝑡) |
107 | 105, 106 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑡 ∈ (SubRing‘𝑅) →
(0g‘𝑅)
∈ 𝑡) |
108 | 107 | adantl 481 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) → (0g‘𝑅) ∈ 𝑡) |
109 | 108 | ad4antr 732 |
. . . . . . . . . . . . . . . . 17
⊢
((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ 𝑓 ∈ 𝐹) ∧ (𝑓 supp 0) = ∅) →
(0g‘𝑅)
∈ 𝑡) |
110 | 104, 109 | eqeltrd 2838 |
. . . . . . . . . . . . . . . 16
⊢
((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ 𝑓 ∈ 𝐹) ∧ (𝑓 supp 0) = ∅) → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑓‘𝑤) · (𝑀 Σg 𝑤)))) ∈ 𝑡) |
111 | 110 | ex 412 |
. . . . . . . . . . . . . . 15
⊢
(((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ 𝑓 ∈ 𝐹) → ((𝑓 supp 0) = ∅ → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑓‘𝑤) · (𝑀 Σg 𝑤)))) ∈ 𝑡)) |
112 | 111 | ralrimiva 3143 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) → ∀𝑓 ∈ 𝐹 ((𝑓 supp 0) = ∅ → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑓‘𝑤) · (𝑀 Σg 𝑤)))) ∈ 𝑡)) |
113 | 42 | ad7antr 738 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) → 𝑅 ∈ CMnd) |
114 | 48 | ad7antr 738 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) → Word 𝐴 ∈ V) |
115 | | simp-5l 785 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢
((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ 𝑒 ∈ 𝐹) → 𝜑) |
116 | | breq1 5150 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ (𝑓 = 𝑒 → (𝑓 finSupp 0 ↔ 𝑒 finSupp 0)) |
117 | 116, 12 | elrab2 3697 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ (𝑒 ∈ 𝐹 ↔ (𝑒 ∈ (ℤ ↑m Word
𝐴) ∧ 𝑒 finSupp 0)) |
118 | 117 | simplbi 497 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ (𝑒 ∈ 𝐹 → 𝑒 ∈ (ℤ ↑m Word
𝐴)) |
119 | 55, 48 | elmapd 8878 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ (𝜑 → (𝑒 ∈ (ℤ ↑m Word
𝐴) ↔ 𝑒:Word 𝐴⟶ℤ)) |
120 | 119 | biimpa 476 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ ((𝜑 ∧ 𝑒 ∈ (ℤ ↑m Word
𝐴)) → 𝑒:Word 𝐴⟶ℤ) |
121 | 118, 120 | sylan2 593 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ ((𝜑 ∧ 𝑒 ∈ 𝐹) → 𝑒:Word 𝐴⟶ℤ) |
122 | 115, 121 | sylancom 588 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢
((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ 𝑒 ∈ 𝐹) → 𝑒:Word 𝐴⟶ℤ) |
123 | 122 | adantl3r 750 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢
(((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ 𝑒 ∈ 𝐹) → 𝑒:Word 𝐴⟶ℤ) |
124 | 123 | ffnd 6737 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢
(((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ 𝑒 ∈ 𝐹) → 𝑒 Fn Word 𝐴) |
125 | 124 | ad2antrr 726 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢
(((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) ∧ 𝑤 ∈ (Word 𝐴 ∖ (𝑒 supp 0))) → 𝑒 Fn Word 𝐴) |
126 | 114 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢
(((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) ∧ 𝑤 ∈ (Word 𝐴 ∖ (𝑒 supp 0))) → Word 𝐴 ∈ V) |
127 | | 0zd 12622 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢
(((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) ∧ 𝑤 ∈ (Word 𝐴 ∖ (𝑒 supp 0))) → 0 ∈
ℤ) |
128 | | simpr 484 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢
(((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) ∧ 𝑤 ∈ (Word 𝐴 ∖ (𝑒 supp 0))) → 𝑤 ∈ (Word 𝐴 ∖ (𝑒 supp 0))) |
129 | 125, 126,
127, 128 | fvdifsupp 8194 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢
(((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) ∧ 𝑤 ∈ (Word 𝐴 ∖ (𝑒 supp 0))) → (𝑒‘𝑤) = 0) |
130 | 129 | oveq1d 7445 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
(((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) ∧ 𝑤 ∈ (Word 𝐴 ∖ (𝑒 supp 0))) → ((𝑒‘𝑤) · (𝑀 Σg 𝑤)) = (0 · (𝑀 Σg 𝑤))) |
131 | 72 | ad8antr 740 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢
(((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) ∧ 𝑤 ∈ (Word 𝐴 ∖ (𝑒 supp 0))) → 𝑀 ∈ Mnd) |
132 | 75 | ad8antr 740 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢
(((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) ∧ 𝑤 ∈ (Word 𝐴 ∖ (𝑒 supp 0))) → Word 𝐴 ⊆ Word 𝐵) |
133 | 128 | eldifad 3974 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢
(((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) ∧ 𝑤 ∈ (Word 𝐴 ∖ (𝑒 supp 0))) → 𝑤 ∈ Word 𝐴) |
134 | 132, 133 | sseldd 3995 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢
(((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) ∧ 𝑤 ∈ (Word 𝐴 ∖ (𝑒 supp 0))) → 𝑤 ∈ Word 𝐵) |
135 | 131, 134,
79 | syl2anc 584 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢
(((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) ∧ 𝑤 ∈ (Word 𝐴 ∖ (𝑒 supp 0))) → (𝑀 Σg 𝑤) ∈ 𝐵) |
136 | 135, 81 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
(((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) ∧ 𝑤 ∈ (Word 𝐴 ∖ (𝑒 supp 0))) → (0 · (𝑀 Σg 𝑤)) = (0g‘𝑅)) |
137 | 130, 136 | eqtrd 2774 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
(((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) ∧ 𝑤 ∈ (Word 𝐴 ∖ (𝑒 supp 0))) → ((𝑒‘𝑤) · (𝑀 Σg 𝑤)) = (0g‘𝑅)) |
138 | 117 | simprbi 496 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑒 ∈ 𝐹 → 𝑒 finSupp 0) |
139 | 138 | ad2antlr 727 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) → 𝑒 finSupp 0) |
140 | 139 | fsuppimpd 9406 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) → (𝑒 supp 0) ∈ Fin) |
141 | 86 | ad8antr 740 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
(((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) ∧ 𝑤 ∈ Word 𝐴) → 𝑅 ∈ Grp) |
142 | 123 | ad2antrr 726 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢
(((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) ∧ 𝑤 ∈ Word 𝐴) → 𝑒:Word 𝐴⟶ℤ) |
143 | | simpr 484 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢
(((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) ∧ 𝑤 ∈ Word 𝐴) → 𝑤 ∈ Word 𝐴) |
144 | 142, 143 | ffvelcdmd 7104 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
(((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) ∧ 𝑤 ∈ Word 𝐴) → (𝑒‘𝑤) ∈ ℤ) |
145 | 72 | ad8antr 740 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢
(((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) ∧ 𝑤 ∈ Word 𝐴) → 𝑀 ∈ Mnd) |
146 | 75 | ad7antr 738 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢
((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) → Word 𝐴 ⊆ Word 𝐵) |
147 | 146 | sselda 3994 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢
(((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) ∧ 𝑤 ∈ Word 𝐴) → 𝑤 ∈ Word 𝐵) |
148 | 145, 147,
79 | syl2anc 584 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
(((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) ∧ 𝑤 ∈ Word 𝐴) → (𝑀 Σg 𝑤) ∈ 𝐵) |
149 | 2, 11, 141, 144, 148 | mulgcld 19126 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
(((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) ∧ 𝑤 ∈ Word 𝐴) → ((𝑒‘𝑤) · (𝑀 Σg 𝑤)) ∈ 𝐵) |
150 | | suppssdm 8200 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑒 supp 0) ⊆ dom 𝑒 |
151 | 123 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) → 𝑒:Word 𝐴⟶ℤ) |
152 | 150, 151 | fssdm 6755 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) → (𝑒 supp 0) ⊆ Word 𝐴) |
153 | 2, 41, 113, 114, 137, 140, 149, 152 | gsummptres2 33038 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑒‘𝑤) · (𝑀 Σg 𝑤)))) = (𝑅 Σg (𝑤 ∈ (𝑒 supp 0) ↦ ((𝑒‘𝑤) · (𝑀 Σg 𝑤))))) |
154 | 153 | adantllr 719 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
(((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ ∀𝑓 ∈ 𝐹 ((𝑓 supp 0) = ℎ → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑓‘𝑤) · (𝑀 Σg 𝑤)))) ∈ 𝑡)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑒‘𝑤) · (𝑀 Σg 𝑤)))) = (𝑅 Σg (𝑤 ∈ (𝑒 supp 0) ↦ ((𝑒‘𝑤) · (𝑀 Σg 𝑤))))) |
155 | | simpr 484 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
(((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ ∀𝑓 ∈ 𝐹 ((𝑓 supp 0) = ℎ → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑓‘𝑤) · (𝑀 Σg 𝑤)))) ∈ 𝑡)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) → (𝑒 supp 0) = (ℎ ∪ {𝑥})) |
156 | 155 | mpteq1d 5242 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
(((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ ∀𝑓 ∈ 𝐹 ((𝑓 supp 0) = ℎ → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑓‘𝑤) · (𝑀 Σg 𝑤)))) ∈ 𝑡)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) → (𝑤 ∈ (𝑒 supp 0) ↦ ((𝑒‘𝑤) · (𝑀 Σg 𝑤))) = (𝑤 ∈ (ℎ ∪ {𝑥}) ↦ ((𝑒‘𝑤) · (𝑀 Σg 𝑤)))) |
157 | 156 | oveq2d 7446 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
(((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ ∀𝑓 ∈ 𝐹 ((𝑓 supp 0) = ℎ → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑓‘𝑤) · (𝑀 Σg 𝑤)))) ∈ 𝑡)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) → (𝑅 Σg (𝑤 ∈ (𝑒 supp 0) ↦ ((𝑒‘𝑤) · (𝑀 Σg 𝑤)))) = (𝑅 Σg (𝑤 ∈ (ℎ ∪ {𝑥}) ↦ ((𝑒‘𝑤) · (𝑀 Σg 𝑤))))) |
158 | | eqid 2734 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
(+g‘𝑅) = (+g‘𝑅) |
159 | | breq1 5150 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (𝑓 = 𝑔 → (𝑓 finSupp 0 ↔ 𝑔 finSupp 0)) |
160 | 159, 12 | elrab2 3697 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (𝑔 ∈ 𝐹 ↔ (𝑔 ∈ (ℤ ↑m Word
𝐴) ∧ 𝑔 finSupp 0)) |
161 | 160 | simprbi 496 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝑔 ∈ 𝐹 → 𝑔 finSupp 0) |
162 | 161 | adantl 481 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) → 𝑔 finSupp 0) |
163 | 162 | fsuppimpd 9406 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) → (𝑔 supp 0) ∈ Fin) |
164 | 163 | ad4antr 732 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) → (𝑔 supp 0) ∈ Fin) |
165 | | simp-4r 784 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) → ℎ ⊆ (𝑔 supp 0)) |
166 | 164, 165 | ssfid 9298 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) → ℎ ∈ Fin) |
167 | 86 | ad8antr 740 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
(((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) ∧ 𝑤 ∈ ℎ) → 𝑅 ∈ Grp) |
168 | 151 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢
(((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) ∧ 𝑤 ∈ ℎ) → 𝑒:Word 𝐴⟶ℤ) |
169 | | suppssdm 8200 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (𝑔 supp 0) ⊆ dom 𝑔 |
170 | | simp-7l 789 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢
((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) → 𝜑) |
171 | | simp-5r 786 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢
((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) → 𝑔 ∈ 𝐹) |
172 | 160 | simplbi 497 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ (𝑔 ∈ 𝐹 → 𝑔 ∈ (ℤ ↑m Word
𝐴)) |
173 | 55, 48 | elmapd 8878 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ (𝜑 → (𝑔 ∈ (ℤ ↑m Word
𝐴) ↔ 𝑔:Word 𝐴⟶ℤ)) |
174 | 173 | biimpa 476 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ ((𝜑 ∧ 𝑔 ∈ (ℤ ↑m Word
𝐴)) → 𝑔:Word 𝐴⟶ℤ) |
175 | 172, 174 | sylan2 593 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ ((𝜑 ∧ 𝑔 ∈ 𝐹) → 𝑔:Word 𝐴⟶ℤ) |
176 | 170, 171,
175 | syl2anc 584 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢
((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) → 𝑔:Word 𝐴⟶ℤ) |
177 | 169, 176 | fssdm 6755 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢
((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) → (𝑔 supp 0) ⊆ Word 𝐴) |
178 | 165, 177 | sstrd 4005 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢
((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) → ℎ ⊆ Word 𝐴) |
179 | 178 | sselda 3994 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢
(((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) ∧ 𝑤 ∈ ℎ) → 𝑤 ∈ Word 𝐴) |
180 | 168, 179 | ffvelcdmd 7104 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
(((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) ∧ 𝑤 ∈ ℎ) → (𝑒‘𝑤) ∈ ℤ) |
181 | 179, 148 | syldan 591 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
(((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) ∧ 𝑤 ∈ ℎ) → (𝑀 Σg 𝑤) ∈ 𝐵) |
182 | 2, 11, 167, 180, 181 | mulgcld 19126 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
(((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) ∧ 𝑤 ∈ ℎ) → ((𝑒‘𝑤) · (𝑀 Σg 𝑤)) ∈ 𝐵) |
183 | | simpllr 776 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) → 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) |
184 | 183 | eldifbd 3975 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) → ¬ 𝑥 ∈ ℎ) |
185 | 170, 86 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) → 𝑅 ∈ Grp) |
186 | 183 | eldifad 3974 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢
((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) → 𝑥 ∈ (𝑔 supp 0)) |
187 | 177, 186 | sseldd 3995 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢
((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) → 𝑥 ∈ Word 𝐴) |
188 | 151, 187 | ffvelcdmd 7104 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) → (𝑒‘𝑥) ∈ ℤ) |
189 | 170, 72 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢
((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) → 𝑀 ∈ Mnd) |
190 | 146, 187 | sseldd 3995 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢
((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) → 𝑥 ∈ Word 𝐵) |
191 | 78 | gsumwcl 18864 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝑀 ∈ Mnd ∧ 𝑥 ∈ Word 𝐵) → (𝑀 Σg 𝑥) ∈ 𝐵) |
192 | 189, 190,
191 | syl2anc 584 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) → (𝑀 Σg 𝑥) ∈ 𝐵) |
193 | 2, 11, 185, 188, 192 | mulgcld 19126 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) → ((𝑒‘𝑥) · (𝑀 Σg 𝑥)) ∈ 𝐵) |
194 | | fveq2 6906 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑤 = 𝑥 → (𝑒‘𝑤) = (𝑒‘𝑥)) |
195 | | oveq2 7438 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑤 = 𝑥 → (𝑀 Σg 𝑤) = (𝑀 Σg 𝑥)) |
196 | 194, 195 | oveq12d 7448 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑤 = 𝑥 → ((𝑒‘𝑤) · (𝑀 Σg 𝑤)) = ((𝑒‘𝑥) · (𝑀 Σg 𝑥))) |
197 | 2, 158, 113, 166, 182, 183, 184, 193, 196 | gsumunsn 19992 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) → (𝑅 Σg (𝑤 ∈ (ℎ ∪ {𝑥}) ↦ ((𝑒‘𝑤) · (𝑀 Σg 𝑤)))) = ((𝑅 Σg (𝑤 ∈ ℎ ↦ ((𝑒‘𝑤) · (𝑀 Σg 𝑤))))(+g‘𝑅)((𝑒‘𝑥) · (𝑀 Σg 𝑥)))) |
198 | 197 | adantllr 719 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
(((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ ∀𝑓 ∈ 𝐹 ((𝑓 supp 0) = ℎ → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑓‘𝑤) · (𝑀 Σg 𝑤)))) ∈ 𝑡)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) → (𝑅 Σg (𝑤 ∈ (ℎ ∪ {𝑥}) ↦ ((𝑒‘𝑤) · (𝑀 Σg 𝑤)))) = ((𝑅 Σg (𝑤 ∈ ℎ ↦ ((𝑒‘𝑤) · (𝑀 Σg 𝑤))))(+g‘𝑅)((𝑒‘𝑥) · (𝑀 Σg 𝑥)))) |
199 | 154, 157,
198 | 3eqtrd 2778 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ ∀𝑓 ∈ 𝐹 ((𝑓 supp 0) = ℎ → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑓‘𝑤) · (𝑀 Σg 𝑤)))) ∈ 𝑡)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑒‘𝑤) · (𝑀 Σg 𝑤)))) = ((𝑅 Σg (𝑤 ∈ ℎ ↦ ((𝑒‘𝑤) · (𝑀 Σg 𝑤))))(+g‘𝑅)((𝑒‘𝑥) · (𝑀 Σg 𝑥)))) |
200 | 105 | ad8antlr 741 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
(((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ ∀𝑓 ∈ 𝐹 ((𝑓 supp 0) = ℎ → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑓‘𝑤) · (𝑀 Σg 𝑤)))) ∈ 𝑡)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) → 𝑡 ∈ (SubGrp‘𝑅)) |
201 | 124 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢
((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) → 𝑒 Fn Word 𝐴) |
202 | | 0zd 12622 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢
((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) → 0 ∈ ℤ) |
203 | 201, 187,
202 | fmptunsnop 32714 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢
((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) → (𝑦 ∈ Word 𝐴 ↦ if(𝑦 = 𝑥, 0, (𝑒‘𝑦))) = ((𝑒 ↾ (Word 𝐴 ∖ {𝑥})) ∪ {〈𝑥, 0〉})) |
204 | 203 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢
(((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) ∧ 𝑤 ∈ (Word 𝐴 ∖ ℎ)) → (𝑦 ∈ Word 𝐴 ↦ if(𝑦 = 𝑥, 0, (𝑒‘𝑦))) = ((𝑒 ↾ (Word 𝐴 ∖ {𝑥})) ∪ {〈𝑥, 0〉})) |
205 | 204 | fveq1d 6908 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢
(((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) ∧ 𝑤 ∈ (Word 𝐴 ∖ ℎ)) → ((𝑦 ∈ Word 𝐴 ↦ if(𝑦 = 𝑥, 0, (𝑒‘𝑦)))‘𝑤) = (((𝑒 ↾ (Word 𝐴 ∖ {𝑥})) ∪ {〈𝑥, 0〉})‘𝑤)) |
206 | | eqid 2734 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (𝑦 ∈ Word 𝐴 ↦ if(𝑦 = 𝑥, 0, (𝑒‘𝑦))) = (𝑦 ∈ Word 𝐴 ↦ if(𝑦 = 𝑥, 0, (𝑒‘𝑦))) |
207 | | eqidd 2735 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢
(((((((((((𝜑 ∧
𝑡 ∈
(SubRing‘𝑅)) ∧
𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) ∧ 𝑤 ∈ (Word 𝐴 ∖ ℎ)) ∧ 𝑦 = 𝑤) ∧ 𝑦 = 𝑥) → 0 = 0) |
208 | 201 | ad3antrrr 730 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢
(((((((((((𝜑 ∧
𝑡 ∈
(SubRing‘𝑅)) ∧
𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) ∧ 𝑤 ∈ (Word 𝐴 ∖ ℎ)) ∧ 𝑦 = 𝑤) ∧ ¬ 𝑦 = 𝑥) → 𝑒 Fn Word 𝐴) |
209 | 114 | ad3antrrr 730 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢
(((((((((((𝜑 ∧
𝑡 ∈
(SubRing‘𝑅)) ∧
𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) ∧ 𝑤 ∈ (Word 𝐴 ∖ ℎ)) ∧ 𝑦 = 𝑤) ∧ ¬ 𝑦 = 𝑥) → Word 𝐴 ∈ V) |
210 | | 0zd 12622 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢
(((((((((((𝜑 ∧
𝑡 ∈
(SubRing‘𝑅)) ∧
𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) ∧ 𝑤 ∈ (Word 𝐴 ∖ ℎ)) ∧ 𝑦 = 𝑤) ∧ ¬ 𝑦 = 𝑥) → 0 ∈ ℤ) |
211 | | simplr 769 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢
(((((((((((𝜑 ∧
𝑡 ∈
(SubRing‘𝑅)) ∧
𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) ∧ 𝑤 ∈ (Word 𝐴 ∖ ℎ)) ∧ 𝑦 = 𝑤) ∧ ¬ 𝑦 = 𝑥) → 𝑦 = 𝑤) |
212 | | simpllr 776 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢
(((((((((((𝜑 ∧
𝑡 ∈
(SubRing‘𝑅)) ∧
𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) ∧ 𝑤 ∈ (Word 𝐴 ∖ ℎ)) ∧ 𝑦 = 𝑤) ∧ ¬ 𝑦 = 𝑥) → 𝑤 ∈ (Word 𝐴 ∖ ℎ)) |
213 | 212 | eldifad 3974 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢
(((((((((((𝜑 ∧
𝑡 ∈
(SubRing‘𝑅)) ∧
𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) ∧ 𝑤 ∈ (Word 𝐴 ∖ ℎ)) ∧ 𝑦 = 𝑤) ∧ ¬ 𝑦 = 𝑥) → 𝑤 ∈ Word 𝐴) |
214 | 211, 213 | eqeltrd 2838 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢
(((((((((((𝜑 ∧
𝑡 ∈
(SubRing‘𝑅)) ∧
𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) ∧ 𝑤 ∈ (Word 𝐴 ∖ ℎ)) ∧ 𝑦 = 𝑤) ∧ ¬ 𝑦 = 𝑥) → 𝑦 ∈ Word 𝐴) |
215 | | simp-4r 784 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢
(((((((((((𝜑 ∧
𝑡 ∈
(SubRing‘𝑅)) ∧
𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) ∧ 𝑤 ∈ (Word 𝐴 ∖ ℎ)) ∧ 𝑦 = 𝑤) ∧ ¬ 𝑦 = 𝑥) → (𝑒 supp 0) = (ℎ ∪ {𝑥})) |
216 | 212 | eldifbd 3975 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢
(((((((((((𝜑 ∧
𝑡 ∈
(SubRing‘𝑅)) ∧
𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) ∧ 𝑤 ∈ (Word 𝐴 ∖ ℎ)) ∧ 𝑦 = 𝑤) ∧ ¬ 𝑦 = 𝑥) → ¬ 𝑤 ∈ ℎ) |
217 | 211, 216 | eqneltrd 2858 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢
(((((((((((𝜑 ∧
𝑡 ∈
(SubRing‘𝑅)) ∧
𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) ∧ 𝑤 ∈ (Word 𝐴 ∖ ℎ)) ∧ 𝑦 = 𝑤) ∧ ¬ 𝑦 = 𝑥) → ¬ 𝑦 ∈ ℎ) |
218 | | simpr 484 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
⊢
(((((((((((𝜑 ∧
𝑡 ∈
(SubRing‘𝑅)) ∧
𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) ∧ 𝑤 ∈ (Word 𝐴 ∖ ℎ)) ∧ 𝑦 = 𝑤) ∧ ¬ 𝑦 = 𝑥) → ¬ 𝑦 = 𝑥) |
219 | 218 | neqned 2944 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢
(((((((((((𝜑 ∧
𝑡 ∈
(SubRing‘𝑅)) ∧
𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) ∧ 𝑤 ∈ (Word 𝐴 ∖ ℎ)) ∧ 𝑦 = 𝑤) ∧ ¬ 𝑦 = 𝑥) → 𝑦 ≠ 𝑥) |
220 | | nelsn 4670 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢ (𝑦 ≠ 𝑥 → ¬ 𝑦 ∈ {𝑥}) |
221 | 219, 220 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢
(((((((((((𝜑 ∧
𝑡 ∈
(SubRing‘𝑅)) ∧
𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) ∧ 𝑤 ∈ (Word 𝐴 ∖ ℎ)) ∧ 𝑦 = 𝑤) ∧ ¬ 𝑦 = 𝑥) → ¬ 𝑦 ∈ {𝑥}) |
222 | | nelun 32540 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢ ((𝑒 supp 0) = (ℎ ∪ {𝑥}) → (¬ 𝑦 ∈ (𝑒 supp 0) ↔ (¬ 𝑦 ∈ ℎ ∧ ¬ 𝑦 ∈ {𝑥}))) |
223 | 222 | biimpar 477 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ (((𝑒 supp 0) = (ℎ ∪ {𝑥}) ∧ (¬ 𝑦 ∈ ℎ ∧ ¬ 𝑦 ∈ {𝑥})) → ¬ 𝑦 ∈ (𝑒 supp 0)) |
224 | 215, 217,
221, 223 | syl12anc 837 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢
(((((((((((𝜑 ∧
𝑡 ∈
(SubRing‘𝑅)) ∧
𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) ∧ 𝑤 ∈ (Word 𝐴 ∖ ℎ)) ∧ 𝑦 = 𝑤) ∧ ¬ 𝑦 = 𝑥) → ¬ 𝑦 ∈ (𝑒 supp 0)) |
225 | 214, 224 | eldifd 3973 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢
(((((((((((𝜑 ∧
𝑡 ∈
(SubRing‘𝑅)) ∧
𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) ∧ 𝑤 ∈ (Word 𝐴 ∖ ℎ)) ∧ 𝑦 = 𝑤) ∧ ¬ 𝑦 = 𝑥) → 𝑦 ∈ (Word 𝐴 ∖ (𝑒 supp 0))) |
226 | 208, 209,
210, 225 | fvdifsupp 8194 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢
(((((((((((𝜑 ∧
𝑡 ∈
(SubRing‘𝑅)) ∧
𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) ∧ 𝑤 ∈ (Word 𝐴 ∖ ℎ)) ∧ 𝑦 = 𝑤) ∧ ¬ 𝑦 = 𝑥) → (𝑒‘𝑦) = 0) |
227 | 207, 226 | ifeqda 4566 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢
((((((((((𝜑 ∧
𝑡 ∈
(SubRing‘𝑅)) ∧
𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) ∧ 𝑤 ∈ (Word 𝐴 ∖ ℎ)) ∧ 𝑦 = 𝑤) → if(𝑦 = 𝑥, 0, (𝑒‘𝑦)) = 0) |
228 | | simpr 484 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢
(((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) ∧ 𝑤 ∈ (Word 𝐴 ∖ ℎ)) → 𝑤 ∈ (Word 𝐴 ∖ ℎ)) |
229 | 228 | eldifad 3974 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢
(((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) ∧ 𝑤 ∈ (Word 𝐴 ∖ ℎ)) → 𝑤 ∈ Word 𝐴) |
230 | | 0zd 12622 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢
(((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) ∧ 𝑤 ∈ (Word 𝐴 ∖ ℎ)) → 0 ∈ ℤ) |
231 | 206, 227,
229, 230 | fvmptd2 7023 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢
(((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) ∧ 𝑤 ∈ (Word 𝐴 ∖ ℎ)) → ((𝑦 ∈ Word 𝐴 ↦ if(𝑦 = 𝑥, 0, (𝑒‘𝑦)))‘𝑤) = 0) |
232 | 205, 231 | eqtr3d 2776 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢
(((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) ∧ 𝑤 ∈ (Word 𝐴 ∖ ℎ)) → (((𝑒 ↾ (Word 𝐴 ∖ {𝑥})) ∪ {〈𝑥, 0〉})‘𝑤) = 0) |
233 | 232 | oveq1d 7445 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢
(((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) ∧ 𝑤 ∈ (Word 𝐴 ∖ ℎ)) → ((((𝑒 ↾ (Word 𝐴 ∖ {𝑥})) ∪ {〈𝑥, 0〉})‘𝑤) · (𝑀 Σg 𝑤)) = (0 · (𝑀 Σg 𝑤))) |
234 | 229, 148 | syldan 591 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢
(((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) ∧ 𝑤 ∈ (Word 𝐴 ∖ ℎ)) → (𝑀 Σg 𝑤) ∈ 𝐵) |
235 | 234, 81 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢
(((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) ∧ 𝑤 ∈ (Word 𝐴 ∖ ℎ)) → (0 · (𝑀 Σg 𝑤)) = (0g‘𝑅)) |
236 | 233, 235 | eqtrd 2774 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢
(((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) ∧ 𝑤 ∈ (Word 𝐴 ∖ ℎ)) → ((((𝑒 ↾ (Word 𝐴 ∖ {𝑥})) ∪ {〈𝑥, 0〉})‘𝑤) · (𝑀 Σg 𝑤)) = (0g‘𝑅)) |
237 | 203 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢
(((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) ∧ 𝑤 ∈ Word 𝐴) → (𝑦 ∈ Word 𝐴 ↦ if(𝑦 = 𝑥, 0, (𝑒‘𝑦))) = ((𝑒 ↾ (Word 𝐴 ∖ {𝑥})) ∪ {〈𝑥, 0〉})) |
238 | 237 | fveq1d 6908 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢
(((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) ∧ 𝑤 ∈ Word 𝐴) → ((𝑦 ∈ Word 𝐴 ↦ if(𝑦 = 𝑥, 0, (𝑒‘𝑦)))‘𝑤) = (((𝑒 ↾ (Word 𝐴 ∖ {𝑥})) ∪ {〈𝑥, 0〉})‘𝑤)) |
239 | | 0zd 12622 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢
((((((((((𝜑 ∧
𝑡 ∈
(SubRing‘𝑅)) ∧
𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) ∧ 𝑦 ∈ Word 𝐴) ∧ 𝑦 = 𝑥) → 0 ∈ ℤ) |
240 | 151 | ad2antrr 726 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢
((((((((((𝜑 ∧
𝑡 ∈
(SubRing‘𝑅)) ∧
𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) ∧ 𝑦 ∈ Word 𝐴) ∧ ¬ 𝑦 = 𝑥) → 𝑒:Word 𝐴⟶ℤ) |
241 | | simplr 769 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢
((((((((((𝜑 ∧
𝑡 ∈
(SubRing‘𝑅)) ∧
𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) ∧ 𝑦 ∈ Word 𝐴) ∧ ¬ 𝑦 = 𝑥) → 𝑦 ∈ Word 𝐴) |
242 | 240, 241 | ffvelcdmd 7104 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢
((((((((((𝜑 ∧
𝑡 ∈
(SubRing‘𝑅)) ∧
𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) ∧ 𝑦 ∈ Word 𝐴) ∧ ¬ 𝑦 = 𝑥) → (𝑒‘𝑦) ∈ ℤ) |
243 | 239, 242 | ifclda 4565 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢
(((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) ∧ 𝑦 ∈ Word 𝐴) → if(𝑦 = 𝑥, 0, (𝑒‘𝑦)) ∈ ℤ) |
244 | 243 | fmpttd 7134 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢
((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) → (𝑦 ∈ Word 𝐴 ↦ if(𝑦 = 𝑥, 0, (𝑒‘𝑦))):Word 𝐴⟶ℤ) |
245 | 244 | ffvelcdmda 7103 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢
(((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) ∧ 𝑤 ∈ Word 𝐴) → ((𝑦 ∈ Word 𝐴 ↦ if(𝑦 = 𝑥, 0, (𝑒‘𝑦)))‘𝑤) ∈ ℤ) |
246 | 238, 245 | eqeltrrd 2839 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢
(((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) ∧ 𝑤 ∈ Word 𝐴) → (((𝑒 ↾ (Word 𝐴 ∖ {𝑥})) ∪ {〈𝑥, 0〉})‘𝑤) ∈ ℤ) |
247 | 2, 11, 141, 246, 148 | mulgcld 19126 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢
(((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) ∧ 𝑤 ∈ Word 𝐴) → ((((𝑒 ↾ (Word 𝐴 ∖ {𝑥})) ∪ {〈𝑥, 0〉})‘𝑤) · (𝑀 Σg 𝑤)) ∈ 𝐵) |
248 | 2, 41, 113, 114, 236, 166, 247, 178 | gsummptres2 33038 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((((𝑒 ↾ (Word 𝐴 ∖ {𝑥})) ∪ {〈𝑥, 0〉})‘𝑤) · (𝑀 Σg 𝑤)))) = (𝑅 Σg (𝑤 ∈ ℎ ↦ ((((𝑒 ↾ (Word 𝐴 ∖ {𝑥})) ∪ {〈𝑥, 0〉})‘𝑤) · (𝑀 Σg 𝑤))))) |
249 | 248 | adantllr 719 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
(((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ ∀𝑓 ∈ 𝐹 ((𝑓 supp 0) = ℎ → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑓‘𝑤) · (𝑀 Σg 𝑤)))) ∈ 𝑡)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((((𝑒 ↾ (Word 𝐴 ∖ {𝑥})) ∪ {〈𝑥, 0〉})‘𝑤) · (𝑀 Σg 𝑤)))) = (𝑅 Σg (𝑤 ∈ ℎ ↦ ((((𝑒 ↾ (Word 𝐴 ∖ {𝑥})) ∪ {〈𝑥, 0〉})‘𝑤) · (𝑀 Σg 𝑤))))) |
250 | 203 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢
(((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) ∧ 𝑤 ∈ ℎ) → (𝑦 ∈ Word 𝐴 ↦ if(𝑦 = 𝑥, 0, (𝑒‘𝑦))) = ((𝑒 ↾ (Word 𝐴 ∖ {𝑥})) ∪ {〈𝑥, 0〉})) |
251 | 250 | fveq1d 6908 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢
(((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) ∧ 𝑤 ∈ ℎ) → ((𝑦 ∈ Word 𝐴 ↦ if(𝑦 = 𝑥, 0, (𝑒‘𝑦)))‘𝑤) = (((𝑒 ↾ (Word 𝐴 ∖ {𝑥})) ∪ {〈𝑥, 0〉})‘𝑤)) |
252 | | simpr 484 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢
((((((((((𝜑 ∧
𝑡 ∈
(SubRing‘𝑅)) ∧
𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) ∧ 𝑤 ∈ ℎ) ∧ 𝑦 = 𝑤) → 𝑦 = 𝑤) |
253 | | simplr 769 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢
((((((((((𝜑 ∧
𝑡 ∈
(SubRing‘𝑅)) ∧
𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) ∧ 𝑤 ∈ ℎ) ∧ 𝑦 = 𝑤) → 𝑤 ∈ ℎ) |
254 | 252, 253 | eqeltrd 2838 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢
((((((((((𝜑 ∧
𝑡 ∈
(SubRing‘𝑅)) ∧
𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) ∧ 𝑤 ∈ ℎ) ∧ 𝑦 = 𝑤) → 𝑦 ∈ ℎ) |
255 | 184 | ad2antrr 726 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢
((((((((((𝜑 ∧
𝑡 ∈
(SubRing‘𝑅)) ∧
𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) ∧ 𝑤 ∈ ℎ) ∧ 𝑦 = 𝑤) → ¬ 𝑥 ∈ ℎ) |
256 | | nelneq 2862 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ ((𝑦 ∈ ℎ ∧ ¬ 𝑥 ∈ ℎ) → ¬ 𝑦 = 𝑥) |
257 | 254, 255,
256 | syl2anc 584 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢
((((((((((𝜑 ∧
𝑡 ∈
(SubRing‘𝑅)) ∧
𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) ∧ 𝑤 ∈ ℎ) ∧ 𝑦 = 𝑤) → ¬ 𝑦 = 𝑥) |
258 | 257 | iffalsed 4541 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢
((((((((((𝜑 ∧
𝑡 ∈
(SubRing‘𝑅)) ∧
𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) ∧ 𝑤 ∈ ℎ) ∧ 𝑦 = 𝑤) → if(𝑦 = 𝑥, 0, (𝑒‘𝑦)) = (𝑒‘𝑦)) |
259 | 252 | fveq2d 6910 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢
((((((((((𝜑 ∧
𝑡 ∈
(SubRing‘𝑅)) ∧
𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) ∧ 𝑤 ∈ ℎ) ∧ 𝑦 = 𝑤) → (𝑒‘𝑦) = (𝑒‘𝑤)) |
260 | 258, 259 | eqtrd 2774 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢
((((((((((𝜑 ∧
𝑡 ∈
(SubRing‘𝑅)) ∧
𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) ∧ 𝑤 ∈ ℎ) ∧ 𝑦 = 𝑤) → if(𝑦 = 𝑥, 0, (𝑒‘𝑦)) = (𝑒‘𝑤)) |
261 | 206, 260,
179, 180 | fvmptd2 7023 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢
(((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) ∧ 𝑤 ∈ ℎ) → ((𝑦 ∈ Word 𝐴 ↦ if(𝑦 = 𝑥, 0, (𝑒‘𝑦)))‘𝑤) = (𝑒‘𝑤)) |
262 | 251, 261 | eqtr3d 2776 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢
(((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) ∧ 𝑤 ∈ ℎ) → (((𝑒 ↾ (Word 𝐴 ∖ {𝑥})) ∪ {〈𝑥, 0〉})‘𝑤) = (𝑒‘𝑤)) |
263 | 262 | oveq1d 7445 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢
(((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) ∧ 𝑤 ∈ ℎ) → ((((𝑒 ↾ (Word 𝐴 ∖ {𝑥})) ∪ {〈𝑥, 0〉})‘𝑤) · (𝑀 Σg 𝑤)) = ((𝑒‘𝑤) · (𝑀 Σg 𝑤))) |
264 | 263 | mpteq2dva 5247 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢
((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) → (𝑤 ∈ ℎ ↦ ((((𝑒 ↾ (Word 𝐴 ∖ {𝑥})) ∪ {〈𝑥, 0〉})‘𝑤) · (𝑀 Σg 𝑤))) = (𝑤 ∈ ℎ ↦ ((𝑒‘𝑤) · (𝑀 Σg 𝑤)))) |
265 | 264 | adantllr 719 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
(((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ ∀𝑓 ∈ 𝐹 ((𝑓 supp 0) = ℎ → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑓‘𝑤) · (𝑀 Σg 𝑤)))) ∈ 𝑡)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) → (𝑤 ∈ ℎ ↦ ((((𝑒 ↾ (Word 𝐴 ∖ {𝑥})) ∪ {〈𝑥, 0〉})‘𝑤) · (𝑀 Σg 𝑤))) = (𝑤 ∈ ℎ ↦ ((𝑒‘𝑤) · (𝑀 Σg 𝑤)))) |
266 | 265 | oveq2d 7446 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
(((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ ∀𝑓 ∈ 𝐹 ((𝑓 supp 0) = ℎ → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑓‘𝑤) · (𝑀 Σg 𝑤)))) ∈ 𝑡)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) → (𝑅 Σg (𝑤 ∈ ℎ ↦ ((((𝑒 ↾ (Word 𝐴 ∖ {𝑥})) ∪ {〈𝑥, 0〉})‘𝑤) · (𝑀 Σg 𝑤)))) = (𝑅 Σg (𝑤 ∈ ℎ ↦ ((𝑒‘𝑤) · (𝑀 Σg 𝑤))))) |
267 | 249, 266 | eqtrd 2774 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
(((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ ∀𝑓 ∈ 𝐹 ((𝑓 supp 0) = ℎ → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑓‘𝑤) · (𝑀 Σg 𝑤)))) ∈ 𝑡)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((((𝑒 ↾ (Word 𝐴 ∖ {𝑥})) ∪ {〈𝑥, 0〉})‘𝑤) · (𝑀 Σg 𝑤)))) = (𝑅 Σg (𝑤 ∈ ℎ ↦ ((𝑒‘𝑤) · (𝑀 Σg 𝑤))))) |
268 | | simplr 769 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢
((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) → 𝑒 ∈ 𝐹) |
269 | 268 | resexd 6047 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢
((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) → (𝑒 ↾ (Word 𝐴 ∖ {𝑥})) ∈ V) |
270 | | snex 5441 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢
{〈𝑥, 0〉}
∈ V |
271 | 270 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢
((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) → {〈𝑥, 0〉} ∈ V) |
272 | 269, 271,
202 | suppun2 32698 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢
((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) → (((𝑒 ↾ (Word 𝐴 ∖ {𝑥})) ∪ {〈𝑥, 0〉}) supp 0) = (((𝑒 ↾ (Word 𝐴 ∖ {𝑥})) supp 0) ∪ ({〈𝑥, 0〉} supp 0))) |
273 | 114, 202,
201 | fdifsupp 32699 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢
((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) → ((𝑒 ↾ (Word 𝐴 ∖ {𝑥})) supp 0) = ((𝑒 supp 0) ∖ {𝑥})) |
274 | | simpr 484 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢
((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) → (𝑒 supp 0) = (ℎ ∪ {𝑥})) |
275 | 274 | difeq1d 4134 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢
((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) → ((𝑒 supp 0) ∖ {𝑥}) = ((ℎ ∪ {𝑥}) ∖ {𝑥})) |
276 | | disjsn 4715 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ ((ℎ ∩ {𝑥}) = ∅ ↔ ¬ 𝑥 ∈ ℎ) |
277 | | undif5 4490 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ ((ℎ ∩ {𝑥}) = ∅ → ((ℎ ∪ {𝑥}) ∖ {𝑥}) = ℎ) |
278 | 276, 277 | sylbir 235 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (¬
𝑥 ∈ ℎ → ((ℎ ∪ {𝑥}) ∖ {𝑥}) = ℎ) |
279 | 184, 278 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢
((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) → ((ℎ ∪ {𝑥}) ∖ {𝑥}) = ℎ) |
280 | 273, 275,
279 | 3eqtrd 2778 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢
((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) → ((𝑒 ↾ (Word 𝐴 ∖ {𝑥})) supp 0) = ℎ) |
281 | | vex 3481 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ 𝑥 ∈ V |
282 | | c0ex 11252 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ 0 ∈
V |
283 | 281, 282 | xpsn 7160 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ ({𝑥} × {0}) = {〈𝑥, 0〉} |
284 | 283 | oveq1i 7440 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (({𝑥} × {0}) supp 0) =
({〈𝑥, 0〉} supp
0) |
285 | | fczsupp0 8216 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (({𝑥} × {0}) supp 0) =
∅ |
286 | 284, 285 | eqtr3i 2764 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢
({〈𝑥, 0〉}
supp 0) = ∅ |
287 | 286 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢
((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) → ({〈𝑥, 0〉} supp 0) =
∅) |
288 | 280, 287 | uneq12d 4178 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢
((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) → (((𝑒 ↾ (Word 𝐴 ∖ {𝑥})) supp 0) ∪ ({〈𝑥, 0〉} supp 0)) = (ℎ ∪ ∅)) |
289 | | un0 4399 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (ℎ ∪ ∅) = ℎ |
290 | 289 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢
((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) → (ℎ ∪ ∅) = ℎ) |
291 | 272, 288,
290 | 3eqtrd 2778 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) → (((𝑒 ↾ (Word 𝐴 ∖ {𝑥})) ∪ {〈𝑥, 0〉}) supp 0) = ℎ) |
292 | 291 | adantllr 719 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
(((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ ∀𝑓 ∈ 𝐹 ((𝑓 supp 0) = ℎ → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑓‘𝑤) · (𝑀 Σg 𝑤)))) ∈ 𝑡)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) → (((𝑒 ↾ (Word 𝐴 ∖ {𝑥})) ∪ {〈𝑥, 0〉}) supp 0) = ℎ) |
293 | | oveq1 7437 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑓 = ((𝑒 ↾ (Word 𝐴 ∖ {𝑥})) ∪ {〈𝑥, 0〉}) → (𝑓 supp 0) = (((𝑒 ↾ (Word 𝐴 ∖ {𝑥})) ∪ {〈𝑥, 0〉}) supp 0)) |
294 | 293 | eqeq1d 2736 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑓 = ((𝑒 ↾ (Word 𝐴 ∖ {𝑥})) ∪ {〈𝑥, 0〉}) → ((𝑓 supp 0) = ℎ ↔ (((𝑒 ↾ (Word 𝐴 ∖ {𝑥})) ∪ {〈𝑥, 0〉}) supp 0) = ℎ)) |
295 | | fveq1 6905 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (𝑓 = ((𝑒 ↾ (Word 𝐴 ∖ {𝑥})) ∪ {〈𝑥, 0〉}) → (𝑓‘𝑤) = (((𝑒 ↾ (Word 𝐴 ∖ {𝑥})) ∪ {〈𝑥, 0〉})‘𝑤)) |
296 | 295 | oveq1d 7445 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (𝑓 = ((𝑒 ↾ (Word 𝐴 ∖ {𝑥})) ∪ {〈𝑥, 0〉}) → ((𝑓‘𝑤) · (𝑀 Σg 𝑤)) = ((((𝑒 ↾ (Word 𝐴 ∖ {𝑥})) ∪ {〈𝑥, 0〉})‘𝑤) · (𝑀 Σg 𝑤))) |
297 | 296 | mpteq2dv 5249 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝑓 = ((𝑒 ↾ (Word 𝐴 ∖ {𝑥})) ∪ {〈𝑥, 0〉}) → (𝑤 ∈ Word 𝐴 ↦ ((𝑓‘𝑤) · (𝑀 Σg 𝑤))) = (𝑤 ∈ Word 𝐴 ↦ ((((𝑒 ↾ (Word 𝐴 ∖ {𝑥})) ∪ {〈𝑥, 0〉})‘𝑤) · (𝑀 Σg 𝑤)))) |
298 | 297 | oveq2d 7446 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑓 = ((𝑒 ↾ (Word 𝐴 ∖ {𝑥})) ∪ {〈𝑥, 0〉}) → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑓‘𝑤) · (𝑀 Σg 𝑤)))) = (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((((𝑒 ↾ (Word 𝐴 ∖ {𝑥})) ∪ {〈𝑥, 0〉})‘𝑤) · (𝑀 Σg 𝑤))))) |
299 | 298 | eleq1d 2823 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑓 = ((𝑒 ↾ (Word 𝐴 ∖ {𝑥})) ∪ {〈𝑥, 0〉}) → ((𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑓‘𝑤) · (𝑀 Σg 𝑤)))) ∈ 𝑡 ↔ (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((((𝑒 ↾ (Word 𝐴 ∖ {𝑥})) ∪ {〈𝑥, 0〉})‘𝑤) · (𝑀 Σg 𝑤)))) ∈ 𝑡)) |
300 | 294, 299 | imbi12d 344 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑓 = ((𝑒 ↾ (Word 𝐴 ∖ {𝑥})) ∪ {〈𝑥, 0〉}) → (((𝑓 supp 0) = ℎ → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑓‘𝑤) · (𝑀 Σg 𝑤)))) ∈ 𝑡) ↔ ((((𝑒 ↾ (Word 𝐴 ∖ {𝑥})) ∪ {〈𝑥, 0〉}) supp 0) = ℎ → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((((𝑒 ↾ (Word 𝐴 ∖ {𝑥})) ∪ {〈𝑥, 0〉})‘𝑤) · (𝑀 Σg 𝑤)))) ∈ 𝑡))) |
301 | | simpllr 776 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
(((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ ∀𝑓 ∈ 𝐹 ((𝑓 supp 0) = ℎ → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑓‘𝑤) · (𝑀 Σg 𝑤)))) ∈ 𝑡)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) → ∀𝑓 ∈ 𝐹 ((𝑓 supp 0) = ℎ → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑓‘𝑤) · (𝑀 Σg 𝑤)))) ∈ 𝑡)) |
302 | | breq1 5150 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑓 = ((𝑒 ↾ (Word 𝐴 ∖ {𝑥})) ∪ {〈𝑥, 0〉}) → (𝑓 finSupp 0 ↔ ((𝑒 ↾ (Word 𝐴 ∖ {𝑥})) ∪ {〈𝑥, 0〉}) finSupp 0)) |
303 | 54 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢
(((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ ∀𝑓 ∈ 𝐹 ((𝑓 supp 0) = ℎ → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑓‘𝑤) · (𝑀 Σg 𝑤)))) ∈ 𝑡)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) → ℤ ∈ V) |
304 | 114 | adantllr 719 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢
(((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ ∀𝑓 ∈ 𝐹 ((𝑓 supp 0) = ℎ → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑓‘𝑤) · (𝑀 Σg 𝑤)))) ∈ 𝑡)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) → Word 𝐴 ∈ V) |
305 | 203 | adantllr 719 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢
(((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ ∀𝑓 ∈ 𝐹 ((𝑓 supp 0) = ℎ → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑓‘𝑤) · (𝑀 Σg 𝑤)))) ∈ 𝑡)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) → (𝑦 ∈ Word 𝐴 ↦ if(𝑦 = 𝑥, 0, (𝑒‘𝑦))) = ((𝑒 ↾ (Word 𝐴 ∖ {𝑥})) ∪ {〈𝑥, 0〉})) |
306 | | 0zd 12622 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢
(((((((((((𝜑 ∧
𝑡 ∈
(SubRing‘𝑅)) ∧
𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ ∀𝑓 ∈ 𝐹 ((𝑓 supp 0) = ℎ → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑓‘𝑤) · (𝑀 Σg 𝑤)))) ∈ 𝑡)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) ∧ 𝑦 ∈ Word 𝐴) ∧ 𝑦 = 𝑥) → 0 ∈ ℤ) |
307 | | simp-10l 795 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢
(((((((((((𝜑 ∧
𝑡 ∈
(SubRing‘𝑅)) ∧
𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ ∀𝑓 ∈ 𝐹 ((𝑓 supp 0) = ℎ → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑓‘𝑤) · (𝑀 Σg 𝑤)))) ∈ 𝑡)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) ∧ 𝑦 ∈ Word 𝐴) ∧ ¬ 𝑦 = 𝑥) → 𝜑) |
308 | | simp-4r 784 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢
(((((((((((𝜑 ∧
𝑡 ∈
(SubRing‘𝑅)) ∧
𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ ∀𝑓 ∈ 𝐹 ((𝑓 supp 0) = ℎ → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑓‘𝑤) · (𝑀 Σg 𝑤)))) ∈ 𝑡)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) ∧ 𝑦 ∈ Word 𝐴) ∧ ¬ 𝑦 = 𝑥) → 𝑒 ∈ 𝐹) |
309 | 307, 308,
121 | syl2anc 584 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢
(((((((((((𝜑 ∧
𝑡 ∈
(SubRing‘𝑅)) ∧
𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ ∀𝑓 ∈ 𝐹 ((𝑓 supp 0) = ℎ → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑓‘𝑤) · (𝑀 Σg 𝑤)))) ∈ 𝑡)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) ∧ 𝑦 ∈ Word 𝐴) ∧ ¬ 𝑦 = 𝑥) → 𝑒:Word 𝐴⟶ℤ) |
310 | | simplr 769 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢
(((((((((((𝜑 ∧
𝑡 ∈
(SubRing‘𝑅)) ∧
𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ ∀𝑓 ∈ 𝐹 ((𝑓 supp 0) = ℎ → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑓‘𝑤) · (𝑀 Σg 𝑤)))) ∈ 𝑡)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) ∧ 𝑦 ∈ Word 𝐴) ∧ ¬ 𝑦 = 𝑥) → 𝑦 ∈ Word 𝐴) |
311 | 309, 310 | ffvelcdmd 7104 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢
(((((((((((𝜑 ∧
𝑡 ∈
(SubRing‘𝑅)) ∧
𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ ∀𝑓 ∈ 𝐹 ((𝑓 supp 0) = ℎ → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑓‘𝑤) · (𝑀 Σg 𝑤)))) ∈ 𝑡)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) ∧ 𝑦 ∈ Word 𝐴) ∧ ¬ 𝑦 = 𝑥) → (𝑒‘𝑦) ∈ ℤ) |
312 | 306, 311 | ifclda 4565 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢
((((((((((𝜑 ∧
𝑡 ∈
(SubRing‘𝑅)) ∧
𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ ∀𝑓 ∈ 𝐹 ((𝑓 supp 0) = ℎ → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑓‘𝑤) · (𝑀 Σg 𝑤)))) ∈ 𝑡)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) ∧ 𝑦 ∈ Word 𝐴) → if(𝑦 = 𝑥, 0, (𝑒‘𝑦)) ∈ ℤ) |
313 | 312 | fmpttd 7134 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢
(((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ ∀𝑓 ∈ 𝐹 ((𝑓 supp 0) = ℎ → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑓‘𝑤) · (𝑀 Σg 𝑤)))) ∈ 𝑡)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) → (𝑦 ∈ Word 𝐴 ↦ if(𝑦 = 𝑥, 0, (𝑒‘𝑦))):Word 𝐴⟶ℤ) |
314 | 305, 313 | feq1dd 6721 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢
(((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ ∀𝑓 ∈ 𝐹 ((𝑓 supp 0) = ℎ → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑓‘𝑤) · (𝑀 Σg 𝑤)))) ∈ 𝑡)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) → ((𝑒 ↾ (Word 𝐴 ∖ {𝑥})) ∪ {〈𝑥, 0〉}):Word 𝐴⟶ℤ) |
315 | 303, 304,
314 | elmapdd 8879 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢
(((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ ∀𝑓 ∈ 𝐹 ((𝑓 supp 0) = ℎ → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑓‘𝑤) · (𝑀 Σg 𝑤)))) ∈ 𝑡)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) → ((𝑒 ↾ (Word 𝐴 ∖ {𝑥})) ∪ {〈𝑥, 0〉}) ∈ (ℤ
↑m Word 𝐴)) |
316 | | 0zd 12622 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢
(((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ ∀𝑓 ∈ 𝐹 ((𝑓 supp 0) = ℎ → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑓‘𝑤) · (𝑀 Σg 𝑤)))) ∈ 𝑡)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) → 0 ∈ ℤ) |
317 | 314 | ffund 6740 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢
(((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ ∀𝑓 ∈ 𝐹 ((𝑓 supp 0) = ℎ → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑓‘𝑤) · (𝑀 Σg 𝑤)))) ∈ 𝑡)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) → Fun ((𝑒 ↾ (Word 𝐴 ∖ {𝑥})) ∪ {〈𝑥, 0〉})) |
318 | 166 | adantllr 719 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢
(((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ ∀𝑓 ∈ 𝐹 ((𝑓 supp 0) = ℎ → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑓‘𝑤) · (𝑀 Σg 𝑤)))) ∈ 𝑡)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) → ℎ ∈ Fin) |
319 | 292, 318 | eqeltrd 2838 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢
(((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ ∀𝑓 ∈ 𝐹 ((𝑓 supp 0) = ℎ → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑓‘𝑤) · (𝑀 Σg 𝑤)))) ∈ 𝑡)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) → (((𝑒 ↾ (Word 𝐴 ∖ {𝑥})) ∪ {〈𝑥, 0〉}) supp 0) ∈
Fin) |
320 | 315, 316,
317, 319 | isfsuppd 9403 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢
(((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ ∀𝑓 ∈ 𝐹 ((𝑓 supp 0) = ℎ → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑓‘𝑤) · (𝑀 Σg 𝑤)))) ∈ 𝑡)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) → ((𝑒 ↾ (Word 𝐴 ∖ {𝑥})) ∪ {〈𝑥, 0〉}) finSupp 0) |
321 | 302, 315,
320 | elrabd 3696 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢
(((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ ∀𝑓 ∈ 𝐹 ((𝑓 supp 0) = ℎ → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑓‘𝑤) · (𝑀 Σg 𝑤)))) ∈ 𝑡)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) → ((𝑒 ↾ (Word 𝐴 ∖ {𝑥})) ∪ {〈𝑥, 0〉}) ∈ {𝑓 ∈ (ℤ ↑m Word
𝐴) ∣ 𝑓 finSupp 0}) |
322 | 321, 12 | eleqtrrdi 2849 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
(((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ ∀𝑓 ∈ 𝐹 ((𝑓 supp 0) = ℎ → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑓‘𝑤) · (𝑀 Σg 𝑤)))) ∈ 𝑡)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) → ((𝑒 ↾ (Word 𝐴 ∖ {𝑥})) ∪ {〈𝑥, 0〉}) ∈ 𝐹) |
323 | 300, 301,
322 | rspcdva 3622 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
(((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ ∀𝑓 ∈ 𝐹 ((𝑓 supp 0) = ℎ → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑓‘𝑤) · (𝑀 Σg 𝑤)))) ∈ 𝑡)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) → ((((𝑒 ↾ (Word 𝐴 ∖ {𝑥})) ∪ {〈𝑥, 0〉}) supp 0) = ℎ → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((((𝑒 ↾ (Word 𝐴 ∖ {𝑥})) ∪ {〈𝑥, 0〉})‘𝑤) · (𝑀 Σg 𝑤)))) ∈ 𝑡)) |
324 | 292, 323 | mpd 15 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
(((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ ∀𝑓 ∈ 𝐹 ((𝑓 supp 0) = ℎ → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑓‘𝑤) · (𝑀 Σg 𝑤)))) ∈ 𝑡)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((((𝑒 ↾ (Word 𝐴 ∖ {𝑥})) ∪ {〈𝑥, 0〉})‘𝑤) · (𝑀 Σg 𝑤)))) ∈ 𝑡) |
325 | 267, 324 | eqeltrrd 2839 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
(((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ ∀𝑓 ∈ 𝐹 ((𝑓 supp 0) = ℎ → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑓‘𝑤) · (𝑀 Σg 𝑤)))) ∈ 𝑡)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) → (𝑅 Σg (𝑤 ∈ ℎ ↦ ((𝑒‘𝑤) · (𝑀 Σg 𝑤)))) ∈ 𝑡) |
326 | 86 | ad8antr 740 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
(((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ ∀𝑓 ∈ 𝐹 ((𝑓 supp 0) = ℎ → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑓‘𝑤) · (𝑀 Σg 𝑤)))) ∈ 𝑡)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) → 𝑅 ∈ Grp) |
327 | 10 | subrgsubm 20601 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑡 ∈ (SubRing‘𝑅) → 𝑡 ∈ (SubMnd‘𝑀)) |
328 | 327 | ad8antlr 741 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
(((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ ∀𝑓 ∈ 𝐹 ((𝑓 supp 0) = ℎ → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑓‘𝑤) · (𝑀 Σg 𝑤)))) ∈ 𝑡)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) → 𝑡 ∈ (SubMnd‘𝑀)) |
329 | | sswrd 14556 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝐴 ⊆ 𝑡 → Word 𝐴 ⊆ Word 𝑡) |
330 | 329 | ad7antlr 739 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
(((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ ∀𝑓 ∈ 𝐹 ((𝑓 supp 0) = ℎ → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑓‘𝑤) · (𝑀 Σg 𝑤)))) ∈ 𝑡)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) → Word 𝐴 ⊆ Word 𝑡) |
331 | 187 | adantllr 719 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
(((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ ∀𝑓 ∈ 𝐹 ((𝑓 supp 0) = ℎ → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑓‘𝑤) · (𝑀 Σg 𝑤)))) ∈ 𝑡)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) → 𝑥 ∈ Word 𝐴) |
332 | 330, 331 | sseldd 3995 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
(((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ ∀𝑓 ∈ 𝐹 ((𝑓 supp 0) = ℎ → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑓‘𝑤) · (𝑀 Σg 𝑤)))) ∈ 𝑡)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) → 𝑥 ∈ Word 𝑡) |
333 | | gsumwsubmcl 18862 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝑡 ∈ (SubMnd‘𝑀) ∧ 𝑥 ∈ Word 𝑡) → (𝑀 Σg 𝑥) ∈ 𝑡) |
334 | 328, 332,
333 | syl2anc 584 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
(((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ ∀𝑓 ∈ 𝐹 ((𝑓 supp 0) = ℎ → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑓‘𝑤) · (𝑀 Σg 𝑤)))) ∈ 𝑡)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) → (𝑀 Σg 𝑥) ∈ 𝑡) |
335 | 123 | ad4ant13 751 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
(((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ ∀𝑓 ∈ 𝐹 ((𝑓 supp 0) = ℎ → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑓‘𝑤) · (𝑀 Σg 𝑤)))) ∈ 𝑡)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) → 𝑒:Word 𝐴⟶ℤ) |
336 | 335, 331 | ffvelcdmd 7104 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
(((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ ∀𝑓 ∈ 𝐹 ((𝑓 supp 0) = ℎ → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑓‘𝑤) · (𝑀 Σg 𝑤)))) ∈ 𝑡)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) → (𝑒‘𝑥) ∈ ℤ) |
337 | 2, 11, 326, 334, 200, 336 | subgmulgcld 33030 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
(((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ ∀𝑓 ∈ 𝐹 ((𝑓 supp 0) = ℎ → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑓‘𝑤) · (𝑀 Σg 𝑤)))) ∈ 𝑡)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) → ((𝑒‘𝑥) · (𝑀 Σg 𝑥)) ∈ 𝑡) |
338 | 158, 200,
325, 337 | subgcld 33028 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ ∀𝑓 ∈ 𝐹 ((𝑓 supp 0) = ℎ → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑓‘𝑤) · (𝑀 Σg 𝑤)))) ∈ 𝑡)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) → ((𝑅 Σg (𝑤 ∈ ℎ ↦ ((𝑒‘𝑤) · (𝑀 Σg 𝑤))))(+g‘𝑅)((𝑒‘𝑥) · (𝑀 Σg 𝑥))) ∈ 𝑡) |
339 | 199, 338 | eqeltrd 2838 |
. . . . . . . . . . . . . . . . . . 19
⊢
(((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ ∀𝑓 ∈ 𝐹 ((𝑓 supp 0) = ℎ → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑓‘𝑤) · (𝑀 Σg 𝑤)))) ∈ 𝑡)) ∧ 𝑒 ∈ 𝐹) ∧ (𝑒 supp 0) = (ℎ ∪ {𝑥})) → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑒‘𝑤) · (𝑀 Σg 𝑤)))) ∈ 𝑡) |
340 | 339 | ex 412 |
. . . . . . . . . . . . . . . . . 18
⊢
((((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ ∀𝑓 ∈ 𝐹 ((𝑓 supp 0) = ℎ → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑓‘𝑤) · (𝑀 Σg 𝑤)))) ∈ 𝑡)) ∧ 𝑒 ∈ 𝐹) → ((𝑒 supp 0) = (ℎ ∪ {𝑥}) → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑒‘𝑤) · (𝑀 Σg 𝑤)))) ∈ 𝑡)) |
341 | 340 | ralrimiva 3143 |
. . . . . . . . . . . . . . . . 17
⊢
(((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) ∧ ∀𝑓 ∈ 𝐹 ((𝑓 supp 0) = ℎ → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑓‘𝑤) · (𝑀 Σg 𝑤)))) ∈ 𝑡)) → ∀𝑒 ∈ 𝐹 ((𝑒 supp 0) = (ℎ ∪ {𝑥}) → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑒‘𝑤) · (𝑀 Σg 𝑤)))) ∈ 𝑡)) |
342 | 341 | ex 412 |
. . . . . . . . . . . . . . . 16
⊢
((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ ℎ ⊆ (𝑔 supp 0)) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ)) → (∀𝑓 ∈ 𝐹 ((𝑓 supp 0) = ℎ → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑓‘𝑤) · (𝑀 Σg 𝑤)))) ∈ 𝑡) → ∀𝑒 ∈ 𝐹 ((𝑒 supp 0) = (ℎ ∪ {𝑥}) → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑒‘𝑤) · (𝑀 Σg 𝑤)))) ∈ 𝑡))) |
343 | 342 | anasss 466 |
. . . . . . . . . . . . . . 15
⊢
(((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ (ℎ ⊆ (𝑔 supp 0) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ))) → (∀𝑓 ∈ 𝐹 ((𝑓 supp 0) = ℎ → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑓‘𝑤) · (𝑀 Σg 𝑤)))) ∈ 𝑡) → ∀𝑒 ∈ 𝐹 ((𝑒 supp 0) = (ℎ ∪ {𝑥}) → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑒‘𝑤) · (𝑀 Σg 𝑤)))) ∈ 𝑡))) |
344 | | oveq1 7437 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑒 = 𝑓 → (𝑒 supp 0) = (𝑓 supp 0)) |
345 | 344 | eqeq1d 2736 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑒 = 𝑓 → ((𝑒 supp 0) = (ℎ ∪ {𝑥}) ↔ (𝑓 supp 0) = (ℎ ∪ {𝑥}))) |
346 | | fveq1 6905 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑒 = 𝑓 → (𝑒‘𝑤) = (𝑓‘𝑤)) |
347 | 346 | oveq1d 7445 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑒 = 𝑓 → ((𝑒‘𝑤) · (𝑀 Σg 𝑤)) = ((𝑓‘𝑤) · (𝑀 Σg 𝑤))) |
348 | 347 | mpteq2dv 5249 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑒 = 𝑓 → (𝑤 ∈ Word 𝐴 ↦ ((𝑒‘𝑤) · (𝑀 Σg 𝑤))) = (𝑤 ∈ Word 𝐴 ↦ ((𝑓‘𝑤) · (𝑀 Σg 𝑤)))) |
349 | 348 | oveq2d 7446 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑒 = 𝑓 → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑒‘𝑤) · (𝑀 Σg 𝑤)))) = (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑓‘𝑤) · (𝑀 Σg 𝑤))))) |
350 | 349 | eleq1d 2823 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑒 = 𝑓 → ((𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑒‘𝑤) · (𝑀 Σg 𝑤)))) ∈ 𝑡 ↔ (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑓‘𝑤) · (𝑀 Σg 𝑤)))) ∈ 𝑡)) |
351 | 345, 350 | imbi12d 344 |
. . . . . . . . . . . . . . . 16
⊢ (𝑒 = 𝑓 → (((𝑒 supp 0) = (ℎ ∪ {𝑥}) → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑒‘𝑤) · (𝑀 Σg 𝑤)))) ∈ 𝑡) ↔ ((𝑓 supp 0) = (ℎ ∪ {𝑥}) → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑓‘𝑤) · (𝑀 Σg 𝑤)))) ∈ 𝑡))) |
352 | 351 | cbvralvw 3234 |
. . . . . . . . . . . . . . 15
⊢
(∀𝑒 ∈
𝐹 ((𝑒 supp 0) = (ℎ ∪ {𝑥}) → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑒‘𝑤) · (𝑀 Σg 𝑤)))) ∈ 𝑡) ↔ ∀𝑓 ∈ 𝐹 ((𝑓 supp 0) = (ℎ ∪ {𝑥}) → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑓‘𝑤) · (𝑀 Σg 𝑤)))) ∈ 𝑡)) |
353 | 343, 352 | imbitrdi 251 |
. . . . . . . . . . . . . 14
⊢
(((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) ∧ (ℎ ⊆ (𝑔 supp 0) ∧ 𝑥 ∈ ((𝑔 supp 0) ∖ ℎ))) → (∀𝑓 ∈ 𝐹 ((𝑓 supp 0) = ℎ → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑓‘𝑤) · (𝑀 Σg 𝑤)))) ∈ 𝑡) → ∀𝑓 ∈ 𝐹 ((𝑓 supp 0) = (ℎ ∪ {𝑥}) → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑓‘𝑤) · (𝑀 Σg 𝑤)))) ∈ 𝑡))) |
354 | 31, 34, 37, 40, 112, 353, 163 | findcard2d 9204 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) → ∀𝑓 ∈ 𝐹 ((𝑓 supp 0) = (𝑔 supp 0) → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑓‘𝑤) · (𝑀 Σg 𝑤)))) ∈ 𝑡)) |
355 | | simpr 484 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) → 𝑔 ∈ 𝐹) |
356 | 28, 354, 355 | rspcdva 3622 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) → ((𝑔 supp 0) = (𝑔 supp 0) → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑔‘𝑤) · (𝑀 Σg 𝑤)))) ∈ 𝑡)) |
357 | 20, 356 | mpd 15 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑔 ∈ 𝐹) → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑔‘𝑤) · (𝑀 Σg 𝑤)))) ∈ 𝑡) |
358 | 357 | ad4ant13 751 |
. . . . . . . . . 10
⊢
((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑠 ∈ 𝑆) ∧ 𝑔 ∈ 𝐹) ∧ 𝑠 = (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑔‘𝑤) · (𝑀 Σg 𝑤))))) → (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑔‘𝑤) · (𝑀 Σg 𝑤)))) ∈ 𝑡) |
359 | 19, 358 | eqeltrd 2838 |
. . . . . . . . 9
⊢
((((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑠 ∈ 𝑆) ∧ 𝑔 ∈ 𝐹) ∧ 𝑠 = (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑔‘𝑤) · (𝑀 Σg 𝑤))))) → 𝑠 ∈ 𝑡) |
360 | | eqid 2734 |
. . . . . . . . . 10
⊢ (𝑔 ∈ 𝐹 ↦ (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑔‘𝑤) · (𝑀 Σg 𝑤))))) = (𝑔 ∈ 𝐹 ↦ (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑔‘𝑤) · (𝑀 Σg 𝑤))))) |
361 | 13 | eleq2i 2830 |
. . . . . . . . . . . 12
⊢ (𝑠 ∈ 𝑆 ↔ 𝑠 ∈ ran (𝑔 ∈ 𝐹 ↦ (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑔‘𝑤) · (𝑀 Σg 𝑤)))))) |
362 | 361 | biimpi 216 |
. . . . . . . . . . 11
⊢ (𝑠 ∈ 𝑆 → 𝑠 ∈ ran (𝑔 ∈ 𝐹 ↦ (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑔‘𝑤) · (𝑀 Σg 𝑤)))))) |
363 | 362 | adantl 481 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑠 ∈ 𝑆) → 𝑠 ∈ ran (𝑔 ∈ 𝐹 ↦ (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑔‘𝑤) · (𝑀 Σg 𝑤)))))) |
364 | 360, 363 | elrnmpt2d 5979 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑠 ∈ 𝑆) → ∃𝑔 ∈ 𝐹 𝑠 = (𝑅 Σg (𝑤 ∈ Word 𝐴 ↦ ((𝑔‘𝑤) · (𝑀 Σg 𝑤))))) |
365 | 359, 364 | r19.29a 3159 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) ∧ 𝑠 ∈ 𝑆) → 𝑠 ∈ 𝑡) |
366 | 365 | ex 412 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) → (𝑠 ∈ 𝑆 → 𝑠 ∈ 𝑡)) |
367 | 366 | ssrdv 4000 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) ∧ 𝐴 ⊆ 𝑡) → 𝑆 ⊆ 𝑡) |
368 | 367 | ex 412 |
. . . . 5
⊢ ((𝜑 ∧ 𝑡 ∈ (SubRing‘𝑅)) → (𝐴 ⊆ 𝑡 → 𝑆 ⊆ 𝑡)) |
369 | 368 | ralrimiva 3143 |
. . . 4
⊢ (𝜑 → ∀𝑡 ∈ (SubRing‘𝑅)(𝐴 ⊆ 𝑡 → 𝑆 ⊆ 𝑡)) |
370 | | ssintrab 4975 |
. . . 4
⊢ (𝑆 ⊆ ∩ {𝑡
∈ (SubRing‘𝑅)
∣ 𝐴 ⊆ 𝑡} ↔ ∀𝑡 ∈ (SubRing‘𝑅)(𝐴 ⊆ 𝑡 → 𝑆 ⊆ 𝑡)) |
371 | 369, 370 | sylibr 234 |
. . 3
⊢ (𝜑 → 𝑆 ⊆ ∩ {𝑡 ∈ (SubRing‘𝑅) ∣ 𝐴 ⊆ 𝑡}) |
372 | 18, 371 | eqssd 4012 |
. 2
⊢ (𝜑 → ∩ {𝑡
∈ (SubRing‘𝑅)
∣ 𝐴 ⊆ 𝑡} = 𝑆) |
373 | 8, 372 | eqtrd 2774 |
1
⊢ (𝜑 → (𝑁‘𝐴) = 𝑆) |