gsumccat

Description: Homomorphic property of composites. Second formula in Lang p. 4. (Contributed by Stefan O'Rear, 16-Aug-2015) (Revised by Mario Carneiro, 1-Oct-2015) (Proof shortened by AV, 26-Dec-2023)

	Ref	Expression
Hypotheses	gsumccat.b	$⊢ B = {Base}_{G}$
	gsumccat.p	$⊢ \underset{˙}{+} = +_{G}$
Assertion	gsumccat	$⊢ (G \in Mnd \land W \in Word B \land X \in Word B) \to \sum_{G} (W ++ X) = (\sum_{G}, W) \underset{˙}{+} (\sum_{G}, X)$

Proof

Step	Hyp	Ref	Expression
1		gsumccat.b	$⊢ B = {Base}_{G}$
2		gsumccat.p	$⊢ \underset{˙}{+} = +_{G}$
3		oveq1	$⊢ W = \emptyset \to W ++ X = \emptyset ++ X$
4	3	oveq2d	$⊢ W = \emptyset \to \sum_{G} (W ++ X) = \sum_{G} (\emptyset ++ X)$
5		oveq2	$⊢ W = \emptyset \to \sum_{G} W = \sum_{G} \emptyset$
6		eqid	$⊢ 0_{G} = 0_{G}$
7	6	gsum0	$⊢ \sum_{G} \emptyset = 0_{G}$
8	5 7	syl6eq	$⊢ W = \emptyset \to \sum_{G} W = 0_{G}$
9	8	oveq1d	$⊢ W = \emptyset \to (\sum_{G}, W) \underset{˙}{+} (\sum_{G}, X) = 0_{G} \underset{˙}{+} (\sum_{G}, X)$
10	4 9	eqeq12d	$⊢ W = \emptyset \to (\sum_{G} (W ++ X) = (\sum_{G}, W) \underset{˙}{+} (\sum_{G}, X) \leftrightarrow \sum_{G} (\emptyset ++ X) = 0_{G} \underset{˙}{+} (\sum_{G}, X))$
11		oveq2	$⊢ X = \emptyset \to W ++ X = W ++ \emptyset$
12	11	oveq2d	$⊢ X = \emptyset \to \sum_{G} (W ++ X) = \sum_{G} (W ++ \emptyset)$
13		oveq2	$⊢ X = \emptyset \to \sum_{G} X = \sum_{G} \emptyset$
14	13 7	syl6eq	$⊢ X = \emptyset \to \sum_{G} X = 0_{G}$
15	14	oveq2d	$⊢ X = \emptyset \to (\sum_{G}, W) \underset{˙}{+} (\sum_{G}, X) = (\sum_{G}, W) \underset{˙}{+} 0_{G}$
16	12 15	eqeq12d	$⊢ X = \emptyset \to (\sum_{G} (W ++ X) = (\sum_{G}, W) \underset{˙}{+} (\sum_{G}, X) \leftrightarrow \sum_{G} (W ++ \emptyset) = (\sum_{G}, W) \underset{˙}{+} 0_{G})$
17		mndsgrp	Could not format ( G e. Mnd -> G e. Smgrp ) : No typesetting found for \|- ( G e. Mnd -> G e. Smgrp ) with typecode \|-
18	17	3ad2ant1	Could not format ( ( G e. Mnd /\ W e. Word B /\ X e. Word B ) -> G e. Smgrp ) : No typesetting found for \|- ( ( G e. Mnd /\ W e. Word B /\ X e. Word B ) -> G e. Smgrp ) with typecode \|-
19	18	ad2antrr	Could not format ( ( ( ( G e. Mnd /\ W e. Word B /\ X e. Word B ) /\ W =/= (/) ) /\ X =/= (/) ) -> G e. Smgrp ) : No typesetting found for \|- ( ( ( ( G e. Mnd /\ W e. Word B /\ X e. Word B ) /\ W =/= (/) ) /\ X =/= (/) ) -> G e. Smgrp ) with typecode \|-
20		3simpc	$⊢ (G \in Mnd \land W \in Word B \land X \in Word B) \to (W \in Word B \land X \in Word B)$
21	20	ad2antrr	$⊢ (((G \in Mnd \land W \in Word B \land X \in Word B) \land W \neq \emptyset) \land X \neq \emptyset) \to (W \in Word B \land X \in Word B)$
22		simpr	$⊢ ((G \in Mnd \land W \in Word B \land X \in Word B) \land W \neq \emptyset) \to W \neq \emptyset$
23	22	anim1i	$⊢ (((G \in Mnd \land W \in Word B \land X \in Word B) \land W \neq \emptyset) \land X \neq \emptyset) \to (W \neq \emptyset \land X \neq \emptyset)$
24	1 2	gsumsgrpccat	Could not format ( ( G e. Smgrp /\ ( W e. Word B /\ X e. Word B ) /\ ( W =/= (/) /\ X =/= (/) ) ) -> ( G gsum ( W ++ X ) ) = ( ( G gsum W ) .+ ( G gsum X ) ) ) : No typesetting found for \|- ( ( G e. Smgrp /\ ( W e. Word B /\ X e. Word B ) /\ ( W =/= (/) /\ X =/= (/) ) ) -> ( G gsum ( W ++ X ) ) = ( ( G gsum W ) .+ ( G gsum X ) ) ) with typecode \|-
25	19 21 23 24	syl3anc	$⊢ (((G \in Mnd \land W \in Word B \land X \in Word B) \land W \neq \emptyset) \land X \neq \emptyset) \to \sum_{G} (W ++ X) = (\sum_{G}, W) \underset{˙}{+} (\sum_{G}, X)$
26		simpl2	$⊢ ((G \in Mnd \land W \in Word B \land X \in Word B) \land W \neq \emptyset) \to W \in Word B$
27		ccatrid	$⊢ W \in Word B \to W ++ \emptyset = W$
28	26 27	syl	$⊢ ((G \in Mnd \land W \in Word B \land X \in Word B) \land W \neq \emptyset) \to W ++ \emptyset = W$
29	28	oveq2d	$⊢ ((G \in Mnd \land W \in Word B \land X \in Word B) \land W \neq \emptyset) \to \sum_{G} (W ++ \emptyset) = \sum_{G} W$
30		simpl1	$⊢ ((G \in Mnd \land W \in Word B \land X \in Word B) \land W \neq \emptyset) \to G \in Mnd$
31	1	gsumwcl	$⊢ (G \in Mnd \land W \in Word B) \to \sum_{G} W \in B$
32	31	3adant3	$⊢ (G \in Mnd \land W \in Word B \land X \in Word B) \to \sum_{G} W \in B$
33	32	adantr	$⊢ ((G \in Mnd \land W \in Word B \land X \in Word B) \land W \neq \emptyset) \to \sum_{G} W \in B$
34	1 2 6	mndrid	$⊢ (G \in Mnd \land \sum_{G} W \in B) \to (\sum_{G}, W) \underset{˙}{+} 0_{G} = \sum_{G} W$
35	30 33 34	syl2anc	$⊢ ((G \in Mnd \land W \in Word B \land X \in Word B) \land W \neq \emptyset) \to (\sum_{G}, W) \underset{˙}{+} 0_{G} = \sum_{G} W$
36	29 35	eqtr4d	$⊢ ((G \in Mnd \land W \in Word B \land X \in Word B) \land W \neq \emptyset) \to \sum_{G} (W ++ \emptyset) = (\sum_{G}, W) \underset{˙}{+} 0_{G}$
37	16 25 36	pm2.61ne	$⊢ ((G \in Mnd \land W \in Word B \land X \in Word B) \land W \neq \emptyset) \to \sum_{G} (W ++ X) = (\sum_{G}, W) \underset{˙}{+} (\sum_{G}, X)$
38		ccatlid	$⊢ X \in Word B \to \emptyset ++ X = X$
39	38	3ad2ant3	$⊢ (G \in Mnd \land W \in Word B \land X \in Word B) \to \emptyset ++ X = X$
40	39	oveq2d	$⊢ (G \in Mnd \land W \in Word B \land X \in Word B) \to \sum_{G} (\emptyset ++ X) = \sum_{G} X$
41		simp1	$⊢ (G \in Mnd \land W \in Word B \land X \in Word B) \to G \in Mnd$
42	1	gsumwcl	$⊢ (G \in Mnd \land X \in Word B) \to \sum_{G} X \in B$
43	1 2 6	mndlid	$⊢ (G \in Mnd \land \sum_{G} X \in B) \to 0_{G} \underset{˙}{+} (\sum_{G}, X) = \sum_{G} X$
44	41 42 43	3imp3i2an	$⊢ (G \in Mnd \land W \in Word B \land X \in Word B) \to 0_{G} \underset{˙}{+} (\sum_{G}, X) = \sum_{G} X$
45	40 44	eqtr4d	$⊢ (G \in Mnd \land W \in Word B \land X \in Word B) \to \sum_{G} (\emptyset ++ X) = 0_{G} \underset{˙}{+} (\sum_{G}, X)$
46	10 37 45	pm2.61ne	$⊢ (G \in Mnd \land W \in Word B \land X \in Word B) \to \sum_{G} (W ++ X) = (\sum_{G}, W) \underset{˙}{+} (\sum_{G}, X)$

Metamath Proof Explorer

Theorem gsumccat

Proof