cshf1 - Metamath Proof Explorer

	Metamath Proof Explorer		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > cshf1		Structured version Visualization version GIF version

Theorem cshf1 13556

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.)

**Assertion**
Ref	Expression
cshf1	⊢ ((𝐹:(0..^(#‘𝐹))–1-1→𝐴 ∧ 𝑆 ∈ ℤ ∧ 𝐺 = (𝐹 cyclShift 𝑆)) → 𝐺:(0..^(#‘𝐹))–1-1→𝐴)

Proof of Theorem cshf1 Dummy variables 𝑖 𝑗 𝑥 𝑦 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		f1f 6101	. . . . 5 ⊢ (𝐹:(0..^(#‘𝐹))–1-1→𝐴 → 𝐹:(0..^(#‘𝐹))⟶𝐴)
2		iswrdi 13309	. . . . 5 ⊢ (𝐹:(0..^(#‘𝐹))⟶𝐴 → 𝐹 ∈ Word 𝐴)
3	1, 2	syl 17	. . . 4 ⊢ (𝐹:(0..^(#‘𝐹))–1-1→𝐴 → 𝐹 ∈ Word 𝐴)
4		cshwf 13546	. . . . . . . . 9 ⊢ ((𝐹 ∈ Word 𝐴 ∧ 𝑆 ∈ ℤ) → (𝐹 cyclShift 𝑆):(0..^(#‘𝐹))⟶𝐴)
5	4	3adant1 1079	. . . . . . . 8 ⊢ ((𝐹:(0..^(#‘𝐹))–1-1→𝐴 ∧ 𝐹 ∈ Word 𝐴 ∧ 𝑆 ∈ ℤ) → (𝐹 cyclShift 𝑆):(0..^(#‘𝐹))⟶𝐴)
6	5	adantr 481	. . . . . . 7 ⊢ (((𝐹:(0..^(#‘𝐹))–1-1→𝐴 ∧ 𝐹 ∈ Word 𝐴 ∧ 𝑆 ∈ ℤ) ∧ 𝐺 = (𝐹 cyclShift 𝑆)) → (𝐹 cyclShift 𝑆):(0..^(#‘𝐹))⟶𝐴)
7		feq1 6026	. . . . . . . 8 ⊢ (𝐺 = (𝐹 cyclShift 𝑆) → (𝐺:(0..^(#‘𝐹))⟶𝐴 ↔ (𝐹 cyclShift 𝑆):(0..^(#‘𝐹))⟶𝐴))
8	7	adantl 482	. . . . . . 7 ⊢ (((𝐹:(0..^(#‘𝐹))–1-1→𝐴 ∧ 𝐹 ∈ Word 𝐴 ∧ 𝑆 ∈ ℤ) ∧ 𝐺 = (𝐹 cyclShift 𝑆)) → (𝐺:(0..^(#‘𝐹))⟶𝐴 ↔ (𝐹 cyclShift 𝑆):(0..^(#‘𝐹))⟶𝐴))
9	6, 8	mpbird 247	. . . . . 6 ⊢ (((𝐹:(0..^(#‘𝐹))–1-1→𝐴 ∧ 𝐹 ∈ Word 𝐴 ∧ 𝑆 ∈ ℤ) ∧ 𝐺 = (𝐹 cyclShift 𝑆)) → 𝐺:(0..^(#‘𝐹))⟶𝐴)
10		dff13 6512	. . . . . . . 8 ⊢ (𝐹:(0..^(#‘𝐹))–1-1→𝐴 ↔ (𝐹:(0..^(#‘𝐹))⟶𝐴 ∧ ∀𝑥 ∈ (0..^(#‘𝐹))∀𝑦 ∈ (0..^(#‘𝐹))((𝐹‘𝑥) = (𝐹‘𝑦) → 𝑥 = 𝑦)))
11		fveq1 6190	. . . . . . . . . . . . . . . . . 18 ⊢ (𝐺 = (𝐹 cyclShift 𝑆) → (𝐺‘𝑖) = ((𝐹 cyclShift 𝑆)‘𝑖))
12	11	3ad2ant1 1082	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐺 = (𝐹 cyclShift 𝑆) ∧ 𝐹 ∈ Word 𝐴 ∧ 𝑆 ∈ ℤ) → (𝐺‘𝑖) = ((𝐹 cyclShift 𝑆)‘𝑖))
13	12	adantr 481	. . . . . . . . . . . . . . . 16 ⊢ (((𝐺 = (𝐹 cyclShift 𝑆) ∧ 𝐹 ∈ Word 𝐴 ∧ 𝑆 ∈ ℤ) ∧ (𝑖 ∈ (0..^(#‘𝐹)) ∧ 𝑗 ∈ (0..^(#‘𝐹)))) → (𝐺‘𝑖) = ((𝐹 cyclShift 𝑆)‘𝑖))
14		cshwidxmod 13549	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝐹 ∈ Word 𝐴 ∧ 𝑆 ∈ ℤ ∧ 𝑖 ∈ (0..^(#‘𝐹))) → ((𝐹 cyclShift 𝑆)‘𝑖) = (𝐹‘((𝑖 + 𝑆) mod (#‘𝐹))))
15	14	3expia 1267	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝐹 ∈ Word 𝐴 ∧ 𝑆 ∈ ℤ) → (𝑖 ∈ (0..^(#‘𝐹)) → ((𝐹 cyclShift 𝑆)‘𝑖) = (𝐹‘((𝑖 + 𝑆) mod (#‘𝐹)))))
16	15	3adant1 1079	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝐺 = (𝐹 cyclShift 𝑆) ∧ 𝐹 ∈ Word 𝐴 ∧ 𝑆 ∈ ℤ) → (𝑖 ∈ (0..^(#‘𝐹)) → ((𝐹 cyclShift 𝑆)‘𝑖) = (𝐹‘((𝑖 + 𝑆) mod (#‘𝐹)))))
17	16	com12 32	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑖 ∈ (0..^(#‘𝐹)) → ((𝐺 = (𝐹 cyclShift 𝑆) ∧ 𝐹 ∈ Word 𝐴 ∧ 𝑆 ∈ ℤ) → ((𝐹 cyclShift 𝑆)‘𝑖) = (𝐹‘((𝑖 + 𝑆) mod (#‘𝐹)))))
18	17	adantr 481	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑖 ∈ (0..^(#‘𝐹)) ∧ 𝑗 ∈ (0..^(#‘𝐹))) → ((𝐺 = (𝐹 cyclShift 𝑆) ∧ 𝐹 ∈ Word 𝐴 ∧ 𝑆 ∈ ℤ) → ((𝐹 cyclShift 𝑆)‘𝑖) = (𝐹‘((𝑖 + 𝑆) mod (#‘𝐹)))))
19	18	impcom 446	. . . . . . . . . . . . . . . 16 ⊢ (((𝐺 = (𝐹 cyclShift 𝑆) ∧ 𝐹 ∈ Word 𝐴 ∧ 𝑆 ∈ ℤ) ∧ (𝑖 ∈ (0..^(#‘𝐹)) ∧ 𝑗 ∈ (0..^(#‘𝐹)))) → ((𝐹 cyclShift 𝑆)‘𝑖) = (𝐹‘((𝑖 + 𝑆) mod (#‘𝐹))))
20	13, 19	eqtrd 2656	. . . . . . . . . . . . . . 15 ⊢ (((𝐺 = (𝐹 cyclShift 𝑆) ∧ 𝐹 ∈ Word 𝐴 ∧ 𝑆 ∈ ℤ) ∧ (𝑖 ∈ (0..^(#‘𝐹)) ∧ 𝑗 ∈ (0..^(#‘𝐹)))) → (𝐺‘𝑖) = (𝐹‘((𝑖 + 𝑆) mod (#‘𝐹))))
21		fveq1 6190	. . . . . . . . . . . . . . . . . 18 ⊢ (𝐺 = (𝐹 cyclShift 𝑆) → (𝐺‘𝑗) = ((𝐹 cyclShift 𝑆)‘𝑗))
22	21	3ad2ant1 1082	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐺 = (𝐹 cyclShift 𝑆) ∧ 𝐹 ∈ Word 𝐴 ∧ 𝑆 ∈ ℤ) → (𝐺‘𝑗) = ((𝐹 cyclShift 𝑆)‘𝑗))
23	22	adantr 481	. . . . . . . . . . . . . . . 16 ⊢ (((𝐺 = (𝐹 cyclShift 𝑆) ∧ 𝐹 ∈ Word 𝐴 ∧ 𝑆 ∈ ℤ) ∧ (𝑖 ∈ (0..^(#‘𝐹)) ∧ 𝑗 ∈ (0..^(#‘𝐹)))) → (𝐺‘𝑗) = ((𝐹 cyclShift 𝑆)‘𝑗))
24		cshwidxmod 13549	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝐹 ∈ Word 𝐴 ∧ 𝑆 ∈ ℤ ∧ 𝑗 ∈ (0..^(#‘𝐹))) → ((𝐹 cyclShift 𝑆)‘𝑗) = (𝐹‘((𝑗 + 𝑆) mod (#‘𝐹))))
25	24	3expia 1267	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝐹 ∈ Word 𝐴 ∧ 𝑆 ∈ ℤ) → (𝑗 ∈ (0..^(#‘𝐹)) → ((𝐹 cyclShift 𝑆)‘𝑗) = (𝐹‘((𝑗 + 𝑆) mod (#‘𝐹)))))
26	25	3adant1 1079	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐺 = (𝐹 cyclShift 𝑆) ∧ 𝐹 ∈ Word 𝐴 ∧ 𝑆 ∈ ℤ) → (𝑗 ∈ (0..^(#‘𝐹)) → ((𝐹 cyclShift 𝑆)‘𝑗) = (𝐹‘((𝑗 + 𝑆) mod (#‘𝐹)))))
27	26	adantld 483	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐺 = (𝐹 cyclShift 𝑆) ∧ 𝐹 ∈ Word 𝐴 ∧ 𝑆 ∈ ℤ) → ((𝑖 ∈ (0..^(#‘𝐹)) ∧ 𝑗 ∈ (0..^(#‘𝐹))) → ((𝐹 cyclShift 𝑆)‘𝑗) = (𝐹‘((𝑗 + 𝑆) mod (#‘𝐹)))))
28	27	imp 445	. . . . . . . . . . . . . . . 16 ⊢ (((𝐺 = (𝐹 cyclShift 𝑆) ∧ 𝐹 ∈ Word 𝐴 ∧ 𝑆 ∈ ℤ) ∧ (𝑖 ∈ (0..^(#‘𝐹)) ∧ 𝑗 ∈ (0..^(#‘𝐹)))) → ((𝐹 cyclShift 𝑆)‘𝑗) = (𝐹‘((𝑗 + 𝑆) mod (#‘𝐹))))
29	23, 28	eqtrd 2656	. . . . . . . . . . . . . . 15 ⊢ (((𝐺 = (𝐹 cyclShift 𝑆) ∧ 𝐹 ∈ Word 𝐴 ∧ 𝑆 ∈ ℤ) ∧ (𝑖 ∈ (0..^(#‘𝐹)) ∧ 𝑗 ∈ (0..^(#‘𝐹)))) → (𝐺‘𝑗) = (𝐹‘((𝑗 + 𝑆) mod (#‘𝐹))))
30	20, 29	eqeq12d 2637	. . . . . . . . . . . . . 14 ⊢ (((𝐺 = (𝐹 cyclShift 𝑆) ∧ 𝐹 ∈ Word 𝐴 ∧ 𝑆 ∈ ℤ) ∧ (𝑖 ∈ (0..^(#‘𝐹)) ∧ 𝑗 ∈ (0..^(#‘𝐹)))) → ((𝐺‘𝑖) = (𝐺‘𝑗) ↔ (𝐹‘((𝑖 + 𝑆) mod (#‘𝐹))) = (𝐹‘((𝑗 + 𝑆) mod (#‘𝐹)))))
31	30	adantlr 751	. . . . . . . . . . . . 13 ⊢ ((((𝐺 = (𝐹 cyclShift 𝑆) ∧ 𝐹 ∈ Word 𝐴 ∧ 𝑆 ∈ ℤ) ∧ ∀𝑥 ∈ (0..^(#‘𝐹))∀𝑦 ∈ (0..^(#‘𝐹))((𝐹‘𝑥) = (𝐹‘𝑦) → 𝑥 = 𝑦)) ∧ (𝑖 ∈ (0..^(#‘𝐹)) ∧ 𝑗 ∈ (0..^(#‘𝐹)))) → ((𝐺‘𝑖) = (𝐺‘𝑗) ↔ (𝐹‘((𝑖 + 𝑆) mod (#‘𝐹))) = (𝐹‘((𝑗 + 𝑆) mod (#‘𝐹)))))
32		elfzo0 12508	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑖 ∈ (0..^(#‘𝐹)) ↔ (𝑖 ∈ ℕ₀ ∧ (#‘𝐹) ∈ ℕ ∧ 𝑖 < (#‘𝐹)))
33		nn0z 11400	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝑖 ∈ ℕ₀ → 𝑖 ∈ ℤ)
34	33	adantr 481	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((𝑖 ∈ ℕ₀ ∧ (#‘𝐹) ∈ ℕ) → 𝑖 ∈ ℤ)
35	34	adantl 482	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝑆 ∈ ℤ ∧ (𝑖 ∈ ℕ₀ ∧ (#‘𝐹) ∈ ℕ)) → 𝑖 ∈ ℤ)
36		simpl 473	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝑆 ∈ ℤ ∧ (𝑖 ∈ ℕ₀ ∧ (#‘𝐹) ∈ ℕ)) → 𝑆 ∈ ℤ)
37	35, 36	zaddcld 11486	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝑆 ∈ ℤ ∧ (𝑖 ∈ ℕ₀ ∧ (#‘𝐹) ∈ ℕ)) → (𝑖 + 𝑆) ∈ ℤ)
38		simpr 477	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝑖 ∈ ℕ₀ ∧ (#‘𝐹) ∈ ℕ) → (#‘𝐹) ∈ ℕ)
39	38	adantl 482	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝑆 ∈ ℤ ∧ (𝑖 ∈ ℕ₀ ∧ (#‘𝐹) ∈ ℕ)) → (#‘𝐹) ∈ ℕ)
40	37, 39	jca 554	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝑆 ∈ ℤ ∧ (𝑖 ∈ ℕ₀ ∧ (#‘𝐹) ∈ ℕ)) → ((𝑖 + 𝑆) ∈ ℤ ∧ (#‘𝐹) ∈ ℕ))
41	40	ex 450	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑆 ∈ ℤ → ((𝑖 ∈ ℕ₀ ∧ (#‘𝐹) ∈ ℕ) → ((𝑖 + 𝑆) ∈ ℤ ∧ (#‘𝐹) ∈ ℕ)))
42	41	3ad2ant3 1084	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝐺 = (𝐹 cyclShift 𝑆) ∧ 𝐹 ∈ Word 𝐴 ∧ 𝑆 ∈ ℤ) → ((𝑖 ∈ ℕ₀ ∧ (#‘𝐹) ∈ ℕ) → ((𝑖 + 𝑆) ∈ ℤ ∧ (#‘𝐹) ∈ ℕ)))
43	42	com12 32	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑖 ∈ ℕ₀ ∧ (#‘𝐹) ∈ ℕ) → ((𝐺 = (𝐹 cyclShift 𝑆) ∧ 𝐹 ∈ Word 𝐴 ∧ 𝑆 ∈ ℤ) → ((𝑖 + 𝑆) ∈ ℤ ∧ (#‘𝐹) ∈ ℕ)))
44	43	3adant3 1081	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑖 ∈ ℕ₀ ∧ (#‘𝐹) ∈ ℕ ∧ 𝑖 < (#‘𝐹)) → ((𝐺 = (𝐹 cyclShift 𝑆) ∧ 𝐹 ∈ Word 𝐴 ∧ 𝑆 ∈ ℤ) → ((𝑖 + 𝑆) ∈ ℤ ∧ (#‘𝐹) ∈ ℕ)))
45	32, 44	sylbi 207	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑖 ∈ (0..^(#‘𝐹)) → ((𝐺 = (𝐹 cyclShift 𝑆) ∧ 𝐹 ∈ Word 𝐴 ∧ 𝑆 ∈ ℤ) → ((𝑖 + 𝑆) ∈ ℤ ∧ (#‘𝐹) ∈ ℕ)))
46	45	adantr 481	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑖 ∈ (0..^(#‘𝐹)) ∧ 𝑗 ∈ (0..^(#‘𝐹))) → ((𝐺 = (𝐹 cyclShift 𝑆) ∧ 𝐹 ∈ Word 𝐴 ∧ 𝑆 ∈ ℤ) → ((𝑖 + 𝑆) ∈ ℤ ∧ (#‘𝐹) ∈ ℕ)))
47	46	impcom 446	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝐺 = (𝐹 cyclShift 𝑆) ∧ 𝐹 ∈ Word 𝐴 ∧ 𝑆 ∈ ℤ) ∧ (𝑖 ∈ (0..^(#‘𝐹)) ∧ 𝑗 ∈ (0..^(#‘𝐹)))) → ((𝑖 + 𝑆) ∈ ℤ ∧ (#‘𝐹) ∈ ℕ))
48		zmodfzo 12693	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑖 + 𝑆) ∈ ℤ ∧ (#‘𝐹) ∈ ℕ) → ((𝑖 + 𝑆) mod (#‘𝐹)) ∈ (0..^(#‘𝐹)))
49	47, 48	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ (((𝐺 = (𝐹 cyclShift 𝑆) ∧ 𝐹 ∈ Word 𝐴 ∧ 𝑆 ∈ ℤ) ∧ (𝑖 ∈ (0..^(#‘𝐹)) ∧ 𝑗 ∈ (0..^(#‘𝐹)))) → ((𝑖 + 𝑆) mod (#‘𝐹)) ∈ (0..^(#‘𝐹)))
50		elfzo0 12508	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑗 ∈ (0..^(#‘𝐹)) ↔ (𝑗 ∈ ℕ₀ ∧ (#‘𝐹) ∈ ℕ ∧ 𝑗 < (#‘𝐹)))
51		nn0z 11400	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝑗 ∈ ℕ₀ → 𝑗 ∈ ℤ)
52	51	adantr 481	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((𝑗 ∈ ℕ₀ ∧ (#‘𝐹) ∈ ℕ) → 𝑗 ∈ ℤ)
53	52	adantl 482	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝑆 ∈ ℤ ∧ (𝑗 ∈ ℕ₀ ∧ (#‘𝐹) ∈ ℕ)) → 𝑗 ∈ ℤ)
54		simpl 473	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝑆 ∈ ℤ ∧ (𝑗 ∈ ℕ₀ ∧ (#‘𝐹) ∈ ℕ)) → 𝑆 ∈ ℤ)
55	53, 54	zaddcld 11486	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝑆 ∈ ℤ ∧ (𝑗 ∈ ℕ₀ ∧ (#‘𝐹) ∈ ℕ)) → (𝑗 + 𝑆) ∈ ℤ)
56		simpr 477	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝑗 ∈ ℕ₀ ∧ (#‘𝐹) ∈ ℕ) → (#‘𝐹) ∈ ℕ)
57	56	adantl 482	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝑆 ∈ ℤ ∧ (𝑗 ∈ ℕ₀ ∧ (#‘𝐹) ∈ ℕ)) → (#‘𝐹) ∈ ℕ)
58	55, 57	jca 554	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝑆 ∈ ℤ ∧ (𝑗 ∈ ℕ₀ ∧ (#‘𝐹) ∈ ℕ)) → ((𝑗 + 𝑆) ∈ ℤ ∧ (#‘𝐹) ∈ ℕ))
59	58	expcom 451	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑗 ∈ ℕ₀ ∧ (#‘𝐹) ∈ ℕ) → (𝑆 ∈ ℤ → ((𝑗 + 𝑆) ∈ ℤ ∧ (#‘𝐹) ∈ ℕ)))
60	59	3adant3 1081	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑗 ∈ ℕ₀ ∧ (#‘𝐹) ∈ ℕ ∧ 𝑗 < (#‘𝐹)) → (𝑆 ∈ ℤ → ((𝑗 + 𝑆) ∈ ℤ ∧ (#‘𝐹) ∈ ℕ)))
61	50, 60	sylbi 207	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑗 ∈ (0..^(#‘𝐹)) → (𝑆 ∈ ℤ → ((𝑗 + 𝑆) ∈ ℤ ∧ (#‘𝐹) ∈ ℕ)))
62	61	com12 32	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑆 ∈ ℤ → (𝑗 ∈ (0..^(#‘𝐹)) → ((𝑗 + 𝑆) ∈ ℤ ∧ (#‘𝐹) ∈ ℕ)))
63	62	3ad2ant3 1084	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝐺 = (𝐹 cyclShift 𝑆) ∧ 𝐹 ∈ Word 𝐴 ∧ 𝑆 ∈ ℤ) → (𝑗 ∈ (0..^(#‘𝐹)) → ((𝑗 + 𝑆) ∈ ℤ ∧ (#‘𝐹) ∈ ℕ)))
64	63	adantld 483	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝐺 = (𝐹 cyclShift 𝑆) ∧ 𝐹 ∈ Word 𝐴 ∧ 𝑆 ∈ ℤ) → ((𝑖 ∈ (0..^(#‘𝐹)) ∧ 𝑗 ∈ (0..^(#‘𝐹))) → ((𝑗 + 𝑆) ∈ ℤ ∧ (#‘𝐹) ∈ ℕ)))
65	64	imp 445	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝐺 = (𝐹 cyclShift 𝑆) ∧ 𝐹 ∈ Word 𝐴 ∧ 𝑆 ∈ ℤ) ∧ (𝑖 ∈ (0..^(#‘𝐹)) ∧ 𝑗 ∈ (0..^(#‘𝐹)))) → ((𝑗 + 𝑆) ∈ ℤ ∧ (#‘𝐹) ∈ ℕ))
66		zmodfzo 12693	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑗 + 𝑆) ∈ ℤ ∧ (#‘𝐹) ∈ ℕ) → ((𝑗 + 𝑆) mod (#‘𝐹)) ∈ (0..^(#‘𝐹)))
67	65, 66	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ (((𝐺 = (𝐹 cyclShift 𝑆) ∧ 𝐹 ∈ Word 𝐴 ∧ 𝑆 ∈ ℤ) ∧ (𝑖 ∈ (0..^(#‘𝐹)) ∧ 𝑗 ∈ (0..^(#‘𝐹)))) → ((𝑗 + 𝑆) mod (#‘𝐹)) ∈ (0..^(#‘𝐹)))
68		fveq2 6191	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑥 = ((𝑖 + 𝑆) mod (#‘𝐹)) → (𝐹‘𝑥) = (𝐹‘((𝑖 + 𝑆) mod (#‘𝐹))))
69	68	eqeq1d 2624	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑥 = ((𝑖 + 𝑆) mod (#‘𝐹)) → ((𝐹‘𝑥) = (𝐹‘𝑦) ↔ (𝐹‘((𝑖 + 𝑆) mod (#‘𝐹))) = (𝐹‘𝑦)))
70		eqeq1 2626	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑥 = ((𝑖 + 𝑆) mod (#‘𝐹)) → (𝑥 = 𝑦 ↔ ((𝑖 + 𝑆) mod (#‘𝐹)) = 𝑦))
71	69, 70	imbi12d 334	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥 = ((𝑖 + 𝑆) mod (#‘𝐹)) → (((𝐹‘𝑥) = (𝐹‘𝑦) → 𝑥 = 𝑦) ↔ ((𝐹‘((𝑖 + 𝑆) mod (#‘𝐹))) = (𝐹‘𝑦) → ((𝑖 + 𝑆) mod (#‘𝐹)) = 𝑦)))
72		fveq2 6191	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑦 = ((𝑗 + 𝑆) mod (#‘𝐹)) → (𝐹‘𝑦) = (𝐹‘((𝑗 + 𝑆) mod (#‘𝐹))))
73	72	eqeq2d 2632	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑦 = ((𝑗 + 𝑆) mod (#‘𝐹)) → ((𝐹‘((𝑖 + 𝑆) mod (#‘𝐹))) = (𝐹‘𝑦) ↔ (𝐹‘((𝑖 + 𝑆) mod (#‘𝐹))) = (𝐹‘((𝑗 + 𝑆) mod (#‘𝐹)))))
74		eqeq2 2633	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑦 = ((𝑗 + 𝑆) mod (#‘𝐹)) → (((𝑖 + 𝑆) mod (#‘𝐹)) = 𝑦 ↔ ((𝑖 + 𝑆) mod (#‘𝐹)) = ((𝑗 + 𝑆) mod (#‘𝐹))))
75	73, 74	imbi12d 334	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑦 = ((𝑗 + 𝑆) mod (#‘𝐹)) → (((𝐹‘((𝑖 + 𝑆) mod (#‘𝐹))) = (𝐹‘𝑦) → ((𝑖 + 𝑆) mod (#‘𝐹)) = 𝑦) ↔ ((𝐹‘((𝑖 + 𝑆) mod (#‘𝐹))) = (𝐹‘((𝑗 + 𝑆) mod (#‘𝐹))) → ((𝑖 + 𝑆) mod (#‘𝐹)) = ((𝑗 + 𝑆) mod (#‘𝐹)))))
76	71, 75	rspc2v 3322	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝑖 + 𝑆) mod (#‘𝐹)) ∈ (0..^(#‘𝐹)) ∧ ((𝑗 + 𝑆) mod (#‘𝐹)) ∈ (0..^(#‘𝐹))) → (∀𝑥 ∈ (0..^(#‘𝐹))∀𝑦 ∈ (0..^(#‘𝐹))((𝐹‘𝑥) = (𝐹‘𝑦) → 𝑥 = 𝑦) → ((𝐹‘((𝑖 + 𝑆) mod (#‘𝐹))) = (𝐹‘((𝑗 + 𝑆) mod (#‘𝐹))) → ((𝑖 + 𝑆) mod (#‘𝐹)) = ((𝑗 + 𝑆) mod (#‘𝐹)))))
77	49, 67, 76	syl2anc 693	. . . . . . . . . . . . . . . 16 ⊢ (((𝐺 = (𝐹 cyclShift 𝑆) ∧ 𝐹 ∈ Word 𝐴 ∧ 𝑆 ∈ ℤ) ∧ (𝑖 ∈ (0..^(#‘𝐹)) ∧ 𝑗 ∈ (0..^(#‘𝐹)))) → (∀𝑥 ∈ (0..^(#‘𝐹))∀𝑦 ∈ (0..^(#‘𝐹))((𝐹‘𝑥) = (𝐹‘𝑦) → 𝑥 = 𝑦) → ((𝐹‘((𝑖 + 𝑆) mod (#‘𝐹))) = (𝐹‘((𝑗 + 𝑆) mod (#‘𝐹))) → ((𝑖 + 𝑆) mod (#‘𝐹)) = ((𝑗 + 𝑆) mod (#‘𝐹)))))
78		simpr 477	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝐺 = (𝐹 cyclShift 𝑆) ∧ 𝐹 ∈ Word 𝐴 ∧ 𝑆 ∈ ℤ) ∧ (𝑖 ∈ (0..^(#‘𝐹)) ∧ 𝑗 ∈ (0..^(#‘𝐹)))) ∧ ((𝐹‘((𝑖 + 𝑆) mod (#‘𝐹))) = (𝐹‘((𝑗 + 𝑆) mod (#‘𝐹))) → ((𝑖 + 𝑆) mod (#‘𝐹)) = ((𝑗 + 𝑆) mod (#‘𝐹)))) → ((𝐹‘((𝑖 + 𝑆) mod (#‘𝐹))) = (𝐹‘((𝑗 + 𝑆) mod (#‘𝐹))) → ((𝑖 + 𝑆) mod (#‘𝐹)) = ((𝑗 + 𝑆) mod (#‘𝐹))))
79		addmodlteq 12745	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝑖 ∈ (0..^(#‘𝐹)) ∧ 𝑗 ∈ (0..^(#‘𝐹)) ∧ 𝑆 ∈ ℤ) → (((𝑖 + 𝑆) mod (#‘𝐹)) = ((𝑗 + 𝑆) mod (#‘𝐹)) ↔ 𝑖 = 𝑗))
80	79	3expa 1265	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝑖 ∈ (0..^(#‘𝐹)) ∧ 𝑗 ∈ (0..^(#‘𝐹))) ∧ 𝑆 ∈ ℤ) → (((𝑖 + 𝑆) mod (#‘𝐹)) = ((𝑗 + 𝑆) mod (#‘𝐹)) ↔ 𝑖 = 𝑗))
81	80	ancoms 469	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑆 ∈ ℤ ∧ (𝑖 ∈ (0..^(#‘𝐹)) ∧ 𝑗 ∈ (0..^(#‘𝐹)))) → (((𝑖 + 𝑆) mod (#‘𝐹)) = ((𝑗 + 𝑆) mod (#‘𝐹)) ↔ 𝑖 = 𝑗))
82	81	bicomd 213	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑆 ∈ ℤ ∧ (𝑖 ∈ (0..^(#‘𝐹)) ∧ 𝑗 ∈ (0..^(#‘𝐹)))) → (𝑖 = 𝑗 ↔ ((𝑖 + 𝑆) mod (#‘𝐹)) = ((𝑗 + 𝑆) mod (#‘𝐹))))
83	82	ex 450	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑆 ∈ ℤ → ((𝑖 ∈ (0..^(#‘𝐹)) ∧ 𝑗 ∈ (0..^(#‘𝐹))) → (𝑖 = 𝑗 ↔ ((𝑖 + 𝑆) mod (#‘𝐹)) = ((𝑗 + 𝑆) mod (#‘𝐹)))))
84	83	3ad2ant3 1084	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝐺 = (𝐹 cyclShift 𝑆) ∧ 𝐹 ∈ Word 𝐴 ∧ 𝑆 ∈ ℤ) → ((𝑖 ∈ (0..^(#‘𝐹)) ∧ 𝑗 ∈ (0..^(#‘𝐹))) → (𝑖 = 𝑗 ↔ ((𝑖 + 𝑆) mod (#‘𝐹)) = ((𝑗 + 𝑆) mod (#‘𝐹)))))
85	84	imp 445	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝐺 = (𝐹 cyclShift 𝑆) ∧ 𝐹 ∈ Word 𝐴 ∧ 𝑆 ∈ ℤ) ∧ (𝑖 ∈ (0..^(#‘𝐹)) ∧ 𝑗 ∈ (0..^(#‘𝐹)))) → (𝑖 = 𝑗 ↔ ((𝑖 + 𝑆) mod (#‘𝐹)) = ((𝑗 + 𝑆) mod (#‘𝐹))))
86	85	adantr 481	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝐺 = (𝐹 cyclShift 𝑆) ∧ 𝐹 ∈ Word 𝐴 ∧ 𝑆 ∈ ℤ) ∧ (𝑖 ∈ (0..^(#‘𝐹)) ∧ 𝑗 ∈ (0..^(#‘𝐹)))) ∧ ((𝐹‘((𝑖 + 𝑆) mod (#‘𝐹))) = (𝐹‘((𝑗 + 𝑆) mod (#‘𝐹))) → ((𝑖 + 𝑆) mod (#‘𝐹)) = ((𝑗 + 𝑆) mod (#‘𝐹)))) → (𝑖 = 𝑗 ↔ ((𝑖 + 𝑆) mod (#‘𝐹)) = ((𝑗 + 𝑆) mod (#‘𝐹))))
87	78, 86	sylibrd 249	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝐺 = (𝐹 cyclShift 𝑆) ∧ 𝐹 ∈ Word 𝐴 ∧ 𝑆 ∈ ℤ) ∧ (𝑖 ∈ (0..^(#‘𝐹)) ∧ 𝑗 ∈ (0..^(#‘𝐹)))) ∧ ((𝐹‘((𝑖 + 𝑆) mod (#‘𝐹))) = (𝐹‘((𝑗 + 𝑆) mod (#‘𝐹))) → ((𝑖 + 𝑆) mod (#‘𝐹)) = ((𝑗 + 𝑆) mod (#‘𝐹)))) → ((𝐹‘((𝑖 + 𝑆) mod (#‘𝐹))) = (𝐹‘((𝑗 + 𝑆) mod (#‘𝐹))) → 𝑖 = 𝑗))
88	87	ex 450	. . . . . . . . . . . . . . . 16 ⊢ (((𝐺 = (𝐹 cyclShift 𝑆) ∧ 𝐹 ∈ Word 𝐴 ∧ 𝑆 ∈ ℤ) ∧ (𝑖 ∈ (0..^(#‘𝐹)) ∧ 𝑗 ∈ (0..^(#‘𝐹)))) → (((𝐹‘((𝑖 + 𝑆) mod (#‘𝐹))) = (𝐹‘((𝑗 + 𝑆) mod (#‘𝐹))) → ((𝑖 + 𝑆) mod (#‘𝐹)) = ((𝑗 + 𝑆) mod (#‘𝐹))) → ((𝐹‘((𝑖 + 𝑆) mod (#‘𝐹))) = (𝐹‘((𝑗 + 𝑆) mod (#‘𝐹))) → 𝑖 = 𝑗)))
89	77, 88	syld 47	. . . . . . . . . . . . . . 15 ⊢ (((𝐺 = (𝐹 cyclShift 𝑆) ∧ 𝐹 ∈ Word 𝐴 ∧ 𝑆 ∈ ℤ) ∧ (𝑖 ∈ (0..^(#‘𝐹)) ∧ 𝑗 ∈ (0..^(#‘𝐹)))) → (∀𝑥 ∈ (0..^(#‘𝐹))∀𝑦 ∈ (0..^(#‘𝐹))((𝐹‘𝑥) = (𝐹‘𝑦) → 𝑥 = 𝑦) → ((𝐹‘((𝑖 + 𝑆) mod (#‘𝐹))) = (𝐹‘((𝑗 + 𝑆) mod (#‘𝐹))) → 𝑖 = 𝑗)))
90	89	impancom 456	. . . . . . . . . . . . . 14 ⊢ (((𝐺 = (𝐹 cyclShift 𝑆) ∧ 𝐹 ∈ Word 𝐴 ∧ 𝑆 ∈ ℤ) ∧ ∀𝑥 ∈ (0..^(#‘𝐹))∀𝑦 ∈ (0..^(#‘𝐹))((𝐹‘𝑥) = (𝐹‘𝑦) → 𝑥 = 𝑦)) → ((𝑖 ∈ (0..^(#‘𝐹)) ∧ 𝑗 ∈ (0..^(#‘𝐹))) → ((𝐹‘((𝑖 + 𝑆) mod (#‘𝐹))) = (𝐹‘((𝑗 + 𝑆) mod (#‘𝐹))) → 𝑖 = 𝑗)))
91	90	imp 445	. . . . . . . . . . . . 13 ⊢ ((((𝐺 = (𝐹 cyclShift 𝑆) ∧ 𝐹 ∈ Word 𝐴 ∧ 𝑆 ∈ ℤ) ∧ ∀𝑥 ∈ (0..^(#‘𝐹))∀𝑦 ∈ (0..^(#‘𝐹))((𝐹‘𝑥) = (𝐹‘𝑦) → 𝑥 = 𝑦)) ∧ (𝑖 ∈ (0..^(#‘𝐹)) ∧ 𝑗 ∈ (0..^(#‘𝐹)))) → ((𝐹‘((𝑖 + 𝑆) mod (#‘𝐹))) = (𝐹‘((𝑗 + 𝑆) mod (#‘𝐹))) → 𝑖 = 𝑗))
92	31, 91	sylbid 230	. . . . . . . . . . . 12 ⊢ ((((𝐺 = (𝐹 cyclShift 𝑆) ∧ 𝐹 ∈ Word 𝐴 ∧ 𝑆 ∈ ℤ) ∧ ∀𝑥 ∈ (0..^(#‘𝐹))∀𝑦 ∈ (0..^(#‘𝐹))((𝐹‘𝑥) = (𝐹‘𝑦) → 𝑥 = 𝑦)) ∧ (𝑖 ∈ (0..^(#‘𝐹)) ∧ 𝑗 ∈ (0..^(#‘𝐹)))) → ((𝐺‘𝑖) = (𝐺‘𝑗) → 𝑖 = 𝑗))
93	92	ralrimivva 2971	. . . . . . . . . . 11 ⊢ (((𝐺 = (𝐹 cyclShift 𝑆) ∧ 𝐹 ∈ Word 𝐴 ∧ 𝑆 ∈ ℤ) ∧ ∀𝑥 ∈ (0..^(#‘𝐹))∀𝑦 ∈ (0..^(#‘𝐹))((𝐹‘𝑥) = (𝐹‘𝑦) → 𝑥 = 𝑦)) → ∀𝑖 ∈ (0..^(#‘𝐹))∀𝑗 ∈ (0..^(#‘𝐹))((𝐺‘𝑖) = (𝐺‘𝑗) → 𝑖 = 𝑗))
94	93	3exp1 1283	. . . . . . . . . 10 ⊢ (𝐺 = (𝐹 cyclShift 𝑆) → (𝐹 ∈ Word 𝐴 → (𝑆 ∈ ℤ → (∀𝑥 ∈ (0..^(#‘𝐹))∀𝑦 ∈ (0..^(#‘𝐹))((𝐹‘𝑥) = (𝐹‘𝑦) → 𝑥 = 𝑦) → ∀𝑖 ∈ (0..^(#‘𝐹))∀𝑗 ∈ (0..^(#‘𝐹))((𝐺‘𝑖) = (𝐺‘𝑗) → 𝑖 = 𝑗)))))
95	94	com14 96	. . . . . . . . 9 ⊢ (∀𝑥 ∈ (0..^(#‘𝐹))∀𝑦 ∈ (0..^(#‘𝐹))((𝐹‘𝑥) = (𝐹‘𝑦) → 𝑥 = 𝑦) → (𝐹 ∈ Word 𝐴 → (𝑆 ∈ ℤ → (𝐺 = (𝐹 cyclShift 𝑆) → ∀𝑖 ∈ (0..^(#‘𝐹))∀𝑗 ∈ (0..^(#‘𝐹))((𝐺‘𝑖) = (𝐺‘𝑗) → 𝑖 = 𝑗)))))
96	95	adantl 482	. . . . . . . 8 ⊢ ((𝐹:(0..^(#‘𝐹))⟶𝐴 ∧ ∀𝑥 ∈ (0..^(#‘𝐹))∀𝑦 ∈ (0..^(#‘𝐹))((𝐹‘𝑥) = (𝐹‘𝑦) → 𝑥 = 𝑦)) → (𝐹 ∈ Word 𝐴 → (𝑆 ∈ ℤ → (𝐺 = (𝐹 cyclShift 𝑆) → ∀𝑖 ∈ (0..^(#‘𝐹))∀𝑗 ∈ (0..^(#‘𝐹))((𝐺‘𝑖) = (𝐺‘𝑗) → 𝑖 = 𝑗)))))
97	10, 96	sylbi 207	. . . . . . 7 ⊢ (𝐹:(0..^(#‘𝐹))–1-1→𝐴 → (𝐹 ∈ Word 𝐴 → (𝑆 ∈ ℤ → (𝐺 = (𝐹 cyclShift 𝑆) → ∀𝑖 ∈ (0..^(#‘𝐹))∀𝑗 ∈ (0..^(#‘𝐹))((𝐺‘𝑖) = (𝐺‘𝑗) → 𝑖 = 𝑗)))))
98	97	3imp1 1280	. . . . . 6 ⊢ (((𝐹:(0..^(#‘𝐹))–1-1→𝐴 ∧ 𝐹 ∈ Word 𝐴 ∧ 𝑆 ∈ ℤ) ∧ 𝐺 = (𝐹 cyclShift 𝑆)) → ∀𝑖 ∈ (0..^(#‘𝐹))∀𝑗 ∈ (0..^(#‘𝐹))((𝐺‘𝑖) = (𝐺‘𝑗) → 𝑖 = 𝑗))
99	9, 98	jca 554	. . . . 5 ⊢ (((𝐹:(0..^(#‘𝐹))–1-1→𝐴 ∧ 𝐹 ∈ Word 𝐴 ∧ 𝑆 ∈ ℤ) ∧ 𝐺 = (𝐹 cyclShift 𝑆)) → (𝐺:(0..^(#‘𝐹))⟶𝐴 ∧ ∀𝑖 ∈ (0..^(#‘𝐹))∀𝑗 ∈ (0..^(#‘𝐹))((𝐺‘𝑖) = (𝐺‘𝑗) → 𝑖 = 𝑗)))
100	99	3exp1 1283	. . . 4 ⊢ (𝐹:(0..^(#‘𝐹))–1-1→𝐴 → (𝐹 ∈ Word 𝐴 → (𝑆 ∈ ℤ → (𝐺 = (𝐹 cyclShift 𝑆) → (𝐺:(0..^(#‘𝐹))⟶𝐴 ∧ ∀𝑖 ∈ (0..^(#‘𝐹))∀𝑗 ∈ (0..^(#‘𝐹))((𝐺‘𝑖) = (𝐺‘𝑗) → 𝑖 = 𝑗))))))
101	3, 100	mpd 15	. . 3 ⊢ (𝐹:(0..^(#‘𝐹))–1-1→𝐴 → (𝑆 ∈ ℤ → (𝐺 = (𝐹 cyclShift 𝑆) → (𝐺:(0..^(#‘𝐹))⟶𝐴 ∧ ∀𝑖 ∈ (0..^(#‘𝐹))∀𝑗 ∈ (0..^(#‘𝐹))((𝐺‘𝑖) = (𝐺‘𝑗) → 𝑖 = 𝑗)))))
102	101	3imp 1256	. 2 ⊢ ((𝐹:(0..^(#‘𝐹))–1-1→𝐴 ∧ 𝑆 ∈ ℤ ∧ 𝐺 = (𝐹 cyclShift 𝑆)) → (𝐺:(0..^(#‘𝐹))⟶𝐴 ∧ ∀𝑖 ∈ (0..^(#‘𝐹))∀𝑗 ∈ (0..^(#‘𝐹))((𝐺‘𝑖) = (𝐺‘𝑗) → 𝑖 = 𝑗)))
103		dff13 6512	. 2 ⊢ (𝐺:(0..^(#‘𝐹))–1-1→𝐴 ↔ (𝐺:(0..^(#‘𝐹))⟶𝐴 ∧ ∀𝑖 ∈ (0..^(#‘𝐹))∀𝑗 ∈ (0..^(#‘𝐹))((𝐺‘𝑖) = (𝐺‘𝑗) → 𝑖 = 𝑗)))
104	102, 103	sylibr 224	1 ⊢ ((𝐹:(0..^(#‘𝐹))–1-1→𝐴 ∧ 𝑆 ∈ ℤ ∧ 𝐺 = (𝐹 cyclShift 𝑆)) → 𝐺:(0..^(#‘𝐹))–1-1→𝐴)

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 196 ∧ wa 384 ∧ w3a 1037 = wceq 1483 ∈ wcel 1990 ∀wral 2912 class class class wbr 4653 ⟶wf 5884 –1-1→wf1 5885 ‘cfv 5888 (class class class)co 6650 0cc0 9936 + caddc 9939 < clt 10074 ℕcn 11020 ℕ₀cn0 11292 ℤcz 11377 ..^cfzo 12465 mod cmo 12668 #chash 13117 Word cword 13291 cyclShift ccsh 13534

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1722 ax-4 1737 ax-5 1839 ax-6 1888 ax-7 1935 ax-8 1992 ax-9 1999 ax-10 2019 ax-11 2034 ax-12 2047 ax-13 2246 ax-ext 2602 ax-rep 4771 ax-sep 4781 ax-nul 4789 ax-pow 4843 ax-pr 4906 ax-un 6949 ax-cnex 9992 ax-resscn 9993 ax-1cn 9994 ax-icn 9995 ax-addcl 9996 ax-addrcl 9997 ax-mulcl 9998 ax-mulrcl 9999 ax-mulcom 10000 ax-addass 10001 ax-mulass 10002 ax-distr 10003 ax-i2m1 10004 ax-1ne0 10005 ax-1rid 10006 ax-rnegex 10007 ax-rrecex 10008 ax-cnre 10009 ax-pre-lttri 10010 ax-pre-lttrn 10011 ax-pre-ltadd 10012 ax-pre-mulgt0 10013 ax-pre-sup 10014

This theorem depends on definitions: df-bi 197 df-or 385 df-an 386 df-3or 1038 df-3an 1039 df-tru 1486 df-ex 1705 df-nf 1710 df-sb 1881 df-eu 2474 df-mo 2475 df-clab 2609 df-cleq 2615 df-clel 2618 df-nfc 2753 df-ne 2795 df-nel 2898 df-ral 2917 df-rex 2918 df-reu 2919 df-rmo 2920 df-rab 2921 df-v 3202 df-sbc 3436 df-csb 3534 df-dif 3577 df-un 3579 df-in 3581 df-ss 3588 df-pss 3590 df-nul 3916 df-if 4087 df-pw 4160 df-sn 4178 df-pr 4180 df-tp 4182 df-op 4184 df-uni 4437 df-int 4476 df-iun 4522 df-br 4654 df-opab 4713 df-mpt 4730 df-tr 4753 df-id 5024 df-eprel 5029 df-po 5035 df-so 5036 df-fr 5073 df-we 5075 df-xp 5120 df-rel 5121 df-cnv 5122 df-co 5123 df-dm 5124 df-rn 5125 df-res 5126 df-ima 5127 df-pred 5680 df-ord 5726 df-on 5727 df-lim 5728 df-suc 5729 df-iota 5851 df-fun 5890 df-fn 5891 df-f 5892 df-f1 5893 df-fo 5894 df-f1o 5895 df-fv 5896 df-riota 6611 df-ov 6653 df-oprab 6654 df-mpt2 6655 df-om 7066 df-1st 7168 df-2nd 7169 df-wrecs 7407 df-recs 7468 df-rdg 7506 df-1o 7560 df-oadd 7564 df-er 7742 df-en 7956 df-dom 7957 df-sdom 7958 df-fin 7959 df-sup 8348 df-inf 8349 df-card 8765 df-pnf 10076 df-mnf 10077 df-xr 10078 df-ltxr 10079 df-le 10080 df-sub 10268 df-neg 10269 df-div 10685 df-nn 11021 df-2 11079 df-n0 11293 df-z 11378 df-uz 11688 df-rp 11833 df-fz 12327 df-fzo 12466 df-fl 12593 df-mod 12669 df-hash 13118 df-word 13299 df-concat 13301 df-substr 13303 df-csh 13535

This theorem is referenced by: cshinj 13557

W3C validator