elrgspnsubrunlem2

	Ref	Expression
Hypotheses	elrgspnsubrun.b	$⊢ B = {Base}_{R}$
	elrgspnsubrun.t	$⊢ \underset{˙}{\cdot} = \cdot_{R}$
	elrgspnsubrun.z	$⊢ \underset{˙}{0} = 0_{R}$
	elrgspnsubrun.n	$⊢ N = RingSpan (R)$
	elrgspnsubrun.r	$⊢ φ \to R \in CRing$
	elrgspnsubrun.e	$⊢ φ \to E \in SubRing (R)$
	elrgspnsubrun.f	$⊢ φ \to F \in SubRing (R)$
	elrgspnsubrunlem2.x	$⊢ φ \to X \in B$
	elrgspnsubrunlem2.1	$⊢ φ \to G : Word (E \cup F) ⟶ ℤ$
	elrgspnsubrunlem2.2	$⊢ φ \to {finSupp}_{0} (G)$
	elrgspnsubrunlem2.3	$⊢ φ \to X = \underset{w \in Word (E \cup F)}{\sum_{R}} (G (w) \cdot_{R} (\sum_{{mulGrp}_{R}}, w))$
Assertion	elrgspnsubrunlem2	$⊢ φ \to \exists p \in (E^{F}) ({finSupp}_{\underset{˙}{0}} (p) \land X = \underset{f \in F}{\sum_{R}} (p (f) \underset{˙}{\cdot} f))$

Proof

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

Metamath Proof Explorer

Theorem elrgspnsubrunlem2

Proof