cyc3genpmlem

	Ref	Expression
Hypotheses	cyc3genpm.t	$⊢ C = M [{\|.\|}^{-1} [\{3\}]]$
	cyc3genpm.a	$⊢ A = pmEven (D)$
	cyc3genpm.s	$⊢ S = SymGrp (D)$
	cyc3genpm.n	$⊢ N = \|D\|$
	cyc3genpm.m	$⊢ M = toCyc (D)$
	cyc3genpmlem.t	$⊢ \underset{˙}{\cdot} = +_{S}$
	cyc3genpmlem.i	$⊢ φ \to I \in D$
	cyc3genpmlem.j	$⊢ φ \to J \in D$
	cyc3genpmlem.k	$⊢ φ \to K \in D$
	cyc3genpmlem.l	$⊢ φ \to L \in D$
	cyc3genpmlem.e	$⊢ φ \to E = M (⟨“ I J ”⟩)$
	cyc3genpmlem.f	$⊢ φ \to F = M (⟨“ K L ”⟩)$
	cyc3genpmlem.d	$⊢ φ \to D \in V$
	cyc3genpmlem.1	$⊢ φ \to I \neq J$
	cyc3genpmlem.2	$⊢ φ \to K \neq L$
Assertion	cyc3genpmlem	$⊢ φ \to \exists c \in Word C E \underset{˙}{\cdot} F = \sum_{S} c$

Proof

