Proof of Theorem gsumccat
Step | Hyp | Ref
| Expression |
1 | | oveq1 7220 |
. . . 4
⊢ (𝑊 = ∅ → (𝑊 ++ 𝑋) = (∅ ++ 𝑋)) |
2 | 1 | oveq2d 7229 |
. . 3
⊢ (𝑊 = ∅ → (𝐺 Σg
(𝑊 ++ 𝑋)) = (𝐺 Σg (∅ ++
𝑋))) |
3 | | oveq2 7221 |
. . . . 5
⊢ (𝑊 = ∅ → (𝐺 Σg
𝑊) = (𝐺 Σg
∅)) |
4 | | eqid 2737 |
. . . . . 6
⊢
(0g‘𝐺) = (0g‘𝐺) |
5 | 4 | gsum0 18156 |
. . . . 5
⊢ (𝐺 Σg
∅) = (0g‘𝐺) |
6 | 3, 5 | eqtrdi 2794 |
. . . 4
⊢ (𝑊 = ∅ → (𝐺 Σg
𝑊) =
(0g‘𝐺)) |
7 | 6 | oveq1d 7228 |
. . 3
⊢ (𝑊 = ∅ → ((𝐺 Σg
𝑊) + (𝐺 Σg 𝑋)) = ((0g‘𝐺) + (𝐺 Σg 𝑋))) |
8 | 2, 7 | eqeq12d 2753 |
. 2
⊢ (𝑊 = ∅ → ((𝐺 Σg
(𝑊 ++ 𝑋)) = ((𝐺 Σg 𝑊) + (𝐺 Σg 𝑋)) ↔ (𝐺 Σg (∅ ++
𝑋)) =
((0g‘𝐺)
+ (𝐺 Σg
𝑋)))) |
9 | | oveq2 7221 |
. . . . 5
⊢ (𝑋 = ∅ → (𝑊 ++ 𝑋) = (𝑊 ++ ∅)) |
10 | 9 | oveq2d 7229 |
. . . 4
⊢ (𝑋 = ∅ → (𝐺 Σg
(𝑊 ++ 𝑋)) = (𝐺 Σg (𝑊 ++ ∅))) |
11 | | oveq2 7221 |
. . . . . 6
⊢ (𝑋 = ∅ → (𝐺 Σg
𝑋) = (𝐺 Σg
∅)) |
12 | 11, 5 | eqtrdi 2794 |
. . . . 5
⊢ (𝑋 = ∅ → (𝐺 Σg
𝑋) =
(0g‘𝐺)) |
13 | 12 | oveq2d 7229 |
. . . 4
⊢ (𝑋 = ∅ → ((𝐺 Σg
𝑊) + (𝐺 Σg 𝑋)) = ((𝐺 Σg 𝑊) + (0g‘𝐺))) |
14 | 10, 13 | eqeq12d 2753 |
. . 3
⊢ (𝑋 = ∅ → ((𝐺 Σg
(𝑊 ++ 𝑋)) = ((𝐺 Σg 𝑊) + (𝐺 Σg 𝑋)) ↔ (𝐺 Σg (𝑊 ++ ∅)) = ((𝐺 Σg
𝑊) + (0g‘𝐺)))) |
15 | | mndsgrp 18179 |
. . . . . 6
⊢ (𝐺 ∈ Mnd → 𝐺 ∈ Smgrp) |
16 | 15 | 3ad2ant1 1135 |
. . . . 5
⊢ ((𝐺 ∈ Mnd ∧ 𝑊 ∈ Word 𝐵 ∧ 𝑋 ∈ Word 𝐵) → 𝐺 ∈ Smgrp) |
17 | 16 | ad2antrr 726 |
. . . 4
⊢ ((((𝐺 ∈ Mnd ∧ 𝑊 ∈ Word 𝐵 ∧ 𝑋 ∈ Word 𝐵) ∧ 𝑊 ≠ ∅) ∧ 𝑋 ≠ ∅) → 𝐺 ∈ Smgrp) |
18 | | 3simpc 1152 |
. . . . 5
⊢ ((𝐺 ∈ Mnd ∧ 𝑊 ∈ Word 𝐵 ∧ 𝑋 ∈ Word 𝐵) → (𝑊 ∈ Word 𝐵 ∧ 𝑋 ∈ Word 𝐵)) |
19 | 18 | ad2antrr 726 |
. . . 4
⊢ ((((𝐺 ∈ Mnd ∧ 𝑊 ∈ Word 𝐵 ∧ 𝑋 ∈ Word 𝐵) ∧ 𝑊 ≠ ∅) ∧ 𝑋 ≠ ∅) → (𝑊 ∈ Word 𝐵 ∧ 𝑋 ∈ Word 𝐵)) |
20 | | simpr 488 |
. . . . 5
⊢ (((𝐺 ∈ Mnd ∧ 𝑊 ∈ Word 𝐵 ∧ 𝑋 ∈ Word 𝐵) ∧ 𝑊 ≠ ∅) → 𝑊 ≠ ∅) |
21 | 20 | anim1i 618 |
. . . 4
⊢ ((((𝐺 ∈ Mnd ∧ 𝑊 ∈ Word 𝐵 ∧ 𝑋 ∈ Word 𝐵) ∧ 𝑊 ≠ ∅) ∧ 𝑋 ≠ ∅) → (𝑊 ≠ ∅ ∧ 𝑋 ≠ ∅)) |
22 | | gsumccat.b |
. . . . 5
⊢ 𝐵 = (Base‘𝐺) |
23 | | gsumccat.p |
. . . . 5
⊢ + =
(+g‘𝐺) |
24 | 22, 23 | gsumsgrpccat 18266 |
. . . 4
⊢ ((𝐺 ∈ Smgrp ∧ (𝑊 ∈ Word 𝐵 ∧ 𝑋 ∈ Word 𝐵) ∧ (𝑊 ≠ ∅ ∧ 𝑋 ≠ ∅)) → (𝐺 Σg (𝑊 ++ 𝑋)) = ((𝐺 Σg 𝑊) + (𝐺 Σg 𝑋))) |
25 | 17, 19, 21, 24 | syl3anc 1373 |
. . 3
⊢ ((((𝐺 ∈ Mnd ∧ 𝑊 ∈ Word 𝐵 ∧ 𝑋 ∈ Word 𝐵) ∧ 𝑊 ≠ ∅) ∧ 𝑋 ≠ ∅) → (𝐺 Σg (𝑊 ++ 𝑋)) = ((𝐺 Σg 𝑊) + (𝐺 Σg 𝑋))) |
26 | | simpl2 1194 |
. . . . . 6
⊢ (((𝐺 ∈ Mnd ∧ 𝑊 ∈ Word 𝐵 ∧ 𝑋 ∈ Word 𝐵) ∧ 𝑊 ≠ ∅) → 𝑊 ∈ Word 𝐵) |
27 | | ccatrid 14144 |
. . . . . 6
⊢ (𝑊 ∈ Word 𝐵 → (𝑊 ++ ∅) = 𝑊) |
28 | 26, 27 | syl 17 |
. . . . 5
⊢ (((𝐺 ∈ Mnd ∧ 𝑊 ∈ Word 𝐵 ∧ 𝑋 ∈ Word 𝐵) ∧ 𝑊 ≠ ∅) → (𝑊 ++ ∅) = 𝑊) |
29 | 28 | oveq2d 7229 |
. . . 4
⊢ (((𝐺 ∈ Mnd ∧ 𝑊 ∈ Word 𝐵 ∧ 𝑋 ∈ Word 𝐵) ∧ 𝑊 ≠ ∅) → (𝐺 Σg (𝑊 ++ ∅)) = (𝐺 Σg
𝑊)) |
30 | | simpl1 1193 |
. . . . 5
⊢ (((𝐺 ∈ Mnd ∧ 𝑊 ∈ Word 𝐵 ∧ 𝑋 ∈ Word 𝐵) ∧ 𝑊 ≠ ∅) → 𝐺 ∈ Mnd) |
31 | 22 | gsumwcl 18265 |
. . . . . . 7
⊢ ((𝐺 ∈ Mnd ∧ 𝑊 ∈ Word 𝐵) → (𝐺 Σg 𝑊) ∈ 𝐵) |
32 | 31 | 3adant3 1134 |
. . . . . 6
⊢ ((𝐺 ∈ Mnd ∧ 𝑊 ∈ Word 𝐵 ∧ 𝑋 ∈ Word 𝐵) → (𝐺 Σg 𝑊) ∈ 𝐵) |
33 | 32 | adantr 484 |
. . . . 5
⊢ (((𝐺 ∈ Mnd ∧ 𝑊 ∈ Word 𝐵 ∧ 𝑋 ∈ Word 𝐵) ∧ 𝑊 ≠ ∅) → (𝐺 Σg 𝑊) ∈ 𝐵) |
34 | 22, 23, 4 | mndrid 18194 |
. . . . 5
⊢ ((𝐺 ∈ Mnd ∧ (𝐺 Σg
𝑊) ∈ 𝐵) → ((𝐺 Σg 𝑊) + (0g‘𝐺)) = (𝐺 Σg 𝑊)) |
35 | 30, 33, 34 | syl2anc 587 |
. . . 4
⊢ (((𝐺 ∈ Mnd ∧ 𝑊 ∈ Word 𝐵 ∧ 𝑋 ∈ Word 𝐵) ∧ 𝑊 ≠ ∅) → ((𝐺 Σg 𝑊) + (0g‘𝐺)) = (𝐺 Σg 𝑊)) |
36 | 29, 35 | eqtr4d 2780 |
. . 3
⊢ (((𝐺 ∈ Mnd ∧ 𝑊 ∈ Word 𝐵 ∧ 𝑋 ∈ Word 𝐵) ∧ 𝑊 ≠ ∅) → (𝐺 Σg (𝑊 ++ ∅)) = ((𝐺 Σg
𝑊) + (0g‘𝐺))) |
37 | 14, 25, 36 | pm2.61ne 3027 |
. 2
⊢ (((𝐺 ∈ Mnd ∧ 𝑊 ∈ Word 𝐵 ∧ 𝑋 ∈ Word 𝐵) ∧ 𝑊 ≠ ∅) → (𝐺 Σg (𝑊 ++ 𝑋)) = ((𝐺 Σg 𝑊) + (𝐺 Σg 𝑋))) |
38 | | ccatlid 14143 |
. . . . 5
⊢ (𝑋 ∈ Word 𝐵 → (∅ ++ 𝑋) = 𝑋) |
39 | 38 | 3ad2ant3 1137 |
. . . 4
⊢ ((𝐺 ∈ Mnd ∧ 𝑊 ∈ Word 𝐵 ∧ 𝑋 ∈ Word 𝐵) → (∅ ++ 𝑋) = 𝑋) |
40 | 39 | oveq2d 7229 |
. . 3
⊢ ((𝐺 ∈ Mnd ∧ 𝑊 ∈ Word 𝐵 ∧ 𝑋 ∈ Word 𝐵) → (𝐺 Σg (∅ ++
𝑋)) = (𝐺 Σg 𝑋)) |
41 | | simp1 1138 |
. . . 4
⊢ ((𝐺 ∈ Mnd ∧ 𝑊 ∈ Word 𝐵 ∧ 𝑋 ∈ Word 𝐵) → 𝐺 ∈ Mnd) |
42 | 22 | gsumwcl 18265 |
. . . 4
⊢ ((𝐺 ∈ Mnd ∧ 𝑋 ∈ Word 𝐵) → (𝐺 Σg 𝑋) ∈ 𝐵) |
43 | 22, 23, 4 | mndlid 18193 |
. . . 4
⊢ ((𝐺 ∈ Mnd ∧ (𝐺 Σg
𝑋) ∈ 𝐵) → ((0g‘𝐺) + (𝐺 Σg 𝑋)) = (𝐺 Σg 𝑋)) |
44 | 41, 42, 43 | 3imp3i2an 1347 |
. . 3
⊢ ((𝐺 ∈ Mnd ∧ 𝑊 ∈ Word 𝐵 ∧ 𝑋 ∈ Word 𝐵) → ((0g‘𝐺) + (𝐺 Σg 𝑋)) = (𝐺 Σg 𝑋)) |
45 | 40, 44 | eqtr4d 2780 |
. 2
⊢ ((𝐺 ∈ Mnd ∧ 𝑊 ∈ Word 𝐵 ∧ 𝑋 ∈ Word 𝐵) → (𝐺 Σg (∅ ++
𝑋)) =
((0g‘𝐺)
+ (𝐺 Σg
𝑋))) |
46 | 8, 37, 45 | pm2.61ne 3027 |
1
⊢ ((𝐺 ∈ Mnd ∧ 𝑊 ∈ Word 𝐵 ∧ 𝑋 ∈ Word 𝐵) → (𝐺 Σg (𝑊 ++ 𝑋)) = ((𝐺 Σg 𝑊) + (𝐺 Σg 𝑋))) |