elrgspnsubrunlem2

	Ref	Expression
Hypotheses	elrgspnsubrun.b	⊢ 𝐵 = ( Base ‘ 𝑅 )
	elrgspnsubrun.t	⊢ · = ( ._r ‘ 𝑅 )
	elrgspnsubrun.z	⊢ 0 = ( 0_g ‘ 𝑅 )
	elrgspnsubrun.n	⊢ 𝑁 = ( RingSpan ‘ 𝑅 )
	elrgspnsubrun.r	⊢ ( 𝜑 → 𝑅 ∈ CRing )
	elrgspnsubrun.e	⊢ ( 𝜑 → 𝐸 ∈ ( SubRing ‘ 𝑅 ) )
	elrgspnsubrun.f	⊢ ( 𝜑 → 𝐹 ∈ ( SubRing ‘ 𝑅 ) )
	elrgspnsubrunlem2.x	⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
	elrgspnsubrunlem2.1	⊢ ( 𝜑 → 𝐺 : Word ( 𝐸 ∪ 𝐹 ) ⟶ ℤ )
	elrgspnsubrunlem2.2	⊢ ( 𝜑 → 𝐺 finSupp 0 )
	elrgspnsubrunlem2.3	⊢ ( 𝜑 → 𝑋 = ( 𝑅 Σ_g ( 𝑤 ∈ Word ( 𝐸 ∪ 𝐹 ) ↦ ( ( 𝐺 ‘ 𝑤 ) ( ._g ‘ 𝑅 ) ( ( mulGrp ‘ 𝑅 ) Σ_g 𝑤 ) ) ) ) )
