Metamath Proof Explorer


Theorem cyc3conja

Description: All 3-cycles are conjugate in the alternating group A_n for n>= 5. Property (b) of Lang p. 32. (Contributed by Thierry Arnoux, 15-Oct-2023)

Ref Expression
Hypotheses cyc3conja.c 𝐶 = ( 𝑀 “ ( ♯ “ { 3 } ) )
cyc3conja.a 𝐴 = ( pmEven ‘ 𝐷 )
cyc3conja.s 𝑆 = ( SymGrp ‘ 𝐷 )
cyc3conja.n 𝑁 = ( ♯ ‘ 𝐷 )
cyc3conja.m 𝑀 = ( toCyc ‘ 𝐷 )
cyc3conja.p + = ( +g𝑆 )
cyc3conja.l = ( -g𝑆 )
cyc3conja.1 ( 𝜑 → 5 ≤ 𝑁 )
cyc3conja.d ( 𝜑𝐷 ∈ Fin )
cyc3conja.q ( 𝜑𝑄𝐶 )
cyc3conja.t ( 𝜑𝑇𝐶 )
Assertion cyc3conja ( 𝜑 → ∃ 𝑝𝐴 𝑄 = ( ( 𝑝 + 𝑇 ) 𝑝 ) )

Proof

Step Hyp Ref Expression
1 cyc3conja.c 𝐶 = ( 𝑀 “ ( ♯ “ { 3 } ) )
2 cyc3conja.a 𝐴 = ( pmEven ‘ 𝐷 )
3 cyc3conja.s 𝑆 = ( SymGrp ‘ 𝐷 )
4 cyc3conja.n 𝑁 = ( ♯ ‘ 𝐷 )
5 cyc3conja.m 𝑀 = ( toCyc ‘ 𝐷 )
6 cyc3conja.p + = ( +g𝑆 )
7 cyc3conja.l = ( -g𝑆 )
8 cyc3conja.1 ( 𝜑 → 5 ≤ 𝑁 )
9 cyc3conja.d ( 𝜑𝐷 ∈ Fin )
10 cyc3conja.q ( 𝜑𝑄𝐶 )
11 cyc3conja.t ( 𝜑𝑇𝐶 )
12 simpr ( ( ( ( 𝜑𝑔 ∈ ( Base ‘ 𝑆 ) ) ∧ 𝑄 = ( ( 𝑔 + 𝑇 ) 𝑔 ) ) ∧ 𝑔𝐴 ) → 𝑔𝐴 )
13 simpr ( ( ( ( ( 𝜑𝑔 ∈ ( Base ‘ 𝑆 ) ) ∧ 𝑄 = ( ( 𝑔 + 𝑇 ) 𝑔 ) ) ∧ 𝑔𝐴 ) ∧ 𝑝 = 𝑔 ) → 𝑝 = 𝑔 )
14 13 oveq1d ( ( ( ( ( 𝜑𝑔 ∈ ( Base ‘ 𝑆 ) ) ∧ 𝑄 = ( ( 𝑔 + 𝑇 ) 𝑔 ) ) ∧ 𝑔𝐴 ) ∧ 𝑝 = 𝑔 ) → ( 𝑝 + 𝑇 ) = ( 𝑔 + 𝑇 ) )
15 14 13 oveq12d ( ( ( ( ( 𝜑𝑔 ∈ ( Base ‘ 𝑆 ) ) ∧ 𝑄 = ( ( 𝑔 + 𝑇 ) 𝑔 ) ) ∧ 𝑔𝐴 ) ∧ 𝑝 = 𝑔 ) → ( ( 𝑝 + 𝑇 ) 𝑝 ) = ( ( 𝑔 + 𝑇 ) 𝑔 ) )
16 15 eqeq2d ( ( ( ( ( 𝜑𝑔 ∈ ( Base ‘ 𝑆 ) ) ∧ 𝑄 = ( ( 𝑔 + 𝑇 ) 𝑔 ) ) ∧ 𝑔𝐴 ) ∧ 𝑝 = 𝑔 ) → ( 𝑄 = ( ( 𝑝 + 𝑇 ) 𝑝 ) ↔ 𝑄 = ( ( 𝑔 + 𝑇 ) 𝑔 ) ) )
17 simplr ( ( ( ( 𝜑𝑔 ∈ ( Base ‘ 𝑆 ) ) ∧ 𝑄 = ( ( 𝑔 + 𝑇 ) 𝑔 ) ) ∧ 𝑔𝐴 ) → 𝑄 = ( ( 𝑔 + 𝑇 ) 𝑔 ) )
18 12 16 17 rspcedvd ( ( ( ( 𝜑𝑔 ∈ ( Base ‘ 𝑆 ) ) ∧ 𝑄 = ( ( 𝑔 + 𝑇 ) 𝑔 ) ) ∧ 𝑔𝐴 ) → ∃ 𝑝𝐴 𝑄 = ( ( 𝑝 + 𝑇 ) 𝑝 ) )
19 9 ad5antr ( ( ( ( ( ( 𝜑𝑔 ∈ ( Base ‘ 𝑆 ) ) ∧ 𝑄 = ( ( 𝑔 + 𝑇 ) 𝑔 ) ) ∧ ¬ 𝑔𝐴 ) ∧ 𝑢 ∈ ( { 𝑤 ∈ Word 𝐷𝑤 : dom 𝑤1-1𝐷 } ∩ ( ♯ “ { 3 } ) ) ) ∧ ( 𝑀𝑢 ) = 𝑇 ) → 𝐷 ∈ Fin )
20 19 ad3antrrr ( ( ( ( ( ( ( ( ( 𝜑𝑔 ∈ ( Base ‘ 𝑆 ) ) ∧ 𝑄 = ( ( 𝑔 + 𝑇 ) 𝑔 ) ) ∧ ¬ 𝑔𝐴 ) ∧ 𝑢 ∈ ( { 𝑤 ∈ Word 𝐷𝑤 : dom 𝑤1-1𝐷 } ∩ ( ♯ “ { 3 } ) ) ) ∧ ( 𝑀𝑢 ) = 𝑇 ) ∧ 𝑥 ∈ ( 𝐷 ∖ ran 𝑢 ) ) ∧ 𝑦 ∈ ( 𝐷 ∖ ran 𝑢 ) ) ∧ 𝑥𝑦 ) → 𝐷 ∈ Fin )
21 simp-8r ( ( ( ( ( ( ( ( ( 𝜑𝑔 ∈ ( Base ‘ 𝑆 ) ) ∧ 𝑄 = ( ( 𝑔 + 𝑇 ) 𝑔 ) ) ∧ ¬ 𝑔𝐴 ) ∧ 𝑢 ∈ ( { 𝑤 ∈ Word 𝐷𝑤 : dom 𝑤1-1𝐷 } ∩ ( ♯ “ { 3 } ) ) ) ∧ ( 𝑀𝑢 ) = 𝑇 ) ∧ 𝑥 ∈ ( 𝐷 ∖ ran 𝑢 ) ) ∧ 𝑦 ∈ ( 𝐷 ∖ ran 𝑢 ) ) ∧ 𝑥𝑦 ) → 𝑔 ∈ ( Base ‘ 𝑆 ) )
22 simp-6r ( ( ( ( ( ( ( ( ( 𝜑𝑔 ∈ ( Base ‘ 𝑆 ) ) ∧ 𝑄 = ( ( 𝑔 + 𝑇 ) 𝑔 ) ) ∧ ¬ 𝑔𝐴 ) ∧ 𝑢 ∈ ( { 𝑤 ∈ Word 𝐷𝑤 : dom 𝑤1-1𝐷 } ∩ ( ♯ “ { 3 } ) ) ) ∧ ( 𝑀𝑢 ) = 𝑇 ) ∧ 𝑥 ∈ ( 𝐷 ∖ ran 𝑢 ) ) ∧ 𝑦 ∈ ( 𝐷 ∖ ran 𝑢 ) ) ∧ 𝑥𝑦 ) → ¬ 𝑔𝐴 )
23 21 22 eldifd ( ( ( ( ( ( ( ( ( 𝜑𝑔 ∈ ( Base ‘ 𝑆 ) ) ∧ 𝑄 = ( ( 𝑔 + 𝑇 ) 𝑔 ) ) ∧ ¬ 𝑔𝐴 ) ∧ 𝑢 ∈ ( { 𝑤 ∈ Word 𝐷𝑤 : dom 𝑤1-1𝐷 } ∩ ( ♯ “ { 3 } ) ) ) ∧ ( 𝑀𝑢 ) = 𝑇 ) ∧ 𝑥 ∈ ( 𝐷 ∖ ran 𝑢 ) ) ∧ 𝑦 ∈ ( 𝐷 ∖ ran 𝑢 ) ) ∧ 𝑥𝑦 ) → 𝑔 ∈ ( ( Base ‘ 𝑆 ) ∖ 𝐴 ) )
24 simpllr ( ( ( ( ( ( ( ( ( 𝜑𝑔 ∈ ( Base ‘ 𝑆 ) ) ∧ 𝑄 = ( ( 𝑔 + 𝑇 ) 𝑔 ) ) ∧ ¬ 𝑔𝐴 ) ∧ 𝑢 ∈ ( { 𝑤 ∈ Word 𝐷𝑤 : dom 𝑤1-1𝐷 } ∩ ( ♯ “ { 3 } ) ) ) ∧ ( 𝑀𝑢 ) = 𝑇 ) ∧ 𝑥 ∈ ( 𝐷 ∖ ran 𝑢 ) ) ∧ 𝑦 ∈ ( 𝐷 ∖ ran 𝑢 ) ) ∧ 𝑥𝑦 ) → 𝑥 ∈ ( 𝐷 ∖ ran 𝑢 ) )
25 24 eldifad ( ( ( ( ( ( ( ( ( 𝜑𝑔 ∈ ( Base ‘ 𝑆 ) ) ∧ 𝑄 = ( ( 𝑔 + 𝑇 ) 𝑔 ) ) ∧ ¬ 𝑔𝐴 ) ∧ 𝑢 ∈ ( { 𝑤 ∈ Word 𝐷𝑤 : dom 𝑤1-1𝐷 } ∩ ( ♯ “ { 3 } ) ) ) ∧ ( 𝑀𝑢 ) = 𝑇 ) ∧ 𝑥 ∈ ( 𝐷 ∖ ran 𝑢 ) ) ∧ 𝑦 ∈ ( 𝐷 ∖ ran 𝑢 ) ) ∧ 𝑥𝑦 ) → 𝑥𝐷 )
26 simplr ( ( ( ( ( ( ( ( ( 𝜑𝑔 ∈ ( Base ‘ 𝑆 ) ) ∧ 𝑄 = ( ( 𝑔 + 𝑇 ) 𝑔 ) ) ∧ ¬ 𝑔𝐴 ) ∧ 𝑢 ∈ ( { 𝑤 ∈ Word 𝐷𝑤 : dom 𝑤1-1𝐷 } ∩ ( ♯ “ { 3 } ) ) ) ∧ ( 𝑀𝑢 ) = 𝑇 ) ∧ 𝑥 ∈ ( 𝐷 ∖ ran 𝑢 ) ) ∧ 𝑦 ∈ ( 𝐷 ∖ ran 𝑢 ) ) ∧ 𝑥𝑦 ) → 𝑦 ∈ ( 𝐷 ∖ ran 𝑢 ) )
27 26 eldifad ( ( ( ( ( ( ( ( ( 𝜑𝑔 ∈ ( Base ‘ 𝑆 ) ) ∧ 𝑄 = ( ( 𝑔 + 𝑇 ) 𝑔 ) ) ∧ ¬ 𝑔𝐴 ) ∧ 𝑢 ∈ ( { 𝑤 ∈ Word 𝐷𝑤 : dom 𝑤1-1𝐷 } ∩ ( ♯ “ { 3 } ) ) ) ∧ ( 𝑀𝑢 ) = 𝑇 ) ∧ 𝑥 ∈ ( 𝐷 ∖ ran 𝑢 ) ) ∧ 𝑦 ∈ ( 𝐷 ∖ ran 𝑢 ) ) ∧ 𝑥𝑦 ) → 𝑦𝐷 )
28 25 27 prssd ( ( ( ( ( ( ( ( ( 𝜑𝑔 ∈ ( Base ‘ 𝑆 ) ) ∧ 𝑄 = ( ( 𝑔 + 𝑇 ) 𝑔 ) ) ∧ ¬ 𝑔𝐴 ) ∧ 𝑢 ∈ ( { 𝑤 ∈ Word 𝐷𝑤 : dom 𝑤1-1𝐷 } ∩ ( ♯ “ { 3 } ) ) ) ∧ ( 𝑀𝑢 ) = 𝑇 ) ∧ 𝑥 ∈ ( 𝐷 ∖ ran 𝑢 ) ) ∧ 𝑦 ∈ ( 𝐷 ∖ ran 𝑢 ) ) ∧ 𝑥𝑦 ) → { 𝑥 , 𝑦 } ⊆ 𝐷 )
29 simpr ( ( ( ( ( ( ( ( ( 𝜑𝑔 ∈ ( Base ‘ 𝑆 ) ) ∧ 𝑄 = ( ( 𝑔 + 𝑇 ) 𝑔 ) ) ∧ ¬ 𝑔𝐴 ) ∧ 𝑢 ∈ ( { 𝑤 ∈ Word 𝐷𝑤 : dom 𝑤1-1𝐷 } ∩ ( ♯ “ { 3 } ) ) ) ∧ ( 𝑀𝑢 ) = 𝑇 ) ∧ 𝑥 ∈ ( 𝐷 ∖ ran 𝑢 ) ) ∧ 𝑦 ∈ ( 𝐷 ∖ ran 𝑢 ) ) ∧ 𝑥𝑦 ) → 𝑥𝑦 )
30 pr2nelem ( ( 𝑥 ∈ ( 𝐷 ∖ ran 𝑢 ) ∧ 𝑦 ∈ ( 𝐷 ∖ ran 𝑢 ) ∧ 𝑥𝑦 ) → { 𝑥 , 𝑦 } ≈ 2o )
31 24 26 29 30 syl3anc ( ( ( ( ( ( ( ( ( 𝜑𝑔 ∈ ( Base ‘ 𝑆 ) ) ∧ 𝑄 = ( ( 𝑔 + 𝑇 ) 𝑔 ) ) ∧ ¬ 𝑔𝐴 ) ∧ 𝑢 ∈ ( { 𝑤 ∈ Word 𝐷𝑤 : dom 𝑤1-1𝐷 } ∩ ( ♯ “ { 3 } ) ) ) ∧ ( 𝑀𝑢 ) = 𝑇 ) ∧ 𝑥 ∈ ( 𝐷 ∖ ran 𝑢 ) ) ∧ 𝑦 ∈ ( 𝐷 ∖ ran 𝑢 ) ) ∧ 𝑥𝑦 ) → { 𝑥 , 𝑦 } ≈ 2o )
32 eqid ( pmTrsp ‘ 𝐷 ) = ( pmTrsp ‘ 𝐷 )
33 eqid ran ( pmTrsp ‘ 𝐷 ) = ran ( pmTrsp ‘ 𝐷 )
34 32 33 pmtrrn ( ( 𝐷 ∈ Fin ∧ { 𝑥 , 𝑦 } ⊆ 𝐷 ∧ { 𝑥 , 𝑦 } ≈ 2o ) → ( ( pmTrsp ‘ 𝐷 ) ‘ { 𝑥 , 𝑦 } ) ∈ ran ( pmTrsp ‘ 𝐷 ) )
35 20 28 31 34 syl3anc ( ( ( ( ( ( ( ( ( 𝜑𝑔 ∈ ( Base ‘ 𝑆 ) ) ∧ 𝑄 = ( ( 𝑔 + 𝑇 ) 𝑔 ) ) ∧ ¬ 𝑔𝐴 ) ∧ 𝑢 ∈ ( { 𝑤 ∈ Word 𝐷𝑤 : dom 𝑤1-1𝐷 } ∩ ( ♯ “ { 3 } ) ) ) ∧ ( 𝑀𝑢 ) = 𝑇 ) ∧ 𝑥 ∈ ( 𝐷 ∖ ran 𝑢 ) ) ∧ 𝑦 ∈ ( 𝐷 ∖ ran 𝑢 ) ) ∧ 𝑥𝑦 ) → ( ( pmTrsp ‘ 𝐷 ) ‘ { 𝑥 , 𝑦 } ) ∈ ran ( pmTrsp ‘ 𝐷 ) )
36 eqid ( Base ‘ 𝑆 ) = ( Base ‘ 𝑆 )
37 3 36 33 pmtrodpm ( ( 𝐷 ∈ Fin ∧ ( ( pmTrsp ‘ 𝐷 ) ‘ { 𝑥 , 𝑦 } ) ∈ ran ( pmTrsp ‘ 𝐷 ) ) → ( ( pmTrsp ‘ 𝐷 ) ‘ { 𝑥 , 𝑦 } ) ∈ ( ( Base ‘ 𝑆 ) ∖ ( pmEven ‘ 𝐷 ) ) )
38 20 35 37 syl2anc ( ( ( ( ( ( ( ( ( 𝜑𝑔 ∈ ( Base ‘ 𝑆 ) ) ∧ 𝑄 = ( ( 𝑔 + 𝑇 ) 𝑔 ) ) ∧ ¬ 𝑔𝐴 ) ∧ 𝑢 ∈ ( { 𝑤 ∈ Word 𝐷𝑤 : dom 𝑤1-1𝐷 } ∩ ( ♯ “ { 3 } ) ) ) ∧ ( 𝑀𝑢 ) = 𝑇 ) ∧ 𝑥 ∈ ( 𝐷 ∖ ran 𝑢 ) ) ∧ 𝑦 ∈ ( 𝐷 ∖ ran 𝑢 ) ) ∧ 𝑥𝑦 ) → ( ( pmTrsp ‘ 𝐷 ) ‘ { 𝑥 , 𝑦 } ) ∈ ( ( Base ‘ 𝑆 ) ∖ ( pmEven ‘ 𝐷 ) ) )
39 2 difeq2i ( ( Base ‘ 𝑆 ) ∖ 𝐴 ) = ( ( Base ‘ 𝑆 ) ∖ ( pmEven ‘ 𝐷 ) )
40 38 39 eleqtrrdi ( ( ( ( ( ( ( ( ( 𝜑𝑔 ∈ ( Base ‘ 𝑆 ) ) ∧ 𝑄 = ( ( 𝑔 + 𝑇 ) 𝑔 ) ) ∧ ¬ 𝑔𝐴 ) ∧ 𝑢 ∈ ( { 𝑤 ∈ Word 𝐷𝑤 : dom 𝑤1-1𝐷 } ∩ ( ♯ “ { 3 } ) ) ) ∧ ( 𝑀𝑢 ) = 𝑇 ) ∧ 𝑥 ∈ ( 𝐷 ∖ ran 𝑢 ) ) ∧ 𝑦 ∈ ( 𝐷 ∖ ran 𝑢 ) ) ∧ 𝑥𝑦 ) → ( ( pmTrsp ‘ 𝐷 ) ‘ { 𝑥 , 𝑦 } ) ∈ ( ( Base ‘ 𝑆 ) ∖ 𝐴 ) )
41 3 36 2 odpmco ( ( 𝐷 ∈ Fin ∧ 𝑔 ∈ ( ( Base ‘ 𝑆 ) ∖ 𝐴 ) ∧ ( ( pmTrsp ‘ 𝐷 ) ‘ { 𝑥 , 𝑦 } ) ∈ ( ( Base ‘ 𝑆 ) ∖ 𝐴 ) ) → ( 𝑔 ∘ ( ( pmTrsp ‘ 𝐷 ) ‘ { 𝑥 , 𝑦 } ) ) ∈ 𝐴 )
42 20 23 40 41 syl3anc ( ( ( ( ( ( ( ( ( 𝜑𝑔 ∈ ( Base ‘ 𝑆 ) ) ∧ 𝑄 = ( ( 𝑔 + 𝑇 ) 𝑔 ) ) ∧ ¬ 𝑔𝐴 ) ∧ 𝑢 ∈ ( { 𝑤 ∈ Word 𝐷𝑤 : dom 𝑤1-1𝐷 } ∩ ( ♯ “ { 3 } ) ) ) ∧ ( 𝑀𝑢 ) = 𝑇 ) ∧ 𝑥 ∈ ( 𝐷 ∖ ran 𝑢 ) ) ∧ 𝑦 ∈ ( 𝐷 ∖ ran 𝑢 ) ) ∧ 𝑥𝑦 ) → ( 𝑔 ∘ ( ( pmTrsp ‘ 𝐷 ) ‘ { 𝑥 , 𝑦 } ) ) ∈ 𝐴 )
43 simpr ( ( ( ( ( ( ( ( ( ( 𝜑𝑔 ∈ ( Base ‘ 𝑆 ) ) ∧ 𝑄 = ( ( 𝑔 + 𝑇 ) 𝑔 ) ) ∧ ¬ 𝑔𝐴 ) ∧ 𝑢 ∈ ( { 𝑤 ∈ Word 𝐷𝑤 : dom 𝑤1-1𝐷 } ∩ ( ♯ “ { 3 } ) ) ) ∧ ( 𝑀𝑢 ) = 𝑇 ) ∧ 𝑥 ∈ ( 𝐷 ∖ ran 𝑢 ) ) ∧ 𝑦 ∈ ( 𝐷 ∖ ran 𝑢 ) ) ∧ 𝑥𝑦 ) ∧ 𝑝 = ( 𝑔 ∘ ( ( pmTrsp ‘ 𝐷 ) ‘ { 𝑥 , 𝑦 } ) ) ) → 𝑝 = ( 𝑔 ∘ ( ( pmTrsp ‘ 𝐷 ) ‘ { 𝑥 , 𝑦 } ) ) )
44 43 oveq1d ( ( ( ( ( ( ( ( ( ( 𝜑𝑔 ∈ ( Base ‘ 𝑆 ) ) ∧ 𝑄 = ( ( 𝑔 + 𝑇 ) 𝑔 ) ) ∧ ¬ 𝑔𝐴 ) ∧ 𝑢 ∈ ( { 𝑤 ∈ Word 𝐷𝑤 : dom 𝑤1-1𝐷 } ∩ ( ♯ “ { 3 } ) ) ) ∧ ( 𝑀𝑢 ) = 𝑇 ) ∧ 𝑥 ∈ ( 𝐷 ∖ ran 𝑢 ) ) ∧ 𝑦 ∈ ( 𝐷 ∖ ran 𝑢 ) ) ∧ 𝑥𝑦 ) ∧ 𝑝 = ( 𝑔 ∘ ( ( pmTrsp ‘ 𝐷 ) ‘ { 𝑥 , 𝑦 } ) ) ) → ( 𝑝 + 𝑇 ) = ( ( 𝑔 ∘ ( ( pmTrsp ‘ 𝐷 ) ‘ { 𝑥 , 𝑦 } ) ) + 𝑇 ) )
45 44 43 oveq12d ( ( ( ( ( ( ( ( ( ( 𝜑𝑔 ∈ ( Base ‘ 𝑆 ) ) ∧ 𝑄 = ( ( 𝑔 + 𝑇 ) 𝑔 ) ) ∧ ¬ 𝑔𝐴 ) ∧ 𝑢 ∈ ( { 𝑤 ∈ Word 𝐷𝑤 : dom 𝑤1-1𝐷 } ∩ ( ♯ “ { 3 } ) ) ) ∧ ( 𝑀𝑢 ) = 𝑇 ) ∧ 𝑥 ∈ ( 𝐷 ∖ ran 𝑢 ) ) ∧ 𝑦 ∈ ( 𝐷 ∖ ran 𝑢 ) ) ∧ 𝑥𝑦 ) ∧ 𝑝 = ( 𝑔 ∘ ( ( pmTrsp ‘ 𝐷 ) ‘ { 𝑥 , 𝑦 } ) ) ) → ( ( 𝑝 + 𝑇 ) 𝑝 ) = ( ( ( 𝑔 ∘ ( ( pmTrsp ‘ 𝐷 ) ‘ { 𝑥 , 𝑦 } ) ) + 𝑇 ) ( 𝑔 ∘ ( ( pmTrsp ‘ 𝐷 ) ‘ { 𝑥 , 𝑦 } ) ) ) )
46 45 eqeq2d ( ( ( ( ( ( ( ( ( ( 𝜑𝑔 ∈ ( Base ‘ 𝑆 ) ) ∧ 𝑄 = ( ( 𝑔 + 𝑇 ) 𝑔 ) ) ∧ ¬ 𝑔𝐴 ) ∧ 𝑢 ∈ ( { 𝑤 ∈ Word 𝐷𝑤 : dom 𝑤1-1𝐷 } ∩ ( ♯ “ { 3 } ) ) ) ∧ ( 𝑀𝑢 ) = 𝑇 ) ∧ 𝑥 ∈ ( 𝐷 ∖ ran 𝑢 ) ) ∧ 𝑦 ∈ ( 𝐷 ∖ ran 𝑢 ) ) ∧ 𝑥𝑦 ) ∧ 𝑝 = ( 𝑔 ∘ ( ( pmTrsp ‘ 𝐷 ) ‘ { 𝑥 , 𝑦 } ) ) ) → ( 𝑄 = ( ( 𝑝 + 𝑇 ) 𝑝 ) ↔ 𝑄 = ( ( ( 𝑔 ∘ ( ( pmTrsp ‘ 𝐷 ) ‘ { 𝑥 , 𝑦 } ) ) + 𝑇 ) ( 𝑔 ∘ ( ( pmTrsp ‘ 𝐷 ) ‘ { 𝑥 , 𝑦 } ) ) ) ) )
47 38 eldifad ( ( ( ( ( ( ( ( ( 𝜑𝑔 ∈ ( Base ‘ 𝑆 ) ) ∧ 𝑄 = ( ( 𝑔 + 𝑇 ) 𝑔 ) ) ∧ ¬ 𝑔𝐴 ) ∧ 𝑢 ∈ ( { 𝑤 ∈ Word 𝐷𝑤 : dom 𝑤1-1𝐷 } ∩ ( ♯ “ { 3 } ) ) ) ∧ ( 𝑀𝑢 ) = 𝑇 ) ∧ 𝑥 ∈ ( 𝐷 ∖ ran 𝑢 ) ) ∧ 𝑦 ∈ ( 𝐷 ∖ ran 𝑢 ) ) ∧ 𝑥𝑦 ) → ( ( pmTrsp ‘ 𝐷 ) ‘ { 𝑥 , 𝑦 } ) ∈ ( Base ‘ 𝑆 ) )
48 0zd ( 𝜑 → 0 ∈ ℤ )
49 hashcl ( 𝐷 ∈ Fin → ( ♯ ‘ 𝐷 ) ∈ ℕ0 )
50 9 49 syl ( 𝜑 → ( ♯ ‘ 𝐷 ) ∈ ℕ0 )
51 4 50 eqeltrid ( 𝜑𝑁 ∈ ℕ0 )
52 51 nn0zd ( 𝜑𝑁 ∈ ℤ )
53 3z 3 ∈ ℤ
54 53 a1i ( 𝜑 → 3 ∈ ℤ )
55 0red ( 𝜑 → 0 ∈ ℝ )
56 54 zred ( 𝜑 → 3 ∈ ℝ )
57 3pos 0 < 3
58 57 a1i ( 𝜑 → 0 < 3 )
59 55 56 58 ltled ( 𝜑 → 0 ≤ 3 )
60 5re 5 ∈ ℝ
61 60 a1i ( 𝜑 → 5 ∈ ℝ )
62 51 nn0red ( 𝜑𝑁 ∈ ℝ )
63 3lt5 3 < 5
64 63 a1i ( 𝜑 → 3 < 5 )
65 56 61 64 ltled ( 𝜑 → 3 ≤ 5 )
66 56 61 62 65 8 letrd ( 𝜑 → 3 ≤ 𝑁 )
67 48 52 54 59 66 elfzd ( 𝜑 → 3 ∈ ( 0 ... 𝑁 ) )
68 1 3 4 5 36 cycpmgcl ( ( 𝐷 ∈ Fin ∧ 3 ∈ ( 0 ... 𝑁 ) ) → 𝐶 ⊆ ( Base ‘ 𝑆 ) )
69 9 67 68 syl2anc ( 𝜑𝐶 ⊆ ( Base ‘ 𝑆 ) )
70 69 11 sseldd ( 𝜑𝑇 ∈ ( Base ‘ 𝑆 ) )
71 70 ad8antr ( ( ( ( ( ( ( ( ( 𝜑𝑔 ∈ ( Base ‘ 𝑆 ) ) ∧ 𝑄 = ( ( 𝑔 + 𝑇 ) 𝑔 ) ) ∧ ¬ 𝑔𝐴 ) ∧ 𝑢 ∈ ( { 𝑤 ∈ Word 𝐷𝑤 : dom 𝑤1-1𝐷 } ∩ ( ♯ “ { 3 } ) ) ) ∧ ( 𝑀𝑢 ) = 𝑇 ) ∧ 𝑥 ∈ ( 𝐷 ∖ ran 𝑢 ) ) ∧ 𝑦 ∈ ( 𝐷 ∖ ran 𝑢 ) ) ∧ 𝑥𝑦 ) → 𝑇 ∈ ( Base ‘ 𝑆 ) )
72 5 20 25 27 29 32 cycpm2tr ( ( ( ( ( ( ( ( ( 𝜑𝑔 ∈ ( Base ‘ 𝑆 ) ) ∧ 𝑄 = ( ( 𝑔 + 𝑇 ) 𝑔 ) ) ∧ ¬ 𝑔𝐴 ) ∧ 𝑢 ∈ ( { 𝑤 ∈ Word 𝐷𝑤 : dom 𝑤1-1𝐷 } ∩ ( ♯ “ { 3 } ) ) ) ∧ ( 𝑀𝑢 ) = 𝑇 ) ∧ 𝑥 ∈ ( 𝐷 ∖ ran 𝑢 ) ) ∧ 𝑦 ∈ ( 𝐷 ∖ ran 𝑢 ) ) ∧ 𝑥𝑦 ) → ( 𝑀 ‘ ⟨“ 𝑥 𝑦 ”⟩ ) = ( ( pmTrsp ‘ 𝐷 ) ‘ { 𝑥 , 𝑦 } ) )
73 72 reseq1d ( ( ( ( ( ( ( ( ( 𝜑𝑔 ∈ ( Base ‘ 𝑆 ) ) ∧ 𝑄 = ( ( 𝑔 + 𝑇 ) 𝑔 ) ) ∧ ¬ 𝑔𝐴 ) ∧ 𝑢 ∈ ( { 𝑤 ∈ Word 𝐷𝑤 : dom 𝑤1-1𝐷 } ∩ ( ♯ “ { 3 } ) ) ) ∧ ( 𝑀𝑢 ) = 𝑇 ) ∧ 𝑥 ∈ ( 𝐷 ∖ ran 𝑢 ) ) ∧ 𝑦 ∈ ( 𝐷 ∖ ran 𝑢 ) ) ∧ 𝑥𝑦 ) → ( ( 𝑀 ‘ ⟨“ 𝑥 𝑦 ”⟩ ) ↾ ran 𝑢 ) = ( ( ( pmTrsp ‘ 𝐷 ) ‘ { 𝑥 , 𝑦 } ) ↾ ran 𝑢 ) )
74 25 27 s2cld ( ( ( ( ( ( ( ( ( 𝜑𝑔 ∈ ( Base ‘ 𝑆 ) ) ∧ 𝑄 = ( ( 𝑔 + 𝑇 ) 𝑔 ) ) ∧ ¬ 𝑔𝐴 ) ∧ 𝑢 ∈ ( { 𝑤 ∈ Word 𝐷𝑤 : dom 𝑤1-1𝐷 } ∩ ( ♯ “ { 3 } ) ) ) ∧ ( 𝑀𝑢 ) = 𝑇 ) ∧ 𝑥 ∈ ( 𝐷 ∖ ran 𝑢 ) ) ∧ 𝑦 ∈ ( 𝐷 ∖ ran 𝑢 ) ) ∧ 𝑥𝑦 ) → ⟨“ 𝑥 𝑦 ”⟩ ∈ Word 𝐷 )
75 25 27 29 s2f1 ( ( ( ( ( ( ( ( ( 𝜑𝑔 ∈ ( Base ‘ 𝑆 ) ) ∧ 𝑄 = ( ( 𝑔 + 𝑇 ) 𝑔 ) ) ∧ ¬ 𝑔𝐴 ) ∧ 𝑢 ∈ ( { 𝑤 ∈ Word 𝐷𝑤 : dom 𝑤1-1𝐷 } ∩ ( ♯ “ { 3 } ) ) ) ∧ ( 𝑀𝑢 ) = 𝑇 ) ∧ 𝑥 ∈ ( 𝐷 ∖ ran 𝑢 ) ) ∧ 𝑦 ∈ ( 𝐷 ∖ ran 𝑢 ) ) ∧ 𝑥𝑦 ) → ⟨“ 𝑥 𝑦 ”⟩ : dom ⟨“ 𝑥 𝑦 ”⟩ –1-1𝐷 )
76 5 20 74 75 tocycfvres2 ( ( ( ( ( ( ( ( ( 𝜑𝑔 ∈ ( Base ‘ 𝑆 ) ) ∧ 𝑄 = ( ( 𝑔 + 𝑇 ) 𝑔 ) ) ∧ ¬ 𝑔𝐴 ) ∧ 𝑢 ∈ ( { 𝑤 ∈ Word 𝐷𝑤 : dom 𝑤1-1𝐷 } ∩ ( ♯ “ { 3 } ) ) ) ∧ ( 𝑀𝑢 ) = 𝑇 ) ∧ 𝑥 ∈ ( 𝐷 ∖ ran 𝑢 ) ) ∧ 𝑦 ∈ ( 𝐷 ∖ ran 𝑢 ) ) ∧ 𝑥𝑦 ) → ( ( 𝑀 ‘ ⟨“ 𝑥 𝑦 ”⟩ ) ↾ ( 𝐷 ∖ ran ⟨“ 𝑥 𝑦 ”⟩ ) ) = ( I ↾ ( 𝐷 ∖ ran ⟨“ 𝑥 𝑦 ”⟩ ) ) )
77 76 reseq1d ( ( ( ( ( ( ( ( ( 𝜑𝑔 ∈ ( Base ‘ 𝑆 ) ) ∧ 𝑄 = ( ( 𝑔 + 𝑇 ) 𝑔 ) ) ∧ ¬ 𝑔𝐴 ) ∧ 𝑢 ∈ ( { 𝑤 ∈ Word 𝐷𝑤 : dom 𝑤1-1𝐷 } ∩ ( ♯ “ { 3 } ) ) ) ∧ ( 𝑀𝑢 ) = 𝑇 ) ∧ 𝑥 ∈ ( 𝐷 ∖ ran 𝑢 ) ) ∧ 𝑦 ∈ ( 𝐷 ∖ ran 𝑢 ) ) ∧ 𝑥𝑦 ) → ( ( ( 𝑀 ‘ ⟨“ 𝑥 𝑦 ”⟩ ) ↾ ( 𝐷 ∖ ran ⟨“ 𝑥 𝑦 ”⟩ ) ) ↾ ran 𝑢 ) = ( ( I ↾ ( 𝐷 ∖ ran ⟨“ 𝑥 𝑦 ”⟩ ) ) ↾ ran 𝑢 ) )
78 simplr ( ( ( ( ( ( 𝜑𝑔 ∈ ( Base ‘ 𝑆 ) ) ∧ 𝑄 = ( ( 𝑔 + 𝑇 ) 𝑔 ) ) ∧ ¬ 𝑔𝐴 ) ∧ 𝑢 ∈ ( { 𝑤 ∈ Word 𝐷𝑤 : dom 𝑤1-1𝐷 } ∩ ( ♯ “ { 3 } ) ) ) ∧ ( 𝑀𝑢 ) = 𝑇 ) → 𝑢 ∈ ( { 𝑤 ∈ Word 𝐷𝑤 : dom 𝑤1-1𝐷 } ∩ ( ♯ “ { 3 } ) ) )
79 78 elin1d ( ( ( ( ( ( 𝜑𝑔 ∈ ( Base ‘ 𝑆 ) ) ∧ 𝑄 = ( ( 𝑔 + 𝑇 ) 𝑔 ) ) ∧ ¬ 𝑔𝐴 ) ∧ 𝑢 ∈ ( { 𝑤 ∈ Word 𝐷𝑤 : dom 𝑤1-1𝐷 } ∩ ( ♯ “ { 3 } ) ) ) ∧ ( 𝑀𝑢 ) = 𝑇 ) → 𝑢 ∈ { 𝑤 ∈ Word 𝐷𝑤 : dom 𝑤1-1𝐷 } )
80 id ( 𝑤 = 𝑢𝑤 = 𝑢 )
81 dmeq ( 𝑤 = 𝑢 → dom 𝑤 = dom 𝑢 )
82 eqidd ( 𝑤 = 𝑢𝐷 = 𝐷 )
83 80 81 82 f1eq123d ( 𝑤 = 𝑢 → ( 𝑤 : dom 𝑤1-1𝐷𝑢 : dom 𝑢1-1𝐷 ) )
84 83 elrab ( 𝑢 ∈ { 𝑤 ∈ Word 𝐷𝑤 : dom 𝑤1-1𝐷 } ↔ ( 𝑢 ∈ Word 𝐷𝑢 : dom 𝑢1-1𝐷 ) )
85 79 84 sylib ( ( ( ( ( ( 𝜑𝑔 ∈ ( Base ‘ 𝑆 ) ) ∧ 𝑄 = ( ( 𝑔 + 𝑇 ) 𝑔 ) ) ∧ ¬ 𝑔𝐴 ) ∧ 𝑢 ∈ ( { 𝑤 ∈ Word 𝐷𝑤 : dom 𝑤1-1𝐷 } ∩ ( ♯ “ { 3 } ) ) ) ∧ ( 𝑀𝑢 ) = 𝑇 ) → ( 𝑢 ∈ Word 𝐷𝑢 : dom 𝑢1-1𝐷 ) )
86 85 simprd ( ( ( ( ( ( 𝜑𝑔 ∈ ( Base ‘ 𝑆 ) ) ∧ 𝑄 = ( ( 𝑔 + 𝑇 ) 𝑔 ) ) ∧ ¬ 𝑔𝐴 ) ∧ 𝑢 ∈ ( { 𝑤 ∈ Word 𝐷𝑤 : dom 𝑤1-1𝐷 } ∩ ( ♯ “ { 3 } ) ) ) ∧ ( 𝑀𝑢 ) = 𝑇 ) → 𝑢 : dom 𝑢1-1𝐷 )
87 f1f ( 𝑢 : dom 𝑢1-1𝐷𝑢 : dom 𝑢𝐷 )
88 frn ( 𝑢 : dom 𝑢𝐷 → ran 𝑢𝐷 )
89 86 87 88 3syl ( ( ( ( ( ( 𝜑𝑔 ∈ ( Base ‘ 𝑆 ) ) ∧ 𝑄 = ( ( 𝑔 + 𝑇 ) 𝑔 ) ) ∧ ¬ 𝑔𝐴 ) ∧ 𝑢 ∈ ( { 𝑤 ∈ Word 𝐷𝑤 : dom 𝑤1-1𝐷 } ∩ ( ♯ “ { 3 } ) ) ) ∧ ( 𝑀𝑢 ) = 𝑇 ) → ran 𝑢𝐷 )
90 89 ad3antrrr ( ( ( ( ( ( ( ( ( 𝜑𝑔 ∈ ( Base ‘ 𝑆 ) ) ∧ 𝑄 = ( ( 𝑔 + 𝑇 ) 𝑔 ) ) ∧ ¬ 𝑔𝐴 ) ∧ 𝑢 ∈ ( { 𝑤 ∈ Word 𝐷𝑤 : dom 𝑤1-1𝐷 } ∩ ( ♯ “ { 3 } ) ) ) ∧ ( 𝑀𝑢 ) = 𝑇 ) ∧ 𝑥 ∈ ( 𝐷 ∖ ran 𝑢 ) ) ∧ 𝑦 ∈ ( 𝐷 ∖ ran 𝑢 ) ) ∧ 𝑥𝑦 ) → ran 𝑢𝐷 )
91 24 26 prssd ( ( ( ( ( ( ( ( ( 𝜑𝑔 ∈ ( Base ‘ 𝑆 ) ) ∧ 𝑄 = ( ( 𝑔 + 𝑇 ) 𝑔 ) ) ∧ ¬ 𝑔𝐴 ) ∧ 𝑢 ∈ ( { 𝑤 ∈ Word 𝐷𝑤 : dom 𝑤1-1𝐷 } ∩ ( ♯ “ { 3 } ) ) ) ∧ ( 𝑀𝑢 ) = 𝑇 ) ∧ 𝑥 ∈ ( 𝐷 ∖ ran 𝑢 ) ) ∧ 𝑦 ∈ ( 𝐷 ∖ ran 𝑢 ) ) ∧ 𝑥𝑦 ) → { 𝑥 , 𝑦 } ⊆ ( 𝐷 ∖ ran 𝑢 ) )
92 ssconb ( ( { 𝑥 , 𝑦 } ⊆ 𝐷 ∧ ran 𝑢𝐷 ) → ( { 𝑥 , 𝑦 } ⊆ ( 𝐷 ∖ ran 𝑢 ) ↔ ran 𝑢 ⊆ ( 𝐷 ∖ { 𝑥 , 𝑦 } ) ) )
93 92 biimpa ( ( ( { 𝑥 , 𝑦 } ⊆ 𝐷 ∧ ran 𝑢𝐷 ) ∧ { 𝑥 , 𝑦 } ⊆ ( 𝐷 ∖ ran 𝑢 ) ) → ran 𝑢 ⊆ ( 𝐷 ∖ { 𝑥 , 𝑦 } ) )
94 28 90 91 93 syl21anc ( ( ( ( ( ( ( ( ( 𝜑𝑔 ∈ ( Base ‘ 𝑆 ) ) ∧ 𝑄 = ( ( 𝑔 + 𝑇 ) 𝑔 ) ) ∧ ¬ 𝑔𝐴 ) ∧ 𝑢 ∈ ( { 𝑤 ∈ Word 𝐷𝑤 : dom 𝑤1-1𝐷 } ∩ ( ♯ “ { 3 } ) ) ) ∧ ( 𝑀𝑢 ) = 𝑇 ) ∧ 𝑥 ∈ ( 𝐷 ∖ ran 𝑢 ) ) ∧ 𝑦 ∈ ( 𝐷 ∖ ran 𝑢 ) ) ∧ 𝑥𝑦 ) → ran 𝑢 ⊆ ( 𝐷 ∖ { 𝑥 , 𝑦 } ) )
95 24 26 s2rn ( ( ( ( ( ( ( ( ( 𝜑𝑔 ∈ ( Base ‘ 𝑆 ) ) ∧ 𝑄 = ( ( 𝑔 + 𝑇 ) 𝑔 ) ) ∧ ¬ 𝑔𝐴 ) ∧ 𝑢 ∈ ( { 𝑤 ∈ Word 𝐷𝑤 : dom 𝑤1-1𝐷 } ∩ ( ♯ “ { 3 } ) ) ) ∧ ( 𝑀𝑢 ) = 𝑇 ) ∧ 𝑥 ∈ ( 𝐷 ∖ ran 𝑢 ) ) ∧ 𝑦 ∈ ( 𝐷 ∖ ran 𝑢 ) ) ∧ 𝑥𝑦 ) → ran ⟨“ 𝑥 𝑦 ”⟩ = { 𝑥 , 𝑦 } )
96 95 difeq2d ( ( ( ( ( ( ( ( ( 𝜑𝑔 ∈ ( Base ‘ 𝑆 ) ) ∧ 𝑄 = ( ( 𝑔 + 𝑇 ) 𝑔 ) ) ∧ ¬ 𝑔𝐴 ) ∧ 𝑢 ∈ ( { 𝑤 ∈ Word 𝐷𝑤 : dom 𝑤1-1𝐷 } ∩ ( ♯ “ { 3 } ) ) ) ∧ ( 𝑀𝑢 ) = 𝑇 ) ∧ 𝑥 ∈ ( 𝐷 ∖ ran 𝑢 ) ) ∧ 𝑦 ∈ ( 𝐷 ∖ ran 𝑢 ) ) ∧ 𝑥𝑦 ) → ( 𝐷 ∖ ran ⟨“ 𝑥 𝑦 ”⟩ ) = ( 𝐷 ∖ { 𝑥 , 𝑦 } ) )
97 94 96 sseqtrrd ( ( ( ( ( ( ( ( ( 𝜑𝑔 ∈ ( Base ‘ 𝑆 ) ) ∧ 𝑄 = ( ( 𝑔 + 𝑇 ) 𝑔 ) ) ∧ ¬ 𝑔𝐴 ) ∧ 𝑢 ∈ ( { 𝑤 ∈ Word 𝐷𝑤 : dom 𝑤1-1𝐷 } ∩ ( ♯ “ { 3 } ) ) ) ∧ ( 𝑀𝑢 ) = 𝑇 ) ∧ 𝑥 ∈ ( 𝐷 ∖ ran 𝑢 ) ) ∧ 𝑦 ∈ ( 𝐷 ∖ ran 𝑢 ) ) ∧ 𝑥𝑦 ) → ran 𝑢 ⊆ ( 𝐷 ∖ ran ⟨“ 𝑥 𝑦 ”⟩ ) )
98 97 resabs1d ( ( ( ( ( ( ( ( ( 𝜑𝑔 ∈ ( Base ‘ 𝑆 ) ) ∧ 𝑄 = ( ( 𝑔 + 𝑇 ) 𝑔 ) ) ∧ ¬ 𝑔𝐴 ) ∧ 𝑢 ∈ ( { 𝑤 ∈ Word 𝐷𝑤 : dom 𝑤1-1𝐷 } ∩ ( ♯ “ { 3 } ) ) ) ∧ ( 𝑀𝑢 ) = 𝑇 ) ∧ 𝑥 ∈ ( 𝐷 ∖ ran 𝑢 ) ) ∧ 𝑦 ∈ ( 𝐷 ∖ ran 𝑢 ) ) ∧ 𝑥𝑦 ) → ( ( ( 𝑀 ‘ ⟨“ 𝑥 𝑦 ”⟩ ) ↾ ( 𝐷 ∖ ran ⟨“ 𝑥 𝑦 ”⟩ ) ) ↾ ran 𝑢 ) = ( ( 𝑀 ‘ ⟨“ 𝑥 𝑦 ”⟩ ) ↾ ran 𝑢 ) )
99 97 resabs1d ( ( ( ( ( ( ( ( ( 𝜑𝑔 ∈ ( Base ‘ 𝑆 ) ) ∧ 𝑄 = ( ( 𝑔 + 𝑇 ) 𝑔 ) ) ∧ ¬ 𝑔𝐴 ) ∧ 𝑢 ∈ ( { 𝑤 ∈ Word 𝐷𝑤 : dom 𝑤1-1𝐷 } ∩ ( ♯ “ { 3 } ) ) ) ∧ ( 𝑀𝑢 ) = 𝑇 ) ∧ 𝑥 ∈ ( 𝐷 ∖ ran 𝑢 ) ) ∧ 𝑦 ∈ ( 𝐷 ∖ ran 𝑢 ) ) ∧ 𝑥𝑦 ) → ( ( I ↾ ( 𝐷 ∖ ran ⟨“ 𝑥 𝑦 ”⟩ ) ) ↾ ran 𝑢 ) = ( I ↾ ran 𝑢 ) )
100 77 98 99 3eqtr3d ( ( ( ( ( ( ( ( ( 𝜑𝑔 ∈ ( Base ‘ 𝑆 ) ) ∧ 𝑄 = ( ( 𝑔 + 𝑇 ) 𝑔 ) ) ∧ ¬ 𝑔𝐴 ) ∧ 𝑢 ∈ ( { 𝑤 ∈ Word 𝐷𝑤 : dom 𝑤1-1𝐷 } ∩ ( ♯ “ { 3 } ) ) ) ∧ ( 𝑀𝑢 ) = 𝑇 ) ∧ 𝑥 ∈ ( 𝐷 ∖ ran 𝑢 ) ) ∧ 𝑦 ∈ ( 𝐷 ∖ ran 𝑢 ) ) ∧ 𝑥𝑦 ) → ( ( 𝑀 ‘ ⟨“ 𝑥 𝑦 ”⟩ ) ↾ ran 𝑢 ) = ( I ↾ ran 𝑢 ) )
101 73 100 eqtr3d ( ( ( ( ( ( ( ( ( 𝜑𝑔 ∈ ( Base ‘ 𝑆 ) ) ∧ 𝑄 = ( ( 𝑔 + 𝑇 ) 𝑔 ) ) ∧ ¬ 𝑔𝐴 ) ∧ 𝑢 ∈ ( { 𝑤 ∈ Word 𝐷𝑤 : dom 𝑤1-1𝐷 } ∩ ( ♯ “ { 3 } ) ) ) ∧ ( 𝑀𝑢 ) = 𝑇 ) ∧ 𝑥 ∈ ( 𝐷 ∖ ran 𝑢 ) ) ∧ 𝑦 ∈ ( 𝐷 ∖ ran 𝑢 ) ) ∧ 𝑥𝑦 ) → ( ( ( pmTrsp ‘ 𝐷 ) ‘ { 𝑥 , 𝑦 } ) ↾ ran 𝑢 ) = ( I ↾ ran 𝑢 ) )
102 simp-4r ( ( ( ( ( ( ( ( ( 𝜑𝑔 ∈ ( Base ‘ 𝑆 ) ) ∧ 𝑄 = ( ( 𝑔 + 𝑇 ) 𝑔 ) ) ∧ ¬ 𝑔𝐴 ) ∧ 𝑢 ∈ ( { 𝑤 ∈ Word 𝐷𝑤 : dom 𝑤1-1𝐷 } ∩ ( ♯ “ { 3 } ) ) ) ∧ ( 𝑀𝑢 ) = 𝑇 ) ∧ 𝑥 ∈ ( 𝐷 ∖ ran 𝑢 ) ) ∧ 𝑦 ∈ ( 𝐷 ∖ ran 𝑢 ) ) ∧ 𝑥𝑦 ) → ( 𝑀𝑢 ) = 𝑇 )
103 102 reseq1d ( ( ( ( ( ( ( ( ( 𝜑𝑔 ∈ ( Base ‘ 𝑆 ) ) ∧ 𝑄 = ( ( 𝑔 + 𝑇 ) 𝑔 ) ) ∧ ¬ 𝑔𝐴 ) ∧ 𝑢 ∈ ( { 𝑤 ∈ Word 𝐷𝑤 : dom 𝑤1-1𝐷 } ∩ ( ♯ “ { 3 } ) ) ) ∧ ( 𝑀𝑢 ) = 𝑇 ) ∧ 𝑥 ∈ ( 𝐷 ∖ ran 𝑢 ) ) ∧ 𝑦 ∈ ( 𝐷 ∖ ran 𝑢 ) ) ∧ 𝑥𝑦 ) → ( ( 𝑀𝑢 ) ↾ ( 𝐷 ∖ ran 𝑢 ) ) = ( 𝑇 ↾ ( 𝐷 ∖ ran 𝑢 ) ) )
104 85 simpld ( ( ( ( ( ( 𝜑𝑔 ∈ ( Base ‘ 𝑆 ) ) ∧ 𝑄 = ( ( 𝑔 + 𝑇 ) 𝑔 ) ) ∧ ¬ 𝑔𝐴 ) ∧ 𝑢 ∈ ( { 𝑤 ∈ Word 𝐷𝑤 : dom 𝑤1-1𝐷 } ∩ ( ♯ “ { 3 } ) ) ) ∧ ( 𝑀𝑢 ) = 𝑇 ) → 𝑢 ∈ Word 𝐷 )
105 104 ad3antrrr ( ( ( ( ( ( ( ( ( 𝜑𝑔 ∈ ( Base ‘ 𝑆 ) ) ∧ 𝑄 = ( ( 𝑔 + 𝑇 ) 𝑔 ) ) ∧ ¬ 𝑔𝐴 ) ∧ 𝑢 ∈ ( { 𝑤 ∈ Word 𝐷𝑤 : dom 𝑤1-1𝐷 } ∩ ( ♯ “ { 3 } ) ) ) ∧ ( 𝑀𝑢 ) = 𝑇 ) ∧ 𝑥 ∈ ( 𝐷 ∖ ran 𝑢 ) ) ∧ 𝑦 ∈ ( 𝐷 ∖ ran 𝑢 ) ) ∧ 𝑥𝑦 ) → 𝑢 ∈ Word 𝐷 )
106 86 ad3antrrr ( ( ( ( ( ( ( ( ( 𝜑𝑔 ∈ ( Base ‘ 𝑆 ) ) ∧ 𝑄 = ( ( 𝑔 + 𝑇 ) 𝑔 ) ) ∧ ¬ 𝑔𝐴 ) ∧ 𝑢 ∈ ( { 𝑤 ∈ Word 𝐷𝑤 : dom 𝑤1-1𝐷 } ∩ ( ♯ “ { 3 } ) ) ) ∧ ( 𝑀𝑢 ) = 𝑇 ) ∧ 𝑥 ∈ ( 𝐷 ∖ ran 𝑢 ) ) ∧ 𝑦 ∈ ( 𝐷 ∖ ran 𝑢 ) ) ∧ 𝑥𝑦 ) → 𝑢 : dom 𝑢1-1𝐷 )
107 5 20 105 106 tocycfvres2 ( ( ( ( ( ( ( ( ( 𝜑𝑔 ∈ ( Base ‘ 𝑆 ) ) ∧ 𝑄 = ( ( 𝑔 + 𝑇 ) 𝑔 ) ) ∧ ¬ 𝑔𝐴 ) ∧ 𝑢 ∈ ( { 𝑤 ∈ Word 𝐷𝑤 : dom 𝑤1-1𝐷 } ∩ ( ♯ “ { 3 } ) ) ) ∧ ( 𝑀𝑢 ) = 𝑇 ) ∧ 𝑥 ∈ ( 𝐷 ∖ ran 𝑢 ) ) ∧ 𝑦 ∈ ( 𝐷 ∖ ran 𝑢 ) ) ∧ 𝑥𝑦 ) → ( ( 𝑀𝑢 ) ↾ ( 𝐷 ∖ ran 𝑢 ) ) = ( I ↾ ( 𝐷 ∖ ran 𝑢 ) ) )
108 103 107 eqtr3d ( ( ( ( ( ( ( ( ( 𝜑𝑔 ∈ ( Base ‘ 𝑆 ) ) ∧ 𝑄 = ( ( 𝑔 + 𝑇 ) 𝑔 ) ) ∧ ¬ 𝑔𝐴 ) ∧ 𝑢 ∈ ( { 𝑤 ∈ Word 𝐷𝑤 : dom 𝑤1-1𝐷 } ∩ ( ♯ “ { 3 } ) ) ) ∧ ( 𝑀𝑢 ) = 𝑇 ) ∧ 𝑥 ∈ ( 𝐷 ∖ ran 𝑢 ) ) ∧ 𝑦 ∈ ( 𝐷 ∖ ran 𝑢 ) ) ∧ 𝑥𝑦 ) → ( 𝑇 ↾ ( 𝐷 ∖ ran 𝑢 ) ) = ( I ↾ ( 𝐷 ∖ ran 𝑢 ) ) )
109 disjdif ( ran 𝑢 ∩ ( 𝐷 ∖ ran 𝑢 ) ) = ∅
110 109 a1i ( ( ( ( ( ( ( ( ( 𝜑𝑔 ∈ ( Base ‘ 𝑆 ) ) ∧ 𝑄 = ( ( 𝑔 + 𝑇 ) 𝑔 ) ) ∧ ¬ 𝑔𝐴 ) ∧ 𝑢 ∈ ( { 𝑤 ∈ Word 𝐷𝑤 : dom 𝑤1-1𝐷 } ∩ ( ♯ “ { 3 } ) ) ) ∧ ( 𝑀𝑢 ) = 𝑇 ) ∧ 𝑥 ∈ ( 𝐷 ∖ ran 𝑢 ) ) ∧ 𝑦 ∈ ( 𝐷 ∖ ran 𝑢 ) ) ∧ 𝑥𝑦 ) → ( ran 𝑢 ∩ ( 𝐷 ∖ ran 𝑢 ) ) = ∅ )
111 undif ( ran 𝑢𝐷 ↔ ( ran 𝑢 ∪ ( 𝐷 ∖ ran 𝑢 ) ) = 𝐷 )
112 90 111 sylib ( ( ( ( ( ( ( ( ( 𝜑𝑔 ∈ ( Base ‘ 𝑆 ) ) ∧ 𝑄 = ( ( 𝑔 + 𝑇 ) 𝑔 ) ) ∧ ¬ 𝑔𝐴 ) ∧ 𝑢 ∈ ( { 𝑤 ∈ Word 𝐷𝑤 : dom 𝑤1-1𝐷 } ∩ ( ♯ “ { 3 } ) ) ) ∧ ( 𝑀𝑢 ) = 𝑇 ) ∧ 𝑥 ∈ ( 𝐷 ∖ ran 𝑢 ) ) ∧ 𝑦 ∈ ( 𝐷 ∖ ran 𝑢 ) ) ∧ 𝑥𝑦 ) → ( ran 𝑢 ∪ ( 𝐷 ∖ ran 𝑢 ) ) = 𝐷 )
113 3 36 47 71 101 108 110 112 symgcom ( ( ( ( ( ( ( ( ( 𝜑𝑔 ∈ ( Base ‘ 𝑆 ) ) ∧ 𝑄 = ( ( 𝑔 + 𝑇 ) 𝑔 ) ) ∧ ¬ 𝑔𝐴 ) ∧ 𝑢 ∈ ( { 𝑤 ∈ Word 𝐷𝑤 : dom 𝑤1-1𝐷 } ∩ ( ♯ “ { 3 } ) ) ) ∧ ( 𝑀𝑢 ) = 𝑇 ) ∧ 𝑥 ∈ ( 𝐷 ∖ ran 𝑢 ) ) ∧ 𝑦 ∈ ( 𝐷 ∖ ran 𝑢 ) ) ∧ 𝑥𝑦 ) → ( ( ( pmTrsp ‘ 𝐷 ) ‘ { 𝑥 , 𝑦 } ) ∘ 𝑇 ) = ( 𝑇 ∘ ( ( pmTrsp ‘ 𝐷 ) ‘ { 𝑥 , 𝑦 } ) ) )
114 113 coeq2d ( ( ( ( ( ( ( ( ( 𝜑𝑔 ∈ ( Base ‘ 𝑆 ) ) ∧ 𝑄 = ( ( 𝑔 + 𝑇 ) 𝑔 ) ) ∧ ¬ 𝑔𝐴 ) ∧ 𝑢 ∈ ( { 𝑤 ∈ Word 𝐷𝑤 : dom 𝑤1-1𝐷 } ∩ ( ♯ “ { 3 } ) ) ) ∧ ( 𝑀𝑢 ) = 𝑇 ) ∧ 𝑥 ∈ ( 𝐷 ∖ ran 𝑢 ) ) ∧ 𝑦 ∈ ( 𝐷 ∖ ran 𝑢 ) ) ∧ 𝑥𝑦 ) → ( 𝑔 ∘ ( ( ( pmTrsp ‘ 𝐷 ) ‘ { 𝑥 , 𝑦 } ) ∘ 𝑇 ) ) = ( 𝑔 ∘ ( 𝑇 ∘ ( ( pmTrsp ‘ 𝐷 ) ‘ { 𝑥 , 𝑦 } ) ) ) )
115 3 36 6 symgov ( ( 𝑔 ∈ ( Base ‘ 𝑆 ) ∧ ( ( pmTrsp ‘ 𝐷 ) ‘ { 𝑥 , 𝑦 } ) ∈ ( Base ‘ 𝑆 ) ) → ( 𝑔 + ( ( pmTrsp ‘ 𝐷 ) ‘ { 𝑥 , 𝑦 } ) ) = ( 𝑔 ∘ ( ( pmTrsp ‘ 𝐷 ) ‘ { 𝑥 , 𝑦 } ) ) )
116 21 47 115 syl2anc ( ( ( ( ( ( ( ( ( 𝜑𝑔 ∈ ( Base ‘ 𝑆 ) ) ∧ 𝑄 = ( ( 𝑔 + 𝑇 ) 𝑔 ) ) ∧ ¬ 𝑔𝐴 ) ∧ 𝑢 ∈ ( { 𝑤 ∈ Word 𝐷𝑤 : dom 𝑤1-1𝐷 } ∩ ( ♯ “ { 3 } ) ) ) ∧ ( 𝑀𝑢 ) = 𝑇 ) ∧ 𝑥 ∈ ( 𝐷 ∖ ran 𝑢 ) ) ∧ 𝑦 ∈ ( 𝐷 ∖ ran 𝑢 ) ) ∧ 𝑥𝑦 ) → ( 𝑔 + ( ( pmTrsp ‘ 𝐷 ) ‘ { 𝑥 , 𝑦 } ) ) = ( 𝑔 ∘ ( ( pmTrsp ‘ 𝐷 ) ‘ { 𝑥 , 𝑦 } ) ) )
117 3 36 6 symgcl ( ( 𝑔 ∈ ( Base ‘ 𝑆 ) ∧ ( ( pmTrsp ‘ 𝐷 ) ‘ { 𝑥 , 𝑦 } ) ∈ ( Base ‘ 𝑆 ) ) → ( 𝑔 + ( ( pmTrsp ‘ 𝐷 ) ‘ { 𝑥 , 𝑦 } ) ) ∈ ( Base ‘ 𝑆 ) )
118 21 47 117 syl2anc ( ( ( ( ( ( ( ( ( 𝜑𝑔 ∈ ( Base ‘ 𝑆 ) ) ∧ 𝑄 = ( ( 𝑔 + 𝑇 ) 𝑔 ) ) ∧ ¬ 𝑔𝐴 ) ∧ 𝑢 ∈ ( { 𝑤 ∈ Word 𝐷𝑤 : dom 𝑤1-1𝐷 } ∩ ( ♯ “ { 3 } ) ) ) ∧ ( 𝑀𝑢 ) = 𝑇 ) ∧ 𝑥 ∈ ( 𝐷 ∖ ran 𝑢 ) ) ∧ 𝑦 ∈ ( 𝐷 ∖ ran 𝑢 ) ) ∧ 𝑥𝑦 ) → ( 𝑔 + ( ( pmTrsp ‘ 𝐷 ) ‘ { 𝑥 , 𝑦 } ) ) ∈ ( Base ‘ 𝑆 ) )
119 116 118 eqeltrrd ( ( ( ( ( ( ( ( ( 𝜑𝑔 ∈ ( Base ‘ 𝑆 ) ) ∧ 𝑄 = ( ( 𝑔 + 𝑇 ) 𝑔 ) ) ∧ ¬ 𝑔𝐴 ) ∧ 𝑢 ∈ ( { 𝑤 ∈ Word 𝐷𝑤 : dom 𝑤1-1𝐷 } ∩ ( ♯ “ { 3 } ) ) ) ∧ ( 𝑀𝑢 ) = 𝑇 ) ∧ 𝑥 ∈ ( 𝐷 ∖ ran 𝑢 ) ) ∧ 𝑦 ∈ ( 𝐷 ∖ ran 𝑢 ) ) ∧ 𝑥𝑦 ) → ( 𝑔 ∘ ( ( pmTrsp ‘ 𝐷 ) ‘ { 𝑥 , 𝑦 } ) ) ∈ ( Base ‘ 𝑆 ) )
120 3 36 6 symgov ( ( ( 𝑔 ∘ ( ( pmTrsp ‘ 𝐷 ) ‘ { 𝑥 , 𝑦 } ) ) ∈ ( Base ‘ 𝑆 ) ∧ 𝑇 ∈ ( Base ‘ 𝑆 ) ) → ( ( 𝑔 ∘ ( ( pmTrsp ‘ 𝐷 ) ‘ { 𝑥 , 𝑦 } ) ) + 𝑇 ) = ( ( 𝑔 ∘ ( ( pmTrsp ‘ 𝐷 ) ‘ { 𝑥 , 𝑦 } ) ) ∘ 𝑇 ) )
121 119 71 120 syl2anc ( ( ( ( ( ( ( ( ( 𝜑𝑔 ∈ ( Base ‘ 𝑆 ) ) ∧ 𝑄 = ( ( 𝑔 + 𝑇 ) 𝑔 ) ) ∧ ¬ 𝑔𝐴 ) ∧ 𝑢 ∈ ( { 𝑤 ∈ Word 𝐷𝑤 : dom 𝑤1-1𝐷 } ∩ ( ♯ “ { 3 } ) ) ) ∧ ( 𝑀𝑢 ) = 𝑇 ) ∧ 𝑥 ∈ ( 𝐷 ∖ ran 𝑢 ) ) ∧ 𝑦 ∈ ( 𝐷 ∖ ran 𝑢 ) ) ∧ 𝑥𝑦 ) → ( ( 𝑔 ∘ ( ( pmTrsp ‘ 𝐷 ) ‘ { 𝑥 , 𝑦 } ) ) + 𝑇 ) = ( ( 𝑔 ∘ ( ( pmTrsp ‘ 𝐷 ) ‘ { 𝑥 , 𝑦 } ) ) ∘ 𝑇 ) )
122 coass ( ( 𝑔 ∘ ( ( pmTrsp ‘ 𝐷 ) ‘ { 𝑥 , 𝑦 } ) ) ∘ 𝑇 ) = ( 𝑔 ∘ ( ( ( pmTrsp ‘ 𝐷 ) ‘ { 𝑥 , 𝑦 } ) ∘ 𝑇 ) )
123 121 122 eqtrdi ( ( ( ( ( ( ( ( ( 𝜑𝑔 ∈ ( Base ‘ 𝑆 ) ) ∧ 𝑄 = ( ( 𝑔 + 𝑇 ) 𝑔 ) ) ∧ ¬ 𝑔𝐴 ) ∧ 𝑢 ∈ ( { 𝑤 ∈ Word 𝐷𝑤 : dom 𝑤1-1𝐷 } ∩ ( ♯ “ { 3 } ) ) ) ∧ ( 𝑀𝑢 ) = 𝑇 ) ∧ 𝑥 ∈ ( 𝐷 ∖ ran 𝑢 ) ) ∧ 𝑦 ∈ ( 𝐷 ∖ ran 𝑢 ) ) ∧ 𝑥𝑦 ) → ( ( 𝑔 ∘ ( ( pmTrsp ‘ 𝐷 ) ‘ { 𝑥 , 𝑦 } ) ) + 𝑇 ) = ( 𝑔 ∘ ( ( ( pmTrsp ‘ 𝐷 ) ‘ { 𝑥 , 𝑦 } ) ∘ 𝑇 ) ) )
124 coass ( ( 𝑔𝑇 ) ∘ ( ( pmTrsp ‘ 𝐷 ) ‘ { 𝑥 , 𝑦 } ) ) = ( 𝑔 ∘ ( 𝑇 ∘ ( ( pmTrsp ‘ 𝐷 ) ‘ { 𝑥 , 𝑦 } ) ) )
125 124 a1i ( ( ( ( ( ( ( ( ( 𝜑𝑔 ∈ ( Base ‘ 𝑆 ) ) ∧ 𝑄 = ( ( 𝑔 + 𝑇 ) 𝑔 ) ) ∧ ¬ 𝑔𝐴 ) ∧ 𝑢 ∈ ( { 𝑤 ∈ Word 𝐷𝑤 : dom 𝑤1-1𝐷 } ∩ ( ♯ “ { 3 } ) ) ) ∧ ( 𝑀𝑢 ) = 𝑇 ) ∧ 𝑥 ∈ ( 𝐷 ∖ ran 𝑢 ) ) ∧ 𝑦 ∈ ( 𝐷 ∖ ran 𝑢 ) ) ∧ 𝑥𝑦 ) → ( ( 𝑔𝑇 ) ∘ ( ( pmTrsp ‘ 𝐷 ) ‘ { 𝑥 , 𝑦 } ) ) = ( 𝑔 ∘ ( 𝑇 ∘ ( ( pmTrsp ‘ 𝐷 ) ‘ { 𝑥 , 𝑦 } ) ) ) )
126 114 123 125 3eqtr4d ( ( ( ( ( ( ( ( ( 𝜑𝑔 ∈ ( Base ‘ 𝑆 ) ) ∧ 𝑄 = ( ( 𝑔 + 𝑇 ) 𝑔 ) ) ∧ ¬ 𝑔𝐴 ) ∧ 𝑢 ∈ ( { 𝑤 ∈ Word 𝐷𝑤 : dom 𝑤1-1𝐷 } ∩ ( ♯ “ { 3 } ) ) ) ∧ ( 𝑀𝑢 ) = 𝑇 ) ∧ 𝑥 ∈ ( 𝐷 ∖ ran 𝑢 ) ) ∧ 𝑦 ∈ ( 𝐷 ∖ ran 𝑢 ) ) ∧ 𝑥𝑦 ) → ( ( 𝑔 ∘ ( ( pmTrsp ‘ 𝐷 ) ‘ { 𝑥 , 𝑦 } ) ) + 𝑇 ) = ( ( 𝑔𝑇 ) ∘ ( ( pmTrsp ‘ 𝐷 ) ‘ { 𝑥 , 𝑦 } ) ) )
127 cnvco ( 𝑔 ∘ ( ( pmTrsp ‘ 𝐷 ) ‘ { 𝑥 , 𝑦 } ) ) = ( ( ( pmTrsp ‘ 𝐷 ) ‘ { 𝑥 , 𝑦 } ) ∘ 𝑔 )
128 127 a1i ( ( ( ( ( ( ( ( ( 𝜑𝑔 ∈ ( Base ‘ 𝑆 ) ) ∧ 𝑄 = ( ( 𝑔 + 𝑇 ) 𝑔 ) ) ∧ ¬ 𝑔𝐴 ) ∧ 𝑢 ∈ ( { 𝑤 ∈ Word 𝐷𝑤 : dom 𝑤1-1𝐷 } ∩ ( ♯ “ { 3 } ) ) ) ∧ ( 𝑀𝑢 ) = 𝑇 ) ∧ 𝑥 ∈ ( 𝐷 ∖ ran 𝑢 ) ) ∧ 𝑦 ∈ ( 𝐷 ∖ ran 𝑢 ) ) ∧ 𝑥𝑦 ) → ( 𝑔 ∘ ( ( pmTrsp ‘ 𝐷 ) ‘ { 𝑥 , 𝑦 } ) ) = ( ( ( pmTrsp ‘ 𝐷 ) ‘ { 𝑥 , 𝑦 } ) ∘ 𝑔 ) )
129 126 128 coeq12d ( ( ( ( ( ( ( ( ( 𝜑𝑔 ∈ ( Base ‘ 𝑆 ) ) ∧ 𝑄 = ( ( 𝑔 + 𝑇 ) 𝑔 ) ) ∧ ¬ 𝑔𝐴 ) ∧ 𝑢 ∈ ( { 𝑤 ∈ Word 𝐷𝑤 : dom 𝑤1-1𝐷 } ∩ ( ♯ “ { 3 } ) ) ) ∧ ( 𝑀𝑢 ) = 𝑇 ) ∧ 𝑥 ∈ ( 𝐷 ∖ ran 𝑢 ) ) ∧ 𝑦 ∈ ( 𝐷 ∖ ran 𝑢 ) ) ∧ 𝑥𝑦 ) → ( ( ( 𝑔 ∘ ( ( pmTrsp ‘ 𝐷 ) ‘ { 𝑥 , 𝑦 } ) ) + 𝑇 ) ∘ ( 𝑔 ∘ ( ( pmTrsp ‘ 𝐷 ) ‘ { 𝑥 , 𝑦 } ) ) ) = ( ( ( 𝑔𝑇 ) ∘ ( ( pmTrsp ‘ 𝐷 ) ‘ { 𝑥 , 𝑦 } ) ) ∘ ( ( ( pmTrsp ‘ 𝐷 ) ‘ { 𝑥 , 𝑦 } ) ∘ 𝑔 ) ) )
130 coass ( ( ( ( 𝑔𝑇 ) ∘ ( ( pmTrsp ‘ 𝐷 ) ‘ { 𝑥 , 𝑦 } ) ) ∘ ( ( pmTrsp ‘ 𝐷 ) ‘ { 𝑥 , 𝑦 } ) ) ∘ 𝑔 ) = ( ( ( 𝑔𝑇 ) ∘ ( ( pmTrsp ‘ 𝐷 ) ‘ { 𝑥 , 𝑦 } ) ) ∘ ( ( ( pmTrsp ‘ 𝐷 ) ‘ { 𝑥 , 𝑦 } ) ∘ 𝑔 ) )
131 coass ( ( ( 𝑔𝑇 ) ∘ ( ( pmTrsp ‘ 𝐷 ) ‘ { 𝑥 , 𝑦 } ) ) ∘ ( ( pmTrsp ‘ 𝐷 ) ‘ { 𝑥 , 𝑦 } ) ) = ( ( 𝑔𝑇 ) ∘ ( ( ( pmTrsp ‘ 𝐷 ) ‘ { 𝑥 , 𝑦 } ) ∘ ( ( pmTrsp ‘ 𝐷 ) ‘ { 𝑥 , 𝑦 } ) ) )
132 131 coeq1i ( ( ( ( 𝑔𝑇 ) ∘ ( ( pmTrsp ‘ 𝐷 ) ‘ { 𝑥 , 𝑦 } ) ) ∘ ( ( pmTrsp ‘ 𝐷 ) ‘ { 𝑥 , 𝑦 } ) ) ∘ 𝑔 ) = ( ( ( 𝑔𝑇 ) ∘ ( ( ( pmTrsp ‘ 𝐷 ) ‘ { 𝑥 , 𝑦 } ) ∘ ( ( pmTrsp ‘ 𝐷 ) ‘ { 𝑥 , 𝑦 } ) ) ) ∘ 𝑔 )
133 130 132 eqtr3i ( ( ( 𝑔𝑇 ) ∘ ( ( pmTrsp ‘ 𝐷 ) ‘ { 𝑥 , 𝑦 } ) ) ∘ ( ( ( pmTrsp ‘ 𝐷 ) ‘ { 𝑥 , 𝑦 } ) ∘ 𝑔 ) ) = ( ( ( 𝑔𝑇 ) ∘ ( ( ( pmTrsp ‘ 𝐷 ) ‘ { 𝑥 , 𝑦 } ) ∘ ( ( pmTrsp ‘ 𝐷 ) ‘ { 𝑥 , 𝑦 } ) ) ) ∘ 𝑔 )
134 133 a1i ( ( ( ( ( ( ( ( ( 𝜑𝑔 ∈ ( Base ‘ 𝑆 ) ) ∧ 𝑄 = ( ( 𝑔 + 𝑇 ) 𝑔 ) ) ∧ ¬ 𝑔𝐴 ) ∧ 𝑢 ∈ ( { 𝑤 ∈ Word 𝐷𝑤 : dom 𝑤1-1𝐷 } ∩ ( ♯ “ { 3 } ) ) ) ∧ ( 𝑀𝑢 ) = 𝑇 ) ∧ 𝑥 ∈ ( 𝐷 ∖ ran 𝑢 ) ) ∧ 𝑦 ∈ ( 𝐷 ∖ ran 𝑢 ) ) ∧ 𝑥𝑦 ) → ( ( ( 𝑔𝑇 ) ∘ ( ( pmTrsp ‘ 𝐷 ) ‘ { 𝑥 , 𝑦 } ) ) ∘ ( ( ( pmTrsp ‘ 𝐷 ) ‘ { 𝑥 , 𝑦 } ) ∘ 𝑔 ) ) = ( ( ( 𝑔𝑇 ) ∘ ( ( ( pmTrsp ‘ 𝐷 ) ‘ { 𝑥 , 𝑦 } ) ∘ ( ( pmTrsp ‘ 𝐷 ) ‘ { 𝑥 , 𝑦 } ) ) ) ∘ 𝑔 ) )
135 3 36 6 symgov ( ( 𝑔 ∈ ( Base ‘ 𝑆 ) ∧ 𝑇 ∈ ( Base ‘ 𝑆 ) ) → ( 𝑔 + 𝑇 ) = ( 𝑔𝑇 ) )
136 21 71 135 syl2anc ( ( ( ( ( ( ( ( ( 𝜑𝑔 ∈ ( Base ‘ 𝑆 ) ) ∧ 𝑄 = ( ( 𝑔 + 𝑇 ) 𝑔 ) ) ∧ ¬ 𝑔𝐴 ) ∧ 𝑢 ∈ ( { 𝑤 ∈ Word 𝐷𝑤 : dom 𝑤1-1𝐷 } ∩ ( ♯ “ { 3 } ) ) ) ∧ ( 𝑀𝑢 ) = 𝑇 ) ∧ 𝑥 ∈ ( 𝐷 ∖ ran 𝑢 ) ) ∧ 𝑦 ∈ ( 𝐷 ∖ ran 𝑢 ) ) ∧ 𝑥𝑦 ) → ( 𝑔 + 𝑇 ) = ( 𝑔𝑇 ) )
137 3 36 6 symgcl ( ( 𝑔 ∈ ( Base ‘ 𝑆 ) ∧ 𝑇 ∈ ( Base ‘ 𝑆 ) ) → ( 𝑔 + 𝑇 ) ∈ ( Base ‘ 𝑆 ) )
138 21 71 137 syl2anc ( ( ( ( ( ( ( ( ( 𝜑𝑔 ∈ ( Base ‘ 𝑆 ) ) ∧ 𝑄 = ( ( 𝑔 + 𝑇 ) 𝑔 ) ) ∧ ¬ 𝑔𝐴 ) ∧ 𝑢 ∈ ( { 𝑤 ∈ Word 𝐷𝑤 : dom 𝑤1-1𝐷 } ∩ ( ♯ “ { 3 } ) ) ) ∧ ( 𝑀𝑢 ) = 𝑇 ) ∧ 𝑥 ∈ ( 𝐷 ∖ ran 𝑢 ) ) ∧ 𝑦 ∈ ( 𝐷 ∖ ran 𝑢 ) ) ∧ 𝑥𝑦 ) → ( 𝑔 + 𝑇 ) ∈ ( Base ‘ 𝑆 ) )
139 136 138 eqeltrrd ( ( ( ( ( ( ( ( ( 𝜑𝑔 ∈ ( Base ‘ 𝑆 ) ) ∧ 𝑄 = ( ( 𝑔 + 𝑇 ) 𝑔 ) ) ∧ ¬ 𝑔𝐴 ) ∧ 𝑢 ∈ ( { 𝑤 ∈ Word 𝐷𝑤 : dom 𝑤1-1𝐷 } ∩ ( ♯ “ { 3 } ) ) ) ∧ ( 𝑀𝑢 ) = 𝑇 ) ∧ 𝑥 ∈ ( 𝐷 ∖ ran 𝑢 ) ) ∧ 𝑦 ∈ ( 𝐷 ∖ ran 𝑢 ) ) ∧ 𝑥𝑦 ) → ( 𝑔𝑇 ) ∈ ( Base ‘ 𝑆 ) )
140 3 36 symgbasf ( ( 𝑔𝑇 ) ∈ ( Base ‘ 𝑆 ) → ( 𝑔𝑇 ) : 𝐷𝐷 )
141 fcoi1 ( ( 𝑔𝑇 ) : 𝐷𝐷 → ( ( 𝑔𝑇 ) ∘ ( I ↾ 𝐷 ) ) = ( 𝑔𝑇 ) )
142 139 140 141 3syl ( ( ( ( ( ( ( ( ( 𝜑𝑔 ∈ ( Base ‘ 𝑆 ) ) ∧ 𝑄 = ( ( 𝑔 + 𝑇 ) 𝑔 ) ) ∧ ¬ 𝑔𝐴 ) ∧ 𝑢 ∈ ( { 𝑤 ∈ Word 𝐷𝑤 : dom 𝑤1-1𝐷 } ∩ ( ♯ “ { 3 } ) ) ) ∧ ( 𝑀𝑢 ) = 𝑇 ) ∧ 𝑥 ∈ ( 𝐷 ∖ ran 𝑢 ) ) ∧ 𝑦 ∈ ( 𝐷 ∖ ran 𝑢 ) ) ∧ 𝑥𝑦 ) → ( ( 𝑔𝑇 ) ∘ ( I ↾ 𝐷 ) ) = ( 𝑔𝑇 ) )
143 3 36 elsymgbas ( 𝐷 ∈ Fin → ( ( ( pmTrsp ‘ 𝐷 ) ‘ { 𝑥 , 𝑦 } ) ∈ ( Base ‘ 𝑆 ) ↔ ( ( pmTrsp ‘ 𝐷 ) ‘ { 𝑥 , 𝑦 } ) : 𝐷1-1-onto𝐷 ) )
144 143 biimpa ( ( 𝐷 ∈ Fin ∧ ( ( pmTrsp ‘ 𝐷 ) ‘ { 𝑥 , 𝑦 } ) ∈ ( Base ‘ 𝑆 ) ) → ( ( pmTrsp ‘ 𝐷 ) ‘ { 𝑥 , 𝑦 } ) : 𝐷1-1-onto𝐷 )
145 20 47 144 syl2anc ( ( ( ( ( ( ( ( ( 𝜑𝑔 ∈ ( Base ‘ 𝑆 ) ) ∧ 𝑄 = ( ( 𝑔 + 𝑇 ) 𝑔 ) ) ∧ ¬ 𝑔𝐴 ) ∧ 𝑢 ∈ ( { 𝑤 ∈ Word 𝐷𝑤 : dom 𝑤1-1𝐷 } ∩ ( ♯ “ { 3 } ) ) ) ∧ ( 𝑀𝑢 ) = 𝑇 ) ∧ 𝑥 ∈ ( 𝐷 ∖ ran 𝑢 ) ) ∧ 𝑦 ∈ ( 𝐷 ∖ ran 𝑢 ) ) ∧ 𝑥𝑦 ) → ( ( pmTrsp ‘ 𝐷 ) ‘ { 𝑥 , 𝑦 } ) : 𝐷1-1-onto𝐷 )
146 f1ococnv2 ( ( ( pmTrsp ‘ 𝐷 ) ‘ { 𝑥 , 𝑦 } ) : 𝐷1-1-onto𝐷 → ( ( ( pmTrsp ‘ 𝐷 ) ‘ { 𝑥 , 𝑦 } ) ∘ ( ( pmTrsp ‘ 𝐷 ) ‘ { 𝑥 , 𝑦 } ) ) = ( I ↾ 𝐷 ) )
147 145 146 syl ( ( ( ( ( ( ( ( ( 𝜑𝑔 ∈ ( Base ‘ 𝑆 ) ) ∧ 𝑄 = ( ( 𝑔 + 𝑇 ) 𝑔 ) ) ∧ ¬ 𝑔𝐴 ) ∧ 𝑢 ∈ ( { 𝑤 ∈ Word 𝐷𝑤 : dom 𝑤1-1𝐷 } ∩ ( ♯ “ { 3 } ) ) ) ∧ ( 𝑀𝑢 ) = 𝑇 ) ∧ 𝑥 ∈ ( 𝐷 ∖ ran 𝑢 ) ) ∧ 𝑦 ∈ ( 𝐷 ∖ ran 𝑢 ) ) ∧ 𝑥𝑦 ) → ( ( ( pmTrsp ‘ 𝐷 ) ‘ { 𝑥 , 𝑦 } ) ∘ ( ( pmTrsp ‘ 𝐷 ) ‘ { 𝑥 , 𝑦 } ) ) = ( I ↾ 𝐷 ) )
148 147 coeq2d ( ( ( ( ( ( ( ( ( 𝜑𝑔 ∈ ( Base ‘ 𝑆 ) ) ∧ 𝑄 = ( ( 𝑔 + 𝑇 ) 𝑔 ) ) ∧ ¬ 𝑔𝐴 ) ∧ 𝑢 ∈ ( { 𝑤 ∈ Word 𝐷𝑤 : dom 𝑤1-1𝐷 } ∩ ( ♯ “ { 3 } ) ) ) ∧ ( 𝑀𝑢 ) = 𝑇 ) ∧ 𝑥 ∈ ( 𝐷 ∖ ran 𝑢 ) ) ∧ 𝑦 ∈ ( 𝐷 ∖ ran 𝑢 ) ) ∧ 𝑥𝑦 ) → ( ( 𝑔𝑇 ) ∘ ( ( ( pmTrsp ‘ 𝐷 ) ‘ { 𝑥 , 𝑦 } ) ∘ ( ( pmTrsp ‘ 𝐷 ) ‘ { 𝑥 , 𝑦 } ) ) ) = ( ( 𝑔𝑇 ) ∘ ( I ↾ 𝐷 ) ) )
149 142 148 136 3eqtr4d ( ( ( ( ( ( ( ( ( 𝜑𝑔 ∈ ( Base ‘ 𝑆 ) ) ∧ 𝑄 = ( ( 𝑔 + 𝑇 ) 𝑔 ) ) ∧ ¬ 𝑔𝐴 ) ∧ 𝑢 ∈ ( { 𝑤 ∈ Word 𝐷𝑤 : dom 𝑤1-1𝐷 } ∩ ( ♯ “ { 3 } ) ) ) ∧ ( 𝑀𝑢 ) = 𝑇 ) ∧ 𝑥 ∈ ( 𝐷 ∖ ran 𝑢 ) ) ∧ 𝑦 ∈ ( 𝐷 ∖ ran 𝑢 ) ) ∧ 𝑥𝑦 ) → ( ( 𝑔𝑇 ) ∘ ( ( ( pmTrsp ‘ 𝐷 ) ‘ { 𝑥 , 𝑦 } ) ∘ ( ( pmTrsp ‘ 𝐷 ) ‘ { 𝑥 , 𝑦 } ) ) ) = ( 𝑔 + 𝑇 ) )
150 149 coeq1d ( ( ( ( ( ( ( ( ( 𝜑𝑔 ∈ ( Base ‘ 𝑆 ) ) ∧ 𝑄 = ( ( 𝑔 + 𝑇 ) 𝑔 ) ) ∧ ¬ 𝑔𝐴 ) ∧ 𝑢 ∈ ( { 𝑤 ∈ Word 𝐷𝑤 : dom 𝑤1-1𝐷 } ∩ ( ♯ “ { 3 } ) ) ) ∧ ( 𝑀𝑢 ) = 𝑇 ) ∧ 𝑥 ∈ ( 𝐷 ∖ ran 𝑢 ) ) ∧ 𝑦 ∈ ( 𝐷 ∖ ran 𝑢 ) ) ∧ 𝑥𝑦 ) → ( ( ( 𝑔𝑇 ) ∘ ( ( ( pmTrsp ‘ 𝐷 ) ‘ { 𝑥 , 𝑦 } ) ∘ ( ( pmTrsp ‘ 𝐷 ) ‘ { 𝑥 , 𝑦 } ) ) ) ∘ 𝑔 ) = ( ( 𝑔 + 𝑇 ) ∘ 𝑔 ) )
151 3 36 7 symgsubg ( ( ( 𝑔 + 𝑇 ) ∈ ( Base ‘ 𝑆 ) ∧ 𝑔 ∈ ( Base ‘ 𝑆 ) ) → ( ( 𝑔 + 𝑇 ) 𝑔 ) = ( ( 𝑔 + 𝑇 ) ∘ 𝑔 ) )
152 138 21 151 syl2anc ( ( ( ( ( ( ( ( ( 𝜑𝑔 ∈ ( Base ‘ 𝑆 ) ) ∧ 𝑄 = ( ( 𝑔 + 𝑇 ) 𝑔 ) ) ∧ ¬ 𝑔𝐴 ) ∧ 𝑢 ∈ ( { 𝑤 ∈ Word 𝐷𝑤 : dom 𝑤1-1𝐷 } ∩ ( ♯ “ { 3 } ) ) ) ∧ ( 𝑀𝑢 ) = 𝑇 ) ∧ 𝑥 ∈ ( 𝐷 ∖ ran 𝑢 ) ) ∧ 𝑦 ∈ ( 𝐷 ∖ ran 𝑢 ) ) ∧ 𝑥𝑦 ) → ( ( 𝑔 + 𝑇 ) 𝑔 ) = ( ( 𝑔 + 𝑇 ) ∘ 𝑔 ) )
153 150 152 eqtr4d ( ( ( ( ( ( ( ( ( 𝜑𝑔 ∈ ( Base ‘ 𝑆 ) ) ∧ 𝑄 = ( ( 𝑔 + 𝑇 ) 𝑔 ) ) ∧ ¬ 𝑔𝐴 ) ∧ 𝑢 ∈ ( { 𝑤 ∈ Word 𝐷𝑤 : dom 𝑤1-1𝐷 } ∩ ( ♯ “ { 3 } ) ) ) ∧ ( 𝑀𝑢 ) = 𝑇 ) ∧ 𝑥 ∈ ( 𝐷 ∖ ran 𝑢 ) ) ∧ 𝑦 ∈ ( 𝐷 ∖ ran 𝑢 ) ) ∧ 𝑥𝑦 ) → ( ( ( 𝑔𝑇 ) ∘ ( ( ( pmTrsp ‘ 𝐷 ) ‘ { 𝑥 , 𝑦 } ) ∘ ( ( pmTrsp ‘ 𝐷 ) ‘ { 𝑥 , 𝑦 } ) ) ) ∘ 𝑔 ) = ( ( 𝑔 + 𝑇 ) 𝑔 ) )
154 129 134 153 3eqtrd ( ( ( ( ( ( ( ( ( 𝜑𝑔 ∈ ( Base ‘ 𝑆 ) ) ∧ 𝑄 = ( ( 𝑔 + 𝑇 ) 𝑔 ) ) ∧ ¬ 𝑔𝐴 ) ∧ 𝑢 ∈ ( { 𝑤 ∈ Word 𝐷𝑤 : dom 𝑤1-1𝐷 } ∩ ( ♯ “ { 3 } ) ) ) ∧ ( 𝑀𝑢 ) = 𝑇 ) ∧ 𝑥 ∈ ( 𝐷 ∖ ran 𝑢 ) ) ∧ 𝑦 ∈ ( 𝐷 ∖ ran 𝑢 ) ) ∧ 𝑥𝑦 ) → ( ( ( 𝑔 ∘ ( ( pmTrsp ‘ 𝐷 ) ‘ { 𝑥 , 𝑦 } ) ) + 𝑇 ) ∘ ( 𝑔 ∘ ( ( pmTrsp ‘ 𝐷 ) ‘ { 𝑥 , 𝑦 } ) ) ) = ( ( 𝑔 + 𝑇 ) 𝑔 ) )
155 3 symggrp ( 𝐷 ∈ Fin → 𝑆 ∈ Grp )
156 9 155 syl ( 𝜑𝑆 ∈ Grp )
157 156 ad8antr ( ( ( ( ( ( ( ( ( 𝜑𝑔 ∈ ( Base ‘ 𝑆 ) ) ∧ 𝑄 = ( ( 𝑔 + 𝑇 ) 𝑔 ) ) ∧ ¬ 𝑔𝐴 ) ∧ 𝑢 ∈ ( { 𝑤 ∈ Word 𝐷𝑤 : dom 𝑤1-1𝐷 } ∩ ( ♯ “ { 3 } ) ) ) ∧ ( 𝑀𝑢 ) = 𝑇 ) ∧ 𝑥 ∈ ( 𝐷 ∖ ran 𝑢 ) ) ∧ 𝑦 ∈ ( 𝐷 ∖ ran 𝑢 ) ) ∧ 𝑥𝑦 ) → 𝑆 ∈ Grp )
158 36 6 grpcl ( ( 𝑆 ∈ Grp ∧ ( 𝑔 ∘ ( ( pmTrsp ‘ 𝐷 ) ‘ { 𝑥 , 𝑦 } ) ) ∈ ( Base ‘ 𝑆 ) ∧ 𝑇 ∈ ( Base ‘ 𝑆 ) ) → ( ( 𝑔 ∘ ( ( pmTrsp ‘ 𝐷 ) ‘ { 𝑥 , 𝑦 } ) ) + 𝑇 ) ∈ ( Base ‘ 𝑆 ) )
159 157 119 71 158 syl3anc ( ( ( ( ( ( ( ( ( 𝜑𝑔 ∈ ( Base ‘ 𝑆 ) ) ∧ 𝑄 = ( ( 𝑔 + 𝑇 ) 𝑔 ) ) ∧ ¬ 𝑔𝐴 ) ∧ 𝑢 ∈ ( { 𝑤 ∈ Word 𝐷𝑤 : dom 𝑤1-1𝐷 } ∩ ( ♯ “ { 3 } ) ) ) ∧ ( 𝑀𝑢 ) = 𝑇 ) ∧ 𝑥 ∈ ( 𝐷 ∖ ran 𝑢 ) ) ∧ 𝑦 ∈ ( 𝐷 ∖ ran 𝑢 ) ) ∧ 𝑥𝑦 ) → ( ( 𝑔 ∘ ( ( pmTrsp ‘ 𝐷 ) ‘ { 𝑥 , 𝑦 } ) ) + 𝑇 ) ∈ ( Base ‘ 𝑆 ) )
160 3 36 7 symgsubg ( ( ( ( 𝑔 ∘ ( ( pmTrsp ‘ 𝐷 ) ‘ { 𝑥 , 𝑦 } ) ) + 𝑇 ) ∈ ( Base ‘ 𝑆 ) ∧ ( 𝑔 ∘ ( ( pmTrsp ‘ 𝐷 ) ‘ { 𝑥 , 𝑦 } ) ) ∈ ( Base ‘ 𝑆 ) ) → ( ( ( 𝑔 ∘ ( ( pmTrsp ‘ 𝐷 ) ‘ { 𝑥 , 𝑦 } ) ) + 𝑇 ) ( 𝑔 ∘ ( ( pmTrsp ‘ 𝐷 ) ‘ { 𝑥 , 𝑦 } ) ) ) = ( ( ( 𝑔 ∘ ( ( pmTrsp ‘ 𝐷 ) ‘ { 𝑥 , 𝑦 } ) ) + 𝑇 ) ∘ ( 𝑔 ∘ ( ( pmTrsp ‘ 𝐷 ) ‘ { 𝑥 , 𝑦 } ) ) ) )
161 159 119 160 syl2anc ( ( ( ( ( ( ( ( ( 𝜑𝑔 ∈ ( Base ‘ 𝑆 ) ) ∧ 𝑄 = ( ( 𝑔 + 𝑇 ) 𝑔 ) ) ∧ ¬ 𝑔𝐴 ) ∧ 𝑢 ∈ ( { 𝑤 ∈ Word 𝐷𝑤 : dom 𝑤1-1𝐷 } ∩ ( ♯ “ { 3 } ) ) ) ∧ ( 𝑀𝑢 ) = 𝑇 ) ∧ 𝑥 ∈ ( 𝐷 ∖ ran 𝑢 ) ) ∧ 𝑦 ∈ ( 𝐷 ∖ ran 𝑢 ) ) ∧ 𝑥𝑦 ) → ( ( ( 𝑔 ∘ ( ( pmTrsp ‘ 𝐷 ) ‘ { 𝑥 , 𝑦 } ) ) + 𝑇 ) ( 𝑔 ∘ ( ( pmTrsp ‘ 𝐷 ) ‘ { 𝑥 , 𝑦 } ) ) ) = ( ( ( 𝑔 ∘ ( ( pmTrsp ‘ 𝐷 ) ‘ { 𝑥 , 𝑦 } ) ) + 𝑇 ) ∘ ( 𝑔 ∘ ( ( pmTrsp ‘ 𝐷 ) ‘ { 𝑥 , 𝑦 } ) ) ) )
162 simp-7r ( ( ( ( ( ( ( ( ( 𝜑𝑔 ∈ ( Base ‘ 𝑆 ) ) ∧ 𝑄 = ( ( 𝑔 + 𝑇 ) 𝑔 ) ) ∧ ¬ 𝑔𝐴 ) ∧ 𝑢 ∈ ( { 𝑤 ∈ Word 𝐷𝑤 : dom 𝑤1-1𝐷 } ∩ ( ♯ “ { 3 } ) ) ) ∧ ( 𝑀𝑢 ) = 𝑇 ) ∧ 𝑥 ∈ ( 𝐷 ∖ ran 𝑢 ) ) ∧ 𝑦 ∈ ( 𝐷 ∖ ran 𝑢 ) ) ∧ 𝑥𝑦 ) → 𝑄 = ( ( 𝑔 + 𝑇 ) 𝑔 ) )
163 154 161 162 3eqtr4rd ( ( ( ( ( ( ( ( ( 𝜑𝑔 ∈ ( Base ‘ 𝑆 ) ) ∧ 𝑄 = ( ( 𝑔 + 𝑇 ) 𝑔 ) ) ∧ ¬ 𝑔𝐴 ) ∧ 𝑢 ∈ ( { 𝑤 ∈ Word 𝐷𝑤 : dom 𝑤1-1𝐷 } ∩ ( ♯ “ { 3 } ) ) ) ∧ ( 𝑀𝑢 ) = 𝑇 ) ∧ 𝑥 ∈ ( 𝐷 ∖ ran 𝑢 ) ) ∧ 𝑦 ∈ ( 𝐷 ∖ ran 𝑢 ) ) ∧ 𝑥𝑦 ) → 𝑄 = ( ( ( 𝑔 ∘ ( ( pmTrsp ‘ 𝐷 ) ‘ { 𝑥 , 𝑦 } ) ) + 𝑇 ) ( 𝑔 ∘ ( ( pmTrsp ‘ 𝐷 ) ‘ { 𝑥 , 𝑦 } ) ) ) )
164 42 46 163 rspcedvd ( ( ( ( ( ( ( ( ( 𝜑𝑔 ∈ ( Base ‘ 𝑆 ) ) ∧ 𝑄 = ( ( 𝑔 + 𝑇 ) 𝑔 ) ) ∧ ¬ 𝑔𝐴 ) ∧ 𝑢 ∈ ( { 𝑤 ∈ Word 𝐷𝑤 : dom 𝑤1-1𝐷 } ∩ ( ♯ “ { 3 } ) ) ) ∧ ( 𝑀𝑢 ) = 𝑇 ) ∧ 𝑥 ∈ ( 𝐷 ∖ ran 𝑢 ) ) ∧ 𝑦 ∈ ( 𝐷 ∖ ran 𝑢 ) ) ∧ 𝑥𝑦 ) → ∃ 𝑝𝐴 𝑄 = ( ( 𝑝 + 𝑇 ) 𝑝 ) )
165 9 difexd ( 𝜑 → ( 𝐷 ∖ ran 𝑢 ) ∈ V )
166 165 ad5antr ( ( ( ( ( ( 𝜑𝑔 ∈ ( Base ‘ 𝑆 ) ) ∧ 𝑄 = ( ( 𝑔 + 𝑇 ) 𝑔 ) ) ∧ ¬ 𝑔𝐴 ) ∧ 𝑢 ∈ ( { 𝑤 ∈ Word 𝐷𝑤 : dom 𝑤1-1𝐷 } ∩ ( ♯ “ { 3 } ) ) ) ∧ ( 𝑀𝑢 ) = 𝑇 ) → ( 𝐷 ∖ ran 𝑢 ) ∈ V )
167 3p2e5 ( 3 + 2 ) = 5
168 167 8 eqbrtrid ( 𝜑 → ( 3 + 2 ) ≤ 𝑁 )
169 2re 2 ∈ ℝ
170 169 a1i ( 𝜑 → 2 ∈ ℝ )
171 56 170 62 leaddsub2d ( 𝜑 → ( ( 3 + 2 ) ≤ 𝑁 ↔ 2 ≤ ( 𝑁 − 3 ) ) )
172 168 171 mpbid ( 𝜑 → 2 ≤ ( 𝑁 − 3 ) )
173 172 ad5antr ( ( ( ( ( ( 𝜑𝑔 ∈ ( Base ‘ 𝑆 ) ) ∧ 𝑄 = ( ( 𝑔 + 𝑇 ) 𝑔 ) ) ∧ ¬ 𝑔𝐴 ) ∧ 𝑢 ∈ ( { 𝑤 ∈ Word 𝐷𝑤 : dom 𝑤1-1𝐷 } ∩ ( ♯ “ { 3 } ) ) ) ∧ ( 𝑀𝑢 ) = 𝑇 ) → 2 ≤ ( 𝑁 − 3 ) )
174 4 a1i ( ( ( ( ( ( 𝜑𝑔 ∈ ( Base ‘ 𝑆 ) ) ∧ 𝑄 = ( ( 𝑔 + 𝑇 ) 𝑔 ) ) ∧ ¬ 𝑔𝐴 ) ∧ 𝑢 ∈ ( { 𝑤 ∈ Word 𝐷𝑤 : dom 𝑤1-1𝐷 } ∩ ( ♯ “ { 3 } ) ) ) ∧ ( 𝑀𝑢 ) = 𝑇 ) → 𝑁 = ( ♯ ‘ 𝐷 ) )
175 78 elin2d ( ( ( ( ( ( 𝜑𝑔 ∈ ( Base ‘ 𝑆 ) ) ∧ 𝑄 = ( ( 𝑔 + 𝑇 ) 𝑔 ) ) ∧ ¬ 𝑔𝐴 ) ∧ 𝑢 ∈ ( { 𝑤 ∈ Word 𝐷𝑤 : dom 𝑤1-1𝐷 } ∩ ( ♯ “ { 3 } ) ) ) ∧ ( 𝑀𝑢 ) = 𝑇 ) → 𝑢 ∈ ( ♯ “ { 3 } ) )
176 hashf ♯ : V ⟶ ( ℕ0 ∪ { +∞ } )
177 ffn ( ♯ : V ⟶ ( ℕ0 ∪ { +∞ } ) → ♯ Fn V )
178 fniniseg ( ♯ Fn V → ( 𝑢 ∈ ( ♯ “ { 3 } ) ↔ ( 𝑢 ∈ V ∧ ( ♯ ‘ 𝑢 ) = 3 ) ) )
179 176 177 178 mp2b ( 𝑢 ∈ ( ♯ “ { 3 } ) ↔ ( 𝑢 ∈ V ∧ ( ♯ ‘ 𝑢 ) = 3 ) )
180 179 simprbi ( 𝑢 ∈ ( ♯ “ { 3 } ) → ( ♯ ‘ 𝑢 ) = 3 )
181 175 180 syl ( ( ( ( ( ( 𝜑𝑔 ∈ ( Base ‘ 𝑆 ) ) ∧ 𝑄 = ( ( 𝑔 + 𝑇 ) 𝑔 ) ) ∧ ¬ 𝑔𝐴 ) ∧ 𝑢 ∈ ( { 𝑤 ∈ Word 𝐷𝑤 : dom 𝑤1-1𝐷 } ∩ ( ♯ “ { 3 } ) ) ) ∧ ( 𝑀𝑢 ) = 𝑇 ) → ( ♯ ‘ 𝑢 ) = 3 )
182 vex 𝑢 ∈ V
183 182 dmex dom 𝑢 ∈ V
184 hashf1rn ( ( dom 𝑢 ∈ V ∧ 𝑢 : dom 𝑢1-1𝐷 ) → ( ♯ ‘ 𝑢 ) = ( ♯ ‘ ran 𝑢 ) )
185 183 86 184 sylancr ( ( ( ( ( ( 𝜑𝑔 ∈ ( Base ‘ 𝑆 ) ) ∧ 𝑄 = ( ( 𝑔 + 𝑇 ) 𝑔 ) ) ∧ ¬ 𝑔𝐴 ) ∧ 𝑢 ∈ ( { 𝑤 ∈ Word 𝐷𝑤 : dom 𝑤1-1𝐷 } ∩ ( ♯ “ { 3 } ) ) ) ∧ ( 𝑀𝑢 ) = 𝑇 ) → ( ♯ ‘ 𝑢 ) = ( ♯ ‘ ran 𝑢 ) )
186 181 185 eqtr3d ( ( ( ( ( ( 𝜑𝑔 ∈ ( Base ‘ 𝑆 ) ) ∧ 𝑄 = ( ( 𝑔 + 𝑇 ) 𝑔 ) ) ∧ ¬ 𝑔𝐴 ) ∧ 𝑢 ∈ ( { 𝑤 ∈ Word 𝐷𝑤 : dom 𝑤1-1𝐷 } ∩ ( ♯ “ { 3 } ) ) ) ∧ ( 𝑀𝑢 ) = 𝑇 ) → 3 = ( ♯ ‘ ran 𝑢 ) )
187 174 186 oveq12d ( ( ( ( ( ( 𝜑𝑔 ∈ ( Base ‘ 𝑆 ) ) ∧ 𝑄 = ( ( 𝑔 + 𝑇 ) 𝑔 ) ) ∧ ¬ 𝑔𝐴 ) ∧ 𝑢 ∈ ( { 𝑤 ∈ Word 𝐷𝑤 : dom 𝑤1-1𝐷 } ∩ ( ♯ “ { 3 } ) ) ) ∧ ( 𝑀𝑢 ) = 𝑇 ) → ( 𝑁 − 3 ) = ( ( ♯ ‘ 𝐷 ) − ( ♯ ‘ ran 𝑢 ) ) )
188 173 187 breqtrd ( ( ( ( ( ( 𝜑𝑔 ∈ ( Base ‘ 𝑆 ) ) ∧ 𝑄 = ( ( 𝑔 + 𝑇 ) 𝑔 ) ) ∧ ¬ 𝑔𝐴 ) ∧ 𝑢 ∈ ( { 𝑤 ∈ Word 𝐷𝑤 : dom 𝑤1-1𝐷 } ∩ ( ♯ “ { 3 } ) ) ) ∧ ( 𝑀𝑢 ) = 𝑇 ) → 2 ≤ ( ( ♯ ‘ 𝐷 ) − ( ♯ ‘ ran 𝑢 ) ) )
189 hashssdif ( ( 𝐷 ∈ Fin ∧ ran 𝑢𝐷 ) → ( ♯ ‘ ( 𝐷 ∖ ran 𝑢 ) ) = ( ( ♯ ‘ 𝐷 ) − ( ♯ ‘ ran 𝑢 ) ) )
190 19 89 189 syl2anc ( ( ( ( ( ( 𝜑𝑔 ∈ ( Base ‘ 𝑆 ) ) ∧ 𝑄 = ( ( 𝑔 + 𝑇 ) 𝑔 ) ) ∧ ¬ 𝑔𝐴 ) ∧ 𝑢 ∈ ( { 𝑤 ∈ Word 𝐷𝑤 : dom 𝑤1-1𝐷 } ∩ ( ♯ “ { 3 } ) ) ) ∧ ( 𝑀𝑢 ) = 𝑇 ) → ( ♯ ‘ ( 𝐷 ∖ ran 𝑢 ) ) = ( ( ♯ ‘ 𝐷 ) − ( ♯ ‘ ran 𝑢 ) ) )
191 188 190 breqtrrd ( ( ( ( ( ( 𝜑𝑔 ∈ ( Base ‘ 𝑆 ) ) ∧ 𝑄 = ( ( 𝑔 + 𝑇 ) 𝑔 ) ) ∧ ¬ 𝑔𝐴 ) ∧ 𝑢 ∈ ( { 𝑤 ∈ Word 𝐷𝑤 : dom 𝑤1-1𝐷 } ∩ ( ♯ “ { 3 } ) ) ) ∧ ( 𝑀𝑢 ) = 𝑇 ) → 2 ≤ ( ♯ ‘ ( 𝐷 ∖ ran 𝑢 ) ) )
192 hashge2el2dif ( ( ( 𝐷 ∖ ran 𝑢 ) ∈ V ∧ 2 ≤ ( ♯ ‘ ( 𝐷 ∖ ran 𝑢 ) ) ) → ∃ 𝑥 ∈ ( 𝐷 ∖ ran 𝑢 ) ∃ 𝑦 ∈ ( 𝐷 ∖ ran 𝑢 ) 𝑥𝑦 )
193 166 191 192 syl2anc ( ( ( ( ( ( 𝜑𝑔 ∈ ( Base ‘ 𝑆 ) ) ∧ 𝑄 = ( ( 𝑔 + 𝑇 ) 𝑔 ) ) ∧ ¬ 𝑔𝐴 ) ∧ 𝑢 ∈ ( { 𝑤 ∈ Word 𝐷𝑤 : dom 𝑤1-1𝐷 } ∩ ( ♯ “ { 3 } ) ) ) ∧ ( 𝑀𝑢 ) = 𝑇 ) → ∃ 𝑥 ∈ ( 𝐷 ∖ ran 𝑢 ) ∃ 𝑦 ∈ ( 𝐷 ∖ ran 𝑢 ) 𝑥𝑦 )
194 164 193 r19.29vva ( ( ( ( ( ( 𝜑𝑔 ∈ ( Base ‘ 𝑆 ) ) ∧ 𝑄 = ( ( 𝑔 + 𝑇 ) 𝑔 ) ) ∧ ¬ 𝑔𝐴 ) ∧ 𝑢 ∈ ( { 𝑤 ∈ Word 𝐷𝑤 : dom 𝑤1-1𝐷 } ∩ ( ♯ “ { 3 } ) ) ) ∧ ( 𝑀𝑢 ) = 𝑇 ) → ∃ 𝑝𝐴 𝑄 = ( ( 𝑝 + 𝑇 ) 𝑝 ) )
195 nfcv 𝑢 𝑀
196 5 3 36 tocycf ( 𝐷 ∈ Fin → 𝑀 : { 𝑤 ∈ Word 𝐷𝑤 : dom 𝑤1-1𝐷 } ⟶ ( Base ‘ 𝑆 ) )
197 ffn ( 𝑀 : { 𝑤 ∈ Word 𝐷𝑤 : dom 𝑤1-1𝐷 } ⟶ ( Base ‘ 𝑆 ) → 𝑀 Fn { 𝑤 ∈ Word 𝐷𝑤 : dom 𝑤1-1𝐷 } )
198 9 196 197 3syl ( 𝜑𝑀 Fn { 𝑤 ∈ Word 𝐷𝑤 : dom 𝑤1-1𝐷 } )
199 11 1 eleqtrdi ( 𝜑𝑇 ∈ ( 𝑀 “ ( ♯ “ { 3 } ) ) )
200 195 198 199 fvelimad ( 𝜑 → ∃ 𝑢 ∈ ( { 𝑤 ∈ Word 𝐷𝑤 : dom 𝑤1-1𝐷 } ∩ ( ♯ “ { 3 } ) ) ( 𝑀𝑢 ) = 𝑇 )
201 200 ad3antrrr ( ( ( ( 𝜑𝑔 ∈ ( Base ‘ 𝑆 ) ) ∧ 𝑄 = ( ( 𝑔 + 𝑇 ) 𝑔 ) ) ∧ ¬ 𝑔𝐴 ) → ∃ 𝑢 ∈ ( { 𝑤 ∈ Word 𝐷𝑤 : dom 𝑤1-1𝐷 } ∩ ( ♯ “ { 3 } ) ) ( 𝑀𝑢 ) = 𝑇 )
202 194 201 r19.29a ( ( ( ( 𝜑𝑔 ∈ ( Base ‘ 𝑆 ) ) ∧ 𝑄 = ( ( 𝑔 + 𝑇 ) 𝑔 ) ) ∧ ¬ 𝑔𝐴 ) → ∃ 𝑝𝐴 𝑄 = ( ( 𝑝 + 𝑇 ) 𝑝 ) )
203 18 202 pm2.61dan ( ( ( 𝜑𝑔 ∈ ( Base ‘ 𝑆 ) ) ∧ 𝑄 = ( ( 𝑔 + 𝑇 ) 𝑔 ) ) → ∃ 𝑝𝐴 𝑄 = ( ( 𝑝 + 𝑇 ) 𝑝 ) )
204 1 3 4 5 36 6 7 67 9 10 11 cycpmconjs ( 𝜑 → ∃ 𝑔 ∈ ( Base ‘ 𝑆 ) 𝑄 = ( ( 𝑔 + 𝑇 ) 𝑔 ) )
205 203 204 r19.29a ( 𝜑 → ∃ 𝑝𝐴 𝑄 = ( ( 𝑝 + 𝑇 ) 𝑝 ) )