Users' Mathboxes Mathbox for Thierry Arnoux < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  cyc3genpmlem Structured version   Visualization version   GIF version

Theorem cyc3genpmlem 31137
Description: Lemma for cyc3genpm 31138. (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
StepHypRef Expression
1 wrd0 14094 . . . . 5 ∅ ∈ Word 𝐶
21a1i 11 . . . 4 (((𝜑𝐼 ∈ {𝐾, 𝐿}) ∧ 𝐽 ∈ {𝐾, 𝐿}) → ∅ ∈ Word 𝐶)
3 simpr 488 . . . . . 6 ((((𝜑𝐼 ∈ {𝐾, 𝐿}) ∧ 𝐽 ∈ {𝐾, 𝐿}) ∧ 𝑐 = ∅) → 𝑐 = ∅)
43oveq2d 7229 . . . . 5 ((((𝜑𝐼 ∈ {𝐾, 𝐿}) ∧ 𝐽 ∈ {𝐾, 𝐿}) ∧ 𝑐 = ∅) → (𝑆 Σg 𝑐) = (𝑆 Σg ∅))
54eqeq2d 2748 . . . 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‘𝐷)
137, 8, 9, 10, 11, 12cycpm2cl 31106 . . . . . . . . 9 (𝜑 → (𝑀‘⟨“𝐼𝐽”⟩) ∈ (Base‘𝑆))
146, 13eqeltrd 2838 . . . . . . . 8 (𝜑𝐸 ∈ (Base‘𝑆))
15 cyc3genpmlem.f . . . . . . . . 9 (𝜑𝐹 = (𝑀‘⟨“𝐾𝐿”⟩))
16 cyc3genpmlem.k . . . . . . . . . 10 (𝜑𝐾𝐷)
17 cyc3genpmlem.l . . . . . . . . . 10 (𝜑𝐿𝐷)
18 cyc3genpmlem.2 . . . . . . . . . 10 (𝜑𝐾𝐿)
197, 8, 16, 17, 18, 12cycpm2cl 31106 . . . . . . . . 9 (𝜑 → (𝑀‘⟨“𝐾𝐿”⟩) ∈ (Base‘𝑆))
2015, 19eqeltrd 2838 . . . . . . . 8 (𝜑𝐹 ∈ (Base‘𝑆))
21 eqid 2737 . . . . . . . . 9 (Base‘𝑆) = (Base‘𝑆)
22 cyc3genpmlem.t . . . . . . . . 9 · = (+g𝑆)
2312, 21, 22symgov 18776 . . . . . . . 8 ((𝐸 ∈ (Base‘𝑆) ∧ 𝐹 ∈ (Base‘𝑆)) → (𝐸 · 𝐹) = (𝐸𝐹))
2414, 20, 23syl2anc 587 . . . . . . 7 (𝜑 → (𝐸 · 𝐹) = (𝐸𝐹))
2524ad2antrr 726 . . . . . 6 (((𝜑𝐼 ∈ {𝐾, 𝐿}) ∧ 𝐽 ∈ {𝐾, 𝐿}) → (𝐸 · 𝐹) = (𝐸𝐹))
266ad2antrr 726 . . . . . . . 8 (((𝜑𝐼 ∈ {𝐾, 𝐿}) ∧ 𝐽 ∈ {𝐾, 𝐿}) → 𝐸 = (𝑀‘⟨“𝐼𝐽”⟩))
27 eqid 2737 . . . . . . . . . 10 (pmTrsp‘𝐷) = (pmTrsp‘𝐷)
287, 8, 9, 10, 11, 27cycpm2tr 31105 . . . . . . . . 9 (𝜑 → (𝑀‘⟨“𝐼𝐽”⟩) = ((pmTrsp‘𝐷)‘{𝐼, 𝐽}))
2928ad2antrr 726 . . . . . . . 8 (((𝜑𝐼 ∈ {𝐾, 𝐿}) ∧ 𝐽 ∈ {𝐾, 𝐿}) → (𝑀‘⟨“𝐼𝐽”⟩) = ((pmTrsp‘𝐷)‘{𝐼, 𝐽}))
3026, 29eqtrd 2777 . . . . . . 7 (((𝜑𝐼 ∈ {𝐾, 𝐿}) ∧ 𝐽 ∈ {𝐾, 𝐿}) → 𝐸 = ((pmTrsp‘𝐷)‘{𝐼, 𝐽}))
317, 8, 16, 17, 18, 27cycpm2tr 31105 . . . . . . . . 9 (𝜑 → (𝑀‘⟨“𝐾𝐿”⟩) = ((pmTrsp‘𝐷)‘{𝐾, 𝐿}))
3231ad2antrr 726 . . . . . . . 8 (((𝜑𝐼 ∈ {𝐾, 𝐿}) ∧ 𝐽 ∈ {𝐾, 𝐿}) → (𝑀‘⟨“𝐾𝐿”⟩) = ((pmTrsp‘𝐷)‘{𝐾, 𝐿}))
3315ad2antrr 726 . . . . . . . 8 (((𝜑𝐼 ∈ {𝐾, 𝐿}) ∧ 𝐽 ∈ {𝐾, 𝐿}) → 𝐹 = (𝑀‘⟨“𝐾𝐿”⟩))
349ad2antrr 726 . . . . . . . . . 10 (((𝜑𝐼 ∈ {𝐾, 𝐿}) ∧ 𝐽 ∈ {𝐾, 𝐿}) → 𝐼𝐷)
3510ad2antrr 726 . . . . . . . . . 10 (((𝜑𝐼 ∈ {𝐾, 𝐿}) ∧ 𝐽 ∈ {𝐾, 𝐿}) → 𝐽𝐷)
3611ad2antrr 726 . . . . . . . . . 10 (((𝜑𝐼 ∈ {𝐾, 𝐿}) ∧ 𝐽 ∈ {𝐾, 𝐿}) → 𝐼𝐽)
37 simplr 769 . . . . . . . . . . 11 (((𝜑𝐼 ∈ {𝐾, 𝐿}) ∧ 𝐽 ∈ {𝐾, 𝐿}) → 𝐼 ∈ {𝐾, 𝐿})
38 simpr 488 . . . . . . . . . . 11 (((𝜑𝐼 ∈ {𝐾, 𝐿}) ∧ 𝐽 ∈ {𝐾, 𝐿}) → 𝐽 ∈ {𝐾, 𝐿})
3937, 38prssd 4735 . . . . . . . . . 10 (((𝜑𝐼 ∈ {𝐾, 𝐿}) ∧ 𝐽 ∈ {𝐾, 𝐿}) → {𝐼, 𝐽} ⊆ {𝐾, 𝐿})
40 ssprsseq 4738 . . . . . . . . . . 11 ((𝐼𝐷𝐽𝐷𝐼𝐽) → ({𝐼, 𝐽} ⊆ {𝐾, 𝐿} ↔ {𝐼, 𝐽} = {𝐾, 𝐿}))
4140biimpa 480 . . . . . . . . . 10 (((𝐼𝐷𝐽𝐷𝐼𝐽) ∧ {𝐼, 𝐽} ⊆ {𝐾, 𝐿}) → {𝐼, 𝐽} = {𝐾, 𝐿})
4234, 35, 36, 39, 41syl31anc 1375 . . . . . . . . 9 (((𝜑𝐼 ∈ {𝐾, 𝐿}) ∧ 𝐽 ∈ {𝐾, 𝐿}) → {𝐼, 𝐽} = {𝐾, 𝐿})
4342fveq2d 6721 . . . . . . . 8 (((𝜑𝐼 ∈ {𝐾, 𝐿}) ∧ 𝐽 ∈ {𝐾, 𝐿}) → ((pmTrsp‘𝐷)‘{𝐼, 𝐽}) = ((pmTrsp‘𝐷)‘{𝐾, 𝐿}))
4432, 33, 433eqtr4d 2787 . . . . . . 7 (((𝜑𝐼 ∈ {𝐾, 𝐿}) ∧ 𝐽 ∈ {𝐾, 𝐿}) → 𝐹 = ((pmTrsp‘𝐷)‘{𝐼, 𝐽}))
4530, 44coeq12d 5733 . . . . . 6 (((𝜑𝐼 ∈ {𝐾, 𝐿}) ∧ 𝐽 ∈ {𝐾, 𝐿}) → (𝐸𝐹) = (((pmTrsp‘𝐷)‘{𝐼, 𝐽}) ∘ ((pmTrsp‘𝐷)‘{𝐼, 𝐽})))
468ad2antrr 726 . . . . . . . 8 (((𝜑𝐼 ∈ {𝐾, 𝐿}) ∧ 𝐽 ∈ {𝐾, 𝐿}) → 𝐷𝑉)
4734, 35prssd 4735 . . . . . . . 8 (((𝜑𝐼 ∈ {𝐾, 𝐿}) ∧ 𝐽 ∈ {𝐾, 𝐿}) → {𝐼, 𝐽} ⊆ 𝐷)
48 pr2nelem 9618 . . . . . . . . 9 ((𝐼𝐷𝐽𝐷𝐼𝐽) → {𝐼, 𝐽} ≈ 2o)
4934, 35, 36, 48syl3anc 1373 . . . . . . . 8 (((𝜑𝐼 ∈ {𝐾, 𝐿}) ∧ 𝐽 ∈ {𝐾, 𝐿}) → {𝐼, 𝐽} ≈ 2o)
50 eqid 2737 . . . . . . . . 9 ran (pmTrsp‘𝐷) = ran (pmTrsp‘𝐷)
5127, 50pmtrrn 18849 . . . . . . . 8 ((𝐷𝑉 ∧ {𝐼, 𝐽} ⊆ 𝐷 ∧ {𝐼, 𝐽} ≈ 2o) → ((pmTrsp‘𝐷)‘{𝐼, 𝐽}) ∈ ran (pmTrsp‘𝐷))
5246, 47, 49, 51syl3anc 1373 . . . . . . 7 (((𝜑𝐼 ∈ {𝐾, 𝐿}) ∧ 𝐽 ∈ {𝐾, 𝐿}) → ((pmTrsp‘𝐷)‘{𝐼, 𝐽}) ∈ ran (pmTrsp‘𝐷))
5327, 50pmtrfinv 18853 . . . . . . 7 (((pmTrsp‘𝐷)‘{𝐼, 𝐽}) ∈ ran (pmTrsp‘𝐷) → (((pmTrsp‘𝐷)‘{𝐼, 𝐽}) ∘ ((pmTrsp‘𝐷)‘{𝐼, 𝐽})) = ( I ↾ 𝐷))
5452, 53syl 17 . . . . . 6 (((𝜑𝐼 ∈ {𝐾, 𝐿}) ∧ 𝐽 ∈ {𝐾, 𝐿}) → (((pmTrsp‘𝐷)‘{𝐼, 𝐽}) ∘ ((pmTrsp‘𝐷)‘{𝐼, 𝐽})) = ( I ↾ 𝐷))
5525, 45, 543eqtrd 2781 . . . . 5 (((𝜑𝐼 ∈ {𝐾, 𝐿}) ∧ 𝐽 ∈ {𝐾, 𝐿}) → (𝐸 · 𝐹) = ( I ↾ 𝐷))
5612symgid 18793 . . . . . . 7 (𝐷𝑉 → ( I ↾ 𝐷) = (0g𝑆))
5746, 56syl 17 . . . . . 6 (((𝜑𝐼 ∈ {𝐾, 𝐿}) ∧ 𝐽 ∈ {𝐾, 𝐿}) → ( I ↾ 𝐷) = (0g𝑆))
58 eqid 2737 . . . . . . 7 (0g𝑆) = (0g𝑆)
5958gsum0 18156 . . . . . 6 (𝑆 Σg ∅) = (0g𝑆)
6057, 59eqtr4di 2796 . . . . 5 (((𝜑𝐼 ∈ {𝐾, 𝐿}) ∧ 𝐽 ∈ {𝐾, 𝐿}) → ( I ↾ 𝐷) = (𝑆 Σg ∅))
6155, 60eqtrd 2777 . . . 4 (((𝜑𝐼 ∈ {𝐾, 𝐿}) ∧ 𝐽 ∈ {𝐾, 𝐿}) → (𝐸 · 𝐹) = (𝑆 Σg ∅))
622, 5, 61rspcedvd 3540 . . 3 (((𝜑𝐼 ∈ {𝐾, 𝐿}) ∧ 𝐽 ∈ {𝐾, 𝐿}) → ∃𝑐 ∈ Word 𝐶(𝐸 · 𝐹) = (𝑆 Σg 𝑐))
638ad2antrr 726 . . . . . . 7 (((𝜑𝐼 ∈ {𝐾, 𝐿}) ∧ ¬ 𝐽 ∈ {𝐾, 𝐿}) → 𝐷𝑉)
649ad2antrr 726 . . . . . . 7 (((𝜑𝐼 ∈ {𝐾, 𝐿}) ∧ ¬ 𝐽 ∈ {𝐾, 𝐿}) → 𝐼𝐷)
6516, 17prssd 4735 . . . . . . . . 9 (𝜑 → {𝐾, 𝐿} ⊆ 𝐷)
6665ad2antrr 726 . . . . . . . 8 (((𝜑𝐼 ∈ {𝐾, 𝐿}) ∧ ¬ 𝐽 ∈ {𝐾, 𝐿}) → {𝐾, 𝐿} ⊆ 𝐷)
67 simplr 769 . . . . . . . . 9 (((𝜑𝐼 ∈ {𝐾, 𝐿}) ∧ ¬ 𝐽 ∈ {𝐾, 𝐿}) → 𝐼 ∈ {𝐾, 𝐿})
68 pr2nelem 9618 . . . . . . . . . . 11 ((𝐾𝐷𝐿𝐷𝐾𝐿) → {𝐾, 𝐿} ≈ 2o)
6916, 17, 18, 68syl3anc 1373 . . . . . . . . . 10 (𝜑 → {𝐾, 𝐿} ≈ 2o)
7069ad2antrr 726 . . . . . . . . 9 (((𝜑𝐼 ∈ {𝐾, 𝐿}) ∧ ¬ 𝐽 ∈ {𝐾, 𝐿}) → {𝐾, 𝐿} ≈ 2o)
71 unidifsnel 30602 . . . . . . . . 9 ((𝐼 ∈ {𝐾, 𝐿} ∧ {𝐾, 𝐿} ≈ 2o) → ({𝐾, 𝐿} ∖ {𝐼}) ∈ {𝐾, 𝐿})
7267, 70, 71syl2anc 587 . . . . . . . 8 (((𝜑𝐼 ∈ {𝐾, 𝐿}) ∧ ¬ 𝐽 ∈ {𝐾, 𝐿}) → ({𝐾, 𝐿} ∖ {𝐼}) ∈ {𝐾, 𝐿})
7366, 72sseldd 3902 . . . . . . 7 (((𝜑𝐼 ∈ {𝐾, 𝐿}) ∧ ¬ 𝐽 ∈ {𝐾, 𝐿}) → ({𝐾, 𝐿} ∖ {𝐼}) ∈ 𝐷)
7410ad2antrr 726 . . . . . . 7 (((𝜑𝐼 ∈ {𝐾, 𝐿}) ∧ ¬ 𝐽 ∈ {𝐾, 𝐿}) → 𝐽𝐷)
75 unidifsnne 30603 . . . . . . . . 9 ((𝐼 ∈ {𝐾, 𝐿} ∧ {𝐾, 𝐿} ≈ 2o) → ({𝐾, 𝐿} ∖ {𝐼}) ≠ 𝐼)
7667, 70, 75syl2anc 587 . . . . . . . 8 (((𝜑𝐼 ∈ {𝐾, 𝐿}) ∧ ¬ 𝐽 ∈ {𝐾, 𝐿}) → ({𝐾, 𝐿} ∖ {𝐼}) ≠ 𝐼)
7776necomd 2996 . . . . . . 7 (((𝜑𝐼 ∈ {𝐾, 𝐿}) ∧ ¬ 𝐽 ∈ {𝐾, 𝐿}) → 𝐼 ({𝐾, 𝐿} ∖ {𝐼}))
78 nelne2 3039 . . . . . . . 8 (( ({𝐾, 𝐿} ∖ {𝐼}) ∈ {𝐾, 𝐿} ∧ ¬ 𝐽 ∈ {𝐾, 𝐿}) → ({𝐾, 𝐿} ∖ {𝐼}) ≠ 𝐽)
7972, 78sylancom 591 . . . . . . 7 (((𝜑𝐼 ∈ {𝐾, 𝐿}) ∧ ¬ 𝐽 ∈ {𝐾, 𝐿}) → ({𝐾, 𝐿} ∖ {𝐼}) ≠ 𝐽)
8011necomd 2996 . . . . . . . 8 (𝜑𝐽𝐼)
8180ad2antrr 726 . . . . . . 7 (((𝜑𝐼 ∈ {𝐾, 𝐿}) ∧ ¬ 𝐽 ∈ {𝐾, 𝐿}) → 𝐽𝐼)
827, 12, 63, 64, 73, 74, 77, 79, 81cycpm3cl2 31122 . . . . . 6 (((𝜑𝐼 ∈ {𝐾, 𝐿}) ∧ ¬ 𝐽 ∈ {𝐾, 𝐿}) → (𝑀‘⟨“𝐼 ({𝐾, 𝐿} ∖ {𝐼})𝐽”⟩) ∈ (𝑀 “ (♯ “ {3})))
83 cyc3genpm.t . . . . . 6 𝐶 = (𝑀 “ (♯ “ {3}))
8482, 83eleqtrrdi 2849 . . . . 5 (((𝜑𝐼 ∈ {𝐾, 𝐿}) ∧ ¬ 𝐽 ∈ {𝐾, 𝐿}) → (𝑀‘⟨“𝐼 ({𝐾, 𝐿} ∖ {𝐼})𝐽”⟩) ∈ 𝐶)
8584s1cld 14160 . . . 4 (((𝜑𝐼 ∈ {𝐾, 𝐿}) ∧ ¬ 𝐽 ∈ {𝐾, 𝐿}) → ⟨“(𝑀‘⟨“𝐼 ({𝐾, 𝐿} ∖ {𝐼})𝐽”⟩)”⟩ ∈ Word 𝐶)
86 simpr 488 . . . . . 6 ((((𝜑𝐼 ∈ {𝐾, 𝐿}) ∧ ¬ 𝐽 ∈ {𝐾, 𝐿}) ∧ 𝑐 = ⟨“(𝑀‘⟨“𝐼 ({𝐾, 𝐿} ∖ {𝐼})𝐽”⟩)”⟩) → 𝑐 = ⟨“(𝑀‘⟨“𝐼 ({𝐾, 𝐿} ∖ {𝐼})𝐽”⟩)”⟩)
8786oveq2d 7229 . . . . 5 ((((𝜑𝐼 ∈ {𝐾, 𝐿}) ∧ ¬ 𝐽 ∈ {𝐾, 𝐿}) ∧ 𝑐 = ⟨“(𝑀‘⟨“𝐼 ({𝐾, 𝐿} ∖ {𝐼})𝐽”⟩)”⟩) → (𝑆 Σg 𝑐) = (𝑆 Σg ⟨“(𝑀‘⟨“𝐼 ({𝐾, 𝐿} ∖ {𝐼})𝐽”⟩)”⟩))
8887eqeq2d 2748 . . . 4 ((((𝜑𝐼 ∈ {𝐾, 𝐿}) ∧ ¬ 𝐽 ∈ {𝐾, 𝐿}) ∧ 𝑐 = ⟨“(𝑀‘⟨“𝐼 ({𝐾, 𝐿} ∖ {𝐼})𝐽”⟩)”⟩) → ((𝐸 · 𝐹) = (𝑆 Σg 𝑐) ↔ (𝐸 · 𝐹) = (𝑆 Σg ⟨“(𝑀‘⟨“𝐼 ({𝐾, 𝐿} ∖ {𝐼})𝐽”⟩)”⟩)))
897, 12, 63, 64, 73, 74, 77, 79, 81, 22cyc3co2 31126 . . . . 5 (((𝜑𝐼 ∈ {𝐾, 𝐿}) ∧ ¬ 𝐽 ∈ {𝐾, 𝐿}) → (𝑀‘⟨“𝐼 ({𝐾, 𝐿} ∖ {𝐼})𝐽”⟩) = ((𝑀‘⟨“𝐼𝐽”⟩) · (𝑀‘⟨“𝐼 ({𝐾, 𝐿} ∖ {𝐼})”⟩)))
907, 12, 63, 64, 73, 74, 77, 79, 81cycpm3cl 31121 . . . . . 6 (((𝜑𝐼 ∈ {𝐾, 𝐿}) ∧ ¬ 𝐽 ∈ {𝐾, 𝐿}) → (𝑀‘⟨“𝐼 ({𝐾, 𝐿} ∖ {𝐼})𝐽”⟩) ∈ (Base‘𝑆))
9121gsumws1 18264 . . . . . 6 ((𝑀‘⟨“𝐼 ({𝐾, 𝐿} ∖ {𝐼})𝐽”⟩) ∈ (Base‘𝑆) → (𝑆 Σg ⟨“(𝑀‘⟨“𝐼 ({𝐾, 𝐿} ∖ {𝐼})𝐽”⟩)”⟩) = (𝑀‘⟨“𝐼 ({𝐾, 𝐿} ∖ {𝐼})𝐽”⟩))
9290, 91syl 17 . . . . 5 (((𝜑𝐼 ∈ {𝐾, 𝐿}) ∧ ¬ 𝐽 ∈ {𝐾, 𝐿}) → (𝑆 Σg ⟨“(𝑀‘⟨“𝐼 ({𝐾, 𝐿} ∖ {𝐼})𝐽”⟩)”⟩) = (𝑀‘⟨“𝐼 ({𝐾, 𝐿} ∖ {𝐼})𝐽”⟩))
936ad2antrr 726 . . . . . 6 (((𝜑𝐼 ∈ {𝐾, 𝐿}) ∧ ¬ 𝐽 ∈ {𝐾, 𝐿}) → 𝐸 = (𝑀‘⟨“𝐼𝐽”⟩))
94 en2eleq 9622 . . . . . . . . 9 ((𝐼 ∈ {𝐾, 𝐿} ∧ {𝐾, 𝐿} ≈ 2o) → {𝐾, 𝐿} = {𝐼, ({𝐾, 𝐿} ∖ {𝐼})})
9567, 70, 94syl2anc 587 . . . . . . . 8 (((𝜑𝐼 ∈ {𝐾, 𝐿}) ∧ ¬ 𝐽 ∈ {𝐾, 𝐿}) → {𝐾, 𝐿} = {𝐼, ({𝐾, 𝐿} ∖ {𝐼})})
9695fveq2d 6721 . . . . . . 7 (((𝜑𝐼 ∈ {𝐾, 𝐿}) ∧ ¬ 𝐽 ∈ {𝐾, 𝐿}) → ((pmTrsp‘𝐷)‘{𝐾, 𝐿}) = ((pmTrsp‘𝐷)‘{𝐼, ({𝐾, 𝐿} ∖ {𝐼})}))
9715, 31eqtrd 2777 . . . . . . . 8 (𝜑𝐹 = ((pmTrsp‘𝐷)‘{𝐾, 𝐿}))
9897ad2antrr 726 . . . . . . 7 (((𝜑𝐼 ∈ {𝐾, 𝐿}) ∧ ¬ 𝐽 ∈ {𝐾, 𝐿}) → 𝐹 = ((pmTrsp‘𝐷)‘{𝐾, 𝐿}))
997, 63, 64, 73, 77, 27cycpm2tr 31105 . . . . . . 7 (((𝜑𝐼 ∈ {𝐾, 𝐿}) ∧ ¬ 𝐽 ∈ {𝐾, 𝐿}) → (𝑀‘⟨“𝐼 ({𝐾, 𝐿} ∖ {𝐼})”⟩) = ((pmTrsp‘𝐷)‘{𝐼, ({𝐾, 𝐿} ∖ {𝐼})}))
10096, 98, 993eqtr4d 2787 . . . . . 6 (((𝜑𝐼 ∈ {𝐾, 𝐿}) ∧ ¬ 𝐽 ∈ {𝐾, 𝐿}) → 𝐹 = (𝑀‘⟨“𝐼 ({𝐾, 𝐿} ∖ {𝐼})”⟩))
10193, 100oveq12d 7231 . . . . 5 (((𝜑𝐼 ∈ {𝐾, 𝐿}) ∧ ¬ 𝐽 ∈ {𝐾, 𝐿}) → (𝐸 · 𝐹) = ((𝑀‘⟨“𝐼𝐽”⟩) · (𝑀‘⟨“𝐼 ({𝐾, 𝐿} ∖ {𝐼})”⟩)))
10289, 92, 1013eqtr4rd 2788 . . . 4 (((𝜑𝐼 ∈ {𝐾, 𝐿}) ∧ ¬ 𝐽 ∈ {𝐾, 𝐿}) → (𝐸 · 𝐹) = (𝑆 Σg ⟨“(𝑀‘⟨“𝐼 ({𝐾, 𝐿} ∖ {𝐼})𝐽”⟩)”⟩))
10385, 88, 102rspcedvd 3540 . . 3 (((𝜑𝐼 ∈ {𝐾, 𝐿}) ∧ ¬ 𝐽 ∈ {𝐾, 𝐿}) → ∃𝑐 ∈ Word 𝐶(𝐸 · 𝐹) = (𝑆 Σg 𝑐))
10462, 103pm2.61dan 813 . 2 ((𝜑𝐼 ∈ {𝐾, 𝐿}) → ∃𝑐 ∈ Word 𝐶(𝐸 · 𝐹) = (𝑆 Σg 𝑐))
1058ad2antrr 726 . . . . . . 7 (((𝜑 ∧ ¬ 𝐼 ∈ {𝐾, 𝐿}) ∧ 𝐽 ∈ {𝐾, 𝐿}) → 𝐷𝑉)
10610ad2antrr 726 . . . . . . 7 (((𝜑 ∧ ¬ 𝐼 ∈ {𝐾, 𝐿}) ∧ 𝐽 ∈ {𝐾, 𝐿}) → 𝐽𝐷)
10765ad2antrr 726 . . . . . . . 8 (((𝜑 ∧ ¬ 𝐼 ∈ {𝐾, 𝐿}) ∧ 𝐽 ∈ {𝐾, 𝐿}) → {𝐾, 𝐿} ⊆ 𝐷)
108 simpr 488 . . . . . . . . 9 (((𝜑 ∧ ¬ 𝐼 ∈ {𝐾, 𝐿}) ∧ 𝐽 ∈ {𝐾, 𝐿}) → 𝐽 ∈ {𝐾, 𝐿})
10969ad2antrr 726 . . . . . . . . 9 (((𝜑 ∧ ¬ 𝐼 ∈ {𝐾, 𝐿}) ∧ 𝐽 ∈ {𝐾, 𝐿}) → {𝐾, 𝐿} ≈ 2o)
110 unidifsnel 30602 . . . . . . . . 9 ((𝐽 ∈ {𝐾, 𝐿} ∧ {𝐾, 𝐿} ≈ 2o) → ({𝐾, 𝐿} ∖ {𝐽}) ∈ {𝐾, 𝐿})
111108, 109, 110syl2anc 587 . . . . . . . 8 (((𝜑 ∧ ¬ 𝐼 ∈ {𝐾, 𝐿}) ∧ 𝐽 ∈ {𝐾, 𝐿}) → ({𝐾, 𝐿} ∖ {𝐽}) ∈ {𝐾, 𝐿})
112107, 111sseldd 3902 . . . . . . 7 (((𝜑 ∧ ¬ 𝐼 ∈ {𝐾, 𝐿}) ∧ 𝐽 ∈ {𝐾, 𝐿}) → ({𝐾, 𝐿} ∖ {𝐽}) ∈ 𝐷)
1139ad2antrr 726 . . . . . . 7 (((𝜑 ∧ ¬ 𝐼 ∈ {𝐾, 𝐿}) ∧ 𝐽 ∈ {𝐾, 𝐿}) → 𝐼𝐷)
114 unidifsnne 30603 . . . . . . . . 9 ((𝐽 ∈ {𝐾, 𝐿} ∧ {𝐾, 𝐿} ≈ 2o) → ({𝐾, 𝐿} ∖ {𝐽}) ≠ 𝐽)
115108, 109, 114syl2anc 587 . . . . . . . 8 (((𝜑 ∧ ¬ 𝐼 ∈ {𝐾, 𝐿}) ∧ 𝐽 ∈ {𝐾, 𝐿}) → ({𝐾, 𝐿} ∖ {𝐽}) ≠ 𝐽)
116115necomd 2996 . . . . . . 7 (((𝜑 ∧ ¬ 𝐼 ∈ {𝐾, 𝐿}) ∧ 𝐽 ∈ {𝐾, 𝐿}) → 𝐽 ({𝐾, 𝐿} ∖ {𝐽}))
117 simplr 769 . . . . . . . 8 (((𝜑 ∧ ¬ 𝐼 ∈ {𝐾, 𝐿}) ∧ 𝐽 ∈ {𝐾, 𝐿}) → ¬ 𝐼 ∈ {𝐾, 𝐿})
118 nelne2 3039 . . . . . . . 8 (( ({𝐾, 𝐿} ∖ {𝐽}) ∈ {𝐾, 𝐿} ∧ ¬ 𝐼 ∈ {𝐾, 𝐿}) → ({𝐾, 𝐿} ∖ {𝐽}) ≠ 𝐼)
119111, 117, 118syl2anc 587 . . . . . . 7 (((𝜑 ∧ ¬ 𝐼 ∈ {𝐾, 𝐿}) ∧ 𝐽 ∈ {𝐾, 𝐿}) → ({𝐾, 𝐿} ∖ {𝐽}) ≠ 𝐼)
12011ad2antrr 726 . . . . . . 7 (((𝜑 ∧ ¬ 𝐼 ∈ {𝐾, 𝐿}) ∧ 𝐽 ∈ {𝐾, 𝐿}) → 𝐼𝐽)
1217, 12, 105, 106, 112, 113, 116, 119, 120cycpm3cl2 31122 . . . . . 6 (((𝜑 ∧ ¬ 𝐼 ∈ {𝐾, 𝐿}) ∧ 𝐽 ∈ {𝐾, 𝐿}) → (𝑀‘⟨“𝐽 ({𝐾, 𝐿} ∖ {𝐽})𝐼”⟩) ∈ (𝑀 “ (♯ “ {3})))
122121, 83eleqtrrdi 2849 . . . . 5 (((𝜑 ∧ ¬ 𝐼 ∈ {𝐾, 𝐿}) ∧ 𝐽 ∈ {𝐾, 𝐿}) → (𝑀‘⟨“𝐽 ({𝐾, 𝐿} ∖ {𝐽})𝐼”⟩) ∈ 𝐶)
123122s1cld 14160 . . . 4 (((𝜑 ∧ ¬ 𝐼 ∈ {𝐾, 𝐿}) ∧ 𝐽 ∈ {𝐾, 𝐿}) → ⟨“(𝑀‘⟨“𝐽 ({𝐾, 𝐿} ∖ {𝐽})𝐼”⟩)”⟩ ∈ Word 𝐶)
124 simpr 488 . . . . . 6 ((((𝜑 ∧ ¬ 𝐼 ∈ {𝐾, 𝐿}) ∧ 𝐽 ∈ {𝐾, 𝐿}) ∧ 𝑐 = ⟨“(𝑀‘⟨“𝐽 ({𝐾, 𝐿} ∖ {𝐽})𝐼”⟩)”⟩) → 𝑐 = ⟨“(𝑀‘⟨“𝐽 ({𝐾, 𝐿} ∖ {𝐽})𝐼”⟩)”⟩)
125124oveq2d 7229 . . . . 5 ((((𝜑 ∧ ¬ 𝐼 ∈ {𝐾, 𝐿}) ∧ 𝐽 ∈ {𝐾, 𝐿}) ∧ 𝑐 = ⟨“(𝑀‘⟨“𝐽 ({𝐾, 𝐿} ∖ {𝐽})𝐼”⟩)”⟩) → (𝑆 Σg 𝑐) = (𝑆 Σg ⟨“(𝑀‘⟨“𝐽 ({𝐾, 𝐿} ∖ {𝐽})𝐼”⟩)”⟩))
126125eqeq2d 2748 . . . 4 ((((𝜑 ∧ ¬ 𝐼 ∈ {𝐾, 𝐿}) ∧ 𝐽 ∈ {𝐾, 𝐿}) ∧ 𝑐 = ⟨“(𝑀‘⟨“𝐽 ({𝐾, 𝐿} ∖ {𝐽})𝐼”⟩)”⟩) → ((𝐸 · 𝐹) = (𝑆 Σg 𝑐) ↔ (𝐸 · 𝐹) = (𝑆 Σg ⟨“(𝑀‘⟨“𝐽 ({𝐾, 𝐿} ∖ {𝐽})𝐼”⟩)”⟩)))
1277, 12, 105, 106, 112, 113, 116, 119, 120, 22cyc3co2 31126 . . . . 5 (((𝜑 ∧ ¬ 𝐼 ∈ {𝐾, 𝐿}) ∧ 𝐽 ∈ {𝐾, 𝐿}) → (𝑀‘⟨“𝐽 ({𝐾, 𝐿} ∖ {𝐽})𝐼”⟩) = ((𝑀‘⟨“𝐽𝐼”⟩) · (𝑀‘⟨“𝐽 ({𝐾, 𝐿} ∖ {𝐽})”⟩)))
1287, 12, 105, 106, 112, 113, 116, 119, 120cycpm3cl 31121 . . . . . 6 (((𝜑 ∧ ¬ 𝐼 ∈ {𝐾, 𝐿}) ∧ 𝐽 ∈ {𝐾, 𝐿}) → (𝑀‘⟨“𝐽 ({𝐾, 𝐿} ∖ {𝐽})𝐼”⟩) ∈ (Base‘𝑆))
12921gsumws1 18264 . . . . . 6 ((𝑀‘⟨“𝐽 ({𝐾, 𝐿} ∖ {𝐽})𝐼”⟩) ∈ (Base‘𝑆) → (𝑆 Σg ⟨“(𝑀‘⟨“𝐽 ({𝐾, 𝐿} ∖ {𝐽})𝐼”⟩)”⟩) = (𝑀‘⟨“𝐽 ({𝐾, 𝐿} ∖ {𝐽})𝐼”⟩))
130128, 129syl 17 . . . . 5 (((𝜑 ∧ ¬ 𝐼 ∈ {𝐾, 𝐿}) ∧ 𝐽 ∈ {𝐾, 𝐿}) → (𝑆 Σg ⟨“(𝑀‘⟨“𝐽 ({𝐾, 𝐿} ∖ {𝐽})𝐼”⟩)”⟩) = (𝑀‘⟨“𝐽 ({𝐾, 𝐿} ∖ {𝐽})𝐼”⟩))
131 prcom 4648 . . . . . . . . . 10 {𝐼, 𝐽} = {𝐽, 𝐼}
132131fveq2i 6720 . . . . . . . . 9 ((pmTrsp‘𝐷)‘{𝐼, 𝐽}) = ((pmTrsp‘𝐷)‘{𝐽, 𝐼})
1337, 8, 10, 9, 80, 27cycpm2tr 31105 . . . . . . . . 9 (𝜑 → (𝑀‘⟨“𝐽𝐼”⟩) = ((pmTrsp‘𝐷)‘{𝐽, 𝐼}))
134132, 28, 1333eqtr4a 2804 . . . . . . . 8 (𝜑 → (𝑀‘⟨“𝐼𝐽”⟩) = (𝑀‘⟨“𝐽𝐼”⟩))
1356, 134eqtrd 2777 . . . . . . 7 (𝜑𝐸 = (𝑀‘⟨“𝐽𝐼”⟩))
136135ad2antrr 726 . . . . . 6 (((𝜑 ∧ ¬ 𝐼 ∈ {𝐾, 𝐿}) ∧ 𝐽 ∈ {𝐾, 𝐿}) → 𝐸 = (𝑀‘⟨“𝐽𝐼”⟩))
137 en2eleq 9622 . . . . . . . . 9 ((𝐽 ∈ {𝐾, 𝐿} ∧ {𝐾, 𝐿} ≈ 2o) → {𝐾, 𝐿} = {𝐽, ({𝐾, 𝐿} ∖ {𝐽})})
138108, 109, 137syl2anc 587 . . . . . . . 8 (((𝜑 ∧ ¬ 𝐼 ∈ {𝐾, 𝐿}) ∧ 𝐽 ∈ {𝐾, 𝐿}) → {𝐾, 𝐿} = {𝐽, ({𝐾, 𝐿} ∖ {𝐽})})
139138fveq2d 6721 . . . . . . 7 (((𝜑 ∧ ¬ 𝐼 ∈ {𝐾, 𝐿}) ∧ 𝐽 ∈ {𝐾, 𝐿}) → ((pmTrsp‘𝐷)‘{𝐾, 𝐿}) = ((pmTrsp‘𝐷)‘{𝐽, ({𝐾, 𝐿} ∖ {𝐽})}))
14097ad2antrr 726 . . . . . . 7 (((𝜑 ∧ ¬ 𝐼 ∈ {𝐾, 𝐿}) ∧ 𝐽 ∈ {𝐾, 𝐿}) → 𝐹 = ((pmTrsp‘𝐷)‘{𝐾, 𝐿}))
1417, 105, 106, 112, 116, 27cycpm2tr 31105 . . . . . . 7 (((𝜑 ∧ ¬ 𝐼 ∈ {𝐾, 𝐿}) ∧ 𝐽 ∈ {𝐾, 𝐿}) → (𝑀‘⟨“𝐽 ({𝐾, 𝐿} ∖ {𝐽})”⟩) = ((pmTrsp‘𝐷)‘{𝐽, ({𝐾, 𝐿} ∖ {𝐽})}))
142139, 140, 1413eqtr4d 2787 . . . . . 6 (((𝜑 ∧ ¬ 𝐼 ∈ {𝐾, 𝐿}) ∧ 𝐽 ∈ {𝐾, 𝐿}) → 𝐹 = (𝑀‘⟨“𝐽 ({𝐾, 𝐿} ∖ {𝐽})”⟩))
143136, 142oveq12d 7231 . . . . 5 (((𝜑 ∧ ¬ 𝐼 ∈ {𝐾, 𝐿}) ∧ 𝐽 ∈ {𝐾, 𝐿}) → (𝐸 · 𝐹) = ((𝑀‘⟨“𝐽𝐼”⟩) · (𝑀‘⟨“𝐽 ({𝐾, 𝐿} ∖ {𝐽})”⟩)))
144127, 130, 1433eqtr4rd 2788 . . . 4 (((𝜑 ∧ ¬ 𝐼 ∈ {𝐾, 𝐿}) ∧ 𝐽 ∈ {𝐾, 𝐿}) → (𝐸 · 𝐹) = (𝑆 Σg ⟨“(𝑀‘⟨“𝐽 ({𝐾, 𝐿} ∖ {𝐽})𝐼”⟩)”⟩))
145123, 126, 144rspcedvd 3540 . . 3 (((𝜑 ∧ ¬ 𝐼 ∈ {𝐾, 𝐿}) ∧ 𝐽 ∈ {𝐾, 𝐿}) → ∃𝑐 ∈ Word 𝐶(𝐸 · 𝐹) = (𝑆 Σg 𝑐))
1468ad2antrr 726 . . . . . . 7 (((𝜑 ∧ ¬ 𝐼 ∈ {𝐾, 𝐿}) ∧ ¬ 𝐽 ∈ {𝐾, 𝐿}) → 𝐷𝑉)
14710ad2antrr 726 . . . . . . 7 (((𝜑 ∧ ¬ 𝐼 ∈ {𝐾, 𝐿}) ∧ ¬ 𝐽 ∈ {𝐾, 𝐿}) → 𝐽𝐷)
14816ad2antrr 726 . . . . . . 7 (((𝜑 ∧ ¬ 𝐼 ∈ {𝐾, 𝐿}) ∧ ¬ 𝐽 ∈ {𝐾, 𝐿}) → 𝐾𝐷)
1499ad2antrr 726 . . . . . . 7 (((𝜑 ∧ ¬ 𝐼 ∈ {𝐾, 𝐿}) ∧ ¬ 𝐽 ∈ {𝐾, 𝐿}) → 𝐼𝐷)
150 simpr 488 . . . . . . . 8 (((𝜑 ∧ ¬ 𝐼 ∈ {𝐾, 𝐿}) ∧ ¬ 𝐽 ∈ {𝐾, 𝐿}) → ¬ 𝐽 ∈ {𝐾, 𝐿})
151147, 150nelpr1 4569 . . . . . . 7 (((𝜑 ∧ ¬ 𝐼 ∈ {𝐾, 𝐿}) ∧ ¬ 𝐽 ∈ {𝐾, 𝐿}) → 𝐽𝐾)
152 prid1g 4676 . . . . . . . . . 10 (𝐾𝐷𝐾 ∈ {𝐾, 𝐿})
15316, 152syl 17 . . . . . . . . 9 (𝜑𝐾 ∈ {𝐾, 𝐿})
154153ad2antrr 726 . . . . . . . 8 (((𝜑 ∧ ¬ 𝐼 ∈ {𝐾, 𝐿}) ∧ ¬ 𝐽 ∈ {𝐾, 𝐿}) → 𝐾 ∈ {𝐾, 𝐿})
155 simplr 769 . . . . . . . 8 (((𝜑 ∧ ¬ 𝐼 ∈ {𝐾, 𝐿}) ∧ ¬ 𝐽 ∈ {𝐾, 𝐿}) → ¬ 𝐼 ∈ {𝐾, 𝐿})
156 nelne2 3039 . . . . . . . 8 ((𝐾 ∈ {𝐾, 𝐿} ∧ ¬ 𝐼 ∈ {𝐾, 𝐿}) → 𝐾𝐼)
157154, 155, 156syl2anc 587 . . . . . . 7 (((𝜑 ∧ ¬ 𝐼 ∈ {𝐾, 𝐿}) ∧ ¬ 𝐽 ∈ {𝐾, 𝐿}) → 𝐾𝐼)
15811ad2antrr 726 . . . . . . 7 (((𝜑 ∧ ¬ 𝐼 ∈ {𝐾, 𝐿}) ∧ ¬ 𝐽 ∈ {𝐾, 𝐿}) → 𝐼𝐽)
1597, 12, 146, 147, 148, 149, 151, 157, 158cycpm3cl2 31122 . . . . . 6 (((𝜑 ∧ ¬ 𝐼 ∈ {𝐾, 𝐿}) ∧ ¬ 𝐽 ∈ {𝐾, 𝐿}) → (𝑀‘⟨“𝐽𝐾𝐼”⟩) ∈ (𝑀 “ (♯ “ {3})))
160159, 83eleqtrrdi 2849 . . . . 5 (((𝜑 ∧ ¬ 𝐼 ∈ {𝐾, 𝐿}) ∧ ¬ 𝐽 ∈ {𝐾, 𝐿}) → (𝑀‘⟨“𝐽𝐾𝐼”⟩) ∈ 𝐶)
16117ad2antrr 726 . . . . . . 7 (((𝜑 ∧ ¬ 𝐼 ∈ {𝐾, 𝐿}) ∧ ¬ 𝐽 ∈ {𝐾, 𝐿}) → 𝐿𝐷)
16218ad2antrr 726 . . . . . . 7 (((𝜑 ∧ ¬ 𝐼 ∈ {𝐾, 𝐿}) ∧ ¬ 𝐽 ∈ {𝐾, 𝐿}) → 𝐾𝐿)
163 prid2g 4677 . . . . . . . . 9 (𝐿𝐷𝐿 ∈ {𝐾, 𝐿})
164161, 163syl 17 . . . . . . . 8 (((𝜑 ∧ ¬ 𝐼 ∈ {𝐾, 𝐿}) ∧ ¬ 𝐽 ∈ {𝐾, 𝐿}) → 𝐿 ∈ {𝐾, 𝐿})
165 nelne2 3039 . . . . . . . 8 ((𝐿 ∈ {𝐾, 𝐿} ∧ ¬ 𝐽 ∈ {𝐾, 𝐿}) → 𝐿𝐽)
166164, 165sylancom 591 . . . . . . 7 (((𝜑 ∧ ¬ 𝐼 ∈ {𝐾, 𝐿}) ∧ ¬ 𝐽 ∈ {𝐾, 𝐿}) → 𝐿𝐽)
1677, 12, 146, 148, 161, 147, 162, 166, 151cycpm3cl2 31122 . . . . . 6 (((𝜑 ∧ ¬ 𝐼 ∈ {𝐾, 𝐿}) ∧ ¬ 𝐽 ∈ {𝐾, 𝐿}) → (𝑀‘⟨“𝐾𝐿𝐽”⟩) ∈ (𝑀 “ (♯ “ {3})))
168167, 83eleqtrrdi 2849 . . . . 5 (((𝜑 ∧ ¬ 𝐼 ∈ {𝐾, 𝐿}) ∧ ¬ 𝐽 ∈ {𝐾, 𝐿}) → (𝑀‘⟨“𝐾𝐿𝐽”⟩) ∈ 𝐶)
169160, 168s2cld 14436 . . . 4 (((𝜑 ∧ ¬ 𝐼 ∈ {𝐾, 𝐿}) ∧ ¬ 𝐽 ∈ {𝐾, 𝐿}) → ⟨“(𝑀‘⟨“𝐽𝐾𝐼”⟩)(𝑀‘⟨“𝐾𝐿𝐽”⟩)”⟩ ∈ Word 𝐶)
170 simpr 488 . . . . . 6 ((((𝜑 ∧ ¬ 𝐼 ∈ {𝐾, 𝐿}) ∧ ¬ 𝐽 ∈ {𝐾, 𝐿}) ∧ 𝑐 = ⟨“(𝑀‘⟨“𝐽𝐾𝐼”⟩)(𝑀‘⟨“𝐾𝐿𝐽”⟩)”⟩) → 𝑐 = ⟨“(𝑀‘⟨“𝐽𝐾𝐼”⟩)(𝑀‘⟨“𝐾𝐿𝐽”⟩)”⟩)
171170oveq2d 7229 . . . . 5 ((((𝜑 ∧ ¬ 𝐼 ∈ {𝐾, 𝐿}) ∧ ¬ 𝐽 ∈ {𝐾, 𝐿}) ∧ 𝑐 = ⟨“(𝑀‘⟨“𝐽𝐾𝐼”⟩)(𝑀‘⟨“𝐾𝐿𝐽”⟩)”⟩) → (𝑆 Σg 𝑐) = (𝑆 Σg ⟨“(𝑀‘⟨“𝐽𝐾𝐼”⟩)(𝑀‘⟨“𝐾𝐿𝐽”⟩)”⟩))
172171eqeq2d 2748 . . . 4 ((((𝜑 ∧ ¬ 𝐼 ∈ {𝐾, 𝐿}) ∧ ¬ 𝐽 ∈ {𝐾, 𝐿}) ∧ 𝑐 = ⟨“(𝑀‘⟨“𝐽𝐾𝐼”⟩)(𝑀‘⟨“𝐾𝐿𝐽”⟩)”⟩) → ((𝐸 · 𝐹) = (𝑆 Σg 𝑐) ↔ (𝐸 · 𝐹) = (𝑆 Σg ⟨“(𝑀‘⟨“𝐽𝐾𝐼”⟩)(𝑀‘⟨“𝐾𝐿𝐽”⟩)”⟩)))
173146, 56syl 17 . . . . . . . . . 10 (((𝜑 ∧ ¬ 𝐼 ∈ {𝐾, 𝐿}) ∧ ¬ 𝐽 ∈ {𝐾, 𝐿}) → ( I ↾ 𝐷) = (0g𝑆))
174173oveq1d 7228 . . . . . . . . 9 (((𝜑 ∧ ¬ 𝐼 ∈ {𝐾, 𝐿}) ∧ ¬ 𝐽 ∈ {𝐾, 𝐿}) → (( I ↾ 𝐷) · (𝑀‘⟨“𝐾𝐿”⟩)) = ((0g𝑆) · (𝑀‘⟨“𝐾𝐿”⟩)))
17512symggrp 18792 . . . . . . . . . . . 12 (𝐷𝑉𝑆 ∈ Grp)
1768, 175syl 17 . . . . . . . . . . 11 (𝜑𝑆 ∈ Grp)
177176ad2antrr 726 . . . . . . . . . 10 (((𝜑 ∧ ¬ 𝐼 ∈ {𝐾, 𝐿}) ∧ ¬ 𝐽 ∈ {𝐾, 𝐿}) → 𝑆 ∈ Grp)
17819ad2antrr 726 . . . . . . . . . 10 (((𝜑 ∧ ¬ 𝐼 ∈ {𝐾, 𝐿}) ∧ ¬ 𝐽 ∈ {𝐾, 𝐿}) → (𝑀‘⟨“𝐾𝐿”⟩) ∈ (Base‘𝑆))
17921, 22, 58grplid 18397 . . . . . . . . . 10 ((𝑆 ∈ Grp ∧ (𝑀‘⟨“𝐾𝐿”⟩) ∈ (Base‘𝑆)) → ((0g𝑆) · (𝑀‘⟨“𝐾𝐿”⟩)) = (𝑀‘⟨“𝐾𝐿”⟩))
180177, 178, 179syl2anc 587 . . . . . . . . 9 (((𝜑 ∧ ¬ 𝐼 ∈ {𝐾, 𝐿}) ∧ ¬ 𝐽 ∈ {𝐾, 𝐿}) → ((0g𝑆) · (𝑀‘⟨“𝐾𝐿”⟩)) = (𝑀‘⟨“𝐾𝐿”⟩))
181174, 180eqtrd 2777 . . . . . . . 8 (((𝜑 ∧ ¬ 𝐼 ∈ {𝐾, 𝐿}) ∧ ¬ 𝐽 ∈ {𝐾, 𝐿}) → (( I ↾ 𝐷) · (𝑀‘⟨“𝐾𝐿”⟩)) = (𝑀‘⟨“𝐾𝐿”⟩))
182181oveq2d 7229 . . . . . . 7 (((𝜑 ∧ ¬ 𝐼 ∈ {𝐾, 𝐿}) ∧ ¬ 𝐽 ∈ {𝐾, 𝐿}) → ((𝑀‘⟨“𝐼𝐽”⟩) · (( I ↾ 𝐷) · (𝑀‘⟨“𝐾𝐿”⟩))) = ((𝑀‘⟨“𝐼𝐽”⟩) · (𝑀‘⟨“𝐾𝐿”⟩)))
18313ad2antrr 726 . . . . . . . . 9 (((𝜑 ∧ ¬ 𝐼 ∈ {𝐾, 𝐿}) ∧ ¬ 𝐽 ∈ {𝐾, 𝐿}) → (𝑀‘⟨“𝐼𝐽”⟩) ∈ (Base‘𝑆))
1847, 146, 147, 148, 151, 27cycpm2tr 31105 . . . . . . . . . 10 (((𝜑 ∧ ¬ 𝐼 ∈ {𝐾, 𝐿}) ∧ ¬ 𝐽 ∈ {𝐾, 𝐿}) → (𝑀‘⟨“𝐽𝐾”⟩) = ((pmTrsp‘𝐷)‘{𝐽, 𝐾}))
18550, 12, 21symgtrf 18861 . . . . . . . . . . 11 ran (pmTrsp‘𝐷) ⊆ (Base‘𝑆)
18610, 16prssd 4735 . . . . . . . . . . . . 13 (𝜑 → {𝐽, 𝐾} ⊆ 𝐷)
187186ad2antrr 726 . . . . . . . . . . . 12 (((𝜑 ∧ ¬ 𝐼 ∈ {𝐾, 𝐿}) ∧ ¬ 𝐽 ∈ {𝐾, 𝐿}) → {𝐽, 𝐾} ⊆ 𝐷)
188 pr2nelem 9618 . . . . . . . . . . . . 13 ((𝐽𝐷𝐾𝐷𝐽𝐾) → {𝐽, 𝐾} ≈ 2o)
189147, 148, 151, 188syl3anc 1373 . . . . . . . . . . . 12 (((𝜑 ∧ ¬ 𝐼 ∈ {𝐾, 𝐿}) ∧ ¬ 𝐽 ∈ {𝐾, 𝐿}) → {𝐽, 𝐾} ≈ 2o)
19027, 50pmtrrn 18849 . . . . . . . . . . . 12 ((𝐷𝑉 ∧ {𝐽, 𝐾} ⊆ 𝐷 ∧ {𝐽, 𝐾} ≈ 2o) → ((pmTrsp‘𝐷)‘{𝐽, 𝐾}) ∈ ran (pmTrsp‘𝐷))
191146, 187, 189, 190syl3anc 1373 . . . . . . . . . . 11 (((𝜑 ∧ ¬ 𝐼 ∈ {𝐾, 𝐿}) ∧ ¬ 𝐽 ∈ {𝐾, 𝐿}) → ((pmTrsp‘𝐷)‘{𝐽, 𝐾}) ∈ ran (pmTrsp‘𝐷))
192185, 191sseldi 3899 . . . . . . . . . 10 (((𝜑 ∧ ¬ 𝐼 ∈ {𝐾, 𝐿}) ∧ ¬ 𝐽 ∈ {𝐾, 𝐿}) → ((pmTrsp‘𝐷)‘{𝐽, 𝐾}) ∈ (Base‘𝑆))
193184, 192eqeltrd 2838 . . . . . . . . 9 (((𝜑 ∧ ¬ 𝐼 ∈ {𝐾, 𝐿}) ∧ ¬ 𝐽 ∈ {𝐾, 𝐿}) → (𝑀‘⟨“𝐽𝐾”⟩) ∈ (Base‘𝑆))
194151necomd 2996 . . . . . . . . . . . . 13 (((𝜑 ∧ ¬ 𝐼 ∈ {𝐾, 𝐿}) ∧ ¬ 𝐽 ∈ {𝐾, 𝐿}) → 𝐾𝐽)
1957, 146, 148, 147, 194, 27cycpm2tr 31105 . . . . . . . . . . . 12 (((𝜑 ∧ ¬ 𝐼 ∈ {𝐾, 𝐿}) ∧ ¬ 𝐽 ∈ {𝐾, 𝐿}) → (𝑀‘⟨“𝐾𝐽”⟩) = ((pmTrsp‘𝐷)‘{𝐾, 𝐽}))
196 prcom 4648 . . . . . . . . . . . . . 14 {𝐽, 𝐾} = {𝐾, 𝐽}
197196a1i 11 . . . . . . . . . . . . 13 (((𝜑 ∧ ¬ 𝐼 ∈ {𝐾, 𝐿}) ∧ ¬ 𝐽 ∈ {𝐾, 𝐿}) → {𝐽, 𝐾} = {𝐾, 𝐽})
198197fveq2d 6721 . . . . . . . . . . . 12 (((𝜑 ∧ ¬ 𝐼 ∈ {𝐾, 𝐿}) ∧ ¬ 𝐽 ∈ {𝐾, 𝐿}) → ((pmTrsp‘𝐷)‘{𝐽, 𝐾}) = ((pmTrsp‘𝐷)‘{𝐾, 𝐽}))
199195, 198eqtr4d 2780 . . . . . . . . . . 11 (((𝜑 ∧ ¬ 𝐼 ∈ {𝐾, 𝐿}) ∧ ¬ 𝐽 ∈ {𝐾, 𝐿}) → (𝑀‘⟨“𝐾𝐽”⟩) = ((pmTrsp‘𝐷)‘{𝐽, 𝐾}))
200199, 192eqeltrd 2838 . . . . . . . . . 10 (((𝜑 ∧ ¬ 𝐼 ∈ {𝐾, 𝐿}) ∧ ¬ 𝐽 ∈ {𝐾, 𝐿}) → (𝑀‘⟨“𝐾𝐽”⟩) ∈ (Base‘𝑆))
20121, 22grpcl 18373 . . . . . . . . . 10 ((𝑆 ∈ Grp ∧ (𝑀‘⟨“𝐾𝐽”⟩) ∈ (Base‘𝑆) ∧ (𝑀‘⟨“𝐾𝐿”⟩) ∈ (Base‘𝑆)) → ((𝑀‘⟨“𝐾𝐽”⟩) · (𝑀‘⟨“𝐾𝐿”⟩)) ∈ (Base‘𝑆))
202177, 200, 178, 201syl3anc 1373 . . . . . . . . 9 (((𝜑 ∧ ¬ 𝐼 ∈ {𝐾, 𝐿}) ∧ ¬ 𝐽 ∈ {𝐾, 𝐿}) → ((𝑀‘⟨“𝐾𝐽”⟩) · (𝑀‘⟨“𝐾𝐿”⟩)) ∈ (Base‘𝑆))
20321, 22grpass 18374 . . . . . . . . 9 ((𝑆 ∈ Grp ∧ ((𝑀‘⟨“𝐼𝐽”⟩) ∈ (Base‘𝑆) ∧ (𝑀‘⟨“𝐽𝐾”⟩) ∈ (Base‘𝑆) ∧ ((𝑀‘⟨“𝐾𝐽”⟩) · (𝑀‘⟨“𝐾𝐿”⟩)) ∈ (Base‘𝑆))) → (((𝑀‘⟨“𝐼𝐽”⟩) · (𝑀‘⟨“𝐽𝐾”⟩)) · ((𝑀‘⟨“𝐾𝐽”⟩) · (𝑀‘⟨“𝐾𝐿”⟩))) = ((𝑀‘⟨“𝐼𝐽”⟩) · ((𝑀‘⟨“𝐽𝐾”⟩) · ((𝑀‘⟨“𝐾𝐽”⟩) · (𝑀‘⟨“𝐾𝐿”⟩)))))
204177, 183, 193, 202, 203syl13anc 1374 . . . . . . . 8 (((𝜑 ∧ ¬ 𝐼 ∈ {𝐾, 𝐿}) ∧ ¬ 𝐽 ∈ {𝐾, 𝐿}) → (((𝑀‘⟨“𝐼𝐽”⟩) · (𝑀‘⟨“𝐽𝐾”⟩)) · ((𝑀‘⟨“𝐾𝐽”⟩) · (𝑀‘⟨“𝐾𝐿”⟩))) = ((𝑀‘⟨“𝐼𝐽”⟩) · ((𝑀‘⟨“𝐽𝐾”⟩) · ((𝑀‘⟨“𝐾𝐽”⟩) · (𝑀‘⟨“𝐾𝐿”⟩)))))
20521, 22grpass 18374 . . . . . . . . . 10 ((𝑆 ∈ Grp ∧ ((𝑀‘⟨“𝐽𝐾”⟩) ∈ (Base‘𝑆) ∧ (𝑀‘⟨“𝐾𝐽”⟩) ∈ (Base‘𝑆) ∧ (𝑀‘⟨“𝐾𝐿”⟩) ∈ (Base‘𝑆))) → (((𝑀‘⟨“𝐽𝐾”⟩) · (𝑀‘⟨“𝐾𝐽”⟩)) · (𝑀‘⟨“𝐾𝐿”⟩)) = ((𝑀‘⟨“𝐽𝐾”⟩) · ((𝑀‘⟨“𝐾𝐽”⟩) · (𝑀‘⟨“𝐾𝐿”⟩))))
206177, 193, 200, 178, 205syl13anc 1374 . . . . . . . . 9 (((𝜑 ∧ ¬ 𝐼 ∈ {𝐾, 𝐿}) ∧ ¬ 𝐽 ∈ {𝐾, 𝐿}) → (((𝑀‘⟨“𝐽𝐾”⟩) · (𝑀‘⟨“𝐾𝐽”⟩)) · (𝑀‘⟨“𝐾𝐿”⟩)) = ((𝑀‘⟨“𝐽𝐾”⟩) · ((𝑀‘⟨“𝐾𝐽”⟩) · (𝑀‘⟨“𝐾𝐿”⟩))))
207206oveq2d 7229 . . . . . . . 8 (((𝜑 ∧ ¬ 𝐼 ∈ {𝐾, 𝐿}) ∧ ¬ 𝐽 ∈ {𝐾, 𝐿}) → ((𝑀‘⟨“𝐼𝐽”⟩) · (((𝑀‘⟨“𝐽𝐾”⟩) · (𝑀‘⟨“𝐾𝐽”⟩)) · (𝑀‘⟨“𝐾𝐿”⟩))) = ((𝑀‘⟨“𝐼𝐽”⟩) · ((𝑀‘⟨“𝐽𝐾”⟩) · ((𝑀‘⟨“𝐾𝐽”⟩) · (𝑀‘⟨“𝐾𝐿”⟩)))))
208184, 199oveq12d 7231 . . . . . . . . . . 11 (((𝜑 ∧ ¬ 𝐼 ∈ {𝐾, 𝐿}) ∧ ¬ 𝐽 ∈ {𝐾, 𝐿}) → ((𝑀‘⟨“𝐽𝐾”⟩) · (𝑀‘⟨“𝐾𝐽”⟩)) = (((pmTrsp‘𝐷)‘{𝐽, 𝐾}) · ((pmTrsp‘𝐷)‘{𝐽, 𝐾})))
20912, 21, 22symgov 18776 . . . . . . . . . . . 12 ((((pmTrsp‘𝐷)‘{𝐽, 𝐾}) ∈ (Base‘𝑆) ∧ ((pmTrsp‘𝐷)‘{𝐽, 𝐾}) ∈ (Base‘𝑆)) → (((pmTrsp‘𝐷)‘{𝐽, 𝐾}) · ((pmTrsp‘𝐷)‘{𝐽, 𝐾})) = (((pmTrsp‘𝐷)‘{𝐽, 𝐾}) ∘ ((pmTrsp‘𝐷)‘{𝐽, 𝐾})))
210192, 192, 209syl2anc 587 . . . . . . . . . . 11 (((𝜑 ∧ ¬ 𝐼 ∈ {𝐾, 𝐿}) ∧ ¬ 𝐽 ∈ {𝐾, 𝐿}) → (((pmTrsp‘𝐷)‘{𝐽, 𝐾}) · ((pmTrsp‘𝐷)‘{𝐽, 𝐾})) = (((pmTrsp‘𝐷)‘{𝐽, 𝐾}) ∘ ((pmTrsp‘𝐷)‘{𝐽, 𝐾})))
21127, 50pmtrfinv 18853 . . . . . . . . . . . 12 (((pmTrsp‘𝐷)‘{𝐽, 𝐾}) ∈ ran (pmTrsp‘𝐷) → (((pmTrsp‘𝐷)‘{𝐽, 𝐾}) ∘ ((pmTrsp‘𝐷)‘{𝐽, 𝐾})) = ( I ↾ 𝐷))
212191, 211syl 17 . . . . . . . . . . 11 (((𝜑 ∧ ¬ 𝐼 ∈ {𝐾, 𝐿}) ∧ ¬ 𝐽 ∈ {𝐾, 𝐿}) → (((pmTrsp‘𝐷)‘{𝐽, 𝐾}) ∘ ((pmTrsp‘𝐷)‘{𝐽, 𝐾})) = ( I ↾ 𝐷))
213208, 210, 2123eqtrd 2781 . . . . . . . . . 10 (((𝜑 ∧ ¬ 𝐼 ∈ {𝐾, 𝐿}) ∧ ¬ 𝐽 ∈ {𝐾, 𝐿}) → ((𝑀‘⟨“𝐽𝐾”⟩) · (𝑀‘⟨“𝐾𝐽”⟩)) = ( I ↾ 𝐷))
214213oveq1d 7228 . . . . . . . . 9 (((𝜑 ∧ ¬ 𝐼 ∈ {𝐾, 𝐿}) ∧ ¬ 𝐽 ∈ {𝐾, 𝐿}) → (((𝑀‘⟨“𝐽𝐾”⟩) · (𝑀‘⟨“𝐾𝐽”⟩)) · (𝑀‘⟨“𝐾𝐿”⟩)) = (( I ↾ 𝐷) · (𝑀‘⟨“𝐾𝐿”⟩)))
215214oveq2d 7229 . . . . . . . 8 (((𝜑 ∧ ¬ 𝐼 ∈ {𝐾, 𝐿}) ∧ ¬ 𝐽 ∈ {𝐾, 𝐿}) → ((𝑀‘⟨“𝐼𝐽”⟩) · (((𝑀‘⟨“𝐽𝐾”⟩) · (𝑀‘⟨“𝐾𝐽”⟩)) · (𝑀‘⟨“𝐾𝐿”⟩))) = ((𝑀‘⟨“𝐼𝐽”⟩) · (( I ↾ 𝐷) · (𝑀‘⟨“𝐾𝐿”⟩))))
216204, 207, 2153eqtr2rd 2784 . . . . . . 7 (((𝜑 ∧ ¬ 𝐼 ∈ {𝐾, 𝐿}) ∧ ¬ 𝐽 ∈ {𝐾, 𝐿}) → ((𝑀‘⟨“𝐼𝐽”⟩) · (( I ↾ 𝐷) · (𝑀‘⟨“𝐾𝐿”⟩))) = (((𝑀‘⟨“𝐼𝐽”⟩) · (𝑀‘⟨“𝐽𝐾”⟩)) · ((𝑀‘⟨“𝐾𝐽”⟩) · (𝑀‘⟨“𝐾𝐿”⟩))))
217182, 216eqtr3d 2779 . . . . . 6 (((𝜑 ∧ ¬ 𝐼 ∈ {𝐾, 𝐿}) ∧ ¬ 𝐽 ∈ {𝐾, 𝐿}) → ((𝑀‘⟨“𝐼𝐽”⟩) · (𝑀‘⟨“𝐾𝐿”⟩)) = (((𝑀‘⟨“𝐼𝐽”⟩) · (𝑀‘⟨“𝐽𝐾”⟩)) · ((𝑀‘⟨“𝐾𝐽”⟩) · (𝑀‘⟨“𝐾𝐿”⟩))))
2186, 15oveq12d 7231 . . . . . . 7 (𝜑 → (𝐸 · 𝐹) = ((𝑀‘⟨“𝐼𝐽”⟩) · (𝑀‘⟨“𝐾𝐿”⟩)))
219218ad2antrr 726 . . . . . 6 (((𝜑 ∧ ¬ 𝐼 ∈ {𝐾, 𝐿}) ∧ ¬ 𝐽 ∈ {𝐾, 𝐿}) → (𝐸 · 𝐹) = ((𝑀‘⟨“𝐼𝐽”⟩) · (𝑀‘⟨“𝐾𝐿”⟩)))
2207, 12, 146, 147, 148, 149, 151, 157, 158, 22cyc3co2 31126 . . . . . . . 8 (((𝜑 ∧ ¬ 𝐼 ∈ {𝐾, 𝐿}) ∧ ¬ 𝐽 ∈ {𝐾, 𝐿}) → (𝑀‘⟨“𝐽𝐾𝐼”⟩) = ((𝑀‘⟨“𝐽𝐼”⟩) · (𝑀‘⟨“𝐽𝐾”⟩)))
221134oveq1d 7228 . . . . . . . . 9 (𝜑 → ((𝑀‘⟨“𝐼𝐽”⟩) · (𝑀‘⟨“𝐽𝐾”⟩)) = ((𝑀‘⟨“𝐽𝐼”⟩) · (𝑀‘⟨“𝐽𝐾”⟩)))
222221ad2antrr 726 . . . . . . . 8 (((𝜑 ∧ ¬ 𝐼 ∈ {𝐾, 𝐿}) ∧ ¬ 𝐽 ∈ {𝐾, 𝐿}) → ((𝑀‘⟨“𝐼𝐽”⟩) · (𝑀‘⟨“𝐽𝐾”⟩)) = ((𝑀‘⟨“𝐽𝐼”⟩) · (𝑀‘⟨“𝐽𝐾”⟩)))
223220, 222eqtr4d 2780 . . . . . . 7 (((𝜑 ∧ ¬ 𝐼 ∈ {𝐾, 𝐿}) ∧ ¬ 𝐽 ∈ {𝐾, 𝐿}) → (𝑀‘⟨“𝐽𝐾𝐼”⟩) = ((𝑀‘⟨“𝐼𝐽”⟩) · (𝑀‘⟨“𝐽𝐾”⟩)))
2247, 12, 146, 148, 161, 147, 162, 166, 151, 22cyc3co2 31126 . . . . . . 7 (((𝜑 ∧ ¬ 𝐼 ∈ {𝐾, 𝐿}) ∧ ¬ 𝐽 ∈ {𝐾, 𝐿}) → (𝑀‘⟨“𝐾𝐿𝐽”⟩) = ((𝑀‘⟨“𝐾𝐽”⟩) · (𝑀‘⟨“𝐾𝐿”⟩)))
225223, 224oveq12d 7231 . . . . . 6 (((𝜑 ∧ ¬ 𝐼 ∈ {𝐾, 𝐿}) ∧ ¬ 𝐽 ∈ {𝐾, 𝐿}) → ((𝑀‘⟨“𝐽𝐾𝐼”⟩) · (𝑀‘⟨“𝐾𝐿𝐽”⟩)) = (((𝑀‘⟨“𝐼𝐽”⟩) · (𝑀‘⟨“𝐽𝐾”⟩)) · ((𝑀‘⟨“𝐾𝐽”⟩) · (𝑀‘⟨“𝐾𝐿”⟩))))
226217, 219, 2253eqtr4d 2787 . . . . 5 (((𝜑 ∧ ¬ 𝐼 ∈ {𝐾, 𝐿}) ∧ ¬ 𝐽 ∈ {𝐾, 𝐿}) → (𝐸 · 𝐹) = ((𝑀‘⟨“𝐽𝐾𝐼”⟩) · (𝑀‘⟨“𝐾𝐿𝐽”⟩)))
227176grpmndd 18377 . . . . . . 7 (𝜑𝑆 ∈ Mnd)
228227ad2antrr 726 . . . . . 6 (((𝜑 ∧ ¬ 𝐼 ∈ {𝐾, 𝐿}) ∧ ¬ 𝐽 ∈ {𝐾, 𝐿}) → 𝑆 ∈ Mnd)
2297, 12, 146, 147, 148, 149, 151, 157, 158cycpm3cl 31121 . . . . . 6 (((𝜑 ∧ ¬ 𝐼 ∈ {𝐾, 𝐿}) ∧ ¬ 𝐽 ∈ {𝐾, 𝐿}) → (𝑀‘⟨“𝐽𝐾𝐼”⟩) ∈ (Base‘𝑆))
230224, 202eqeltrd 2838 . . . . . 6 (((𝜑 ∧ ¬ 𝐼 ∈ {𝐾, 𝐿}) ∧ ¬ 𝐽 ∈ {𝐾, 𝐿}) → (𝑀‘⟨“𝐾𝐿𝐽”⟩) ∈ (Base‘𝑆))
23121, 22gsumws2 18269 . . . . . 6 ((𝑆 ∈ Mnd ∧ (𝑀‘⟨“𝐽𝐾𝐼”⟩) ∈ (Base‘𝑆) ∧ (𝑀‘⟨“𝐾𝐿𝐽”⟩) ∈ (Base‘𝑆)) → (𝑆 Σg ⟨“(𝑀‘⟨“𝐽𝐾𝐼”⟩)(𝑀‘⟨“𝐾𝐿𝐽”⟩)”⟩) = ((𝑀‘⟨“𝐽𝐾𝐼”⟩) · (𝑀‘⟨“𝐾𝐿𝐽”⟩)))
232228, 229, 230, 231syl3anc 1373 . . . . 5 (((𝜑 ∧ ¬ 𝐼 ∈ {𝐾, 𝐿}) ∧ ¬ 𝐽 ∈ {𝐾, 𝐿}) → (𝑆 Σg ⟨“(𝑀‘⟨“𝐽𝐾𝐼”⟩)(𝑀‘⟨“𝐾𝐿𝐽”⟩)”⟩) = ((𝑀‘⟨“𝐽𝐾𝐼”⟩) · (𝑀‘⟨“𝐾𝐿𝐽”⟩)))
233226, 232eqtr4d 2780 . . . 4 (((𝜑 ∧ ¬ 𝐼 ∈ {𝐾, 𝐿}) ∧ ¬ 𝐽 ∈ {𝐾, 𝐿}) → (𝐸 · 𝐹) = (𝑆 Σg ⟨“(𝑀‘⟨“𝐽𝐾𝐼”⟩)(𝑀‘⟨“𝐾𝐿𝐽”⟩)”⟩))
234169, 172, 233rspcedvd 3540 . . 3 (((𝜑 ∧ ¬ 𝐼 ∈ {𝐾, 𝐿}) ∧ ¬ 𝐽 ∈ {𝐾, 𝐿}) → ∃𝑐 ∈ Word 𝐶(𝐸 · 𝐹) = (𝑆 Σg 𝑐))
235145, 234pm2.61dan 813 . 2 ((𝜑 ∧ ¬ 𝐼 ∈ {𝐾, 𝐿}) → ∃𝑐 ∈ Word 𝐶(𝐸 · 𝐹) = (𝑆 Σg 𝑐))
236104, 235pm2.61dan 813 1 (𝜑 → ∃𝑐 ∈ Word 𝐶(𝐸 · 𝐹) = (𝑆 Σg 𝑐))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wa 399  w3a 1089   = wceq 1543  wcel 2110  wne 2940  wrex 3062  cdif 3863  wss 3866  c0 4237  {csn 4541  {cpr 4543   cuni 4819   class class class wbr 5053   I cid 5454  ccnv 5550  ran crn 5552  cres 5553  cima 5554  ccom 5555  cfv 6380  (class class class)co 7213  2oc2o 8196  cen 8623  3c3 11886  chash 13896  Word cword 14069  ⟨“cs1 14152  ⟨“cs2 14406  ⟨“cs3 14407  Basecbs 16760  +gcplusg 16802  0gc0g 16944   Σg cgsu 16945  Mndcmnd 18173  Grpcgrp 18365  SymGrpcsymg 18759  pmTrspcpmtr 18833  pmEvencevpm 18882  toCycctocyc 31092
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2016  ax-8 2112  ax-9 2120  ax-10 2141  ax-11 2158  ax-12 2175  ax-ext 2708  ax-rep 5179  ax-sep 5192  ax-nul 5199  ax-pow 5258  ax-pr 5322  ax-un 7523  ax-reg 9208  ax-ac2 10077  ax-cnex 10785  ax-resscn 10786  ax-1cn 10787  ax-icn 10788  ax-addcl 10789  ax-addrcl 10790  ax-mulcl 10791  ax-mulrcl 10792  ax-mulcom 10793  ax-addass 10794  ax-mulass 10795  ax-distr 10796  ax-i2m1 10797  ax-1ne0 10798  ax-1rid 10799  ax-rnegex 10800  ax-rrecex 10801  ax-cnre 10802  ax-pre-lttri 10803  ax-pre-lttrn 10804  ax-pre-ltadd 10805  ax-pre-mulgt0 10806  ax-pre-sup 10807
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 848  df-3or 1090  df-3an 1091  df-tru 1546  df-fal 1556  df-ex 1788  df-nf 1792  df-sb 2071  df-mo 2539  df-eu 2568  df-clab 2715  df-cleq 2729  df-clel 2816  df-nfc 2886  df-ne 2941  df-nel 3047  df-ral 3066  df-rex 3067  df-reu 3068  df-rmo 3069  df-rab 3070  df-v 3410  df-sbc 3695  df-csb 3812  df-dif 3869  df-un 3871  df-in 3873  df-ss 3883  df-pss 3885  df-nul 4238  df-if 4440  df-pw 4515  df-sn 4542  df-pr 4544  df-tp 4546  df-op 4548  df-uni 4820  df-int 4860  df-iun 4906  df-br 5054  df-opab 5116  df-mpt 5136  df-tr 5162  df-id 5455  df-eprel 5460  df-po 5468  df-so 5469  df-fr 5509  df-se 5510  df-we 5511  df-xp 5557  df-rel 5558  df-cnv 5559  df-co 5560  df-dm 5561  df-rn 5562  df-res 5563  df-ima 5564  df-pred 6160  df-ord 6216  df-on 6217  df-lim 6218  df-suc 6219  df-iota 6338  df-fun 6382  df-fn 6383  df-f 6384  df-f1 6385  df-fo 6386  df-f1o 6387  df-fv 6388  df-isom 6389  df-riota 7170  df-ov 7216  df-oprab 7217  df-mpo 7218  df-om 7645  df-1st 7761  df-2nd 7762  df-wrecs 8047  df-recs 8108  df-rdg 8146  df-1o 8202  df-2o 8203  df-er 8391  df-map 8510  df-en 8627  df-dom 8628  df-sdom 8629  df-fin 8630  df-sup 9058  df-inf 9059  df-card 9555  df-ac 9730  df-pnf 10869  df-mnf 10870  df-xr 10871  df-ltxr 10872  df-le 10873  df-sub 11064  df-neg 11065  df-div 11490  df-nn 11831  df-2 11893  df-3 11894  df-4 11895  df-5 11896  df-6 11897  df-7 11898  df-8 11899  df-9 11900  df-n0 12091  df-xnn0 12163  df-z 12177  df-uz 12439  df-rp 12587  df-fz 13096  df-fzo 13239  df-fl 13367  df-mod 13443  df-seq 13575  df-hash 13897  df-word 14070  df-concat 14126  df-s1 14153  df-substr 14206  df-pfx 14236  df-csh 14354  df-s2 14413  df-s3 14414  df-struct 16700  df-sets 16717  df-slot 16735  df-ndx 16745  df-base 16761  df-ress 16785  df-plusg 16815  df-tset 16821  df-0g 16946  df-gsum 16947  df-mgm 18114  df-sgrp 18163  df-mnd 18174  df-submnd 18219  df-efmnd 18296  df-grp 18368  df-symg 18760  df-pmtr 18834  df-tocyc 31093
This theorem is referenced by:  cyc3genpm  31138
  Copyright terms: Public domain W3C validator