1arithidomlem2

Description: Lemma for 1arithidom : induction step. (Contributed by Thierry Arnoux, 27-May-2025)

	Ref	Expression
Hypotheses	1arithidom.u	$⊢ U = Unit (R)$
	1arithidom.i	$⊢ P = RPrime (R)$
	1arithidom.m	$⊢ M = {mulGrp}_{R}$
	1arithidom.t	$⊢ \underset{˙}{\cdot} = \cdot_{R}$
	1arithidom.j	$⊢ J = (0 ..^\|F\|)$
	1arithidom.r	$⊢ φ \to R \in IDomn$
	1arithidom.f	$⊢ φ \to F \in Word P$
	1arithidom.g	$⊢ φ \to G \in Word P$
	1arithidom.1	$⊢ φ \to \sum_{M} F = \sum_{M} G$
	1arithidomlem.1	$⊢ φ \to Q \in P$
	1arithidomlem.2	$⊢ φ \to \forall g \in Word P (\exists k \in U \sum_{M} F = k \underset{˙}{\cdot} (\sum_{M}, g) \to \exists w \exists u \in (U^{(0 ..^\|F\|)}) (w : (0 ..^\|F\|) \underset{1-1 onto}{⟶} (0 ..^\|F\|) \land g = u {\underset{˙}{\cdot}}_{f} (F \circ w)))$
	1arithidomlem.3	$⊢ φ \to H \in Word P$
	1arithidomlem.4	$⊢ φ \to \exists k \in U \sum_{M} (F ++ ⟨“ Q ”⟩) = k \underset{˙}{\cdot} (\sum_{M}, H)$
	1arithidomlem.5	$⊢ φ \to K \in (0 ..^\|H\|)$
	1arithidomlem.6	$⊢ φ \to Q ∥_{r} (R) H (K)$
	1arithidomlem.7	$⊢ φ \to T \in U$
	1arithidomlem.8	$⊢ φ \to T \underset{˙}{\cdot} Q = H (K)$
	1arithidomlem.9	$⊢ φ \to S : (0 ..^\|H\|) \underset{1-1 onto}{⟶} (0 ..^\|H\|)$
	1arithidomlem.10	$⊢ φ \to H \circ S = ((H \circ S) prefix (\|H\| - 1)) ++ ⟨“ H (K) ”⟩$
	1arithidomlem.11	$⊢ φ \to N \in U$
	1arithidomlem.12	$⊢ φ \to \sum_{M} (F ++ ⟨“ Q ”⟩) = N \underset{˙}{\cdot} (\sum_{M}, H)$
	1arithidomlem.13	$⊢ φ \to D \in (U^{(0 ..^\|F\|)})$
	1arithidomlem.14	$⊢ φ \to C : (0 ..^\|F\|) \underset{1-1 onto}{⟶} (0 ..^\|F\|)$
	1arithidomlem.15	$⊢ φ \to (H \circ S) prefix (\|H\| - 1) = D {\underset{˙}{\cdot}}_{f} (F \circ C)$
Assertion	1arithidomlem2	$⊢ φ \to (((C ++ ⟨“ \|F\| ”⟩) \circ S^{-1}) : (0 ..^\|F ++ ⟨“ Q ”⟩\|) \underset{1-1 onto}{⟶} (0 ..^\|F ++ ⟨“ Q ”⟩\|) \land H = ((D ++ ⟨“ T ”⟩) \circ S^{-1}) {\underset{˙}{\cdot}}_{f} ((F ++ ⟨“ Q ”⟩) \circ ((C ++ ⟨“ \|F\| ”⟩) \circ S^{-1})))$

Proof

