Theorem cycpmco2lem1

Description: Lemma for cycpmco2 . (Contributed by Thierry Arnoux, 4-Jan-2024)

	Ref	Expression
Hypotheses	cycpmco2.c	⊢ 𝑀 = ( toCyc ‘ 𝐷 )
	cycpmco2.s	⊢ 𝑆 = ( SymGrp ‘ 𝐷 )
	cycpmco2.d	⊢ ( 𝜑 → 𝐷 ∈ 𝑉 )
	cycpmco2.w	⊢ ( 𝜑 → 𝑊 ∈ dom 𝑀 )
	cycpmco2.i	⊢ ( 𝜑 → 𝐼 ∈ ( 𝐷 ∖ ran 𝑊 ) )
	cycpmco2.j	⊢ ( 𝜑 → 𝐽 ∈ ran 𝑊 )
	cycpmco2.e	⊢ 𝐸 = ( ( ◡ 𝑊 ‘ 𝐽 ) + 1 )
	cycpmco2.1	⊢ 𝑈 = ( 𝑊 splice ⟨ 𝐸 , 𝐸 , ⟨“ 𝐼 ”⟩ ⟩ )
Assertion	cycpmco2lem1	⊢ ( 𝜑 → ( ( 𝑀 ‘ 𝑊 ) ‘ ( ( 𝑀 ‘ ⟨“ 𝐼 𝐽 ”⟩ ) ‘ 𝐼 ) ) = ( ( 𝑀 ‘ 𝑊 ) ‘ 𝐽 ) )

Proof

Step	Hyp	Ref	Expression
1		cycpmco2.c	⊢ 𝑀 = ( toCyc ‘ 𝐷 )
2		cycpmco2.s	⊢ 𝑆 = ( SymGrp ‘ 𝐷 )
3		cycpmco2.d	⊢ ( 𝜑 → 𝐷 ∈ 𝑉 )
4		cycpmco2.w	⊢ ( 𝜑 → 𝑊 ∈ dom 𝑀 )
5		cycpmco2.i	⊢ ( 𝜑 → 𝐼 ∈ ( 𝐷 ∖ ran 𝑊 ) )
6		cycpmco2.j	⊢ ( 𝜑 → 𝐽 ∈ ran 𝑊 )
7		cycpmco2.e	⊢ 𝐸 = ( ( ◡ 𝑊 ‘ 𝐽 ) + 1 )
8		cycpmco2.1	⊢ 𝑈 = ( 𝑊 splice ⟨ 𝐸 , 𝐸 , ⟨“ 𝐼 ”⟩ ⟩ )
9	5	eldifad	⊢ ( 𝜑 → 𝐼 ∈ 𝐷 )
10		ssrab2	⊢ { 𝑤 ∈ Word 𝐷 ∣ 𝑤 : dom 𝑤 –1-1→ 𝐷 } ⊆ Word 𝐷
11		eqid	⊢ ( Base ‘ 𝑆 ) = ( Base ‘ 𝑆 )
12	1 2 11	tocycf	⊢ ( 𝐷 ∈ 𝑉 → 𝑀 : { 𝑤 ∈ Word 𝐷 ∣ 𝑤 : dom 𝑤 –1-1→ 𝐷 } ⟶ ( Base ‘ 𝑆 ) )
13	3 12	syl	⊢ ( 𝜑 → 𝑀 : { 𝑤 ∈ Word 𝐷 ∣ 𝑤 : dom 𝑤 –1-1→ 𝐷 } ⟶ ( Base ‘ 𝑆 ) )
14	13	fdmd	⊢ ( 𝜑 → dom 𝑀 = { 𝑤 ∈ Word 𝐷 ∣ 𝑤 : dom 𝑤 –1-1→ 𝐷 } )
15	4 14	eleqtrd	⊢ ( 𝜑 → 𝑊 ∈ { 𝑤 ∈ Word 𝐷 ∣ 𝑤 : dom 𝑤 –1-1→ 𝐷 } )
16	10 15	sseldi	⊢ ( 𝜑 → 𝑊 ∈ Word 𝐷 )
17		id	⊢ ( 𝑤 = 𝑊 → 𝑤 = 𝑊 )
18		dmeq	⊢ ( 𝑤 = 𝑊 → dom 𝑤 = dom 𝑊 )
19		eqidd	⊢ ( 𝑤 = 𝑊 → 𝐷 = 𝐷 )
20	17 18 19	f1eq123d	⊢ ( 𝑤 = 𝑊 → ( 𝑤 : dom 𝑤 –1-1→ 𝐷 ↔ 𝑊 : dom 𝑊 –1-1→ 𝐷 ) )
21	20	elrab3	⊢ ( 𝑊 ∈ Word 𝐷 → ( 𝑊 ∈ { 𝑤 ∈ Word 𝐷 ∣ 𝑤 : dom 𝑤 –1-1→ 𝐷 } ↔ 𝑊 : dom 𝑊 –1-1→ 𝐷 ) )
22	21	biimpa	⊢ ( ( 𝑊 ∈ Word 𝐷 ∧ 𝑊 ∈ { 𝑤 ∈ Word 𝐷 ∣ 𝑤 : dom 𝑤 –1-1→ 𝐷 } ) → 𝑊 : dom 𝑊 –1-1→ 𝐷 )
23	16 15 22	syl2anc	⊢ ( 𝜑 → 𝑊 : dom 𝑊 –1-1→ 𝐷 )
24		f1f	⊢ ( 𝑊 : dom 𝑊 –1-1→ 𝐷 → 𝑊 : dom 𝑊 ⟶ 𝐷 )
25	23 24	syl	⊢ ( 𝜑 → 𝑊 : dom 𝑊 ⟶ 𝐷 )
26	25	frnd	⊢ ( 𝜑 → ran 𝑊 ⊆ 𝐷 )
27	26 6	sseldd	⊢ ( 𝜑 → 𝐽 ∈ 𝐷 )
28	5	eldifbd	⊢ ( 𝜑 → ¬ 𝐼 ∈ ran 𝑊 )
29		nelne2	⊢ ( ( 𝐽 ∈ ran 𝑊 ∧ ¬ 𝐼 ∈ ran 𝑊 ) → 𝐽 ≠ 𝐼 )
30	6 28 29	syl2anc	⊢ ( 𝜑 → 𝐽 ≠ 𝐼 )
31	30	necomd	⊢ ( 𝜑 → 𝐼 ≠ 𝐽 )
32	1 3 9 27 31 2	cyc2fv1	⊢ ( 𝜑 → ( ( 𝑀 ‘ ⟨“ 𝐼 𝐽 ”⟩ ) ‘ 𝐼 ) = 𝐽 )
33	32	fveq2d	⊢ ( 𝜑 → ( ( 𝑀 ‘ 𝑊 ) ‘ ( ( 𝑀 ‘ ⟨“ 𝐼 𝐽 ”⟩ ) ‘ 𝐼 ) ) = ( ( 𝑀 ‘ 𝑊 ) ‘ 𝐽 ) )