Theorem gsumsgrpccat

Description: Homomorphic property of not empty composites of a group sum over a semigroup. Formerly part of proof for gsumccat . (Contributed by AV, 26-Dec-2023)

	Ref	Expression
Hypotheses	gsumwcl.b	$$⊢B={\mathrm{Base}}_G$$
	gsumsgrpccat.p	$$⊢\underset{\dot{}}{+}={+}_G$$
Assertion	gsumsgrpccat	Could not format assertion : No typesetting found for |- ( ( G e. Smgrp /\ ( W e. Word B /\ X e. Word B ) /\ ( W =/= (/) /\ X =/= (/) ) ) -> ( G gsum ( W ++ X ) ) = ( ( G gsum W ) .+ ( G gsum X ) ) ) with typecode |-

Proof

Step	Hyp	Ref	Expression
1		gsumwcl.b	$$⊢B={\mathrm{Base}}_G$$
2		gsumsgrpccat.p	$$⊢\underset{\dot{}}{+}={+}_G$$
3		simp1	Could not format ( ( G e. Smgrp /\ ( W e. Word B /\ X e. Word B ) /\ ( W =/= (/) /\ X =/= (/) ) ) -> G e. Smgrp ) : No typesetting found for |- ( ( G e. Smgrp /\ ( W e. Word B /\ X e. Word B ) /\ ( W =/= (/) /\ X =/= (/) ) ) -> G e. Smgrp ) with typecode |-
4		sgrpmgm	Could not format ( G e. Smgrp -> G e. Mgm ) : No typesetting found for |- ( G e. Smgrp -> G e. Mgm ) with typecode |-
5	1 2	mgmcl	$$⊢\left(G\in \mathrm{Mgm}\wedge x\in B\wedge y\in B\right)\to x\underset{\dot{}}{+}y\in B$$
6	4 5	syl3an1	Could not format ( ( G e. Smgrp /\ x e. B /\ y e. B ) -> ( x .+ y ) e. B ) : No typesetting found for |- ( ( G e. Smgrp /\ x e. B /\ y e. B ) -> ( x .+ y ) e. B ) with typecode |-
7	6	3expb	Could not format ( ( G e. Smgrp /\ ( x e. B /\ y e. B ) ) -> ( x .+ y ) e. B ) : No typesetting found for |- ( ( G e. Smgrp /\ ( x e. B /\ y e. B ) ) -> ( x .+ y ) e. B ) with typecode |-
8	3 7	sylan	Could not format ( ( ( G e. Smgrp /\ ( W e. Word B /\ X e. Word B ) /\ ( W =/= (/) /\ X =/= (/) ) ) /\ ( x e. B /\ y e. B ) ) -> ( x .+ y ) e. B ) : No typesetting found for |- ( ( ( G e. Smgrp /\ ( W e. Word B /\ X e. Word B ) /\ ( W =/= (/) /\ X =/= (/) ) ) /\ ( x e. B /\ y e. B ) ) -> ( x .+ y ) e. B ) with typecode |-
9	1 2	sgrpass	Could not format ( ( G e. Smgrp /\ ( x e. B /\ y e. B /\ z e. B ) ) -> ( ( x .+ y ) .+ z ) = ( x .+ ( y .+ z ) ) ) : No typesetting found for |- ( ( G e. Smgrp /\ ( x e. B /\ y e. B /\ z e. B ) ) -> ( ( x .+ y ) .+ z ) = ( x .+ ( y .+ z ) ) ) with typecode |-
10	3 9	sylan	Could not format ( ( ( G e. Smgrp /\ ( W e. Word B /\ X e. Word B ) /\ ( W =/= (/) /\ X =/= (/) ) ) /\ ( x e. B /\ y e. B /\ z e. B ) ) -> ( ( x .+ y ) .+ z ) = ( x .+ ( y .+ z ) ) ) : No typesetting found for |- ( ( ( G e. Smgrp /\ ( W e. Word B /\ X e. Word B ) /\ ( W =/= (/) /\ X =/= (/) ) ) /\ ( x e. B /\ y e. B /\ z e. B ) ) -> ( ( x .+ y ) .+ z ) = ( x .+ ( y .+ z ) ) ) with typecode |-
11		lennncl	$$⊢\left(W\in \mathrm{Word}B\wedge W\ne \varnothing \right)\to \left|W\right|\in \mathbb{N}$$
12	11	ad2ant2r	$$⊢\left(\left(W\in \mathrm{Word}B\wedge X\in \mathrm{Word}B\right)\wedge \left(W\ne \varnothing \wedge X\ne \varnothing \right)\right)\to \left|W\right|\in \mathbb{N}$$
13	12	3adant1	Could not format ( ( G e. Smgrp /\ ( W e. Word B /\ X e. Word B ) /\ ( W =/= (/) /\ X =/= (/) ) ) -> ( # ` W ) e. NN ) : No typesetting found for |- ( ( G e. Smgrp /\ ( W e. Word B /\ X e. Word B ) /\ ( W =/= (/) /\ X =/= (/) ) ) -> ( # ` W ) e. NN ) with typecode |-
14	13	nnzd	Could not format ( ( G e. Smgrp /\ ( W e. Word B /\ X e. Word B ) /\ ( W =/= (/) /\ X =/= (/) ) ) -> ( # ` W ) e. ZZ ) : No typesetting found for |- ( ( G e. Smgrp /\ ( W e. Word B /\ X e. Word B ) /\ ( W =/= (/) /\ X =/= (/) ) ) -> ( # ` W ) e. ZZ ) with typecode |-
15	14	uzidd	Could not format ( ( G e. Smgrp /\ ( W e. Word B /\ X e. Word B ) /\ ( W =/= (/) /\ X =/= (/) ) ) -> ( # ` W ) e. ( ZZ>= ` ( # ` W ) ) ) : No typesetting found for |- ( ( G e. Smgrp /\ ( W e. Word B /\ X e. Word B ) /\ ( W =/= (/) /\ X =/= (/) ) ) -> ( # ` W ) e. ( ZZ>= ` ( # ` W ) ) ) with typecode |-
16		lennncl	$$⊢\left(X\in \mathrm{Word}B\wedge X\ne \varnothing \right)\to \left|X\right|\in \mathbb{N}$$
17	16	ad2ant2l	$$⊢\left(\left(W\in \mathrm{Word}B\wedge X\in \mathrm{Word}B\right)\wedge \left(W\ne \varnothing \wedge X\ne \varnothing \right)\right)\to \left|X\right|\in \mathbb{N}$$
18	17	3adant1	Could not format ( ( G e. Smgrp /\ ( W e. Word B /\ X e. Word B ) /\ ( W =/= (/) /\ X =/= (/) ) ) -> ( # ` X ) e. NN ) : No typesetting found for |- ( ( G e. Smgrp /\ ( W e. Word B /\ X e. Word B ) /\ ( W =/= (/) /\ X =/= (/) ) ) -> ( # ` X ) e. NN ) with typecode |-
19		nnm1nn0	$$⊢\left|X\right|\in \mathbb{N}\to \left|X\right|-1\in {\mathbb{N}}_0$$
20	18 19	syl	Could not format ( ( G e. Smgrp /\ ( W e. Word B /\ X e. Word B ) /\ ( W =/= (/) /\ X =/= (/) ) ) -> ( ( # ` X ) - 1 ) e. NN0 ) : No typesetting found for |- ( ( G e. Smgrp /\ ( W e. Word B /\ X e. Word B ) /\ ( W =/= (/) /\ X =/= (/) ) ) -> ( ( # ` X ) - 1 ) e. NN0 ) with typecode |-
21		uzaddcl	$$⊢\left(\left|W\right|\in {\mathbb{Z}}_{\ge \left|W\right|}\wedge \left|X\right|-1\in {\mathbb{N}}_0\right)\to \left|W\right|+\left|X\right|-1\in {\mathbb{Z}}_{\ge \left|W\right|}$$
22	15 20 21	syl2anc	Could not format ( ( G e. Smgrp /\ ( W e. Word B /\ X e. Word B ) /\ ( W =/= (/) /\ X =/= (/) ) ) -> ( ( # ` W ) + ( ( # ` X ) - 1 ) ) e. ( ZZ>= ` ( # ` W ) ) ) : No typesetting found for |- ( ( G e. Smgrp /\ ( W e. Word B /\ X e. Word B ) /\ ( W =/= (/) /\ X =/= (/) ) ) -> ( ( # ` W ) + ( ( # ` X ) - 1 ) ) e. ( ZZ>= ` ( # ` W ) ) ) with typecode |-
23	13	nncnd	Could not format ( ( G e. Smgrp /\ ( W e. Word B /\ X e. Word B ) /\ ( W =/= (/) /\ X =/= (/) ) ) -> ( # ` W ) e. CC ) : No typesetting found for |- ( ( G e. Smgrp /\ ( W e. Word B /\ X e. Word B ) /\ ( W =/= (/) /\ X =/= (/) ) ) -> ( # ` W ) e. CC ) with typecode |-
24	18	nncnd	Could not format ( ( G e. Smgrp /\ ( W e. Word B /\ X e. Word B ) /\ ( W =/= (/) /\ X =/= (/) ) ) -> ( # ` X ) e. CC ) : No typesetting found for |- ( ( G e. Smgrp /\ ( W e. Word B /\ X e. Word B ) /\ ( W =/= (/) /\ X =/= (/) ) ) -> ( # ` X ) e. CC ) with typecode |-
25		1cnd	Could not format ( ( G e. Smgrp /\ ( W e. Word B /\ X e. Word B ) /\ ( W =/= (/) /\ X =/= (/) ) ) -> 1 e. CC ) : No typesetting found for |- ( ( G e. Smgrp /\ ( W e. Word B /\ X e. Word B ) /\ ( W =/= (/) /\ X =/= (/) ) ) -> 1 e. CC ) with typecode |-
26	23 24 25	addsubassd	Could not format ( ( G e. Smgrp /\ ( W e. Word B /\ X e. Word B ) /\ ( W =/= (/) /\ X =/= (/) ) ) -> ( ( ( # ` W ) + ( # ` X ) ) - 1 ) = ( ( # ` W ) + ( ( # ` X ) - 1 ) ) ) : No typesetting found for |- ( ( G e. Smgrp /\ ( W e. Word B /\ X e. Word B ) /\ ( W =/= (/) /\ X =/= (/) ) ) -> ( ( ( # ` W ) + ( # ` X ) ) - 1 ) = ( ( # ` W ) + ( ( # ` X ) - 1 ) ) ) with typecode |-
27		ax-1cn	$$⊢1\in ℂ$$
28		npcan	$$⊢\left(\left|W\right|\in ℂ\wedge 1\in ℂ\right)\to \left|W\right|-1+1=\left|W\right|$$
29	23 27 28	sylancl	Could not format ( ( G e. Smgrp /\ ( W e. Word B /\ X e. Word B ) /\ ( W =/= (/) /\ X =/= (/) ) ) -> ( ( ( # ` W ) - 1 ) + 1 ) = ( # ` W ) ) : No typesetting found for |- ( ( G e. Smgrp /\ ( W e. Word B /\ X e. Word B ) /\ ( W =/= (/) /\ X =/= (/) ) ) -> ( ( ( # ` W ) - 1 ) + 1 ) = ( # ` W ) ) with typecode |-
30	29	fveq2d	Could not format ( ( G e. Smgrp /\ ( W e. Word B /\ X e. Word B ) /\ ( W =/= (/) /\ X =/= (/) ) ) -> ( ZZ>= ` ( ( ( # ` W ) - 1 ) + 1 ) ) = ( ZZ>= ` ( # ` W ) ) ) : No typesetting found for |- ( ( G e. Smgrp /\ ( W e. Word B /\ X e. Word B ) /\ ( W =/= (/) /\ X =/= (/) ) ) -> ( ZZ>= ` ( ( ( # ` W ) - 1 ) + 1 ) ) = ( ZZ>= ` ( # ` W ) ) ) with typecode |-
31	22 26 30	3eltr4d	Could not format ( ( G e. Smgrp /\ ( W e. Word B /\ X e. Word B ) /\ ( W =/= (/) /\ X =/= (/) ) ) -> ( ( ( # ` W ) + ( # ` X ) ) - 1 ) e. ( ZZ>= ` ( ( ( # ` W ) - 1 ) + 1 ) ) ) : No typesetting found for |- ( ( G e. Smgrp /\ ( W e. Word B /\ X e. Word B ) /\ ( W =/= (/) /\ X =/= (/) ) ) -> ( ( ( # ` W ) + ( # ` X ) ) - 1 ) e. ( ZZ>= ` ( ( ( # ` W ) - 1 ) + 1 ) ) ) with typecode |-
32		nnm1nn0	$$⊢\left|W\right|\in \mathbb{N}\to \left|W\right|-1\in {\mathbb{N}}_0$$
33	13 32	syl	Could not format ( ( G e. Smgrp /\ ( W e. Word B /\ X e. Word B ) /\ ( W =/= (/) /\ X =/= (/) ) ) -> ( ( # ` W ) - 1 ) e. NN0 ) : No typesetting found for |- ( ( G e. Smgrp /\ ( W e. Word B /\ X e. Word B ) /\ ( W =/= (/) /\ X =/= (/) ) ) -> ( ( # ` W ) - 1 ) e. NN0 ) with typecode |-
34		nn0uz	$$⊢{\mathbb{N}}_0={\mathbb{Z}}_{\ge 0}$$
35	33 34	eleqtrdi	Could not format ( ( G e. Smgrp /\ ( W e. Word B /\ X e. Word B ) /\ ( W =/= (/) /\ X =/= (/) ) ) -> ( ( # ` W ) - 1 ) e. ( ZZ>= ` 0 ) ) : No typesetting found for |- ( ( G e. Smgrp /\ ( W e. Word B /\ X e. Word B ) /\ ( W =/= (/) /\ X =/= (/) ) ) -> ( ( # ` W ) - 1 ) e. ( ZZ>= ` 0 ) ) with typecode |-
36		ccatcl	$$⊢\left(W\in \mathrm{Word}B\wedge X\in \mathrm{Word}B\right)\to W\mathrm{++}X\in \mathrm{Word}B$$
37	36	3ad2ant2	Could not format ( ( G e. Smgrp /\ ( W e. Word B /\ X e. Word B ) /\ ( W =/= (/) /\ X =/= (/) ) ) -> ( W ++ X ) e. Word B ) : No typesetting found for |- ( ( G e. Smgrp /\ ( W e. Word B /\ X e. Word B ) /\ ( W =/= (/) /\ X =/= (/) ) ) -> ( W ++ X ) e. Word B ) with typecode |-
38		wrdf	$$⊢W\mathrm{++}X\in \mathrm{Word}B\to \left(W\mathrm{++}X\right):\left(0..^\left|W\mathrm{++}X\right|\right)⟶B$$
39	37 38	syl	Could not format ( ( G e. Smgrp /\ ( W e. Word B /\ X e. Word B ) /\ ( W =/= (/) /\ X =/= (/) ) ) -> ( W ++ X ) : ( 0 ..^ ( # ` ( W ++ X ) ) ) --> B ) : No typesetting found for |- ( ( G e. Smgrp /\ ( W e. Word B /\ X e. Word B ) /\ ( W =/= (/) /\ X =/= (/) ) ) -> ( W ++ X ) : ( 0 ..^ ( # ` ( W ++ X ) ) ) --> B ) with typecode |-
40		ccatlen	$$⊢\left(W\in \mathrm{Word}B\wedge X\in \mathrm{Word}B\right)\to \left|W\mathrm{++}X\right|=\left|W\right|+\left|X\right|$$
41	40	3ad2ant2	Could not format ( ( G e. Smgrp /\ ( W e. Word B /\ X e. Word B ) /\ ( W =/= (/) /\ X =/= (/) ) ) -> ( # ` ( W ++ X ) ) = ( ( # ` W ) + ( # ` X ) ) ) : No typesetting found for |- ( ( G e. Smgrp /\ ( W e. Word B /\ X e. Word B ) /\ ( W =/= (/) /\ X =/= (/) ) ) -> ( # ` ( W ++ X ) ) = ( ( # ` W ) + ( # ` X ) ) ) with typecode |-
42	41	oveq2d	Could not format ( ( G e. Smgrp /\ ( W e. Word B /\ X e. Word B ) /\ ( W =/= (/) /\ X =/= (/) ) ) -> ( 0 ..^ ( # ` ( W ++ X ) ) ) = ( 0 ..^ ( ( # ` W ) + ( # ` X ) ) ) ) : No typesetting found for |- ( ( G e. Smgrp /\ ( W e. Word B /\ X e. Word B ) /\ ( W =/= (/) /\ X =/= (/) ) ) -> ( 0 ..^ ( # ` ( W ++ X ) ) ) = ( 0 ..^ ( ( # ` W ) + ( # ` X ) ) ) ) with typecode |-
43	18	nnzd	Could not format ( ( G e. Smgrp /\ ( W e. Word B /\ X e. Word B ) /\ ( W =/= (/) /\ X =/= (/) ) ) -> ( # ` X ) e. ZZ ) : No typesetting found for |- ( ( G e. Smgrp /\ ( W e. Word B /\ X e. Word B ) /\ ( W =/= (/) /\ X =/= (/) ) ) -> ( # ` X ) e. ZZ ) with typecode |-
44	14 43	zaddcld	Could not format ( ( G e. Smgrp /\ ( W e. Word B /\ X e. Word B ) /\ ( W =/= (/) /\ X =/= (/) ) ) -> ( ( # ` W ) + ( # ` X ) ) e. ZZ ) : No typesetting found for |- ( ( G e. Smgrp /\ ( W e. Word B /\ X e. Word B ) /\ ( W =/= (/) /\ X =/= (/) ) ) -> ( ( # ` W ) + ( # ` X ) ) e. ZZ ) with typecode |-
45		fzoval	$$⊢\left|W\right|+\left|X\right|\in \mathbb{Z}\to \left(0..^\left|W\right|+\left|X\right|\right)=\left(0\dots \left|W\right|+\left|X\right|-1\right)$$
46	44 45	syl	Could not format ( ( G e. Smgrp /\ ( W e. Word B /\ X e. Word B ) /\ ( W =/= (/) /\ X =/= (/) ) ) -> ( 0 ..^ ( ( # ` W ) + ( # ` X ) ) ) = ( 0 ... ( ( ( # ` W ) + ( # ` X ) ) - 1 ) ) ) : No typesetting found for |- ( ( G e. Smgrp /\ ( W e. Word B /\ X e. Word B ) /\ ( W =/= (/) /\ X =/= (/) ) ) -> ( 0 ..^ ( ( # ` W ) + ( # ` X ) ) ) = ( 0 ... ( ( ( # ` W ) + ( # ` X ) ) - 1 ) ) ) with typecode |-
47	42 46	eqtrd	Could not format ( ( G e. Smgrp /\ ( W e. Word B /\ X e. Word B ) /\ ( W =/= (/) /\ X =/= (/) ) ) -> ( 0 ..^ ( # ` ( W ++ X ) ) ) = ( 0 ... ( ( ( # ` W ) + ( # ` X ) ) - 1 ) ) ) : No typesetting found for |- ( ( G e. Smgrp /\ ( W e. Word B /\ X e. Word B ) /\ ( W =/= (/) /\ X =/= (/) ) ) -> ( 0 ..^ ( # ` ( W ++ X ) ) ) = ( 0 ... ( ( ( # ` W ) + ( # ` X ) ) - 1 ) ) ) with typecode |-
48	47	feq2d	Could not format ( ( G e. Smgrp /\ ( W e. Word B /\ X e. Word B ) /\ ( W =/= (/) /\ X =/= (/) ) ) -> ( ( W ++ X ) : ( 0 ..^ ( # ` ( W ++ X ) ) ) --> B <-> ( W ++ X ) : ( 0 ... ( ( ( # ` W ) + ( # ` X ) ) - 1 ) ) --> B ) ) : No typesetting found for |- ( ( G e. Smgrp /\ ( W e. Word B /\ X e. Word B ) /\ ( W =/= (/) /\ X =/= (/) ) ) -> ( ( W ++ X ) : ( 0 ..^ ( # ` ( W ++ X ) ) ) --> B <-> ( W ++ X ) : ( 0 ... ( ( ( # ` W ) + ( # ` X ) ) - 1 ) ) --> B ) ) with typecode |-
49	39 48	mpbid	Could not format ( ( G e. Smgrp /\ ( W e. Word B /\ X e. Word B ) /\ ( W =/= (/) /\ X =/= (/) ) ) -> ( W ++ X ) : ( 0 ... ( ( ( # ` W ) + ( # ` X ) ) - 1 ) ) --> B ) : No typesetting found for |- ( ( G e. Smgrp /\ ( W e. Word B /\ X e. Word B ) /\ ( W =/= (/) /\ X =/= (/) ) ) -> ( W ++ X ) : ( 0 ... ( ( ( # ` W ) + ( # ` X ) ) - 1 ) ) --> B ) with typecode |-
50	49	ffvelcdmda	Could not format ( ( ( G e. Smgrp /\ ( W e. Word B /\ X e. Word B ) /\ ( W =/= (/) /\ X =/= (/) ) ) /\ x e. ( 0 ... ( ( ( # ` W ) + ( # ` X ) ) - 1 ) ) ) -> ( ( W ++ X ) ` x ) e. B ) : No typesetting found for |- ( ( ( G e. Smgrp /\ ( W e. Word B /\ X e. Word B ) /\ ( W =/= (/) /\ X =/= (/) ) ) /\ x e. ( 0 ... ( ( ( # ` W ) + ( # ` X ) ) - 1 ) ) ) -> ( ( W ++ X ) ` x ) e. B ) with typecode |-
51	8 10 31 35 50	seqsplit	Could not format ( ( G e. Smgrp /\ ( W e. Word B /\ X e. Word B ) /\ ( W =/= (/) /\ X =/= (/) ) ) -> ( seq 0 ( .+ , ( W ++ X ) ) ` ( ( ( # ` W ) + ( # ` X ) ) - 1 ) ) = ( ( seq 0 ( .+ , ( W ++ X ) ) ` ( ( # ` W ) - 1 ) ) .+ ( seq ( ( ( # ` W ) - 1 ) + 1 ) ( .+ , ( W ++ X ) ) ` ( ( ( # ` W ) + ( # ` X ) ) - 1 ) ) ) ) : No typesetting found for |- ( ( G e. Smgrp /\ ( W e. Word B /\ X e. Word B ) /\ ( W =/= (/) /\ X =/= (/) ) ) -> ( seq 0 ( .+ , ( W ++ X ) ) ` ( ( ( # ` W ) + ( # ` X ) ) - 1 ) ) = ( ( seq 0 ( .+ , ( W ++ X ) ) ` ( ( # ` W ) - 1 ) ) .+ ( seq ( ( ( # ` W ) - 1 ) + 1 ) ( .+ , ( W ++ X ) ) ` ( ( ( # ` W ) + ( # ` X ) ) - 1 ) ) ) ) with typecode |-
52		simpl2l	Could not format ( ( ( G e. Smgrp /\ ( W e. Word B /\ X e. Word B ) /\ ( W =/= (/) /\ X =/= (/) ) ) /\ x e. ( 0 ... ( ( # ` W ) - 1 ) ) ) -> W e. Word B ) : No typesetting found for |- ( ( ( G e. Smgrp /\ ( W e. Word B /\ X e. Word B ) /\ ( W =/= (/) /\ X =/= (/) ) ) /\ x e. ( 0 ... ( ( # ` W ) - 1 ) ) ) -> W e. Word B ) with typecode |-
53		simpl2r	Could not format ( ( ( G e. Smgrp /\ ( W e. Word B /\ X e. Word B ) /\ ( W =/= (/) /\ X =/= (/) ) ) /\ x e. ( 0 ... ( ( # ` W ) - 1 ) ) ) -> X e. Word B ) : No typesetting found for |- ( ( ( G e. Smgrp /\ ( W e. Word B /\ X e. Word B ) /\ ( W =/= (/) /\ X =/= (/) ) ) /\ x e. ( 0 ... ( ( # ` W ) - 1 ) ) ) -> X e. Word B ) with typecode |-
54		fzoval	$$⊢\left|W\right|\in \mathbb{Z}\to \left(0..^\left|W\right|\right)=\left(0\dots \left|W\right|-1\right)$$
55	14 54	syl	Could not format ( ( G e. Smgrp /\ ( W e. Word B /\ X e. Word B ) /\ ( W =/= (/) /\ X =/= (/) ) ) -> ( 0 ..^ ( # ` W ) ) = ( 0 ... ( ( # ` W ) - 1 ) ) ) : No typesetting found for |- ( ( G e. Smgrp /\ ( W e. Word B /\ X e. Word B ) /\ ( W =/= (/) /\ X =/= (/) ) ) -> ( 0 ..^ ( # ` W ) ) = ( 0 ... ( ( # ` W ) - 1 ) ) ) with typecode |-
56	55	eleq2d	Could not format ( ( G e. Smgrp /\ ( W e. Word B /\ X e. Word B ) /\ ( W =/= (/) /\ X =/= (/) ) ) -> ( x e. ( 0 ..^ ( # ` W ) ) <-> x e. ( 0 ... ( ( # ` W ) - 1 ) ) ) ) : No typesetting found for |- ( ( G e. Smgrp /\ ( W e. Word B /\ X e. Word B ) /\ ( W =/= (/) /\ X =/= (/) ) ) -> ( x e. ( 0 ..^ ( # ` W ) ) <-> x e. ( 0 ... ( ( # ` W ) - 1 ) ) ) ) with typecode |-
57	56	biimpar	Could not format ( ( ( G e. Smgrp /\ ( W e. Word B /\ X e. Word B ) /\ ( W =/= (/) /\ X =/= (/) ) ) /\ x e. ( 0 ... ( ( # ` W ) - 1 ) ) ) -> x e. ( 0 ..^ ( # ` W ) ) ) : No typesetting found for |- ( ( ( G e. Smgrp /\ ( W e. Word B /\ X e. Word B ) /\ ( W =/= (/) /\ X =/= (/) ) ) /\ x e. ( 0 ... ( ( # ` W ) - 1 ) ) ) -> x e. ( 0 ..^ ( # ` W ) ) ) with typecode |-
58		ccatval1	$$⊢\left(W\in \mathrm{Word}B\wedge X\in \mathrm{Word}B\wedge x\in \left(0..^\left|W\right|\right)\right)\to \left(W\mathrm{++}X\right)\left(x\right)=W\left(x\right)$$
59	52 53 57 58	syl3anc	Could not format ( ( ( G e. Smgrp /\ ( W e. Word B /\ X e. Word B ) /\ ( W =/= (/) /\ X =/= (/) ) ) /\ x e. ( 0 ... ( ( # ` W ) - 1 ) ) ) -> ( ( W ++ X ) ` x ) = ( W ` x ) ) : No typesetting found for |- ( ( ( G e. Smgrp /\ ( W e. Word B /\ X e. Word B ) /\ ( W =/= (/) /\ X =/= (/) ) ) /\ x e. ( 0 ... ( ( # ` W ) - 1 ) ) ) -> ( ( W ++ X ) ` x ) = ( W ` x ) ) with typecode |-
60	35 59	seqfveq	Could not format ( ( G e. Smgrp /\ ( W e. Word B /\ X e. Word B ) /\ ( W =/= (/) /\ X =/= (/) ) ) -> ( seq 0 ( .+ , ( W ++ X ) ) ` ( ( # ` W ) - 1 ) ) = ( seq 0 ( .+ , W ) ` ( ( # ` W ) - 1 ) ) ) : No typesetting found for |- ( ( G e. Smgrp /\ ( W e. Word B /\ X e. Word B ) /\ ( W =/= (/) /\ X =/= (/) ) ) -> ( seq 0 ( .+ , ( W ++ X ) ) ` ( ( # ` W ) - 1 ) ) = ( seq 0 ( .+ , W ) ` ( ( # ` W ) - 1 ) ) ) with typecode |-
61	23	addlidd	Could not format ( ( G e. Smgrp /\ ( W e. Word B /\ X e. Word B ) /\ ( W =/= (/) /\ X =/= (/) ) ) -> ( 0 + ( # ` W ) ) = ( # ` W ) ) : No typesetting found for |- ( ( G e. Smgrp /\ ( W e. Word B /\ X e. Word B ) /\ ( W =/= (/) /\ X =/= (/) ) ) -> ( 0 + ( # ` W ) ) = ( # ` W ) ) with typecode |-
62	29 61	eqtr4d	Could not format ( ( G e. Smgrp /\ ( W e. Word B /\ X e. Word B ) /\ ( W =/= (/) /\ X =/= (/) ) ) -> ( ( ( # ` W ) - 1 ) + 1 ) = ( 0 + ( # ` W ) ) ) : No typesetting found for |- ( ( G e. Smgrp /\ ( W e. Word B /\ X e. Word B ) /\ ( W =/= (/) /\ X =/= (/) ) ) -> ( ( ( # ` W ) - 1 ) + 1 ) = ( 0 + ( # ` W ) ) ) with typecode |-
63	62	seqeq1d	Could not format ( ( G e. Smgrp /\ ( W e. Word B /\ X e. Word B ) /\ ( W =/= (/) /\ X =/= (/) ) ) -> seq ( ( ( # ` W ) - 1 ) + 1 ) ( .+ , ( W ++ X ) ) = seq ( 0 + ( # ` W ) ) ( .+ , ( W ++ X ) ) ) : No typesetting found for |- ( ( G e. Smgrp /\ ( W e. Word B /\ X e. Word B ) /\ ( W =/= (/) /\ X =/= (/) ) ) -> seq ( ( ( # ` W ) - 1 ) + 1 ) ( .+ , ( W ++ X ) ) = seq ( 0 + ( # ` W ) ) ( .+ , ( W ++ X ) ) ) with typecode |-
64	23 24	addcomd	Could not format ( ( G e. Smgrp /\ ( W e. Word B /\ X e. Word B ) /\ ( W =/= (/) /\ X =/= (/) ) ) -> ( ( # ` W ) + ( # ` X ) ) = ( ( # ` X ) + ( # ` W ) ) ) : No typesetting found for |- ( ( G e. Smgrp /\ ( W e. Word B /\ X e. Word B ) /\ ( W =/= (/) /\ X =/= (/) ) ) -> ( ( # ` W ) + ( # ` X ) ) = ( ( # ` X ) + ( # ` W ) ) ) with typecode |-
65	64	oveq1d	Could not format ( ( G e. Smgrp /\ ( W e. Word B /\ X e. Word B ) /\ ( W =/= (/) /\ X =/= (/) ) ) -> ( ( ( # ` W ) + ( # ` X ) ) - 1 ) = ( ( ( # ` X ) + ( # ` W ) ) - 1 ) ) : No typesetting found for |- ( ( G e. Smgrp /\ ( W e. Word B /\ X e. Word B ) /\ ( W =/= (/) /\ X =/= (/) ) ) -> ( ( ( # ` W ) + ( # ` X ) ) - 1 ) = ( ( ( # ` X ) + ( # ` W ) ) - 1 ) ) with typecode |-
66	24 23 25	addsubd	Could not format ( ( G e. Smgrp /\ ( W e. Word B /\ X e. Word B ) /\ ( W =/= (/) /\ X =/= (/) ) ) -> ( ( ( # ` X ) + ( # ` W ) ) - 1 ) = ( ( ( # ` X ) - 1 ) + ( # ` W ) ) ) : No typesetting found for |- ( ( G e. Smgrp /\ ( W e. Word B /\ X e. Word B ) /\ ( W =/= (/) /\ X =/= (/) ) ) -> ( ( ( # ` X ) + ( # ` W ) ) - 1 ) = ( ( ( # ` X ) - 1 ) + ( # ` W ) ) ) with typecode |-
67	65 66	eqtrd	Could not format ( ( G e. Smgrp /\ ( W e. Word B /\ X e. Word B ) /\ ( W =/= (/) /\ X =/= (/) ) ) -> ( ( ( # ` W ) + ( # ` X ) ) - 1 ) = ( ( ( # ` X ) - 1 ) + ( # ` W ) ) ) : No typesetting found for |- ( ( G e. Smgrp /\ ( W e. Word B /\ X e. Word B ) /\ ( W =/= (/) /\ X =/= (/) ) ) -> ( ( ( # ` W ) + ( # ` X ) ) - 1 ) = ( ( ( # ` X ) - 1 ) + ( # ` W ) ) ) with typecode |-
68	63 67	fveq12d	Could not format ( ( G e. Smgrp /\ ( W e. Word B /\ X e. Word B ) /\ ( W =/= (/) /\ X =/= (/) ) ) -> ( seq ( ( ( # ` W ) - 1 ) + 1 ) ( .+ , ( W ++ X ) ) ` ( ( ( # ` W ) + ( # ` X ) ) - 1 ) ) = ( seq ( 0 + ( # ` W ) ) ( .+ , ( W ++ X ) ) ` ( ( ( # ` X ) - 1 ) + ( # ` W ) ) ) ) : No typesetting found for |- ( ( G e. Smgrp /\ ( W e. Word B /\ X e. Word B ) /\ ( W =/= (/) /\ X =/= (/) ) ) -> ( seq ( ( ( # ` W ) - 1 ) + 1 ) ( .+ , ( W ++ X ) ) ` ( ( ( # ` W ) + ( # ` X ) ) - 1 ) ) = ( seq ( 0 + ( # ` W ) ) ( .+ , ( W ++ X ) ) ` ( ( ( # ` X ) - 1 ) + ( # ` W ) ) ) ) with typecode |-
69	20 34	eleqtrdi	Could not format ( ( G e. Smgrp /\ ( W e. Word B /\ X e. Word B ) /\ ( W =/= (/) /\ X =/= (/) ) ) -> ( ( # ` X ) - 1 ) e. ( ZZ>= ` 0 ) ) : No typesetting found for |- ( ( G e. Smgrp /\ ( W e. Word B /\ X e. Word B ) /\ ( W =/= (/) /\ X =/= (/) ) ) -> ( ( # ` X ) - 1 ) e. ( ZZ>= ` 0 ) ) with typecode |-
70		simpl2l	Could not format ( ( ( G e. Smgrp /\ ( W e. Word B /\ X e. Word B ) /\ ( W =/= (/) /\ X =/= (/) ) ) /\ x e. ( 0 ... ( ( # ` X ) - 1 ) ) ) -> W e. Word B ) : No typesetting found for |- ( ( ( G e. Smgrp /\ ( W e. Word B /\ X e. Word B ) /\ ( W =/= (/) /\ X =/= (/) ) ) /\ x e. ( 0 ... ( ( # ` X ) - 1 ) ) ) -> W e. Word B ) with typecode |-
71		simpl2r	Could not format ( ( ( G e. Smgrp /\ ( W e. Word B /\ X e. Word B ) /\ ( W =/= (/) /\ X =/= (/) ) ) /\ x e. ( 0 ... ( ( # ` X ) - 1 ) ) ) -> X e. Word B ) : No typesetting found for |- ( ( ( G e. Smgrp /\ ( W e. Word B /\ X e. Word B ) /\ ( W =/= (/) /\ X =/= (/) ) ) /\ x e. ( 0 ... ( ( # ` X ) - 1 ) ) ) -> X e. Word B ) with typecode |-
72		fzoval	$$⊢\left|X\right|\in \mathbb{Z}\to \left(0..^\left|X\right|\right)=\left(0\dots \left|X\right|-1\right)$$
73	43 72	syl	Could not format ( ( G e. Smgrp /\ ( W e. Word B /\ X e. Word B ) /\ ( W =/= (/) /\ X =/= (/) ) ) -> ( 0 ..^ ( # ` X ) ) = ( 0 ... ( ( # ` X ) - 1 ) ) ) : No typesetting found for |- ( ( G e. Smgrp /\ ( W e. Word B /\ X e. Word B ) /\ ( W =/= (/) /\ X =/= (/) ) ) -> ( 0 ..^ ( # ` X ) ) = ( 0 ... ( ( # ` X ) - 1 ) ) ) with typecode |-
74	73	eleq2d	Could not format ( ( G e. Smgrp /\ ( W e. Word B /\ X e. Word B ) /\ ( W =/= (/) /\ X =/= (/) ) ) -> ( x e. ( 0 ..^ ( # ` X ) ) <-> x e. ( 0 ... ( ( # ` X ) - 1 ) ) ) ) : No typesetting found for |- ( ( G e. Smgrp /\ ( W e. Word B /\ X e. Word B ) /\ ( W =/= (/) /\ X =/= (/) ) ) -> ( x e. ( 0 ..^ ( # ` X ) ) <-> x e. ( 0 ... ( ( # ` X ) - 1 ) ) ) ) with typecode |-
75	74	biimpar	Could not format ( ( ( G e. Smgrp /\ ( W e. Word B /\ X e. Word B ) /\ ( W =/= (/) /\ X =/= (/) ) ) /\ x e. ( 0 ... ( ( # ` X ) - 1 ) ) ) -> x e. ( 0 ..^ ( # ` X ) ) ) : No typesetting found for |- ( ( ( G e. Smgrp /\ ( W e. Word B /\ X e. Word B ) /\ ( W =/= (/) /\ X =/= (/) ) ) /\ x e. ( 0 ... ( ( # ` X ) - 1 ) ) ) -> x e. ( 0 ..^ ( # ` X ) ) ) with typecode |-
76		ccatval3	$$⊢\left(W\in \mathrm{Word}B\wedge X\in \mathrm{Word}B\wedge x\in \left(0..^\left|X\right|\right)\right)\to \left(W\mathrm{++}X\right)\left(x+\left|W\right|\right)=X\left(x\right)$$
77	70 71 75 76	syl3anc	Could not format ( ( ( G e. Smgrp /\ ( W e. Word B /\ X e. Word B ) /\ ( W =/= (/) /\ X =/= (/) ) ) /\ x e. ( 0 ... ( ( # ` X ) - 1 ) ) ) -> ( ( W ++ X ) ` ( x + ( # ` W ) ) ) = ( X ` x ) ) : No typesetting found for |- ( ( ( G e. Smgrp /\ ( W e. Word B /\ X e. Word B ) /\ ( W =/= (/) /\ X =/= (/) ) ) /\ x e. ( 0 ... ( ( # ` X ) - 1 ) ) ) -> ( ( W ++ X ) ` ( x + ( # ` W ) ) ) = ( X ` x ) ) with typecode |-
78	77	eqcomd	Could not format ( ( ( G e. Smgrp /\ ( W e. Word B /\ X e. Word B ) /\ ( W =/= (/) /\ X =/= (/) ) ) /\ x e. ( 0 ... ( ( # ` X ) - 1 ) ) ) -> ( X ` x ) = ( ( W ++ X ) ` ( x + ( # ` W ) ) ) ) : No typesetting found for |- ( ( ( G e. Smgrp /\ ( W e. Word B /\ X e. Word B ) /\ ( W =/= (/) /\ X =/= (/) ) ) /\ x e. ( 0 ... ( ( # ` X ) - 1 ) ) ) -> ( X ` x ) = ( ( W ++ X ) ` ( x + ( # ` W ) ) ) ) with typecode |-
79	69 14 78	seqshft2	Could not format ( ( G e. Smgrp /\ ( W e. Word B /\ X e. Word B ) /\ ( W =/= (/) /\ X =/= (/) ) ) -> ( seq 0 ( .+ , X ) ` ( ( # ` X ) - 1 ) ) = ( seq ( 0 + ( # ` W ) ) ( .+ , ( W ++ X ) ) ` ( ( ( # ` X ) - 1 ) + ( # ` W ) ) ) ) : No typesetting found for |- ( ( G e. Smgrp /\ ( W e. Word B /\ X e. Word B ) /\ ( W =/= (/) /\ X =/= (/) ) ) -> ( seq 0 ( .+ , X ) ` ( ( # ` X ) - 1 ) ) = ( seq ( 0 + ( # ` W ) ) ( .+ , ( W ++ X ) ) ` ( ( ( # ` X ) - 1 ) + ( # ` W ) ) ) ) with typecode |-
80	68 79	eqtr4d	Could not format ( ( G e. Smgrp /\ ( W e. Word B /\ X e. Word B ) /\ ( W =/= (/) /\ X =/= (/) ) ) -> ( seq ( ( ( # ` W ) - 1 ) + 1 ) ( .+ , ( W ++ X ) ) ` ( ( ( # ` W ) + ( # ` X ) ) - 1 ) ) = ( seq 0 ( .+ , X ) ` ( ( # ` X ) - 1 ) ) ) : No typesetting found for |- ( ( G e. Smgrp /\ ( W e. Word B /\ X e. Word B ) /\ ( W =/= (/) /\ X =/= (/) ) ) -> ( seq ( ( ( # ` W ) - 1 ) + 1 ) ( .+ , ( W ++ X ) ) ` ( ( ( # ` W ) + ( # ` X ) ) - 1 ) ) = ( seq 0 ( .+ , X ) ` ( ( # ` X ) - 1 ) ) ) with typecode |-
81	60 80	oveq12d	Could not format ( ( G e. Smgrp /\ ( W e. Word B /\ X e. Word B ) /\ ( W =/= (/) /\ X =/= (/) ) ) -> ( ( seq 0 ( .+ , ( W ++ X ) ) ` ( ( # ` W ) - 1 ) ) .+ ( seq ( ( ( # ` W ) - 1 ) + 1 ) ( .+ , ( W ++ X ) ) ` ( ( ( # ` W ) + ( # ` X ) ) - 1 ) ) ) = ( ( seq 0 ( .+ , W ) ` ( ( # ` W ) - 1 ) ) .+ ( seq 0 ( .+ , X ) ` ( ( # ` X ) - 1 ) ) ) ) : No typesetting found for |- ( ( G e. Smgrp /\ ( W e. Word B /\ X e. Word B ) /\ ( W =/= (/) /\ X =/= (/) ) ) -> ( ( seq 0 ( .+ , ( W ++ X ) ) ` ( ( # ` W ) - 1 ) ) .+ ( seq ( ( ( # ` W ) - 1 ) + 1 ) ( .+ , ( W ++ X ) ) ` ( ( ( # ` W ) + ( # ` X ) ) - 1 ) ) ) = ( ( seq 0 ( .+ , W ) ` ( ( # ` W ) - 1 ) ) .+ ( seq 0 ( .+ , X ) ` ( ( # ` X ) - 1 ) ) ) ) with typecode |-
82	51 81	eqtrd	Could not format ( ( G e. Smgrp /\ ( W e. Word B /\ X e. Word B ) /\ ( W =/= (/) /\ X =/= (/) ) ) -> ( seq 0 ( .+ , ( W ++ X ) ) ` ( ( ( # ` W ) + ( # ` X ) ) - 1 ) ) = ( ( seq 0 ( .+ , W ) ` ( ( # ` W ) - 1 ) ) .+ ( seq 0 ( .+ , X ) ` ( ( # ` X ) - 1 ) ) ) ) : No typesetting found for |- ( ( G e. Smgrp /\ ( W e. Word B /\ X e. Word B ) /\ ( W =/= (/) /\ X =/= (/) ) ) -> ( seq 0 ( .+ , ( W ++ X ) ) ` ( ( ( # ` W ) + ( # ` X ) ) - 1 ) ) = ( ( seq 0 ( .+ , W ) ` ( ( # ` W ) - 1 ) ) .+ ( seq 0 ( .+ , X ) ` ( ( # ` X ) - 1 ) ) ) ) with typecode |-
83	13 18	nnaddcld	Could not format ( ( G e. Smgrp /\ ( W e. Word B /\ X e. Word B ) /\ ( W =/= (/) /\ X =/= (/) ) ) -> ( ( # ` W ) + ( # ` X ) ) e. NN ) : No typesetting found for |- ( ( G e. Smgrp /\ ( W e. Word B /\ X e. Word B ) /\ ( W =/= (/) /\ X =/= (/) ) ) -> ( ( # ` W ) + ( # ` X ) ) e. NN ) with typecode |-
84		nnm1nn0	$$⊢\left|W\right|+\left|X\right|\in \mathbb{N}\to \left|W\right|+\left|X\right|-1\in {\mathbb{N}}_0$$
85	83 84	syl	Could not format ( ( G e. Smgrp /\ ( W e. Word B /\ X e. Word B ) /\ ( W =/= (/) /\ X =/= (/) ) ) -> ( ( ( # ` W ) + ( # ` X ) ) - 1 ) e. NN0 ) : No typesetting found for |- ( ( G e. Smgrp /\ ( W e. Word B /\ X e. Word B ) /\ ( W =/= (/) /\ X =/= (/) ) ) -> ( ( ( # ` W ) + ( # ` X ) ) - 1 ) e. NN0 ) with typecode |-
86	85 34	eleqtrdi	Could not format ( ( G e. Smgrp /\ ( W e. Word B /\ X e. Word B ) /\ ( W =/= (/) /\ X =/= (/) ) ) -> ( ( ( # ` W ) + ( # ` X ) ) - 1 ) e. ( ZZ>= ` 0 ) ) : No typesetting found for |- ( ( G e. Smgrp /\ ( W e. Word B /\ X e. Word B ) /\ ( W =/= (/) /\ X =/= (/) ) ) -> ( ( ( # ` W ) + ( # ` X ) ) - 1 ) e. ( ZZ>= ` 0 ) ) with typecode |-
87	1 2 3 86 49	gsumval2	Could not format ( ( G e. Smgrp /\ ( W e. Word B /\ X e. Word B ) /\ ( W =/= (/) /\ X =/= (/) ) ) -> ( G gsum ( W ++ X ) ) = ( seq 0 ( .+ , ( W ++ X ) ) ` ( ( ( # ` W ) + ( # ` X ) ) - 1 ) ) ) : No typesetting found for |- ( ( G e. Smgrp /\ ( W e. Word B /\ X e. Word B ) /\ ( W =/= (/) /\ X =/= (/) ) ) -> ( G gsum ( W ++ X ) ) = ( seq 0 ( .+ , ( W ++ X ) ) ` ( ( ( # ` W ) + ( # ` X ) ) - 1 ) ) ) with typecode |-
88		simp2l	Could not format ( ( G e. Smgrp /\ ( W e. Word B /\ X e. Word B ) /\ ( W =/= (/) /\ X =/= (/) ) ) -> W e. Word B ) : No typesetting found for |- ( ( G e. Smgrp /\ ( W e. Word B /\ X e. Word B ) /\ ( W =/= (/) /\ X =/= (/) ) ) -> W e. Word B ) with typecode |-
89		wrdf	$$⊢W\in \mathrm{Word}B\to W:\left(0..^\left|W\right|\right)⟶B$$
90	88 89	syl	Could not format ( ( G e. Smgrp /\ ( W e. Word B /\ X e. Word B ) /\ ( W =/= (/) /\ X =/= (/) ) ) -> W : ( 0 ..^ ( # ` W ) ) --> B ) : No typesetting found for |- ( ( G e. Smgrp /\ ( W e. Word B /\ X e. Word B ) /\ ( W =/= (/) /\ X =/= (/) ) ) -> W : ( 0 ..^ ( # ` W ) ) --> B ) with typecode |-
91	55	feq2d	Could not format ( ( G e. Smgrp /\ ( W e. Word B /\ X e. Word B ) /\ ( W =/= (/) /\ X =/= (/) ) ) -> ( W : ( 0 ..^ ( # ` W ) ) --> B <-> W : ( 0 ... ( ( # ` W ) - 1 ) ) --> B ) ) : No typesetting found for |- ( ( G e. Smgrp /\ ( W e. Word B /\ X e. Word B ) /\ ( W =/= (/) /\ X =/= (/) ) ) -> ( W : ( 0 ..^ ( # ` W ) ) --> B <-> W : ( 0 ... ( ( # ` W ) - 1 ) ) --> B ) ) with typecode |-
92	90 91	mpbid	Could not format ( ( G e. Smgrp /\ ( W e. Word B /\ X e. Word B ) /\ ( W =/= (/) /\ X =/= (/) ) ) -> W : ( 0 ... ( ( # ` W ) - 1 ) ) --> B ) : No typesetting found for |- ( ( G e. Smgrp /\ ( W e. Word B /\ X e. Word B ) /\ ( W =/= (/) /\ X =/= (/) ) ) -> W : ( 0 ... ( ( # ` W ) - 1 ) ) --> B ) with typecode |-
93	1 2 3 35 92	gsumval2	Could not format ( ( G e. Smgrp /\ ( W e. Word B /\ X e. Word B ) /\ ( W =/= (/) /\ X =/= (/) ) ) -> ( G gsum W ) = ( seq 0 ( .+ , W ) ` ( ( # ` W ) - 1 ) ) ) : No typesetting found for |- ( ( G e. Smgrp /\ ( W e. Word B /\ X e. Word B ) /\ ( W =/= (/) /\ X =/= (/) ) ) -> ( G gsum W ) = ( seq 0 ( .+ , W ) ` ( ( # ` W ) - 1 ) ) ) with typecode |-
94		simp2r	Could not format ( ( G e. Smgrp /\ ( W e. Word B /\ X e. Word B ) /\ ( W =/= (/) /\ X =/= (/) ) ) -> X e. Word B ) : No typesetting found for |- ( ( G e. Smgrp /\ ( W e. Word B /\ X e. Word B ) /\ ( W =/= (/) /\ X =/= (/) ) ) -> X e. Word B ) with typecode |-
95		wrdf	$$⊢X\in \mathrm{Word}B\to X:\left(0..^\left|X\right|\right)⟶B$$
96	94 95	syl	Could not format ( ( G e. Smgrp /\ ( W e. Word B /\ X e. Word B ) /\ ( W =/= (/) /\ X =/= (/) ) ) -> X : ( 0 ..^ ( # ` X ) ) --> B ) : No typesetting found for |- ( ( G e. Smgrp /\ ( W e. Word B /\ X e. Word B ) /\ ( W =/= (/) /\ X =/= (/) ) ) -> X : ( 0 ..^ ( # ` X ) ) --> B ) with typecode |-
97	73	feq2d	Could not format ( ( G e. Smgrp /\ ( W e. Word B /\ X e. Word B ) /\ ( W =/= (/) /\ X =/= (/) ) ) -> ( X : ( 0 ..^ ( # ` X ) ) --> B <-> X : ( 0 ... ( ( # ` X ) - 1 ) ) --> B ) ) : No typesetting found for |- ( ( G e. Smgrp /\ ( W e. Word B /\ X e. Word B ) /\ ( W =/= (/) /\ X =/= (/) ) ) -> ( X : ( 0 ..^ ( # ` X ) ) --> B <-> X : ( 0 ... ( ( # ` X ) - 1 ) ) --> B ) ) with typecode |-
98	96 97	mpbid	Could not format ( ( G e. Smgrp /\ ( W e. Word B /\ X e. Word B ) /\ ( W =/= (/) /\ X =/= (/) ) ) -> X : ( 0 ... ( ( # ` X ) - 1 ) ) --> B ) : No typesetting found for |- ( ( G e. Smgrp /\ ( W e. Word B /\ X e. Word B ) /\ ( W =/= (/) /\ X =/= (/) ) ) -> X : ( 0 ... ( ( # ` X ) - 1 ) ) --> B ) with typecode |-
99	1 2 3 69 98	gsumval2	Could not format ( ( G e. Smgrp /\ ( W e. Word B /\ X e. Word B ) /\ ( W =/= (/) /\ X =/= (/) ) ) -> ( G gsum X ) = ( seq 0 ( .+ , X ) ` ( ( # ` X ) - 1 ) ) ) : No typesetting found for |- ( ( G e. Smgrp /\ ( W e. Word B /\ X e. Word B ) /\ ( W =/= (/) /\ X =/= (/) ) ) -> ( G gsum X ) = ( seq 0 ( .+ , X ) ` ( ( # ` X ) - 1 ) ) ) with typecode |-
100	93 99	oveq12d	Could not format ( ( G e. Smgrp /\ ( W e. Word B /\ X e. Word B ) /\ ( W =/= (/) /\ X =/= (/) ) ) -> ( ( G gsum W ) .+ ( G gsum X ) ) = ( ( seq 0 ( .+ , W ) ` ( ( # ` W ) - 1 ) ) .+ ( seq 0 ( .+ , X ) ` ( ( # ` X ) - 1 ) ) ) ) : No typesetting found for |- ( ( G e. Smgrp /\ ( W e. Word B /\ X e. Word B ) /\ ( W =/= (/) /\ X =/= (/) ) ) -> ( ( G gsum W ) .+ ( G gsum X ) ) = ( ( seq 0 ( .+ , W ) ` ( ( # ` W ) - 1 ) ) .+ ( seq 0 ( .+ , X ) ` ( ( # ` X ) - 1 ) ) ) ) with typecode |-
101	82 87 100	3eqtr4d	Could not format ( ( G e. Smgrp /\ ( W e. Word B /\ X e. Word B ) /\ ( W =/= (/) /\ X =/= (/) ) ) -> ( G gsum ( W ++ X ) ) = ( ( G gsum W ) .+ ( G gsum X ) ) ) : No typesetting found for |- ( ( G e. Smgrp /\ ( W e. Word B /\ X e. Word B ) /\ ( W =/= (/) /\ X =/= (/) ) ) -> ( G gsum ( W ++ X ) ) = ( ( G gsum W ) .+ ( G gsum X ) ) ) with typecode |-