Assertion	elrgspnsubrunlem2	⊢ ( 𝜑 → ∃ 𝑝 ∈ ( 𝐸 ↑_m 𝐹 ) ( 𝑝 finSupp 0 ∧ 𝑋 = ( 𝑅 Σ_g ( 𝑓 ∈ 𝐹 ↦ ( ( 𝑝 ‘ 𝑓 ) · 𝑓 ) ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		elrgspnsubrun.b	⊢ 𝐵 = ( Base ‘ 𝑅 )
2		elrgspnsubrun.t	⊢ · = ( ._r ‘ 𝑅 )
3		elrgspnsubrun.z	⊢ 0 = ( 0_g ‘ 𝑅 )
4		elrgspnsubrun.n	⊢ 𝑁 = ( RingSpan ‘ 𝑅 )
5		elrgspnsubrun.r	⊢ ( 𝜑 → 𝑅 ∈ CRing )
6		elrgspnsubrun.e	⊢ ( 𝜑 → 𝐸 ∈ ( SubRing ‘ 𝑅 ) )
7		elrgspnsubrun.f	⊢ ( 𝜑 → 𝐹 ∈ ( SubRing ‘ 𝑅 ) )
8		elrgspnsubrunlem2.x	⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
9		elrgspnsubrunlem2.1	⊢ ( 𝜑 → 𝐺 : Word ( 𝐸 ∪ 𝐹 ) ⟶ ℤ )
10		elrgspnsubrunlem2.2	⊢ ( 𝜑 → 𝐺 finSupp 0 )
11		elrgspnsubrunlem2.3	⊢ ( 𝜑 → 𝑋 = ( 𝑅 Σ_g ( 𝑤 ∈ Word ( 𝐸 ∪ 𝐹 ) ↦ ( ( 𝐺 ‘ 𝑤 ) ( ._g ‘ 𝑅 ) ( ( mulGrp ‘ 𝑅 ) Σ_g 𝑤 ) ) ) ) )
12	6	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝑞 ∈ ( ( 𝐸 × 𝐹 ) ↑_m Word ( 𝐸 ∪ 𝐹 ) ) ) ∧ ∀ 𝑤 ∈ Word ( 𝐸 ∪ 𝐹 ) ( ( mulGrp ‘ 𝑅 ) Σ_g 𝑤 ) = ( ( 1^st ‘ ( 𝑞 ‘ 𝑤 ) ) · ( 2^nd ‘ ( 𝑞 ‘ 𝑤 ) ) ) ) → 𝐸 ∈ ( SubRing ‘ 𝑅 ) )
13	7	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝑞 ∈ ( ( 𝐸 × 𝐹 ) ↑_m Word ( 𝐸 ∪ 𝐹 ) ) ) ∧ ∀ 𝑤 ∈ Word ( 𝐸 ∪ 𝐹 ) ( ( mulGrp ‘ 𝑅 ) Σ_g 𝑤 ) = ( ( 1^st ‘ ( 𝑞 ‘ 𝑤 ) ) · ( 2^nd ‘ ( 𝑞 ‘ 𝑤 ) ) ) ) → 𝐹 ∈ ( SubRing ‘ 𝑅 ) )
14	5	crngringd	⊢ ( 𝜑 → 𝑅 ∈ Ring )
15	14	ringabld	⊢ ( 𝜑 → 𝑅 ∈ Abel )
16	15	ad3antrrr	⊢ ( ( ( ( 𝜑 ∧ 𝑞 ∈ ( ( 𝐸 × 𝐹 ) ↑_m Word ( 𝐸 ∪ 𝐹 ) ) ) ∧ ∀ 𝑤 ∈ Word ( 𝐸 ∪ 𝐹 ) ( ( mulGrp ‘ 𝑅 ) Σ_g 𝑤 ) = ( ( 1^st ‘ ( 𝑞 ‘ 𝑤 ) ) · ( 2^nd ‘ ( 𝑞 ‘ 𝑤 ) ) ) ) ∧ 𝑓 ∈ 𝐹 ) → 𝑅 ∈ Abel )
17		vex	⊢ 𝑞 ∈ V
18	17	cnvex	⊢ ^◡ 𝑞 ∈ V
19	18	imaex	⊢ ( ^◡ 𝑞 “ ( 𝐸 × { 𝑓 } ) ) ∈ V
20	19	a1i	⊢ ( ( ( ( 𝜑 ∧ 𝑞 ∈ ( ( 𝐸 × 𝐹 ) ↑_m Word ( 𝐸 ∪ 𝐹 ) ) ) ∧ ∀ 𝑤 ∈ Word ( 𝐸 ∪ 𝐹 ) ( ( mulGrp ‘ 𝑅 ) Σ_g 𝑤 ) = ( ( 1^st ‘ ( 𝑞 ‘ 𝑤 ) ) · ( 2^nd ‘ ( 𝑞 ‘ 𝑤 ) ) ) ) ∧ 𝑓 ∈ 𝐹 ) → ( ^◡ 𝑞 “ ( 𝐸 × { 𝑓 } ) ) ∈ V )
21		subrgsubg	⊢ ( 𝐸 ∈ ( SubRing ‘ 𝑅 ) → 𝐸 ∈ ( SubGrp ‘ 𝑅 ) )
22	6 21	syl	⊢ ( 𝜑 → 𝐸 ∈ ( SubGrp ‘ 𝑅 ) )
23	22	ad3antrrr	⊢ ( ( ( ( 𝜑 ∧ 𝑞 ∈ ( ( 𝐸 × 𝐹 ) ↑_m Word ( 𝐸 ∪ 𝐹 ) ) ) ∧ ∀ 𝑤 ∈ Word ( 𝐸 ∪ 𝐹 ) ( ( mulGrp ‘ 𝑅 ) Σ_g 𝑤 ) = ( ( 1^st ‘ ( 𝑞 ‘ 𝑤 ) ) · ( 2^nd ‘ ( 𝑞 ‘ 𝑤 ) ) ) ) ∧ 𝑓 ∈ 𝐹 ) → 𝐸 ∈ ( SubGrp ‘ 𝑅 ) )
24		eqid	⊢ ( ._g ‘ 𝑅 ) = ( ._g ‘ 𝑅 )
25	5	crnggrpd	⊢ ( 𝜑 → 𝑅 ∈ Grp )
26	25	ad4antr	⊢ ( ( ( ( ( 𝜑 ∧ 𝑞 ∈ ( ( 𝐸 × 𝐹 ) ↑_m Word ( 𝐸 ∪ 𝐹 ) ) ) ∧ ∀ 𝑤 ∈ Word ( 𝐸 ∪ 𝐹 ) ( ( mulGrp ‘ 𝑅 ) Σ_g 𝑤 ) = ( ( 1^st ‘ ( 𝑞 ‘ 𝑤 ) ) · ( 2^nd ‘ ( 𝑞 ‘ 𝑤 ) ) ) ) ∧ 𝑓 ∈ 𝐹 ) ∧ 𝑣 ∈ ( ^◡ 𝑞 “ ( 𝐸 × { 𝑓 } ) ) ) → 𝑅 ∈ Grp )
27	6 7	xpexd	⊢ ( 𝜑 → ( 𝐸 × 𝐹 ) ∈ V )
28	6 7	unexd	⊢ ( 𝜑 → ( 𝐸 ∪ 𝐹 ) ∈ V )
29		wrdexg	⊢ ( ( 𝐸 ∪ 𝐹 ) ∈ V → Word ( 𝐸 ∪ 𝐹 ) ∈ V )
30	28 29	syl	⊢ ( 𝜑 → Word ( 𝐸 ∪ 𝐹 ) ∈ V )
31	27 30	elmapd	⊢ ( 𝜑 → ( 𝑞 ∈ ( ( 𝐸 × 𝐹 ) ↑_m Word ( 𝐸 ∪ 𝐹 ) ) ↔ 𝑞 : Word ( 𝐸 ∪ 𝐹 ) ⟶ ( 𝐸 × 𝐹 ) ) )
32	31	biimpa	⊢ ( ( 𝜑 ∧ 𝑞 ∈ ( ( 𝐸 × 𝐹 ) ↑_m Word ( 𝐸 ∪ 𝐹 ) ) ) → 𝑞 : Word ( 𝐸 ∪ 𝐹 ) ⟶ ( 𝐸 × 𝐹 ) )
33	32	ffund	⊢ ( ( 𝜑 ∧ 𝑞 ∈ ( ( 𝐸 × 𝐹 ) ↑_m Word ( 𝐸 ∪ 𝐹 ) ) ) → Fun 𝑞 )
34	33	ad3antrrr	⊢ ( ( ( ( ( 𝜑 ∧ 𝑞 ∈ ( ( 𝐸 × 𝐹 ) ↑_m Word ( 𝐸 ∪ 𝐹 ) ) ) ∧ ∀ 𝑤 ∈ Word ( 𝐸 ∪ 𝐹 ) ( ( mulGrp ‘ 𝑅 ) Σ_g 𝑤 ) = ( ( 1^st ‘ ( 𝑞 ‘ 𝑤 ) ) · ( 2^nd ‘ ( 𝑞 ‘ 𝑤 ) ) ) ) ∧ 𝑓 ∈ 𝐹 ) ∧ 𝑣 ∈ ( ^◡ 𝑞 “ ( 𝐸 × { 𝑓 } ) ) ) → Fun 𝑞 )
35		fvimacnvi	⊢ ( ( Fun 𝑞 ∧ 𝑣 ∈ ( ^◡ 𝑞 “ ( 𝐸 × { 𝑓 } ) ) ) → ( 𝑞 ‘ 𝑣 ) ∈ ( 𝐸 × { 𝑓 } ) )
36	34 35	sylancom	⊢ ( ( ( ( ( 𝜑 ∧ 𝑞 ∈ ( ( 𝐸 × 𝐹 ) ↑_m Word ( 𝐸 ∪ 𝐹 ) ) ) ∧ ∀ 𝑤 ∈ Word ( 𝐸 ∪ 𝐹 ) ( ( mulGrp ‘ 𝑅 ) Σ_g 𝑤 ) = ( ( 1^st ‘ ( 𝑞 ‘ 𝑤 ) ) · ( 2^nd ‘ ( 𝑞 ‘ 𝑤 ) ) ) ) ∧ 𝑓 ∈ 𝐹 ) ∧ 𝑣 ∈ ( ^◡ 𝑞 “ ( 𝐸 × { 𝑓 } ) ) ) → ( 𝑞 ‘ 𝑣 ) ∈ ( 𝐸 × { 𝑓 } ) )
37		xp1st	⊢ ( ( 𝑞 ‘ 𝑣 ) ∈ ( 𝐸 × { 𝑓 } ) → ( 1^st ‘ ( 𝑞 ‘ 𝑣 ) ) ∈ 𝐸 )
38	36 37	syl	⊢ ( ( ( ( ( 𝜑 ∧ 𝑞 ∈ ( ( 𝐸 × 𝐹 ) ↑_m Word ( 𝐸 ∪ 𝐹 ) ) ) ∧ ∀ 𝑤 ∈ Word ( 𝐸 ∪ 𝐹 ) ( ( mulGrp ‘ 𝑅 ) Σ_g 𝑤 ) = ( ( 1^st ‘ ( 𝑞 ‘ 𝑤 ) ) · ( 2^nd ‘ ( 𝑞 ‘ 𝑤 ) ) ) ) ∧ 𝑓 ∈ 𝐹 ) ∧ 𝑣 ∈ ( ^◡ 𝑞 “ ( 𝐸 × { 𝑓 } ) ) ) → ( 1^st ‘ ( 𝑞 ‘ 𝑣 ) ) ∈ 𝐸 )
39	23	adantr	⊢ ( ( ( ( ( 𝜑 ∧ 𝑞 ∈ ( ( 𝐸 × 𝐹 ) ↑_m Word ( 𝐸 ∪ 𝐹 ) ) ) ∧ ∀ 𝑤 ∈ Word ( 𝐸 ∪ 𝐹 ) ( ( mulGrp ‘ 𝑅 ) Σ_g 𝑤 ) = ( ( 1^st ‘ ( 𝑞 ‘ 𝑤 ) ) · ( 2^nd ‘ ( 𝑞 ‘ 𝑤 ) ) ) ) ∧ 𝑓 ∈ 𝐹 ) ∧ 𝑣 ∈ ( ^◡ 𝑞 “ ( 𝐸 × { 𝑓 } ) ) ) → 𝐸 ∈ ( SubGrp ‘ 𝑅 ) )
40	9	ad4antr	⊢ ( ( ( ( ( 𝜑 ∧ 𝑞 ∈ ( ( 𝐸 × 𝐹 ) ↑_m Word ( 𝐸 ∪ 𝐹 ) ) ) ∧ ∀ 𝑤 ∈ Word ( 𝐸 ∪ 𝐹 ) ( ( mulGrp ‘ 𝑅 ) Σ_g 𝑤 ) = ( ( 1^st ‘ ( 𝑞 ‘ 𝑤 ) ) · ( 2^nd ‘ ( 𝑞 ‘ 𝑤 ) ) ) ) ∧ 𝑓 ∈ 𝐹 ) ∧ 𝑣 ∈ ( ^◡ 𝑞 “ ( 𝐸 × { 𝑓 } ) ) ) → 𝐺 : Word ( 𝐸 ∪ 𝐹 ) ⟶ ℤ )
41		cnvimass	⊢ ( ^◡ 𝑞 “ ( 𝐸 × { 𝑓 } ) ) ⊆ dom 𝑞
42	32	fdmd	⊢ ( ( 𝜑 ∧ 𝑞 ∈ ( ( 𝐸 × 𝐹 ) ↑_m Word ( 𝐸 ∪ 𝐹 ) ) ) → dom 𝑞 = Word ( 𝐸 ∪ 𝐹 ) )
43	42	ad2antrr	⊢ ( ( ( ( 𝜑 ∧ 𝑞 ∈ ( ( 𝐸 × 𝐹 ) ↑_m Word ( 𝐸 ∪ 𝐹 ) ) ) ∧ ∀ 𝑤 ∈ Word ( 𝐸 ∪ 𝐹 ) ( ( mulGrp ‘ 𝑅 ) Σ_g 𝑤 ) = ( ( 1^st ‘ ( 𝑞 ‘ 𝑤 ) ) · ( 2^nd ‘ ( 𝑞 ‘ 𝑤 ) ) ) ) ∧ 𝑓 ∈ 𝐹 ) → dom 𝑞 = Word ( 𝐸 ∪ 𝐹 ) )
44	41 43	sseqtrid	⊢ ( ( ( ( 𝜑 ∧ 𝑞 ∈ ( ( 𝐸 × 𝐹 ) ↑_m Word ( 𝐸 ∪ 𝐹 ) ) ) ∧ ∀ 𝑤 ∈ Word ( 𝐸 ∪ 𝐹 ) ( ( mulGrp ‘ 𝑅 ) Σ_g 𝑤 ) = ( ( 1^st ‘ ( 𝑞 ‘ 𝑤 ) ) · ( 2^nd ‘ ( 𝑞 ‘ 𝑤 ) ) ) ) ∧ 𝑓 ∈ 𝐹 ) → ( ^◡ 𝑞 “ ( 𝐸 × { 𝑓 } ) ) ⊆ Word ( 𝐸 ∪ 𝐹 ) )
45	44	sselda	⊢ ( ( ( ( ( 𝜑 ∧ 𝑞 ∈ ( ( 𝐸 × 𝐹 ) ↑_m Word ( 𝐸 ∪ 𝐹 ) ) ) ∧ ∀ 𝑤 ∈ Word ( 𝐸 ∪ 𝐹 ) ( ( mulGrp ‘ 𝑅 ) Σ_g 𝑤 ) = ( ( 1^st ‘ ( 𝑞 ‘ 𝑤 ) ) · ( 2^nd ‘ ( 𝑞 ‘ 𝑤 ) ) ) ) ∧ 𝑓 ∈ 𝐹 ) ∧ 𝑣 ∈ ( ^◡ 𝑞 “ ( 𝐸 × { 𝑓 } ) ) ) → 𝑣 ∈ Word ( 𝐸 ∪ 𝐹 ) )
46	40 45	ffvelcdmd	⊢ ( ( ( ( ( 𝜑 ∧ 𝑞 ∈ ( ( 𝐸 × 𝐹 ) ↑_m Word ( 𝐸 ∪ 𝐹 ) ) ) ∧ ∀ 𝑤 ∈ Word ( 𝐸 ∪ 𝐹 ) ( ( mulGrp ‘ 𝑅 ) Σ_g 𝑤 ) = ( ( 1^st ‘ ( 𝑞 ‘ 𝑤 ) ) · ( 2^nd ‘ ( 𝑞 ‘ 𝑤 ) ) ) ) ∧ 𝑓 ∈ 𝐹 ) ∧ 𝑣 ∈ ( ^◡ 𝑞 “ ( 𝐸 × { 𝑓 } ) ) ) → ( 𝐺 ‘ 𝑣 ) ∈ ℤ )
47	1 24 26 38 39 46	subgmulgcld	⊢ ( ( ( ( ( 𝜑 ∧ 𝑞 ∈ ( ( 𝐸 × 𝐹 ) ↑_m Word ( 𝐸 ∪ 𝐹 ) ) ) ∧ ∀ 𝑤 ∈ Word ( 𝐸 ∪ 𝐹 ) ( ( mulGrp ‘ 𝑅 ) Σ_g 𝑤 ) = ( ( 1^st ‘ ( 𝑞 ‘ 𝑤 ) ) · ( 2^nd ‘ ( 𝑞 ‘ 𝑤 ) ) ) ) ∧ 𝑓 ∈ 𝐹 ) ∧ 𝑣 ∈ ( ^◡ 𝑞 “ ( 𝐸 × { 𝑓 } ) ) ) → ( ( 𝐺 ‘ 𝑣 ) ( ._g ‘ 𝑅 ) ( 1^st ‘ ( 𝑞 ‘ 𝑣 ) ) ) ∈ 𝐸 )
48	47	fmpttd	⊢ ( ( ( ( 𝜑 ∧ 𝑞 ∈ ( ( 𝐸 × 𝐹 ) ↑_m Word ( 𝐸 ∪ 𝐹 ) ) ) ∧ ∀ 𝑤 ∈ Word ( 𝐸 ∪ 𝐹 ) ( ( mulGrp ‘ 𝑅 ) Σ_g 𝑤 ) = ( ( 1^st ‘ ( 𝑞 ‘ 𝑤 ) ) · ( 2^nd ‘ ( 𝑞 ‘ 𝑤 ) ) ) ) ∧ 𝑓 ∈ 𝐹 ) → ( 𝑣 ∈ ( ^◡ 𝑞 “ ( 𝐸 × { 𝑓 } ) ) ↦ ( ( 𝐺 ‘ 𝑣 ) ( ._g ‘ 𝑅 ) ( 1^st ‘ ( 𝑞 ‘ 𝑣 ) ) ) ) : ( ^◡ 𝑞 “ ( 𝐸 × { 𝑓 } ) ) ⟶ 𝐸 )
49	9	feqmptd	⊢ ( 𝜑 → 𝐺 = ( 𝑣 ∈ Word ( 𝐸 ∪ 𝐹 ) ↦ ( 𝐺 ‘ 𝑣 ) ) )
50	49 10	eqbrtrrd	⊢ ( 𝜑 → ( 𝑣 ∈ Word ( 𝐸 ∪ 𝐹 ) ↦ ( 𝐺 ‘ 𝑣 ) ) finSupp 0 )
51	50	ad3antrrr	⊢ ( ( ( ( 𝜑 ∧ 𝑞 ∈ ( ( 𝐸 × 𝐹 ) ↑_m Word ( 𝐸 ∪ 𝐹 ) ) ) ∧ ∀ 𝑤 ∈ Word ( 𝐸 ∪ 𝐹 ) ( ( mulGrp ‘ 𝑅 ) Σ_g 𝑤 ) = ( ( 1^st ‘ ( 𝑞 ‘ 𝑤 ) ) · ( 2^nd ‘ ( 𝑞 ‘ 𝑤 ) ) ) ) ∧ 𝑓 ∈ 𝐹 ) → ( 𝑣 ∈ Word ( 𝐸 ∪ 𝐹 ) ↦ ( 𝐺 ‘ 𝑣 ) ) finSupp 0 )
52		0zd	⊢ ( ( ( ( 𝜑 ∧ 𝑞 ∈ ( ( 𝐸 × 𝐹 ) ↑_m Word ( 𝐸 ∪ 𝐹 ) ) ) ∧ ∀ 𝑤 ∈ Word ( 𝐸 ∪ 𝐹 ) ( ( mulGrp ‘ 𝑅 ) Σ_g 𝑤 ) = ( ( 1^st ‘ ( 𝑞 ‘ 𝑤 ) ) · ( 2^nd ‘ ( 𝑞 ‘ 𝑤 ) ) ) ) ∧ 𝑓 ∈ 𝐹 ) → 0 ∈ ℤ )
53	51 44 52	fmptssfisupp	⊢ ( ( ( ( 𝜑 ∧ 𝑞 ∈ ( ( 𝐸 × 𝐹 ) ↑_m Word ( 𝐸 ∪ 𝐹 ) ) ) ∧ ∀ 𝑤 ∈ Word ( 𝐸 ∪ 𝐹 ) ( ( mulGrp ‘ 𝑅 ) Σ_g 𝑤 ) = ( ( 1^st ‘ ( 𝑞 ‘ 𝑤 ) ) · ( 2^nd ‘ ( 𝑞 ‘ 𝑤 ) ) ) ) ∧ 𝑓 ∈ 𝐹 ) → ( 𝑣 ∈ ( ^◡ 𝑞 “ ( 𝐸 × { 𝑓 } ) ) ↦ ( 𝐺 ‘ 𝑣 ) ) finSupp 0 )
54	1	subrgss	⊢ ( 𝐸 ∈ ( SubRing ‘ 𝑅 ) → 𝐸 ⊆ 𝐵 )
55	6 54	syl	⊢ ( 𝜑 → 𝐸 ⊆ 𝐵 )
56	55	ad3antrrr	⊢ ( ( ( ( 𝜑 ∧ 𝑞 ∈ ( ( 𝐸 × 𝐹 ) ↑_m Word ( 𝐸 ∪ 𝐹 ) ) ) ∧ ∀ 𝑤 ∈ Word ( 𝐸 ∪ 𝐹 ) ( ( mulGrp ‘ 𝑅 ) Σ_g 𝑤 ) = ( ( 1^st ‘ ( 𝑞 ‘ 𝑤 ) ) · ( 2^nd ‘ ( 𝑞 ‘ 𝑤 ) ) ) ) ∧ 𝑓 ∈ 𝐹 ) → 𝐸 ⊆ 𝐵 )
57	56	sselda	⊢ ( ( ( ( ( 𝜑 ∧ 𝑞 ∈ ( ( 𝐸 × 𝐹 ) ↑_m Word ( 𝐸 ∪ 𝐹 ) ) ) ∧ ∀ 𝑤 ∈ Word ( 𝐸 ∪ 𝐹 ) ( ( mulGrp ‘ 𝑅 ) Σ_g 𝑤 ) = ( ( 1^st ‘ ( 𝑞 ‘ 𝑤 ) ) · ( 2^nd ‘ ( 𝑞 ‘ 𝑤 ) ) ) ) ∧ 𝑓 ∈ 𝐹 ) ∧ 𝑦 ∈ 𝐸 ) → 𝑦 ∈ 𝐵 )
58	1 3 24	mulg0	⊢ ( 𝑦 ∈ 𝐵 → ( 0 ( ._g ‘ 𝑅 ) 𝑦 ) = 0 )
59	57 58	syl	⊢ ( ( ( ( ( 𝜑 ∧ 𝑞 ∈ ( ( 𝐸 × 𝐹 ) ↑_m Word ( 𝐸 ∪ 𝐹 ) ) ) ∧ ∀ 𝑤 ∈ Word ( 𝐸 ∪ 𝐹 ) ( ( mulGrp ‘ 𝑅 ) Σ_g 𝑤 ) = ( ( 1^st ‘ ( 𝑞 ‘ 𝑤 ) ) · ( 2^nd ‘ ( 𝑞 ‘ 𝑤 ) ) ) ) ∧ 𝑓 ∈ 𝐹 ) ∧ 𝑦 ∈ 𝐸 ) → ( 0 ( ._g ‘ 𝑅 ) 𝑦 ) = 0 )
60	3	fvexi	⊢ 0 ∈ V
61	60	a1i	⊢ ( ( ( ( 𝜑 ∧ 𝑞 ∈ ( ( 𝐸 × 𝐹 ) ↑_m Word ( 𝐸 ∪ 𝐹 ) ) ) ∧ ∀ 𝑤 ∈ Word ( 𝐸 ∪ 𝐹 ) ( ( mulGrp ‘ 𝑅 ) Σ_g 𝑤 ) = ( ( 1^st ‘ ( 𝑞 ‘ 𝑤 ) ) · ( 2^nd ‘ ( 𝑞 ‘ 𝑤 ) ) ) ) ∧ 𝑓 ∈ 𝐹 ) → 0 ∈ V )
62	53 59 46 38 61	fsuppssov1	⊢ ( ( ( ( 𝜑 ∧ 𝑞 ∈ ( ( 𝐸 × 𝐹 ) ↑_m Word ( 𝐸 ∪ 𝐹 ) ) ) ∧ ∀ 𝑤 ∈ Word ( 𝐸 ∪ 𝐹 ) ( ( mulGrp ‘ 𝑅 ) Σ_g 𝑤 ) = ( ( 1^st ‘ ( 𝑞 ‘ 𝑤 ) ) · ( 2^nd ‘ ( 𝑞 ‘ 𝑤 ) ) ) ) ∧ 𝑓 ∈ 𝐹 ) → ( 𝑣 ∈ ( ^◡ 𝑞 “ ( 𝐸 × { 𝑓 } ) ) ↦ ( ( 𝐺 ‘ 𝑣 ) ( ._g ‘ 𝑅 ) ( 1^st ‘ ( 𝑞 ‘ 𝑣 ) ) ) ) finSupp 0 )
63	3 16 20 23 48 62	gsumsubgcl	⊢ ( ( ( ( 𝜑 ∧ 𝑞 ∈ ( ( 𝐸 × 𝐹 ) ↑_m Word ( 𝐸 ∪ 𝐹 ) ) ) ∧ ∀ 𝑤 ∈ Word ( 𝐸 ∪ 𝐹 ) ( ( mulGrp ‘ 𝑅 ) Σ_g 𝑤 ) = ( ( 1^st ‘ ( 𝑞 ‘ 𝑤 ) ) · ( 2^nd ‘ ( 𝑞 ‘ 𝑤 ) ) ) ) ∧ 𝑓 ∈ 𝐹 ) → ( 𝑅 Σ_g ( 𝑣 ∈ ( ^◡ 𝑞 “ ( 𝐸 × { 𝑓 } ) ) ↦ ( ( 𝐺 ‘ 𝑣 ) ( ._g ‘ 𝑅 ) ( 1^st ‘ ( 𝑞 ‘ 𝑣 ) ) ) ) ) ∈ 𝐸 )
64	63	fmpttd	⊢ ( ( ( 𝜑 ∧ 𝑞 ∈ ( ( 𝐸 × 𝐹 ) ↑_m Word ( 𝐸 ∪ 𝐹 ) ) ) ∧ ∀ 𝑤 ∈ Word ( 𝐸 ∪ 𝐹 ) ( ( mulGrp ‘ 𝑅 ) Σ_g 𝑤 ) = ( ( 1^st ‘ ( 𝑞 ‘ 𝑤 ) ) · ( 2^nd ‘ ( 𝑞 ‘ 𝑤 ) ) ) ) → ( 𝑓 ∈ 𝐹 ↦ ( 𝑅 Σ_g ( 𝑣 ∈ ( ^◡ 𝑞 “ ( 𝐸 × { 𝑓 } ) ) ↦ ( ( 𝐺 ‘ 𝑣 ) ( ._g ‘ 𝑅 ) ( 1^st ‘ ( 𝑞 ‘ 𝑣 ) ) ) ) ) ) : 𝐹 ⟶ 𝐸 )
65	12 13 64	elmapdd	⊢ ( ( ( 𝜑 ∧ 𝑞 ∈ ( ( 𝐸 × 𝐹 ) ↑_m Word ( 𝐸 ∪ 𝐹 ) ) ) ∧ ∀ 𝑤 ∈ Word ( 𝐸 ∪ 𝐹 ) ( ( mulGrp ‘ 𝑅 ) Σ_g 𝑤 ) = ( ( 1^st ‘ ( 𝑞 ‘ 𝑤 ) ) · ( 2^nd ‘ ( 𝑞 ‘ 𝑤 ) ) ) ) → ( 𝑓 ∈ 𝐹 ↦ ( 𝑅 Σ_g ( 𝑣 ∈ ( ^◡ 𝑞 “ ( 𝐸 × { 𝑓 } ) ) ↦ ( ( 𝐺 ‘ 𝑣 ) ( ._g ‘ 𝑅 ) ( 1^st ‘ ( 𝑞 ‘ 𝑣 ) ) ) ) ) ) ∈ ( 𝐸 ↑_m 𝐹 ) )
66		breq1	⊢ ( 𝑝 = ( 𝑓 ∈ 𝐹 ↦ ( 𝑅 Σ_g ( 𝑣 ∈ ( ^◡ 𝑞 “ ( 𝐸 × { 𝑓 } ) ) ↦ ( ( 𝐺 ‘ 𝑣 ) ( ._g ‘ 𝑅 ) ( 1^st ‘ ( 𝑞 ‘ 𝑣 ) ) ) ) ) ) → ( 𝑝 finSupp 0 ↔ ( 𝑓 ∈ 𝐹 ↦ ( 𝑅 Σ_g ( 𝑣 ∈ ( ^◡ 𝑞 “ ( 𝐸 × { 𝑓 } ) ) ↦ ( ( 𝐺 ‘ 𝑣 ) ( ._g ‘ 𝑅 ) ( 1^st ‘ ( 𝑞 ‘ 𝑣 ) ) ) ) ) ) finSupp 0 ) )
67	66	adantl	⊢ ( ( ( ( 𝜑 ∧ 𝑞 ∈ ( ( 𝐸 × 𝐹 ) ↑_m Word ( 𝐸 ∪ 𝐹 ) ) ) ∧ ∀ 𝑤 ∈ Word ( 𝐸 ∪ 𝐹 ) ( ( mulGrp ‘ 𝑅 ) Σ_g 𝑤 ) = ( ( 1^st ‘ ( 𝑞 ‘ 𝑤 ) ) · ( 2^nd ‘ ( 𝑞 ‘ 𝑤 ) ) ) ) ∧ 𝑝 = ( 𝑓 ∈ 𝐹 ↦ ( 𝑅 Σ_g ( 𝑣 ∈ ( ^◡ 𝑞 “ ( 𝐸 × { 𝑓 } ) ) ↦ ( ( 𝐺 ‘ 𝑣 ) ( ._g ‘ 𝑅 ) ( 1^st ‘ ( 𝑞 ‘ 𝑣 ) ) ) ) ) ) ) → ( 𝑝 finSupp 0 ↔ ( 𝑓 ∈ 𝐹 ↦ ( 𝑅 Σ_g ( 𝑣 ∈ ( ^◡ 𝑞 “ ( 𝐸 × { 𝑓 } ) ) ↦ ( ( 𝐺 ‘ 𝑣 ) ( ._g ‘ 𝑅 ) ( 1^st ‘ ( 𝑞 ‘ 𝑣 ) ) ) ) ) ) finSupp 0 ) )
68		nfv	⊢ Ⅎ 𝑓 ( ( 𝜑 ∧ 𝑞 ∈ ( ( 𝐸 × 𝐹 ) ↑_m Word ( 𝐸 ∪ 𝐹 ) ) ) ∧ ∀ 𝑤 ∈ Word ( 𝐸 ∪ 𝐹 ) ( ( mulGrp ‘ 𝑅 ) Σ_g 𝑤 ) = ( ( 1^st ‘ ( 𝑞 ‘ 𝑤 ) ) · ( 2^nd ‘ ( 𝑞 ‘ 𝑤 ) ) ) )
69		nfmpt1	⊢ Ⅎ 𝑓 ( 𝑓 ∈ 𝐹 ↦ ( 𝑅 Σ_g ( 𝑣 ∈ ( ^◡ 𝑞 “ ( 𝐸 × { 𝑓 } ) ) ↦ ( ( 𝐺 ‘ 𝑣 ) ( ._g ‘ 𝑅 ) ( 1^st ‘ ( 𝑞 ‘ 𝑣 ) ) ) ) ) )
70	69	nfeq2	⊢ Ⅎ 𝑓 𝑝 = ( 𝑓 ∈ 𝐹 ↦ ( 𝑅 Σ_g ( 𝑣 ∈ ( ^◡ 𝑞 “ ( 𝐸 × { 𝑓 } ) ) ↦ ( ( 𝐺 ‘ 𝑣 ) ( ._g ‘ 𝑅 ) ( 1^st ‘ ( 𝑞 ‘ 𝑣 ) ) ) ) ) )
71	68 70	nfan	⊢ Ⅎ 𝑓 ( ( ( 𝜑 ∧ 𝑞 ∈ ( ( 𝐸 × 𝐹 ) ↑_m Word ( 𝐸 ∪ 𝐹 ) ) ) ∧ ∀ 𝑤 ∈ Word ( 𝐸 ∪ 𝐹 ) ( ( mulGrp ‘ 𝑅 ) Σ_g 𝑤 ) = ( ( 1^st ‘ ( 𝑞 ‘ 𝑤 ) ) · ( 2^nd ‘ ( 𝑞 ‘ 𝑤 ) ) ) ) ∧ 𝑝 = ( 𝑓 ∈ 𝐹 ↦ ( 𝑅 Σ_g ( 𝑣 ∈ ( ^◡ 𝑞 “ ( 𝐸 × { 𝑓 } ) ) ↦ ( ( 𝐺 ‘ 𝑣 ) ( ._g ‘ 𝑅 ) ( 1^st ‘ ( 𝑞 ‘ 𝑣 ) ) ) ) ) ) )
72		simpr	⊢ ( ( ( ( 𝜑 ∧ 𝑞 ∈ ( ( 𝐸 × 𝐹 ) ↑_m Word ( 𝐸 ∪ 𝐹 ) ) ) ∧ ∀ 𝑤 ∈ Word ( 𝐸 ∪ 𝐹 ) ( ( mulGrp ‘ 𝑅 ) Σ_g 𝑤 ) = ( ( 1^st ‘ ( 𝑞 ‘ 𝑤 ) ) · ( 2^nd ‘ ( 𝑞 ‘ 𝑤 ) ) ) ) ∧ 𝑝 = ( 𝑓 ∈ 𝐹 ↦ ( 𝑅 Σ_g ( 𝑣 ∈ ( ^◡ 𝑞 “ ( 𝐸 × { 𝑓 } ) ) ↦ ( ( 𝐺 ‘ 𝑣 ) ( ._g ‘ 𝑅 ) ( 1^st ‘ ( 𝑞 ‘ 𝑣 ) ) ) ) ) ) ) → 𝑝 = ( 𝑓 ∈ 𝐹 ↦ ( 𝑅 Σ_g ( 𝑣 ∈ ( ^◡ 𝑞 “ ( 𝐸 × { 𝑓 } ) ) ↦ ( ( 𝐺 ‘ 𝑣 ) ( ._g ‘ 𝑅 ) ( 1^st ‘ ( 𝑞 ‘ 𝑣 ) ) ) ) ) ) )
73		ovexd	⊢ ( ( ( ( ( 𝜑 ∧ 𝑞 ∈ ( ( 𝐸 × 𝐹 ) ↑_m Word ( 𝐸 ∪ 𝐹 ) ) ) ∧ ∀ 𝑤 ∈ Word ( 𝐸 ∪ 𝐹 ) ( ( mulGrp ‘ 𝑅 ) Σ_g 𝑤 ) = ( ( 1^st ‘ ( 𝑞 ‘ 𝑤 ) ) · ( 2^nd ‘ ( 𝑞 ‘ 𝑤 ) ) ) ) ∧ 𝑝 = ( 𝑓 ∈ 𝐹 ↦ ( 𝑅 Σ_g ( 𝑣 ∈ ( ^◡ 𝑞 “ ( 𝐸 × { 𝑓 } ) ) ↦ ( ( 𝐺 ‘ 𝑣 ) ( ._g ‘ 𝑅 ) ( 1^st ‘ ( 𝑞 ‘ 𝑣 ) ) ) ) ) ) ) ∧ 𝑓 ∈ 𝐹 ) → ( 𝑅 Σ_g ( 𝑣 ∈ ( ^◡ 𝑞 “ ( 𝐸 × { 𝑓 } ) ) ↦ ( ( 𝐺 ‘ 𝑣 ) ( ._g ‘ 𝑅 ) ( 1^st ‘ ( 𝑞 ‘ 𝑣 ) ) ) ) ) ∈ V )
74	72 73	fvmpt2d	⊢ ( ( ( ( ( 𝜑 ∧ 𝑞 ∈ ( ( 𝐸 × 𝐹 ) ↑_m Word ( 𝐸 ∪ 𝐹 ) ) ) ∧ ∀ 𝑤 ∈ Word ( 𝐸 ∪ 𝐹 ) ( ( mulGrp ‘ 𝑅 ) Σ_g 𝑤 ) = ( ( 1^st ‘ ( 𝑞 ‘ 𝑤 ) ) · ( 2^nd ‘ ( 𝑞 ‘ 𝑤 ) ) ) ) ∧ 𝑝 = ( 𝑓 ∈ 𝐹 ↦ ( 𝑅 Σ_g ( 𝑣 ∈ ( ^◡ 𝑞 “ ( 𝐸 × { 𝑓 } ) ) ↦ ( ( 𝐺 ‘ 𝑣 ) ( ._g ‘ 𝑅 ) ( 1^st ‘ ( 𝑞 ‘ 𝑣 ) ) ) ) ) ) ) ∧ 𝑓 ∈ 𝐹 ) → ( 𝑝 ‘ 𝑓 ) = ( 𝑅 Σ_g ( 𝑣 ∈ ( ^◡ 𝑞 “ ( 𝐸 × { 𝑓 } ) ) ↦ ( ( 𝐺 ‘ 𝑣 ) ( ._g ‘ 𝑅 ) ( 1^st ‘ ( 𝑞 ‘ 𝑣 ) ) ) ) ) )
75	74	oveq1d	⊢ ( ( ( ( ( 𝜑 ∧ 𝑞 ∈ ( ( 𝐸 × 𝐹 ) ↑_m Word ( 𝐸 ∪ 𝐹 ) ) ) ∧ ∀ 𝑤 ∈ Word ( 𝐸 ∪ 𝐹 ) ( ( mulGrp ‘ 𝑅 ) Σ_g 𝑤 ) = ( ( 1^st ‘ ( 𝑞 ‘ 𝑤 ) ) · ( 2^nd ‘ ( 𝑞 ‘ 𝑤 ) ) ) ) ∧ 𝑝 = ( 𝑓 ∈ 𝐹 ↦ ( 𝑅 Σ_g ( 𝑣 ∈ ( ^◡ 𝑞 “ ( 𝐸 × { 𝑓 } ) ) ↦ ( ( 𝐺 ‘ 𝑣 ) ( ._g ‘ 𝑅 ) ( 1^st ‘ ( 𝑞 ‘ 𝑣 ) ) ) ) ) ) ) ∧ 𝑓 ∈ 𝐹 ) → ( ( 𝑝 ‘ 𝑓 ) · 𝑓 ) = ( ( 𝑅 Σ_g ( 𝑣 ∈ ( ^◡ 𝑞 “ ( 𝐸 × { 𝑓 } ) ) ↦ ( ( 𝐺 ‘ 𝑣 ) ( ._g ‘ 𝑅 ) ( 1^st ‘ ( 𝑞 ‘ 𝑣 ) ) ) ) ) · 𝑓 ) )
76	71 75	mpteq2da	⊢ ( ( ( ( 𝜑 ∧ 𝑞 ∈ ( ( 𝐸 × 𝐹 ) ↑_m Word ( 𝐸 ∪ 𝐹 ) ) ) ∧ ∀ 𝑤 ∈ Word ( 𝐸 ∪ 𝐹 ) ( ( mulGrp ‘ 𝑅 ) Σ_g 𝑤 ) = ( ( 1^st ‘ ( 𝑞 ‘ 𝑤 ) ) · ( 2^nd ‘ ( 𝑞 ‘ 𝑤 ) ) ) ) ∧ 𝑝 = ( 𝑓 ∈ 𝐹 ↦ ( 𝑅 Σ_g ( 𝑣 ∈ ( ^◡ 𝑞 “ ( 𝐸 × { 𝑓 } ) ) ↦ ( ( 𝐺 ‘ 𝑣 ) ( ._g ‘ 𝑅 ) ( 1^st ‘ ( 𝑞 ‘ 𝑣 ) ) ) ) ) ) ) → ( 𝑓 ∈ 𝐹 ↦ ( ( 𝑝 ‘ 𝑓 ) · 𝑓 ) ) = ( 𝑓 ∈ 𝐹 ↦ ( ( 𝑅 Σ_g ( 𝑣 ∈ ( ^◡ 𝑞 “ ( 𝐸 × { 𝑓 } ) ) ↦ ( ( 𝐺 ‘ 𝑣 ) ( ._g ‘ 𝑅 ) ( 1^st ‘ ( 𝑞 ‘ 𝑣 ) ) ) ) ) · 𝑓 ) ) )
77	76	oveq2d	⊢ ( ( ( ( 𝜑 ∧ 𝑞 ∈ ( ( 𝐸 × 𝐹 ) ↑_m Word ( 𝐸 ∪ 𝐹 ) ) ) ∧ ∀ 𝑤 ∈ Word ( 𝐸 ∪ 𝐹 ) ( ( mulGrp ‘ 𝑅 ) Σ_g 𝑤 ) = ( ( 1^st ‘ ( 𝑞 ‘ 𝑤 ) ) · ( 2^nd ‘ ( 𝑞 ‘ 𝑤 ) ) ) ) ∧ 𝑝 = ( 𝑓 ∈ 𝐹 ↦ ( 𝑅 Σ_g ( 𝑣 ∈ ( ^◡ 𝑞 “ ( 𝐸 × { 𝑓 } ) ) ↦ ( ( 𝐺 ‘ 𝑣 ) ( ._g ‘ 𝑅 ) ( 1^st ‘ ( 𝑞 ‘ 𝑣 ) ) ) ) ) ) ) → ( 𝑅 Σ_g ( 𝑓 ∈ 𝐹 ↦ ( ( 𝑝 ‘ 𝑓 ) · 𝑓 ) ) ) = ( 𝑅 Σ_g ( 𝑓 ∈ 𝐹 ↦ ( ( 𝑅 Σ_g ( 𝑣 ∈ ( ^◡ 𝑞 “ ( 𝐸 × { 𝑓 } ) ) ↦ ( ( 𝐺 ‘ 𝑣 ) ( ._g ‘ 𝑅 ) ( 1^st ‘ ( 𝑞 ‘ 𝑣 ) ) ) ) ) · 𝑓 ) ) ) )
78	77	eqeq2d	⊢ ( ( ( ( 𝜑 ∧ 𝑞 ∈ ( ( 𝐸 × 𝐹 ) ↑_m Word ( 𝐸 ∪ 𝐹 ) ) ) ∧ ∀ 𝑤 ∈ Word ( 𝐸 ∪ 𝐹 ) ( ( mulGrp ‘ 𝑅 ) Σ_g 𝑤 ) = ( ( 1^st ‘ ( 𝑞 ‘ 𝑤 ) ) · ( 2^nd ‘ ( 𝑞 ‘ 𝑤 ) ) ) ) ∧ 𝑝 = ( 𝑓 ∈ 𝐹 ↦ ( 𝑅 Σ_g ( 𝑣 ∈ ( ^◡ 𝑞 “ ( 𝐸 × { 𝑓 } ) ) ↦ ( ( 𝐺 ‘ 𝑣 ) ( ._g ‘ 𝑅 ) ( 1^st ‘ ( 𝑞 ‘ 𝑣 ) ) ) ) ) ) ) → ( 𝑋 = ( 𝑅 Σ_g ( 𝑓 ∈ 𝐹 ↦ ( ( 𝑝 ‘ 𝑓 ) · 𝑓 ) ) ) ↔ 𝑋 = ( 𝑅 Σ_g ( 𝑓 ∈ 𝐹 ↦ ( ( 𝑅 Σ_g ( 𝑣 ∈ ( ^◡ 𝑞 “ ( 𝐸 × { 𝑓 } ) ) ↦ ( ( 𝐺 ‘ 𝑣 ) ( ._g ‘ 𝑅 ) ( 1^st ‘ ( 𝑞 ‘ 𝑣 ) ) ) ) ) · 𝑓 ) ) ) ) )
79	67 78	anbi12d	⊢ ( ( ( ( 𝜑 ∧ 𝑞 ∈ ( ( 𝐸 × 𝐹 ) ↑_m Word ( 𝐸 ∪ 𝐹 ) ) ) ∧ ∀ 𝑤 ∈ Word ( 𝐸 ∪ 𝐹 ) ( ( mulGrp ‘ 𝑅 ) Σ_g 𝑤 ) = ( ( 1^st ‘ ( 𝑞 ‘ 𝑤 ) ) · ( 2^nd ‘ ( 𝑞 ‘ 𝑤 ) ) ) ) ∧ 𝑝 = ( 𝑓 ∈ 𝐹 ↦ ( 𝑅 Σ_g ( 𝑣 ∈ ( ^◡ 𝑞 “ ( 𝐸 × { 𝑓 } ) ) ↦ ( ( 𝐺 ‘ 𝑣 ) ( ._g ‘ 𝑅 ) ( 1^st ‘ ( 𝑞 ‘ 𝑣 ) ) ) ) ) ) ) → ( ( 𝑝 finSupp 0 ∧ 𝑋 = ( 𝑅 Σ_g ( 𝑓 ∈ 𝐹 ↦ ( ( 𝑝 ‘ 𝑓 ) · 𝑓 ) ) ) ) ↔ ( ( 𝑓 ∈ 𝐹 ↦ ( 𝑅 Σ_g ( 𝑣 ∈ ( ^◡ 𝑞 “ ( 𝐸 × { 𝑓 } ) ) ↦ ( ( 𝐺 ‘ 𝑣 ) ( ._g ‘ 𝑅 ) ( 1^st ‘ ( 𝑞 ‘ 𝑣 ) ) ) ) ) ) finSupp 0 ∧ 𝑋 = ( 𝑅 Σ_g ( 𝑓 ∈ 𝐹 ↦ ( ( 𝑅 Σ_g ( 𝑣 ∈ ( ^◡ 𝑞 “ ( 𝐸 × { 𝑓 } ) ) ↦ ( ( 𝐺 ‘ 𝑣 ) ( ._g ‘ 𝑅 ) ( 1^st ‘ ( 𝑞 ‘ 𝑣 ) ) ) ) ) · 𝑓 ) ) ) ) ) )
80	60	a1i	⊢ ( ( ( 𝜑 ∧ 𝑞 ∈ ( ( 𝐸 × 𝐹 ) ↑_m Word ( 𝐸 ∪ 𝐹 ) ) ) ∧ ∀ 𝑤 ∈ Word ( 𝐸 ∪ 𝐹 ) ( ( mulGrp ‘ 𝑅 ) Σ_g 𝑤 ) = ( ( 1^st ‘ ( 𝑞 ‘ 𝑤 ) ) · ( 2^nd ‘ ( 𝑞 ‘ 𝑤 ) ) ) ) → 0 ∈ V )
81	64	ffund	⊢ ( ( ( 𝜑 ∧ 𝑞 ∈ ( ( 𝐸 × 𝐹 ) ↑_m Word ( 𝐸 ∪ 𝐹 ) ) ) ∧ ∀ 𝑤 ∈ Word ( 𝐸 ∪ 𝐹 ) ( ( mulGrp ‘ 𝑅 ) Σ_g 𝑤 ) = ( ( 1^st ‘ ( 𝑞 ‘ 𝑤 ) ) · ( 2^nd ‘ ( 𝑞 ‘ 𝑤 ) ) ) ) → Fun ( 𝑓 ∈ 𝐹 ↦ ( 𝑅 Σ_g ( 𝑣 ∈ ( ^◡ 𝑞 “ ( 𝐸 × { 𝑓 } ) ) ↦ ( ( 𝐺 ‘ 𝑣 ) ( ._g ‘ 𝑅 ) ( 1^st ‘ ( 𝑞 ‘ 𝑣 ) ) ) ) ) ) )
82	33	adantr	⊢ ( ( ( 𝜑 ∧ 𝑞 ∈ ( ( 𝐸 × 𝐹 ) ↑_m Word ( 𝐸 ∪ 𝐹 ) ) ) ∧ ∀ 𝑤 ∈ Word ( 𝐸 ∪ 𝐹 ) ( ( mulGrp ‘ 𝑅 ) Σ_g 𝑤 ) = ( ( 1^st ‘ ( 𝑞 ‘ 𝑤 ) ) · ( 2^nd ‘ ( 𝑞 ‘ 𝑤 ) ) ) ) → Fun 𝑞 )
83	10	fsuppimpd	⊢ ( 𝜑 → ( 𝐺 supp 0 ) ∈ Fin )
84	83	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝑞 ∈ ( ( 𝐸 × 𝐹 ) ↑_m Word ( 𝐸 ∪ 𝐹 ) ) ) ∧ ∀ 𝑤 ∈ Word ( 𝐸 ∪ 𝐹 ) ( ( mulGrp ‘ 𝑅 ) Σ_g 𝑤 ) = ( ( 1^st ‘ ( 𝑞 ‘ 𝑤 ) ) · ( 2^nd ‘ ( 𝑞 ‘ 𝑤 ) ) ) ) → ( 𝐺 supp 0 ) ∈ Fin )
85		imafi	⊢ ( ( Fun 𝑞 ∧ ( 𝐺 supp 0 ) ∈ Fin ) → ( 𝑞 “ ( 𝐺 supp 0 ) ) ∈ Fin )
86	82 84 85	syl2anc	⊢ ( ( ( 𝜑 ∧ 𝑞 ∈ ( ( 𝐸 × 𝐹 ) ↑_m Word ( 𝐸 ∪ 𝐹 ) ) ) ∧ ∀ 𝑤 ∈ Word ( 𝐸 ∪ 𝐹 ) ( ( mulGrp ‘ 𝑅 ) Σ_g 𝑤 ) = ( ( 1^st ‘ ( 𝑞 ‘ 𝑤 ) ) · ( 2^nd ‘ ( 𝑞 ‘ 𝑤 ) ) ) ) → ( 𝑞 “ ( 𝐺 supp 0 ) ) ∈ Fin )
87		rnfi	⊢ ( ( 𝑞 “ ( 𝐺 supp 0 ) ) ∈ Fin → ran ( 𝑞 “ ( 𝐺 supp 0 ) ) ∈ Fin )
88	86 87	syl	⊢ ( ( ( 𝜑 ∧ 𝑞 ∈ ( ( 𝐸 × 𝐹 ) ↑_m Word ( 𝐸 ∪ 𝐹 ) ) ) ∧ ∀ 𝑤 ∈ Word ( 𝐸 ∪ 𝐹 ) ( ( mulGrp ‘ 𝑅 ) Σ_g 𝑤 ) = ( ( 1^st ‘ ( 𝑞 ‘ 𝑤 ) ) · ( 2^nd ‘ ( 𝑞 ‘ 𝑤 ) ) ) ) → ran ( 𝑞 “ ( 𝐺 supp 0 ) ) ∈ Fin )
89	9	ffnd	⊢ ( 𝜑 → 𝐺 Fn Word ( 𝐸 ∪ 𝐹 ) )
90	89	ad4antr	⊢ ( ( ( ( ( 𝜑 ∧ 𝑞 ∈ ( ( 𝐸 × 𝐹 ) ↑_m Word ( 𝐸 ∪ 𝐹 ) ) ) ∧ ∀ 𝑤 ∈ Word ( 𝐸 ∪ 𝐹 ) ( ( mulGrp ‘ 𝑅 ) Σ_g 𝑤 ) = ( ( 1^st ‘ ( 𝑞 ‘ 𝑤 ) ) · ( 2^nd ‘ ( 𝑞 ‘ 𝑤 ) ) ) ) ∧ 𝑓 ∈ ( 𝐹 ∖ ran ( 𝑞 “ ( 𝐺 supp 0 ) ) ) ) ∧ 𝑣 ∈ ( ^◡ 𝑞 “ ( 𝐸 × { 𝑓 } ) ) ) → 𝐺 Fn Word ( 𝐸 ∪ 𝐹 ) )
91	30	ad4antr	⊢ ( ( ( ( ( 𝜑 ∧ 𝑞 ∈ ( ( 𝐸 × 𝐹 ) ↑_m Word ( 𝐸 ∪ 𝐹 ) ) ) ∧ ∀ 𝑤 ∈ Word ( 𝐸 ∪ 𝐹 ) ( ( mulGrp ‘ 𝑅 ) Σ_g 𝑤 ) = ( ( 1^st ‘ ( 𝑞 ‘ 𝑤 ) ) · ( 2^nd ‘ ( 𝑞 ‘ 𝑤 ) ) ) ) ∧ 𝑓 ∈ ( 𝐹 ∖ ran ( 𝑞 “ ( 𝐺 supp 0 ) ) ) ) ∧ 𝑣 ∈ ( ^◡ 𝑞 “ ( 𝐸 × { 𝑓 } ) ) ) → Word ( 𝐸 ∪ 𝐹 ) ∈ V )
92		0zd	⊢ ( ( ( ( ( 𝜑 ∧ 𝑞 ∈ ( ( 𝐸 × 𝐹 ) ↑_m Word ( 𝐸 ∪ 𝐹 ) ) ) ∧ ∀ 𝑤 ∈ Word ( 𝐸 ∪ 𝐹 ) ( ( mulGrp ‘ 𝑅 ) Σ_g 𝑤 ) = ( ( 1^st ‘ ( 𝑞 ‘ 𝑤 ) ) · ( 2^nd ‘ ( 𝑞 ‘ 𝑤 ) ) ) ) ∧ 𝑓 ∈ ( 𝐹 ∖ ran ( 𝑞 “ ( 𝐺 supp 0 ) ) ) ) ∧ 𝑣 ∈ ( ^◡ 𝑞 “ ( 𝐸 × { 𝑓 } ) ) ) → 0 ∈ ℤ )
93		snssi	⊢ ( 𝑓 ∈ ( 𝐹 ∖ ran ( 𝑞 “ ( 𝐺 supp 0 ) ) ) → { 𝑓 } ⊆ ( 𝐹 ∖ ran ( 𝑞 “ ( 𝐺 supp 0 ) ) ) )
94	93	adantl	⊢ ( ( ( 𝜑 ∧ 𝑞 ∈ ( ( 𝐸 × 𝐹 ) ↑_m Word ( 𝐸 ∪ 𝐹 ) ) ) ∧ 𝑓 ∈ ( 𝐹 ∖ ran ( 𝑞 “ ( 𝐺 supp 0 ) ) ) ) → { 𝑓 } ⊆ ( 𝐹 ∖ ran ( 𝑞 “ ( 𝐺 supp 0 ) ) ) )
95		xpss2	⊢ ( { 𝑓 } ⊆ ( 𝐹 ∖ ran ( 𝑞 “ ( 𝐺 supp 0 ) ) ) → ( 𝐸 × { 𝑓 } ) ⊆ ( 𝐸 × ( 𝐹 ∖ ran ( 𝑞 “ ( 𝐺 supp 0 ) ) ) ) )
96		ssun2	⊢ ( 𝐸 × ( 𝐹 ∖ ran ( 𝑞 “ ( 𝐺 supp 0 ) ) ) ) ⊆ ( ( ( 𝐸 ∖ dom ( 𝑞 “ ( 𝐺 supp 0 ) ) ) × 𝐹 ) ∪ ( 𝐸 × ( 𝐹 ∖ ran ( 𝑞 “ ( 𝐺 supp 0 ) ) ) ) )
97		difxp	⊢ ( ( 𝐸 × 𝐹 ) ∖ ( dom ( 𝑞 “ ( 𝐺 supp 0 ) ) × ran ( 𝑞 “ ( 𝐺 supp 0 ) ) ) ) = ( ( ( 𝐸 ∖ dom ( 𝑞 “ ( 𝐺 supp 0 ) ) ) × 𝐹 ) ∪ ( 𝐸 × ( 𝐹 ∖ ran ( 𝑞 “ ( 𝐺 supp 0 ) ) ) ) )
98	96 97	sseqtrri	⊢ ( 𝐸 × ( 𝐹 ∖ ran ( 𝑞 “ ( 𝐺 supp 0 ) ) ) ) ⊆ ( ( 𝐸 × 𝐹 ) ∖ ( dom ( 𝑞 “ ( 𝐺 supp 0 ) ) × ran ( 𝑞 “ ( 𝐺 supp 0 ) ) ) )
99	95 98	sstrdi	⊢ ( { 𝑓 } ⊆ ( 𝐹 ∖ ran ( 𝑞 “ ( 𝐺 supp 0 ) ) ) → ( 𝐸 × { 𝑓 } ) ⊆ ( ( 𝐸 × 𝐹 ) ∖ ( dom ( 𝑞 “ ( 𝐺 supp 0 ) ) × ran ( 𝑞 “ ( 𝐺 supp 0 ) ) ) ) )
100	94 99	syl	⊢ ( ( ( 𝜑 ∧ 𝑞 ∈ ( ( 𝐸 × 𝐹 ) ↑_m Word ( 𝐸 ∪ 𝐹 ) ) ) ∧ 𝑓 ∈ ( 𝐹 ∖ ran ( 𝑞 “ ( 𝐺 supp 0 ) ) ) ) → ( 𝐸 × { 𝑓 } ) ⊆ ( ( 𝐸 × 𝐹 ) ∖ ( dom ( 𝑞 “ ( 𝐺 supp 0 ) ) × ran ( 𝑞 “ ( 𝐺 supp 0 ) ) ) ) )
101		imassrn	⊢ ( 𝑞 “ ( 𝐺 supp 0 ) ) ⊆ ran 𝑞
102	32	frnd	⊢ ( ( 𝜑 ∧ 𝑞 ∈ ( ( 𝐸 × 𝐹 ) ↑_m Word ( 𝐸 ∪ 𝐹 ) ) ) → ran 𝑞 ⊆ ( 𝐸 × 𝐹 ) )
103	102	adantr	⊢ ( ( ( 𝜑 ∧ 𝑞 ∈ ( ( 𝐸 × 𝐹 ) ↑_m Word ( 𝐸 ∪ 𝐹 ) ) ) ∧ 𝑓 ∈ ( 𝐹 ∖ ran ( 𝑞 “ ( 𝐺 supp 0 ) ) ) ) → ran 𝑞 ⊆ ( 𝐸 × 𝐹 ) )
104	101 103	sstrid	⊢ ( ( ( 𝜑 ∧ 𝑞 ∈ ( ( 𝐸 × 𝐹 ) ↑_m Word ( 𝐸 ∪ 𝐹 ) ) ) ∧ 𝑓 ∈ ( 𝐹 ∖ ran ( 𝑞 “ ( 𝐺 supp 0 ) ) ) ) → ( 𝑞 “ ( 𝐺 supp 0 ) ) ⊆ ( 𝐸 × 𝐹 ) )
105		relxp	⊢ Rel ( 𝐸 × 𝐹 )
106		relss	⊢ ( ( 𝑞 “ ( 𝐺 supp 0 ) ) ⊆ ( 𝐸 × 𝐹 ) → ( Rel ( 𝐸 × 𝐹 ) → Rel ( 𝑞 “ ( 𝐺 supp 0 ) ) ) )
107	105 106	mpi	⊢ ( ( 𝑞 “ ( 𝐺 supp 0 ) ) ⊆ ( 𝐸 × 𝐹 ) → Rel ( 𝑞 “ ( 𝐺 supp 0 ) ) )
108		relssdmrn	⊢ ( Rel ( 𝑞 “ ( 𝐺 supp 0 ) ) → ( 𝑞 “ ( 𝐺 supp 0 ) ) ⊆ ( dom ( 𝑞 “ ( 𝐺 supp 0 ) ) × ran ( 𝑞 “ ( 𝐺 supp 0 ) ) ) )
109	104 107 108	3syl	⊢ ( ( ( 𝜑 ∧ 𝑞 ∈ ( ( 𝐸 × 𝐹 ) ↑_m Word ( 𝐸 ∪ 𝐹 ) ) ) ∧ 𝑓 ∈ ( 𝐹 ∖ ran ( 𝑞 “ ( 𝐺 supp 0 ) ) ) ) → ( 𝑞 “ ( 𝐺 supp 0 ) ) ⊆ ( dom ( 𝑞 “ ( 𝐺 supp 0 ) ) × ran ( 𝑞 “ ( 𝐺 supp 0 ) ) ) )
110	109	sscond	⊢ ( ( ( 𝜑 ∧ 𝑞 ∈ ( ( 𝐸 × 𝐹 ) ↑_m Word ( 𝐸 ∪ 𝐹 ) ) ) ∧ 𝑓 ∈ ( 𝐹 ∖ ran ( 𝑞 “ ( 𝐺 supp 0 ) ) ) ) → ( ( 𝐸 × 𝐹 ) ∖ ( dom ( 𝑞 “ ( 𝐺 supp 0 ) ) × ran ( 𝑞 “ ( 𝐺 supp 0 ) ) ) ) ⊆ ( ( 𝐸 × 𝐹 ) ∖ ( 𝑞 “ ( 𝐺 supp 0 ) ) ) )
111	100 110	sstrd	⊢ ( ( ( 𝜑 ∧ 𝑞 ∈ ( ( 𝐸 × 𝐹 ) ↑_m Word ( 𝐸 ∪ 𝐹 ) ) ) ∧ 𝑓 ∈ ( 𝐹 ∖ ran ( 𝑞 “ ( 𝐺 supp 0 ) ) ) ) → ( 𝐸 × { 𝑓 } ) ⊆ ( ( 𝐸 × 𝐹 ) ∖ ( 𝑞 “ ( 𝐺 supp 0 ) ) ) )
112		imass2	⊢ ( ( 𝐸 × { 𝑓 } ) ⊆ ( ( 𝐸 × 𝐹 ) ∖ ( 𝑞 “ ( 𝐺 supp 0 ) ) ) → ( ^◡ 𝑞 “ ( 𝐸 × { 𝑓 } ) ) ⊆ ( ^◡ 𝑞 “ ( ( 𝐸 × 𝐹 ) ∖ ( 𝑞 “ ( 𝐺 supp 0 ) ) ) ) )
113	111 112	syl	⊢ ( ( ( 𝜑 ∧ 𝑞 ∈ ( ( 𝐸 × 𝐹 ) ↑_m Word ( 𝐸 ∪ 𝐹 ) ) ) ∧ 𝑓 ∈ ( 𝐹 ∖ ran ( 𝑞 “ ( 𝐺 supp 0 ) ) ) ) → ( ^◡ 𝑞 “ ( 𝐸 × { 𝑓 } ) ) ⊆ ( ^◡ 𝑞 “ ( ( 𝐸 × 𝐹 ) ∖ ( 𝑞 “ ( 𝐺 supp 0 ) ) ) ) )
114	113	adantlr	⊢ ( ( ( ( 𝜑 ∧ 𝑞 ∈ ( ( 𝐸 × 𝐹 ) ↑_m Word ( 𝐸 ∪ 𝐹 ) ) ) ∧ ∀ 𝑤 ∈ Word ( 𝐸 ∪ 𝐹 ) ( ( mulGrp ‘ 𝑅 ) Σ_g 𝑤 ) = ( ( 1^st ‘ ( 𝑞 ‘ 𝑤 ) ) · ( 2^nd ‘ ( 𝑞 ‘ 𝑤 ) ) ) ) ∧ 𝑓 ∈ ( 𝐹 ∖ ran ( 𝑞 “ ( 𝐺 supp 0 ) ) ) ) → ( ^◡ 𝑞 “ ( 𝐸 × { 𝑓 } ) ) ⊆ ( ^◡ 𝑞 “ ( ( 𝐸 × 𝐹 ) ∖ ( 𝑞 “ ( 𝐺 supp 0 ) ) ) ) )
115	82	adantr	⊢ ( ( ( ( 𝜑 ∧ 𝑞 ∈ ( ( 𝐸 × 𝐹 ) ↑_m Word ( 𝐸 ∪ 𝐹 ) ) ) ∧ ∀ 𝑤 ∈ Word ( 𝐸 ∪ 𝐹 ) ( ( mulGrp ‘ 𝑅 ) Σ_g 𝑤 ) = ( ( 1^st ‘ ( 𝑞 ‘ 𝑤 ) ) · ( 2^nd ‘ ( 𝑞 ‘ 𝑤 ) ) ) ) ∧ 𝑓 ∈ ( 𝐹 ∖ ran ( 𝑞 “ ( 𝐺 supp 0 ) ) ) ) → Fun 𝑞 )
116		difpreima	⊢ ( Fun 𝑞 → ( ^◡ 𝑞 “ ( ( 𝐸 × 𝐹 ) ∖ ( 𝑞 “ ( 𝐺 supp 0 ) ) ) ) = ( ( ^◡ 𝑞 “ ( 𝐸 × 𝐹 ) ) ∖ ( ^◡ 𝑞 “ ( 𝑞 “ ( 𝐺 supp 0 ) ) ) ) )
117	115 116	syl	⊢ ( ( ( ( 𝜑 ∧ 𝑞 ∈ ( ( 𝐸 × 𝐹 ) ↑_m Word ( 𝐸 ∪ 𝐹 ) ) ) ∧ ∀ 𝑤 ∈ Word ( 𝐸 ∪ 𝐹 ) ( ( mulGrp ‘ 𝑅 ) Σ_g 𝑤 ) = ( ( 1^st ‘ ( 𝑞 ‘ 𝑤 ) ) · ( 2^nd ‘ ( 𝑞 ‘ 𝑤 ) ) ) ) ∧ 𝑓 ∈ ( 𝐹 ∖ ran ( 𝑞 “ ( 𝐺 supp 0 ) ) ) ) → ( ^◡ 𝑞 “ ( ( 𝐸 × 𝐹 ) ∖ ( 𝑞 “ ( 𝐺 supp 0 ) ) ) ) = ( ( ^◡ 𝑞 “ ( 𝐸 × 𝐹 ) ) ∖ ( ^◡ 𝑞 “ ( 𝑞 “ ( 𝐺 supp 0 ) ) ) ) )
118		cnvimass	⊢ ( ^◡ 𝑞 “ ( 𝐸 × 𝐹 ) ) ⊆ dom 𝑞
119	42	ad2antrr	⊢ ( ( ( ( 𝜑 ∧ 𝑞 ∈ ( ( 𝐸 × 𝐹 ) ↑_m Word ( 𝐸 ∪ 𝐹 ) ) ) ∧ ∀ 𝑤 ∈ Word ( 𝐸 ∪ 𝐹 ) ( ( mulGrp ‘ 𝑅 ) Σ_g 𝑤 ) = ( ( 1^st ‘ ( 𝑞 ‘ 𝑤 ) ) · ( 2^nd ‘ ( 𝑞 ‘ 𝑤 ) ) ) ) ∧ 𝑓 ∈ ( 𝐹 ∖ ran ( 𝑞 “ ( 𝐺 supp 0 ) ) ) ) → dom 𝑞 = Word ( 𝐸 ∪ 𝐹 ) )
120	118 119	sseqtrid	⊢ ( ( ( ( 𝜑 ∧ 𝑞 ∈ ( ( 𝐸 × 𝐹 ) ↑_m Word ( 𝐸 ∪ 𝐹 ) ) ) ∧ ∀ 𝑤 ∈ Word ( 𝐸 ∪ 𝐹 ) ( ( mulGrp ‘ 𝑅 ) Σ_g 𝑤 ) = ( ( 1^st ‘ ( 𝑞 ‘ 𝑤 ) ) · ( 2^nd ‘ ( 𝑞 ‘ 𝑤 ) ) ) ) ∧ 𝑓 ∈ ( 𝐹 ∖ ran ( 𝑞 “ ( 𝐺 supp 0 ) ) ) ) → ( ^◡ 𝑞 “ ( 𝐸 × 𝐹 ) ) ⊆ Word ( 𝐸 ∪ 𝐹 ) )
121		suppssdm	⊢ ( 𝐺 supp 0 ) ⊆ dom 𝐺
122	9	fdmd	⊢ ( 𝜑 → dom 𝐺 = Word ( 𝐸 ∪ 𝐹 ) )
123	122	ad3antrrr	⊢ ( ( ( ( 𝜑 ∧ 𝑞 ∈ ( ( 𝐸 × 𝐹 ) ↑_m Word ( 𝐸 ∪ 𝐹 ) ) ) ∧ ∀ 𝑤 ∈ Word ( 𝐸 ∪ 𝐹 ) ( ( mulGrp ‘ 𝑅 ) Σ_g 𝑤 ) = ( ( 1^st ‘ ( 𝑞 ‘ 𝑤 ) ) · ( 2^nd ‘ ( 𝑞 ‘ 𝑤 ) ) ) ) ∧ 𝑓 ∈ ( 𝐹 ∖ ran ( 𝑞 “ ( 𝐺 supp 0 ) ) ) ) → dom 𝐺 = Word ( 𝐸 ∪ 𝐹 ) )
124	121 123	sseqtrid	⊢ ( ( ( ( 𝜑 ∧ 𝑞 ∈ ( ( 𝐸 × 𝐹 ) ↑_m Word ( 𝐸 ∪ 𝐹 ) ) ) ∧ ∀ 𝑤 ∈ Word ( 𝐸 ∪ 𝐹 ) ( ( mulGrp ‘ 𝑅 ) Σ_g 𝑤 ) = ( ( 1^st ‘ ( 𝑞 ‘ 𝑤 ) ) · ( 2^nd ‘ ( 𝑞 ‘ 𝑤 ) ) ) ) ∧ 𝑓 ∈ ( 𝐹 ∖ ran ( 𝑞 “ ( 𝐺 supp 0 ) ) ) ) → ( 𝐺 supp 0 ) ⊆ Word ( 𝐸 ∪ 𝐹 ) )
125	124 119	sseqtrrd	⊢ ( ( ( ( 𝜑 ∧ 𝑞 ∈ ( ( 𝐸 × 𝐹 ) ↑_m Word ( 𝐸 ∪ 𝐹 ) ) ) ∧ ∀ 𝑤 ∈ Word ( 𝐸 ∪ 𝐹 ) ( ( mulGrp ‘ 𝑅 ) Σ_g 𝑤 ) = ( ( 1^st ‘ ( 𝑞 ‘ 𝑤 ) ) · ( 2^nd ‘ ( 𝑞 ‘ 𝑤 ) ) ) ) ∧ 𝑓 ∈ ( 𝐹 ∖ ran ( 𝑞 “ ( 𝐺 supp 0 ) ) ) ) → ( 𝐺 supp 0 ) ⊆ dom 𝑞 )
126		sseqin2	⊢ ( ( 𝐺 supp 0 ) ⊆ dom 𝑞 ↔ ( dom 𝑞 ∩ ( 𝐺 supp 0 ) ) = ( 𝐺 supp 0 ) )
127	126	biimpi	⊢ ( ( 𝐺 supp 0 ) ⊆ dom 𝑞 → ( dom 𝑞 ∩ ( 𝐺 supp 0 ) ) = ( 𝐺 supp 0 ) )
128		dminss	⊢ ( dom 𝑞 ∩ ( 𝐺 supp 0 ) ) ⊆ ( ^◡ 𝑞 “ ( 𝑞 “ ( 𝐺 supp 0 ) ) )
129	127 128	eqsstrrdi	⊢ ( ( 𝐺 supp 0 ) ⊆ dom 𝑞 → ( 𝐺 supp 0 ) ⊆ ( ^◡ 𝑞 “ ( 𝑞 “ ( 𝐺 supp 0 ) ) ) )
130	125 129	syl	⊢ ( ( ( ( 𝜑 ∧ 𝑞 ∈ ( ( 𝐸 × 𝐹 ) ↑_m Word ( 𝐸 ∪ 𝐹 ) ) ) ∧ ∀ 𝑤 ∈ Word ( 𝐸 ∪ 𝐹 ) ( ( mulGrp ‘ 𝑅 ) Σ_g 𝑤 ) = ( ( 1^st ‘ ( 𝑞 ‘ 𝑤 ) ) · ( 2^nd ‘ ( 𝑞 ‘ 𝑤 ) ) ) ) ∧ 𝑓 ∈ ( 𝐹 ∖ ran ( 𝑞 “ ( 𝐺 supp 0 ) ) ) ) → ( 𝐺 supp 0 ) ⊆ ( ^◡ 𝑞 “ ( 𝑞 “ ( 𝐺 supp 0 ) ) ) )
131	120 130	ssdif2d	⊢ ( ( ( ( 𝜑 ∧ 𝑞 ∈ ( ( 𝐸 × 𝐹 ) ↑_m Word ( 𝐸 ∪ 𝐹 ) ) ) ∧ ∀ 𝑤 ∈ Word ( 𝐸 ∪ 𝐹 ) ( ( mulGrp ‘ 𝑅 ) Σ_g 𝑤 ) = ( ( 1^st ‘ ( 𝑞 ‘ 𝑤 ) ) · ( 2^nd ‘ ( 𝑞 ‘ 𝑤 ) ) ) ) ∧ 𝑓 ∈ ( 𝐹 ∖ ran ( 𝑞 “ ( 𝐺 supp 0 ) ) ) ) → ( ( ^◡ 𝑞 “ ( 𝐸 × 𝐹 ) ) ∖ ( ^◡ 𝑞 “ ( 𝑞 “ ( 𝐺 supp 0 ) ) ) ) ⊆ ( Word ( 𝐸 ∪ 𝐹 ) ∖ ( 𝐺 supp 0 ) ) )
132	117 131	eqsstrd	⊢ ( ( ( ( 𝜑 ∧ 𝑞 ∈ ( ( 𝐸 × 𝐹 ) ↑_m Word ( 𝐸 ∪ 𝐹 ) ) ) ∧ ∀ 𝑤 ∈ Word ( 𝐸 ∪ 𝐹 ) ( ( mulGrp ‘ 𝑅 ) Σ_g 𝑤 ) = ( ( 1^st ‘ ( 𝑞 ‘ 𝑤 ) ) · ( 2^nd ‘ ( 𝑞 ‘ 𝑤 ) ) ) ) ∧ 𝑓 ∈ ( 𝐹 ∖ ran ( 𝑞 “ ( 𝐺 supp 0 ) ) ) ) → ( ^◡ 𝑞 “ ( ( 𝐸 × 𝐹 ) ∖ ( 𝑞 “ ( 𝐺 supp 0 ) ) ) ) ⊆ ( Word ( 𝐸 ∪ 𝐹 ) ∖ ( 𝐺 supp 0 ) ) )
133	114 132	sstrd	⊢ ( ( ( ( 𝜑 ∧ 𝑞 ∈ ( ( 𝐸 × 𝐹 ) ↑_m Word ( 𝐸 ∪ 𝐹 ) ) ) ∧ ∀ 𝑤 ∈ Word ( 𝐸 ∪ 𝐹 ) ( ( mulGrp ‘ 𝑅 ) Σ_g 𝑤 ) = ( ( 1^st ‘ ( 𝑞 ‘ 𝑤 ) ) · ( 2^nd ‘ ( 𝑞 ‘ 𝑤 ) ) ) ) ∧ 𝑓 ∈ ( 𝐹 ∖ ran ( 𝑞 “ ( 𝐺 supp 0 ) ) ) ) → ( ^◡ 𝑞 “ ( 𝐸 × { 𝑓 } ) ) ⊆ ( Word ( 𝐸 ∪ 𝐹 ) ∖ ( 𝐺 supp 0 ) ) )
134	133	sselda	⊢ ( ( ( ( ( 𝜑 ∧ 𝑞 ∈ ( ( 𝐸 × 𝐹 ) ↑_m Word ( 𝐸 ∪ 𝐹 ) ) ) ∧ ∀ 𝑤 ∈ Word ( 𝐸 ∪ 𝐹 ) ( ( mulGrp ‘ 𝑅 ) Σ_g 𝑤 ) = ( ( 1^st ‘ ( 𝑞 ‘ 𝑤 ) ) · ( 2^nd ‘ ( 𝑞 ‘ 𝑤 ) ) ) ) ∧ 𝑓 ∈ ( 𝐹 ∖ ran ( 𝑞 “ ( 𝐺 supp 0 ) ) ) ) ∧ 𝑣 ∈ ( ^◡ 𝑞 “ ( 𝐸 × { 𝑓 } ) ) ) → 𝑣 ∈ ( Word ( 𝐸 ∪ 𝐹 ) ∖ ( 𝐺 supp 0 ) ) )
135	90 91 92 134	fvdifsupp	⊢ ( ( ( ( ( 𝜑 ∧ 𝑞 ∈ ( ( 𝐸 × 𝐹 ) ↑_m Word ( 𝐸 ∪ 𝐹 ) ) ) ∧ ∀ 𝑤 ∈ Word ( 𝐸 ∪ 𝐹 ) ( ( mulGrp ‘ 𝑅 ) Σ_g 𝑤 ) = ( ( 1^st ‘ ( 𝑞 ‘ 𝑤 ) ) · ( 2^nd ‘ ( 𝑞 ‘ 𝑤 ) ) ) ) ∧ 𝑓 ∈ ( 𝐹 ∖ ran ( 𝑞 “ ( 𝐺 supp 0 ) ) ) ) ∧ 𝑣 ∈ ( ^◡ 𝑞 “ ( 𝐸 × { 𝑓 } ) ) ) → ( 𝐺 ‘ 𝑣 ) = 0 )
136	135	oveq1d	⊢ ( ( ( ( ( 𝜑 ∧ 𝑞 ∈ ( ( 𝐸 × 𝐹 ) ↑_m Word ( 𝐸 ∪ 𝐹 ) ) ) ∧ ∀ 𝑤 ∈ Word ( 𝐸 ∪ 𝐹 ) ( ( mulGrp ‘ 𝑅 ) Σ_g 𝑤 ) = ( ( 1^st ‘ ( 𝑞 ‘ 𝑤 ) ) · ( 2^nd ‘ ( 𝑞 ‘ 𝑤 ) ) ) ) ∧ 𝑓 ∈ ( 𝐹 ∖ ran ( 𝑞 “ ( 𝐺 supp 0 ) ) ) ) ∧ 𝑣 ∈ ( ^◡ 𝑞 “ ( 𝐸 × { 𝑓 } ) ) ) → ( ( 𝐺 ‘ 𝑣 ) ( ._g ‘ 𝑅 ) ( 1^st ‘ ( 𝑞 ‘ 𝑣 ) ) ) = ( 0 ( ._g ‘ 𝑅 ) ( 1^st ‘ ( 𝑞 ‘ 𝑣 ) ) ) )
137	55	ad4antr	⊢ ( ( ( ( ( 𝜑 ∧ 𝑞 ∈ ( ( 𝐸 × 𝐹 ) ↑_m Word ( 𝐸 ∪ 𝐹 ) ) ) ∧ ∀ 𝑤 ∈ Word ( 𝐸 ∪ 𝐹 ) ( ( mulGrp ‘ 𝑅 ) Σ_g 𝑤 ) = ( ( 1^st ‘ ( 𝑞 ‘ 𝑤 ) ) · ( 2^nd ‘ ( 𝑞 ‘ 𝑤 ) ) ) ) ∧ 𝑓 ∈ ( 𝐹 ∖ ran ( 𝑞 “ ( 𝐺 supp 0 ) ) ) ) ∧ 𝑣 ∈ ( ^◡ 𝑞 “ ( 𝐸 × { 𝑓 } ) ) ) → 𝐸 ⊆ 𝐵 )
138	32	ad3antrrr	⊢ ( ( ( ( ( 𝜑 ∧ 𝑞 ∈ ( ( 𝐸 × 𝐹 ) ↑_m Word ( 𝐸 ∪ 𝐹 ) ) ) ∧ ∀ 𝑤 ∈ Word ( 𝐸 ∪ 𝐹 ) ( ( mulGrp ‘ 𝑅 ) Σ_g 𝑤 ) = ( ( 1^st ‘ ( 𝑞 ‘ 𝑤 ) ) · ( 2^nd ‘ ( 𝑞 ‘ 𝑤 ) ) ) ) ∧ 𝑓 ∈ ( 𝐹 ∖ ran ( 𝑞 “ ( 𝐺 supp 0 ) ) ) ) ∧ 𝑣 ∈ ( ^◡ 𝑞 “ ( 𝐸 × { 𝑓 } ) ) ) → 𝑞 : Word ( 𝐸 ∪ 𝐹 ) ⟶ ( 𝐸 × 𝐹 ) )
139	41 42	sseqtrid	⊢ ( ( 𝜑 ∧ 𝑞 ∈ ( ( 𝐸 × 𝐹 ) ↑_m Word ( 𝐸 ∪ 𝐹 ) ) ) → ( ^◡ 𝑞 “ ( 𝐸 × { 𝑓 } ) ) ⊆ Word ( 𝐸 ∪ 𝐹 ) )
140	139	ad2antrr	⊢ ( ( ( ( 𝜑 ∧ 𝑞 ∈ ( ( 𝐸 × 𝐹 ) ↑_m Word ( 𝐸 ∪ 𝐹 ) ) ) ∧ ∀ 𝑤 ∈ Word ( 𝐸 ∪ 𝐹 ) ( ( mulGrp ‘ 𝑅 ) Σ_g 𝑤 ) = ( ( 1^st ‘ ( 𝑞 ‘ 𝑤 ) ) · ( 2^nd ‘ ( 𝑞 ‘ 𝑤 ) ) ) ) ∧ 𝑓 ∈ ( 𝐹 ∖ ran ( 𝑞 “ ( 𝐺 supp 0 ) ) ) ) → ( ^◡ 𝑞 “ ( 𝐸 × { 𝑓 } ) ) ⊆ Word ( 𝐸 ∪ 𝐹 ) )
141	140	sselda	⊢ ( ( ( ( ( 𝜑 ∧ 𝑞 ∈ ( ( 𝐸 × 𝐹 ) ↑_m Word ( 𝐸 ∪ 𝐹 ) ) ) ∧ ∀ 𝑤 ∈ Word ( 𝐸 ∪ 𝐹 ) ( ( mulGrp ‘ 𝑅 ) Σ_g 𝑤 ) = ( ( 1^st ‘ ( 𝑞 ‘ 𝑤 ) ) · ( 2^nd ‘ ( 𝑞 ‘ 𝑤 ) ) ) ) ∧ 𝑓 ∈ ( 𝐹 ∖ ran ( 𝑞 “ ( 𝐺 supp 0 ) ) ) ) ∧ 𝑣 ∈ ( ^◡ 𝑞 “ ( 𝐸 × { 𝑓 } ) ) ) → 𝑣 ∈ Word ( 𝐸 ∪ 𝐹 ) )
142	138 141	ffvelcdmd	⊢ ( ( ( ( ( 𝜑 ∧ 𝑞 ∈ ( ( 𝐸 × 𝐹 ) ↑_m Word ( 𝐸 ∪ 𝐹 ) ) ) ∧ ∀ 𝑤 ∈ Word ( 𝐸 ∪ 𝐹 ) ( ( mulGrp ‘ 𝑅 ) Σ_g 𝑤 ) = ( ( 1^st ‘ ( 𝑞 ‘ 𝑤 ) ) · ( 2^nd ‘ ( 𝑞 ‘ 𝑤 ) ) ) ) ∧ 𝑓 ∈ ( 𝐹 ∖ ran ( 𝑞 “ ( 𝐺 supp 0 ) ) ) ) ∧ 𝑣 ∈ ( ^◡ 𝑞 “ ( 𝐸 × { 𝑓 } ) ) ) → ( 𝑞 ‘ 𝑣 ) ∈ ( 𝐸 × 𝐹 ) )
143		xp1st	⊢ ( ( 𝑞 ‘ 𝑣 ) ∈ ( 𝐸 × 𝐹 ) → ( 1^st ‘ ( 𝑞 ‘ 𝑣 ) ) ∈ 𝐸 )
144	142 143	syl	⊢ ( ( ( ( ( 𝜑 ∧ 𝑞 ∈ ( ( 𝐸 × 𝐹 ) ↑_m Word ( 𝐸 ∪ 𝐹 ) ) ) ∧ ∀ 𝑤 ∈ Word ( 𝐸 ∪ 𝐹 ) ( ( mulGrp ‘ 𝑅 ) Σ_g 𝑤 ) = ( ( 1^st ‘ ( 𝑞 ‘ 𝑤 ) ) · ( 2^nd ‘ ( 𝑞 ‘ 𝑤 ) ) ) ) ∧ 𝑓 ∈ ( 𝐹 ∖ ran ( 𝑞 “ ( 𝐺 supp 0 ) ) ) ) ∧ 𝑣 ∈ ( ^◡ 𝑞 “ ( 𝐸 × { 𝑓 } ) ) ) → ( 1^st ‘ ( 𝑞 ‘ 𝑣 ) ) ∈ 𝐸 )
145	137 144	sseldd	⊢ ( ( ( ( ( 𝜑 ∧ 𝑞 ∈ ( ( 𝐸 × 𝐹 ) ↑_m Word ( 𝐸 ∪ 𝐹 ) ) ) ∧ ∀ 𝑤 ∈ Word ( 𝐸 ∪ 𝐹 ) ( ( mulGrp ‘ 𝑅 ) Σ_g 𝑤 ) = ( ( 1^st ‘ ( 𝑞 ‘ 𝑤 ) ) · ( 2^nd ‘ ( 𝑞 ‘ 𝑤 ) ) ) ) ∧ 𝑓 ∈ ( 𝐹 ∖ ran ( 𝑞 “ ( 𝐺 supp 0 ) ) ) ) ∧ 𝑣 ∈ ( ^◡ 𝑞 “ ( 𝐸 × { 𝑓 } ) ) ) → ( 1^st ‘ ( 𝑞 ‘ 𝑣 ) ) ∈ 𝐵 )
146	1 3 24	mulg0	⊢ ( ( 1^st ‘ ( 𝑞 ‘ 𝑣 ) ) ∈ 𝐵 → ( 0 ( ._g ‘ 𝑅 ) ( 1^st ‘ ( 𝑞 ‘ 𝑣 ) ) ) = 0 )
147	145 146	syl	⊢ ( ( ( ( ( 𝜑 ∧ 𝑞 ∈ ( ( 𝐸 × 𝐹 ) ↑_m Word ( 𝐸 ∪ 𝐹 ) ) ) ∧ ∀ 𝑤 ∈ Word ( 𝐸 ∪ 𝐹 ) ( ( mulGrp ‘ 𝑅 ) Σ_g 𝑤 ) = ( ( 1^st ‘ ( 𝑞 ‘ 𝑤 ) ) · ( 2^nd ‘ ( 𝑞 ‘ 𝑤 ) ) ) ) ∧ 𝑓 ∈ ( 𝐹 ∖ ran ( 𝑞 “ ( 𝐺 supp 0 ) ) ) ) ∧ 𝑣 ∈ ( ^◡ 𝑞 “ ( 𝐸 × { 𝑓 } ) ) ) → ( 0 ( ._g ‘ 𝑅 ) ( 1^st ‘ ( 𝑞 ‘ 𝑣 ) ) ) = 0 )
148	136 147	eqtrd	⊢ ( ( ( ( ( 𝜑 ∧ 𝑞 ∈ ( ( 𝐸 × 𝐹 ) ↑_m Word ( 𝐸 ∪ 𝐹 ) ) ) ∧ ∀ 𝑤 ∈ Word ( 𝐸 ∪ 𝐹 ) ( ( mulGrp ‘ 𝑅 ) Σ_g 𝑤 ) = ( ( 1^st ‘ ( 𝑞 ‘ 𝑤 ) ) · ( 2^nd ‘ ( 𝑞 ‘ 𝑤 ) ) ) ) ∧ 𝑓 ∈ ( 𝐹 ∖ ran ( 𝑞 “ ( 𝐺 supp 0 ) ) ) ) ∧ 𝑣 ∈ ( ^◡ 𝑞 “ ( 𝐸 × { 𝑓 } ) ) ) → ( ( 𝐺 ‘ 𝑣 ) ( ._g ‘ 𝑅 ) ( 1^st ‘ ( 𝑞 ‘ 𝑣 ) ) ) = 0 )
149	148	mpteq2dva	⊢ ( ( ( ( 𝜑 ∧ 𝑞 ∈ ( ( 𝐸 × 𝐹 ) ↑_m Word ( 𝐸 ∪ 𝐹 ) ) ) ∧ ∀ 𝑤 ∈ Word ( 𝐸 ∪ 𝐹 ) ( ( mulGrp ‘ 𝑅 ) Σ_g 𝑤 ) = ( ( 1^st ‘ ( 𝑞 ‘ 𝑤 ) ) · ( 2^nd ‘ ( 𝑞 ‘ 𝑤 ) ) ) ) ∧ 𝑓 ∈ ( 𝐹 ∖ ran ( 𝑞 “ ( 𝐺 supp 0 ) ) ) ) → ( 𝑣 ∈ ( ^◡ 𝑞 “ ( 𝐸 × { 𝑓 } ) ) ↦ ( ( 𝐺 ‘ 𝑣 ) ( ._g ‘ 𝑅 ) ( 1^st ‘ ( 𝑞 ‘ 𝑣 ) ) ) ) = ( 𝑣 ∈ ( ^◡ 𝑞 “ ( 𝐸 × { 𝑓 } ) ) ↦ 0 ) )
150	149	oveq2d	⊢ ( ( ( ( 𝜑 ∧ 𝑞 ∈ ( ( 𝐸 × 𝐹 ) ↑_m Word ( 𝐸 ∪ 𝐹 ) ) ) ∧ ∀ 𝑤 ∈ Word ( 𝐸 ∪ 𝐹 ) ( ( mulGrp ‘ 𝑅 ) Σ_g 𝑤 ) = ( ( 1^st ‘ ( 𝑞 ‘ 𝑤 ) ) · ( 2^nd ‘ ( 𝑞 ‘ 𝑤 ) ) ) ) ∧ 𝑓 ∈ ( 𝐹 ∖ ran ( 𝑞 “ ( 𝐺 supp 0 ) ) ) ) → ( 𝑅 Σ_g ( 𝑣 ∈ ( ^◡ 𝑞 “ ( 𝐸 × { 𝑓 } ) ) ↦ ( ( 𝐺 ‘ 𝑣 ) ( ._g ‘ 𝑅 ) ( 1^st ‘ ( 𝑞 ‘ 𝑣 ) ) ) ) ) = ( 𝑅 Σ_g ( 𝑣 ∈ ( ^◡ 𝑞 “ ( 𝐸 × { 𝑓 } ) ) ↦ 0 ) ) )
151	25	grpmndd	⊢ ( 𝜑 → 𝑅 ∈ Mnd )
152	151	ad3antrrr	⊢ ( ( ( ( 𝜑 ∧ 𝑞 ∈ ( ( 𝐸 × 𝐹 ) ↑_m Word ( 𝐸 ∪ 𝐹 ) ) ) ∧ ∀ 𝑤 ∈ Word ( 𝐸 ∪ 𝐹 ) ( ( mulGrp ‘ 𝑅 ) Σ_g 𝑤 ) = ( ( 1^st ‘ ( 𝑞 ‘ 𝑤 ) ) · ( 2^nd ‘ ( 𝑞 ‘ 𝑤 ) ) ) ) ∧ 𝑓 ∈ ( 𝐹 ∖ ran ( 𝑞 “ ( 𝐺 supp 0 ) ) ) ) → 𝑅 ∈ Mnd )
153	19	a1i	⊢ ( ( ( ( 𝜑 ∧ 𝑞 ∈ ( ( 𝐸 × 𝐹 ) ↑_m Word ( 𝐸 ∪ 𝐹 ) ) ) ∧ ∀ 𝑤 ∈ Word ( 𝐸 ∪ 𝐹 ) ( ( mulGrp ‘ 𝑅 ) Σ_g 𝑤 ) = ( ( 1^st ‘ ( 𝑞 ‘ 𝑤 ) ) · ( 2^nd ‘ ( 𝑞 ‘ 𝑤 ) ) ) ) ∧ 𝑓 ∈ ( 𝐹 ∖ ran ( 𝑞 “ ( 𝐺 supp 0 ) ) ) ) → ( ^◡ 𝑞 “ ( 𝐸 × { 𝑓 } ) ) ∈ V )
154	3	gsumz	⊢ ( ( 𝑅 ∈ Mnd ∧ ( ^◡ 𝑞 “ ( 𝐸 × { 𝑓 } ) ) ∈ V ) → ( 𝑅 Σ_g ( 𝑣 ∈ ( ^◡ 𝑞 “ ( 𝐸 × { 𝑓 } ) ) ↦ 0 ) ) = 0 )
155	152 153 154	syl2anc	⊢ ( ( ( ( 𝜑 ∧ 𝑞 ∈ ( ( 𝐸 × 𝐹 ) ↑_m Word ( 𝐸 ∪ 𝐹 ) ) ) ∧ ∀ 𝑤 ∈ Word ( 𝐸 ∪ 𝐹 ) ( ( mulGrp ‘ 𝑅 ) Σ_g 𝑤 ) = ( ( 1^st ‘ ( 𝑞 ‘ 𝑤 ) ) · ( 2^nd ‘ ( 𝑞 ‘ 𝑤 ) ) ) ) ∧ 𝑓 ∈ ( 𝐹 ∖ ran ( 𝑞 “ ( 𝐺 supp 0 ) ) ) ) → ( 𝑅 Σ_g ( 𝑣 ∈ ( ^◡ 𝑞 “ ( 𝐸 × { 𝑓 } ) ) ↦ 0 ) ) = 0 )
156	150 155	eqtrd	⊢ ( ( ( ( 𝜑 ∧ 𝑞 ∈ ( ( 𝐸 × 𝐹 ) ↑_m Word ( 𝐸 ∪ 𝐹 ) ) ) ∧ ∀ 𝑤 ∈ Word ( 𝐸 ∪ 𝐹 ) ( ( mulGrp ‘ 𝑅 ) Σ_g 𝑤 ) = ( ( 1^st ‘ ( 𝑞 ‘ 𝑤 ) ) · ( 2^nd ‘ ( 𝑞 ‘ 𝑤 ) ) ) ) ∧ 𝑓 ∈ ( 𝐹 ∖ ran ( 𝑞 “ ( 𝐺 supp 0 ) ) ) ) → ( 𝑅 Σ_g ( 𝑣 ∈ ( ^◡ 𝑞 “ ( 𝐸 × { 𝑓 } ) ) ↦ ( ( 𝐺 ‘ 𝑣 ) ( ._g ‘ 𝑅 ) ( 1^st ‘ ( 𝑞 ‘ 𝑣 ) ) ) ) ) = 0 )
157	156 13	suppss2	⊢ ( ( ( 𝜑 ∧ 𝑞 ∈ ( ( 𝐸 × 𝐹 ) ↑_m Word ( 𝐸 ∪ 𝐹 ) ) ) ∧ ∀ 𝑤 ∈ Word ( 𝐸 ∪ 𝐹 ) ( ( mulGrp ‘ 𝑅 ) Σ_g 𝑤 ) = ( ( 1^st ‘ ( 𝑞 ‘ 𝑤 ) ) · ( 2^nd ‘ ( 𝑞 ‘ 𝑤 ) ) ) ) → ( ( 𝑓 ∈ 𝐹 ↦ ( 𝑅 Σ_g ( 𝑣 ∈ ( ^◡ 𝑞 “ ( 𝐸 × { 𝑓 } ) ) ↦ ( ( 𝐺 ‘ 𝑣 ) ( ._g ‘ 𝑅 ) ( 1^st ‘ ( 𝑞 ‘ 𝑣 ) ) ) ) ) ) supp 0 ) ⊆ ran ( 𝑞 “ ( 𝐺 supp 0 ) ) )
158	88 157	ssfid	⊢ ( ( ( 𝜑 ∧ 𝑞 ∈ ( ( 𝐸 × 𝐹 ) ↑_m Word ( 𝐸 ∪ 𝐹 ) ) ) ∧ ∀ 𝑤 ∈ Word ( 𝐸 ∪ 𝐹 ) ( ( mulGrp ‘ 𝑅 ) Σ_g 𝑤 ) = ( ( 1^st ‘ ( 𝑞 ‘ 𝑤 ) ) · ( 2^nd ‘ ( 𝑞 ‘ 𝑤 ) ) ) ) → ( ( 𝑓 ∈ 𝐹 ↦ ( 𝑅 Σ_g ( 𝑣 ∈ ( ^◡ 𝑞 “ ( 𝐸 × { 𝑓 } ) ) ↦ ( ( 𝐺 ‘ 𝑣 ) ( ._g ‘ 𝑅 ) ( 1^st ‘ ( 𝑞 ‘ 𝑣 ) ) ) ) ) ) supp 0 ) ∈ Fin )
159	65 80 81 158	isfsuppd	⊢ ( ( ( 𝜑 ∧ 𝑞 ∈ ( ( 𝐸 × 𝐹 ) ↑_m Word ( 𝐸 ∪ 𝐹 ) ) ) ∧ ∀ 𝑤 ∈ Word ( 𝐸 ∪ 𝐹 ) ( ( mulGrp ‘ 𝑅 ) Σ_g 𝑤 ) = ( ( 1^st ‘ ( 𝑞 ‘ 𝑤 ) ) · ( 2^nd ‘ ( 𝑞 ‘ 𝑤 ) ) ) ) → ( 𝑓 ∈ 𝐹 ↦ ( 𝑅 Σ_g ( 𝑣 ∈ ( ^◡ 𝑞 “ ( 𝐸 × { 𝑓 } ) ) ↦ ( ( 𝐺 ‘ 𝑣 ) ( ._g ‘ 𝑅 ) ( 1^st ‘ ( 𝑞 ‘ 𝑣 ) ) ) ) ) ) finSupp 0 )
160	15	ablcmnd	⊢ ( 𝜑 → 𝑅 ∈ CMnd )
161	160	adantr	⊢ ( ( 𝜑 ∧ 𝑞 ∈ ( ( 𝐸 × 𝐹 ) ↑_m Word ( 𝐸 ∪ 𝐹 ) ) ) → 𝑅 ∈ CMnd )
162	30	adantr	⊢ ( ( 𝜑 ∧ 𝑞 ∈ ( ( 𝐸 × 𝐹 ) ↑_m Word ( 𝐸 ∪ 𝐹 ) ) ) → Word ( 𝐸 ∪ 𝐹 ) ∈ V )
163	89	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝑞 ∈ ( ( 𝐸 × 𝐹 ) ↑_m Word ( 𝐸 ∪ 𝐹 ) ) ) ∧ 𝑤 ∈ ( Word ( 𝐸 ∪ 𝐹 ) ∖ ( 𝐺 supp 0 ) ) ) → 𝐺 Fn Word ( 𝐸 ∪ 𝐹 ) )
164	162	adantr	⊢ ( ( ( 𝜑 ∧ 𝑞 ∈ ( ( 𝐸 × 𝐹 ) ↑_m Word ( 𝐸 ∪ 𝐹 ) ) ) ∧ 𝑤 ∈ ( Word ( 𝐸 ∪ 𝐹 ) ∖ ( 𝐺 supp 0 ) ) ) → Word ( 𝐸 ∪ 𝐹 ) ∈ V )
165		0zd	⊢ ( ( ( 𝜑 ∧ 𝑞 ∈ ( ( 𝐸 × 𝐹 ) ↑_m Word ( 𝐸 ∪ 𝐹 ) ) ) ∧ 𝑤 ∈ ( Word ( 𝐸 ∪ 𝐹 ) ∖ ( 𝐺 supp 0 ) ) ) → 0 ∈ ℤ )
166		simpr	⊢ ( ( ( 𝜑 ∧ 𝑞 ∈ ( ( 𝐸 × 𝐹 ) ↑_m Word ( 𝐸 ∪ 𝐹 ) ) ) ∧ 𝑤 ∈ ( Word ( 𝐸 ∪ 𝐹 ) ∖ ( 𝐺 supp 0 ) ) ) → 𝑤 ∈ ( Word ( 𝐸 ∪ 𝐹 ) ∖ ( 𝐺 supp 0 ) ) )
167	163 164 165 166	fvdifsupp	⊢ ( ( ( 𝜑 ∧ 𝑞 ∈ ( ( 𝐸 × 𝐹 ) ↑_m Word ( 𝐸 ∪ 𝐹 ) ) ) ∧ 𝑤 ∈ ( Word ( 𝐸 ∪ 𝐹 ) ∖ ( 𝐺 supp 0 ) ) ) → ( 𝐺 ‘ 𝑤 ) = 0 )
168	167	oveq1d	⊢ ( ( ( 𝜑 ∧ 𝑞 ∈ ( ( 𝐸 × 𝐹 ) ↑_m Word ( 𝐸 ∪ 𝐹 ) ) ) ∧ 𝑤 ∈ ( Word ( 𝐸 ∪ 𝐹 ) ∖ ( 𝐺 supp 0 ) ) ) → ( ( 𝐺 ‘ 𝑤 ) ( ._g ‘ 𝑅 ) ( ( mulGrp ‘ 𝑅 ) Σ_g 𝑤 ) ) = ( 0 ( ._g ‘ 𝑅 ) ( ( mulGrp ‘ 𝑅 ) Σ_g 𝑤 ) ) )
169		eqid	⊢ ( mulGrp ‘ 𝑅 ) = ( mulGrp ‘ 𝑅 )
170	169	crngmgp	⊢ ( 𝑅 ∈ CRing → ( mulGrp ‘ 𝑅 ) ∈ CMnd )
171	5 170	syl	⊢ ( 𝜑 → ( mulGrp ‘ 𝑅 ) ∈ CMnd )
172	171	cmnmndd	⊢ ( 𝜑 → ( mulGrp ‘ 𝑅 ) ∈ Mnd )
173	172	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝑞 ∈ ( ( 𝐸 × 𝐹 ) ↑_m Word ( 𝐸 ∪ 𝐹 ) ) ) ∧ 𝑤 ∈ ( Word ( 𝐸 ∪ 𝐹 ) ∖ ( 𝐺 supp 0 ) ) ) → ( mulGrp ‘ 𝑅 ) ∈ Mnd )
174	1	subrgss	⊢ ( 𝐹 ∈ ( SubRing ‘ 𝑅 ) → 𝐹 ⊆ 𝐵 )
175	7 174	syl	⊢ ( 𝜑 → 𝐹 ⊆ 𝐵 )
176	55 175	unssd	⊢ ( 𝜑 → ( 𝐸 ∪ 𝐹 ) ⊆ 𝐵 )
177		sswrd	⊢ ( ( 𝐸 ∪ 𝐹 ) ⊆ 𝐵 → Word ( 𝐸 ∪ 𝐹 ) ⊆ Word 𝐵 )
178	176 177	syl	⊢ ( 𝜑 → Word ( 𝐸 ∪ 𝐹 ) ⊆ Word 𝐵 )
179	178	adantr	⊢ ( ( 𝜑 ∧ 𝑞 ∈ ( ( 𝐸 × 𝐹 ) ↑_m Word ( 𝐸 ∪ 𝐹 ) ) ) → Word ( 𝐸 ∪ 𝐹 ) ⊆ Word 𝐵 )
180	179	adantr	⊢ ( ( ( 𝜑 ∧ 𝑞 ∈ ( ( 𝐸 × 𝐹 ) ↑_m Word ( 𝐸 ∪ 𝐹 ) ) ) ∧ 𝑤 ∈ ( Word ( 𝐸 ∪ 𝐹 ) ∖ ( 𝐺 supp 0 ) ) ) → Word ( 𝐸 ∪ 𝐹 ) ⊆ Word 𝐵 )
181	166	eldifad	⊢ ( ( ( 𝜑 ∧ 𝑞 ∈ ( ( 𝐸 × 𝐹 ) ↑_m Word ( 𝐸 ∪ 𝐹 ) ) ) ∧ 𝑤 ∈ ( Word ( 𝐸 ∪ 𝐹 ) ∖ ( 𝐺 supp 0 ) ) ) → 𝑤 ∈ Word ( 𝐸 ∪ 𝐹 ) )
182	180 181	sseldd	⊢ ( ( ( 𝜑 ∧ 𝑞 ∈ ( ( 𝐸 × 𝐹 ) ↑_m Word ( 𝐸 ∪ 𝐹 ) ) ) ∧ 𝑤 ∈ ( Word ( 𝐸 ∪ 𝐹 ) ∖ ( 𝐺 supp 0 ) ) ) → 𝑤 ∈ Word 𝐵 )
183	169 1	mgpbas	⊢ 𝐵 = ( Base ‘ ( mulGrp ‘ 𝑅 ) )
184	183	gsumwcl	⊢ ( ( ( mulGrp ‘ 𝑅 ) ∈ Mnd ∧ 𝑤 ∈ Word 𝐵 ) → ( ( mulGrp ‘ 𝑅 ) Σ_g 𝑤 ) ∈ 𝐵 )
185	173 182 184	syl2anc	⊢ ( ( ( 𝜑 ∧ 𝑞 ∈ ( ( 𝐸 × 𝐹 ) ↑_m Word ( 𝐸 ∪ 𝐹 ) ) ) ∧ 𝑤 ∈ ( Word ( 𝐸 ∪ 𝐹 ) ∖ ( 𝐺 supp 0 ) ) ) → ( ( mulGrp ‘ 𝑅 ) Σ_g 𝑤 ) ∈ 𝐵 )
186	1 3 24	mulg0	⊢ ( ( ( mulGrp ‘ 𝑅 ) Σ_g 𝑤 ) ∈ 𝐵 → ( 0 ( ._g ‘ 𝑅 ) ( ( mulGrp ‘ 𝑅 ) Σ_g 𝑤 ) ) = 0 )
187	185 186	syl	⊢ ( ( ( 𝜑 ∧ 𝑞 ∈ ( ( 𝐸 × 𝐹 ) ↑_m Word ( 𝐸 ∪ 𝐹 ) ) ) ∧ 𝑤 ∈ ( Word ( 𝐸 ∪ 𝐹 ) ∖ ( 𝐺 supp 0 ) ) ) → ( 0 ( ._g ‘ 𝑅 ) ( ( mulGrp ‘ 𝑅 ) Σ_g 𝑤 ) ) = 0 )
188	168 187	eqtrd	⊢ ( ( ( 𝜑 ∧ 𝑞 ∈ ( ( 𝐸 × 𝐹 ) ↑_m Word ( 𝐸 ∪ 𝐹 ) ) ) ∧ 𝑤 ∈ ( Word ( 𝐸 ∪ 𝐹 ) ∖ ( 𝐺 supp 0 ) ) ) → ( ( 𝐺 ‘ 𝑤 ) ( ._g ‘ 𝑅 ) ( ( mulGrp ‘ 𝑅 ) Σ_g 𝑤 ) ) = 0 )
189	83	adantr	⊢ ( ( 𝜑 ∧ 𝑞 ∈ ( ( 𝐸 × 𝐹 ) ↑_m Word ( 𝐸 ∪ 𝐹 ) ) ) → ( 𝐺 supp 0 ) ∈ Fin )
190	25	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝑞 ∈ ( ( 𝐸 × 𝐹 ) ↑_m Word ( 𝐸 ∪ 𝐹 ) ) ) ∧ 𝑤 ∈ Word ( 𝐸 ∪ 𝐹 ) ) → 𝑅 ∈ Grp )
191	9	adantr	⊢ ( ( 𝜑 ∧ 𝑞 ∈ ( ( 𝐸 × 𝐹 ) ↑_m Word ( 𝐸 ∪ 𝐹 ) ) ) → 𝐺 : Word ( 𝐸 ∪ 𝐹 ) ⟶ ℤ )
192	191	ffvelcdmda	⊢ ( ( ( 𝜑 ∧ 𝑞 ∈ ( ( 𝐸 × 𝐹 ) ↑_m Word ( 𝐸 ∪ 𝐹 ) ) ) ∧ 𝑤 ∈ Word ( 𝐸 ∪ 𝐹 ) ) → ( 𝐺 ‘ 𝑤 ) ∈ ℤ )
193	172	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝑞 ∈ ( ( 𝐸 × 𝐹 ) ↑_m Word ( 𝐸 ∪ 𝐹 ) ) ) ∧ 𝑤 ∈ Word ( 𝐸 ∪ 𝐹 ) ) → ( mulGrp ‘ 𝑅 ) ∈ Mnd )
194	179	sselda	⊢ ( ( ( 𝜑 ∧ 𝑞 ∈ ( ( 𝐸 × 𝐹 ) ↑_m Word ( 𝐸 ∪ 𝐹 ) ) ) ∧ 𝑤 ∈ Word ( 𝐸 ∪ 𝐹 ) ) → 𝑤 ∈ Word 𝐵 )
195	193 194 184	syl2anc	⊢ ( ( ( 𝜑 ∧ 𝑞 ∈ ( ( 𝐸 × 𝐹 ) ↑_m Word ( 𝐸 ∪ 𝐹 ) ) ) ∧ 𝑤 ∈ Word ( 𝐸 ∪ 𝐹 ) ) → ( ( mulGrp ‘ 𝑅 ) Σ_g 𝑤 ) ∈ 𝐵 )
196	1 24 190 192 195	mulgcld	⊢ ( ( ( 𝜑 ∧ 𝑞 ∈ ( ( 𝐸 × 𝐹 ) ↑_m Word ( 𝐸 ∪ 𝐹 ) ) ) ∧ 𝑤 ∈ Word ( 𝐸 ∪ 𝐹 ) ) → ( ( 𝐺 ‘ 𝑤 ) ( ._g ‘ 𝑅 ) ( ( mulGrp ‘ 𝑅 ) Σ_g 𝑤 ) ) ∈ 𝐵 )
197	121 122	sseqtrid	⊢ ( 𝜑 → ( 𝐺 supp 0 ) ⊆ Word ( 𝐸 ∪ 𝐹 ) )
198	197	adantr	⊢ ( ( 𝜑 ∧ 𝑞 ∈ ( ( 𝐸 × 𝐹 ) ↑_m Word ( 𝐸 ∪ 𝐹 ) ) ) → ( 𝐺 supp 0 ) ⊆ Word ( 𝐸 ∪ 𝐹 ) )
199	1 3 161 162 188 189 196 198	gsummptres2	⊢ ( ( 𝜑 ∧ 𝑞 ∈ ( ( 𝐸 × 𝐹 ) ↑_m Word ( 𝐸 ∪ 𝐹 ) ) ) → ( 𝑅 Σ_g ( 𝑤 ∈ Word ( 𝐸 ∪ 𝐹 ) ↦ ( ( 𝐺 ‘ 𝑤 ) ( ._g ‘ 𝑅 ) ( ( mulGrp ‘ 𝑅 ) Σ_g 𝑤 ) ) ) ) = ( 𝑅 Σ_g ( 𝑤 ∈ ( 𝐺 supp 0 ) ↦ ( ( 𝐺 ‘ 𝑤 ) ( ._g ‘ 𝑅 ) ( ( mulGrp ‘ 𝑅 ) Σ_g 𝑤 ) ) ) ) )
200	7	adantr	⊢ ( ( 𝜑 ∧ 𝑞 ∈ ( ( 𝐸 × 𝐹 ) ↑_m Word ( 𝐸 ∪ 𝐹 ) ) ) → 𝐹 ∈ ( SubRing ‘ 𝑅 ) )
201	25	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝑞 ∈ ( ( 𝐸 × 𝐹 ) ↑_m Word ( 𝐸 ∪ 𝐹 ) ) ) ∧ 𝑤 ∈ ( 𝐺 supp 0 ) ) → 𝑅 ∈ Grp )
202	9	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝑞 ∈ ( ( 𝐸 × 𝐹 ) ↑_m Word ( 𝐸 ∪ 𝐹 ) ) ) ∧ 𝑤 ∈ ( 𝐺 supp 0 ) ) → 𝐺 : Word ( 𝐸 ∪ 𝐹 ) ⟶ ℤ )
203	198	sselda	⊢ ( ( ( 𝜑 ∧ 𝑞 ∈ ( ( 𝐸 × 𝐹 ) ↑_m Word ( 𝐸 ∪ 𝐹 ) ) ) ∧ 𝑤 ∈ ( 𝐺 supp 0 ) ) → 𝑤 ∈ Word ( 𝐸 ∪ 𝐹 ) )
204	202 203	ffvelcdmd	⊢ ( ( ( 𝜑 ∧ 𝑞 ∈ ( ( 𝐸 × 𝐹 ) ↑_m Word ( 𝐸 ∪ 𝐹 ) ) ) ∧ 𝑤 ∈ ( 𝐺 supp 0 ) ) → ( 𝐺 ‘ 𝑤 ) ∈ ℤ )
205	172	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝑞 ∈ ( ( 𝐸 × 𝐹 ) ↑_m Word ( 𝐸 ∪ 𝐹 ) ) ) ∧ 𝑤 ∈ ( 𝐺 supp 0 ) ) → ( mulGrp ‘ 𝑅 ) ∈ Mnd )
206	198 179	sstrd	⊢ ( ( 𝜑 ∧ 𝑞 ∈ ( ( 𝐸 × 𝐹 ) ↑_m Word ( 𝐸 ∪ 𝐹 ) ) ) → ( 𝐺 supp 0 ) ⊆ Word 𝐵 )
207	206	sselda	⊢ ( ( ( 𝜑 ∧ 𝑞 ∈ ( ( 𝐸 × 𝐹 ) ↑_m Word ( 𝐸 ∪ 𝐹 ) ) ) ∧ 𝑤 ∈ ( 𝐺 supp 0 ) ) → 𝑤 ∈ Word 𝐵 )
208	205 207 184	syl2anc	⊢ ( ( ( 𝜑 ∧ 𝑞 ∈ ( ( 𝐸 × 𝐹 ) ↑_m Word ( 𝐸 ∪ 𝐹 ) ) ) ∧ 𝑤 ∈ ( 𝐺 supp 0 ) ) → ( ( mulGrp ‘ 𝑅 ) Σ_g 𝑤 ) ∈ 𝐵 )
209	1 24 201 204 208	mulgcld	⊢ ( ( ( 𝜑 ∧ 𝑞 ∈ ( ( 𝐸 × 𝐹 ) ↑_m Word ( 𝐸 ∪ 𝐹 ) ) ) ∧ 𝑤 ∈ ( 𝐺 supp 0 ) ) → ( ( 𝐺 ‘ 𝑤 ) ( ._g ‘ 𝑅 ) ( ( mulGrp ‘ 𝑅 ) Σ_g 𝑤 ) ) ∈ 𝐵 )
210	32	adantr	⊢ ( ( ( 𝜑 ∧ 𝑞 ∈ ( ( 𝐸 × 𝐹 ) ↑_m Word ( 𝐸 ∪ 𝐹 ) ) ) ∧ 𝑤 ∈ ( 𝐺 supp 0 ) ) → 𝑞 : Word ( 𝐸 ∪ 𝐹 ) ⟶ ( 𝐸 × 𝐹 ) )
211	210 203	ffvelcdmd	⊢ ( ( ( 𝜑 ∧ 𝑞 ∈ ( ( 𝐸 × 𝐹 ) ↑_m Word ( 𝐸 ∪ 𝐹 ) ) ) ∧ 𝑤 ∈ ( 𝐺 supp 0 ) ) → ( 𝑞 ‘ 𝑤 ) ∈ ( 𝐸 × 𝐹 ) )
212		xp2nd	⊢ ( ( 𝑞 ‘ 𝑤 ) ∈ ( 𝐸 × 𝐹 ) → ( 2^nd ‘ ( 𝑞 ‘ 𝑤 ) ) ∈ 𝐹 )
213	211 212	syl	⊢ ( ( ( 𝜑 ∧ 𝑞 ∈ ( ( 𝐸 × 𝐹 ) ↑_m Word ( 𝐸 ∪ 𝐹 ) ) ) ∧ 𝑤 ∈ ( 𝐺 supp 0 ) ) → ( 2^nd ‘ ( 𝑞 ‘ 𝑤 ) ) ∈ 𝐹 )
214		2fveq3	⊢ ( 𝑣 = 𝑤 → ( 2^nd ‘ ( 𝑞 ‘ 𝑣 ) ) = ( 2^nd ‘ ( 𝑞 ‘ 𝑤 ) ) )
215	214	cbvmptv	⊢ ( 𝑣 ∈ ( 𝐺 supp 0 ) ↦ ( 2^nd ‘ ( 𝑞 ‘ 𝑣 ) ) ) = ( 𝑤 ∈ ( 𝐺 supp 0 ) ↦ ( 2^nd ‘ ( 𝑞 ‘ 𝑤 ) ) )
216	1 3 161 189 200 209 213 215	gsummpt2co	⊢ ( ( 𝜑 ∧ 𝑞 ∈ ( ( 𝐸 × 𝐹 ) ↑_m Word ( 𝐸 ∪ 𝐹 ) ) ) → ( 𝑅 Σ_g ( 𝑤 ∈ ( 𝐺 supp 0 ) ↦ ( ( 𝐺 ‘ 𝑤 ) ( ._g ‘ 𝑅 ) ( ( mulGrp ‘ 𝑅 ) Σ_g 𝑤 ) ) ) ) = ( 𝑅 Σ_g ( 𝑓 ∈ 𝐹 ↦ ( 𝑅 Σ_g ( 𝑤 ∈ ( ^◡ ( 𝑣 ∈ ( 𝐺 supp 0 ) ↦ ( 2^nd ‘ ( 𝑞 ‘ 𝑣 ) ) ) “ { 𝑓 } ) ↦ ( ( 𝐺 ‘ 𝑤 ) ( ._g ‘ 𝑅 ) ( ( mulGrp ‘ 𝑅 ) Σ_g 𝑤 ) ) ) ) ) ) )
217	199 216	eqtrd	⊢ ( ( 𝜑 ∧ 𝑞 ∈ ( ( 𝐸 × 𝐹 ) ↑_m Word ( 𝐸 ∪ 𝐹 ) ) ) → ( 𝑅 Σ_g ( 𝑤 ∈ Word ( 𝐸 ∪ 𝐹 ) ↦ ( ( 𝐺 ‘ 𝑤 ) ( ._g ‘ 𝑅 ) ( ( mulGrp ‘ 𝑅 ) Σ_g 𝑤 ) ) ) ) = ( 𝑅 Σ_g ( 𝑓 ∈ 𝐹 ↦ ( 𝑅 Σ_g ( 𝑤 ∈ ( ^◡ ( 𝑣 ∈ ( 𝐺 supp 0 ) ↦ ( 2^nd ‘ ( 𝑞 ‘ 𝑣 ) ) ) “ { 𝑓 } ) ↦ ( ( 𝐺 ‘ 𝑤 ) ( ._g ‘ 𝑅 ) ( ( mulGrp ‘ 𝑅 ) Σ_g 𝑤 ) ) ) ) ) ) )
218	217	adantr	⊢ ( ( ( 𝜑 ∧ 𝑞 ∈ ( ( 𝐸 × 𝐹 ) ↑_m Word ( 𝐸 ∪ 𝐹 ) ) ) ∧ ∀ 𝑤 ∈ Word ( 𝐸 ∪ 𝐹 ) ( ( mulGrp ‘ 𝑅 ) Σ_g 𝑤 ) = ( ( 1^st ‘ ( 𝑞 ‘ 𝑤 ) ) · ( 2^nd ‘ ( 𝑞 ‘ 𝑤 ) ) ) ) → ( 𝑅 Σ_g ( 𝑤 ∈ Word ( 𝐸 ∪ 𝐹 ) ↦ ( ( 𝐺 ‘ 𝑤 ) ( ._g ‘ 𝑅 ) ( ( mulGrp ‘ 𝑅 ) Σ_g 𝑤 ) ) ) ) = ( 𝑅 Σ_g ( 𝑓 ∈ 𝐹 ↦ ( 𝑅 Σ_g ( 𝑤 ∈ ( ^◡ ( 𝑣 ∈ ( 𝐺 supp 0 ) ↦ ( 2^nd ‘ ( 𝑞 ‘ 𝑣 ) ) ) “ { 𝑓 } ) ↦ ( ( 𝐺 ‘ 𝑤 ) ( ._g ‘ 𝑅 ) ( ( mulGrp ‘ 𝑅 ) Σ_g 𝑤 ) ) ) ) ) ) )
219	11	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝑞 ∈ ( ( 𝐸 × 𝐹 ) ↑_m Word ( 𝐸 ∪ 𝐹 ) ) ) ∧ ∀ 𝑤 ∈ Word ( 𝐸 ∪ 𝐹 ) ( ( mulGrp ‘ 𝑅 ) Σ_g 𝑤 ) = ( ( 1^st ‘ ( 𝑞 ‘ 𝑤 ) ) · ( 2^nd ‘ ( 𝑞 ‘ 𝑤 ) ) ) ) → 𝑋 = ( 𝑅 Σ_g ( 𝑤 ∈ Word ( 𝐸 ∪ 𝐹 ) ↦ ( ( 𝐺 ‘ 𝑤 ) ( ._g ‘ 𝑅 ) ( ( mulGrp ‘ 𝑅 ) Σ_g 𝑤 ) ) ) ) )
220	14	ad4antr	⊢ ( ( ( ( ( 𝜑 ∧ 𝑞 ∈ ( ( 𝐸 × 𝐹 ) ↑_m Word ( 𝐸 ∪ 𝐹 ) ) ) ∧ ∀ 𝑤 ∈ Word ( 𝐸 ∪ 𝐹 ) ( ( mulGrp ‘ 𝑅 ) Σ_g 𝑤 ) = ( ( 1^st ‘ ( 𝑞 ‘ 𝑤 ) ) · ( 2^nd ‘ ( 𝑞 ‘ 𝑤 ) ) ) ) ∧ 𝑓 ∈ 𝐹 ) ∧ 𝑣 ∈ ( ^◡ 𝑞 “ ( 𝐸 × { 𝑓 } ) ) ) → 𝑅 ∈ Ring )
221	55	ad3antrrr	⊢ ( ( ( ( 𝜑 ∧ 𝑞 ∈ ( ( 𝐸 × 𝐹 ) ↑_m Word ( 𝐸 ∪ 𝐹 ) ) ) ∧ 𝑓 ∈ 𝐹 ) ∧ 𝑣 ∈ ( ^◡ 𝑞 “ ( 𝐸 × { 𝑓 } ) ) ) → 𝐸 ⊆ 𝐵 )
222	32	ad2antrr	⊢ ( ( ( ( 𝜑 ∧ 𝑞 ∈ ( ( 𝐸 × 𝐹 ) ↑_m Word ( 𝐸 ∪ 𝐹 ) ) ) ∧ 𝑓 ∈ 𝐹 ) ∧ 𝑣 ∈ ( ^◡ 𝑞 “ ( 𝐸 × { 𝑓 } ) ) ) → 𝑞 : Word ( 𝐸 ∪ 𝐹 ) ⟶ ( 𝐸 × 𝐹 ) )
223	139	adantr	⊢ ( ( ( 𝜑 ∧ 𝑞 ∈ ( ( 𝐸 × 𝐹 ) ↑_m Word ( 𝐸 ∪ 𝐹 ) ) ) ∧ 𝑓 ∈ 𝐹 ) → ( ^◡ 𝑞 “ ( 𝐸 × { 𝑓 } ) ) ⊆ Word ( 𝐸 ∪ 𝐹 ) )
224	223	sselda	⊢ ( ( ( ( 𝜑 ∧ 𝑞 ∈ ( ( 𝐸 × 𝐹 ) ↑_m Word ( 𝐸 ∪ 𝐹 ) ) ) ∧ 𝑓 ∈ 𝐹 ) ∧ 𝑣 ∈ ( ^◡ 𝑞 “ ( 𝐸 × { 𝑓 } ) ) ) → 𝑣 ∈ Word ( 𝐸 ∪ 𝐹 ) )
225	222 224	ffvelcdmd	⊢ ( ( ( ( 𝜑 ∧ 𝑞 ∈ ( ( 𝐸 × 𝐹 ) ↑_m Word ( 𝐸 ∪ 𝐹 ) ) ) ∧ 𝑓 ∈ 𝐹 ) ∧ 𝑣 ∈ ( ^◡ 𝑞 “ ( 𝐸 × { 𝑓 } ) ) ) → ( 𝑞 ‘ 𝑣 ) ∈ ( 𝐸 × 𝐹 ) )
226	225 143	syl	⊢ ( ( ( ( 𝜑 ∧ 𝑞 ∈ ( ( 𝐸 × 𝐹 ) ↑_m Word ( 𝐸 ∪ 𝐹 ) ) ) ∧ 𝑓 ∈ 𝐹 ) ∧ 𝑣 ∈ ( ^◡ 𝑞 “ ( 𝐸 × { 𝑓 } ) ) ) → ( 1^st ‘ ( 𝑞 ‘ 𝑣 ) ) ∈ 𝐸 )
227	221 226	sseldd	⊢ ( ( ( ( 𝜑 ∧ 𝑞 ∈ ( ( 𝐸 × 𝐹 ) ↑_m Word ( 𝐸 ∪ 𝐹 ) ) ) ∧ 𝑓 ∈ 𝐹 ) ∧ 𝑣 ∈ ( ^◡ 𝑞 “ ( 𝐸 × { 𝑓 } ) ) ) → ( 1^st ‘ ( 𝑞 ‘ 𝑣 ) ) ∈ 𝐵 )
228	227	adantllr	⊢ ( ( ( ( ( 𝜑 ∧ 𝑞 ∈ ( ( 𝐸 × 𝐹 ) ↑_m Word ( 𝐸 ∪ 𝐹 ) ) ) ∧ ∀ 𝑤 ∈ Word ( 𝐸 ∪ 𝐹 ) ( ( mulGrp ‘ 𝑅 ) Σ_g 𝑤 ) = ( ( 1^st ‘ ( 𝑞 ‘ 𝑤 ) ) · ( 2^nd ‘ ( 𝑞 ‘ 𝑤 ) ) ) ) ∧ 𝑓 ∈ 𝐹 ) ∧ 𝑣 ∈ ( ^◡ 𝑞 “ ( 𝐸 × { 𝑓 } ) ) ) → ( 1^st ‘ ( 𝑞 ‘ 𝑣 ) ) ∈ 𝐵 )
229	200 174	syl	⊢ ( ( 𝜑 ∧ 𝑞 ∈ ( ( 𝐸 × 𝐹 ) ↑_m Word ( 𝐸 ∪ 𝐹 ) ) ) → 𝐹 ⊆ 𝐵 )
230	229	sselda	⊢ ( ( ( 𝜑 ∧ 𝑞 ∈ ( ( 𝐸 × 𝐹 ) ↑_m Word ( 𝐸 ∪ 𝐹 ) ) ) ∧ 𝑓 ∈ 𝐹 ) → 𝑓 ∈ 𝐵 )
231	230	ad4ant13	⊢ ( ( ( ( ( 𝜑 ∧ 𝑞 ∈ ( ( 𝐸 × 𝐹 ) ↑_m Word ( 𝐸 ∪ 𝐹 ) ) ) ∧ ∀ 𝑤 ∈ Word ( 𝐸 ∪ 𝐹 ) ( ( mulGrp ‘ 𝑅 ) Σ_g 𝑤 ) = ( ( 1^st ‘ ( 𝑞 ‘ 𝑤 ) ) · ( 2^nd ‘ ( 𝑞 ‘ 𝑤 ) ) ) ) ∧ 𝑓 ∈ 𝐹 ) ∧ 𝑣 ∈ ( ^◡ 𝑞 “ ( 𝐸 × { 𝑓 } ) ) ) → 𝑓 ∈ 𝐵 )
232	1 24 2	mulgass2	⊢ ( ( 𝑅 ∈ Ring ∧ ( ( 𝐺 ‘ 𝑣 ) ∈ ℤ ∧ ( 1^st ‘ ( 𝑞 ‘ 𝑣 ) ) ∈ 𝐵 ∧ 𝑓 ∈ 𝐵 ) ) → ( ( ( 𝐺 ‘ 𝑣 ) ( ._g ‘ 𝑅 ) ( 1^st ‘ ( 𝑞 ‘ 𝑣 ) ) ) · 𝑓 ) = ( ( 𝐺 ‘ 𝑣 ) ( ._g ‘ 𝑅 ) ( ( 1^st ‘ ( 𝑞 ‘ 𝑣 ) ) · 𝑓 ) ) )
233	220 46 228 231 232	syl13anc	⊢ ( ( ( ( ( 𝜑 ∧ 𝑞 ∈ ( ( 𝐸 × 𝐹 ) ↑_m Word ( 𝐸 ∪ 𝐹 ) ) ) ∧ ∀ 𝑤 ∈ Word ( 𝐸 ∪ 𝐹 ) ( ( mulGrp ‘ 𝑅 ) Σ_g 𝑤 ) = ( ( 1^st ‘ ( 𝑞 ‘ 𝑤 ) ) · ( 2^nd ‘ ( 𝑞 ‘ 𝑤 ) ) ) ) ∧ 𝑓 ∈ 𝐹 ) ∧ 𝑣 ∈ ( ^◡ 𝑞 “ ( 𝐸 × { 𝑓 } ) ) ) → ( ( ( 𝐺 ‘ 𝑣 ) ( ._g ‘ 𝑅 ) ( 1^st ‘ ( 𝑞 ‘ 𝑣 ) ) ) · 𝑓 ) = ( ( 𝐺 ‘ 𝑣 ) ( ._g ‘ 𝑅 ) ( ( 1^st ‘ ( 𝑞 ‘ 𝑣 ) ) · 𝑓 ) ) )
234		oveq2	⊢ ( 𝑤 = 𝑣 → ( ( mulGrp ‘ 𝑅 ) Σ_g 𝑤 ) = ( ( mulGrp ‘ 𝑅 ) Σ_g 𝑣 ) )
235		2fveq3	⊢ ( 𝑤 = 𝑣 → ( 1^st ‘ ( 𝑞 ‘ 𝑤 ) ) = ( 1^st ‘ ( 𝑞 ‘ 𝑣 ) ) )
236		2fveq3	⊢ ( 𝑤 = 𝑣 → ( 2^nd ‘ ( 𝑞 ‘ 𝑤 ) ) = ( 2^nd ‘ ( 𝑞 ‘ 𝑣 ) ) )
237	235 236	oveq12d	⊢ ( 𝑤 = 𝑣 → ( ( 1^st ‘ ( 𝑞 ‘ 𝑤 ) ) · ( 2^nd ‘ ( 𝑞 ‘ 𝑤 ) ) ) = ( ( 1^st ‘ ( 𝑞 ‘ 𝑣 ) ) · ( 2^nd ‘ ( 𝑞 ‘ 𝑣 ) ) ) )
238	234 237	eqeq12d	⊢ ( 𝑤 = 𝑣 → ( ( ( mulGrp ‘ 𝑅 ) Σ_g 𝑤 ) = ( ( 1^st ‘ ( 𝑞 ‘ 𝑤 ) ) · ( 2^nd ‘ ( 𝑞 ‘ 𝑤 ) ) ) ↔ ( ( mulGrp ‘ 𝑅 ) Σ_g 𝑣 ) = ( ( 1^st ‘ ( 𝑞 ‘ 𝑣 ) ) · ( 2^nd ‘ ( 𝑞 ‘ 𝑣 ) ) ) ) )
239		simpllr	⊢ ( ( ( ( ( 𝜑 ∧ 𝑞 ∈ ( ( 𝐸 × 𝐹 ) ↑_m Word ( 𝐸 ∪ 𝐹 ) ) ) ∧ ∀ 𝑤 ∈ Word ( 𝐸 ∪ 𝐹 ) ( ( mulGrp ‘ 𝑅 ) Σ_g 𝑤 ) = ( ( 1^st ‘ ( 𝑞 ‘ 𝑤 ) ) · ( 2^nd ‘ ( 𝑞 ‘ 𝑤 ) ) ) ) ∧ 𝑓 ∈ 𝐹 ) ∧ 𝑣 ∈ ( ^◡ 𝑞 “ ( 𝐸 × { 𝑓 } ) ) ) → ∀ 𝑤 ∈ Word ( 𝐸 ∪ 𝐹 ) ( ( mulGrp ‘ 𝑅 ) Σ_g 𝑤 ) = ( ( 1^st ‘ ( 𝑞 ‘ 𝑤 ) ) · ( 2^nd ‘ ( 𝑞 ‘ 𝑤 ) ) ) )
240	238 239 45	rspcdva	⊢ ( ( ( ( ( 𝜑 ∧ 𝑞 ∈ ( ( 𝐸 × 𝐹 ) ↑_m Word ( 𝐸 ∪ 𝐹 ) ) ) ∧ ∀ 𝑤 ∈ Word ( 𝐸 ∪ 𝐹 ) ( ( mulGrp ‘ 𝑅 ) Σ_g 𝑤 ) = ( ( 1^st ‘ ( 𝑞 ‘ 𝑤 ) ) · ( 2^nd ‘ ( 𝑞 ‘ 𝑤 ) ) ) ) ∧ 𝑓 ∈ 𝐹 ) ∧ 𝑣 ∈ ( ^◡ 𝑞 “ ( 𝐸 × { 𝑓 } ) ) ) → ( ( mulGrp ‘ 𝑅 ) Σ_g 𝑣 ) = ( ( 1^st ‘ ( 𝑞 ‘ 𝑣 ) ) · ( 2^nd ‘ ( 𝑞 ‘ 𝑣 ) ) ) )
241	32	ffnd	⊢ ( ( 𝜑 ∧ 𝑞 ∈ ( ( 𝐸 × 𝐹 ) ↑_m Word ( 𝐸 ∪ 𝐹 ) ) ) → 𝑞 Fn Word ( 𝐸 ∪ 𝐹 ) )
242	241	ad2antrr	⊢ ( ( ( ( 𝜑 ∧ 𝑞 ∈ ( ( 𝐸 × 𝐹 ) ↑_m Word ( 𝐸 ∪ 𝐹 ) ) ) ∧ 𝑓 ∈ 𝐹 ) ∧ 𝑣 ∈ ( ^◡ 𝑞 “ ( 𝐸 × { 𝑓 } ) ) ) → 𝑞 Fn Word ( 𝐸 ∪ 𝐹 ) )
243		elpreima	⊢ ( 𝑞 Fn Word ( 𝐸 ∪ 𝐹 ) → ( 𝑣 ∈ ( ^◡ 𝑞 “ ( 𝐸 × { 𝑓 } ) ) ↔ ( 𝑣 ∈ Word ( 𝐸 ∪ 𝐹 ) ∧ ( 𝑞 ‘ 𝑣 ) ∈ ( 𝐸 × { 𝑓 } ) ) ) )
244	243	simplbda	⊢ ( ( 𝑞 Fn Word ( 𝐸 ∪ 𝐹 ) ∧ 𝑣 ∈ ( ^◡ 𝑞 “ ( 𝐸 × { 𝑓 } ) ) ) → ( 𝑞 ‘ 𝑣 ) ∈ ( 𝐸 × { 𝑓 } ) )
245	242 244	sylancom	⊢ ( ( ( ( 𝜑 ∧ 𝑞 ∈ ( ( 𝐸 × 𝐹 ) ↑_m Word ( 𝐸 ∪ 𝐹 ) ) ) ∧ 𝑓 ∈ 𝐹 ) ∧ 𝑣 ∈ ( ^◡ 𝑞 “ ( 𝐸 × { 𝑓 } ) ) ) → ( 𝑞 ‘ 𝑣 ) ∈ ( 𝐸 × { 𝑓 } ) )
246		xp2nd	⊢ ( ( 𝑞 ‘ 𝑣 ) ∈ ( 𝐸 × { 𝑓 } ) → ( 2^nd ‘ ( 𝑞 ‘ 𝑣 ) ) ∈ { 𝑓 } )
247	245 246	syl	⊢ ( ( ( ( 𝜑 ∧ 𝑞 ∈ ( ( 𝐸 × 𝐹 ) ↑_m Word ( 𝐸 ∪ 𝐹 ) ) ) ∧ 𝑓 ∈ 𝐹 ) ∧ 𝑣 ∈ ( ^◡ 𝑞 “ ( 𝐸 × { 𝑓 } ) ) ) → ( 2^nd ‘ ( 𝑞 ‘ 𝑣 ) ) ∈ { 𝑓 } )
248	247	elsnd	⊢ ( ( ( ( 𝜑 ∧ 𝑞 ∈ ( ( 𝐸 × 𝐹 ) ↑_m Word ( 𝐸 ∪ 𝐹 ) ) ) ∧ 𝑓 ∈ 𝐹 ) ∧ 𝑣 ∈ ( ^◡ 𝑞 “ ( 𝐸 × { 𝑓 } ) ) ) → ( 2^nd ‘ ( 𝑞 ‘ 𝑣 ) ) = 𝑓 )
249	248	adantllr	⊢ ( ( ( ( ( 𝜑 ∧ 𝑞 ∈ ( ( 𝐸 × 𝐹 ) ↑_m Word ( 𝐸 ∪ 𝐹 ) ) ) ∧ ∀ 𝑤 ∈ Word ( 𝐸 ∪ 𝐹 ) ( ( mulGrp ‘ 𝑅 ) Σ_g 𝑤 ) = ( ( 1^st ‘ ( 𝑞 ‘ 𝑤 ) ) · ( 2^nd ‘ ( 𝑞 ‘ 𝑤 ) ) ) ) ∧ 𝑓 ∈ 𝐹 ) ∧ 𝑣 ∈ ( ^◡ 𝑞 “ ( 𝐸 × { 𝑓 } ) ) ) → ( 2^nd ‘ ( 𝑞 ‘ 𝑣 ) ) = 𝑓 )
250	249	oveq2d	⊢ ( ( ( ( ( 𝜑 ∧ 𝑞 ∈ ( ( 𝐸 × 𝐹 ) ↑_m Word ( 𝐸 ∪ 𝐹 ) ) ) ∧ ∀ 𝑤 ∈ Word ( 𝐸 ∪ 𝐹 ) ( ( mulGrp ‘ 𝑅 ) Σ_g 𝑤 ) = ( ( 1^st ‘ ( 𝑞 ‘ 𝑤 ) ) · ( 2^nd ‘ ( 𝑞 ‘ 𝑤 ) ) ) ) ∧ 𝑓 ∈ 𝐹 ) ∧ 𝑣 ∈ ( ^◡ 𝑞 “ ( 𝐸 × { 𝑓 } ) ) ) → ( ( 1^st ‘ ( 𝑞 ‘ 𝑣 ) ) · ( 2^nd ‘ ( 𝑞 ‘ 𝑣 ) ) ) = ( ( 1^st ‘ ( 𝑞 ‘ 𝑣 ) ) · 𝑓 ) )
251	240 250	eqtrd	⊢ ( ( ( ( ( 𝜑 ∧ 𝑞 ∈ ( ( 𝐸 × 𝐹 ) ↑_m Word ( 𝐸 ∪ 𝐹 ) ) ) ∧ ∀ 𝑤 ∈ Word ( 𝐸 ∪ 𝐹 ) ( ( mulGrp ‘ 𝑅 ) Σ_g 𝑤 ) = ( ( 1^st ‘ ( 𝑞 ‘ 𝑤 ) ) · ( 2^nd ‘ ( 𝑞 ‘ 𝑤 ) ) ) ) ∧ 𝑓 ∈ 𝐹 ) ∧ 𝑣 ∈ ( ^◡ 𝑞 “ ( 𝐸 × { 𝑓 } ) ) ) → ( ( mulGrp ‘ 𝑅 ) Σ_g 𝑣 ) = ( ( 1^st ‘ ( 𝑞 ‘ 𝑣 ) ) · 𝑓 ) )
252	251	oveq2d	⊢ ( ( ( ( ( 𝜑 ∧ 𝑞 ∈ ( ( 𝐸 × 𝐹 ) ↑_m Word ( 𝐸 ∪ 𝐹 ) ) ) ∧ ∀ 𝑤 ∈ Word ( 𝐸 ∪ 𝐹 ) ( ( mulGrp ‘ 𝑅 ) Σ_g 𝑤 ) = ( ( 1^st ‘ ( 𝑞 ‘ 𝑤 ) ) · ( 2^nd ‘ ( 𝑞 ‘ 𝑤 ) ) ) ) ∧ 𝑓 ∈ 𝐹 ) ∧ 𝑣 ∈ ( ^◡ 𝑞 “ ( 𝐸 × { 𝑓 } ) ) ) → ( ( 𝐺 ‘ 𝑣 ) ( ._g ‘ 𝑅 ) ( ( mulGrp ‘ 𝑅 ) Σ_g 𝑣 ) ) = ( ( 𝐺 ‘ 𝑣 ) ( ._g ‘ 𝑅 ) ( ( 1^st ‘ ( 𝑞 ‘ 𝑣 ) ) · 𝑓 ) ) )
253	233 252	eqtr4d	⊢ ( ( ( ( ( 𝜑 ∧ 𝑞 ∈ ( ( 𝐸 × 𝐹 ) ↑_m Word ( 𝐸 ∪ 𝐹 ) ) ) ∧ ∀ 𝑤 ∈ Word ( 𝐸 ∪ 𝐹 ) ( ( mulGrp ‘ 𝑅 ) Σ_g 𝑤 ) = ( ( 1^st ‘ ( 𝑞 ‘ 𝑤 ) ) · ( 2^nd ‘ ( 𝑞 ‘ 𝑤 ) ) ) ) ∧ 𝑓 ∈ 𝐹 ) ∧ 𝑣 ∈ ( ^◡ 𝑞 “ ( 𝐸 × { 𝑓 } ) ) ) → ( ( ( 𝐺 ‘ 𝑣 ) ( ._g ‘ 𝑅 ) ( 1^st ‘ ( 𝑞 ‘ 𝑣 ) ) ) · 𝑓 ) = ( ( 𝐺 ‘ 𝑣 ) ( ._g ‘ 𝑅 ) ( ( mulGrp ‘ 𝑅 ) Σ_g 𝑣 ) ) )
254	253	mpteq2dva	⊢ ( ( ( ( 𝜑 ∧ 𝑞 ∈ ( ( 𝐸 × 𝐹 ) ↑_m Word ( 𝐸 ∪ 𝐹 ) ) ) ∧ ∀ 𝑤 ∈ Word ( 𝐸 ∪ 𝐹 ) ( ( mulGrp ‘ 𝑅 ) Σ_g 𝑤 ) = ( ( 1^st ‘ ( 𝑞 ‘ 𝑤 ) ) · ( 2^nd ‘ ( 𝑞 ‘ 𝑤 ) ) ) ) ∧ 𝑓 ∈ 𝐹 ) → ( 𝑣 ∈ ( ^◡ 𝑞 “ ( 𝐸 × { 𝑓 } ) ) ↦ ( ( ( 𝐺 ‘ 𝑣 ) ( ._g ‘ 𝑅 ) ( 1^st ‘ ( 𝑞 ‘ 𝑣 ) ) ) · 𝑓 ) ) = ( 𝑣 ∈ ( ^◡ 𝑞 “ ( 𝐸 × { 𝑓 } ) ) ↦ ( ( 𝐺 ‘ 𝑣 ) ( ._g ‘ 𝑅 ) ( ( mulGrp ‘ 𝑅 ) Σ_g 𝑣 ) ) ) )
255		fveq2	⊢ ( 𝑣 = 𝑤 → ( 𝐺 ‘ 𝑣 ) = ( 𝐺 ‘ 𝑤 ) )
256		oveq2	⊢ ( 𝑣 = 𝑤 → ( ( mulGrp ‘ 𝑅 ) Σ_g 𝑣 ) = ( ( mulGrp ‘ 𝑅 ) Σ_g 𝑤 ) )
257	255 256	oveq12d	⊢ ( 𝑣 = 𝑤 → ( ( 𝐺 ‘ 𝑣 ) ( ._g ‘ 𝑅 ) ( ( mulGrp ‘ 𝑅 ) Σ_g 𝑣 ) ) = ( ( 𝐺 ‘ 𝑤 ) ( ._g ‘ 𝑅 ) ( ( mulGrp ‘ 𝑅 ) Σ_g 𝑤 ) ) )
258	257	cbvmptv	⊢ ( 𝑣 ∈ ( ^◡ 𝑞 “ ( 𝐸 × { 𝑓 } ) ) ↦ ( ( 𝐺 ‘ 𝑣 ) ( ._g ‘ 𝑅 ) ( ( mulGrp ‘ 𝑅 ) Σ_g 𝑣 ) ) ) = ( 𝑤 ∈ ( ^◡ 𝑞 “ ( 𝐸 × { 𝑓 } ) ) ↦ ( ( 𝐺 ‘ 𝑤 ) ( ._g ‘ 𝑅 ) ( ( mulGrp ‘ 𝑅 ) Σ_g 𝑤 ) ) )
259	254 258	eqtrdi	⊢ ( ( ( ( 𝜑 ∧ 𝑞 ∈ ( ( 𝐸 × 𝐹 ) ↑_m Word ( 𝐸 ∪ 𝐹 ) ) ) ∧ ∀ 𝑤 ∈ Word ( 𝐸 ∪ 𝐹 ) ( ( mulGrp ‘ 𝑅 ) Σ_g 𝑤 ) = ( ( 1^st ‘ ( 𝑞 ‘ 𝑤 ) ) · ( 2^nd ‘ ( 𝑞 ‘ 𝑤 ) ) ) ) ∧ 𝑓 ∈ 𝐹 ) → ( 𝑣 ∈ ( ^◡ 𝑞 “ ( 𝐸 × { 𝑓 } ) ) ↦ ( ( ( 𝐺 ‘ 𝑣 ) ( ._g ‘ 𝑅 ) ( 1^st ‘ ( 𝑞 ‘ 𝑣 ) ) ) · 𝑓 ) ) = ( 𝑤 ∈ ( ^◡ 𝑞 “ ( 𝐸 × { 𝑓 } ) ) ↦ ( ( 𝐺 ‘ 𝑤 ) ( ._g ‘ 𝑅 ) ( ( mulGrp ‘ 𝑅 ) Σ_g 𝑤 ) ) ) )
260	259	oveq2d	⊢ ( ( ( ( 𝜑 ∧ 𝑞 ∈ ( ( 𝐸 × 𝐹 ) ↑_m Word ( 𝐸 ∪ 𝐹 ) ) ) ∧ ∀ 𝑤 ∈ Word ( 𝐸 ∪ 𝐹 ) ( ( mulGrp ‘ 𝑅 ) Σ_g 𝑤 ) = ( ( 1^st ‘ ( 𝑞 ‘ 𝑤 ) ) · ( 2^nd ‘ ( 𝑞 ‘ 𝑤 ) ) ) ) ∧ 𝑓 ∈ 𝐹 ) → ( 𝑅 Σ_g ( 𝑣 ∈ ( ^◡ 𝑞 “ ( 𝐸 × { 𝑓 } ) ) ↦ ( ( ( 𝐺 ‘ 𝑣 ) ( ._g ‘ 𝑅 ) ( 1^st ‘ ( 𝑞 ‘ 𝑣 ) ) ) · 𝑓 ) ) ) = ( 𝑅 Σ_g ( 𝑤 ∈ ( ^◡ 𝑞 “ ( 𝐸 × { 𝑓 } ) ) ↦ ( ( 𝐺 ‘ 𝑤 ) ( ._g ‘ 𝑅 ) ( ( mulGrp ‘ 𝑅 ) Σ_g 𝑤 ) ) ) ) )
261	14	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝑞 ∈ ( ( 𝐸 × 𝐹 ) ↑_m Word ( 𝐸 ∪ 𝐹 ) ) ) ∧ 𝑓 ∈ 𝐹 ) → 𝑅 ∈ Ring )
262	19	a1i	⊢ ( ( ( 𝜑 ∧ 𝑞 ∈ ( ( 𝐸 × 𝐹 ) ↑_m Word ( 𝐸 ∪ 𝐹 ) ) ) ∧ 𝑓 ∈ 𝐹 ) → ( ^◡ 𝑞 “ ( 𝐸 × { 𝑓 } ) ) ∈ V )
263	25	ad3antrrr	⊢ ( ( ( ( 𝜑 ∧ 𝑞 ∈ ( ( 𝐸 × 𝐹 ) ↑_m Word ( 𝐸 ∪ 𝐹 ) ) ) ∧ 𝑓 ∈ 𝐹 ) ∧ 𝑣 ∈ ( ^◡ 𝑞 “ ( 𝐸 × { 𝑓 } ) ) ) → 𝑅 ∈ Grp )
264	191	ad2antrr	⊢ ( ( ( ( 𝜑 ∧ 𝑞 ∈ ( ( 𝐸 × 𝐹 ) ↑_m Word ( 𝐸 ∪ 𝐹 ) ) ) ∧ 𝑓 ∈ 𝐹 ) ∧ 𝑣 ∈ ( ^◡ 𝑞 “ ( 𝐸 × { 𝑓 } ) ) ) → 𝐺 : Word ( 𝐸 ∪ 𝐹 ) ⟶ ℤ )
265	264 224	ffvelcdmd	⊢ ( ( ( ( 𝜑 ∧ 𝑞 ∈ ( ( 𝐸 × 𝐹 ) ↑_m Word ( 𝐸 ∪ 𝐹 ) ) ) ∧ 𝑓 ∈ 𝐹 ) ∧ 𝑣 ∈ ( ^◡ 𝑞 “ ( 𝐸 × { 𝑓 } ) ) ) → ( 𝐺 ‘ 𝑣 ) ∈ ℤ )
266	1 24 263 265 227	mulgcld	⊢ ( ( ( ( 𝜑 ∧ 𝑞 ∈ ( ( 𝐸 × 𝐹 ) ↑_m Word ( 𝐸 ∪ 𝐹 ) ) ) ∧ 𝑓 ∈ 𝐹 ) ∧ 𝑣 ∈ ( ^◡ 𝑞 “ ( 𝐸 × { 𝑓 } ) ) ) → ( ( 𝐺 ‘ 𝑣 ) ( ._g ‘ 𝑅 ) ( 1^st ‘ ( 𝑞 ‘ 𝑣 ) ) ) ∈ 𝐵 )
267	50	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝑞 ∈ ( ( 𝐸 × 𝐹 ) ↑_m Word ( 𝐸 ∪ 𝐹 ) ) ) ∧ 𝑓 ∈ 𝐹 ) → ( 𝑣 ∈ Word ( 𝐸 ∪ 𝐹 ) ↦ ( 𝐺 ‘ 𝑣 ) ) finSupp 0 )
268		0zd	⊢ ( ( ( 𝜑 ∧ 𝑞 ∈ ( ( 𝐸 × 𝐹 ) ↑_m Word ( 𝐸 ∪ 𝐹 ) ) ) ∧ 𝑓 ∈ 𝐹 ) → 0 ∈ ℤ )
269	267 223 268	fmptssfisupp	⊢ ( ( ( 𝜑 ∧ 𝑞 ∈ ( ( 𝐸 × 𝐹 ) ↑_m Word ( 𝐸 ∪ 𝐹 ) ) ) ∧ 𝑓 ∈ 𝐹 ) → ( 𝑣 ∈ ( ^◡ 𝑞 “ ( 𝐸 × { 𝑓 } ) ) ↦ ( 𝐺 ‘ 𝑣 ) ) finSupp 0 )
270	58	adantl	⊢ ( ( ( ( 𝜑 ∧ 𝑞 ∈ ( ( 𝐸 × 𝐹 ) ↑_m Word ( 𝐸 ∪ 𝐹 ) ) ) ∧ 𝑓 ∈ 𝐹 ) ∧ 𝑦 ∈ 𝐵 ) → ( 0 ( ._g ‘ 𝑅 ) 𝑦 ) = 0 )
271	60	a1i	⊢ ( ( ( 𝜑 ∧ 𝑞 ∈ ( ( 𝐸 × 𝐹 ) ↑_m Word ( 𝐸 ∪ 𝐹 ) ) ) ∧ 𝑓 ∈ 𝐹 ) → 0 ∈ V )
272	269 270 265 227 271	fsuppssov1	⊢ ( ( ( 𝜑 ∧ 𝑞 ∈ ( ( 𝐸 × 𝐹 ) ↑_m Word ( 𝐸 ∪ 𝐹 ) ) ) ∧ 𝑓 ∈ 𝐹 ) → ( 𝑣 ∈ ( ^◡ 𝑞 “ ( 𝐸 × { 𝑓 } ) ) ↦ ( ( 𝐺 ‘ 𝑣 ) ( ._g ‘ 𝑅 ) ( 1^st ‘ ( 𝑞 ‘ 𝑣 ) ) ) ) finSupp 0 )
273	1 3 2 261 262 230 266 272	gsummulc1	⊢ ( ( ( 𝜑 ∧ 𝑞 ∈ ( ( 𝐸 × 𝐹 ) ↑_m Word ( 𝐸 ∪ 𝐹 ) ) ) ∧ 𝑓 ∈ 𝐹 ) → ( 𝑅 Σ_g ( 𝑣 ∈ ( ^◡ 𝑞 “ ( 𝐸 × { 𝑓 } ) ) ↦ ( ( ( 𝐺 ‘ 𝑣 ) ( ._g ‘ 𝑅 ) ( 1^st ‘ ( 𝑞 ‘ 𝑣 ) ) ) · 𝑓 ) ) ) = ( ( 𝑅 Σ_g ( 𝑣 ∈ ( ^◡ 𝑞 “ ( 𝐸 × { 𝑓 } ) ) ↦ ( ( 𝐺 ‘ 𝑣 ) ( ._g ‘ 𝑅 ) ( 1^st ‘ ( 𝑞 ‘ 𝑣 ) ) ) ) ) · 𝑓 ) )
274	273	adantlr	⊢ ( ( ( ( 𝜑 ∧ 𝑞 ∈ ( ( 𝐸 × 𝐹 ) ↑_m Word ( 𝐸 ∪ 𝐹 ) ) ) ∧ ∀ 𝑤 ∈ Word ( 𝐸 ∪ 𝐹 ) ( ( mulGrp ‘ 𝑅 ) Σ_g 𝑤 ) = ( ( 1^st ‘ ( 𝑞 ‘ 𝑤 ) ) · ( 2^nd ‘ ( 𝑞 ‘ 𝑤 ) ) ) ) ∧ 𝑓 ∈ 𝐹 ) → ( 𝑅 Σ_g ( 𝑣 ∈ ( ^◡ 𝑞 “ ( 𝐸 × { 𝑓 } ) ) ↦ ( ( ( 𝐺 ‘ 𝑣 ) ( ._g ‘ 𝑅 ) ( 1^st ‘ ( 𝑞 ‘ 𝑣 ) ) ) · 𝑓 ) ) ) = ( ( 𝑅 Σ_g ( 𝑣 ∈ ( ^◡ 𝑞 “ ( 𝐸 × { 𝑓 } ) ) ↦ ( ( 𝐺 ‘ 𝑣 ) ( ._g ‘ 𝑅 ) ( 1^st ‘ ( 𝑞 ‘ 𝑣 ) ) ) ) ) · 𝑓 ) )
275	161	adantr	⊢ ( ( ( 𝜑 ∧ 𝑞 ∈ ( ( 𝐸 × 𝐹 ) ↑_m Word ( 𝐸 ∪ 𝐹 ) ) ) ∧ 𝑓 ∈ 𝐹 ) → 𝑅 ∈ CMnd )
276	89	ad3antrrr	⊢ ( ( ( ( 𝜑 ∧ 𝑞 ∈ ( ( 𝐸 × 𝐹 ) ↑_m Word ( 𝐸 ∪ 𝐹 ) ) ) ∧ 𝑓 ∈ 𝐹 ) ∧ 𝑣 ∈ ( ( ^◡ 𝑞 “ ( 𝐸 × { 𝑓 } ) ) ∖ ( ^◡ ( 𝑢 ∈ ( 𝐺 supp 0 ) ↦ ( 2^nd ‘ ( 𝑞 ‘ 𝑢 ) ) ) “ { 𝑓 } ) ) ) → 𝐺 Fn Word ( 𝐸 ∪ 𝐹 ) )
277	162	ad2antrr	⊢ ( ( ( ( 𝜑 ∧ 𝑞 ∈ ( ( 𝐸 × 𝐹 ) ↑_m Word ( 𝐸 ∪ 𝐹 ) ) ) ∧ 𝑓 ∈ 𝐹 ) ∧ 𝑣 ∈ ( ( ^◡ 𝑞 “ ( 𝐸 × { 𝑓 } ) ) ∖ ( ^◡ ( 𝑢 ∈ ( 𝐺 supp 0 ) ↦ ( 2^nd ‘ ( 𝑞 ‘ 𝑢 ) ) ) “ { 𝑓 } ) ) ) → Word ( 𝐸 ∪ 𝐹 ) ∈ V )
278		0zd	⊢ ( ( ( ( 𝜑 ∧ 𝑞 ∈ ( ( 𝐸 × 𝐹 ) ↑_m Word ( 𝐸 ∪ 𝐹 ) ) ) ∧ 𝑓 ∈ 𝐹 ) ∧ 𝑣 ∈ ( ( ^◡ 𝑞 “ ( 𝐸 × { 𝑓 } ) ) ∖ ( ^◡ ( 𝑢 ∈ ( 𝐺 supp 0 ) ↦ ( 2^nd ‘ ( 𝑞 ‘ 𝑢 ) ) ) “ { 𝑓 } ) ) ) → 0 ∈ ℤ )
279	139	ad2antrr	⊢ ( ( ( ( 𝜑 ∧ 𝑞 ∈ ( ( 𝐸 × 𝐹 ) ↑_m Word ( 𝐸 ∪ 𝐹 ) ) ) ∧ 𝑓 ∈ 𝐹 ) ∧ 𝑣 ∈ ( ( ^◡ 𝑞 “ ( 𝐸 × { 𝑓 } ) ) ∖ ( ^◡ ( 𝑢 ∈ ( 𝐺 supp 0 ) ↦ ( 2^nd ‘ ( 𝑞 ‘ 𝑢 ) ) ) “ { 𝑓 } ) ) ) → ( ^◡ 𝑞 “ ( 𝐸 × { 𝑓 } ) ) ⊆ Word ( 𝐸 ∪ 𝐹 ) )
280		simpr	⊢ ( ( ( ( 𝜑 ∧ 𝑞 ∈ ( ( 𝐸 × 𝐹 ) ↑_m Word ( 𝐸 ∪ 𝐹 ) ) ) ∧ 𝑓 ∈ 𝐹 ) ∧ 𝑣 ∈ ( ( ^◡ 𝑞 “ ( 𝐸 × { 𝑓 } ) ) ∖ ( ^◡ ( 𝑢 ∈ ( 𝐺 supp 0 ) ↦ ( 2^nd ‘ ( 𝑞 ‘ 𝑢 ) ) ) “ { 𝑓 } ) ) ) → 𝑣 ∈ ( ( ^◡ 𝑞 “ ( 𝐸 × { 𝑓 } ) ) ∖ ( ^◡ ( 𝑢 ∈ ( 𝐺 supp 0 ) ↦ ( 2^nd ‘ ( 𝑞 ‘ 𝑢 ) ) ) “ { 𝑓 } ) ) )
281	280	eldifad	⊢ ( ( ( ( 𝜑 ∧ 𝑞 ∈ ( ( 𝐸 × 𝐹 ) ↑_m Word ( 𝐸 ∪ 𝐹 ) ) ) ∧ 𝑓 ∈ 𝐹 ) ∧ 𝑣 ∈ ( ( ^◡ 𝑞 “ ( 𝐸 × { 𝑓 } ) ) ∖ ( ^◡ ( 𝑢 ∈ ( 𝐺 supp 0 ) ↦ ( 2^nd ‘ ( 𝑞 ‘ 𝑢 ) ) ) “ { 𝑓 } ) ) ) → 𝑣 ∈ ( ^◡ 𝑞 “ ( 𝐸 × { 𝑓 } ) ) )
282	279 281	sseldd	⊢ ( ( ( ( 𝜑 ∧ 𝑞 ∈ ( ( 𝐸 × 𝐹 ) ↑_m Word ( 𝐸 ∪ 𝐹 ) ) ) ∧ 𝑓 ∈ 𝐹 ) ∧ 𝑣 ∈ ( ( ^◡ 𝑞 “ ( 𝐸 × { 𝑓 } ) ) ∖ ( ^◡ ( 𝑢 ∈ ( 𝐺 supp 0 ) ↦ ( 2^nd ‘ ( 𝑞 ‘ 𝑢 ) ) ) “ { 𝑓 } ) ) ) → 𝑣 ∈ Word ( 𝐸 ∪ 𝐹 ) )
283		eldif	⊢ ( 𝑣 ∈ ( ( ^◡ 𝑞 “ ( 𝐸 × { 𝑓 } ) ) ∖ ( ^◡ ( 𝑢 ∈ ( 𝐺 supp 0 ) ↦ ( 2^nd ‘ ( 𝑞 ‘ 𝑢 ) ) ) “ { 𝑓 } ) ) ↔ ( 𝑣 ∈ ( ^◡ 𝑞 “ ( 𝐸 × { 𝑓 } ) ) ∧ ¬ 𝑣 ∈ ( ^◡ ( 𝑢 ∈ ( 𝐺 supp 0 ) ↦ ( 2^nd ‘ ( 𝑞 ‘ 𝑢 ) ) ) “ { 𝑓 } ) ) )
284		nfv	⊢ Ⅎ 𝑢 ( ( ( 𝜑 ∧ 𝑞 ∈ ( ( 𝐸 × 𝐹 ) ↑_m Word ( 𝐸 ∪ 𝐹 ) ) ) ∧ 𝑓 ∈ 𝐹 ) ∧ 𝑣 ∈ ( 𝐺 supp 0 ) )
285		fvexd	⊢ ( ( ( ( ( 𝜑 ∧ 𝑞 ∈ ( ( 𝐸 × 𝐹 ) ↑_m Word ( 𝐸 ∪ 𝐹 ) ) ) ∧ 𝑓 ∈ 𝐹 ) ∧ 𝑣 ∈ ( 𝐺 supp 0 ) ) ∧ 𝑢 ∈ ( 𝐺 supp 0 ) ) → ( 2^nd ‘ ( 𝑞 ‘ 𝑢 ) ) ∈ V )
286		eqid	⊢ ( 𝑢 ∈ ( 𝐺 supp 0 ) ↦ ( 2^nd ‘ ( 𝑞 ‘ 𝑢 ) ) ) = ( 𝑢 ∈ ( 𝐺 supp 0 ) ↦ ( 2^nd ‘ ( 𝑞 ‘ 𝑢 ) ) )
287	284 285 286	fnmptd	⊢ ( ( ( ( 𝜑 ∧ 𝑞 ∈ ( ( 𝐸 × 𝐹 ) ↑_m Word ( 𝐸 ∪ 𝐹 ) ) ) ∧ 𝑓 ∈ 𝐹 ) ∧ 𝑣 ∈ ( 𝐺 supp 0 ) ) → ( 𝑢 ∈ ( 𝐺 supp 0 ) ↦ ( 2^nd ‘ ( 𝑞 ‘ 𝑢 ) ) ) Fn ( 𝐺 supp 0 ) )
288	287	adantlr	⊢ ( ( ( ( ( 𝜑 ∧ 𝑞 ∈ ( ( 𝐸 × 𝐹 ) ↑_m Word ( 𝐸 ∪ 𝐹 ) ) ) ∧ 𝑓 ∈ 𝐹 ) ∧ 𝑣 ∈ ( ^◡ 𝑞 “ ( 𝐸 × { 𝑓 } ) ) ) ∧ 𝑣 ∈ ( 𝐺 supp 0 ) ) → ( 𝑢 ∈ ( 𝐺 supp 0 ) ↦ ( 2^nd ‘ ( 𝑞 ‘ 𝑢 ) ) ) Fn ( 𝐺 supp 0 ) )
289		simpr	⊢ ( ( ( ( ( 𝜑 ∧ 𝑞 ∈ ( ( 𝐸 × 𝐹 ) ↑_m Word ( 𝐸 ∪ 𝐹 ) ) ) ∧ 𝑓 ∈ 𝐹 ) ∧ 𝑣 ∈ ( ^◡ 𝑞 “ ( 𝐸 × { 𝑓 } ) ) ) ∧ 𝑣 ∈ ( 𝐺 supp 0 ) ) → 𝑣 ∈ ( 𝐺 supp 0 ) )
290		2fveq3	⊢ ( 𝑢 = 𝑣 → ( 2^nd ‘ ( 𝑞 ‘ 𝑢 ) ) = ( 2^nd ‘ ( 𝑞 ‘ 𝑣 ) ) )
291		simpr	⊢ ( ( ( ( 𝜑 ∧ 𝑞 ∈ ( ( 𝐸 × 𝐹 ) ↑_m Word ( 𝐸 ∪ 𝐹 ) ) ) ∧ 𝑓 ∈ 𝐹 ) ∧ 𝑣 ∈ ( 𝐺 supp 0 ) ) → 𝑣 ∈ ( 𝐺 supp 0 ) )
292		fvexd	⊢ ( ( ( ( 𝜑 ∧ 𝑞 ∈ ( ( 𝐸 × 𝐹 ) ↑_m Word ( 𝐸 ∪ 𝐹 ) ) ) ∧ 𝑓 ∈ 𝐹 ) ∧ 𝑣 ∈ ( 𝐺 supp 0 ) ) → ( 2^nd ‘ ( 𝑞 ‘ 𝑣 ) ) ∈ V )
293	286 290 291 292	fvmptd3	⊢ ( ( ( ( 𝜑 ∧ 𝑞 ∈ ( ( 𝐸 × 𝐹 ) ↑_m Word ( 𝐸 ∪ 𝐹 ) ) ) ∧ 𝑓 ∈ 𝐹 ) ∧ 𝑣 ∈ ( 𝐺 supp 0 ) ) → ( ( 𝑢 ∈ ( 𝐺 supp 0 ) ↦ ( 2^nd ‘ ( 𝑞 ‘ 𝑢 ) ) ) ‘ 𝑣 ) = ( 2^nd ‘ ( 𝑞 ‘ 𝑣 ) ) )
294	293	adantlr	⊢ ( ( ( ( ( 𝜑 ∧ 𝑞 ∈ ( ( 𝐸 × 𝐹 ) ↑_m Word ( 𝐸 ∪ 𝐹 ) ) ) ∧ 𝑓 ∈ 𝐹 ) ∧ 𝑣 ∈ ( ^◡ 𝑞 “ ( 𝐸 × { 𝑓 } ) ) ) ∧ 𝑣 ∈ ( 𝐺 supp 0 ) ) → ( ( 𝑢 ∈ ( 𝐺 supp 0 ) ↦ ( 2^nd ‘ ( 𝑞 ‘ 𝑢 ) ) ) ‘ 𝑣 ) = ( 2^nd ‘ ( 𝑞 ‘ 𝑣 ) ) )
295	241	ad3antrrr	⊢ ( ( ( ( ( 𝜑 ∧ 𝑞 ∈ ( ( 𝐸 × 𝐹 ) ↑_m Word ( 𝐸 ∪ 𝐹 ) ) ) ∧ 𝑓 ∈ 𝐹 ) ∧ 𝑣 ∈ ( ^◡ 𝑞 “ ( 𝐸 × { 𝑓 } ) ) ) ∧ 𝑣 ∈ ( 𝐺 supp 0 ) ) → 𝑞 Fn Word ( 𝐸 ∪ 𝐹 ) )
296		simplr	⊢ ( ( ( ( ( 𝜑 ∧ 𝑞 ∈ ( ( 𝐸 × 𝐹 ) ↑_m Word ( 𝐸 ∪ 𝐹 ) ) ) ∧ 𝑓 ∈ 𝐹 ) ∧ 𝑣 ∈ ( ^◡ 𝑞 “ ( 𝐸 × { 𝑓 } ) ) ) ∧ 𝑣 ∈ ( 𝐺 supp 0 ) ) → 𝑣 ∈ ( ^◡ 𝑞 “ ( 𝐸 × { 𝑓 } ) ) )
297	295 296 244	syl2anc	⊢ ( ( ( ( ( 𝜑 ∧ 𝑞 ∈ ( ( 𝐸 × 𝐹 ) ↑_m Word ( 𝐸 ∪ 𝐹 ) ) ) ∧ 𝑓 ∈ 𝐹 ) ∧ 𝑣 ∈ ( ^◡ 𝑞 “ ( 𝐸 × { 𝑓 } ) ) ) ∧ 𝑣 ∈ ( 𝐺 supp 0 ) ) → ( 𝑞 ‘ 𝑣 ) ∈ ( 𝐸 × { 𝑓 } ) )
298	297 246	syl	⊢ ( ( ( ( ( 𝜑 ∧ 𝑞 ∈ ( ( 𝐸 × 𝐹 ) ↑_m Word ( 𝐸 ∪ 𝐹 ) ) ) ∧ 𝑓 ∈ 𝐹 ) ∧ 𝑣 ∈ ( ^◡ 𝑞 “ ( 𝐸 × { 𝑓 } ) ) ) ∧ 𝑣 ∈ ( 𝐺 supp 0 ) ) → ( 2^nd ‘ ( 𝑞 ‘ 𝑣 ) ) ∈ { 𝑓 } )
299	294 298	eqeltrd	⊢ ( ( ( ( ( 𝜑 ∧ 𝑞 ∈ ( ( 𝐸 × 𝐹 ) ↑_m Word ( 𝐸 ∪ 𝐹 ) ) ) ∧ 𝑓 ∈ 𝐹 ) ∧ 𝑣 ∈ ( ^◡ 𝑞 “ ( 𝐸 × { 𝑓 } ) ) ) ∧ 𝑣 ∈ ( 𝐺 supp 0 ) ) → ( ( 𝑢 ∈ ( 𝐺 supp 0 ) ↦ ( 2^nd ‘ ( 𝑞 ‘ 𝑢 ) ) ) ‘ 𝑣 ) ∈ { 𝑓 } )
300	288 289 299	elpreimad	⊢ ( ( ( ( ( 𝜑 ∧ 𝑞 ∈ ( ( 𝐸 × 𝐹 ) ↑_m Word ( 𝐸 ∪ 𝐹 ) ) ) ∧ 𝑓 ∈ 𝐹 ) ∧ 𝑣 ∈ ( ^◡ 𝑞 “ ( 𝐸 × { 𝑓 } ) ) ) ∧ 𝑣 ∈ ( 𝐺 supp 0 ) ) → 𝑣 ∈ ( ^◡ ( 𝑢 ∈ ( 𝐺 supp 0 ) ↦ ( 2^nd ‘ ( 𝑞 ‘ 𝑢 ) ) ) “ { 𝑓 } ) )
301	300	stoic1a	⊢ ( ( ( ( ( 𝜑 ∧ 𝑞 ∈ ( ( 𝐸 × 𝐹 ) ↑_m Word ( 𝐸 ∪ 𝐹 ) ) ) ∧ 𝑓 ∈ 𝐹 ) ∧ 𝑣 ∈ ( ^◡ 𝑞 “ ( 𝐸 × { 𝑓 } ) ) ) ∧ ¬ 𝑣 ∈ ( ^◡ ( 𝑢 ∈ ( 𝐺 supp 0 ) ↦ ( 2^nd ‘ ( 𝑞 ‘ 𝑢 ) ) ) “ { 𝑓 } ) ) → ¬ 𝑣 ∈ ( 𝐺 supp 0 ) )
302	301	anasss	⊢ ( ( ( ( 𝜑 ∧ 𝑞 ∈ ( ( 𝐸 × 𝐹 ) ↑_m Word ( 𝐸 ∪ 𝐹 ) ) ) ∧ 𝑓 ∈ 𝐹 ) ∧ ( 𝑣 ∈ ( ^◡ 𝑞 “ ( 𝐸 × { 𝑓 } ) ) ∧ ¬ 𝑣 ∈ ( ^◡ ( 𝑢 ∈ ( 𝐺 supp 0 ) ↦ ( 2^nd ‘ ( 𝑞 ‘ 𝑢 ) ) ) “ { 𝑓 } ) ) ) → ¬ 𝑣 ∈ ( 𝐺 supp 0 ) )
303	283 302	sylan2b	⊢ ( ( ( ( 𝜑 ∧ 𝑞 ∈ ( ( 𝐸 × 𝐹 ) ↑_m Word ( 𝐸 ∪ 𝐹 ) ) ) ∧ 𝑓 ∈ 𝐹 ) ∧ 𝑣 ∈ ( ( ^◡ 𝑞 “ ( 𝐸 × { 𝑓 } ) ) ∖ ( ^◡ ( 𝑢 ∈ ( 𝐺 supp 0 ) ↦ ( 2^nd ‘ ( 𝑞 ‘ 𝑢 ) ) ) “ { 𝑓 } ) ) ) → ¬ 𝑣 ∈ ( 𝐺 supp 0 ) )
304	282 303	eldifd	⊢ ( ( ( ( 𝜑 ∧ 𝑞 ∈ ( ( 𝐸 × 𝐹 ) ↑_m Word ( 𝐸 ∪ 𝐹 ) ) ) ∧ 𝑓 ∈ 𝐹 ) ∧ 𝑣 ∈ ( ( ^◡ 𝑞 “ ( 𝐸 × { 𝑓 } ) ) ∖ ( ^◡ ( 𝑢 ∈ ( 𝐺 supp 0 ) ↦ ( 2^nd ‘ ( 𝑞 ‘ 𝑢 ) ) ) “ { 𝑓 } ) ) ) → 𝑣 ∈ ( Word ( 𝐸 ∪ 𝐹 ) ∖ ( 𝐺 supp 0 ) ) )
305	276 277 278 304	fvdifsupp	⊢ ( ( ( ( 𝜑 ∧ 𝑞 ∈ ( ( 𝐸 × 𝐹 ) ↑_m Word ( 𝐸 ∪ 𝐹 ) ) ) ∧ 𝑓 ∈ 𝐹 ) ∧ 𝑣 ∈ ( ( ^◡ 𝑞 “ ( 𝐸 × { 𝑓 } ) ) ∖ ( ^◡ ( 𝑢 ∈ ( 𝐺 supp 0 ) ↦ ( 2^nd ‘ ( 𝑞 ‘ 𝑢 ) ) ) “ { 𝑓 } ) ) ) → ( 𝐺 ‘ 𝑣 ) = 0 )
306	305	oveq1d	⊢ ( ( ( ( 𝜑 ∧ 𝑞 ∈ ( ( 𝐸 × 𝐹 ) ↑_m Word ( 𝐸 ∪ 𝐹 ) ) ) ∧ 𝑓 ∈ 𝐹 ) ∧ 𝑣 ∈ ( ( ^◡ 𝑞 “ ( 𝐸 × { 𝑓 } ) ) ∖ ( ^◡ ( 𝑢 ∈ ( 𝐺 supp 0 ) ↦ ( 2^nd ‘ ( 𝑞 ‘ 𝑢 ) ) ) “ { 𝑓 } ) ) ) → ( ( 𝐺 ‘ 𝑣 ) ( ._g ‘ 𝑅 ) ( ( mulGrp ‘ 𝑅 ) Σ_g 𝑣 ) ) = ( 0 ( ._g ‘ 𝑅 ) ( ( mulGrp ‘ 𝑅 ) Σ_g 𝑣 ) ) )
307	172	ad3antrrr	⊢ ( ( ( ( 𝜑 ∧ 𝑞 ∈ ( ( 𝐸 × 𝐹 ) ↑_m Word ( 𝐸 ∪ 𝐹 ) ) ) ∧ 𝑓 ∈ 𝐹 ) ∧ 𝑣 ∈ ( ( ^◡ 𝑞 “ ( 𝐸 × { 𝑓 } ) ) ∖ ( ^◡ ( 𝑢 ∈ ( 𝐺 supp 0 ) ↦ ( 2^nd ‘ ( 𝑞 ‘ 𝑢 ) ) ) “ { 𝑓 } ) ) ) → ( mulGrp ‘ 𝑅 ) ∈ Mnd )
308	179	adantr	⊢ ( ( ( 𝜑 ∧ 𝑞 ∈ ( ( 𝐸 × 𝐹 ) ↑_m Word ( 𝐸 ∪ 𝐹 ) ) ) ∧ 𝑓 ∈ 𝐹 ) → Word ( 𝐸 ∪ 𝐹 ) ⊆ Word 𝐵 )
309	223 308	sstrd	⊢ ( ( ( 𝜑 ∧ 𝑞 ∈ ( ( 𝐸 × 𝐹 ) ↑_m Word ( 𝐸 ∪ 𝐹 ) ) ) ∧ 𝑓 ∈ 𝐹 ) → ( ^◡ 𝑞 “ ( 𝐸 × { 𝑓 } ) ) ⊆ Word 𝐵 )
310	309	ssdifssd	⊢ ( ( ( 𝜑 ∧ 𝑞 ∈ ( ( 𝐸 × 𝐹 ) ↑_m Word ( 𝐸 ∪ 𝐹 ) ) ) ∧ 𝑓 ∈ 𝐹 ) → ( ( ^◡ 𝑞 “ ( 𝐸 × { 𝑓 } ) ) ∖ ( ^◡ ( 𝑢 ∈ ( 𝐺 supp 0 ) ↦ ( 2^nd ‘ ( 𝑞 ‘ 𝑢 ) ) ) “ { 𝑓 } ) ) ⊆ Word 𝐵 )
311	310	sselda	⊢ ( ( ( ( 𝜑 ∧ 𝑞 ∈ ( ( 𝐸 × 𝐹 ) ↑_m Word ( 𝐸 ∪ 𝐹 ) ) ) ∧ 𝑓 ∈ 𝐹 ) ∧ 𝑣 ∈ ( ( ^◡ 𝑞 “ ( 𝐸 × { 𝑓 } ) ) ∖ ( ^◡ ( 𝑢 ∈ ( 𝐺 supp 0 ) ↦ ( 2^nd ‘ ( 𝑞 ‘ 𝑢 ) ) ) “ { 𝑓 } ) ) ) → 𝑣 ∈ Word 𝐵 )
312	183	gsumwcl	⊢ ( ( ( mulGrp ‘ 𝑅 ) ∈ Mnd ∧ 𝑣 ∈ Word 𝐵 ) → ( ( mulGrp ‘ 𝑅 ) Σ_g 𝑣 ) ∈ 𝐵 )
313	307 311 312	syl2anc	⊢ ( ( ( ( 𝜑 ∧ 𝑞 ∈ ( ( 𝐸 × 𝐹 ) ↑_m Word ( 𝐸 ∪ 𝐹 ) ) ) ∧ 𝑓 ∈ 𝐹 ) ∧ 𝑣 ∈ ( ( ^◡ 𝑞 “ ( 𝐸 × { 𝑓 } ) ) ∖ ( ^◡ ( 𝑢 ∈ ( 𝐺 supp 0 ) ↦ ( 2^nd ‘ ( 𝑞 ‘ 𝑢 ) ) ) “ { 𝑓 } ) ) ) → ( ( mulGrp ‘ 𝑅 ) Σ_g 𝑣 ) ∈ 𝐵 )
314	1 3 24	mulg0	⊢ ( ( ( mulGrp ‘ 𝑅 ) Σ_g 𝑣 ) ∈ 𝐵 → ( 0 ( ._g ‘ 𝑅 ) ( ( mulGrp ‘ 𝑅 ) Σ_g 𝑣 ) ) = 0 )
315	313 314	syl	⊢ ( ( ( ( 𝜑 ∧ 𝑞 ∈ ( ( 𝐸 × 𝐹 ) ↑_m Word ( 𝐸 ∪ 𝐹 ) ) ) ∧ 𝑓 ∈ 𝐹 ) ∧ 𝑣 ∈ ( ( ^◡ 𝑞 “ ( 𝐸 × { 𝑓 } ) ) ∖ ( ^◡ ( 𝑢 ∈ ( 𝐺 supp 0 ) ↦ ( 2^nd ‘ ( 𝑞 ‘ 𝑢 ) ) ) “ { 𝑓 } ) ) ) → ( 0 ( ._g ‘ 𝑅 ) ( ( mulGrp ‘ 𝑅 ) Σ_g 𝑣 ) ) = 0 )
316	306 315	eqtrd	⊢ ( ( ( ( 𝜑 ∧ 𝑞 ∈ ( ( 𝐸 × 𝐹 ) ↑_m Word ( 𝐸 ∪ 𝐹 ) ) ) ∧ 𝑓 ∈ 𝐹 ) ∧ 𝑣 ∈ ( ( ^◡ 𝑞 “ ( 𝐸 × { 𝑓 } ) ) ∖ ( ^◡ ( 𝑢 ∈ ( 𝐺 supp 0 ) ↦ ( 2^nd ‘ ( 𝑞 ‘ 𝑢 ) ) ) “ { 𝑓 } ) ) ) → ( ( 𝐺 ‘ 𝑣 ) ( ._g ‘ 𝑅 ) ( ( mulGrp ‘ 𝑅 ) Σ_g 𝑣 ) ) = 0 )
317	316	ralrimiva	⊢ ( ( ( 𝜑 ∧ 𝑞 ∈ ( ( 𝐸 × 𝐹 ) ↑_m Word ( 𝐸 ∪ 𝐹 ) ) ) ∧ 𝑓 ∈ 𝐹 ) → ∀ 𝑣 ∈ ( ( ^◡ 𝑞 “ ( 𝐸 × { 𝑓 } ) ) ∖ ( ^◡ ( 𝑢 ∈ ( 𝐺 supp 0 ) ↦ ( 2^nd ‘ ( 𝑞 ‘ 𝑢 ) ) ) “ { 𝑓 } ) ) ( ( 𝐺 ‘ 𝑣 ) ( ._g ‘ 𝑅 ) ( ( mulGrp ‘ 𝑅 ) Σ_g 𝑣 ) ) = 0 )
318	257	eqeq1d	⊢ ( 𝑣 = 𝑤 → ( ( ( 𝐺 ‘ 𝑣 ) ( ._g ‘ 𝑅 ) ( ( mulGrp ‘ 𝑅 ) Σ_g 𝑣 ) ) = 0 ↔ ( ( 𝐺 ‘ 𝑤 ) ( ._g ‘ 𝑅 ) ( ( mulGrp ‘ 𝑅 ) Σ_g 𝑤 ) ) = 0 ) )
319	318	cbvralvw	⊢ ( ∀ 𝑣 ∈ ( ( ^◡ 𝑞 “ ( 𝐸 × { 𝑓 } ) ) ∖ ( ^◡ ( 𝑢 ∈ ( 𝐺 supp 0 ) ↦ ( 2^nd ‘ ( 𝑞 ‘ 𝑢 ) ) ) “ { 𝑓 } ) ) ( ( 𝐺 ‘ 𝑣 ) ( ._g ‘ 𝑅 ) ( ( mulGrp ‘ 𝑅 ) Σ_g 𝑣 ) ) = 0 ↔ ∀ 𝑤 ∈ ( ( ^◡ 𝑞 “ ( 𝐸 × { 𝑓 } ) ) ∖ ( ^◡ ( 𝑢 ∈ ( 𝐺 supp 0 ) ↦ ( 2^nd ‘ ( 𝑞 ‘ 𝑢 ) ) ) “ { 𝑓 } ) ) ( ( 𝐺 ‘ 𝑤 ) ( ._g ‘ 𝑅 ) ( ( mulGrp ‘ 𝑅 ) Σ_g 𝑤 ) ) = 0 )
320		2fveq3	⊢ ( 𝑢 = 𝑤 → ( 2^nd ‘ ( 𝑞 ‘ 𝑢 ) ) = ( 2^nd ‘ ( 𝑞 ‘ 𝑤 ) ) )
321	320	cbvmptv	⊢ ( 𝑢 ∈ ( 𝐺 supp 0 ) ↦ ( 2^nd ‘ ( 𝑞 ‘ 𝑢 ) ) ) = ( 𝑤 ∈ ( 𝐺 supp 0 ) ↦ ( 2^nd ‘ ( 𝑞 ‘ 𝑤 ) ) )
322	321 215	eqtr4i	⊢ ( 𝑢 ∈ ( 𝐺 supp 0 ) ↦ ( 2^nd ‘ ( 𝑞 ‘ 𝑢 ) ) ) = ( 𝑣 ∈ ( 𝐺 supp 0 ) ↦ ( 2^nd ‘ ( 𝑞 ‘ 𝑣 ) ) )
323	322	cnveqi	⊢ ^◡ ( 𝑢 ∈ ( 𝐺 supp 0 ) ↦ ( 2^nd ‘ ( 𝑞 ‘ 𝑢 ) ) ) = ^◡ ( 𝑣 ∈ ( 𝐺 supp 0 ) ↦ ( 2^nd ‘ ( 𝑞 ‘ 𝑣 ) ) )
324	323	imaeq1i	⊢ ( ^◡ ( 𝑢 ∈ ( 𝐺 supp 0 ) ↦ ( 2^nd ‘ ( 𝑞 ‘ 𝑢 ) ) ) “ { 𝑓 } ) = ( ^◡ ( 𝑣 ∈ ( 𝐺 supp 0 ) ↦ ( 2^nd ‘ ( 𝑞 ‘ 𝑣 ) ) ) “ { 𝑓 } )
325	324	difeq2i	⊢ ( ( ^◡ 𝑞 “ ( 𝐸 × { 𝑓 } ) ) ∖ ( ^◡ ( 𝑢 ∈ ( 𝐺 supp 0 ) ↦ ( 2^nd ‘ ( 𝑞 ‘ 𝑢 ) ) ) “ { 𝑓 } ) ) = ( ( ^◡ 𝑞 “ ( 𝐸 × { 𝑓 } ) ) ∖ ( ^◡ ( 𝑣 ∈ ( 𝐺 supp 0 ) ↦ ( 2^nd ‘ ( 𝑞 ‘ 𝑣 ) ) ) “ { 𝑓 } ) )
326	325	raleqi	⊢ ( ∀ 𝑤 ∈ ( ( ^◡ 𝑞 “ ( 𝐸 × { 𝑓 } ) ) ∖ ( ^◡ ( 𝑢 ∈ ( 𝐺 supp 0 ) ↦ ( 2^nd ‘ ( 𝑞 ‘ 𝑢 ) ) ) “ { 𝑓 } ) ) ( ( 𝐺 ‘ 𝑤 ) ( ._g ‘ 𝑅 ) ( ( mulGrp ‘ 𝑅 ) Σ_g 𝑤 ) ) = 0 ↔ ∀ 𝑤 ∈ ( ( ^◡ 𝑞 “ ( 𝐸 × { 𝑓 } ) ) ∖ ( ^◡ ( 𝑣 ∈ ( 𝐺 supp 0 ) ↦ ( 2^nd ‘ ( 𝑞 ‘ 𝑣 ) ) ) “ { 𝑓 } ) ) ( ( 𝐺 ‘ 𝑤 ) ( ._g ‘ 𝑅 ) ( ( mulGrp ‘ 𝑅 ) Σ_g 𝑤 ) ) = 0 )
327	319 326	bitri	⊢ ( ∀ 𝑣 ∈ ( ( ^◡ 𝑞 “ ( 𝐸 × { 𝑓 } ) ) ∖ ( ^◡ ( 𝑢 ∈ ( 𝐺 supp 0 ) ↦ ( 2^nd ‘ ( 𝑞 ‘ 𝑢 ) ) ) “ { 𝑓 } ) ) ( ( 𝐺 ‘ 𝑣 ) ( ._g ‘ 𝑅 ) ( ( mulGrp ‘ 𝑅 ) Σ_g 𝑣 ) ) = 0 ↔ ∀ 𝑤 ∈ ( ( ^◡ 𝑞 “ ( 𝐸 × { 𝑓 } ) ) ∖ ( ^◡ ( 𝑣 ∈ ( 𝐺 supp 0 ) ↦ ( 2^nd ‘ ( 𝑞 ‘ 𝑣 ) ) ) “ { 𝑓 } ) ) ( ( 𝐺 ‘ 𝑤 ) ( ._g ‘ 𝑅 ) ( ( mulGrp ‘ 𝑅 ) Σ_g 𝑤 ) ) = 0 )
328	317 327	sylib	⊢ ( ( ( 𝜑 ∧ 𝑞 ∈ ( ( 𝐸 × 𝐹 ) ↑_m Word ( 𝐸 ∪ 𝐹 ) ) ) ∧ 𝑓 ∈ 𝐹 ) → ∀ 𝑤 ∈ ( ( ^◡ 𝑞 “ ( 𝐸 × { 𝑓 } ) ) ∖ ( ^◡ ( 𝑣 ∈ ( 𝐺 supp 0 ) ↦ ( 2^nd ‘ ( 𝑞 ‘ 𝑣 ) ) ) “ { 𝑓 } ) ) ( ( 𝐺 ‘ 𝑤 ) ( ._g ‘ 𝑅 ) ( ( mulGrp ‘ 𝑅 ) Σ_g 𝑤 ) ) = 0 )
329	328	r19.21bi	⊢ ( ( ( ( 𝜑 ∧ 𝑞 ∈ ( ( 𝐸 × 𝐹 ) ↑_m Word ( 𝐸 ∪ 𝐹 ) ) ) ∧ 𝑓 ∈ 𝐹 ) ∧ 𝑤 ∈ ( ( ^◡ 𝑞 “ ( 𝐸 × { 𝑓 } ) ) ∖ ( ^◡ ( 𝑣 ∈ ( 𝐺 supp 0 ) ↦ ( 2^nd ‘ ( 𝑞 ‘ 𝑣 ) ) ) “ { 𝑓 } ) ) ) → ( ( 𝐺 ‘ 𝑤 ) ( ._g ‘ 𝑅 ) ( ( mulGrp ‘ 𝑅 ) Σ_g 𝑤 ) ) = 0 )
330	189	adantr	⊢ ( ( ( 𝜑 ∧ 𝑞 ∈ ( ( 𝐸 × 𝐹 ) ↑_m Word ( 𝐸 ∪ 𝐹 ) ) ) ∧ 𝑓 ∈ 𝐹 ) → ( 𝐺 supp 0 ) ∈ Fin )
331	330	cnvimamptfin	⊢ ( ( ( 𝜑 ∧ 𝑞 ∈ ( ( 𝐸 × 𝐹 ) ↑_m Word ( 𝐸 ∪ 𝐹 ) ) ) ∧ 𝑓 ∈ 𝐹 ) → ( ^◡ ( 𝑣 ∈ ( 𝐺 supp 0 ) ↦ ( 2^nd ‘ ( 𝑞 ‘ 𝑣 ) ) ) “ { 𝑓 } ) ∈ Fin )
332	25	ad3antrrr	⊢ ( ( ( ( 𝜑 ∧ 𝑞 ∈ ( ( 𝐸 × 𝐹 ) ↑_m Word ( 𝐸 ∪ 𝐹 ) ) ) ∧ 𝑓 ∈ 𝐹 ) ∧ 𝑤 ∈ ( ^◡ 𝑞 “ ( 𝐸 × { 𝑓 } ) ) ) → 𝑅 ∈ Grp )
333	191	ad2antrr	⊢ ( ( ( ( 𝜑 ∧ 𝑞 ∈ ( ( 𝐸 × 𝐹 ) ↑_m Word ( 𝐸 ∪ 𝐹 ) ) ) ∧ 𝑓 ∈ 𝐹 ) ∧ 𝑤 ∈ ( ^◡ 𝑞 “ ( 𝐸 × { 𝑓 } ) ) ) → 𝐺 : Word ( 𝐸 ∪ 𝐹 ) ⟶ ℤ )
334	223	sselda	⊢ ( ( ( ( 𝜑 ∧ 𝑞 ∈ ( ( 𝐸 × 𝐹 ) ↑_m Word ( 𝐸 ∪ 𝐹 ) ) ) ∧ 𝑓 ∈ 𝐹 ) ∧ 𝑤 ∈ ( ^◡ 𝑞 “ ( 𝐸 × { 𝑓 } ) ) ) → 𝑤 ∈ Word ( 𝐸 ∪ 𝐹 ) )
335	333 334	ffvelcdmd	⊢ ( ( ( ( 𝜑 ∧ 𝑞 ∈ ( ( 𝐸 × 𝐹 ) ↑_m Word ( 𝐸 ∪ 𝐹 ) ) ) ∧ 𝑓 ∈ 𝐹 ) ∧ 𝑤 ∈ ( ^◡ 𝑞 “ ( 𝐸 × { 𝑓 } ) ) ) → ( 𝐺 ‘ 𝑤 ) ∈ ℤ )
336	172	ad3antrrr	⊢ ( ( ( ( 𝜑 ∧ 𝑞 ∈ ( ( 𝐸 × 𝐹 ) ↑_m Word ( 𝐸 ∪ 𝐹 ) ) ) ∧ 𝑓 ∈ 𝐹 ) ∧ 𝑤 ∈ ( ^◡ 𝑞 “ ( 𝐸 × { 𝑓 } ) ) ) → ( mulGrp ‘ 𝑅 ) ∈ Mnd )
337	309	sselda	⊢ ( ( ( ( 𝜑 ∧ 𝑞 ∈ ( ( 𝐸 × 𝐹 ) ↑_m Word ( 𝐸 ∪ 𝐹 ) ) ) ∧ 𝑓 ∈ 𝐹 ) ∧ 𝑤 ∈ ( ^◡ 𝑞 “ ( 𝐸 × { 𝑓 } ) ) ) → 𝑤 ∈ Word 𝐵 )
338	336 337 184	syl2anc	⊢ ( ( ( ( 𝜑 ∧ 𝑞 ∈ ( ( 𝐸 × 𝐹 ) ↑_m Word ( 𝐸 ∪ 𝐹 ) ) ) ∧ 𝑓 ∈ 𝐹 ) ∧ 𝑤 ∈ ( ^◡ 𝑞 “ ( 𝐸 × { 𝑓 } ) ) ) → ( ( mulGrp ‘ 𝑅 ) Σ_g 𝑤 ) ∈ 𝐵 )
339	1 24 332 335 338	mulgcld	⊢ ( ( ( ( 𝜑 ∧ 𝑞 ∈ ( ( 𝐸 × 𝐹 ) ↑_m Word ( 𝐸 ∪ 𝐹 ) ) ) ∧ 𝑓 ∈ 𝐹 ) ∧ 𝑤 ∈ ( ^◡ 𝑞 “ ( 𝐸 × { 𝑓 } ) ) ) → ( ( 𝐺 ‘ 𝑤 ) ( ._g ‘ 𝑅 ) ( ( mulGrp ‘ 𝑅 ) Σ_g 𝑤 ) ) ∈ 𝐵 )
340	241	ad2antrr	⊢ ( ( ( ( 𝜑 ∧ 𝑞 ∈ ( ( 𝐸 × 𝐹 ) ↑_m Word ( 𝐸 ∪ 𝐹 ) ) ) ∧ 𝑓 ∈ 𝐹 ) ∧ 𝑣 ∈ ( ^◡ ( 𝑢 ∈ ( 𝐺 supp 0 ) ↦ ( 2^nd ‘ ( 𝑞 ‘ 𝑢 ) ) ) “ { 𝑓 } ) ) → 𝑞 Fn Word ( 𝐸 ∪ 𝐹 ) )
341	198	ad2antrr	⊢ ( ( ( ( 𝜑 ∧ 𝑞 ∈ ( ( 𝐸 × 𝐹 ) ↑_m Word ( 𝐸 ∪ 𝐹 ) ) ) ∧ 𝑓 ∈ 𝐹 ) ∧ 𝑣 ∈ ( ^◡ ( 𝑢 ∈ ( 𝐺 supp 0 ) ↦ ( 2^nd ‘ ( 𝑞 ‘ 𝑢 ) ) ) “ { 𝑓 } ) ) → ( 𝐺 supp 0 ) ⊆ Word ( 𝐸 ∪ 𝐹 ) )
342		nfv	⊢ Ⅎ 𝑤 ( ( ( 𝜑 ∧ 𝑞 ∈ ( ( 𝐸 × 𝐹 ) ↑_m Word ( 𝐸 ∪ 𝐹 ) ) ) ∧ 𝑓 ∈ 𝐹 ) ∧ 𝑣 ∈ ( ^◡ ( 𝑢 ∈ ( 𝐺 supp 0 ) ↦ ( 2^nd ‘ ( 𝑞 ‘ 𝑢 ) ) ) “ { 𝑓 } ) )
343		fvexd	⊢ ( ( ( ( ( 𝜑 ∧ 𝑞 ∈ ( ( 𝐸 × 𝐹 ) ↑_m Word ( 𝐸 ∪ 𝐹 ) ) ) ∧ 𝑓 ∈ 𝐹 ) ∧ 𝑣 ∈ ( ^◡ ( 𝑢 ∈ ( 𝐺 supp 0 ) ↦ ( 2^nd ‘ ( 𝑞 ‘ 𝑢 ) ) ) “ { 𝑓 } ) ) ∧ 𝑤 ∈ ( 𝐺 supp 0 ) ) → ( 2^nd ‘ ( 𝑞 ‘ 𝑤 ) ) ∈ V )
344	342 343 321	fnmptd	⊢ ( ( ( ( 𝜑 ∧ 𝑞 ∈ ( ( 𝐸 × 𝐹 ) ↑_m Word ( 𝐸 ∪ 𝐹 ) ) ) ∧ 𝑓 ∈ 𝐹 ) ∧ 𝑣 ∈ ( ^◡ ( 𝑢 ∈ ( 𝐺 supp 0 ) ↦ ( 2^nd ‘ ( 𝑞 ‘ 𝑢 ) ) ) “ { 𝑓 } ) ) → ( 𝑢 ∈ ( 𝐺 supp 0 ) ↦ ( 2^nd ‘ ( 𝑞 ‘ 𝑢 ) ) ) Fn ( 𝐺 supp 0 ) )
345		elpreima	⊢ ( ( 𝑢 ∈ ( 𝐺 supp 0 ) ↦ ( 2^nd ‘ ( 𝑞 ‘ 𝑢 ) ) ) Fn ( 𝐺 supp 0 ) → ( 𝑣 ∈ ( ^◡ ( 𝑢 ∈ ( 𝐺 supp 0 ) ↦ ( 2^nd ‘ ( 𝑞 ‘ 𝑢 ) ) ) “ { 𝑓 } ) ↔ ( 𝑣 ∈ ( 𝐺 supp 0 ) ∧ ( ( 𝑢 ∈ ( 𝐺 supp 0 ) ↦ ( 2^nd ‘ ( 𝑞 ‘ 𝑢 ) ) ) ‘ 𝑣 ) ∈ { 𝑓 } ) ) )
346	345	simprbda	⊢ ( ( ( 𝑢 ∈ ( 𝐺 supp 0 ) ↦ ( 2^nd ‘ ( 𝑞 ‘ 𝑢 ) ) ) Fn ( 𝐺 supp 0 ) ∧ 𝑣 ∈ ( ^◡ ( 𝑢 ∈ ( 𝐺 supp 0 ) ↦ ( 2^nd ‘ ( 𝑞 ‘ 𝑢 ) ) ) “ { 𝑓 } ) ) → 𝑣 ∈ ( 𝐺 supp 0 ) )
347	344 346	sylancom	⊢ ( ( ( ( 𝜑 ∧ 𝑞 ∈ ( ( 𝐸 × 𝐹 ) ↑_m Word ( 𝐸 ∪ 𝐹 ) ) ) ∧ 𝑓 ∈ 𝐹 ) ∧ 𝑣 ∈ ( ^◡ ( 𝑢 ∈ ( 𝐺 supp 0 ) ↦ ( 2^nd ‘ ( 𝑞 ‘ 𝑢 ) ) ) “ { 𝑓 } ) ) → 𝑣 ∈ ( 𝐺 supp 0 ) )
348	341 347	sseldd	⊢ ( ( ( ( 𝜑 ∧ 𝑞 ∈ ( ( 𝐸 × 𝐹 ) ↑_m Word ( 𝐸 ∪ 𝐹 ) ) ) ∧ 𝑓 ∈ 𝐹 ) ∧ 𝑣 ∈ ( ^◡ ( 𝑢 ∈ ( 𝐺 supp 0 ) ↦ ( 2^nd ‘ ( 𝑞 ‘ 𝑢 ) ) ) “ { 𝑓 } ) ) → 𝑣 ∈ Word ( 𝐸 ∪ 𝐹 ) )
349	32	ad2antrr	⊢ ( ( ( ( 𝜑 ∧ 𝑞 ∈ ( ( 𝐸 × 𝐹 ) ↑_m Word ( 𝐸 ∪ 𝐹 ) ) ) ∧ 𝑓 ∈ 𝐹 ) ∧ 𝑣 ∈ ( ^◡ ( 𝑢 ∈ ( 𝐺 supp 0 ) ↦ ( 2^nd ‘ ( 𝑞 ‘ 𝑢 ) ) ) “ { 𝑓 } ) ) → 𝑞 : Word ( 𝐸 ∪ 𝐹 ) ⟶ ( 𝐸 × 𝐹 ) )
350	349 348	ffvelcdmd	⊢ ( ( ( ( 𝜑 ∧ 𝑞 ∈ ( ( 𝐸 × 𝐹 ) ↑_m Word ( 𝐸 ∪ 𝐹 ) ) ) ∧ 𝑓 ∈ 𝐹 ) ∧ 𝑣 ∈ ( ^◡ ( 𝑢 ∈ ( 𝐺 supp 0 ) ↦ ( 2^nd ‘ ( 𝑞 ‘ 𝑢 ) ) ) “ { 𝑓 } ) ) → ( 𝑞 ‘ 𝑣 ) ∈ ( 𝐸 × 𝐹 ) )
351		1st2nd2	⊢ ( ( 𝑞 ‘ 𝑣 ) ∈ ( 𝐸 × 𝐹 ) → ( 𝑞 ‘ 𝑣 ) = ⟨ ( 1^st ‘ ( 𝑞 ‘ 𝑣 ) ) , ( 2^nd ‘ ( 𝑞 ‘ 𝑣 ) ) ⟩ )
352	350 351	syl	⊢ ( ( ( ( 𝜑 ∧ 𝑞 ∈ ( ( 𝐸 × 𝐹 ) ↑_m Word ( 𝐸 ∪ 𝐹 ) ) ) ∧ 𝑓 ∈ 𝐹 ) ∧ 𝑣 ∈ ( ^◡ ( 𝑢 ∈ ( 𝐺 supp 0 ) ↦ ( 2^nd ‘ ( 𝑞 ‘ 𝑢 ) ) ) “ { 𝑓 } ) ) → ( 𝑞 ‘ 𝑣 ) = ⟨ ( 1^st ‘ ( 𝑞 ‘ 𝑣 ) ) , ( 2^nd ‘ ( 𝑞 ‘ 𝑣 ) ) ⟩ )
353	350 143	syl	⊢ ( ( ( ( 𝜑 ∧ 𝑞 ∈ ( ( 𝐸 × 𝐹 ) ↑_m Word ( 𝐸 ∪ 𝐹 ) ) ) ∧ 𝑓 ∈ 𝐹 ) ∧ 𝑣 ∈ ( ^◡ ( 𝑢 ∈ ( 𝐺 supp 0 ) ↦ ( 2^nd ‘ ( 𝑞 ‘ 𝑢 ) ) ) “ { 𝑓 } ) ) → ( 1^st ‘ ( 𝑞 ‘ 𝑣 ) ) ∈ 𝐸 )
354	347 293	syldan	⊢ ( ( ( ( 𝜑 ∧ 𝑞 ∈ ( ( 𝐸 × 𝐹 ) ↑_m Word ( 𝐸 ∪ 𝐹 ) ) ) ∧ 𝑓 ∈ 𝐹 ) ∧ 𝑣 ∈ ( ^◡ ( 𝑢 ∈ ( 𝐺 supp 0 ) ↦ ( 2^nd ‘ ( 𝑞 ‘ 𝑢 ) ) ) “ { 𝑓 } ) ) → ( ( 𝑢 ∈ ( 𝐺 supp 0 ) ↦ ( 2^nd ‘ ( 𝑞 ‘ 𝑢 ) ) ) ‘ 𝑣 ) = ( 2^nd ‘ ( 𝑞 ‘ 𝑣 ) ) )
355	345	simplbda	⊢ ( ( ( 𝑢 ∈ ( 𝐺 supp 0 ) ↦ ( 2^nd ‘ ( 𝑞 ‘ 𝑢 ) ) ) Fn ( 𝐺 supp 0 ) ∧ 𝑣 ∈ ( ^◡ ( 𝑢 ∈ ( 𝐺 supp 0 ) ↦ ( 2^nd ‘ ( 𝑞 ‘ 𝑢 ) ) ) “ { 𝑓 } ) ) → ( ( 𝑢 ∈ ( 𝐺 supp 0 ) ↦ ( 2^nd ‘ ( 𝑞 ‘ 𝑢 ) ) ) ‘ 𝑣 ) ∈ { 𝑓 } )
356	344 355	sylancom	⊢ ( ( ( ( 𝜑 ∧ 𝑞 ∈ ( ( 𝐸 × 𝐹 ) ↑_m Word ( 𝐸 ∪ 𝐹 ) ) ) ∧ 𝑓 ∈ 𝐹 ) ∧ 𝑣 ∈ ( ^◡ ( 𝑢 ∈ ( 𝐺 supp 0 ) ↦ ( 2^nd ‘ ( 𝑞 ‘ 𝑢 ) ) ) “ { 𝑓 } ) ) → ( ( 𝑢 ∈ ( 𝐺 supp 0 ) ↦ ( 2^nd ‘ ( 𝑞 ‘ 𝑢 ) ) ) ‘ 𝑣 ) ∈ { 𝑓 } )
357	354 356	eqeltrrd	⊢ ( ( ( ( 𝜑 ∧ 𝑞 ∈ ( ( 𝐸 × 𝐹 ) ↑_m Word ( 𝐸 ∪ 𝐹 ) ) ) ∧ 𝑓 ∈ 𝐹 ) ∧ 𝑣 ∈ ( ^◡ ( 𝑢 ∈ ( 𝐺 supp 0 ) ↦ ( 2^nd ‘ ( 𝑞 ‘ 𝑢 ) ) ) “ { 𝑓 } ) ) → ( 2^nd ‘ ( 𝑞 ‘ 𝑣 ) ) ∈ { 𝑓 } )
358	353 357	opelxpd	⊢ ( ( ( ( 𝜑 ∧ 𝑞 ∈ ( ( 𝐸 × 𝐹 ) ↑_m Word ( 𝐸 ∪ 𝐹 ) ) ) ∧ 𝑓 ∈ 𝐹 ) ∧ 𝑣 ∈ ( ^◡ ( 𝑢 ∈ ( 𝐺 supp 0 ) ↦ ( 2^nd ‘ ( 𝑞 ‘ 𝑢 ) ) ) “ { 𝑓 } ) ) → ⟨ ( 1^st ‘ ( 𝑞 ‘ 𝑣 ) ) , ( 2^nd ‘ ( 𝑞 ‘ 𝑣 ) ) ⟩ ∈ ( 𝐸 × { 𝑓 } ) )
359	352 358	eqeltrd	⊢ ( ( ( ( 𝜑 ∧ 𝑞 ∈ ( ( 𝐸 × 𝐹 ) ↑_m Word ( 𝐸 ∪ 𝐹 ) ) ) ∧ 𝑓 ∈ 𝐹 ) ∧ 𝑣 ∈ ( ^◡ ( 𝑢 ∈ ( 𝐺 supp 0 ) ↦ ( 2^nd ‘ ( 𝑞 ‘ 𝑢 ) ) ) “ { 𝑓 } ) ) → ( 𝑞 ‘ 𝑣 ) ∈ ( 𝐸 × { 𝑓 } ) )
360	340 348 359	elpreimad	⊢ ( ( ( ( 𝜑 ∧ 𝑞 ∈ ( ( 𝐸 × 𝐹 ) ↑_m Word ( 𝐸 ∪ 𝐹 ) ) ) ∧ 𝑓 ∈ 𝐹 ) ∧ 𝑣 ∈ ( ^◡ ( 𝑢 ∈ ( 𝐺 supp 0 ) ↦ ( 2^nd ‘ ( 𝑞 ‘ 𝑢 ) ) ) “ { 𝑓 } ) ) → 𝑣 ∈ ( ^◡ 𝑞 “ ( 𝐸 × { 𝑓 } ) ) )
361	360	ex	⊢ ( ( ( 𝜑 ∧ 𝑞 ∈ ( ( 𝐸 × 𝐹 ) ↑_m Word ( 𝐸 ∪ 𝐹 ) ) ) ∧ 𝑓 ∈ 𝐹 ) → ( 𝑣 ∈ ( ^◡ ( 𝑢 ∈ ( 𝐺 supp 0 ) ↦ ( 2^nd ‘ ( 𝑞 ‘ 𝑢 ) ) ) “ { 𝑓 } ) → 𝑣 ∈ ( ^◡ 𝑞 “ ( 𝐸 × { 𝑓 } ) ) ) )
362	361	ssrdv	⊢ ( ( ( 𝜑 ∧ 𝑞 ∈ ( ( 𝐸 × 𝐹 ) ↑_m Word ( 𝐸 ∪ 𝐹 ) ) ) ∧ 𝑓 ∈ 𝐹 ) → ( ^◡ ( 𝑢 ∈ ( 𝐺 supp 0 ) ↦ ( 2^nd ‘ ( 𝑞 ‘ 𝑢 ) ) ) “ { 𝑓 } ) ⊆ ( ^◡ 𝑞 “ ( 𝐸 × { 𝑓 } ) ) )
363	324 362	eqsstrrid	⊢ ( ( ( 𝜑 ∧ 𝑞 ∈ ( ( 𝐸 × 𝐹 ) ↑_m Word ( 𝐸 ∪ 𝐹 ) ) ) ∧ 𝑓 ∈ 𝐹 ) → ( ^◡ ( 𝑣 ∈ ( 𝐺 supp 0 ) ↦ ( 2^nd ‘ ( 𝑞 ‘ 𝑣 ) ) ) “ { 𝑓 } ) ⊆ ( ^◡ 𝑞 “ ( 𝐸 × { 𝑓 } ) ) )
364	1 3 275 262 329 331 339 363	gsummptres2	⊢ ( ( ( 𝜑 ∧ 𝑞 ∈ ( ( 𝐸 × 𝐹 ) ↑_m Word ( 𝐸 ∪ 𝐹 ) ) ) ∧ 𝑓 ∈ 𝐹 ) → ( 𝑅 Σ_g ( 𝑤 ∈ ( ^◡ 𝑞 “ ( 𝐸 × { 𝑓 } ) ) ↦ ( ( 𝐺 ‘ 𝑤 ) ( ._g ‘ 𝑅 ) ( ( mulGrp ‘ 𝑅 ) Σ_g 𝑤 ) ) ) ) = ( 𝑅 Σ_g ( 𝑤 ∈ ( ^◡ ( 𝑣 ∈ ( 𝐺 supp 0 ) ↦ ( 2^nd ‘ ( 𝑞 ‘ 𝑣 ) ) ) “ { 𝑓 } ) ↦ ( ( 𝐺 ‘ 𝑤 ) ( ._g ‘ 𝑅 ) ( ( mulGrp ‘ 𝑅 ) Σ_g 𝑤 ) ) ) ) )
365	364	adantlr	⊢ ( ( ( ( 𝜑 ∧ 𝑞 ∈ ( ( 𝐸 × 𝐹 ) ↑_m Word ( 𝐸 ∪ 𝐹 ) ) ) ∧ ∀ 𝑤 ∈ Word ( 𝐸 ∪ 𝐹 ) ( ( mulGrp ‘ 𝑅 ) Σ_g 𝑤 ) = ( ( 1^st ‘ ( 𝑞 ‘ 𝑤 ) ) · ( 2^nd ‘ ( 𝑞 ‘ 𝑤 ) ) ) ) ∧ 𝑓 ∈ 𝐹 ) → ( 𝑅 Σ_g ( 𝑤 ∈ ( ^◡ 𝑞 “ ( 𝐸 × { 𝑓 } ) ) ↦ ( ( 𝐺 ‘ 𝑤 ) ( ._g ‘ 𝑅 ) ( ( mulGrp ‘ 𝑅 ) Σ_g 𝑤 ) ) ) ) = ( 𝑅 Σ_g ( 𝑤 ∈ ( ^◡ ( 𝑣 ∈ ( 𝐺 supp 0 ) ↦ ( 2^nd ‘ ( 𝑞 ‘ 𝑣 ) ) ) “ { 𝑓 } ) ↦ ( ( 𝐺 ‘ 𝑤 ) ( ._g ‘ 𝑅 ) ( ( mulGrp ‘ 𝑅 ) Σ_g 𝑤 ) ) ) ) )
366	260 274 365	3eqtr3d	⊢ ( ( ( ( 𝜑 ∧ 𝑞 ∈ ( ( 𝐸 × 𝐹 ) ↑_m Word ( 𝐸 ∪ 𝐹 ) ) ) ∧ ∀ 𝑤 ∈ Word ( 𝐸 ∪ 𝐹 ) ( ( mulGrp ‘ 𝑅 ) Σ_g 𝑤 ) = ( ( 1^st ‘ ( 𝑞 ‘ 𝑤 ) ) · ( 2^nd ‘ ( 𝑞 ‘ 𝑤 ) ) ) ) ∧ 𝑓 ∈ 𝐹 ) → ( ( 𝑅 Σ_g ( 𝑣 ∈ ( ^◡ 𝑞 “ ( 𝐸 × { 𝑓 } ) ) ↦ ( ( 𝐺 ‘ 𝑣 ) ( ._g ‘ 𝑅 ) ( 1^st ‘ ( 𝑞 ‘ 𝑣 ) ) ) ) ) · 𝑓 ) = ( 𝑅 Σ_g ( 𝑤 ∈ ( ^◡ ( 𝑣 ∈ ( 𝐺 supp 0 ) ↦ ( 2^nd ‘ ( 𝑞 ‘ 𝑣 ) ) ) “ { 𝑓 } ) ↦ ( ( 𝐺 ‘ 𝑤 ) ( ._g ‘ 𝑅 ) ( ( mulGrp ‘ 𝑅 ) Σ_g 𝑤 ) ) ) ) )
367	366	mpteq2dva	⊢ ( ( ( 𝜑 ∧ 𝑞 ∈ ( ( 𝐸 × 𝐹 ) ↑_m Word ( 𝐸 ∪ 𝐹 ) ) ) ∧ ∀ 𝑤 ∈ Word ( 𝐸 ∪ 𝐹 ) ( ( mulGrp ‘ 𝑅 ) Σ_g 𝑤 ) = ( ( 1^st ‘ ( 𝑞 ‘ 𝑤 ) ) · ( 2^nd ‘ ( 𝑞 ‘ 𝑤 ) ) ) ) → ( 𝑓 ∈ 𝐹 ↦ ( ( 𝑅 Σ_g ( 𝑣 ∈ ( ^◡ 𝑞 “ ( 𝐸 × { 𝑓 } ) ) ↦ ( ( 𝐺 ‘ 𝑣 ) ( ._g ‘ 𝑅 ) ( 1^st ‘ ( 𝑞 ‘ 𝑣 ) ) ) ) ) · 𝑓 ) ) = ( 𝑓 ∈ 𝐹 ↦ ( 𝑅 Σ_g ( 𝑤 ∈ ( ^◡ ( 𝑣 ∈ ( 𝐺 supp 0 ) ↦ ( 2^nd ‘ ( 𝑞 ‘ 𝑣 ) ) ) “ { 𝑓 } ) ↦ ( ( 𝐺 ‘ 𝑤 ) ( ._g ‘ 𝑅 ) ( ( mulGrp ‘ 𝑅 ) Σ_g 𝑤 ) ) ) ) ) )
368	367	oveq2d	⊢ ( ( ( 𝜑 ∧ 𝑞 ∈ ( ( 𝐸 × 𝐹 ) ↑_m Word ( 𝐸 ∪ 𝐹 ) ) ) ∧ ∀ 𝑤 ∈ Word ( 𝐸 ∪ 𝐹 ) ( ( mulGrp ‘ 𝑅 ) Σ_g 𝑤 ) = ( ( 1^st ‘ ( 𝑞 ‘ 𝑤 ) ) · ( 2^nd ‘ ( 𝑞 ‘ 𝑤 ) ) ) ) → ( 𝑅 Σ_g ( 𝑓 ∈ 𝐹 ↦ ( ( 𝑅 Σ_g ( 𝑣 ∈ ( ^◡ 𝑞 “ ( 𝐸 × { 𝑓 } ) ) ↦ ( ( 𝐺 ‘ 𝑣 ) ( ._g ‘ 𝑅 ) ( 1^st ‘ ( 𝑞 ‘ 𝑣 ) ) ) ) ) · 𝑓 ) ) ) = ( 𝑅 Σ_g ( 𝑓 ∈ 𝐹 ↦ ( 𝑅 Σ_g ( 𝑤 ∈ ( ^◡ ( 𝑣 ∈ ( 𝐺 supp 0 ) ↦ ( 2^nd ‘ ( 𝑞 ‘ 𝑣 ) ) ) “ { 𝑓 } ) ↦ ( ( 𝐺 ‘ 𝑤 ) ( ._g ‘ 𝑅 ) ( ( mulGrp ‘ 𝑅 ) Σ_g 𝑤 ) ) ) ) ) ) )
369	218 219 368	3eqtr4d	⊢ ( ( ( 𝜑 ∧ 𝑞 ∈ ( ( 𝐸 × 𝐹 ) ↑_m Word ( 𝐸 ∪ 𝐹 ) ) ) ∧ ∀ 𝑤 ∈ Word ( 𝐸 ∪ 𝐹 ) ( ( mulGrp ‘ 𝑅 ) Σ_g 𝑤 ) = ( ( 1^st ‘ ( 𝑞 ‘ 𝑤 ) ) · ( 2^nd ‘ ( 𝑞 ‘ 𝑤 ) ) ) ) → 𝑋 = ( 𝑅 Σ_g ( 𝑓 ∈ 𝐹 ↦ ( ( 𝑅 Σ_g ( 𝑣 ∈ ( ^◡ 𝑞 “ ( 𝐸 × { 𝑓 } ) ) ↦ ( ( 𝐺 ‘ 𝑣 ) ( ._g ‘ 𝑅 ) ( 1^st ‘ ( 𝑞 ‘ 𝑣 ) ) ) ) ) · 𝑓 ) ) ) )
370	159 369	jca	⊢ ( ( ( 𝜑 ∧ 𝑞 ∈ ( ( 𝐸 × 𝐹 ) ↑_m Word ( 𝐸 ∪ 𝐹 ) ) ) ∧ ∀ 𝑤 ∈ Word ( 𝐸 ∪ 𝐹 ) ( ( mulGrp ‘ 𝑅 ) Σ_g 𝑤 ) = ( ( 1^st ‘ ( 𝑞 ‘ 𝑤 ) ) · ( 2^nd ‘ ( 𝑞 ‘ 𝑤 ) ) ) ) → ( ( 𝑓 ∈ 𝐹 ↦ ( 𝑅 Σ_g ( 𝑣 ∈ ( ^◡ 𝑞 “ ( 𝐸 × { 𝑓 } ) ) ↦ ( ( 𝐺 ‘ 𝑣 ) ( ._g ‘ 𝑅 ) ( 1^st ‘ ( 𝑞 ‘ 𝑣 ) ) ) ) ) ) finSupp 0 ∧ 𝑋 = ( 𝑅 Σ_g ( 𝑓 ∈ 𝐹 ↦ ( ( 𝑅 Σ_g ( 𝑣 ∈ ( ^◡ 𝑞 “ ( 𝐸 × { 𝑓 } ) ) ↦ ( ( 𝐺 ‘ 𝑣 ) ( ._g ‘ 𝑅 ) ( 1^st ‘ ( 𝑞 ‘ 𝑣 ) ) ) ) ) · 𝑓 ) ) ) ) )
371	65 79 370	rspcedvd	⊢ ( ( ( 𝜑 ∧ 𝑞 ∈ ( ( 𝐸 × 𝐹 ) ↑_m Word ( 𝐸 ∪ 𝐹 ) ) ) ∧ ∀ 𝑤 ∈ Word ( 𝐸 ∪ 𝐹 ) ( ( mulGrp ‘ 𝑅 ) Σ_g 𝑤 ) = ( ( 1^st ‘ ( 𝑞 ‘ 𝑤 ) ) · ( 2^nd ‘ ( 𝑞 ‘ 𝑤 ) ) ) ) → ∃ 𝑝 ∈ ( 𝐸 ↑_m 𝐹 ) ( 𝑝 finSupp 0 ∧ 𝑋 = ( 𝑅 Σ_g ( 𝑓 ∈ 𝐹 ↦ ( ( 𝑝 ‘ 𝑓 ) · 𝑓 ) ) ) ) )
372		fveq2	⊢ ( 𝑎 = ( 𝑞 ‘ 𝑤 ) → ( 1^st ‘ 𝑎 ) = ( 1^st ‘ ( 𝑞 ‘ 𝑤 ) ) )
373		fveq2	⊢ ( 𝑎 = ( 𝑞 ‘ 𝑤 ) → ( 2^nd ‘ 𝑎 ) = ( 2^nd ‘ ( 𝑞 ‘ 𝑤 ) ) )
374	372 373	oveq12d	⊢ ( 𝑎 = ( 𝑞 ‘ 𝑤 ) → ( ( 1^st ‘ 𝑎 ) · ( 2^nd ‘ 𝑎 ) ) = ( ( 1^st ‘ ( 𝑞 ‘ 𝑤 ) ) · ( 2^nd ‘ ( 𝑞 ‘ 𝑤 ) ) ) )
375	374	eqeq2d	⊢ ( 𝑎 = ( 𝑞 ‘ 𝑤 ) → ( ( ( mulGrp ‘ 𝑅 ) Σ_g 𝑤 ) = ( ( 1^st ‘ 𝑎 ) · ( 2^nd ‘ 𝑎 ) ) ↔ ( ( mulGrp ‘ 𝑅 ) Σ_g 𝑤 ) = ( ( 1^st ‘ ( 𝑞 ‘ 𝑤 ) ) · ( 2^nd ‘ ( 𝑞 ‘ 𝑤 ) ) ) ) )
376		vex	⊢ 𝑒 ∈ V
377		vex	⊢ 𝑓 ∈ V
378	376 377	op1std	⊢ ( 𝑎 = ⟨ 𝑒 , 𝑓 ⟩ → ( 1^st ‘ 𝑎 ) = 𝑒 )
379	376 377	op2ndd	⊢ ( 𝑎 = ⟨ 𝑒 , 𝑓 ⟩ → ( 2^nd ‘ 𝑎 ) = 𝑓 )
380	378 379	oveq12d	⊢ ( 𝑎 = ⟨ 𝑒 , 𝑓 ⟩ → ( ( 1^st ‘ 𝑎 ) · ( 2^nd ‘ 𝑎 ) ) = ( 𝑒 · 𝑓 ) )
381	380	eqeq2d	⊢ ( 𝑎 = ⟨ 𝑒 , 𝑓 ⟩ → ( ( ( mulGrp ‘ 𝑅 ) Σ_g 𝑤 ) = ( ( 1^st ‘ 𝑎 ) · ( 2^nd ‘ 𝑎 ) ) ↔ ( ( mulGrp ‘ 𝑅 ) Σ_g 𝑤 ) = ( 𝑒 · 𝑓 ) ) )
382		simpllr	⊢ ( ( ( ( ( 𝜑 ∧ 𝑤 ∈ Word ( 𝐸 ∪ 𝐹 ) ) ∧ 𝑒 ∈ 𝐸 ) ∧ 𝑓 ∈ 𝐹 ) ∧ ( ( mulGrp ‘ 𝑅 ) Σ_g 𝑤 ) = ( 𝑒 · 𝑓 ) ) → 𝑒 ∈ 𝐸 )
383		simplr	⊢ ( ( ( ( ( 𝜑 ∧ 𝑤 ∈ Word ( 𝐸 ∪ 𝐹 ) ) ∧ 𝑒 ∈ 𝐸 ) ∧ 𝑓 ∈ 𝐹 ) ∧ ( ( mulGrp ‘ 𝑅 ) Σ_g 𝑤 ) = ( 𝑒 · 𝑓 ) ) → 𝑓 ∈ 𝐹 )
384	382 383	opelxpd	⊢ ( ( ( ( ( 𝜑 ∧ 𝑤 ∈ Word ( 𝐸 ∪ 𝐹 ) ) ∧ 𝑒 ∈ 𝐸 ) ∧ 𝑓 ∈ 𝐹 ) ∧ ( ( mulGrp ‘ 𝑅 ) Σ_g 𝑤 ) = ( 𝑒 · 𝑓 ) ) → ⟨ 𝑒 , 𝑓 ⟩ ∈ ( 𝐸 × 𝐹 ) )
385		simpr	⊢ ( ( ( ( ( 𝜑 ∧ 𝑤 ∈ Word ( 𝐸 ∪ 𝐹 ) ) ∧ 𝑒 ∈ 𝐸 ) ∧ 𝑓 ∈ 𝐹 ) ∧ ( ( mulGrp ‘ 𝑅 ) Σ_g 𝑤 ) = ( 𝑒 · 𝑓 ) ) → ( ( mulGrp ‘ 𝑅 ) Σ_g 𝑤 ) = ( 𝑒 · 𝑓 ) )
386	381 384 385	rspcedvdw	⊢ ( ( ( ( ( 𝜑 ∧ 𝑤 ∈ Word ( 𝐸 ∪ 𝐹 ) ) ∧ 𝑒 ∈ 𝐸 ) ∧ 𝑓 ∈ 𝐹 ) ∧ ( ( mulGrp ‘ 𝑅 ) Σ_g 𝑤 ) = ( 𝑒 · 𝑓 ) ) → ∃ 𝑎 ∈ ( 𝐸 × 𝐹 ) ( ( mulGrp ‘ 𝑅 ) Σ_g 𝑤 ) = ( ( 1^st ‘ 𝑎 ) · ( 2^nd ‘ 𝑎 ) ) )
387	169 2	mgpplusg	⊢ · = ( +_g ‘ ( mulGrp ‘ 𝑅 ) )
388	171	adantr	⊢ ( ( 𝜑 ∧ 𝑤 ∈ Word ( 𝐸 ∪ 𝐹 ) ) → ( mulGrp ‘ 𝑅 ) ∈ CMnd )
389	169	subrgsubm	⊢ ( 𝐸 ∈ ( SubRing ‘ 𝑅 ) → 𝐸 ∈ ( SubMnd ‘ ( mulGrp ‘ 𝑅 ) ) )
390	6 389	syl	⊢ ( 𝜑 → 𝐸 ∈ ( SubMnd ‘ ( mulGrp ‘ 𝑅 ) ) )
391	390	adantr	⊢ ( ( 𝜑 ∧ 𝑤 ∈ Word ( 𝐸 ∪ 𝐹 ) ) → 𝐸 ∈ ( SubMnd ‘ ( mulGrp ‘ 𝑅 ) ) )
392	169	subrgsubm	⊢ ( 𝐹 ∈ ( SubRing ‘ 𝑅 ) → 𝐹 ∈ ( SubMnd ‘ ( mulGrp ‘ 𝑅 ) ) )
393	7 392	syl	⊢ ( 𝜑 → 𝐹 ∈ ( SubMnd ‘ ( mulGrp ‘ 𝑅 ) ) )
394	393	adantr	⊢ ( ( 𝜑 ∧ 𝑤 ∈ Word ( 𝐸 ∪ 𝐹 ) ) → 𝐹 ∈ ( SubMnd ‘ ( mulGrp ‘ 𝑅 ) ) )
395		simpr	⊢ ( ( 𝜑 ∧ 𝑤 ∈ Word ( 𝐸 ∪ 𝐹 ) ) → 𝑤 ∈ Word ( 𝐸 ∪ 𝐹 ) )
396	387 388 391 394 395	gsumwun	⊢ ( ( 𝜑 ∧ 𝑤 ∈ Word ( 𝐸 ∪ 𝐹 ) ) → ∃ 𝑒 ∈ 𝐸 ∃ 𝑓 ∈ 𝐹 ( ( mulGrp ‘ 𝑅 ) Σ_g 𝑤 ) = ( 𝑒 · 𝑓 ) )
397	386 396	r19.29vva	⊢ ( ( 𝜑 ∧ 𝑤 ∈ Word ( 𝐸 ∪ 𝐹 ) ) → ∃ 𝑎 ∈ ( 𝐸 × 𝐹 ) ( ( mulGrp ‘ 𝑅 ) Σ_g 𝑤 ) = ( ( 1^st ‘ 𝑎 ) · ( 2^nd ‘ 𝑎 ) ) )
398	375 30 27 397	ac6mapd	⊢ ( 𝜑 → ∃ 𝑞 ∈ ( ( 𝐸 × 𝐹 ) ↑_m Word ( 𝐸 ∪ 𝐹 ) ) ∀ 𝑤 ∈ Word ( 𝐸 ∪ 𝐹 ) ( ( mulGrp ‘ 𝑅 ) Σ_g 𝑤 ) = ( ( 1^st ‘ ( 𝑞 ‘ 𝑤 ) ) · ( 2^nd ‘ ( 𝑞 ‘ 𝑤 ) ) ) )
399	371 398	r19.29a	⊢ ( 𝜑 → ∃ 𝑝 ∈ ( 𝐸 ↑_m 𝐹 ) ( 𝑝 finSupp 0 ∧ 𝑋 = ( 𝑅 Σ_g ( 𝑓 ∈ 𝐹 ↦ ( ( 𝑝 ‘ 𝑓 ) · 𝑓 ) ) ) ) )

Metamath Proof Explorer

Theorem elrgspnsubrunlem2

Proof