Step | Hyp | Ref
| Expression |
1 | | oveq2 5918 |
. . . . 5
⊢ (𝑊 = ∅ → (𝐺 Σg
𝑊) = (𝐺 Σg
∅)) |
2 | 1 | adantl 277 |
. . . 4
⊢ (((𝑆 ∈ (SubMnd‘𝐺) ∧ 𝑊 ∈ Word 𝑆) ∧ 𝑊 = ∅) → (𝐺 Σg 𝑊) = (𝐺 Σg
∅)) |
3 | | submrcl 13033 |
. . . . . 6
⊢ (𝑆 ∈ (SubMnd‘𝐺) → 𝐺 ∈ Mnd) |
4 | | eqid 2193 |
. . . . . . 7
⊢
(0g‘𝐺) = (0g‘𝐺) |
5 | 4 | gsum0g 12969 |
. . . . . 6
⊢ (𝐺 ∈ Mnd → (𝐺 Σg
∅) = (0g‘𝐺)) |
6 | 3, 5 | syl 14 |
. . . . 5
⊢ (𝑆 ∈ (SubMnd‘𝐺) → (𝐺 Σg ∅) =
(0g‘𝐺)) |
7 | 6 | ad2antrr 488 |
. . . 4
⊢ (((𝑆 ∈ (SubMnd‘𝐺) ∧ 𝑊 ∈ Word 𝑆) ∧ 𝑊 = ∅) → (𝐺 Σg ∅) =
(0g‘𝐺)) |
8 | 2, 7 | eqtrd 2226 |
. . 3
⊢ (((𝑆 ∈ (SubMnd‘𝐺) ∧ 𝑊 ∈ Word 𝑆) ∧ 𝑊 = ∅) → (𝐺 Σg 𝑊) = (0g‘𝐺)) |
9 | 4 | subm0cl 13040 |
. . . 4
⊢ (𝑆 ∈ (SubMnd‘𝐺) →
(0g‘𝐺)
∈ 𝑆) |
10 | 9 | ad2antrr 488 |
. . 3
⊢ (((𝑆 ∈ (SubMnd‘𝐺) ∧ 𝑊 ∈ Word 𝑆) ∧ 𝑊 = ∅) →
(0g‘𝐺)
∈ 𝑆) |
11 | 8, 10 | eqeltrd 2270 |
. 2
⊢ (((𝑆 ∈ (SubMnd‘𝐺) ∧ 𝑊 ∈ Word 𝑆) ∧ 𝑊 = ∅) → (𝐺 Σg 𝑊) ∈ 𝑆) |
12 | | eqid 2193 |
. . . 4
⊢
(Base‘𝐺) =
(Base‘𝐺) |
13 | | eqid 2193 |
. . . 4
⊢
(+g‘𝐺) = (+g‘𝐺) |
14 | 3 | ad2antrr 488 |
. . . 4
⊢ (((𝑆 ∈ (SubMnd‘𝐺) ∧ 𝑊 ∈ Word 𝑆) ∧ 𝑊 ≠ ∅) → 𝐺 ∈ Mnd) |
15 | | lennncl 10924 |
. . . . . . 7
⊢ ((𝑊 ∈ Word 𝑆 ∧ 𝑊 ≠ ∅) → (♯‘𝑊) ∈
ℕ) |
16 | 15 | adantll 476 |
. . . . . 6
⊢ (((𝑆 ∈ (SubMnd‘𝐺) ∧ 𝑊 ∈ Word 𝑆) ∧ 𝑊 ≠ ∅) → (♯‘𝑊) ∈
ℕ) |
17 | | nnm1nn0 9271 |
. . . . . 6
⊢
((♯‘𝑊)
∈ ℕ → ((♯‘𝑊) − 1) ∈
ℕ0) |
18 | 16, 17 | syl 14 |
. . . . 5
⊢ (((𝑆 ∈ (SubMnd‘𝐺) ∧ 𝑊 ∈ Word 𝑆) ∧ 𝑊 ≠ ∅) → ((♯‘𝑊) − 1) ∈
ℕ0) |
19 | | nn0uz 9617 |
. . . . 5
⊢
ℕ0 = (ℤ≥‘0) |
20 | 18, 19 | eleqtrdi 2286 |
. . . 4
⊢ (((𝑆 ∈ (SubMnd‘𝐺) ∧ 𝑊 ∈ Word 𝑆) ∧ 𝑊 ≠ ∅) → ((♯‘𝑊) − 1) ∈
(ℤ≥‘0)) |
21 | | wrdf 10910 |
. . . . . . 7
⊢ (𝑊 ∈ Word 𝑆 → 𝑊:(0..^(♯‘𝑊))⟶𝑆) |
22 | 21 | ad2antlr 489 |
. . . . . 6
⊢ (((𝑆 ∈ (SubMnd‘𝐺) ∧ 𝑊 ∈ Word 𝑆) ∧ 𝑊 ≠ ∅) → 𝑊:(0..^(♯‘𝑊))⟶𝑆) |
23 | 16 | nnzd 9428 |
. . . . . . . 8
⊢ (((𝑆 ∈ (SubMnd‘𝐺) ∧ 𝑊 ∈ Word 𝑆) ∧ 𝑊 ≠ ∅) → (♯‘𝑊) ∈
ℤ) |
24 | | fzoval 10204 |
. . . . . . . 8
⊢
((♯‘𝑊)
∈ ℤ → (0..^(♯‘𝑊)) = (0...((♯‘𝑊) − 1))) |
25 | 23, 24 | syl 14 |
. . . . . . 7
⊢ (((𝑆 ∈ (SubMnd‘𝐺) ∧ 𝑊 ∈ Word 𝑆) ∧ 𝑊 ≠ ∅) →
(0..^(♯‘𝑊)) =
(0...((♯‘𝑊)
− 1))) |
26 | 25 | feq2d 5383 |
. . . . . 6
⊢ (((𝑆 ∈ (SubMnd‘𝐺) ∧ 𝑊 ∈ Word 𝑆) ∧ 𝑊 ≠ ∅) → (𝑊:(0..^(♯‘𝑊))⟶𝑆 ↔ 𝑊:(0...((♯‘𝑊) − 1))⟶𝑆)) |
27 | 22, 26 | mpbid 147 |
. . . . 5
⊢ (((𝑆 ∈ (SubMnd‘𝐺) ∧ 𝑊 ∈ Word 𝑆) ∧ 𝑊 ≠ ∅) → 𝑊:(0...((♯‘𝑊) − 1))⟶𝑆) |
28 | 12 | submss 13038 |
. . . . . 6
⊢ (𝑆 ∈ (SubMnd‘𝐺) → 𝑆 ⊆ (Base‘𝐺)) |
29 | 28 | ad2antrr 488 |
. . . . 5
⊢ (((𝑆 ∈ (SubMnd‘𝐺) ∧ 𝑊 ∈ Word 𝑆) ∧ 𝑊 ≠ ∅) → 𝑆 ⊆ (Base‘𝐺)) |
30 | 27, 29 | fssd 5408 |
. . . 4
⊢ (((𝑆 ∈ (SubMnd‘𝐺) ∧ 𝑊 ∈ Word 𝑆) ∧ 𝑊 ≠ ∅) → 𝑊:(0...((♯‘𝑊) − 1))⟶(Base‘𝐺)) |
31 | 12, 13, 14, 20, 30 | gsumval2 12970 |
. . 3
⊢ (((𝑆 ∈ (SubMnd‘𝐺) ∧ 𝑊 ∈ Word 𝑆) ∧ 𝑊 ≠ ∅) → (𝐺 Σg 𝑊) =
(seq0((+g‘𝐺), 𝑊)‘((♯‘𝑊) − 1))) |
32 | | fvexg 5565 |
. . . . 5
⊢ ((𝑊 ∈ Word 𝑆 ∧ 𝑥 ∈ (ℤ≥‘0))
→ (𝑊‘𝑥) ∈ V) |
33 | 32 | ad4ant24 516 |
. . . 4
⊢ ((((𝑆 ∈ (SubMnd‘𝐺) ∧ 𝑊 ∈ Word 𝑆) ∧ 𝑊 ≠ ∅) ∧ 𝑥 ∈ (ℤ≥‘0))
→ (𝑊‘𝑥) ∈ V) |
34 | 27 | ffvelcdmda 5685 |
. . . 4
⊢ ((((𝑆 ∈ (SubMnd‘𝐺) ∧ 𝑊 ∈ Word 𝑆) ∧ 𝑊 ≠ ∅) ∧ 𝑥 ∈ (0...((♯‘𝑊) − 1))) → (𝑊‘𝑥) ∈ 𝑆) |
35 | 13 | submcl 13041 |
. . . . . 6
⊢ ((𝑆 ∈ (SubMnd‘𝐺) ∧ 𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆) → (𝑥(+g‘𝐺)𝑦) ∈ 𝑆) |
36 | 35 | 3expb 1206 |
. . . . 5
⊢ ((𝑆 ∈ (SubMnd‘𝐺) ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆)) → (𝑥(+g‘𝐺)𝑦) ∈ 𝑆) |
37 | 36 | ad4ant14 514 |
. . . 4
⊢ ((((𝑆 ∈ (SubMnd‘𝐺) ∧ 𝑊 ∈ Word 𝑆) ∧ 𝑊 ≠ ∅) ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆)) → (𝑥(+g‘𝐺)𝑦) ∈ 𝑆) |
38 | | ssv 3201 |
. . . . 5
⊢ 𝑆 ⊆ V |
39 | 38 | a1i 9 |
. . . 4
⊢ (((𝑆 ∈ (SubMnd‘𝐺) ∧ 𝑊 ∈ Word 𝑆) ∧ 𝑊 ≠ ∅) → 𝑆 ⊆ V) |
40 | | simprl 529 |
. . . . 5
⊢ ((((𝑆 ∈ (SubMnd‘𝐺) ∧ 𝑊 ∈ Word 𝑆) ∧ 𝑊 ≠ ∅) ∧ (𝑥 ∈ V ∧ 𝑦 ∈ V)) → 𝑥 ∈ V) |
41 | 14 | adantr 276 |
. . . . . 6
⊢ ((((𝑆 ∈ (SubMnd‘𝐺) ∧ 𝑊 ∈ Word 𝑆) ∧ 𝑊 ≠ ∅) ∧ (𝑥 ∈ V ∧ 𝑦 ∈ V)) → 𝐺 ∈ Mnd) |
42 | | plusgslid 12720 |
. . . . . . 7
⊢
(+g = Slot (+g‘ndx) ∧
(+g‘ndx) ∈ ℕ) |
43 | 42 | slotex 12635 |
. . . . . 6
⊢ (𝐺 ∈ Mnd →
(+g‘𝐺)
∈ V) |
44 | 41, 43 | syl 14 |
. . . . 5
⊢ ((((𝑆 ∈ (SubMnd‘𝐺) ∧ 𝑊 ∈ Word 𝑆) ∧ 𝑊 ≠ ∅) ∧ (𝑥 ∈ V ∧ 𝑦 ∈ V)) → (+g‘𝐺) ∈ V) |
45 | | simprr 531 |
. . . . 5
⊢ ((((𝑆 ∈ (SubMnd‘𝐺) ∧ 𝑊 ∈ Word 𝑆) ∧ 𝑊 ≠ ∅) ∧ (𝑥 ∈ V ∧ 𝑦 ∈ V)) → 𝑦 ∈ V) |
46 | | ovexg 5944 |
. . . . 5
⊢ ((𝑥 ∈ V ∧
(+g‘𝐺)
∈ V ∧ 𝑦 ∈ V)
→ (𝑥(+g‘𝐺)𝑦) ∈ V) |
47 | 40, 44, 45, 46 | syl3anc 1249 |
. . . 4
⊢ ((((𝑆 ∈ (SubMnd‘𝐺) ∧ 𝑊 ∈ Word 𝑆) ∧ 𝑊 ≠ ∅) ∧ (𝑥 ∈ V ∧ 𝑦 ∈ V)) → (𝑥(+g‘𝐺)𝑦) ∈ V) |
48 | 20, 33, 34, 37, 39, 47 | seq3clss 10532 |
. . 3
⊢ (((𝑆 ∈ (SubMnd‘𝐺) ∧ 𝑊 ∈ Word 𝑆) ∧ 𝑊 ≠ ∅) →
(seq0((+g‘𝐺), 𝑊)‘((♯‘𝑊) − 1)) ∈ 𝑆) |
49 | 31, 48 | eqeltrd 2270 |
. 2
⊢ (((𝑆 ∈ (SubMnd‘𝐺) ∧ 𝑊 ∈ Word 𝑆) ∧ 𝑊 ≠ ∅) → (𝐺 Σg 𝑊) ∈ 𝑆) |
50 | | wrdfin 10923 |
. . . . 5
⊢ (𝑊 ∈ Word 𝑆 → 𝑊 ∈ Fin) |
51 | | fin0or 6933 |
. . . . 5
⊢ (𝑊 ∈ Fin → (𝑊 = ∅ ∨ ∃𝑗 𝑗 ∈ 𝑊)) |
52 | 50, 51 | syl 14 |
. . . 4
⊢ (𝑊 ∈ Word 𝑆 → (𝑊 = ∅ ∨ ∃𝑗 𝑗 ∈ 𝑊)) |
53 | | n0r 3460 |
. . . . 5
⊢
(∃𝑗 𝑗 ∈ 𝑊 → 𝑊 ≠ ∅) |
54 | 53 | orim2i 762 |
. . . 4
⊢ ((𝑊 = ∅ ∨ ∃𝑗 𝑗 ∈ 𝑊) → (𝑊 = ∅ ∨ 𝑊 ≠ ∅)) |
55 | 52, 54 | syl 14 |
. . 3
⊢ (𝑊 ∈ Word 𝑆 → (𝑊 = ∅ ∨ 𝑊 ≠ ∅)) |
56 | 55 | adantl 277 |
. 2
⊢ ((𝑆 ∈ (SubMnd‘𝐺) ∧ 𝑊 ∈ Word 𝑆) → (𝑊 = ∅ ∨ 𝑊 ≠ ∅)) |
57 | 11, 49, 56 | mpjaodan 799 |
1
⊢ ((𝑆 ∈ (SubMnd‘𝐺) ∧ 𝑊 ∈ Word 𝑆) → (𝐺 Σg 𝑊) ∈ 𝑆) |