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 enpr2 ⊢ ( ( 𝐼 ∈ 𝐷 ∧ 𝐽 ∈ 𝐷 ∧ 𝐼 ≠ 𝐽 ) → { 𝐼 , 𝐽 } ≈ 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 enpr2 ⊢ ( ( 𝐾 ∈ 𝐷 ∧ 𝐿 ∈ 𝐷 ∧ 𝐾 ≠ 𝐿 ) → { 𝐾 , 𝐿 } ≈ 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 enpr2 ⊢ ( ( 𝐽 ∈ 𝐷 ∧ 𝐾 ∈ 𝐷 ∧ 𝐽 ≠ 𝐾 ) → { 𝐽 , 𝐾 } ≈ 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 sselid ⊢ ( ( ( 𝜑 ∧ ¬ 𝐼 ∈ { 𝐾 , 𝐿 } ) ∧ ¬ 𝐽 ∈ { 𝐾 , 𝐿 } ) → ( ( 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 𝑐 ) )