Theorem cyc3genpmlem 33537

Description: Lemma for cyc3genpm 33538. (Contributed by Thierry Arnoux, 24-Sep-2023.)

Hypotheses

Ref	Expression
cyc3genpm.t	⊢ 𝐶 = (𝑀 “ (◡♯ “ {3}))
cyc3genpm.a	⊢ 𝐴 = (pmEven‘𝐷)
cyc3genpm.s	⊢ 𝑆 = (SymGrp‘𝐷)
cyc3genpm.n	⊢ 𝑁 = (♯‘𝐷)
cyc3genpm.m	⊢ 𝑀 = (toCyc‘𝐷)
cyc3genpmlem.t	⊢ · = (+g‘𝑆)
cyc3genpmlem.i	⊢ (𝜑 → 𝐼 ∈ 𝐷)
cyc3genpmlem.j	⊢ (𝜑 → 𝐽 ∈ 𝐷)
cyc3genpmlem.k	⊢ (𝜑 → 𝐾 ∈ 𝐷)
cyc3genpmlem.l	⊢ (𝜑 → 𝐿 ∈ 𝐷)
cyc3genpmlem.e	⊢ (𝜑 → 𝐸 = (𝑀‘⟨“𝐼𝐽”⟩))
cyc3genpmlem.f	⊢ (𝜑 → 𝐹 = (𝑀‘⟨“𝐾𝐿”⟩))
cyc3genpmlem.d	⊢ (𝜑 → 𝐷 ∈ 𝑉)
cyc3genpmlem.1	⊢ (𝜑 → 𝐼 ≠ 𝐽)
cyc3genpmlem.2	⊢ (𝜑 → 𝐾 ≠ 𝐿)

Assertion

Ref	Expression
cyc3genpmlem	⊢ (𝜑 → ∃𝑐 ∈ Word 𝐶(𝐸 · 𝐹) = (𝑆 Σg 𝑐))

Distinct variable groups:   · ,𝑐   𝐶,𝑐   𝐷,𝑐   𝐸,𝑐   𝐹,𝑐   𝐼,𝑐   𝐽,𝑐   𝐾,𝑐   𝐿,𝑐   𝑀,𝑐   𝑆,𝑐   𝜑,𝑐

Allowed substitution hints:   𝐴(𝑐)   𝑁(𝑐)   𝑉(𝑐)

Proof of Theorem cyc3genpmlem

