Theorem cyc3genpmlem 32000

Description: Lemma for cyc3genpm 32001. (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 14427	. . . . 5 ⊢ ∅ ∈ Word 𝐶
2	1	a1i 11	. . . 4 ⊢ (((𝜑 ∧ 𝐼 ∈ {𝐾, 𝐿}) ∧ 𝐽 ∈ {𝐾, 𝐿}) → ∅ ∈ Word 𝐶)
3		simpr 485	. . . . . 6 ⊢ ((((𝜑 ∧ 𝐼 ∈ {𝐾, 𝐿}) ∧ 𝐽 ∈ {𝐾, 𝐿}) ∧ 𝑐 = ∅) → 𝑐 = ∅)
4	3	oveq2d 7373	. . . . 5 ⊢ ((((𝜑 ∧ 𝐼 ∈ {𝐾, 𝐿}) ∧ 𝐽 ∈ {𝐾, 𝐿}) ∧ 𝑐 = ∅) → (𝑆 Σg 𝑐) = (𝑆 Σg ∅))
5	4	eqeq2d 2747	. . . 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 31969	. . . . . . . . 9 ⊢ (𝜑 → (𝑀‘⟨“𝐼𝐽”⟩) ∈ (Base‘𝑆))
14	6, 13	eqeltrd 2838	. . . . . . . 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 31969	. . . . . . . . 9 ⊢ (𝜑 → (𝑀‘⟨“𝐾𝐿”⟩) ∈ (Base‘𝑆))
20	15, 19	eqeltrd 2838	. . . . . . . 8 ⊢ (𝜑 → 𝐹 ∈ (Base‘𝑆))
21		eqid 2736	. . . . . . . . 9 ⊢ (Base‘𝑆) = (Base‘𝑆)
22		cyc3genpmlem.t	. . . . . . . . 9 ⊢ · = (+g‘𝑆)
23	12, 21, 22	symgov 19165	. . . . . . . 8 ⊢ ((𝐸 ∈ (Base‘𝑆) ∧ 𝐹 ∈ (Base‘𝑆)) → (𝐸 · 𝐹) = (𝐸 ∘ 𝐹))
24	14, 20, 23	syl2anc 584	. . . . . . 7 ⊢ (𝜑 → (𝐸 · 𝐹) = (𝐸 ∘ 𝐹))
25	24	ad2antrr 724	. . . . . 6 ⊢ (((𝜑 ∧ 𝐼 ∈ {𝐾, 𝐿}) ∧ 𝐽 ∈ {𝐾, 𝐿}) → (𝐸 · 𝐹) = (𝐸 ∘ 𝐹))
26	6	ad2antrr 724	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝐼 ∈ {𝐾, 𝐿}) ∧ 𝐽 ∈ {𝐾, 𝐿}) → 𝐸 = (𝑀‘⟨“𝐼𝐽”⟩))
27		eqid 2736	. . . . . . . . . 10 ⊢ (pmTrsp‘𝐷) = (pmTrsp‘𝐷)
28	7, 8, 9, 10, 11, 27	cycpm2tr 31968	. . . . . . . . 9 ⊢ (𝜑 → (𝑀‘⟨“𝐼𝐽”⟩) = ((pmTrsp‘𝐷)‘{𝐼, 𝐽}))
29	28	ad2antrr 724	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝐼 ∈ {𝐾, 𝐿}) ∧ 𝐽 ∈ {𝐾, 𝐿}) → (𝑀‘⟨“𝐼𝐽”⟩) = ((pmTrsp‘𝐷)‘{𝐼, 𝐽}))
30	26, 29	eqtrd 2776	. . . . . . 7 ⊢ (((𝜑 ∧ 𝐼 ∈ {𝐾, 𝐿}) ∧ 𝐽 ∈ {𝐾, 𝐿}) → 𝐸 = ((pmTrsp‘𝐷)‘{𝐼, 𝐽}))
31	7, 8, 16, 17, 18, 27	cycpm2tr 31968	. . . . . . . . 9 ⊢ (𝜑 → (𝑀‘⟨“𝐾𝐿”⟩) = ((pmTrsp‘𝐷)‘{𝐾, 𝐿}))
32	31	ad2antrr 724	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝐼 ∈ {𝐾, 𝐿}) ∧ 𝐽 ∈ {𝐾, 𝐿}) → (𝑀‘⟨“𝐾𝐿”⟩) = ((pmTrsp‘𝐷)‘{𝐾, 𝐿}))
33	15	ad2antrr 724	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝐼 ∈ {𝐾, 𝐿}) ∧ 𝐽 ∈ {𝐾, 𝐿}) → 𝐹 = (𝑀‘⟨“𝐾𝐿”⟩))
34	9	ad2antrr 724	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝐼 ∈ {𝐾, 𝐿}) ∧ 𝐽 ∈ {𝐾, 𝐿}) → 𝐼 ∈ 𝐷)
35	10	ad2antrr 724	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝐼 ∈ {𝐾, 𝐿}) ∧ 𝐽 ∈ {𝐾, 𝐿}) → 𝐽 ∈ 𝐷)
36	11	ad2antrr 724	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝐼 ∈ {𝐾, 𝐿}) ∧ 𝐽 ∈ {𝐾, 𝐿}) → 𝐼 ≠ 𝐽)
37		simplr 767	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝐼 ∈ {𝐾, 𝐿}) ∧ 𝐽 ∈ {𝐾, 𝐿}) → 𝐼 ∈ {𝐾, 𝐿})
38		simpr 485	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝐼 ∈ {𝐾, 𝐿}) ∧ 𝐽 ∈ {𝐾, 𝐿}) → 𝐽 ∈ {𝐾, 𝐿})
39	37, 38	prssd 4782	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝐼 ∈ {𝐾, 𝐿}) ∧ 𝐽 ∈ {𝐾, 𝐿}) → {𝐼, 𝐽} ⊆ {𝐾, 𝐿})
40		ssprsseq 4785	. . . . . . . . . . 11 ⊢ ((𝐼 ∈ 𝐷 ∧ 𝐽 ∈ 𝐷 ∧ 𝐼 ≠ 𝐽) → ({𝐼, 𝐽} ⊆ {𝐾, 𝐿} ↔ {𝐼, 𝐽} = {𝐾, 𝐿}))
41	40	biimpa 477	. . . . . . . . . 10 ⊢ (((𝐼 ∈ 𝐷 ∧ 𝐽 ∈ 𝐷 ∧ 𝐼 ≠ 𝐽) ∧ {𝐼, 𝐽} ⊆ {𝐾, 𝐿}) → {𝐼, 𝐽} = {𝐾, 𝐿})
42	34, 35, 36, 39, 41	syl31anc 1373	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝐼 ∈ {𝐾, 𝐿}) ∧ 𝐽 ∈ {𝐾, 𝐿}) → {𝐼, 𝐽} = {𝐾, 𝐿})
43	42	fveq2d 6846	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝐼 ∈ {𝐾, 𝐿}) ∧ 𝐽 ∈ {𝐾, 𝐿}) → ((pmTrsp‘𝐷)‘{𝐼, 𝐽}) = ((pmTrsp‘𝐷)‘{𝐾, 𝐿}))
44	32, 33, 43	3eqtr4d 2786	. . . . . . 7 ⊢ (((𝜑 ∧ 𝐼 ∈ {𝐾, 𝐿}) ∧ 𝐽 ∈ {𝐾, 𝐿}) → 𝐹 = ((pmTrsp‘𝐷)‘{𝐼, 𝐽}))
45	30, 44	coeq12d 5820	. . . . . 6 ⊢ (((𝜑 ∧ 𝐼 ∈ {𝐾, 𝐿}) ∧ 𝐽 ∈ {𝐾, 𝐿}) → (𝐸 ∘ 𝐹) = (((pmTrsp‘𝐷)‘{𝐼, 𝐽}) ∘ ((pmTrsp‘𝐷)‘{𝐼, 𝐽})))
46	8	ad2antrr 724	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝐼 ∈ {𝐾, 𝐿}) ∧ 𝐽 ∈ {𝐾, 𝐿}) → 𝐷 ∈ 𝑉)
47	34, 35	prssd 4782	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝐼 ∈ {𝐾, 𝐿}) ∧ 𝐽 ∈ {𝐾, 𝐿}) → {𝐼, 𝐽} ⊆ 𝐷)
48		enpr2 9938	. . . . . . . . 9 ⊢ ((𝐼 ∈ 𝐷 ∧ 𝐽 ∈ 𝐷 ∧ 𝐼 ≠ 𝐽) → {𝐼, 𝐽} ≈ 2o)
49	34, 35, 36, 48	syl3anc 1371	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝐼 ∈ {𝐾, 𝐿}) ∧ 𝐽 ∈ {𝐾, 𝐿}) → {𝐼, 𝐽} ≈ 2o)
50		eqid 2736	. . . . . . . . 9 ⊢ ran (pmTrsp‘𝐷) = ran (pmTrsp‘𝐷)
51	27, 50	pmtrrn 19239	. . . . . . . 8 ⊢ ((𝐷 ∈ 𝑉 ∧ {𝐼, 𝐽} ⊆ 𝐷 ∧ {𝐼, 𝐽} ≈ 2o) → ((pmTrsp‘𝐷)‘{𝐼, 𝐽}) ∈ ran (pmTrsp‘𝐷))
52	46, 47, 49, 51	syl3anc 1371	. . . . . . 7 ⊢ (((𝜑 ∧ 𝐼 ∈ {𝐾, 𝐿}) ∧ 𝐽 ∈ {𝐾, 𝐿}) → ((pmTrsp‘𝐷)‘{𝐼, 𝐽}) ∈ ran (pmTrsp‘𝐷))
53	27, 50	pmtrfinv 19243	. . . . . . 7 ⊢ (((pmTrsp‘𝐷)‘{𝐼, 𝐽}) ∈ ran (pmTrsp‘𝐷) → (((pmTrsp‘𝐷)‘{𝐼, 𝐽}) ∘ ((pmTrsp‘𝐷)‘{𝐼, 𝐽})) = ( I ↾ 𝐷))
54	52, 53	syl 17	. . . . . 6 ⊢ (((𝜑 ∧ 𝐼 ∈ {𝐾, 𝐿}) ∧ 𝐽 ∈ {𝐾, 𝐿}) → (((pmTrsp‘𝐷)‘{𝐼, 𝐽}) ∘ ((pmTrsp‘𝐷)‘{𝐼, 𝐽})) = ( I ↾ 𝐷))
55	25, 45, 54	3eqtrd 2780	. . . . 5 ⊢ (((𝜑 ∧ 𝐼 ∈ {𝐾, 𝐿}) ∧ 𝐽 ∈ {𝐾, 𝐿}) → (𝐸 · 𝐹) = ( I ↾ 𝐷))
56	12	symgid 19183	. . . . . . 7 ⊢ (𝐷 ∈ 𝑉 → ( I ↾ 𝐷) = (0g‘𝑆))
57	46, 56	syl 17	. . . . . 6 ⊢ (((𝜑 ∧ 𝐼 ∈ {𝐾, 𝐿}) ∧ 𝐽 ∈ {𝐾, 𝐿}) → ( I ↾ 𝐷) = (0g‘𝑆))
58		eqid 2736	. . . . . . 7 ⊢ (0g‘𝑆) = (0g‘𝑆)
59	58	gsum0 18539	. . . . . 6 ⊢ (𝑆 Σg ∅) = (0g‘𝑆)
60	57, 59	eqtr4di 2794	. . . . 5 ⊢ (((𝜑 ∧ 𝐼 ∈ {𝐾, 𝐿}) ∧ 𝐽 ∈ {𝐾, 𝐿}) → ( I ↾ 𝐷) = (𝑆 Σg ∅))
61	55, 60	eqtrd 2776	. . . 4 ⊢ (((𝜑 ∧ 𝐼 ∈ {𝐾, 𝐿}) ∧ 𝐽 ∈ {𝐾, 𝐿}) → (𝐸 · 𝐹) = (𝑆 Σg ∅))
62	2, 5, 61	rspcedvd 3583	. . 3 ⊢ (((𝜑 ∧ 𝐼 ∈ {𝐾, 𝐿}) ∧ 𝐽 ∈ {𝐾, 𝐿}) → ∃𝑐 ∈ Word 𝐶(𝐸 · 𝐹) = (𝑆 Σg 𝑐))
63	8	ad2antrr 724	. . . . . . 7 ⊢ (((𝜑 ∧ 𝐼 ∈ {𝐾, 𝐿}) ∧ ¬ 𝐽 ∈ {𝐾, 𝐿}) → 𝐷 ∈ 𝑉)
64	9	ad2antrr 724	. . . . . . 7 ⊢ (((𝜑 ∧ 𝐼 ∈ {𝐾, 𝐿}) ∧ ¬ 𝐽 ∈ {𝐾, 𝐿}) → 𝐼 ∈ 𝐷)
65	16, 17	prssd 4782	. . . . . . . . 9 ⊢ (𝜑 → {𝐾, 𝐿} ⊆ 𝐷)
66	65	ad2antrr 724	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝐼 ∈ {𝐾, 𝐿}) ∧ ¬ 𝐽 ∈ {𝐾, 𝐿}) → {𝐾, 𝐿} ⊆ 𝐷)
67		simplr 767	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝐼 ∈ {𝐾, 𝐿}) ∧ ¬ 𝐽 ∈ {𝐾, 𝐿}) → 𝐼 ∈ {𝐾, 𝐿})
68		enpr2 9938	. . . . . . . . . . 11 ⊢ ((𝐾 ∈ 𝐷 ∧ 𝐿 ∈ 𝐷 ∧ 𝐾 ≠ 𝐿) → {𝐾, 𝐿} ≈ 2o)
69	16, 17, 18, 68	syl3anc 1371	. . . . . . . . . 10 ⊢ (𝜑 → {𝐾, 𝐿} ≈ 2o)
70	69	ad2antrr 724	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝐼 ∈ {𝐾, 𝐿}) ∧ ¬ 𝐽 ∈ {𝐾, 𝐿}) → {𝐾, 𝐿} ≈ 2o)
71		unidifsnel 31462	. . . . . . . . 9 ⊢ ((𝐼 ∈ {𝐾, 𝐿} ∧ {𝐾, 𝐿} ≈ 2o) → ∪ ({𝐾, 𝐿} ∖ {𝐼}) ∈ {𝐾, 𝐿})
72	67, 70, 71	syl2anc 584	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝐼 ∈ {𝐾, 𝐿}) ∧ ¬ 𝐽 ∈ {𝐾, 𝐿}) → ∪ ({𝐾, 𝐿} ∖ {𝐼}) ∈ {𝐾, 𝐿})
73	66, 72	sseldd 3945	. . . . . . 7 ⊢ (((𝜑 ∧ 𝐼 ∈ {𝐾, 𝐿}) ∧ ¬ 𝐽 ∈ {𝐾, 𝐿}) → ∪ ({𝐾, 𝐿} ∖ {𝐼}) ∈ 𝐷)
74	10	ad2antrr 724	. . . . . . 7 ⊢ (((𝜑 ∧ 𝐼 ∈ {𝐾, 𝐿}) ∧ ¬ 𝐽 ∈ {𝐾, 𝐿}) → 𝐽 ∈ 𝐷)
75		unidifsnne 31463	. . . . . . . . 9 ⊢ ((𝐼 ∈ {𝐾, 𝐿} ∧ {𝐾, 𝐿} ≈ 2o) → ∪ ({𝐾, 𝐿} ∖ {𝐼}) ≠ 𝐼)
76	67, 70, 75	syl2anc 584	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝐼 ∈ {𝐾, 𝐿}) ∧ ¬ 𝐽 ∈ {𝐾, 𝐿}) → ∪ ({𝐾, 𝐿} ∖ {𝐼}) ≠ 𝐼)
77	76	necomd 2999	. . . . . . 7 ⊢ (((𝜑 ∧ 𝐼 ∈ {𝐾, 𝐿}) ∧ ¬ 𝐽 ∈ {𝐾, 𝐿}) → 𝐼 ≠ ∪ ({𝐾, 𝐿} ∖ {𝐼}))
78		nelne2 3042	. . . . . . . 8 ⊢ ((∪ ({𝐾, 𝐿} ∖ {𝐼}) ∈ {𝐾, 𝐿} ∧ ¬ 𝐽 ∈ {𝐾, 𝐿}) → ∪ ({𝐾, 𝐿} ∖ {𝐼}) ≠ 𝐽)
79	72, 78	sylancom 588	. . . . . . 7 ⊢ (((𝜑 ∧ 𝐼 ∈ {𝐾, 𝐿}) ∧ ¬ 𝐽 ∈ {𝐾, 𝐿}) → ∪ ({𝐾, 𝐿} ∖ {𝐼}) ≠ 𝐽)
80	11	necomd 2999	. . . . . . . 8 ⊢ (𝜑 → 𝐽 ≠ 𝐼)
81	80	ad2antrr 724	. . . . . . 7 ⊢ (((𝜑 ∧ 𝐼 ∈ {𝐾, 𝐿}) ∧ ¬ 𝐽 ∈ {𝐾, 𝐿}) → 𝐽 ≠ 𝐼)
82	7, 12, 63, 64, 73, 74, 77, 79, 81	cycpm3cl2 31985	. . . . . 6 ⊢ (((𝜑 ∧ 𝐼 ∈ {𝐾, 𝐿}) ∧ ¬ 𝐽 ∈ {𝐾, 𝐿}) → (𝑀‘⟨“𝐼∪ ({𝐾, 𝐿} ∖ {𝐼})𝐽”⟩) ∈ (𝑀 “ (◡♯ “ {3})))
83		cyc3genpm.t	. . . . . 6 ⊢ 𝐶 = (𝑀 “ (◡♯ “ {3}))
84	82, 83	eleqtrrdi 2849	. . . . 5 ⊢ (((𝜑 ∧ 𝐼 ∈ {𝐾, 𝐿}) ∧ ¬ 𝐽 ∈ {𝐾, 𝐿}) → (𝑀‘⟨“𝐼∪ ({𝐾, 𝐿} ∖ {𝐼})𝐽”⟩) ∈ 𝐶)
85	84	s1cld 14491	. . . 4 ⊢ (((𝜑 ∧ 𝐼 ∈ {𝐾, 𝐿}) ∧ ¬ 𝐽 ∈ {𝐾, 𝐿}) → ⟨“(𝑀‘⟨“𝐼∪ ({𝐾, 𝐿} ∖ {𝐼})𝐽”⟩)”⟩ ∈ Word 𝐶)
86		simpr 485	. . . . . 6 ⊢ ((((𝜑 ∧ 𝐼 ∈ {𝐾, 𝐿}) ∧ ¬ 𝐽 ∈ {𝐾, 𝐿}) ∧ 𝑐 = ⟨“(𝑀‘⟨“𝐼∪ ({𝐾, 𝐿} ∖ {𝐼})𝐽”⟩)”⟩) → 𝑐 = ⟨“(𝑀‘⟨“𝐼∪ ({𝐾, 𝐿} ∖ {𝐼})𝐽”⟩)”⟩)
87	86	oveq2d 7373	. . . . 5 ⊢ ((((𝜑 ∧ 𝐼 ∈ {𝐾, 𝐿}) ∧ ¬ 𝐽 ∈ {𝐾, 𝐿}) ∧ 𝑐 = ⟨“(𝑀‘⟨“𝐼∪ ({𝐾, 𝐿} ∖ {𝐼})𝐽”⟩)”⟩) → (𝑆 Σg 𝑐) = (𝑆 Σg ⟨“(𝑀‘⟨“𝐼∪ ({𝐾, 𝐿} ∖ {𝐼})𝐽”⟩)”⟩))
88	87	eqeq2d 2747	. . . 4 ⊢ ((((𝜑 ∧ 𝐼 ∈ {𝐾, 𝐿}) ∧ ¬ 𝐽 ∈ {𝐾, 𝐿}) ∧ 𝑐 = ⟨“(𝑀‘⟨“𝐼∪ ({𝐾, 𝐿} ∖ {𝐼})𝐽”⟩)”⟩) → ((𝐸 · 𝐹) = (𝑆 Σg 𝑐) ↔ (𝐸 · 𝐹) = (𝑆 Σg ⟨“(𝑀‘⟨“𝐼∪ ({𝐾, 𝐿} ∖ {𝐼})𝐽”⟩)”⟩)))
89	7, 12, 63, 64, 73, 74, 77, 79, 81, 22	cyc3co2 31989	. . . . 5 ⊢ (((𝜑 ∧ 𝐼 ∈ {𝐾, 𝐿}) ∧ ¬ 𝐽 ∈ {𝐾, 𝐿}) → (𝑀‘⟨“𝐼∪ ({𝐾, 𝐿} ∖ {𝐼})𝐽”⟩) = ((𝑀‘⟨“𝐼𝐽”⟩) · (𝑀‘⟨“𝐼∪ ({𝐾, 𝐿} ∖ {𝐼})”⟩)))
90	7, 12, 63, 64, 73, 74, 77, 79, 81	cycpm3cl 31984	. . . . . 6 ⊢ (((𝜑 ∧ 𝐼 ∈ {𝐾, 𝐿}) ∧ ¬ 𝐽 ∈ {𝐾, 𝐿}) → (𝑀‘⟨“𝐼∪ ({𝐾, 𝐿} ∖ {𝐼})𝐽”⟩) ∈ (Base‘𝑆))
91	21	gsumws1 18648	. . . . . 6 ⊢ ((𝑀‘⟨“𝐼∪ ({𝐾, 𝐿} ∖ {𝐼})𝐽”⟩) ∈ (Base‘𝑆) → (𝑆 Σg ⟨“(𝑀‘⟨“𝐼∪ ({𝐾, 𝐿} ∖ {𝐼})𝐽”⟩)”⟩) = (𝑀‘⟨“𝐼∪ ({𝐾, 𝐿} ∖ {𝐼})𝐽”⟩))
92	90, 91	syl 17	. . . . 5 ⊢ (((𝜑 ∧ 𝐼 ∈ {𝐾, 𝐿}) ∧ ¬ 𝐽 ∈ {𝐾, 𝐿}) → (𝑆 Σg ⟨“(𝑀‘⟨“𝐼∪ ({𝐾, 𝐿} ∖ {𝐼})𝐽”⟩)”⟩) = (𝑀‘⟨“𝐼∪ ({𝐾, 𝐿} ∖ {𝐼})𝐽”⟩))
93	6	ad2antrr 724	. . . . . 6 ⊢ (((𝜑 ∧ 𝐼 ∈ {𝐾, 𝐿}) ∧ ¬ 𝐽 ∈ {𝐾, 𝐿}) → 𝐸 = (𝑀‘⟨“𝐼𝐽”⟩))
94		en2eleq 9944	. . . . . . . . 9 ⊢ ((𝐼 ∈ {𝐾, 𝐿} ∧ {𝐾, 𝐿} ≈ 2o) → {𝐾, 𝐿} = {𝐼, ∪ ({𝐾, 𝐿} ∖ {𝐼})})
95	67, 70, 94	syl2anc 584	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝐼 ∈ {𝐾, 𝐿}) ∧ ¬ 𝐽 ∈ {𝐾, 𝐿}) → {𝐾, 𝐿} = {𝐼, ∪ ({𝐾, 𝐿} ∖ {𝐼})})
96	95	fveq2d 6846	. . . . . . 7 ⊢ (((𝜑 ∧ 𝐼 ∈ {𝐾, 𝐿}) ∧ ¬ 𝐽 ∈ {𝐾, 𝐿}) → ((pmTrsp‘𝐷)‘{𝐾, 𝐿}) = ((pmTrsp‘𝐷)‘{𝐼, ∪ ({𝐾, 𝐿} ∖ {𝐼})}))
97	15, 31	eqtrd 2776	. . . . . . . 8 ⊢ (𝜑 → 𝐹 = ((pmTrsp‘𝐷)‘{𝐾, 𝐿}))
98	97	ad2antrr 724	. . . . . . 7 ⊢ (((𝜑 ∧ 𝐼 ∈ {𝐾, 𝐿}) ∧ ¬ 𝐽 ∈ {𝐾, 𝐿}) → 𝐹 = ((pmTrsp‘𝐷)‘{𝐾, 𝐿}))
99	7, 63, 64, 73, 77, 27	cycpm2tr 31968	. . . . . . 7 ⊢ (((𝜑 ∧ 𝐼 ∈ {𝐾, 𝐿}) ∧ ¬ 𝐽 ∈ {𝐾, 𝐿}) → (𝑀‘⟨“𝐼∪ ({𝐾, 𝐿} ∖ {𝐼})”⟩) = ((pmTrsp‘𝐷)‘{𝐼, ∪ ({𝐾, 𝐿} ∖ {𝐼})}))
100	96, 98, 99	3eqtr4d 2786	. . . . . 6 ⊢ (((𝜑 ∧ 𝐼 ∈ {𝐾, 𝐿}) ∧ ¬ 𝐽 ∈ {𝐾, 𝐿}) → 𝐹 = (𝑀‘⟨“𝐼∪ ({𝐾, 𝐿} ∖ {𝐼})”⟩))
101	93, 100	oveq12d 7375	. . . . 5 ⊢ (((𝜑 ∧ 𝐼 ∈ {𝐾, 𝐿}) ∧ ¬ 𝐽 ∈ {𝐾, 𝐿}) → (𝐸 · 𝐹) = ((𝑀‘⟨“𝐼𝐽”⟩) · (𝑀‘⟨“𝐼∪ ({𝐾, 𝐿} ∖ {𝐼})”⟩)))
102	89, 92, 101	3eqtr4rd 2787	. . . 4 ⊢ (((𝜑 ∧ 𝐼 ∈ {𝐾, 𝐿}) ∧ ¬ 𝐽 ∈ {𝐾, 𝐿}) → (𝐸 · 𝐹) = (𝑆 Σg ⟨“(𝑀‘⟨“𝐼∪ ({𝐾, 𝐿} ∖ {𝐼})𝐽”⟩)”⟩))
103	85, 88, 102	rspcedvd 3583	. . 3 ⊢ (((𝜑 ∧ 𝐼 ∈ {𝐾, 𝐿}) ∧ ¬ 𝐽 ∈ {𝐾, 𝐿}) → ∃𝑐 ∈ Word 𝐶(𝐸 · 𝐹) = (𝑆 Σg 𝑐))
104	62, 103	pm2.61dan 811	. 2 ⊢ ((𝜑 ∧ 𝐼 ∈ {𝐾, 𝐿}) → ∃𝑐 ∈ Word 𝐶(𝐸 · 𝐹) = (𝑆 Σg 𝑐))
105	8	ad2antrr 724	. . . . . . 7 ⊢ (((𝜑 ∧ ¬ 𝐼 ∈ {𝐾, 𝐿}) ∧ 𝐽 ∈ {𝐾, 𝐿}) → 𝐷 ∈ 𝑉)
106	10	ad2antrr 724	. . . . . . 7 ⊢ (((𝜑 ∧ ¬ 𝐼 ∈ {𝐾, 𝐿}) ∧ 𝐽 ∈ {𝐾, 𝐿}) → 𝐽 ∈ 𝐷)
107	65	ad2antrr 724	. . . . . . . 8 ⊢ (((𝜑 ∧ ¬ 𝐼 ∈ {𝐾, 𝐿}) ∧ 𝐽 ∈ {𝐾, 𝐿}) → {𝐾, 𝐿} ⊆ 𝐷)
108		simpr 485	. . . . . . . . 9 ⊢ (((𝜑 ∧ ¬ 𝐼 ∈ {𝐾, 𝐿}) ∧ 𝐽 ∈ {𝐾, 𝐿}) → 𝐽 ∈ {𝐾, 𝐿})
109	69	ad2antrr 724	. . . . . . . . 9 ⊢ (((𝜑 ∧ ¬ 𝐼 ∈ {𝐾, 𝐿}) ∧ 𝐽 ∈ {𝐾, 𝐿}) → {𝐾, 𝐿} ≈ 2o)
110		unidifsnel 31462	. . . . . . . . 9 ⊢ ((𝐽 ∈ {𝐾, 𝐿} ∧ {𝐾, 𝐿} ≈ 2o) → ∪ ({𝐾, 𝐿} ∖ {𝐽}) ∈ {𝐾, 𝐿})
111	108, 109, 110	syl2anc 584	. . . . . . . 8 ⊢ (((𝜑 ∧ ¬ 𝐼 ∈ {𝐾, 𝐿}) ∧ 𝐽 ∈ {𝐾, 𝐿}) → ∪ ({𝐾, 𝐿} ∖ {𝐽}) ∈ {𝐾, 𝐿})
112	107, 111	sseldd 3945	. . . . . . 7 ⊢ (((𝜑 ∧ ¬ 𝐼 ∈ {𝐾, 𝐿}) ∧ 𝐽 ∈ {𝐾, 𝐿}) → ∪ ({𝐾, 𝐿} ∖ {𝐽}) ∈ 𝐷)
113	9	ad2antrr 724	. . . . . . 7 ⊢ (((𝜑 ∧ ¬ 𝐼 ∈ {𝐾, 𝐿}) ∧ 𝐽 ∈ {𝐾, 𝐿}) → 𝐼 ∈ 𝐷)
114		unidifsnne 31463	. . . . . . . . 9 ⊢ ((𝐽 ∈ {𝐾, 𝐿} ∧ {𝐾, 𝐿} ≈ 2o) → ∪ ({𝐾, 𝐿} ∖ {𝐽}) ≠ 𝐽)
115	108, 109, 114	syl2anc 584	. . . . . . . 8 ⊢ (((𝜑 ∧ ¬ 𝐼 ∈ {𝐾, 𝐿}) ∧ 𝐽 ∈ {𝐾, 𝐿}) → ∪ ({𝐾, 𝐿} ∖ {𝐽}) ≠ 𝐽)
116	115	necomd 2999	. . . . . . 7 ⊢ (((𝜑 ∧ ¬ 𝐼 ∈ {𝐾, 𝐿}) ∧ 𝐽 ∈ {𝐾, 𝐿}) → 𝐽 ≠ ∪ ({𝐾, 𝐿} ∖ {𝐽}))
117		simplr 767	. . . . . . . 8 ⊢ (((𝜑 ∧ ¬ 𝐼 ∈ {𝐾, 𝐿}) ∧ 𝐽 ∈ {𝐾, 𝐿}) → ¬ 𝐼 ∈ {𝐾, 𝐿})
118		nelne2 3042	. . . . . . . 8 ⊢ ((∪ ({𝐾, 𝐿} ∖ {𝐽}) ∈ {𝐾, 𝐿} ∧ ¬ 𝐼 ∈ {𝐾, 𝐿}) → ∪ ({𝐾, 𝐿} ∖ {𝐽}) ≠ 𝐼)
119	111, 117, 118	syl2anc 584	. . . . . . 7 ⊢ (((𝜑 ∧ ¬ 𝐼 ∈ {𝐾, 𝐿}) ∧ 𝐽 ∈ {𝐾, 𝐿}) → ∪ ({𝐾, 𝐿} ∖ {𝐽}) ≠ 𝐼)
120	11	ad2antrr 724	. . . . . . 7 ⊢ (((𝜑 ∧ ¬ 𝐼 ∈ {𝐾, 𝐿}) ∧ 𝐽 ∈ {𝐾, 𝐿}) → 𝐼 ≠ 𝐽)
121	7, 12, 105, 106, 112, 113, 116, 119, 120	cycpm3cl2 31985	. . . . . 6 ⊢ (((𝜑 ∧ ¬ 𝐼 ∈ {𝐾, 𝐿}) ∧ 𝐽 ∈ {𝐾, 𝐿}) → (𝑀‘⟨“𝐽∪ ({𝐾, 𝐿} ∖ {𝐽})𝐼”⟩) ∈ (𝑀 “ (◡♯ “ {3})))
122	121, 83	eleqtrrdi 2849	. . . . 5 ⊢ (((𝜑 ∧ ¬ 𝐼 ∈ {𝐾, 𝐿}) ∧ 𝐽 ∈ {𝐾, 𝐿}) → (𝑀‘⟨“𝐽∪ ({𝐾, 𝐿} ∖ {𝐽})𝐼”⟩) ∈ 𝐶)
123	122	s1cld 14491	. . . 4 ⊢ (((𝜑 ∧ ¬ 𝐼 ∈ {𝐾, 𝐿}) ∧ 𝐽 ∈ {𝐾, 𝐿}) → ⟨“(𝑀‘⟨“𝐽∪ ({𝐾, 𝐿} ∖ {𝐽})𝐼”⟩)”⟩ ∈ Word 𝐶)
124		simpr 485	. . . . . 6 ⊢ ((((𝜑 ∧ ¬ 𝐼 ∈ {𝐾, 𝐿}) ∧ 𝐽 ∈ {𝐾, 𝐿}) ∧ 𝑐 = ⟨“(𝑀‘⟨“𝐽∪ ({𝐾, 𝐿} ∖ {𝐽})𝐼”⟩)”⟩) → 𝑐 = ⟨“(𝑀‘⟨“𝐽∪ ({𝐾, 𝐿} ∖ {𝐽})𝐼”⟩)”⟩)
125	124	oveq2d 7373	. . . . 5 ⊢ ((((𝜑 ∧ ¬ 𝐼 ∈ {𝐾, 𝐿}) ∧ 𝐽 ∈ {𝐾, 𝐿}) ∧ 𝑐 = ⟨“(𝑀‘⟨“𝐽∪ ({𝐾, 𝐿} ∖ {𝐽})𝐼”⟩)”⟩) → (𝑆 Σg 𝑐) = (𝑆 Σg ⟨“(𝑀‘⟨“𝐽∪ ({𝐾, 𝐿} ∖ {𝐽})𝐼”⟩)”⟩))
126	125	eqeq2d 2747	. . . 4 ⊢ ((((𝜑 ∧ ¬ 𝐼 ∈ {𝐾, 𝐿}) ∧ 𝐽 ∈ {𝐾, 𝐿}) ∧ 𝑐 = ⟨“(𝑀‘⟨“𝐽∪ ({𝐾, 𝐿} ∖ {𝐽})𝐼”⟩)”⟩) → ((𝐸 · 𝐹) = (𝑆 Σg 𝑐) ↔ (𝐸 · 𝐹) = (𝑆 Σg ⟨“(𝑀‘⟨“𝐽∪ ({𝐾, 𝐿} ∖ {𝐽})𝐼”⟩)”⟩)))
127	7, 12, 105, 106, 112, 113, 116, 119, 120, 22	cyc3co2 31989	. . . . 5 ⊢ (((𝜑 ∧ ¬ 𝐼 ∈ {𝐾, 𝐿}) ∧ 𝐽 ∈ {𝐾, 𝐿}) → (𝑀‘⟨“𝐽∪ ({𝐾, 𝐿} ∖ {𝐽})𝐼”⟩) = ((𝑀‘⟨“𝐽𝐼”⟩) · (𝑀‘⟨“𝐽∪ ({𝐾, 𝐿} ∖ {𝐽})”⟩)))
128	7, 12, 105, 106, 112, 113, 116, 119, 120	cycpm3cl 31984	. . . . . 6 ⊢ (((𝜑 ∧ ¬ 𝐼 ∈ {𝐾, 𝐿}) ∧ 𝐽 ∈ {𝐾, 𝐿}) → (𝑀‘⟨“𝐽∪ ({𝐾, 𝐿} ∖ {𝐽})𝐼”⟩) ∈ (Base‘𝑆))
129	21	gsumws1 18648	. . . . . 6 ⊢ ((𝑀‘⟨“𝐽∪ ({𝐾, 𝐿} ∖ {𝐽})𝐼”⟩) ∈ (Base‘𝑆) → (𝑆 Σg ⟨“(𝑀‘⟨“𝐽∪ ({𝐾, 𝐿} ∖ {𝐽})𝐼”⟩)”⟩) = (𝑀‘⟨“𝐽∪ ({𝐾, 𝐿} ∖ {𝐽})𝐼”⟩))
130	128, 129	syl 17	. . . . 5 ⊢ (((𝜑 ∧ ¬ 𝐼 ∈ {𝐾, 𝐿}) ∧ 𝐽 ∈ {𝐾, 𝐿}) → (𝑆 Σg ⟨“(𝑀‘⟨“𝐽∪ ({𝐾, 𝐿} ∖ {𝐽})𝐼”⟩)”⟩) = (𝑀‘⟨“𝐽∪ ({𝐾, 𝐿} ∖ {𝐽})𝐼”⟩))
131		prcom 4693	. . . . . . . . . 10 ⊢ {𝐼, 𝐽} = {𝐽, 𝐼}
132	131	fveq2i 6845	. . . . . . . . 9 ⊢ ((pmTrsp‘𝐷)‘{𝐼, 𝐽}) = ((pmTrsp‘𝐷)‘{𝐽, 𝐼})
133	7, 8, 10, 9, 80, 27	cycpm2tr 31968	. . . . . . . . 9 ⊢ (𝜑 → (𝑀‘⟨“𝐽𝐼”⟩) = ((pmTrsp‘𝐷)‘{𝐽, 𝐼}))
134	132, 28, 133	3eqtr4a 2802	. . . . . . . 8 ⊢ (𝜑 → (𝑀‘⟨“𝐼𝐽”⟩) = (𝑀‘⟨“𝐽𝐼”⟩))
135	6, 134	eqtrd 2776	. . . . . . 7 ⊢ (𝜑 → 𝐸 = (𝑀‘⟨“𝐽𝐼”⟩))
136	135	ad2antrr 724	. . . . . 6 ⊢ (((𝜑 ∧ ¬ 𝐼 ∈ {𝐾, 𝐿}) ∧ 𝐽 ∈ {𝐾, 𝐿}) → 𝐸 = (𝑀‘⟨“𝐽𝐼”⟩))
137		en2eleq 9944	. . . . . . . . 9 ⊢ ((𝐽 ∈ {𝐾, 𝐿} ∧ {𝐾, 𝐿} ≈ 2o) → {𝐾, 𝐿} = {𝐽, ∪ ({𝐾, 𝐿} ∖ {𝐽})})
138	108, 109, 137	syl2anc 584	. . . . . . . 8 ⊢ (((𝜑 ∧ ¬ 𝐼 ∈ {𝐾, 𝐿}) ∧ 𝐽 ∈ {𝐾, 𝐿}) → {𝐾, 𝐿} = {𝐽, ∪ ({𝐾, 𝐿} ∖ {𝐽})})
139	138	fveq2d 6846	. . . . . . 7 ⊢ (((𝜑 ∧ ¬ 𝐼 ∈ {𝐾, 𝐿}) ∧ 𝐽 ∈ {𝐾, 𝐿}) → ((pmTrsp‘𝐷)‘{𝐾, 𝐿}) = ((pmTrsp‘𝐷)‘{𝐽, ∪ ({𝐾, 𝐿} ∖ {𝐽})}))
140	97	ad2antrr 724	. . . . . . 7 ⊢ (((𝜑 ∧ ¬ 𝐼 ∈ {𝐾, 𝐿}) ∧ 𝐽 ∈ {𝐾, 𝐿}) → 𝐹 = ((pmTrsp‘𝐷)‘{𝐾, 𝐿}))
141	7, 105, 106, 112, 116, 27	cycpm2tr 31968	. . . . . . 7 ⊢ (((𝜑 ∧ ¬ 𝐼 ∈ {𝐾, 𝐿}) ∧ 𝐽 ∈ {𝐾, 𝐿}) → (𝑀‘⟨“𝐽∪ ({𝐾, 𝐿} ∖ {𝐽})”⟩) = ((pmTrsp‘𝐷)‘{𝐽, ∪ ({𝐾, 𝐿} ∖ {𝐽})}))
142	139, 140, 141	3eqtr4d 2786	. . . . . 6 ⊢ (((𝜑 ∧ ¬ 𝐼 ∈ {𝐾, 𝐿}) ∧ 𝐽 ∈ {𝐾, 𝐿}) → 𝐹 = (𝑀‘⟨“𝐽∪ ({𝐾, 𝐿} ∖ {𝐽})”⟩))
143	136, 142	oveq12d 7375	. . . . 5 ⊢ (((𝜑 ∧ ¬ 𝐼 ∈ {𝐾, 𝐿}) ∧ 𝐽 ∈ {𝐾, 𝐿}) → (𝐸 · 𝐹) = ((𝑀‘⟨“𝐽𝐼”⟩) · (𝑀‘⟨“𝐽∪ ({𝐾, 𝐿} ∖ {𝐽})”⟩)))
144	127, 130, 143	3eqtr4rd 2787	. . . 4 ⊢ (((𝜑 ∧ ¬ 𝐼 ∈ {𝐾, 𝐿}) ∧ 𝐽 ∈ {𝐾, 𝐿}) → (𝐸 · 𝐹) = (𝑆 Σg ⟨“(𝑀‘⟨“𝐽∪ ({𝐾, 𝐿} ∖ {𝐽})𝐼”⟩)”⟩))
145	123, 126, 144	rspcedvd 3583	. . 3 ⊢ (((𝜑 ∧ ¬ 𝐼 ∈ {𝐾, 𝐿}) ∧ 𝐽 ∈ {𝐾, 𝐿}) → ∃𝑐 ∈ Word 𝐶(𝐸 · 𝐹) = (𝑆 Σg 𝑐))
146	8	ad2antrr 724	. . . . . . 7 ⊢ (((𝜑 ∧ ¬ 𝐼 ∈ {𝐾, 𝐿}) ∧ ¬ 𝐽 ∈ {𝐾, 𝐿}) → 𝐷 ∈ 𝑉)
147	10	ad2antrr 724	. . . . . . 7 ⊢ (((𝜑 ∧ ¬ 𝐼 ∈ {𝐾, 𝐿}) ∧ ¬ 𝐽 ∈ {𝐾, 𝐿}) → 𝐽 ∈ 𝐷)
148	16	ad2antrr 724	. . . . . . 7 ⊢ (((𝜑 ∧ ¬ 𝐼 ∈ {𝐾, 𝐿}) ∧ ¬ 𝐽 ∈ {𝐾, 𝐿}) → 𝐾 ∈ 𝐷)
149	9	ad2antrr 724	. . . . . . 7 ⊢ (((𝜑 ∧ ¬ 𝐼 ∈ {𝐾, 𝐿}) ∧ ¬ 𝐽 ∈ {𝐾, 𝐿}) → 𝐼 ∈ 𝐷)
150		simpr 485	. . . . . . . 8 ⊢ (((𝜑 ∧ ¬ 𝐼 ∈ {𝐾, 𝐿}) ∧ ¬ 𝐽 ∈ {𝐾, 𝐿}) → ¬ 𝐽 ∈ {𝐾, 𝐿})
151	147, 150	nelpr1 4614	. . . . . . 7 ⊢ (((𝜑 ∧ ¬ 𝐼 ∈ {𝐾, 𝐿}) ∧ ¬ 𝐽 ∈ {𝐾, 𝐿}) → 𝐽 ≠ 𝐾)
152		prid1g 4721	. . . . . . . . . 10 ⊢ (𝐾 ∈ 𝐷 → 𝐾 ∈ {𝐾, 𝐿})
153	16, 152	syl 17	. . . . . . . . 9 ⊢ (𝜑 → 𝐾 ∈ {𝐾, 𝐿})
154	153	ad2antrr 724	. . . . . . . 8 ⊢ (((𝜑 ∧ ¬ 𝐼 ∈ {𝐾, 𝐿}) ∧ ¬ 𝐽 ∈ {𝐾, 𝐿}) → 𝐾 ∈ {𝐾, 𝐿})
155		simplr 767	. . . . . . . 8 ⊢ (((𝜑 ∧ ¬ 𝐼 ∈ {𝐾, 𝐿}) ∧ ¬ 𝐽 ∈ {𝐾, 𝐿}) → ¬ 𝐼 ∈ {𝐾, 𝐿})
156		nelne2 3042	. . . . . . . 8 ⊢ ((𝐾 ∈ {𝐾, 𝐿} ∧ ¬ 𝐼 ∈ {𝐾, 𝐿}) → 𝐾 ≠ 𝐼)
157	154, 155, 156	syl2anc 584	. . . . . . 7 ⊢ (((𝜑 ∧ ¬ 𝐼 ∈ {𝐾, 𝐿}) ∧ ¬ 𝐽 ∈ {𝐾, 𝐿}) → 𝐾 ≠ 𝐼)
158	11	ad2antrr 724	. . . . . . 7 ⊢ (((𝜑 ∧ ¬ 𝐼 ∈ {𝐾, 𝐿}) ∧ ¬ 𝐽 ∈ {𝐾, 𝐿}) → 𝐼 ≠ 𝐽)
159	7, 12, 146, 147, 148, 149, 151, 157, 158	cycpm3cl2 31985	. . . . . 6 ⊢ (((𝜑 ∧ ¬ 𝐼 ∈ {𝐾, 𝐿}) ∧ ¬ 𝐽 ∈ {𝐾, 𝐿}) → (𝑀‘⟨“𝐽𝐾𝐼”⟩) ∈ (𝑀 “ (◡♯ “ {3})))
160	159, 83	eleqtrrdi 2849	. . . . 5 ⊢ (((𝜑 ∧ ¬ 𝐼 ∈ {𝐾, 𝐿}) ∧ ¬ 𝐽 ∈ {𝐾, 𝐿}) → (𝑀‘⟨“𝐽𝐾𝐼”⟩) ∈ 𝐶)
161	17	ad2antrr 724	. . . . . . 7 ⊢ (((𝜑 ∧ ¬ 𝐼 ∈ {𝐾, 𝐿}) ∧ ¬ 𝐽 ∈ {𝐾, 𝐿}) → 𝐿 ∈ 𝐷)
162	18	ad2antrr 724	. . . . . . 7 ⊢ (((𝜑 ∧ ¬ 𝐼 ∈ {𝐾, 𝐿}) ∧ ¬ 𝐽 ∈ {𝐾, 𝐿}) → 𝐾 ≠ 𝐿)
163		prid2g 4722	. . . . . . . . 9 ⊢ (𝐿 ∈ 𝐷 → 𝐿 ∈ {𝐾, 𝐿})
164	161, 163	syl 17	. . . . . . . 8 ⊢ (((𝜑 ∧ ¬ 𝐼 ∈ {𝐾, 𝐿}) ∧ ¬ 𝐽 ∈ {𝐾, 𝐿}) → 𝐿 ∈ {𝐾, 𝐿})
165		nelne2 3042	. . . . . . . 8 ⊢ ((𝐿 ∈ {𝐾, 𝐿} ∧ ¬ 𝐽 ∈ {𝐾, 𝐿}) → 𝐿 ≠ 𝐽)
166	164, 165	sylancom 588	. . . . . . 7 ⊢ (((𝜑 ∧ ¬ 𝐼 ∈ {𝐾, 𝐿}) ∧ ¬ 𝐽 ∈ {𝐾, 𝐿}) → 𝐿 ≠ 𝐽)
167	7, 12, 146, 148, 161, 147, 162, 166, 151	cycpm3cl2 31985	. . . . . 6 ⊢ (((𝜑 ∧ ¬ 𝐼 ∈ {𝐾, 𝐿}) ∧ ¬ 𝐽 ∈ {𝐾, 𝐿}) → (𝑀‘⟨“𝐾𝐿𝐽”⟩) ∈ (𝑀 “ (◡♯ “ {3})))
168	167, 83	eleqtrrdi 2849	. . . . 5 ⊢ (((𝜑 ∧ ¬ 𝐼 ∈ {𝐾, 𝐿}) ∧ ¬ 𝐽 ∈ {𝐾, 𝐿}) → (𝑀‘⟨“𝐾𝐿𝐽”⟩) ∈ 𝐶)
169	160, 168	s2cld 14760	. . . 4 ⊢ (((𝜑 ∧ ¬ 𝐼 ∈ {𝐾, 𝐿}) ∧ ¬ 𝐽 ∈ {𝐾, 𝐿}) → ⟨“(𝑀‘⟨“𝐽𝐾𝐼”⟩)(𝑀‘⟨“𝐾𝐿𝐽”⟩)”⟩ ∈ Word 𝐶)
170		simpr 485	. . . . . 6 ⊢ ((((𝜑 ∧ ¬ 𝐼 ∈ {𝐾, 𝐿}) ∧ ¬ 𝐽 ∈ {𝐾, 𝐿}) ∧ 𝑐 = ⟨“(𝑀‘⟨“𝐽𝐾𝐼”⟩)(𝑀‘⟨“𝐾𝐿𝐽”⟩)”⟩) → 𝑐 = ⟨“(𝑀‘⟨“𝐽𝐾𝐼”⟩)(𝑀‘⟨“𝐾𝐿𝐽”⟩)”⟩)
171	170	oveq2d 7373	. . . . 5 ⊢ ((((𝜑 ∧ ¬ 𝐼 ∈ {𝐾, 𝐿}) ∧ ¬ 𝐽 ∈ {𝐾, 𝐿}) ∧ 𝑐 = ⟨“(𝑀‘⟨“𝐽𝐾𝐼”⟩)(𝑀‘⟨“𝐾𝐿𝐽”⟩)”⟩) → (𝑆 Σg 𝑐) = (𝑆 Σg ⟨“(𝑀‘⟨“𝐽𝐾𝐼”⟩)(𝑀‘⟨“𝐾𝐿𝐽”⟩)”⟩))
172	171	eqeq2d 2747	. . . 4 ⊢ ((((𝜑 ∧ ¬ 𝐼 ∈ {𝐾, 𝐿}) ∧ ¬ 𝐽 ∈ {𝐾, 𝐿}) ∧ 𝑐 = ⟨“(𝑀‘⟨“𝐽𝐾𝐼”⟩)(𝑀‘⟨“𝐾𝐿𝐽”⟩)”⟩) → ((𝐸 · 𝐹) = (𝑆 Σg 𝑐) ↔ (𝐸 · 𝐹) = (𝑆 Σg ⟨“(𝑀‘⟨“𝐽𝐾𝐼”⟩)(𝑀‘⟨“𝐾𝐿𝐽”⟩)”⟩)))
173	146, 56	syl 17	. . . . . . . . . 10 ⊢ (((𝜑 ∧ ¬ 𝐼 ∈ {𝐾, 𝐿}) ∧ ¬ 𝐽 ∈ {𝐾, 𝐿}) → ( I ↾ 𝐷) = (0g‘𝑆))
174	173	oveq1d 7372	. . . . . . . . 9 ⊢ (((𝜑 ∧ ¬ 𝐼 ∈ {𝐾, 𝐿}) ∧ ¬ 𝐽 ∈ {𝐾, 𝐿}) → (( I ↾ 𝐷) · (𝑀‘⟨“𝐾𝐿”⟩)) = ((0g‘𝑆) · (𝑀‘⟨“𝐾𝐿”⟩)))
175	12	symggrp 19182	. . . . . . . . . . . 12 ⊢ (𝐷 ∈ 𝑉 → 𝑆 ∈ Grp)
176	8, 175	syl 17	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑆 ∈ Grp)
177	176	ad2antrr 724	. . . . . . . . . 10 ⊢ (((𝜑 ∧ ¬ 𝐼 ∈ {𝐾, 𝐿}) ∧ ¬ 𝐽 ∈ {𝐾, 𝐿}) → 𝑆 ∈ Grp)
178	19	ad2antrr 724	. . . . . . . . . 10 ⊢ (((𝜑 ∧ ¬ 𝐼 ∈ {𝐾, 𝐿}) ∧ ¬ 𝐽 ∈ {𝐾, 𝐿}) → (𝑀‘⟨“𝐾𝐿”⟩) ∈ (Base‘𝑆))
179	21, 22, 58	grplid 18780	. . . . . . . . . 10 ⊢ ((𝑆 ∈ Grp ∧ (𝑀‘⟨“𝐾𝐿”⟩) ∈ (Base‘𝑆)) → ((0g‘𝑆) · (𝑀‘⟨“𝐾𝐿”⟩)) = (𝑀‘⟨“𝐾𝐿”⟩))
180	177, 178, 179	syl2anc 584	. . . . . . . . 9 ⊢ (((𝜑 ∧ ¬ 𝐼 ∈ {𝐾, 𝐿}) ∧ ¬ 𝐽 ∈ {𝐾, 𝐿}) → ((0g‘𝑆) · (𝑀‘⟨“𝐾𝐿”⟩)) = (𝑀‘⟨“𝐾𝐿”⟩))
181	174, 180	eqtrd 2776	. . . . . . . 8 ⊢ (((𝜑 ∧ ¬ 𝐼 ∈ {𝐾, 𝐿}) ∧ ¬ 𝐽 ∈ {𝐾, 𝐿}) → (( I ↾ 𝐷) · (𝑀‘⟨“𝐾𝐿”⟩)) = (𝑀‘⟨“𝐾𝐿”⟩))
182	181	oveq2d 7373	. . . . . . 7 ⊢ (((𝜑 ∧ ¬ 𝐼 ∈ {𝐾, 𝐿}) ∧ ¬ 𝐽 ∈ {𝐾, 𝐿}) → ((𝑀‘⟨“𝐼𝐽”⟩) · (( I ↾ 𝐷) · (𝑀‘⟨“𝐾𝐿”⟩))) = ((𝑀‘⟨“𝐼𝐽”⟩) · (𝑀‘⟨“𝐾𝐿”⟩)))
183	13	ad2antrr 724	. . . . . . . . 9 ⊢ (((𝜑 ∧ ¬ 𝐼 ∈ {𝐾, 𝐿}) ∧ ¬ 𝐽 ∈ {𝐾, 𝐿}) → (𝑀‘⟨“𝐼𝐽”⟩) ∈ (Base‘𝑆))
184	7, 146, 147, 148, 151, 27	cycpm2tr 31968	. . . . . . . . . 10 ⊢ (((𝜑 ∧ ¬ 𝐼 ∈ {𝐾, 𝐿}) ∧ ¬ 𝐽 ∈ {𝐾, 𝐿}) → (𝑀‘⟨“𝐽𝐾”⟩) = ((pmTrsp‘𝐷)‘{𝐽, 𝐾}))
185	50, 12, 21	symgtrf 19251	. . . . . . . . . . 11 ⊢ ran (pmTrsp‘𝐷) ⊆ (Base‘𝑆)
186	10, 16	prssd 4782	. . . . . . . . . . . . 13 ⊢ (𝜑 → {𝐽, 𝐾} ⊆ 𝐷)
187	186	ad2antrr 724	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ ¬ 𝐼 ∈ {𝐾, 𝐿}) ∧ ¬ 𝐽 ∈ {𝐾, 𝐿}) → {𝐽, 𝐾} ⊆ 𝐷)
188		enpr2 9938	. . . . . . . . . . . . 13 ⊢ ((𝐽 ∈ 𝐷 ∧ 𝐾 ∈ 𝐷 ∧ 𝐽 ≠ 𝐾) → {𝐽, 𝐾} ≈ 2o)
189	147, 148, 151, 188	syl3anc 1371	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ ¬ 𝐼 ∈ {𝐾, 𝐿}) ∧ ¬ 𝐽 ∈ {𝐾, 𝐿}) → {𝐽, 𝐾} ≈ 2o)
190	27, 50	pmtrrn 19239	. . . . . . . . . . . 12 ⊢ ((𝐷 ∈ 𝑉 ∧ {𝐽, 𝐾} ⊆ 𝐷 ∧ {𝐽, 𝐾} ≈ 2o) → ((pmTrsp‘𝐷)‘{𝐽, 𝐾}) ∈ ran (pmTrsp‘𝐷))
191	146, 187, 189, 190	syl3anc 1371	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ ¬ 𝐼 ∈ {𝐾, 𝐿}) ∧ ¬ 𝐽 ∈ {𝐾, 𝐿}) → ((pmTrsp‘𝐷)‘{𝐽, 𝐾}) ∈ ran (pmTrsp‘𝐷))
192	185, 191	sselid 3942	. . . . . . . . . 10 ⊢ (((𝜑 ∧ ¬ 𝐼 ∈ {𝐾, 𝐿}) ∧ ¬ 𝐽 ∈ {𝐾, 𝐿}) → ((pmTrsp‘𝐷)‘{𝐽, 𝐾}) ∈ (Base‘𝑆))
193	184, 192	eqeltrd 2838	. . . . . . . . 9 ⊢ (((𝜑 ∧ ¬ 𝐼 ∈ {𝐾, 𝐿}) ∧ ¬ 𝐽 ∈ {𝐾, 𝐿}) → (𝑀‘⟨“𝐽𝐾”⟩) ∈ (Base‘𝑆))
194	151	necomd 2999	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ ¬ 𝐼 ∈ {𝐾, 𝐿}) ∧ ¬ 𝐽 ∈ {𝐾, 𝐿}) → 𝐾 ≠ 𝐽)
195	7, 146, 148, 147, 194, 27	cycpm2tr 31968	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ ¬ 𝐼 ∈ {𝐾, 𝐿}) ∧ ¬ 𝐽 ∈ {𝐾, 𝐿}) → (𝑀‘⟨“𝐾𝐽”⟩) = ((pmTrsp‘𝐷)‘{𝐾, 𝐽}))
196		prcom 4693	. . . . . . . . . . . . . 14 ⊢ {𝐽, 𝐾} = {𝐾, 𝐽}
197	196	a1i 11	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ ¬ 𝐼 ∈ {𝐾, 𝐿}) ∧ ¬ 𝐽 ∈ {𝐾, 𝐿}) → {𝐽, 𝐾} = {𝐾, 𝐽})
198	197	fveq2d 6846	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ ¬ 𝐼 ∈ {𝐾, 𝐿}) ∧ ¬ 𝐽 ∈ {𝐾, 𝐿}) → ((pmTrsp‘𝐷)‘{𝐽, 𝐾}) = ((pmTrsp‘𝐷)‘{𝐾, 𝐽}))
199	195, 198	eqtr4d 2779	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ ¬ 𝐼 ∈ {𝐾, 𝐿}) ∧ ¬ 𝐽 ∈ {𝐾, 𝐿}) → (𝑀‘⟨“𝐾𝐽”⟩) = ((pmTrsp‘𝐷)‘{𝐽, 𝐾}))
200	199, 192	eqeltrd 2838	. . . . . . . . . 10 ⊢ (((𝜑 ∧ ¬ 𝐼 ∈ {𝐾, 𝐿}) ∧ ¬ 𝐽 ∈ {𝐾, 𝐿}) → (𝑀‘⟨“𝐾𝐽”⟩) ∈ (Base‘𝑆))
201	21, 22	grpcl 18756	. . . . . . . . . 10 ⊢ ((𝑆 ∈ Grp ∧ (𝑀‘⟨“𝐾𝐽”⟩) ∈ (Base‘𝑆) ∧ (𝑀‘⟨“𝐾𝐿”⟩) ∈ (Base‘𝑆)) → ((𝑀‘⟨“𝐾𝐽”⟩) · (𝑀‘⟨“𝐾𝐿”⟩)) ∈ (Base‘𝑆))
202	177, 200, 178, 201	syl3anc 1371	. . . . . . . . 9 ⊢ (((𝜑 ∧ ¬ 𝐼 ∈ {𝐾, 𝐿}) ∧ ¬ 𝐽 ∈ {𝐾, 𝐿}) → ((𝑀‘⟨“𝐾𝐽”⟩) · (𝑀‘⟨“𝐾𝐿”⟩)) ∈ (Base‘𝑆))
203	21, 22	grpass 18757	. . . . . . . . 9 ⊢ ((𝑆 ∈ Grp ∧ ((𝑀‘⟨“𝐼𝐽”⟩) ∈ (Base‘𝑆) ∧ (𝑀‘⟨“𝐽𝐾”⟩) ∈ (Base‘𝑆) ∧ ((𝑀‘⟨“𝐾𝐽”⟩) · (𝑀‘⟨“𝐾𝐿”⟩)) ∈ (Base‘𝑆))) → (((𝑀‘⟨“𝐼𝐽”⟩) · (𝑀‘⟨“𝐽𝐾”⟩)) · ((𝑀‘⟨“𝐾𝐽”⟩) · (𝑀‘⟨“𝐾𝐿”⟩))) = ((𝑀‘⟨“𝐼𝐽”⟩) · ((𝑀‘⟨“𝐽𝐾”⟩) · ((𝑀‘⟨“𝐾𝐽”⟩) · (𝑀‘⟨“𝐾𝐿”⟩)))))
204	177, 183, 193, 202, 203	syl13anc 1372	. . . . . . . 8 ⊢ (((𝜑 ∧ ¬ 𝐼 ∈ {𝐾, 𝐿}) ∧ ¬ 𝐽 ∈ {𝐾, 𝐿}) → (((𝑀‘⟨“𝐼𝐽”⟩) · (𝑀‘⟨“𝐽𝐾”⟩)) · ((𝑀‘⟨“𝐾𝐽”⟩) · (𝑀‘⟨“𝐾𝐿”⟩))) = ((𝑀‘⟨“𝐼𝐽”⟩) · ((𝑀‘⟨“𝐽𝐾”⟩) · ((𝑀‘⟨“𝐾𝐽”⟩) · (𝑀‘⟨“𝐾𝐿”⟩)))))
205	21, 22	grpass 18757	. . . . . . . . . 10 ⊢ ((𝑆 ∈ Grp ∧ ((𝑀‘⟨“𝐽𝐾”⟩) ∈ (Base‘𝑆) ∧ (𝑀‘⟨“𝐾𝐽”⟩) ∈ (Base‘𝑆) ∧ (𝑀‘⟨“𝐾𝐿”⟩) ∈ (Base‘𝑆))) → (((𝑀‘⟨“𝐽𝐾”⟩) · (𝑀‘⟨“𝐾𝐽”⟩)) · (𝑀‘⟨“𝐾𝐿”⟩)) = ((𝑀‘⟨“𝐽𝐾”⟩) · ((𝑀‘⟨“𝐾𝐽”⟩) · (𝑀‘⟨“𝐾𝐿”⟩))))
206	177, 193, 200, 178, 205	syl13anc 1372	. . . . . . . . 9 ⊢ (((𝜑 ∧ ¬ 𝐼 ∈ {𝐾, 𝐿}) ∧ ¬ 𝐽 ∈ {𝐾, 𝐿}) → (((𝑀‘⟨“𝐽𝐾”⟩) · (𝑀‘⟨“𝐾𝐽”⟩)) · (𝑀‘⟨“𝐾𝐿”⟩)) = ((𝑀‘⟨“𝐽𝐾”⟩) · ((𝑀‘⟨“𝐾𝐽”⟩) · (𝑀‘⟨“𝐾𝐿”⟩))))
207	206	oveq2d 7373	. . . . . . . 8 ⊢ (((𝜑 ∧ ¬ 𝐼 ∈ {𝐾, 𝐿}) ∧ ¬ 𝐽 ∈ {𝐾, 𝐿}) → ((𝑀‘⟨“𝐼𝐽”⟩) · (((𝑀‘⟨“𝐽𝐾”⟩) · (𝑀‘⟨“𝐾𝐽”⟩)) · (𝑀‘⟨“𝐾𝐿”⟩))) = ((𝑀‘⟨“𝐼𝐽”⟩) · ((𝑀‘⟨“𝐽𝐾”⟩) · ((𝑀‘⟨“𝐾𝐽”⟩) · (𝑀‘⟨“𝐾𝐿”⟩)))))
208	184, 199	oveq12d 7375	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ ¬ 𝐼 ∈ {𝐾, 𝐿}) ∧ ¬ 𝐽 ∈ {𝐾, 𝐿}) → ((𝑀‘⟨“𝐽𝐾”⟩) · (𝑀‘⟨“𝐾𝐽”⟩)) = (((pmTrsp‘𝐷)‘{𝐽, 𝐾}) · ((pmTrsp‘𝐷)‘{𝐽, 𝐾})))
209	12, 21, 22	symgov 19165	. . . . . . . . . . . 12 ⊢ ((((pmTrsp‘𝐷)‘{𝐽, 𝐾}) ∈ (Base‘𝑆) ∧ ((pmTrsp‘𝐷)‘{𝐽, 𝐾}) ∈ (Base‘𝑆)) → (((pmTrsp‘𝐷)‘{𝐽, 𝐾}) · ((pmTrsp‘𝐷)‘{𝐽, 𝐾})) = (((pmTrsp‘𝐷)‘{𝐽, 𝐾}) ∘ ((pmTrsp‘𝐷)‘{𝐽, 𝐾})))
210	192, 192, 209	syl2anc 584	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ ¬ 𝐼 ∈ {𝐾, 𝐿}) ∧ ¬ 𝐽 ∈ {𝐾, 𝐿}) → (((pmTrsp‘𝐷)‘{𝐽, 𝐾}) · ((pmTrsp‘𝐷)‘{𝐽, 𝐾})) = (((pmTrsp‘𝐷)‘{𝐽, 𝐾}) ∘ ((pmTrsp‘𝐷)‘{𝐽, 𝐾})))
211	27, 50	pmtrfinv 19243	. . . . . . . . . . . 12 ⊢ (((pmTrsp‘𝐷)‘{𝐽, 𝐾}) ∈ ran (pmTrsp‘𝐷) → (((pmTrsp‘𝐷)‘{𝐽, 𝐾}) ∘ ((pmTrsp‘𝐷)‘{𝐽, 𝐾})) = ( I ↾ 𝐷))
212	191, 211	syl 17	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ ¬ 𝐼 ∈ {𝐾, 𝐿}) ∧ ¬ 𝐽 ∈ {𝐾, 𝐿}) → (((pmTrsp‘𝐷)‘{𝐽, 𝐾}) ∘ ((pmTrsp‘𝐷)‘{𝐽, 𝐾})) = ( I ↾ 𝐷))
213	208, 210, 212	3eqtrd 2780	. . . . . . . . . 10 ⊢ (((𝜑 ∧ ¬ 𝐼 ∈ {𝐾, 𝐿}) ∧ ¬ 𝐽 ∈ {𝐾, 𝐿}) → ((𝑀‘⟨“𝐽𝐾”⟩) · (𝑀‘⟨“𝐾𝐽”⟩)) = ( I ↾ 𝐷))
214	213	oveq1d 7372	. . . . . . . . 9 ⊢ (((𝜑 ∧ ¬ 𝐼 ∈ {𝐾, 𝐿}) ∧ ¬ 𝐽 ∈ {𝐾, 𝐿}) → (((𝑀‘⟨“𝐽𝐾”⟩) · (𝑀‘⟨“𝐾𝐽”⟩)) · (𝑀‘⟨“𝐾𝐿”⟩)) = (( I ↾ 𝐷) · (𝑀‘⟨“𝐾𝐿”⟩)))
215	214	oveq2d 7373	. . . . . . . 8 ⊢ (((𝜑 ∧ ¬ 𝐼 ∈ {𝐾, 𝐿}) ∧ ¬ 𝐽 ∈ {𝐾, 𝐿}) → ((𝑀‘⟨“𝐼𝐽”⟩) · (((𝑀‘⟨“𝐽𝐾”⟩) · (𝑀‘⟨“𝐾𝐽”⟩)) · (𝑀‘⟨“𝐾𝐿”⟩))) = ((𝑀‘⟨“𝐼𝐽”⟩) · (( I ↾ 𝐷) · (𝑀‘⟨“𝐾𝐿”⟩))))
216	204, 207, 215	3eqtr2rd 2783	. . . . . . 7 ⊢ (((𝜑 ∧ ¬ 𝐼 ∈ {𝐾, 𝐿}) ∧ ¬ 𝐽 ∈ {𝐾, 𝐿}) → ((𝑀‘⟨“𝐼𝐽”⟩) · (( I ↾ 𝐷) · (𝑀‘⟨“𝐾𝐿”⟩))) = (((𝑀‘⟨“𝐼𝐽”⟩) · (𝑀‘⟨“𝐽𝐾”⟩)) · ((𝑀‘⟨“𝐾𝐽”⟩) · (𝑀‘⟨“𝐾𝐿”⟩))))
217	182, 216	eqtr3d 2778	. . . . . 6 ⊢ (((𝜑 ∧ ¬ 𝐼 ∈ {𝐾, 𝐿}) ∧ ¬ 𝐽 ∈ {𝐾, 𝐿}) → ((𝑀‘⟨“𝐼𝐽”⟩) · (𝑀‘⟨“𝐾𝐿”⟩)) = (((𝑀‘⟨“𝐼𝐽”⟩) · (𝑀‘⟨“𝐽𝐾”⟩)) · ((𝑀‘⟨“𝐾𝐽”⟩) · (𝑀‘⟨“𝐾𝐿”⟩))))
218	6, 15	oveq12d 7375	. . . . . . 7 ⊢ (𝜑 → (𝐸 · 𝐹) = ((𝑀‘⟨“𝐼𝐽”⟩) · (𝑀‘⟨“𝐾𝐿”⟩)))
219	218	ad2antrr 724	. . . . . 6 ⊢ (((𝜑 ∧ ¬ 𝐼 ∈ {𝐾, 𝐿}) ∧ ¬ 𝐽 ∈ {𝐾, 𝐿}) → (𝐸 · 𝐹) = ((𝑀‘⟨“𝐼𝐽”⟩) · (𝑀‘⟨“𝐾𝐿”⟩)))
220	7, 12, 146, 147, 148, 149, 151, 157, 158, 22	cyc3co2 31989	. . . . . . . 8 ⊢ (((𝜑 ∧ ¬ 𝐼 ∈ {𝐾, 𝐿}) ∧ ¬ 𝐽 ∈ {𝐾, 𝐿}) → (𝑀‘⟨“𝐽𝐾𝐼”⟩) = ((𝑀‘⟨“𝐽𝐼”⟩) · (𝑀‘⟨“𝐽𝐾”⟩)))
221	134	oveq1d 7372	. . . . . . . . 9 ⊢ (𝜑 → ((𝑀‘⟨“𝐼𝐽”⟩) · (𝑀‘⟨“𝐽𝐾”⟩)) = ((𝑀‘⟨“𝐽𝐼”⟩) · (𝑀‘⟨“𝐽𝐾”⟩)))
222	221	ad2antrr 724	. . . . . . . 8 ⊢ (((𝜑 ∧ ¬ 𝐼 ∈ {𝐾, 𝐿}) ∧ ¬ 𝐽 ∈ {𝐾, 𝐿}) → ((𝑀‘⟨“𝐼𝐽”⟩) · (𝑀‘⟨“𝐽𝐾”⟩)) = ((𝑀‘⟨“𝐽𝐼”⟩) · (𝑀‘⟨“𝐽𝐾”⟩)))
223	220, 222	eqtr4d 2779	. . . . . . 7 ⊢ (((𝜑 ∧ ¬ 𝐼 ∈ {𝐾, 𝐿}) ∧ ¬ 𝐽 ∈ {𝐾, 𝐿}) → (𝑀‘⟨“𝐽𝐾𝐼”⟩) = ((𝑀‘⟨“𝐼𝐽”⟩) · (𝑀‘⟨“𝐽𝐾”⟩)))
224	7, 12, 146, 148, 161, 147, 162, 166, 151, 22	cyc3co2 31989	. . . . . . 7 ⊢ (((𝜑 ∧ ¬ 𝐼 ∈ {𝐾, 𝐿}) ∧ ¬ 𝐽 ∈ {𝐾, 𝐿}) → (𝑀‘⟨“𝐾𝐿𝐽”⟩) = ((𝑀‘⟨“𝐾𝐽”⟩) · (𝑀‘⟨“𝐾𝐿”⟩)))
225	223, 224	oveq12d 7375	. . . . . 6 ⊢ (((𝜑 ∧ ¬ 𝐼 ∈ {𝐾, 𝐿}) ∧ ¬ 𝐽 ∈ {𝐾, 𝐿}) → ((𝑀‘⟨“𝐽𝐾𝐼”⟩) · (𝑀‘⟨“𝐾𝐿𝐽”⟩)) = (((𝑀‘⟨“𝐼𝐽”⟩) · (𝑀‘⟨“𝐽𝐾”⟩)) · ((𝑀‘⟨“𝐾𝐽”⟩) · (𝑀‘⟨“𝐾𝐿”⟩))))
226	217, 219, 225	3eqtr4d 2786	. . . . 5 ⊢ (((𝜑 ∧ ¬ 𝐼 ∈ {𝐾, 𝐿}) ∧ ¬ 𝐽 ∈ {𝐾, 𝐿}) → (𝐸 · 𝐹) = ((𝑀‘⟨“𝐽𝐾𝐼”⟩) · (𝑀‘⟨“𝐾𝐿𝐽”⟩)))
227	176	grpmndd 18760	. . . . . . 7 ⊢ (𝜑 → 𝑆 ∈ Mnd)
228	227	ad2antrr 724	. . . . . 6 ⊢ (((𝜑 ∧ ¬ 𝐼 ∈ {𝐾, 𝐿}) ∧ ¬ 𝐽 ∈ {𝐾, 𝐿}) → 𝑆 ∈ Mnd)
229	7, 12, 146, 147, 148, 149, 151, 157, 158	cycpm3cl 31984	. . . . . 6 ⊢ (((𝜑 ∧ ¬ 𝐼 ∈ {𝐾, 𝐿}) ∧ ¬ 𝐽 ∈ {𝐾, 𝐿}) → (𝑀‘⟨“𝐽𝐾𝐼”⟩) ∈ (Base‘𝑆))
230	224, 202	eqeltrd 2838	. . . . . 6 ⊢ (((𝜑 ∧ ¬ 𝐼 ∈ {𝐾, 𝐿}) ∧ ¬ 𝐽 ∈ {𝐾, 𝐿}) → (𝑀‘⟨“𝐾𝐿𝐽”⟩) ∈ (Base‘𝑆))
231	21, 22	gsumws2 18652	. . . . . 6 ⊢ ((𝑆 ∈ Mnd ∧ (𝑀‘⟨“𝐽𝐾𝐼”⟩) ∈ (Base‘𝑆) ∧ (𝑀‘⟨“𝐾𝐿𝐽”⟩) ∈ (Base‘𝑆)) → (𝑆 Σg ⟨“(𝑀‘⟨“𝐽𝐾𝐼”⟩)(𝑀‘⟨“𝐾𝐿𝐽”⟩)”⟩) = ((𝑀‘⟨“𝐽𝐾𝐼”⟩) · (𝑀‘⟨“𝐾𝐿𝐽”⟩)))
232	228, 229, 230, 231	syl3anc 1371	. . . . 5 ⊢ (((𝜑 ∧ ¬ 𝐼 ∈ {𝐾, 𝐿}) ∧ ¬ 𝐽 ∈ {𝐾, 𝐿}) → (𝑆 Σg ⟨“(𝑀‘⟨“𝐽𝐾𝐼”⟩)(𝑀‘⟨“𝐾𝐿𝐽”⟩)”⟩) = ((𝑀‘⟨“𝐽𝐾𝐼”⟩) · (𝑀‘⟨“𝐾𝐿𝐽”⟩)))
233	226, 232	eqtr4d 2779	. . . 4 ⊢ (((𝜑 ∧ ¬ 𝐼 ∈ {𝐾, 𝐿}) ∧ ¬ 𝐽 ∈ {𝐾, 𝐿}) → (𝐸 · 𝐹) = (𝑆 Σg ⟨“(𝑀‘⟨“𝐽𝐾𝐼”⟩)(𝑀‘⟨“𝐾𝐿𝐽”⟩)”⟩))
234	169, 172, 233	rspcedvd 3583	. . 3 ⊢ (((𝜑 ∧ ¬ 𝐼 ∈ {𝐾, 𝐿}) ∧ ¬ 𝐽 ∈ {𝐾, 𝐿}) → ∃𝑐 ∈ Word 𝐶(𝐸 · 𝐹) = (𝑆 Σg 𝑐))
235	145, 234	pm2.61dan 811	. 2 ⊢ ((𝜑 ∧ ¬ 𝐼 ∈ {𝐾, 𝐿}) → ∃𝑐 ∈ Word 𝐶(𝐸 · 𝐹) = (𝑆 Σg 𝑐))
236	104, 235	pm2.61dan 811	1 ⊢ (𝜑 → ∃𝑐 ∈ Word 𝐶(𝐸 · 𝐹) = (𝑆 Σg 𝑐))

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 396   ∧ w3a 1087   = wceq 1541   ∈ wcel 2106   ≠ wne 2943  ∃wrex 3073   ∖ cdif 3907   ⊆ wss 3910  ∅c0 4282  {csn 4586  {cpr 4588  ∪ cuni 4865   class class class wbr 5105   I cid 5530  ^◡ccnv 5632  ran crn 5634   ↾ cres 5635   “ cima 5636   ∘ ccom 5637  ‘cfv 6496  (class class class)co 7357  2_oc2o 8406   ≈ cen 8880  3c3 12209  ♯chash 14230  Word cword 14402  ⟨“cs1 14483  ⟨“cs2 14730  ⟨“cs3 14731  Basecbs 17083  +_gcplusg 17133  0_gc0g 17321   Σ_g cgsu 17322  Mndcmnd 18556  Grpcgrp 18748  SymGrpcsymg 19148  pmTrspcpmtr 19223  pmEvencevpm 19272  toCycctocyc 31955

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2707  ax-rep 5242  ax-sep 5256  ax-nul 5263  ax-pow 5320  ax-pr 5384  ax-un 7672  ax-reg 9528  ax-ac2 10399  ax-cnex 11107  ax-resscn 11108  ax-1cn 11109  ax-icn 11110  ax-addcl 11111  ax-addrcl 11112  ax-mulcl 11113  ax-mulrcl 11114  ax-mulcom 11115  ax-addass 11116  ax-mulass 11117  ax-distr 11118  ax-i2m1 11119  ax-1ne0 11120  ax-1rid 11121  ax-rnegex 11122  ax-rrecex 11123  ax-cnre 11124  ax-pre-lttri 11125  ax-pre-lttrn 11126  ax-pre-ltadd 11127  ax-pre-mulgt0 11128  ax-pre-sup 11129

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3or 1088  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2538  df-eu 2567  df-clab 2714  df-cleq 2728  df-clel 2814  df-nfc 2889  df-ne 2944  df-nel 3050  df-ral 3065  df-rex 3074  df-rmo 3353  df-reu 3354  df-rab 3408  df-v 3447  df-sbc 3740  df-csb 3856  df-dif 3913  df-un 3915  df-in 3917  df-ss 3927  df-pss 3929  df-nul 4283  df-if 4487  df-pw 4562  df-sn 4587  df-pr 4589  df-tp 4591  df-op 4593  df-uni 4866  df-int 4908  df-iun 4956  df-br 5106  df-opab 5168  df-mpt 5189  df-tr 5223  df-id 5531  df-eprel 5537  df-po 5545  df-so 5546  df-fr 5588  df-se 5589  df-we 5590  df-xp 5639  df-rel 5640  df-cnv 5641  df-co 5642  df-dm 5643  df-rn 5644  df-res 5645  df-ima 5646  df-pred 6253  df-ord 6320  df-on 6321  df-lim 6322  df-suc 6323  df-iota 6448  df-fun 6498  df-fn 6499  df-f 6500  df-f1 6501  df-fo 6502  df-f1o 6503  df-fv 6504  df-isom 6505  df-riota 7313  df-ov 7360  df-oprab 7361  df-mpo 7362  df-om 7803  df-1st 7921  df-2nd 7922  df-frecs 8212  df-wrecs 8243  df-recs 8317  df-rdg 8356  df-1o 8412  df-2o 8413  df-er 8648  df-map 8767  df-en 8884  df-dom 8885  df-sdom 8886  df-fin 8887  df-sup 9378  df-inf 9379  df-card 9875  df-ac 10052  df-pnf 11191  df-mnf 11192  df-xr 11193  df-ltxr 11194  df-le 11195  df-sub 11387  df-neg 11388  df-div 11813  df-nn 12154  df-2 12216  df-3 12217  df-4 12218  df-5 12219  df-6 12220  df-7 12221  df-8 12222  df-9 12223  df-n0 12414  df-xnn0 12486  df-z 12500  df-uz 12764  df-rp 12916  df-fz 13425  df-fzo 13568  df-fl 13697  df-mod 13775  df-seq 13907  df-hash 14231  df-word 14403  df-concat 14459  df-s1 14484  df-substr 14529  df-pfx 14559  df-csh 14677  df-s2 14737  df-s3 14738  df-struct 17019  df-sets 17036  df-slot 17054  df-ndx 17066  df-base 17084  df-ress 17113  df-plusg 17146  df-tset 17152  df-0g 17323  df-gsum 17324  df-mgm 18497  df-sgrp 18546  df-mnd 18557  df-submnd 18602  df-efmnd 18679  df-grp 18751  df-symg 19149  df-pmtr 19224  df-tocyc 31956

This theorem is referenced by:  cyc3genpm  32001