gsmsymgreqlem1

	Ref	Expression
Hypotheses	gsmsymgrfix.s	$⊢ S = SymGrp (N)$
	gsmsymgrfix.b	$⊢ B = {Base}_{S}$
	gsmsymgreq.z	$⊢ Z = SymGrp (M)$
	gsmsymgreq.p	$⊢ P = {Base}_{Z}$
	gsmsymgreq.i	$⊢ I = N \cap M$
Assertion	gsmsymgreqlem1	$⊢ ((N \in Fin \land M \in Fin \land J \in I) \land ((X \in Word B \land C \in B) \land (Y \in Word P \land R \in P) \land \|X\| = \|Y\|)) \to ((\forall n \in I (\sum_{S}, X) (n) = (\sum_{Z}, Y) (n) \land C (J) = R (J)) \to (\sum_{S}, (X ++ ⟨“ C ”⟩)) (J) = (\sum_{Z}, (Y ++ ⟨“ R ”⟩)) (J))$

Proof

Step	Hyp	Ref	Expression
1		gsmsymgrfix.s	$⊢ S = SymGrp (N)$
2		gsmsymgrfix.b	$⊢ B = {Base}_{S}$
3		gsmsymgreq.z	$⊢ Z = SymGrp (M)$
4		gsmsymgreq.p	$⊢ P = {Base}_{Z}$
5		gsmsymgreq.i	$⊢ I = N \cap M$
6		simpr	$⊢ (X \in Word B \land C \in B) \to C \in B$
7		simpr	$⊢ (Y \in Word P \land R \in P) \to R \in P$
8	6 7	anim12i	$⊢ ((X \in Word B \land C \in B) \land (Y \in Word P \land R \in P)) \to (C \in B \land R \in P)$
9	8	3adant3	$⊢ ((X \in Word B \land C \in B) \land (Y \in Word P \land R \in P) \land \|X\| = \|Y\|) \to (C \in B \land R \in P)$
10	9	adantl	$⊢ ((N \in Fin \land M \in Fin \land J \in I) \land ((X \in Word B \land C \in B) \land (Y \in Word P \land R \in P) \land \|X\| = \|Y\|)) \to (C \in B \land R \in P)$
11	10	adantr	$⊢ (((N \in Fin \land M \in Fin \land J \in I) \land ((X \in Word B \land C \in B) \land (Y \in Word P \land R \in P) \land \|X\| = \|Y\|)) \land (\forall n \in I (\sum_{S}, X) (n) = (\sum_{Z}, Y) (n) \land C (J) = R (J))) \to (C \in B \land R \in P)$
12		simpll3	$⊢ (((N \in Fin \land M \in Fin \land J \in I) \land ((X \in Word B \land C \in B) \land (Y \in Word P \land R \in P) \land \|X\| = \|Y\|)) \land (\forall n \in I (\sum_{S}, X) (n) = (\sum_{Z}, Y) (n) \land C (J) = R (J))) \to J \in I$
13		simpr	$⊢ (\forall n \in I (\sum_{S}, X) (n) = (\sum_{Z}, Y) (n) \land C (J) = R (J)) \to C (J) = R (J)$
14	13	adantl	$⊢ (((N \in Fin \land M \in Fin \land J \in I) \land ((X \in Word B \land C \in B) \land (Y \in Word P \land R \in P) \land \|X\| = \|Y\|)) \land (\forall n \in I (\sum_{S}, X) (n) = (\sum_{Z}, Y) (n) \land C (J) = R (J))) \to C (J) = R (J)$
15		simprl	$⊢ (((N \in Fin \land M \in Fin \land J \in I) \land ((X \in Word B \land C \in B) \land (Y \in Word P \land R \in P) \land \|X\| = \|Y\|)) \land (\forall n \in I (\sum_{S}, X) (n) = (\sum_{Z}, Y) (n) \land C (J) = R (J))) \to \forall n \in I (\sum_{S}, X) (n) = (\sum_{Z}, Y) (n)$
16	12 14 15	3jca	$⊢ (((N \in Fin \land M \in Fin \land J \in I) \land ((X \in Word B \land C \in B) \land (Y \in Word P \land R \in P) \land \|X\| = \|Y\|)) \land (\forall n \in I (\sum_{S}, X) (n) = (\sum_{Z}, Y) (n) \land C (J) = R (J))) \to (J \in I \land C (J) = R (J) \land \forall n \in I (\sum_{S}, X) (n) = (\sum_{Z}, Y) (n))$
17	1 2 3 4 5	fvcosymgeq	$⊢ (C \in B \land R \in P) \to ((J \in I \land C (J) = R (J) \land \forall n \in I (\sum_{S}, X) (n) = (\sum_{Z}, Y) (n)) \to ((\sum_{S}, X) \circ C) (J) = ((\sum_{Z}, Y) \circ R) (J))$
18	11 16 17	sylc	$⊢ (((N \in Fin \land M \in Fin \land J \in I) \land ((X \in Word B \land C \in B) \land (Y \in Word P \land R \in P) \land \|X\| = \|Y\|)) \land (\forall n \in I (\sum_{S}, X) (n) = (\sum_{Z}, Y) (n) \land C (J) = R (J))) \to ((\sum_{S}, X) \circ C) (J) = ((\sum_{Z}, Y) \circ R) (J)$
19		simpl1	$⊢ ((N \in Fin \land M \in Fin \land J \in I) \land ((X \in Word B \land C \in B) \land (Y \in Word P \land R \in P) \land \|X\| = \|Y\|)) \to N \in Fin$
20		simpr1l	$⊢ ((N \in Fin \land M \in Fin \land J \in I) \land ((X \in Word B \land C \in B) \land (Y \in Word P \land R \in P) \land \|X\| = \|Y\|)) \to X \in Word B$
21		simpr1r	$⊢ ((N \in Fin \land M \in Fin \land J \in I) \land ((X \in Word B \land C \in B) \land (Y \in Word P \land R \in P) \land \|X\| = \|Y\|)) \to C \in B$
22	19 20 21	3jca	$⊢ ((N \in Fin \land M \in Fin \land J \in I) \land ((X \in Word B \land C \in B) \land (Y \in Word P \land R \in P) \land \|X\| = \|Y\|)) \to (N \in Fin \land X \in Word B \land C \in B)$
23	22	adantr	$⊢ (((N \in Fin \land M \in Fin \land J \in I) \land ((X \in Word B \land C \in B) \land (Y \in Word P \land R \in P) \land \|X\| = \|Y\|)) \land (\forall n \in I (\sum_{S}, X) (n) = (\sum_{Z}, Y) (n) \land C (J) = R (J))) \to (N \in Fin \land X \in Word B \land C \in B)$
24	1 2	gsumccatsymgsn	$⊢ (N \in Fin \land X \in Word B \land C \in B) \to \sum_{S} (X ++ ⟨“ C ”⟩) = (\sum_{S}, X) \circ C$
25	23 24	syl	$⊢ (((N \in Fin \land M \in Fin \land J \in I) \land ((X \in Word B \land C \in B) \land (Y \in Word P \land R \in P) \land \|X\| = \|Y\|)) \land (\forall n \in I (\sum_{S}, X) (n) = (\sum_{Z}, Y) (n) \land C (J) = R (J))) \to \sum_{S} (X ++ ⟨“ C ”⟩) = (\sum_{S}, X) \circ C$
26	25	fveq1d	$⊢ (((N \in Fin \land M \in Fin \land J \in I) \land ((X \in Word B \land C \in B) \land (Y \in Word P \land R \in P) \land \|X\| = \|Y\|)) \land (\forall n \in I (\sum_{S}, X) (n) = (\sum_{Z}, Y) (n) \land C (J) = R (J))) \to (\sum_{S}, (X ++ ⟨“ C ”⟩)) (J) = ((\sum_{S}, X) \circ C) (J)$
27		simpl2	$⊢ ((N \in Fin \land M \in Fin \land J \in I) \land ((X \in Word B \land C \in B) \land (Y \in Word P \land R \in P) \land \|X\| = \|Y\|)) \to M \in Fin$
28		simpr2l	$⊢ ((N \in Fin \land M \in Fin \land J \in I) \land ((X \in Word B \land C \in B) \land (Y \in Word P \land R \in P) \land \|X\| = \|Y\|)) \to Y \in Word P$
29		simpr2r	$⊢ ((N \in Fin \land M \in Fin \land J \in I) \land ((X \in Word B \land C \in B) \land (Y \in Word P \land R \in P) \land \|X\| = \|Y\|)) \to R \in P$
30	27 28 29	3jca	$⊢ ((N \in Fin \land M \in Fin \land J \in I) \land ((X \in Word B \land C \in B) \land (Y \in Word P \land R \in P) \land \|X\| = \|Y\|)) \to (M \in Fin \land Y \in Word P \land R \in P)$
31	30	adantr	$⊢ (((N \in Fin \land M \in Fin \land J \in I) \land ((X \in Word B \land C \in B) \land (Y \in Word P \land R \in P) \land \|X\| = \|Y\|)) \land (\forall n \in I (\sum_{S}, X) (n) = (\sum_{Z}, Y) (n) \land C (J) = R (J))) \to (M \in Fin \land Y \in Word P \land R \in P)$
32	3 4	gsumccatsymgsn	$⊢ (M \in Fin \land Y \in Word P \land R \in P) \to \sum_{Z} (Y ++ ⟨“ R ”⟩) = (\sum_{Z}, Y) \circ R$
33	31 32	syl	$⊢ (((N \in Fin \land M \in Fin \land J \in I) \land ((X \in Word B \land C \in B) \land (Y \in Word P \land R \in P) \land \|X\| = \|Y\|)) \land (\forall n \in I (\sum_{S}, X) (n) = (\sum_{Z}, Y) (n) \land C (J) = R (J))) \to \sum_{Z} (Y ++ ⟨“ R ”⟩) = (\sum_{Z}, Y) \circ R$
34	33	fveq1d	$⊢ (((N \in Fin \land M \in Fin \land J \in I) \land ((X \in Word B \land C \in B) \land (Y \in Word P \land R \in P) \land \|X\| = \|Y\|)) \land (\forall n \in I (\sum_{S}, X) (n) = (\sum_{Z}, Y) (n) \land C (J) = R (J))) \to (\sum_{Z}, (Y ++ ⟨“ R ”⟩)) (J) = ((\sum_{Z}, Y) \circ R) (J)$
35	18 26 34	3eqtr4d	$⊢ (((N \in Fin \land M \in Fin \land J \in I) \land ((X \in Word B \land C \in B) \land (Y \in Word P \land R \in P) \land \|X\| = \|Y\|)) \land (\forall n \in I (\sum_{S}, X) (n) = (\sum_{Z}, Y) (n) \land C (J) = R (J))) \to (\sum_{S}, (X ++ ⟨“ C ”⟩)) (J) = (\sum_{Z}, (Y ++ ⟨“ R ”⟩)) (J)$
36	35	ex	$⊢ ((N \in Fin \land M \in Fin \land J \in I) \land ((X \in Word B \land C \in B) \land (Y \in Word P \land R \in P) \land \|X\| = \|Y\|)) \to ((\forall n \in I (\sum_{S}, X) (n) = (\sum_{Z}, Y) (n) \land C (J) = R (J)) \to (\sum_{S}, (X ++ ⟨“ C ”⟩)) (J) = (\sum_{Z}, (Y ++ ⟨“ R ”⟩)) (J))$

Metamath Proof Explorer

Theorem gsmsymgreqlem1

Proof