Theorem cyc3genpmlem 31418

Description: Lemma for cyc3genpm 31419. (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 14242	. . . . 5 ⊢ ∅ ∈ Word 𝐶
2	1	a1i 11	. . . 4 ⊢ (((𝜑 ∧ 𝐼 ∈ {𝐾, 𝐿}) ∧ 𝐽 ∈ {𝐾, 𝐿}) → ∅ ∈ Word 𝐶)
3		simpr 485	. . . . . 6 ⊢ ((((𝜑 ∧ 𝐼 ∈ {𝐾, 𝐿}) ∧ 𝐽 ∈ {𝐾, 𝐿}) ∧ 𝑐 = ∅) → 𝑐 = ∅)
4	3	oveq2d 7291	. . . . 5 ⊢ ((((𝜑 ∧ 𝐼 ∈ {𝐾, 𝐿}) ∧ 𝐽 ∈ {𝐾, 𝐿}) ∧ 𝑐 = ∅) → (𝑆 Σg 𝑐) = (𝑆 Σg ∅))
5	4	eqeq2d 2749	. . . 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 31387	. . . . . . . . 9 ⊢ (𝜑 → (𝑀‘⟨“𝐼𝐽”⟩) ∈ (Base‘𝑆))
14	6, 13	eqeltrd 2839	. . . . . . . 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 31387	. . . . . . . . 9 ⊢ (𝜑 → (𝑀‘⟨“𝐾𝐿”⟩) ∈ (Base‘𝑆))
20	15, 19	eqeltrd 2839	. . . . . . . 8 ⊢ (𝜑 → 𝐹 ∈ (Base‘𝑆))
21		eqid 2738	. . . . . . . . 9 ⊢ (Base‘𝑆) = (Base‘𝑆)
22		cyc3genpmlem.t	. . . . . . . . 9 ⊢ · = (+g‘𝑆)
23	12, 21, 22	symgov 18991	. . . . . . . 8 ⊢ ((𝐸 ∈ (Base‘𝑆) ∧ 𝐹 ∈ (Base‘𝑆)) → (𝐸 · 𝐹) = (𝐸 ∘ 𝐹))
24	14, 20, 23	syl2anc 584	. . . . . . 7 ⊢ (𝜑 → (𝐸 · 𝐹) = (𝐸 ∘ 𝐹))
25	24	ad2antrr 723	. . . . . 6 ⊢ (((𝜑 ∧ 𝐼 ∈ {𝐾, 𝐿}) ∧ 𝐽 ∈ {𝐾, 𝐿}) → (𝐸 · 𝐹) = (𝐸 ∘ 𝐹))
26	6	ad2antrr 723	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝐼 ∈ {𝐾, 𝐿}) ∧ 𝐽 ∈ {𝐾, 𝐿}) → 𝐸 = (𝑀‘⟨“𝐼𝐽”⟩))
27		eqid 2738	. . . . . . . . . 10 ⊢ (pmTrsp‘𝐷) = (pmTrsp‘𝐷)
28	7, 8, 9, 10, 11, 27	cycpm2tr 31386	. . . . . . . . 9 ⊢ (𝜑 → (𝑀‘⟨“𝐼𝐽”⟩) = ((pmTrsp‘𝐷)‘{𝐼, 𝐽}))
29	28	ad2antrr 723	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝐼 ∈ {𝐾, 𝐿}) ∧ 𝐽 ∈ {𝐾, 𝐿}) → (𝑀‘⟨“𝐼𝐽”⟩) = ((pmTrsp‘𝐷)‘{𝐼, 𝐽}))
30	26, 29	eqtrd 2778	. . . . . . 7 ⊢ (((𝜑 ∧ 𝐼 ∈ {𝐾, 𝐿}) ∧ 𝐽 ∈ {𝐾, 𝐿}) → 𝐸 = ((pmTrsp‘𝐷)‘{𝐼, 𝐽}))
31	7, 8, 16, 17, 18, 27	cycpm2tr 31386	. . . . . . . . 9 ⊢ (𝜑 → (𝑀‘⟨“𝐾𝐿”⟩) = ((pmTrsp‘𝐷)‘{𝐾, 𝐿}))
32	31	ad2antrr 723	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝐼 ∈ {𝐾, 𝐿}) ∧ 𝐽 ∈ {𝐾, 𝐿}) → (𝑀‘⟨“𝐾𝐿”⟩) = ((pmTrsp‘𝐷)‘{𝐾, 𝐿}))
33	15	ad2antrr 723	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝐼 ∈ {𝐾, 𝐿}) ∧ 𝐽 ∈ {𝐾, 𝐿}) → 𝐹 = (𝑀‘⟨“𝐾𝐿”⟩))
34	9	ad2antrr 723	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝐼 ∈ {𝐾, 𝐿}) ∧ 𝐽 ∈ {𝐾, 𝐿}) → 𝐼 ∈ 𝐷)
35	10	ad2antrr 723	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝐼 ∈ {𝐾, 𝐿}) ∧ 𝐽 ∈ {𝐾, 𝐿}) → 𝐽 ∈ 𝐷)
36	11	ad2antrr 723	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝐼 ∈ {𝐾, 𝐿}) ∧ 𝐽 ∈ {𝐾, 𝐿}) → 𝐼 ≠ 𝐽)
37		simplr 766	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝐼 ∈ {𝐾, 𝐿}) ∧ 𝐽 ∈ {𝐾, 𝐿}) → 𝐼 ∈ {𝐾, 𝐿})
38		simpr 485	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝐼 ∈ {𝐾, 𝐿}) ∧ 𝐽 ∈ {𝐾, 𝐿}) → 𝐽 ∈ {𝐾, 𝐿})
39	37, 38	prssd 4755	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝐼 ∈ {𝐾, 𝐿}) ∧ 𝐽 ∈ {𝐾, 𝐿}) → {𝐼, 𝐽} ⊆ {𝐾, 𝐿})
40		ssprsseq 4758	. . . . . . . . . . 11 ⊢ ((𝐼 ∈ 𝐷 ∧ 𝐽 ∈ 𝐷 ∧ 𝐼 ≠ 𝐽) → ({𝐼, 𝐽} ⊆ {𝐾, 𝐿} ↔ {𝐼, 𝐽} = {𝐾, 𝐿}))
41	40	biimpa 477	. . . . . . . . . 10 ⊢ (((𝐼 ∈ 𝐷 ∧ 𝐽 ∈ 𝐷 ∧ 𝐼 ≠ 𝐽) ∧ {𝐼, 𝐽} ⊆ {𝐾, 𝐿}) → {𝐼, 𝐽} = {𝐾, 𝐿})
42	34, 35, 36, 39, 41	syl31anc 1372	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝐼 ∈ {𝐾, 𝐿}) ∧ 𝐽 ∈ {𝐾, 𝐿}) → {𝐼, 𝐽} = {𝐾, 𝐿})
43	42	fveq2d 6778	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝐼 ∈ {𝐾, 𝐿}) ∧ 𝐽 ∈ {𝐾, 𝐿}) → ((pmTrsp‘𝐷)‘{𝐼, 𝐽}) = ((pmTrsp‘𝐷)‘{𝐾, 𝐿}))
44	32, 33, 43	3eqtr4d 2788	. . . . . . 7 ⊢ (((𝜑 ∧ 𝐼 ∈ {𝐾, 𝐿}) ∧ 𝐽 ∈ {𝐾, 𝐿}) → 𝐹 = ((pmTrsp‘𝐷)‘{𝐼, 𝐽}))
45	30, 44	coeq12d 5773	. . . . . 6 ⊢ (((𝜑 ∧ 𝐼 ∈ {𝐾, 𝐿}) ∧ 𝐽 ∈ {𝐾, 𝐿}) → (𝐸 ∘ 𝐹) = (((pmTrsp‘𝐷)‘{𝐼, 𝐽}) ∘ ((pmTrsp‘𝐷)‘{𝐼, 𝐽})))
46	8	ad2antrr 723	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝐼 ∈ {𝐾, 𝐿}) ∧ 𝐽 ∈ {𝐾, 𝐿}) → 𝐷 ∈ 𝑉)
47	34, 35	prssd 4755	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝐼 ∈ {𝐾, 𝐿}) ∧ 𝐽 ∈ {𝐾, 𝐿}) → {𝐼, 𝐽} ⊆ 𝐷)
48		pr2nelem 9760	. . . . . . . . 9 ⊢ ((𝐼 ∈ 𝐷 ∧ 𝐽 ∈ 𝐷 ∧ 𝐼 ≠ 𝐽) → {𝐼, 𝐽} ≈ 2o)
49	34, 35, 36, 48	syl3anc 1370	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝐼 ∈ {𝐾, 𝐿}) ∧ 𝐽 ∈ {𝐾, 𝐿}) → {𝐼, 𝐽} ≈ 2o)
50		eqid 2738	. . . . . . . . 9 ⊢ ran (pmTrsp‘𝐷) = ran (pmTrsp‘𝐷)
51	27, 50	pmtrrn 19065	. . . . . . . 8 ⊢ ((𝐷 ∈ 𝑉 ∧ {𝐼, 𝐽} ⊆ 𝐷 ∧ {𝐼, 𝐽} ≈ 2o) → ((pmTrsp‘𝐷)‘{𝐼, 𝐽}) ∈ ran (pmTrsp‘𝐷))
52	46, 47, 49, 51	syl3anc 1370	. . . . . . 7 ⊢ (((𝜑 ∧ 𝐼 ∈ {𝐾, 𝐿}) ∧ 𝐽 ∈ {𝐾, 𝐿}) → ((pmTrsp‘𝐷)‘{𝐼, 𝐽}) ∈ ran (pmTrsp‘𝐷))
53	27, 50	pmtrfinv 19069	. . . . . . 7 ⊢ (((pmTrsp‘𝐷)‘{𝐼, 𝐽}) ∈ ran (pmTrsp‘𝐷) → (((pmTrsp‘𝐷)‘{𝐼, 𝐽}) ∘ ((pmTrsp‘𝐷)‘{𝐼, 𝐽})) = ( I ↾ 𝐷))
54	52, 53	syl 17	. . . . . 6 ⊢ (((𝜑 ∧ 𝐼 ∈ {𝐾, 𝐿}) ∧ 𝐽 ∈ {𝐾, 𝐿}) → (((pmTrsp‘𝐷)‘{𝐼, 𝐽}) ∘ ((pmTrsp‘𝐷)‘{𝐼, 𝐽})) = ( I ↾ 𝐷))
55	25, 45, 54	3eqtrd 2782	. . . . 5 ⊢ (((𝜑 ∧ 𝐼 ∈ {𝐾, 𝐿}) ∧ 𝐽 ∈ {𝐾, 𝐿}) → (𝐸 · 𝐹) = ( I ↾ 𝐷))
56	12	symgid 19009	. . . . . . 7 ⊢ (𝐷 ∈ 𝑉 → ( I ↾ 𝐷) = (0g‘𝑆))
57	46, 56	syl 17	. . . . . 6 ⊢ (((𝜑 ∧ 𝐼 ∈ {𝐾, 𝐿}) ∧ 𝐽 ∈ {𝐾, 𝐿}) → ( I ↾ 𝐷) = (0g‘𝑆))
58		eqid 2738	. . . . . . 7 ⊢ (0g‘𝑆) = (0g‘𝑆)
59	58	gsum0 18368	. . . . . 6 ⊢ (𝑆 Σg ∅) = (0g‘𝑆)
60	57, 59	eqtr4di 2796	. . . . 5 ⊢ (((𝜑 ∧ 𝐼 ∈ {𝐾, 𝐿}) ∧ 𝐽 ∈ {𝐾, 𝐿}) → ( I ↾ 𝐷) = (𝑆 Σg ∅))
61	55, 60	eqtrd 2778	. . . 4 ⊢ (((𝜑 ∧ 𝐼 ∈ {𝐾, 𝐿}) ∧ 𝐽 ∈ {𝐾, 𝐿}) → (𝐸 · 𝐹) = (𝑆 Σg ∅))
62	2, 5, 61	rspcedvd 3563	. . 3 ⊢ (((𝜑 ∧ 𝐼 ∈ {𝐾, 𝐿}) ∧ 𝐽 ∈ {𝐾, 𝐿}) → ∃𝑐 ∈ Word 𝐶(𝐸 · 𝐹) = (𝑆 Σg 𝑐))
63	8	ad2antrr 723	. . . . . . 7 ⊢ (((𝜑 ∧ 𝐼 ∈ {𝐾, 𝐿}) ∧ ¬ 𝐽 ∈ {𝐾, 𝐿}) → 𝐷 ∈ 𝑉)
64	9	ad2antrr 723	. . . . . . 7 ⊢ (((𝜑 ∧ 𝐼 ∈ {𝐾, 𝐿}) ∧ ¬ 𝐽 ∈ {𝐾, 𝐿}) → 𝐼 ∈ 𝐷)
65	16, 17	prssd 4755	. . . . . . . . 9 ⊢ (𝜑 → {𝐾, 𝐿} ⊆ 𝐷)
66	65	ad2antrr 723	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝐼 ∈ {𝐾, 𝐿}) ∧ ¬ 𝐽 ∈ {𝐾, 𝐿}) → {𝐾, 𝐿} ⊆ 𝐷)
67		simplr 766	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝐼 ∈ {𝐾, 𝐿}) ∧ ¬ 𝐽 ∈ {𝐾, 𝐿}) → 𝐼 ∈ {𝐾, 𝐿})
68		pr2nelem 9760	. . . . . . . . . . 11 ⊢ ((𝐾 ∈ 𝐷 ∧ 𝐿 ∈ 𝐷 ∧ 𝐾 ≠ 𝐿) → {𝐾, 𝐿} ≈ 2o)
69	16, 17, 18, 68	syl3anc 1370	. . . . . . . . . 10 ⊢ (𝜑 → {𝐾, 𝐿} ≈ 2o)
70	69	ad2antrr 723	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝐼 ∈ {𝐾, 𝐿}) ∧ ¬ 𝐽 ∈ {𝐾, 𝐿}) → {𝐾, 𝐿} ≈ 2o)
71		unidifsnel 30883	. . . . . . . . 9 ⊢ ((𝐼 ∈ {𝐾, 𝐿} ∧ {𝐾, 𝐿} ≈ 2o) → ∪ ({𝐾, 𝐿} ∖ {𝐼}) ∈ {𝐾, 𝐿})
72	67, 70, 71	syl2anc 584	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝐼 ∈ {𝐾, 𝐿}) ∧ ¬ 𝐽 ∈ {𝐾, 𝐿}) → ∪ ({𝐾, 𝐿} ∖ {𝐼}) ∈ {𝐾, 𝐿})
73	66, 72	sseldd 3922	. . . . . . 7 ⊢ (((𝜑 ∧ 𝐼 ∈ {𝐾, 𝐿}) ∧ ¬ 𝐽 ∈ {𝐾, 𝐿}) → ∪ ({𝐾, 𝐿} ∖ {𝐼}) ∈ 𝐷)
74	10	ad2antrr 723	. . . . . . 7 ⊢ (((𝜑 ∧ 𝐼 ∈ {𝐾, 𝐿}) ∧ ¬ 𝐽 ∈ {𝐾, 𝐿}) → 𝐽 ∈ 𝐷)
75		unidifsnne 30884	. . . . . . . . 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 723	. . . . . . 7 ⊢ (((𝜑 ∧ 𝐼 ∈ {𝐾, 𝐿}) ∧ ¬ 𝐽 ∈ {𝐾, 𝐿}) → 𝐽 ≠ 𝐼)
82	7, 12, 63, 64, 73, 74, 77, 79, 81	cycpm3cl2 31403	. . . . . 6 ⊢ (((𝜑 ∧ 𝐼 ∈ {𝐾, 𝐿}) ∧ ¬ 𝐽 ∈ {𝐾, 𝐿}) → (𝑀‘⟨“𝐼∪ ({𝐾, 𝐿} ∖ {𝐼})𝐽”⟩) ∈ (𝑀 “ (◡♯ “ {3})))
83		cyc3genpm.t	. . . . . 6 ⊢ 𝐶 = (𝑀 “ (◡♯ “ {3}))
84	82, 83	eleqtrrdi 2850	. . . . 5 ⊢ (((𝜑 ∧ 𝐼 ∈ {𝐾, 𝐿}) ∧ ¬ 𝐽 ∈ {𝐾, 𝐿}) → (𝑀‘⟨“𝐼∪ ({𝐾, 𝐿} ∖ {𝐼})𝐽”⟩) ∈ 𝐶)
85	84	s1cld 14308	. . . 4 ⊢ (((𝜑 ∧ 𝐼 ∈ {𝐾, 𝐿}) ∧ ¬ 𝐽 ∈ {𝐾, 𝐿}) → ⟨“(𝑀‘⟨“𝐼∪ ({𝐾, 𝐿} ∖ {𝐼})𝐽”⟩)”⟩ ∈ Word 𝐶)
86		simpr 485	. . . . . 6 ⊢ ((((𝜑 ∧ 𝐼 ∈ {𝐾, 𝐿}) ∧ ¬ 𝐽 ∈ {𝐾, 𝐿}) ∧ 𝑐 = ⟨“(𝑀‘⟨“𝐼∪ ({𝐾, 𝐿} ∖ {𝐼})𝐽”⟩)”⟩) → 𝑐 = ⟨“(𝑀‘⟨“𝐼∪ ({𝐾, 𝐿} ∖ {𝐼})𝐽”⟩)”⟩)
87	86	oveq2d 7291	. . . . 5 ⊢ ((((𝜑 ∧ 𝐼 ∈ {𝐾, 𝐿}) ∧ ¬ 𝐽 ∈ {𝐾, 𝐿}) ∧ 𝑐 = ⟨“(𝑀‘⟨“𝐼∪ ({𝐾, 𝐿} ∖ {𝐼})𝐽”⟩)”⟩) → (𝑆 Σg 𝑐) = (𝑆 Σg ⟨“(𝑀‘⟨“𝐼∪ ({𝐾, 𝐿} ∖ {𝐼})𝐽”⟩)”⟩))
88	87	eqeq2d 2749	. . . 4 ⊢ ((((𝜑 ∧ 𝐼 ∈ {𝐾, 𝐿}) ∧ ¬ 𝐽 ∈ {𝐾, 𝐿}) ∧ 𝑐 = ⟨“(𝑀‘⟨“𝐼∪ ({𝐾, 𝐿} ∖ {𝐼})𝐽”⟩)”⟩) → ((𝐸 · 𝐹) = (𝑆 Σg 𝑐) ↔ (𝐸 · 𝐹) = (𝑆 Σg ⟨“(𝑀‘⟨“𝐼∪ ({𝐾, 𝐿} ∖ {𝐼})𝐽”⟩)”⟩)))
89	7, 12, 63, 64, 73, 74, 77, 79, 81, 22	cyc3co2 31407	. . . . 5 ⊢ (((𝜑 ∧ 𝐼 ∈ {𝐾, 𝐿}) ∧ ¬ 𝐽 ∈ {𝐾, 𝐿}) → (𝑀‘⟨“𝐼∪ ({𝐾, 𝐿} ∖ {𝐼})𝐽”⟩) = ((𝑀‘⟨“𝐼𝐽”⟩) · (𝑀‘⟨“𝐼∪ ({𝐾, 𝐿} ∖ {𝐼})”⟩)))
90	7, 12, 63, 64, 73, 74, 77, 79, 81	cycpm3cl 31402	. . . . . 6 ⊢ (((𝜑 ∧ 𝐼 ∈ {𝐾, 𝐿}) ∧ ¬ 𝐽 ∈ {𝐾, 𝐿}) → (𝑀‘⟨“𝐼∪ ({𝐾, 𝐿} ∖ {𝐼})𝐽”⟩) ∈ (Base‘𝑆))
91	21	gsumws1 18476	. . . . . 6 ⊢ ((𝑀‘⟨“𝐼∪ ({𝐾, 𝐿} ∖ {𝐼})𝐽”⟩) ∈ (Base‘𝑆) → (𝑆 Σg ⟨“(𝑀‘⟨“𝐼∪ ({𝐾, 𝐿} ∖ {𝐼})𝐽”⟩)”⟩) = (𝑀‘⟨“𝐼∪ ({𝐾, 𝐿} ∖ {𝐼})𝐽”⟩))
92	90, 91	syl 17	. . . . 5 ⊢ (((𝜑 ∧ 𝐼 ∈ {𝐾, 𝐿}) ∧ ¬ 𝐽 ∈ {𝐾, 𝐿}) → (𝑆 Σg ⟨“(𝑀‘⟨“𝐼∪ ({𝐾, 𝐿} ∖ {𝐼})𝐽”⟩)”⟩) = (𝑀‘⟨“𝐼∪ ({𝐾, 𝐿} ∖ {𝐼})𝐽”⟩))
93	6	ad2antrr 723	. . . . . 6 ⊢ (((𝜑 ∧ 𝐼 ∈ {𝐾, 𝐿}) ∧ ¬ 𝐽 ∈ {𝐾, 𝐿}) → 𝐸 = (𝑀‘⟨“𝐼𝐽”⟩))
94		en2eleq 9764	. . . . . . . . 9 ⊢ ((𝐼 ∈ {𝐾, 𝐿} ∧ {𝐾, 𝐿} ≈ 2o) → {𝐾, 𝐿} = {𝐼, ∪ ({𝐾, 𝐿} ∖ {𝐼})})
95	67, 70, 94	syl2anc 584	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝐼 ∈ {𝐾, 𝐿}) ∧ ¬ 𝐽 ∈ {𝐾, 𝐿}) → {𝐾, 𝐿} = {𝐼, ∪ ({𝐾, 𝐿} ∖ {𝐼})})
96	95	fveq2d 6778	. . . . . . 7 ⊢ (((𝜑 ∧ 𝐼 ∈ {𝐾, 𝐿}) ∧ ¬ 𝐽 ∈ {𝐾, 𝐿}) → ((pmTrsp‘𝐷)‘{𝐾, 𝐿}) = ((pmTrsp‘𝐷)‘{𝐼, ∪ ({𝐾, 𝐿} ∖ {𝐼})}))
97	15, 31	eqtrd 2778	. . . . . . . 8 ⊢ (𝜑 → 𝐹 = ((pmTrsp‘𝐷)‘{𝐾, 𝐿}))
98	97	ad2antrr 723	. . . . . . 7 ⊢ (((𝜑 ∧ 𝐼 ∈ {𝐾, 𝐿}) ∧ ¬ 𝐽 ∈ {𝐾, 𝐿}) → 𝐹 = ((pmTrsp‘𝐷)‘{𝐾, 𝐿}))
99	7, 63, 64, 73, 77, 27	cycpm2tr 31386	. . . . . . 7 ⊢ (((𝜑 ∧ 𝐼 ∈ {𝐾, 𝐿}) ∧ ¬ 𝐽 ∈ {𝐾, 𝐿}) → (𝑀‘⟨“𝐼∪ ({𝐾, 𝐿} ∖ {𝐼})”⟩) = ((pmTrsp‘𝐷)‘{𝐼, ∪ ({𝐾, 𝐿} ∖ {𝐼})}))
100	96, 98, 99	3eqtr4d 2788	. . . . . 6 ⊢ (((𝜑 ∧ 𝐼 ∈ {𝐾, 𝐿}) ∧ ¬ 𝐽 ∈ {𝐾, 𝐿}) → 𝐹 = (𝑀‘⟨“𝐼∪ ({𝐾, 𝐿} ∖ {𝐼})”⟩))
101	93, 100	oveq12d 7293	. . . . 5 ⊢ (((𝜑 ∧ 𝐼 ∈ {𝐾, 𝐿}) ∧ ¬ 𝐽 ∈ {𝐾, 𝐿}) → (𝐸 · 𝐹) = ((𝑀‘⟨“𝐼𝐽”⟩) · (𝑀‘⟨“𝐼∪ ({𝐾, 𝐿} ∖ {𝐼})”⟩)))
102	89, 92, 101	3eqtr4rd 2789	. . . 4 ⊢ (((𝜑 ∧ 𝐼 ∈ {𝐾, 𝐿}) ∧ ¬ 𝐽 ∈ {𝐾, 𝐿}) → (𝐸 · 𝐹) = (𝑆 Σg ⟨“(𝑀‘⟨“𝐼∪ ({𝐾, 𝐿} ∖ {𝐼})𝐽”⟩)”⟩))
103	85, 88, 102	rspcedvd 3563	. . 3 ⊢ (((𝜑 ∧ 𝐼 ∈ {𝐾, 𝐿}) ∧ ¬ 𝐽 ∈ {𝐾, 𝐿}) → ∃𝑐 ∈ Word 𝐶(𝐸 · 𝐹) = (𝑆 Σg 𝑐))
104	62, 103	pm2.61dan 810	. 2 ⊢ ((𝜑 ∧ 𝐼 ∈ {𝐾, 𝐿}) → ∃𝑐 ∈ Word 𝐶(𝐸 · 𝐹) = (𝑆 Σg 𝑐))
105	8	ad2antrr 723	. . . . . . 7 ⊢ (((𝜑 ∧ ¬ 𝐼 ∈ {𝐾, 𝐿}) ∧ 𝐽 ∈ {𝐾, 𝐿}) → 𝐷 ∈ 𝑉)
106	10	ad2antrr 723	. . . . . . 7 ⊢ (((𝜑 ∧ ¬ 𝐼 ∈ {𝐾, 𝐿}) ∧ 𝐽 ∈ {𝐾, 𝐿}) → 𝐽 ∈ 𝐷)
107	65	ad2antrr 723	. . . . . . . 8 ⊢ (((𝜑 ∧ ¬ 𝐼 ∈ {𝐾, 𝐿}) ∧ 𝐽 ∈ {𝐾, 𝐿}) → {𝐾, 𝐿} ⊆ 𝐷)
108		simpr 485	. . . . . . . . 9 ⊢ (((𝜑 ∧ ¬ 𝐼 ∈ {𝐾, 𝐿}) ∧ 𝐽 ∈ {𝐾, 𝐿}) → 𝐽 ∈ {𝐾, 𝐿})
109	69	ad2antrr 723	. . . . . . . . 9 ⊢ (((𝜑 ∧ ¬ 𝐼 ∈ {𝐾, 𝐿}) ∧ 𝐽 ∈ {𝐾, 𝐿}) → {𝐾, 𝐿} ≈ 2o)
110		unidifsnel 30883	. . . . . . . . 9 ⊢ ((𝐽 ∈ {𝐾, 𝐿} ∧ {𝐾, 𝐿} ≈ 2o) → ∪ ({𝐾, 𝐿} ∖ {𝐽}) ∈ {𝐾, 𝐿})
111	108, 109, 110	syl2anc 584	. . . . . . . 8 ⊢ (((𝜑 ∧ ¬ 𝐼 ∈ {𝐾, 𝐿}) ∧ 𝐽 ∈ {𝐾, 𝐿}) → ∪ ({𝐾, 𝐿} ∖ {𝐽}) ∈ {𝐾, 𝐿})
112	107, 111	sseldd 3922	. . . . . . 7 ⊢ (((𝜑 ∧ ¬ 𝐼 ∈ {𝐾, 𝐿}) ∧ 𝐽 ∈ {𝐾, 𝐿}) → ∪ ({𝐾, 𝐿} ∖ {𝐽}) ∈ 𝐷)
113	9	ad2antrr 723	. . . . . . 7 ⊢ (((𝜑 ∧ ¬ 𝐼 ∈ {𝐾, 𝐿}) ∧ 𝐽 ∈ {𝐾, 𝐿}) → 𝐼 ∈ 𝐷)
114		unidifsnne 30884	. . . . . . . . 9 ⊢ ((𝐽 ∈ {𝐾, 𝐿} ∧ {𝐾, 𝐿} ≈ 2o) → ∪ ({𝐾, 𝐿} ∖ {𝐽}) ≠ 𝐽)
115	108, 109, 114	syl2anc 584	. . . . . . . 8 ⊢ (((𝜑 ∧ ¬ 𝐼 ∈ {𝐾, 𝐿}) ∧ 𝐽 ∈ {𝐾, 𝐿}) → ∪ ({𝐾, 𝐿} ∖ {𝐽}) ≠ 𝐽)
116	115	necomd 2999	. . . . . . 7 ⊢ (((𝜑 ∧ ¬ 𝐼 ∈ {𝐾, 𝐿}) ∧ 𝐽 ∈ {𝐾, 𝐿}) → 𝐽 ≠ ∪ ({𝐾, 𝐿} ∖ {𝐽}))
117		simplr 766	. . . . . . . 8 ⊢ (((𝜑 ∧ ¬ 𝐼 ∈ {𝐾, 𝐿}) ∧ 𝐽 ∈ {𝐾, 𝐿}) → ¬ 𝐼 ∈ {𝐾, 𝐿})
118		nelne2 3042	. . . . . . . 8 ⊢ ((∪ ({𝐾, 𝐿} ∖ {𝐽}) ∈ {𝐾, 𝐿} ∧ ¬ 𝐼 ∈ {𝐾, 𝐿}) → ∪ ({𝐾, 𝐿} ∖ {𝐽}) ≠ 𝐼)
119	111, 117, 118	syl2anc 584	. . . . . . 7 ⊢ (((𝜑 ∧ ¬ 𝐼 ∈ {𝐾, 𝐿}) ∧ 𝐽 ∈ {𝐾, 𝐿}) → ∪ ({𝐾, 𝐿} ∖ {𝐽}) ≠ 𝐼)
120	11	ad2antrr 723	. . . . . . 7 ⊢ (((𝜑 ∧ ¬ 𝐼 ∈ {𝐾, 𝐿}) ∧ 𝐽 ∈ {𝐾, 𝐿}) → 𝐼 ≠ 𝐽)
121	7, 12, 105, 106, 112, 113, 116, 119, 120	cycpm3cl2 31403	. . . . . 6 ⊢ (((𝜑 ∧ ¬ 𝐼 ∈ {𝐾, 𝐿}) ∧ 𝐽 ∈ {𝐾, 𝐿}) → (𝑀‘⟨“𝐽∪ ({𝐾, 𝐿} ∖ {𝐽})𝐼”⟩) ∈ (𝑀 “ (◡♯ “ {3})))
122	121, 83	eleqtrrdi 2850	. . . . 5 ⊢ (((𝜑 ∧ ¬ 𝐼 ∈ {𝐾, 𝐿}) ∧ 𝐽 ∈ {𝐾, 𝐿}) → (𝑀‘⟨“𝐽∪ ({𝐾, 𝐿} ∖ {𝐽})𝐼”⟩) ∈ 𝐶)
123	122	s1cld 14308	. . . 4 ⊢ (((𝜑 ∧ ¬ 𝐼 ∈ {𝐾, 𝐿}) ∧ 𝐽 ∈ {𝐾, 𝐿}) → ⟨“(𝑀‘⟨“𝐽∪ ({𝐾, 𝐿} ∖ {𝐽})𝐼”⟩)”⟩ ∈ Word 𝐶)
124		simpr 485	. . . . . 6 ⊢ ((((𝜑 ∧ ¬ 𝐼 ∈ {𝐾, 𝐿}) ∧ 𝐽 ∈ {𝐾, 𝐿}) ∧ 𝑐 = ⟨“(𝑀‘⟨“𝐽∪ ({𝐾, 𝐿} ∖ {𝐽})𝐼”⟩)”⟩) → 𝑐 = ⟨“(𝑀‘⟨“𝐽∪ ({𝐾, 𝐿} ∖ {𝐽})𝐼”⟩)”⟩)
125	124	oveq2d 7291	. . . . 5 ⊢ ((((𝜑 ∧ ¬ 𝐼 ∈ {𝐾, 𝐿}) ∧ 𝐽 ∈ {𝐾, 𝐿}) ∧ 𝑐 = ⟨“(𝑀‘⟨“𝐽∪ ({𝐾, 𝐿} ∖ {𝐽})𝐼”⟩)”⟩) → (𝑆 Σg 𝑐) = (𝑆 Σg ⟨“(𝑀‘⟨“𝐽∪ ({𝐾, 𝐿} ∖ {𝐽})𝐼”⟩)”⟩))
126	125	eqeq2d 2749	. . . 4 ⊢ ((((𝜑 ∧ ¬ 𝐼 ∈ {𝐾, 𝐿}) ∧ 𝐽 ∈ {𝐾, 𝐿}) ∧ 𝑐 = ⟨“(𝑀‘⟨“𝐽∪ ({𝐾, 𝐿} ∖ {𝐽})𝐼”⟩)”⟩) → ((𝐸 · 𝐹) = (𝑆 Σg 𝑐) ↔ (𝐸 · 𝐹) = (𝑆 Σg ⟨“(𝑀‘⟨“𝐽∪ ({𝐾, 𝐿} ∖ {𝐽})𝐼”⟩)”⟩)))
127	7, 12, 105, 106, 112, 113, 116, 119, 120, 22	cyc3co2 31407	. . . . 5 ⊢ (((𝜑 ∧ ¬ 𝐼 ∈ {𝐾, 𝐿}) ∧ 𝐽 ∈ {𝐾, 𝐿}) → (𝑀‘⟨“𝐽∪ ({𝐾, 𝐿} ∖ {𝐽})𝐼”⟩) = ((𝑀‘⟨“𝐽𝐼”⟩) · (𝑀‘⟨“𝐽∪ ({𝐾, 𝐿} ∖ {𝐽})”⟩)))
128	7, 12, 105, 106, 112, 113, 116, 119, 120	cycpm3cl 31402	. . . . . 6 ⊢ (((𝜑 ∧ ¬ 𝐼 ∈ {𝐾, 𝐿}) ∧ 𝐽 ∈ {𝐾, 𝐿}) → (𝑀‘⟨“𝐽∪ ({𝐾, 𝐿} ∖ {𝐽})𝐼”⟩) ∈ (Base‘𝑆))
129	21	gsumws1 18476	. . . . . 6 ⊢ ((𝑀‘⟨“𝐽∪ ({𝐾, 𝐿} ∖ {𝐽})𝐼”⟩) ∈ (Base‘𝑆) → (𝑆 Σg ⟨“(𝑀‘⟨“𝐽∪ ({𝐾, 𝐿} ∖ {𝐽})𝐼”⟩)”⟩) = (𝑀‘⟨“𝐽∪ ({𝐾, 𝐿} ∖ {𝐽})𝐼”⟩))
130	128, 129	syl 17	. . . . 5 ⊢ (((𝜑 ∧ ¬ 𝐼 ∈ {𝐾, 𝐿}) ∧ 𝐽 ∈ {𝐾, 𝐿}) → (𝑆 Σg ⟨“(𝑀‘⟨“𝐽∪ ({𝐾, 𝐿} ∖ {𝐽})𝐼”⟩)”⟩) = (𝑀‘⟨“𝐽∪ ({𝐾, 𝐿} ∖ {𝐽})𝐼”⟩))
131		prcom 4668	. . . . . . . . . 10 ⊢ {𝐼, 𝐽} = {𝐽, 𝐼}
132	131	fveq2i 6777	. . . . . . . . 9 ⊢ ((pmTrsp‘𝐷)‘{𝐼, 𝐽}) = ((pmTrsp‘𝐷)‘{𝐽, 𝐼})
133	7, 8, 10, 9, 80, 27	cycpm2tr 31386	. . . . . . . . 9 ⊢ (𝜑 → (𝑀‘⟨“𝐽𝐼”⟩) = ((pmTrsp‘𝐷)‘{𝐽, 𝐼}))
134	132, 28, 133	3eqtr4a 2804	. . . . . . . 8 ⊢ (𝜑 → (𝑀‘⟨“𝐼𝐽”⟩) = (𝑀‘⟨“𝐽𝐼”⟩))
135	6, 134	eqtrd 2778	. . . . . . 7 ⊢ (𝜑 → 𝐸 = (𝑀‘⟨“𝐽𝐼”⟩))
136	135	ad2antrr 723	. . . . . 6 ⊢ (((𝜑 ∧ ¬ 𝐼 ∈ {𝐾, 𝐿}) ∧ 𝐽 ∈ {𝐾, 𝐿}) → 𝐸 = (𝑀‘⟨“𝐽𝐼”⟩))
137		en2eleq 9764	. . . . . . . . 9 ⊢ ((𝐽 ∈ {𝐾, 𝐿} ∧ {𝐾, 𝐿} ≈ 2o) → {𝐾, 𝐿} = {𝐽, ∪ ({𝐾, 𝐿} ∖ {𝐽})})
138	108, 109, 137	syl2anc 584	. . . . . . . 8 ⊢ (((𝜑 ∧ ¬ 𝐼 ∈ {𝐾, 𝐿}) ∧ 𝐽 ∈ {𝐾, 𝐿}) → {𝐾, 𝐿} = {𝐽, ∪ ({𝐾, 𝐿} ∖ {𝐽})})
139	138	fveq2d 6778	. . . . . . 7 ⊢ (((𝜑 ∧ ¬ 𝐼 ∈ {𝐾, 𝐿}) ∧ 𝐽 ∈ {𝐾, 𝐿}) → ((pmTrsp‘𝐷)‘{𝐾, 𝐿}) = ((pmTrsp‘𝐷)‘{𝐽, ∪ ({𝐾, 𝐿} ∖ {𝐽})}))
140	97	ad2antrr 723	. . . . . . 7 ⊢ (((𝜑 ∧ ¬ 𝐼 ∈ {𝐾, 𝐿}) ∧ 𝐽 ∈ {𝐾, 𝐿}) → 𝐹 = ((pmTrsp‘𝐷)‘{𝐾, 𝐿}))
141	7, 105, 106, 112, 116, 27	cycpm2tr 31386	. . . . . . 7 ⊢ (((𝜑 ∧ ¬ 𝐼 ∈ {𝐾, 𝐿}) ∧ 𝐽 ∈ {𝐾, 𝐿}) → (𝑀‘⟨“𝐽∪ ({𝐾, 𝐿} ∖ {𝐽})”⟩) = ((pmTrsp‘𝐷)‘{𝐽, ∪ ({𝐾, 𝐿} ∖ {𝐽})}))
142	139, 140, 141	3eqtr4d 2788	. . . . . 6 ⊢ (((𝜑 ∧ ¬ 𝐼 ∈ {𝐾, 𝐿}) ∧ 𝐽 ∈ {𝐾, 𝐿}) → 𝐹 = (𝑀‘⟨“𝐽∪ ({𝐾, 𝐿} ∖ {𝐽})”⟩))
143	136, 142	oveq12d 7293	. . . . 5 ⊢ (((𝜑 ∧ ¬ 𝐼 ∈ {𝐾, 𝐿}) ∧ 𝐽 ∈ {𝐾, 𝐿}) → (𝐸 · 𝐹) = ((𝑀‘⟨“𝐽𝐼”⟩) · (𝑀‘⟨“𝐽∪ ({𝐾, 𝐿} ∖ {𝐽})”⟩)))
144	127, 130, 143	3eqtr4rd 2789	. . . 4 ⊢ (((𝜑 ∧ ¬ 𝐼 ∈ {𝐾, 𝐿}) ∧ 𝐽 ∈ {𝐾, 𝐿}) → (𝐸 · 𝐹) = (𝑆 Σg ⟨“(𝑀‘⟨“𝐽∪ ({𝐾, 𝐿} ∖ {𝐽})𝐼”⟩)”⟩))
145	123, 126, 144	rspcedvd 3563	. . 3 ⊢ (((𝜑 ∧ ¬ 𝐼 ∈ {𝐾, 𝐿}) ∧ 𝐽 ∈ {𝐾, 𝐿}) → ∃𝑐 ∈ Word 𝐶(𝐸 · 𝐹) = (𝑆 Σg 𝑐))
146	8	ad2antrr 723	. . . . . . 7 ⊢ (((𝜑 ∧ ¬ 𝐼 ∈ {𝐾, 𝐿}) ∧ ¬ 𝐽 ∈ {𝐾, 𝐿}) → 𝐷 ∈ 𝑉)
147	10	ad2antrr 723	. . . . . . 7 ⊢ (((𝜑 ∧ ¬ 𝐼 ∈ {𝐾, 𝐿}) ∧ ¬ 𝐽 ∈ {𝐾, 𝐿}) → 𝐽 ∈ 𝐷)
148	16	ad2antrr 723	. . . . . . 7 ⊢ (((𝜑 ∧ ¬ 𝐼 ∈ {𝐾, 𝐿}) ∧ ¬ 𝐽 ∈ {𝐾, 𝐿}) → 𝐾 ∈ 𝐷)
149	9	ad2antrr 723	. . . . . . 7 ⊢ (((𝜑 ∧ ¬ 𝐼 ∈ {𝐾, 𝐿}) ∧ ¬ 𝐽 ∈ {𝐾, 𝐿}) → 𝐼 ∈ 𝐷)
150		simpr 485	. . . . . . . 8 ⊢ (((𝜑 ∧ ¬ 𝐼 ∈ {𝐾, 𝐿}) ∧ ¬ 𝐽 ∈ {𝐾, 𝐿}) → ¬ 𝐽 ∈ {𝐾, 𝐿})
151	147, 150	nelpr1 4589	. . . . . . 7 ⊢ (((𝜑 ∧ ¬ 𝐼 ∈ {𝐾, 𝐿}) ∧ ¬ 𝐽 ∈ {𝐾, 𝐿}) → 𝐽 ≠ 𝐾)
152		prid1g 4696	. . . . . . . . . 10 ⊢ (𝐾 ∈ 𝐷 → 𝐾 ∈ {𝐾, 𝐿})
153	16, 152	syl 17	. . . . . . . . 9 ⊢ (𝜑 → 𝐾 ∈ {𝐾, 𝐿})
154	153	ad2antrr 723	. . . . . . . 8 ⊢ (((𝜑 ∧ ¬ 𝐼 ∈ {𝐾, 𝐿}) ∧ ¬ 𝐽 ∈ {𝐾, 𝐿}) → 𝐾 ∈ {𝐾, 𝐿})
155		simplr 766	. . . . . . . 8 ⊢ (((𝜑 ∧ ¬ 𝐼 ∈ {𝐾, 𝐿}) ∧ ¬ 𝐽 ∈ {𝐾, 𝐿}) → ¬ 𝐼 ∈ {𝐾, 𝐿})
156		nelne2 3042	. . . . . . . 8 ⊢ ((𝐾 ∈ {𝐾, 𝐿} ∧ ¬ 𝐼 ∈ {𝐾, 𝐿}) → 𝐾 ≠ 𝐼)
157	154, 155, 156	syl2anc 584	. . . . . . 7 ⊢ (((𝜑 ∧ ¬ 𝐼 ∈ {𝐾, 𝐿}) ∧ ¬ 𝐽 ∈ {𝐾, 𝐿}) → 𝐾 ≠ 𝐼)
158	11	ad2antrr 723	. . . . . . 7 ⊢ (((𝜑 ∧ ¬ 𝐼 ∈ {𝐾, 𝐿}) ∧ ¬ 𝐽 ∈ {𝐾, 𝐿}) → 𝐼 ≠ 𝐽)
159	7, 12, 146, 147, 148, 149, 151, 157, 158	cycpm3cl2 31403	. . . . . 6 ⊢ (((𝜑 ∧ ¬ 𝐼 ∈ {𝐾, 𝐿}) ∧ ¬ 𝐽 ∈ {𝐾, 𝐿}) → (𝑀‘⟨“𝐽𝐾𝐼”⟩) ∈ (𝑀 “ (◡♯ “ {3})))
160	159, 83	eleqtrrdi 2850	. . . . 5 ⊢ (((𝜑 ∧ ¬ 𝐼 ∈ {𝐾, 𝐿}) ∧ ¬ 𝐽 ∈ {𝐾, 𝐿}) → (𝑀‘⟨“𝐽𝐾𝐼”⟩) ∈ 𝐶)
161	17	ad2antrr 723	. . . . . . 7 ⊢ (((𝜑 ∧ ¬ 𝐼 ∈ {𝐾, 𝐿}) ∧ ¬ 𝐽 ∈ {𝐾, 𝐿}) → 𝐿 ∈ 𝐷)
162	18	ad2antrr 723	. . . . . . 7 ⊢ (((𝜑 ∧ ¬ 𝐼 ∈ {𝐾, 𝐿}) ∧ ¬ 𝐽 ∈ {𝐾, 𝐿}) → 𝐾 ≠ 𝐿)
163		prid2g 4697	. . . . . . . . 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 31403	. . . . . 6 ⊢ (((𝜑 ∧ ¬ 𝐼 ∈ {𝐾, 𝐿}) ∧ ¬ 𝐽 ∈ {𝐾, 𝐿}) → (𝑀‘⟨“𝐾𝐿𝐽”⟩) ∈ (𝑀 “ (◡♯ “ {3})))
168	167, 83	eleqtrrdi 2850	. . . . 5 ⊢ (((𝜑 ∧ ¬ 𝐼 ∈ {𝐾, 𝐿}) ∧ ¬ 𝐽 ∈ {𝐾, 𝐿}) → (𝑀‘⟨“𝐾𝐿𝐽”⟩) ∈ 𝐶)
169	160, 168	s2cld 14584	. . . 4 ⊢ (((𝜑 ∧ ¬ 𝐼 ∈ {𝐾, 𝐿}) ∧ ¬ 𝐽 ∈ {𝐾, 𝐿}) → ⟨“(𝑀‘⟨“𝐽𝐾𝐼”⟩)(𝑀‘⟨“𝐾𝐿𝐽”⟩)”⟩ ∈ Word 𝐶)
170		simpr 485	. . . . . 6 ⊢ ((((𝜑 ∧ ¬ 𝐼 ∈ {𝐾, 𝐿}) ∧ ¬ 𝐽 ∈ {𝐾, 𝐿}) ∧ 𝑐 = ⟨“(𝑀‘⟨“𝐽𝐾𝐼”⟩)(𝑀‘⟨“𝐾𝐿𝐽”⟩)”⟩) → 𝑐 = ⟨“(𝑀‘⟨“𝐽𝐾𝐼”⟩)(𝑀‘⟨“𝐾𝐿𝐽”⟩)”⟩)
171	170	oveq2d 7291	. . . . 5 ⊢ ((((𝜑 ∧ ¬ 𝐼 ∈ {𝐾, 𝐿}) ∧ ¬ 𝐽 ∈ {𝐾, 𝐿}) ∧ 𝑐 = ⟨“(𝑀‘⟨“𝐽𝐾𝐼”⟩)(𝑀‘⟨“𝐾𝐿𝐽”⟩)”⟩) → (𝑆 Σg 𝑐) = (𝑆 Σg ⟨“(𝑀‘⟨“𝐽𝐾𝐼”⟩)(𝑀‘⟨“𝐾𝐿𝐽”⟩)”⟩))
172	171	eqeq2d 2749	. . . 4 ⊢ ((((𝜑 ∧ ¬ 𝐼 ∈ {𝐾, 𝐿}) ∧ ¬ 𝐽 ∈ {𝐾, 𝐿}) ∧ 𝑐 = ⟨“(𝑀‘⟨“𝐽𝐾𝐼”⟩)(𝑀‘⟨“𝐾𝐿𝐽”⟩)”⟩) → ((𝐸 · 𝐹) = (𝑆 Σg 𝑐) ↔ (𝐸 · 𝐹) = (𝑆 Σg ⟨“(𝑀‘⟨“𝐽𝐾𝐼”⟩)(𝑀‘⟨“𝐾𝐿𝐽”⟩)”⟩)))
173	146, 56	syl 17	. . . . . . . . . 10 ⊢ (((𝜑 ∧ ¬ 𝐼 ∈ {𝐾, 𝐿}) ∧ ¬ 𝐽 ∈ {𝐾, 𝐿}) → ( I ↾ 𝐷) = (0g‘𝑆))
174	173	oveq1d 7290	. . . . . . . . 9 ⊢ (((𝜑 ∧ ¬ 𝐼 ∈ {𝐾, 𝐿}) ∧ ¬ 𝐽 ∈ {𝐾, 𝐿}) → (( I ↾ 𝐷) · (𝑀‘⟨“𝐾𝐿”⟩)) = ((0g‘𝑆) · (𝑀‘⟨“𝐾𝐿”⟩)))
175	12	symggrp 19008	. . . . . . . . . . . 12 ⊢ (𝐷 ∈ 𝑉 → 𝑆 ∈ Grp)
176	8, 175	syl 17	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑆 ∈ Grp)
177	176	ad2antrr 723	. . . . . . . . . 10 ⊢ (((𝜑 ∧ ¬ 𝐼 ∈ {𝐾, 𝐿}) ∧ ¬ 𝐽 ∈ {𝐾, 𝐿}) → 𝑆 ∈ Grp)
178	19	ad2antrr 723	. . . . . . . . . 10 ⊢ (((𝜑 ∧ ¬ 𝐼 ∈ {𝐾, 𝐿}) ∧ ¬ 𝐽 ∈ {𝐾, 𝐿}) → (𝑀‘⟨“𝐾𝐿”⟩) ∈ (Base‘𝑆))
179	21, 22, 58	grplid 18609	. . . . . . . . . 10 ⊢ ((𝑆 ∈ Grp ∧ (𝑀‘⟨“𝐾𝐿”⟩) ∈ (Base‘𝑆)) → ((0g‘𝑆) · (𝑀‘⟨“𝐾𝐿”⟩)) = (𝑀‘⟨“𝐾𝐿”⟩))
180	177, 178, 179	syl2anc 584	. . . . . . . . 9 ⊢ (((𝜑 ∧ ¬ 𝐼 ∈ {𝐾, 𝐿}) ∧ ¬ 𝐽 ∈ {𝐾, 𝐿}) → ((0g‘𝑆) · (𝑀‘⟨“𝐾𝐿”⟩)) = (𝑀‘⟨“𝐾𝐿”⟩))
181	174, 180	eqtrd 2778	. . . . . . . 8 ⊢ (((𝜑 ∧ ¬ 𝐼 ∈ {𝐾, 𝐿}) ∧ ¬ 𝐽 ∈ {𝐾, 𝐿}) → (( I ↾ 𝐷) · (𝑀‘⟨“𝐾𝐿”⟩)) = (𝑀‘⟨“𝐾𝐿”⟩))
182	181	oveq2d 7291	. . . . . . 7 ⊢ (((𝜑 ∧ ¬ 𝐼 ∈ {𝐾, 𝐿}) ∧ ¬ 𝐽 ∈ {𝐾, 𝐿}) → ((𝑀‘⟨“𝐼𝐽”⟩) · (( I ↾ 𝐷) · (𝑀‘⟨“𝐾𝐿”⟩))) = ((𝑀‘⟨“𝐼𝐽”⟩) · (𝑀‘⟨“𝐾𝐿”⟩)))
183	13	ad2antrr 723	. . . . . . . . 9 ⊢ (((𝜑 ∧ ¬ 𝐼 ∈ {𝐾, 𝐿}) ∧ ¬ 𝐽 ∈ {𝐾, 𝐿}) → (𝑀‘⟨“𝐼𝐽”⟩) ∈ (Base‘𝑆))
184	7, 146, 147, 148, 151, 27	cycpm2tr 31386	. . . . . . . . . 10 ⊢ (((𝜑 ∧ ¬ 𝐼 ∈ {𝐾, 𝐿}) ∧ ¬ 𝐽 ∈ {𝐾, 𝐿}) → (𝑀‘⟨“𝐽𝐾”⟩) = ((pmTrsp‘𝐷)‘{𝐽, 𝐾}))
185	50, 12, 21	symgtrf 19077	. . . . . . . . . . 11 ⊢ ran (pmTrsp‘𝐷) ⊆ (Base‘𝑆)
186	10, 16	prssd 4755	. . . . . . . . . . . . 13 ⊢ (𝜑 → {𝐽, 𝐾} ⊆ 𝐷)
187	186	ad2antrr 723	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ ¬ 𝐼 ∈ {𝐾, 𝐿}) ∧ ¬ 𝐽 ∈ {𝐾, 𝐿}) → {𝐽, 𝐾} ⊆ 𝐷)
188		pr2nelem 9760	. . . . . . . . . . . . 13 ⊢ ((𝐽 ∈ 𝐷 ∧ 𝐾 ∈ 𝐷 ∧ 𝐽 ≠ 𝐾) → {𝐽, 𝐾} ≈ 2o)
189	147, 148, 151, 188	syl3anc 1370	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ ¬ 𝐼 ∈ {𝐾, 𝐿}) ∧ ¬ 𝐽 ∈ {𝐾, 𝐿}) → {𝐽, 𝐾} ≈ 2o)
190	27, 50	pmtrrn 19065	. . . . . . . . . . . 12 ⊢ ((𝐷 ∈ 𝑉 ∧ {𝐽, 𝐾} ⊆ 𝐷 ∧ {𝐽, 𝐾} ≈ 2o) → ((pmTrsp‘𝐷)‘{𝐽, 𝐾}) ∈ ran (pmTrsp‘𝐷))
191	146, 187, 189, 190	syl3anc 1370	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ ¬ 𝐼 ∈ {𝐾, 𝐿}) ∧ ¬ 𝐽 ∈ {𝐾, 𝐿}) → ((pmTrsp‘𝐷)‘{𝐽, 𝐾}) ∈ ran (pmTrsp‘𝐷))
192	185, 191	sselid 3919	. . . . . . . . . 10 ⊢ (((𝜑 ∧ ¬ 𝐼 ∈ {𝐾, 𝐿}) ∧ ¬ 𝐽 ∈ {𝐾, 𝐿}) → ((pmTrsp‘𝐷)‘{𝐽, 𝐾}) ∈ (Base‘𝑆))
193	184, 192	eqeltrd 2839	. . . . . . . . 9 ⊢ (((𝜑 ∧ ¬ 𝐼 ∈ {𝐾, 𝐿}) ∧ ¬ 𝐽 ∈ {𝐾, 𝐿}) → (𝑀‘⟨“𝐽𝐾”⟩) ∈ (Base‘𝑆))
194	151	necomd 2999	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ ¬ 𝐼 ∈ {𝐾, 𝐿}) ∧ ¬ 𝐽 ∈ {𝐾, 𝐿}) → 𝐾 ≠ 𝐽)
195	7, 146, 148, 147, 194, 27	cycpm2tr 31386	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ ¬ 𝐼 ∈ {𝐾, 𝐿}) ∧ ¬ 𝐽 ∈ {𝐾, 𝐿}) → (𝑀‘⟨“𝐾𝐽”⟩) = ((pmTrsp‘𝐷)‘{𝐾, 𝐽}))
196		prcom 4668	. . . . . . . . . . . . . 14 ⊢ {𝐽, 𝐾} = {𝐾, 𝐽}
197	196	a1i 11	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ ¬ 𝐼 ∈ {𝐾, 𝐿}) ∧ ¬ 𝐽 ∈ {𝐾, 𝐿}) → {𝐽, 𝐾} = {𝐾, 𝐽})
198	197	fveq2d 6778	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ ¬ 𝐼 ∈ {𝐾, 𝐿}) ∧ ¬ 𝐽 ∈ {𝐾, 𝐿}) → ((pmTrsp‘𝐷)‘{𝐽, 𝐾}) = ((pmTrsp‘𝐷)‘{𝐾, 𝐽}))
199	195, 198	eqtr4d 2781	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ ¬ 𝐼 ∈ {𝐾, 𝐿}) ∧ ¬ 𝐽 ∈ {𝐾, 𝐿}) → (𝑀‘⟨“𝐾𝐽”⟩) = ((pmTrsp‘𝐷)‘{𝐽, 𝐾}))
200	199, 192	eqeltrd 2839	. . . . . . . . . 10 ⊢ (((𝜑 ∧ ¬ 𝐼 ∈ {𝐾, 𝐿}) ∧ ¬ 𝐽 ∈ {𝐾, 𝐿}) → (𝑀‘⟨“𝐾𝐽”⟩) ∈ (Base‘𝑆))
201	21, 22	grpcl 18585	. . . . . . . . . 10 ⊢ ((𝑆 ∈ Grp ∧ (𝑀‘⟨“𝐾𝐽”⟩) ∈ (Base‘𝑆) ∧ (𝑀‘⟨“𝐾𝐿”⟩) ∈ (Base‘𝑆)) → ((𝑀‘⟨“𝐾𝐽”⟩) · (𝑀‘⟨“𝐾𝐿”⟩)) ∈ (Base‘𝑆))
202	177, 200, 178, 201	syl3anc 1370	. . . . . . . . 9 ⊢ (((𝜑 ∧ ¬ 𝐼 ∈ {𝐾, 𝐿}) ∧ ¬ 𝐽 ∈ {𝐾, 𝐿}) → ((𝑀‘⟨“𝐾𝐽”⟩) · (𝑀‘⟨“𝐾𝐿”⟩)) ∈ (Base‘𝑆))
203	21, 22	grpass 18586	. . . . . . . . 9 ⊢ ((𝑆 ∈ Grp ∧ ((𝑀‘⟨“𝐼𝐽”⟩) ∈ (Base‘𝑆) ∧ (𝑀‘⟨“𝐽𝐾”⟩) ∈ (Base‘𝑆) ∧ ((𝑀‘⟨“𝐾𝐽”⟩) · (𝑀‘⟨“𝐾𝐿”⟩)) ∈ (Base‘𝑆))) → (((𝑀‘⟨“𝐼𝐽”⟩) · (𝑀‘⟨“𝐽𝐾”⟩)) · ((𝑀‘⟨“𝐾𝐽”⟩) · (𝑀‘⟨“𝐾𝐿”⟩))) = ((𝑀‘⟨“𝐼𝐽”⟩) · ((𝑀‘⟨“𝐽𝐾”⟩) · ((𝑀‘⟨“𝐾𝐽”⟩) · (𝑀‘⟨“𝐾𝐿”⟩)))))
204	177, 183, 193, 202, 203	syl13anc 1371	. . . . . . . 8 ⊢ (((𝜑 ∧ ¬ 𝐼 ∈ {𝐾, 𝐿}) ∧ ¬ 𝐽 ∈ {𝐾, 𝐿}) → (((𝑀‘⟨“𝐼𝐽”⟩) · (𝑀‘⟨“𝐽𝐾”⟩)) · ((𝑀‘⟨“𝐾𝐽”⟩) · (𝑀‘⟨“𝐾𝐿”⟩))) = ((𝑀‘⟨“𝐼𝐽”⟩) · ((𝑀‘⟨“𝐽𝐾”⟩) · ((𝑀‘⟨“𝐾𝐽”⟩) · (𝑀‘⟨“𝐾𝐿”⟩)))))
205	21, 22	grpass 18586	. . . . . . . . . 10 ⊢ ((𝑆 ∈ Grp ∧ ((𝑀‘⟨“𝐽𝐾”⟩) ∈ (Base‘𝑆) ∧ (𝑀‘⟨“𝐾𝐽”⟩) ∈ (Base‘𝑆) ∧ (𝑀‘⟨“𝐾𝐿”⟩) ∈ (Base‘𝑆))) → (((𝑀‘⟨“𝐽𝐾”⟩) · (𝑀‘⟨“𝐾𝐽”⟩)) · (𝑀‘⟨“𝐾𝐿”⟩)) = ((𝑀‘⟨“𝐽𝐾”⟩) · ((𝑀‘⟨“𝐾𝐽”⟩) · (𝑀‘⟨“𝐾𝐿”⟩))))
206	177, 193, 200, 178, 205	syl13anc 1371	. . . . . . . . 9 ⊢ (((𝜑 ∧ ¬ 𝐼 ∈ {𝐾, 𝐿}) ∧ ¬ 𝐽 ∈ {𝐾, 𝐿}) → (((𝑀‘⟨“𝐽𝐾”⟩) · (𝑀‘⟨“𝐾𝐽”⟩)) · (𝑀‘⟨“𝐾𝐿”⟩)) = ((𝑀‘⟨“𝐽𝐾”⟩) · ((𝑀‘⟨“𝐾𝐽”⟩) · (𝑀‘⟨“𝐾𝐿”⟩))))
207	206	oveq2d 7291	. . . . . . . 8 ⊢ (((𝜑 ∧ ¬ 𝐼 ∈ {𝐾, 𝐿}) ∧ ¬ 𝐽 ∈ {𝐾, 𝐿}) → ((𝑀‘⟨“𝐼𝐽”⟩) · (((𝑀‘⟨“𝐽𝐾”⟩) · (𝑀‘⟨“𝐾𝐽”⟩)) · (𝑀‘⟨“𝐾𝐿”⟩))) = ((𝑀‘⟨“𝐼𝐽”⟩) · ((𝑀‘⟨“𝐽𝐾”⟩) · ((𝑀‘⟨“𝐾𝐽”⟩) · (𝑀‘⟨“𝐾𝐿”⟩)))))
208	184, 199	oveq12d 7293	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ ¬ 𝐼 ∈ {𝐾, 𝐿}) ∧ ¬ 𝐽 ∈ {𝐾, 𝐿}) → ((𝑀‘⟨“𝐽𝐾”⟩) · (𝑀‘⟨“𝐾𝐽”⟩)) = (((pmTrsp‘𝐷)‘{𝐽, 𝐾}) · ((pmTrsp‘𝐷)‘{𝐽, 𝐾})))
209	12, 21, 22	symgov 18991	. . . . . . . . . . . 12 ⊢ ((((pmTrsp‘𝐷)‘{𝐽, 𝐾}) ∈ (Base‘𝑆) ∧ ((pmTrsp‘𝐷)‘{𝐽, 𝐾}) ∈ (Base‘𝑆)) → (((pmTrsp‘𝐷)‘{𝐽, 𝐾}) · ((pmTrsp‘𝐷)‘{𝐽, 𝐾})) = (((pmTrsp‘𝐷)‘{𝐽, 𝐾}) ∘ ((pmTrsp‘𝐷)‘{𝐽, 𝐾})))
210	192, 192, 209	syl2anc 584	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ ¬ 𝐼 ∈ {𝐾, 𝐿}) ∧ ¬ 𝐽 ∈ {𝐾, 𝐿}) → (((pmTrsp‘𝐷)‘{𝐽, 𝐾}) · ((pmTrsp‘𝐷)‘{𝐽, 𝐾})) = (((pmTrsp‘𝐷)‘{𝐽, 𝐾}) ∘ ((pmTrsp‘𝐷)‘{𝐽, 𝐾})))
211	27, 50	pmtrfinv 19069	. . . . . . . . . . . 12 ⊢ (((pmTrsp‘𝐷)‘{𝐽, 𝐾}) ∈ ran (pmTrsp‘𝐷) → (((pmTrsp‘𝐷)‘{𝐽, 𝐾}) ∘ ((pmTrsp‘𝐷)‘{𝐽, 𝐾})) = ( I ↾ 𝐷))
212	191, 211	syl 17	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ ¬ 𝐼 ∈ {𝐾, 𝐿}) ∧ ¬ 𝐽 ∈ {𝐾, 𝐿}) → (((pmTrsp‘𝐷)‘{𝐽, 𝐾}) ∘ ((pmTrsp‘𝐷)‘{𝐽, 𝐾})) = ( I ↾ 𝐷))
213	208, 210, 212	3eqtrd 2782	. . . . . . . . . 10 ⊢ (((𝜑 ∧ ¬ 𝐼 ∈ {𝐾, 𝐿}) ∧ ¬ 𝐽 ∈ {𝐾, 𝐿}) → ((𝑀‘⟨“𝐽𝐾”⟩) · (𝑀‘⟨“𝐾𝐽”⟩)) = ( I ↾ 𝐷))
214	213	oveq1d 7290	. . . . . . . . 9 ⊢ (((𝜑 ∧ ¬ 𝐼 ∈ {𝐾, 𝐿}) ∧ ¬ 𝐽 ∈ {𝐾, 𝐿}) → (((𝑀‘⟨“𝐽𝐾”⟩) · (𝑀‘⟨“𝐾𝐽”⟩)) · (𝑀‘⟨“𝐾𝐿”⟩)) = (( I ↾ 𝐷) · (𝑀‘⟨“𝐾𝐿”⟩)))
215	214	oveq2d 7291	. . . . . . . 8 ⊢ (((𝜑 ∧ ¬ 𝐼 ∈ {𝐾, 𝐿}) ∧ ¬ 𝐽 ∈ {𝐾, 𝐿}) → ((𝑀‘⟨“𝐼𝐽”⟩) · (((𝑀‘⟨“𝐽𝐾”⟩) · (𝑀‘⟨“𝐾𝐽”⟩)) · (𝑀‘⟨“𝐾𝐿”⟩))) = ((𝑀‘⟨“𝐼𝐽”⟩) · (( I ↾ 𝐷) · (𝑀‘⟨“𝐾𝐿”⟩))))
216	204, 207, 215	3eqtr2rd 2785	. . . . . . 7 ⊢ (((𝜑 ∧ ¬ 𝐼 ∈ {𝐾, 𝐿}) ∧ ¬ 𝐽 ∈ {𝐾, 𝐿}) → ((𝑀‘⟨“𝐼𝐽”⟩) · (( I ↾ 𝐷) · (𝑀‘⟨“𝐾𝐿”⟩))) = (((𝑀‘⟨“𝐼𝐽”⟩) · (𝑀‘⟨“𝐽𝐾”⟩)) · ((𝑀‘⟨“𝐾𝐽”⟩) · (𝑀‘⟨“𝐾𝐿”⟩))))
217	182, 216	eqtr3d 2780	. . . . . 6 ⊢ (((𝜑 ∧ ¬ 𝐼 ∈ {𝐾, 𝐿}) ∧ ¬ 𝐽 ∈ {𝐾, 𝐿}) → ((𝑀‘⟨“𝐼𝐽”⟩) · (𝑀‘⟨“𝐾𝐿”⟩)) = (((𝑀‘⟨“𝐼𝐽”⟩) · (𝑀‘⟨“𝐽𝐾”⟩)) · ((𝑀‘⟨“𝐾𝐽”⟩) · (𝑀‘⟨“𝐾𝐿”⟩))))
218	6, 15	oveq12d 7293	. . . . . . 7 ⊢ (𝜑 → (𝐸 · 𝐹) = ((𝑀‘⟨“𝐼𝐽”⟩) · (𝑀‘⟨“𝐾𝐿”⟩)))
219	218	ad2antrr 723	. . . . . 6 ⊢ (((𝜑 ∧ ¬ 𝐼 ∈ {𝐾, 𝐿}) ∧ ¬ 𝐽 ∈ {𝐾, 𝐿}) → (𝐸 · 𝐹) = ((𝑀‘⟨“𝐼𝐽”⟩) · (𝑀‘⟨“𝐾𝐿”⟩)))
220	7, 12, 146, 147, 148, 149, 151, 157, 158, 22	cyc3co2 31407	. . . . . . . 8 ⊢ (((𝜑 ∧ ¬ 𝐼 ∈ {𝐾, 𝐿}) ∧ ¬ 𝐽 ∈ {𝐾, 𝐿}) → (𝑀‘⟨“𝐽𝐾𝐼”⟩) = ((𝑀‘⟨“𝐽𝐼”⟩) · (𝑀‘⟨“𝐽𝐾”⟩)))
221	134	oveq1d 7290	. . . . . . . . 9 ⊢ (𝜑 → ((𝑀‘⟨“𝐼𝐽”⟩) · (𝑀‘⟨“𝐽𝐾”⟩)) = ((𝑀‘⟨“𝐽𝐼”⟩) · (𝑀‘⟨“𝐽𝐾”⟩)))
222	221	ad2antrr 723	. . . . . . . 8 ⊢ (((𝜑 ∧ ¬ 𝐼 ∈ {𝐾, 𝐿}) ∧ ¬ 𝐽 ∈ {𝐾, 𝐿}) → ((𝑀‘⟨“𝐼𝐽”⟩) · (𝑀‘⟨“𝐽𝐾”⟩)) = ((𝑀‘⟨“𝐽𝐼”⟩) · (𝑀‘⟨“𝐽𝐾”⟩)))
223	220, 222	eqtr4d 2781	. . . . . . 7 ⊢ (((𝜑 ∧ ¬ 𝐼 ∈ {𝐾, 𝐿}) ∧ ¬ 𝐽 ∈ {𝐾, 𝐿}) → (𝑀‘⟨“𝐽𝐾𝐼”⟩) = ((𝑀‘⟨“𝐼𝐽”⟩) · (𝑀‘⟨“𝐽𝐾”⟩)))
224	7, 12, 146, 148, 161, 147, 162, 166, 151, 22	cyc3co2 31407	. . . . . . 7 ⊢ (((𝜑 ∧ ¬ 𝐼 ∈ {𝐾, 𝐿}) ∧ ¬ 𝐽 ∈ {𝐾, 𝐿}) → (𝑀‘⟨“𝐾𝐿𝐽”⟩) = ((𝑀‘⟨“𝐾𝐽”⟩) · (𝑀‘⟨“𝐾𝐿”⟩)))
225	223, 224	oveq12d 7293	. . . . . 6 ⊢ (((𝜑 ∧ ¬ 𝐼 ∈ {𝐾, 𝐿}) ∧ ¬ 𝐽 ∈ {𝐾, 𝐿}) → ((𝑀‘⟨“𝐽𝐾𝐼”⟩) · (𝑀‘⟨“𝐾𝐿𝐽”⟩)) = (((𝑀‘⟨“𝐼𝐽”⟩) · (𝑀‘⟨“𝐽𝐾”⟩)) · ((𝑀‘⟨“𝐾𝐽”⟩) · (𝑀‘⟨“𝐾𝐿”⟩))))
226	217, 219, 225	3eqtr4d 2788	. . . . 5 ⊢ (((𝜑 ∧ ¬ 𝐼 ∈ {𝐾, 𝐿}) ∧ ¬ 𝐽 ∈ {𝐾, 𝐿}) → (𝐸 · 𝐹) = ((𝑀‘⟨“𝐽𝐾𝐼”⟩) · (𝑀‘⟨“𝐾𝐿𝐽”⟩)))
227	176	grpmndd 18589	. . . . . . 7 ⊢ (𝜑 → 𝑆 ∈ Mnd)
228	227	ad2antrr 723	. . . . . 6 ⊢ (((𝜑 ∧ ¬ 𝐼 ∈ {𝐾, 𝐿}) ∧ ¬ 𝐽 ∈ {𝐾, 𝐿}) → 𝑆 ∈ Mnd)
229	7, 12, 146, 147, 148, 149, 151, 157, 158	cycpm3cl 31402	. . . . . 6 ⊢ (((𝜑 ∧ ¬ 𝐼 ∈ {𝐾, 𝐿}) ∧ ¬ 𝐽 ∈ {𝐾, 𝐿}) → (𝑀‘⟨“𝐽𝐾𝐼”⟩) ∈ (Base‘𝑆))
230	224, 202	eqeltrd 2839	. . . . . 6 ⊢ (((𝜑 ∧ ¬ 𝐼 ∈ {𝐾, 𝐿}) ∧ ¬ 𝐽 ∈ {𝐾, 𝐿}) → (𝑀‘⟨“𝐾𝐿𝐽”⟩) ∈ (Base‘𝑆))
231	21, 22	gsumws2 18481	. . . . . 6 ⊢ ((𝑆 ∈ Mnd ∧ (𝑀‘⟨“𝐽𝐾𝐼”⟩) ∈ (Base‘𝑆) ∧ (𝑀‘⟨“𝐾𝐿𝐽”⟩) ∈ (Base‘𝑆)) → (𝑆 Σg ⟨“(𝑀‘⟨“𝐽𝐾𝐼”⟩)(𝑀‘⟨“𝐾𝐿𝐽”⟩)”⟩) = ((𝑀‘⟨“𝐽𝐾𝐼”⟩) · (𝑀‘⟨“𝐾𝐿𝐽”⟩)))
232	228, 229, 230, 231	syl3anc 1370	. . . . 5 ⊢ (((𝜑 ∧ ¬ 𝐼 ∈ {𝐾, 𝐿}) ∧ ¬ 𝐽 ∈ {𝐾, 𝐿}) → (𝑆 Σg ⟨“(𝑀‘⟨“𝐽𝐾𝐼”⟩)(𝑀‘⟨“𝐾𝐿𝐽”⟩)”⟩) = ((𝑀‘⟨“𝐽𝐾𝐼”⟩) · (𝑀‘⟨“𝐾𝐿𝐽”⟩)))
233	226, 232	eqtr4d 2781	. . . 4 ⊢ (((𝜑 ∧ ¬ 𝐼 ∈ {𝐾, 𝐿}) ∧ ¬ 𝐽 ∈ {𝐾, 𝐿}) → (𝐸 · 𝐹) = (𝑆 Σg ⟨“(𝑀‘⟨“𝐽𝐾𝐼”⟩)(𝑀‘⟨“𝐾𝐿𝐽”⟩)”⟩))
234	169, 172, 233	rspcedvd 3563	. . 3 ⊢ (((𝜑 ∧ ¬ 𝐼 ∈ {𝐾, 𝐿}) ∧ ¬ 𝐽 ∈ {𝐾, 𝐿}) → ∃𝑐 ∈ Word 𝐶(𝐸 · 𝐹) = (𝑆 Σg 𝑐))
235	145, 234	pm2.61dan 810	. 2 ⊢ ((𝜑 ∧ ¬ 𝐼 ∈ {𝐾, 𝐿}) → ∃𝑐 ∈ Word 𝐶(𝐸 · 𝐹) = (𝑆 Σg 𝑐))
236	104, 235	pm2.61dan 810	1 ⊢ (𝜑 → ∃𝑐 ∈ Word 𝐶(𝐸 · 𝐹) = (𝑆 Σg 𝑐))

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 396   ∧ w3a 1086   = wceq 1539   ∈ wcel 2106   ≠ wne 2943  ∃wrex 3065   ∖ cdif 3884   ⊆ wss 3887  ∅c0 4256  {csn 4561  {cpr 4563  ∪ cuni 4839   class class class wbr 5074   I cid 5488  ^◡ccnv 5588  ran crn 5590   ↾ cres 5591   “ cima 5592   ∘ ccom 5593  ‘cfv 6433  (class class class)co 7275  2_oc2o 8291   ≈ cen 8730  3c3 12029  ♯chash 14044  Word cword 14217  ⟨“cs1 14300  ⟨“cs2 14554  ⟨“cs3 14555  Basecbs 16912  +_gcplusg 16962  0_gc0g 17150   Σ_g cgsu 17151  Mndcmnd 18385  Grpcgrp 18577  SymGrpcsymg 18974  pmTrspcpmtr 19049  pmEvencevpm 19098  toCycctocyc 31373

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  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 2709  ax-rep 5209  ax-sep 5223  ax-nul 5230  ax-pow 5288  ax-pr 5352  ax-un 7588  ax-reg 9351  ax-ac2 10219  ax-cnex 10927  ax-resscn 10928  ax-1cn 10929  ax-icn 10930  ax-addcl 10931  ax-addrcl 10932  ax-mulcl 10933  ax-mulrcl 10934  ax-mulcom 10935  ax-addass 10936  ax-mulass 10937  ax-distr 10938  ax-i2m1 10939  ax-1ne0 10940  ax-1rid 10941  ax-rnegex 10942  ax-rrecex 10943  ax-cnre 10944  ax-pre-lttri 10945  ax-pre-lttrn 10946  ax-pre-ltadd 10947  ax-pre-mulgt0 10948  ax-pre-sup 10949

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3or 1087  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1783  df-nf 1787  df-sb 2068  df-mo 2540  df-eu 2569  df-clab 2716  df-cleq 2730  df-clel 2816  df-nfc 2889  df-ne 2944  df-nel 3050  df-ral 3069  df-rex 3070  df-rmo 3071  df-reu 3072  df-rab 3073  df-v 3434  df-sbc 3717  df-csb 3833  df-dif 3890  df-un 3892  df-in 3894  df-ss 3904  df-pss 3906  df-nul 4257  df-if 4460  df-pw 4535  df-sn 4562  df-pr 4564  df-tp 4566  df-op 4568  df-uni 4840  df-int 4880  df-iun 4926  df-br 5075  df-opab 5137  df-mpt 5158  df-tr 5192  df-id 5489  df-eprel 5495  df-po 5503  df-so 5504  df-fr 5544  df-se 5545  df-we 5546  df-xp 5595  df-rel 5596  df-cnv 5597  df-co 5598  df-dm 5599  df-rn 5600  df-res 5601  df-ima 5602  df-pred 6202  df-ord 6269  df-on 6270  df-lim 6271  df-suc 6272  df-iota 6391  df-fun 6435  df-fn 6436  df-f 6437  df-f1 6438  df-fo 6439  df-f1o 6440  df-fv 6441  df-isom 6442  df-riota 7232  df-ov 7278  df-oprab 7279  df-mpo 7280  df-om 7713  df-1st 7831  df-2nd 7832  df-frecs 8097  df-wrecs 8128  df-recs 8202  df-rdg 8241  df-1o 8297  df-2o 8298  df-er 8498  df-map 8617  df-en 8734  df-dom 8735  df-sdom 8736  df-fin 8737  df-sup 9201  df-inf 9202  df-card 9697  df-ac 9872  df-pnf 11011  df-mnf 11012  df-xr 11013  df-ltxr 11014  df-le 11015  df-sub 11207  df-neg 11208  df-div 11633  df-nn 11974  df-2 12036  df-3 12037  df-4 12038  df-5 12039  df-6 12040  df-7 12041  df-8 12042  df-9 12043  df-n0 12234  df-xnn0 12306  df-z 12320  df-uz 12583  df-rp 12731  df-fz 13240  df-fzo 13383  df-fl 13512  df-mod 13590  df-seq 13722  df-hash 14045  df-word 14218  df-concat 14274  df-s1 14301  df-substr 14354  df-pfx 14384  df-csh 14502  df-s2 14561  df-s3 14562  df-struct 16848  df-sets 16865  df-slot 16883  df-ndx 16895  df-base 16913  df-ress 16942  df-plusg 16975  df-tset 16981  df-0g 17152  df-gsum 17153  df-mgm 18326  df-sgrp 18375  df-mnd 18386  df-submnd 18431  df-efmnd 18508  df-grp 18580  df-symg 18975  df-pmtr 19050  df-tocyc 31374

This theorem is referenced by:  cyc3genpm  31419