Theorem 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	|- .x. = ( .r ` R )
	1arithidom.j	|- J = ( 0 ..^ ( # ` F ) )
	1arithidom.r	|- ( ph -> R e. IDomn )
	1arithidom.f	|- ( ph -> F e. Word P )
	1arithidom.g	|- ( ph -> G e. Word P )
	1arithidom.1	|- ( ph -> ( M gsum F ) = ( M gsum G ) )
	1arithidomlem.1	|- ( ph -> Q e. P )
	1arithidomlem.2	|- ( ph -> A. g e. Word P ( E. k e. U ( M gsum F ) = ( k .x. ( M gsum g ) ) -> E. w E. u e. ( U ^m ( 0 ..^ ( # ` F ) ) ) ( w : ( 0 ..^ ( # ` F ) ) -1-1-onto-> ( 0 ..^ ( # ` F ) ) /\ g = ( u oF .x. ( F o. w ) ) ) ) )
	1arithidomlem.3	|- ( ph -> H e. Word P )
	1arithidomlem.4	|- ( ph -> E. k e. U ( M gsum ( F ++ <" Q "> ) ) = ( k .x. ( M gsum H ) ) )
	1arithidomlem.5	|- ( ph -> K e. ( 0 ..^ ( # ` H ) ) )
	1arithidomlem.6	|- ( ph -> Q ( ||r ` R ) ( H ` K ) )
	1arithidomlem.7	|- ( ph -> T e. U )
	1arithidomlem.8	|- ( ph -> ( T .x. Q ) = ( H ` K ) )
	1arithidomlem.9	|- ( ph -> S : ( 0 ..^ ( # ` H ) ) -1-1-onto-> ( 0 ..^ ( # ` H ) ) )
	1arithidomlem.10	|- ( ph -> ( H o. S ) = ( ( ( H o. S ) prefix ( ( # ` H ) - 1 ) ) ++ <" ( H ` K ) "> ) )
	1arithidomlem.11	|- ( ph -> N e. U )
	1arithidomlem.12	|- ( ph -> ( M gsum ( F ++ <" Q "> ) ) = ( N .x. ( M gsum H ) ) )
	1arithidomlem.13	|- ( ph -> D e. ( U ^m ( 0 ..^ ( # ` F ) ) ) )
	1arithidomlem.14	|- ( ph -> C : ( 0 ..^ ( # ` F ) ) -1-1-onto-> ( 0 ..^ ( # ` F ) ) )
	1arithidomlem.15	|- ( ph -> ( ( H o. S ) prefix ( ( # ` H ) - 1 ) ) = ( D oF .x. ( F o. C ) ) )
Assertion	1arithidomlem2	|- ( ph -> ( ( ( C ++ <" ( # ` F ) "> ) o. `' S ) : ( 0 ..^ ( # ` ( F ++ <" Q "> ) ) ) -1-1-onto-> ( 0 ..^ ( # ` ( F ++ <" Q "> ) ) ) /\ H = ( ( ( D ++ <" T "> ) o. `' S ) oF .x. ( ( F ++ <" Q "> ) o. ( ( C ++ <" ( # ` F ) "> ) o. `' S ) ) ) ) )

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