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

Theorem gsumccat 17660
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 6853 . . . 4 (𝑊 = ∅ → (𝑊 ++ 𝑋) = (∅ ++ 𝑋))
21oveq2d 6862 . . 3 (𝑊 = ∅ → (𝐺 Σg (𝑊 ++ 𝑋)) = (𝐺 Σg (∅ ++ 𝑋)))
3 oveq2 6854 . . . . 5 (𝑊 = ∅ → (𝐺 Σg 𝑊) = (𝐺 Σg ∅))
4 eqid 2765 . . . . . 6 (0g𝐺) = (0g𝐺)
54gsum0 17560 . . . . 5 (𝐺 Σg ∅) = (0g𝐺)
63, 5syl6eq 2815 . . . 4 (𝑊 = ∅ → (𝐺 Σg 𝑊) = (0g𝐺))
76oveq1d 6861 . . 3 (𝑊 = ∅ → ((𝐺 Σg 𝑊) + (𝐺 Σg 𝑋)) = ((0g𝐺) + (𝐺 Σg 𝑋)))
82, 7eqeq12d 2780 . 2 (𝑊 = ∅ → ((𝐺 Σg (𝑊 ++ 𝑋)) = ((𝐺 Σg 𝑊) + (𝐺 Σg 𝑋)) ↔ (𝐺 Σg (∅ ++ 𝑋)) = ((0g𝐺) + (𝐺 Σg 𝑋))))
9 oveq2 6854 . . . . 5 (𝑋 = ∅ → (𝑊 ++ 𝑋) = (𝑊 ++ ∅))
109oveq2d 6862 . . . 4 (𝑋 = ∅ → (𝐺 Σg (𝑊 ++ 𝑋)) = (𝐺 Σg (𝑊 ++ ∅)))
11 oveq2 6854 . . . . . 6 (𝑋 = ∅ → (𝐺 Σg 𝑋) = (𝐺 Σg ∅))
1211, 5syl6eq 2815 . . . . 5 (𝑋 = ∅ → (𝐺 Σg 𝑋) = (0g𝐺))
1312oveq2d 6862 . . . 4 (𝑋 = ∅ → ((𝐺 Σg 𝑊) + (𝐺 Σg 𝑋)) = ((𝐺 Σg 𝑊) + (0g𝐺)))
1410, 13eqeq12d 2780 . . 3 (𝑋 = ∅ → ((𝐺 Σg (𝑊 ++ 𝑋)) = ((𝐺 Σg 𝑊) + (𝐺 Σg 𝑋)) ↔ (𝐺 Σg (𝑊 ++ ∅)) = ((𝐺 Σg 𝑊) + (0g𝐺))))
15 gsumwcl.b . . . . . 6 𝐵 = (Base‘𝐺)
16 gsumccat.p . . . . . 6 + = (+g𝐺)
17 simpl1 1242 . . . . . 6 (((𝐺 ∈ Mnd ∧ 𝑊 ∈ Word 𝐵𝑋 ∈ Word 𝐵) ∧ (𝑊 ≠ ∅ ∧ 𝑋 ≠ ∅)) → 𝐺 ∈ Mnd)
18 lennncl 13513 . . . . . . . . . . 11 ((𝑊 ∈ Word 𝐵𝑊 ≠ ∅) → (♯‘𝑊) ∈ ℕ)
19183ad2antl2 1237 . . . . . . . . . 10 (((𝐺 ∈ Mnd ∧ 𝑊 ∈ Word 𝐵𝑋 ∈ Word 𝐵) ∧ 𝑊 ≠ ∅) → (♯‘𝑊) ∈ ℕ)
2019adantrr 708 . . . . . . . . 9 (((𝐺 ∈ Mnd ∧ 𝑊 ∈ Word 𝐵𝑋 ∈ Word 𝐵) ∧ (𝑊 ≠ ∅ ∧ 𝑋 ≠ ∅)) → (♯‘𝑊) ∈ ℕ)
21 lennncl 13513 . . . . . . . . . . 11 ((𝑋 ∈ Word 𝐵𝑋 ≠ ∅) → (♯‘𝑋) ∈ ℕ)
22213ad2antl3 1238 . . . . . . . . . 10 (((𝐺 ∈ Mnd ∧ 𝑊 ∈ Word 𝐵𝑋 ∈ Word 𝐵) ∧ 𝑋 ≠ ∅) → (♯‘𝑋) ∈ ℕ)
2322adantrl 707 . . . . . . . . 9 (((𝐺 ∈ Mnd ∧ 𝑊 ∈ Word 𝐵𝑋 ∈ Word 𝐵) ∧ (𝑊 ≠ ∅ ∧ 𝑋 ≠ ∅)) → (♯‘𝑋) ∈ ℕ)
2420, 23nnaddcld 11329 . . . . . . . 8 (((𝐺 ∈ Mnd ∧ 𝑊 ∈ Word 𝐵𝑋 ∈ Word 𝐵) ∧ (𝑊 ≠ ∅ ∧ 𝑋 ≠ ∅)) → ((♯‘𝑊) + (♯‘𝑋)) ∈ ℕ)
25 nnm1nn0 11586 . . . . . . . 8 (((♯‘𝑊) + (♯‘𝑋)) ∈ ℕ → (((♯‘𝑊) + (♯‘𝑋)) − 1) ∈ ℕ0)
2624, 25syl 17 . . . . . . 7 (((𝐺 ∈ Mnd ∧ 𝑊 ∈ Word 𝐵𝑋 ∈ Word 𝐵) ∧ (𝑊 ≠ ∅ ∧ 𝑋 ≠ ∅)) → (((♯‘𝑊) + (♯‘𝑋)) − 1) ∈ ℕ0)
27 nn0uz 11929 . . . . . . 7 0 = (ℤ‘0)
2826, 27syl6eleq 2854 . . . . . 6 (((𝐺 ∈ Mnd ∧ 𝑊 ∈ Word 𝐵𝑋 ∈ Word 𝐵) ∧ (𝑊 ≠ ∅ ∧ 𝑋 ≠ ∅)) → (((♯‘𝑊) + (♯‘𝑋)) − 1) ∈ (ℤ‘0))
29 simpl2 1244 . . . . . . . . 9 (((𝐺 ∈ Mnd ∧ 𝑊 ∈ Word 𝐵𝑋 ∈ Word 𝐵) ∧ (𝑊 ≠ ∅ ∧ 𝑋 ≠ ∅)) → 𝑊 ∈ Word 𝐵)
30 simpl3 1246 . . . . . . . . 9 (((𝐺 ∈ Mnd ∧ 𝑊 ∈ Word 𝐵𝑋 ∈ Word 𝐵) ∧ (𝑊 ≠ ∅ ∧ 𝑋 ≠ ∅)) → 𝑋 ∈ Word 𝐵)
31 ccatcl 13553 . . . . . . . . 9 ((𝑊 ∈ Word 𝐵𝑋 ∈ Word 𝐵) → (𝑊 ++ 𝑋) ∈ Word 𝐵)
3229, 30, 31syl2anc 579 . . . . . . . 8 (((𝐺 ∈ Mnd ∧ 𝑊 ∈ Word 𝐵𝑋 ∈ Word 𝐵) ∧ (𝑊 ≠ ∅ ∧ 𝑋 ≠ ∅)) → (𝑊 ++ 𝑋) ∈ Word 𝐵)
33 wrdf 13498 . . . . . . . 8 ((𝑊 ++ 𝑋) ∈ Word 𝐵 → (𝑊 ++ 𝑋):(0..^(♯‘(𝑊 ++ 𝑋)))⟶𝐵)
3432, 33syl 17 . . . . . . 7 (((𝐺 ∈ Mnd ∧ 𝑊 ∈ Word 𝐵𝑋 ∈ Word 𝐵) ∧ (𝑊 ≠ ∅ ∧ 𝑋 ≠ ∅)) → (𝑊 ++ 𝑋):(0..^(♯‘(𝑊 ++ 𝑋)))⟶𝐵)
35 ccatlen 13554 . . . . . . . . . . 11 ((𝑊 ∈ Word 𝐵𝑋 ∈ Word 𝐵) → (♯‘(𝑊 ++ 𝑋)) = ((♯‘𝑊) + (♯‘𝑋)))
3629, 30, 35syl2anc 579 . . . . . . . . . 10 (((𝐺 ∈ Mnd ∧ 𝑊 ∈ Word 𝐵𝑋 ∈ Word 𝐵) ∧ (𝑊 ≠ ∅ ∧ 𝑋 ≠ ∅)) → (♯‘(𝑊 ++ 𝑋)) = ((♯‘𝑊) + (♯‘𝑋)))
3736oveq2d 6862 . . . . . . . . 9 (((𝐺 ∈ Mnd ∧ 𝑊 ∈ Word 𝐵𝑋 ∈ Word 𝐵) ∧ (𝑊 ≠ ∅ ∧ 𝑋 ≠ ∅)) → (0..^(♯‘(𝑊 ++ 𝑋))) = (0..^((♯‘𝑊) + (♯‘𝑋))))
3820nnzd 11734 . . . . . . . . . . 11 (((𝐺 ∈ Mnd ∧ 𝑊 ∈ Word 𝐵𝑋 ∈ Word 𝐵) ∧ (𝑊 ≠ ∅ ∧ 𝑋 ≠ ∅)) → (♯‘𝑊) ∈ ℤ)
3923nnzd 11734 . . . . . . . . . . 11 (((𝐺 ∈ Mnd ∧ 𝑊 ∈ Word 𝐵𝑋 ∈ Word 𝐵) ∧ (𝑊 ≠ ∅ ∧ 𝑋 ≠ ∅)) → (♯‘𝑋) ∈ ℤ)
4038, 39zaddcld 11739 . . . . . . . . . 10 (((𝐺 ∈ Mnd ∧ 𝑊 ∈ Word 𝐵𝑋 ∈ Word 𝐵) ∧ (𝑊 ≠ ∅ ∧ 𝑋 ≠ ∅)) → ((♯‘𝑊) + (♯‘𝑋)) ∈ ℤ)
41 fzoval 12686 . . . . . . . . . 10 (((♯‘𝑊) + (♯‘𝑋)) ∈ ℤ → (0..^((♯‘𝑊) + (♯‘𝑋))) = (0...(((♯‘𝑊) + (♯‘𝑋)) − 1)))
4240, 41syl 17 . . . . . . . . 9 (((𝐺 ∈ Mnd ∧ 𝑊 ∈ Word 𝐵𝑋 ∈ Word 𝐵) ∧ (𝑊 ≠ ∅ ∧ 𝑋 ≠ ∅)) → (0..^((♯‘𝑊) + (♯‘𝑋))) = (0...(((♯‘𝑊) + (♯‘𝑋)) − 1)))
4337, 42eqtrd 2799 . . . . . . . 8 (((𝐺 ∈ Mnd ∧ 𝑊 ∈ Word 𝐵𝑋 ∈ Word 𝐵) ∧ (𝑊 ≠ ∅ ∧ 𝑋 ≠ ∅)) → (0..^(♯‘(𝑊 ++ 𝑋))) = (0...(((♯‘𝑊) + (♯‘𝑋)) − 1)))
4443feq2d 6211 . . . . . . 7 (((𝐺 ∈ Mnd ∧ 𝑊 ∈ Word 𝐵𝑋 ∈ Word 𝐵) ∧ (𝑊 ≠ ∅ ∧ 𝑋 ≠ ∅)) → ((𝑊 ++ 𝑋):(0..^(♯‘(𝑊 ++ 𝑋)))⟶𝐵 ↔ (𝑊 ++ 𝑋):(0...(((♯‘𝑊) + (♯‘𝑋)) − 1))⟶𝐵))
4534, 44mpbid 223 . . . . . 6 (((𝐺 ∈ Mnd ∧ 𝑊 ∈ Word 𝐵𝑋 ∈ Word 𝐵) ∧ (𝑊 ≠ ∅ ∧ 𝑋 ≠ ∅)) → (𝑊 ++ 𝑋):(0...(((♯‘𝑊) + (♯‘𝑋)) − 1))⟶𝐵)
4615, 16, 17, 28, 45gsumval2 17562 . . . . 5 (((𝐺 ∈ Mnd ∧ 𝑊 ∈ Word 𝐵𝑋 ∈ Word 𝐵) ∧ (𝑊 ≠ ∅ ∧ 𝑋 ≠ ∅)) → (𝐺 Σg (𝑊 ++ 𝑋)) = (seq0( + , (𝑊 ++ 𝑋))‘(((♯‘𝑊) + (♯‘𝑋)) − 1)))
47 nnm1nn0 11586 . . . . . . . . . 10 ((♯‘𝑊) ∈ ℕ → ((♯‘𝑊) − 1) ∈ ℕ0)
4820, 47syl 17 . . . . . . . . 9 (((𝐺 ∈ Mnd ∧ 𝑊 ∈ Word 𝐵𝑋 ∈ Word 𝐵) ∧ (𝑊 ≠ ∅ ∧ 𝑋 ≠ ∅)) → ((♯‘𝑊) − 1) ∈ ℕ0)
4948, 27syl6eleq 2854 . . . . . . . 8 (((𝐺 ∈ Mnd ∧ 𝑊 ∈ Word 𝐵𝑋 ∈ Word 𝐵) ∧ (𝑊 ≠ ∅ ∧ 𝑋 ≠ ∅)) → ((♯‘𝑊) − 1) ∈ (ℤ‘0))
50 wrdf 13498 . . . . . . . . . 10 (𝑊 ∈ Word 𝐵𝑊:(0..^(♯‘𝑊))⟶𝐵)
5129, 50syl 17 . . . . . . . . 9 (((𝐺 ∈ Mnd ∧ 𝑊 ∈ Word 𝐵𝑋 ∈ Word 𝐵) ∧ (𝑊 ≠ ∅ ∧ 𝑋 ≠ ∅)) → 𝑊:(0..^(♯‘𝑊))⟶𝐵)
52 fzoval 12686 . . . . . . . . . . 11 ((♯‘𝑊) ∈ ℤ → (0..^(♯‘𝑊)) = (0...((♯‘𝑊) − 1)))
5338, 52syl 17 . . . . . . . . . 10 (((𝐺 ∈ Mnd ∧ 𝑊 ∈ Word 𝐵𝑋 ∈ Word 𝐵) ∧ (𝑊 ≠ ∅ ∧ 𝑋 ≠ ∅)) → (0..^(♯‘𝑊)) = (0...((♯‘𝑊) − 1)))
5453feq2d 6211 . . . . . . . . 9 (((𝐺 ∈ Mnd ∧ 𝑊 ∈ Word 𝐵𝑋 ∈ Word 𝐵) ∧ (𝑊 ≠ ∅ ∧ 𝑋 ≠ ∅)) → (𝑊:(0..^(♯‘𝑊))⟶𝐵𝑊:(0...((♯‘𝑊) − 1))⟶𝐵))
5551, 54mpbid 223 . . . . . . . 8 (((𝐺 ∈ Mnd ∧ 𝑊 ∈ Word 𝐵𝑋 ∈ Word 𝐵) ∧ (𝑊 ≠ ∅ ∧ 𝑋 ≠ ∅)) → 𝑊:(0...((♯‘𝑊) − 1))⟶𝐵)
5615, 16, 17, 49, 55gsumval2 17562 . . . . . . 7 (((𝐺 ∈ Mnd ∧ 𝑊 ∈ Word 𝐵𝑋 ∈ Word 𝐵) ∧ (𝑊 ≠ ∅ ∧ 𝑋 ≠ ∅)) → (𝐺 Σg 𝑊) = (seq0( + , 𝑊)‘((♯‘𝑊) − 1)))
57 nnm1nn0 11586 . . . . . . . . . 10 ((♯‘𝑋) ∈ ℕ → ((♯‘𝑋) − 1) ∈ ℕ0)
5823, 57syl 17 . . . . . . . . 9 (((𝐺 ∈ Mnd ∧ 𝑊 ∈ Word 𝐵𝑋 ∈ Word 𝐵) ∧ (𝑊 ≠ ∅ ∧ 𝑋 ≠ ∅)) → ((♯‘𝑋) − 1) ∈ ℕ0)
5958, 27syl6eleq 2854 . . . . . . . 8 (((𝐺 ∈ Mnd ∧ 𝑊 ∈ Word 𝐵𝑋 ∈ Word 𝐵) ∧ (𝑊 ≠ ∅ ∧ 𝑋 ≠ ∅)) → ((♯‘𝑋) − 1) ∈ (ℤ‘0))
60 wrdf 13498 . . . . . . . . . 10 (𝑋 ∈ Word 𝐵𝑋:(0..^(♯‘𝑋))⟶𝐵)
6130, 60syl 17 . . . . . . . . 9 (((𝐺 ∈ Mnd ∧ 𝑊 ∈ Word 𝐵𝑋 ∈ Word 𝐵) ∧ (𝑊 ≠ ∅ ∧ 𝑋 ≠ ∅)) → 𝑋:(0..^(♯‘𝑋))⟶𝐵)
62 fzoval 12686 . . . . . . . . . . 11 ((♯‘𝑋) ∈ ℤ → (0..^(♯‘𝑋)) = (0...((♯‘𝑋) − 1)))
6339, 62syl 17 . . . . . . . . . 10 (((𝐺 ∈ Mnd ∧ 𝑊 ∈ Word 𝐵𝑋 ∈ Word 𝐵) ∧ (𝑊 ≠ ∅ ∧ 𝑋 ≠ ∅)) → (0..^(♯‘𝑋)) = (0...((♯‘𝑋) − 1)))
6463feq2d 6211 . . . . . . . . 9 (((𝐺 ∈ Mnd ∧ 𝑊 ∈ Word 𝐵𝑋 ∈ Word 𝐵) ∧ (𝑊 ≠ ∅ ∧ 𝑋 ≠ ∅)) → (𝑋:(0..^(♯‘𝑋))⟶𝐵𝑋:(0...((♯‘𝑋) − 1))⟶𝐵))
6561, 64mpbid 223 . . . . . . . 8 (((𝐺 ∈ Mnd ∧ 𝑊 ∈ Word 𝐵𝑋 ∈ Word 𝐵) ∧ (𝑊 ≠ ∅ ∧ 𝑋 ≠ ∅)) → 𝑋:(0...((♯‘𝑋) − 1))⟶𝐵)
6615, 16, 17, 59, 65gsumval2 17562 . . . . . . 7 (((𝐺 ∈ Mnd ∧ 𝑊 ∈ Word 𝐵𝑋 ∈ Word 𝐵) ∧ (𝑊 ≠ ∅ ∧ 𝑋 ≠ ∅)) → (𝐺 Σg 𝑋) = (seq0( + , 𝑋)‘((♯‘𝑋) − 1)))
6756, 66oveq12d 6864 . . . . . 6 (((𝐺 ∈ Mnd ∧ 𝑊 ∈ Word 𝐵𝑋 ∈ Word 𝐵) ∧ (𝑊 ≠ ∅ ∧ 𝑋 ≠ ∅)) → ((𝐺 Σg 𝑊) + (𝐺 Σg 𝑋)) = ((seq0( + , 𝑊)‘((♯‘𝑊) − 1)) + (seq0( + , 𝑋)‘((♯‘𝑋) − 1))))
6815, 16mndcl 17583 . . . . . . . . . 10 ((𝐺 ∈ Mnd ∧ 𝑥𝐵𝑦𝐵) → (𝑥 + 𝑦) ∈ 𝐵)
69683expb 1149 . . . . . . . . 9 ((𝐺 ∈ Mnd ∧ (𝑥𝐵𝑦𝐵)) → (𝑥 + 𝑦) ∈ 𝐵)
7017, 69sylan 575 . . . . . . . 8 ((((𝐺 ∈ Mnd ∧ 𝑊 ∈ Word 𝐵𝑋 ∈ Word 𝐵) ∧ (𝑊 ≠ ∅ ∧ 𝑋 ≠ ∅)) ∧ (𝑥𝐵𝑦𝐵)) → (𝑥 + 𝑦) ∈ 𝐵)
7115, 16mndass 17584 . . . . . . . . 9 ((𝐺 ∈ Mnd ∧ (𝑥𝐵𝑦𝐵𝑧𝐵)) → ((𝑥 + 𝑦) + 𝑧) = (𝑥 + (𝑦 + 𝑧)))
7217, 71sylan 575 . . . . . . . 8 ((((𝐺 ∈ Mnd ∧ 𝑊 ∈ Word 𝐵𝑋 ∈ Word 𝐵) ∧ (𝑊 ≠ ∅ ∧ 𝑋 ≠ ∅)) ∧ (𝑥𝐵𝑦𝐵𝑧𝐵)) → ((𝑥 + 𝑦) + 𝑧) = (𝑥 + (𝑦 + 𝑧)))
73 uzid 11908 . . . . . . . . . . 11 ((♯‘𝑊) ∈ ℤ → (♯‘𝑊) ∈ (ℤ‘(♯‘𝑊)))
7438, 73syl 17 . . . . . . . . . 10 (((𝐺 ∈ Mnd ∧ 𝑊 ∈ Word 𝐵𝑋 ∈ Word 𝐵) ∧ (𝑊 ≠ ∅ ∧ 𝑋 ≠ ∅)) → (♯‘𝑊) ∈ (ℤ‘(♯‘𝑊)))
75 uzaddcl 11951 . . . . . . . . . 10 (((♯‘𝑊) ∈ (ℤ‘(♯‘𝑊)) ∧ ((♯‘𝑋) − 1) ∈ ℕ0) → ((♯‘𝑊) + ((♯‘𝑋) − 1)) ∈ (ℤ‘(♯‘𝑊)))
7674, 58, 75syl2anc 579 . . . . . . . . 9 (((𝐺 ∈ Mnd ∧ 𝑊 ∈ Word 𝐵𝑋 ∈ Word 𝐵) ∧ (𝑊 ≠ ∅ ∧ 𝑋 ≠ ∅)) → ((♯‘𝑊) + ((♯‘𝑋) − 1)) ∈ (ℤ‘(♯‘𝑊)))
7720nncnd 11297 . . . . . . . . . 10 (((𝐺 ∈ Mnd ∧ 𝑊 ∈ Word 𝐵𝑋 ∈ Word 𝐵) ∧ (𝑊 ≠ ∅ ∧ 𝑋 ≠ ∅)) → (♯‘𝑊) ∈ ℂ)
7823nncnd 11297 . . . . . . . . . 10 (((𝐺 ∈ Mnd ∧ 𝑊 ∈ Word 𝐵𝑋 ∈ Word 𝐵) ∧ (𝑊 ≠ ∅ ∧ 𝑋 ≠ ∅)) → (♯‘𝑋) ∈ ℂ)
79 1cnd 10292 . . . . . . . . . 10 (((𝐺 ∈ Mnd ∧ 𝑊 ∈ Word 𝐵𝑋 ∈ Word 𝐵) ∧ (𝑊 ≠ ∅ ∧ 𝑋 ≠ ∅)) → 1 ∈ ℂ)
8077, 78, 79addsubassd 10671 . . . . . . . . 9 (((𝐺 ∈ Mnd ∧ 𝑊 ∈ Word 𝐵𝑋 ∈ Word 𝐵) ∧ (𝑊 ≠ ∅ ∧ 𝑋 ≠ ∅)) → (((♯‘𝑊) + (♯‘𝑋)) − 1) = ((♯‘𝑊) + ((♯‘𝑋) − 1)))
81 ax-1cn 10251 . . . . . . . . . . 11 1 ∈ ℂ
82 npcan 10549 . . . . . . . . . . 11 (((♯‘𝑊) ∈ ℂ ∧ 1 ∈ ℂ) → (((♯‘𝑊) − 1) + 1) = (♯‘𝑊))
8377, 81, 82sylancl 580 . . . . . . . . . 10 (((𝐺 ∈ Mnd ∧ 𝑊 ∈ Word 𝐵𝑋 ∈ Word 𝐵) ∧ (𝑊 ≠ ∅ ∧ 𝑋 ≠ ∅)) → (((♯‘𝑊) − 1) + 1) = (♯‘𝑊))
8483fveq2d 6383 . . . . . . . . 9 (((𝐺 ∈ Mnd ∧ 𝑊 ∈ Word 𝐵𝑋 ∈ Word 𝐵) ∧ (𝑊 ≠ ∅ ∧ 𝑋 ≠ ∅)) → (ℤ‘(((♯‘𝑊) − 1) + 1)) = (ℤ‘(♯‘𝑊)))
8576, 80, 843eltr4d 2859 . . . . . . . 8 (((𝐺 ∈ Mnd ∧ 𝑊 ∈ Word 𝐵𝑋 ∈ Word 𝐵) ∧ (𝑊 ≠ ∅ ∧ 𝑋 ≠ ∅)) → (((♯‘𝑊) + (♯‘𝑋)) − 1) ∈ (ℤ‘(((♯‘𝑊) − 1) + 1)))
8645ffvelrnda 6553 . . . . . . . 8 ((((𝐺 ∈ Mnd ∧ 𝑊 ∈ Word 𝐵𝑋 ∈ Word 𝐵) ∧ (𝑊 ≠ ∅ ∧ 𝑋 ≠ ∅)) ∧ 𝑥 ∈ (0...(((♯‘𝑊) + (♯‘𝑋)) − 1))) → ((𝑊 ++ 𝑋)‘𝑥) ∈ 𝐵)
8770, 72, 85, 49, 86seqsplit 13048 . . . . . . 7 (((𝐺 ∈ Mnd ∧ 𝑊 ∈ Word 𝐵𝑋 ∈ Word 𝐵) ∧ (𝑊 ≠ ∅ ∧ 𝑋 ≠ ∅)) → (seq0( + , (𝑊 ++ 𝑋))‘(((♯‘𝑊) + (♯‘𝑋)) − 1)) = ((seq0( + , (𝑊 ++ 𝑋))‘((♯‘𝑊) − 1)) + (seq(((♯‘𝑊) − 1) + 1)( + , (𝑊 ++ 𝑋))‘(((♯‘𝑊) + (♯‘𝑋)) − 1))))
88 simpll2 1271 . . . . . . . . . 10 ((((𝐺 ∈ Mnd ∧ 𝑊 ∈ Word 𝐵𝑋 ∈ Word 𝐵) ∧ (𝑊 ≠ ∅ ∧ 𝑋 ≠ ∅)) ∧ 𝑥 ∈ (0...((♯‘𝑊) − 1))) → 𝑊 ∈ Word 𝐵)
89 simpll3 1273 . . . . . . . . . 10 ((((𝐺 ∈ Mnd ∧ 𝑊 ∈ Word 𝐵𝑋 ∈ Word 𝐵) ∧ (𝑊 ≠ ∅ ∧ 𝑋 ≠ ∅)) ∧ 𝑥 ∈ (0...((♯‘𝑊) − 1))) → 𝑋 ∈ Word 𝐵)
9053eleq2d 2830 . . . . . . . . . . 11 (((𝐺 ∈ Mnd ∧ 𝑊 ∈ Word 𝐵𝑋 ∈ Word 𝐵) ∧ (𝑊 ≠ ∅ ∧ 𝑋 ≠ ∅)) → (𝑥 ∈ (0..^(♯‘𝑊)) ↔ 𝑥 ∈ (0...((♯‘𝑊) − 1))))
9190biimpar 469 . . . . . . . . . 10 ((((𝐺 ∈ Mnd ∧ 𝑊 ∈ Word 𝐵𝑋 ∈ Word 𝐵) ∧ (𝑊 ≠ ∅ ∧ 𝑋 ≠ ∅)) ∧ 𝑥 ∈ (0...((♯‘𝑊) − 1))) → 𝑥 ∈ (0..^(♯‘𝑊)))
92 ccatval1 13556 . . . . . . . . . 10 ((𝑊 ∈ Word 𝐵𝑋 ∈ Word 𝐵𝑥 ∈ (0..^(♯‘𝑊))) → ((𝑊 ++ 𝑋)‘𝑥) = (𝑊𝑥))
9388, 89, 91, 92syl3anc 1490 . . . . . . . . 9 ((((𝐺 ∈ Mnd ∧ 𝑊 ∈ Word 𝐵𝑋 ∈ Word 𝐵) ∧ (𝑊 ≠ ∅ ∧ 𝑋 ≠ ∅)) ∧ 𝑥 ∈ (0...((♯‘𝑊) − 1))) → ((𝑊 ++ 𝑋)‘𝑥) = (𝑊𝑥))
9449, 93seqfveq 13039 . . . . . . . 8 (((𝐺 ∈ Mnd ∧ 𝑊 ∈ Word 𝐵𝑋 ∈ Word 𝐵) ∧ (𝑊 ≠ ∅ ∧ 𝑋 ≠ ∅)) → (seq0( + , (𝑊 ++ 𝑋))‘((♯‘𝑊) − 1)) = (seq0( + , 𝑊)‘((♯‘𝑊) − 1)))
9577addid2d 10496 . . . . . . . . . . . 12 (((𝐺 ∈ Mnd ∧ 𝑊 ∈ Word 𝐵𝑋 ∈ Word 𝐵) ∧ (𝑊 ≠ ∅ ∧ 𝑋 ≠ ∅)) → (0 + (♯‘𝑊)) = (♯‘𝑊))
9683, 95eqtr4d 2802 . . . . . . . . . . 11 (((𝐺 ∈ Mnd ∧ 𝑊 ∈ Word 𝐵𝑋 ∈ Word 𝐵) ∧ (𝑊 ≠ ∅ ∧ 𝑋 ≠ ∅)) → (((♯‘𝑊) − 1) + 1) = (0 + (♯‘𝑊)))
9796seqeq1d 13021 . . . . . . . . . 10 (((𝐺 ∈ Mnd ∧ 𝑊 ∈ Word 𝐵𝑋 ∈ Word 𝐵) ∧ (𝑊 ≠ ∅ ∧ 𝑋 ≠ ∅)) → seq(((♯‘𝑊) − 1) + 1)( + , (𝑊 ++ 𝑋)) = seq(0 + (♯‘𝑊))( + , (𝑊 ++ 𝑋)))
9877, 78addcomd 10497 . . . . . . . . . . . 12 (((𝐺 ∈ Mnd ∧ 𝑊 ∈ Word 𝐵𝑋 ∈ Word 𝐵) ∧ (𝑊 ≠ ∅ ∧ 𝑋 ≠ ∅)) → ((♯‘𝑊) + (♯‘𝑋)) = ((♯‘𝑋) + (♯‘𝑊)))
9998oveq1d 6861 . . . . . . . . . . 11 (((𝐺 ∈ Mnd ∧ 𝑊 ∈ Word 𝐵𝑋 ∈ Word 𝐵) ∧ (𝑊 ≠ ∅ ∧ 𝑋 ≠ ∅)) → (((♯‘𝑊) + (♯‘𝑋)) − 1) = (((♯‘𝑋) + (♯‘𝑊)) − 1))
10078, 77, 79addsubd 10672 . . . . . . . . . . 11 (((𝐺 ∈ Mnd ∧ 𝑊 ∈ Word 𝐵𝑋 ∈ Word 𝐵) ∧ (𝑊 ≠ ∅ ∧ 𝑋 ≠ ∅)) → (((♯‘𝑋) + (♯‘𝑊)) − 1) = (((♯‘𝑋) − 1) + (♯‘𝑊)))
10199, 100eqtrd 2799 . . . . . . . . . 10 (((𝐺 ∈ Mnd ∧ 𝑊 ∈ Word 𝐵𝑋 ∈ Word 𝐵) ∧ (𝑊 ≠ ∅ ∧ 𝑋 ≠ ∅)) → (((♯‘𝑊) + (♯‘𝑋)) − 1) = (((♯‘𝑋) − 1) + (♯‘𝑊)))
10297, 101fveq12d 6386 . . . . . . . . 9 (((𝐺 ∈ Mnd ∧ 𝑊 ∈ Word 𝐵𝑋 ∈ Word 𝐵) ∧ (𝑊 ≠ ∅ ∧ 𝑋 ≠ ∅)) → (seq(((♯‘𝑊) − 1) + 1)( + , (𝑊 ++ 𝑋))‘(((♯‘𝑊) + (♯‘𝑋)) − 1)) = (seq(0 + (♯‘𝑊))( + , (𝑊 ++ 𝑋))‘(((♯‘𝑋) − 1) + (♯‘𝑊))))
103 simpll2 1271 . . . . . . . . . . . 12 ((((𝐺 ∈ Mnd ∧ 𝑊 ∈ Word 𝐵𝑋 ∈ Word 𝐵) ∧ (𝑊 ≠ ∅ ∧ 𝑋 ≠ ∅)) ∧ 𝑥 ∈ (0...((♯‘𝑋) − 1))) → 𝑊 ∈ Word 𝐵)
104 simpll3 1273 . . . . . . . . . . . 12 ((((𝐺 ∈ Mnd ∧ 𝑊 ∈ Word 𝐵𝑋 ∈ Word 𝐵) ∧ (𝑊 ≠ ∅ ∧ 𝑋 ≠ ∅)) ∧ 𝑥 ∈ (0...((♯‘𝑋) − 1))) → 𝑋 ∈ Word 𝐵)
10563eleq2d 2830 . . . . . . . . . . . . 13 (((𝐺 ∈ Mnd ∧ 𝑊 ∈ Word 𝐵𝑋 ∈ Word 𝐵) ∧ (𝑊 ≠ ∅ ∧ 𝑋 ≠ ∅)) → (𝑥 ∈ (0..^(♯‘𝑋)) ↔ 𝑥 ∈ (0...((♯‘𝑋) − 1))))
106105biimpar 469 . . . . . . . . . . . 12 ((((𝐺 ∈ Mnd ∧ 𝑊 ∈ Word 𝐵𝑋 ∈ Word 𝐵) ∧ (𝑊 ≠ ∅ ∧ 𝑋 ≠ ∅)) ∧ 𝑥 ∈ (0...((♯‘𝑋) − 1))) → 𝑥 ∈ (0..^(♯‘𝑋)))
107 ccatval3 13558 . . . . . . . . . . . 12 ((𝑊 ∈ Word 𝐵𝑋 ∈ Word 𝐵𝑥 ∈ (0..^(♯‘𝑋))) → ((𝑊 ++ 𝑋)‘(𝑥 + (♯‘𝑊))) = (𝑋𝑥))
108103, 104, 106, 107syl3anc 1490 . . . . . . . . . . 11 ((((𝐺 ∈ Mnd ∧ 𝑊 ∈ Word 𝐵𝑋 ∈ Word 𝐵) ∧ (𝑊 ≠ ∅ ∧ 𝑋 ≠ ∅)) ∧ 𝑥 ∈ (0...((♯‘𝑋) − 1))) → ((𝑊 ++ 𝑋)‘(𝑥 + (♯‘𝑊))) = (𝑋𝑥))
109108eqcomd 2771 . . . . . . . . . 10 ((((𝐺 ∈ Mnd ∧ 𝑊 ∈ Word 𝐵𝑋 ∈ Word 𝐵) ∧ (𝑊 ≠ ∅ ∧ 𝑋 ≠ ∅)) ∧ 𝑥 ∈ (0...((♯‘𝑋) − 1))) → (𝑋𝑥) = ((𝑊 ++ 𝑋)‘(𝑥 + (♯‘𝑊))))
11059, 38, 109seqshft2 13041 . . . . . . . . 9 (((𝐺 ∈ Mnd ∧ 𝑊 ∈ Word 𝐵𝑋 ∈ Word 𝐵) ∧ (𝑊 ≠ ∅ ∧ 𝑋 ≠ ∅)) → (seq0( + , 𝑋)‘((♯‘𝑋) − 1)) = (seq(0 + (♯‘𝑊))( + , (𝑊 ++ 𝑋))‘(((♯‘𝑋) − 1) + (♯‘𝑊))))
111102, 110eqtr4d 2802 . . . . . . . 8 (((𝐺 ∈ Mnd ∧ 𝑊 ∈ Word 𝐵𝑋 ∈ Word 𝐵) ∧ (𝑊 ≠ ∅ ∧ 𝑋 ≠ ∅)) → (seq(((♯‘𝑊) − 1) + 1)( + , (𝑊 ++ 𝑋))‘(((♯‘𝑊) + (♯‘𝑋)) − 1)) = (seq0( + , 𝑋)‘((♯‘𝑋) − 1)))
11294, 111oveq12d 6864 . . . . . . 7 (((𝐺 ∈ Mnd ∧ 𝑊 ∈ Word 𝐵𝑋 ∈ Word 𝐵) ∧ (𝑊 ≠ ∅ ∧ 𝑋 ≠ ∅)) → ((seq0( + , (𝑊 ++ 𝑋))‘((♯‘𝑊) − 1)) + (seq(((♯‘𝑊) − 1) + 1)( + , (𝑊 ++ 𝑋))‘(((♯‘𝑊) + (♯‘𝑋)) − 1))) = ((seq0( + , 𝑊)‘((♯‘𝑊) − 1)) + (seq0( + , 𝑋)‘((♯‘𝑋) − 1))))
11387, 112eqtrd 2799 . . . . . 6 (((𝐺 ∈ Mnd ∧ 𝑊 ∈ Word 𝐵𝑋 ∈ Word 𝐵) ∧ (𝑊 ≠ ∅ ∧ 𝑋 ≠ ∅)) → (seq0( + , (𝑊 ++ 𝑋))‘(((♯‘𝑊) + (♯‘𝑋)) − 1)) = ((seq0( + , 𝑊)‘((♯‘𝑊) − 1)) + (seq0( + , 𝑋)‘((♯‘𝑋) − 1))))
11467, 113eqtr4d 2802 . . . . 5 (((𝐺 ∈ Mnd ∧ 𝑊 ∈ Word 𝐵𝑋 ∈ Word 𝐵) ∧ (𝑊 ≠ ∅ ∧ 𝑋 ≠ ∅)) → ((𝐺 Σg 𝑊) + (𝐺 Σg 𝑋)) = (seq0( + , (𝑊 ++ 𝑋))‘(((♯‘𝑊) + (♯‘𝑋)) − 1)))
11546, 114eqtr4d 2802 . . . 4 (((𝐺 ∈ Mnd ∧ 𝑊 ∈ Word 𝐵𝑋 ∈ Word 𝐵) ∧ (𝑊 ≠ ∅ ∧ 𝑋 ≠ ∅)) → (𝐺 Σg (𝑊 ++ 𝑋)) = ((𝐺 Σg 𝑊) + (𝐺 Σg 𝑋)))
116115anassrs 459 . . 3 ((((𝐺 ∈ Mnd ∧ 𝑊 ∈ Word 𝐵𝑋 ∈ Word 𝐵) ∧ 𝑊 ≠ ∅) ∧ 𝑋 ≠ ∅) → (𝐺 Σg (𝑊 ++ 𝑋)) = ((𝐺 Σg 𝑊) + (𝐺 Σg 𝑋)))
117 simpl2 1244 . . . . . 6 (((𝐺 ∈ Mnd ∧ 𝑊 ∈ Word 𝐵𝑋 ∈ Word 𝐵) ∧ 𝑊 ≠ ∅) → 𝑊 ∈ Word 𝐵)
118 ccatrid 13566 . . . . . 6 (𝑊 ∈ Word 𝐵 → (𝑊 ++ ∅) = 𝑊)
119117, 118syl 17 . . . . 5 (((𝐺 ∈ Mnd ∧ 𝑊 ∈ Word 𝐵𝑋 ∈ Word 𝐵) ∧ 𝑊 ≠ ∅) → (𝑊 ++ ∅) = 𝑊)
120119oveq2d 6862 . . . 4 (((𝐺 ∈ Mnd ∧ 𝑊 ∈ Word 𝐵𝑋 ∈ Word 𝐵) ∧ 𝑊 ≠ ∅) → (𝐺 Σg (𝑊 ++ ∅)) = (𝐺 Σg 𝑊))
121 simpl1 1242 . . . . 5 (((𝐺 ∈ Mnd ∧ 𝑊 ∈ Word 𝐵𝑋 ∈ Word 𝐵) ∧ 𝑊 ≠ ∅) → 𝐺 ∈ Mnd)
12215gsumwcl 17659 . . . . . . 7 ((𝐺 ∈ Mnd ∧ 𝑊 ∈ Word 𝐵) → (𝐺 Σg 𝑊) ∈ 𝐵)
1231223adant3 1162 . . . . . 6 ((𝐺 ∈ Mnd ∧ 𝑊 ∈ Word 𝐵𝑋 ∈ Word 𝐵) → (𝐺 Σg 𝑊) ∈ 𝐵)
124123adantr 472 . . . . 5 (((𝐺 ∈ Mnd ∧ 𝑊 ∈ Word 𝐵𝑋 ∈ Word 𝐵) ∧ 𝑊 ≠ ∅) → (𝐺 Σg 𝑊) ∈ 𝐵)
12515, 16, 4mndrid 17594 . . . . 5 ((𝐺 ∈ Mnd ∧ (𝐺 Σg 𝑊) ∈ 𝐵) → ((𝐺 Σg 𝑊) + (0g𝐺)) = (𝐺 Σg 𝑊))
126121, 124, 125syl2anc 579 . . . 4 (((𝐺 ∈ Mnd ∧ 𝑊 ∈ Word 𝐵𝑋 ∈ Word 𝐵) ∧ 𝑊 ≠ ∅) → ((𝐺 Σg 𝑊) + (0g𝐺)) = (𝐺 Σg 𝑊))
127120, 126eqtr4d 2802 . . 3 (((𝐺 ∈ Mnd ∧ 𝑊 ∈ Word 𝐵𝑋 ∈ Word 𝐵) ∧ 𝑊 ≠ ∅) → (𝐺 Σg (𝑊 ++ ∅)) = ((𝐺 Σg 𝑊) + (0g𝐺)))
12814, 116, 127pm2.61ne 3022 . 2 (((𝐺 ∈ Mnd ∧ 𝑊 ∈ Word 𝐵𝑋 ∈ Word 𝐵) ∧ 𝑊 ≠ ∅) → (𝐺 Σg (𝑊 ++ 𝑋)) = ((𝐺 Σg 𝑊) + (𝐺 Σg 𝑋)))
129 ccatlid 13565 . . . . 5 (𝑋 ∈ Word 𝐵 → (∅ ++ 𝑋) = 𝑋)
1301293ad2ant3 1165 . . . 4 ((𝐺 ∈ Mnd ∧ 𝑊 ∈ Word 𝐵𝑋 ∈ Word 𝐵) → (∅ ++ 𝑋) = 𝑋)
131130oveq2d 6862 . . 3 ((𝐺 ∈ Mnd ∧ 𝑊 ∈ Word 𝐵𝑋 ∈ Word 𝐵) → (𝐺 Σg (∅ ++ 𝑋)) = (𝐺 Σg 𝑋))
132 simp1 1166 . . . 4 ((𝐺 ∈ Mnd ∧ 𝑊 ∈ Word 𝐵𝑋 ∈ Word 𝐵) → 𝐺 ∈ Mnd)
13315gsumwcl 17659 . . . . 5 ((𝐺 ∈ Mnd ∧ 𝑋 ∈ Word 𝐵) → (𝐺 Σg 𝑋) ∈ 𝐵)
1341333adant2 1161 . . . 4 ((𝐺 ∈ Mnd ∧ 𝑊 ∈ Word 𝐵𝑋 ∈ Word 𝐵) → (𝐺 Σg 𝑋) ∈ 𝐵)
13515, 16, 4mndlid 17593 . . . 4 ((𝐺 ∈ Mnd ∧ (𝐺 Σg 𝑋) ∈ 𝐵) → ((0g𝐺) + (𝐺 Σg 𝑋)) = (𝐺 Σg 𝑋))
136132, 134, 135syl2anc 579 . . 3 ((𝐺 ∈ Mnd ∧ 𝑊 ∈ Word 𝐵𝑋 ∈ Word 𝐵) → ((0g𝐺) + (𝐺 Σg 𝑋)) = (𝐺 Σg 𝑋))
137131, 136eqtr4d 2802 . 2 ((𝐺 ∈ Mnd ∧ 𝑊 ∈ Word 𝐵𝑋 ∈ Word 𝐵) → (𝐺 Σg (∅ ++ 𝑋)) = ((0g𝐺) + (𝐺 Σg 𝑋)))
1388, 128, 137pm2.61ne 3022 1 ((𝐺 ∈ Mnd ∧ 𝑊 ∈ Word 𝐵𝑋 ∈ Word 𝐵) → (𝐺 Σg (𝑊 ++ 𝑋)) = ((𝐺 Σg 𝑊) + (𝐺 Σg 𝑋)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 384  w3a 1107   = wceq 1652  wcel 2155  wne 2937  c0 4081  wf 6066  cfv 6070  (class class class)co 6846  cc 10191  0cc0 10193  1c1 10194   + caddc 10196  cmin 10525  cn 11279  0cn0 11543  cz 11629  cuz 11893  ...cfz 12540  ..^cfzo 12680  seqcseq 13015  chash 13328  Word cword 13493   ++ cconcat 13549  Basecbs 16146  +gcplusg 16230  0gc0g 16382   Σg cgsu 16383  Mndcmnd 17576
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1890  ax-4 1904  ax-5 2005  ax-6 2070  ax-7 2105  ax-8 2157  ax-9 2164  ax-10 2183  ax-11 2198  ax-12 2211  ax-13 2352  ax-ext 2743  ax-rep 4932  ax-sep 4943  ax-nul 4951  ax-pow 5003  ax-pr 5064  ax-un 7151  ax-cnex 10249  ax-resscn 10250  ax-1cn 10251  ax-icn 10252  ax-addcl 10253  ax-addrcl 10254  ax-mulcl 10255  ax-mulrcl 10256  ax-mulcom 10257  ax-addass 10258  ax-mulass 10259  ax-distr 10260  ax-i2m1 10261  ax-1ne0 10262  ax-1rid 10263  ax-rnegex 10264  ax-rrecex 10265  ax-cnre 10266  ax-pre-lttri 10267  ax-pre-lttrn 10268  ax-pre-ltadd 10269  ax-pre-mulgt0 10270
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 874  df-3or 1108  df-3an 1109  df-tru 1656  df-ex 1875  df-nf 1879  df-sb 2063  df-mo 2565  df-eu 2582  df-clab 2752  df-cleq 2758  df-clel 2761  df-nfc 2896  df-ne 2938  df-nel 3041  df-ral 3060  df-rex 3061  df-reu 3062  df-rmo 3063  df-rab 3064  df-v 3352  df-sbc 3599  df-csb 3694  df-dif 3737  df-un 3739  df-in 3741  df-ss 3748  df-pss 3750  df-nul 4082  df-if 4246  df-pw 4319  df-sn 4337  df-pr 4339  df-tp 4341  df-op 4343  df-uni 4597  df-int 4636  df-iun 4680  df-br 4812  df-opab 4874  df-mpt 4891  df-tr 4914  df-id 5187  df-eprel 5192  df-po 5200  df-so 5201  df-fr 5238  df-we 5240  df-xp 5285  df-rel 5286  df-cnv 5287  df-co 5288  df-dm 5289  df-rn 5290  df-res 5291  df-ima 5292  df-pred 5867  df-ord 5913  df-on 5914  df-lim 5915  df-suc 5916  df-iota 6033  df-fun 6072  df-fn 6073  df-f 6074  df-f1 6075  df-fo 6076  df-f1o 6077  df-fv 6078  df-riota 6807  df-ov 6849  df-oprab 6850  df-mpt2 6851  df-om 7268  df-1st 7370  df-2nd 7371  df-wrecs 7614  df-recs 7676  df-rdg 7714  df-1o 7768  df-oadd 7772  df-er 7951  df-en 8165  df-dom 8166  df-sdom 8167  df-fin 8168  df-card 9020  df-pnf 10334  df-mnf 10335  df-xr 10336  df-ltxr 10337  df-le 10338  df-sub 10527  df-neg 10528  df-nn 11280  df-2 11340  df-n0 11544  df-z 11630  df-uz 11894  df-fz 12541  df-fzo 12681  df-seq 13016  df-hash 13329  df-word 13494  df-concat 13550  df-ndx 16149  df-slot 16150  df-base 16152  df-sets 16153  df-ress 16154  df-plusg 16243  df-0g 16384  df-gsum 16385  df-mgm 17524  df-sgrp 17566  df-mnd 17577  df-submnd 17618
This theorem is referenced by:  gsumws2  17661  gsumccatsn  17662  gsumspl  17663  gsumsplOLD  17664  gsumwspan  17666  frmdgsum  17682  frmdup1  17684  gsumwrev  18075  psgnunilem5  18193  psgnunilem5OLD  18194  psgnuni  18199  frgpuplem  18467  frgpup1  18470  psgnghm  20214  mrsubccat  31886  gsumws3  39199  gsumws4  39200
  Copyright terms: Public domain W3C validator