Theorem cyc3genpmlem 33591

Description: Lemma for cyc3genpm 33592. (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 14604	. . . . 5 ⊢ ∅ ∈ Word 𝐶
2	1	a1i 11	. . . 4 ⊢ (((𝜑 ∧ 𝐼 ∈ {𝐾, 𝐿}) ∧ 𝐽 ∈ {𝐾, 𝐿}) → ∅ ∈ Word 𝐶)
3		simpr 490	. . . . . 6 ⊢ ((((𝜑 ∧ 𝐼 ∈ {𝐾, 𝐿}) ∧ 𝐽 ∈ {𝐾, 𝐿}) ∧ 𝑐 = ∅) → 𝑐 = ∅)
4	3	oveq2d 7429	. . . . 5 ⊢ ((((𝜑 ∧ 𝐼 ∈ {𝐾, 𝐿}) ∧ 𝐽 ∈ {𝐾, 𝐿}) ∧ 𝑐 = ∅) → (𝑆 Σg 𝑐) = (𝑆 Σg ∅))
5	4	eqeq2d 2771	. . . 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 33560	. . . . . . . . 9 ⊢ (𝜑 → (𝑀‘⟨“𝐼𝐽”⟩) ∈ (Base‘𝑆))
14	6, 13	eqeltrd 2860	. . . . . . . 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 33560	. . . . . . . . 9 ⊢ (𝜑 → (𝑀‘⟨“𝐾𝐿”⟩) ∈ (Base‘𝑆))
20	15, 19	eqeltrd 2860	. . . . . . . 8 ⊢ (𝜑 → 𝐹 ∈ (Base‘𝑆))
21		eqid 2760	. . . . . . . . 9 ⊢ (Base‘𝑆) = (Base‘𝑆)
22		cyc3genpmlem.t	. . . . . . . . 9 ⊢ · = (+g‘𝑆)
23	12, 21, 22	symgov 19511	. . . . . . . 8 ⊢ ((𝐸 ∈ (Base‘𝑆) ∧ 𝐹 ∈ (Base‘𝑆)) → (𝐸 · 𝐹) = (𝐸 ∘ 𝐹))
24	14, 20, 23	syl2anc 596	. . . . . . 7 ⊢ (𝜑 → (𝐸 · 𝐹) = (𝐸 ∘ 𝐹))
25	24	ad2antrr 739	. . . . . 6 ⊢ (((𝜑 ∧ 𝐼 ∈ {𝐾, 𝐿}) ∧ 𝐽 ∈ {𝐾, 𝐿}) → (𝐸 · 𝐹) = (𝐸 ∘ 𝐹))
26	6	ad2antrr 739	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝐼 ∈ {𝐾, 𝐿}) ∧ 𝐽 ∈ {𝐾, 𝐿}) → 𝐸 = (𝑀‘⟨“𝐼𝐽”⟩))
27		eqid 2760	. . . . . . . . . 10 ⊢ (pmTrsp‘𝐷) = (pmTrsp‘𝐷)
28	7, 8, 9, 10, 11, 27	cycpm2tr 33559	. . . . . . . . 9 ⊢ (𝜑 → (𝑀‘⟨“𝐼𝐽”⟩) = ((pmTrsp‘𝐷)‘{𝐼, 𝐽}))
29	28	ad2antrr 739	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝐼 ∈ {𝐾, 𝐿}) ∧ 𝐽 ∈ {𝐾, 𝐿}) → (𝑀‘⟨“𝐼𝐽”⟩) = ((pmTrsp‘𝐷)‘{𝐼, 𝐽}))
30	26, 29	eqtrd 2795	. . . . . . 7 ⊢ (((𝜑 ∧ 𝐼 ∈ {𝐾, 𝐿}) ∧ 𝐽 ∈ {𝐾, 𝐿}) → 𝐸 = ((pmTrsp‘𝐷)‘{𝐼, 𝐽}))
31	7, 8, 16, 17, 18, 27	cycpm2tr 33559	. . . . . . . . 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 4783	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝐼 ∈ {𝐾, 𝐿}) ∧ 𝐽 ∈ {𝐾, 𝐿}) → {𝐼, 𝐽} ⊆ {𝐾, 𝐿})
40		ssprsseq 4786	. . . . . . . . . . 11 ⊢ ((𝐼 ∈ 𝐷 ∧ 𝐽 ∈ 𝐷 ∧ 𝐼 ≠ 𝐽) → ({𝐼, 𝐽} ⊆ {𝐾, 𝐿} ↔ {𝐼, 𝐽} = {𝐾, 𝐿}))
41	40	biimpa 482	. . . . . . . . . 10 ⊢ (((𝐼 ∈ 𝐷 ∧ 𝐽 ∈ 𝐷 ∧ 𝐼 ≠ 𝐽) ∧ {𝐼, 𝐽} ⊆ {𝐾, 𝐿}) → {𝐼, 𝐽} = {𝐾, 𝐿})
42	34, 35, 36, 39, 41	syl31anc 1400	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝐼 ∈ {𝐾, 𝐿}) ∧ 𝐽 ∈ {𝐾, 𝐿}) → {𝐼, 𝐽} = {𝐾, 𝐿})
43	42	fveq2d 6882	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝐼 ∈ {𝐾, 𝐿}) ∧ 𝐽 ∈ {𝐾, 𝐿}) → ((pmTrsp‘𝐷)‘{𝐼, 𝐽}) = ((pmTrsp‘𝐷)‘{𝐾, 𝐿}))
44	32, 33, 43	3eqtr4d 2805	. . . . . . 7 ⊢ (((𝜑 ∧ 𝐼 ∈ {𝐾, 𝐿}) ∧ 𝐽 ∈ {𝐾, 𝐿}) → 𝐹 = ((pmTrsp‘𝐷)‘{𝐼, 𝐽}))
45	30, 44	coeq12d 5844	. . . . . 6 ⊢ (((𝜑 ∧ 𝐼 ∈ {𝐾, 𝐿}) ∧ 𝐽 ∈ {𝐾, 𝐿}) → (𝐸 ∘ 𝐹) = (((pmTrsp‘𝐷)‘{𝐼, 𝐽}) ∘ ((pmTrsp‘𝐷)‘{𝐼, 𝐽})))
46	8	ad2antrr 739	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝐼 ∈ {𝐾, 𝐿}) ∧ 𝐽 ∈ {𝐾, 𝐿}) → 𝐷 ∈ 𝑉)
47	34, 35	prssd 4783	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝐼 ∈ {𝐾, 𝐿}) ∧ 𝐽 ∈ {𝐾, 𝐿}) → {𝐼, 𝐽} ⊆ 𝐷)
48		enpr2 10007	. . . . . . . . 9 ⊢ ((𝐼 ∈ 𝐷 ∧ 𝐽 ∈ 𝐷 ∧ 𝐼 ≠ 𝐽) → {𝐼, 𝐽} ≈ 2o)
49	34, 35, 36, 48	syl3anc 1398	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝐼 ∈ {𝐾, 𝐿}) ∧ 𝐽 ∈ {𝐾, 𝐿}) → {𝐼, 𝐽} ≈ 2o)
50		eqid 2760	. . . . . . . . 9 ⊢ ran (pmTrsp‘𝐷) = ran (pmTrsp‘𝐷)
51	27, 50	pmtrrn 19584	. . . . . . . 8 ⊢ ((𝐷 ∈ 𝑉 ∧ {𝐼, 𝐽} ⊆ 𝐷 ∧ {𝐼, 𝐽} ≈ 2o) → ((pmTrsp‘𝐷)‘{𝐼, 𝐽}) ∈ ran (pmTrsp‘𝐷))
52	46, 47, 49, 51	syl3anc 1398	. . . . . . 7 ⊢ (((𝜑 ∧ 𝐼 ∈ {𝐾, 𝐿}) ∧ 𝐽 ∈ {𝐾, 𝐿}) → ((pmTrsp‘𝐷)‘{𝐼, 𝐽}) ∈ ran (pmTrsp‘𝐷))
53	27, 50	pmtrfinv 19588	. . . . . . 7 ⊢ (((pmTrsp‘𝐷)‘{𝐼, 𝐽}) ∈ ran (pmTrsp‘𝐷) → (((pmTrsp‘𝐷)‘{𝐼, 𝐽}) ∘ ((pmTrsp‘𝐷)‘{𝐼, 𝐽})) = ( I ↾ 𝐷))
54	52, 53	syl 18	. . . . . 6 ⊢ (((𝜑 ∧ 𝐼 ∈ {𝐾, 𝐿}) ∧ 𝐽 ∈ {𝐾, 𝐿}) → (((pmTrsp‘𝐷)‘{𝐼, 𝐽}) ∘ ((pmTrsp‘𝐷)‘{𝐼, 𝐽})) = ( I ↾ 𝐷))
55	25, 45, 54	3eqtrd 2799	. . . . 5 ⊢ (((𝜑 ∧ 𝐼 ∈ {𝐾, 𝐿}) ∧ 𝐽 ∈ {𝐾, 𝐿}) → (𝐸 · 𝐹) = ( I ↾ 𝐷))
56	12	symgid 19528	. . . . . . 7 ⊢ (𝐷 ∈ 𝑉 → ( I ↾ 𝐷) = (0g‘𝑆))
57	46, 56	syl 18	. . . . . 6 ⊢ (((𝜑 ∧ 𝐼 ∈ {𝐾, 𝐿}) ∧ 𝐽 ∈ {𝐾, 𝐿}) → ( I ↾ 𝐷) = (0g‘𝑆))
58		eqid 2760	. . . . . . 7 ⊢ (0g‘𝑆) = (0g‘𝑆)
59	58	gsum0 18786	. . . . . 6 ⊢ (𝑆 Σg ∅) = (0g‘𝑆)
60	57, 59	eqtr4di 2813	. . . . 5 ⊢ (((𝜑 ∧ 𝐼 ∈ {𝐾, 𝐿}) ∧ 𝐽 ∈ {𝐾, 𝐿}) → ( I ↾ 𝐷) = (𝑆 Σg ∅))
61	55, 60	eqtrd 2795	. . . 4 ⊢ (((𝜑 ∧ 𝐼 ∈ {𝐾, 𝐿}) ∧ 𝐽 ∈ {𝐾, 𝐿}) → (𝐸 · 𝐹) = (𝑆 Σg ∅))
62	2, 5, 61	rspcedvd 3578	. . 3 ⊢ (((𝜑 ∧ 𝐼 ∈ {𝐾, 𝐿}) ∧ 𝐽 ∈ {𝐾, 𝐿}) → ∃𝑐 ∈ Word 𝐶(𝐸 · 𝐹) = (𝑆 Σg 𝑐))
63	8	ad2antrr 739	. . . . . . 7 ⊢ (((𝜑 ∧ 𝐼 ∈ {𝐾, 𝐿}) ∧ ¬ 𝐽 ∈ {𝐾, 𝐿}) → 𝐷 ∈ 𝑉)
64	9	ad2antrr 739	. . . . . . 7 ⊢ (((𝜑 ∧ 𝐼 ∈ {𝐾, 𝐿}) ∧ ¬ 𝐽 ∈ {𝐾, 𝐿}) → 𝐼 ∈ 𝐷)
65	16, 17	prssd 4783	. . . . . . . . 9 ⊢ (𝜑 → {𝐾, 𝐿} ⊆ 𝐷)
66	65	ad2antrr 739	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝐼 ∈ {𝐾, 𝐿}) ∧ ¬ 𝐽 ∈ {𝐾, 𝐿}) → {𝐾, 𝐿} ⊆ 𝐷)
67		simplr 781	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝐼 ∈ {𝐾, 𝐿}) ∧ ¬ 𝐽 ∈ {𝐾, 𝐿}) → 𝐼 ∈ {𝐾, 𝐿})
68		enpr2 10007	. . . . . . . . . . 11 ⊢ ((𝐾 ∈ 𝐷 ∧ 𝐿 ∈ 𝐷 ∧ 𝐾 ≠ 𝐿) → {𝐾, 𝐿} ≈ 2o)
69	16, 17, 18, 68	syl3anc 1398	. . . . . . . . . 10 ⊢ (𝜑 → {𝐾, 𝐿} ≈ 2o)
70	69	ad2antrr 739	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝐼 ∈ {𝐾, 𝐿}) ∧ ¬ 𝐽 ∈ {𝐾, 𝐿}) → {𝐾, 𝐿} ≈ 2o)
71		unidifsnel 33010	. . . . . . . . 9 ⊢ ((𝐼 ∈ {𝐾, 𝐿} ∧ {𝐾, 𝐿} ≈ 2o) → ∪ ({𝐾, 𝐿} ∖ {𝐼}) ∈ {𝐾, 𝐿})
72	67, 70, 71	syl2anc 596	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝐼 ∈ {𝐾, 𝐿}) ∧ ¬ 𝐽 ∈ {𝐾, 𝐿}) → ∪ ({𝐾, 𝐿} ∖ {𝐼}) ∈ {𝐾, 𝐿})
73	66, 72	sseldd 3932	. . . . . . 7 ⊢ (((𝜑 ∧ 𝐼 ∈ {𝐾, 𝐿}) ∧ ¬ 𝐽 ∈ {𝐾, 𝐿}) → ∪ ({𝐾, 𝐿} ∖ {𝐼}) ∈ 𝐷)
74	10	ad2antrr 739	. . . . . . 7 ⊢ (((𝜑 ∧ 𝐼 ∈ {𝐾, 𝐿}) ∧ ¬ 𝐽 ∈ {𝐾, 𝐿}) → 𝐽 ∈ 𝐷)
75		unidifsnne 33011	. . . . . . . . 9 ⊢ ((𝐼 ∈ {𝐾, 𝐿} ∧ {𝐾, 𝐿} ≈ 2o) → ∪ ({𝐾, 𝐿} ∖ {𝐼}) ≠ 𝐼)
76	67, 70, 75	syl2anc 596	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝐼 ∈ {𝐾, 𝐿}) ∧ ¬ 𝐽 ∈ {𝐾, 𝐿}) → ∪ ({𝐾, 𝐿} ∖ {𝐼}) ≠ 𝐼)
77	76	necomd 3010	. . . . . . 7 ⊢ (((𝜑 ∧ 𝐼 ∈ {𝐾, 𝐿}) ∧ ¬ 𝐽 ∈ {𝐾, 𝐿}) → 𝐼 ≠ ∪ ({𝐾, 𝐿} ∖ {𝐼}))
78		nelne2 3053	. . . . . . . 8 ⊢ ((∪ ({𝐾, 𝐿} ∖ {𝐼}) ∈ {𝐾, 𝐿} ∧ ¬ 𝐽 ∈ {𝐾, 𝐿}) → ∪ ({𝐾, 𝐿} ∖ {𝐼}) ≠ 𝐽)
79	72, 78	sylancom 600	. . . . . . 7 ⊢ (((𝜑 ∧ 𝐼 ∈ {𝐾, 𝐿}) ∧ ¬ 𝐽 ∈ {𝐾, 𝐿}) → ∪ ({𝐾, 𝐿} ∖ {𝐼}) ≠ 𝐽)
80	11	necomd 3010	. . . . . . . 8 ⊢ (𝜑 → 𝐽 ≠ 𝐼)
81	80	ad2antrr 739	. . . . . . 7 ⊢ (((𝜑 ∧ 𝐼 ∈ {𝐾, 𝐿}) ∧ ¬ 𝐽 ∈ {𝐾, 𝐿}) → 𝐽 ≠ 𝐼)
82	7, 12, 63, 64, 73, 74, 77, 79, 81	cycpm3cl2 33576	. . . . . 6 ⊢ (((𝜑 ∧ 𝐼 ∈ {𝐾, 𝐿}) ∧ ¬ 𝐽 ∈ {𝐾, 𝐿}) → (𝑀‘⟨“𝐼∪ ({𝐾, 𝐿} ∖ {𝐼})𝐽”⟩) ∈ (𝑀 “ (◡♯ “ {3})))
83		cyc3genpm.t	. . . . . 6 ⊢ 𝐶 = (𝑀 “ (◡♯ “ {3}))
84	82, 83	eleqtrrdi 2871	. . . . 5 ⊢ (((𝜑 ∧ 𝐼 ∈ {𝐾, 𝐿}) ∧ ¬ 𝐽 ∈ {𝐾, 𝐿}) → (𝑀‘⟨“𝐼∪ ({𝐾, 𝐿} ∖ {𝐼})𝐽”⟩) ∈ 𝐶)
85	84	s1cld 14670	. . . 4 ⊢ (((𝜑 ∧ 𝐼 ∈ {𝐾, 𝐿}) ∧ ¬ 𝐽 ∈ {𝐾, 𝐿}) → ⟨“(𝑀‘⟨“𝐼∪ ({𝐾, 𝐿} ∖ {𝐼})𝐽”⟩)”⟩ ∈ Word 𝐶)
86		simpr 490	. . . . . 6 ⊢ ((((𝜑 ∧ 𝐼 ∈ {𝐾, 𝐿}) ∧ ¬ 𝐽 ∈ {𝐾, 𝐿}) ∧ 𝑐 = ⟨“(𝑀‘⟨“𝐼∪ ({𝐾, 𝐿} ∖ {𝐼})𝐽”⟩)”⟩) → 𝑐 = ⟨“(𝑀‘⟨“𝐼∪ ({𝐾, 𝐿} ∖ {𝐼})𝐽”⟩)”⟩)
87	86	oveq2d 7429	. . . . 5 ⊢ ((((𝜑 ∧ 𝐼 ∈ {𝐾, 𝐿}) ∧ ¬ 𝐽 ∈ {𝐾, 𝐿}) ∧ 𝑐 = ⟨“(𝑀‘⟨“𝐼∪ ({𝐾, 𝐿} ∖ {𝐼})𝐽”⟩)”⟩) → (𝑆 Σg 𝑐) = (𝑆 Σg ⟨“(𝑀‘⟨“𝐼∪ ({𝐾, 𝐿} ∖ {𝐼})𝐽”⟩)”⟩))
88	87	eqeq2d 2771	. . . 4 ⊢ ((((𝜑 ∧ 𝐼 ∈ {𝐾, 𝐿}) ∧ ¬ 𝐽 ∈ {𝐾, 𝐿}) ∧ 𝑐 = ⟨“(𝑀‘⟨“𝐼∪ ({𝐾, 𝐿} ∖ {𝐼})𝐽”⟩)”⟩) → ((𝐸 · 𝐹) = (𝑆 Σg 𝑐) ↔ (𝐸 · 𝐹) = (𝑆 Σg ⟨“(𝑀‘⟨“𝐼∪ ({𝐾, 𝐿} ∖ {𝐼})𝐽”⟩)”⟩)))
89	7, 12, 63, 64, 73, 74, 77, 79, 81, 22	cyc3co2 33580	. . . . 5 ⊢ (((𝜑 ∧ 𝐼 ∈ {𝐾, 𝐿}) ∧ ¬ 𝐽 ∈ {𝐾, 𝐿}) → (𝑀‘⟨“𝐼∪ ({𝐾, 𝐿} ∖ {𝐼})𝐽”⟩) = ((𝑀‘⟨“𝐼𝐽”⟩) · (𝑀‘⟨“𝐼∪ ({𝐾, 𝐿} ∖ {𝐼})”⟩)))
90	7, 12, 63, 64, 73, 74, 77, 79, 81	cycpm3cl 33575	. . . . . 6 ⊢ (((𝜑 ∧ 𝐼 ∈ {𝐾, 𝐿}) ∧ ¬ 𝐽 ∈ {𝐾, 𝐿}) → (𝑀‘⟨“𝐼∪ ({𝐾, 𝐿} ∖ {𝐼})𝐽”⟩) ∈ (Base‘𝑆))
91	21	gsumws1 18947	. . . . . 6 ⊢ ((𝑀‘⟨“𝐼∪ ({𝐾, 𝐿} ∖ {𝐼})𝐽”⟩) ∈ (Base‘𝑆) → (𝑆 Σg ⟨“(𝑀‘⟨“𝐼∪ ({𝐾, 𝐿} ∖ {𝐼})𝐽”⟩)”⟩) = (𝑀‘⟨“𝐼∪ ({𝐾, 𝐿} ∖ {𝐼})𝐽”⟩))
92	90, 91	syl 18	. . . . 5 ⊢ (((𝜑 ∧ 𝐼 ∈ {𝐾, 𝐿}) ∧ ¬ 𝐽 ∈ {𝐾, 𝐿}) → (𝑆 Σg ⟨“(𝑀‘⟨“𝐼∪ ({𝐾, 𝐿} ∖ {𝐼})𝐽”⟩)”⟩) = (𝑀‘⟨“𝐼∪ ({𝐾, 𝐿} ∖ {𝐼})𝐽”⟩))
93	6	ad2antrr 739	. . . . . 6 ⊢ (((𝜑 ∧ 𝐼 ∈ {𝐾, 𝐿}) ∧ ¬ 𝐽 ∈ {𝐾, 𝐿}) → 𝐸 = (𝑀‘⟨“𝐼𝐽”⟩))
94		en2eleq 10011	. . . . . . . . 9 ⊢ ((𝐼 ∈ {𝐾, 𝐿} ∧ {𝐾, 𝐿} ≈ 2o) → {𝐾, 𝐿} = {𝐼, ∪ ({𝐾, 𝐿} ∖ {𝐼})})
95	67, 70, 94	syl2anc 596	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝐼 ∈ {𝐾, 𝐿}) ∧ ¬ 𝐽 ∈ {𝐾, 𝐿}) → {𝐾, 𝐿} = {𝐼, ∪ ({𝐾, 𝐿} ∖ {𝐼})})
96	95	fveq2d 6882	. . . . . . 7 ⊢ (((𝜑 ∧ 𝐼 ∈ {𝐾, 𝐿}) ∧ ¬ 𝐽 ∈ {𝐾, 𝐿}) → ((pmTrsp‘𝐷)‘{𝐾, 𝐿}) = ((pmTrsp‘𝐷)‘{𝐼, ∪ ({𝐾, 𝐿} ∖ {𝐼})}))
97	15, 31	eqtrd 2795	. . . . . . . 8 ⊢ (𝜑 → 𝐹 = ((pmTrsp‘𝐷)‘{𝐾, 𝐿}))
98	97	ad2antrr 739	. . . . . . 7 ⊢ (((𝜑 ∧ 𝐼 ∈ {𝐾, 𝐿}) ∧ ¬ 𝐽 ∈ {𝐾, 𝐿}) → 𝐹 = ((pmTrsp‘𝐷)‘{𝐾, 𝐿}))
99	7, 63, 64, 73, 77, 27	cycpm2tr 33559	. . . . . . 7 ⊢ (((𝜑 ∧ 𝐼 ∈ {𝐾, 𝐿}) ∧ ¬ 𝐽 ∈ {𝐾, 𝐿}) → (𝑀‘⟨“𝐼∪ ({𝐾, 𝐿} ∖ {𝐼})”⟩) = ((pmTrsp‘𝐷)‘{𝐼, ∪ ({𝐾, 𝐿} ∖ {𝐼})}))
100	96, 98, 99	3eqtr4d 2805	. . . . . 6 ⊢ (((𝜑 ∧ 𝐼 ∈ {𝐾, 𝐿}) ∧ ¬ 𝐽 ∈ {𝐾, 𝐿}) → 𝐹 = (𝑀‘⟨“𝐼∪ ({𝐾, 𝐿} ∖ {𝐼})”⟩))
101	93, 100	oveq12d 7431	. . . . 5 ⊢ (((𝜑 ∧ 𝐼 ∈ {𝐾, 𝐿}) ∧ ¬ 𝐽 ∈ {𝐾, 𝐿}) → (𝐸 · 𝐹) = ((𝑀‘⟨“𝐼𝐽”⟩) · (𝑀‘⟨“𝐼∪ ({𝐾, 𝐿} ∖ {𝐼})”⟩)))
102	89, 92, 101	3eqtr4rd 2806	. . . 4 ⊢ (((𝜑 ∧ 𝐼 ∈ {𝐾, 𝐿}) ∧ ¬ 𝐽 ∈ {𝐾, 𝐿}) → (𝐸 · 𝐹) = (𝑆 Σg ⟨“(𝑀‘⟨“𝐼∪ ({𝐾, 𝐿} ∖ {𝐼})𝐽”⟩)”⟩))
103	85, 88, 102	rspcedvd 3578	. . 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 33010	. . . . . . . . 9 ⊢ ((𝐽 ∈ {𝐾, 𝐿} ∧ {𝐾, 𝐿} ≈ 2o) → ∪ ({𝐾, 𝐿} ∖ {𝐽}) ∈ {𝐾, 𝐿})
111	108, 109, 110	syl2anc 596	. . . . . . . 8 ⊢ (((𝜑 ∧ ¬ 𝐼 ∈ {𝐾, 𝐿}) ∧ 𝐽 ∈ {𝐾, 𝐿}) → ∪ ({𝐾, 𝐿} ∖ {𝐽}) ∈ {𝐾, 𝐿})
112	107, 111	sseldd 3932	. . . . . . 7 ⊢ (((𝜑 ∧ ¬ 𝐼 ∈ {𝐾, 𝐿}) ∧ 𝐽 ∈ {𝐾, 𝐿}) → ∪ ({𝐾, 𝐿} ∖ {𝐽}) ∈ 𝐷)
113	9	ad2antrr 739	. . . . . . 7 ⊢ (((𝜑 ∧ ¬ 𝐼 ∈ {𝐾, 𝐿}) ∧ 𝐽 ∈ {𝐾, 𝐿}) → 𝐼 ∈ 𝐷)
114		unidifsnne 33011	. . . . . . . . 9 ⊢ ((𝐽 ∈ {𝐾, 𝐿} ∧ {𝐾, 𝐿} ≈ 2o) → ∪ ({𝐾, 𝐿} ∖ {𝐽}) ≠ 𝐽)
115	108, 109, 114	syl2anc 596	. . . . . . . 8 ⊢ (((𝜑 ∧ ¬ 𝐼 ∈ {𝐾, 𝐿}) ∧ 𝐽 ∈ {𝐾, 𝐿}) → ∪ ({𝐾, 𝐿} ∖ {𝐽}) ≠ 𝐽)
116	115	necomd 3010	. . . . . . 7 ⊢ (((𝜑 ∧ ¬ 𝐼 ∈ {𝐾, 𝐿}) ∧ 𝐽 ∈ {𝐾, 𝐿}) → 𝐽 ≠ ∪ ({𝐾, 𝐿} ∖ {𝐽}))
117		simplr 781	. . . . . . . 8 ⊢ (((𝜑 ∧ ¬ 𝐼 ∈ {𝐾, 𝐿}) ∧ 𝐽 ∈ {𝐾, 𝐿}) → ¬ 𝐼 ∈ {𝐾, 𝐿})
118		nelne2 3053	. . . . . . . 8 ⊢ ((∪ ({𝐾, 𝐿} ∖ {𝐽}) ∈ {𝐾, 𝐿} ∧ ¬ 𝐼 ∈ {𝐾, 𝐿}) → ∪ ({𝐾, 𝐿} ∖ {𝐽}) ≠ 𝐼)
119	111, 117, 118	syl2anc 596	. . . . . . 7 ⊢ (((𝜑 ∧ ¬ 𝐼 ∈ {𝐾, 𝐿}) ∧ 𝐽 ∈ {𝐾, 𝐿}) → ∪ ({𝐾, 𝐿} ∖ {𝐽}) ≠ 𝐼)
120	11	ad2antrr 739	. . . . . . 7 ⊢ (((𝜑 ∧ ¬ 𝐼 ∈ {𝐾, 𝐿}) ∧ 𝐽 ∈ {𝐾, 𝐿}) → 𝐼 ≠ 𝐽)
121	7, 12, 105, 106, 112, 113, 116, 119, 120	cycpm3cl2 33576	. . . . . 6 ⊢ (((𝜑 ∧ ¬ 𝐼 ∈ {𝐾, 𝐿}) ∧ 𝐽 ∈ {𝐾, 𝐿}) → (𝑀‘⟨“𝐽∪ ({𝐾, 𝐿} ∖ {𝐽})𝐼”⟩) ∈ (𝑀 “ (◡♯ “ {3})))
122	121, 83	eleqtrrdi 2871	. . . . 5 ⊢ (((𝜑 ∧ ¬ 𝐼 ∈ {𝐾, 𝐿}) ∧ 𝐽 ∈ {𝐾, 𝐿}) → (𝑀‘⟨“𝐽∪ ({𝐾, 𝐿} ∖ {𝐽})𝐼”⟩) ∈ 𝐶)
123	122	s1cld 14670	. . . 4 ⊢ (((𝜑 ∧ ¬ 𝐼 ∈ {𝐾, 𝐿}) ∧ 𝐽 ∈ {𝐾, 𝐿}) → ⟨“(𝑀‘⟨“𝐽∪ ({𝐾, 𝐿} ∖ {𝐽})𝐼”⟩)”⟩ ∈ Word 𝐶)
124		simpr 490	. . . . . 6 ⊢ ((((𝜑 ∧ ¬ 𝐼 ∈ {𝐾, 𝐿}) ∧ 𝐽 ∈ {𝐾, 𝐿}) ∧ 𝑐 = ⟨“(𝑀‘⟨“𝐽∪ ({𝐾, 𝐿} ∖ {𝐽})𝐼”⟩)”⟩) → 𝑐 = ⟨“(𝑀‘⟨“𝐽∪ ({𝐾, 𝐿} ∖ {𝐽})𝐼”⟩)”⟩)
125	124	oveq2d 7429	. . . . 5 ⊢ ((((𝜑 ∧ ¬ 𝐼 ∈ {𝐾, 𝐿}) ∧ 𝐽 ∈ {𝐾, 𝐿}) ∧ 𝑐 = ⟨“(𝑀‘⟨“𝐽∪ ({𝐾, 𝐿} ∖ {𝐽})𝐼”⟩)”⟩) → (𝑆 Σg 𝑐) = (𝑆 Σg ⟨“(𝑀‘⟨“𝐽∪ ({𝐾, 𝐿} ∖ {𝐽})𝐼”⟩)”⟩))
126	125	eqeq2d 2771	. . . 4 ⊢ ((((𝜑 ∧ ¬ 𝐼 ∈ {𝐾, 𝐿}) ∧ 𝐽 ∈ {𝐾, 𝐿}) ∧ 𝑐 = ⟨“(𝑀‘⟨“𝐽∪ ({𝐾, 𝐿} ∖ {𝐽})𝐼”⟩)”⟩) → ((𝐸 · 𝐹) = (𝑆 Σg 𝑐) ↔ (𝐸 · 𝐹) = (𝑆 Σg ⟨“(𝑀‘⟨“𝐽∪ ({𝐾, 𝐿} ∖ {𝐽})𝐼”⟩)”⟩)))
127	7, 12, 105, 106, 112, 113, 116, 119, 120, 22	cyc3co2 33580	. . . . 5 ⊢ (((𝜑 ∧ ¬ 𝐼 ∈ {𝐾, 𝐿}) ∧ 𝐽 ∈ {𝐾, 𝐿}) → (𝑀‘⟨“𝐽∪ ({𝐾, 𝐿} ∖ {𝐽})𝐼”⟩) = ((𝑀‘⟨“𝐽𝐼”⟩) · (𝑀‘⟨“𝐽∪ ({𝐾, 𝐿} ∖ {𝐽})”⟩)))
128	7, 12, 105, 106, 112, 113, 116, 119, 120	cycpm3cl 33575	. . . . . 6 ⊢ (((𝜑 ∧ ¬ 𝐼 ∈ {𝐾, 𝐿}) ∧ 𝐽 ∈ {𝐾, 𝐿}) → (𝑀‘⟨“𝐽∪ ({𝐾, 𝐿} ∖ {𝐽})𝐼”⟩) ∈ (Base‘𝑆))
129	21	gsumws1 18947	. . . . . 6 ⊢ ((𝑀‘⟨“𝐽∪ ({𝐾, 𝐿} ∖ {𝐽})𝐼”⟩) ∈ (Base‘𝑆) → (𝑆 Σg ⟨“(𝑀‘⟨“𝐽∪ ({𝐾, 𝐿} ∖ {𝐽})𝐼”⟩)”⟩) = (𝑀‘⟨“𝐽∪ ({𝐾, 𝐿} ∖ {𝐽})𝐼”⟩))
130	128, 129	syl 18	. . . . 5 ⊢ (((𝜑 ∧ ¬ 𝐼 ∈ {𝐾, 𝐿}) ∧ 𝐽 ∈ {𝐾, 𝐿}) → (𝑆 Σg ⟨“(𝑀‘⟨“𝐽∪ ({𝐾, 𝐿} ∖ {𝐽})𝐼”⟩)”⟩) = (𝑀‘⟨“𝐽∪ ({𝐾, 𝐿} ∖ {𝐽})𝐼”⟩))
131		prcom 4693	. . . . . . . . . 10 ⊢ {𝐼, 𝐽} = {𝐽, 𝐼}
132	131	fveq2i 6881	. . . . . . . . 9 ⊢ ((pmTrsp‘𝐷)‘{𝐼, 𝐽}) = ((pmTrsp‘𝐷)‘{𝐽, 𝐼})
133	7, 8, 10, 9, 80, 27	cycpm2tr 33559	. . . . . . . . 9 ⊢ (𝜑 → (𝑀‘⟨“𝐽𝐼”⟩) = ((pmTrsp‘𝐷)‘{𝐽, 𝐼}))
134	132, 28, 133	3eqtr4a 2821	. . . . . . . 8 ⊢ (𝜑 → (𝑀‘⟨“𝐼𝐽”⟩) = (𝑀‘⟨“𝐽𝐼”⟩))
135	6, 134	eqtrd 2795	. . . . . . 7 ⊢ (𝜑 → 𝐸 = (𝑀‘⟨“𝐽𝐼”⟩))
136	135	ad2antrr 739	. . . . . 6 ⊢ (((𝜑 ∧ ¬ 𝐼 ∈ {𝐾, 𝐿}) ∧ 𝐽 ∈ {𝐾, 𝐿}) → 𝐸 = (𝑀‘⟨“𝐽𝐼”⟩))
137		en2eleq 10011	. . . . . . . . 9 ⊢ ((𝐽 ∈ {𝐾, 𝐿} ∧ {𝐾, 𝐿} ≈ 2o) → {𝐾, 𝐿} = {𝐽, ∪ ({𝐾, 𝐿} ∖ {𝐽})})
138	108, 109, 137	syl2anc 596	. . . . . . . 8 ⊢ (((𝜑 ∧ ¬ 𝐼 ∈ {𝐾, 𝐿}) ∧ 𝐽 ∈ {𝐾, 𝐿}) → {𝐾, 𝐿} = {𝐽, ∪ ({𝐾, 𝐿} ∖ {𝐽})})
139	138	fveq2d 6882	. . . . . . 7 ⊢ (((𝜑 ∧ ¬ 𝐼 ∈ {𝐾, 𝐿}) ∧ 𝐽 ∈ {𝐾, 𝐿}) → ((pmTrsp‘𝐷)‘{𝐾, 𝐿}) = ((pmTrsp‘𝐷)‘{𝐽, ∪ ({𝐾, 𝐿} ∖ {𝐽})}))
140	97	ad2antrr 739	. . . . . . 7 ⊢ (((𝜑 ∧ ¬ 𝐼 ∈ {𝐾, 𝐿}) ∧ 𝐽 ∈ {𝐾, 𝐿}) → 𝐹 = ((pmTrsp‘𝐷)‘{𝐾, 𝐿}))
141	7, 105, 106, 112, 116, 27	cycpm2tr 33559	. . . . . . 7 ⊢ (((𝜑 ∧ ¬ 𝐼 ∈ {𝐾, 𝐿}) ∧ 𝐽 ∈ {𝐾, 𝐿}) → (𝑀‘⟨“𝐽∪ ({𝐾, 𝐿} ∖ {𝐽})”⟩) = ((pmTrsp‘𝐷)‘{𝐽, ∪ ({𝐾, 𝐿} ∖ {𝐽})}))
142	139, 140, 141	3eqtr4d 2805	. . . . . 6 ⊢ (((𝜑 ∧ ¬ 𝐼 ∈ {𝐾, 𝐿}) ∧ 𝐽 ∈ {𝐾, 𝐿}) → 𝐹 = (𝑀‘⟨“𝐽∪ ({𝐾, 𝐿} ∖ {𝐽})”⟩))
143	136, 142	oveq12d 7431	. . . . 5 ⊢ (((𝜑 ∧ ¬ 𝐼 ∈ {𝐾, 𝐿}) ∧ 𝐽 ∈ {𝐾, 𝐿}) → (𝐸 · 𝐹) = ((𝑀‘⟨“𝐽𝐼”⟩) · (𝑀‘⟨“𝐽∪ ({𝐾, 𝐿} ∖ {𝐽})”⟩)))
144	127, 130, 143	3eqtr4rd 2806	. . . 4 ⊢ (((𝜑 ∧ ¬ 𝐼 ∈ {𝐾, 𝐿}) ∧ 𝐽 ∈ {𝐾, 𝐿}) → (𝐸 · 𝐹) = (𝑆 Σg ⟨“(𝑀‘⟨“𝐽∪ ({𝐾, 𝐿} ∖ {𝐽})𝐼”⟩)”⟩))
145	123, 126, 144	rspcedvd 3578	. . 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 4615	. . . . . . 7 ⊢ (((𝜑 ∧ ¬ 𝐼 ∈ {𝐾, 𝐿}) ∧ ¬ 𝐽 ∈ {𝐾, 𝐿}) → 𝐽 ≠ 𝐾)
152		prid1g 4721	. . . . . . . . . 10 ⊢ (𝐾 ∈ 𝐷 → 𝐾 ∈ {𝐾, 𝐿})
153	16, 152	syl 18	. . . . . . . . 9 ⊢ (𝜑 → 𝐾 ∈ {𝐾, 𝐿})
154	153	ad2antrr 739	. . . . . . . 8 ⊢ (((𝜑 ∧ ¬ 𝐼 ∈ {𝐾, 𝐿}) ∧ ¬ 𝐽 ∈ {𝐾, 𝐿}) → 𝐾 ∈ {𝐾, 𝐿})
155		simplr 781	. . . . . . . 8 ⊢ (((𝜑 ∧ ¬ 𝐼 ∈ {𝐾, 𝐿}) ∧ ¬ 𝐽 ∈ {𝐾, 𝐿}) → ¬ 𝐼 ∈ {𝐾, 𝐿})
156		nelne2 3053	. . . . . . . 8 ⊢ ((𝐾 ∈ {𝐾, 𝐿} ∧ ¬ 𝐼 ∈ {𝐾, 𝐿}) → 𝐾 ≠ 𝐼)
157	154, 155, 156	syl2anc 596	. . . . . . 7 ⊢ (((𝜑 ∧ ¬ 𝐼 ∈ {𝐾, 𝐿}) ∧ ¬ 𝐽 ∈ {𝐾, 𝐿}) → 𝐾 ≠ 𝐼)
158	11	ad2antrr 739	. . . . . . 7 ⊢ (((𝜑 ∧ ¬ 𝐼 ∈ {𝐾, 𝐿}) ∧ ¬ 𝐽 ∈ {𝐾, 𝐿}) → 𝐼 ≠ 𝐽)
159	7, 12, 146, 147, 148, 149, 151, 157, 158	cycpm3cl2 33576	. . . . . 6 ⊢ (((𝜑 ∧ ¬ 𝐼 ∈ {𝐾, 𝐿}) ∧ ¬ 𝐽 ∈ {𝐾, 𝐿}) → (𝑀‘⟨“𝐽𝐾𝐼”⟩) ∈ (𝑀 “ (◡♯ “ {3})))
160	159, 83	eleqtrrdi 2871	. . . . 5 ⊢ (((𝜑 ∧ ¬ 𝐼 ∈ {𝐾, 𝐿}) ∧ ¬ 𝐽 ∈ {𝐾, 𝐿}) → (𝑀‘⟨“𝐽𝐾𝐼”⟩) ∈ 𝐶)
161	17	ad2antrr 739	. . . . . . 7 ⊢ (((𝜑 ∧ ¬ 𝐼 ∈ {𝐾, 𝐿}) ∧ ¬ 𝐽 ∈ {𝐾, 𝐿}) → 𝐿 ∈ 𝐷)
162	18	ad2antrr 739	. . . . . . 7 ⊢ (((𝜑 ∧ ¬ 𝐼 ∈ {𝐾, 𝐿}) ∧ ¬ 𝐽 ∈ {𝐾, 𝐿}) → 𝐾 ≠ 𝐿)
163		prid2g 4722	. . . . . . . . 9 ⊢ (𝐿 ∈ 𝐷 → 𝐿 ∈ {𝐾, 𝐿})
164	161, 163	syl 18	. . . . . . . 8 ⊢ (((𝜑 ∧ ¬ 𝐼 ∈ {𝐾, 𝐿}) ∧ ¬ 𝐽 ∈ {𝐾, 𝐿}) → 𝐿 ∈ {𝐾, 𝐿})
165		nelne2 3053	. . . . . . . 8 ⊢ ((𝐿 ∈ {𝐾, 𝐿} ∧ ¬ 𝐽 ∈ {𝐾, 𝐿}) → 𝐿 ≠ 𝐽)
166	164, 165	sylancom 600	. . . . . . 7 ⊢ (((𝜑 ∧ ¬ 𝐼 ∈ {𝐾, 𝐿}) ∧ ¬ 𝐽 ∈ {𝐾, 𝐿}) → 𝐿 ≠ 𝐽)
167	7, 12, 146, 148, 161, 147, 162, 166, 151	cycpm3cl2 33576	. . . . . 6 ⊢ (((𝜑 ∧ ¬ 𝐼 ∈ {𝐾, 𝐿}) ∧ ¬ 𝐽 ∈ {𝐾, 𝐿}) → (𝑀‘⟨“𝐾𝐿𝐽”⟩) ∈ (𝑀 “ (◡♯ “ {3})))
168	167, 83	eleqtrrdi 2871	. . . . 5 ⊢ (((𝜑 ∧ ¬ 𝐼 ∈ {𝐾, 𝐿}) ∧ ¬ 𝐽 ∈ {𝐾, 𝐿}) → (𝑀‘⟨“𝐾𝐿𝐽”⟩) ∈ 𝐶)
169	160, 168	s2cld 14942	. . . 4 ⊢ (((𝜑 ∧ ¬ 𝐼 ∈ {𝐾, 𝐿}) ∧ ¬ 𝐽 ∈ {𝐾, 𝐿}) → ⟨“(𝑀‘⟨“𝐽𝐾𝐼”⟩)(𝑀‘⟨“𝐾𝐿𝐽”⟩)”⟩ ∈ Word 𝐶)
170		simpr 490	. . . . . 6 ⊢ ((((𝜑 ∧ ¬ 𝐼 ∈ {𝐾, 𝐿}) ∧ ¬ 𝐽 ∈ {𝐾, 𝐿}) ∧ 𝑐 = ⟨“(𝑀‘⟨“𝐽𝐾𝐼”⟩)(𝑀‘⟨“𝐾𝐿𝐽”⟩)”⟩) → 𝑐 = ⟨“(𝑀‘⟨“𝐽𝐾𝐼”⟩)(𝑀‘⟨“𝐾𝐿𝐽”⟩)”⟩)
171	170	oveq2d 7429	. . . . 5 ⊢ ((((𝜑 ∧ ¬ 𝐼 ∈ {𝐾, 𝐿}) ∧ ¬ 𝐽 ∈ {𝐾, 𝐿}) ∧ 𝑐 = ⟨“(𝑀‘⟨“𝐽𝐾𝐼”⟩)(𝑀‘⟨“𝐾𝐿𝐽”⟩)”⟩) → (𝑆 Σg 𝑐) = (𝑆 Σg ⟨“(𝑀‘⟨“𝐽𝐾𝐼”⟩)(𝑀‘⟨“𝐾𝐿𝐽”⟩)”⟩))
172	171	eqeq2d 2771	. . . 4 ⊢ ((((𝜑 ∧ ¬ 𝐼 ∈ {𝐾, 𝐿}) ∧ ¬ 𝐽 ∈ {𝐾, 𝐿}) ∧ 𝑐 = ⟨“(𝑀‘⟨“𝐽𝐾𝐼”⟩)(𝑀‘⟨“𝐾𝐿𝐽”⟩)”⟩) → ((𝐸 · 𝐹) = (𝑆 Σg 𝑐) ↔ (𝐸 · 𝐹) = (𝑆 Σg ⟨“(𝑀‘⟨“𝐽𝐾𝐼”⟩)(𝑀‘⟨“𝐾𝐿𝐽”⟩)”⟩)))
173	146, 56	syl 18	. . . . . . . . . 10 ⊢ (((𝜑 ∧ ¬ 𝐼 ∈ {𝐾, 𝐿}) ∧ ¬ 𝐽 ∈ {𝐾, 𝐿}) → ( I ↾ 𝐷) = (0g‘𝑆))
174	173	oveq1d 7428	. . . . . . . . 9 ⊢ (((𝜑 ∧ ¬ 𝐼 ∈ {𝐾, 𝐿}) ∧ ¬ 𝐽 ∈ {𝐾, 𝐿}) → (( I ↾ 𝐷) · (𝑀‘⟨“𝐾𝐿”⟩)) = ((0g‘𝑆) · (𝑀‘⟨“𝐾𝐿”⟩)))
175	12	symggrp 19527	. . . . . . . . . . . 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 19091	. . . . . . . . . 10 ⊢ ((𝑆 ∈ Grp ∧ (𝑀‘⟨“𝐾𝐿”⟩) ∈ (Base‘𝑆)) → ((0g‘𝑆) · (𝑀‘⟨“𝐾𝐿”⟩)) = (𝑀‘⟨“𝐾𝐿”⟩))
180	177, 178, 179	syl2anc 596	. . . . . . . . 9 ⊢ (((𝜑 ∧ ¬ 𝐼 ∈ {𝐾, 𝐿}) ∧ ¬ 𝐽 ∈ {𝐾, 𝐿}) → ((0g‘𝑆) · (𝑀‘⟨“𝐾𝐿”⟩)) = (𝑀‘⟨“𝐾𝐿”⟩))
181	174, 180	eqtrd 2795	. . . . . . . 8 ⊢ (((𝜑 ∧ ¬ 𝐼 ∈ {𝐾, 𝐿}) ∧ ¬ 𝐽 ∈ {𝐾, 𝐿}) → (( I ↾ 𝐷) · (𝑀‘⟨“𝐾𝐿”⟩)) = (𝑀‘⟨“𝐾𝐿”⟩))
182	181	oveq2d 7429	. . . . . . 7 ⊢ (((𝜑 ∧ ¬ 𝐼 ∈ {𝐾, 𝐿}) ∧ ¬ 𝐽 ∈ {𝐾, 𝐿}) → ((𝑀‘⟨“𝐼𝐽”⟩) · (( I ↾ 𝐷) · (𝑀‘⟨“𝐾𝐿”⟩))) = ((𝑀‘⟨“𝐼𝐽”⟩) · (𝑀‘⟨“𝐾𝐿”⟩)))
183	13	ad2antrr 739	. . . . . . . . 9 ⊢ (((𝜑 ∧ ¬ 𝐼 ∈ {𝐾, 𝐿}) ∧ ¬ 𝐽 ∈ {𝐾, 𝐿}) → (𝑀‘⟨“𝐼𝐽”⟩) ∈ (Base‘𝑆))
184	7, 146, 147, 148, 151, 27	cycpm2tr 33559	. . . . . . . . . 10 ⊢ (((𝜑 ∧ ¬ 𝐼 ∈ {𝐾, 𝐿}) ∧ ¬ 𝐽 ∈ {𝐾, 𝐿}) → (𝑀‘⟨“𝐽𝐾”⟩) = ((pmTrsp‘𝐷)‘{𝐽, 𝐾}))
185	50, 12, 21	symgtrf 19596	. . . . . . . . . . 11 ⊢ ran (pmTrsp‘𝐷) ⊆ (Base‘𝑆)
186	10, 16	prssd 4783	. . . . . . . . . . . . 13 ⊢ (𝜑 → {𝐽, 𝐾} ⊆ 𝐷)
187	186	ad2antrr 739	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ ¬ 𝐼 ∈ {𝐾, 𝐿}) ∧ ¬ 𝐽 ∈ {𝐾, 𝐿}) → {𝐽, 𝐾} ⊆ 𝐷)
188		enpr2 10007	. . . . . . . . . . . . 13 ⊢ ((𝐽 ∈ 𝐷 ∧ 𝐾 ∈ 𝐷 ∧ 𝐽 ≠ 𝐾) → {𝐽, 𝐾} ≈ 2o)
189	147, 148, 151, 188	syl3anc 1398	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ ¬ 𝐼 ∈ {𝐾, 𝐿}) ∧ ¬ 𝐽 ∈ {𝐾, 𝐿}) → {𝐽, 𝐾} ≈ 2o)
190	27, 50	pmtrrn 19584	. . . . . . . . . . . 12 ⊢ ((𝐷 ∈ 𝑉 ∧ {𝐽, 𝐾} ⊆ 𝐷 ∧ {𝐽, 𝐾} ≈ 2o) → ((pmTrsp‘𝐷)‘{𝐽, 𝐾}) ∈ ran (pmTrsp‘𝐷))
191	146, 187, 189, 190	syl3anc 1398	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ ¬ 𝐼 ∈ {𝐾, 𝐿}) ∧ ¬ 𝐽 ∈ {𝐾, 𝐿}) → ((pmTrsp‘𝐷)‘{𝐽, 𝐾}) ∈ ran (pmTrsp‘𝐷))
192	185, 191	sselid 3929	. . . . . . . . . 10 ⊢ (((𝜑 ∧ ¬ 𝐼 ∈ {𝐾, 𝐿}) ∧ ¬ 𝐽 ∈ {𝐾, 𝐿}) → ((pmTrsp‘𝐷)‘{𝐽, 𝐾}) ∈ (Base‘𝑆))
193	184, 192	eqeltrd 2860	. . . . . . . . 9 ⊢ (((𝜑 ∧ ¬ 𝐼 ∈ {𝐾, 𝐿}) ∧ ¬ 𝐽 ∈ {𝐾, 𝐿}) → (𝑀‘⟨“𝐽𝐾”⟩) ∈ (Base‘𝑆))
194	151	necomd 3010	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ ¬ 𝐼 ∈ {𝐾, 𝐿}) ∧ ¬ 𝐽 ∈ {𝐾, 𝐿}) → 𝐾 ≠ 𝐽)
195	7, 146, 148, 147, 194, 27	cycpm2tr 33559	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ ¬ 𝐼 ∈ {𝐾, 𝐿}) ∧ ¬ 𝐽 ∈ {𝐾, 𝐿}) → (𝑀‘⟨“𝐾𝐽”⟩) = ((pmTrsp‘𝐷)‘{𝐾, 𝐽}))
196		prcom 4693	. . . . . . . . . . . . . 14 ⊢ {𝐽, 𝐾} = {𝐾, 𝐽}
197	196	a1i 11	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ ¬ 𝐼 ∈ {𝐾, 𝐿}) ∧ ¬ 𝐽 ∈ {𝐾, 𝐿}) → {𝐽, 𝐾} = {𝐾, 𝐽})
198	197	fveq2d 6882	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ ¬ 𝐼 ∈ {𝐾, 𝐿}) ∧ ¬ 𝐽 ∈ {𝐾, 𝐿}) → ((pmTrsp‘𝐷)‘{𝐽, 𝐾}) = ((pmTrsp‘𝐷)‘{𝐾, 𝐽}))
199	195, 198	eqtr4d 2798	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ ¬ 𝐼 ∈ {𝐾, 𝐿}) ∧ ¬ 𝐽 ∈ {𝐾, 𝐿}) → (𝑀‘⟨“𝐾𝐽”⟩) = ((pmTrsp‘𝐷)‘{𝐽, 𝐾}))
200	199, 192	eqeltrd 2860	. . . . . . . . . 10 ⊢ (((𝜑 ∧ ¬ 𝐼 ∈ {𝐾, 𝐿}) ∧ ¬ 𝐽 ∈ {𝐾, 𝐿}) → (𝑀‘⟨“𝐾𝐽”⟩) ∈ (Base‘𝑆))
201	21, 22	grpcl 19065	. . . . . . . . . 10 ⊢ ((𝑆 ∈ Grp ∧ (𝑀‘⟨“𝐾𝐽”⟩) ∈ (Base‘𝑆) ∧ (𝑀‘⟨“𝐾𝐿”⟩) ∈ (Base‘𝑆)) → ((𝑀‘⟨“𝐾𝐽”⟩) · (𝑀‘⟨“𝐾𝐿”⟩)) ∈ (Base‘𝑆))
202	177, 200, 178, 201	syl3anc 1398	. . . . . . . . 9 ⊢ (((𝜑 ∧ ¬ 𝐼 ∈ {𝐾, 𝐿}) ∧ ¬ 𝐽 ∈ {𝐾, 𝐿}) → ((𝑀‘⟨“𝐾𝐽”⟩) · (𝑀‘⟨“𝐾𝐿”⟩)) ∈ (Base‘𝑆))
203	21, 22	grpass 19066	. . . . . . . . 9 ⊢ ((𝑆 ∈ Grp ∧ ((𝑀‘⟨“𝐼𝐽”⟩) ∈ (Base‘𝑆) ∧ (𝑀‘⟨“𝐽𝐾”⟩) ∈ (Base‘𝑆) ∧ ((𝑀‘⟨“𝐾𝐽”⟩) · (𝑀‘⟨“𝐾𝐿”⟩)) ∈ (Base‘𝑆))) → (((𝑀‘⟨“𝐼𝐽”⟩) · (𝑀‘⟨“𝐽𝐾”⟩)) · ((𝑀‘⟨“𝐾𝐽”⟩) · (𝑀‘⟨“𝐾𝐿”⟩))) = ((𝑀‘⟨“𝐼𝐽”⟩) · ((𝑀‘⟨“𝐽𝐾”⟩) · ((𝑀‘⟨“𝐾𝐽”⟩) · (𝑀‘⟨“𝐾𝐿”⟩)))))
204	177, 183, 193, 202, 203	syl13anc 1399	. . . . . . . 8 ⊢ (((𝜑 ∧ ¬ 𝐼 ∈ {𝐾, 𝐿}) ∧ ¬ 𝐽 ∈ {𝐾, 𝐿}) → (((𝑀‘⟨“𝐼𝐽”⟩) · (𝑀‘⟨“𝐽𝐾”⟩)) · ((𝑀‘⟨“𝐾𝐽”⟩) · (𝑀‘⟨“𝐾𝐿”⟩))) = ((𝑀‘⟨“𝐼𝐽”⟩) · ((𝑀‘⟨“𝐽𝐾”⟩) · ((𝑀‘⟨“𝐾𝐽”⟩) · (𝑀‘⟨“𝐾𝐿”⟩)))))
205	21, 22	grpass 19066	. . . . . . . . . 10 ⊢ ((𝑆 ∈ Grp ∧ ((𝑀‘⟨“𝐽𝐾”⟩) ∈ (Base‘𝑆) ∧ (𝑀‘⟨“𝐾𝐽”⟩) ∈ (Base‘𝑆) ∧ (𝑀‘⟨“𝐾𝐿”⟩) ∈ (Base‘𝑆))) → (((𝑀‘⟨“𝐽𝐾”⟩) · (𝑀‘⟨“𝐾𝐽”⟩)) · (𝑀‘⟨“𝐾𝐿”⟩)) = ((𝑀‘⟨“𝐽𝐾”⟩) · ((𝑀‘⟨“𝐾𝐽”⟩) · (𝑀‘⟨“𝐾𝐿”⟩))))
206	177, 193, 200, 178, 205	syl13anc 1399	. . . . . . . . 9 ⊢ (((𝜑 ∧ ¬ 𝐼 ∈ {𝐾, 𝐿}) ∧ ¬ 𝐽 ∈ {𝐾, 𝐿}) → (((𝑀‘⟨“𝐽𝐾”⟩) · (𝑀‘⟨“𝐾𝐽”⟩)) · (𝑀‘⟨“𝐾𝐿”⟩)) = ((𝑀‘⟨“𝐽𝐾”⟩) · ((𝑀‘⟨“𝐾𝐽”⟩) · (𝑀‘⟨“𝐾𝐿”⟩))))
207	206	oveq2d 7429	. . . . . . . 8 ⊢ (((𝜑 ∧ ¬ 𝐼 ∈ {𝐾, 𝐿}) ∧ ¬ 𝐽 ∈ {𝐾, 𝐿}) → ((𝑀‘⟨“𝐼𝐽”⟩) · (((𝑀‘⟨“𝐽𝐾”⟩) · (𝑀‘⟨“𝐾𝐽”⟩)) · (𝑀‘⟨“𝐾𝐿”⟩))) = ((𝑀‘⟨“𝐼𝐽”⟩) · ((𝑀‘⟨“𝐽𝐾”⟩) · ((𝑀‘⟨“𝐾𝐽”⟩) · (𝑀‘⟨“𝐾𝐿”⟩)))))
208	184, 199	oveq12d 7431	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ ¬ 𝐼 ∈ {𝐾, 𝐿}) ∧ ¬ 𝐽 ∈ {𝐾, 𝐿}) → ((𝑀‘⟨“𝐽𝐾”⟩) · (𝑀‘⟨“𝐾𝐽”⟩)) = (((pmTrsp‘𝐷)‘{𝐽, 𝐾}) · ((pmTrsp‘𝐷)‘{𝐽, 𝐾})))
209	12, 21, 22	symgov 19511	. . . . . . . . . . . 12 ⊢ ((((pmTrsp‘𝐷)‘{𝐽, 𝐾}) ∈ (Base‘𝑆) ∧ ((pmTrsp‘𝐷)‘{𝐽, 𝐾}) ∈ (Base‘𝑆)) → (((pmTrsp‘𝐷)‘{𝐽, 𝐾}) · ((pmTrsp‘𝐷)‘{𝐽, 𝐾})) = (((pmTrsp‘𝐷)‘{𝐽, 𝐾}) ∘ ((pmTrsp‘𝐷)‘{𝐽, 𝐾})))
210	192, 192, 209	syl2anc 596	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ ¬ 𝐼 ∈ {𝐾, 𝐿}) ∧ ¬ 𝐽 ∈ {𝐾, 𝐿}) → (((pmTrsp‘𝐷)‘{𝐽, 𝐾}) · ((pmTrsp‘𝐷)‘{𝐽, 𝐾})) = (((pmTrsp‘𝐷)‘{𝐽, 𝐾}) ∘ ((pmTrsp‘𝐷)‘{𝐽, 𝐾})))
211	27, 50	pmtrfinv 19588	. . . . . . . . . . . 12 ⊢ (((pmTrsp‘𝐷)‘{𝐽, 𝐾}) ∈ ran (pmTrsp‘𝐷) → (((pmTrsp‘𝐷)‘{𝐽, 𝐾}) ∘ ((pmTrsp‘𝐷)‘{𝐽, 𝐾})) = ( I ↾ 𝐷))
212	191, 211	syl 18	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ ¬ 𝐼 ∈ {𝐾, 𝐿}) ∧ ¬ 𝐽 ∈ {𝐾, 𝐿}) → (((pmTrsp‘𝐷)‘{𝐽, 𝐾}) ∘ ((pmTrsp‘𝐷)‘{𝐽, 𝐾})) = ( I ↾ 𝐷))
213	208, 210, 212	3eqtrd 2799	. . . . . . . . . 10 ⊢ (((𝜑 ∧ ¬ 𝐼 ∈ {𝐾, 𝐿}) ∧ ¬ 𝐽 ∈ {𝐾, 𝐿}) → ((𝑀‘⟨“𝐽𝐾”⟩) · (𝑀‘⟨“𝐾𝐽”⟩)) = ( I ↾ 𝐷))
214	213	oveq1d 7428	. . . . . . . . 9 ⊢ (((𝜑 ∧ ¬ 𝐼 ∈ {𝐾, 𝐿}) ∧ ¬ 𝐽 ∈ {𝐾, 𝐿}) → (((𝑀‘⟨“𝐽𝐾”⟩) · (𝑀‘⟨“𝐾𝐽”⟩)) · (𝑀‘⟨“𝐾𝐿”⟩)) = (( I ↾ 𝐷) · (𝑀‘⟨“𝐾𝐿”⟩)))
215	214	oveq2d 7429	. . . . . . . 8 ⊢ (((𝜑 ∧ ¬ 𝐼 ∈ {𝐾, 𝐿}) ∧ ¬ 𝐽 ∈ {𝐾, 𝐿}) → ((𝑀‘⟨“𝐼𝐽”⟩) · (((𝑀‘⟨“𝐽𝐾”⟩) · (𝑀‘⟨“𝐾𝐽”⟩)) · (𝑀‘⟨“𝐾𝐿”⟩))) = ((𝑀‘⟨“𝐼𝐽”⟩) · (( I ↾ 𝐷) · (𝑀‘⟨“𝐾𝐿”⟩))))
216	204, 207, 215	3eqtr2rd 2802	. . . . . . 7 ⊢ (((𝜑 ∧ ¬ 𝐼 ∈ {𝐾, 𝐿}) ∧ ¬ 𝐽 ∈ {𝐾, 𝐿}) → ((𝑀‘⟨“𝐼𝐽”⟩) · (( I ↾ 𝐷) · (𝑀‘⟨“𝐾𝐿”⟩))) = (((𝑀‘⟨“𝐼𝐽”⟩) · (𝑀‘⟨“𝐽𝐾”⟩)) · ((𝑀‘⟨“𝐾𝐽”⟩) · (𝑀‘⟨“𝐾𝐿”⟩))))
217	182, 216	eqtr3d 2797	. . . . . 6 ⊢ (((𝜑 ∧ ¬ 𝐼 ∈ {𝐾, 𝐿}) ∧ ¬ 𝐽 ∈ {𝐾, 𝐿}) → ((𝑀‘⟨“𝐼𝐽”⟩) · (𝑀‘⟨“𝐾𝐿”⟩)) = (((𝑀‘⟨“𝐼𝐽”⟩) · (𝑀‘⟨“𝐽𝐾”⟩)) · ((𝑀‘⟨“𝐾𝐽”⟩) · (𝑀‘⟨“𝐾𝐿”⟩))))
218	6, 15	oveq12d 7431	. . . . . . 7 ⊢ (𝜑 → (𝐸 · 𝐹) = ((𝑀‘⟨“𝐼𝐽”⟩) · (𝑀‘⟨“𝐾𝐿”⟩)))
219	218	ad2antrr 739	. . . . . 6 ⊢ (((𝜑 ∧ ¬ 𝐼 ∈ {𝐾, 𝐿}) ∧ ¬ 𝐽 ∈ {𝐾, 𝐿}) → (𝐸 · 𝐹) = ((𝑀‘⟨“𝐼𝐽”⟩) · (𝑀‘⟨“𝐾𝐿”⟩)))
220	7, 12, 146, 147, 148, 149, 151, 157, 158, 22	cyc3co2 33580	. . . . . . . 8 ⊢ (((𝜑 ∧ ¬ 𝐼 ∈ {𝐾, 𝐿}) ∧ ¬ 𝐽 ∈ {𝐾, 𝐿}) → (𝑀‘⟨“𝐽𝐾𝐼”⟩) = ((𝑀‘⟨“𝐽𝐼”⟩) · (𝑀‘⟨“𝐽𝐾”⟩)))
221	134	oveq1d 7428	. . . . . . . . 9 ⊢ (𝜑 → ((𝑀‘⟨“𝐼𝐽”⟩) · (𝑀‘⟨“𝐽𝐾”⟩)) = ((𝑀‘⟨“𝐽𝐼”⟩) · (𝑀‘⟨“𝐽𝐾”⟩)))
222	221	ad2antrr 739	. . . . . . . 8 ⊢ (((𝜑 ∧ ¬ 𝐼 ∈ {𝐾, 𝐿}) ∧ ¬ 𝐽 ∈ {𝐾, 𝐿}) → ((𝑀‘⟨“𝐼𝐽”⟩) · (𝑀‘⟨“𝐽𝐾”⟩)) = ((𝑀‘⟨“𝐽𝐼”⟩) · (𝑀‘⟨“𝐽𝐾”⟩)))
223	220, 222	eqtr4d 2798	. . . . . . 7 ⊢ (((𝜑 ∧ ¬ 𝐼 ∈ {𝐾, 𝐿}) ∧ ¬ 𝐽 ∈ {𝐾, 𝐿}) → (𝑀‘⟨“𝐽𝐾𝐼”⟩) = ((𝑀‘⟨“𝐼𝐽”⟩) · (𝑀‘⟨“𝐽𝐾”⟩)))
224	7, 12, 146, 148, 161, 147, 162, 166, 151, 22	cyc3co2 33580	. . . . . . 7 ⊢ (((𝜑 ∧ ¬ 𝐼 ∈ {𝐾, 𝐿}) ∧ ¬ 𝐽 ∈ {𝐾, 𝐿}) → (𝑀‘⟨“𝐾𝐿𝐽”⟩) = ((𝑀‘⟨“𝐾𝐽”⟩) · (𝑀‘⟨“𝐾𝐿”⟩)))
225	223, 224	oveq12d 7431	. . . . . 6 ⊢ (((𝜑 ∧ ¬ 𝐼 ∈ {𝐾, 𝐿}) ∧ ¬ 𝐽 ∈ {𝐾, 𝐿}) → ((𝑀‘⟨“𝐽𝐾𝐼”⟩) · (𝑀‘⟨“𝐾𝐿𝐽”⟩)) = (((𝑀‘⟨“𝐼𝐽”⟩) · (𝑀‘⟨“𝐽𝐾”⟩)) · ((𝑀‘⟨“𝐾𝐽”⟩) · (𝑀‘⟨“𝐾𝐿”⟩))))
226	217, 219, 225	3eqtr4d 2805	. . . . 5 ⊢ (((𝜑 ∧ ¬ 𝐼 ∈ {𝐾, 𝐿}) ∧ ¬ 𝐽 ∈ {𝐾, 𝐿}) → (𝐸 · 𝐹) = ((𝑀‘⟨“𝐽𝐾𝐼”⟩) · (𝑀‘⟨“𝐾𝐿𝐽”⟩)))
227	176	grpmndd 19070	. . . . . . 7 ⊢ (𝜑 → 𝑆 ∈ Mnd)
228	227	ad2antrr 739	. . . . . 6 ⊢ (((𝜑 ∧ ¬ 𝐼 ∈ {𝐾, 𝐿}) ∧ ¬ 𝐽 ∈ {𝐾, 𝐿}) → 𝑆 ∈ Mnd)
229	7, 12, 146, 147, 148, 149, 151, 157, 158	cycpm3cl 33575	. . . . . 6 ⊢ (((𝜑 ∧ ¬ 𝐼 ∈ {𝐾, 𝐿}) ∧ ¬ 𝐽 ∈ {𝐾, 𝐿}) → (𝑀‘⟨“𝐽𝐾𝐼”⟩) ∈ (Base‘𝑆))
230	224, 202	eqeltrd 2860	. . . . . 6 ⊢ (((𝜑 ∧ ¬ 𝐼 ∈ {𝐾, 𝐿}) ∧ ¬ 𝐽 ∈ {𝐾, 𝐿}) → (𝑀‘⟨“𝐾𝐿𝐽”⟩) ∈ (Base‘𝑆))
231	21, 22	gsumws2 18951	. . . . . 6 ⊢ ((𝑆 ∈ Mnd ∧ (𝑀‘⟨“𝐽𝐾𝐼”⟩) ∈ (Base‘𝑆) ∧ (𝑀‘⟨“𝐾𝐿𝐽”⟩) ∈ (Base‘𝑆)) → (𝑆 Σg ⟨“(𝑀‘⟨“𝐽𝐾𝐼”⟩)(𝑀‘⟨“𝐾𝐿𝐽”⟩)”⟩) = ((𝑀‘⟨“𝐽𝐾𝐼”⟩) · (𝑀‘⟨“𝐾𝐿𝐽”⟩)))
232	228, 229, 230, 231	syl3anc 1398	. . . . 5 ⊢ (((𝜑 ∧ ¬ 𝐼 ∈ {𝐾, 𝐿}) ∧ ¬ 𝐽 ∈ {𝐾, 𝐿}) → (𝑆 Σg ⟨“(𝑀‘⟨“𝐽𝐾𝐼”⟩)(𝑀‘⟨“𝐾𝐿𝐽”⟩)”⟩) = ((𝑀‘⟨“𝐽𝐾𝐼”⟩) · (𝑀‘⟨“𝐾𝐿𝐽”⟩)))
233	226, 232	eqtr4d 2798	. . . 4 ⊢ (((𝜑 ∧ ¬ 𝐼 ∈ {𝐾, 𝐿}) ∧ ¬ 𝐽 ∈ {𝐾, 𝐿}) → (𝐸 · 𝐹) = (𝑆 Σg ⟨“(𝑀‘⟨“𝐽𝐾𝐼”⟩)(𝑀‘⟨“𝐾𝐿𝐽”⟩)”⟩))
234	169, 172, 233	rspcedvd 3578	. . 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 2145   ≠ wne 2955  ∃wrex 3086   ∖ cdif 3896   ⊆ wss 3899  ∅c0 4279  {csn 4584  {cpr 4586  ∪ cuni 4867   class class class wbr 5103   I cid 5549  ^◡ccnv 5654  ran crn 5656   ↾ cres 5657   “ cima 5658   ∘ ccom 5659  ‘cfv 6533  (class class class)co 7413  2_oc2o 8449   ≈ cen 8949  3c3 12320  ♯chash 14394  Word cword 14578  ⟨“cs1 14662  ⟨“cs2 14912  ⟨“cs3 14913  Basecbs 17301  +_gcplusg 17342  0_gc0g 17524   Σ_g cgsu 17525  Mndcmnd 18836  Grpcgrp 19057  SymGrpcsymg 19496  pmTrspcpmtr 19568  pmEvencevpm 19617  toCycctocyc 33546

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 2147  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2213  ax-ext 2732  ax-rep 5232  ax-sep 5251  ax-nul 5263  ax-pow 5330  ax-pr 5398  ax-un 7736  ax-reg 9564  ax-ac2 10465  ax-cnex 11180  ax-resscn 11181  ax-1cn 11182  ax-icn 11183  ax-addcl 11184  ax-addrcl 11185  ax-mulcl 11186  ax-mulrcl 11187  ax-mulcom 11188  ax-addass 11189  ax-mulass 11190  ax-distr 11191  ax-i2m1 11192  ax-1ne0 11193  ax-1rid 11194  ax-rnegex 11195  ax-rrecex 11196  ax-cnre 11197  ax-pre-lttri 11198  ax-pre-lttrn 11199  ax-pre-ltadd 11200  ax-pre-mulgt0 11201  ax-pre-sup 11202

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 2564  df-eu 2594  df-clab 2739  df-cleq 2752  df-clel 2835  df-nfc 2909  df-ne 2956  df-nel 3062  df-ral 3077  df-rex 3087  df-rmo 3365  df-reu 3366  df-rab 3413  df-v 3452  df-sbc 3740  df-csb 3848  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-pss 3919  df-nul 4280  df-if 4483  df-pw 4559  df-sn 4585  df-pr 4587  df-tp 4589  df-op 4591  df-uni 4868  df-int 4908  df-iun 4953  df-br 5104  df-opab 5168  df-mpt 5187  df-tr 5213  df-id 5550  df-eprel 5555  df-po 5563  df-so 5564  df-fr 5608  df-se 5609  df-we 5610  df-xp 5661  df-rel 5662  df-cnv 5663  df-co 5664  df-dm 5665  df-rn 5666  df-res 5667  df-ima 5668  df-pred 6299  df-ord 6360  df-on 6361  df-lim 6362  df-suc 6363  df-iota 6489  df-fun 6535  df-fn 6536  df-f 6537  df-f1 6538  df-fo 6539  df-f1o 6540  df-fv 6541  df-isom 6542  df-riota 7370  df-ov 7416  df-oprab 7417  df-mpo 7418  df-om 7863  df-1st 7986  df-2nd 7987  df-frecs 8280  df-wrecs 8311  df-recs 8360  df-rdg 8399  df-1o 8455  df-2o 8456  df-er 8696  df-map 8828  df-en 8953  df-dom 8954  df-sdom 8955  df-fin 8956  df-sup 9412  df-inf 9413  df-card 9944  df-ac 10119  df-pnf 11269  df-mnf 11270  df-xr 11271  df-ltxr 11272  df-le 11273  df-sub 11467  df-neg 11468  df-div 11896  df-nn 12258  df-2 12327  df-3 12328  df-4 12329  df-5 12330  df-6 12331  df-7 12332  df-8 12333  df-9 12334  df-n0 12529  df-xnn0 12602  df-z 12616  df-uz 12888  df-rp 13043  df-fz 13562  df-fzo 13710  df-fl 13853  df-mod 13931  df-seq 14066  df-hash 14395  df-word 14579  df-concat 14636  df-s1 14663  df-substr 14709  df-pfx 14741  df-csh 14860  df-s2 14919  df-s3 14920  df-struct 17239  df-sets 17256  df-slot 17274  df-ndx 17286  df-base 17302  df-ress 17323  df-plusg 17355  df-tset 17361  df-0g 17526  df-gsum 17527  df-mgm 18730  df-sgrp 18821  df-mnd 18837  df-submnd 18892  df-efmnd 18978  df-grp 19060  df-symg 19497  df-pmtr 19569  df-tocyc 33547

This theorem is used by:  cyc3genpm  33592