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 enpr2 ⊢ ( ( 𝑥 ∈ ( 𝐷 ∖ 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 ⊢ ( 𝜑 → ∃ 𝑝 ∈ 𝐴 𝑄 = ( ( 𝑝 + 𝑇 ) − 𝑝 ) )