Step	Hyp	Ref	Expression
1		wrd0 14596	. . . . 5 ⊢ ∅ ∈ Word 𝐶
2	1	a1i 11	. . . 4 ⊢ (((𝜑 ∧ 𝐼 ∈ {𝐾, 𝐿}) ∧ 𝐽 ∈ {𝐾, 𝐿}) → ∅ ∈ Word 𝐶)
3		simpr 490	. . . . . 6 ⊢ ((((𝜑 ∧ 𝐼 ∈ {𝐾, 𝐿}) ∧ 𝐽 ∈ {𝐾, 𝐿}) ∧ 𝑐 = ∅) → 𝑐 = ∅)
4	3	oveq2d 7435	. . . . 5 ⊢ ((((𝜑 ∧ 𝐼 ∈ {𝐾, 𝐿}) ∧ 𝐽 ∈ {𝐾, 𝐿}) ∧ 𝑐 = ∅) → (𝑆 Σg 𝑐) = (𝑆 Σg ∅))
5	4	eqeq2d 2776	. . . 4 ⊢ ((((𝜑 ∧ 𝐼 ∈ {𝐾, 𝐿}) ∧ 𝐽 ∈ {𝐾, 𝐿}) ∧ 𝑐 = ∅) → ((𝐸 · 𝐹) = (𝑆 Σg 𝑐) ↔ (𝐸 · 𝐹) = (𝑆 Σg ∅)))
6		cyc3genpmlem.e	. . . . . . . . 9 ⊢ (𝜑 → 𝐸 = (𝑀‘⟨“𝐼𝐽”⟩))
7		cyc3genpm.m	. . . . . . . . . 10 ⊢ 𝑀 = (toCyc‘𝐷)
8		cyc3genpmlem.d	. . . . . . . . . 10 ⊢ (𝜑 → 𝐷 ∈ 𝑉)
9		cyc3genpmlem.i	. . . . . . . . . 10 ⊢ (𝜑 → 𝐼 ∈ 𝐷)
10		cyc3genpmlem.j	. . . . . . . . . 10 ⊢ (𝜑 → 𝐽 ∈ 𝐷)
11		cyc3genpmlem.1	. . . . . . . . . 10 ⊢ (𝜑 → 𝐼 ≠ 𝐽)
12		cyc3genpm.s	. . . . . . . . . 10 ⊢ 𝑆 = (SymGrp‘𝐷)
13	7, 8, 9, 10, 11, 12	cycpm2cl 33506	. . . . . . . . 9 ⊢ (𝜑 → (𝑀‘⟨“𝐼𝐽”⟩) ∈ (Base‘𝑆))
14	6, 13	eqeltrd 2865	. . . . . . . 8 ⊢ (𝜑 → 𝐸 ∈ (Base‘𝑆))
15		cyc3genpmlem.f	. . . . . . . . 9 ⊢ (𝜑 → 𝐹 = (𝑀‘⟨“𝐾𝐿”⟩))
16		cyc3genpmlem.k	. . . . . . . . . 10 ⊢ (𝜑 → 𝐾 ∈ 𝐷)
17		cyc3genpmlem.l	. . . . . . . . . 10 ⊢ (𝜑 → 𝐿 ∈ 𝐷)
18		cyc3genpmlem.2	. . . . . . . . . 10 ⊢ (𝜑 → 𝐾 ≠ 𝐿)
19	7, 8, 16, 17, 18, 12	cycpm2cl 33506	. . . . . . . . 9 ⊢ (𝜑 → (𝑀‘⟨“𝐾𝐿”⟩) ∈ (Base‘𝑆))
20	15, 19	eqeltrd 2865	. . . . . . . 8 ⊢ (𝜑 → 𝐹 ∈ (Base‘𝑆))
21		eqid 2765	. . . . . . . . 9 ⊢ (Base‘𝑆) = (Base‘𝑆)
22		cyc3genpmlem.t	. . . . . . . . 9 ⊢ · = (+g‘𝑆)
23	12, 21, 22	symgov 19500	. . . . . . . 8 ⊢ ((𝐸 ∈ (Base‘𝑆) ∧ 𝐹 ∈ (Base‘𝑆)) → (𝐸 · 𝐹) = (𝐸 ∘ 𝐹))
24	14, 20, 23	syl2anc 596	. . . . . . 7 ⊢ (𝜑 → (𝐸 · 𝐹) = (𝐸 ∘ 𝐹))
25	24	ad2antrr 739	. . . . . 6 ⊢ (((𝜑 ∧ 𝐼 ∈ {𝐾, 𝐿}) ∧ 𝐽 ∈ {𝐾, 𝐿}) → (𝐸 · 𝐹) = (𝐸 ∘ 𝐹))
26	6	ad2antrr 739	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝐼 ∈ {𝐾, 𝐿}) ∧ 𝐽 ∈ {𝐾, 𝐿}) → 𝐸 = (𝑀‘⟨“𝐼𝐽”⟩))
27		eqid 2765	. . . . . . . . . 10 ⊢ (pmTrsp‘𝐷) = (pmTrsp‘𝐷)
28	7, 8, 9, 10, 11, 27	cycpm2tr 33505	. . . . . . . . 9 ⊢ (𝜑 → (𝑀‘⟨“𝐼𝐽”⟩) = ((pmTrsp‘𝐷)‘{𝐼, 𝐽}))
29	28	ad2antrr 739	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝐼 ∈ {𝐾, 𝐿}) ∧ 𝐽 ∈ {𝐾, 𝐿}) → (𝑀‘⟨“𝐼𝐽”⟩) = ((pmTrsp‘𝐷)‘{𝐼, 𝐽}))
30	26, 29	eqtrd 2800	. . . . . . 7 ⊢ (((𝜑 ∧ 𝐼 ∈ {𝐾, 𝐿}) ∧ 𝐽 ∈ {𝐾, 𝐿}) → 𝐸 = ((pmTrsp‘𝐷)‘{𝐼, 𝐽}))
31	7, 8, 16, 17, 18, 27	cycpm2tr 33505	. . . . . . . . 9 ⊢ (𝜑 → (𝑀‘⟨“𝐾𝐿”⟩) = ((pmTrsp‘𝐷)‘{𝐾, 𝐿}))
32	31	ad2antrr 739	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝐼 ∈ {𝐾, 𝐿}) ∧ 𝐽 ∈ {𝐾, 𝐿}) → (𝑀‘⟨“𝐾𝐿”⟩) = ((pmTrsp‘𝐷)‘{𝐾, 𝐿}))
33	15	ad2antrr 739	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝐼 ∈ {𝐾, 𝐿}) ∧ 𝐽 ∈ {𝐾, 𝐿}) → 𝐹 = (𝑀‘⟨“𝐾𝐿”⟩))
34	9	ad2antrr 739	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝐼 ∈ {𝐾, 𝐿}) ∧ 𝐽 ∈ {𝐾, 𝐿}) → 𝐼 ∈ 𝐷)
35	10	ad2antrr 739	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝐼 ∈ {𝐾, 𝐿}) ∧ 𝐽 ∈ {𝐾, 𝐿}) → 𝐽 ∈ 𝐷)
36	11	ad2antrr 739	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝐼 ∈ {𝐾, 𝐿}) ∧ 𝐽 ∈ {𝐾, 𝐿}) → 𝐼 ≠ 𝐽)
37		simplr 781	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝐼 ∈ {𝐾, 𝐿}) ∧ 𝐽 ∈ {𝐾, 𝐿}) → 𝐼 ∈ {𝐾, 𝐿})
38		simpr 490	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝐼 ∈ {𝐾, 𝐿}) ∧ 𝐽 ∈ {𝐾, 𝐿}) → 𝐽 ∈ {𝐾, 𝐿})
39	37, 38	prssd 4790	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝐼 ∈ {𝐾, 𝐿}) ∧ 𝐽 ∈ {𝐾, 𝐿}) → {𝐼, 𝐽} ⊆ {𝐾, 𝐿})
40		ssprsseq 4793	. . . . . . . . . . 11 ⊢ ((𝐼 ∈ 𝐷 ∧ 𝐽 ∈ 𝐷 ∧ 𝐼 ≠ 𝐽) → ({𝐼, 𝐽} ⊆ {𝐾, 𝐿} ↔ {𝐼, 𝐽} = {𝐾, 𝐿}))
41	40	biimpa 482	. . . . . . . . . 10 ⊢ (((𝐼 ∈ 𝐷 ∧ 𝐽 ∈ 𝐷 ∧ 𝐼 ≠ 𝐽) ∧ {𝐼, 𝐽} ⊆ {𝐾, 𝐿}) → {𝐼, 𝐽} = {𝐾, 𝐿})
42	34, 35, 36, 39, 41	syl31anc 1400	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝐼 ∈ {𝐾, 𝐿}) ∧ 𝐽 ∈ {𝐾, 𝐿}) → {𝐼, 𝐽} = {𝐾, 𝐿})
43	42	fveq2d 6889	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝐼 ∈ {𝐾, 𝐿}) ∧ 𝐽 ∈ {𝐾, 𝐿}) → ((pmTrsp‘𝐷)‘{𝐼, 𝐽}) = ((pmTrsp‘𝐷)‘{𝐾, 𝐿}))
44	32, 33, 43	3eqtr4d 2810	. . . . . . 7 ⊢ (((𝜑 ∧ 𝐼 ∈ {𝐾, 𝐿}) ∧ 𝐽 ∈ {𝐾, 𝐿}) → 𝐹 = ((pmTrsp‘𝐷)‘{𝐼, 𝐽}))
45	30, 44	coeq12d 5852	. . . . . 6 ⊢ (((𝜑 ∧ 𝐼 ∈ {𝐾, 𝐿}) ∧ 𝐽 ∈ {𝐾, 𝐿}) → (𝐸 ∘ 𝐹) = (((pmTrsp‘𝐷)‘{𝐼, 𝐽}) ∘ ((pmTrsp‘𝐷)‘{𝐼, 𝐽})))
46	8	ad2antrr 739	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝐼 ∈ {𝐾, 𝐿}) ∧ 𝐽 ∈ {𝐾, 𝐿}) → 𝐷 ∈ 𝑉)
47	34, 35	prssd 4790	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝐼 ∈ {𝐾, 𝐿}) ∧ 𝐽 ∈ {𝐾, 𝐿}) → {𝐼, 𝐽} ⊆ 𝐷)
48		enpr2 10004	. . . . . . . . 9 ⊢ ((𝐼 ∈ 𝐷 ∧ 𝐽 ∈ 𝐷 ∧ 𝐼 ≠ 𝐽) → {𝐼, 𝐽} ≈ 2o)
49	34, 35, 36, 48	syl3anc 1398	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝐼 ∈ {𝐾, 𝐿}) ∧ 𝐽 ∈ {𝐾, 𝐿}) → {𝐼, 𝐽} ≈ 2o)
50		eqid 2765	. . . . . . . . 9 ⊢ ran (pmTrsp‘𝐷) = ran (pmTrsp‘𝐷)
51	27, 50	pmtrrn 19573	. . . . . . . 8 ⊢ ((𝐷 ∈ 𝑉 ∧ {𝐼, 𝐽} ⊆ 𝐷 ∧ {𝐼, 𝐽} ≈ 2o) → ((pmTrsp‘𝐷)‘{𝐼, 𝐽}) ∈ ran (pmTrsp‘𝐷))
52	46, 47, 49, 51	syl3anc 1398	. . . . . . 7 ⊢ (((𝜑 ∧ 𝐼 ∈ {𝐾, 𝐿}) ∧ 𝐽 ∈ {𝐾, 𝐿}) → ((pmTrsp‘𝐷)‘{𝐼, 𝐽}) ∈ ran (pmTrsp‘𝐷))
53	27, 50	pmtrfinv 19577	. . . . . . 7 ⊢ (((pmTrsp‘𝐷)‘{𝐼, 𝐽}) ∈ ran (pmTrsp‘𝐷) → (((pmTrsp‘𝐷)‘{𝐼, 𝐽}) ∘ ((pmTrsp‘𝐷)‘{𝐼, 𝐽})) = ( I ↾ 𝐷))
54	52, 53	syl 18	. . . . . 6 ⊢ (((𝜑 ∧ 𝐼 ∈ {𝐾, 𝐿}) ∧ 𝐽 ∈ {𝐾, 𝐿}) → (((pmTrsp‘𝐷)‘{𝐼, 𝐽}) ∘ ((pmTrsp‘𝐷)‘{𝐼, 𝐽})) = ( I ↾ 𝐷))
55	25, 45, 54	3eqtrd 2804	. . . . 5 ⊢ (((𝜑 ∧ 𝐼 ∈ {𝐾, 𝐿}) ∧ 𝐽 ∈ {𝐾, 𝐿}) → (𝐸 · 𝐹) = ( I ↾ 𝐷))
56	12	symgid 19517	. . . . . . 7 ⊢ (𝐷 ∈ 𝑉 → ( I ↾ 𝐷) = (0g‘𝑆))
57	46, 56	syl 18	. . . . . 6 ⊢ (((𝜑 ∧ 𝐼 ∈ {𝐾, 𝐿}) ∧ 𝐽 ∈ {𝐾, 𝐿}) → ( I ↾ 𝐷) = (0g‘𝑆))
58		eqid 2765	. . . . . . 7 ⊢ (0g‘𝑆) = (0g‘𝑆)
59	58	gsum0 18776	. . . . . 6 ⊢ (𝑆 Σg ∅) = (0g‘𝑆)
60	57, 59	eqtr4di 2818	. . . . 5 ⊢ (((𝜑 ∧ 𝐼 ∈ {𝐾, 𝐿}) ∧ 𝐽 ∈ {𝐾, 𝐿}) → ( I ↾ 𝐷) = (𝑆 Σg ∅))
61	55, 60	eqtrd 2800	. . . 4 ⊢ (((𝜑 ∧ 𝐼 ∈ {𝐾, 𝐿}) ∧ 𝐽 ∈ {𝐾, 𝐿}) → (𝐸 · 𝐹) = (𝑆 Σg ∅))
62	2, 5, 61	rspcedvd 3585	. . 3 ⊢ (((𝜑 ∧ 𝐼 ∈ {𝐾, 𝐿}) ∧ 𝐽 ∈ {𝐾, 𝐿}) → ∃𝑐 ∈ Word 𝐶(𝐸 · 𝐹) = (𝑆 Σg 𝑐))
63	8	ad2antrr 739	. . . . . . 7 ⊢ (((𝜑 ∧ 𝐼 ∈ {𝐾, 𝐿}) ∧ ¬ 𝐽 ∈ {𝐾, 𝐿}) → 𝐷 ∈ 𝑉)
64	9	ad2antrr 739	. . . . . . 7 ⊢ (((𝜑 ∧ 𝐼 ∈ {𝐾, 𝐿}) ∧ ¬ 𝐽 ∈ {𝐾, 𝐿}) → 𝐼 ∈ 𝐷)
65	16, 17	prssd 4790	. . . . . . . . 9 ⊢ (𝜑 → {𝐾, 𝐿} ⊆ 𝐷)
66	65	ad2antrr 739	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝐼 ∈ {𝐾, 𝐿}) ∧ ¬ 𝐽 ∈ {𝐾, 𝐿}) → {𝐾, 𝐿} ⊆ 𝐷)
67		simplr 781	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝐼 ∈ {𝐾, 𝐿}) ∧ ¬ 𝐽 ∈ {𝐾, 𝐿}) → 𝐼 ∈ {𝐾, 𝐿})
68		enpr2 10004	. . . . . . . . . . 11 ⊢ ((𝐾 ∈ 𝐷 ∧ 𝐿 ∈ 𝐷 ∧ 𝐾 ≠ 𝐿) → {𝐾, 𝐿} ≈ 2o)
69	16, 17, 18, 68	syl3anc 1398	. . . . . . . . . 10 ⊢ (𝜑 → {𝐾, 𝐿} ≈ 2o)
70	69	ad2antrr 739	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝐼 ∈ {𝐾, 𝐿}) ∧ ¬ 𝐽 ∈ {𝐾, 𝐿}) → {𝐾, 𝐿} ≈ 2o)
71		unidifsnel 32954	. . . . . . . . 9 ⊢ ((𝐼 ∈ {𝐾, 𝐿} ∧ {𝐾, 𝐿} ≈ 2o) → ∪ ({𝐾, 𝐿} ∖ {𝐼}) ∈ {𝐾, 𝐿})
72	67, 70, 71	syl2anc 596	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝐼 ∈ {𝐾, 𝐿}) ∧ ¬ 𝐽 ∈ {𝐾, 𝐿}) → ∪ ({𝐾, 𝐿} ∖ {𝐼}) ∈ {𝐾, 𝐿})
73	66, 72	sseldd 3939	. . . . . . 7 ⊢ (((𝜑 ∧ 𝐼 ∈ {𝐾, 𝐿}) ∧ ¬ 𝐽 ∈ {𝐾, 𝐿}) → ∪ ({𝐾, 𝐿} ∖ {𝐼}) ∈ 𝐷)
74	10	ad2antrr 739	. . . . . . 7 ⊢ (((𝜑 ∧ 𝐼 ∈ {𝐾, 𝐿}) ∧ ¬ 𝐽 ∈ {𝐾, 𝐿}) → 𝐽 ∈ 𝐷)
75		unidifsnne 32955	. . . . . . . . 9 ⊢ ((𝐼 ∈ {𝐾, 𝐿} ∧ {𝐾, 𝐿} ≈ 2o) → ∪ ({𝐾, 𝐿} ∖ {𝐼}) ≠ 𝐼)
76	67, 70, 75	syl2anc 596	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝐼 ∈ {𝐾, 𝐿}) ∧ ¬ 𝐽 ∈ {𝐾, 𝐿}) → ∪ ({𝐾, 𝐿} ∖ {𝐼}) ≠ 𝐼)
77	76	necomd 3015	. . . . . . 7 ⊢ (((𝜑 ∧ 𝐼 ∈ {𝐾, 𝐿}) ∧ ¬ 𝐽 ∈ {𝐾, 𝐿}) → 𝐼 ≠ ∪ ({𝐾, 𝐿} ∖ {𝐼}))
78		nelne2 3058	. . . . . . . 8 ⊢ ((∪ ({𝐾, 𝐿} ∖ {𝐼}) ∈ {𝐾, 𝐿} ∧ ¬ 𝐽 ∈ {𝐾, 𝐿}) → ∪ ({𝐾, 𝐿} ∖ {𝐼}) ≠ 𝐽)
79	72, 78	sylancom 600	. . . . . . 7 ⊢ (((𝜑 ∧ 𝐼 ∈ {𝐾, 𝐿}) ∧ ¬ 𝐽 ∈ {𝐾, 𝐿}) → ∪ ({𝐾, 𝐿} ∖ {𝐼}) ≠ 𝐽)
80	11	necomd 3015	. . . . . . . 8 ⊢ (𝜑 → 𝐽 ≠ 𝐼)
81	80	ad2antrr 739	. . . . . . 7 ⊢ (((𝜑 ∧ 𝐼 ∈ {𝐾, 𝐿}) ∧ ¬ 𝐽 ∈ {𝐾, 𝐿}) → 𝐽 ≠ 𝐼)
82	7, 12, 63, 64, 73, 74, 77, 79, 81	cycpm3cl2 33522	. . . . . 6 ⊢ (((𝜑 ∧ 𝐼 ∈ {𝐾, 𝐿}) ∧ ¬ 𝐽 ∈ {𝐾, 𝐿}) → (𝑀‘⟨“𝐼∪ ({𝐾, 𝐿} ∖ {𝐼})𝐽”⟩) ∈ (𝑀 “ (◡♯ “ {3})))
83		cyc3genpm.t	. . . . . 6 ⊢ 𝐶 = (𝑀 “ (◡♯ “ {3}))
84	82, 83	eleqtrrdi 2876	. . . . 5 ⊢ (((𝜑 ∧ 𝐼 ∈ {𝐾, 𝐿}) ∧ ¬ 𝐽 ∈ {𝐾, 𝐿}) → (𝑀‘⟨“𝐼∪ ({𝐾, 𝐿} ∖ {𝐼})𝐽”⟩) ∈ 𝐶)
85	84	s1cld 14662	. . . 4 ⊢ (((𝜑 ∧ 𝐼 ∈ {𝐾, 𝐿}) ∧ ¬ 𝐽 ∈ {𝐾, 𝐿}) → ⟨“(𝑀‘⟨“𝐼∪ ({𝐾, 𝐿} ∖ {𝐼})𝐽”⟩)”⟩ ∈ Word 𝐶)
86		simpr 490	. . . . . 6 ⊢ ((((𝜑 ∧ 𝐼 ∈ {𝐾, 𝐿}) ∧ ¬ 𝐽 ∈ {𝐾, 𝐿}) ∧ 𝑐 = ⟨“(𝑀‘⟨“𝐼∪ ({𝐾, 𝐿} ∖ {𝐼})𝐽”⟩)”⟩) → 𝑐 = ⟨“(𝑀‘⟨“𝐼∪ ({𝐾, 𝐿} ∖ {𝐼})𝐽”⟩)”⟩)
87	86	oveq2d 7435	. . . . 5 ⊢ ((((𝜑 ∧ 𝐼 ∈ {𝐾, 𝐿}) ∧ ¬ 𝐽 ∈ {𝐾, 𝐿}) ∧ 𝑐 = ⟨“(𝑀‘⟨“𝐼∪ ({𝐾, 𝐿} ∖ {𝐼})𝐽”⟩)”⟩) → (𝑆 Σg 𝑐) = (𝑆 Σg ⟨“(𝑀‘⟨“𝐼∪ ({𝐾, 𝐿} ∖ {𝐼})𝐽”⟩)”⟩))
88	87	eqeq2d 2776	. . . 4 ⊢ ((((𝜑 ∧ 𝐼 ∈ {𝐾, 𝐿}) ∧ ¬ 𝐽 ∈ {𝐾, 𝐿}) ∧ 𝑐 = ⟨“(𝑀‘⟨“𝐼∪ ({𝐾, 𝐿} ∖ {𝐼})𝐽”⟩)”⟩) → ((𝐸 · 𝐹) = (𝑆 Σg 𝑐) ↔ (𝐸 · 𝐹) = (𝑆 Σg ⟨“(𝑀‘⟨“𝐼∪ ({𝐾, 𝐿} ∖ {𝐼})𝐽”⟩)”⟩)))
89	7, 12, 63, 64, 73, 74, 77, 79, 81, 22	cyc3co2 33526	. . . . 5 ⊢ (((𝜑 ∧ 𝐼 ∈ {𝐾, 𝐿}) ∧ ¬ 𝐽 ∈ {𝐾, 𝐿}) → (𝑀‘⟨“𝐼∪ ({𝐾, 𝐿} ∖ {𝐼})𝐽”⟩) = ((𝑀‘⟨“𝐼𝐽”⟩) · (𝑀‘⟨“𝐼∪ ({𝐾, 𝐿} ∖ {𝐼})”⟩)))
90	7, 12, 63, 64, 73, 74, 77, 79, 81	cycpm3cl 33521	. . . . . 6 ⊢ (((𝜑 ∧ 𝐼 ∈ {𝐾, 𝐿}) ∧ ¬ 𝐽 ∈ {𝐾, 𝐿}) → (𝑀‘⟨“𝐼∪ ({𝐾, 𝐿} ∖ {𝐼})𝐽”⟩) ∈ (Base‘𝑆))
91	21	gsumws1 18936	. . . . . 6 ⊢ ((𝑀‘⟨“𝐼∪ ({𝐾, 𝐿} ∖ {𝐼})𝐽”⟩) ∈ (Base‘𝑆) → (𝑆 Σg ⟨“(𝑀‘⟨“𝐼∪ ({𝐾, 𝐿} ∖ {𝐼})𝐽”⟩)”⟩) = (𝑀‘⟨“𝐼∪ ({𝐾, 𝐿} ∖ {𝐼})𝐽”⟩))
92	90, 91	syl 18	. . . . 5 ⊢ (((𝜑 ∧ 𝐼 ∈ {𝐾, 𝐿}) ∧ ¬ 𝐽 ∈ {𝐾, 𝐿}) → (𝑆 Σg ⟨“(𝑀‘⟨“𝐼∪ ({𝐾, 𝐿} ∖ {𝐼})𝐽”⟩)”⟩) = (𝑀‘⟨“𝐼∪ ({𝐾, 𝐿} ∖ {𝐼})𝐽”⟩))
93	6	ad2antrr 739	. . . . . 6 ⊢ (((𝜑 ∧ 𝐼 ∈ {𝐾, 𝐿}) ∧ ¬ 𝐽 ∈ {𝐾, 𝐿}) → 𝐸 = (𝑀‘⟨“𝐼𝐽”⟩))
94		en2eleq 10008	. . . . . . . . 9 ⊢ ((𝐼 ∈ {𝐾, 𝐿} ∧ {𝐾, 𝐿} ≈ 2o) → {𝐾, 𝐿} = {𝐼, ∪ ({𝐾, 𝐿} ∖ {𝐼})})
95	67, 70, 94	syl2anc 596	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝐼 ∈ {𝐾, 𝐿}) ∧ ¬ 𝐽 ∈ {𝐾, 𝐿}) → {𝐾, 𝐿} = {𝐼, ∪ ({𝐾, 𝐿} ∖ {𝐼})})
96	95	fveq2d 6889	. . . . . . 7 ⊢ (((𝜑 ∧ 𝐼 ∈ {𝐾, 𝐿}) ∧ ¬ 𝐽 ∈ {𝐾, 𝐿}) → ((pmTrsp‘𝐷)‘{𝐾, 𝐿}) = ((pmTrsp‘𝐷)‘{𝐼, ∪ ({𝐾, 𝐿} ∖ {𝐼})}))
97	15, 31	eqtrd 2800	. . . . . . . 8 ⊢ (𝜑 → 𝐹 = ((pmTrsp‘𝐷)‘{𝐾, 𝐿}))
98	97	ad2antrr 739	. . . . . . 7 ⊢ (((𝜑 ∧ 𝐼 ∈ {𝐾, 𝐿}) ∧ ¬ 𝐽 ∈ {𝐾, 𝐿}) → 𝐹 = ((pmTrsp‘𝐷)‘{𝐾, 𝐿}))
99	7, 63, 64, 73, 77, 27	cycpm2tr 33505	. . . . . . 7 ⊢ (((𝜑 ∧ 𝐼 ∈ {𝐾, 𝐿}) ∧ ¬ 𝐽 ∈ {𝐾, 𝐿}) → (𝑀‘⟨“𝐼∪ ({𝐾, 𝐿} ∖ {𝐼})”⟩) = ((pmTrsp‘𝐷)‘{𝐼, ∪ ({𝐾, 𝐿} ∖ {𝐼})}))
100	96, 98, 99	3eqtr4d 2810	. . . . . 6 ⊢ (((𝜑 ∧ 𝐼 ∈ {𝐾, 𝐿}) ∧ ¬ 𝐽 ∈ {𝐾, 𝐿}) → 𝐹 = (𝑀‘⟨“𝐼∪ ({𝐾, 𝐿} ∖ {𝐼})”⟩))
101	93, 100	oveq12d 7437	. . . . 5 ⊢ (((𝜑 ∧ 𝐼 ∈ {𝐾, 𝐿}) ∧ ¬ 𝐽 ∈ {𝐾, 𝐿}) → (𝐸 · 𝐹) = ((𝑀‘⟨“𝐼𝐽”⟩) · (𝑀‘⟨“𝐼∪ ({𝐾, 𝐿} ∖ {𝐼})”⟩)))
102	89, 92, 101	3eqtr4rd 2811	. . . 4 ⊢ (((𝜑 ∧ 𝐼 ∈ {𝐾, 𝐿}) ∧ ¬ 𝐽 ∈ {𝐾, 𝐿}) → (𝐸 · 𝐹) = (𝑆 Σg ⟨“(𝑀‘⟨“𝐼∪ ({𝐾, 𝐿} ∖ {𝐼})𝐽”⟩)”⟩))
103	85, 88, 102	rspcedvd 3585	. . 3 ⊢ (((𝜑 ∧ 𝐼 ∈ {𝐾, 𝐿}) ∧ ¬ 𝐽 ∈ {𝐾, 𝐿}) → ∃𝑐 ∈ Word 𝐶(𝐸 · 𝐹) = (𝑆 Σg 𝑐))
104	62, 103	pm2.61dan 825	. 2 ⊢ ((𝜑 ∧ 𝐼 ∈ {𝐾, 𝐿}) → ∃𝑐 ∈ Word 𝐶(𝐸 · 𝐹) = (𝑆 Σg 𝑐))
105	8	ad2antrr 739	. . . . . . 7 ⊢ (((𝜑 ∧ ¬ 𝐼 ∈ {𝐾, 𝐿}) ∧ 𝐽 ∈ {𝐾, 𝐿}) → 𝐷 ∈ 𝑉)
106	10	ad2antrr 739	. . . . . . 7 ⊢ (((𝜑 ∧ ¬ 𝐼 ∈ {𝐾, 𝐿}) ∧ 𝐽 ∈ {𝐾, 𝐿}) → 𝐽 ∈ 𝐷)
107	65	ad2antrr 739	. . . . . . . 8 ⊢ (((𝜑 ∧ ¬ 𝐼 ∈ {𝐾, 𝐿}) ∧ 𝐽 ∈ {𝐾, 𝐿}) → {𝐾, 𝐿} ⊆ 𝐷)
108		simpr 490	. . . . . . . . 9 ⊢ (((𝜑 ∧ ¬ 𝐼 ∈ {𝐾, 𝐿}) ∧ 𝐽 ∈ {𝐾, 𝐿}) → 𝐽 ∈ {𝐾, 𝐿})
109	69	ad2antrr 739	. . . . . . . . 9 ⊢ (((𝜑 ∧ ¬ 𝐼 ∈ {𝐾, 𝐿}) ∧ 𝐽 ∈ {𝐾, 𝐿}) → {𝐾, 𝐿} ≈ 2o)
110		unidifsnel 32954	. . . . . . . . 9 ⊢ ((𝐽 ∈ {𝐾, 𝐿} ∧ {𝐾, 𝐿} ≈ 2o) → ∪ ({𝐾, 𝐿} ∖ {𝐽}) ∈ {𝐾, 𝐿})
111	108, 109, 110	syl2anc 596	. . . . . . . 8 ⊢ (((𝜑 ∧ ¬ 𝐼 ∈ {𝐾, 𝐿}) ∧ 𝐽 ∈ {𝐾, 𝐿}) → ∪ ({𝐾, 𝐿} ∖ {𝐽}) ∈ {𝐾, 𝐿})
112	107, 111	sseldd 3939	. . . . . . 7 ⊢ (((𝜑 ∧ ¬ 𝐼 ∈ {𝐾, 𝐿}) ∧ 𝐽 ∈ {𝐾, 𝐿}) → ∪ ({𝐾, 𝐿} ∖ {𝐽}) ∈ 𝐷)
113	9	ad2antrr 739	. . . . . . 7 ⊢ (((𝜑 ∧ ¬ 𝐼 ∈ {𝐾, 𝐿}) ∧ 𝐽 ∈ {𝐾, 𝐿}) → 𝐼 ∈ 𝐷)
114		unidifsnne 32955	. . . . . . . . 9 ⊢ ((𝐽 ∈ {𝐾, 𝐿} ∧ {𝐾, 𝐿} ≈ 2o) → ∪ ({𝐾, 𝐿} ∖ {𝐽}) ≠ 𝐽)
115	108, 109, 114	syl2anc 596	. . . . . . . 8 ⊢ (((𝜑 ∧ ¬ 𝐼 ∈ {𝐾, 𝐿}) ∧ 𝐽 ∈ {𝐾, 𝐿}) → ∪ ({𝐾, 𝐿} ∖ {𝐽}) ≠ 𝐽)
116	115	necomd 3015	. . . . . . 7 ⊢ (((𝜑 ∧ ¬ 𝐼 ∈ {𝐾, 𝐿}) ∧ 𝐽 ∈ {𝐾, 𝐿}) → 𝐽 ≠ ∪ ({𝐾, 𝐿} ∖ {𝐽}))
117		simplr 781	. . . . . . . 8 ⊢ (((𝜑 ∧ ¬ 𝐼 ∈ {𝐾, 𝐿}) ∧ 𝐽 ∈ {𝐾, 𝐿}) → ¬ 𝐼 ∈ {𝐾, 𝐿})
118		nelne2 3058	. . . . . . . 8 ⊢ ((∪ ({𝐾, 𝐿} ∖ {𝐽}) ∈ {𝐾, 𝐿} ∧ ¬ 𝐼 ∈ {𝐾, 𝐿}) → ∪ ({𝐾, 𝐿} ∖ {𝐽}) ≠ 𝐼)
119	111, 117, 118	syl2anc 596	. . . . . . 7 ⊢ (((𝜑 ∧ ¬ 𝐼 ∈ {𝐾, 𝐿}) ∧ 𝐽 ∈ {𝐾, 𝐿}) → ∪ ({𝐾, 𝐿} ∖ {𝐽}) ≠ 𝐼)
120	11	ad2antrr 739	. . . . . . 7 ⊢ (((𝜑 ∧ ¬ 𝐼 ∈ {𝐾, 𝐿}) ∧ 𝐽 ∈ {𝐾, 𝐿}) → 𝐼 ≠ 𝐽)
121	7, 12, 105, 106, 112, 113, 116, 119, 120	cycpm3cl2 33522	. . . . . 6 ⊢ (((𝜑 ∧ ¬ 𝐼 ∈ {𝐾, 𝐿}) ∧ 𝐽 ∈ {𝐾, 𝐿}) → (𝑀‘⟨“𝐽∪ ({𝐾, 𝐿} ∖ {𝐽})𝐼”⟩) ∈ (𝑀 “ (◡♯ “ {3})))
122	121, 83	eleqtrrdi 2876	. . . . 5 ⊢ (((𝜑 ∧ ¬ 𝐼 ∈ {𝐾, 𝐿}) ∧ 𝐽 ∈ {𝐾, 𝐿}) → (𝑀‘⟨“𝐽∪ ({𝐾, 𝐿} ∖ {𝐽})𝐼”⟩) ∈ 𝐶)
123	122	s1cld 14662	. . . 4 ⊢ (((𝜑 ∧ ¬ 𝐼 ∈ {𝐾, 𝐿}) ∧ 𝐽 ∈ {𝐾, 𝐿}) → ⟨“(𝑀‘⟨“𝐽∪ ({𝐾, 𝐿} ∖ {𝐽})𝐼”⟩)”⟩ ∈ Word 𝐶)
124		simpr 490	. . . . . 6 ⊢ ((((𝜑 ∧ ¬ 𝐼 ∈ {𝐾, 𝐿}) ∧ 𝐽 ∈ {𝐾, 𝐿}) ∧ 𝑐 = ⟨“(𝑀‘⟨“𝐽∪ ({𝐾, 𝐿} ∖ {𝐽})𝐼”⟩)”⟩) → 𝑐 = ⟨“(𝑀‘⟨“𝐽∪ ({𝐾, 𝐿} ∖ {𝐽})𝐼”⟩)”⟩)
125	124	oveq2d 7435	. . . . 5 ⊢ ((((𝜑 ∧ ¬ 𝐼 ∈ {𝐾, 𝐿}) ∧ 𝐽 ∈ {𝐾, 𝐿}) ∧ 𝑐 = ⟨“(𝑀‘⟨“𝐽∪ ({𝐾, 𝐿} ∖ {𝐽})𝐼”⟩)”⟩) → (𝑆 Σg 𝑐) = (𝑆 Σg ⟨“(𝑀‘⟨“𝐽∪ ({𝐾, 𝐿} ∖ {𝐽})𝐼”⟩)”⟩))
126	125	eqeq2d 2776	. . . 4 ⊢ ((((𝜑 ∧ ¬ 𝐼 ∈ {𝐾, 𝐿}) ∧ 𝐽 ∈ {𝐾, 𝐿}) ∧ 𝑐 = ⟨“(𝑀‘⟨“𝐽∪ ({𝐾, 𝐿} ∖ {𝐽})𝐼”⟩)”⟩) → ((𝐸 · 𝐹) = (𝑆 Σg 𝑐) ↔ (𝐸 · 𝐹) = (𝑆 Σg ⟨“(𝑀‘⟨“𝐽∪ ({𝐾, 𝐿} ∖ {𝐽})𝐼”⟩)”⟩)))
127	7, 12, 105, 106, 112, 113, 116, 119, 120, 22	cyc3co2 33526	. . . . 5 ⊢ (((𝜑 ∧ ¬ 𝐼 ∈ {𝐾, 𝐿}) ∧ 𝐽 ∈ {𝐾, 𝐿}) → (𝑀‘⟨“𝐽∪ ({𝐾, 𝐿} ∖ {𝐽})𝐼”⟩) = ((𝑀‘⟨“𝐽𝐼”⟩) · (𝑀‘⟨“𝐽∪ ({𝐾, 𝐿} ∖ {𝐽})”⟩)))
128	7, 12, 105, 106, 112, 113, 116, 119, 120	cycpm3cl 33521	. . . . . 6 ⊢ (((𝜑 ∧ ¬ 𝐼 ∈ {𝐾, 𝐿}) ∧ 𝐽 ∈ {𝐾, 𝐿}) → (𝑀‘⟨“𝐽∪ ({𝐾, 𝐿} ∖ {𝐽})𝐼”⟩) ∈ (Base‘𝑆))
129	21	gsumws1 18936	. . . . . 6 ⊢ ((𝑀‘⟨“𝐽∪ ({𝐾, 𝐿} ∖ {𝐽})𝐼”⟩) ∈ (Base‘𝑆) → (𝑆 Σg ⟨“(𝑀‘⟨“𝐽∪ ({𝐾, 𝐿} ∖ {𝐽})𝐼”⟩)”⟩) = (𝑀‘⟨“𝐽∪ ({𝐾, 𝐿} ∖ {𝐽})𝐼”⟩))
130	128, 129	syl 18	. . . . 5 ⊢ (((𝜑 ∧ ¬ 𝐼 ∈ {𝐾, 𝐿}) ∧ 𝐽 ∈ {𝐾, 𝐿}) → (𝑆 Σg ⟨“(𝑀‘⟨“𝐽∪ ({𝐾, 𝐿} ∖ {𝐽})𝐼”⟩)”⟩) = (𝑀‘⟨“𝐽∪ ({𝐾, 𝐿} ∖ {𝐽})𝐼”⟩))
131		prcom 4700	. . . . . . . . . 10 ⊢ {𝐼, 𝐽} = {𝐽, 𝐼}
132	131	fveq2i 6888	. . . . . . . . 9 ⊢ ((pmTrsp‘𝐷)‘{𝐼, 𝐽}) = ((pmTrsp‘𝐷)‘{𝐽, 𝐼})
133	7, 8, 10, 9, 80, 27	cycpm2tr 33505	. . . . . . . . 9 ⊢ (𝜑 → (𝑀‘⟨“𝐽𝐼”⟩) = ((pmTrsp‘𝐷)‘{𝐽, 𝐼}))
134	132, 28, 133	3eqtr4a 2826	. . . . . . . 8 ⊢ (𝜑 → (𝑀‘⟨“𝐼𝐽”⟩) = (𝑀‘⟨“𝐽𝐼”⟩))
135	6, 134	eqtrd 2800	. . . . . . 7 ⊢ (𝜑 → 𝐸 = (𝑀‘⟨“𝐽𝐼”⟩))
136	135	ad2antrr 739	. . . . . 6 ⊢ (((𝜑 ∧ ¬ 𝐼 ∈ {𝐾, 𝐿}) ∧ 𝐽 ∈ {𝐾, 𝐿}) → 𝐸 = (𝑀‘⟨“𝐽𝐼”⟩))
137		en2eleq 10008	. . . . . . . . 9 ⊢ ((𝐽 ∈ {𝐾, 𝐿} ∧ {𝐾, 𝐿} ≈ 2o) → {𝐾, 𝐿} = {𝐽, ∪ ({𝐾, 𝐿} ∖ {𝐽})})
138	108, 109, 137	syl2anc 596	. . . . . . . 8 ⊢ (((𝜑 ∧ ¬ 𝐼 ∈ {𝐾, 𝐿}) ∧ 𝐽 ∈ {𝐾, 𝐿}) → {𝐾, 𝐿} = {𝐽, ∪ ({𝐾, 𝐿} ∖ {𝐽})})
139	138	fveq2d 6889	. . . . . . 7 ⊢ (((𝜑 ∧ ¬ 𝐼 ∈ {𝐾, 𝐿}) ∧ 𝐽 ∈ {𝐾, 𝐿}) → ((pmTrsp‘𝐷)‘{𝐾, 𝐿}) = ((pmTrsp‘𝐷)‘{𝐽, ∪ ({𝐾, 𝐿} ∖ {𝐽})}))
140	97	ad2antrr 739	. . . . . . 7 ⊢ (((𝜑 ∧ ¬ 𝐼 ∈ {𝐾, 𝐿}) ∧ 𝐽 ∈ {𝐾, 𝐿}) → 𝐹 = ((pmTrsp‘𝐷)‘{𝐾, 𝐿}))
141	7, 105, 106, 112, 116, 27	cycpm2tr 33505	. . . . . . 7 ⊢ (((𝜑 ∧ ¬ 𝐼 ∈ {𝐾, 𝐿}) ∧ 𝐽 ∈ {𝐾, 𝐿}) → (𝑀‘⟨“𝐽∪ ({𝐾, 𝐿} ∖ {𝐽})”⟩) = ((pmTrsp‘𝐷)‘{𝐽, ∪ ({𝐾, 𝐿} ∖ {𝐽})}))
142	139, 140, 141	3eqtr4d 2810	. . . . . 6 ⊢ (((𝜑 ∧ ¬ 𝐼 ∈ {𝐾, 𝐿}) ∧ 𝐽 ∈ {𝐾, 𝐿}) → 𝐹 = (𝑀‘⟨“𝐽∪ ({𝐾, 𝐿} ∖ {𝐽})”⟩))
143	136, 142	oveq12d 7437	. . . . 5 ⊢ (((𝜑 ∧ ¬ 𝐼 ∈ {𝐾, 𝐿}) ∧ 𝐽 ∈ {𝐾, 𝐿}) → (𝐸 · 𝐹) = ((𝑀‘⟨“𝐽𝐼”⟩) · (𝑀‘⟨“𝐽∪ ({𝐾, 𝐿} ∖ {𝐽})”⟩)))
144	127, 130, 143	3eqtr4rd 2811	. . . 4 ⊢ (((𝜑 ∧ ¬ 𝐼 ∈ {𝐾, 𝐿}) ∧ 𝐽 ∈ {𝐾, 𝐿}) → (𝐸 · 𝐹) = (𝑆 Σg ⟨“(𝑀‘⟨“𝐽∪ ({𝐾, 𝐿} ∖ {𝐽})𝐼”⟩)”⟩))
145	123, 126, 144	rspcedvd 3585	. . 3 ⊢ (((𝜑 ∧ ¬ 𝐼 ∈ {𝐾, 𝐿}) ∧ 𝐽 ∈ {𝐾, 𝐿}) → ∃𝑐 ∈ Word 𝐶(𝐸 · 𝐹) = (𝑆 Σg 𝑐))
146	8	ad2antrr 739	. . . . . . 7 ⊢ (((𝜑 ∧ ¬ 𝐼 ∈ {𝐾, 𝐿}) ∧ ¬ 𝐽 ∈ {𝐾, 𝐿}) → 𝐷 ∈ 𝑉)
147	10	ad2antrr 739	. . . . . . 7 ⊢ (((𝜑 ∧ ¬ 𝐼 ∈ {𝐾, 𝐿}) ∧ ¬ 𝐽 ∈ {𝐾, 𝐿}) → 𝐽 ∈ 𝐷)
148	16	ad2antrr 739	. . . . . . 7 ⊢ (((𝜑 ∧ ¬ 𝐼 ∈ {𝐾, 𝐿}) ∧ ¬ 𝐽 ∈ {𝐾, 𝐿}) → 𝐾 ∈ 𝐷)
149	9	ad2antrr 739	. . . . . . 7 ⊢ (((𝜑 ∧ ¬ 𝐼 ∈ {𝐾, 𝐿}) ∧ ¬ 𝐽 ∈ {𝐾, 𝐿}) → 𝐼 ∈ 𝐷)
150		simpr 490	. . . . . . . 8 ⊢ (((𝜑 ∧ ¬ 𝐼 ∈ {𝐾, 𝐿}) ∧ ¬ 𝐽 ∈ {𝐾, 𝐿}) → ¬ 𝐽 ∈ {𝐾, 𝐿})
151	147, 150	nelpr1 4622	. . . . . . 7 ⊢ (((𝜑 ∧ ¬ 𝐼 ∈ {𝐾, 𝐿}) ∧ ¬ 𝐽 ∈ {𝐾, 𝐿}) → 𝐽 ≠ 𝐾)
152		prid1g 4728	. . . . . . . . . 10 ⊢ (𝐾 ∈ 𝐷 → 𝐾 ∈ {𝐾, 𝐿})
153	16, 152	syl 18	. . . . . . . . 9 ⊢ (𝜑 → 𝐾 ∈ {𝐾, 𝐿})
154	153	ad2antrr 739	. . . . . . . 8 ⊢ (((𝜑 ∧ ¬ 𝐼 ∈ {𝐾, 𝐿}) ∧ ¬ 𝐽 ∈ {𝐾, 𝐿}) → 𝐾 ∈ {𝐾, 𝐿})
155		simplr 781	. . . . . . . 8 ⊢ (((𝜑 ∧ ¬ 𝐼 ∈ {𝐾, 𝐿}) ∧ ¬ 𝐽 ∈ {𝐾, 𝐿}) → ¬ 𝐼 ∈ {𝐾, 𝐿})
156		nelne2 3058	. . . . . . . 8 ⊢ ((𝐾 ∈ {𝐾, 𝐿} ∧ ¬ 𝐼 ∈ {𝐾, 𝐿}) → 𝐾 ≠ 𝐼)
157	154, 155, 156	syl2anc 596	. . . . . . 7 ⊢ (((𝜑 ∧ ¬ 𝐼 ∈ {𝐾, 𝐿}) ∧ ¬ 𝐽 ∈ {𝐾, 𝐿}) → 𝐾 ≠ 𝐼)
158	11	ad2antrr 739	. . . . . . 7 ⊢ (((𝜑 ∧ ¬ 𝐼 ∈ {𝐾, 𝐿}) ∧ ¬ 𝐽 ∈ {𝐾, 𝐿}) → 𝐼 ≠ 𝐽)
159	7, 12, 146, 147, 148, 149, 151, 157, 158	cycpm3cl2 33522	. . . . . 6 ⊢ (((𝜑 ∧ ¬ 𝐼 ∈ {𝐾, 𝐿}) ∧ ¬ 𝐽 ∈ {𝐾, 𝐿}) → (𝑀‘⟨“𝐽𝐾𝐼”⟩) ∈ (𝑀 “ (◡♯ “ {3})))
160	159, 83	eleqtrrdi 2876	. . . . 5 ⊢ (((𝜑 ∧ ¬ 𝐼 ∈ {𝐾, 𝐿}) ∧ ¬ 𝐽 ∈ {𝐾, 𝐿}) → (𝑀‘⟨“𝐽𝐾𝐼”⟩) ∈ 𝐶)
161	17	ad2antrr 739	. . . . . . 7 ⊢ (((𝜑 ∧ ¬ 𝐼 ∈ {𝐾, 𝐿}) ∧ ¬ 𝐽 ∈ {𝐾, 𝐿}) → 𝐿 ∈ 𝐷)
162	18	ad2antrr 739	. . . . . . 7 ⊢ (((𝜑 ∧ ¬ 𝐼 ∈ {𝐾, 𝐿}) ∧ ¬ 𝐽 ∈ {𝐾, 𝐿}) → 𝐾 ≠ 𝐿)
163		prid2g 4729	. . . . . . . . 9 ⊢ (𝐿 ∈ 𝐷 → 𝐿 ∈ {𝐾, 𝐿})
164	161, 163	syl 18	. . . . . . . 8 ⊢ (((𝜑 ∧ ¬ 𝐼 ∈ {𝐾, 𝐿}) ∧ ¬ 𝐽 ∈ {𝐾, 𝐿}) → 𝐿 ∈ {𝐾, 𝐿})
165		nelne2 3058	. . . . . . . 8 ⊢ ((𝐿 ∈ {𝐾, 𝐿} ∧ ¬ 𝐽 ∈ {𝐾, 𝐿}) → 𝐿 ≠ 𝐽)
166	164, 165	sylancom 600	. . . . . . 7 ⊢ (((𝜑 ∧ ¬ 𝐼 ∈ {𝐾, 𝐿}) ∧ ¬ 𝐽 ∈ {𝐾, 𝐿}) → 𝐿 ≠ 𝐽)
167	7, 12, 146, 148, 161, 147, 162, 166, 151	cycpm3cl2 33522	. . . . . 6 ⊢ (((𝜑 ∧ ¬ 𝐼 ∈ {𝐾, 𝐿}) ∧ ¬ 𝐽 ∈ {𝐾, 𝐿}) → (𝑀‘⟨“𝐾𝐿𝐽”⟩) ∈ (𝑀 “ (◡♯ “ {3})))
168	167, 83	eleqtrrdi 2876	. . . . 5 ⊢ (((𝜑 ∧ ¬ 𝐼 ∈ {𝐾, 𝐿}) ∧ ¬ 𝐽 ∈ {𝐾, 𝐿}) → (𝑀‘⟨“𝐾𝐿𝐽”⟩) ∈ 𝐶)
169	160, 168	s2cld 14934	. . . 4 ⊢ (((𝜑 ∧ ¬ 𝐼 ∈ {𝐾, 𝐿}) ∧ ¬ 𝐽 ∈ {𝐾, 𝐿}) → ⟨“(𝑀‘⟨“𝐽𝐾𝐼”⟩)(𝑀‘⟨“𝐾𝐿𝐽”⟩)”⟩ ∈ Word 𝐶)
170		simpr 490	. . . . . 6 ⊢ ((((𝜑 ∧ ¬ 𝐼 ∈ {𝐾, 𝐿}) ∧ ¬ 𝐽 ∈ {𝐾, 𝐿}) ∧ 𝑐 = ⟨“(𝑀‘⟨“𝐽𝐾𝐼”⟩)(𝑀‘⟨“𝐾𝐿𝐽”⟩)”⟩) → 𝑐 = ⟨“(𝑀‘⟨“𝐽𝐾𝐼”⟩)(𝑀‘⟨“𝐾𝐿𝐽”⟩)”⟩)
171	170	oveq2d 7435	. . . . 5 ⊢ ((((𝜑 ∧ ¬ 𝐼 ∈ {𝐾, 𝐿}) ∧ ¬ 𝐽 ∈ {𝐾, 𝐿}) ∧ 𝑐 = ⟨“(𝑀‘⟨“𝐽𝐾𝐼”⟩)(𝑀‘⟨“𝐾𝐿𝐽”⟩)”⟩) → (𝑆 Σg 𝑐) = (𝑆 Σg ⟨“(𝑀‘⟨“𝐽𝐾𝐼”⟩)(𝑀‘⟨“𝐾𝐿𝐽”⟩)”⟩))
172	171	eqeq2d 2776	. . . 4 ⊢ ((((𝜑 ∧ ¬ 𝐼 ∈ {𝐾, 𝐿}) ∧ ¬ 𝐽 ∈ {𝐾, 𝐿}) ∧ 𝑐 = ⟨“(𝑀‘⟨“𝐽𝐾𝐼”⟩)(𝑀‘⟨“𝐾𝐿𝐽”⟩)”⟩) → ((𝐸 · 𝐹) = (𝑆 Σg 𝑐) ↔ (𝐸 · 𝐹) = (𝑆 Σg ⟨“(𝑀‘⟨“𝐽𝐾𝐼”⟩)(𝑀‘⟨“𝐾𝐿𝐽”⟩)”⟩)))
173	146, 56	syl 18	. . . . . . . . . 10 ⊢ (((𝜑 ∧ ¬ 𝐼 ∈ {𝐾, 𝐿}) ∧ ¬ 𝐽 ∈ {𝐾, 𝐿}) → ( I ↾ 𝐷) = (0g‘𝑆))
174	173	oveq1d 7434	. . . . . . . . 9 ⊢ (((𝜑 ∧ ¬ 𝐼 ∈ {𝐾, 𝐿}) ∧ ¬ 𝐽 ∈ {𝐾, 𝐿}) → (( I ↾ 𝐷) · (𝑀‘⟨“𝐾𝐿”⟩)) = ((0g‘𝑆) · (𝑀‘⟨“𝐾𝐿”⟩)))
175	12	symggrp 19516	. . . . . . . . . . . 12 ⊢ (𝐷 ∈ 𝑉 → 𝑆 ∈ Grp)
176	8, 175	syl 18	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑆 ∈ Grp)
177	176	ad2antrr 739	. . . . . . . . . 10 ⊢ (((𝜑 ∧ ¬ 𝐼 ∈ {𝐾, 𝐿}) ∧ ¬ 𝐽 ∈ {𝐾, 𝐿}) → 𝑆 ∈ Grp)
178	19	ad2antrr 739	. . . . . . . . . 10 ⊢ (((𝜑 ∧ ¬ 𝐼 ∈ {𝐾, 𝐿}) ∧ ¬ 𝐽 ∈ {𝐾, 𝐿}) → (𝑀‘⟨“𝐾𝐿”⟩) ∈ (Base‘𝑆))
179	21, 22, 58	grplid 19080	. . . . . . . . . 10 ⊢ ((𝑆 ∈ Grp ∧ (𝑀‘⟨“𝐾𝐿”⟩) ∈ (Base‘𝑆)) → ((0g‘𝑆) · (𝑀‘⟨“𝐾𝐿”⟩)) = (𝑀‘⟨“𝐾𝐿”⟩))
180	177, 178, 179	syl2anc 596	. . . . . . . . 9 ⊢ (((𝜑 ∧ ¬ 𝐼 ∈ {𝐾, 𝐿}) ∧ ¬ 𝐽 ∈ {𝐾, 𝐿}) → ((0g‘𝑆) · (𝑀‘⟨“𝐾𝐿”⟩)) = (𝑀‘⟨“𝐾𝐿”⟩))
181	174, 180	eqtrd 2800	. . . . . . . 8 ⊢ (((𝜑 ∧ ¬ 𝐼 ∈ {𝐾, 𝐿}) ∧ ¬ 𝐽 ∈ {𝐾, 𝐿}) → (( I ↾ 𝐷) · (𝑀‘⟨“𝐾𝐿”⟩)) = (𝑀‘⟨“𝐾𝐿”⟩))
182	181	oveq2d 7435	. . . . . . 7 ⊢ (((𝜑 ∧ ¬ 𝐼 ∈ {𝐾, 𝐿}) ∧ ¬ 𝐽 ∈ {𝐾, 𝐿}) → ((𝑀‘⟨“𝐼𝐽”⟩) · (( I ↾ 𝐷) · (𝑀‘⟨“𝐾𝐿”⟩))) = ((𝑀‘⟨“𝐼𝐽”⟩) · (𝑀‘⟨“𝐾𝐿”⟩)))
183	13	ad2antrr 739	. . . . . . . . 9 ⊢ (((𝜑 ∧ ¬ 𝐼 ∈ {𝐾, 𝐿}) ∧ ¬ 𝐽 ∈ {𝐾, 𝐿}) → (𝑀‘⟨“𝐼𝐽”⟩) ∈ (Base‘𝑆))
184	7, 146, 147, 148, 151, 27	cycpm2tr 33505	. . . . . . . . . 10 ⊢ (((𝜑 ∧ ¬ 𝐼 ∈ {𝐾, 𝐿}) ∧ ¬ 𝐽 ∈ {𝐾, 𝐿}) → (𝑀‘⟨“𝐽𝐾”⟩) = ((pmTrsp‘𝐷)‘{𝐽, 𝐾}))
185	50, 12, 21	symgtrf 19585	. . . . . . . . . . 11 ⊢ ran (pmTrsp‘𝐷) ⊆ (Base‘𝑆)
186	10, 16	prssd 4790	. . . . . . . . . . . . 13 ⊢ (𝜑 → {𝐽, 𝐾} ⊆ 𝐷)
187	186	ad2antrr 739	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ ¬ 𝐼 ∈ {𝐾, 𝐿}) ∧ ¬ 𝐽 ∈ {𝐾, 𝐿}) → {𝐽, 𝐾} ⊆ 𝐷)
188		enpr2 10004	. . . . . . . . . . . . 13 ⊢ ((𝐽 ∈ 𝐷 ∧ 𝐾 ∈ 𝐷 ∧ 𝐽 ≠ 𝐾) → {𝐽, 𝐾} ≈ 2o)
189	147, 148, 151, 188	syl3anc 1398	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ ¬ 𝐼 ∈ {𝐾, 𝐿}) ∧ ¬ 𝐽 ∈ {𝐾, 𝐿}) → {𝐽, 𝐾} ≈ 2o)
190	27, 50	pmtrrn 19573	. . . . . . . . . . . 12 ⊢ ((𝐷 ∈ 𝑉 ∧ {𝐽, 𝐾} ⊆ 𝐷 ∧ {𝐽, 𝐾} ≈ 2o) → ((pmTrsp‘𝐷)‘{𝐽, 𝐾}) ∈ ran (pmTrsp‘𝐷))
191	146, 187, 189, 190	syl3anc 1398	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ ¬ 𝐼 ∈ {𝐾, 𝐿}) ∧ ¬ 𝐽 ∈ {𝐾, 𝐿}) → ((pmTrsp‘𝐷)‘{𝐽, 𝐾}) ∈ ran (pmTrsp‘𝐷))
192	185, 191	sselid 3936	. . . . . . . . . 10 ⊢ (((𝜑 ∧ ¬ 𝐼 ∈ {𝐾, 𝐿}) ∧ ¬ 𝐽 ∈ {𝐾, 𝐿}) → ((pmTrsp‘𝐷)‘{𝐽, 𝐾}) ∈ (Base‘𝑆))
193	184, 192	eqeltrd 2865	. . . . . . . . 9 ⊢ (((𝜑 ∧ ¬ 𝐼 ∈ {𝐾, 𝐿}) ∧ ¬ 𝐽 ∈ {𝐾, 𝐿}) → (𝑀‘⟨“𝐽𝐾”⟩) ∈ (Base‘𝑆))
194	151	necomd 3015	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ ¬ 𝐼 ∈ {𝐾, 𝐿}) ∧ ¬ 𝐽 ∈ {𝐾, 𝐿}) → 𝐾 ≠ 𝐽)
195	7, 146, 148, 147, 194, 27	cycpm2tr 33505	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ ¬ 𝐼 ∈ {𝐾, 𝐿}) ∧ ¬ 𝐽 ∈ {𝐾, 𝐿}) → (𝑀‘⟨“𝐾𝐽”⟩) = ((pmTrsp‘𝐷)‘{𝐾, 𝐽}))
196		prcom 4700	. . . . . . . . . . . . . 14 ⊢ {𝐽, 𝐾} = {𝐾, 𝐽}
197	196	a1i 11	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ ¬ 𝐼 ∈ {𝐾, 𝐿}) ∧ ¬ 𝐽 ∈ {𝐾, 𝐿}) → {𝐽, 𝐾} = {𝐾, 𝐽})
198	197	fveq2d 6889	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ ¬ 𝐼 ∈ {𝐾, 𝐿}) ∧ ¬ 𝐽 ∈ {𝐾, 𝐿}) → ((pmTrsp‘𝐷)‘{𝐽, 𝐾}) = ((pmTrsp‘𝐷)‘{𝐾, 𝐽}))
199	195, 198	eqtr4d 2803	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ ¬ 𝐼 ∈ {𝐾, 𝐿}) ∧ ¬ 𝐽 ∈ {𝐾, 𝐿}) → (𝑀‘⟨“𝐾𝐽”⟩) = ((pmTrsp‘𝐷)‘{𝐽, 𝐾}))
200	199, 192	eqeltrd 2865	. . . . . . . . . 10 ⊢ (((𝜑 ∧ ¬ 𝐼 ∈ {𝐾, 𝐿}) ∧ ¬ 𝐽 ∈ {𝐾, 𝐿}) → (𝑀‘⟨“𝐾𝐽”⟩) ∈ (Base‘𝑆))
201	21, 22	grpcl 19054	. . . . . . . . . 10 ⊢ ((𝑆 ∈ Grp ∧ (𝑀‘⟨“𝐾𝐽”⟩) ∈ (Base‘𝑆) ∧ (𝑀‘⟨“𝐾𝐿”⟩) ∈ (Base‘𝑆)) → ((𝑀‘⟨“𝐾𝐽”⟩) · (𝑀‘⟨“𝐾𝐿”⟩)) ∈ (Base‘𝑆))
202	177, 200, 178, 201	syl3anc 1398	. . . . . . . . 9 ⊢ (((𝜑 ∧ ¬ 𝐼 ∈ {𝐾, 𝐿}) ∧ ¬ 𝐽 ∈ {𝐾, 𝐿}) → ((𝑀‘⟨“𝐾𝐽”⟩) · (𝑀‘⟨“𝐾𝐿”⟩)) ∈ (Base‘𝑆))
203	21, 22	grpass 19055	. . . . . . . . 9 ⊢ ((𝑆 ∈ Grp ∧ ((𝑀‘⟨“𝐼𝐽”⟩) ∈ (Base‘𝑆) ∧ (𝑀‘⟨“𝐽𝐾”⟩) ∈ (Base‘𝑆) ∧ ((𝑀‘⟨“𝐾𝐽”⟩) · (𝑀‘⟨“𝐾𝐿”⟩)) ∈ (Base‘𝑆))) → (((𝑀‘⟨“𝐼𝐽”⟩) · (𝑀‘⟨“𝐽𝐾”⟩)) · ((𝑀‘⟨“𝐾𝐽”⟩) · (𝑀‘⟨“𝐾𝐿”⟩))) = ((𝑀‘⟨“𝐼𝐽”⟩) · ((𝑀‘⟨“𝐽𝐾”⟩) · ((𝑀‘⟨“𝐾𝐽”⟩) · (𝑀‘⟨“𝐾𝐿”⟩)))))
204	177, 183, 193, 202, 203	syl13anc 1399	. . . . . . . 8 ⊢ (((𝜑 ∧ ¬ 𝐼 ∈ {𝐾, 𝐿}) ∧ ¬ 𝐽 ∈ {𝐾, 𝐿}) → (((𝑀‘⟨“𝐼𝐽”⟩) · (𝑀‘⟨“𝐽𝐾”⟩)) · ((𝑀‘⟨“𝐾𝐽”⟩) · (𝑀‘⟨“𝐾𝐿”⟩))) = ((𝑀‘⟨“𝐼𝐽”⟩) · ((𝑀‘⟨“𝐽𝐾”⟩) · ((𝑀‘⟨“𝐾𝐽”⟩) · (𝑀‘⟨“𝐾𝐿”⟩)))))
205	21, 22	grpass 19055	. . . . . . . . . 10 ⊢ ((𝑆 ∈ Grp ∧ ((𝑀‘⟨“𝐽𝐾”⟩) ∈ (Base‘𝑆) ∧ (𝑀‘⟨“𝐾𝐽”⟩) ∈ (Base‘𝑆) ∧ (𝑀‘⟨“𝐾𝐿”⟩) ∈ (Base‘𝑆))) → (((𝑀‘⟨“𝐽𝐾”⟩) · (𝑀‘⟨“𝐾𝐽”⟩)) · (𝑀‘⟨“𝐾𝐿”⟩)) = ((𝑀‘⟨“𝐽𝐾”⟩) · ((𝑀‘⟨“𝐾𝐽”⟩) · (𝑀‘⟨“𝐾𝐿”⟩))))
206	177, 193, 200, 178, 205	syl13anc 1399	. . . . . . . . 9 ⊢ (((𝜑 ∧ ¬ 𝐼 ∈ {𝐾, 𝐿}) ∧ ¬ 𝐽 ∈ {𝐾, 𝐿}) → (((𝑀‘⟨“𝐽𝐾”⟩) · (𝑀‘⟨“𝐾𝐽”⟩)) · (𝑀‘⟨“𝐾𝐿”⟩)) = ((𝑀‘⟨“𝐽𝐾”⟩) · ((𝑀‘⟨“𝐾𝐽”⟩) · (𝑀‘⟨“𝐾𝐿”⟩))))
207	206	oveq2d 7435	. . . . . . . 8 ⊢ (((𝜑 ∧ ¬ 𝐼 ∈ {𝐾, 𝐿}) ∧ ¬ 𝐽 ∈ {𝐾, 𝐿}) → ((𝑀‘⟨“𝐼𝐽”⟩) · (((𝑀‘⟨“𝐽𝐾”⟩) · (𝑀‘⟨“𝐾𝐽”⟩)) · (𝑀‘⟨“𝐾𝐿”⟩))) = ((𝑀‘⟨“𝐼𝐽”⟩) · ((𝑀‘⟨“𝐽𝐾”⟩) · ((𝑀‘⟨“𝐾𝐽”⟩) · (𝑀‘⟨“𝐾𝐿”⟩)))))
208	184, 199	oveq12d 7437	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ ¬ 𝐼 ∈ {𝐾, 𝐿}) ∧ ¬ 𝐽 ∈ {𝐾, 𝐿}) → ((𝑀‘⟨“𝐽𝐾”⟩) · (𝑀‘⟨“𝐾𝐽”⟩)) = (((pmTrsp‘𝐷)‘{𝐽, 𝐾}) · ((pmTrsp‘𝐷)‘{𝐽, 𝐾})))
209	12, 21, 22	symgov 19500	. . . . . . . . . . . 12 ⊢ ((((pmTrsp‘𝐷)‘{𝐽, 𝐾}) ∈ (Base‘𝑆) ∧ ((pmTrsp‘𝐷)‘{𝐽, 𝐾}) ∈ (Base‘𝑆)) → (((pmTrsp‘𝐷)‘{𝐽, 𝐾}) · ((pmTrsp‘𝐷)‘{𝐽, 𝐾})) = (((pmTrsp‘𝐷)‘{𝐽, 𝐾}) ∘ ((pmTrsp‘𝐷)‘{𝐽, 𝐾})))
210	192, 192, 209	syl2anc 596	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ ¬ 𝐼 ∈ {𝐾, 𝐿}) ∧ ¬ 𝐽 ∈ {𝐾, 𝐿}) → (((pmTrsp‘𝐷)‘{𝐽, 𝐾}) · ((pmTrsp‘𝐷)‘{𝐽, 𝐾})) = (((pmTrsp‘𝐷)‘{𝐽, 𝐾}) ∘ ((pmTrsp‘𝐷)‘{𝐽, 𝐾})))
211	27, 50	pmtrfinv 19577	. . . . . . . . . . . 12 ⊢ (((pmTrsp‘𝐷)‘{𝐽, 𝐾}) ∈ ran (pmTrsp‘𝐷) → (((pmTrsp‘𝐷)‘{𝐽, 𝐾}) ∘ ((pmTrsp‘𝐷)‘{𝐽, 𝐾})) = ( I ↾ 𝐷))
212	191, 211	syl 18	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ ¬ 𝐼 ∈ {𝐾, 𝐿}) ∧ ¬ 𝐽 ∈ {𝐾, 𝐿}) → (((pmTrsp‘𝐷)‘{𝐽, 𝐾}) ∘ ((pmTrsp‘𝐷)‘{𝐽, 𝐾})) = ( I ↾ 𝐷))
213	208, 210, 212	3eqtrd 2804	. . . . . . . . . 10 ⊢ (((𝜑 ∧ ¬ 𝐼 ∈ {𝐾, 𝐿}) ∧ ¬ 𝐽 ∈ {𝐾, 𝐿}) → ((𝑀‘⟨“𝐽𝐾”⟩) · (𝑀‘⟨“𝐾𝐽”⟩)) = ( I ↾ 𝐷))
214	213	oveq1d 7434	. . . . . . . . 9 ⊢ (((𝜑 ∧ ¬ 𝐼 ∈ {𝐾, 𝐿}) ∧ ¬ 𝐽 ∈ {𝐾, 𝐿}) → (((𝑀‘⟨“𝐽𝐾”⟩) · (𝑀‘⟨“𝐾𝐽”⟩)) · (𝑀‘⟨“𝐾𝐿”⟩)) = (( I ↾ 𝐷) · (𝑀‘⟨“𝐾𝐿”⟩)))
215	214	oveq2d 7435	. . . . . . . 8 ⊢ (((𝜑 ∧ ¬ 𝐼 ∈ {𝐾, 𝐿}) ∧ ¬ 𝐽 ∈ {𝐾, 𝐿}) → ((𝑀‘⟨“𝐼𝐽”⟩) · (((𝑀‘⟨“𝐽𝐾”⟩) · (𝑀‘⟨“𝐾𝐽”⟩)) · (𝑀‘⟨“𝐾𝐿”⟩))) = ((𝑀‘⟨“𝐼𝐽”⟩) · (( I ↾ 𝐷) · (𝑀‘⟨“𝐾𝐿”⟩))))
216	204, 207, 215	3eqtr2rd 2807	. . . . . . 7 ⊢ (((𝜑 ∧ ¬ 𝐼 ∈ {𝐾, 𝐿}) ∧ ¬ 𝐽 ∈ {𝐾, 𝐿}) → ((𝑀‘⟨“𝐼𝐽”⟩) · (( I ↾ 𝐷) · (𝑀‘⟨“𝐾𝐿”⟩))) = (((𝑀‘⟨“𝐼𝐽”⟩) · (𝑀‘⟨“𝐽𝐾”⟩)) · ((𝑀‘⟨“𝐾𝐽”⟩) · (𝑀‘⟨“𝐾𝐿”⟩))))
217	182, 216	eqtr3d 2802	. . . . . 6 ⊢ (((𝜑 ∧ ¬ 𝐼 ∈ {𝐾, 𝐿}) ∧ ¬ 𝐽 ∈ {𝐾, 𝐿}) → ((𝑀‘⟨“𝐼𝐽”⟩) · (𝑀‘⟨“𝐾𝐿”⟩)) = (((𝑀‘⟨“𝐼𝐽”⟩) · (𝑀‘⟨“𝐽𝐾”⟩)) · ((𝑀‘⟨“𝐾𝐽”⟩) · (𝑀‘⟨“𝐾𝐿”⟩))))
218	6, 15	oveq12d 7437	. . . . . . 7 ⊢ (𝜑 → (𝐸 · 𝐹) = ((𝑀‘⟨“𝐼𝐽”⟩) · (𝑀‘⟨“𝐾𝐿”⟩)))
219	218	ad2antrr 739	. . . . . 6 ⊢ (((𝜑 ∧ ¬ 𝐼 ∈ {𝐾, 𝐿}) ∧ ¬ 𝐽 ∈ {𝐾, 𝐿}) → (𝐸 · 𝐹) = ((𝑀‘⟨“𝐼𝐽”⟩) · (𝑀‘⟨“𝐾𝐿”⟩)))
220	7, 12, 146, 147, 148, 149, 151, 157, 158, 22	cyc3co2 33526	. . . . . . . 8 ⊢ (((𝜑 ∧ ¬ 𝐼 ∈ {𝐾, 𝐿}) ∧ ¬ 𝐽 ∈ {𝐾, 𝐿}) → (𝑀‘⟨“𝐽𝐾𝐼”⟩) = ((𝑀‘⟨“𝐽𝐼”⟩) · (𝑀‘⟨“𝐽𝐾”⟩)))
221	134	oveq1d 7434	. . . . . . . . 9 ⊢ (𝜑 → ((𝑀‘⟨“𝐼𝐽”⟩) · (𝑀‘⟨“𝐽𝐾”⟩)) = ((𝑀‘⟨“𝐽𝐼”⟩) · (𝑀‘⟨“𝐽𝐾”⟩)))
222	221	ad2antrr 739	. . . . . . . 8 ⊢ (((𝜑 ∧ ¬ 𝐼 ∈ {𝐾, 𝐿}) ∧ ¬ 𝐽 ∈ {𝐾, 𝐿}) → ((𝑀‘⟨“𝐼𝐽”⟩) · (𝑀‘⟨“𝐽𝐾”⟩)) = ((𝑀‘⟨“𝐽𝐼”⟩) · (𝑀‘⟨“𝐽𝐾”⟩)))
223	220, 222	eqtr4d 2803	. . . . . . 7 ⊢ (((𝜑 ∧ ¬ 𝐼 ∈ {𝐾, 𝐿}) ∧ ¬ 𝐽 ∈ {𝐾, 𝐿}) → (𝑀‘⟨“𝐽𝐾𝐼”⟩) = ((𝑀‘⟨“𝐼𝐽”⟩) · (𝑀‘⟨“𝐽𝐾”⟩)))
224	7, 12, 146, 148, 161, 147, 162, 166, 151, 22	cyc3co2 33526	. . . . . . 7 ⊢ (((𝜑 ∧ ¬ 𝐼 ∈ {𝐾, 𝐿}) ∧ ¬ 𝐽 ∈ {𝐾, 𝐿}) → (𝑀‘⟨“𝐾𝐿𝐽”⟩) = ((𝑀‘⟨“𝐾𝐽”⟩) · (𝑀‘⟨“𝐾𝐿”⟩)))
225	223, 224	oveq12d 7437	. . . . . 6 ⊢ (((𝜑 ∧ ¬ 𝐼 ∈ {𝐾, 𝐿}) ∧ ¬ 𝐽 ∈ {𝐾, 𝐿}) → ((𝑀‘⟨“𝐽𝐾𝐼”⟩) · (𝑀‘⟨“𝐾𝐿𝐽”⟩)) = (((𝑀‘⟨“𝐼𝐽”⟩) · (𝑀‘⟨“𝐽𝐾”⟩)) · ((𝑀‘⟨“𝐾𝐽”⟩) · (𝑀‘⟨“𝐾𝐿”⟩))))
226	217, 219, 225	3eqtr4d 2810	. . . . 5 ⊢ (((𝜑 ∧ ¬ 𝐼 ∈ {𝐾, 𝐿}) ∧ ¬ 𝐽 ∈ {𝐾, 𝐿}) → (𝐸 · 𝐹) = ((𝑀‘⟨“𝐽𝐾𝐼”⟩) · (𝑀‘⟨“𝐾𝐿𝐽”⟩)))
227	176	grpmndd 19059	. . . . . . 7 ⊢ (𝜑 → 𝑆 ∈ Mnd)
228	227	ad2antrr 739	. . . . . 6 ⊢ (((𝜑 ∧ ¬ 𝐼 ∈ {𝐾, 𝐿}) ∧ ¬ 𝐽 ∈ {𝐾, 𝐿}) → 𝑆 ∈ Mnd)
229	7, 12, 146, 147, 148, 149, 151, 157, 158	cycpm3cl 33521	. . . . . 6 ⊢ (((𝜑 ∧ ¬ 𝐼 ∈ {𝐾, 𝐿}) ∧ ¬ 𝐽 ∈ {𝐾, 𝐿}) → (𝑀‘⟨“𝐽𝐾𝐼”⟩) ∈ (Base‘𝑆))
230	224, 202	eqeltrd 2865	. . . . . 6 ⊢ (((𝜑 ∧ ¬ 𝐼 ∈ {𝐾, 𝐿}) ∧ ¬ 𝐽 ∈ {𝐾, 𝐿}) → (𝑀‘⟨“𝐾𝐿𝐽”⟩) ∈ (Base‘𝑆))
231	21, 22	gsumws2 18940	. . . . . 6 ⊢ ((𝑆 ∈ Mnd ∧ (𝑀‘⟨“𝐽𝐾𝐼”⟩) ∈ (Base‘𝑆) ∧ (𝑀‘⟨“𝐾𝐿𝐽”⟩) ∈ (Base‘𝑆)) → (𝑆 Σg ⟨“(𝑀‘⟨“𝐽𝐾𝐼”⟩)(𝑀‘⟨“𝐾𝐿𝐽”⟩)”⟩) = ((𝑀‘⟨“𝐽𝐾𝐼”⟩) · (𝑀‘⟨“𝐾𝐿𝐽”⟩)))
232	228, 229, 230, 231	syl3anc 1398	. . . . 5 ⊢ (((𝜑 ∧ ¬ 𝐼 ∈ {𝐾, 𝐿}) ∧ ¬ 𝐽 ∈ {𝐾, 𝐿}) → (𝑆 Σg ⟨“(𝑀‘⟨“𝐽𝐾𝐼”⟩)(𝑀‘⟨“𝐾𝐿𝐽”⟩)”⟩) = ((𝑀‘⟨“𝐽𝐾𝐼”⟩) · (𝑀‘⟨“𝐾𝐿𝐽”⟩)))
233	226, 232	eqtr4d 2803	. . . 4 ⊢ (((𝜑 ∧ ¬ 𝐼 ∈ {𝐾, 𝐿}) ∧ ¬ 𝐽 ∈ {𝐾, 𝐿}) → (𝐸 · 𝐹) = (𝑆 Σg ⟨“(𝑀‘⟨“𝐽𝐾𝐼”⟩)(𝑀‘⟨“𝐾𝐿𝐽”⟩)”⟩))
234	169, 172, 233	rspcedvd 3585	. . 3 ⊢ (((𝜑 ∧ ¬ 𝐼 ∈ {𝐾, 𝐿}) ∧ ¬ 𝐽 ∈ {𝐾, 𝐿}) → ∃𝑐 ∈ Word 𝐶(𝐸 · 𝐹) = (𝑆 Σg 𝑐))
235	145, 234	pm2.61dan 825	. 2 ⊢ ((𝜑 ∧ ¬ 𝐼 ∈ {𝐾, 𝐿}) → ∃𝑐 ∈ Word 𝐶(𝐸 · 𝐹) = (𝑆 Σg 𝑐))
236	104, 235	pm2.61dan 825	1 ⊢ (𝜑 → ∃𝑐 ∈ Word 𝐶(𝐸 · 𝐹) = (𝑆 Σg 𝑐))