Step	Hyp	Ref	Expression
1		cyc3genpm.t	$⊢ C = M [{\|.\|}^{-1} [\{3\}]]$
2		cyc3genpm.a	$⊢ A = pmEven (D)$
3		cyc3genpm.s	$⊢ S = SymGrp (D)$
4		cyc3genpm.n	$⊢ N = \|D\|$
5		cyc3genpm.m	$⊢ M = toCyc (D)$
6		cyc3genpmlem.t	$⊢ \underset{˙}{\cdot} = +_{S}$
7		cyc3genpmlem.i	$⊢ φ \to I \in D$
8		cyc3genpmlem.j	$⊢ φ \to J \in D$
9		cyc3genpmlem.k	$⊢ φ \to K \in D$
10		cyc3genpmlem.l	$⊢ φ \to L \in D$
11		cyc3genpmlem.e	$⊢ φ \to E = M (⟨“ I J ”⟩)$
12		cyc3genpmlem.f	$⊢ φ \to F = M (⟨“ K L ”⟩)$
13		cyc3genpmlem.d	$⊢ φ \to D \in V$
14		cyc3genpmlem.1	$⊢ φ \to I \neq J$
15		cyc3genpmlem.2	$⊢ φ \to K \neq L$
16		wrd0	$⊢ \emptyset \in Word C$
17	16	a1i	$⊢ ((φ \land I \in \{K, L\}) \land J \in \{K, L\}) \to \emptyset \in Word C$
18		simpr	$⊢ (((φ \land I \in \{K, L\}) \land J \in \{K, L\}) \land c = \emptyset) \to c = \emptyset$
19	18	oveq2d	$⊢ (((φ \land I \in \{K, L\}) \land J \in \{K, L\}) \land c = \emptyset) \to \sum_{S} c = \sum_{S} \emptyset$
20	19	eqeq2d	$⊢ (((φ \land I \in \{K, L\}) \land J \in \{K, L\}) \land c = \emptyset) \to (E \underset{˙}{\cdot} F = \sum_{S} c \leftrightarrow E \underset{˙}{\cdot} F = \sum_{S} \emptyset)$
21	5 13 7 8 14 3	cycpm2cl	$⊢ φ \to M (⟨“ I J ”⟩) \in {Base}_{S}$
22	11 21	eqeltrd	$⊢ φ \to E \in {Base}_{S}$
23	5 13 9 10 15 3	cycpm2cl	$⊢ φ \to M (⟨“ K L ”⟩) \in {Base}_{S}$
24	12 23	eqeltrd	$⊢ φ \to F \in {Base}_{S}$
25		eqid	$⊢ {Base}_{S} = {Base}_{S}$
26	3 25 6	symgov	$⊢ (E \in {Base}_{S} \land F \in {Base}_{S}) \to E \underset{˙}{\cdot} F = E \circ F$
27	22 24 26	syl2anc	$⊢ φ \to E \underset{˙}{\cdot} F = E \circ F$
28	27	ad2antrr	$⊢ ((φ \land I \in \{K, L\}) \land J \in \{K, L\}) \to E \underset{˙}{\cdot} F = E \circ F$
29	11	ad2antrr	$⊢ ((φ \land I \in \{K, L\}) \land J \in \{K, L\}) \to E = M (⟨“ I J ”⟩)$
30		eqid	$⊢ pmTrsp (D) = pmTrsp (D)$
31	5 13 7 8 14 30	cycpm2tr	$⊢ φ \to M (⟨“ I J ”⟩) = pmTrsp (D) (\{I, J\})$
32	31	ad2antrr	$⊢ ((φ \land I \in \{K, L\}) \land J \in \{K, L\}) \to M (⟨“ I J ”⟩) = pmTrsp (D) (\{I, J\})$
33	29 32	eqtrd	$⊢ ((φ \land I \in \{K, L\}) \land J \in \{K, L\}) \to E = pmTrsp (D) (\{I, J\})$
34	5 13 9 10 15 30	cycpm2tr	$⊢ φ \to M (⟨“ K L ”⟩) = pmTrsp (D) (\{K, L\})$
35	34	ad2antrr	$⊢ ((φ \land I \in \{K, L\}) \land J \in \{K, L\}) \to M (⟨“ K L ”⟩) = pmTrsp (D) (\{K, L\})$
36	12	ad2antrr	$⊢ ((φ \land I \in \{K, L\}) \land J \in \{K, L\}) \to F = M (⟨“ K L ”⟩)$
37	7	ad2antrr	$⊢ ((φ \land I \in \{K, L\}) \land J \in \{K, L\}) \to I \in D$
38	8	ad2antrr	$⊢ ((φ \land I \in \{K, L\}) \land J \in \{K, L\}) \to J \in D$
39	14	ad2antrr	$⊢ ((φ \land I \in \{K, L\}) \land J \in \{K, L\}) \to I \neq J$
40		simplr	$⊢ ((φ \land I \in \{K, L\}) \land J \in \{K, L\}) \to I \in \{K, L\}$
41		simpr	$⊢ ((φ \land I \in \{K, L\}) \land J \in \{K, L\}) \to J \in \{K, L\}$
42	40 41	prssd	$⊢ ((φ \land I \in \{K, L\}) \land J \in \{K, L\}) \to \{I, J\} \subseteq \{K, L\}$
43		ssprsseq	$⊢ (I \in D \land J \in D \land I \neq J) \to (\{I, J\} \subseteq \{K, L\} \leftrightarrow \{I, J\} = \{K, L\})$
44	43	biimpa	$⊢ ((I \in D \land J \in D \land I \neq J) \land \{I, J\} \subseteq \{K, L\}) \to \{I, J\} = \{K, L\}$
45	37 38 39 42 44	syl31anc	$⊢ ((φ \land I \in \{K, L\}) \land J \in \{K, L\}) \to \{I, J\} = \{K, L\}$
46	45	fveq2d	$⊢ ((φ \land I \in \{K, L\}) \land J \in \{K, L\}) \to pmTrsp (D) (\{I, J\}) = pmTrsp (D) (\{K, L\})$
47	35 36 46	3eqtr4d	$⊢ ((φ \land I \in \{K, L\}) \land J \in \{K, L\}) \to F = pmTrsp (D) (\{I, J\})$
48	33 47	coeq12d	$⊢ ((φ \land I \in \{K, L\}) \land J \in \{K, L\}) \to E \circ F = pmTrsp (D) (\{I, J\}) \circ pmTrsp (D) (\{I, J\})$
49	13	ad2antrr	$⊢ ((φ \land I \in \{K, L\}) \land J \in \{K, L\}) \to D \in V$
50	37 38	prssd	$⊢ ((φ \land I \in \{K, L\}) \land J \in \{K, L\}) \to \{I, J\} \subseteq D$
51		pr2nelem	$⊢ (I \in D \land J \in D \land I \neq J) \to \{I, J\} \approx 2_{𝑜}$
52	37 38 39 51	syl3anc	$⊢ ((φ \land I \in \{K, L\}) \land J \in \{K, L\}) \to \{I, J\} \approx 2_{𝑜}$
53		eqid	$⊢ ran pmTrsp (D) = ran pmTrsp (D)$
54	30 53	pmtrrn	$⊢ (D \in V \land \{I, J\} \subseteq D \land \{I, J\} \approx 2_{𝑜}) \to pmTrsp (D) (\{I, J\}) \in ran pmTrsp (D)$
55	49 50 52 54	syl3anc	$⊢ ((φ \land I \in \{K, L\}) \land J \in \{K, L\}) \to pmTrsp (D) (\{I, J\}) \in ran pmTrsp (D)$
56	30 53	pmtrfinv	$⊢ pmTrsp (D) (\{I, J\}) \in ran pmTrsp (D) \to pmTrsp (D) (\{I, J\}) \circ pmTrsp (D) (\{I, J\}) = {I ↾}_{D}$
57	55 56	syl	$⊢ ((φ \land I \in \{K, L\}) \land J \in \{K, L\}) \to pmTrsp (D) (\{I, J\}) \circ pmTrsp (D) (\{I, J\}) = {I ↾}_{D}$
58	28 48 57	3eqtrd	$⊢ ((φ \land I \in \{K, L\}) \land J \in \{K, L\}) \to E \underset{˙}{\cdot} F = {I ↾}_{D}$
59	3	symgid	$⊢ D \in V \to {I ↾}_{D} = 0_{S}$
60	49 59	syl	$⊢ ((φ \land I \in \{K, L\}) \land J \in \{K, L\}) \to {I ↾}_{D} = 0_{S}$
61		eqid	$⊢ 0_{S} = 0_{S}$
62	61	gsum0	$⊢ \sum_{S} \emptyset = 0_{S}$
63	60 62	eqtr4di	$⊢ ((φ \land I \in \{K, L\}) \land J \in \{K, L\}) \to {I ↾}_{D} = \sum_{S} \emptyset$
64	58 63	eqtrd	$⊢ ((φ \land I \in \{K, L\}) \land J \in \{K, L\}) \to E \underset{˙}{\cdot} F = \sum_{S} \emptyset$
65	17 20 64	rspcedvd	$⊢ ((φ \land I \in \{K, L\}) \land J \in \{K, L\}) \to \exists c \in Word C E \underset{˙}{\cdot} F = \sum_{S} c$
66	13	ad2antrr	$⊢ ((φ \land I \in \{K, L\}) \land \neg J \in \{K, L\}) \to D \in V$
67	7	ad2antrr	$⊢ ((φ \land I \in \{K, L\}) \land \neg J \in \{K, L\}) \to I \in D$
68	9 10	prssd	$⊢ φ \to \{K, L\} \subseteq D$
69	68	ad2antrr	$⊢ ((φ \land I \in \{K, L\}) \land \neg J \in \{K, L\}) \to \{K, L\} \subseteq D$
70		simplr	$⊢ ((φ \land I \in \{K, L\}) \land \neg J \in \{K, L\}) \to I \in \{K, L\}$
71		pr2nelem	$⊢ (K \in D \land L \in D \land K \neq L) \to \{K, L\} \approx 2_{𝑜}$
72	9 10 15 71	syl3anc	$⊢ φ \to \{K, L\} \approx 2_{𝑜}$
73	72	ad2antrr	$⊢ ((φ \land I \in \{K, L\}) \land \neg J \in \{K, L\}) \to \{K, L\} \approx 2_{𝑜}$
74		unidifsnel	$⊢ (I \in \{K, L\} \land \{K, L\} \approx 2_{𝑜}) \to ⋃ (\{K, L\} ∖ \{I\}) \in \{K, L\}$
75	70 73 74	syl2anc	$⊢ ((φ \land I \in \{K, L\}) \land \neg J \in \{K, L\}) \to ⋃ (\{K, L\} ∖ \{I\}) \in \{K, L\}$
76	69 75	sseldd	$⊢ ((φ \land I \in \{K, L\}) \land \neg J \in \{K, L\}) \to ⋃ (\{K, L\} ∖ \{I\}) \in D$
77	8	ad2antrr	$⊢ ((φ \land I \in \{K, L\}) \land \neg J \in \{K, L\}) \to J \in D$
78		unidifsnne	$⊢ (I \in \{K, L\} \land \{K, L\} \approx 2_{𝑜}) \to ⋃ (\{K, L\} ∖ \{I\}) \neq I$
79	70 73 78	syl2anc	$⊢ ((φ \land I \in \{K, L\}) \land \neg J \in \{K, L\}) \to ⋃ (\{K, L\} ∖ \{I\}) \neq I$
80	79	necomd	$⊢ ((φ \land I \in \{K, L\}) \land \neg J \in \{K, L\}) \to I \neq ⋃ (\{K, L\} ∖ \{I\})$
81		nelne2	$⊢ (⋃ (\{K, L\} ∖ \{I\}) \in \{K, L\} \land \neg J \in \{K, L\}) \to ⋃ (\{K, L\} ∖ \{I\}) \neq J$
82	75 81	sylancom	$⊢ ((φ \land I \in \{K, L\}) \land \neg J \in \{K, L\}) \to ⋃ (\{K, L\} ∖ \{I\}) \neq J$
83	14	necomd	$⊢ φ \to J \neq I$
84	83	ad2antrr	$⊢ ((φ \land I \in \{K, L\}) \land \neg J \in \{K, L\}) \to J \neq I$
85	5 3 66 67 76 77 80 82 84	cycpm3cl2	$⊢ ((φ \land I \in \{K, L\}) \land \neg J \in \{K, L\}) \to M (⟨“ I ⋃ (\{K, L\} ∖ \{I\}) J ”⟩) \in M [{\|.\|}^{-1} [\{3\}]]$
86	85 1	eleqtrrdi	$⊢ ((φ \land I \in \{K, L\}) \land \neg J \in \{K, L\}) \to M (⟨“ I ⋃ (\{K, L\} ∖ \{I\}) J ”⟩) \in C$
87	86	s1cld	$⊢ ((φ \land I \in \{K, L\}) \land \neg J \in \{K, L\}) \to ⟨“ M (⟨“ I ⋃ (\{K, L\} ∖ \{I\}) J ”⟩) ”⟩ \in Word C$
88		simpr	$⊢ (((φ \land I \in \{K, L\}) \land \neg J \in \{K, L\}) \land c = ⟨“ M (⟨“ I ⋃ (\{K, L\} ∖ \{I\}) J ”⟩) ”⟩) \to c = ⟨“ M (⟨“ I ⋃ (\{K, L\} ∖ \{I\}) J ”⟩) ”⟩$
89	88	oveq2d	$⊢ (((φ \land I \in \{K, L\}) \land \neg J \in \{K, L\}) \land c = ⟨“ M (⟨“ I ⋃ (\{K, L\} ∖ \{I\}) J ”⟩) ”⟩) \to \sum_{S} c = \sum_{S} ⟨“ M (⟨“ I ⋃ (\{K, L\} ∖ \{I\}) J ”⟩) ”⟩$
90	89	eqeq2d	$⊢ (((φ \land I \in \{K, L\}) \land \neg J \in \{K, L\}) \land c = ⟨“ M (⟨“ I ⋃ (\{K, L\} ∖ \{I\}) J ”⟩) ”⟩) \to (E \underset{˙}{\cdot} F = \sum_{S} c \leftrightarrow E \underset{˙}{\cdot} F = \sum_{S} ⟨“ M (⟨“ I ⋃ (\{K, L\} ∖ \{I\}) J ”⟩) ”⟩)$
91	5 3 66 67 76 77 80 82 84 6	cyc3co2	$⊢ ((φ \land I \in \{K, L\}) \land \neg J \in \{K, L\}) \to M (⟨“ I ⋃ (\{K, L\} ∖ \{I\}) J ”⟩) = M (⟨“ I J ”⟩) \underset{˙}{\cdot} M (⟨“ I ⋃ (\{K, L\} ∖ \{I\}) ”⟩)$
92	5 3 66 67 76 77 80 82 84	cycpm3cl	$⊢ ((φ \land I \in \{K, L\}) \land \neg J \in \{K, L\}) \to M (⟨“ I ⋃ (\{K, L\} ∖ \{I\}) J ”⟩) \in {Base}_{S}$
93	25	gsumws1	$⊢ M (⟨“ I ⋃ (\{K, L\} ∖ \{I\}) J ”⟩) \in {Base}_{S} \to \sum_{S} ⟨“ M (⟨“ I ⋃ (\{K, L\} ∖ \{I\}) J ”⟩) ”⟩ = M (⟨“ I ⋃ (\{K, L\} ∖ \{I\}) J ”⟩)$
94	92 93	syl	$⊢ ((φ \land I \in \{K, L\}) \land \neg J \in \{K, L\}) \to \sum_{S} ⟨“ M (⟨“ I ⋃ (\{K, L\} ∖ \{I\}) J ”⟩) ”⟩ = M (⟨“ I ⋃ (\{K, L\} ∖ \{I\}) J ”⟩)$
95	11	ad2antrr	$⊢ ((φ \land I \in \{K, L\}) \land \neg J \in \{K, L\}) \to E = M (⟨“ I J ”⟩)$
96		en2eleq	$⊢ (I \in \{K, L\} \land \{K, L\} \approx 2_{𝑜}) \to \{K, L\} = \{I, ⋃ (\{K, L\} ∖ \{I\})\}$
97	70 73 96	syl2anc	$⊢ ((φ \land I \in \{K, L\}) \land \neg J \in \{K, L\}) \to \{K, L\} = \{I, ⋃ (\{K, L\} ∖ \{I\})\}$
98	97	fveq2d	$⊢ ((φ \land I \in \{K, L\}) \land \neg J \in \{K, L\}) \to pmTrsp (D) (\{K, L\}) = pmTrsp (D) (\{I, ⋃ (\{K, L\} ∖ \{I\})\})$
99	12 34	eqtrd	$⊢ φ \to F = pmTrsp (D) (\{K, L\})$
100	99	ad2antrr	$⊢ ((φ \land I \in \{K, L\}) \land \neg J \in \{K, L\}) \to F = pmTrsp (D) (\{K, L\})$
101	5 66 67 76 80 30	cycpm2tr	$⊢ ((φ \land I \in \{K, L\}) \land \neg J \in \{K, L\}) \to M (⟨“ I ⋃ (\{K, L\} ∖ \{I\}) ”⟩) = pmTrsp (D) (\{I, ⋃ (\{K, L\} ∖ \{I\})\})$
102	98 100 101	3eqtr4d	$⊢ ((φ \land I \in \{K, L\}) \land \neg J \in \{K, L\}) \to F = M (⟨“ I ⋃ (\{K, L\} ∖ \{I\}) ”⟩)$
103	95 102	oveq12d	$⊢ ((φ \land I \in \{K, L\}) \land \neg J \in \{K, L\}) \to E \underset{˙}{\cdot} F = M (⟨“ I J ”⟩) \underset{˙}{\cdot} M (⟨“ I ⋃ (\{K, L\} ∖ \{I\}) ”⟩)$
104	91 94 103	3eqtr4rd	$⊢ ((φ \land I \in \{K, L\}) \land \neg J \in \{K, L\}) \to E \underset{˙}{\cdot} F = \sum_{S} ⟨“ M (⟨“ I ⋃ (\{K, L\} ∖ \{I\}) J ”⟩) ”⟩$
105	87 90 104	rspcedvd	$⊢ ((φ \land I \in \{K, L\}) \land \neg J \in \{K, L\}) \to \exists c \in Word C E \underset{˙}{\cdot} F = \sum_{S} c$
106	65 105	pm2.61dan	$⊢ (φ \land I \in \{K, L\}) \to \exists c \in Word C E \underset{˙}{\cdot} F = \sum_{S} c$
107	13	ad2antrr	$⊢ ((φ \land \neg I \in \{K, L\}) \land J \in \{K, L\}) \to D \in V$
108	8	ad2antrr	$⊢ ((φ \land \neg I \in \{K, L\}) \land J \in \{K, L\}) \to J \in D$
109	68	ad2antrr	$⊢ ((φ \land \neg I \in \{K, L\}) \land J \in \{K, L\}) \to \{K, L\} \subseteq D$
110		simpr	$⊢ ((φ \land \neg I \in \{K, L\}) \land J \in \{K, L\}) \to J \in \{K, L\}$
111	72	ad2antrr	$⊢ ((φ \land \neg I \in \{K, L\}) \land J \in \{K, L\}) \to \{K, L\} \approx 2_{𝑜}$
112		unidifsnel	$⊢ (J \in \{K, L\} \land \{K, L\} \approx 2_{𝑜}) \to ⋃ (\{K, L\} ∖ \{J\}) \in \{K, L\}$
113	110 111 112	syl2anc	$⊢ ((φ \land \neg I \in \{K, L\}) \land J \in \{K, L\}) \to ⋃ (\{K, L\} ∖ \{J\}) \in \{K, L\}$
114	109 113	sseldd	$⊢ ((φ \land \neg I \in \{K, L\}) \land J \in \{K, L\}) \to ⋃ (\{K, L\} ∖ \{J\}) \in D$
115	7	ad2antrr	$⊢ ((φ \land \neg I \in \{K, L\}) \land J \in \{K, L\}) \to I \in D$
116		unidifsnne	$⊢ (J \in \{K, L\} \land \{K, L\} \approx 2_{𝑜}) \to ⋃ (\{K, L\} ∖ \{J\}) \neq J$
117	110 111 116	syl2anc	$⊢ ((φ \land \neg I \in \{K, L\}) \land J \in \{K, L\}) \to ⋃ (\{K, L\} ∖ \{J\}) \neq J$
118	117	necomd	$⊢ ((φ \land \neg I \in \{K, L\}) \land J \in \{K, L\}) \to J \neq ⋃ (\{K, L\} ∖ \{J\})$
119		simplr	$⊢ ((φ \land \neg I \in \{K, L\}) \land J \in \{K, L\}) \to \neg I \in \{K, L\}$
120		nelne2	$⊢ (⋃ (\{K, L\} ∖ \{J\}) \in \{K, L\} \land \neg I \in \{K, L\}) \to ⋃ (\{K, L\} ∖ \{J\}) \neq I$
121	113 119 120	syl2anc	$⊢ ((φ \land \neg I \in \{K, L\}) \land J \in \{K, L\}) \to ⋃ (\{K, L\} ∖ \{J\}) \neq I$
122	14	ad2antrr	$⊢ ((φ \land \neg I \in \{K, L\}) \land J \in \{K, L\}) \to I \neq J$
123	5 3 107 108 114 115 118 121 122	cycpm3cl2	$⊢ ((φ \land \neg I \in \{K, L\}) \land J \in \{K, L\}) \to M (⟨“ J ⋃ (\{K, L\} ∖ \{J\}) I ”⟩) \in M [{\|.\|}^{-1} [\{3\}]]$
124	123 1	eleqtrrdi	$⊢ ((φ \land \neg I \in \{K, L\}) \land J \in \{K, L\}) \to M (⟨“ J ⋃ (\{K, L\} ∖ \{J\}) I ”⟩) \in C$
125	124	s1cld	$⊢ ((φ \land \neg I \in \{K, L\}) \land J \in \{K, L\}) \to ⟨“ M (⟨“ J ⋃ (\{K, L\} ∖ \{J\}) I ”⟩) ”⟩ \in Word C$
126		simpr	$⊢ (((φ \land \neg I \in \{K, L\}) \land J \in \{K, L\}) \land c = ⟨“ M (⟨“ J ⋃ (\{K, L\} ∖ \{J\}) I ”⟩) ”⟩) \to c = ⟨“ M (⟨“ J ⋃ (\{K, L\} ∖ \{J\}) I ”⟩) ”⟩$
127	126	oveq2d	$⊢ (((φ \land \neg I \in \{K, L\}) \land J \in \{K, L\}) \land c = ⟨“ M (⟨“ J ⋃ (\{K, L\} ∖ \{J\}) I ”⟩) ”⟩) \to \sum_{S} c = \sum_{S} ⟨“ M (⟨“ J ⋃ (\{K, L\} ∖ \{J\}) I ”⟩) ”⟩$
128	127	eqeq2d	$⊢ (((φ \land \neg I \in \{K, L\}) \land J \in \{K, L\}) \land c = ⟨“ M (⟨“ J ⋃ (\{K, L\} ∖ \{J\}) I ”⟩) ”⟩) \to (E \underset{˙}{\cdot} F = \sum_{S} c \leftrightarrow E \underset{˙}{\cdot} F = \sum_{S} ⟨“ M (⟨“ J ⋃ (\{K, L\} ∖ \{J\}) I ”⟩) ”⟩)$
129	5 3 107 108 114 115 118 121 122 6	cyc3co2	$⊢ ((φ \land \neg I \in \{K, L\}) \land J \in \{K, L\}) \to M (⟨“ J ⋃ (\{K, L\} ∖ \{J\}) I ”⟩) = M (⟨“ J I ”⟩) \underset{˙}{\cdot} M (⟨“ J ⋃ (\{K, L\} ∖ \{J\}) ”⟩)$
130	5 3 107 108 114 115 118 121 122	cycpm3cl	$⊢ ((φ \land \neg I \in \{K, L\}) \land J \in \{K, L\}) \to M (⟨“ J ⋃ (\{K, L\} ∖ \{J\}) I ”⟩) \in {Base}_{S}$
131	25	gsumws1	$⊢ M (⟨“ J ⋃ (\{K, L\} ∖ \{J\}) I ”⟩) \in {Base}_{S} \to \sum_{S} ⟨“ M (⟨“ J ⋃ (\{K, L\} ∖ \{J\}) I ”⟩) ”⟩ = M (⟨“ J ⋃ (\{K, L\} ∖ \{J\}) I ”⟩)$
132	130 131	syl	$⊢ ((φ \land \neg I \in \{K, L\}) \land J \in \{K, L\}) \to \sum_{S} ⟨“ M (⟨“ J ⋃ (\{K, L\} ∖ \{J\}) I ”⟩) ”⟩ = M (⟨“ J ⋃ (\{K, L\} ∖ \{J\}) I ”⟩)$
133		prcom	$⊢ \{I, J\} = \{J, I\}$
134	133	fveq2i	$⊢ pmTrsp (D) (\{I, J\}) = pmTrsp (D) (\{J, I\})$
135	5 13 8 7 83 30	cycpm2tr	$⊢ φ \to M (⟨“ J I ”⟩) = pmTrsp (D) (\{J, I\})$
136	134 31 135	3eqtr4a	$⊢ φ \to M (⟨“ I J ”⟩) = M (⟨“ J I ”⟩)$
137	11 136	eqtrd	$⊢ φ \to E = M (⟨“ J I ”⟩)$
138	137	ad2antrr	$⊢ ((φ \land \neg I \in \{K, L\}) \land J \in \{K, L\}) \to E = M (⟨“ J I ”⟩)$
139		en2eleq	$⊢ (J \in \{K, L\} \land \{K, L\} \approx 2_{𝑜}) \to \{K, L\} = \{J, ⋃ (\{K, L\} ∖ \{J\})\}$
140	110 111 139	syl2anc	$⊢ ((φ \land \neg I \in \{K, L\}) \land J \in \{K, L\}) \to \{K, L\} = \{J, ⋃ (\{K, L\} ∖ \{J\})\}$
141	140	fveq2d	$⊢ ((φ \land \neg I \in \{K, L\}) \land J \in \{K, L\}) \to pmTrsp (D) (\{K, L\}) = pmTrsp (D) (\{J, ⋃ (\{K, L\} ∖ \{J\})\})$
142	99	ad2antrr	$⊢ ((φ \land \neg I \in \{K, L\}) \land J \in \{K, L\}) \to F = pmTrsp (D) (\{K, L\})$
143	5 107 108 114 118 30	cycpm2tr	$⊢ ((φ \land \neg I \in \{K, L\}) \land J \in \{K, L\}) \to M (⟨“ J ⋃ (\{K, L\} ∖ \{J\}) ”⟩) = pmTrsp (D) (\{J, ⋃ (\{K, L\} ∖ \{J\})\})$
144	141 142 143	3eqtr4d	$⊢ ((φ \land \neg I \in \{K, L\}) \land J \in \{K, L\}) \to F = M (⟨“ J ⋃ (\{K, L\} ∖ \{J\}) ”⟩)$
145	138 144	oveq12d	$⊢ ((φ \land \neg I \in \{K, L\}) \land J \in \{K, L\}) \to E \underset{˙}{\cdot} F = M (⟨“ J I ”⟩) \underset{˙}{\cdot} M (⟨“ J ⋃ (\{K, L\} ∖ \{J\}) ”⟩)$
146	129 132 145	3eqtr4rd	$⊢ ((φ \land \neg I \in \{K, L\}) \land J \in \{K, L\}) \to E \underset{˙}{\cdot} F = \sum_{S} ⟨“ M (⟨“ J ⋃ (\{K, L\} ∖ \{J\}) I ”⟩) ”⟩$
147	125 128 146	rspcedvd	$⊢ ((φ \land \neg I \in \{K, L\}) \land J \in \{K, L\}) \to \exists c \in Word C E \underset{˙}{\cdot} F = \sum_{S} c$
148	13	ad2antrr	$⊢ ((φ \land \neg I \in \{K, L\}) \land \neg J \in \{K, L\}) \to D \in V$
149	8	ad2antrr	$⊢ ((φ \land \neg I \in \{K, L\}) \land \neg J \in \{K, L\}) \to J \in D$
150	9	ad2antrr	$⊢ ((φ \land \neg I \in \{K, L\}) \land \neg J \in \{K, L\}) \to K \in D$
151	7	ad2antrr	$⊢ ((φ \land \neg I \in \{K, L\}) \land \neg J \in \{K, L\}) \to I \in D$
152		simpr	$⊢ ((φ \land \neg I \in \{K, L\}) \land \neg J \in \{K, L\}) \to \neg J \in \{K, L\}$
153	149 152	nelpr1	$⊢ ((φ \land \neg I \in \{K, L\}) \land \neg J \in \{K, L\}) \to J \neq K$
154		prid1g	$⊢ K \in D \to K \in \{K, L\}$
155	9 154	syl	$⊢ φ \to K \in \{K, L\}$
156	155	ad2antrr	$⊢ ((φ \land \neg I \in \{K, L\}) \land \neg J \in \{K, L\}) \to K \in \{K, L\}$
157		simplr	$⊢ ((φ \land \neg I \in \{K, L\}) \land \neg J \in \{K, L\}) \to \neg I \in \{K, L\}$
158		nelne2	$⊢ (K \in \{K, L\} \land \neg I \in \{K, L\}) \to K \neq I$
159	156 157 158	syl2anc	$⊢ ((φ \land \neg I \in \{K, L\}) \land \neg J \in \{K, L\}) \to K \neq I$
160	14	ad2antrr	$⊢ ((φ \land \neg I \in \{K, L\}) \land \neg J \in \{K, L\}) \to I \neq J$
161	5 3 148 149 150 151 153 159 160	cycpm3cl2	$⊢ ((φ \land \neg I \in \{K, L\}) \land \neg J \in \{K, L\}) \to M (⟨“ J K I ”⟩) \in M [{\|.\|}^{-1} [\{3\}]]$
162	161 1	eleqtrrdi	$⊢ ((φ \land \neg I \in \{K, L\}) \land \neg J \in \{K, L\}) \to M (⟨“ J K I ”⟩) \in C$
163	10	ad2antrr	$⊢ ((φ \land \neg I \in \{K, L\}) \land \neg J \in \{K, L\}) \to L \in D$
164	15	ad2antrr	$⊢ ((φ \land \neg I \in \{K, L\}) \land \neg J \in \{K, L\}) \to K \neq L$
165		prid2g	$⊢ L \in D \to L \in \{K, L\}$
166	163 165	syl	$⊢ ((φ \land \neg I \in \{K, L\}) \land \neg J \in \{K, L\}) \to L \in \{K, L\}$
167		nelne2	$⊢ (L \in \{K, L\} \land \neg J \in \{K, L\}) \to L \neq J$
168	166 167	sylancom	$⊢ ((φ \land \neg I \in \{K, L\}) \land \neg J \in \{K, L\}) \to L \neq J$
169	5 3 148 150 163 149 164 168 153	cycpm3cl2	$⊢ ((φ \land \neg I \in \{K, L\}) \land \neg J \in \{K, L\}) \to M (⟨“ K L J ”⟩) \in M [{\|.\|}^{-1} [\{3\}]]$
170	169 1	eleqtrrdi	$⊢ ((φ \land \neg I \in \{K, L\}) \land \neg J \in \{K, L\}) \to M (⟨“ K L J ”⟩) \in C$
171	162 170	s2cld	$⊢ ((φ \land \neg I \in \{K, L\}) \land \neg J \in \{K, L\}) \to ⟨“ M (⟨“ J K I ”⟩) M (⟨“ K L J ”⟩) ”⟩ \in Word C$
172		simpr	$⊢ (((φ \land \neg I \in \{K, L\}) \land \neg J \in \{K, L\}) \land c = ⟨“ M (⟨“ J K I ”⟩) M (⟨“ K L J ”⟩) ”⟩) \to c = ⟨“ M (⟨“ J K I ”⟩) M (⟨“ K L J ”⟩) ”⟩$
173	172	oveq2d	$⊢ (((φ \land \neg I \in \{K, L\}) \land \neg J \in \{K, L\}) \land c = ⟨“ M (⟨“ J K I ”⟩) M (⟨“ K L J ”⟩) ”⟩) \to \sum_{S} c = \sum_{S} ⟨“ M (⟨“ J K I ”⟩) M (⟨“ K L J ”⟩) ”⟩$
174	173	eqeq2d	$⊢ (((φ \land \neg I \in \{K, L\}) \land \neg J \in \{K, L\}) \land c = ⟨“ M (⟨“ J K I ”⟩) M (⟨“ K L J ”⟩) ”⟩) \to (E \underset{˙}{\cdot} F = \sum_{S} c \leftrightarrow E \underset{˙}{\cdot} F = \sum_{S} ⟨“ M (⟨“ J K I ”⟩) M (⟨“ K L J ”⟩) ”⟩)$
175	148 59	syl	$⊢ ((φ \land \neg I \in \{K, L\}) \land \neg J \in \{K, L\}) \to {I ↾}_{D} = 0_{S}$
176	175	oveq1d	$⊢ ((φ \land \neg I \in \{K, L\}) \land \neg J \in \{K, L\}) \to ({I ↾}_{D}) \underset{˙}{\cdot} M (⟨“ K L ”⟩) = 0_{S} \underset{˙}{\cdot} M (⟨“ K L ”⟩)$
177	3	symggrp	$⊢ D \in V \to S \in Grp$
178	13 177	syl	$⊢ φ \to S \in Grp$
179	178	ad2antrr	$⊢ ((φ \land \neg I \in \{K, L\}) \land \neg J \in \{K, L\}) \to S \in Grp$
180	23	ad2antrr	$⊢ ((φ \land \neg I \in \{K, L\}) \land \neg J \in \{K, L\}) \to M (⟨“ K L ”⟩) \in {Base}_{S}$
181	25 6 61	grplid	$⊢ (S \in Grp \land M (⟨“ K L ”⟩) \in {Base}_{S}) \to 0_{S} \underset{˙}{\cdot} M (⟨“ K L ”⟩) = M (⟨“ K L ”⟩)$
182	179 180 181	syl2anc	$⊢ ((φ \land \neg I \in \{K, L\}) \land \neg J \in \{K, L\}) \to 0_{S} \underset{˙}{\cdot} M (⟨“ K L ”⟩) = M (⟨“ K L ”⟩)$
183	176 182	eqtrd	$⊢ ((φ \land \neg I \in \{K, L\}) \land \neg J \in \{K, L\}) \to ({I ↾}_{D}) \underset{˙}{\cdot} M (⟨“ K L ”⟩) = M (⟨“ K L ”⟩)$
184	183	oveq2d	$⊢ ((φ \land \neg I \in \{K, L\}) \land \neg J \in \{K, L\}) \to M (⟨“ I J ”⟩) \underset{˙}{\cdot} (({I ↾}_{D}) \underset{˙}{\cdot} M (⟨“ K L ”⟩)) = M (⟨“ I J ”⟩) \underset{˙}{\cdot} M (⟨“ K L ”⟩)$
185	21	ad2antrr	$⊢ ((φ \land \neg I \in \{K, L\}) \land \neg J \in \{K, L\}) \to M (⟨“ I J ”⟩) \in {Base}_{S}$
186	5 148 149 150 153 30	cycpm2tr	$⊢ ((φ \land \neg I \in \{K, L\}) \land \neg J \in \{K, L\}) \to M (⟨“ J K ”⟩) = pmTrsp (D) (\{J, K\})$
187	53 3 25	symgtrf	$⊢ ran pmTrsp (D) \subseteq {Base}_{S}$
188	8 9	prssd	$⊢ φ \to \{J, K\} \subseteq D$
189	188	ad2antrr	$⊢ ((φ \land \neg I \in \{K, L\}) \land \neg J \in \{K, L\}) \to \{J, K\} \subseteq D$
190		pr2nelem	$⊢ (J \in D \land K \in D \land J \neq K) \to \{J, K\} \approx 2_{𝑜}$
191	149 150 153 190	syl3anc	$⊢ ((φ \land \neg I \in \{K, L\}) \land \neg J \in \{K, L\}) \to \{J, K\} \approx 2_{𝑜}$
192	30 53	pmtrrn	$⊢ (D \in V \land \{J, K\} \subseteq D \land \{J, K\} \approx 2_{𝑜}) \to pmTrsp (D) (\{J, K\}) \in ran pmTrsp (D)$
193	148 189 191 192	syl3anc	$⊢ ((φ \land \neg I \in \{K, L\}) \land \neg J \in \{K, L\}) \to pmTrsp (D) (\{J, K\}) \in ran pmTrsp (D)$
194	187 193	sselid	$⊢ ((φ \land \neg I \in \{K, L\}) \land \neg J \in \{K, L\}) \to pmTrsp (D) (\{J, K\}) \in {Base}_{S}$
195	186 194	eqeltrd	$⊢ ((φ \land \neg I \in \{K, L\}) \land \neg J \in \{K, L\}) \to M (⟨“ J K ”⟩) \in {Base}_{S}$
196	153	necomd	$⊢ ((φ \land \neg I \in \{K, L\}) \land \neg J \in \{K, L\}) \to K \neq J$
197	5 148 150 149 196 30	cycpm2tr	$⊢ ((φ \land \neg I \in \{K, L\}) \land \neg J \in \{K, L\}) \to M (⟨“ K J ”⟩) = pmTrsp (D) (\{K, J\})$
198		prcom	$⊢ \{J, K\} = \{K, J\}$
199	198	a1i	$⊢ ((φ \land \neg I \in \{K, L\}) \land \neg J \in \{K, L\}) \to \{J, K\} = \{K, J\}$
200	199	fveq2d	$⊢ ((φ \land \neg I \in \{K, L\}) \land \neg J \in \{K, L\}) \to pmTrsp (D) (\{J, K\}) = pmTrsp (D) (\{K, J\})$
201	197 200	eqtr4d	$⊢ ((φ \land \neg I \in \{K, L\}) \land \neg J \in \{K, L\}) \to M (⟨“ K J ”⟩) = pmTrsp (D) (\{J, K\})$
202	201 194	eqeltrd	$⊢ ((φ \land \neg I \in \{K, L\}) \land \neg J \in \{K, L\}) \to M (⟨“ K J ”⟩) \in {Base}_{S}$
203	25 6	grpcl	$⊢ (S \in Grp \land M (⟨“ K J ”⟩) \in {Base}_{S} \land M (⟨“ K L ”⟩) \in {Base}_{S}) \to M (⟨“ K J ”⟩) \underset{˙}{\cdot} M (⟨“ K L ”⟩) \in {Base}_{S}$
204	179 202 180 203	syl3anc	$⊢ ((φ \land \neg I \in \{K, L\}) \land \neg J \in \{K, L\}) \to M (⟨“ K J ”⟩) \underset{˙}{\cdot} M (⟨“ K L ”⟩) \in {Base}_{S}$
205	25 6	grpass	$⊢ (S \in Grp \land (M (⟨“ I J ”⟩) \in {Base}_{S} \land M (⟨“ J K ”⟩) \in {Base}_{S} \land M (⟨“ K J ”⟩) \underset{˙}{\cdot} M (⟨“ K L ”⟩) \in {Base}_{S})) \to (M (⟨“ I J ”⟩) \underset{˙}{\cdot} M (⟨“ J K ”⟩)) \underset{˙}{\cdot} (M (⟨“ K J ”⟩) \underset{˙}{\cdot} M (⟨“ K L ”⟩)) = M (⟨“ I J ”⟩) \underset{˙}{\cdot} (M (⟨“ J K ”⟩) \underset{˙}{\cdot} (M (⟨“ K J ”⟩) \underset{˙}{\cdot} M (⟨“ K L ”⟩)))$
206	179 185 195 204 205	syl13anc	$⊢ ((φ \land \neg I \in \{K, L\}) \land \neg J \in \{K, L\}) \to (M (⟨“ I J ”⟩) \underset{˙}{\cdot} M (⟨“ J K ”⟩)) \underset{˙}{\cdot} (M (⟨“ K J ”⟩) \underset{˙}{\cdot} M (⟨“ K L ”⟩)) = M (⟨“ I J ”⟩) \underset{˙}{\cdot} (M (⟨“ J K ”⟩) \underset{˙}{\cdot} (M (⟨“ K J ”⟩) \underset{˙}{\cdot} M (⟨“ K L ”⟩)))$
207	25 6	grpass	$⊢ (S \in Grp \land (M (⟨“ J K ”⟩) \in {Base}_{S} \land M (⟨“ K J ”⟩) \in {Base}_{S} \land M (⟨“ K L ”⟩) \in {Base}_{S})) \to (M (⟨“ J K ”⟩) \underset{˙}{\cdot} M (⟨“ K J ”⟩)) \underset{˙}{\cdot} M (⟨“ K L ”⟩) = M (⟨“ J K ”⟩) \underset{˙}{\cdot} (M (⟨“ K J ”⟩) \underset{˙}{\cdot} M (⟨“ K L ”⟩))$
208	179 195 202 180 207	syl13anc	$⊢ ((φ \land \neg I \in \{K, L\}) \land \neg J \in \{K, L\}) \to (M (⟨“ J K ”⟩) \underset{˙}{\cdot} M (⟨“ K J ”⟩)) \underset{˙}{\cdot} M (⟨“ K L ”⟩) = M (⟨“ J K ”⟩) \underset{˙}{\cdot} (M (⟨“ K J ”⟩) \underset{˙}{\cdot} M (⟨“ K L ”⟩))$
209	208	oveq2d	$⊢ ((φ \land \neg I \in \{K, L\}) \land \neg J \in \{K, L\}) \to M (⟨“ I J ”⟩) \underset{˙}{\cdot} ((M (⟨“ J K ”⟩) \underset{˙}{\cdot} M (⟨“ K J ”⟩)) \underset{˙}{\cdot} M (⟨“ K L ”⟩)) = M (⟨“ I J ”⟩) \underset{˙}{\cdot} (M (⟨“ J K ”⟩) \underset{˙}{\cdot} (M (⟨“ K J ”⟩) \underset{˙}{\cdot} M (⟨“ K L ”⟩)))$
210	186 201	oveq12d	$⊢ ((φ \land \neg I \in \{K, L\}) \land \neg J \in \{K, L\}) \to M (⟨“ J K ”⟩) \underset{˙}{\cdot} M (⟨“ K J ”⟩) = pmTrsp (D) (\{J, K\}) \underset{˙}{\cdot} pmTrsp (D) (\{J, K\})$
211	3 25 6	symgov	$⊢ (pmTrsp (D) (\{J, K\}) \in {Base}_{S} \land pmTrsp (D) (\{J, K\}) \in {Base}_{S}) \to pmTrsp (D) (\{J, K\}) \underset{˙}{\cdot} pmTrsp (D) (\{J, K\}) = pmTrsp (D) (\{J, K\}) \circ pmTrsp (D) (\{J, K\})$
212	194 194 211	syl2anc	$⊢ ((φ \land \neg I \in \{K, L\}) \land \neg J \in \{K, L\}) \to pmTrsp (D) (\{J, K\}) \underset{˙}{\cdot} pmTrsp (D) (\{J, K\}) = pmTrsp (D) (\{J, K\}) \circ pmTrsp (D) (\{J, K\})$
213	30 53	pmtrfinv	$⊢ pmTrsp (D) (\{J, K\}) \in ran pmTrsp (D) \to pmTrsp (D) (\{J, K\}) \circ pmTrsp (D) (\{J, K\}) = {I ↾}_{D}$
214	193 213	syl	$⊢ ((φ \land \neg I \in \{K, L\}) \land \neg J \in \{K, L\}) \to pmTrsp (D) (\{J, K\}) \circ pmTrsp (D) (\{J, K\}) = {I ↾}_{D}$
215	210 212 214	3eqtrd	$⊢ ((φ \land \neg I \in \{K, L\}) \land \neg J \in \{K, L\}) \to M (⟨“ J K ”⟩) \underset{˙}{\cdot} M (⟨“ K J ”⟩) = {I ↾}_{D}$
216	215	oveq1d	$⊢ ((φ \land \neg I \in \{K, L\}) \land \neg J \in \{K, L\}) \to (M (⟨“ J K ”⟩) \underset{˙}{\cdot} M (⟨“ K J ”⟩)) \underset{˙}{\cdot} M (⟨“ K L ”⟩) = ({I ↾}_{D}) \underset{˙}{\cdot} M (⟨“ K L ”⟩)$
217	216	oveq2d	$⊢ ((φ \land \neg I \in \{K, L\}) \land \neg J \in \{K, L\}) \to M (⟨“ I J ”⟩) \underset{˙}{\cdot} ((M (⟨“ J K ”⟩) \underset{˙}{\cdot} M (⟨“ K J ”⟩)) \underset{˙}{\cdot} M (⟨“ K L ”⟩)) = M (⟨“ I J ”⟩) \underset{˙}{\cdot} (({I ↾}_{D}) \underset{˙}{\cdot} M (⟨“ K L ”⟩))$
218	206 209 217	3eqtr2rd	$⊢ ((φ \land \neg I \in \{K, L\}) \land \neg J \in \{K, L\}) \to M (⟨“ I J ”⟩) \underset{˙}{\cdot} (({I ↾}_{D}) \underset{˙}{\cdot} M (⟨“ K L ”⟩)) = (M (⟨“ I J ”⟩) \underset{˙}{\cdot} M (⟨“ J K ”⟩)) \underset{˙}{\cdot} (M (⟨“ K J ”⟩) \underset{˙}{\cdot} M (⟨“ K L ”⟩))$
219	184 218	eqtr3d	$⊢ ((φ \land \neg I \in \{K, L\}) \land \neg J \in \{K, L\}) \to M (⟨“ I J ”⟩) \underset{˙}{\cdot} M (⟨“ K L ”⟩) = (M (⟨“ I J ”⟩) \underset{˙}{\cdot} M (⟨“ J K ”⟩)) \underset{˙}{\cdot} (M (⟨“ K J ”⟩) \underset{˙}{\cdot} M (⟨“ K L ”⟩))$
220	11 12	oveq12d	$⊢ φ \to E \underset{˙}{\cdot} F = M (⟨“ I J ”⟩) \underset{˙}{\cdot} M (⟨“ K L ”⟩)$
221	220	ad2antrr	$⊢ ((φ \land \neg I \in \{K, L\}) \land \neg J \in \{K, L\}) \to E \underset{˙}{\cdot} F = M (⟨“ I J ”⟩) \underset{˙}{\cdot} M (⟨“ K L ”⟩)$
222	5 3 148 149 150 151 153 159 160 6	cyc3co2	$⊢ ((φ \land \neg I \in \{K, L\}) \land \neg J \in \{K, L\}) \to M (⟨“ J K I ”⟩) = M (⟨“ J I ”⟩) \underset{˙}{\cdot} M (⟨“ J K ”⟩)$
223	136	oveq1d	$⊢ φ \to M (⟨“ I J ”⟩) \underset{˙}{\cdot} M (⟨“ J K ”⟩) = M (⟨“ J I ”⟩) \underset{˙}{\cdot} M (⟨“ J K ”⟩)$
224	223	ad2antrr	$⊢ ((φ \land \neg I \in \{K, L\}) \land \neg J \in \{K, L\}) \to M (⟨“ I J ”⟩) \underset{˙}{\cdot} M (⟨“ J K ”⟩) = M (⟨“ J I ”⟩) \underset{˙}{\cdot} M (⟨“ J K ”⟩)$
225	222 224	eqtr4d	$⊢ ((φ \land \neg I \in \{K, L\}) \land \neg J \in \{K, L\}) \to M (⟨“ J K I ”⟩) = M (⟨“ I J ”⟩) \underset{˙}{\cdot} M (⟨“ J K ”⟩)$
226	5 3 148 150 163 149 164 168 153 6	cyc3co2	$⊢ ((φ \land \neg I \in \{K, L\}) \land \neg J \in \{K, L\}) \to M (⟨“ K L J ”⟩) = M (⟨“ K J ”⟩) \underset{˙}{\cdot} M (⟨“ K L ”⟩)$
227	225 226	oveq12d	$⊢ ((φ \land \neg I \in \{K, L\}) \land \neg J \in \{K, L\}) \to M (⟨“ J K I ”⟩) \underset{˙}{\cdot} M (⟨“ K L J ”⟩) = (M (⟨“ I J ”⟩) \underset{˙}{\cdot} M (⟨“ J K ”⟩)) \underset{˙}{\cdot} (M (⟨“ K J ”⟩) \underset{˙}{\cdot} M (⟨“ K L ”⟩))$
228	219 221 227	3eqtr4d	$⊢ ((φ \land \neg I \in \{K, L\}) \land \neg J \in \{K, L\}) \to E \underset{˙}{\cdot} F = M (⟨“ J K I ”⟩) \underset{˙}{\cdot} M (⟨“ K L J ”⟩)$
229	178	grpmndd	$⊢ φ \to S \in Mnd$
230	229	ad2antrr	$⊢ ((φ \land \neg I \in \{K, L\}) \land \neg J \in \{K, L\}) \to S \in Mnd$
231	5 3 148 149 150 151 153 159 160	cycpm3cl	$⊢ ((φ \land \neg I \in \{K, L\}) \land \neg J \in \{K, L\}) \to M (⟨“ J K I ”⟩) \in {Base}_{S}$
232	226 204	eqeltrd	$⊢ ((φ \land \neg I \in \{K, L\}) \land \neg J \in \{K, L\}) \to M (⟨“ K L J ”⟩) \in {Base}_{S}$
233	25 6	gsumws2	$⊢ (S \in Mnd \land M (⟨“ J K I ”⟩) \in {Base}_{S} \land M (⟨“ K L J ”⟩) \in {Base}_{S}) \to \sum_{S} ⟨“ M (⟨“ J K I ”⟩) M (⟨“ K L J ”⟩) ”⟩ = M (⟨“ J K I ”⟩) \underset{˙}{\cdot} M (⟨“ K L J ”⟩)$
234	230 231 232 233	syl3anc	$⊢ ((φ \land \neg I \in \{K, L\}) \land \neg J \in \{K, L\}) \to \sum_{S} ⟨“ M (⟨“ J K I ”⟩) M (⟨“ K L J ”⟩) ”⟩ = M (⟨“ J K I ”⟩) \underset{˙}{\cdot} M (⟨“ K L J ”⟩)$
235	228 234	eqtr4d	$⊢ ((φ \land \neg I \in \{K, L\}) \land \neg J \in \{K, L\}) \to E \underset{˙}{\cdot} F = \sum_{S} ⟨“ M (⟨“ J K I ”⟩) M (⟨“ K L J ”⟩) ”⟩$
236	171 174 235	rspcedvd	$⊢ ((φ \land \neg I \in \{K, L\}) \land \neg J \in \{K, L\}) \to \exists c \in Word C E \underset{˙}{\cdot} F = \sum_{S} c$
237	147 236	pm2.61dan	$⊢ (φ \land \neg I \in \{K, L\}) \to \exists c \in Word C E \underset{˙}{\cdot} F = \sum_{S} c$
238	106 237	pm2.61dan	$⊢ φ \to \exists c \in Word C E \underset{˙}{\cdot} F = \sum_{S} c$

Metamath Proof Explorer

Theorem cyc3genpmlem

Proof