gsmsymgrfixlem1

	Ref	Expression
Hypotheses	gsmsymgrfix.s	$⊢ S = SymGrp (N)$
	gsmsymgrfix.b	$⊢ B = {Base}_{S}$
Assertion	gsmsymgrfixlem1	$⊢ ((W \in Word B \land P \in B) \land (N \in Fin \land K \in N) \land (\forall i \in (0 ..^\|W\|) W (i) (K) = K \to (\sum_{S}, W) (K) = K)) \to (\forall i \in (0 ..^\|W\| + 1) (W ++ ⟨“ P ”⟩) (i) (K) = K \to (\sum_{S}, (W ++ ⟨“ P ”⟩)) (K) = K)$

Proof

Step	Hyp	Ref	Expression
1		gsmsymgrfix.s	$⊢ S = SymGrp (N)$
2		gsmsymgrfix.b	$⊢ B = {Base}_{S}$
3		lencl	$⊢ W \in Word B \to \|W\| \in ℕ_{0}$
4		elnn0uz	$⊢ \|W\| \in ℕ_{0} \leftrightarrow \|W\| \in ℤ_{\geq 0}$
5	3 4	sylib	$⊢ W \in Word B \to \|W\| \in ℤ_{\geq 0}$
6	5	adantr	$⊢ (W \in Word B \land P \in B) \to \|W\| \in ℤ_{\geq 0}$
7	6	3ad2ant1	$⊢ ((W \in Word B \land P \in B) \land (N \in Fin \land K \in N) \land (\forall i \in (0 ..^\|W\|) W (i) (K) = K \to (\sum_{S}, W) (K) = K)) \to \|W\| \in ℤ_{\geq 0}$
8		fzosplitsn	$⊢ \|W\| \in ℤ_{\geq 0} \to (0 ..^\|W\| + 1) = (0 ..^\|W\|) \cup \{\|W\|\}$
9	7 8	syl	$⊢ ((W \in Word B \land P \in B) \land (N \in Fin \land K \in N) \land (\forall i \in (0 ..^\|W\|) W (i) (K) = K \to (\sum_{S}, W) (K) = K)) \to (0 ..^\|W\| + 1) = (0 ..^\|W\|) \cup \{\|W\|\}$
10	9	raleqdv	$⊢ ((W \in Word B \land P \in B) \land (N \in Fin \land K \in N) \land (\forall i \in (0 ..^\|W\|) W (i) (K) = K \to (\sum_{S}, W) (K) = K)) \to (\forall i \in (0 ..^\|W\| + 1) (W ++ ⟨“ P ”⟩) (i) (K) = K \leftrightarrow \forall i \in ((0 ..^\|W\|) \cup \{\|W\|\}) (W ++ ⟨“ P ”⟩) (i) (K) = K)$
11	3	adantr	$⊢ (W \in Word B \land P \in B) \to \|W\| \in ℕ_{0}$
12	11	3ad2ant1	$⊢ ((W \in Word B \land P \in B) \land (N \in Fin \land K \in N) \land (\forall i \in (0 ..^\|W\|) W (i) (K) = K \to (\sum_{S}, W) (K) = K)) \to \|W\| \in ℕ_{0}$
13		fveq2	$⊢ i = \|W\| \to (W ++ ⟨“ P ”⟩) (i) = (W ++ ⟨“ P ”⟩) (\|W\|)$
14	13	fveq1d	$⊢ i = \|W\| \to (W ++ ⟨“ P ”⟩) (i) (K) = (W ++ ⟨“ P ”⟩) (\|W\|) (K)$
15	14	eqeq1d	$⊢ i = \|W\| \to ((W ++ ⟨“ P ”⟩) (i) (K) = K \leftrightarrow (W ++ ⟨“ P ”⟩) (\|W\|) (K) = K)$
16	15	ralunsn	$⊢ \|W\| \in ℕ_{0} \to (\forall i \in ((0 ..^\|W\|) \cup \{\|W\|\}) (W ++ ⟨“ P ”⟩) (i) (K) = K \leftrightarrow (\forall i \in (0 ..^\|W\|) (W ++ ⟨“ P ”⟩) (i) (K) = K \land (W ++ ⟨“ P ”⟩) (\|W\|) (K) = K))$
17	12 16	syl	$⊢ ((W \in Word B \land P \in B) \land (N \in Fin \land K \in N) \land (\forall i \in (0 ..^\|W\|) W (i) (K) = K \to (\sum_{S}, W) (K) = K)) \to (\forall i \in ((0 ..^\|W\|) \cup \{\|W\|\}) (W ++ ⟨“ P ”⟩) (i) (K) = K \leftrightarrow (\forall i \in (0 ..^\|W\|) (W ++ ⟨“ P ”⟩) (i) (K) = K \land (W ++ ⟨“ P ”⟩) (\|W\|) (K) = K))$
18	10 17	bitrd	$⊢ ((W \in Word B \land P \in B) \land (N \in Fin \land K \in N) \land (\forall i \in (0 ..^\|W\|) W (i) (K) = K \to (\sum_{S}, W) (K) = K)) \to (\forall i \in (0 ..^\|W\| + 1) (W ++ ⟨“ P ”⟩) (i) (K) = K \leftrightarrow (\forall i \in (0 ..^\|W\|) (W ++ ⟨“ P ”⟩) (i) (K) = K \land (W ++ ⟨“ P ”⟩) (\|W\|) (K) = K))$
19		eqidd	$⊢ (W \in Word B \land P \in B) \to \|W\| = \|W\|$
20		ccats1val2	$⊢ (W \in Word B \land P \in B \land \|W\| = \|W\|) \to (W ++ ⟨“ P ”⟩) (\|W\|) = P$
21	20	fveq1d	$⊢ (W \in Word B \land P \in B \land \|W\| = \|W\|) \to (W ++ ⟨“ P ”⟩) (\|W\|) (K) = P (K)$
22	21	eqeq1d	$⊢ (W \in Word B \land P \in B \land \|W\| = \|W\|) \to ((W ++ ⟨“ P ”⟩) (\|W\|) (K) = K \leftrightarrow P (K) = K)$
23	19 22	mpd3an3	$⊢ (W \in Word B \land P \in B) \to ((W ++ ⟨“ P ”⟩) (\|W\|) (K) = K \leftrightarrow P (K) = K)$
24	23	3ad2ant1	$⊢ ((W \in Word B \land P \in B) \land (N \in Fin \land K \in N) \land (\forall i \in (0 ..^\|W\|) W (i) (K) = K \to (\sum_{S}, W) (K) = K)) \to ((W ++ ⟨“ P ”⟩) (\|W\|) (K) = K \leftrightarrow P (K) = K)$
25		simprl	$⊢ ((W \in Word B \land P \in B) \land (N \in Fin \land K \in N)) \to N \in Fin$
26		simpll	$⊢ ((W \in Word B \land P \in B) \land (N \in Fin \land K \in N)) \to W \in Word B$
27		simplr	$⊢ ((W \in Word B \land P \in B) \land (N \in Fin \land K \in N)) \to P \in B$
28	1 2	gsumccatsymgsn	$⊢ (N \in Fin \land W \in Word B \land P \in B) \to \sum_{S} (W ++ ⟨“ P ”⟩) = (\sum_{S}, W) \circ P$
29	28	fveq1d	$⊢ (N \in Fin \land W \in Word B \land P \in B) \to (\sum_{S}, (W ++ ⟨“ P ”⟩)) (K) = ((\sum_{S}, W) \circ P) (K)$
30	25 26 27 29	syl3anc	$⊢ ((W \in Word B \land P \in B) \land (N \in Fin \land K \in N)) \to (\sum_{S}, (W ++ ⟨“ P ”⟩)) (K) = ((\sum_{S}, W) \circ P) (K)$
31	30	3adant3	$⊢ ((W \in Word B \land P \in B) \land (N \in Fin \land K \in N) \land (\forall i \in (0 ..^\|W\|) W (i) (K) = K \to (\sum_{S}, W) (K) = K)) \to (\sum_{S}, (W ++ ⟨“ P ”⟩)) (K) = ((\sum_{S}, W) \circ P) (K)$
32	31	adantr	$⊢ (((W \in Word B \land P \in B) \land (N \in Fin \land K \in N) \land (\forall i \in (0 ..^\|W\|) W (i) (K) = K \to (\sum_{S}, W) (K) = K)) \land (P (K) = K \land \forall i \in (0 ..^\|W\|) (W ++ ⟨“ P ”⟩) (i) (K) = K)) \to (\sum_{S}, (W ++ ⟨“ P ”⟩)) (K) = ((\sum_{S}, W) \circ P) (K)$
33	1 2	symgbasf	$⊢ P \in B \to P : N ⟶ N$
34	33	ffnd	$⊢ P \in B \to P Fn N$
35	34	adantl	$⊢ (W \in Word B \land P \in B) \to P Fn N$
36		simpr	$⊢ (N \in Fin \land K \in N) \to K \in N$
37		fvco2	$⊢ (P Fn N \land K \in N) \to ((\sum_{S}, W) \circ P) (K) = (\sum_{S}, W) (P (K))$
38	35 36 37	syl2an	$⊢ ((W \in Word B \land P \in B) \land (N \in Fin \land K \in N)) \to ((\sum_{S}, W) \circ P) (K) = (\sum_{S}, W) (P (K))$
39	38	3adant3	$⊢ ((W \in Word B \land P \in B) \land (N \in Fin \land K \in N) \land (\forall i \in (0 ..^\|W\|) W (i) (K) = K \to (\sum_{S}, W) (K) = K)) \to ((\sum_{S}, W) \circ P) (K) = (\sum_{S}, W) (P (K))$
40	39	adantr	$⊢ (((W \in Word B \land P \in B) \land (N \in Fin \land K \in N) \land (\forall i \in (0 ..^\|W\|) W (i) (K) = K \to (\sum_{S}, W) (K) = K)) \land (P (K) = K \land \forall i \in (0 ..^\|W\|) (W ++ ⟨“ P ”⟩) (i) (K) = K)) \to ((\sum_{S}, W) \circ P) (K) = (\sum_{S}, W) (P (K))$
41		fveq2	$⊢ P (K) = K \to (\sum_{S}, W) (P (K)) = (\sum_{S}, W) (K)$
42	41	ad2antrl	$⊢ (((W \in Word B \land P \in B) \land (N \in Fin \land K \in N) \land (\forall i \in (0 ..^\|W\|) W (i) (K) = K \to (\sum_{S}, W) (K) = K)) \land (P (K) = K \land \forall i \in (0 ..^\|W\|) (W ++ ⟨“ P ”⟩) (i) (K) = K)) \to (\sum_{S}, W) (P (K)) = (\sum_{S}, W) (K)$
43		ccats1val1	$⊢ (W \in Word B \land i \in (0 ..^\|W\|)) \to (W ++ ⟨“ P ”⟩) (i) = W (i)$
44	43	ad4ant14	$⊢ (((W \in Word B \land P \in B) \land (N \in Fin \land K \in N)) \land i \in (0 ..^\|W\|)) \to (W ++ ⟨“ P ”⟩) (i) = W (i)$
45	44	fveq1d	$⊢ (((W \in Word B \land P \in B) \land (N \in Fin \land K \in N)) \land i \in (0 ..^\|W\|)) \to (W ++ ⟨“ P ”⟩) (i) (K) = W (i) (K)$
46	45	eqeq1d	$⊢ (((W \in Word B \land P \in B) \land (N \in Fin \land K \in N)) \land i \in (0 ..^\|W\|)) \to ((W ++ ⟨“ P ”⟩) (i) (K) = K \leftrightarrow W (i) (K) = K)$
47	46	ralbidva	$⊢ ((W \in Word B \land P \in B) \land (N \in Fin \land K \in N)) \to (\forall i \in (0 ..^\|W\|) (W ++ ⟨“ P ”⟩) (i) (K) = K \leftrightarrow \forall i \in (0 ..^\|W\|) W (i) (K) = K)$
48	47	biimpd	$⊢ ((W \in Word B \land P \in B) \land (N \in Fin \land K \in N)) \to (\forall i \in (0 ..^\|W\|) (W ++ ⟨“ P ”⟩) (i) (K) = K \to \forall i \in (0 ..^\|W\|) W (i) (K) = K)$
49	48	adantld	$⊢ ((W \in Word B \land P \in B) \land (N \in Fin \land K \in N)) \to ((P (K) = K \land \forall i \in (0 ..^\|W\|) (W ++ ⟨“ P ”⟩) (i) (K) = K) \to \forall i \in (0 ..^\|W\|) W (i) (K) = K)$
50	49	3adant3	$⊢ ((W \in Word B \land P \in B) \land (N \in Fin \land K \in N) \land (\forall i \in (0 ..^\|W\|) W (i) (K) = K \to (\sum_{S}, W) (K) = K)) \to ((P (K) = K \land \forall i \in (0 ..^\|W\|) (W ++ ⟨“ P ”⟩) (i) (K) = K) \to \forall i \in (0 ..^\|W\|) W (i) (K) = K)$
51		simp3	$⊢ ((W \in Word B \land P \in B) \land (N \in Fin \land K \in N) \land (\forall i \in (0 ..^\|W\|) W (i) (K) = K \to (\sum_{S}, W) (K) = K)) \to (\forall i \in (0 ..^\|W\|) W (i) (K) = K \to (\sum_{S}, W) (K) = K)$
52	50 51	syld	$⊢ ((W \in Word B \land P \in B) \land (N \in Fin \land K \in N) \land (\forall i \in (0 ..^\|W\|) W (i) (K) = K \to (\sum_{S}, W) (K) = K)) \to ((P (K) = K \land \forall i \in (0 ..^\|W\|) (W ++ ⟨“ P ”⟩) (i) (K) = K) \to (\sum_{S}, W) (K) = K)$
53	52	imp	$⊢ (((W \in Word B \land P \in B) \land (N \in Fin \land K \in N) \land (\forall i \in (0 ..^\|W\|) W (i) (K) = K \to (\sum_{S}, W) (K) = K)) \land (P (K) = K \land \forall i \in (0 ..^\|W\|) (W ++ ⟨“ P ”⟩) (i) (K) = K)) \to (\sum_{S}, W) (K) = K$
54	42 53	eqtrd	$⊢ (((W \in Word B \land P \in B) \land (N \in Fin \land K \in N) \land (\forall i \in (0 ..^\|W\|) W (i) (K) = K \to (\sum_{S}, W) (K) = K)) \land (P (K) = K \land \forall i \in (0 ..^\|W\|) (W ++ ⟨“ P ”⟩) (i) (K) = K)) \to (\sum_{S}, W) (P (K)) = K$
55	32 40 54	3eqtrd	$⊢ (((W \in Word B \land P \in B) \land (N \in Fin \land K \in N) \land (\forall i \in (0 ..^\|W\|) W (i) (K) = K \to (\sum_{S}, W) (K) = K)) \land (P (K) = K \land \forall i \in (0 ..^\|W\|) (W ++ ⟨“ P ”⟩) (i) (K) = K)) \to (\sum_{S}, (W ++ ⟨“ P ”⟩)) (K) = K$
56	55	exp32	$⊢ ((W \in Word B \land P \in B) \land (N \in Fin \land K \in N) \land (\forall i \in (0 ..^\|W\|) W (i) (K) = K \to (\sum_{S}, W) (K) = K)) \to (P (K) = K \to (\forall i \in (0 ..^\|W\|) (W ++ ⟨“ P ”⟩) (i) (K) = K \to (\sum_{S}, (W ++ ⟨“ P ”⟩)) (K) = K))$
57	24 56	sylbid	$⊢ ((W \in Word B \land P \in B) \land (N \in Fin \land K \in N) \land (\forall i \in (0 ..^\|W\|) W (i) (K) = K \to (\sum_{S}, W) (K) = K)) \to ((W ++ ⟨“ P ”⟩) (\|W\|) (K) = K \to (\forall i \in (0 ..^\|W\|) (W ++ ⟨“ P ”⟩) (i) (K) = K \to (\sum_{S}, (W ++ ⟨“ P ”⟩)) (K) = K))$
58	57	impcomd	$⊢ ((W \in Word B \land P \in B) \land (N \in Fin \land K \in N) \land (\forall i \in (0 ..^\|W\|) W (i) (K) = K \to (\sum_{S}, W) (K) = K)) \to ((\forall i \in (0 ..^\|W\|) (W ++ ⟨“ P ”⟩) (i) (K) = K \land (W ++ ⟨“ P ”⟩) (\|W\|) (K) = K) \to (\sum_{S}, (W ++ ⟨“ P ”⟩)) (K) = K)$
59	18 58	sylbid	$⊢ ((W \in Word B \land P \in B) \land (N \in Fin \land K \in N) \land (\forall i \in (0 ..^\|W\|) W (i) (K) = K \to (\sum_{S}, W) (K) = K)) \to (\forall i \in (0 ..^\|W\| + 1) (W ++ ⟨“ P ”⟩) (i) (K) = K \to (\sum_{S}, (W ++ ⟨“ P ”⟩)) (K) = K)$

Metamath Proof Explorer

Theorem gsmsymgrfixlem1

Proof