Theorem cyc2fv2

Description: Function value of a 2-cycle at the second point. (Contributed by Thierry Arnoux, 24-Sep-2023)

	Ref	Expression
Hypotheses	cycpm2.c	$$⊢C=\mathrm{toCyc}\left(D\right)$$
	cycpm2.d	$$⊢\phi \to D\in V$$
	cycpm2.i	$$⊢\phi \to I\in D$$
	cycpm2.j	$$⊢\phi \to J\in D$$
	cycpm2.1	$$⊢\phi \to I\ne J$$
	cycpm2cl.s	$$⊢S=\mathrm{SymGrp}\left(D\right)$$
Assertion	cyc2fv2	$$⊢\phi \to C\left(⟨“IJ”⟩\right)\left(J\right)=I$$

Proof

Step	Hyp	Ref	Expression
1		cycpm2.c	$$⊢C=\mathrm{toCyc}\left(D\right)$$
2		cycpm2.d	$$⊢\phi \to D\in V$$
3		cycpm2.i	$$⊢\phi \to I\in D$$
4		cycpm2.j	$$⊢\phi \to J\in D$$
5		cycpm2.1	$$⊢\phi \to I\ne J$$
6		cycpm2cl.s	$$⊢S=\mathrm{SymGrp}\left(D\right)$$
7	3 4	s2cld	$$⊢\phi \to ⟨“IJ”⟩\in \mathrm{Word}D$$
8	3 4 5	s2f1	$$⊢\phi \to ⟨“IJ”⟩:\mathrm{dom}⟨“IJ”⟩\underset{1-1}{⟶}D$$
9		2pos	$$⊢0<2$$
10		s2len	$$⊢\left|⟨“IJ”⟩\right|=2$$
11	9 10	breqtrri	$$⊢0<\left|⟨“IJ”⟩\right|$$
12	11	a1i	$$⊢\phi \to 0<\left|⟨“IJ”⟩\right|$$
13	10	oveq1i	$$⊢\left|⟨“IJ”⟩\right|-1=2-1$$
14		2m1e1	$$⊢2-1=1$$
15	13 14	eqtr2i	$$⊢1=\left|⟨“IJ”⟩\right|-1$$
16	15	a1i	$$⊢\phi \to 1=\left|⟨“IJ”⟩\right|-1$$
17	1 2 7 8 12 16	cycpmfv2	$$⊢\phi \to C\left(⟨“IJ”⟩\right)\left(⟨“IJ”⟩\left(1\right)\right)=⟨“IJ”⟩\left(0\right)$$
18		s2fv1	$$⊢J\in D\to ⟨“IJ”⟩\left(1\right)=J$$
19	4 18	syl	$$⊢\phi \to ⟨“IJ”⟩\left(1\right)=J$$
20	19	fveq2d	$$⊢\phi \to C\left(⟨“IJ”⟩\right)\left(⟨“IJ”⟩\left(1\right)\right)=C\left(⟨“IJ”⟩\right)\left(J\right)$$
21		s2fv0	$$⊢I\in D\to ⟨“IJ”⟩\left(0\right)=I$$
22	3 21	syl	$$⊢\phi \to ⟨“IJ”⟩\left(0\right)=I$$
23	17 20 22	3eqtr3d	$$⊢\phi \to C\left(⟨“IJ”⟩\right)\left(J\right)=I$$