Theorem cyc3genpmlem 33120

Description: Lemma for cyc3genpm 33121. (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 14446	. . . . 5 ⊢ ∅ ∈ Word 𝐶
2	1	a1i 11	. . . 4 ⊢ (((𝜑 ∧ 𝐼 ∈ {𝐾, 𝐿}) ∧ 𝐽 ∈ {𝐾, 𝐿}) → ∅ ∈ Word 𝐶)
3		simpr 484	. . . . . 6 ⊢ ((((𝜑 ∧ 𝐼 ∈ {𝐾, 𝐿}) ∧ 𝐽 ∈ {𝐾, 𝐿}) ∧ 𝑐 = ∅) → 𝑐 = ∅)
4	3	oveq2d 7362	. . . . 5 ⊢ ((((𝜑 ∧ 𝐼 ∈ {𝐾, 𝐿}) ∧ 𝐽 ∈ {𝐾, 𝐿}) ∧ 𝑐 = ∅) → (𝑆 Σg 𝑐) = (𝑆 Σg ∅))
5	4	eqeq2d 2742	. . . 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 33089	. . . . . . . . 9 ⊢ (𝜑 → (𝑀‘⟨“𝐼𝐽”⟩) ∈ (Base‘𝑆))
14	6, 13	eqeltrd 2831	. . . . . . . 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 33089	. . . . . . . . 9 ⊢ (𝜑 → (𝑀‘⟨“𝐾𝐿”⟩) ∈ (Base‘𝑆))
20	15, 19	eqeltrd 2831	. . . . . . . 8 ⊢ (𝜑 → 𝐹 ∈ (Base‘𝑆))
21		eqid 2731	. . . . . . . . 9 ⊢ (Base‘𝑆) = (Base‘𝑆)
22		cyc3genpmlem.t	. . . . . . . . 9 ⊢ · = (+g‘𝑆)
23	12, 21, 22	symgov 19296	. . . . . . . 8 ⊢ ((𝐸 ∈ (Base‘𝑆) ∧ 𝐹 ∈ (Base‘𝑆)) → (𝐸 · 𝐹) = (𝐸 ∘ 𝐹))
24	14, 20, 23	syl2anc 584	. . . . . . 7 ⊢ (𝜑 → (𝐸 · 𝐹) = (𝐸 ∘ 𝐹))
25	24	ad2antrr 726	. . . . . 6 ⊢ (((𝜑 ∧ 𝐼 ∈ {𝐾, 𝐿}) ∧ 𝐽 ∈ {𝐾, 𝐿}) → (𝐸 · 𝐹) = (𝐸 ∘ 𝐹))
26	6	ad2antrr 726	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝐼 ∈ {𝐾, 𝐿}) ∧ 𝐽 ∈ {𝐾, 𝐿}) → 𝐸 = (𝑀‘⟨“𝐼𝐽”⟩))
27		eqid 2731	. . . . . . . . . 10 ⊢ (pmTrsp‘𝐷) = (pmTrsp‘𝐷)
28	7, 8, 9, 10, 11, 27	cycpm2tr 33088	. . . . . . . . 9 ⊢ (𝜑 → (𝑀‘⟨“𝐼𝐽”⟩) = ((pmTrsp‘𝐷)‘{𝐼, 𝐽}))
29	28	ad2antrr 726	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝐼 ∈ {𝐾, 𝐿}) ∧ 𝐽 ∈ {𝐾, 𝐿}) → (𝑀‘⟨“𝐼𝐽”⟩) = ((pmTrsp‘𝐷)‘{𝐼, 𝐽}))
30	26, 29	eqtrd 2766	. . . . . . 7 ⊢ (((𝜑 ∧ 𝐼 ∈ {𝐾, 𝐿}) ∧ 𝐽 ∈ {𝐾, 𝐿}) → 𝐸 = ((pmTrsp‘𝐷)‘{𝐼, 𝐽}))
31	7, 8, 16, 17, 18, 27	cycpm2tr 33088	. . . . . . . . 9 ⊢ (𝜑 → (𝑀‘⟨“𝐾𝐿”⟩) = ((pmTrsp‘𝐷)‘{𝐾, 𝐿}))
32	31	ad2antrr 726	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝐼 ∈ {𝐾, 𝐿}) ∧ 𝐽 ∈ {𝐾, 𝐿}) → (𝑀‘⟨“𝐾𝐿”⟩) = ((pmTrsp‘𝐷)‘{𝐾, 𝐿}))
33	15	ad2antrr 726	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝐼 ∈ {𝐾, 𝐿}) ∧ 𝐽 ∈ {𝐾, 𝐿}) → 𝐹 = (𝑀‘⟨“𝐾𝐿”⟩))
34	9	ad2antrr 726	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝐼 ∈ {𝐾, 𝐿}) ∧ 𝐽 ∈ {𝐾, 𝐿}) → 𝐼 ∈ 𝐷)
35	10	ad2antrr 726	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝐼 ∈ {𝐾, 𝐿}) ∧ 𝐽 ∈ {𝐾, 𝐿}) → 𝐽 ∈ 𝐷)
36	11	ad2antrr 726	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝐼 ∈ {𝐾, 𝐿}) ∧ 𝐽 ∈ {𝐾, 𝐿}) → 𝐼 ≠ 𝐽)
37		simplr 768	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝐼 ∈ {𝐾, 𝐿}) ∧ 𝐽 ∈ {𝐾, 𝐿}) → 𝐼 ∈ {𝐾, 𝐿})
38		simpr 484	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝐼 ∈ {𝐾, 𝐿}) ∧ 𝐽 ∈ {𝐾, 𝐿}) → 𝐽 ∈ {𝐾, 𝐿})
39	37, 38	prssd 4771	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝐼 ∈ {𝐾, 𝐿}) ∧ 𝐽 ∈ {𝐾, 𝐿}) → {𝐼, 𝐽} ⊆ {𝐾, 𝐿})
40		ssprsseq 4774	. . . . . . . . . . 11 ⊢ ((𝐼 ∈ 𝐷 ∧ 𝐽 ∈ 𝐷 ∧ 𝐼 ≠ 𝐽) → ({𝐼, 𝐽} ⊆ {𝐾, 𝐿} ↔ {𝐼, 𝐽} = {𝐾, 𝐿}))
41	40	biimpa 476	. . . . . . . . . 10 ⊢ (((𝐼 ∈ 𝐷 ∧ 𝐽 ∈ 𝐷 ∧ 𝐼 ≠ 𝐽) ∧ {𝐼, 𝐽} ⊆ {𝐾, 𝐿}) → {𝐼, 𝐽} = {𝐾, 𝐿})
42	34, 35, 36, 39, 41	syl31anc 1375	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝐼 ∈ {𝐾, 𝐿}) ∧ 𝐽 ∈ {𝐾, 𝐿}) → {𝐼, 𝐽} = {𝐾, 𝐿})
43	42	fveq2d 6826	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝐼 ∈ {𝐾, 𝐿}) ∧ 𝐽 ∈ {𝐾, 𝐿}) → ((pmTrsp‘𝐷)‘{𝐼, 𝐽}) = ((pmTrsp‘𝐷)‘{𝐾, 𝐿}))
44	32, 33, 43	3eqtr4d 2776	. . . . . . 7 ⊢ (((𝜑 ∧ 𝐼 ∈ {𝐾, 𝐿}) ∧ 𝐽 ∈ {𝐾, 𝐿}) → 𝐹 = ((pmTrsp‘𝐷)‘{𝐼, 𝐽}))
45	30, 44	coeq12d 5803	. . . . . 6 ⊢ (((𝜑 ∧ 𝐼 ∈ {𝐾, 𝐿}) ∧ 𝐽 ∈ {𝐾, 𝐿}) → (𝐸 ∘ 𝐹) = (((pmTrsp‘𝐷)‘{𝐼, 𝐽}) ∘ ((pmTrsp‘𝐷)‘{𝐼, 𝐽})))
46	8	ad2antrr 726	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝐼 ∈ {𝐾, 𝐿}) ∧ 𝐽 ∈ {𝐾, 𝐿}) → 𝐷 ∈ 𝑉)
47	34, 35	prssd 4771	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝐼 ∈ {𝐾, 𝐿}) ∧ 𝐽 ∈ {𝐾, 𝐿}) → {𝐼, 𝐽} ⊆ 𝐷)
48		enpr2 9895	. . . . . . . . 9 ⊢ ((𝐼 ∈ 𝐷 ∧ 𝐽 ∈ 𝐷 ∧ 𝐼 ≠ 𝐽) → {𝐼, 𝐽} ≈ 2o)
49	34, 35, 36, 48	syl3anc 1373	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝐼 ∈ {𝐾, 𝐿}) ∧ 𝐽 ∈ {𝐾, 𝐿}) → {𝐼, 𝐽} ≈ 2o)
50		eqid 2731	. . . . . . . . 9 ⊢ ran (pmTrsp‘𝐷) = ran (pmTrsp‘𝐷)
51	27, 50	pmtrrn 19369	. . . . . . . 8 ⊢ ((𝐷 ∈ 𝑉 ∧ {𝐼, 𝐽} ⊆ 𝐷 ∧ {𝐼, 𝐽} ≈ 2o) → ((pmTrsp‘𝐷)‘{𝐼, 𝐽}) ∈ ran (pmTrsp‘𝐷))
52	46, 47, 49, 51	syl3anc 1373	. . . . . . 7 ⊢ (((𝜑 ∧ 𝐼 ∈ {𝐾, 𝐿}) ∧ 𝐽 ∈ {𝐾, 𝐿}) → ((pmTrsp‘𝐷)‘{𝐼, 𝐽}) ∈ ran (pmTrsp‘𝐷))
53	27, 50	pmtrfinv 19373	. . . . . . 7 ⊢ (((pmTrsp‘𝐷)‘{𝐼, 𝐽}) ∈ ran (pmTrsp‘𝐷) → (((pmTrsp‘𝐷)‘{𝐼, 𝐽}) ∘ ((pmTrsp‘𝐷)‘{𝐼, 𝐽})) = ( I ↾ 𝐷))
54	52, 53	syl 17	. . . . . 6 ⊢ (((𝜑 ∧ 𝐼 ∈ {𝐾, 𝐿}) ∧ 𝐽 ∈ {𝐾, 𝐿}) → (((pmTrsp‘𝐷)‘{𝐼, 𝐽}) ∘ ((pmTrsp‘𝐷)‘{𝐼, 𝐽})) = ( I ↾ 𝐷))
55	25, 45, 54	3eqtrd 2770	. . . . 5 ⊢ (((𝜑 ∧ 𝐼 ∈ {𝐾, 𝐿}) ∧ 𝐽 ∈ {𝐾, 𝐿}) → (𝐸 · 𝐹) = ( I ↾ 𝐷))
56	12	symgid 19313	. . . . . . 7 ⊢ (𝐷 ∈ 𝑉 → ( I ↾ 𝐷) = (0g‘𝑆))
57	46, 56	syl 17	. . . . . 6 ⊢ (((𝜑 ∧ 𝐼 ∈ {𝐾, 𝐿}) ∧ 𝐽 ∈ {𝐾, 𝐿}) → ( I ↾ 𝐷) = (0g‘𝑆))
58		eqid 2731	. . . . . . 7 ⊢ (0g‘𝑆) = (0g‘𝑆)
59	58	gsum0 18592	. . . . . 6 ⊢ (𝑆 Σg ∅) = (0g‘𝑆)
60	57, 59	eqtr4di 2784	. . . . 5 ⊢ (((𝜑 ∧ 𝐼 ∈ {𝐾, 𝐿}) ∧ 𝐽 ∈ {𝐾, 𝐿}) → ( I ↾ 𝐷) = (𝑆 Σg ∅))
61	55, 60	eqtrd 2766	. . . 4 ⊢ (((𝜑 ∧ 𝐼 ∈ {𝐾, 𝐿}) ∧ 𝐽 ∈ {𝐾, 𝐿}) → (𝐸 · 𝐹) = (𝑆 Σg ∅))
62	2, 5, 61	rspcedvd 3574	. . 3 ⊢ (((𝜑 ∧ 𝐼 ∈ {𝐾, 𝐿}) ∧ 𝐽 ∈ {𝐾, 𝐿}) → ∃𝑐 ∈ Word 𝐶(𝐸 · 𝐹) = (𝑆 Σg 𝑐))
63	8	ad2antrr 726	. . . . . . 7 ⊢ (((𝜑 ∧ 𝐼 ∈ {𝐾, 𝐿}) ∧ ¬ 𝐽 ∈ {𝐾, 𝐿}) → 𝐷 ∈ 𝑉)
64	9	ad2antrr 726	. . . . . . 7 ⊢ (((𝜑 ∧ 𝐼 ∈ {𝐾, 𝐿}) ∧ ¬ 𝐽 ∈ {𝐾, 𝐿}) → 𝐼 ∈ 𝐷)
65	16, 17	prssd 4771	. . . . . . . . 9 ⊢ (𝜑 → {𝐾, 𝐿} ⊆ 𝐷)
66	65	ad2antrr 726	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝐼 ∈ {𝐾, 𝐿}) ∧ ¬ 𝐽 ∈ {𝐾, 𝐿}) → {𝐾, 𝐿} ⊆ 𝐷)
67		simplr 768	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝐼 ∈ {𝐾, 𝐿}) ∧ ¬ 𝐽 ∈ {𝐾, 𝐿}) → 𝐼 ∈ {𝐾, 𝐿})
68		enpr2 9895	. . . . . . . . . . 11 ⊢ ((𝐾 ∈ 𝐷 ∧ 𝐿 ∈ 𝐷 ∧ 𝐾 ≠ 𝐿) → {𝐾, 𝐿} ≈ 2o)
69	16, 17, 18, 68	syl3anc 1373	. . . . . . . . . 10 ⊢ (𝜑 → {𝐾, 𝐿} ≈ 2o)
70	69	ad2antrr 726	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝐼 ∈ {𝐾, 𝐿}) ∧ ¬ 𝐽 ∈ {𝐾, 𝐿}) → {𝐾, 𝐿} ≈ 2o)
71		unidifsnel 32515	. . . . . . . . 9 ⊢ ((𝐼 ∈ {𝐾, 𝐿} ∧ {𝐾, 𝐿} ≈ 2o) → ∪ ({𝐾, 𝐿} ∖ {𝐼}) ∈ {𝐾, 𝐿})
72	67, 70, 71	syl2anc 584	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝐼 ∈ {𝐾, 𝐿}) ∧ ¬ 𝐽 ∈ {𝐾, 𝐿}) → ∪ ({𝐾, 𝐿} ∖ {𝐼}) ∈ {𝐾, 𝐿})
73	66, 72	sseldd 3930	. . . . . . 7 ⊢ (((𝜑 ∧ 𝐼 ∈ {𝐾, 𝐿}) ∧ ¬ 𝐽 ∈ {𝐾, 𝐿}) → ∪ ({𝐾, 𝐿} ∖ {𝐼}) ∈ 𝐷)
74	10	ad2antrr 726	. . . . . . 7 ⊢ (((𝜑 ∧ 𝐼 ∈ {𝐾, 𝐿}) ∧ ¬ 𝐽 ∈ {𝐾, 𝐿}) → 𝐽 ∈ 𝐷)
75		unidifsnne 32516	. . . . . . . . 9 ⊢ ((𝐼 ∈ {𝐾, 𝐿} ∧ {𝐾, 𝐿} ≈ 2o) → ∪ ({𝐾, 𝐿} ∖ {𝐼}) ≠ 𝐼)
76	67, 70, 75	syl2anc 584	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝐼 ∈ {𝐾, 𝐿}) ∧ ¬ 𝐽 ∈ {𝐾, 𝐿}) → ∪ ({𝐾, 𝐿} ∖ {𝐼}) ≠ 𝐼)
77	76	necomd 2983	. . . . . . 7 ⊢ (((𝜑 ∧ 𝐼 ∈ {𝐾, 𝐿}) ∧ ¬ 𝐽 ∈ {𝐾, 𝐿}) → 𝐼 ≠ ∪ ({𝐾, 𝐿} ∖ {𝐼}))
78		nelne2 3026	. . . . . . . 8 ⊢ ((∪ ({𝐾, 𝐿} ∖ {𝐼}) ∈ {𝐾, 𝐿} ∧ ¬ 𝐽 ∈ {𝐾, 𝐿}) → ∪ ({𝐾, 𝐿} ∖ {𝐼}) ≠ 𝐽)
79	72, 78	sylancom 588	. . . . . . 7 ⊢ (((𝜑 ∧ 𝐼 ∈ {𝐾, 𝐿}) ∧ ¬ 𝐽 ∈ {𝐾, 𝐿}) → ∪ ({𝐾, 𝐿} ∖ {𝐼}) ≠ 𝐽)
80	11	necomd 2983	. . . . . . . 8 ⊢ (𝜑 → 𝐽 ≠ 𝐼)
81	80	ad2antrr 726	. . . . . . 7 ⊢ (((𝜑 ∧ 𝐼 ∈ {𝐾, 𝐿}) ∧ ¬ 𝐽 ∈ {𝐾, 𝐿}) → 𝐽 ≠ 𝐼)
82	7, 12, 63, 64, 73, 74, 77, 79, 81	cycpm3cl2 33105	. . . . . 6 ⊢ (((𝜑 ∧ 𝐼 ∈ {𝐾, 𝐿}) ∧ ¬ 𝐽 ∈ {𝐾, 𝐿}) → (𝑀‘⟨“𝐼∪ ({𝐾, 𝐿} ∖ {𝐼})𝐽”⟩) ∈ (𝑀 “ (◡♯ “ {3})))
83		cyc3genpm.t	. . . . . 6 ⊢ 𝐶 = (𝑀 “ (◡♯ “ {3}))
84	82, 83	eleqtrrdi 2842	. . . . 5 ⊢ (((𝜑 ∧ 𝐼 ∈ {𝐾, 𝐿}) ∧ ¬ 𝐽 ∈ {𝐾, 𝐿}) → (𝑀‘⟨“𝐼∪ ({𝐾, 𝐿} ∖ {𝐼})𝐽”⟩) ∈ 𝐶)
85	84	s1cld 14511	. . . 4 ⊢ (((𝜑 ∧ 𝐼 ∈ {𝐾, 𝐿}) ∧ ¬ 𝐽 ∈ {𝐾, 𝐿}) → ⟨“(𝑀‘⟨“𝐼∪ ({𝐾, 𝐿} ∖ {𝐼})𝐽”⟩)”⟩ ∈ Word 𝐶)
86		simpr 484	. . . . . 6 ⊢ ((((𝜑 ∧ 𝐼 ∈ {𝐾, 𝐿}) ∧ ¬ 𝐽 ∈ {𝐾, 𝐿}) ∧ 𝑐 = ⟨“(𝑀‘⟨“𝐼∪ ({𝐾, 𝐿} ∖ {𝐼})𝐽”⟩)”⟩) → 𝑐 = ⟨“(𝑀‘⟨“𝐼∪ ({𝐾, 𝐿} ∖ {𝐼})𝐽”⟩)”⟩)
87	86	oveq2d 7362	. . . . 5 ⊢ ((((𝜑 ∧ 𝐼 ∈ {𝐾, 𝐿}) ∧ ¬ 𝐽 ∈ {𝐾, 𝐿}) ∧ 𝑐 = ⟨“(𝑀‘⟨“𝐼∪ ({𝐾, 𝐿} ∖ {𝐼})𝐽”⟩)”⟩) → (𝑆 Σg 𝑐) = (𝑆 Σg ⟨“(𝑀‘⟨“𝐼∪ ({𝐾, 𝐿} ∖ {𝐼})𝐽”⟩)”⟩))
88	87	eqeq2d 2742	. . . 4 ⊢ ((((𝜑 ∧ 𝐼 ∈ {𝐾, 𝐿}) ∧ ¬ 𝐽 ∈ {𝐾, 𝐿}) ∧ 𝑐 = ⟨“(𝑀‘⟨“𝐼∪ ({𝐾, 𝐿} ∖ {𝐼})𝐽”⟩)”⟩) → ((𝐸 · 𝐹) = (𝑆 Σg 𝑐) ↔ (𝐸 · 𝐹) = (𝑆 Σg ⟨“(𝑀‘⟨“𝐼∪ ({𝐾, 𝐿} ∖ {𝐼})𝐽”⟩)”⟩)))
89	7, 12, 63, 64, 73, 74, 77, 79, 81, 22	cyc3co2 33109	. . . . 5 ⊢ (((𝜑 ∧ 𝐼 ∈ {𝐾, 𝐿}) ∧ ¬ 𝐽 ∈ {𝐾, 𝐿}) → (𝑀‘⟨“𝐼∪ ({𝐾, 𝐿} ∖ {𝐼})𝐽”⟩) = ((𝑀‘⟨“𝐼𝐽”⟩) · (𝑀‘⟨“𝐼∪ ({𝐾, 𝐿} ∖ {𝐼})”⟩)))
90	7, 12, 63, 64, 73, 74, 77, 79, 81	cycpm3cl 33104	. . . . . 6 ⊢ (((𝜑 ∧ 𝐼 ∈ {𝐾, 𝐿}) ∧ ¬ 𝐽 ∈ {𝐾, 𝐿}) → (𝑀‘⟨“𝐼∪ ({𝐾, 𝐿} ∖ {𝐼})𝐽”⟩) ∈ (Base‘𝑆))
91	21	gsumws1 18746	. . . . . 6 ⊢ ((𝑀‘⟨“𝐼∪ ({𝐾, 𝐿} ∖ {𝐼})𝐽”⟩) ∈ (Base‘𝑆) → (𝑆 Σg ⟨“(𝑀‘⟨“𝐼∪ ({𝐾, 𝐿} ∖ {𝐼})𝐽”⟩)”⟩) = (𝑀‘⟨“𝐼∪ ({𝐾, 𝐿} ∖ {𝐼})𝐽”⟩))
92	90, 91	syl 17	. . . . 5 ⊢ (((𝜑 ∧ 𝐼 ∈ {𝐾, 𝐿}) ∧ ¬ 𝐽 ∈ {𝐾, 𝐿}) → (𝑆 Σg ⟨“(𝑀‘⟨“𝐼∪ ({𝐾, 𝐿} ∖ {𝐼})𝐽”⟩)”⟩) = (𝑀‘⟨“𝐼∪ ({𝐾, 𝐿} ∖ {𝐼})𝐽”⟩))
93	6	ad2antrr 726	. . . . . 6 ⊢ (((𝜑 ∧ 𝐼 ∈ {𝐾, 𝐿}) ∧ ¬ 𝐽 ∈ {𝐾, 𝐿}) → 𝐸 = (𝑀‘⟨“𝐼𝐽”⟩))
94		en2eleq 9899	. . . . . . . . 9 ⊢ ((𝐼 ∈ {𝐾, 𝐿} ∧ {𝐾, 𝐿} ≈ 2o) → {𝐾, 𝐿} = {𝐼, ∪ ({𝐾, 𝐿} ∖ {𝐼})})
95	67, 70, 94	syl2anc 584	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝐼 ∈ {𝐾, 𝐿}) ∧ ¬ 𝐽 ∈ {𝐾, 𝐿}) → {𝐾, 𝐿} = {𝐼, ∪ ({𝐾, 𝐿} ∖ {𝐼})})
96	95	fveq2d 6826	. . . . . . 7 ⊢ (((𝜑 ∧ 𝐼 ∈ {𝐾, 𝐿}) ∧ ¬ 𝐽 ∈ {𝐾, 𝐿}) → ((pmTrsp‘𝐷)‘{𝐾, 𝐿}) = ((pmTrsp‘𝐷)‘{𝐼, ∪ ({𝐾, 𝐿} ∖ {𝐼})}))
97	15, 31	eqtrd 2766	. . . . . . . 8 ⊢ (𝜑 → 𝐹 = ((pmTrsp‘𝐷)‘{𝐾, 𝐿}))
98	97	ad2antrr 726	. . . . . . 7 ⊢ (((𝜑 ∧ 𝐼 ∈ {𝐾, 𝐿}) ∧ ¬ 𝐽 ∈ {𝐾, 𝐿}) → 𝐹 = ((pmTrsp‘𝐷)‘{𝐾, 𝐿}))
99	7, 63, 64, 73, 77, 27	cycpm2tr 33088	. . . . . . 7 ⊢ (((𝜑 ∧ 𝐼 ∈ {𝐾, 𝐿}) ∧ ¬ 𝐽 ∈ {𝐾, 𝐿}) → (𝑀‘⟨“𝐼∪ ({𝐾, 𝐿} ∖ {𝐼})”⟩) = ((pmTrsp‘𝐷)‘{𝐼, ∪ ({𝐾, 𝐿} ∖ {𝐼})}))
100	96, 98, 99	3eqtr4d 2776	. . . . . 6 ⊢ (((𝜑 ∧ 𝐼 ∈ {𝐾, 𝐿}) ∧ ¬ 𝐽 ∈ {𝐾, 𝐿}) → 𝐹 = (𝑀‘⟨“𝐼∪ ({𝐾, 𝐿} ∖ {𝐼})”⟩))
101	93, 100	oveq12d 7364	. . . . 5 ⊢ (((𝜑 ∧ 𝐼 ∈ {𝐾, 𝐿}) ∧ ¬ 𝐽 ∈ {𝐾, 𝐿}) → (𝐸 · 𝐹) = ((𝑀‘⟨“𝐼𝐽”⟩) · (𝑀‘⟨“𝐼∪ ({𝐾, 𝐿} ∖ {𝐼})”⟩)))
102	89, 92, 101	3eqtr4rd 2777	. . . 4 ⊢ (((𝜑 ∧ 𝐼 ∈ {𝐾, 𝐿}) ∧ ¬ 𝐽 ∈ {𝐾, 𝐿}) → (𝐸 · 𝐹) = (𝑆 Σg ⟨“(𝑀‘⟨“𝐼∪ ({𝐾, 𝐿} ∖ {𝐼})𝐽”⟩)”⟩))
103	85, 88, 102	rspcedvd 3574	. . 3 ⊢ (((𝜑 ∧ 𝐼 ∈ {𝐾, 𝐿}) ∧ ¬ 𝐽 ∈ {𝐾, 𝐿}) → ∃𝑐 ∈ Word 𝐶(𝐸 · 𝐹) = (𝑆 Σg 𝑐))
104	62, 103	pm2.61dan 812	. 2 ⊢ ((𝜑 ∧ 𝐼 ∈ {𝐾, 𝐿}) → ∃𝑐 ∈ Word 𝐶(𝐸 · 𝐹) = (𝑆 Σg 𝑐))
105	8	ad2antrr 726	. . . . . . 7 ⊢ (((𝜑 ∧ ¬ 𝐼 ∈ {𝐾, 𝐿}) ∧ 𝐽 ∈ {𝐾, 𝐿}) → 𝐷 ∈ 𝑉)
106	10	ad2antrr 726	. . . . . . 7 ⊢ (((𝜑 ∧ ¬ 𝐼 ∈ {𝐾, 𝐿}) ∧ 𝐽 ∈ {𝐾, 𝐿}) → 𝐽 ∈ 𝐷)
107	65	ad2antrr 726	. . . . . . . 8 ⊢ (((𝜑 ∧ ¬ 𝐼 ∈ {𝐾, 𝐿}) ∧ 𝐽 ∈ {𝐾, 𝐿}) → {𝐾, 𝐿} ⊆ 𝐷)
108		simpr 484	. . . . . . . . 9 ⊢ (((𝜑 ∧ ¬ 𝐼 ∈ {𝐾, 𝐿}) ∧ 𝐽 ∈ {𝐾, 𝐿}) → 𝐽 ∈ {𝐾, 𝐿})
109	69	ad2antrr 726	. . . . . . . . 9 ⊢ (((𝜑 ∧ ¬ 𝐼 ∈ {𝐾, 𝐿}) ∧ 𝐽 ∈ {𝐾, 𝐿}) → {𝐾, 𝐿} ≈ 2o)
110		unidifsnel 32515	. . . . . . . . 9 ⊢ ((𝐽 ∈ {𝐾, 𝐿} ∧ {𝐾, 𝐿} ≈ 2o) → ∪ ({𝐾, 𝐿} ∖ {𝐽}) ∈ {𝐾, 𝐿})
111	108, 109, 110	syl2anc 584	. . . . . . . 8 ⊢ (((𝜑 ∧ ¬ 𝐼 ∈ {𝐾, 𝐿}) ∧ 𝐽 ∈ {𝐾, 𝐿}) → ∪ ({𝐾, 𝐿} ∖ {𝐽}) ∈ {𝐾, 𝐿})
112	107, 111	sseldd 3930	. . . . . . 7 ⊢ (((𝜑 ∧ ¬ 𝐼 ∈ {𝐾, 𝐿}) ∧ 𝐽 ∈ {𝐾, 𝐿}) → ∪ ({𝐾, 𝐿} ∖ {𝐽}) ∈ 𝐷)
113	9	ad2antrr 726	. . . . . . 7 ⊢ (((𝜑 ∧ ¬ 𝐼 ∈ {𝐾, 𝐿}) ∧ 𝐽 ∈ {𝐾, 𝐿}) → 𝐼 ∈ 𝐷)
114		unidifsnne 32516	. . . . . . . . 9 ⊢ ((𝐽 ∈ {𝐾, 𝐿} ∧ {𝐾, 𝐿} ≈ 2o) → ∪ ({𝐾, 𝐿} ∖ {𝐽}) ≠ 𝐽)
115	108, 109, 114	syl2anc 584	. . . . . . . 8 ⊢ (((𝜑 ∧ ¬ 𝐼 ∈ {𝐾, 𝐿}) ∧ 𝐽 ∈ {𝐾, 𝐿}) → ∪ ({𝐾, 𝐿} ∖ {𝐽}) ≠ 𝐽)
116	115	necomd 2983	. . . . . . 7 ⊢ (((𝜑 ∧ ¬ 𝐼 ∈ {𝐾, 𝐿}) ∧ 𝐽 ∈ {𝐾, 𝐿}) → 𝐽 ≠ ∪ ({𝐾, 𝐿} ∖ {𝐽}))
117		simplr 768	. . . . . . . 8 ⊢ (((𝜑 ∧ ¬ 𝐼 ∈ {𝐾, 𝐿}) ∧ 𝐽 ∈ {𝐾, 𝐿}) → ¬ 𝐼 ∈ {𝐾, 𝐿})
118		nelne2 3026	. . . . . . . 8 ⊢ ((∪ ({𝐾, 𝐿} ∖ {𝐽}) ∈ {𝐾, 𝐿} ∧ ¬ 𝐼 ∈ {𝐾, 𝐿}) → ∪ ({𝐾, 𝐿} ∖ {𝐽}) ≠ 𝐼)
119	111, 117, 118	syl2anc 584	. . . . . . 7 ⊢ (((𝜑 ∧ ¬ 𝐼 ∈ {𝐾, 𝐿}) ∧ 𝐽 ∈ {𝐾, 𝐿}) → ∪ ({𝐾, 𝐿} ∖ {𝐽}) ≠ 𝐼)
120	11	ad2antrr 726	. . . . . . 7 ⊢ (((𝜑 ∧ ¬ 𝐼 ∈ {𝐾, 𝐿}) ∧ 𝐽 ∈ {𝐾, 𝐿}) → 𝐼 ≠ 𝐽)
121	7, 12, 105, 106, 112, 113, 116, 119, 120	cycpm3cl2 33105	. . . . . 6 ⊢ (((𝜑 ∧ ¬ 𝐼 ∈ {𝐾, 𝐿}) ∧ 𝐽 ∈ {𝐾, 𝐿}) → (𝑀‘⟨“𝐽∪ ({𝐾, 𝐿} ∖ {𝐽})𝐼”⟩) ∈ (𝑀 “ (◡♯ “ {3})))
122	121, 83	eleqtrrdi 2842	. . . . 5 ⊢ (((𝜑 ∧ ¬ 𝐼 ∈ {𝐾, 𝐿}) ∧ 𝐽 ∈ {𝐾, 𝐿}) → (𝑀‘⟨“𝐽∪ ({𝐾, 𝐿} ∖ {𝐽})𝐼”⟩) ∈ 𝐶)
123	122	s1cld 14511	. . . 4 ⊢ (((𝜑 ∧ ¬ 𝐼 ∈ {𝐾, 𝐿}) ∧ 𝐽 ∈ {𝐾, 𝐿}) → ⟨“(𝑀‘⟨“𝐽∪ ({𝐾, 𝐿} ∖ {𝐽})𝐼”⟩)”⟩ ∈ Word 𝐶)
124		simpr 484	. . . . . 6 ⊢ ((((𝜑 ∧ ¬ 𝐼 ∈ {𝐾, 𝐿}) ∧ 𝐽 ∈ {𝐾, 𝐿}) ∧ 𝑐 = ⟨“(𝑀‘⟨“𝐽∪ ({𝐾, 𝐿} ∖ {𝐽})𝐼”⟩)”⟩) → 𝑐 = ⟨“(𝑀‘⟨“𝐽∪ ({𝐾, 𝐿} ∖ {𝐽})𝐼”⟩)”⟩)
125	124	oveq2d 7362	. . . . 5 ⊢ ((((𝜑 ∧ ¬ 𝐼 ∈ {𝐾, 𝐿}) ∧ 𝐽 ∈ {𝐾, 𝐿}) ∧ 𝑐 = ⟨“(𝑀‘⟨“𝐽∪ ({𝐾, 𝐿} ∖ {𝐽})𝐼”⟩)”⟩) → (𝑆 Σg 𝑐) = (𝑆 Σg ⟨“(𝑀‘⟨“𝐽∪ ({𝐾, 𝐿} ∖ {𝐽})𝐼”⟩)”⟩))
126	125	eqeq2d 2742	. . . 4 ⊢ ((((𝜑 ∧ ¬ 𝐼 ∈ {𝐾, 𝐿}) ∧ 𝐽 ∈ {𝐾, 𝐿}) ∧ 𝑐 = ⟨“(𝑀‘⟨“𝐽∪ ({𝐾, 𝐿} ∖ {𝐽})𝐼”⟩)”⟩) → ((𝐸 · 𝐹) = (𝑆 Σg 𝑐) ↔ (𝐸 · 𝐹) = (𝑆 Σg ⟨“(𝑀‘⟨“𝐽∪ ({𝐾, 𝐿} ∖ {𝐽})𝐼”⟩)”⟩)))
127	7, 12, 105, 106, 112, 113, 116, 119, 120, 22	cyc3co2 33109	. . . . 5 ⊢ (((𝜑 ∧ ¬ 𝐼 ∈ {𝐾, 𝐿}) ∧ 𝐽 ∈ {𝐾, 𝐿}) → (𝑀‘⟨“𝐽∪ ({𝐾, 𝐿} ∖ {𝐽})𝐼”⟩) = ((𝑀‘⟨“𝐽𝐼”⟩) · (𝑀‘⟨“𝐽∪ ({𝐾, 𝐿} ∖ {𝐽})”⟩)))
128	7, 12, 105, 106, 112, 113, 116, 119, 120	cycpm3cl 33104	. . . . . 6 ⊢ (((𝜑 ∧ ¬ 𝐼 ∈ {𝐾, 𝐿}) ∧ 𝐽 ∈ {𝐾, 𝐿}) → (𝑀‘⟨“𝐽∪ ({𝐾, 𝐿} ∖ {𝐽})𝐼”⟩) ∈ (Base‘𝑆))
129	21	gsumws1 18746	. . . . . 6 ⊢ ((𝑀‘⟨“𝐽∪ ({𝐾, 𝐿} ∖ {𝐽})𝐼”⟩) ∈ (Base‘𝑆) → (𝑆 Σg ⟨“(𝑀‘⟨“𝐽∪ ({𝐾, 𝐿} ∖ {𝐽})𝐼”⟩)”⟩) = (𝑀‘⟨“𝐽∪ ({𝐾, 𝐿} ∖ {𝐽})𝐼”⟩))
130	128, 129	syl 17	. . . . 5 ⊢ (((𝜑 ∧ ¬ 𝐼 ∈ {𝐾, 𝐿}) ∧ 𝐽 ∈ {𝐾, 𝐿}) → (𝑆 Σg ⟨“(𝑀‘⟨“𝐽∪ ({𝐾, 𝐿} ∖ {𝐽})𝐼”⟩)”⟩) = (𝑀‘⟨“𝐽∪ ({𝐾, 𝐿} ∖ {𝐽})𝐼”⟩))
131		prcom 4682	. . . . . . . . . 10 ⊢ {𝐼, 𝐽} = {𝐽, 𝐼}
132	131	fveq2i 6825	. . . . . . . . 9 ⊢ ((pmTrsp‘𝐷)‘{𝐼, 𝐽}) = ((pmTrsp‘𝐷)‘{𝐽, 𝐼})
133	7, 8, 10, 9, 80, 27	cycpm2tr 33088	. . . . . . . . 9 ⊢ (𝜑 → (𝑀‘⟨“𝐽𝐼”⟩) = ((pmTrsp‘𝐷)‘{𝐽, 𝐼}))
134	132, 28, 133	3eqtr4a 2792	. . . . . . . 8 ⊢ (𝜑 → (𝑀‘⟨“𝐼𝐽”⟩) = (𝑀‘⟨“𝐽𝐼”⟩))
135	6, 134	eqtrd 2766	. . . . . . 7 ⊢ (𝜑 → 𝐸 = (𝑀‘⟨“𝐽𝐼”⟩))
136	135	ad2antrr 726	. . . . . 6 ⊢ (((𝜑 ∧ ¬ 𝐼 ∈ {𝐾, 𝐿}) ∧ 𝐽 ∈ {𝐾, 𝐿}) → 𝐸 = (𝑀‘⟨“𝐽𝐼”⟩))
137		en2eleq 9899	. . . . . . . . 9 ⊢ ((𝐽 ∈ {𝐾, 𝐿} ∧ {𝐾, 𝐿} ≈ 2o) → {𝐾, 𝐿} = {𝐽, ∪ ({𝐾, 𝐿} ∖ {𝐽})})
138	108, 109, 137	syl2anc 584	. . . . . . . 8 ⊢ (((𝜑 ∧ ¬ 𝐼 ∈ {𝐾, 𝐿}) ∧ 𝐽 ∈ {𝐾, 𝐿}) → {𝐾, 𝐿} = {𝐽, ∪ ({𝐾, 𝐿} ∖ {𝐽})})
139	138	fveq2d 6826	. . . . . . 7 ⊢ (((𝜑 ∧ ¬ 𝐼 ∈ {𝐾, 𝐿}) ∧ 𝐽 ∈ {𝐾, 𝐿}) → ((pmTrsp‘𝐷)‘{𝐾, 𝐿}) = ((pmTrsp‘𝐷)‘{𝐽, ∪ ({𝐾, 𝐿} ∖ {𝐽})}))
140	97	ad2antrr 726	. . . . . . 7 ⊢ (((𝜑 ∧ ¬ 𝐼 ∈ {𝐾, 𝐿}) ∧ 𝐽 ∈ {𝐾, 𝐿}) → 𝐹 = ((pmTrsp‘𝐷)‘{𝐾, 𝐿}))
141	7, 105, 106, 112, 116, 27	cycpm2tr 33088	. . . . . . 7 ⊢ (((𝜑 ∧ ¬ 𝐼 ∈ {𝐾, 𝐿}) ∧ 𝐽 ∈ {𝐾, 𝐿}) → (𝑀‘⟨“𝐽∪ ({𝐾, 𝐿} ∖ {𝐽})”⟩) = ((pmTrsp‘𝐷)‘{𝐽, ∪ ({𝐾, 𝐿} ∖ {𝐽})}))
142	139, 140, 141	3eqtr4d 2776	. . . . . 6 ⊢ (((𝜑 ∧ ¬ 𝐼 ∈ {𝐾, 𝐿}) ∧ 𝐽 ∈ {𝐾, 𝐿}) → 𝐹 = (𝑀‘⟨“𝐽∪ ({𝐾, 𝐿} ∖ {𝐽})”⟩))
143	136, 142	oveq12d 7364	. . . . 5 ⊢ (((𝜑 ∧ ¬ 𝐼 ∈ {𝐾, 𝐿}) ∧ 𝐽 ∈ {𝐾, 𝐿}) → (𝐸 · 𝐹) = ((𝑀‘⟨“𝐽𝐼”⟩) · (𝑀‘⟨“𝐽∪ ({𝐾, 𝐿} ∖ {𝐽})”⟩)))
144	127, 130, 143	3eqtr4rd 2777	. . . 4 ⊢ (((𝜑 ∧ ¬ 𝐼 ∈ {𝐾, 𝐿}) ∧ 𝐽 ∈ {𝐾, 𝐿}) → (𝐸 · 𝐹) = (𝑆 Σg ⟨“(𝑀‘⟨“𝐽∪ ({𝐾, 𝐿} ∖ {𝐽})𝐼”⟩)”⟩))
145	123, 126, 144	rspcedvd 3574	. . 3 ⊢ (((𝜑 ∧ ¬ 𝐼 ∈ {𝐾, 𝐿}) ∧ 𝐽 ∈ {𝐾, 𝐿}) → ∃𝑐 ∈ Word 𝐶(𝐸 · 𝐹) = (𝑆 Σg 𝑐))
146	8	ad2antrr 726	. . . . . . 7 ⊢ (((𝜑 ∧ ¬ 𝐼 ∈ {𝐾, 𝐿}) ∧ ¬ 𝐽 ∈ {𝐾, 𝐿}) → 𝐷 ∈ 𝑉)
147	10	ad2antrr 726	. . . . . . 7 ⊢ (((𝜑 ∧ ¬ 𝐼 ∈ {𝐾, 𝐿}) ∧ ¬ 𝐽 ∈ {𝐾, 𝐿}) → 𝐽 ∈ 𝐷)
148	16	ad2antrr 726	. . . . . . 7 ⊢ (((𝜑 ∧ ¬ 𝐼 ∈ {𝐾, 𝐿}) ∧ ¬ 𝐽 ∈ {𝐾, 𝐿}) → 𝐾 ∈ 𝐷)
149	9	ad2antrr 726	. . . . . . 7 ⊢ (((𝜑 ∧ ¬ 𝐼 ∈ {𝐾, 𝐿}) ∧ ¬ 𝐽 ∈ {𝐾, 𝐿}) → 𝐼 ∈ 𝐷)
150		simpr 484	. . . . . . . 8 ⊢ (((𝜑 ∧ ¬ 𝐼 ∈ {𝐾, 𝐿}) ∧ ¬ 𝐽 ∈ {𝐾, 𝐿}) → ¬ 𝐽 ∈ {𝐾, 𝐿})
151	147, 150	nelpr1 4604	. . . . . . 7 ⊢ (((𝜑 ∧ ¬ 𝐼 ∈ {𝐾, 𝐿}) ∧ ¬ 𝐽 ∈ {𝐾, 𝐿}) → 𝐽 ≠ 𝐾)
152		prid1g 4710	. . . . . . . . . 10 ⊢ (𝐾 ∈ 𝐷 → 𝐾 ∈ {𝐾, 𝐿})
153	16, 152	syl 17	. . . . . . . . 9 ⊢ (𝜑 → 𝐾 ∈ {𝐾, 𝐿})
154	153	ad2antrr 726	. . . . . . . 8 ⊢ (((𝜑 ∧ ¬ 𝐼 ∈ {𝐾, 𝐿}) ∧ ¬ 𝐽 ∈ {𝐾, 𝐿}) → 𝐾 ∈ {𝐾, 𝐿})
155		simplr 768	. . . . . . . 8 ⊢ (((𝜑 ∧ ¬ 𝐼 ∈ {𝐾, 𝐿}) ∧ ¬ 𝐽 ∈ {𝐾, 𝐿}) → ¬ 𝐼 ∈ {𝐾, 𝐿})
156		nelne2 3026	. . . . . . . 8 ⊢ ((𝐾 ∈ {𝐾, 𝐿} ∧ ¬ 𝐼 ∈ {𝐾, 𝐿}) → 𝐾 ≠ 𝐼)
157	154, 155, 156	syl2anc 584	. . . . . . 7 ⊢ (((𝜑 ∧ ¬ 𝐼 ∈ {𝐾, 𝐿}) ∧ ¬ 𝐽 ∈ {𝐾, 𝐿}) → 𝐾 ≠ 𝐼)
158	11	ad2antrr 726	. . . . . . 7 ⊢ (((𝜑 ∧ ¬ 𝐼 ∈ {𝐾, 𝐿}) ∧ ¬ 𝐽 ∈ {𝐾, 𝐿}) → 𝐼 ≠ 𝐽)
159	7, 12, 146, 147, 148, 149, 151, 157, 158	cycpm3cl2 33105	. . . . . 6 ⊢ (((𝜑 ∧ ¬ 𝐼 ∈ {𝐾, 𝐿}) ∧ ¬ 𝐽 ∈ {𝐾, 𝐿}) → (𝑀‘⟨“𝐽𝐾𝐼”⟩) ∈ (𝑀 “ (◡♯ “ {3})))
160	159, 83	eleqtrrdi 2842	. . . . 5 ⊢ (((𝜑 ∧ ¬ 𝐼 ∈ {𝐾, 𝐿}) ∧ ¬ 𝐽 ∈ {𝐾, 𝐿}) → (𝑀‘⟨“𝐽𝐾𝐼”⟩) ∈ 𝐶)
161	17	ad2antrr 726	. . . . . . 7 ⊢ (((𝜑 ∧ ¬ 𝐼 ∈ {𝐾, 𝐿}) ∧ ¬ 𝐽 ∈ {𝐾, 𝐿}) → 𝐿 ∈ 𝐷)
162	18	ad2antrr 726	. . . . . . 7 ⊢ (((𝜑 ∧ ¬ 𝐼 ∈ {𝐾, 𝐿}) ∧ ¬ 𝐽 ∈ {𝐾, 𝐿}) → 𝐾 ≠ 𝐿)
163		prid2g 4711	. . . . . . . . 9 ⊢ (𝐿 ∈ 𝐷 → 𝐿 ∈ {𝐾, 𝐿})
164	161, 163	syl 17	. . . . . . . 8 ⊢ (((𝜑 ∧ ¬ 𝐼 ∈ {𝐾, 𝐿}) ∧ ¬ 𝐽 ∈ {𝐾, 𝐿}) → 𝐿 ∈ {𝐾, 𝐿})
165		nelne2 3026	. . . . . . . 8 ⊢ ((𝐿 ∈ {𝐾, 𝐿} ∧ ¬ 𝐽 ∈ {𝐾, 𝐿}) → 𝐿 ≠ 𝐽)
166	164, 165	sylancom 588	. . . . . . 7 ⊢ (((𝜑 ∧ ¬ 𝐼 ∈ {𝐾, 𝐿}) ∧ ¬ 𝐽 ∈ {𝐾, 𝐿}) → 𝐿 ≠ 𝐽)
167	7, 12, 146, 148, 161, 147, 162, 166, 151	cycpm3cl2 33105	. . . . . 6 ⊢ (((𝜑 ∧ ¬ 𝐼 ∈ {𝐾, 𝐿}) ∧ ¬ 𝐽 ∈ {𝐾, 𝐿}) → (𝑀‘⟨“𝐾𝐿𝐽”⟩) ∈ (𝑀 “ (◡♯ “ {3})))
168	167, 83	eleqtrrdi 2842	. . . . 5 ⊢ (((𝜑 ∧ ¬ 𝐼 ∈ {𝐾, 𝐿}) ∧ ¬ 𝐽 ∈ {𝐾, 𝐿}) → (𝑀‘⟨“𝐾𝐿𝐽”⟩) ∈ 𝐶)
169	160, 168	s2cld 14778	. . . 4 ⊢ (((𝜑 ∧ ¬ 𝐼 ∈ {𝐾, 𝐿}) ∧ ¬ 𝐽 ∈ {𝐾, 𝐿}) → ⟨“(𝑀‘⟨“𝐽𝐾𝐼”⟩)(𝑀‘⟨“𝐾𝐿𝐽”⟩)”⟩ ∈ Word 𝐶)
170		simpr 484	. . . . . 6 ⊢ ((((𝜑 ∧ ¬ 𝐼 ∈ {𝐾, 𝐿}) ∧ ¬ 𝐽 ∈ {𝐾, 𝐿}) ∧ 𝑐 = ⟨“(𝑀‘⟨“𝐽𝐾𝐼”⟩)(𝑀‘⟨“𝐾𝐿𝐽”⟩)”⟩) → 𝑐 = ⟨“(𝑀‘⟨“𝐽𝐾𝐼”⟩)(𝑀‘⟨“𝐾𝐿𝐽”⟩)”⟩)
171	170	oveq2d 7362	. . . . 5 ⊢ ((((𝜑 ∧ ¬ 𝐼 ∈ {𝐾, 𝐿}) ∧ ¬ 𝐽 ∈ {𝐾, 𝐿}) ∧ 𝑐 = ⟨“(𝑀‘⟨“𝐽𝐾𝐼”⟩)(𝑀‘⟨“𝐾𝐿𝐽”⟩)”⟩) → (𝑆 Σg 𝑐) = (𝑆 Σg ⟨“(𝑀‘⟨“𝐽𝐾𝐼”⟩)(𝑀‘⟨“𝐾𝐿𝐽”⟩)”⟩))
172	171	eqeq2d 2742	. . . 4 ⊢ ((((𝜑 ∧ ¬ 𝐼 ∈ {𝐾, 𝐿}) ∧ ¬ 𝐽 ∈ {𝐾, 𝐿}) ∧ 𝑐 = ⟨“(𝑀‘⟨“𝐽𝐾𝐼”⟩)(𝑀‘⟨“𝐾𝐿𝐽”⟩)”⟩) → ((𝐸 · 𝐹) = (𝑆 Σg 𝑐) ↔ (𝐸 · 𝐹) = (𝑆 Σg ⟨“(𝑀‘⟨“𝐽𝐾𝐼”⟩)(𝑀‘⟨“𝐾𝐿𝐽”⟩)”⟩)))
173	146, 56	syl 17	. . . . . . . . . 10 ⊢ (((𝜑 ∧ ¬ 𝐼 ∈ {𝐾, 𝐿}) ∧ ¬ 𝐽 ∈ {𝐾, 𝐿}) → ( I ↾ 𝐷) = (0g‘𝑆))
174	173	oveq1d 7361	. . . . . . . . 9 ⊢ (((𝜑 ∧ ¬ 𝐼 ∈ {𝐾, 𝐿}) ∧ ¬ 𝐽 ∈ {𝐾, 𝐿}) → (( I ↾ 𝐷) · (𝑀‘⟨“𝐾𝐿”⟩)) = ((0g‘𝑆) · (𝑀‘⟨“𝐾𝐿”⟩)))
175	12	symggrp 19312	. . . . . . . . . . . 12 ⊢ (𝐷 ∈ 𝑉 → 𝑆 ∈ Grp)
176	8, 175	syl 17	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑆 ∈ Grp)
177	176	ad2antrr 726	. . . . . . . . . 10 ⊢ (((𝜑 ∧ ¬ 𝐼 ∈ {𝐾, 𝐿}) ∧ ¬ 𝐽 ∈ {𝐾, 𝐿}) → 𝑆 ∈ Grp)
178	19	ad2antrr 726	. . . . . . . . . 10 ⊢ (((𝜑 ∧ ¬ 𝐼 ∈ {𝐾, 𝐿}) ∧ ¬ 𝐽 ∈ {𝐾, 𝐿}) → (𝑀‘⟨“𝐾𝐿”⟩) ∈ (Base‘𝑆))
179	21, 22, 58	grplid 18880	. . . . . . . . . 10 ⊢ ((𝑆 ∈ Grp ∧ (𝑀‘⟨“𝐾𝐿”⟩) ∈ (Base‘𝑆)) → ((0g‘𝑆) · (𝑀‘⟨“𝐾𝐿”⟩)) = (𝑀‘⟨“𝐾𝐿”⟩))
180	177, 178, 179	syl2anc 584	. . . . . . . . 9 ⊢ (((𝜑 ∧ ¬ 𝐼 ∈ {𝐾, 𝐿}) ∧ ¬ 𝐽 ∈ {𝐾, 𝐿}) → ((0g‘𝑆) · (𝑀‘⟨“𝐾𝐿”⟩)) = (𝑀‘⟨“𝐾𝐿”⟩))
181	174, 180	eqtrd 2766	. . . . . . . 8 ⊢ (((𝜑 ∧ ¬ 𝐼 ∈ {𝐾, 𝐿}) ∧ ¬ 𝐽 ∈ {𝐾, 𝐿}) → (( I ↾ 𝐷) · (𝑀‘⟨“𝐾𝐿”⟩)) = (𝑀‘⟨“𝐾𝐿”⟩))
182	181	oveq2d 7362	. . . . . . 7 ⊢ (((𝜑 ∧ ¬ 𝐼 ∈ {𝐾, 𝐿}) ∧ ¬ 𝐽 ∈ {𝐾, 𝐿}) → ((𝑀‘⟨“𝐼𝐽”⟩) · (( I ↾ 𝐷) · (𝑀‘⟨“𝐾𝐿”⟩))) = ((𝑀‘⟨“𝐼𝐽”⟩) · (𝑀‘⟨“𝐾𝐿”⟩)))
183	13	ad2antrr 726	. . . . . . . . 9 ⊢ (((𝜑 ∧ ¬ 𝐼 ∈ {𝐾, 𝐿}) ∧ ¬ 𝐽 ∈ {𝐾, 𝐿}) → (𝑀‘⟨“𝐼𝐽”⟩) ∈ (Base‘𝑆))
184	7, 146, 147, 148, 151, 27	cycpm2tr 33088	. . . . . . . . . 10 ⊢ (((𝜑 ∧ ¬ 𝐼 ∈ {𝐾, 𝐿}) ∧ ¬ 𝐽 ∈ {𝐾, 𝐿}) → (𝑀‘⟨“𝐽𝐾”⟩) = ((pmTrsp‘𝐷)‘{𝐽, 𝐾}))
185	50, 12, 21	symgtrf 19381	. . . . . . . . . . 11 ⊢ ran (pmTrsp‘𝐷) ⊆ (Base‘𝑆)
186	10, 16	prssd 4771	. . . . . . . . . . . . 13 ⊢ (𝜑 → {𝐽, 𝐾} ⊆ 𝐷)
187	186	ad2antrr 726	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ ¬ 𝐼 ∈ {𝐾, 𝐿}) ∧ ¬ 𝐽 ∈ {𝐾, 𝐿}) → {𝐽, 𝐾} ⊆ 𝐷)
188		enpr2 9895	. . . . . . . . . . . . 13 ⊢ ((𝐽 ∈ 𝐷 ∧ 𝐾 ∈ 𝐷 ∧ 𝐽 ≠ 𝐾) → {𝐽, 𝐾} ≈ 2o)
189	147, 148, 151, 188	syl3anc 1373	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ ¬ 𝐼 ∈ {𝐾, 𝐿}) ∧ ¬ 𝐽 ∈ {𝐾, 𝐿}) → {𝐽, 𝐾} ≈ 2o)
190	27, 50	pmtrrn 19369	. . . . . . . . . . . 12 ⊢ ((𝐷 ∈ 𝑉 ∧ {𝐽, 𝐾} ⊆ 𝐷 ∧ {𝐽, 𝐾} ≈ 2o) → ((pmTrsp‘𝐷)‘{𝐽, 𝐾}) ∈ ran (pmTrsp‘𝐷))
191	146, 187, 189, 190	syl3anc 1373	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ ¬ 𝐼 ∈ {𝐾, 𝐿}) ∧ ¬ 𝐽 ∈ {𝐾, 𝐿}) → ((pmTrsp‘𝐷)‘{𝐽, 𝐾}) ∈ ran (pmTrsp‘𝐷))
192	185, 191	sselid 3927	. . . . . . . . . 10 ⊢ (((𝜑 ∧ ¬ 𝐼 ∈ {𝐾, 𝐿}) ∧ ¬ 𝐽 ∈ {𝐾, 𝐿}) → ((pmTrsp‘𝐷)‘{𝐽, 𝐾}) ∈ (Base‘𝑆))
193	184, 192	eqeltrd 2831	. . . . . . . . 9 ⊢ (((𝜑 ∧ ¬ 𝐼 ∈ {𝐾, 𝐿}) ∧ ¬ 𝐽 ∈ {𝐾, 𝐿}) → (𝑀‘⟨“𝐽𝐾”⟩) ∈ (Base‘𝑆))
194	151	necomd 2983	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ ¬ 𝐼 ∈ {𝐾, 𝐿}) ∧ ¬ 𝐽 ∈ {𝐾, 𝐿}) → 𝐾 ≠ 𝐽)
195	7, 146, 148, 147, 194, 27	cycpm2tr 33088	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ ¬ 𝐼 ∈ {𝐾, 𝐿}) ∧ ¬ 𝐽 ∈ {𝐾, 𝐿}) → (𝑀‘⟨“𝐾𝐽”⟩) = ((pmTrsp‘𝐷)‘{𝐾, 𝐽}))
196		prcom 4682	. . . . . . . . . . . . . 14 ⊢ {𝐽, 𝐾} = {𝐾, 𝐽}
197	196	a1i 11	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ ¬ 𝐼 ∈ {𝐾, 𝐿}) ∧ ¬ 𝐽 ∈ {𝐾, 𝐿}) → {𝐽, 𝐾} = {𝐾, 𝐽})
198	197	fveq2d 6826	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ ¬ 𝐼 ∈ {𝐾, 𝐿}) ∧ ¬ 𝐽 ∈ {𝐾, 𝐿}) → ((pmTrsp‘𝐷)‘{𝐽, 𝐾}) = ((pmTrsp‘𝐷)‘{𝐾, 𝐽}))
199	195, 198	eqtr4d 2769	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ ¬ 𝐼 ∈ {𝐾, 𝐿}) ∧ ¬ 𝐽 ∈ {𝐾, 𝐿}) → (𝑀‘⟨“𝐾𝐽”⟩) = ((pmTrsp‘𝐷)‘{𝐽, 𝐾}))
200	199, 192	eqeltrd 2831	. . . . . . . . . 10 ⊢ (((𝜑 ∧ ¬ 𝐼 ∈ {𝐾, 𝐿}) ∧ ¬ 𝐽 ∈ {𝐾, 𝐿}) → (𝑀‘⟨“𝐾𝐽”⟩) ∈ (Base‘𝑆))
201	21, 22	grpcl 18854	. . . . . . . . . 10 ⊢ ((𝑆 ∈ Grp ∧ (𝑀‘⟨“𝐾𝐽”⟩) ∈ (Base‘𝑆) ∧ (𝑀‘⟨“𝐾𝐿”⟩) ∈ (Base‘𝑆)) → ((𝑀‘⟨“𝐾𝐽”⟩) · (𝑀‘⟨“𝐾𝐿”⟩)) ∈ (Base‘𝑆))
202	177, 200, 178, 201	syl3anc 1373	. . . . . . . . 9 ⊢ (((𝜑 ∧ ¬ 𝐼 ∈ {𝐾, 𝐿}) ∧ ¬ 𝐽 ∈ {𝐾, 𝐿}) → ((𝑀‘⟨“𝐾𝐽”⟩) · (𝑀‘⟨“𝐾𝐿”⟩)) ∈ (Base‘𝑆))
203	21, 22	grpass 18855	. . . . . . . . 9 ⊢ ((𝑆 ∈ Grp ∧ ((𝑀‘⟨“𝐼𝐽”⟩) ∈ (Base‘𝑆) ∧ (𝑀‘⟨“𝐽𝐾”⟩) ∈ (Base‘𝑆) ∧ ((𝑀‘⟨“𝐾𝐽”⟩) · (𝑀‘⟨“𝐾𝐿”⟩)) ∈ (Base‘𝑆))) → (((𝑀‘⟨“𝐼𝐽”⟩) · (𝑀‘⟨“𝐽𝐾”⟩)) · ((𝑀‘⟨“𝐾𝐽”⟩) · (𝑀‘⟨“𝐾𝐿”⟩))) = ((𝑀‘⟨“𝐼𝐽”⟩) · ((𝑀‘⟨“𝐽𝐾”⟩) · ((𝑀‘⟨“𝐾𝐽”⟩) · (𝑀‘⟨“𝐾𝐿”⟩)))))
204	177, 183, 193, 202, 203	syl13anc 1374	. . . . . . . 8 ⊢ (((𝜑 ∧ ¬ 𝐼 ∈ {𝐾, 𝐿}) ∧ ¬ 𝐽 ∈ {𝐾, 𝐿}) → (((𝑀‘⟨“𝐼𝐽”⟩) · (𝑀‘⟨“𝐽𝐾”⟩)) · ((𝑀‘⟨“𝐾𝐽”⟩) · (𝑀‘⟨“𝐾𝐿”⟩))) = ((𝑀‘⟨“𝐼𝐽”⟩) · ((𝑀‘⟨“𝐽𝐾”⟩) · ((𝑀‘⟨“𝐾𝐽”⟩) · (𝑀‘⟨“𝐾𝐿”⟩)))))
205	21, 22	grpass 18855	. . . . . . . . . 10 ⊢ ((𝑆 ∈ Grp ∧ ((𝑀‘⟨“𝐽𝐾”⟩) ∈ (Base‘𝑆) ∧ (𝑀‘⟨“𝐾𝐽”⟩) ∈ (Base‘𝑆) ∧ (𝑀‘⟨“𝐾𝐿”⟩) ∈ (Base‘𝑆))) → (((𝑀‘⟨“𝐽𝐾”⟩) · (𝑀‘⟨“𝐾𝐽”⟩)) · (𝑀‘⟨“𝐾𝐿”⟩)) = ((𝑀‘⟨“𝐽𝐾”⟩) · ((𝑀‘⟨“𝐾𝐽”⟩) · (𝑀‘⟨“𝐾𝐿”⟩))))
206	177, 193, 200, 178, 205	syl13anc 1374	. . . . . . . . 9 ⊢ (((𝜑 ∧ ¬ 𝐼 ∈ {𝐾, 𝐿}) ∧ ¬ 𝐽 ∈ {𝐾, 𝐿}) → (((𝑀‘⟨“𝐽𝐾”⟩) · (𝑀‘⟨“𝐾𝐽”⟩)) · (𝑀‘⟨“𝐾𝐿”⟩)) = ((𝑀‘⟨“𝐽𝐾”⟩) · ((𝑀‘⟨“𝐾𝐽”⟩) · (𝑀‘⟨“𝐾𝐿”⟩))))
207	206	oveq2d 7362	. . . . . . . 8 ⊢ (((𝜑 ∧ ¬ 𝐼 ∈ {𝐾, 𝐿}) ∧ ¬ 𝐽 ∈ {𝐾, 𝐿}) → ((𝑀‘⟨“𝐼𝐽”⟩) · (((𝑀‘⟨“𝐽𝐾”⟩) · (𝑀‘⟨“𝐾𝐽”⟩)) · (𝑀‘⟨“𝐾𝐿”⟩))) = ((𝑀‘⟨“𝐼𝐽”⟩) · ((𝑀‘⟨“𝐽𝐾”⟩) · ((𝑀‘⟨“𝐾𝐽”⟩) · (𝑀‘⟨“𝐾𝐿”⟩)))))
208	184, 199	oveq12d 7364	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ ¬ 𝐼 ∈ {𝐾, 𝐿}) ∧ ¬ 𝐽 ∈ {𝐾, 𝐿}) → ((𝑀‘⟨“𝐽𝐾”⟩) · (𝑀‘⟨“𝐾𝐽”⟩)) = (((pmTrsp‘𝐷)‘{𝐽, 𝐾}) · ((pmTrsp‘𝐷)‘{𝐽, 𝐾})))
209	12, 21, 22	symgov 19296	. . . . . . . . . . . 12 ⊢ ((((pmTrsp‘𝐷)‘{𝐽, 𝐾}) ∈ (Base‘𝑆) ∧ ((pmTrsp‘𝐷)‘{𝐽, 𝐾}) ∈ (Base‘𝑆)) → (((pmTrsp‘𝐷)‘{𝐽, 𝐾}) · ((pmTrsp‘𝐷)‘{𝐽, 𝐾})) = (((pmTrsp‘𝐷)‘{𝐽, 𝐾}) ∘ ((pmTrsp‘𝐷)‘{𝐽, 𝐾})))
210	192, 192, 209	syl2anc 584	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ ¬ 𝐼 ∈ {𝐾, 𝐿}) ∧ ¬ 𝐽 ∈ {𝐾, 𝐿}) → (((pmTrsp‘𝐷)‘{𝐽, 𝐾}) · ((pmTrsp‘𝐷)‘{𝐽, 𝐾})) = (((pmTrsp‘𝐷)‘{𝐽, 𝐾}) ∘ ((pmTrsp‘𝐷)‘{𝐽, 𝐾})))
211	27, 50	pmtrfinv 19373	. . . . . . . . . . . 12 ⊢ (((pmTrsp‘𝐷)‘{𝐽, 𝐾}) ∈ ran (pmTrsp‘𝐷) → (((pmTrsp‘𝐷)‘{𝐽, 𝐾}) ∘ ((pmTrsp‘𝐷)‘{𝐽, 𝐾})) = ( I ↾ 𝐷))
212	191, 211	syl 17	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ ¬ 𝐼 ∈ {𝐾, 𝐿}) ∧ ¬ 𝐽 ∈ {𝐾, 𝐿}) → (((pmTrsp‘𝐷)‘{𝐽, 𝐾}) ∘ ((pmTrsp‘𝐷)‘{𝐽, 𝐾})) = ( I ↾ 𝐷))
213	208, 210, 212	3eqtrd 2770	. . . . . . . . . 10 ⊢ (((𝜑 ∧ ¬ 𝐼 ∈ {𝐾, 𝐿}) ∧ ¬ 𝐽 ∈ {𝐾, 𝐿}) → ((𝑀‘⟨“𝐽𝐾”⟩) · (𝑀‘⟨“𝐾𝐽”⟩)) = ( I ↾ 𝐷))
214	213	oveq1d 7361	. . . . . . . . 9 ⊢ (((𝜑 ∧ ¬ 𝐼 ∈ {𝐾, 𝐿}) ∧ ¬ 𝐽 ∈ {𝐾, 𝐿}) → (((𝑀‘⟨“𝐽𝐾”⟩) · (𝑀‘⟨“𝐾𝐽”⟩)) · (𝑀‘⟨“𝐾𝐿”⟩)) = (( I ↾ 𝐷) · (𝑀‘⟨“𝐾𝐿”⟩)))
215	214	oveq2d 7362	. . . . . . . 8 ⊢ (((𝜑 ∧ ¬ 𝐼 ∈ {𝐾, 𝐿}) ∧ ¬ 𝐽 ∈ {𝐾, 𝐿}) → ((𝑀‘⟨“𝐼𝐽”⟩) · (((𝑀‘⟨“𝐽𝐾”⟩) · (𝑀‘⟨“𝐾𝐽”⟩)) · (𝑀‘⟨“𝐾𝐿”⟩))) = ((𝑀‘⟨“𝐼𝐽”⟩) · (( I ↾ 𝐷) · (𝑀‘⟨“𝐾𝐿”⟩))))
216	204, 207, 215	3eqtr2rd 2773	. . . . . . 7 ⊢ (((𝜑 ∧ ¬ 𝐼 ∈ {𝐾, 𝐿}) ∧ ¬ 𝐽 ∈ {𝐾, 𝐿}) → ((𝑀‘⟨“𝐼𝐽”⟩) · (( I ↾ 𝐷) · (𝑀‘⟨“𝐾𝐿”⟩))) = (((𝑀‘⟨“𝐼𝐽”⟩) · (𝑀‘⟨“𝐽𝐾”⟩)) · ((𝑀‘⟨“𝐾𝐽”⟩) · (𝑀‘⟨“𝐾𝐿”⟩))))
217	182, 216	eqtr3d 2768	. . . . . 6 ⊢ (((𝜑 ∧ ¬ 𝐼 ∈ {𝐾, 𝐿}) ∧ ¬ 𝐽 ∈ {𝐾, 𝐿}) → ((𝑀‘⟨“𝐼𝐽”⟩) · (𝑀‘⟨“𝐾𝐿”⟩)) = (((𝑀‘⟨“𝐼𝐽”⟩) · (𝑀‘⟨“𝐽𝐾”⟩)) · ((𝑀‘⟨“𝐾𝐽”⟩) · (𝑀‘⟨“𝐾𝐿”⟩))))
218	6, 15	oveq12d 7364	. . . . . . 7 ⊢ (𝜑 → (𝐸 · 𝐹) = ((𝑀‘⟨“𝐼𝐽”⟩) · (𝑀‘⟨“𝐾𝐿”⟩)))
219	218	ad2antrr 726	. . . . . 6 ⊢ (((𝜑 ∧ ¬ 𝐼 ∈ {𝐾, 𝐿}) ∧ ¬ 𝐽 ∈ {𝐾, 𝐿}) → (𝐸 · 𝐹) = ((𝑀‘⟨“𝐼𝐽”⟩) · (𝑀‘⟨“𝐾𝐿”⟩)))
220	7, 12, 146, 147, 148, 149, 151, 157, 158, 22	cyc3co2 33109	. . . . . . . 8 ⊢ (((𝜑 ∧ ¬ 𝐼 ∈ {𝐾, 𝐿}) ∧ ¬ 𝐽 ∈ {𝐾, 𝐿}) → (𝑀‘⟨“𝐽𝐾𝐼”⟩) = ((𝑀‘⟨“𝐽𝐼”⟩) · (𝑀‘⟨“𝐽𝐾”⟩)))
221	134	oveq1d 7361	. . . . . . . . 9 ⊢ (𝜑 → ((𝑀‘⟨“𝐼𝐽”⟩) · (𝑀‘⟨“𝐽𝐾”⟩)) = ((𝑀‘⟨“𝐽𝐼”⟩) · (𝑀‘⟨“𝐽𝐾”⟩)))
222	221	ad2antrr 726	. . . . . . . 8 ⊢ (((𝜑 ∧ ¬ 𝐼 ∈ {𝐾, 𝐿}) ∧ ¬ 𝐽 ∈ {𝐾, 𝐿}) → ((𝑀‘⟨“𝐼𝐽”⟩) · (𝑀‘⟨“𝐽𝐾”⟩)) = ((𝑀‘⟨“𝐽𝐼”⟩) · (𝑀‘⟨“𝐽𝐾”⟩)))
223	220, 222	eqtr4d 2769	. . . . . . 7 ⊢ (((𝜑 ∧ ¬ 𝐼 ∈ {𝐾, 𝐿}) ∧ ¬ 𝐽 ∈ {𝐾, 𝐿}) → (𝑀‘⟨“𝐽𝐾𝐼”⟩) = ((𝑀‘⟨“𝐼𝐽”⟩) · (𝑀‘⟨“𝐽𝐾”⟩)))
224	7, 12, 146, 148, 161, 147, 162, 166, 151, 22	cyc3co2 33109	. . . . . . 7 ⊢ (((𝜑 ∧ ¬ 𝐼 ∈ {𝐾, 𝐿}) ∧ ¬ 𝐽 ∈ {𝐾, 𝐿}) → (𝑀‘⟨“𝐾𝐿𝐽”⟩) = ((𝑀‘⟨“𝐾𝐽”⟩) · (𝑀‘⟨“𝐾𝐿”⟩)))
225	223, 224	oveq12d 7364	. . . . . 6 ⊢ (((𝜑 ∧ ¬ 𝐼 ∈ {𝐾, 𝐿}) ∧ ¬ 𝐽 ∈ {𝐾, 𝐿}) → ((𝑀‘⟨“𝐽𝐾𝐼”⟩) · (𝑀‘⟨“𝐾𝐿𝐽”⟩)) = (((𝑀‘⟨“𝐼𝐽”⟩) · (𝑀‘⟨“𝐽𝐾”⟩)) · ((𝑀‘⟨“𝐾𝐽”⟩) · (𝑀‘⟨“𝐾𝐿”⟩))))
226	217, 219, 225	3eqtr4d 2776	. . . . 5 ⊢ (((𝜑 ∧ ¬ 𝐼 ∈ {𝐾, 𝐿}) ∧ ¬ 𝐽 ∈ {𝐾, 𝐿}) → (𝐸 · 𝐹) = ((𝑀‘⟨“𝐽𝐾𝐼”⟩) · (𝑀‘⟨“𝐾𝐿𝐽”⟩)))
227	176	grpmndd 18859	. . . . . . 7 ⊢ (𝜑 → 𝑆 ∈ Mnd)
228	227	ad2antrr 726	. . . . . 6 ⊢ (((𝜑 ∧ ¬ 𝐼 ∈ {𝐾, 𝐿}) ∧ ¬ 𝐽 ∈ {𝐾, 𝐿}) → 𝑆 ∈ Mnd)
229	7, 12, 146, 147, 148, 149, 151, 157, 158	cycpm3cl 33104	. . . . . 6 ⊢ (((𝜑 ∧ ¬ 𝐼 ∈ {𝐾, 𝐿}) ∧ ¬ 𝐽 ∈ {𝐾, 𝐿}) → (𝑀‘⟨“𝐽𝐾𝐼”⟩) ∈ (Base‘𝑆))
230	224, 202	eqeltrd 2831	. . . . . 6 ⊢ (((𝜑 ∧ ¬ 𝐼 ∈ {𝐾, 𝐿}) ∧ ¬ 𝐽 ∈ {𝐾, 𝐿}) → (𝑀‘⟨“𝐾𝐿𝐽”⟩) ∈ (Base‘𝑆))
231	21, 22	gsumws2 18750	. . . . . 6 ⊢ ((𝑆 ∈ Mnd ∧ (𝑀‘⟨“𝐽𝐾𝐼”⟩) ∈ (Base‘𝑆) ∧ (𝑀‘⟨“𝐾𝐿𝐽”⟩) ∈ (Base‘𝑆)) → (𝑆 Σg ⟨“(𝑀‘⟨“𝐽𝐾𝐼”⟩)(𝑀‘⟨“𝐾𝐿𝐽”⟩)”⟩) = ((𝑀‘⟨“𝐽𝐾𝐼”⟩) · (𝑀‘⟨“𝐾𝐿𝐽”⟩)))
232	228, 229, 230, 231	syl3anc 1373	. . . . 5 ⊢ (((𝜑 ∧ ¬ 𝐼 ∈ {𝐾, 𝐿}) ∧ ¬ 𝐽 ∈ {𝐾, 𝐿}) → (𝑆 Σg ⟨“(𝑀‘⟨“𝐽𝐾𝐼”⟩)(𝑀‘⟨“𝐾𝐿𝐽”⟩)”⟩) = ((𝑀‘⟨“𝐽𝐾𝐼”⟩) · (𝑀‘⟨“𝐾𝐿𝐽”⟩)))
233	226, 232	eqtr4d 2769	. . . 4 ⊢ (((𝜑 ∧ ¬ 𝐼 ∈ {𝐾, 𝐿}) ∧ ¬ 𝐽 ∈ {𝐾, 𝐿}) → (𝐸 · 𝐹) = (𝑆 Σg ⟨“(𝑀‘⟨“𝐽𝐾𝐼”⟩)(𝑀‘⟨“𝐾𝐿𝐽”⟩)”⟩))
234	169, 172, 233	rspcedvd 3574	. . 3 ⊢ (((𝜑 ∧ ¬ 𝐼 ∈ {𝐾, 𝐿}) ∧ ¬ 𝐽 ∈ {𝐾, 𝐿}) → ∃𝑐 ∈ Word 𝐶(𝐸 · 𝐹) = (𝑆 Σg 𝑐))
235	145, 234	pm2.61dan 812	. 2 ⊢ ((𝜑 ∧ ¬ 𝐼 ∈ {𝐾, 𝐿}) → ∃𝑐 ∈ Word 𝐶(𝐸 · 𝐹) = (𝑆 Σg 𝑐))
236	104, 235	pm2.61dan 812	1 ⊢ (𝜑 → ∃𝑐 ∈ Word 𝐶(𝐸 · 𝐹) = (𝑆 Σg 𝑐))

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 395   ∧ w3a 1086   = wceq 1541   ∈ wcel 2111   ≠ wne 2928  ∃wrex 3056   ∖ cdif 3894   ⊆ wss 3897  ∅c0 4280  {csn 4573  {cpr 4575  ∪ cuni 4856   class class class wbr 5089   I cid 5508  ^◡ccnv 5613  ran crn 5615   ↾ cres 5616   “ cima 5617   ∘ ccom 5618  ‘cfv 6481  (class class class)co 7346  2_oc2o 8379   ≈ cen 8866  3c3 12181  ♯chash 14237  Word cword 14420  ⟨“cs1 14503  ⟨“cs2 14748  ⟨“cs3 14749  Basecbs 17120  +_gcplusg 17161  0_gc0g 17343   Σ_g cgsu 17344  Mndcmnd 18642  Grpcgrp 18846  SymGrpcsymg 19281  pmTrspcpmtr 19353  pmEvencevpm 19402  toCycctocyc 33075

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-10 2144  ax-11 2160  ax-12 2180  ax-ext 2703  ax-rep 5215  ax-sep 5232  ax-nul 5242  ax-pow 5301  ax-pr 5368  ax-un 7668  ax-reg 9478  ax-ac2 10354  ax-cnex 11062  ax-resscn 11063  ax-1cn 11064  ax-icn 11065  ax-addcl 11066  ax-addrcl 11067  ax-mulcl 11068  ax-mulrcl 11069  ax-mulcom 11070  ax-addass 11071  ax-mulass 11072  ax-distr 11073  ax-i2m1 11074  ax-1ne0 11075  ax-1rid 11076  ax-rnegex 11077  ax-rrecex 11078  ax-cnre 11079  ax-pre-lttri 11080  ax-pre-lttrn 11081  ax-pre-ltadd 11082  ax-pre-mulgt0 11083  ax-pre-sup 11084

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-nf 1785  df-sb 2068  df-mo 2535  df-eu 2564  df-clab 2710  df-cleq 2723  df-clel 2806  df-nfc 2881  df-ne 2929  df-nel 3033  df-ral 3048  df-rex 3057  df-rmo 3346  df-reu 3347  df-rab 3396  df-v 3438  df-sbc 3737  df-csb 3846  df-dif 3900  df-un 3902  df-in 3904  df-ss 3914  df-pss 3917  df-nul 4281  df-if 4473  df-pw 4549  df-sn 4574  df-pr 4576  df-tp 4578  df-op 4580  df-uni 4857  df-int 4896  df-iun 4941  df-br 5090  df-opab 5152  df-mpt 5171  df-tr 5197  df-id 5509  df-eprel 5514  df-po 5522  df-so 5523  df-fr 5567  df-se 5568  df-we 5569  df-xp 5620  df-rel 5621  df-cnv 5622  df-co 5623  df-dm 5624  df-rn 5625  df-res 5626  df-ima 5627  df-pred 6248  df-ord 6309  df-on 6310  df-lim 6311  df-suc 6312  df-iota 6437  df-fun 6483  df-fn 6484  df-f 6485  df-f1 6486  df-fo 6487  df-f1o 6488  df-fv 6489  df-isom 6490  df-riota 7303  df-ov 7349  df-oprab 7350  df-mpo 7351  df-om 7797  df-1st 7921  df-2nd 7922  df-frecs 8211  df-wrecs 8242  df-recs 8291  df-rdg 8329  df-1o 8385  df-2o 8386  df-er 8622  df-map 8752  df-en 8870  df-dom 8871  df-sdom 8872  df-fin 8873  df-sup 9326  df-inf 9327  df-card 9832  df-ac 10007  df-pnf 11148  df-mnf 11149  df-xr 11150  df-ltxr 11151  df-le 11152  df-sub 11346  df-neg 11347  df-div 11775  df-nn 12126  df-2 12188  df-3 12189  df-4 12190  df-5 12191  df-6 12192  df-7 12193  df-8 12194  df-9 12195  df-n0 12382  df-xnn0 12455  df-z 12469  df-uz 12733  df-rp 12891  df-fz 13408  df-fzo 13555  df-fl 13696  df-mod 13774  df-seq 13909  df-hash 14238  df-word 14421  df-concat 14478  df-s1 14504  df-substr 14549  df-pfx 14579  df-csh 14696  df-s2 14755  df-s3 14756  df-struct 17058  df-sets 17075  df-slot 17093  df-ndx 17105  df-base 17121  df-ress 17142  df-plusg 17174  df-tset 17180  df-0g 17345  df-gsum 17346  df-mgm 18548  df-sgrp 18627  df-mnd 18643  df-submnd 18692  df-efmnd 18777  df-grp 18849  df-symg 19282  df-pmtr 19354  df-tocyc 33076

This theorem is referenced by:  cyc3genpm  33121