Theorem cyc2fv1

Description: Function value of a 2-cycle at the first 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	cyc2fv1	$$⊢\phi \to C\left(⟨“IJ”⟩\right)\left(I\right)=J$$

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		c0ex	$$⊢0\in \mathrm{V}$$
10	9	snid	$$⊢0\in \left\{0\right\}$$
11		s2len	$$⊢\left|⟨“IJ”⟩\right|=2$$
12	11	oveq1i	$$⊢\left|⟨“IJ”⟩\right|-1=2-1$$
13		2m1e1	$$⊢2-1=1$$
14	12 13	eqtr2i	$$⊢1=\left|⟨“IJ”⟩\right|-1$$
15	14	oveq2i	$$⊢\left(0..^1\right)=\left(0..^\left|⟨“IJ”⟩\right|-1\right)$$
16		fzo01	$$⊢\left(0..^1\right)=\left\{0\right\}$$
17	15 16	eqtr3i	$$⊢\left(0..^\left|⟨“IJ”⟩\right|-1\right)=\left\{0\right\}$$
18	10 17	eleqtrri	$$⊢0\in \left(0..^\left|⟨“IJ”⟩\right|-1\right)$$
19	18	a1i	$$⊢\phi \to 0\in \left(0..^\left|⟨“IJ”⟩\right|-1\right)$$
20	1 2 7 8 19	cycpmfv1	$$⊢\phi \to C\left(⟨“IJ”⟩\right)\left(⟨“IJ”⟩\left(0\right)\right)=⟨“IJ”⟩\left(0+1\right)$$
21		s2fv0	$$⊢I\in D\to ⟨“IJ”⟩\left(0\right)=I$$
22	3 21	syl	$$⊢\phi \to ⟨“IJ”⟩\left(0\right)=I$$
23	22	fveq2d	$$⊢\phi \to C\left(⟨“IJ”⟩\right)\left(⟨“IJ”⟩\left(0\right)\right)=C\left(⟨“IJ”⟩\right)\left(I\right)$$
24		0p1e1	$$⊢0+1=1$$
25	24	fveq2i	$$⊢⟨“IJ”⟩\left(0+1\right)=⟨“IJ”⟩\left(1\right)$$
26		s2fv1	$$⊢J\in D\to ⟨“IJ”⟩\left(1\right)=J$$
27	4 26	syl	$$⊢\phi \to ⟨“IJ”⟩\left(1\right)=J$$
28	25 27	syl5eq	$$⊢\phi \to ⟨“IJ”⟩\left(0+1\right)=J$$
29	20 23 28	3eqtr3d	$$⊢\phi \to C\left(⟨“IJ”⟩\right)\left(I\right)=J$$