Step	Hyp	Ref	Expression
1		1arithidom.u	$⊢ U = Unit (R)$
2		1arithidom.i	$⊢ P = RPrime (R)$
3		1arithidom.m	$⊢ M = {mulGrp}_{R}$
4		1arithidom.t	$⊢ \underset{˙}{\cdot} = \cdot_{R}$
5		1arithidom.j	$⊢ J = (0 ..^\|F\|)$
6		1arithidom.r	$⊢ φ \to R \in IDomn$
7		1arithidom.f	$⊢ φ \to F \in Word P$
8		1arithidom.g	$⊢ φ \to G \in Word P$
9		1arithidom.1	$⊢ φ \to \sum_{M} F = \sum_{M} G$
10		1arithidomlem.1	$⊢ φ \to Q \in P$
11		1arithidomlem.2	$⊢ φ \to \forall g \in Word P (\exists k \in U \sum_{M} F = k \underset{˙}{\cdot} (\sum_{M}, g) \to \exists w \exists u \in (U^{(0 ..^\|F\|)}) (w : (0 ..^\|F\|) \underset{1-1 onto}{⟶} (0 ..^\|F\|) \land g = u {\underset{˙}{\cdot}}_{f} (F \circ w)))$
12		1arithidomlem.3	$⊢ φ \to H \in Word P$
13		1arithidomlem.4	$⊢ φ \to \exists k \in U \sum_{M} (F ++ ⟨“ Q ”⟩) = k \underset{˙}{\cdot} (\sum_{M}, H)$
14		1arithidomlem.5	$⊢ φ \to K \in (0 ..^\|H\|)$
15		1arithidomlem.6	$⊢ φ \to Q ∥_{r} (R) H (K)$
16		1arithidomlem.7	$⊢ φ \to T \in U$
17		1arithidomlem.8	$⊢ φ \to T \underset{˙}{\cdot} Q = H (K)$
18		1arithidomlem.9	$⊢ φ \to S : (0 ..^\|H\|) \underset{1-1 onto}{⟶} (0 ..^\|H\|)$
19		1arithidomlem.10	$⊢ φ \to H \circ S = ((H \circ S) prefix (\|H\| - 1)) ++ ⟨“ H (K) ”⟩$
20		1arithidomlem.11	$⊢ φ \to N \in U$
21		1arithidomlem.12	$⊢ φ \to \sum_{M} (F ++ ⟨“ Q ”⟩) = N \underset{˙}{\cdot} (\sum_{M}, H)$
22		1arithidomlem.13	$⊢ φ \to D \in (U^{(0 ..^\|F\|)})$
23		1arithidomlem.14	$⊢ φ \to C : (0 ..^\|F\|) \underset{1-1 onto}{⟶} (0 ..^\|F\|)$
24		1arithidomlem.15	$⊢ φ \to (H \circ S) prefix (\|H\| - 1) = D {\underset{˙}{\cdot}}_{f} (F \circ C)$
25		ccatws1len	$⊢ F \in Word P \to \|F ++ ⟨“ Q ”⟩\| = \|F\| + 1$
26	7 25	syl	$⊢ φ \to \|F ++ ⟨“ Q ”⟩\| = \|F\| + 1$
27	24	dmeqd	$⊢ φ \to dom ((H \circ S) prefix (\|H\| - 1)) = dom (D {\underset{˙}{\cdot}}_{f} (F \circ C))$
28		f1of	$⊢ S : (0 ..^\|H\|) \underset{1-1 onto}{⟶} (0 ..^\|H\|) \to S : (0 ..^\|H\|) ⟶ (0 ..^\|H\|)$
29		iswrdi	$⊢ S : (0 ..^\|H\|) ⟶ (0 ..^\|H\|) \to S \in Word (0 ..^\|H\|)$
30	18 28 29	3syl	$⊢ φ \to S \in Word (0 ..^\|H\|)$
31		eqidd	$⊢ φ \to \|H\| = \|H\|$
32	31 12	wrdfd	$⊢ φ \to H : (0 ..^\|H\|) ⟶ P$
33		wrdco	$⊢ (S \in Word (0 ..^\|H\|) \land H : (0 ..^\|H\|) ⟶ P) \to H \circ S \in Word P$
34	30 32 33	syl2anc	$⊢ φ \to H \circ S \in Word P$
35		elfzo0	$⊢ K \in (0 ..^\|H\|) \leftrightarrow (K \in ℕ_{0} \land \|H\| \in ℕ \land K < \|H\|)$
36	35	simp2bi	$⊢ K \in (0 ..^\|H\|) \to \|H\| \in ℕ$
37		nnm1nn0	$⊢ \|H\| \in ℕ \to \|H\| - 1 \in ℕ_{0}$
38	14 36 37	3syl	$⊢ φ \to \|H\| - 1 \in ℕ_{0}$
39		lenco	$⊢ (S \in Word (0 ..^\|H\|) \land H : (0 ..^\|H\|) ⟶ P) \to \|H \circ S\| = \|S\|$
40	30 32 39	syl2anc	$⊢ φ \to \|H \circ S\| = \|S\|$
41		lencl	$⊢ S \in Word (0 ..^\|H\|) \to \|S\| \in ℕ_{0}$
42	30 41	syl	$⊢ φ \to \|S\| \in ℕ_{0}$
43	40 42	eqeltrd	$⊢ φ \to \|H \circ S\| \in ℕ_{0}$
44		lencl	$⊢ H \in Word P \to \|H\| \in ℕ_{0}$
45	12 44	syl	$⊢ φ \to \|H\| \in ℕ_{0}$
46	45	nn0red	$⊢ φ \to \|H\| \in ℝ$
47	46	lem1d	$⊢ φ \to \|H\| - 1 \leq \|H\|$
48	18 28	syl	$⊢ φ \to S : (0 ..^\|H\|) ⟶ (0 ..^\|H\|)$
49		ffn	$⊢ S : (0 ..^\|H\|) ⟶ (0 ..^\|H\|) \to S Fn (0 ..^\|H\|)$
50		hashfn	$⊢ S Fn (0 ..^\|H\|) \to \|S\| = \|(0 ..^\|H\|)\|$
51	48 49 50	3syl	$⊢ φ \to \|S\| = \|(0 ..^\|H\|)\|$
52		hashfzo0	$⊢ \|H\| \in ℕ_{0} \to \|(0 ..^\|H\|)\| = \|H\|$
53	12 44 52	3syl	$⊢ φ \to \|(0 ..^\|H\|)\| = \|H\|$
54	40 51 53	3eqtrrd	$⊢ φ \to \|H\| = \|H \circ S\|$
55	47 54	breqtrd	$⊢ φ \to \|H\| - 1 \leq \|H \circ S\|$
56		elfz2nn0	$⊢ \|H\| - 1 \in (0 \dots \|H \circ S\|) \leftrightarrow (\|H\| - 1 \in ℕ_{0} \land \|H \circ S\| \in ℕ_{0} \land \|H\| - 1 \leq \|H \circ S\|)$
57	38 43 55 56	syl3anbrc	$⊢ φ \to \|H\| - 1 \in (0 \dots \|H \circ S\|)$
58		pfxfn	$⊢ (H \circ S \in Word P \land \|H\| - 1 \in (0 \dots \|H \circ S\|)) \to ((H \circ S) prefix (\|H\| - 1)) Fn (0 ..^\|H\| - 1)$
59	34 57 58	syl2anc	$⊢ φ \to ((H \circ S) prefix (\|H\| - 1)) Fn (0 ..^\|H\| - 1)$
60	59	fndmd	$⊢ φ \to dom ((H \circ S) prefix (\|H\| - 1)) = (0 ..^\|H\| - 1)$
61		eqid	$⊢ {Base}_{R} = {Base}_{R}$
62	6	idomringd	$⊢ φ \to R \in Ring$
63	62	adantr	$⊢ (φ \land (x \in U \land y \in P)) \to R \in Ring$
64	61 1	unitcl	$⊢ x \in U \to x \in {Base}_{R}$
65	64	ad2antrl	$⊢ (φ \land (x \in U \land y \in P)) \to x \in {Base}_{R}$
66	6	adantr	$⊢ (φ \land (x \in U \land y \in P)) \to R \in IDomn$
67		simprr	$⊢ (φ \land (x \in U \land y \in P)) \to y \in P$
68	61 2 66 67	rprmcl	$⊢ (φ \land (x \in U \land y \in P)) \to y \in {Base}_{R}$
69	61 4 63 65 68	ringcld	$⊢ (φ \land (x \in U \land y \in P)) \to x \underset{˙}{\cdot} y \in {Base}_{R}$
70		elmapi	$⊢ D \in (U^{(0 ..^\|F\|)}) \to D : (0 ..^\|F\|) ⟶ U$
71	22 70	syl	$⊢ φ \to D : (0 ..^\|F\|) ⟶ U$
72		eqidd	$⊢ φ \to \|F\| = \|F\|$
73	72 7	wrdfd	$⊢ φ \to F : (0 ..^\|F\|) ⟶ P$
74		f1of	$⊢ C : (0 ..^\|F\|) \underset{1-1 onto}{⟶} (0 ..^\|F\|) \to C : (0 ..^\|F\|) ⟶ (0 ..^\|F\|)$
75	23 74	syl	$⊢ φ \to C : (0 ..^\|F\|) ⟶ (0 ..^\|F\|)$
76	73 75	fcod	$⊢ φ \to (F \circ C) : (0 ..^\|F\|) ⟶ P$
77		ovexd	$⊢ φ \to (0 ..^\|F\|) \in V$
78		inidm	$⊢ (0 ..^\|F\|) \cap (0 ..^\|F\|) = (0 ..^\|F\|)$
79	69 71 76 77 77 78	off	$⊢ φ \to (D {\underset{˙}{\cdot}}_{f} (F \circ C)) : (0 ..^\|F\|) ⟶ {Base}_{R}$
80	79	fdmd	$⊢ φ \to dom (D {\underset{˙}{\cdot}}_{f} (F \circ C)) = (0 ..^\|F\|)$
81	27 60 80	3eqtr3d	$⊢ φ \to (0 ..^\|H\| - 1) = (0 ..^\|F\|)$
82		lencl	$⊢ F \in Word P \to \|F\| \in ℕ_{0}$
83	7 82	syl	$⊢ φ \to \|F\| \in ℕ_{0}$
84	38 83	fzo0opth	$⊢ φ \to ((0 ..^\|H\| - 1) = (0 ..^\|F\|) \leftrightarrow \|H\| - 1 = \|F\|)$
85	81 84	mpbid	$⊢ φ \to \|H\| - 1 = \|F\|$
86	85	oveq1d	$⊢ φ \to \|H\| - 1 + 1 = \|F\| + 1$
87	14 36	syl	$⊢ φ \to \|H\| \in ℕ$
88	87	nncnd	$⊢ φ \to \|H\| \in ℂ$
89		npcan1	$⊢ \|H\| \in ℂ \to \|H\| - 1 + 1 = \|H\|$
90	88 89	syl	$⊢ φ \to \|H\| - 1 + 1 = \|H\|$
91	86 90	eqtr3d	$⊢ φ \to \|F\| + 1 = \|H\|$
92	26 91	eqtrd	$⊢ φ \to \|F ++ ⟨“ Q ”⟩\| = \|H\|$
93	92	oveq2d	$⊢ φ \to (0 ..^\|F ++ ⟨“ Q ”⟩\|) = (0 ..^\|H\|)$
94		eqid	$⊢ \|C\| = \|C\|$
95		eqid	$⊢ (0 ..^\|C\| + 1) = (0 ..^\|C\| + 1)$
96		f1ofn	$⊢ C : (0 ..^\|F\|) \underset{1-1 onto}{⟶} (0 ..^\|F\|) \to C Fn (0 ..^\|F\|)$
97		hashfn	$⊢ C Fn (0 ..^\|F\|) \to \|C\| = \|(0 ..^\|F\|)\|$
98	23 96 97	3syl	$⊢ φ \to \|C\| = \|(0 ..^\|F\|)\|$
99		hashfzo0	$⊢ \|F\| \in ℕ_{0} \to \|(0 ..^\|F\|)\| = \|F\|$
100	83 99	syl	$⊢ φ \to \|(0 ..^\|F\|)\| = \|F\|$
101	98 100	eqtrd	$⊢ φ \to \|C\| = \|F\|$
102	101	oveq2d	$⊢ φ \to (0 ..^\|C\|) = (0 ..^\|F\|)$
103		f1oeq23	$⊢ ((0 ..^\|C\|) = (0 ..^\|F\|) \land (0 ..^\|C\|) = (0 ..^\|F\|)) \to (C : (0 ..^\|C\|) \underset{1-1 onto}{⟶} (0 ..^\|C\|) \leftrightarrow C : (0 ..^\|F\|) \underset{1-1 onto}{⟶} (0 ..^\|F\|))$
104	103	biimpar	$⊢ (((0 ..^\|C\|) = (0 ..^\|F\|) \land (0 ..^\|C\|) = (0 ..^\|F\|)) \land C : (0 ..^\|F\|) \underset{1-1 onto}{⟶} (0 ..^\|F\|)) \to C : (0 ..^\|C\|) \underset{1-1 onto}{⟶} (0 ..^\|C\|)$
105	102 102 23 104	syl21anc	$⊢ φ \to C : (0 ..^\|C\|) \underset{1-1 onto}{⟶} (0 ..^\|C\|)$
106	94 95 105	ccatws1f1o	$⊢ φ \to (C ++ ⟨“ \|C\| ”⟩) : (0 ..^\|C\| + 1) \underset{1-1 onto}{⟶} (0 ..^\|C\| + 1)$
107	101	s1eqd	$⊢ φ \to ⟨“ \|C\| ”⟩ = ⟨“ \|F\| ”⟩$
108	107	oveq2d	$⊢ φ \to C ++ ⟨“ \|C\| ”⟩ = C ++ ⟨“ \|F\| ”⟩$
109	101	oveq1d	$⊢ φ \to \|C\| + 1 = \|F\| + 1$
110	109 91	eqtrd	$⊢ φ \to \|C\| + 1 = \|H\|$
111	110	oveq2d	$⊢ φ \to (0 ..^\|C\| + 1) = (0 ..^\|H\|)$
112	108 111 111	f1oeq123d	$⊢ φ \to ((C ++ ⟨“ \|C\| ”⟩) : (0 ..^\|C\| + 1) \underset{1-1 onto}{⟶} (0 ..^\|C\| + 1) \leftrightarrow (C ++ ⟨“ \|F\| ”⟩) : (0 ..^\|H\|) \underset{1-1 onto}{⟶} (0 ..^\|H\|))$
113	106 112	mpbid	$⊢ φ \to (C ++ ⟨“ \|F\| ”⟩) : (0 ..^\|H\|) \underset{1-1 onto}{⟶} (0 ..^\|H\|)$
114		f1ocnv	$⊢ S : (0 ..^\|H\|) \underset{1-1 onto}{⟶} (0 ..^\|H\|) \to S^{-1} : (0 ..^\|H\|) \underset{1-1 onto}{⟶} (0 ..^\|H\|)$
115	18 114	syl	$⊢ φ \to S^{-1} : (0 ..^\|H\|) \underset{1-1 onto}{⟶} (0 ..^\|H\|)$
116		f1oco	$⊢ ((C ++ ⟨“ \|F\| ”⟩) : (0 ..^\|H\|) \underset{1-1 onto}{⟶} (0 ..^\|H\|) \land S^{-1} : (0 ..^\|H\|) \underset{1-1 onto}{⟶} (0 ..^\|H\|)) \to ((C ++ ⟨“ \|F\| ”⟩) \circ S^{-1}) : (0 ..^\|H\|) \underset{1-1 onto}{⟶} (0 ..^\|H\|)$
117	113 115 116	syl2anc	$⊢ φ \to ((C ++ ⟨“ \|F\| ”⟩) \circ S^{-1}) : (0 ..^\|H\|) \underset{1-1 onto}{⟶} (0 ..^\|H\|)$
118		f1oeq23	$⊢ ((0 ..^\|F ++ ⟨“ Q ”⟩\|) = (0 ..^\|H\|) \land (0 ..^\|F ++ ⟨“ Q ”⟩\|) = (0 ..^\|H\|)) \to (((C ++ ⟨“ \|F\| ”⟩) \circ S^{-1}) : (0 ..^\|F ++ ⟨“ Q ”⟩\|) \underset{1-1 onto}{⟶} (0 ..^\|F ++ ⟨“ Q ”⟩\|) \leftrightarrow ((C ++ ⟨“ \|F\| ”⟩) \circ S^{-1}) : (0 ..^\|H\|) \underset{1-1 onto}{⟶} (0 ..^\|H\|))$
119	118	biimpar	$⊢ (((0 ..^\|F ++ ⟨“ Q ”⟩\|) = (0 ..^\|H\|) \land (0 ..^\|F ++ ⟨“ Q ”⟩\|) = (0 ..^\|H\|)) \land ((C ++ ⟨“ \|F\| ”⟩) \circ S^{-1}) : (0 ..^\|H\|) \underset{1-1 onto}{⟶} (0 ..^\|H\|)) \to ((C ++ ⟨“ \|F\| ”⟩) \circ S^{-1}) : (0 ..^\|F ++ ⟨“ Q ”⟩\|) \underset{1-1 onto}{⟶} (0 ..^\|F ++ ⟨“ Q ”⟩\|)$
120	93 93 117 119	syl21anc	$⊢ φ \to ((C ++ ⟨“ \|F\| ”⟩) \circ S^{-1}) : (0 ..^\|F ++ ⟨“ Q ”⟩\|) \underset{1-1 onto}{⟶} (0 ..^\|F ++ ⟨“ Q ”⟩\|)$
121		f1ofo	$⊢ S : (0 ..^\|H\|) \underset{1-1 onto}{⟶} (0 ..^\|H\|) \to S : (0 ..^\|H\|) \underset{onto}{⟶} (0 ..^\|H\|)$
122	18 121	syl	$⊢ φ \to S : (0 ..^\|H\|) \underset{onto}{⟶} (0 ..^\|H\|)$
123	32	ffnd	$⊢ φ \to H Fn (0 ..^\|H\|)$
124		iswrdi	$⊢ D : (0 ..^\|F\|) ⟶ U \to D \in Word U$
125	71 124	syl	$⊢ φ \to D \in Word U$
126		ccatws1len	$⊢ D \in Word U \to \|D ++ ⟨“ T ”⟩\| = \|D\| + 1$
127	125 126	syl	$⊢ φ \to \|D ++ ⟨“ T ”⟩\| = \|D\| + 1$
128		elmapfn	$⊢ D \in (U^{(0 ..^\|F\|)}) \to D Fn (0 ..^\|F\|)$
129		hashfn	$⊢ D Fn (0 ..^\|F\|) \to \|D\| = \|(0 ..^\|F\|)\|$
130	22 128 129	3syl	$⊢ φ \to \|D\| = \|(0 ..^\|F\|)\|$
131	130 100	eqtrd	$⊢ φ \to \|D\| = \|F\|$
132	131	oveq1d	$⊢ φ \to \|D\| + 1 = \|F\| + 1$
133	127 132 91	3eqtrd	$⊢ φ \to \|D ++ ⟨“ T ”⟩\| = \|H\|$
134	133	oveq2d	$⊢ φ \to (0 ..^\|D ++ ⟨“ T ”⟩\|) = (0 ..^\|H\|)$
135		eqidd	$⊢ φ \to \|D ++ ⟨“ T ”⟩\| = \|D ++ ⟨“ T ”⟩\|$
136		ccatws1cl	$⊢ (D \in Word U \land T \in U) \to D ++ ⟨“ T ”⟩ \in Word U$
137	125 16 136	syl2anc	$⊢ φ \to D ++ ⟨“ T ”⟩ \in Word U$
138	135 137	wrdfd	$⊢ φ \to (D ++ ⟨“ T ”⟩) : (0 ..^\|D ++ ⟨“ T ”⟩\|) ⟶ U$
139	134 138	feq2dd	$⊢ φ \to (D ++ ⟨“ T ”⟩) : (0 ..^\|H\|) ⟶ U$
140	139	ffnd	$⊢ φ \to (D ++ ⟨“ T ”⟩) Fn (0 ..^\|H\|)$
141		f1of	$⊢ S^{-1} : (0 ..^\|H\|) \underset{1-1 onto}{⟶} (0 ..^\|H\|) \to S^{-1} : (0 ..^\|H\|) ⟶ (0 ..^\|H\|)$
142	18 114 141	3syl	$⊢ φ \to S^{-1} : (0 ..^\|H\|) ⟶ (0 ..^\|H\|)$
143		fnfco	$⊢ ((D ++ ⟨“ T ”⟩) Fn (0 ..^\|H\|) \land S^{-1} : (0 ..^\|H\|) ⟶ (0 ..^\|H\|)) \to ((D ++ ⟨“ T ”⟩) \circ S^{-1}) Fn (0 ..^\|H\|)$
144	140 142 143	syl2anc	$⊢ φ \to ((D ++ ⟨“ T ”⟩) \circ S^{-1}) Fn (0 ..^\|H\|)$
145	91	oveq2d	$⊢ φ \to (0 ..^\|F\| + 1) = (0 ..^\|H\|)$
146	26	eqcomd	$⊢ φ \to \|F\| + 1 = \|F ++ ⟨“ Q ”⟩\|$
147		ccatws1cl	$⊢ (F \in Word P \land Q \in P) \to F ++ ⟨“ Q ”⟩ \in Word P$
148	7 10 147	syl2anc	$⊢ φ \to F ++ ⟨“ Q ”⟩ \in Word P$
149	146 148	wrdfd	$⊢ φ \to (F ++ ⟨“ Q ”⟩) : (0 ..^\|F\| + 1) ⟶ P$
150	145 149	feq2dd	$⊢ φ \to (F ++ ⟨“ Q ”⟩) : (0 ..^\|H\|) ⟶ P$
151	150	ffnd	$⊢ φ \to (F ++ ⟨“ Q ”⟩) Fn (0 ..^\|H\|)$
152		fzossfzop1	$⊢ \|F\| \in ℕ_{0} \to (0 ..^\|F\|) \subseteq (0 ..^\|F\| + 1)$
153	83 152	syl	$⊢ φ \to (0 ..^\|F\|) \subseteq (0 ..^\|F\| + 1)$
154		sswrd	$⊢ (0 ..^\|F\|) \subseteq (0 ..^\|F\| + 1) \to Word (0 ..^\|F\|) \subseteq Word (0 ..^\|F\| + 1)$
155	153 154	syl	$⊢ φ \to Word (0 ..^\|F\|) \subseteq Word (0 ..^\|F\| + 1)$
156		iswrdi	$⊢ C : (0 ..^\|F\|) ⟶ (0 ..^\|F\|) \to C \in Word (0 ..^\|F\|)$
157	75 156	syl	$⊢ φ \to C \in Word (0 ..^\|F\|)$
158	155 157	sseldd	$⊢ φ \to C \in Word (0 ..^\|F\| + 1)$
159		ccatws1len	$⊢ C \in Word (0 ..^\|F\| + 1) \to \|C ++ ⟨“ \|F\| ”⟩\| = \|C\| + 1$
160	158 159	syl	$⊢ φ \to \|C ++ ⟨“ \|F\| ”⟩\| = \|C\| + 1$
161	160 109 91	3eqtrrd	$⊢ φ \to \|H\| = \|C ++ ⟨“ \|F\| ”⟩\|$
162	153 145	sseqtrd	$⊢ φ \to (0 ..^\|F\|) \subseteq (0 ..^\|H\|)$
163	75 162	fssd	$⊢ φ \to C : (0 ..^\|F\|) ⟶ (0 ..^\|H\|)$
164		iswrdi	$⊢ C : (0 ..^\|F\|) ⟶ (0 ..^\|H\|) \to C \in Word (0 ..^\|H\|)$
165	163 164	syl	$⊢ φ \to C \in Word (0 ..^\|H\|)$
166		fzonn0p1	$⊢ \|F\| \in ℕ_{0} \to \|F\| \in (0 ..^\|F\| + 1)$
167	83 166	syl	$⊢ φ \to \|F\| \in (0 ..^\|F\| + 1)$
168	167 145	eleqtrd	$⊢ φ \to \|F\| \in (0 ..^\|H\|)$
169		ccatws1cl	$⊢ (C \in Word (0 ..^\|H\|) \land \|F\| \in (0 ..^\|H\|)) \to C ++ ⟨“ \|F\| ”⟩ \in Word (0 ..^\|H\|)$
170	165 168 169	syl2anc	$⊢ φ \to C ++ ⟨“ \|F\| ”⟩ \in Word (0 ..^\|H\|)$
171	161 170	wrdfd	$⊢ φ \to (C ++ ⟨“ \|F\| ”⟩) : (0 ..^\|H\|) ⟶ (0 ..^\|H\|)$
172	171 142	fcod	$⊢ φ \to ((C ++ ⟨“ \|F\| ”⟩) \circ S^{-1}) : (0 ..^\|H\|) ⟶ (0 ..^\|H\|)$
173		fnfco	$⊢ ((F ++ ⟨“ Q ”⟩) Fn (0 ..^\|H\|) \land ((C ++ ⟨“ \|F\| ”⟩) \circ S^{-1}) : (0 ..^\|H\|) ⟶ (0 ..^\|H\|)) \to ((F ++ ⟨“ Q ”⟩) \circ ((C ++ ⟨“ \|F\| ”⟩) \circ S^{-1})) Fn (0 ..^\|H\|)$
174	151 172 173	syl2anc	$⊢ φ \to ((F ++ ⟨“ Q ”⟩) \circ ((C ++ ⟨“ \|F\| ”⟩) \circ S^{-1})) Fn (0 ..^\|H\|)$
175		ovexd	$⊢ φ \to (0 ..^\|H\|) \in V$
176		inidm	$⊢ (0 ..^\|H\|) \cap (0 ..^\|H\|) = (0 ..^\|H\|)$
177	144 174 175 175 176	offn	$⊢ φ \to (((D ++ ⟨“ T ”⟩) \circ S^{-1}) {\underset{˙}{\cdot}}_{f} ((F ++ ⟨“ Q ”⟩) \circ ((C ++ ⟨“ \|F\| ”⟩) \circ S^{-1}))) Fn (0 ..^\|H\|)$
178		eqid	$⊢ \|F\| = \|F\|$
179	178 7 10 23	ccatws1f1olast	$⊢ φ \to (F ++ ⟨“ Q ”⟩) \circ (C ++ ⟨“ \|F\| ”⟩) = (F \circ C) ++ ⟨“ Q ”⟩$
180	179	oveq2d	$⊢ φ \to (D ++ ⟨“ T ”⟩) {\underset{˙}{\cdot}}_{f} ((F ++ ⟨“ Q ”⟩) \circ (C ++ ⟨“ \|F\| ”⟩)) = (D ++ ⟨“ T ”⟩) {\underset{˙}{\cdot}}_{f} ((F \circ C) ++ ⟨“ Q ”⟩)$
181	16	s1cld	$⊢ φ \to ⟨“ T ”⟩ \in Word U$
182		iswrdi	$⊢ (F \circ C) : (0 ..^\|F\|) ⟶ P \to F \circ C \in Word P$
183	76 182	syl	$⊢ φ \to F \circ C \in Word P$
184	10	s1cld	$⊢ φ \to ⟨“ Q ”⟩ \in Word P$
185		lenco	$⊢ (C \in Word (0 ..^\|F\|) \land F : (0 ..^\|F\|) ⟶ P) \to \|F \circ C\| = \|C\|$
186	157 73 185	syl2anc	$⊢ φ \to \|F \circ C\| = \|C\|$
187	98 186 130	3eqtr4rd	$⊢ φ \to \|D\| = \|F \circ C\|$
188		s1len	$⊢ \|⟨“ T ”⟩\| = 1$
189		s1len	$⊢ \|⟨“ Q ”⟩\| = 1$
190	188 189	eqtr4i	$⊢ \|⟨“ T ”⟩\| = \|⟨“ Q ”⟩\|$
191	190	a1i	$⊢ φ \to \|⟨“ T ”⟩\| = \|⟨“ Q ”⟩\|$
192	125 181 183 184 187 191	ofccat	$⊢ φ \to (D ++ ⟨“ T ”⟩) {\underset{˙}{\cdot}}_{f} ((F \circ C) ++ ⟨“ Q ”⟩) = (D {\underset{˙}{\cdot}}_{f} (F \circ C)) ++ (⟨“ T ”⟩ {\underset{˙}{\cdot}}_{f} ⟨“ Q ”⟩)$
193	180 192	eqtrd	$⊢ φ \to (D ++ ⟨“ T ”⟩) {\underset{˙}{\cdot}}_{f} ((F ++ ⟨“ Q ”⟩) \circ (C ++ ⟨“ \|F\| ”⟩)) = (D {\underset{˙}{\cdot}}_{f} (F \circ C)) ++ (⟨“ T ”⟩ {\underset{˙}{\cdot}}_{f} ⟨“ Q ”⟩)$
194	150 171	fcod	$⊢ φ \to ((F ++ ⟨“ Q ”⟩) \circ (C ++ ⟨“ \|F\| ”⟩)) : (0 ..^\|H\|) ⟶ P$
195	194	ffnd	$⊢ φ \to ((F ++ ⟨“ Q ”⟩) \circ (C ++ ⟨“ \|F\| ”⟩)) Fn (0 ..^\|H\|)$
196	140 195 142 175 175 175 176	ofco	$⊢ φ \to ((D ++ ⟨“ T ”⟩) {\underset{˙}{\cdot}}_{f} ((F ++ ⟨“ Q ”⟩) \circ (C ++ ⟨“ \|F\| ”⟩))) \circ S^{-1} = ((D ++ ⟨“ T ”⟩) \circ S^{-1}) {\underset{˙}{\cdot}}_{f} (((F ++ ⟨“ Q ”⟩) \circ (C ++ ⟨“ \|F\| ”⟩)) \circ S^{-1})$
197	196	coeq1d	$⊢ φ \to (((D ++ ⟨“ T ”⟩) {\underset{˙}{\cdot}}_{f} ((F ++ ⟨“ Q ”⟩) \circ (C ++ ⟨“ \|F\| ”⟩))) \circ S^{-1}) \circ S = (((D ++ ⟨“ T ”⟩) \circ S^{-1}) {\underset{˙}{\cdot}}_{f} (((F ++ ⟨“ Q ”⟩) \circ (C ++ ⟨“ \|F\| ”⟩)) \circ S^{-1})) \circ S$
198		coass	$⊢ (((D ++ ⟨“ T ”⟩) {\underset{˙}{\cdot}}_{f} ((F ++ ⟨“ Q ”⟩) \circ (C ++ ⟨“ \|F\| ”⟩))) \circ S^{-1}) \circ S = ((D ++ ⟨“ T ”⟩) {\underset{˙}{\cdot}}_{f} ((F ++ ⟨“ Q ”⟩) \circ (C ++ ⟨“ \|F\| ”⟩))) \circ (S^{-1} \circ S)$
199	197 198	eqtr3di	$⊢ φ \to (((D ++ ⟨“ T ”⟩) \circ S^{-1}) {\underset{˙}{\cdot}}_{f} (((F ++ ⟨“ Q ”⟩) \circ (C ++ ⟨“ \|F\| ”⟩)) \circ S^{-1})) \circ S = ((D ++ ⟨“ T ”⟩) {\underset{˙}{\cdot}}_{f} ((F ++ ⟨“ Q ”⟩) \circ (C ++ ⟨“ \|F\| ”⟩))) \circ (S^{-1} \circ S)$
200		f1of1	$⊢ S : (0 ..^\|H\|) \underset{1-1 onto}{⟶} (0 ..^\|H\|) \to S : (0 ..^\|H\|) \underset{1-1}{⟶} (0 ..^\|H\|)$
201	18 200	syl	$⊢ φ \to S : (0 ..^\|H\|) \underset{1-1}{⟶} (0 ..^\|H\|)$
202		f1cocnv1	$⊢ S : (0 ..^\|H\|) \underset{1-1}{⟶} (0 ..^\|H\|) \to S^{-1} \circ S = {I ↾}_{(0 ..^\|H\|)}$
203	201 202	syl	$⊢ φ \to S^{-1} \circ S = {I ↾}_{(0 ..^\|H\|)}$
204	203	coeq2d	$⊢ φ \to ((D ++ ⟨“ T ”⟩) {\underset{˙}{\cdot}}_{f} ((F ++ ⟨“ Q ”⟩) \circ (C ++ ⟨“ \|F\| ”⟩))) \circ (S^{-1} \circ S) = ((D ++ ⟨“ T ”⟩) {\underset{˙}{\cdot}}_{f} ((F ++ ⟨“ Q ”⟩) \circ (C ++ ⟨“ \|F\| ”⟩))) \circ ({I ↾}_{(0 ..^\|H\|)})$
205	69 139 194 175 175 176	off	$⊢ φ \to ((D ++ ⟨“ T ”⟩) {\underset{˙}{\cdot}}_{f} ((F ++ ⟨“ Q ”⟩) \circ (C ++ ⟨“ \|F\| ”⟩))) : (0 ..^\|H\|) ⟶ {Base}_{R}$
206		fcoi1	$⊢ ((D ++ ⟨“ T ”⟩) {\underset{˙}{\cdot}}_{f} ((F ++ ⟨“ Q ”⟩) \circ (C ++ ⟨“ \|F\| ”⟩))) : (0 ..^\|H\|) ⟶ {Base}_{R} \to ((D ++ ⟨“ T ”⟩) {\underset{˙}{\cdot}}_{f} ((F ++ ⟨“ Q ”⟩) \circ (C ++ ⟨“ \|F\| ”⟩))) \circ ({I ↾}_{(0 ..^\|H\|)}) = (D ++ ⟨“ T ”⟩) {\underset{˙}{\cdot}}_{f} ((F ++ ⟨“ Q ”⟩) \circ (C ++ ⟨“ \|F\| ”⟩))$
207	205 206	syl	$⊢ φ \to ((D ++ ⟨“ T ”⟩) {\underset{˙}{\cdot}}_{f} ((F ++ ⟨“ Q ”⟩) \circ (C ++ ⟨“ \|F\| ”⟩))) \circ ({I ↾}_{(0 ..^\|H\|)}) = (D ++ ⟨“ T ”⟩) {\underset{˙}{\cdot}}_{f} ((F ++ ⟨“ Q ”⟩) \circ (C ++ ⟨“ \|F\| ”⟩))$
208	199 204 207	3eqtrd	$⊢ φ \to (((D ++ ⟨“ T ”⟩) \circ S^{-1}) {\underset{˙}{\cdot}}_{f} (((F ++ ⟨“ Q ”⟩) \circ (C ++ ⟨“ \|F\| ”⟩)) \circ S^{-1})) \circ S = (D ++ ⟨“ T ”⟩) {\underset{˙}{\cdot}}_{f} ((F ++ ⟨“ Q ”⟩) \circ (C ++ ⟨“ \|F\| ”⟩))$
209		ofs1	$⊢ (T \in U \land Q \in P) \to ⟨“ T ”⟩ {\underset{˙}{\cdot}}_{f} ⟨“ Q ”⟩ = ⟨“ (T \underset{˙}{\cdot} Q) ”⟩$
210	16 10 209	syl2anc	$⊢ φ \to ⟨“ T ”⟩ {\underset{˙}{\cdot}}_{f} ⟨“ Q ”⟩ = ⟨“ (T \underset{˙}{\cdot} Q) ”⟩$
211	17	s1eqd	$⊢ φ \to ⟨“ (T \underset{˙}{\cdot} Q) ”⟩ = ⟨“ H (K) ”⟩$
212	210 211	eqtr2d	$⊢ φ \to ⟨“ H (K) ”⟩ = ⟨“ T ”⟩ {\underset{˙}{\cdot}}_{f} ⟨“ Q ”⟩$
213	24 212	oveq12d	$⊢ φ \to ((H \circ S) prefix (\|H\| - 1)) ++ ⟨“ H (K) ”⟩ = (D {\underset{˙}{\cdot}}_{f} (F \circ C)) ++ (⟨“ T ”⟩ {\underset{˙}{\cdot}}_{f} ⟨“ Q ”⟩)$
214	193 208 213	3eqtr4rd	$⊢ φ \to ((H \circ S) prefix (\|H\| - 1)) ++ ⟨“ H (K) ”⟩ = (((D ++ ⟨“ T ”⟩) \circ S^{-1}) {\underset{˙}{\cdot}}_{f} (((F ++ ⟨“ Q ”⟩) \circ (C ++ ⟨“ \|F\| ”⟩)) \circ S^{-1})) \circ S$
215		coass	$⊢ ((F ++ ⟨“ Q ”⟩) \circ (C ++ ⟨“ \|F\| ”⟩)) \circ S^{-1} = (F ++ ⟨“ Q ”⟩) \circ ((C ++ ⟨“ \|F\| ”⟩) \circ S^{-1})$
216	215	oveq2i	$⊢ ((D ++ ⟨“ T ”⟩) \circ S^{-1}) {\underset{˙}{\cdot}}_{f} (((F ++ ⟨“ Q ”⟩) \circ (C ++ ⟨“ \|F\| ”⟩)) \circ S^{-1}) = ((D ++ ⟨“ T ”⟩) \circ S^{-1}) {\underset{˙}{\cdot}}_{f} ((F ++ ⟨“ Q ”⟩) \circ ((C ++ ⟨“ \|F\| ”⟩) \circ S^{-1}))$
217	216	coeq1i	$⊢ (((D ++ ⟨“ T ”⟩) \circ S^{-1}) {\underset{˙}{\cdot}}_{f} (((F ++ ⟨“ Q ”⟩) \circ (C ++ ⟨“ \|F\| ”⟩)) \circ S^{-1})) \circ S = (((D ++ ⟨“ T ”⟩) \circ S^{-1}) {\underset{˙}{\cdot}}_{f} ((F ++ ⟨“ Q ”⟩) \circ ((C ++ ⟨“ \|F\| ”⟩) \circ S^{-1}))) \circ S$
218	214 217	eqtrdi	$⊢ φ \to ((H \circ S) prefix (\|H\| - 1)) ++ ⟨“ H (K) ”⟩ = (((D ++ ⟨“ T ”⟩) \circ S^{-1}) {\underset{˙}{\cdot}}_{f} ((F ++ ⟨“ Q ”⟩) \circ ((C ++ ⟨“ \|F\| ”⟩) \circ S^{-1}))) \circ S$
219	19 218	eqtrd	$⊢ φ \to H \circ S = (((D ++ ⟨“ T ”⟩) \circ S^{-1}) {\underset{˙}{\cdot}}_{f} ((F ++ ⟨“ Q ”⟩) \circ ((C ++ ⟨“ \|F\| ”⟩) \circ S^{-1}))) \circ S$
220		cocan2	$⊢ (S : (0 ..^\|H\|) \underset{onto}{⟶} (0 ..^\|H\|) \land H Fn (0 ..^\|H\|) \land (((D ++ ⟨“ T ”⟩) \circ S^{-1}) {\underset{˙}{\cdot}}_{f} ((F ++ ⟨“ Q ”⟩) \circ ((C ++ ⟨“ \|F\| ”⟩) \circ S^{-1}))) Fn (0 ..^\|H\|)) \to (H \circ S = (((D ++ ⟨“ T ”⟩) \circ S^{-1}) {\underset{˙}{\cdot}}_{f} ((F ++ ⟨“ Q ”⟩) \circ ((C ++ ⟨“ \|F\| ”⟩) \circ S^{-1}))) \circ S \leftrightarrow H = ((D ++ ⟨“ T ”⟩) \circ S^{-1}) {\underset{˙}{\cdot}}_{f} ((F ++ ⟨“ Q ”⟩) \circ ((C ++ ⟨“ \|F\| ”⟩) \circ S^{-1})))$
221	220	biimpa	$⊢ ((S : (0 ..^\|H\|) \underset{onto}{⟶} (0 ..^\|H\|) \land H Fn (0 ..^\|H\|) \land (((D ++ ⟨“ T ”⟩) \circ S^{-1}) {\underset{˙}{\cdot}}_{f} ((F ++ ⟨“ Q ”⟩) \circ ((C ++ ⟨“ \|F\| ”⟩) \circ S^{-1}))) Fn (0 ..^\|H\|)) \land H \circ S = (((D ++ ⟨“ T ”⟩) \circ S^{-1}) {\underset{˙}{\cdot}}_{f} ((F ++ ⟨“ Q ”⟩) \circ ((C ++ ⟨“ \|F\| ”⟩) \circ S^{-1}))) \circ S) \to H = ((D ++ ⟨“ T ”⟩) \circ S^{-1}) {\underset{˙}{\cdot}}_{f} ((F ++ ⟨“ Q ”⟩) \circ ((C ++ ⟨“ \|F\| ”⟩) \circ S^{-1}))$
222	122 123 177 219 221	syl31anc	$⊢ φ \to H = ((D ++ ⟨“ T ”⟩) \circ S^{-1}) {\underset{˙}{\cdot}}_{f} ((F ++ ⟨“ Q ”⟩) \circ ((C ++ ⟨“ \|F\| ”⟩) \circ S^{-1}))$
223	120 222	jca	$⊢ φ \to (((C ++ ⟨“ \|F\| ”⟩) \circ S^{-1}) : (0 ..^\|F ++ ⟨“ Q ”⟩\|) \underset{1-1 onto}{⟶} (0 ..^\|F ++ ⟨“ Q ”⟩\|) \land H = ((D ++ ⟨“ T ”⟩) \circ S^{-1}) {\underset{˙}{\cdot}}_{f} ((F ++ ⟨“ Q ”⟩) \circ ((C ++ ⟨“ \|F\| ”⟩) \circ S^{-1})))$

Metamath Proof Explorer

Theorem 1arithidomlem2

Proof