cshf1

Description: Cyclically shifting a word which contains a symbol at most once results in a word which contains a symbol at most once. (Contributed by AV, 14-Mar-2021)

		Ref	Expression
	Assertion	cshf1	$⊢ (F : (0 ..^\|F\|) \underset{1-1}{⟶} A \land S \in ℤ \land G = F cyclShift S) \to G : (0 ..^\|F\|) \underset{1-1}{⟶} A$

Proof

Step	Hyp	Ref	Expression
1		f1f	$⊢ F : (0 ..^\|F\|) \underset{1-1}{⟶} A \to F : (0 ..^\|F\|) ⟶ A$
2		iswrdi	$⊢ F : (0 ..^\|F\|) ⟶ A \to F \in Word A$
3	1 2	syl	$⊢ F : (0 ..^\|F\|) \underset{1-1}{⟶} A \to F \in Word A$
4		cshwf	$⊢ (F \in Word A \land S \in ℤ) \to (F cyclShift S) : (0 ..^\|F\|) ⟶ A$
5	4	3adant1	$⊢ (F : (0 ..^\|F\|) \underset{1-1}{⟶} A \land F \in Word A \land S \in ℤ) \to (F cyclShift S) : (0 ..^\|F\|) ⟶ A$
6	5	adantr	$⊢ ((F : (0 ..^\|F\|) \underset{1-1}{⟶} A \land F \in Word A \land S \in ℤ) \land G = F cyclShift S) \to (F cyclShift S) : (0 ..^\|F\|) ⟶ A$
7		feq1	$⊢ G = F cyclShift S \to (G : (0 ..^\|F\|) ⟶ A \leftrightarrow (F cyclShift S) : (0 ..^\|F\|) ⟶ A)$
8	7	adantl	$⊢ ((F : (0 ..^\|F\|) \underset{1-1}{⟶} A \land F \in Word A \land S \in ℤ) \land G = F cyclShift S) \to (G : (0 ..^\|F\|) ⟶ A \leftrightarrow (F cyclShift S) : (0 ..^\|F\|) ⟶ A)$
9	6 8	mpbird	$⊢ ((F : (0 ..^\|F\|) \underset{1-1}{⟶} A \land F \in Word A \land S \in ℤ) \land G = F cyclShift S) \to G : (0 ..^\|F\|) ⟶ A$
10		dff13	$⊢ F : (0 ..^\|F\|) \underset{1-1}{⟶} A \leftrightarrow (F : (0 ..^\|F\|) ⟶ A \land \forall x \in (0 ..^\|F\|) \forall y \in (0 ..^\|F\|) (F (x) = F (y) \to x = y))$
11		fveq1	$⊢ G = F cyclShift S \to G (i) = (F cyclShift S) (i)$
12	11	3ad2ant1	$⊢ (G = F cyclShift S \land F \in Word A \land S \in ℤ) \to G (i) = (F cyclShift S) (i)$
13	12	adantr	$⊢ ((G = F cyclShift S \land F \in Word A \land S \in ℤ) \land (i \in (0 ..^\|F\|) \land j \in (0 ..^\|F\|))) \to G (i) = (F cyclShift S) (i)$
14		cshwidxmod	$⊢ (F \in Word A \land S \in ℤ \land i \in (0 ..^\|F\|)) \to (F cyclShift S) (i) = F ((i + S) \mod \|F\|)$
15	14	3expia	$⊢ (F \in Word A \land S \in ℤ) \to (i \in (0 ..^\|F\|) \to (F cyclShift S) (i) = F ((i + S) \mod \|F\|))$
16	15	3adant1	$⊢ (G = F cyclShift S \land F \in Word A \land S \in ℤ) \to (i \in (0 ..^\|F\|) \to (F cyclShift S) (i) = F ((i + S) \mod \|F\|))$
17	16	com12	$⊢ i \in (0 ..^\|F\|) \to ((G = F cyclShift S \land F \in Word A \land S \in ℤ) \to (F cyclShift S) (i) = F ((i + S) \mod \|F\|))$
18	17	adantr	$⊢ (i \in (0 ..^\|F\|) \land j \in (0 ..^\|F\|)) \to ((G = F cyclShift S \land F \in Word A \land S \in ℤ) \to (F cyclShift S) (i) = F ((i + S) \mod \|F\|))$
19	18	impcom	$⊢ ((G = F cyclShift S \land F \in Word A \land S \in ℤ) \land (i \in (0 ..^\|F\|) \land j \in (0 ..^\|F\|))) \to (F cyclShift S) (i) = F ((i + S) \mod \|F\|)$
20	13 19	eqtrd	$⊢ ((G = F cyclShift S \land F \in Word A \land S \in ℤ) \land (i \in (0 ..^\|F\|) \land j \in (0 ..^\|F\|))) \to G (i) = F ((i + S) \mod \|F\|)$
21		fveq1	$⊢ G = F cyclShift S \to G (j) = (F cyclShift S) (j)$
22	21	3ad2ant1	$⊢ (G = F cyclShift S \land F \in Word A \land S \in ℤ) \to G (j) = (F cyclShift S) (j)$
23	22	adantr	$⊢ ((G = F cyclShift S \land F \in Word A \land S \in ℤ) \land (i \in (0 ..^\|F\|) \land j \in (0 ..^\|F\|))) \to G (j) = (F cyclShift S) (j)$
24		cshwidxmod	$⊢ (F \in Word A \land S \in ℤ \land j \in (0 ..^\|F\|)) \to (F cyclShift S) (j) = F ((j + S) \mod \|F\|)$
25	24	3expia	$⊢ (F \in Word A \land S \in ℤ) \to (j \in (0 ..^\|F\|) \to (F cyclShift S) (j) = F ((j + S) \mod \|F\|))$
26	25	3adant1	$⊢ (G = F cyclShift S \land F \in Word A \land S \in ℤ) \to (j \in (0 ..^\|F\|) \to (F cyclShift S) (j) = F ((j + S) \mod \|F\|))$
27	26	adantld	$⊢ (G = F cyclShift S \land F \in Word A \land S \in ℤ) \to ((i \in (0 ..^\|F\|) \land j \in (0 ..^\|F\|)) \to (F cyclShift S) (j) = F ((j + S) \mod \|F\|))$
28	27	imp	$⊢ ((G = F cyclShift S \land F \in Word A \land S \in ℤ) \land (i \in (0 ..^\|F\|) \land j \in (0 ..^\|F\|))) \to (F cyclShift S) (j) = F ((j + S) \mod \|F\|)$
29	23 28	eqtrd	$⊢ ((G = F cyclShift S \land F \in Word A \land S \in ℤ) \land (i \in (0 ..^\|F\|) \land j \in (0 ..^\|F\|))) \to G (j) = F ((j + S) \mod \|F\|)$
30	20 29	eqeq12d	$⊢ ((G = F cyclShift S \land F \in Word A \land S \in ℤ) \land (i \in (0 ..^\|F\|) \land j \in (0 ..^\|F\|))) \to (G (i) = G (j) \leftrightarrow F ((i + S) \mod \|F\|) = F ((j + S) \mod \|F\|))$
31	30	adantlr	$⊢ (((G = F cyclShift S \land F \in Word A \land S \in ℤ) \land \forall x \in (0 ..^\|F\|) \forall y \in (0 ..^\|F\|) (F (x) = F (y) \to x = y)) \land (i \in (0 ..^\|F\|) \land j \in (0 ..^\|F\|))) \to (G (i) = G (j) \leftrightarrow F ((i + S) \mod \|F\|) = F ((j + S) \mod \|F\|))$
32		elfzo0	$⊢ i \in (0 ..^\|F\|) \leftrightarrow (i \in ℕ_{0} \land \|F\| \in ℕ \land i < \|F\|)$
33		nn0z	$⊢ i \in ℕ_{0} \to i \in ℤ$
34	33	adantr	$⊢ (i \in ℕ_{0} \land \|F\| \in ℕ) \to i \in ℤ$
35	34	adantl	$⊢ (S \in ℤ \land (i \in ℕ_{0} \land \|F\| \in ℕ)) \to i \in ℤ$
36		simpl	$⊢ (S \in ℤ \land (i \in ℕ_{0} \land \|F\| \in ℕ)) \to S \in ℤ$
37	35 36	zaddcld	$⊢ (S \in ℤ \land (i \in ℕ_{0} \land \|F\| \in ℕ)) \to i + S \in ℤ$
38		simpr	$⊢ (i \in ℕ_{0} \land \|F\| \in ℕ) \to \|F\| \in ℕ$
39	38	adantl	$⊢ (S \in ℤ \land (i \in ℕ_{0} \land \|F\| \in ℕ)) \to \|F\| \in ℕ$
40	37 39	jca	$⊢ (S \in ℤ \land (i \in ℕ_{0} \land \|F\| \in ℕ)) \to (i + S \in ℤ \land \|F\| \in ℕ)$
41	40	ex	$⊢ S \in ℤ \to ((i \in ℕ_{0} \land \|F\| \in ℕ) \to (i + S \in ℤ \land \|F\| \in ℕ))$
42	41	3ad2ant3	$⊢ (G = F cyclShift S \land F \in Word A \land S \in ℤ) \to ((i \in ℕ_{0} \land \|F\| \in ℕ) \to (i + S \in ℤ \land \|F\| \in ℕ))$
43	42	com12	$⊢ (i \in ℕ_{0} \land \|F\| \in ℕ) \to ((G = F cyclShift S \land F \in Word A \land S \in ℤ) \to (i + S \in ℤ \land \|F\| \in ℕ))$
44	43	3adant3	$⊢ (i \in ℕ_{0} \land \|F\| \in ℕ \land i < \|F\|) \to ((G = F cyclShift S \land F \in Word A \land S \in ℤ) \to (i + S \in ℤ \land \|F\| \in ℕ))$
45	32 44	sylbi	$⊢ i \in (0 ..^\|F\|) \to ((G = F cyclShift S \land F \in Word A \land S \in ℤ) \to (i + S \in ℤ \land \|F\| \in ℕ))$
46	45	adantr	$⊢ (i \in (0 ..^\|F\|) \land j \in (0 ..^\|F\|)) \to ((G = F cyclShift S \land F \in Word A \land S \in ℤ) \to (i + S \in ℤ \land \|F\| \in ℕ))$
47	46	impcom	$⊢ ((G = F cyclShift S \land F \in Word A \land S \in ℤ) \land (i \in (0 ..^\|F\|) \land j \in (0 ..^\|F\|))) \to (i + S \in ℤ \land \|F\| \in ℕ)$
48		zmodfzo	$⊢ (i + S \in ℤ \land \|F\| \in ℕ) \to (i + S) \mod \|F\| \in (0 ..^\|F\|)$
49	47 48	syl	$⊢ ((G = F cyclShift S \land F \in Word A \land S \in ℤ) \land (i \in (0 ..^\|F\|) \land j \in (0 ..^\|F\|))) \to (i + S) \mod \|F\| \in (0 ..^\|F\|)$
50		elfzo0	$⊢ j \in (0 ..^\|F\|) \leftrightarrow (j \in ℕ_{0} \land \|F\| \in ℕ \land j < \|F\|)$
51		nn0z	$⊢ j \in ℕ_{0} \to j \in ℤ$
52	51	adantr	$⊢ (j \in ℕ_{0} \land \|F\| \in ℕ) \to j \in ℤ$
53	52	adantl	$⊢ (S \in ℤ \land (j \in ℕ_{0} \land \|F\| \in ℕ)) \to j \in ℤ$
54		simpl	$⊢ (S \in ℤ \land (j \in ℕ_{0} \land \|F\| \in ℕ)) \to S \in ℤ$
55	53 54	zaddcld	$⊢ (S \in ℤ \land (j \in ℕ_{0} \land \|F\| \in ℕ)) \to j + S \in ℤ$
56		simpr	$⊢ (j \in ℕ_{0} \land \|F\| \in ℕ) \to \|F\| \in ℕ$
57	56	adantl	$⊢ (S \in ℤ \land (j \in ℕ_{0} \land \|F\| \in ℕ)) \to \|F\| \in ℕ$
58	55 57	jca	$⊢ (S \in ℤ \land (j \in ℕ_{0} \land \|F\| \in ℕ)) \to (j + S \in ℤ \land \|F\| \in ℕ)$
59	58	expcom	$⊢ (j \in ℕ_{0} \land \|F\| \in ℕ) \to (S \in ℤ \to (j + S \in ℤ \land \|F\| \in ℕ))$
60	59	3adant3	$⊢ (j \in ℕ_{0} \land \|F\| \in ℕ \land j < \|F\|) \to (S \in ℤ \to (j + S \in ℤ \land \|F\| \in ℕ))$
61	50 60	sylbi	$⊢ j \in (0 ..^\|F\|) \to (S \in ℤ \to (j + S \in ℤ \land \|F\| \in ℕ))$
62	61	com12	$⊢ S \in ℤ \to (j \in (0 ..^\|F\|) \to (j + S \in ℤ \land \|F\| \in ℕ))$
63	62	3ad2ant3	$⊢ (G = F cyclShift S \land F \in Word A \land S \in ℤ) \to (j \in (0 ..^\|F\|) \to (j + S \in ℤ \land \|F\| \in ℕ))$
64	63	adantld	$⊢ (G = F cyclShift S \land F \in Word A \land S \in ℤ) \to ((i \in (0 ..^\|F\|) \land j \in (0 ..^\|F\|)) \to (j + S \in ℤ \land \|F\| \in ℕ))$
65	64	imp	$⊢ ((G = F cyclShift S \land F \in Word A \land S \in ℤ) \land (i \in (0 ..^\|F\|) \land j \in (0 ..^\|F\|))) \to (j + S \in ℤ \land \|F\| \in ℕ)$
66		zmodfzo	$⊢ (j + S \in ℤ \land \|F\| \in ℕ) \to (j + S) \mod \|F\| \in (0 ..^\|F\|)$
67	65 66	syl	$⊢ ((G = F cyclShift S \land F \in Word A \land S \in ℤ) \land (i \in (0 ..^\|F\|) \land j \in (0 ..^\|F\|))) \to (j + S) \mod \|F\| \in (0 ..^\|F\|)$
68		fveqeq2	$⊢ x = (i + S) \mod \|F\| \to (F (x) = F (y) \leftrightarrow F ((i + S) \mod \|F\|) = F (y))$
69		eqeq1	$⊢ x = (i + S) \mod \|F\| \to (x = y \leftrightarrow (i + S) \mod \|F\| = y)$
70	68 69	imbi12d	$⊢ x = (i + S) \mod \|F\| \to ((F (x) = F (y) \to x = y) \leftrightarrow (F ((i + S) \mod \|F\|) = F (y) \to (i + S) \mod \|F\| = y))$
71		fveq2	$⊢ y = (j + S) \mod \|F\| \to F (y) = F ((j + S) \mod \|F\|)$
72	71	eqeq2d	$⊢ y = (j + S) \mod \|F\| \to (F ((i + S) \mod \|F\|) = F (y) \leftrightarrow F ((i + S) \mod \|F\|) = F ((j + S) \mod \|F\|))$
73		eqeq2	$⊢ y = (j + S) \mod \|F\| \to ((i + S) \mod \|F\| = y \leftrightarrow (i + S) \mod \|F\| = (j + S) \mod \|F\|)$
74	72 73	imbi12d	$⊢ y = (j + S) \mod \|F\| \to ((F ((i + S) \mod \|F\|) = F (y) \to (i + S) \mod \|F\| = y) \leftrightarrow (F ((i + S) \mod \|F\|) = F ((j + S) \mod \|F\|) \to (i + S) \mod \|F\| = (j + S) \mod \|F\|))$
75	70 74	rspc2v	$⊢ ((i + S) \mod \|F\| \in (0 ..^\|F\|) \land (j + S) \mod \|F\| \in (0 ..^\|F\|)) \to (\forall x \in (0 ..^\|F\|) \forall y \in (0 ..^\|F\|) (F (x) = F (y) \to x = y) \to (F ((i + S) \mod \|F\|) = F ((j + S) \mod \|F\|) \to (i + S) \mod \|F\| = (j + S) \mod \|F\|))$
76	49 67 75	syl2anc	$⊢ ((G = F cyclShift S \land F \in Word A \land S \in ℤ) \land (i \in (0 ..^\|F\|) \land j \in (0 ..^\|F\|))) \to (\forall x \in (0 ..^\|F\|) \forall y \in (0 ..^\|F\|) (F (x) = F (y) \to x = y) \to (F ((i + S) \mod \|F\|) = F ((j + S) \mod \|F\|) \to (i + S) \mod \|F\| = (j + S) \mod \|F\|))$
77		simpr	$⊢ (((G = F cyclShift S \land F \in Word A \land S \in ℤ) \land (i \in (0 ..^\|F\|) \land j \in (0 ..^\|F\|))) \land (F ((i + S) \mod \|F\|) = F ((j + S) \mod \|F\|) \to (i + S) \mod \|F\| = (j + S) \mod \|F\|)) \to (F ((i + S) \mod \|F\|) = F ((j + S) \mod \|F\|) \to (i + S) \mod \|F\| = (j + S) \mod \|F\|)$
78		addmodlteq	$⊢ (i \in (0 ..^\|F\|) \land j \in (0 ..^\|F\|) \land S \in ℤ) \to ((i + S) \mod \|F\| = (j + S) \mod \|F\| \leftrightarrow i = j)$
79	78	3expa	$⊢ ((i \in (0 ..^\|F\|) \land j \in (0 ..^\|F\|)) \land S \in ℤ) \to ((i + S) \mod \|F\| = (j + S) \mod \|F\| \leftrightarrow i = j)$
80	79	ancoms	$⊢ (S \in ℤ \land (i \in (0 ..^\|F\|) \land j \in (0 ..^\|F\|))) \to ((i + S) \mod \|F\| = (j + S) \mod \|F\| \leftrightarrow i = j)$
81	80	bicomd	$⊢ (S \in ℤ \land (i \in (0 ..^\|F\|) \land j \in (0 ..^\|F\|))) \to (i = j \leftrightarrow (i + S) \mod \|F\| = (j + S) \mod \|F\|)$
82	81	3ad2antl3	$⊢ ((G = F cyclShift S \land F \in Word A \land S \in ℤ) \land (i \in (0 ..^\|F\|) \land j \in (0 ..^\|F\|))) \to (i = j \leftrightarrow (i + S) \mod \|F\| = (j + S) \mod \|F\|)$
83	82	adantr	$⊢ (((G = F cyclShift S \land F \in Word A \land S \in ℤ) \land (i \in (0 ..^\|F\|) \land j \in (0 ..^\|F\|))) \land (F ((i + S) \mod \|F\|) = F ((j + S) \mod \|F\|) \to (i + S) \mod \|F\| = (j + S) \mod \|F\|)) \to (i = j \leftrightarrow (i + S) \mod \|F\| = (j + S) \mod \|F\|)$
84	77 83	sylibrd	$⊢ (((G = F cyclShift S \land F \in Word A \land S \in ℤ) \land (i \in (0 ..^\|F\|) \land j \in (0 ..^\|F\|))) \land (F ((i + S) \mod \|F\|) = F ((j + S) \mod \|F\|) \to (i + S) \mod \|F\| = (j + S) \mod \|F\|)) \to (F ((i + S) \mod \|F\|) = F ((j + S) \mod \|F\|) \to i = j)$
85	84	ex	$⊢ ((G = F cyclShift S \land F \in Word A \land S \in ℤ) \land (i \in (0 ..^\|F\|) \land j \in (0 ..^\|F\|))) \to ((F ((i + S) \mod \|F\|) = F ((j + S) \mod \|F\|) \to (i + S) \mod \|F\| = (j + S) \mod \|F\|) \to (F ((i + S) \mod \|F\|) = F ((j + S) \mod \|F\|) \to i = j))$
86	76 85	syld	$⊢ ((G = F cyclShift S \land F \in Word A \land S \in ℤ) \land (i \in (0 ..^\|F\|) \land j \in (0 ..^\|F\|))) \to (\forall x \in (0 ..^\|F\|) \forall y \in (0 ..^\|F\|) (F (x) = F (y) \to x = y) \to (F ((i + S) \mod \|F\|) = F ((j + S) \mod \|F\|) \to i = j))$
87	86	impancom	$⊢ ((G = F cyclShift S \land F \in Word A \land S \in ℤ) \land \forall x \in (0 ..^\|F\|) \forall y \in (0 ..^\|F\|) (F (x) = F (y) \to x = y)) \to ((i \in (0 ..^\|F\|) \land j \in (0 ..^\|F\|)) \to (F ((i + S) \mod \|F\|) = F ((j + S) \mod \|F\|) \to i = j))$
88	87	imp	$⊢ (((G = F cyclShift S \land F \in Word A \land S \in ℤ) \land \forall x \in (0 ..^\|F\|) \forall y \in (0 ..^\|F\|) (F (x) = F (y) \to x = y)) \land (i \in (0 ..^\|F\|) \land j \in (0 ..^\|F\|))) \to (F ((i + S) \mod \|F\|) = F ((j + S) \mod \|F\|) \to i = j)$
89	31 88	sylbid	$⊢ (((G = F cyclShift S \land F \in Word A \land S \in ℤ) \land \forall x \in (0 ..^\|F\|) \forall y \in (0 ..^\|F\|) (F (x) = F (y) \to x = y)) \land (i \in (0 ..^\|F\|) \land j \in (0 ..^\|F\|))) \to (G (i) = G (j) \to i = j)$
90	89	ralrimivva	$⊢ ((G = F cyclShift S \land F \in Word A \land S \in ℤ) \land \forall x \in (0 ..^\|F\|) \forall y \in (0 ..^\|F\|) (F (x) = F (y) \to x = y)) \to \forall i \in (0 ..^\|F\|) \forall j \in (0 ..^\|F\|) (G (i) = G (j) \to i = j)$
91	90	3exp1	$⊢ G = F cyclShift S \to (F \in Word A \to (S \in ℤ \to (\forall x \in (0 ..^\|F\|) \forall y \in (0 ..^\|F\|) (F (x) = F (y) \to x = y) \to \forall i \in (0 ..^\|F\|) \forall j \in (0 ..^\|F\|) (G (i) = G (j) \to i = j))))$
92	91	com14	$⊢ \forall x \in (0 ..^\|F\|) \forall y \in (0 ..^\|F\|) (F (x) = F (y) \to x = y) \to (F \in Word A \to (S \in ℤ \to (G = F cyclShift S \to \forall i \in (0 ..^\|F\|) \forall j \in (0 ..^\|F\|) (G (i) = G (j) \to i = j))))$
93	92	adantl	$⊢ (F : (0 ..^\|F\|) ⟶ A \land \forall x \in (0 ..^\|F\|) \forall y \in (0 ..^\|F\|) (F (x) = F (y) \to x = y)) \to (F \in Word A \to (S \in ℤ \to (G = F cyclShift S \to \forall i \in (0 ..^\|F\|) \forall j \in (0 ..^\|F\|) (G (i) = G (j) \to i = j))))$
94	10 93	sylbi	$⊢ F : (0 ..^\|F\|) \underset{1-1}{⟶} A \to (F \in Word A \to (S \in ℤ \to (G = F cyclShift S \to \forall i \in (0 ..^\|F\|) \forall j \in (0 ..^\|F\|) (G (i) = G (j) \to i = j))))$
95	94	3imp1	$⊢ ((F : (0 ..^\|F\|) \underset{1-1}{⟶} A \land F \in Word A \land S \in ℤ) \land G = F cyclShift S) \to \forall i \in (0 ..^\|F\|) \forall j \in (0 ..^\|F\|) (G (i) = G (j) \to i = j)$
96	9 95	jca	$⊢ ((F : (0 ..^\|F\|) \underset{1-1}{⟶} A \land F \in Word A \land S \in ℤ) \land G = F cyclShift S) \to (G : (0 ..^\|F\|) ⟶ A \land \forall i \in (0 ..^\|F\|) \forall j \in (0 ..^\|F\|) (G (i) = G (j) \to i = j))$
97	96	3exp1	$⊢ F : (0 ..^\|F\|) \underset{1-1}{⟶} A \to (F \in Word A \to (S \in ℤ \to (G = F cyclShift S \to (G : (0 ..^\|F\|) ⟶ A \land \forall i \in (0 ..^\|F\|) \forall j \in (0 ..^\|F\|) (G (i) = G (j) \to i = j)))))$
98	3 97	mpd	$⊢ F : (0 ..^\|F\|) \underset{1-1}{⟶} A \to (S \in ℤ \to (G = F cyclShift S \to (G : (0 ..^\|F\|) ⟶ A \land \forall i \in (0 ..^\|F\|) \forall j \in (0 ..^\|F\|) (G (i) = G (j) \to i = j))))$
99	98	3imp	$⊢ (F : (0 ..^\|F\|) \underset{1-1}{⟶} A \land S \in ℤ \land G = F cyclShift S) \to (G : (0 ..^\|F\|) ⟶ A \land \forall i \in (0 ..^\|F\|) \forall j \in (0 ..^\|F\|) (G (i) = G (j) \to i = j))$
100		dff13	$⊢ G : (0 ..^\|F\|) \underset{1-1}{⟶} A \leftrightarrow (G : (0 ..^\|F\|) ⟶ A \land \forall i \in (0 ..^\|F\|) \forall j \in (0 ..^\|F\|) (G (i) = G (j) \to i = j))$
101	99 100	sylibr	$⊢ (F : (0 ..^\|F\|) \underset{1-1}{⟶} A \land S \in ℤ \land G = F cyclShift S) \to G : (0 ..^\|F\|) \underset{1-1}{⟶} A$

Metamath Proof Explorer

Theorem cshf1

Proof