Metamath Proof Explorer


Theorem cyc3genpmlem

Description: Lemma for cyc3genpm . (Contributed by Thierry Arnoux, 24-Sep-2023)

Ref Expression
Hypotheses 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 cyc3genpmlem ( 𝜑 → ∃ 𝑐 ∈ Word 𝐶 ( 𝐸 · 𝐹 ) = ( 𝑆 Σg 𝑐 ) )

Proof

Step Hyp Ref Expression
1 cyc3genpm.t 𝐶 = ( 𝑀 “ ( ♯ “ { 3 } ) )
2 cyc3genpm.a 𝐴 = ( pmEven ‘ 𝐷 )
3 cyc3genpm.s 𝑆 = ( SymGrp ‘ 𝐷 )
4 cyc3genpm.n 𝑁 = ( ♯ ‘ 𝐷 )
5 cyc3genpm.m 𝑀 = ( toCyc ‘ 𝐷 )
6 cyc3genpmlem.t · = ( +g𝑆 )
7 cyc3genpmlem.i ( 𝜑𝐼𝐷 )
8 cyc3genpmlem.j ( 𝜑𝐽𝐷 )
9 cyc3genpmlem.k ( 𝜑𝐾𝐷 )
10 cyc3genpmlem.l ( 𝜑𝐿𝐷 )
11 cyc3genpmlem.e ( 𝜑𝐸 = ( 𝑀 ‘ ⟨“ 𝐼 𝐽 ”⟩ ) )
12 cyc3genpmlem.f ( 𝜑𝐹 = ( 𝑀 ‘ ⟨“ 𝐾 𝐿 ”⟩ ) )
13 cyc3genpmlem.d ( 𝜑𝐷𝑉 )
14 cyc3genpmlem.1 ( 𝜑𝐼𝐽 )
15 cyc3genpmlem.2 ( 𝜑𝐾𝐿 )
16 wrd0 ∅ ∈ Word 𝐶
17 16 a1i ( ( ( 𝜑𝐼 ∈ { 𝐾 , 𝐿 } ) ∧ 𝐽 ∈ { 𝐾 , 𝐿 } ) → ∅ ∈ Word 𝐶 )
18 simpr ( ( ( ( 𝜑𝐼 ∈ { 𝐾 , 𝐿 } ) ∧ 𝐽 ∈ { 𝐾 , 𝐿 } ) ∧ 𝑐 = ∅ ) → 𝑐 = ∅ )
19 18 oveq2d ( ( ( ( 𝜑𝐼 ∈ { 𝐾 , 𝐿 } ) ∧ 𝐽 ∈ { 𝐾 , 𝐿 } ) ∧ 𝑐 = ∅ ) → ( 𝑆 Σg 𝑐 ) = ( 𝑆 Σg ∅ ) )
20 19 eqeq2d ( ( ( ( 𝜑𝐼 ∈ { 𝐾 , 𝐿 } ) ∧ 𝐽 ∈ { 𝐾 , 𝐿 } ) ∧ 𝑐 = ∅ ) → ( ( 𝐸 · 𝐹 ) = ( 𝑆 Σg 𝑐 ) ↔ ( 𝐸 · 𝐹 ) = ( 𝑆 Σg ∅ ) ) )
21 5 13 7 8 14 3 cycpm2cl ( 𝜑 → ( 𝑀 ‘ ⟨“ 𝐼 𝐽 ”⟩ ) ∈ ( Base ‘ 𝑆 ) )
22 11 21 eqeltrd ( 𝜑𝐸 ∈ ( Base ‘ 𝑆 ) )
23 5 13 9 10 15 3 cycpm2cl ( 𝜑 → ( 𝑀 ‘ ⟨“ 𝐾 𝐿 ”⟩ ) ∈ ( Base ‘ 𝑆 ) )
24 12 23 eqeltrd ( 𝜑𝐹 ∈ ( Base ‘ 𝑆 ) )
25 eqid ( Base ‘ 𝑆 ) = ( Base ‘ 𝑆 )
26 3 25 6 symgov ( ( 𝐸 ∈ ( Base ‘ 𝑆 ) ∧ 𝐹 ∈ ( Base ‘ 𝑆 ) ) → ( 𝐸 · 𝐹 ) = ( 𝐸𝐹 ) )
27 22 24 26 syl2anc ( 𝜑 → ( 𝐸 · 𝐹 ) = ( 𝐸𝐹 ) )
28 27 ad2antrr ( ( ( 𝜑𝐼 ∈ { 𝐾 , 𝐿 } ) ∧ 𝐽 ∈ { 𝐾 , 𝐿 } ) → ( 𝐸 · 𝐹 ) = ( 𝐸𝐹 ) )
29 11 ad2antrr ( ( ( 𝜑𝐼 ∈ { 𝐾 , 𝐿 } ) ∧ 𝐽 ∈ { 𝐾 , 𝐿 } ) → 𝐸 = ( 𝑀 ‘ ⟨“ 𝐼 𝐽 ”⟩ ) )
30 eqid ( pmTrsp ‘ 𝐷 ) = ( pmTrsp ‘ 𝐷 )
31 5 13 7 8 14 30 cycpm2tr ( 𝜑 → ( 𝑀 ‘ ⟨“ 𝐼 𝐽 ”⟩ ) = ( ( pmTrsp ‘ 𝐷 ) ‘ { 𝐼 , 𝐽 } ) )
32 31 ad2antrr ( ( ( 𝜑𝐼 ∈ { 𝐾 , 𝐿 } ) ∧ 𝐽 ∈ { 𝐾 , 𝐿 } ) → ( 𝑀 ‘ ⟨“ 𝐼 𝐽 ”⟩ ) = ( ( pmTrsp ‘ 𝐷 ) ‘ { 𝐼 , 𝐽 } ) )
33 29 32 eqtrd ( ( ( 𝜑𝐼 ∈ { 𝐾 , 𝐿 } ) ∧ 𝐽 ∈ { 𝐾 , 𝐿 } ) → 𝐸 = ( ( pmTrsp ‘ 𝐷 ) ‘ { 𝐼 , 𝐽 } ) )
34 5 13 9 10 15 30 cycpm2tr ( 𝜑 → ( 𝑀 ‘ ⟨“ 𝐾 𝐿 ”⟩ ) = ( ( pmTrsp ‘ 𝐷 ) ‘ { 𝐾 , 𝐿 } ) )
35 34 ad2antrr ( ( ( 𝜑𝐼 ∈ { 𝐾 , 𝐿 } ) ∧ 𝐽 ∈ { 𝐾 , 𝐿 } ) → ( 𝑀 ‘ ⟨“ 𝐾 𝐿 ”⟩ ) = ( ( pmTrsp ‘ 𝐷 ) ‘ { 𝐾 , 𝐿 } ) )
36 12 ad2antrr ( ( ( 𝜑𝐼 ∈ { 𝐾 , 𝐿 } ) ∧ 𝐽 ∈ { 𝐾 , 𝐿 } ) → 𝐹 = ( 𝑀 ‘ ⟨“ 𝐾 𝐿 ”⟩ ) )
37 7 ad2antrr ( ( ( 𝜑𝐼 ∈ { 𝐾 , 𝐿 } ) ∧ 𝐽 ∈ { 𝐾 , 𝐿 } ) → 𝐼𝐷 )
38 8 ad2antrr ( ( ( 𝜑𝐼 ∈ { 𝐾 , 𝐿 } ) ∧ 𝐽 ∈ { 𝐾 , 𝐿 } ) → 𝐽𝐷 )
39 14 ad2antrr ( ( ( 𝜑𝐼 ∈ { 𝐾 , 𝐿 } ) ∧ 𝐽 ∈ { 𝐾 , 𝐿 } ) → 𝐼𝐽 )
40 simplr ( ( ( 𝜑𝐼 ∈ { 𝐾 , 𝐿 } ) ∧ 𝐽 ∈ { 𝐾 , 𝐿 } ) → 𝐼 ∈ { 𝐾 , 𝐿 } )
41 simpr ( ( ( 𝜑𝐼 ∈ { 𝐾 , 𝐿 } ) ∧ 𝐽 ∈ { 𝐾 , 𝐿 } ) → 𝐽 ∈ { 𝐾 , 𝐿 } )
42 40 41 prssd ( ( ( 𝜑𝐼 ∈ { 𝐾 , 𝐿 } ) ∧ 𝐽 ∈ { 𝐾 , 𝐿 } ) → { 𝐼 , 𝐽 } ⊆ { 𝐾 , 𝐿 } )
43 ssprsseq ( ( 𝐼𝐷𝐽𝐷𝐼𝐽 ) → ( { 𝐼 , 𝐽 } ⊆ { 𝐾 , 𝐿 } ↔ { 𝐼 , 𝐽 } = { 𝐾 , 𝐿 } ) )
44 43 biimpa ( ( ( 𝐼𝐷𝐽𝐷𝐼𝐽 ) ∧ { 𝐼 , 𝐽 } ⊆ { 𝐾 , 𝐿 } ) → { 𝐼 , 𝐽 } = { 𝐾 , 𝐿 } )
45 37 38 39 42 44 syl31anc ( ( ( 𝜑𝐼 ∈ { 𝐾 , 𝐿 } ) ∧ 𝐽 ∈ { 𝐾 , 𝐿 } ) → { 𝐼 , 𝐽 } = { 𝐾 , 𝐿 } )
46 45 fveq2d ( ( ( 𝜑𝐼 ∈ { 𝐾 , 𝐿 } ) ∧ 𝐽 ∈ { 𝐾 , 𝐿 } ) → ( ( pmTrsp ‘ 𝐷 ) ‘ { 𝐼 , 𝐽 } ) = ( ( pmTrsp ‘ 𝐷 ) ‘ { 𝐾 , 𝐿 } ) )
47 35 36 46 3eqtr4d ( ( ( 𝜑𝐼 ∈ { 𝐾 , 𝐿 } ) ∧ 𝐽 ∈ { 𝐾 , 𝐿 } ) → 𝐹 = ( ( pmTrsp ‘ 𝐷 ) ‘ { 𝐼 , 𝐽 } ) )
48 33 47 coeq12d ( ( ( 𝜑𝐼 ∈ { 𝐾 , 𝐿 } ) ∧ 𝐽 ∈ { 𝐾 , 𝐿 } ) → ( 𝐸𝐹 ) = ( ( ( pmTrsp ‘ 𝐷 ) ‘ { 𝐼 , 𝐽 } ) ∘ ( ( pmTrsp ‘ 𝐷 ) ‘ { 𝐼 , 𝐽 } ) ) )
49 13 ad2antrr ( ( ( 𝜑𝐼 ∈ { 𝐾 , 𝐿 } ) ∧ 𝐽 ∈ { 𝐾 , 𝐿 } ) → 𝐷𝑉 )
50 37 38 prssd ( ( ( 𝜑𝐼 ∈ { 𝐾 , 𝐿 } ) ∧ 𝐽 ∈ { 𝐾 , 𝐿 } ) → { 𝐼 , 𝐽 } ⊆ 𝐷 )
51 pr2nelem ( ( 𝐼𝐷𝐽𝐷𝐼𝐽 ) → { 𝐼 , 𝐽 } ≈ 2o )
52 37 38 39 51 syl3anc ( ( ( 𝜑𝐼 ∈ { 𝐾 , 𝐿 } ) ∧ 𝐽 ∈ { 𝐾 , 𝐿 } ) → { 𝐼 , 𝐽 } ≈ 2o )
53 eqid ran ( pmTrsp ‘ 𝐷 ) = ran ( pmTrsp ‘ 𝐷 )
54 30 53 pmtrrn ( ( 𝐷𝑉 ∧ { 𝐼 , 𝐽 } ⊆ 𝐷 ∧ { 𝐼 , 𝐽 } ≈ 2o ) → ( ( pmTrsp ‘ 𝐷 ) ‘ { 𝐼 , 𝐽 } ) ∈ ran ( pmTrsp ‘ 𝐷 ) )
55 49 50 52 54 syl3anc ( ( ( 𝜑𝐼 ∈ { 𝐾 , 𝐿 } ) ∧ 𝐽 ∈ { 𝐾 , 𝐿 } ) → ( ( pmTrsp ‘ 𝐷 ) ‘ { 𝐼 , 𝐽 } ) ∈ ran ( pmTrsp ‘ 𝐷 ) )
56 30 53 pmtrfinv ( ( ( pmTrsp ‘ 𝐷 ) ‘ { 𝐼 , 𝐽 } ) ∈ ran ( pmTrsp ‘ 𝐷 ) → ( ( ( pmTrsp ‘ 𝐷 ) ‘ { 𝐼 , 𝐽 } ) ∘ ( ( pmTrsp ‘ 𝐷 ) ‘ { 𝐼 , 𝐽 } ) ) = ( I ↾ 𝐷 ) )
57 55 56 syl ( ( ( 𝜑𝐼 ∈ { 𝐾 , 𝐿 } ) ∧ 𝐽 ∈ { 𝐾 , 𝐿 } ) → ( ( ( pmTrsp ‘ 𝐷 ) ‘ { 𝐼 , 𝐽 } ) ∘ ( ( pmTrsp ‘ 𝐷 ) ‘ { 𝐼 , 𝐽 } ) ) = ( I ↾ 𝐷 ) )
58 28 48 57 3eqtrd ( ( ( 𝜑𝐼 ∈ { 𝐾 , 𝐿 } ) ∧ 𝐽 ∈ { 𝐾 , 𝐿 } ) → ( 𝐸 · 𝐹 ) = ( I ↾ 𝐷 ) )
59 3 symgid ( 𝐷𝑉 → ( I ↾ 𝐷 ) = ( 0g𝑆 ) )
60 49 59 syl ( ( ( 𝜑𝐼 ∈ { 𝐾 , 𝐿 } ) ∧ 𝐽 ∈ { 𝐾 , 𝐿 } ) → ( I ↾ 𝐷 ) = ( 0g𝑆 ) )
61 eqid ( 0g𝑆 ) = ( 0g𝑆 )
62 61 gsum0 ( 𝑆 Σg ∅ ) = ( 0g𝑆 )
63 60 62 eqtr4di ( ( ( 𝜑𝐼 ∈ { 𝐾 , 𝐿 } ) ∧ 𝐽 ∈ { 𝐾 , 𝐿 } ) → ( I ↾ 𝐷 ) = ( 𝑆 Σg ∅ ) )
64 58 63 eqtrd ( ( ( 𝜑𝐼 ∈ { 𝐾 , 𝐿 } ) ∧ 𝐽 ∈ { 𝐾 , 𝐿 } ) → ( 𝐸 · 𝐹 ) = ( 𝑆 Σg ∅ ) )
65 17 20 64 rspcedvd ( ( ( 𝜑𝐼 ∈ { 𝐾 , 𝐿 } ) ∧ 𝐽 ∈ { 𝐾 , 𝐿 } ) → ∃ 𝑐 ∈ Word 𝐶 ( 𝐸 · 𝐹 ) = ( 𝑆 Σg 𝑐 ) )
66 13 ad2antrr ( ( ( 𝜑𝐼 ∈ { 𝐾 , 𝐿 } ) ∧ ¬ 𝐽 ∈ { 𝐾 , 𝐿 } ) → 𝐷𝑉 )
67 7 ad2antrr ( ( ( 𝜑𝐼 ∈ { 𝐾 , 𝐿 } ) ∧ ¬ 𝐽 ∈ { 𝐾 , 𝐿 } ) → 𝐼𝐷 )
68 9 10 prssd ( 𝜑 → { 𝐾 , 𝐿 } ⊆ 𝐷 )
69 68 ad2antrr ( ( ( 𝜑𝐼 ∈ { 𝐾 , 𝐿 } ) ∧ ¬ 𝐽 ∈ { 𝐾 , 𝐿 } ) → { 𝐾 , 𝐿 } ⊆ 𝐷 )
70 simplr ( ( ( 𝜑𝐼 ∈ { 𝐾 , 𝐿 } ) ∧ ¬ 𝐽 ∈ { 𝐾 , 𝐿 } ) → 𝐼 ∈ { 𝐾 , 𝐿 } )
71 pr2nelem ( ( 𝐾𝐷𝐿𝐷𝐾𝐿 ) → { 𝐾 , 𝐿 } ≈ 2o )
72 9 10 15 71 syl3anc ( 𝜑 → { 𝐾 , 𝐿 } ≈ 2o )
73 72 ad2antrr ( ( ( 𝜑𝐼 ∈ { 𝐾 , 𝐿 } ) ∧ ¬ 𝐽 ∈ { 𝐾 , 𝐿 } ) → { 𝐾 , 𝐿 } ≈ 2o )
74 unidifsnel ( ( 𝐼 ∈ { 𝐾 , 𝐿 } ∧ { 𝐾 , 𝐿 } ≈ 2o ) → ( { 𝐾 , 𝐿 } ∖ { 𝐼 } ) ∈ { 𝐾 , 𝐿 } )
75 70 73 74 syl2anc ( ( ( 𝜑𝐼 ∈ { 𝐾 , 𝐿 } ) ∧ ¬ 𝐽 ∈ { 𝐾 , 𝐿 } ) → ( { 𝐾 , 𝐿 } ∖ { 𝐼 } ) ∈ { 𝐾 , 𝐿 } )
76 69 75 sseldd ( ( ( 𝜑𝐼 ∈ { 𝐾 , 𝐿 } ) ∧ ¬ 𝐽 ∈ { 𝐾 , 𝐿 } ) → ( { 𝐾 , 𝐿 } ∖ { 𝐼 } ) ∈ 𝐷 )
77 8 ad2antrr ( ( ( 𝜑𝐼 ∈ { 𝐾 , 𝐿 } ) ∧ ¬ 𝐽 ∈ { 𝐾 , 𝐿 } ) → 𝐽𝐷 )
78 unidifsnne ( ( 𝐼 ∈ { 𝐾 , 𝐿 } ∧ { 𝐾 , 𝐿 } ≈ 2o ) → ( { 𝐾 , 𝐿 } ∖ { 𝐼 } ) ≠ 𝐼 )
79 70 73 78 syl2anc ( ( ( 𝜑𝐼 ∈ { 𝐾 , 𝐿 } ) ∧ ¬ 𝐽 ∈ { 𝐾 , 𝐿 } ) → ( { 𝐾 , 𝐿 } ∖ { 𝐼 } ) ≠ 𝐼 )
80 79 necomd ( ( ( 𝜑𝐼 ∈ { 𝐾 , 𝐿 } ) ∧ ¬ 𝐽 ∈ { 𝐾 , 𝐿 } ) → 𝐼 ( { 𝐾 , 𝐿 } ∖ { 𝐼 } ) )
81 nelne2 ( ( ( { 𝐾 , 𝐿 } ∖ { 𝐼 } ) ∈ { 𝐾 , 𝐿 } ∧ ¬ 𝐽 ∈ { 𝐾 , 𝐿 } ) → ( { 𝐾 , 𝐿 } ∖ { 𝐼 } ) ≠ 𝐽 )
82 75 81 sylancom ( ( ( 𝜑𝐼 ∈ { 𝐾 , 𝐿 } ) ∧ ¬ 𝐽 ∈ { 𝐾 , 𝐿 } ) → ( { 𝐾 , 𝐿 } ∖ { 𝐼 } ) ≠ 𝐽 )
83 14 necomd ( 𝜑𝐽𝐼 )
84 83 ad2antrr ( ( ( 𝜑𝐼 ∈ { 𝐾 , 𝐿 } ) ∧ ¬ 𝐽 ∈ { 𝐾 , 𝐿 } ) → 𝐽𝐼 )
85 5 3 66 67 76 77 80 82 84 cycpm3cl2 ( ( ( 𝜑𝐼 ∈ { 𝐾 , 𝐿 } ) ∧ ¬ 𝐽 ∈ { 𝐾 , 𝐿 } ) → ( 𝑀 ‘ ⟨“ 𝐼 ( { 𝐾 , 𝐿 } ∖ { 𝐼 } ) 𝐽 ”⟩ ) ∈ ( 𝑀 “ ( ♯ “ { 3 } ) ) )
86 85 1 eleqtrrdi ( ( ( 𝜑𝐼 ∈ { 𝐾 , 𝐿 } ) ∧ ¬ 𝐽 ∈ { 𝐾 , 𝐿 } ) → ( 𝑀 ‘ ⟨“ 𝐼 ( { 𝐾 , 𝐿 } ∖ { 𝐼 } ) 𝐽 ”⟩ ) ∈ 𝐶 )
87 86 s1cld ( ( ( 𝜑𝐼 ∈ { 𝐾 , 𝐿 } ) ∧ ¬ 𝐽 ∈ { 𝐾 , 𝐿 } ) → ⟨“ ( 𝑀 ‘ ⟨“ 𝐼 ( { 𝐾 , 𝐿 } ∖ { 𝐼 } ) 𝐽 ”⟩ ) ”⟩ ∈ Word 𝐶 )
88 simpr ( ( ( ( 𝜑𝐼 ∈ { 𝐾 , 𝐿 } ) ∧ ¬ 𝐽 ∈ { 𝐾 , 𝐿 } ) ∧ 𝑐 = ⟨“ ( 𝑀 ‘ ⟨“ 𝐼 ( { 𝐾 , 𝐿 } ∖ { 𝐼 } ) 𝐽 ”⟩ ) ”⟩ ) → 𝑐 = ⟨“ ( 𝑀 ‘ ⟨“ 𝐼 ( { 𝐾 , 𝐿 } ∖ { 𝐼 } ) 𝐽 ”⟩ ) ”⟩ )
89 88 oveq2d ( ( ( ( 𝜑𝐼 ∈ { 𝐾 , 𝐿 } ) ∧ ¬ 𝐽 ∈ { 𝐾 , 𝐿 } ) ∧ 𝑐 = ⟨“ ( 𝑀 ‘ ⟨“ 𝐼 ( { 𝐾 , 𝐿 } ∖ { 𝐼 } ) 𝐽 ”⟩ ) ”⟩ ) → ( 𝑆 Σg 𝑐 ) = ( 𝑆 Σg ⟨“ ( 𝑀 ‘ ⟨“ 𝐼 ( { 𝐾 , 𝐿 } ∖ { 𝐼 } ) 𝐽 ”⟩ ) ”⟩ ) )
90 89 eqeq2d ( ( ( ( 𝜑𝐼 ∈ { 𝐾 , 𝐿 } ) ∧ ¬ 𝐽 ∈ { 𝐾 , 𝐿 } ) ∧ 𝑐 = ⟨“ ( 𝑀 ‘ ⟨“ 𝐼 ( { 𝐾 , 𝐿 } ∖ { 𝐼 } ) 𝐽 ”⟩ ) ”⟩ ) → ( ( 𝐸 · 𝐹 ) = ( 𝑆 Σg 𝑐 ) ↔ ( 𝐸 · 𝐹 ) = ( 𝑆 Σg ⟨“ ( 𝑀 ‘ ⟨“ 𝐼 ( { 𝐾 , 𝐿 } ∖ { 𝐼 } ) 𝐽 ”⟩ ) ”⟩ ) ) )
91 5 3 66 67 76 77 80 82 84 6 cyc3co2 ( ( ( 𝜑𝐼 ∈ { 𝐾 , 𝐿 } ) ∧ ¬ 𝐽 ∈ { 𝐾 , 𝐿 } ) → ( 𝑀 ‘ ⟨“ 𝐼 ( { 𝐾 , 𝐿 } ∖ { 𝐼 } ) 𝐽 ”⟩ ) = ( ( 𝑀 ‘ ⟨“ 𝐼 𝐽 ”⟩ ) · ( 𝑀 ‘ ⟨“ 𝐼 ( { 𝐾 , 𝐿 } ∖ { 𝐼 } ) ”⟩ ) ) )
92 5 3 66 67 76 77 80 82 84 cycpm3cl ( ( ( 𝜑𝐼 ∈ { 𝐾 , 𝐿 } ) ∧ ¬ 𝐽 ∈ { 𝐾 , 𝐿 } ) → ( 𝑀 ‘ ⟨“ 𝐼 ( { 𝐾 , 𝐿 } ∖ { 𝐼 } ) 𝐽 ”⟩ ) ∈ ( Base ‘ 𝑆 ) )
93 25 gsumws1 ( ( 𝑀 ‘ ⟨“ 𝐼 ( { 𝐾 , 𝐿 } ∖ { 𝐼 } ) 𝐽 ”⟩ ) ∈ ( Base ‘ 𝑆 ) → ( 𝑆 Σg ⟨“ ( 𝑀 ‘ ⟨“ 𝐼 ( { 𝐾 , 𝐿 } ∖ { 𝐼 } ) 𝐽 ”⟩ ) ”⟩ ) = ( 𝑀 ‘ ⟨“ 𝐼 ( { 𝐾 , 𝐿 } ∖ { 𝐼 } ) 𝐽 ”⟩ ) )
94 92 93 syl ( ( ( 𝜑𝐼 ∈ { 𝐾 , 𝐿 } ) ∧ ¬ 𝐽 ∈ { 𝐾 , 𝐿 } ) → ( 𝑆 Σg ⟨“ ( 𝑀 ‘ ⟨“ 𝐼 ( { 𝐾 , 𝐿 } ∖ { 𝐼 } ) 𝐽 ”⟩ ) ”⟩ ) = ( 𝑀 ‘ ⟨“ 𝐼 ( { 𝐾 , 𝐿 } ∖ { 𝐼 } ) 𝐽 ”⟩ ) )
95 11 ad2antrr ( ( ( 𝜑𝐼 ∈ { 𝐾 , 𝐿 } ) ∧ ¬ 𝐽 ∈ { 𝐾 , 𝐿 } ) → 𝐸 = ( 𝑀 ‘ ⟨“ 𝐼 𝐽 ”⟩ ) )
96 en2eleq ( ( 𝐼 ∈ { 𝐾 , 𝐿 } ∧ { 𝐾 , 𝐿 } ≈ 2o ) → { 𝐾 , 𝐿 } = { 𝐼 , ( { 𝐾 , 𝐿 } ∖ { 𝐼 } ) } )
97 70 73 96 syl2anc ( ( ( 𝜑𝐼 ∈ { 𝐾 , 𝐿 } ) ∧ ¬ 𝐽 ∈ { 𝐾 , 𝐿 } ) → { 𝐾 , 𝐿 } = { 𝐼 , ( { 𝐾 , 𝐿 } ∖ { 𝐼 } ) } )
98 97 fveq2d ( ( ( 𝜑𝐼 ∈ { 𝐾 , 𝐿 } ) ∧ ¬ 𝐽 ∈ { 𝐾 , 𝐿 } ) → ( ( pmTrsp ‘ 𝐷 ) ‘ { 𝐾 , 𝐿 } ) = ( ( pmTrsp ‘ 𝐷 ) ‘ { 𝐼 , ( { 𝐾 , 𝐿 } ∖ { 𝐼 } ) } ) )
99 12 34 eqtrd ( 𝜑𝐹 = ( ( pmTrsp ‘ 𝐷 ) ‘ { 𝐾 , 𝐿 } ) )
100 99 ad2antrr ( ( ( 𝜑𝐼 ∈ { 𝐾 , 𝐿 } ) ∧ ¬ 𝐽 ∈ { 𝐾 , 𝐿 } ) → 𝐹 = ( ( pmTrsp ‘ 𝐷 ) ‘ { 𝐾 , 𝐿 } ) )
101 5 66 67 76 80 30 cycpm2tr ( ( ( 𝜑𝐼 ∈ { 𝐾 , 𝐿 } ) ∧ ¬ 𝐽 ∈ { 𝐾 , 𝐿 } ) → ( 𝑀 ‘ ⟨“ 𝐼 ( { 𝐾 , 𝐿 } ∖ { 𝐼 } ) ”⟩ ) = ( ( pmTrsp ‘ 𝐷 ) ‘ { 𝐼 , ( { 𝐾 , 𝐿 } ∖ { 𝐼 } ) } ) )
102 98 100 101 3eqtr4d ( ( ( 𝜑𝐼 ∈ { 𝐾 , 𝐿 } ) ∧ ¬ 𝐽 ∈ { 𝐾 , 𝐿 } ) → 𝐹 = ( 𝑀 ‘ ⟨“ 𝐼 ( { 𝐾 , 𝐿 } ∖ { 𝐼 } ) ”⟩ ) )
103 95 102 oveq12d ( ( ( 𝜑𝐼 ∈ { 𝐾 , 𝐿 } ) ∧ ¬ 𝐽 ∈ { 𝐾 , 𝐿 } ) → ( 𝐸 · 𝐹 ) = ( ( 𝑀 ‘ ⟨“ 𝐼 𝐽 ”⟩ ) · ( 𝑀 ‘ ⟨“ 𝐼 ( { 𝐾 , 𝐿 } ∖ { 𝐼 } ) ”⟩ ) ) )
104 91 94 103 3eqtr4rd ( ( ( 𝜑𝐼 ∈ { 𝐾 , 𝐿 } ) ∧ ¬ 𝐽 ∈ { 𝐾 , 𝐿 } ) → ( 𝐸 · 𝐹 ) = ( 𝑆 Σg ⟨“ ( 𝑀 ‘ ⟨“ 𝐼 ( { 𝐾 , 𝐿 } ∖ { 𝐼 } ) 𝐽 ”⟩ ) ”⟩ ) )
105 87 90 104 rspcedvd ( ( ( 𝜑𝐼 ∈ { 𝐾 , 𝐿 } ) ∧ ¬ 𝐽 ∈ { 𝐾 , 𝐿 } ) → ∃ 𝑐 ∈ Word 𝐶 ( 𝐸 · 𝐹 ) = ( 𝑆 Σg 𝑐 ) )
106 65 105 pm2.61dan ( ( 𝜑𝐼 ∈ { 𝐾 , 𝐿 } ) → ∃ 𝑐 ∈ Word 𝐶 ( 𝐸 · 𝐹 ) = ( 𝑆 Σg 𝑐 ) )
107 13 ad2antrr ( ( ( 𝜑 ∧ ¬ 𝐼 ∈ { 𝐾 , 𝐿 } ) ∧ 𝐽 ∈ { 𝐾 , 𝐿 } ) → 𝐷𝑉 )
108 8 ad2antrr ( ( ( 𝜑 ∧ ¬ 𝐼 ∈ { 𝐾 , 𝐿 } ) ∧ 𝐽 ∈ { 𝐾 , 𝐿 } ) → 𝐽𝐷 )
109 68 ad2antrr ( ( ( 𝜑 ∧ ¬ 𝐼 ∈ { 𝐾 , 𝐿 } ) ∧ 𝐽 ∈ { 𝐾 , 𝐿 } ) → { 𝐾 , 𝐿 } ⊆ 𝐷 )
110 simpr ( ( ( 𝜑 ∧ ¬ 𝐼 ∈ { 𝐾 , 𝐿 } ) ∧ 𝐽 ∈ { 𝐾 , 𝐿 } ) → 𝐽 ∈ { 𝐾 , 𝐿 } )
111 72 ad2antrr ( ( ( 𝜑 ∧ ¬ 𝐼 ∈ { 𝐾 , 𝐿 } ) ∧ 𝐽 ∈ { 𝐾 , 𝐿 } ) → { 𝐾 , 𝐿 } ≈ 2o )
112 unidifsnel ( ( 𝐽 ∈ { 𝐾 , 𝐿 } ∧ { 𝐾 , 𝐿 } ≈ 2o ) → ( { 𝐾 , 𝐿 } ∖ { 𝐽 } ) ∈ { 𝐾 , 𝐿 } )
113 110 111 112 syl2anc ( ( ( 𝜑 ∧ ¬ 𝐼 ∈ { 𝐾 , 𝐿 } ) ∧ 𝐽 ∈ { 𝐾 , 𝐿 } ) → ( { 𝐾 , 𝐿 } ∖ { 𝐽 } ) ∈ { 𝐾 , 𝐿 } )
114 109 113 sseldd ( ( ( 𝜑 ∧ ¬ 𝐼 ∈ { 𝐾 , 𝐿 } ) ∧ 𝐽 ∈ { 𝐾 , 𝐿 } ) → ( { 𝐾 , 𝐿 } ∖ { 𝐽 } ) ∈ 𝐷 )
115 7 ad2antrr ( ( ( 𝜑 ∧ ¬ 𝐼 ∈ { 𝐾 , 𝐿 } ) ∧ 𝐽 ∈ { 𝐾 , 𝐿 } ) → 𝐼𝐷 )
116 unidifsnne ( ( 𝐽 ∈ { 𝐾 , 𝐿 } ∧ { 𝐾 , 𝐿 } ≈ 2o ) → ( { 𝐾 , 𝐿 } ∖ { 𝐽 } ) ≠ 𝐽 )
117 110 111 116 syl2anc ( ( ( 𝜑 ∧ ¬ 𝐼 ∈ { 𝐾 , 𝐿 } ) ∧ 𝐽 ∈ { 𝐾 , 𝐿 } ) → ( { 𝐾 , 𝐿 } ∖ { 𝐽 } ) ≠ 𝐽 )
118 117 necomd ( ( ( 𝜑 ∧ ¬ 𝐼 ∈ { 𝐾 , 𝐿 } ) ∧ 𝐽 ∈ { 𝐾 , 𝐿 } ) → 𝐽 ( { 𝐾 , 𝐿 } ∖ { 𝐽 } ) )
119 simplr ( ( ( 𝜑 ∧ ¬ 𝐼 ∈ { 𝐾 , 𝐿 } ) ∧ 𝐽 ∈ { 𝐾 , 𝐿 } ) → ¬ 𝐼 ∈ { 𝐾 , 𝐿 } )
120 nelne2 ( ( ( { 𝐾 , 𝐿 } ∖ { 𝐽 } ) ∈ { 𝐾 , 𝐿 } ∧ ¬ 𝐼 ∈ { 𝐾 , 𝐿 } ) → ( { 𝐾 , 𝐿 } ∖ { 𝐽 } ) ≠ 𝐼 )
121 113 119 120 syl2anc ( ( ( 𝜑 ∧ ¬ 𝐼 ∈ { 𝐾 , 𝐿 } ) ∧ 𝐽 ∈ { 𝐾 , 𝐿 } ) → ( { 𝐾 , 𝐿 } ∖ { 𝐽 } ) ≠ 𝐼 )
122 14 ad2antrr ( ( ( 𝜑 ∧ ¬ 𝐼 ∈ { 𝐾 , 𝐿 } ) ∧ 𝐽 ∈ { 𝐾 , 𝐿 } ) → 𝐼𝐽 )
123 5 3 107 108 114 115 118 121 122 cycpm3cl2 ( ( ( 𝜑 ∧ ¬ 𝐼 ∈ { 𝐾 , 𝐿 } ) ∧ 𝐽 ∈ { 𝐾 , 𝐿 } ) → ( 𝑀 ‘ ⟨“ 𝐽 ( { 𝐾 , 𝐿 } ∖ { 𝐽 } ) 𝐼 ”⟩ ) ∈ ( 𝑀 “ ( ♯ “ { 3 } ) ) )
124 123 1 eleqtrrdi ( ( ( 𝜑 ∧ ¬ 𝐼 ∈ { 𝐾 , 𝐿 } ) ∧ 𝐽 ∈ { 𝐾 , 𝐿 } ) → ( 𝑀 ‘ ⟨“ 𝐽 ( { 𝐾 , 𝐿 } ∖ { 𝐽 } ) 𝐼 ”⟩ ) ∈ 𝐶 )
125 124 s1cld ( ( ( 𝜑 ∧ ¬ 𝐼 ∈ { 𝐾 , 𝐿 } ) ∧ 𝐽 ∈ { 𝐾 , 𝐿 } ) → ⟨“ ( 𝑀 ‘ ⟨“ 𝐽 ( { 𝐾 , 𝐿 } ∖ { 𝐽 } ) 𝐼 ”⟩ ) ”⟩ ∈ Word 𝐶 )
126 simpr ( ( ( ( 𝜑 ∧ ¬ 𝐼 ∈ { 𝐾 , 𝐿 } ) ∧ 𝐽 ∈ { 𝐾 , 𝐿 } ) ∧ 𝑐 = ⟨“ ( 𝑀 ‘ ⟨“ 𝐽 ( { 𝐾 , 𝐿 } ∖ { 𝐽 } ) 𝐼 ”⟩ ) ”⟩ ) → 𝑐 = ⟨“ ( 𝑀 ‘ ⟨“ 𝐽 ( { 𝐾 , 𝐿 } ∖ { 𝐽 } ) 𝐼 ”⟩ ) ”⟩ )
127 126 oveq2d ( ( ( ( 𝜑 ∧ ¬ 𝐼 ∈ { 𝐾 , 𝐿 } ) ∧ 𝐽 ∈ { 𝐾 , 𝐿 } ) ∧ 𝑐 = ⟨“ ( 𝑀 ‘ ⟨“ 𝐽 ( { 𝐾 , 𝐿 } ∖ { 𝐽 } ) 𝐼 ”⟩ ) ”⟩ ) → ( 𝑆 Σg 𝑐 ) = ( 𝑆 Σg ⟨“ ( 𝑀 ‘ ⟨“ 𝐽 ( { 𝐾 , 𝐿 } ∖ { 𝐽 } ) 𝐼 ”⟩ ) ”⟩ ) )
128 127 eqeq2d ( ( ( ( 𝜑 ∧ ¬ 𝐼 ∈ { 𝐾 , 𝐿 } ) ∧ 𝐽 ∈ { 𝐾 , 𝐿 } ) ∧ 𝑐 = ⟨“ ( 𝑀 ‘ ⟨“ 𝐽 ( { 𝐾 , 𝐿 } ∖ { 𝐽 } ) 𝐼 ”⟩ ) ”⟩ ) → ( ( 𝐸 · 𝐹 ) = ( 𝑆 Σg 𝑐 ) ↔ ( 𝐸 · 𝐹 ) = ( 𝑆 Σg ⟨“ ( 𝑀 ‘ ⟨“ 𝐽 ( { 𝐾 , 𝐿 } ∖ { 𝐽 } ) 𝐼 ”⟩ ) ”⟩ ) ) )
129 5 3 107 108 114 115 118 121 122 6 cyc3co2 ( ( ( 𝜑 ∧ ¬ 𝐼 ∈ { 𝐾 , 𝐿 } ) ∧ 𝐽 ∈ { 𝐾 , 𝐿 } ) → ( 𝑀 ‘ ⟨“ 𝐽 ( { 𝐾 , 𝐿 } ∖ { 𝐽 } ) 𝐼 ”⟩ ) = ( ( 𝑀 ‘ ⟨“ 𝐽 𝐼 ”⟩ ) · ( 𝑀 ‘ ⟨“ 𝐽 ( { 𝐾 , 𝐿 } ∖ { 𝐽 } ) ”⟩ ) ) )
130 5 3 107 108 114 115 118 121 122 cycpm3cl ( ( ( 𝜑 ∧ ¬ 𝐼 ∈ { 𝐾 , 𝐿 } ) ∧ 𝐽 ∈ { 𝐾 , 𝐿 } ) → ( 𝑀 ‘ ⟨“ 𝐽 ( { 𝐾 , 𝐿 } ∖ { 𝐽 } ) 𝐼 ”⟩ ) ∈ ( Base ‘ 𝑆 ) )
131 25 gsumws1 ( ( 𝑀 ‘ ⟨“ 𝐽 ( { 𝐾 , 𝐿 } ∖ { 𝐽 } ) 𝐼 ”⟩ ) ∈ ( Base ‘ 𝑆 ) → ( 𝑆 Σg ⟨“ ( 𝑀 ‘ ⟨“ 𝐽 ( { 𝐾 , 𝐿 } ∖ { 𝐽 } ) 𝐼 ”⟩ ) ”⟩ ) = ( 𝑀 ‘ ⟨“ 𝐽 ( { 𝐾 , 𝐿 } ∖ { 𝐽 } ) 𝐼 ”⟩ ) )
132 130 131 syl ( ( ( 𝜑 ∧ ¬ 𝐼 ∈ { 𝐾 , 𝐿 } ) ∧ 𝐽 ∈ { 𝐾 , 𝐿 } ) → ( 𝑆 Σg ⟨“ ( 𝑀 ‘ ⟨“ 𝐽 ( { 𝐾 , 𝐿 } ∖ { 𝐽 } ) 𝐼 ”⟩ ) ”⟩ ) = ( 𝑀 ‘ ⟨“ 𝐽 ( { 𝐾 , 𝐿 } ∖ { 𝐽 } ) 𝐼 ”⟩ ) )
133 prcom { 𝐼 , 𝐽 } = { 𝐽 , 𝐼 }
134 133 fveq2i ( ( pmTrsp ‘ 𝐷 ) ‘ { 𝐼 , 𝐽 } ) = ( ( pmTrsp ‘ 𝐷 ) ‘ { 𝐽 , 𝐼 } )
135 5 13 8 7 83 30 cycpm2tr ( 𝜑 → ( 𝑀 ‘ ⟨“ 𝐽 𝐼 ”⟩ ) = ( ( pmTrsp ‘ 𝐷 ) ‘ { 𝐽 , 𝐼 } ) )
136 134 31 135 3eqtr4a ( 𝜑 → ( 𝑀 ‘ ⟨“ 𝐼 𝐽 ”⟩ ) = ( 𝑀 ‘ ⟨“ 𝐽 𝐼 ”⟩ ) )
137 11 136 eqtrd ( 𝜑𝐸 = ( 𝑀 ‘ ⟨“ 𝐽 𝐼 ”⟩ ) )
138 137 ad2antrr ( ( ( 𝜑 ∧ ¬ 𝐼 ∈ { 𝐾 , 𝐿 } ) ∧ 𝐽 ∈ { 𝐾 , 𝐿 } ) → 𝐸 = ( 𝑀 ‘ ⟨“ 𝐽 𝐼 ”⟩ ) )
139 en2eleq ( ( 𝐽 ∈ { 𝐾 , 𝐿 } ∧ { 𝐾 , 𝐿 } ≈ 2o ) → { 𝐾 , 𝐿 } = { 𝐽 , ( { 𝐾 , 𝐿 } ∖ { 𝐽 } ) } )
140 110 111 139 syl2anc ( ( ( 𝜑 ∧ ¬ 𝐼 ∈ { 𝐾 , 𝐿 } ) ∧ 𝐽 ∈ { 𝐾 , 𝐿 } ) → { 𝐾 , 𝐿 } = { 𝐽 , ( { 𝐾 , 𝐿 } ∖ { 𝐽 } ) } )
141 140 fveq2d ( ( ( 𝜑 ∧ ¬ 𝐼 ∈ { 𝐾 , 𝐿 } ) ∧ 𝐽 ∈ { 𝐾 , 𝐿 } ) → ( ( pmTrsp ‘ 𝐷 ) ‘ { 𝐾 , 𝐿 } ) = ( ( pmTrsp ‘ 𝐷 ) ‘ { 𝐽 , ( { 𝐾 , 𝐿 } ∖ { 𝐽 } ) } ) )
142 99 ad2antrr ( ( ( 𝜑 ∧ ¬ 𝐼 ∈ { 𝐾 , 𝐿 } ) ∧ 𝐽 ∈ { 𝐾 , 𝐿 } ) → 𝐹 = ( ( pmTrsp ‘ 𝐷 ) ‘ { 𝐾 , 𝐿 } ) )
143 5 107 108 114 118 30 cycpm2tr ( ( ( 𝜑 ∧ ¬ 𝐼 ∈ { 𝐾 , 𝐿 } ) ∧ 𝐽 ∈ { 𝐾 , 𝐿 } ) → ( 𝑀 ‘ ⟨“ 𝐽 ( { 𝐾 , 𝐿 } ∖ { 𝐽 } ) ”⟩ ) = ( ( pmTrsp ‘ 𝐷 ) ‘ { 𝐽 , ( { 𝐾 , 𝐿 } ∖ { 𝐽 } ) } ) )
144 141 142 143 3eqtr4d ( ( ( 𝜑 ∧ ¬ 𝐼 ∈ { 𝐾 , 𝐿 } ) ∧ 𝐽 ∈ { 𝐾 , 𝐿 } ) → 𝐹 = ( 𝑀 ‘ ⟨“ 𝐽 ( { 𝐾 , 𝐿 } ∖ { 𝐽 } ) ”⟩ ) )
145 138 144 oveq12d ( ( ( 𝜑 ∧ ¬ 𝐼 ∈ { 𝐾 , 𝐿 } ) ∧ 𝐽 ∈ { 𝐾 , 𝐿 } ) → ( 𝐸 · 𝐹 ) = ( ( 𝑀 ‘ ⟨“ 𝐽 𝐼 ”⟩ ) · ( 𝑀 ‘ ⟨“ 𝐽 ( { 𝐾 , 𝐿 } ∖ { 𝐽 } ) ”⟩ ) ) )
146 129 132 145 3eqtr4rd ( ( ( 𝜑 ∧ ¬ 𝐼 ∈ { 𝐾 , 𝐿 } ) ∧ 𝐽 ∈ { 𝐾 , 𝐿 } ) → ( 𝐸 · 𝐹 ) = ( 𝑆 Σg ⟨“ ( 𝑀 ‘ ⟨“ 𝐽 ( { 𝐾 , 𝐿 } ∖ { 𝐽 } ) 𝐼 ”⟩ ) ”⟩ ) )
147 125 128 146 rspcedvd ( ( ( 𝜑 ∧ ¬ 𝐼 ∈ { 𝐾 , 𝐿 } ) ∧ 𝐽 ∈ { 𝐾 , 𝐿 } ) → ∃ 𝑐 ∈ Word 𝐶 ( 𝐸 · 𝐹 ) = ( 𝑆 Σg 𝑐 ) )
148 13 ad2antrr ( ( ( 𝜑 ∧ ¬ 𝐼 ∈ { 𝐾 , 𝐿 } ) ∧ ¬ 𝐽 ∈ { 𝐾 , 𝐿 } ) → 𝐷𝑉 )
149 8 ad2antrr ( ( ( 𝜑 ∧ ¬ 𝐼 ∈ { 𝐾 , 𝐿 } ) ∧ ¬ 𝐽 ∈ { 𝐾 , 𝐿 } ) → 𝐽𝐷 )
150 9 ad2antrr ( ( ( 𝜑 ∧ ¬ 𝐼 ∈ { 𝐾 , 𝐿 } ) ∧ ¬ 𝐽 ∈ { 𝐾 , 𝐿 } ) → 𝐾𝐷 )
151 7 ad2antrr ( ( ( 𝜑 ∧ ¬ 𝐼 ∈ { 𝐾 , 𝐿 } ) ∧ ¬ 𝐽 ∈ { 𝐾 , 𝐿 } ) → 𝐼𝐷 )
152 simpr ( ( ( 𝜑 ∧ ¬ 𝐼 ∈ { 𝐾 , 𝐿 } ) ∧ ¬ 𝐽 ∈ { 𝐾 , 𝐿 } ) → ¬ 𝐽 ∈ { 𝐾 , 𝐿 } )
153 149 152 nelpr1 ( ( ( 𝜑 ∧ ¬ 𝐼 ∈ { 𝐾 , 𝐿 } ) ∧ ¬ 𝐽 ∈ { 𝐾 , 𝐿 } ) → 𝐽𝐾 )
154 prid1g ( 𝐾𝐷𝐾 ∈ { 𝐾 , 𝐿 } )
155 9 154 syl ( 𝜑𝐾 ∈ { 𝐾 , 𝐿 } )
156 155 ad2antrr ( ( ( 𝜑 ∧ ¬ 𝐼 ∈ { 𝐾 , 𝐿 } ) ∧ ¬ 𝐽 ∈ { 𝐾 , 𝐿 } ) → 𝐾 ∈ { 𝐾 , 𝐿 } )
157 simplr ( ( ( 𝜑 ∧ ¬ 𝐼 ∈ { 𝐾 , 𝐿 } ) ∧ ¬ 𝐽 ∈ { 𝐾 , 𝐿 } ) → ¬ 𝐼 ∈ { 𝐾 , 𝐿 } )
158 nelne2 ( ( 𝐾 ∈ { 𝐾 , 𝐿 } ∧ ¬ 𝐼 ∈ { 𝐾 , 𝐿 } ) → 𝐾𝐼 )
159 156 157 158 syl2anc ( ( ( 𝜑 ∧ ¬ 𝐼 ∈ { 𝐾 , 𝐿 } ) ∧ ¬ 𝐽 ∈ { 𝐾 , 𝐿 } ) → 𝐾𝐼 )
160 14 ad2antrr ( ( ( 𝜑 ∧ ¬ 𝐼 ∈ { 𝐾 , 𝐿 } ) ∧ ¬ 𝐽 ∈ { 𝐾 , 𝐿 } ) → 𝐼𝐽 )
161 5 3 148 149 150 151 153 159 160 cycpm3cl2 ( ( ( 𝜑 ∧ ¬ 𝐼 ∈ { 𝐾 , 𝐿 } ) ∧ ¬ 𝐽 ∈ { 𝐾 , 𝐿 } ) → ( 𝑀 ‘ ⟨“ 𝐽 𝐾 𝐼 ”⟩ ) ∈ ( 𝑀 “ ( ♯ “ { 3 } ) ) )
162 161 1 eleqtrrdi ( ( ( 𝜑 ∧ ¬ 𝐼 ∈ { 𝐾 , 𝐿 } ) ∧ ¬ 𝐽 ∈ { 𝐾 , 𝐿 } ) → ( 𝑀 ‘ ⟨“ 𝐽 𝐾 𝐼 ”⟩ ) ∈ 𝐶 )
163 10 ad2antrr ( ( ( 𝜑 ∧ ¬ 𝐼 ∈ { 𝐾 , 𝐿 } ) ∧ ¬ 𝐽 ∈ { 𝐾 , 𝐿 } ) → 𝐿𝐷 )
164 15 ad2antrr ( ( ( 𝜑 ∧ ¬ 𝐼 ∈ { 𝐾 , 𝐿 } ) ∧ ¬ 𝐽 ∈ { 𝐾 , 𝐿 } ) → 𝐾𝐿 )
165 prid2g ( 𝐿𝐷𝐿 ∈ { 𝐾 , 𝐿 } )
166 163 165 syl ( ( ( 𝜑 ∧ ¬ 𝐼 ∈ { 𝐾 , 𝐿 } ) ∧ ¬ 𝐽 ∈ { 𝐾 , 𝐿 } ) → 𝐿 ∈ { 𝐾 , 𝐿 } )
167 nelne2 ( ( 𝐿 ∈ { 𝐾 , 𝐿 } ∧ ¬ 𝐽 ∈ { 𝐾 , 𝐿 } ) → 𝐿𝐽 )
168 166 167 sylancom ( ( ( 𝜑 ∧ ¬ 𝐼 ∈ { 𝐾 , 𝐿 } ) ∧ ¬ 𝐽 ∈ { 𝐾 , 𝐿 } ) → 𝐿𝐽 )
169 5 3 148 150 163 149 164 168 153 cycpm3cl2 ( ( ( 𝜑 ∧ ¬ 𝐼 ∈ { 𝐾 , 𝐿 } ) ∧ ¬ 𝐽 ∈ { 𝐾 , 𝐿 } ) → ( 𝑀 ‘ ⟨“ 𝐾 𝐿 𝐽 ”⟩ ) ∈ ( 𝑀 “ ( ♯ “ { 3 } ) ) )
170 169 1 eleqtrrdi ( ( ( 𝜑 ∧ ¬ 𝐼 ∈ { 𝐾 , 𝐿 } ) ∧ ¬ 𝐽 ∈ { 𝐾 , 𝐿 } ) → ( 𝑀 ‘ ⟨“ 𝐾 𝐿 𝐽 ”⟩ ) ∈ 𝐶 )
171 162 170 s2cld ( ( ( 𝜑 ∧ ¬ 𝐼 ∈ { 𝐾 , 𝐿 } ) ∧ ¬ 𝐽 ∈ { 𝐾 , 𝐿 } ) → ⟨“ ( 𝑀 ‘ ⟨“ 𝐽 𝐾 𝐼 ”⟩ ) ( 𝑀 ‘ ⟨“ 𝐾 𝐿 𝐽 ”⟩ ) ”⟩ ∈ Word 𝐶 )
172 simpr ( ( ( ( 𝜑 ∧ ¬ 𝐼 ∈ { 𝐾 , 𝐿 } ) ∧ ¬ 𝐽 ∈ { 𝐾 , 𝐿 } ) ∧ 𝑐 = ⟨“ ( 𝑀 ‘ ⟨“ 𝐽 𝐾 𝐼 ”⟩ ) ( 𝑀 ‘ ⟨“ 𝐾 𝐿 𝐽 ”⟩ ) ”⟩ ) → 𝑐 = ⟨“ ( 𝑀 ‘ ⟨“ 𝐽 𝐾 𝐼 ”⟩ ) ( 𝑀 ‘ ⟨“ 𝐾 𝐿 𝐽 ”⟩ ) ”⟩ )
173 172 oveq2d ( ( ( ( 𝜑 ∧ ¬ 𝐼 ∈ { 𝐾 , 𝐿 } ) ∧ ¬ 𝐽 ∈ { 𝐾 , 𝐿 } ) ∧ 𝑐 = ⟨“ ( 𝑀 ‘ ⟨“ 𝐽 𝐾 𝐼 ”⟩ ) ( 𝑀 ‘ ⟨“ 𝐾 𝐿 𝐽 ”⟩ ) ”⟩ ) → ( 𝑆 Σg 𝑐 ) = ( 𝑆 Σg ⟨“ ( 𝑀 ‘ ⟨“ 𝐽 𝐾 𝐼 ”⟩ ) ( 𝑀 ‘ ⟨“ 𝐾 𝐿 𝐽 ”⟩ ) ”⟩ ) )
174 173 eqeq2d ( ( ( ( 𝜑 ∧ ¬ 𝐼 ∈ { 𝐾 , 𝐿 } ) ∧ ¬ 𝐽 ∈ { 𝐾 , 𝐿 } ) ∧ 𝑐 = ⟨“ ( 𝑀 ‘ ⟨“ 𝐽 𝐾 𝐼 ”⟩ ) ( 𝑀 ‘ ⟨“ 𝐾 𝐿 𝐽 ”⟩ ) ”⟩ ) → ( ( 𝐸 · 𝐹 ) = ( 𝑆 Σg 𝑐 ) ↔ ( 𝐸 · 𝐹 ) = ( 𝑆 Σg ⟨“ ( 𝑀 ‘ ⟨“ 𝐽 𝐾 𝐼 ”⟩ ) ( 𝑀 ‘ ⟨“ 𝐾 𝐿 𝐽 ”⟩ ) ”⟩ ) ) )
175 148 59 syl ( ( ( 𝜑 ∧ ¬ 𝐼 ∈ { 𝐾 , 𝐿 } ) ∧ ¬ 𝐽 ∈ { 𝐾 , 𝐿 } ) → ( I ↾ 𝐷 ) = ( 0g𝑆 ) )
176 175 oveq1d ( ( ( 𝜑 ∧ ¬ 𝐼 ∈ { 𝐾 , 𝐿 } ) ∧ ¬ 𝐽 ∈ { 𝐾 , 𝐿 } ) → ( ( I ↾ 𝐷 ) · ( 𝑀 ‘ ⟨“ 𝐾 𝐿 ”⟩ ) ) = ( ( 0g𝑆 ) · ( 𝑀 ‘ ⟨“ 𝐾 𝐿 ”⟩ ) ) )
177 3 symggrp ( 𝐷𝑉𝑆 ∈ Grp )
178 13 177 syl ( 𝜑𝑆 ∈ Grp )
179 178 ad2antrr ( ( ( 𝜑 ∧ ¬ 𝐼 ∈ { 𝐾 , 𝐿 } ) ∧ ¬ 𝐽 ∈ { 𝐾 , 𝐿 } ) → 𝑆 ∈ Grp )
180 23 ad2antrr ( ( ( 𝜑 ∧ ¬ 𝐼 ∈ { 𝐾 , 𝐿 } ) ∧ ¬ 𝐽 ∈ { 𝐾 , 𝐿 } ) → ( 𝑀 ‘ ⟨“ 𝐾 𝐿 ”⟩ ) ∈ ( Base ‘ 𝑆 ) )
181 25 6 61 grplid ( ( 𝑆 ∈ Grp ∧ ( 𝑀 ‘ ⟨“ 𝐾 𝐿 ”⟩ ) ∈ ( Base ‘ 𝑆 ) ) → ( ( 0g𝑆 ) · ( 𝑀 ‘ ⟨“ 𝐾 𝐿 ”⟩ ) ) = ( 𝑀 ‘ ⟨“ 𝐾 𝐿 ”⟩ ) )
182 179 180 181 syl2anc ( ( ( 𝜑 ∧ ¬ 𝐼 ∈ { 𝐾 , 𝐿 } ) ∧ ¬ 𝐽 ∈ { 𝐾 , 𝐿 } ) → ( ( 0g𝑆 ) · ( 𝑀 ‘ ⟨“ 𝐾 𝐿 ”⟩ ) ) = ( 𝑀 ‘ ⟨“ 𝐾 𝐿 ”⟩ ) )
183 176 182 eqtrd ( ( ( 𝜑 ∧ ¬ 𝐼 ∈ { 𝐾 , 𝐿 } ) ∧ ¬ 𝐽 ∈ { 𝐾 , 𝐿 } ) → ( ( I ↾ 𝐷 ) · ( 𝑀 ‘ ⟨“ 𝐾 𝐿 ”⟩ ) ) = ( 𝑀 ‘ ⟨“ 𝐾 𝐿 ”⟩ ) )
184 183 oveq2d ( ( ( 𝜑 ∧ ¬ 𝐼 ∈ { 𝐾 , 𝐿 } ) ∧ ¬ 𝐽 ∈ { 𝐾 , 𝐿 } ) → ( ( 𝑀 ‘ ⟨“ 𝐼 𝐽 ”⟩ ) · ( ( I ↾ 𝐷 ) · ( 𝑀 ‘ ⟨“ 𝐾 𝐿 ”⟩ ) ) ) = ( ( 𝑀 ‘ ⟨“ 𝐼 𝐽 ”⟩ ) · ( 𝑀 ‘ ⟨“ 𝐾 𝐿 ”⟩ ) ) )
185 21 ad2antrr ( ( ( 𝜑 ∧ ¬ 𝐼 ∈ { 𝐾 , 𝐿 } ) ∧ ¬ 𝐽 ∈ { 𝐾 , 𝐿 } ) → ( 𝑀 ‘ ⟨“ 𝐼 𝐽 ”⟩ ) ∈ ( Base ‘ 𝑆 ) )
186 5 148 149 150 153 30 cycpm2tr ( ( ( 𝜑 ∧ ¬ 𝐼 ∈ { 𝐾 , 𝐿 } ) ∧ ¬ 𝐽 ∈ { 𝐾 , 𝐿 } ) → ( 𝑀 ‘ ⟨“ 𝐽 𝐾 ”⟩ ) = ( ( pmTrsp ‘ 𝐷 ) ‘ { 𝐽 , 𝐾 } ) )
187 53 3 25 symgtrf ran ( pmTrsp ‘ 𝐷 ) ⊆ ( Base ‘ 𝑆 )
188 8 9 prssd ( 𝜑 → { 𝐽 , 𝐾 } ⊆ 𝐷 )
189 188 ad2antrr ( ( ( 𝜑 ∧ ¬ 𝐼 ∈ { 𝐾 , 𝐿 } ) ∧ ¬ 𝐽 ∈ { 𝐾 , 𝐿 } ) → { 𝐽 , 𝐾 } ⊆ 𝐷 )
190 pr2nelem ( ( 𝐽𝐷𝐾𝐷𝐽𝐾 ) → { 𝐽 , 𝐾 } ≈ 2o )
191 149 150 153 190 syl3anc ( ( ( 𝜑 ∧ ¬ 𝐼 ∈ { 𝐾 , 𝐿 } ) ∧ ¬ 𝐽 ∈ { 𝐾 , 𝐿 } ) → { 𝐽 , 𝐾 } ≈ 2o )
192 30 53 pmtrrn ( ( 𝐷𝑉 ∧ { 𝐽 , 𝐾 } ⊆ 𝐷 ∧ { 𝐽 , 𝐾 } ≈ 2o ) → ( ( pmTrsp ‘ 𝐷 ) ‘ { 𝐽 , 𝐾 } ) ∈ ran ( pmTrsp ‘ 𝐷 ) )
193 148 189 191 192 syl3anc ( ( ( 𝜑 ∧ ¬ 𝐼 ∈ { 𝐾 , 𝐿 } ) ∧ ¬ 𝐽 ∈ { 𝐾 , 𝐿 } ) → ( ( pmTrsp ‘ 𝐷 ) ‘ { 𝐽 , 𝐾 } ) ∈ ran ( pmTrsp ‘ 𝐷 ) )
194 187 193 sseldi ( ( ( 𝜑 ∧ ¬ 𝐼 ∈ { 𝐾 , 𝐿 } ) ∧ ¬ 𝐽 ∈ { 𝐾 , 𝐿 } ) → ( ( pmTrsp ‘ 𝐷 ) ‘ { 𝐽 , 𝐾 } ) ∈ ( Base ‘ 𝑆 ) )
195 186 194 eqeltrd ( ( ( 𝜑 ∧ ¬ 𝐼 ∈ { 𝐾 , 𝐿 } ) ∧ ¬ 𝐽 ∈ { 𝐾 , 𝐿 } ) → ( 𝑀 ‘ ⟨“ 𝐽 𝐾 ”⟩ ) ∈ ( Base ‘ 𝑆 ) )
196 153 necomd ( ( ( 𝜑 ∧ ¬ 𝐼 ∈ { 𝐾 , 𝐿 } ) ∧ ¬ 𝐽 ∈ { 𝐾 , 𝐿 } ) → 𝐾𝐽 )
197 5 148 150 149 196 30 cycpm2tr ( ( ( 𝜑 ∧ ¬ 𝐼 ∈ { 𝐾 , 𝐿 } ) ∧ ¬ 𝐽 ∈ { 𝐾 , 𝐿 } ) → ( 𝑀 ‘ ⟨“ 𝐾 𝐽 ”⟩ ) = ( ( pmTrsp ‘ 𝐷 ) ‘ { 𝐾 , 𝐽 } ) )
198 prcom { 𝐽 , 𝐾 } = { 𝐾 , 𝐽 }
199 198 a1i ( ( ( 𝜑 ∧ ¬ 𝐼 ∈ { 𝐾 , 𝐿 } ) ∧ ¬ 𝐽 ∈ { 𝐾 , 𝐿 } ) → { 𝐽 , 𝐾 } = { 𝐾 , 𝐽 } )
200 199 fveq2d ( ( ( 𝜑 ∧ ¬ 𝐼 ∈ { 𝐾 , 𝐿 } ) ∧ ¬ 𝐽 ∈ { 𝐾 , 𝐿 } ) → ( ( pmTrsp ‘ 𝐷 ) ‘ { 𝐽 , 𝐾 } ) = ( ( pmTrsp ‘ 𝐷 ) ‘ { 𝐾 , 𝐽 } ) )
201 197 200 eqtr4d ( ( ( 𝜑 ∧ ¬ 𝐼 ∈ { 𝐾 , 𝐿 } ) ∧ ¬ 𝐽 ∈ { 𝐾 , 𝐿 } ) → ( 𝑀 ‘ ⟨“ 𝐾 𝐽 ”⟩ ) = ( ( pmTrsp ‘ 𝐷 ) ‘ { 𝐽 , 𝐾 } ) )
202 201 194 eqeltrd ( ( ( 𝜑 ∧ ¬ 𝐼 ∈ { 𝐾 , 𝐿 } ) ∧ ¬ 𝐽 ∈ { 𝐾 , 𝐿 } ) → ( 𝑀 ‘ ⟨“ 𝐾 𝐽 ”⟩ ) ∈ ( Base ‘ 𝑆 ) )
203 25 6 grpcl ( ( 𝑆 ∈ Grp ∧ ( 𝑀 ‘ ⟨“ 𝐾 𝐽 ”⟩ ) ∈ ( Base ‘ 𝑆 ) ∧ ( 𝑀 ‘ ⟨“ 𝐾 𝐿 ”⟩ ) ∈ ( Base ‘ 𝑆 ) ) → ( ( 𝑀 ‘ ⟨“ 𝐾 𝐽 ”⟩ ) · ( 𝑀 ‘ ⟨“ 𝐾 𝐿 ”⟩ ) ) ∈ ( Base ‘ 𝑆 ) )
204 179 202 180 203 syl3anc ( ( ( 𝜑 ∧ ¬ 𝐼 ∈ { 𝐾 , 𝐿 } ) ∧ ¬ 𝐽 ∈ { 𝐾 , 𝐿 } ) → ( ( 𝑀 ‘ ⟨“ 𝐾 𝐽 ”⟩ ) · ( 𝑀 ‘ ⟨“ 𝐾 𝐿 ”⟩ ) ) ∈ ( Base ‘ 𝑆 ) )
205 25 6 grpass ( ( 𝑆 ∈ Grp ∧ ( ( 𝑀 ‘ ⟨“ 𝐼 𝐽 ”⟩ ) ∈ ( Base ‘ 𝑆 ) ∧ ( 𝑀 ‘ ⟨“ 𝐽 𝐾 ”⟩ ) ∈ ( Base ‘ 𝑆 ) ∧ ( ( 𝑀 ‘ ⟨“ 𝐾 𝐽 ”⟩ ) · ( 𝑀 ‘ ⟨“ 𝐾 𝐿 ”⟩ ) ) ∈ ( Base ‘ 𝑆 ) ) ) → ( ( ( 𝑀 ‘ ⟨“ 𝐼 𝐽 ”⟩ ) · ( 𝑀 ‘ ⟨“ 𝐽 𝐾 ”⟩ ) ) · ( ( 𝑀 ‘ ⟨“ 𝐾 𝐽 ”⟩ ) · ( 𝑀 ‘ ⟨“ 𝐾 𝐿 ”⟩ ) ) ) = ( ( 𝑀 ‘ ⟨“ 𝐼 𝐽 ”⟩ ) · ( ( 𝑀 ‘ ⟨“ 𝐽 𝐾 ”⟩ ) · ( ( 𝑀 ‘ ⟨“ 𝐾 𝐽 ”⟩ ) · ( 𝑀 ‘ ⟨“ 𝐾 𝐿 ”⟩ ) ) ) ) )
206 179 185 195 204 205 syl13anc ( ( ( 𝜑 ∧ ¬ 𝐼 ∈ { 𝐾 , 𝐿 } ) ∧ ¬ 𝐽 ∈ { 𝐾 , 𝐿 } ) → ( ( ( 𝑀 ‘ ⟨“ 𝐼 𝐽 ”⟩ ) · ( 𝑀 ‘ ⟨“ 𝐽 𝐾 ”⟩ ) ) · ( ( 𝑀 ‘ ⟨“ 𝐾 𝐽 ”⟩ ) · ( 𝑀 ‘ ⟨“ 𝐾 𝐿 ”⟩ ) ) ) = ( ( 𝑀 ‘ ⟨“ 𝐼 𝐽 ”⟩ ) · ( ( 𝑀 ‘ ⟨“ 𝐽 𝐾 ”⟩ ) · ( ( 𝑀 ‘ ⟨“ 𝐾 𝐽 ”⟩ ) · ( 𝑀 ‘ ⟨“ 𝐾 𝐿 ”⟩ ) ) ) ) )
207 25 6 grpass ( ( 𝑆 ∈ Grp ∧ ( ( 𝑀 ‘ ⟨“ 𝐽 𝐾 ”⟩ ) ∈ ( Base ‘ 𝑆 ) ∧ ( 𝑀 ‘ ⟨“ 𝐾 𝐽 ”⟩ ) ∈ ( Base ‘ 𝑆 ) ∧ ( 𝑀 ‘ ⟨“ 𝐾 𝐿 ”⟩ ) ∈ ( Base ‘ 𝑆 ) ) ) → ( ( ( 𝑀 ‘ ⟨“ 𝐽 𝐾 ”⟩ ) · ( 𝑀 ‘ ⟨“ 𝐾 𝐽 ”⟩ ) ) · ( 𝑀 ‘ ⟨“ 𝐾 𝐿 ”⟩ ) ) = ( ( 𝑀 ‘ ⟨“ 𝐽 𝐾 ”⟩ ) · ( ( 𝑀 ‘ ⟨“ 𝐾 𝐽 ”⟩ ) · ( 𝑀 ‘ ⟨“ 𝐾 𝐿 ”⟩ ) ) ) )
208 179 195 202 180 207 syl13anc ( ( ( 𝜑 ∧ ¬ 𝐼 ∈ { 𝐾 , 𝐿 } ) ∧ ¬ 𝐽 ∈ { 𝐾 , 𝐿 } ) → ( ( ( 𝑀 ‘ ⟨“ 𝐽 𝐾 ”⟩ ) · ( 𝑀 ‘ ⟨“ 𝐾 𝐽 ”⟩ ) ) · ( 𝑀 ‘ ⟨“ 𝐾 𝐿 ”⟩ ) ) = ( ( 𝑀 ‘ ⟨“ 𝐽 𝐾 ”⟩ ) · ( ( 𝑀 ‘ ⟨“ 𝐾 𝐽 ”⟩ ) · ( 𝑀 ‘ ⟨“ 𝐾 𝐿 ”⟩ ) ) ) )
209 208 oveq2d ( ( ( 𝜑 ∧ ¬ 𝐼 ∈ { 𝐾 , 𝐿 } ) ∧ ¬ 𝐽 ∈ { 𝐾 , 𝐿 } ) → ( ( 𝑀 ‘ ⟨“ 𝐼 𝐽 ”⟩ ) · ( ( ( 𝑀 ‘ ⟨“ 𝐽 𝐾 ”⟩ ) · ( 𝑀 ‘ ⟨“ 𝐾 𝐽 ”⟩ ) ) · ( 𝑀 ‘ ⟨“ 𝐾 𝐿 ”⟩ ) ) ) = ( ( 𝑀 ‘ ⟨“ 𝐼 𝐽 ”⟩ ) · ( ( 𝑀 ‘ ⟨“ 𝐽 𝐾 ”⟩ ) · ( ( 𝑀 ‘ ⟨“ 𝐾 𝐽 ”⟩ ) · ( 𝑀 ‘ ⟨“ 𝐾 𝐿 ”⟩ ) ) ) ) )
210 186 201 oveq12d ( ( ( 𝜑 ∧ ¬ 𝐼 ∈ { 𝐾 , 𝐿 } ) ∧ ¬ 𝐽 ∈ { 𝐾 , 𝐿 } ) → ( ( 𝑀 ‘ ⟨“ 𝐽 𝐾 ”⟩ ) · ( 𝑀 ‘ ⟨“ 𝐾 𝐽 ”⟩ ) ) = ( ( ( pmTrsp ‘ 𝐷 ) ‘ { 𝐽 , 𝐾 } ) · ( ( pmTrsp ‘ 𝐷 ) ‘ { 𝐽 , 𝐾 } ) ) )
211 3 25 6 symgov ( ( ( ( pmTrsp ‘ 𝐷 ) ‘ { 𝐽 , 𝐾 } ) ∈ ( Base ‘ 𝑆 ) ∧ ( ( pmTrsp ‘ 𝐷 ) ‘ { 𝐽 , 𝐾 } ) ∈ ( Base ‘ 𝑆 ) ) → ( ( ( pmTrsp ‘ 𝐷 ) ‘ { 𝐽 , 𝐾 } ) · ( ( pmTrsp ‘ 𝐷 ) ‘ { 𝐽 , 𝐾 } ) ) = ( ( ( pmTrsp ‘ 𝐷 ) ‘ { 𝐽 , 𝐾 } ) ∘ ( ( pmTrsp ‘ 𝐷 ) ‘ { 𝐽 , 𝐾 } ) ) )
212 194 194 211 syl2anc ( ( ( 𝜑 ∧ ¬ 𝐼 ∈ { 𝐾 , 𝐿 } ) ∧ ¬ 𝐽 ∈ { 𝐾 , 𝐿 } ) → ( ( ( pmTrsp ‘ 𝐷 ) ‘ { 𝐽 , 𝐾 } ) · ( ( pmTrsp ‘ 𝐷 ) ‘ { 𝐽 , 𝐾 } ) ) = ( ( ( pmTrsp ‘ 𝐷 ) ‘ { 𝐽 , 𝐾 } ) ∘ ( ( pmTrsp ‘ 𝐷 ) ‘ { 𝐽 , 𝐾 } ) ) )
213 30 53 pmtrfinv ( ( ( pmTrsp ‘ 𝐷 ) ‘ { 𝐽 , 𝐾 } ) ∈ ran ( pmTrsp ‘ 𝐷 ) → ( ( ( pmTrsp ‘ 𝐷 ) ‘ { 𝐽 , 𝐾 } ) ∘ ( ( pmTrsp ‘ 𝐷 ) ‘ { 𝐽 , 𝐾 } ) ) = ( I ↾ 𝐷 ) )
214 193 213 syl ( ( ( 𝜑 ∧ ¬ 𝐼 ∈ { 𝐾 , 𝐿 } ) ∧ ¬ 𝐽 ∈ { 𝐾 , 𝐿 } ) → ( ( ( pmTrsp ‘ 𝐷 ) ‘ { 𝐽 , 𝐾 } ) ∘ ( ( pmTrsp ‘ 𝐷 ) ‘ { 𝐽 , 𝐾 } ) ) = ( I ↾ 𝐷 ) )
215 210 212 214 3eqtrd ( ( ( 𝜑 ∧ ¬ 𝐼 ∈ { 𝐾 , 𝐿 } ) ∧ ¬ 𝐽 ∈ { 𝐾 , 𝐿 } ) → ( ( 𝑀 ‘ ⟨“ 𝐽 𝐾 ”⟩ ) · ( 𝑀 ‘ ⟨“ 𝐾 𝐽 ”⟩ ) ) = ( I ↾ 𝐷 ) )
216 215 oveq1d ( ( ( 𝜑 ∧ ¬ 𝐼 ∈ { 𝐾 , 𝐿 } ) ∧ ¬ 𝐽 ∈ { 𝐾 , 𝐿 } ) → ( ( ( 𝑀 ‘ ⟨“ 𝐽 𝐾 ”⟩ ) · ( 𝑀 ‘ ⟨“ 𝐾 𝐽 ”⟩ ) ) · ( 𝑀 ‘ ⟨“ 𝐾 𝐿 ”⟩ ) ) = ( ( I ↾ 𝐷 ) · ( 𝑀 ‘ ⟨“ 𝐾 𝐿 ”⟩ ) ) )
217 216 oveq2d ( ( ( 𝜑 ∧ ¬ 𝐼 ∈ { 𝐾 , 𝐿 } ) ∧ ¬ 𝐽 ∈ { 𝐾 , 𝐿 } ) → ( ( 𝑀 ‘ ⟨“ 𝐼 𝐽 ”⟩ ) · ( ( ( 𝑀 ‘ ⟨“ 𝐽 𝐾 ”⟩ ) · ( 𝑀 ‘ ⟨“ 𝐾 𝐽 ”⟩ ) ) · ( 𝑀 ‘ ⟨“ 𝐾 𝐿 ”⟩ ) ) ) = ( ( 𝑀 ‘ ⟨“ 𝐼 𝐽 ”⟩ ) · ( ( I ↾ 𝐷 ) · ( 𝑀 ‘ ⟨“ 𝐾 𝐿 ”⟩ ) ) ) )
218 206 209 217 3eqtr2rd ( ( ( 𝜑 ∧ ¬ 𝐼 ∈ { 𝐾 , 𝐿 } ) ∧ ¬ 𝐽 ∈ { 𝐾 , 𝐿 } ) → ( ( 𝑀 ‘ ⟨“ 𝐼 𝐽 ”⟩ ) · ( ( I ↾ 𝐷 ) · ( 𝑀 ‘ ⟨“ 𝐾 𝐿 ”⟩ ) ) ) = ( ( ( 𝑀 ‘ ⟨“ 𝐼 𝐽 ”⟩ ) · ( 𝑀 ‘ ⟨“ 𝐽 𝐾 ”⟩ ) ) · ( ( 𝑀 ‘ ⟨“ 𝐾 𝐽 ”⟩ ) · ( 𝑀 ‘ ⟨“ 𝐾 𝐿 ”⟩ ) ) ) )
219 184 218 eqtr3d ( ( ( 𝜑 ∧ ¬ 𝐼 ∈ { 𝐾 , 𝐿 } ) ∧ ¬ 𝐽 ∈ { 𝐾 , 𝐿 } ) → ( ( 𝑀 ‘ ⟨“ 𝐼 𝐽 ”⟩ ) · ( 𝑀 ‘ ⟨“ 𝐾 𝐿 ”⟩ ) ) = ( ( ( 𝑀 ‘ ⟨“ 𝐼 𝐽 ”⟩ ) · ( 𝑀 ‘ ⟨“ 𝐽 𝐾 ”⟩ ) ) · ( ( 𝑀 ‘ ⟨“ 𝐾 𝐽 ”⟩ ) · ( 𝑀 ‘ ⟨“ 𝐾 𝐿 ”⟩ ) ) ) )
220 11 12 oveq12d ( 𝜑 → ( 𝐸 · 𝐹 ) = ( ( 𝑀 ‘ ⟨“ 𝐼 𝐽 ”⟩ ) · ( 𝑀 ‘ ⟨“ 𝐾 𝐿 ”⟩ ) ) )
221 220 ad2antrr ( ( ( 𝜑 ∧ ¬ 𝐼 ∈ { 𝐾 , 𝐿 } ) ∧ ¬ 𝐽 ∈ { 𝐾 , 𝐿 } ) → ( 𝐸 · 𝐹 ) = ( ( 𝑀 ‘ ⟨“ 𝐼 𝐽 ”⟩ ) · ( 𝑀 ‘ ⟨“ 𝐾 𝐿 ”⟩ ) ) )
222 5 3 148 149 150 151 153 159 160 6 cyc3co2 ( ( ( 𝜑 ∧ ¬ 𝐼 ∈ { 𝐾 , 𝐿 } ) ∧ ¬ 𝐽 ∈ { 𝐾 , 𝐿 } ) → ( 𝑀 ‘ ⟨“ 𝐽 𝐾 𝐼 ”⟩ ) = ( ( 𝑀 ‘ ⟨“ 𝐽 𝐼 ”⟩ ) · ( 𝑀 ‘ ⟨“ 𝐽 𝐾 ”⟩ ) ) )
223 136 oveq1d ( 𝜑 → ( ( 𝑀 ‘ ⟨“ 𝐼 𝐽 ”⟩ ) · ( 𝑀 ‘ ⟨“ 𝐽 𝐾 ”⟩ ) ) = ( ( 𝑀 ‘ ⟨“ 𝐽 𝐼 ”⟩ ) · ( 𝑀 ‘ ⟨“ 𝐽 𝐾 ”⟩ ) ) )
224 223 ad2antrr ( ( ( 𝜑 ∧ ¬ 𝐼 ∈ { 𝐾 , 𝐿 } ) ∧ ¬ 𝐽 ∈ { 𝐾 , 𝐿 } ) → ( ( 𝑀 ‘ ⟨“ 𝐼 𝐽 ”⟩ ) · ( 𝑀 ‘ ⟨“ 𝐽 𝐾 ”⟩ ) ) = ( ( 𝑀 ‘ ⟨“ 𝐽 𝐼 ”⟩ ) · ( 𝑀 ‘ ⟨“ 𝐽 𝐾 ”⟩ ) ) )
225 222 224 eqtr4d ( ( ( 𝜑 ∧ ¬ 𝐼 ∈ { 𝐾 , 𝐿 } ) ∧ ¬ 𝐽 ∈ { 𝐾 , 𝐿 } ) → ( 𝑀 ‘ ⟨“ 𝐽 𝐾 𝐼 ”⟩ ) = ( ( 𝑀 ‘ ⟨“ 𝐼 𝐽 ”⟩ ) · ( 𝑀 ‘ ⟨“ 𝐽 𝐾 ”⟩ ) ) )
226 5 3 148 150 163 149 164 168 153 6 cyc3co2 ( ( ( 𝜑 ∧ ¬ 𝐼 ∈ { 𝐾 , 𝐿 } ) ∧ ¬ 𝐽 ∈ { 𝐾 , 𝐿 } ) → ( 𝑀 ‘ ⟨“ 𝐾 𝐿 𝐽 ”⟩ ) = ( ( 𝑀 ‘ ⟨“ 𝐾 𝐽 ”⟩ ) · ( 𝑀 ‘ ⟨“ 𝐾 𝐿 ”⟩ ) ) )
227 225 226 oveq12d ( ( ( 𝜑 ∧ ¬ 𝐼 ∈ { 𝐾 , 𝐿 } ) ∧ ¬ 𝐽 ∈ { 𝐾 , 𝐿 } ) → ( ( 𝑀 ‘ ⟨“ 𝐽 𝐾 𝐼 ”⟩ ) · ( 𝑀 ‘ ⟨“ 𝐾 𝐿 𝐽 ”⟩ ) ) = ( ( ( 𝑀 ‘ ⟨“ 𝐼 𝐽 ”⟩ ) · ( 𝑀 ‘ ⟨“ 𝐽 𝐾 ”⟩ ) ) · ( ( 𝑀 ‘ ⟨“ 𝐾 𝐽 ”⟩ ) · ( 𝑀 ‘ ⟨“ 𝐾 𝐿 ”⟩ ) ) ) )
228 219 221 227 3eqtr4d ( ( ( 𝜑 ∧ ¬ 𝐼 ∈ { 𝐾 , 𝐿 } ) ∧ ¬ 𝐽 ∈ { 𝐾 , 𝐿 } ) → ( 𝐸 · 𝐹 ) = ( ( 𝑀 ‘ ⟨“ 𝐽 𝐾 𝐼 ”⟩ ) · ( 𝑀 ‘ ⟨“ 𝐾 𝐿 𝐽 ”⟩ ) ) )
229 178 grpmndd ( 𝜑𝑆 ∈ Mnd )
230 229 ad2antrr ( ( ( 𝜑 ∧ ¬ 𝐼 ∈ { 𝐾 , 𝐿 } ) ∧ ¬ 𝐽 ∈ { 𝐾 , 𝐿 } ) → 𝑆 ∈ Mnd )
231 5 3 148 149 150 151 153 159 160 cycpm3cl ( ( ( 𝜑 ∧ ¬ 𝐼 ∈ { 𝐾 , 𝐿 } ) ∧ ¬ 𝐽 ∈ { 𝐾 , 𝐿 } ) → ( 𝑀 ‘ ⟨“ 𝐽 𝐾 𝐼 ”⟩ ) ∈ ( Base ‘ 𝑆 ) )
232 226 204 eqeltrd ( ( ( 𝜑 ∧ ¬ 𝐼 ∈ { 𝐾 , 𝐿 } ) ∧ ¬ 𝐽 ∈ { 𝐾 , 𝐿 } ) → ( 𝑀 ‘ ⟨“ 𝐾 𝐿 𝐽 ”⟩ ) ∈ ( Base ‘ 𝑆 ) )
233 25 6 gsumws2 ( ( 𝑆 ∈ Mnd ∧ ( 𝑀 ‘ ⟨“ 𝐽 𝐾 𝐼 ”⟩ ) ∈ ( Base ‘ 𝑆 ) ∧ ( 𝑀 ‘ ⟨“ 𝐾 𝐿 𝐽 ”⟩ ) ∈ ( Base ‘ 𝑆 ) ) → ( 𝑆 Σg ⟨“ ( 𝑀 ‘ ⟨“ 𝐽 𝐾 𝐼 ”⟩ ) ( 𝑀 ‘ ⟨“ 𝐾 𝐿 𝐽 ”⟩ ) ”⟩ ) = ( ( 𝑀 ‘ ⟨“ 𝐽 𝐾 𝐼 ”⟩ ) · ( 𝑀 ‘ ⟨“ 𝐾 𝐿 𝐽 ”⟩ ) ) )
234 230 231 232 233 syl3anc ( ( ( 𝜑 ∧ ¬ 𝐼 ∈ { 𝐾 , 𝐿 } ) ∧ ¬ 𝐽 ∈ { 𝐾 , 𝐿 } ) → ( 𝑆 Σg ⟨“ ( 𝑀 ‘ ⟨“ 𝐽 𝐾 𝐼 ”⟩ ) ( 𝑀 ‘ ⟨“ 𝐾 𝐿 𝐽 ”⟩ ) ”⟩ ) = ( ( 𝑀 ‘ ⟨“ 𝐽 𝐾 𝐼 ”⟩ ) · ( 𝑀 ‘ ⟨“ 𝐾 𝐿 𝐽 ”⟩ ) ) )
235 228 234 eqtr4d ( ( ( 𝜑 ∧ ¬ 𝐼 ∈ { 𝐾 , 𝐿 } ) ∧ ¬ 𝐽 ∈ { 𝐾 , 𝐿 } ) → ( 𝐸 · 𝐹 ) = ( 𝑆 Σg ⟨“ ( 𝑀 ‘ ⟨“ 𝐽 𝐾 𝐼 ”⟩ ) ( 𝑀 ‘ ⟨“ 𝐾 𝐿 𝐽 ”⟩ ) ”⟩ ) )
236 171 174 235 rspcedvd ( ( ( 𝜑 ∧ ¬ 𝐼 ∈ { 𝐾 , 𝐿 } ) ∧ ¬ 𝐽 ∈ { 𝐾 , 𝐿 } ) → ∃ 𝑐 ∈ Word 𝐶 ( 𝐸 · 𝐹 ) = ( 𝑆 Σg 𝑐 ) )
237 147 236 pm2.61dan ( ( 𝜑 ∧ ¬ 𝐼 ∈ { 𝐾 , 𝐿 } ) → ∃ 𝑐 ∈ Word 𝐶 ( 𝐸 · 𝐹 ) = ( 𝑆 Σg 𝑐 ) )
238 106 237 pm2.61dan ( 𝜑 → ∃ 𝑐 ∈ Word 𝐶 ( 𝐸 · 𝐹 ) = ( 𝑆 Σg 𝑐 ) )