Metamath Proof Explorer

Theorem cyc3genpm

Description: The alternating group A is generated by 3-cycles. Property (a) of Lang p. 32 . (Contributed by Thierry Arnoux, 27-Sep-2023)

Ref Expression
Hypotheses cyc3genpm.t ⊢ 𝐶 = ( 𝑀 “ ( ◡ ♯ “ { 3 } ) )
cyc3genpm.a ⊢ 𝐴 = ( pmEven ‘ 𝐷 )
cyc3genpm.s ⊢ 𝑆 = ( SymGrp ‘ 𝐷 )
cyc3genpm.n ⊢ 𝑁 = ( ♯ ‘ 𝐷 )
cyc3genpm.m ⊢ 𝑀 = ( toCyc ‘ 𝐷 )
Assertion cyc3genpm ( 𝐷 ∈ Fin → ( 𝑄 ∈ 𝐴 ↔ ∃ 𝑤 ∈ 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 simplr ⊢ ( ( ( ( 𝐷 ∈ Fin ∧ 𝑄 ∈ 𝐴 ) ∧ 𝑣 ∈ Word ran ( pmTrsp ‘ 𝐷 ) ) ∧ 𝑄 = ( 𝑆 Σg 𝑣 ) ) → 𝑣 ∈ Word ran ( pmTrsp ‘ 𝐷 ) )
7 lencl ⊢ ( 𝑣 ∈ Word ran ( pmTrsp ‘ 𝐷 ) → ( ♯ ‘ 𝑣 ) ∈ ℕ0 )
8 7 ad2antlr ⊢ ( ( ( ( 𝐷 ∈ Fin ∧ 𝑄 ∈ 𝐴 ) ∧ 𝑣 ∈ Word ran ( pmTrsp ‘ 𝐷 ) ) ∧ 𝑄 = ( 𝑆 Σg 𝑣 ) ) → ( ♯ ‘ 𝑣 ) ∈ ℕ0 )
9 8 nn0zd ⊢ ( ( ( ( 𝐷 ∈ Fin ∧ 𝑄 ∈ 𝐴 ) ∧ 𝑣 ∈ Word ran ( pmTrsp ‘ 𝐷 ) ) ∧ 𝑄 = ( 𝑆 Σg 𝑣 ) ) → ( ♯ ‘ 𝑣 ) ∈ ℤ )
10 simpr ⊢ ( ( ( ( 𝐷 ∈ Fin ∧ 𝑄 ∈ 𝐴 ) ∧ 𝑣 ∈ Word ran ( pmTrsp ‘ 𝐷 ) ) ∧ 𝑄 = ( 𝑆 Σg 𝑣 ) ) → 𝑄 = ( 𝑆 Σg 𝑣 ) )
11 10 fveq2d ⊢ ( ( ( ( 𝐷 ∈ Fin ∧ 𝑄 ∈ 𝐴 ) ∧ 𝑣 ∈ Word ran ( pmTrsp ‘ 𝐷 ) ) ∧ 𝑄 = ( 𝑆 Σg 𝑣 ) ) → ( ( pmSgn ‘ 𝐷 ) ‘ 𝑄 ) = ( ( pmSgn ‘ 𝐷 ) ‘ ( 𝑆 Σg 𝑣 ) ) )
12 simplll ⊢ ( ( ( ( 𝐷 ∈ Fin ∧ 𝑄 ∈ 𝐴 ) ∧ 𝑣 ∈ Word ran ( pmTrsp ‘ 𝐷 ) ) ∧ 𝑄 = ( 𝑆 Σg 𝑣 ) ) → 𝐷 ∈ Fin )
13 simpllr ⊢ ( ( ( ( 𝐷 ∈ Fin ∧ 𝑄 ∈ 𝐴 ) ∧ 𝑣 ∈ Word ran ( pmTrsp ‘ 𝐷 ) ) ∧ 𝑄 = ( 𝑆 Σg 𝑣 ) ) → 𝑄 ∈ 𝐴 )
14 13 2 eleqtrdi ⊢ ( ( ( ( 𝐷 ∈ Fin ∧ 𝑄 ∈ 𝐴 ) ∧ 𝑣 ∈ Word ran ( pmTrsp ‘ 𝐷 ) ) ∧ 𝑄 = ( 𝑆 Σg 𝑣 ) ) → 𝑄 ∈ ( pmEven ‘ 𝐷 ) )
15 eqid ⊢ ( Base ‘ 𝑆 ) = ( Base ‘ 𝑆 )
16 eqid ⊢ ( pmSgn ‘ 𝐷 ) = ( pmSgn ‘ 𝐷 )
17 3 15 16 psgnevpm ⊢ ( ( 𝐷 ∈ Fin ∧ 𝑄 ∈ ( pmEven ‘ 𝐷 ) ) → ( ( pmSgn ‘ 𝐷 ) ‘ 𝑄 ) = 1 )
18 12 14 17 syl2anc ⊢ ( ( ( ( 𝐷 ∈ Fin ∧ 𝑄 ∈ 𝐴 ) ∧ 𝑣 ∈ Word ran ( pmTrsp ‘ 𝐷 ) ) ∧ 𝑄 = ( 𝑆 Σg 𝑣 ) ) → ( ( pmSgn ‘ 𝐷 ) ‘ 𝑄 ) = 1 )
19 eqid ⊢ ran ( pmTrsp ‘ 𝐷 ) = ran ( pmTrsp ‘ 𝐷 )
20 3 19 16 psgnvalii ⊢ ( ( 𝐷 ∈ Fin ∧ 𝑣 ∈ Word ran ( pmTrsp ‘ 𝐷 ) ) → ( ( pmSgn ‘ 𝐷 ) ‘ ( 𝑆 Σg 𝑣 ) ) = ( - 1 ↑ ( ♯ ‘ 𝑣 ) ) )
21 12 6 20 syl2anc ⊢ ( ( ( ( 𝐷 ∈ Fin ∧ 𝑄 ∈ 𝐴 ) ∧ 𝑣 ∈ Word ran ( pmTrsp ‘ 𝐷 ) ) ∧ 𝑄 = ( 𝑆 Σg 𝑣 ) ) → ( ( pmSgn ‘ 𝐷 ) ‘ ( 𝑆 Σg 𝑣 ) ) = ( - 1 ↑ ( ♯ ‘ 𝑣 ) ) )
22 11 18 21 3eqtr3rd ⊢ ( ( ( ( 𝐷 ∈ Fin ∧ 𝑄 ∈ 𝐴 ) ∧ 𝑣 ∈ Word ran ( pmTrsp ‘ 𝐷 ) ) ∧ 𝑄 = ( 𝑆 Σg 𝑣 ) ) → ( - 1 ↑ ( ♯ ‘ 𝑣 ) ) = 1 )
23 m1exp1 ⊢ ( ( ♯ ‘ 𝑣 ) ∈ ℤ → ( ( - 1 ↑ ( ♯ ‘ 𝑣 ) ) = 1 ↔ 2 ∥ ( ♯ ‘ 𝑣 ) ) )
24 23 biimpa ⊢ ( ( ( ♯ ‘ 𝑣 ) ∈ ℤ ∧ ( - 1 ↑ ( ♯ ‘ 𝑣 ) ) = 1 ) → 2 ∥ ( ♯ ‘ 𝑣 ) )
25 9 22 24 syl2anc ⊢ ( ( ( ( 𝐷 ∈ Fin ∧ 𝑄 ∈ 𝐴 ) ∧ 𝑣 ∈ Word ran ( pmTrsp ‘ 𝐷 ) ) ∧ 𝑄 = ( 𝑆 Σg 𝑣 ) ) → 2 ∥ ( ♯ ‘ 𝑣 ) )
26 oveq2 ⊢ ( 𝑥 = ∅ → ( 𝑆 Σg 𝑥 ) = ( 𝑆 Σg ∅ ) )
27 26 eqeq1d ⊢ ( 𝑥 = ∅ → ( ( 𝑆 Σg 𝑥 ) = ( 𝑆 Σg 𝑤 ) ↔ ( 𝑆 Σg ∅ ) = ( 𝑆 Σg 𝑤 ) ) )
28 27 rexbidv ⊢ ( 𝑥 = ∅ → ( ∃ 𝑤 ∈ Word 𝐶 ( 𝑆 Σg 𝑥 ) = ( 𝑆 Σg 𝑤 ) ↔ ∃ 𝑤 ∈ Word 𝐶 ( 𝑆 Σg ∅ ) = ( 𝑆 Σg 𝑤 ) ) )
29 28 imbi2d ⊢ ( 𝑥 = ∅ → ( ( 𝐷 ∈ Fin → ∃ 𝑤 ∈ Word 𝐶 ( 𝑆 Σg 𝑥 ) = ( 𝑆 Σg 𝑤 ) ) ↔ ( 𝐷 ∈ Fin → ∃ 𝑤 ∈ Word 𝐶 ( 𝑆 Σg ∅ ) = ( 𝑆 Σg 𝑤 ) ) ) )
30 oveq2 ⊢ ( 𝑥 = 𝑢 → ( 𝑆 Σg 𝑥 ) = ( 𝑆 Σg 𝑢 ) )
31 30 eqeq1d ⊢ ( 𝑥 = 𝑢 → ( ( 𝑆 Σg 𝑥 ) = ( 𝑆 Σg 𝑤 ) ↔ ( 𝑆 Σg 𝑢 ) = ( 𝑆 Σg 𝑤 ) ) )
32 31 rexbidv ⊢ ( 𝑥 = 𝑢 → ( ∃ 𝑤 ∈ Word 𝐶 ( 𝑆 Σg 𝑥 ) = ( 𝑆 Σg 𝑤 ) ↔ ∃ 𝑤 ∈ Word 𝐶 ( 𝑆 Σg 𝑢 ) = ( 𝑆 Σg 𝑤 ) ) )
33 32 imbi2d ⊢ ( 𝑥 = 𝑢 → ( ( 𝐷 ∈ Fin → ∃ 𝑤 ∈ Word 𝐶 ( 𝑆 Σg 𝑥 ) = ( 𝑆 Σg 𝑤 ) ) ↔ ( 𝐷 ∈ Fin → ∃ 𝑤 ∈ Word 𝐶 ( 𝑆 Σg 𝑢 ) = ( 𝑆 Σg 𝑤 ) ) ) )
34 oveq2 ⊢ ( 𝑥 = ( 𝑢 ++ ⟨“ 𝑖 𝑗 ”⟩ ) → ( 𝑆 Σg 𝑥 ) = ( 𝑆 Σg ( 𝑢 ++ ⟨“ 𝑖 𝑗 ”⟩ ) ) )
35 34 eqeq1d ⊢ ( 𝑥 = ( 𝑢 ++ ⟨“ 𝑖 𝑗 ”⟩ ) → ( ( 𝑆 Σg 𝑥 ) = ( 𝑆 Σg 𝑤 ) ↔ ( 𝑆 Σg ( 𝑢 ++ ⟨“ 𝑖 𝑗 ”⟩ ) ) = ( 𝑆 Σg 𝑤 ) ) )
36 35 rexbidv ⊢ ( 𝑥 = ( 𝑢 ++ ⟨“ 𝑖 𝑗 ”⟩ ) → ( ∃ 𝑤 ∈ Word 𝐶 ( 𝑆 Σg 𝑥 ) = ( 𝑆 Σg 𝑤 ) ↔ ∃ 𝑤 ∈ Word 𝐶 ( 𝑆 Σg ( 𝑢 ++ ⟨“ 𝑖 𝑗 ”⟩ ) ) = ( 𝑆 Σg 𝑤 ) ) )
37 36 imbi2d ⊢ ( 𝑥 = ( 𝑢 ++ ⟨“ 𝑖 𝑗 ”⟩ ) → ( ( 𝐷 ∈ Fin → ∃ 𝑤 ∈ Word 𝐶 ( 𝑆 Σg 𝑥 ) = ( 𝑆 Σg 𝑤 ) ) ↔ ( 𝐷 ∈ Fin → ∃ 𝑤 ∈ Word 𝐶 ( 𝑆 Σg ( 𝑢 ++ ⟨“ 𝑖 𝑗 ”⟩ ) ) = ( 𝑆 Σg 𝑤 ) ) ) )
38 oveq2 ⊢ ( 𝑥 = 𝑣 → ( 𝑆 Σg 𝑥 ) = ( 𝑆 Σg 𝑣 ) )
39 38 eqeq1d ⊢ ( 𝑥 = 𝑣 → ( ( 𝑆 Σg 𝑥 ) = ( 𝑆 Σg 𝑤 ) ↔ ( 𝑆 Σg 𝑣 ) = ( 𝑆 Σg 𝑤 ) ) )
40 39 rexbidv ⊢ ( 𝑥 = 𝑣 → ( ∃ 𝑤 ∈ Word 𝐶 ( 𝑆 Σg 𝑥 ) = ( 𝑆 Σg 𝑤 ) ↔ ∃ 𝑤 ∈ Word 𝐶 ( 𝑆 Σg 𝑣 ) = ( 𝑆 Σg 𝑤 ) ) )
41 40 imbi2d ⊢ ( 𝑥 = 𝑣 → ( ( 𝐷 ∈ Fin → ∃ 𝑤 ∈ Word 𝐶 ( 𝑆 Σg 𝑥 ) = ( 𝑆 Σg 𝑤 ) ) ↔ ( 𝐷 ∈ Fin → ∃ 𝑤 ∈ Word 𝐶 ( 𝑆 Σg 𝑣 ) = ( 𝑆 Σg 𝑤 ) ) ) )
42 wrd0 ⊢ ∅ ∈ Word 𝐶
43 42 a1i ⊢ ( 𝐷 ∈ Fin → ∅ ∈ Word 𝐶 )
44 simpr ⊢ ( ( 𝐷 ∈ Fin ∧ 𝑤 = ∅ ) → 𝑤 = ∅ )
45 44 oveq2d ⊢ ( ( 𝐷 ∈ Fin ∧ 𝑤 = ∅ ) → ( 𝑆 Σg 𝑤 ) = ( 𝑆 Σg ∅ ) )
46 45 eqeq2d ⊢ ( ( 𝐷 ∈ Fin ∧ 𝑤 = ∅ ) → ( ( 𝑆 Σg ∅ ) = ( 𝑆 Σg 𝑤 ) ↔ ( 𝑆 Σg ∅ ) = ( 𝑆 Σg ∅ ) ) )
47 eqidd ⊢ ( 𝐷 ∈ Fin → ( 𝑆 Σg ∅ ) = ( 𝑆 Σg ∅ ) )
48 43 46 47 rspcedvd ⊢ ( 𝐷 ∈ Fin → ∃ 𝑤 ∈ Word 𝐶 ( 𝑆 Σg ∅ ) = ( 𝑆 Σg 𝑤 ) )
49 ccatcl ⊢ ( ( 𝑣 ∈ Word 𝐶 ∧ 𝑐 ∈ Word 𝐶 ) → ( 𝑣 ++ 𝑐 ) ∈ Word 𝐶 )
50 49 ad5ant24 ⊢ ( ( ( ( ( ( ( ( 𝑢 ∈ Word ran ( pmTrsp ‘ 𝐷 ) ∧ 𝑖 ∈ ran ( pmTrsp ‘ 𝐷 ) ) ∧ 𝑗 ∈ ran ( pmTrsp ‘ 𝐷 ) ) ∧ 𝐷 ∈ Fin ) ∧ 𝑣 ∈ Word 𝐶 ) ∧ ( 𝑆 Σg 𝑢 ) = ( 𝑆 Σg 𝑣 ) ) ∧ 𝑐 ∈ Word 𝐶 ) ∧ ( 𝑖 ( +g ‘ 𝑆 ) 𝑗 ) = ( 𝑆 Σg 𝑐 ) ) → ( 𝑣 ++ 𝑐 ) ∈ Word 𝐶 )
51 oveq2 ⊢ ( 𝑤 = ( 𝑣 ++ 𝑐 ) → ( 𝑆 Σg 𝑤 ) = ( 𝑆 Σg ( 𝑣 ++ 𝑐 ) ) )
52 51 eqeq2d ⊢ ( 𝑤 = ( 𝑣 ++ 𝑐 ) → ( ( 𝑆 Σg ( 𝑢 ++ ⟨“ 𝑖 𝑗 ”⟩ ) ) = ( 𝑆 Σg 𝑤 ) ↔ ( 𝑆 Σg ( 𝑢 ++ ⟨“ 𝑖 𝑗 ”⟩ ) ) = ( 𝑆 Σg ( 𝑣 ++ 𝑐 ) ) ) )
53 52 adantl ⊢ ( ( ( ( ( ( ( ( ( 𝑢 ∈ Word ran ( pmTrsp ‘ 𝐷 ) ∧ 𝑖 ∈ ran ( pmTrsp ‘ 𝐷 ) ) ∧ 𝑗 ∈ ran ( pmTrsp ‘ 𝐷 ) ) ∧ 𝐷 ∈ Fin ) ∧ 𝑣 ∈ Word 𝐶 ) ∧ ( 𝑆 Σg 𝑢 ) = ( 𝑆 Σg 𝑣 ) ) ∧ 𝑐 ∈ Word 𝐶 ) ∧ ( 𝑖 ( +g ‘ 𝑆 ) 𝑗 ) = ( 𝑆 Σg 𝑐 ) ) ∧ 𝑤 = ( 𝑣 ++ 𝑐 ) ) → ( ( 𝑆 Σg ( 𝑢 ++ ⟨“ 𝑖 𝑗 ”⟩ ) ) = ( 𝑆 Σg 𝑤 ) ↔ ( 𝑆 Σg ( 𝑢 ++ ⟨“ 𝑖 𝑗 ”⟩ ) ) = ( 𝑆 Σg ( 𝑣 ++ 𝑐 ) ) ) )
54 simpllr ⊢ ( ( ( ( ( ( ( ( 𝑢 ∈ Word ran ( pmTrsp ‘ 𝐷 ) ∧ 𝑖 ∈ ran ( pmTrsp ‘ 𝐷 ) ) ∧ 𝑗 ∈ ran ( pmTrsp ‘ 𝐷 ) ) ∧ 𝐷 ∈ Fin ) ∧ 𝑣 ∈ Word 𝐶 ) ∧ ( 𝑆 Σg 𝑢 ) = ( 𝑆 Σg 𝑣 ) ) ∧ 𝑐 ∈ Word 𝐶 ) ∧ ( 𝑖 ( +g ‘ 𝑆 ) 𝑗 ) = ( 𝑆 Σg 𝑐 ) ) → ( 𝑆 Σg 𝑢 ) = ( 𝑆 Σg 𝑣 ) )
55 simpllr ⊢ ( ( ( ( ( ( 𝑢 ∈ Word ran ( pmTrsp ‘ 𝐷 ) ∧ 𝑖 ∈ ran ( pmTrsp ‘ 𝐷 ) ) ∧ 𝑗 ∈ ran ( pmTrsp ‘ 𝐷 ) ) ∧ 𝐷 ∈ Fin ) ∧ 𝑣 ∈ Word 𝐶 ) ∧ ( 𝑆 Σg 𝑢 ) = ( 𝑆 Σg 𝑣 ) ) → 𝐷 ∈ Fin )
56 55 ad2antrr ⊢ ( ( ( ( ( ( ( ( 𝑢 ∈ Word ran ( pmTrsp ‘ 𝐷 ) ∧ 𝑖 ∈ ran ( pmTrsp ‘ 𝐷 ) ) ∧ 𝑗 ∈ ran ( pmTrsp ‘ 𝐷 ) ) ∧ 𝐷 ∈ Fin ) ∧ 𝑣 ∈ Word 𝐶 ) ∧ ( 𝑆 Σg 𝑢 ) = ( 𝑆 Σg 𝑣 ) ) ∧ 𝑐 ∈ Word 𝐶 ) ∧ ( 𝑖 ( +g ‘ 𝑆 ) 𝑗 ) = ( 𝑆 Σg 𝑐 ) ) → 𝐷 ∈ Fin )
57 3 symggrp ⊢ ( 𝐷 ∈ Fin → 𝑆 ∈ Grp )
58 grpmnd ⊢ ( 𝑆 ∈ Grp → 𝑆 ∈ Mnd )
59 56 57 58 3syl ⊢ ( ( ( ( ( ( ( ( 𝑢 ∈ Word ran ( pmTrsp ‘ 𝐷 ) ∧ 𝑖 ∈ ran ( pmTrsp ‘ 𝐷 ) ) ∧ 𝑗 ∈ ran ( pmTrsp ‘ 𝐷 ) ) ∧ 𝐷 ∈ Fin ) ∧ 𝑣 ∈ Word 𝐶 ) ∧ ( 𝑆 Σg 𝑢 ) = ( 𝑆 Σg 𝑣 ) ) ∧ 𝑐 ∈ Word 𝐶 ) ∧ ( 𝑖 ( +g ‘ 𝑆 ) 𝑗 ) = ( 𝑆 Σg 𝑐 ) ) → 𝑆 ∈ Mnd )
60 19 3 15 symgtrf ⊢ ran ( pmTrsp ‘ 𝐷 ) ⊆ ( Base ‘ 𝑆 )
61 60 a1i ⊢ ( ( ( ( ( ( ( ( 𝑢 ∈ Word ran ( pmTrsp ‘ 𝐷 ) ∧ 𝑖 ∈ ran ( pmTrsp ‘ 𝐷 ) ) ∧ 𝑗 ∈ ran ( pmTrsp ‘ 𝐷 ) ) ∧ 𝐷 ∈ Fin ) ∧ 𝑣 ∈ Word 𝐶 ) ∧ ( 𝑆 Σg 𝑢 ) = ( 𝑆 Σg 𝑣 ) ) ∧ 𝑐 ∈ Word 𝐶 ) ∧ ( 𝑖 ( +g ‘ 𝑆 ) 𝑗 ) = ( 𝑆 Σg 𝑐 ) ) → ran ( pmTrsp ‘ 𝐷 ) ⊆ ( Base ‘ 𝑆 ) )
62 simp-5r ⊢ ( ( ( ( ( ( 𝑢 ∈ Word ran ( pmTrsp ‘ 𝐷 ) ∧ 𝑖 ∈ ran ( pmTrsp ‘ 𝐷 ) ) ∧ 𝑗 ∈ ran ( pmTrsp ‘ 𝐷 ) ) ∧ 𝐷 ∈ Fin ) ∧ 𝑣 ∈ Word 𝐶 ) ∧ ( 𝑆 Σg 𝑢 ) = ( 𝑆 Σg 𝑣 ) ) → 𝑖 ∈ ran ( pmTrsp ‘ 𝐷 ) )
63 62 ad2antrr ⊢ ( ( ( ( ( ( ( ( 𝑢 ∈ Word ran ( pmTrsp ‘ 𝐷 ) ∧ 𝑖 ∈ ran ( pmTrsp ‘ 𝐷 ) ) ∧ 𝑗 ∈ ran ( pmTrsp ‘ 𝐷 ) ) ∧ 𝐷 ∈ Fin ) ∧ 𝑣 ∈ Word 𝐶 ) ∧ ( 𝑆 Σg 𝑢 ) = ( 𝑆 Σg 𝑣 ) ) ∧ 𝑐 ∈ Word 𝐶 ) ∧ ( 𝑖 ( +g ‘ 𝑆 ) 𝑗 ) = ( 𝑆 Σg 𝑐 ) ) → 𝑖 ∈ ran ( pmTrsp ‘ 𝐷 ) )
64 61 63 sseldd ⊢ ( ( ( ( ( ( ( ( 𝑢 ∈ Word ran ( pmTrsp ‘ 𝐷 ) ∧ 𝑖 ∈ ran ( pmTrsp ‘ 𝐷 ) ) ∧ 𝑗 ∈ ran ( pmTrsp ‘ 𝐷 ) ) ∧ 𝐷 ∈ Fin ) ∧ 𝑣 ∈ Word 𝐶 ) ∧ ( 𝑆 Σg 𝑢 ) = ( 𝑆 Σg 𝑣 ) ) ∧ 𝑐 ∈ Word 𝐶 ) ∧ ( 𝑖 ( +g ‘ 𝑆 ) 𝑗 ) = ( 𝑆 Σg 𝑐 ) ) → 𝑖 ∈ ( Base ‘ 𝑆 ) )
65 simp-6r ⊢ ( ( ( ( ( ( ( ( 𝑢 ∈ Word ran ( pmTrsp ‘ 𝐷 ) ∧ 𝑖 ∈ ran ( pmTrsp ‘ 𝐷 ) ) ∧ 𝑗 ∈ ran ( pmTrsp ‘ 𝐷 ) ) ∧ 𝐷 ∈ Fin ) ∧ 𝑣 ∈ Word 𝐶 ) ∧ ( 𝑆 Σg 𝑢 ) = ( 𝑆 Σg 𝑣 ) ) ∧ 𝑐 ∈ Word 𝐶 ) ∧ ( 𝑖 ( +g ‘ 𝑆 ) 𝑗 ) = ( 𝑆 Σg 𝑐 ) ) → 𝑗 ∈ ran ( pmTrsp ‘ 𝐷 ) )
66 61 65 sseldd ⊢ ( ( ( ( ( ( ( ( 𝑢 ∈ Word ran ( pmTrsp ‘ 𝐷 ) ∧ 𝑖 ∈ ran ( pmTrsp ‘ 𝐷 ) ) ∧ 𝑗 ∈ ran ( pmTrsp ‘ 𝐷 ) ) ∧ 𝐷 ∈ Fin ) ∧ 𝑣 ∈ Word 𝐶 ) ∧ ( 𝑆 Σg 𝑢 ) = ( 𝑆 Σg 𝑣 ) ) ∧ 𝑐 ∈ Word 𝐶 ) ∧ ( 𝑖 ( +g ‘ 𝑆 ) 𝑗 ) = ( 𝑆 Σg 𝑐 ) ) → 𝑗 ∈ ( Base ‘ 𝑆 ) )
67 eqid ⊢ ( +g ‘ 𝑆 ) = ( +g ‘ 𝑆 )
68 15 67 gsumws2 ⊢ ( ( 𝑆 ∈ Mnd ∧ 𝑖 ∈ ( Base ‘ 𝑆 ) ∧ 𝑗 ∈ ( Base ‘ 𝑆 ) ) → ( 𝑆 Σg ⟨“ 𝑖 𝑗 ”⟩ ) = ( 𝑖 ( +g ‘ 𝑆 ) 𝑗 ) )
69 59 64 66 68 syl3anc ⊢ ( ( ( ( ( ( ( ( 𝑢 ∈ Word ran ( pmTrsp ‘ 𝐷 ) ∧ 𝑖 ∈ ran ( pmTrsp ‘ 𝐷 ) ) ∧ 𝑗 ∈ ran ( pmTrsp ‘ 𝐷 ) ) ∧ 𝐷 ∈ Fin ) ∧ 𝑣 ∈ Word 𝐶 ) ∧ ( 𝑆 Σg 𝑢 ) = ( 𝑆 Σg 𝑣 ) ) ∧ 𝑐 ∈ Word 𝐶 ) ∧ ( 𝑖 ( +g ‘ 𝑆 ) 𝑗 ) = ( 𝑆 Σg 𝑐 ) ) → ( 𝑆 Σg ⟨“ 𝑖 𝑗 ”⟩ ) = ( 𝑖 ( +g ‘ 𝑆 ) 𝑗 ) )
70 simpr ⊢ ( ( ( ( ( ( ( ( 𝑢 ∈ Word ran ( pmTrsp ‘ 𝐷 ) ∧ 𝑖 ∈ ran ( pmTrsp ‘ 𝐷 ) ) ∧ 𝑗 ∈ ran ( pmTrsp ‘ 𝐷 ) ) ∧ 𝐷 ∈ Fin ) ∧ 𝑣 ∈ Word 𝐶 ) ∧ ( 𝑆 Σg 𝑢 ) = ( 𝑆 Σg 𝑣 ) ) ∧ 𝑐 ∈ Word 𝐶 ) ∧ ( 𝑖 ( +g ‘ 𝑆 ) 𝑗 ) = ( 𝑆 Σg 𝑐 ) ) → ( 𝑖 ( +g ‘ 𝑆 ) 𝑗 ) = ( 𝑆 Σg 𝑐 ) )
71 69 70 eqtrd ⊢ ( ( ( ( ( ( ( ( 𝑢 ∈ Word ran ( pmTrsp ‘ 𝐷 ) ∧ 𝑖 ∈ ran ( pmTrsp ‘ 𝐷 ) ) ∧ 𝑗 ∈ ran ( pmTrsp ‘ 𝐷 ) ) ∧ 𝐷 ∈ Fin ) ∧ 𝑣 ∈ Word 𝐶 ) ∧ ( 𝑆 Σg 𝑢 ) = ( 𝑆 Σg 𝑣 ) ) ∧ 𝑐 ∈ Word 𝐶 ) ∧ ( 𝑖 ( +g ‘ 𝑆 ) 𝑗 ) = ( 𝑆 Σg 𝑐 ) ) → ( 𝑆 Σg ⟨“ 𝑖 𝑗 ”⟩ ) = ( 𝑆 Σg 𝑐 ) )
72 54 71 oveq12d ⊢ ( ( ( ( ( ( ( ( 𝑢 ∈ Word ran ( pmTrsp ‘ 𝐷 ) ∧ 𝑖 ∈ ran ( pmTrsp ‘ 𝐷 ) ) ∧ 𝑗 ∈ ran ( pmTrsp ‘ 𝐷 ) ) ∧ 𝐷 ∈ Fin ) ∧ 𝑣 ∈ Word 𝐶 ) ∧ ( 𝑆 Σg 𝑢 ) = ( 𝑆 Σg 𝑣 ) ) ∧ 𝑐 ∈ Word 𝐶 ) ∧ ( 𝑖 ( +g ‘ 𝑆 ) 𝑗 ) = ( 𝑆 Σg 𝑐 ) ) → ( ( 𝑆 Σg 𝑢 ) ( +g ‘ 𝑆 ) ( 𝑆 Σg ⟨“ 𝑖 𝑗 ”⟩ ) ) = ( ( 𝑆 Σg 𝑣 ) ( +g ‘ 𝑆 ) ( 𝑆 Σg 𝑐 ) ) )
73 sswrd ⊢ ( ran ( pmTrsp ‘ 𝐷 ) ⊆ ( Base ‘ 𝑆 ) → Word ran ( pmTrsp ‘ 𝐷 ) ⊆ Word ( Base ‘ 𝑆 ) )
74 61 73 syl ⊢ ( ( ( ( ( ( ( ( 𝑢 ∈ Word ran ( pmTrsp ‘ 𝐷 ) ∧ 𝑖 ∈ ran ( pmTrsp ‘ 𝐷 ) ) ∧ 𝑗 ∈ ran ( pmTrsp ‘ 𝐷 ) ) ∧ 𝐷 ∈ Fin ) ∧ 𝑣 ∈ Word 𝐶 ) ∧ ( 𝑆 Σg 𝑢 ) = ( 𝑆 Σg 𝑣 ) ) ∧ 𝑐 ∈ Word 𝐶 ) ∧ ( 𝑖 ( +g ‘ 𝑆 ) 𝑗 ) = ( 𝑆 Σg 𝑐 ) ) → Word ran ( pmTrsp ‘ 𝐷 ) ⊆ Word ( Base ‘ 𝑆 ) )
75 simp-7l ⊢ ( ( ( ( ( ( ( ( 𝑢 ∈ Word ran ( pmTrsp ‘ 𝐷 ) ∧ 𝑖 ∈ ran ( pmTrsp ‘ 𝐷 ) ) ∧ 𝑗 ∈ ran ( pmTrsp ‘ 𝐷 ) ) ∧ 𝐷 ∈ Fin ) ∧ 𝑣 ∈ Word 𝐶 ) ∧ ( 𝑆 Σg 𝑢 ) = ( 𝑆 Σg 𝑣 ) ) ∧ 𝑐 ∈ Word 𝐶 ) ∧ ( 𝑖 ( +g ‘ 𝑆 ) 𝑗 ) = ( 𝑆 Σg 𝑐 ) ) → 𝑢 ∈ Word ran ( pmTrsp ‘ 𝐷 ) )
76 74 75 sseldd ⊢ ( ( ( ( ( ( ( ( 𝑢 ∈ Word ran ( pmTrsp ‘ 𝐷 ) ∧ 𝑖 ∈ ran ( pmTrsp ‘ 𝐷 ) ) ∧ 𝑗 ∈ ran ( pmTrsp ‘ 𝐷 ) ) ∧ 𝐷 ∈ Fin ) ∧ 𝑣 ∈ Word 𝐶 ) ∧ ( 𝑆 Σg 𝑢 ) = ( 𝑆 Σg 𝑣 ) ) ∧ 𝑐 ∈ Word 𝐶 ) ∧ ( 𝑖 ( +g ‘ 𝑆 ) 𝑗 ) = ( 𝑆 Σg 𝑐 ) ) → 𝑢 ∈ Word ( Base ‘ 𝑆 ) )
77 64 66 s2cld ⊢ ( ( ( ( ( ( ( ( 𝑢 ∈ Word ran ( pmTrsp ‘ 𝐷 ) ∧ 𝑖 ∈ ran ( pmTrsp ‘ 𝐷 ) ) ∧ 𝑗 ∈ ran ( pmTrsp ‘ 𝐷 ) ) ∧ 𝐷 ∈ Fin ) ∧ 𝑣 ∈ Word 𝐶 ) ∧ ( 𝑆 Σg 𝑢 ) = ( 𝑆 Σg 𝑣 ) ) ∧ 𝑐 ∈ Word 𝐶 ) ∧ ( 𝑖 ( +g ‘ 𝑆 ) 𝑗 ) = ( 𝑆 Σg 𝑐 ) ) → ⟨“ 𝑖 𝑗 ”⟩ ∈ Word ( Base ‘ 𝑆 ) )
78 15 67 gsumccat ⊢ ( ( 𝑆 ∈ Mnd ∧ 𝑢 ∈ Word ( Base ‘ 𝑆 ) ∧ ⟨“ 𝑖 𝑗 ”⟩ ∈ Word ( Base ‘ 𝑆 ) ) → ( 𝑆 Σg ( 𝑢 ++ ⟨“ 𝑖 𝑗 ”⟩ ) ) = ( ( 𝑆 Σg 𝑢 ) ( +g ‘ 𝑆 ) ( 𝑆 Σg ⟨“ 𝑖 𝑗 ”⟩ ) ) )
79 59 76 77 78 syl3anc ⊢ ( ( ( ( ( ( ( ( 𝑢 ∈ Word ran ( pmTrsp ‘ 𝐷 ) ∧ 𝑖 ∈ ran ( pmTrsp ‘ 𝐷 ) ) ∧ 𝑗 ∈ ran ( pmTrsp ‘ 𝐷 ) ) ∧ 𝐷 ∈ Fin ) ∧ 𝑣 ∈ Word 𝐶 ) ∧ ( 𝑆 Σg 𝑢 ) = ( 𝑆 Σg 𝑣 ) ) ∧ 𝑐 ∈ Word 𝐶 ) ∧ ( 𝑖 ( +g ‘ 𝑆 ) 𝑗 ) = ( 𝑆 Σg 𝑐 ) ) → ( 𝑆 Σg ( 𝑢 ++ ⟨“ 𝑖 𝑗 ”⟩ ) ) = ( ( 𝑆 Σg 𝑢 ) ( +g ‘ 𝑆 ) ( 𝑆 Σg ⟨“ 𝑖 𝑗 ”⟩ ) ) )
80 5 imaeq1i ⊢ ( 𝑀 “ ( ◡ ♯ “ { 3 } ) ) = ( ( toCyc ‘ 𝐷 ) “ ( ◡ ♯ “ { 3 } ) )
81 1 80 eqtri ⊢ 𝐶 = ( ( toCyc ‘ 𝐷 ) “ ( ◡ ♯ “ { 3 } ) )
82 81 2 cyc3evpm ⊢ ( 𝐷 ∈ Fin → 𝐶 ⊆ 𝐴 )
83 3 15 evpmss ⊢ ( pmEven ‘ 𝐷 ) ⊆ ( Base ‘ 𝑆 )
84 2 83 eqsstri ⊢ 𝐴 ⊆ ( Base ‘ 𝑆 )
85 82 84 sstrdi ⊢ ( 𝐷 ∈ Fin → 𝐶 ⊆ ( Base ‘ 𝑆 ) )
86 sswrd ⊢ ( 𝐶 ⊆ ( Base ‘ 𝑆 ) → Word 𝐶 ⊆ Word ( Base ‘ 𝑆 ) )
87 56 85 86 3syl ⊢ ( ( ( ( ( ( ( ( 𝑢 ∈ Word ran ( pmTrsp ‘ 𝐷 ) ∧ 𝑖 ∈ ran ( pmTrsp ‘ 𝐷 ) ) ∧ 𝑗 ∈ ran ( pmTrsp ‘ 𝐷 ) ) ∧ 𝐷 ∈ Fin ) ∧ 𝑣 ∈ Word 𝐶 ) ∧ ( 𝑆 Σg 𝑢 ) = ( 𝑆 Σg 𝑣 ) ) ∧ 𝑐 ∈ Word 𝐶 ) ∧ ( 𝑖 ( +g ‘ 𝑆 ) 𝑗 ) = ( 𝑆 Σg 𝑐 ) ) → Word 𝐶 ⊆ Word ( Base ‘ 𝑆 ) )
88 simp-4r ⊢ ( ( ( ( ( ( ( ( 𝑢 ∈ Word ran ( pmTrsp ‘ 𝐷 ) ∧ 𝑖 ∈ ran ( pmTrsp ‘ 𝐷 ) ) ∧ 𝑗 ∈ ran ( pmTrsp ‘ 𝐷 ) ) ∧ 𝐷 ∈ Fin ) ∧ 𝑣 ∈ Word 𝐶 ) ∧ ( 𝑆 Σg 𝑢 ) = ( 𝑆 Σg 𝑣 ) ) ∧ 𝑐 ∈ Word 𝐶 ) ∧ ( 𝑖 ( +g ‘ 𝑆 ) 𝑗 ) = ( 𝑆 Σg 𝑐 ) ) → 𝑣 ∈ Word 𝐶 )
89 87 88 sseldd ⊢ ( ( ( ( ( ( ( ( 𝑢 ∈ Word ran ( pmTrsp ‘ 𝐷 ) ∧ 𝑖 ∈ ran ( pmTrsp ‘ 𝐷 ) ) ∧ 𝑗 ∈ ran ( pmTrsp ‘ 𝐷 ) ) ∧ 𝐷 ∈ Fin ) ∧ 𝑣 ∈ Word 𝐶 ) ∧ ( 𝑆 Σg 𝑢 ) = ( 𝑆 Σg 𝑣 ) ) ∧ 𝑐 ∈ Word 𝐶 ) ∧ ( 𝑖 ( +g ‘ 𝑆 ) 𝑗 ) = ( 𝑆 Σg 𝑐 ) ) → 𝑣 ∈ Word ( Base ‘ 𝑆 ) )
90 simplr ⊢ ( ( ( ( ( ( ( ( 𝑢 ∈ Word ran ( pmTrsp ‘ 𝐷 ) ∧ 𝑖 ∈ ran ( pmTrsp ‘ 𝐷 ) ) ∧ 𝑗 ∈ ran ( pmTrsp ‘ 𝐷 ) ) ∧ 𝐷 ∈ Fin ) ∧ 𝑣 ∈ Word 𝐶 ) ∧ ( 𝑆 Σg 𝑢 ) = ( 𝑆 Σg 𝑣 ) ) ∧ 𝑐 ∈ Word 𝐶 ) ∧ ( 𝑖 ( +g ‘ 𝑆 ) 𝑗 ) = ( 𝑆 Σg 𝑐 ) ) → 𝑐 ∈ Word 𝐶 )
91 87 90 sseldd ⊢ ( ( ( ( ( ( ( ( 𝑢 ∈ Word ran ( pmTrsp ‘ 𝐷 ) ∧ 𝑖 ∈ ran ( pmTrsp ‘ 𝐷 ) ) ∧ 𝑗 ∈ ran ( pmTrsp ‘ 𝐷 ) ) ∧ 𝐷 ∈ Fin ) ∧ 𝑣 ∈ Word 𝐶 ) ∧ ( 𝑆 Σg 𝑢 ) = ( 𝑆 Σg 𝑣 ) ) ∧ 𝑐 ∈ Word 𝐶 ) ∧ ( 𝑖 ( +g ‘ 𝑆 ) 𝑗 ) = ( 𝑆 Σg 𝑐 ) ) → 𝑐 ∈ Word ( Base ‘ 𝑆 ) )
92 15 67 gsumccat ⊢ ( ( 𝑆 ∈ Mnd ∧ 𝑣 ∈ Word ( Base ‘ 𝑆 ) ∧ 𝑐 ∈ Word ( Base ‘ 𝑆 ) ) → ( 𝑆 Σg ( 𝑣 ++ 𝑐 ) ) = ( ( 𝑆 Σg 𝑣 ) ( +g ‘ 𝑆 ) ( 𝑆 Σg 𝑐 ) ) )
93 59 89 91 92 syl3anc ⊢ ( ( ( ( ( ( ( ( 𝑢 ∈ Word ran ( pmTrsp ‘ 𝐷 ) ∧ 𝑖 ∈ ran ( pmTrsp ‘ 𝐷 ) ) ∧ 𝑗 ∈ ran ( pmTrsp ‘ 𝐷 ) ) ∧ 𝐷 ∈ Fin ) ∧ 𝑣 ∈ Word 𝐶 ) ∧ ( 𝑆 Σg 𝑢 ) = ( 𝑆 Σg 𝑣 ) ) ∧ 𝑐 ∈ Word 𝐶 ) ∧ ( 𝑖 ( +g ‘ 𝑆 ) 𝑗 ) = ( 𝑆 Σg 𝑐 ) ) → ( 𝑆 Σg ( 𝑣 ++ 𝑐 ) ) = ( ( 𝑆 Σg 𝑣 ) ( +g ‘ 𝑆 ) ( 𝑆 Σg 𝑐 ) ) )
94 72 79 93 3eqtr4d ⊢ ( ( ( ( ( ( ( ( 𝑢 ∈ Word ran ( pmTrsp ‘ 𝐷 ) ∧ 𝑖 ∈ ran ( pmTrsp ‘ 𝐷 ) ) ∧ 𝑗 ∈ ran ( pmTrsp ‘ 𝐷 ) ) ∧ 𝐷 ∈ Fin ) ∧ 𝑣 ∈ Word 𝐶 ) ∧ ( 𝑆 Σg 𝑢 ) = ( 𝑆 Σg 𝑣 ) ) ∧ 𝑐 ∈ Word 𝐶 ) ∧ ( 𝑖 ( +g ‘ 𝑆 ) 𝑗 ) = ( 𝑆 Σg 𝑐 ) ) → ( 𝑆 Σg ( 𝑢 ++ ⟨“ 𝑖 𝑗 ”⟩ ) ) = ( 𝑆 Σg ( 𝑣 ++ 𝑐 ) ) )
95 50 53 94 rspcedvd ⊢ ( ( ( ( ( ( ( ( 𝑢 ∈ Word ran ( pmTrsp ‘ 𝐷 ) ∧ 𝑖 ∈ ran ( pmTrsp ‘ 𝐷 ) ) ∧ 𝑗 ∈ ran ( pmTrsp ‘ 𝐷 ) ) ∧ 𝐷 ∈ Fin ) ∧ 𝑣 ∈ Word 𝐶 ) ∧ ( 𝑆 Σg 𝑢 ) = ( 𝑆 Σg 𝑣 ) ) ∧ 𝑐 ∈ Word 𝐶 ) ∧ ( 𝑖 ( +g ‘ 𝑆 ) 𝑗 ) = ( 𝑆 Σg 𝑐 ) ) → ∃ 𝑤 ∈ Word 𝐶 ( 𝑆 Σg ( 𝑢 ++ ⟨“ 𝑖 𝑗 ”⟩ ) ) = ( 𝑆 Σg 𝑤 ) )
96 simp-6r ⊢ ( ( ( ( ( ( ( ( ( ( ( ( 𝑢 ∈ Word ran ( pmTrsp ‘ 𝐷 ) ∧ 𝑖 ∈ ran ( pmTrsp ‘ 𝐷 ) ) ∧ 𝑗 ∈ ran ( pmTrsp ‘ 𝐷 ) ) ∧ 𝐷 ∈ Fin ) ∧ 𝑣 ∈ Word 𝐶 ) ∧ ( 𝑆 Σg 𝑢 ) = ( 𝑆 Σg 𝑣 ) ) ∧ 𝑒 ∈ 𝐷 ) ∧ 𝑓 ∈ 𝐷 ) ∧ ( 𝑒 ≠ 𝑓 ∧ 𝑖 = ( 𝑀 ‘ ⟨“ 𝑒 𝑓 ”⟩ ) ) ) ∧ 𝑔 ∈ 𝐷 ) ∧ ℎ ∈ 𝐷 ) ∧ ( 𝑔 ≠ ℎ ∧ 𝑗 = ( 𝑀 ‘ ⟨“ 𝑔 ℎ ”⟩ ) ) ) → 𝑒 ∈ 𝐷 )
97 simp-5r ⊢ ( ( ( ( ( ( ( ( ( ( ( ( 𝑢 ∈ Word ran ( pmTrsp ‘ 𝐷 ) ∧ 𝑖 ∈ ran ( pmTrsp ‘ 𝐷 ) ) ∧ 𝑗 ∈ ran ( pmTrsp ‘ 𝐷 ) ) ∧ 𝐷 ∈ Fin ) ∧ 𝑣 ∈ Word 𝐶 ) ∧ ( 𝑆 Σg 𝑢 ) = ( 𝑆 Σg 𝑣 ) ) ∧ 𝑒 ∈ 𝐷 ) ∧ 𝑓 ∈ 𝐷 ) ∧ ( 𝑒 ≠ 𝑓 ∧ 𝑖 = ( 𝑀 ‘ ⟨“ 𝑒 𝑓 ”⟩ ) ) ) ∧ 𝑔 ∈ 𝐷 ) ∧ ℎ ∈ 𝐷 ) ∧ ( 𝑔 ≠ ℎ ∧ 𝑗 = ( 𝑀 ‘ ⟨“ 𝑔 ℎ ”⟩ ) ) ) → 𝑓 ∈ 𝐷 )
98 simpllr ⊢ ( ( ( ( ( ( ( ( ( ( ( ( 𝑢 ∈ Word ran ( pmTrsp ‘ 𝐷 ) ∧ 𝑖 ∈ ran ( pmTrsp ‘ 𝐷 ) ) ∧ 𝑗 ∈ ran ( pmTrsp ‘ 𝐷 ) ) ∧ 𝐷 ∈ Fin ) ∧ 𝑣 ∈ Word 𝐶 ) ∧ ( 𝑆 Σg 𝑢 ) = ( 𝑆 Σg 𝑣 ) ) ∧ 𝑒 ∈ 𝐷 ) ∧ 𝑓 ∈ 𝐷 ) ∧ ( 𝑒 ≠ 𝑓 ∧ 𝑖 = ( 𝑀 ‘ ⟨“ 𝑒 𝑓 ”⟩ ) ) ) ∧ 𝑔 ∈ 𝐷 ) ∧ ℎ ∈ 𝐷 ) ∧ ( 𝑔 ≠ ℎ ∧ 𝑗 = ( 𝑀 ‘ ⟨“ 𝑔 ℎ ”⟩ ) ) ) → 𝑔 ∈ 𝐷 )
99 simplr ⊢ ( ( ( ( ( ( ( ( ( ( ( ( 𝑢 ∈ Word ran ( pmTrsp ‘ 𝐷 ) ∧ 𝑖 ∈ ran ( pmTrsp ‘ 𝐷 ) ) ∧ 𝑗 ∈ ran ( pmTrsp ‘ 𝐷 ) ) ∧ 𝐷 ∈ Fin ) ∧ 𝑣 ∈ Word 𝐶 ) ∧ ( 𝑆 Σg 𝑢 ) = ( 𝑆 Σg 𝑣 ) ) ∧ 𝑒 ∈ 𝐷 ) ∧ 𝑓 ∈ 𝐷 ) ∧ ( 𝑒 ≠ 𝑓 ∧ 𝑖 = ( 𝑀 ‘ ⟨“ 𝑒 𝑓 ”⟩ ) ) ) ∧ 𝑔 ∈ 𝐷 ) ∧ ℎ ∈ 𝐷 ) ∧ ( 𝑔 ≠ ℎ ∧ 𝑗 = ( 𝑀 ‘ ⟨“ 𝑔 ℎ ”⟩ ) ) ) → ℎ ∈ 𝐷 )
100 simp-4r ⊢ ( ( ( ( ( ( ( ( ( ( ( ( 𝑢 ∈ Word ran ( pmTrsp ‘ 𝐷 ) ∧ 𝑖 ∈ ran ( pmTrsp ‘ 𝐷 ) ) ∧ 𝑗 ∈ ran ( pmTrsp ‘ 𝐷 ) ) ∧ 𝐷 ∈ Fin ) ∧ 𝑣 ∈ Word 𝐶 ) ∧ ( 𝑆 Σg 𝑢 ) = ( 𝑆 Σg 𝑣 ) ) ∧ 𝑒 ∈ 𝐷 ) ∧ 𝑓 ∈ 𝐷 ) ∧ ( 𝑒 ≠ 𝑓 ∧ 𝑖 = ( 𝑀 ‘ ⟨“ 𝑒 𝑓 ”⟩ ) ) ) ∧ 𝑔 ∈ 𝐷 ) ∧ ℎ ∈ 𝐷 ) ∧ ( 𝑔 ≠ ℎ ∧ 𝑗 = ( 𝑀 ‘ ⟨“ 𝑔 ℎ ”⟩ ) ) ) → ( 𝑒 ≠ 𝑓 ∧ 𝑖 = ( 𝑀 ‘ ⟨“ 𝑒 𝑓 ”⟩ ) ) )
101 100 simprd ⊢ ( ( ( ( ( ( ( ( ( ( ( ( 𝑢 ∈ Word ran ( pmTrsp ‘ 𝐷 ) ∧ 𝑖 ∈ ran ( pmTrsp ‘ 𝐷 ) ) ∧ 𝑗 ∈ ran ( pmTrsp ‘ 𝐷 ) ) ∧ 𝐷 ∈ Fin ) ∧ 𝑣 ∈ Word 𝐶 ) ∧ ( 𝑆 Σg 𝑢 ) = ( 𝑆 Σg 𝑣 ) ) ∧ 𝑒 ∈ 𝐷 ) ∧ 𝑓 ∈ 𝐷 ) ∧ ( 𝑒 ≠ 𝑓 ∧ 𝑖 = ( 𝑀 ‘ ⟨“ 𝑒 𝑓 ”⟩ ) ) ) ∧ 𝑔 ∈ 𝐷 ) ∧ ℎ ∈ 𝐷 ) ∧ ( 𝑔 ≠ ℎ ∧ 𝑗 = ( 𝑀 ‘ ⟨“ 𝑔 ℎ ”⟩ ) ) ) → 𝑖 = ( 𝑀 ‘ ⟨“ 𝑒 𝑓 ”⟩ ) )
102 simprr ⊢ ( ( ( ( ( ( ( ( ( ( ( ( 𝑢 ∈ Word ran ( pmTrsp ‘ 𝐷 ) ∧ 𝑖 ∈ ran ( pmTrsp ‘ 𝐷 ) ) ∧ 𝑗 ∈ ran ( pmTrsp ‘ 𝐷 ) ) ∧ 𝐷 ∈ Fin ) ∧ 𝑣 ∈ Word 𝐶 ) ∧ ( 𝑆 Σg 𝑢 ) = ( 𝑆 Σg 𝑣 ) ) ∧ 𝑒 ∈ 𝐷 ) ∧ 𝑓 ∈ 𝐷 ) ∧ ( 𝑒 ≠ 𝑓 ∧ 𝑖 = ( 𝑀 ‘ ⟨“ 𝑒 𝑓 ”⟩ ) ) ) ∧ 𝑔 ∈ 𝐷 ) ∧ ℎ ∈ 𝐷 ) ∧ ( 𝑔 ≠ ℎ ∧ 𝑗 = ( 𝑀 ‘ ⟨“ 𝑔 ℎ ”⟩ ) ) ) → 𝑗 = ( 𝑀 ‘ ⟨“ 𝑔 ℎ ”⟩ ) )
103 55 ad6antr ⊢ ( ( ( ( ( ( ( ( ( ( ( ( 𝑢 ∈ Word ran ( pmTrsp ‘ 𝐷 ) ∧ 𝑖 ∈ ran ( pmTrsp ‘ 𝐷 ) ) ∧ 𝑗 ∈ ran ( pmTrsp ‘ 𝐷 ) ) ∧ 𝐷 ∈ Fin ) ∧ 𝑣 ∈ Word 𝐶 ) ∧ ( 𝑆 Σg 𝑢 ) = ( 𝑆 Σg 𝑣 ) ) ∧ 𝑒 ∈ 𝐷 ) ∧ 𝑓 ∈ 𝐷 ) ∧ ( 𝑒 ≠ 𝑓 ∧ 𝑖 = ( 𝑀 ‘ ⟨“ 𝑒 𝑓 ”⟩ ) ) ) ∧ 𝑔 ∈ 𝐷 ) ∧ ℎ ∈ 𝐷 ) ∧ ( 𝑔 ≠ ℎ ∧ 𝑗 = ( 𝑀 ‘ ⟨“ 𝑔 ℎ ”⟩ ) ) ) → 𝐷 ∈ Fin )
104 100 simpld ⊢ ( ( ( ( ( ( ( ( ( ( ( ( 𝑢 ∈ Word ran ( pmTrsp ‘ 𝐷 ) ∧ 𝑖 ∈ ran ( pmTrsp ‘ 𝐷 ) ) ∧ 𝑗 ∈ ran ( pmTrsp ‘ 𝐷 ) ) ∧ 𝐷 ∈ Fin ) ∧ 𝑣 ∈ Word 𝐶 ) ∧ ( 𝑆 Σg 𝑢 ) = ( 𝑆 Σg 𝑣 ) ) ∧ 𝑒 ∈ 𝐷 ) ∧ 𝑓 ∈ 𝐷 ) ∧ ( 𝑒 ≠ 𝑓 ∧ 𝑖 = ( 𝑀 ‘ ⟨“ 𝑒 𝑓 ”⟩ ) ) ) ∧ 𝑔 ∈ 𝐷 ) ∧ ℎ ∈ 𝐷 ) ∧ ( 𝑔 ≠ ℎ ∧ 𝑗 = ( 𝑀 ‘ ⟨“ 𝑔 ℎ ”⟩ ) ) ) → 𝑒 ≠ 𝑓 )
105 simprl ⊢ ( ( ( ( ( ( ( ( ( ( ( ( 𝑢 ∈ Word ran ( pmTrsp ‘ 𝐷 ) ∧ 𝑖 ∈ ran ( pmTrsp ‘ 𝐷 ) ) ∧ 𝑗 ∈ ran ( pmTrsp ‘ 𝐷 ) ) ∧ 𝐷 ∈ Fin ) ∧ 𝑣 ∈ Word 𝐶 ) ∧ ( 𝑆 Σg 𝑢 ) = ( 𝑆 Σg 𝑣 ) ) ∧ 𝑒 ∈ 𝐷 ) ∧ 𝑓 ∈ 𝐷 ) ∧ ( 𝑒 ≠ 𝑓 ∧ 𝑖 = ( 𝑀 ‘ ⟨“ 𝑒 𝑓 ”⟩ ) ) ) ∧ 𝑔 ∈ 𝐷 ) ∧ ℎ ∈ 𝐷 ) ∧ ( 𝑔 ≠ ℎ ∧ 𝑗 = ( 𝑀 ‘ ⟨“ 𝑔 ℎ ”⟩ ) ) ) → 𝑔 ≠ ℎ )
106 1 2 3 4 5 67 96 97 98 99 101 102 103 104 105 cyc3genpmlem ⊢ ( ( ( ( ( ( ( ( ( ( ( ( 𝑢 ∈ Word ran ( pmTrsp ‘ 𝐷 ) ∧ 𝑖 ∈ ran ( pmTrsp ‘ 𝐷 ) ) ∧ 𝑗 ∈ ran ( pmTrsp ‘ 𝐷 ) ) ∧ 𝐷 ∈ Fin ) ∧ 𝑣 ∈ Word 𝐶 ) ∧ ( 𝑆 Σg 𝑢 ) = ( 𝑆 Σg 𝑣 ) ) ∧ 𝑒 ∈ 𝐷 ) ∧ 𝑓 ∈ 𝐷 ) ∧ ( 𝑒 ≠ 𝑓 ∧ 𝑖 = ( 𝑀 ‘ ⟨“ 𝑒 𝑓 ”⟩ ) ) ) ∧ 𝑔 ∈ 𝐷 ) ∧ ℎ ∈ 𝐷 ) ∧ ( 𝑔 ≠ ℎ ∧ 𝑗 = ( 𝑀 ‘ ⟨“ 𝑔 ℎ ”⟩ ) ) ) → ∃ 𝑐 ∈ Word 𝐶 ( 𝑖 ( +g ‘ 𝑆 ) 𝑗 ) = ( 𝑆 Σg 𝑐 ) )
107 simp-6r ⊢ ( ( ( ( ( ( ( ( ( 𝑢 ∈ Word ran ( pmTrsp ‘ 𝐷 ) ∧ 𝑖 ∈ ran ( pmTrsp ‘ 𝐷 ) ) ∧ 𝑗 ∈ ran ( pmTrsp ‘ 𝐷 ) ) ∧ 𝐷 ∈ Fin ) ∧ 𝑣 ∈ Word 𝐶 ) ∧ ( 𝑆 Σg 𝑢 ) = ( 𝑆 Σg 𝑣 ) ) ∧ 𝑒 ∈ 𝐷 ) ∧ 𝑓 ∈ 𝐷 ) ∧ ( 𝑒 ≠ 𝑓 ∧ 𝑖 = ( 𝑀 ‘ ⟨“ 𝑒 𝑓 ”⟩ ) ) ) → 𝐷 ∈ Fin )
108 simp-7r ⊢ ( ( ( ( ( ( ( ( ( 𝑢 ∈ Word ran ( pmTrsp ‘ 𝐷 ) ∧ 𝑖 ∈ ran ( pmTrsp ‘ 𝐷 ) ) ∧ 𝑗 ∈ ran ( pmTrsp ‘ 𝐷 ) ) ∧ 𝐷 ∈ Fin ) ∧ 𝑣 ∈ Word 𝐶 ) ∧ ( 𝑆 Σg 𝑢 ) = ( 𝑆 Σg 𝑣 ) ) ∧ 𝑒 ∈ 𝐷 ) ∧ 𝑓 ∈ 𝐷 ) ∧ ( 𝑒 ≠ 𝑓 ∧ 𝑖 = ( 𝑀 ‘ ⟨“ 𝑒 𝑓 ”⟩ ) ) ) → 𝑗 ∈ ran ( pmTrsp ‘ 𝐷 ) )
109 19 5 trsp2cyc ⊢ ( ( 𝐷 ∈ Fin ∧ 𝑗 ∈ ran ( pmTrsp ‘ 𝐷 ) ) → ∃ 𝑔 ∈ 𝐷 ∃ ℎ ∈ 𝐷 ( 𝑔 ≠ ℎ ∧ 𝑗 = ( 𝑀 ‘ ⟨“ 𝑔 ℎ ”⟩ ) ) )
110 107 108 109 syl2anc ⊢ ( ( ( ( ( ( ( ( ( 𝑢 ∈ Word ran ( pmTrsp ‘ 𝐷 ) ∧ 𝑖 ∈ ran ( pmTrsp ‘ 𝐷 ) ) ∧ 𝑗 ∈ ran ( pmTrsp ‘ 𝐷 ) ) ∧ 𝐷 ∈ Fin ) ∧ 𝑣 ∈ Word 𝐶 ) ∧ ( 𝑆 Σg 𝑢 ) = ( 𝑆 Σg 𝑣 ) ) ∧ 𝑒 ∈ 𝐷 ) ∧ 𝑓 ∈ 𝐷 ) ∧ ( 𝑒 ≠ 𝑓 ∧ 𝑖 = ( 𝑀 ‘ ⟨“ 𝑒 𝑓 ”⟩ ) ) ) → ∃ 𝑔 ∈ 𝐷 ∃ ℎ ∈ 𝐷 ( 𝑔 ≠ ℎ ∧ 𝑗 = ( 𝑀 ‘ ⟨“ 𝑔 ℎ ”⟩ ) ) )
111 106 110 r19.29vva ⊢ ( ( ( ( ( ( ( ( ( 𝑢 ∈ Word ran ( pmTrsp ‘ 𝐷 ) ∧ 𝑖 ∈ ran ( pmTrsp ‘ 𝐷 ) ) ∧ 𝑗 ∈ ran ( pmTrsp ‘ 𝐷 ) ) ∧ 𝐷 ∈ Fin ) ∧ 𝑣 ∈ Word 𝐶 ) ∧ ( 𝑆 Σg 𝑢 ) = ( 𝑆 Σg 𝑣 ) ) ∧ 𝑒 ∈ 𝐷 ) ∧ 𝑓 ∈ 𝐷 ) ∧ ( 𝑒 ≠ 𝑓 ∧ 𝑖 = ( 𝑀 ‘ ⟨“ 𝑒 𝑓 ”⟩ ) ) ) → ∃ 𝑐 ∈ Word 𝐶 ( 𝑖 ( +g ‘ 𝑆 ) 𝑗 ) = ( 𝑆 Σg 𝑐 ) )
112 19 5 trsp2cyc ⊢ ( ( 𝐷 ∈ Fin ∧ 𝑖 ∈ ran ( pmTrsp ‘ 𝐷 ) ) → ∃ 𝑒 ∈ 𝐷 ∃ 𝑓 ∈ 𝐷 ( 𝑒 ≠ 𝑓 ∧ 𝑖 = ( 𝑀 ‘ ⟨“ 𝑒 𝑓 ”⟩ ) ) )
113 55 62 112 syl2anc ⊢ ( ( ( ( ( ( 𝑢 ∈ Word ran ( pmTrsp ‘ 𝐷 ) ∧ 𝑖 ∈ ran ( pmTrsp ‘ 𝐷 ) ) ∧ 𝑗 ∈ ran ( pmTrsp ‘ 𝐷 ) ) ∧ 𝐷 ∈ Fin ) ∧ 𝑣 ∈ Word 𝐶 ) ∧ ( 𝑆 Σg 𝑢 ) = ( 𝑆 Σg 𝑣 ) ) → ∃ 𝑒 ∈ 𝐷 ∃ 𝑓 ∈ 𝐷 ( 𝑒 ≠ 𝑓 ∧ 𝑖 = ( 𝑀 ‘ ⟨“ 𝑒 𝑓 ”⟩ ) ) )
114 111 113 r19.29vva ⊢ ( ( ( ( ( ( 𝑢 ∈ Word ran ( pmTrsp ‘ 𝐷 ) ∧ 𝑖 ∈ ran ( pmTrsp ‘ 𝐷 ) ) ∧ 𝑗 ∈ ran ( pmTrsp ‘ 𝐷 ) ) ∧ 𝐷 ∈ Fin ) ∧ 𝑣 ∈ Word 𝐶 ) ∧ ( 𝑆 Σg 𝑢 ) = ( 𝑆 Σg 𝑣 ) ) → ∃ 𝑐 ∈ Word 𝐶 ( 𝑖 ( +g ‘ 𝑆 ) 𝑗 ) = ( 𝑆 Σg 𝑐 ) )
115 95 114 r19.29a ⊢ ( ( ( ( ( ( 𝑢 ∈ Word ran ( pmTrsp ‘ 𝐷 ) ∧ 𝑖 ∈ ran ( pmTrsp ‘ 𝐷 ) ) ∧ 𝑗 ∈ ran ( pmTrsp ‘ 𝐷 ) ) ∧ 𝐷 ∈ Fin ) ∧ 𝑣 ∈ Word 𝐶 ) ∧ ( 𝑆 Σg 𝑢 ) = ( 𝑆 Σg 𝑣 ) ) → ∃ 𝑤 ∈ Word 𝐶 ( 𝑆 Σg ( 𝑢 ++ ⟨“ 𝑖 𝑗 ”⟩ ) ) = ( 𝑆 Σg 𝑤 ) )
116 115 adantl3r ⊢ ( ( ( ( ( ( ( 𝑢 ∈ Word ran ( pmTrsp ‘ 𝐷 ) ∧ 𝑖 ∈ ran ( pmTrsp ‘ 𝐷 ) ) ∧ 𝑗 ∈ ran ( pmTrsp ‘ 𝐷 ) ) ∧ ( 𝐷 ∈ Fin → ∃ 𝑤 ∈ Word 𝐶 ( 𝑆 Σg 𝑢 ) = ( 𝑆 Σg 𝑤 ) ) ) ∧ 𝐷 ∈ Fin ) ∧ 𝑣 ∈ Word 𝐶 ) ∧ ( 𝑆 Σg 𝑢 ) = ( 𝑆 Σg 𝑣 ) ) → ∃ 𝑤 ∈ Word 𝐶 ( 𝑆 Σg ( 𝑢 ++ ⟨“ 𝑖 𝑗 ”⟩ ) ) = ( 𝑆 Σg 𝑤 ) )
117 simpr ⊢ ( ( ( ( ( 𝑢 ∈ Word ran ( pmTrsp ‘ 𝐷 ) ∧ 𝑖 ∈ ran ( pmTrsp ‘ 𝐷 ) ) ∧ 𝑗 ∈ ran ( pmTrsp ‘ 𝐷 ) ) ∧ ( 𝐷 ∈ Fin → ∃ 𝑤 ∈ Word 𝐶 ( 𝑆 Σg 𝑢 ) = ( 𝑆 Σg 𝑤 ) ) ) ∧ 𝐷 ∈ Fin ) → 𝐷 ∈ Fin )
118 simplr ⊢ ( ( ( ( ( 𝑢 ∈ Word ran ( pmTrsp ‘ 𝐷 ) ∧ 𝑖 ∈ ran ( pmTrsp ‘ 𝐷 ) ) ∧ 𝑗 ∈ ran ( pmTrsp ‘ 𝐷 ) ) ∧ ( 𝐷 ∈ Fin → ∃ 𝑤 ∈ Word 𝐶 ( 𝑆 Σg 𝑢 ) = ( 𝑆 Σg 𝑤 ) ) ) ∧ 𝐷 ∈ Fin ) → ( 𝐷 ∈ Fin → ∃ 𝑤 ∈ Word 𝐶 ( 𝑆 Σg 𝑢 ) = ( 𝑆 Σg 𝑤 ) ) )
119 117 118 mpd ⊢ ( ( ( ( ( 𝑢 ∈ Word ran ( pmTrsp ‘ 𝐷 ) ∧ 𝑖 ∈ ran ( pmTrsp ‘ 𝐷 ) ) ∧ 𝑗 ∈ ran ( pmTrsp ‘ 𝐷 ) ) ∧ ( 𝐷 ∈ Fin → ∃ 𝑤 ∈ Word 𝐶 ( 𝑆 Σg 𝑢 ) = ( 𝑆 Σg 𝑤 ) ) ) ∧ 𝐷 ∈ Fin ) → ∃ 𝑤 ∈ Word 𝐶 ( 𝑆 Σg 𝑢 ) = ( 𝑆 Σg 𝑤 ) )
120 oveq2 ⊢ ( 𝑣 = 𝑤 → ( 𝑆 Σg 𝑣 ) = ( 𝑆 Σg 𝑤 ) )
121 120 eqeq2d ⊢ ( 𝑣 = 𝑤 → ( ( 𝑆 Σg 𝑢 ) = ( 𝑆 Σg 𝑣 ) ↔ ( 𝑆 Σg 𝑢 ) = ( 𝑆 Σg 𝑤 ) ) )
122 121 cbvrexvw ⊢ ( ∃ 𝑣 ∈ Word 𝐶 ( 𝑆 Σg 𝑢 ) = ( 𝑆 Σg 𝑣 ) ↔ ∃ 𝑤 ∈ Word 𝐶 ( 𝑆 Σg 𝑢 ) = ( 𝑆 Σg 𝑤 ) )
123 119 122 sylibr ⊢ ( ( ( ( ( 𝑢 ∈ Word ran ( pmTrsp ‘ 𝐷 ) ∧ 𝑖 ∈ ran ( pmTrsp ‘ 𝐷 ) ) ∧ 𝑗 ∈ ran ( pmTrsp ‘ 𝐷 ) ) ∧ ( 𝐷 ∈ Fin → ∃ 𝑤 ∈ Word 𝐶 ( 𝑆 Σg 𝑢 ) = ( 𝑆 Σg 𝑤 ) ) ) ∧ 𝐷 ∈ Fin ) → ∃ 𝑣 ∈ Word 𝐶 ( 𝑆 Σg 𝑢 ) = ( 𝑆 Σg 𝑣 ) )
124 116 123 r19.29a ⊢ ( ( ( ( ( 𝑢 ∈ Word ran ( pmTrsp ‘ 𝐷 ) ∧ 𝑖 ∈ ran ( pmTrsp ‘ 𝐷 ) ) ∧ 𝑗 ∈ ran ( pmTrsp ‘ 𝐷 ) ) ∧ ( 𝐷 ∈ Fin → ∃ 𝑤 ∈ Word 𝐶 ( 𝑆 Σg 𝑢 ) = ( 𝑆 Σg 𝑤 ) ) ) ∧ 𝐷 ∈ Fin ) → ∃ 𝑤 ∈ Word 𝐶 ( 𝑆 Σg ( 𝑢 ++ ⟨“ 𝑖 𝑗 ”⟩ ) ) = ( 𝑆 Σg 𝑤 ) )
125 124 ex ⊢ ( ( ( ( 𝑢 ∈ Word ran ( pmTrsp ‘ 𝐷 ) ∧ 𝑖 ∈ ran ( pmTrsp ‘ 𝐷 ) ) ∧ 𝑗 ∈ ran ( pmTrsp ‘ 𝐷 ) ) ∧ ( 𝐷 ∈ Fin → ∃ 𝑤 ∈ Word 𝐶 ( 𝑆 Σg 𝑢 ) = ( 𝑆 Σg 𝑤 ) ) ) → ( 𝐷 ∈ Fin → ∃ 𝑤 ∈ Word 𝐶 ( 𝑆 Σg ( 𝑢 ++ ⟨“ 𝑖 𝑗 ”⟩ ) ) = ( 𝑆 Σg 𝑤 ) ) )
126 125 ex3 ⊢ ( ( 𝑢 ∈ Word ran ( pmTrsp ‘ 𝐷 ) ∧ 𝑖 ∈ ran ( pmTrsp ‘ 𝐷 ) ∧ 𝑗 ∈ ran ( pmTrsp ‘ 𝐷 ) ) → ( ( 𝐷 ∈ Fin → ∃ 𝑤 ∈ Word 𝐶 ( 𝑆 Σg 𝑢 ) = ( 𝑆 Σg 𝑤 ) ) → ( 𝐷 ∈ Fin → ∃ 𝑤 ∈ Word 𝐶 ( 𝑆 Σg ( 𝑢 ++ ⟨“ 𝑖 𝑗 ”⟩ ) ) = ( 𝑆 Σg 𝑤 ) ) ) )
127 29 33 37 41 48 126 wrdt2ind ⊢ ( ( 𝑣 ∈ Word ran ( pmTrsp ‘ 𝐷 ) ∧ 2 ∥ ( ♯ ‘ 𝑣 ) ) → ( 𝐷 ∈ Fin → ∃ 𝑤 ∈ Word 𝐶 ( 𝑆 Σg 𝑣 ) = ( 𝑆 Σg 𝑤 ) ) )
128 127 imp ⊢ ( ( ( 𝑣 ∈ Word ran ( pmTrsp ‘ 𝐷 ) ∧ 2 ∥ ( ♯ ‘ 𝑣 ) ) ∧ 𝐷 ∈ Fin ) → ∃ 𝑤 ∈ Word 𝐶 ( 𝑆 Σg 𝑣 ) = ( 𝑆 Σg 𝑤 ) )
129 6 25 12 128 syl21anc ⊢ ( ( ( ( 𝐷 ∈ Fin ∧ 𝑄 ∈ 𝐴 ) ∧ 𝑣 ∈ Word ran ( pmTrsp ‘ 𝐷 ) ) ∧ 𝑄 = ( 𝑆 Σg 𝑣 ) ) → ∃ 𝑤 ∈ Word 𝐶 ( 𝑆 Σg 𝑣 ) = ( 𝑆 Σg 𝑤 ) )
130 10 eqeq1d ⊢ ( ( ( ( 𝐷 ∈ Fin ∧ 𝑄 ∈ 𝐴 ) ∧ 𝑣 ∈ Word ran ( pmTrsp ‘ 𝐷 ) ) ∧ 𝑄 = ( 𝑆 Σg 𝑣 ) ) → ( 𝑄 = ( 𝑆 Σg 𝑤 ) ↔ ( 𝑆 Σg 𝑣 ) = ( 𝑆 Σg 𝑤 ) ) )
131 130 rexbidv ⊢ ( ( ( ( 𝐷 ∈ Fin ∧ 𝑄 ∈ 𝐴 ) ∧ 𝑣 ∈ Word ran ( pmTrsp ‘ 𝐷 ) ) ∧ 𝑄 = ( 𝑆 Σg 𝑣 ) ) → ( ∃ 𝑤 ∈ Word 𝐶 𝑄 = ( 𝑆 Σg 𝑤 ) ↔ ∃ 𝑤 ∈ Word 𝐶 ( 𝑆 Σg 𝑣 ) = ( 𝑆 Σg 𝑤 ) ) )
132 129 131 mpbird ⊢ ( ( ( ( 𝐷 ∈ Fin ∧ 𝑄 ∈ 𝐴 ) ∧ 𝑣 ∈ Word ran ( pmTrsp ‘ 𝐷 ) ) ∧ 𝑄 = ( 𝑆 Σg 𝑣 ) ) → ∃ 𝑤 ∈ Word 𝐶 𝑄 = ( 𝑆 Σg 𝑤 ) )
133 84 sseli ⊢ ( 𝑄 ∈ 𝐴 → 𝑄 ∈ ( Base ‘ 𝑆 ) )
134 3 15 19 psgnfitr ⊢ ( 𝐷 ∈ Fin → ( 𝑄 ∈ ( Base ‘ 𝑆 ) ↔ ∃ 𝑣 ∈ Word ran ( pmTrsp ‘ 𝐷 ) 𝑄 = ( 𝑆 Σg 𝑣 ) ) )
135 134 biimpa ⊢ ( ( 𝐷 ∈ Fin ∧ 𝑄 ∈ ( Base ‘ 𝑆 ) ) → ∃ 𝑣 ∈ Word ran ( pmTrsp ‘ 𝐷 ) 𝑄 = ( 𝑆 Σg 𝑣 ) )
136 133 135 sylan2 ⊢ ( ( 𝐷 ∈ Fin ∧ 𝑄 ∈ 𝐴 ) → ∃ 𝑣 ∈ Word ran ( pmTrsp ‘ 𝐷 ) 𝑄 = ( 𝑆 Σg 𝑣 ) )
137 132 136 r19.29a ⊢ ( ( 𝐷 ∈ Fin ∧ 𝑄 ∈ 𝐴 ) → ∃ 𝑤 ∈ Word 𝐶 𝑄 = ( 𝑆 Σg 𝑤 ) )
138 simpr ⊢ ( ( ( 𝐷 ∈ Fin ∧ 𝑤 ∈ Word 𝐶 ) ∧ 𝑄 = ( 𝑆 Σg 𝑤 ) ) → 𝑄 = ( 𝑆 Σg 𝑤 ) )
139 3 altgnsg ⊢ ( 𝐷 ∈ Fin → ( pmEven ‘ 𝐷 ) ∈ ( NrmSGrp ‘ 𝑆 ) )
140 2 139 eqeltrid ⊢ ( 𝐷 ∈ Fin → 𝐴 ∈ ( NrmSGrp ‘ 𝑆 ) )
141 nsgsubg ⊢ ( 𝐴 ∈ ( NrmSGrp ‘ 𝑆 ) → 𝐴 ∈ ( SubGrp ‘ 𝑆 ) )
142 subgsubm ⊢ ( 𝐴 ∈ ( SubGrp ‘ 𝑆 ) → 𝐴 ∈ ( SubMnd ‘ 𝑆 ) )
143 140 141 142 3syl ⊢ ( 𝐷 ∈ Fin → 𝐴 ∈ ( SubMnd ‘ 𝑆 ) )
144 143 adantr ⊢ ( ( 𝐷 ∈ Fin ∧ 𝑤 ∈ Word 𝐶 ) → 𝐴 ∈ ( SubMnd ‘ 𝑆 ) )
145 sswrd ⊢ ( 𝐶 ⊆ 𝐴 → Word 𝐶 ⊆ Word 𝐴 )
146 82 145 syl ⊢ ( 𝐷 ∈ Fin → Word 𝐶 ⊆ Word 𝐴 )
147 146 sselda ⊢ ( ( 𝐷 ∈ Fin ∧ 𝑤 ∈ Word 𝐶 ) → 𝑤 ∈ Word 𝐴 )
148 gsumwsubmcl ⊢ ( ( 𝐴 ∈ ( SubMnd ‘ 𝑆 ) ∧ 𝑤 ∈ Word 𝐴 ) → ( 𝑆 Σg 𝑤 ) ∈ 𝐴 )
149 144 147 148 syl2anc ⊢ ( ( 𝐷 ∈ Fin ∧ 𝑤 ∈ Word 𝐶 ) → ( 𝑆 Σg 𝑤 ) ∈ 𝐴 )
150 149 adantr ⊢ ( ( ( 𝐷 ∈ Fin ∧ 𝑤 ∈ Word 𝐶 ) ∧ 𝑄 = ( 𝑆 Σg 𝑤 ) ) → ( 𝑆 Σg 𝑤 ) ∈ 𝐴 )
151 138 150 eqeltrd ⊢ ( ( ( 𝐷 ∈ Fin ∧ 𝑤 ∈ Word 𝐶 ) ∧ 𝑄 = ( 𝑆 Σg 𝑤 ) ) → 𝑄 ∈ 𝐴 )
152 151 r19.29an ⊢ ( ( 𝐷 ∈ Fin ∧ ∃ 𝑤 ∈ Word 𝐶 𝑄 = ( 𝑆 Σg 𝑤 ) ) → 𝑄 ∈ 𝐴 )
153 137 152 impbida ⊢ ( 𝐷 ∈ Fin → ( 𝑄 ∈ 𝐴 ↔ ∃ 𝑤 ∈ Word 𝐶 𝑄 = ( 𝑆 Σg 𝑤 ) ) )