MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  gsumccat Structured version   Visualization version   GIF version

Theorem gsumccat 17425
Description: Homomorphic property of composites. (Contributed by Stefan O'Rear, 16-Aug-2015.) (Revised by Mario Carneiro, 1-Oct-2015.)
Hypotheses
Ref Expression
gsumwcl.b 𝐵 = (Base‘𝐺)
gsumccat.p + = (+g𝐺)
Assertion
Ref Expression
gsumccat ((𝐺 ∈ Mnd ∧ 𝑊 ∈ Word 𝐵𝑋 ∈ Word 𝐵) → (𝐺 Σg (𝑊 ++ 𝑋)) = ((𝐺 Σg 𝑊) + (𝐺 Σg 𝑋)))

Proof of Theorem gsumccat
Dummy variables 𝑥 𝑦 𝑧 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 oveq1 6697 . . . 4 (𝑊 = ∅ → (𝑊 ++ 𝑋) = (∅ ++ 𝑋))
21oveq2d 6706 . . 3 (𝑊 = ∅ → (𝐺 Σg (𝑊 ++ 𝑋)) = (𝐺 Σg (∅ ++ 𝑋)))
3 oveq2 6698 . . . . 5 (𝑊 = ∅ → (𝐺 Σg 𝑊) = (𝐺 Σg ∅))
4 eqid 2651 . . . . . 6 (0g𝐺) = (0g𝐺)
54gsum0 17325 . . . . 5 (𝐺 Σg ∅) = (0g𝐺)
63, 5syl6eq 2701 . . . 4 (𝑊 = ∅ → (𝐺 Σg 𝑊) = (0g𝐺))
76oveq1d 6705 . . 3 (𝑊 = ∅ → ((𝐺 Σg 𝑊) + (𝐺 Σg 𝑋)) = ((0g𝐺) + (𝐺 Σg 𝑋)))
82, 7eqeq12d 2666 . 2 (𝑊 = ∅ → ((𝐺 Σg (𝑊 ++ 𝑋)) = ((𝐺 Σg 𝑊) + (𝐺 Σg 𝑋)) ↔ (𝐺 Σg (∅ ++ 𝑋)) = ((0g𝐺) + (𝐺 Σg 𝑋))))
9 oveq2 6698 . . . . 5 (𝑋 = ∅ → (𝑊 ++ 𝑋) = (𝑊 ++ ∅))
109oveq2d 6706 . . . 4 (𝑋 = ∅ → (𝐺 Σg (𝑊 ++ 𝑋)) = (𝐺 Σg (𝑊 ++ ∅)))
11 oveq2 6698 . . . . . 6 (𝑋 = ∅ → (𝐺 Σg 𝑋) = (𝐺 Σg ∅))
1211, 5syl6eq 2701 . . . . 5 (𝑋 = ∅ → (𝐺 Σg 𝑋) = (0g𝐺))
1312oveq2d 6706 . . . 4 (𝑋 = ∅ → ((𝐺 Σg 𝑊) + (𝐺 Σg 𝑋)) = ((𝐺 Σg 𝑊) + (0g𝐺)))
1410, 13eqeq12d 2666 . . 3 (𝑋 = ∅ → ((𝐺 Σg (𝑊 ++ 𝑋)) = ((𝐺 Σg 𝑊) + (𝐺 Σg 𝑋)) ↔ (𝐺 Σg (𝑊 ++ ∅)) = ((𝐺 Σg 𝑊) + (0g𝐺))))
15 gsumwcl.b . . . . . 6 𝐵 = (Base‘𝐺)
16 gsumccat.p . . . . . 6 + = (+g𝐺)
17 simpl1 1084 . . . . . 6 (((𝐺 ∈ Mnd ∧ 𝑊 ∈ Word 𝐵𝑋 ∈ Word 𝐵) ∧ (𝑊 ≠ ∅ ∧ 𝑋 ≠ ∅)) → 𝐺 ∈ Mnd)
18 lennncl 13357 . . . . . . . . . . 11 ((𝑊 ∈ Word 𝐵𝑊 ≠ ∅) → (#‘𝑊) ∈ ℕ)
19183ad2antl2 1244 . . . . . . . . . 10 (((𝐺 ∈ Mnd ∧ 𝑊 ∈ Word 𝐵𝑋 ∈ Word 𝐵) ∧ 𝑊 ≠ ∅) → (#‘𝑊) ∈ ℕ)
2019adantrr 753 . . . . . . . . 9 (((𝐺 ∈ Mnd ∧ 𝑊 ∈ Word 𝐵𝑋 ∈ Word 𝐵) ∧ (𝑊 ≠ ∅ ∧ 𝑋 ≠ ∅)) → (#‘𝑊) ∈ ℕ)
21 lennncl 13357 . . . . . . . . . . 11 ((𝑋 ∈ Word 𝐵𝑋 ≠ ∅) → (#‘𝑋) ∈ ℕ)
22213ad2antl3 1245 . . . . . . . . . 10 (((𝐺 ∈ Mnd ∧ 𝑊 ∈ Word 𝐵𝑋 ∈ Word 𝐵) ∧ 𝑋 ≠ ∅) → (#‘𝑋) ∈ ℕ)
2322adantrl 752 . . . . . . . . 9 (((𝐺 ∈ Mnd ∧ 𝑊 ∈ Word 𝐵𝑋 ∈ Word 𝐵) ∧ (𝑊 ≠ ∅ ∧ 𝑋 ≠ ∅)) → (#‘𝑋) ∈ ℕ)
2420, 23nnaddcld 11105 . . . . . . . 8 (((𝐺 ∈ Mnd ∧ 𝑊 ∈ Word 𝐵𝑋 ∈ Word 𝐵) ∧ (𝑊 ≠ ∅ ∧ 𝑋 ≠ ∅)) → ((#‘𝑊) + (#‘𝑋)) ∈ ℕ)
25 nnm1nn0 11372 . . . . . . . 8 (((#‘𝑊) + (#‘𝑋)) ∈ ℕ → (((#‘𝑊) + (#‘𝑋)) − 1) ∈ ℕ0)
2624, 25syl 17 . . . . . . 7 (((𝐺 ∈ Mnd ∧ 𝑊 ∈ Word 𝐵𝑋 ∈ Word 𝐵) ∧ (𝑊 ≠ ∅ ∧ 𝑋 ≠ ∅)) → (((#‘𝑊) + (#‘𝑋)) − 1) ∈ ℕ0)
27 nn0uz 11760 . . . . . . 7 0 = (ℤ‘0)
2826, 27syl6eleq 2740 . . . . . 6 (((𝐺 ∈ Mnd ∧ 𝑊 ∈ Word 𝐵𝑋 ∈ Word 𝐵) ∧ (𝑊 ≠ ∅ ∧ 𝑋 ≠ ∅)) → (((#‘𝑊) + (#‘𝑋)) − 1) ∈ (ℤ‘0))
29 simpl2 1085 . . . . . . . . 9 (((𝐺 ∈ Mnd ∧ 𝑊 ∈ Word 𝐵𝑋 ∈ Word 𝐵) ∧ (𝑊 ≠ ∅ ∧ 𝑋 ≠ ∅)) → 𝑊 ∈ Word 𝐵)
30 simpl3 1086 . . . . . . . . 9 (((𝐺 ∈ Mnd ∧ 𝑊 ∈ Word 𝐵𝑋 ∈ Word 𝐵) ∧ (𝑊 ≠ ∅ ∧ 𝑋 ≠ ∅)) → 𝑋 ∈ Word 𝐵)
31 ccatcl 13392 . . . . . . . . 9 ((𝑊 ∈ Word 𝐵𝑋 ∈ Word 𝐵) → (𝑊 ++ 𝑋) ∈ Word 𝐵)
3229, 30, 31syl2anc 694 . . . . . . . 8 (((𝐺 ∈ Mnd ∧ 𝑊 ∈ Word 𝐵𝑋 ∈ Word 𝐵) ∧ (𝑊 ≠ ∅ ∧ 𝑋 ≠ ∅)) → (𝑊 ++ 𝑋) ∈ Word 𝐵)
33 wrdf 13342 . . . . . . . 8 ((𝑊 ++ 𝑋) ∈ Word 𝐵 → (𝑊 ++ 𝑋):(0..^(#‘(𝑊 ++ 𝑋)))⟶𝐵)
3432, 33syl 17 . . . . . . 7 (((𝐺 ∈ Mnd ∧ 𝑊 ∈ Word 𝐵𝑋 ∈ Word 𝐵) ∧ (𝑊 ≠ ∅ ∧ 𝑋 ≠ ∅)) → (𝑊 ++ 𝑋):(0..^(#‘(𝑊 ++ 𝑋)))⟶𝐵)
35 ccatlen 13393 . . . . . . . . . . 11 ((𝑊 ∈ Word 𝐵𝑋 ∈ Word 𝐵) → (#‘(𝑊 ++ 𝑋)) = ((#‘𝑊) + (#‘𝑋)))
3629, 30, 35syl2anc 694 . . . . . . . . . 10 (((𝐺 ∈ Mnd ∧ 𝑊 ∈ Word 𝐵𝑋 ∈ Word 𝐵) ∧ (𝑊 ≠ ∅ ∧ 𝑋 ≠ ∅)) → (#‘(𝑊 ++ 𝑋)) = ((#‘𝑊) + (#‘𝑋)))
3736oveq2d 6706 . . . . . . . . 9 (((𝐺 ∈ Mnd ∧ 𝑊 ∈ Word 𝐵𝑋 ∈ Word 𝐵) ∧ (𝑊 ≠ ∅ ∧ 𝑋 ≠ ∅)) → (0..^(#‘(𝑊 ++ 𝑋))) = (0..^((#‘𝑊) + (#‘𝑋))))
3820nnzd 11519 . . . . . . . . . . 11 (((𝐺 ∈ Mnd ∧ 𝑊 ∈ Word 𝐵𝑋 ∈ Word 𝐵) ∧ (𝑊 ≠ ∅ ∧ 𝑋 ≠ ∅)) → (#‘𝑊) ∈ ℤ)
3923nnzd 11519 . . . . . . . . . . 11 (((𝐺 ∈ Mnd ∧ 𝑊 ∈ Word 𝐵𝑋 ∈ Word 𝐵) ∧ (𝑊 ≠ ∅ ∧ 𝑋 ≠ ∅)) → (#‘𝑋) ∈ ℤ)
4038, 39zaddcld 11524 . . . . . . . . . 10 (((𝐺 ∈ Mnd ∧ 𝑊 ∈ Word 𝐵𝑋 ∈ Word 𝐵) ∧ (𝑊 ≠ ∅ ∧ 𝑋 ≠ ∅)) → ((#‘𝑊) + (#‘𝑋)) ∈ ℤ)
41 fzoval 12510 . . . . . . . . . 10 (((#‘𝑊) + (#‘𝑋)) ∈ ℤ → (0..^((#‘𝑊) + (#‘𝑋))) = (0...(((#‘𝑊) + (#‘𝑋)) − 1)))
4240, 41syl 17 . . . . . . . . 9 (((𝐺 ∈ Mnd ∧ 𝑊 ∈ Word 𝐵𝑋 ∈ Word 𝐵) ∧ (𝑊 ≠ ∅ ∧ 𝑋 ≠ ∅)) → (0..^((#‘𝑊) + (#‘𝑋))) = (0...(((#‘𝑊) + (#‘𝑋)) − 1)))
4337, 42eqtrd 2685 . . . . . . . 8 (((𝐺 ∈ Mnd ∧ 𝑊 ∈ Word 𝐵𝑋 ∈ Word 𝐵) ∧ (𝑊 ≠ ∅ ∧ 𝑋 ≠ ∅)) → (0..^(#‘(𝑊 ++ 𝑋))) = (0...(((#‘𝑊) + (#‘𝑋)) − 1)))
4443feq2d 6069 . . . . . . 7 (((𝐺 ∈ Mnd ∧ 𝑊 ∈ Word 𝐵𝑋 ∈ Word 𝐵) ∧ (𝑊 ≠ ∅ ∧ 𝑋 ≠ ∅)) → ((𝑊 ++ 𝑋):(0..^(#‘(𝑊 ++ 𝑋)))⟶𝐵 ↔ (𝑊 ++ 𝑋):(0...(((#‘𝑊) + (#‘𝑋)) − 1))⟶𝐵))
4534, 44mpbid 222 . . . . . 6 (((𝐺 ∈ Mnd ∧ 𝑊 ∈ Word 𝐵𝑋 ∈ Word 𝐵) ∧ (𝑊 ≠ ∅ ∧ 𝑋 ≠ ∅)) → (𝑊 ++ 𝑋):(0...(((#‘𝑊) + (#‘𝑋)) − 1))⟶𝐵)
4615, 16, 17, 28, 45gsumval2 17327 . . . . 5 (((𝐺 ∈ Mnd ∧ 𝑊 ∈ Word 𝐵𝑋 ∈ Word 𝐵) ∧ (𝑊 ≠ ∅ ∧ 𝑋 ≠ ∅)) → (𝐺 Σg (𝑊 ++ 𝑋)) = (seq0( + , (𝑊 ++ 𝑋))‘(((#‘𝑊) + (#‘𝑋)) − 1)))
47 nnm1nn0 11372 . . . . . . . . . 10 ((#‘𝑊) ∈ ℕ → ((#‘𝑊) − 1) ∈ ℕ0)
4820, 47syl 17 . . . . . . . . 9 (((𝐺 ∈ Mnd ∧ 𝑊 ∈ Word 𝐵𝑋 ∈ Word 𝐵) ∧ (𝑊 ≠ ∅ ∧ 𝑋 ≠ ∅)) → ((#‘𝑊) − 1) ∈ ℕ0)
4948, 27syl6eleq 2740 . . . . . . . 8 (((𝐺 ∈ Mnd ∧ 𝑊 ∈ Word 𝐵𝑋 ∈ Word 𝐵) ∧ (𝑊 ≠ ∅ ∧ 𝑋 ≠ ∅)) → ((#‘𝑊) − 1) ∈ (ℤ‘0))
50 wrdf 13342 . . . . . . . . . 10 (𝑊 ∈ Word 𝐵𝑊:(0..^(#‘𝑊))⟶𝐵)
5129, 50syl 17 . . . . . . . . 9 (((𝐺 ∈ Mnd ∧ 𝑊 ∈ Word 𝐵𝑋 ∈ Word 𝐵) ∧ (𝑊 ≠ ∅ ∧ 𝑋 ≠ ∅)) → 𝑊:(0..^(#‘𝑊))⟶𝐵)
52 fzoval 12510 . . . . . . . . . . 11 ((#‘𝑊) ∈ ℤ → (0..^(#‘𝑊)) = (0...((#‘𝑊) − 1)))
5338, 52syl 17 . . . . . . . . . 10 (((𝐺 ∈ Mnd ∧ 𝑊 ∈ Word 𝐵𝑋 ∈ Word 𝐵) ∧ (𝑊 ≠ ∅ ∧ 𝑋 ≠ ∅)) → (0..^(#‘𝑊)) = (0...((#‘𝑊) − 1)))
5453feq2d 6069 . . . . . . . . 9 (((𝐺 ∈ Mnd ∧ 𝑊 ∈ Word 𝐵𝑋 ∈ Word 𝐵) ∧ (𝑊 ≠ ∅ ∧ 𝑋 ≠ ∅)) → (𝑊:(0..^(#‘𝑊))⟶𝐵𝑊:(0...((#‘𝑊) − 1))⟶𝐵))
5551, 54mpbid 222 . . . . . . . 8 (((𝐺 ∈ Mnd ∧ 𝑊 ∈ Word 𝐵𝑋 ∈ Word 𝐵) ∧ (𝑊 ≠ ∅ ∧ 𝑋 ≠ ∅)) → 𝑊:(0...((#‘𝑊) − 1))⟶𝐵)
5615, 16, 17, 49, 55gsumval2 17327 . . . . . . 7 (((𝐺 ∈ Mnd ∧ 𝑊 ∈ Word 𝐵𝑋 ∈ Word 𝐵) ∧ (𝑊 ≠ ∅ ∧ 𝑋 ≠ ∅)) → (𝐺 Σg 𝑊) = (seq0( + , 𝑊)‘((#‘𝑊) − 1)))
57 nnm1nn0 11372 . . . . . . . . . 10 ((#‘𝑋) ∈ ℕ → ((#‘𝑋) − 1) ∈ ℕ0)
5823, 57syl 17 . . . . . . . . 9 (((𝐺 ∈ Mnd ∧ 𝑊 ∈ Word 𝐵𝑋 ∈ Word 𝐵) ∧ (𝑊 ≠ ∅ ∧ 𝑋 ≠ ∅)) → ((#‘𝑋) − 1) ∈ ℕ0)
5958, 27syl6eleq 2740 . . . . . . . 8 (((𝐺 ∈ Mnd ∧ 𝑊 ∈ Word 𝐵𝑋 ∈ Word 𝐵) ∧ (𝑊 ≠ ∅ ∧ 𝑋 ≠ ∅)) → ((#‘𝑋) − 1) ∈ (ℤ‘0))
60 wrdf 13342 . . . . . . . . . 10 (𝑋 ∈ Word 𝐵𝑋:(0..^(#‘𝑋))⟶𝐵)
6130, 60syl 17 . . . . . . . . 9 (((𝐺 ∈ Mnd ∧ 𝑊 ∈ Word 𝐵𝑋 ∈ Word 𝐵) ∧ (𝑊 ≠ ∅ ∧ 𝑋 ≠ ∅)) → 𝑋:(0..^(#‘𝑋))⟶𝐵)
62 fzoval 12510 . . . . . . . . . . 11 ((#‘𝑋) ∈ ℤ → (0..^(#‘𝑋)) = (0...((#‘𝑋) − 1)))
6339, 62syl 17 . . . . . . . . . 10 (((𝐺 ∈ Mnd ∧ 𝑊 ∈ Word 𝐵𝑋 ∈ Word 𝐵) ∧ (𝑊 ≠ ∅ ∧ 𝑋 ≠ ∅)) → (0..^(#‘𝑋)) = (0...((#‘𝑋) − 1)))
6463feq2d 6069 . . . . . . . . 9 (((𝐺 ∈ Mnd ∧ 𝑊 ∈ Word 𝐵𝑋 ∈ Word 𝐵) ∧ (𝑊 ≠ ∅ ∧ 𝑋 ≠ ∅)) → (𝑋:(0..^(#‘𝑋))⟶𝐵𝑋:(0...((#‘𝑋) − 1))⟶𝐵))
6561, 64mpbid 222 . . . . . . . 8 (((𝐺 ∈ Mnd ∧ 𝑊 ∈ Word 𝐵𝑋 ∈ Word 𝐵) ∧ (𝑊 ≠ ∅ ∧ 𝑋 ≠ ∅)) → 𝑋:(0...((#‘𝑋) − 1))⟶𝐵)
6615, 16, 17, 59, 65gsumval2 17327 . . . . . . 7 (((𝐺 ∈ Mnd ∧ 𝑊 ∈ Word 𝐵𝑋 ∈ Word 𝐵) ∧ (𝑊 ≠ ∅ ∧ 𝑋 ≠ ∅)) → (𝐺 Σg 𝑋) = (seq0( + , 𝑋)‘((#‘𝑋) − 1)))
6756, 66oveq12d 6708 . . . . . 6 (((𝐺 ∈ Mnd ∧ 𝑊 ∈ Word 𝐵𝑋 ∈ Word 𝐵) ∧ (𝑊 ≠ ∅ ∧ 𝑋 ≠ ∅)) → ((𝐺 Σg 𝑊) + (𝐺 Σg 𝑋)) = ((seq0( + , 𝑊)‘((#‘𝑊) − 1)) + (seq0( + , 𝑋)‘((#‘𝑋) − 1))))
6815, 16mndcl 17348 . . . . . . . . . 10 ((𝐺 ∈ Mnd ∧ 𝑥𝐵𝑦𝐵) → (𝑥 + 𝑦) ∈ 𝐵)
69683expb 1285 . . . . . . . . 9 ((𝐺 ∈ Mnd ∧ (𝑥𝐵𝑦𝐵)) → (𝑥 + 𝑦) ∈ 𝐵)
7017, 69sylan 487 . . . . . . . 8 ((((𝐺 ∈ Mnd ∧ 𝑊 ∈ Word 𝐵𝑋 ∈ Word 𝐵) ∧ (𝑊 ≠ ∅ ∧ 𝑋 ≠ ∅)) ∧ (𝑥𝐵𝑦𝐵)) → (𝑥 + 𝑦) ∈ 𝐵)
7115, 16mndass 17349 . . . . . . . . 9 ((𝐺 ∈ Mnd ∧ (𝑥𝐵𝑦𝐵𝑧𝐵)) → ((𝑥 + 𝑦) + 𝑧) = (𝑥 + (𝑦 + 𝑧)))
7217, 71sylan 487 . . . . . . . 8 ((((𝐺 ∈ Mnd ∧ 𝑊 ∈ Word 𝐵𝑋 ∈ Word 𝐵) ∧ (𝑊 ≠ ∅ ∧ 𝑋 ≠ ∅)) ∧ (𝑥𝐵𝑦𝐵𝑧𝐵)) → ((𝑥 + 𝑦) + 𝑧) = (𝑥 + (𝑦 + 𝑧)))
73 uzid 11740 . . . . . . . . . . 11 ((#‘𝑊) ∈ ℤ → (#‘𝑊) ∈ (ℤ‘(#‘𝑊)))
7438, 73syl 17 . . . . . . . . . 10 (((𝐺 ∈ Mnd ∧ 𝑊 ∈ Word 𝐵𝑋 ∈ Word 𝐵) ∧ (𝑊 ≠ ∅ ∧ 𝑋 ≠ ∅)) → (#‘𝑊) ∈ (ℤ‘(#‘𝑊)))
75 uzaddcl 11782 . . . . . . . . . 10 (((#‘𝑊) ∈ (ℤ‘(#‘𝑊)) ∧ ((#‘𝑋) − 1) ∈ ℕ0) → ((#‘𝑊) + ((#‘𝑋) − 1)) ∈ (ℤ‘(#‘𝑊)))
7674, 58, 75syl2anc 694 . . . . . . . . 9 (((𝐺 ∈ Mnd ∧ 𝑊 ∈ Word 𝐵𝑋 ∈ Word 𝐵) ∧ (𝑊 ≠ ∅ ∧ 𝑋 ≠ ∅)) → ((#‘𝑊) + ((#‘𝑋) − 1)) ∈ (ℤ‘(#‘𝑊)))
7720nncnd 11074 . . . . . . . . . 10 (((𝐺 ∈ Mnd ∧ 𝑊 ∈ Word 𝐵𝑋 ∈ Word 𝐵) ∧ (𝑊 ≠ ∅ ∧ 𝑋 ≠ ∅)) → (#‘𝑊) ∈ ℂ)
7823nncnd 11074 . . . . . . . . . 10 (((𝐺 ∈ Mnd ∧ 𝑊 ∈ Word 𝐵𝑋 ∈ Word 𝐵) ∧ (𝑊 ≠ ∅ ∧ 𝑋 ≠ ∅)) → (#‘𝑋) ∈ ℂ)
79 1cnd 10094 . . . . . . . . . 10 (((𝐺 ∈ Mnd ∧ 𝑊 ∈ Word 𝐵𝑋 ∈ Word 𝐵) ∧ (𝑊 ≠ ∅ ∧ 𝑋 ≠ ∅)) → 1 ∈ ℂ)
8077, 78, 79addsubassd 10450 . . . . . . . . 9 (((𝐺 ∈ Mnd ∧ 𝑊 ∈ Word 𝐵𝑋 ∈ Word 𝐵) ∧ (𝑊 ≠ ∅ ∧ 𝑋 ≠ ∅)) → (((#‘𝑊) + (#‘𝑋)) − 1) = ((#‘𝑊) + ((#‘𝑋) − 1)))
81 ax-1cn 10032 . . . . . . . . . . 11 1 ∈ ℂ
82 npcan 10328 . . . . . . . . . . 11 (((#‘𝑊) ∈ ℂ ∧ 1 ∈ ℂ) → (((#‘𝑊) − 1) + 1) = (#‘𝑊))
8377, 81, 82sylancl 695 . . . . . . . . . 10 (((𝐺 ∈ Mnd ∧ 𝑊 ∈ Word 𝐵𝑋 ∈ Word 𝐵) ∧ (𝑊 ≠ ∅ ∧ 𝑋 ≠ ∅)) → (((#‘𝑊) − 1) + 1) = (#‘𝑊))
8483fveq2d 6233 . . . . . . . . 9 (((𝐺 ∈ Mnd ∧ 𝑊 ∈ Word 𝐵𝑋 ∈ Word 𝐵) ∧ (𝑊 ≠ ∅ ∧ 𝑋 ≠ ∅)) → (ℤ‘(((#‘𝑊) − 1) + 1)) = (ℤ‘(#‘𝑊)))
8576, 80, 843eltr4d 2745 . . . . . . . 8 (((𝐺 ∈ Mnd ∧ 𝑊 ∈ Word 𝐵𝑋 ∈ Word 𝐵) ∧ (𝑊 ≠ ∅ ∧ 𝑋 ≠ ∅)) → (((#‘𝑊) + (#‘𝑋)) − 1) ∈ (ℤ‘(((#‘𝑊) − 1) + 1)))
8645ffvelrnda 6399 . . . . . . . 8 ((((𝐺 ∈ Mnd ∧ 𝑊 ∈ Word 𝐵𝑋 ∈ Word 𝐵) ∧ (𝑊 ≠ ∅ ∧ 𝑋 ≠ ∅)) ∧ 𝑥 ∈ (0...(((#‘𝑊) + (#‘𝑋)) − 1))) → ((𝑊 ++ 𝑋)‘𝑥) ∈ 𝐵)
8770, 72, 85, 49, 86seqsplit 12874 . . . . . . 7 (((𝐺 ∈ Mnd ∧ 𝑊 ∈ Word 𝐵𝑋 ∈ Word 𝐵) ∧ (𝑊 ≠ ∅ ∧ 𝑋 ≠ ∅)) → (seq0( + , (𝑊 ++ 𝑋))‘(((#‘𝑊) + (#‘𝑋)) − 1)) = ((seq0( + , (𝑊 ++ 𝑋))‘((#‘𝑊) − 1)) + (seq(((#‘𝑊) − 1) + 1)( + , (𝑊 ++ 𝑋))‘(((#‘𝑊) + (#‘𝑋)) − 1))))
88 simpll2 1121 . . . . . . . . . 10 ((((𝐺 ∈ Mnd ∧ 𝑊 ∈ Word 𝐵𝑋 ∈ Word 𝐵) ∧ (𝑊 ≠ ∅ ∧ 𝑋 ≠ ∅)) ∧ 𝑥 ∈ (0...((#‘𝑊) − 1))) → 𝑊 ∈ Word 𝐵)
89 simpll3 1122 . . . . . . . . . 10 ((((𝐺 ∈ Mnd ∧ 𝑊 ∈ Word 𝐵𝑋 ∈ Word 𝐵) ∧ (𝑊 ≠ ∅ ∧ 𝑋 ≠ ∅)) ∧ 𝑥 ∈ (0...((#‘𝑊) − 1))) → 𝑋 ∈ Word 𝐵)
9053eleq2d 2716 . . . . . . . . . . 11 (((𝐺 ∈ Mnd ∧ 𝑊 ∈ Word 𝐵𝑋 ∈ Word 𝐵) ∧ (𝑊 ≠ ∅ ∧ 𝑋 ≠ ∅)) → (𝑥 ∈ (0..^(#‘𝑊)) ↔ 𝑥 ∈ (0...((#‘𝑊) − 1))))
9190biimpar 501 . . . . . . . . . 10 ((((𝐺 ∈ Mnd ∧ 𝑊 ∈ Word 𝐵𝑋 ∈ Word 𝐵) ∧ (𝑊 ≠ ∅ ∧ 𝑋 ≠ ∅)) ∧ 𝑥 ∈ (0...((#‘𝑊) − 1))) → 𝑥 ∈ (0..^(#‘𝑊)))
92 ccatval1 13395 . . . . . . . . . 10 ((𝑊 ∈ Word 𝐵𝑋 ∈ Word 𝐵𝑥 ∈ (0..^(#‘𝑊))) → ((𝑊 ++ 𝑋)‘𝑥) = (𝑊𝑥))
9388, 89, 91, 92syl3anc 1366 . . . . . . . . 9 ((((𝐺 ∈ Mnd ∧ 𝑊 ∈ Word 𝐵𝑋 ∈ Word 𝐵) ∧ (𝑊 ≠ ∅ ∧ 𝑋 ≠ ∅)) ∧ 𝑥 ∈ (0...((#‘𝑊) − 1))) → ((𝑊 ++ 𝑋)‘𝑥) = (𝑊𝑥))
9449, 93seqfveq 12865 . . . . . . . 8 (((𝐺 ∈ Mnd ∧ 𝑊 ∈ Word 𝐵𝑋 ∈ Word 𝐵) ∧ (𝑊 ≠ ∅ ∧ 𝑋 ≠ ∅)) → (seq0( + , (𝑊 ++ 𝑋))‘((#‘𝑊) − 1)) = (seq0( + , 𝑊)‘((#‘𝑊) − 1)))
9577addid2d 10275 . . . . . . . . . . . 12 (((𝐺 ∈ Mnd ∧ 𝑊 ∈ Word 𝐵𝑋 ∈ Word 𝐵) ∧ (𝑊 ≠ ∅ ∧ 𝑋 ≠ ∅)) → (0 + (#‘𝑊)) = (#‘𝑊))
9683, 95eqtr4d 2688 . . . . . . . . . . 11 (((𝐺 ∈ Mnd ∧ 𝑊 ∈ Word 𝐵𝑋 ∈ Word 𝐵) ∧ (𝑊 ≠ ∅ ∧ 𝑋 ≠ ∅)) → (((#‘𝑊) − 1) + 1) = (0 + (#‘𝑊)))
9796seqeq1d 12847 . . . . . . . . . 10 (((𝐺 ∈ Mnd ∧ 𝑊 ∈ Word 𝐵𝑋 ∈ Word 𝐵) ∧ (𝑊 ≠ ∅ ∧ 𝑋 ≠ ∅)) → seq(((#‘𝑊) − 1) + 1)( + , (𝑊 ++ 𝑋)) = seq(0 + (#‘𝑊))( + , (𝑊 ++ 𝑋)))
9877, 78addcomd 10276 . . . . . . . . . . . 12 (((𝐺 ∈ Mnd ∧ 𝑊 ∈ Word 𝐵𝑋 ∈ Word 𝐵) ∧ (𝑊 ≠ ∅ ∧ 𝑋 ≠ ∅)) → ((#‘𝑊) + (#‘𝑋)) = ((#‘𝑋) + (#‘𝑊)))
9998oveq1d 6705 . . . . . . . . . . 11 (((𝐺 ∈ Mnd ∧ 𝑊 ∈ Word 𝐵𝑋 ∈ Word 𝐵) ∧ (𝑊 ≠ ∅ ∧ 𝑋 ≠ ∅)) → (((#‘𝑊) + (#‘𝑋)) − 1) = (((#‘𝑋) + (#‘𝑊)) − 1))
10078, 77, 79addsubd 10451 . . . . . . . . . . 11 (((𝐺 ∈ Mnd ∧ 𝑊 ∈ Word 𝐵𝑋 ∈ Word 𝐵) ∧ (𝑊 ≠ ∅ ∧ 𝑋 ≠ ∅)) → (((#‘𝑋) + (#‘𝑊)) − 1) = (((#‘𝑋) − 1) + (#‘𝑊)))
10199, 100eqtrd 2685 . . . . . . . . . 10 (((𝐺 ∈ Mnd ∧ 𝑊 ∈ Word 𝐵𝑋 ∈ Word 𝐵) ∧ (𝑊 ≠ ∅ ∧ 𝑋 ≠ ∅)) → (((#‘𝑊) + (#‘𝑋)) − 1) = (((#‘𝑋) − 1) + (#‘𝑊)))
10297, 101fveq12d 6235 . . . . . . . . 9 (((𝐺 ∈ Mnd ∧ 𝑊 ∈ Word 𝐵𝑋 ∈ Word 𝐵) ∧ (𝑊 ≠ ∅ ∧ 𝑋 ≠ ∅)) → (seq(((#‘𝑊) − 1) + 1)( + , (𝑊 ++ 𝑋))‘(((#‘𝑊) + (#‘𝑋)) − 1)) = (seq(0 + (#‘𝑊))( + , (𝑊 ++ 𝑋))‘(((#‘𝑋) − 1) + (#‘𝑊))))
103 simpll2 1121 . . . . . . . . . . . 12 ((((𝐺 ∈ Mnd ∧ 𝑊 ∈ Word 𝐵𝑋 ∈ Word 𝐵) ∧ (𝑊 ≠ ∅ ∧ 𝑋 ≠ ∅)) ∧ 𝑥 ∈ (0...((#‘𝑋) − 1))) → 𝑊 ∈ Word 𝐵)
104 simpll3 1122 . . . . . . . . . . . 12 ((((𝐺 ∈ Mnd ∧ 𝑊 ∈ Word 𝐵𝑋 ∈ Word 𝐵) ∧ (𝑊 ≠ ∅ ∧ 𝑋 ≠ ∅)) ∧ 𝑥 ∈ (0...((#‘𝑋) − 1))) → 𝑋 ∈ Word 𝐵)
10563eleq2d 2716 . . . . . . . . . . . . 13 (((𝐺 ∈ Mnd ∧ 𝑊 ∈ Word 𝐵𝑋 ∈ Word 𝐵) ∧ (𝑊 ≠ ∅ ∧ 𝑋 ≠ ∅)) → (𝑥 ∈ (0..^(#‘𝑋)) ↔ 𝑥 ∈ (0...((#‘𝑋) − 1))))
106105biimpar 501 . . . . . . . . . . . 12 ((((𝐺 ∈ Mnd ∧ 𝑊 ∈ Word 𝐵𝑋 ∈ Word 𝐵) ∧ (𝑊 ≠ ∅ ∧ 𝑋 ≠ ∅)) ∧ 𝑥 ∈ (0...((#‘𝑋) − 1))) → 𝑥 ∈ (0..^(#‘𝑋)))
107 ccatval3 13397 . . . . . . . . . . . 12 ((𝑊 ∈ Word 𝐵𝑋 ∈ Word 𝐵𝑥 ∈ (0..^(#‘𝑋))) → ((𝑊 ++ 𝑋)‘(𝑥 + (#‘𝑊))) = (𝑋𝑥))
108103, 104, 106, 107syl3anc 1366 . . . . . . . . . . 11 ((((𝐺 ∈ Mnd ∧ 𝑊 ∈ Word 𝐵𝑋 ∈ Word 𝐵) ∧ (𝑊 ≠ ∅ ∧ 𝑋 ≠ ∅)) ∧ 𝑥 ∈ (0...((#‘𝑋) − 1))) → ((𝑊 ++ 𝑋)‘(𝑥 + (#‘𝑊))) = (𝑋𝑥))
109108eqcomd 2657 . . . . . . . . . 10 ((((𝐺 ∈ Mnd ∧ 𝑊 ∈ Word 𝐵𝑋 ∈ Word 𝐵) ∧ (𝑊 ≠ ∅ ∧ 𝑋 ≠ ∅)) ∧ 𝑥 ∈ (0...((#‘𝑋) − 1))) → (𝑋𝑥) = ((𝑊 ++ 𝑋)‘(𝑥 + (#‘𝑊))))
11059, 38, 109seqshft2 12867 . . . . . . . . 9 (((𝐺 ∈ Mnd ∧ 𝑊 ∈ Word 𝐵𝑋 ∈ Word 𝐵) ∧ (𝑊 ≠ ∅ ∧ 𝑋 ≠ ∅)) → (seq0( + , 𝑋)‘((#‘𝑋) − 1)) = (seq(0 + (#‘𝑊))( + , (𝑊 ++ 𝑋))‘(((#‘𝑋) − 1) + (#‘𝑊))))
111102, 110eqtr4d 2688 . . . . . . . 8 (((𝐺 ∈ Mnd ∧ 𝑊 ∈ Word 𝐵𝑋 ∈ Word 𝐵) ∧ (𝑊 ≠ ∅ ∧ 𝑋 ≠ ∅)) → (seq(((#‘𝑊) − 1) + 1)( + , (𝑊 ++ 𝑋))‘(((#‘𝑊) + (#‘𝑋)) − 1)) = (seq0( + , 𝑋)‘((#‘𝑋) − 1)))
11294, 111oveq12d 6708 . . . . . . 7 (((𝐺 ∈ Mnd ∧ 𝑊 ∈ Word 𝐵𝑋 ∈ Word 𝐵) ∧ (𝑊 ≠ ∅ ∧ 𝑋 ≠ ∅)) → ((seq0( + , (𝑊 ++ 𝑋))‘((#‘𝑊) − 1)) + (seq(((#‘𝑊) − 1) + 1)( + , (𝑊 ++ 𝑋))‘(((#‘𝑊) + (#‘𝑋)) − 1))) = ((seq0( + , 𝑊)‘((#‘𝑊) − 1)) + (seq0( + , 𝑋)‘((#‘𝑋) − 1))))
11387, 112eqtrd 2685 . . . . . 6 (((𝐺 ∈ Mnd ∧ 𝑊 ∈ Word 𝐵𝑋 ∈ Word 𝐵) ∧ (𝑊 ≠ ∅ ∧ 𝑋 ≠ ∅)) → (seq0( + , (𝑊 ++ 𝑋))‘(((#‘𝑊) + (#‘𝑋)) − 1)) = ((seq0( + , 𝑊)‘((#‘𝑊) − 1)) + (seq0( + , 𝑋)‘((#‘𝑋) − 1))))
11467, 113eqtr4d 2688 . . . . 5 (((𝐺 ∈ Mnd ∧ 𝑊 ∈ Word 𝐵𝑋 ∈ Word 𝐵) ∧ (𝑊 ≠ ∅ ∧ 𝑋 ≠ ∅)) → ((𝐺 Σg 𝑊) + (𝐺 Σg 𝑋)) = (seq0( + , (𝑊 ++ 𝑋))‘(((#‘𝑊) + (#‘𝑋)) − 1)))
11546, 114eqtr4d 2688 . . . 4 (((𝐺 ∈ Mnd ∧ 𝑊 ∈ Word 𝐵𝑋 ∈ Word 𝐵) ∧ (𝑊 ≠ ∅ ∧ 𝑋 ≠ ∅)) → (𝐺 Σg (𝑊 ++ 𝑋)) = ((𝐺 Σg 𝑊) + (𝐺 Σg 𝑋)))
116115anassrs 681 . . 3 ((((𝐺 ∈ Mnd ∧ 𝑊 ∈ Word 𝐵𝑋 ∈ Word 𝐵) ∧ 𝑊 ≠ ∅) ∧ 𝑋 ≠ ∅) → (𝐺 Σg (𝑊 ++ 𝑋)) = ((𝐺 Σg 𝑊) + (𝐺 Σg 𝑋)))
117 simpl2 1085 . . . . . 6 (((𝐺 ∈ Mnd ∧ 𝑊 ∈ Word 𝐵𝑋 ∈ Word 𝐵) ∧ 𝑊 ≠ ∅) → 𝑊 ∈ Word 𝐵)
118 ccatrid 13405 . . . . . 6 (𝑊 ∈ Word 𝐵 → (𝑊 ++ ∅) = 𝑊)
119117, 118syl 17 . . . . 5 (((𝐺 ∈ Mnd ∧ 𝑊 ∈ Word 𝐵𝑋 ∈ Word 𝐵) ∧ 𝑊 ≠ ∅) → (𝑊 ++ ∅) = 𝑊)
120119oveq2d 6706 . . . 4 (((𝐺 ∈ Mnd ∧ 𝑊 ∈ Word 𝐵𝑋 ∈ Word 𝐵) ∧ 𝑊 ≠ ∅) → (𝐺 Σg (𝑊 ++ ∅)) = (𝐺 Σg 𝑊))
121 simpl1 1084 . . . . 5 (((𝐺 ∈ Mnd ∧ 𝑊 ∈ Word 𝐵𝑋 ∈ Word 𝐵) ∧ 𝑊 ≠ ∅) → 𝐺 ∈ Mnd)
12215gsumwcl 17424 . . . . . . 7 ((𝐺 ∈ Mnd ∧ 𝑊 ∈ Word 𝐵) → (𝐺 Σg 𝑊) ∈ 𝐵)
1231223adant3 1101 . . . . . 6 ((𝐺 ∈ Mnd ∧ 𝑊 ∈ Word 𝐵𝑋 ∈ Word 𝐵) → (𝐺 Σg 𝑊) ∈ 𝐵)
124123adantr 480 . . . . 5 (((𝐺 ∈ Mnd ∧ 𝑊 ∈ Word 𝐵𝑋 ∈ Word 𝐵) ∧ 𝑊 ≠ ∅) → (𝐺 Σg 𝑊) ∈ 𝐵)
12515, 16, 4mndrid 17359 . . . . 5 ((𝐺 ∈ Mnd ∧ (𝐺 Σg 𝑊) ∈ 𝐵) → ((𝐺 Σg 𝑊) + (0g𝐺)) = (𝐺 Σg 𝑊))
126121, 124, 125syl2anc 694 . . . 4 (((𝐺 ∈ Mnd ∧ 𝑊 ∈ Word 𝐵𝑋 ∈ Word 𝐵) ∧ 𝑊 ≠ ∅) → ((𝐺 Σg 𝑊) + (0g𝐺)) = (𝐺 Σg 𝑊))
127120, 126eqtr4d 2688 . . 3 (((𝐺 ∈ Mnd ∧ 𝑊 ∈ Word 𝐵𝑋 ∈ Word 𝐵) ∧ 𝑊 ≠ ∅) → (𝐺 Σg (𝑊 ++ ∅)) = ((𝐺 Σg 𝑊) + (0g𝐺)))
12814, 116, 127pm2.61ne 2908 . 2 (((𝐺 ∈ Mnd ∧ 𝑊 ∈ Word 𝐵𝑋 ∈ Word 𝐵) ∧ 𝑊 ≠ ∅) → (𝐺 Σg (𝑊 ++ 𝑋)) = ((𝐺 Σg 𝑊) + (𝐺 Σg 𝑋)))
129 ccatlid 13404 . . . . 5 (𝑋 ∈ Word 𝐵 → (∅ ++ 𝑋) = 𝑋)
1301293ad2ant3 1104 . . . 4 ((𝐺 ∈ Mnd ∧ 𝑊 ∈ Word 𝐵𝑋 ∈ Word 𝐵) → (∅ ++ 𝑋) = 𝑋)
131130oveq2d 6706 . . 3 ((𝐺 ∈ Mnd ∧ 𝑊 ∈ Word 𝐵𝑋 ∈ Word 𝐵) → (𝐺 Σg (∅ ++ 𝑋)) = (𝐺 Σg 𝑋))
132 simp1 1081 . . . 4 ((𝐺 ∈ Mnd ∧ 𝑊 ∈ Word 𝐵𝑋 ∈ Word 𝐵) → 𝐺 ∈ Mnd)
13315gsumwcl 17424 . . . . 5 ((𝐺 ∈ Mnd ∧ 𝑋 ∈ Word 𝐵) → (𝐺 Σg 𝑋) ∈ 𝐵)
1341333adant2 1100 . . . 4 ((𝐺 ∈ Mnd ∧ 𝑊 ∈ Word 𝐵𝑋 ∈ Word 𝐵) → (𝐺 Σg 𝑋) ∈ 𝐵)
13515, 16, 4mndlid 17358 . . . 4 ((𝐺 ∈ Mnd ∧ (𝐺 Σg 𝑋) ∈ 𝐵) → ((0g𝐺) + (𝐺 Σg 𝑋)) = (𝐺 Σg 𝑋))
136132, 134, 135syl2anc 694 . . 3 ((𝐺 ∈ Mnd ∧ 𝑊 ∈ Word 𝐵𝑋 ∈ Word 𝐵) → ((0g𝐺) + (𝐺 Σg 𝑋)) = (𝐺 Σg 𝑋))
137131, 136eqtr4d 2688 . 2 ((𝐺 ∈ Mnd ∧ 𝑊 ∈ Word 𝐵𝑋 ∈ Word 𝐵) → (𝐺 Σg (∅ ++ 𝑋)) = ((0g𝐺) + (𝐺 Σg 𝑋)))
1388, 128, 137pm2.61ne 2908 1 ((𝐺 ∈ Mnd ∧ 𝑊 ∈ Word 𝐵𝑋 ∈ Word 𝐵) → (𝐺 Σg (𝑊 ++ 𝑋)) = ((𝐺 Σg 𝑊) + (𝐺 Σg 𝑋)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 383  w3a 1054   = wceq 1523  wcel 2030  wne 2823  c0 3948  wf 5922  cfv 5926  (class class class)co 6690  cc 9972  0cc0 9974  1c1 9975   + caddc 9977  cmin 10304  cn 11058  0cn0 11330  cz 11415  cuz 11725  ...cfz 12364  ..^cfzo 12504  seqcseq 12841  #chash 13157  Word cword 13323   ++ cconcat 13325  Basecbs 15904  +gcplusg 15988  0gc0g 16147   Σg cgsu 16148  Mndcmnd 17341
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-8 2032  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631  ax-rep 4804  ax-sep 4814  ax-nul 4822  ax-pow 4873  ax-pr 4936  ax-un 6991  ax-cnex 10030  ax-resscn 10031  ax-1cn 10032  ax-icn 10033  ax-addcl 10034  ax-addrcl 10035  ax-mulcl 10036  ax-mulrcl 10037  ax-mulcom 10038  ax-addass 10039  ax-mulass 10040  ax-distr 10041  ax-i2m1 10042  ax-1ne0 10043  ax-1rid 10044  ax-rnegex 10045  ax-rrecex 10046  ax-cnre 10047  ax-pre-lttri 10048  ax-pre-lttrn 10049  ax-pre-ltadd 10050  ax-pre-mulgt0 10051
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3or 1055  df-3an 1056  df-tru 1526  df-ex 1745  df-nf 1750  df-sb 1938  df-eu 2502  df-mo 2503  df-clab 2638  df-cleq 2644  df-clel 2647  df-nfc 2782  df-ne 2824  df-nel 2927  df-ral 2946  df-rex 2947  df-reu 2948  df-rmo 2949  df-rab 2950  df-v 3233  df-sbc 3469  df-csb 3567  df-dif 3610  df-un 3612  df-in 3614  df-ss 3621  df-pss 3623  df-nul 3949  df-if 4120  df-pw 4193  df-sn 4211  df-pr 4213  df-tp 4215  df-op 4217  df-uni 4469  df-int 4508  df-iun 4554  df-br 4686  df-opab 4746  df-mpt 4763  df-tr 4786  df-id 5053  df-eprel 5058  df-po 5064  df-so 5065  df-fr 5102  df-we 5104  df-xp 5149  df-rel 5150  df-cnv 5151  df-co 5152  df-dm 5153  df-rn 5154  df-res 5155  df-ima 5156  df-pred 5718  df-ord 5764  df-on 5765  df-lim 5766  df-suc 5767  df-iota 5889  df-fun 5928  df-fn 5929  df-f 5930  df-f1 5931  df-fo 5932  df-f1o 5933  df-fv 5934  df-riota 6651  df-ov 6693  df-oprab 6694  df-mpt2 6695  df-om 7108  df-1st 7210  df-2nd 7211  df-wrecs 7452  df-recs 7513  df-rdg 7551  df-1o 7605  df-oadd 7609  df-er 7787  df-en 7998  df-dom 7999  df-sdom 8000  df-fin 8001  df-card 8803  df-pnf 10114  df-mnf 10115  df-xr 10116  df-ltxr 10117  df-le 10118  df-sub 10306  df-neg 10307  df-nn 11059  df-2 11117  df-n0 11331  df-z 11416  df-uz 11726  df-fz 12365  df-fzo 12505  df-seq 12842  df-hash 13158  df-word 13331  df-concat 13333  df-ndx 15907  df-slot 15908  df-base 15910  df-sets 15911  df-ress 15912  df-plusg 16001  df-0g 16149  df-gsum 16150  df-mgm 17289  df-sgrp 17331  df-mnd 17342  df-submnd 17383
This theorem is referenced by:  gsumws2  17426  gsumccatsn  17427  gsumspl  17428  gsumwspan  17430  frmdgsum  17446  frmdup1  17448  gsumwrev  17842  psgnunilem5  17960  psgnuni  17965  frgpuplem  18231  frgpup1  18234  psgnghm  19974  mrsubccat  31541  gsumws3  38816  gsumws4  38817
  Copyright terms: Public domain W3C validator