gsmsymgreqlem2

	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	gsmsymgreqlem2	$⊢ ((N \in Fin \land M \in Fin) \land ((X \in Word B \land C \in B) \land (Y \in Word P \land R \in P) \land \|X\| = \|Y\|)) \to ((\forall i \in (0 ..^\|X\|) \forall n \in I X (i) (n) = Y (i) (n) \to \forall n \in I (\sum_{S}, X) (n) = (\sum_{Z}, Y) (n)) \to (\forall i \in (0 ..^\|X ++ ⟨“ C ”⟩\|) \forall n \in I (X ++ ⟨“ C ”⟩) (i) (n) = (Y ++ ⟨“ R ”⟩) (i) (n) \to \forall n \in I (\sum_{S}, (X ++ ⟨“ C ”⟩)) (n) = (\sum_{Z}, (Y ++ ⟨“ R ”⟩)) (n)))$

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		ccatws1len	$⊢ X \in Word B \to \|X ++ ⟨“ C ”⟩\| = \|X\| + 1$
7	6	oveq2d	$⊢ X \in Word B \to (0 ..^\|X ++ ⟨“ C ”⟩\|) = (0 ..^\|X\| + 1)$
8		lencl	$⊢ X \in Word B \to \|X\| \in ℕ_{0}$
9		elnn0uz	$⊢ \|X\| \in ℕ_{0} \leftrightarrow \|X\| \in ℤ_{\geq 0}$
10	8 9	sylib	$⊢ X \in Word B \to \|X\| \in ℤ_{\geq 0}$
11		fzosplitsn	$⊢ \|X\| \in ℤ_{\geq 0} \to (0 ..^\|X\| + 1) = (0 ..^\|X\|) \cup \{\|X\|\}$
12	10 11	syl	$⊢ X \in Word B \to (0 ..^\|X\| + 1) = (0 ..^\|X\|) \cup \{\|X\|\}$
13	7 12	eqtrd	$⊢ X \in Word B \to (0 ..^\|X ++ ⟨“ C ”⟩\|) = (0 ..^\|X\|) \cup \{\|X\|\}$
14	13	adantr	$⊢ (X \in Word B \land C \in B) \to (0 ..^\|X ++ ⟨“ C ”⟩\|) = (0 ..^\|X\|) \cup \{\|X\|\}$
15	14	3ad2ant1	$⊢ ((X \in Word B \land C \in B) \land (Y \in Word P \land R \in P) \land \|X\| = \|Y\|) \to (0 ..^\|X ++ ⟨“ C ”⟩\|) = (0 ..^\|X\|) \cup \{\|X\|\}$
16	15	raleqdv	$⊢ ((X \in Word B \land C \in B) \land (Y \in Word P \land R \in P) \land \|X\| = \|Y\|) \to (\forall i \in (0 ..^\|X ++ ⟨“ C ”⟩\|) \forall n \in I (X ++ ⟨“ C ”⟩) (i) (n) = (Y ++ ⟨“ R ”⟩) (i) (n) \leftrightarrow \forall i \in ((0 ..^\|X\|) \cup \{\|X\|\}) \forall n \in I (X ++ ⟨“ C ”⟩) (i) (n) = (Y ++ ⟨“ R ”⟩) (i) (n))$
17	8	adantr	$⊢ (X \in Word B \land C \in B) \to \|X\| \in ℕ_{0}$
18	17	3ad2ant1	$⊢ ((X \in Word B \land C \in B) \land (Y \in Word P \land R \in P) \land \|X\| = \|Y\|) \to \|X\| \in ℕ_{0}$
19		fveq2	$⊢ i = \|X\| \to (X ++ ⟨“ C ”⟩) (i) = (X ++ ⟨“ C ”⟩) (\|X\|)$
20	19	fveq1d	$⊢ i = \|X\| \to (X ++ ⟨“ C ”⟩) (i) (n) = (X ++ ⟨“ C ”⟩) (\|X\|) (n)$
21		fveq2	$⊢ i = \|X\| \to (Y ++ ⟨“ R ”⟩) (i) = (Y ++ ⟨“ R ”⟩) (\|X\|)$
22	21	fveq1d	$⊢ i = \|X\| \to (Y ++ ⟨“ R ”⟩) (i) (n) = (Y ++ ⟨“ R ”⟩) (\|X\|) (n)$
23	20 22	eqeq12d	$⊢ i = \|X\| \to ((X ++ ⟨“ C ”⟩) (i) (n) = (Y ++ ⟨“ R ”⟩) (i) (n) \leftrightarrow (X ++ ⟨“ C ”⟩) (\|X\|) (n) = (Y ++ ⟨“ R ”⟩) (\|X\|) (n))$
24	23	ralbidv	$⊢ i = \|X\| \to (\forall n \in I (X ++ ⟨“ C ”⟩) (i) (n) = (Y ++ ⟨“ R ”⟩) (i) (n) \leftrightarrow \forall n \in I (X ++ ⟨“ C ”⟩) (\|X\|) (n) = (Y ++ ⟨“ R ”⟩) (\|X\|) (n))$
25	24	ralunsn	$⊢ \|X\| \in ℕ_{0} \to (\forall i \in ((0 ..^\|X\|) \cup \{\|X\|\}) \forall n \in I (X ++ ⟨“ C ”⟩) (i) (n) = (Y ++ ⟨“ R ”⟩) (i) (n) \leftrightarrow (\forall i \in (0 ..^\|X\|) \forall n \in I (X ++ ⟨“ C ”⟩) (i) (n) = (Y ++ ⟨“ R ”⟩) (i) (n) \land \forall n \in I (X ++ ⟨“ C ”⟩) (\|X\|) (n) = (Y ++ ⟨“ R ”⟩) (\|X\|) (n)))$
26	18 25	syl	$⊢ ((X \in Word B \land C \in B) \land (Y \in Word P \land R \in P) \land \|X\| = \|Y\|) \to (\forall i \in ((0 ..^\|X\|) \cup \{\|X\|\}) \forall n \in I (X ++ ⟨“ C ”⟩) (i) (n) = (Y ++ ⟨“ R ”⟩) (i) (n) \leftrightarrow (\forall i \in (0 ..^\|X\|) \forall n \in I (X ++ ⟨“ C ”⟩) (i) (n) = (Y ++ ⟨“ R ”⟩) (i) (n) \land \forall n \in I (X ++ ⟨“ C ”⟩) (\|X\|) (n) = (Y ++ ⟨“ R ”⟩) (\|X\|) (n)))$
27		simp1l	$⊢ ((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$
28		ccats1val1	$⊢ (X \in Word B \land i \in (0 ..^\|X\|)) \to (X ++ ⟨“ C ”⟩) (i) = X (i)$
29	27 28	sylan	$⊢ (((X \in Word B \land C \in B) \land (Y \in Word P \land R \in P) \land \|X\| = \|Y\|) \land i \in (0 ..^\|X\|)) \to (X ++ ⟨“ C ”⟩) (i) = X (i)$
30	29	fveq1d	$⊢ (((X \in Word B \land C \in B) \land (Y \in Word P \land R \in P) \land \|X\| = \|Y\|) \land i \in (0 ..^\|X\|)) \to (X ++ ⟨“ C ”⟩) (i) (n) = X (i) (n)$
31		simp2l	$⊢ ((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$
32		oveq2	$⊢ \|X\| = \|Y\| \to (0 ..^\|X\|) = (0 ..^\|Y\|)$
33	32	eleq2d	$⊢ \|X\| = \|Y\| \to (i \in (0 ..^\|X\|) \leftrightarrow i \in (0 ..^\|Y\|))$
34	33	biimpd	$⊢ \|X\| = \|Y\| \to (i \in (0 ..^\|X\|) \to i \in (0 ..^\|Y\|))$
35	34	3ad2ant3	$⊢ ((X \in Word B \land C \in B) \land (Y \in Word P \land R \in P) \land \|X\| = \|Y\|) \to (i \in (0 ..^\|X\|) \to i \in (0 ..^\|Y\|))$
36	35	imp	$⊢ (((X \in Word B \land C \in B) \land (Y \in Word P \land R \in P) \land \|X\| = \|Y\|) \land i \in (0 ..^\|X\|)) \to i \in (0 ..^\|Y\|)$
37		ccats1val1	$⊢ (Y \in Word P \land i \in (0 ..^\|Y\|)) \to (Y ++ ⟨“ R ”⟩) (i) = Y (i)$
38	31 36 37	syl2an2r	$⊢ (((X \in Word B \land C \in B) \land (Y \in Word P \land R \in P) \land \|X\| = \|Y\|) \land i \in (0 ..^\|X\|)) \to (Y ++ ⟨“ R ”⟩) (i) = Y (i)$
39	38	fveq1d	$⊢ (((X \in Word B \land C \in B) \land (Y \in Word P \land R \in P) \land \|X\| = \|Y\|) \land i \in (0 ..^\|X\|)) \to (Y ++ ⟨“ R ”⟩) (i) (n) = Y (i) (n)$
40	30 39	eqeq12d	$⊢ (((X \in Word B \land C \in B) \land (Y \in Word P \land R \in P) \land \|X\| = \|Y\|) \land i \in (0 ..^\|X\|)) \to ((X ++ ⟨“ C ”⟩) (i) (n) = (Y ++ ⟨“ R ”⟩) (i) (n) \leftrightarrow X (i) (n) = Y (i) (n))$
41	40	ralbidv	$⊢ (((X \in Word B \land C \in B) \land (Y \in Word P \land R \in P) \land \|X\| = \|Y\|) \land i \in (0 ..^\|X\|)) \to (\forall n \in I (X ++ ⟨“ C ”⟩) (i) (n) = (Y ++ ⟨“ R ”⟩) (i) (n) \leftrightarrow \forall n \in I X (i) (n) = Y (i) (n))$
42	41	ralbidva	$⊢ ((X \in Word B \land C \in B) \land (Y \in Word P \land R \in P) \land \|X\| = \|Y\|) \to (\forall i \in (0 ..^\|X\|) \forall n \in I (X ++ ⟨“ C ”⟩) (i) (n) = (Y ++ ⟨“ R ”⟩) (i) (n) \leftrightarrow \forall i \in (0 ..^\|X\|) \forall n \in I X (i) (n) = Y (i) (n))$
43		eqidd	$⊢ (X \in Word B \land C \in B) \to \|X\| = \|X\|$
44		ccats1val2	$⊢ (X \in Word B \land C \in B \land \|X\| = \|X\|) \to (X ++ ⟨“ C ”⟩) (\|X\|) = C$
45	44	fveq1d	$⊢ (X \in Word B \land C \in B \land \|X\| = \|X\|) \to (X ++ ⟨“ C ”⟩) (\|X\|) (n) = C (n)$
46	43 45	mpd3an3	$⊢ (X \in Word B \land C \in B) \to (X ++ ⟨“ C ”⟩) (\|X\|) (n) = C (n)$
47	46	3ad2ant1	$⊢ ((X \in Word B \land C \in B) \land (Y \in Word P \land R \in P) \land \|X\| = \|Y\|) \to (X ++ ⟨“ C ”⟩) (\|X\|) (n) = C (n)$
48		ccats1val2	$⊢ (Y \in Word P \land R \in P \land \|X\| = \|Y\|) \to (Y ++ ⟨“ R ”⟩) (\|X\|) = R$
49	48	fveq1d	$⊢ (Y \in Word P \land R \in P \land \|X\| = \|Y\|) \to (Y ++ ⟨“ R ”⟩) (\|X\|) (n) = R (n)$
50	49	3expa	$⊢ ((Y \in Word P \land R \in P) \land \|X\| = \|Y\|) \to (Y ++ ⟨“ R ”⟩) (\|X\|) (n) = R (n)$
51	50	3adant1	$⊢ ((X \in Word B \land C \in B) \land (Y \in Word P \land R \in P) \land \|X\| = \|Y\|) \to (Y ++ ⟨“ R ”⟩) (\|X\|) (n) = R (n)$
52	47 51	eqeq12d	$⊢ ((X \in Word B \land C \in B) \land (Y \in Word P \land R \in P) \land \|X\| = \|Y\|) \to ((X ++ ⟨“ C ”⟩) (\|X\|) (n) = (Y ++ ⟨“ R ”⟩) (\|X\|) (n) \leftrightarrow C (n) = R (n))$
53	52	ralbidv	$⊢ ((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 (X ++ ⟨“ C ”⟩) (\|X\|) (n) = (Y ++ ⟨“ R ”⟩) (\|X\|) (n) \leftrightarrow \forall n \in I C (n) = R (n))$
54	42 53	anbi12d	$⊢ ((X \in Word B \land C \in B) \land (Y \in Word P \land R \in P) \land \|X\| = \|Y\|) \to ((\forall i \in (0 ..^\|X\|) \forall n \in I (X ++ ⟨“ C ”⟩) (i) (n) = (Y ++ ⟨“ R ”⟩) (i) (n) \land \forall n \in I (X ++ ⟨“ C ”⟩) (\|X\|) (n) = (Y ++ ⟨“ R ”⟩) (\|X\|) (n)) \leftrightarrow (\forall i \in (0 ..^\|X\|) \forall n \in I X (i) (n) = Y (i) (n) \land \forall n \in I C (n) = R (n)))$
55	16 26 54	3bitrd	$⊢ ((X \in Word B \land C \in B) \land (Y \in Word P \land R \in P) \land \|X\| = \|Y\|) \to (\forall i \in (0 ..^\|X ++ ⟨“ C ”⟩\|) \forall n \in I (X ++ ⟨“ C ”⟩) (i) (n) = (Y ++ ⟨“ R ”⟩) (i) (n) \leftrightarrow (\forall i \in (0 ..^\|X\|) \forall n \in I X (i) (n) = Y (i) (n) \land \forall n \in I C (n) = R (n)))$
56	55	ad2antlr	$⊢ (((N \in Fin \land M \in Fin) \land ((X \in Word B \land C \in B) \land (Y \in Word P \land R \in P) \land \|X\| = \|Y\|)) \land (\forall i \in (0 ..^\|X\|) \forall n \in I X (i) (n) = Y (i) (n) \to \forall n \in I (\sum_{S}, X) (n) = (\sum_{Z}, Y) (n))) \to (\forall i \in (0 ..^\|X ++ ⟨“ C ”⟩\|) \forall n \in I (X ++ ⟨“ C ”⟩) (i) (n) = (Y ++ ⟨“ R ”⟩) (i) (n) \leftrightarrow (\forall i \in (0 ..^\|X\|) \forall n \in I X (i) (n) = Y (i) (n) \land \forall n \in I C (n) = R (n)))$
57		pm3.35	$⊢ (\forall i \in (0 ..^\|X\|) \forall n \in I X (i) (n) = Y (i) (n) \land (\forall i \in (0 ..^\|X\|) \forall n \in I X (i) (n) = Y (i) (n) \to \forall n \in I (\sum_{S}, X) (n) = (\sum_{Z}, Y) (n))) \to \forall n \in I (\sum_{S}, X) (n) = (\sum_{Z}, Y) (n)$
58		fveq2	$⊢ n = j \to (\sum_{S}, X) (n) = (\sum_{S}, X) (j)$
59		fveq2	$⊢ n = j \to (\sum_{Z}, Y) (n) = (\sum_{Z}, Y) (j)$
60	58 59	eqeq12d	$⊢ n = j \to ((\sum_{S}, X) (n) = (\sum_{Z}, Y) (n) \leftrightarrow (\sum_{S}, X) (j) = (\sum_{Z}, Y) (j))$
61	60	cbvralvw	$⊢ \forall n \in I (\sum_{S}, X) (n) = (\sum_{Z}, Y) (n) \leftrightarrow \forall j \in I (\sum_{S}, X) (j) = (\sum_{Z}, Y) (j)$
62		simp-4l	$⊢ ((((N \in Fin \land M \in Fin) \land ((X \in Word B \land C \in B) \land (Y \in Word P \land R \in P) \land \|X\| = \|Y\|)) \land \forall j \in I (\sum_{S}, X) (j) = (\sum_{Z}, Y) (j)) \land n \in I) \to N \in Fin$
63		simp-4r	$⊢ ((((N \in Fin \land M \in Fin) \land ((X \in Word B \land C \in B) \land (Y \in Word P \land R \in P) \land \|X\| = \|Y\|)) \land \forall j \in I (\sum_{S}, X) (j) = (\sum_{Z}, Y) (j)) \land n \in I) \to M \in Fin$
64		simpr	$⊢ ((((N \in Fin \land M \in Fin) \land ((X \in Word B \land C \in B) \land (Y \in Word P \land R \in P) \land \|X\| = \|Y\|)) \land \forall j \in I (\sum_{S}, X) (j) = (\sum_{Z}, Y) (j)) \land n \in I) \to n \in I$
65	62 63 64	3jca	$⊢ ((((N \in Fin \land M \in Fin) \land ((X \in Word B \land C \in B) \land (Y \in Word P \land R \in P) \land \|X\| = \|Y\|)) \land \forall j \in I (\sum_{S}, X) (j) = (\sum_{Z}, Y) (j)) \land n \in I) \to (N \in Fin \land M \in Fin \land n \in I)$
66	65	adantr	$⊢ (((((N \in Fin \land M \in Fin) \land ((X \in Word B \land C \in B) \land (Y \in Word P \land R \in P) \land \|X\| = \|Y\|)) \land \forall j \in I (\sum_{S}, X) (j) = (\sum_{Z}, Y) (j)) \land n \in I) \land C (n) = R (n)) \to (N \in Fin \land M \in Fin \land n \in I)$
67		simp-4r	$⊢ (((((N \in Fin \land M \in Fin) \land ((X \in Word B \land C \in B) \land (Y \in Word P \land R \in P) \land \|X\| = \|Y\|)) \land \forall j \in I (\sum_{S}, X) (j) = (\sum_{Z}, Y) (j)) \land n \in I) \land C (n) = R (n)) \to ((X \in Word B \land C \in B) \land (Y \in Word P \land R \in P) \land \|X\| = \|Y\|)$
68		simplr	$⊢ ((((N \in Fin \land M \in Fin) \land ((X \in Word B \land C \in B) \land (Y \in Word P \land R \in P) \land \|X\| = \|Y\|)) \land \forall j \in I (\sum_{S}, X) (j) = (\sum_{Z}, Y) (j)) \land n \in I) \to \forall j \in I (\sum_{S}, X) (j) = (\sum_{Z}, Y) (j)$
69	68	anim1i	$⊢ (((((N \in Fin \land M \in Fin) \land ((X \in Word B \land C \in B) \land (Y \in Word P \land R \in P) \land \|X\| = \|Y\|)) \land \forall j \in I (\sum_{S}, X) (j) = (\sum_{Z}, Y) (j)) \land n \in I) \land C (n) = R (n)) \to (\forall j \in I (\sum_{S}, X) (j) = (\sum_{Z}, Y) (j) \land C (n) = R (n))$
70	1 2 3 4 5	gsmsymgreqlem1	$⊢ ((N \in Fin \land M \in Fin \land n \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 j \in I (\sum_{S}, X) (j) = (\sum_{Z}, Y) (j) \land C (n) = R (n)) \to (\sum_{S}, (X ++ ⟨“ C ”⟩)) (n) = (\sum_{Z}, (Y ++ ⟨“ R ”⟩)) (n))$
71	70	imp	$⊢ (((N \in Fin \land M \in Fin \land n \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 j \in I (\sum_{S}, X) (j) = (\sum_{Z}, Y) (j) \land C (n) = R (n))) \to (\sum_{S}, (X ++ ⟨“ C ”⟩)) (n) = (\sum_{Z}, (Y ++ ⟨“ R ”⟩)) (n)$
72	66 67 69 71	syl21anc	$⊢ (((((N \in Fin \land M \in Fin) \land ((X \in Word B \land C \in B) \land (Y \in Word P \land R \in P) \land \|X\| = \|Y\|)) \land \forall j \in I (\sum_{S}, X) (j) = (\sum_{Z}, Y) (j)) \land n \in I) \land C (n) = R (n)) \to (\sum_{S}, (X ++ ⟨“ C ”⟩)) (n) = (\sum_{Z}, (Y ++ ⟨“ R ”⟩)) (n)$
73	72	ex	$⊢ ((((N \in Fin \land M \in Fin) \land ((X \in Word B \land C \in B) \land (Y \in Word P \land R \in P) \land \|X\| = \|Y\|)) \land \forall j \in I (\sum_{S}, X) (j) = (\sum_{Z}, Y) (j)) \land n \in I) \to (C (n) = R (n) \to (\sum_{S}, (X ++ ⟨“ C ”⟩)) (n) = (\sum_{Z}, (Y ++ ⟨“ R ”⟩)) (n))$
74	73	ralimdva	$⊢ (((N \in Fin \land M \in Fin) \land ((X \in Word B \land C \in B) \land (Y \in Word P \land R \in P) \land \|X\| = \|Y\|)) \land \forall j \in I (\sum_{S}, X) (j) = (\sum_{Z}, Y) (j)) \to (\forall n \in I C (n) = R (n) \to \forall n \in I (\sum_{S}, (X ++ ⟨“ C ”⟩)) (n) = (\sum_{Z}, (Y ++ ⟨“ R ”⟩)) (n))$
75	74	expcom	$⊢ \forall j \in I (\sum_{S}, X) (j) = (\sum_{Z}, Y) (j) \to (((N \in Fin \land M \in Fin) \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 C (n) = R (n) \to \forall n \in I (\sum_{S}, (X ++ ⟨“ C ”⟩)) (n) = (\sum_{Z}, (Y ++ ⟨“ R ”⟩)) (n)))$
76	61 75	sylbi	$⊢ \forall n \in I (\sum_{S}, X) (n) = (\sum_{Z}, Y) (n) \to (((N \in Fin \land M \in Fin) \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 C (n) = R (n) \to \forall n \in I (\sum_{S}, (X ++ ⟨“ C ”⟩)) (n) = (\sum_{Z}, (Y ++ ⟨“ R ”⟩)) (n)))$
77	76	com23	$⊢ \forall n \in I (\sum_{S}, X) (n) = (\sum_{Z}, Y) (n) \to (\forall n \in I C (n) = R (n) \to (((N \in Fin \land M \in Fin) \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 ++ ⟨“ C ”⟩)) (n) = (\sum_{Z}, (Y ++ ⟨“ R ”⟩)) (n)))$
78	57 77	syl	$⊢ (\forall i \in (0 ..^\|X\|) \forall n \in I X (i) (n) = Y (i) (n) \land (\forall i \in (0 ..^\|X\|) \forall n \in I X (i) (n) = Y (i) (n) \to \forall n \in I (\sum_{S}, X) (n) = (\sum_{Z}, Y) (n))) \to (\forall n \in I C (n) = R (n) \to (((N \in Fin \land M \in Fin) \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 ++ ⟨“ C ”⟩)) (n) = (\sum_{Z}, (Y ++ ⟨“ R ”⟩)) (n)))$
79	78	impancom	$⊢ (\forall i \in (0 ..^\|X\|) \forall n \in I X (i) (n) = Y (i) (n) \land \forall n \in I C (n) = R (n)) \to ((\forall i \in (0 ..^\|X\|) \forall n \in I X (i) (n) = Y (i) (n) \to \forall n \in I (\sum_{S}, X) (n) = (\sum_{Z}, Y) (n)) \to (((N \in Fin \land M \in Fin) \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 ++ ⟨“ C ”⟩)) (n) = (\sum_{Z}, (Y ++ ⟨“ R ”⟩)) (n)))$
80	79	com13	$⊢ ((N \in Fin \land M \in Fin) \land ((X \in Word B \land C \in B) \land (Y \in Word P \land R \in P) \land \|X\| = \|Y\|)) \to ((\forall i \in (0 ..^\|X\|) \forall n \in I X (i) (n) = Y (i) (n) \to \forall n \in I (\sum_{S}, X) (n) = (\sum_{Z}, Y) (n)) \to ((\forall i \in (0 ..^\|X\|) \forall n \in I X (i) (n) = Y (i) (n) \land \forall n \in I C (n) = R (n)) \to \forall n \in I (\sum_{S}, (X ++ ⟨“ C ”⟩)) (n) = (\sum_{Z}, (Y ++ ⟨“ R ”⟩)) (n)))$
81	80	imp	$⊢ (((N \in Fin \land M \in Fin) \land ((X \in Word B \land C \in B) \land (Y \in Word P \land R \in P) \land \|X\| = \|Y\|)) \land (\forall i \in (0 ..^\|X\|) \forall n \in I X (i) (n) = Y (i) (n) \to \forall n \in I (\sum_{S}, X) (n) = (\sum_{Z}, Y) (n))) \to ((\forall i \in (0 ..^\|X\|) \forall n \in I X (i) (n) = Y (i) (n) \land \forall n \in I C (n) = R (n)) \to \forall n \in I (\sum_{S}, (X ++ ⟨“ C ”⟩)) (n) = (\sum_{Z}, (Y ++ ⟨“ R ”⟩)) (n))$
82	56 81	sylbid	$⊢ (((N \in Fin \land M \in Fin) \land ((X \in Word B \land C \in B) \land (Y \in Word P \land R \in P) \land \|X\| = \|Y\|)) \land (\forall i \in (0 ..^\|X\|) \forall n \in I X (i) (n) = Y (i) (n) \to \forall n \in I (\sum_{S}, X) (n) = (\sum_{Z}, Y) (n))) \to (\forall i \in (0 ..^\|X ++ ⟨“ C ”⟩\|) \forall n \in I (X ++ ⟨“ C ”⟩) (i) (n) = (Y ++ ⟨“ R ”⟩) (i) (n) \to \forall n \in I (\sum_{S}, (X ++ ⟨“ C ”⟩)) (n) = (\sum_{Z}, (Y ++ ⟨“ R ”⟩)) (n))$
83	82	ex	$⊢ ((N \in Fin \land M \in Fin) \land ((X \in Word B \land C \in B) \land (Y \in Word P \land R \in P) \land \|X\| = \|Y\|)) \to ((\forall i \in (0 ..^\|X\|) \forall n \in I X (i) (n) = Y (i) (n) \to \forall n \in I (\sum_{S}, X) (n) = (\sum_{Z}, Y) (n)) \to (\forall i \in (0 ..^\|X ++ ⟨“ C ”⟩\|) \forall n \in I (X ++ ⟨“ C ”⟩) (i) (n) = (Y ++ ⟨“ R ”⟩) (i) (n) \to \forall n \in I (\sum_{S}, (X ++ ⟨“ C ”⟩)) (n) = (\sum_{Z}, (Y ++ ⟨“ R ”⟩)) (n)))$

Metamath Proof Explorer

Theorem gsmsymgreqlem2

Proof