This proof depends on syntax axioms:  ¬ wn 3   → wi 4   ∧ wa 401   ∧ w3a 1103   = wceq 1570   ∈ wcel 2146   ≠ wne 2960  ∃wrex 3091   ∖ cdif 3903   ⊆ wss 3906  ∅c0 4286  {csn 4591  {cpr 4593  ∪ cuni 4874   class class class wbr 5111   I cid 5557  ^◡ccnv 5662  ran crn 5664   ↾ cres 5665   “ cima 5666   ∘ ccom 5667  ‘cfv 6540  (class class class)co 7419  2_oc2o 8453   ≈ cen 8946  3c3 12313  ♯chash 14386  Word cword 14570  ⟨“cs1 14654  ⟨“cs2 14904  ⟨“cs3 14905  Basecbs 17293  +_gcplusg 17334  0_gc0g 17516   Σ_g cgsu 17517  Mndcmnd 18826  Grpcgrp 19046  SymGrpcsymg 19485  pmTrspcpmtr 19557  pmEvencevpm 19606  toCycctocyc 33492

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2148  ax-9 2156  ax-10 2179  ax-11 2195  ax-12 2216  ax-ext 2737  ax-rep 5240  ax-sep 5259  ax-nul 5271  ax-pow 5338  ax-pr 5406  ax-un 7742  ax-reg 9561  ax-ac2 10462  ax-cnex 11173  ax-resscn 11174  ax-1cn 11175  ax-icn 11176  ax-addcl 11177  ax-addrcl 11178  ax-mulcl 11179  ax-mulrcl 11180  ax-mulcom 11181  ax-addass 11182  ax-mulass 11183  ax-distr 11184  ax-i2m1 11185  ax-1ne0 11186  ax-1rid 11187  ax-rnegex 11188  ax-rrecex 11189  ax-cnre 11190  ax-pre-lttri 11191  ax-pre-lttrn 11192  ax-pre-ltadd 11193  ax-pre-mulgt0 11194  ax-pre-sup 11195

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2100  df-mo 2569  df-eu 2599  df-clab 2744  df-cleq 2757  df-clel 2840  df-nfc 2914  df-ne 2961  df-nel 3067  df-ral 3082  df-rex 3092  df-rmo 3371  df-reu 3372  df-rab 3419  df-v 3459  df-sbc 3747  df-csb 3855  df-dif 3909  df-un 3911  df-in 3913  df-ss 3923  df-pss 3926  df-nul 4287  df-if 4490  df-pw 4566  df-sn 4592  df-pr 4594  df-tp 4596  df-op 4598  df-uni 4875  df-int 4915  df-iun 4960  df-br 5112  df-opab 5176  df-mpt 5195  df-tr 5221  df-id 5558  df-eprel 5563  df-po 5571  df-so 5572  df-fr 5616  df-se 5617  df-we 5618  df-xp 5669  df-rel 5670  df-cnv 5671  df-co 5672  df-dm 5673  df-rn 5674  df-res 5675  df-ima 5676  df-pred 6306  df-ord 6367  df-on 6368  df-lim 6369  df-suc 6370  df-iota 6496  df-fun 6542  df-fn 6543  df-f 6544  df-f1 6545  df-fo 6546  df-f1o 6547  df-fv 6548  df-isom 6549  df-riota 7376  df-ov 7422  df-oprab 7423  df-mpo 7424  df-om 7869  df-1st 7992  df-2nd 7993  df-frecs 8284  df-wrecs 8315  df-recs 8364  df-rdg 8403  df-1o 8459  df-2o 8460  df-er 8700  df-map 8832  df-en 8950  df-dom 8951  df-sdom 8952  df-fin 8953  df-sup 9409  df-inf 9410  df-card 9941  df-ac 10116  df-pnf 11262  df-mnf 11263  df-xr 11264  df-ltxr 11265  df-le 11266  df-sub 11460  df-neg 11461  df-div 11889  df-nn 12251  df-2 12320  df-3 12321  df-4 12322  df-5 12323  df-6 12324  df-7 12325  df-8 12326  df-9 12327  df-n0 12522  df-xnn0 12595  df-z 12609  df-uz 12881  df-rp 13035  df-fz 13554  df-fzo 13702  df-fl 13845  df-mod 13923  df-seq 14058  df-hash 14387  df-word 14571  df-concat 14628  df-s1 14655  df-substr 14701  df-pfx 14733  df-csh 14852  df-s2 14911  df-s3 14912  df-struct 17231  df-sets 17248  df-slot 17266  df-ndx 17278  df-base 17294  df-ress 17315  df-plusg 17347  df-tset 17353  df-0g 17518  df-gsum 17519  df-mgm 18722  df-sgrp 18811  df-mnd 18827  df-submnd 18881  df-efmnd 18967  df-grp 19049  df-symg 19486  df-pmtr 19558  df-tocyc 33493

This theorem is used by:  cyc3genpm  33538