cshweqdif2 - Metamath Proof Explorer

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

Theorem cshweqdif2 14776

Description: If cyclically shifting two words (of the same length) results in the same word, cyclically shifting one of the words by the difference of the numbers of shifts results in the other word. (Contributed by AV, 21-Apr-2018.) (Revised by AV, 6-Jun-2018.) (Revised by AV, 1-Nov-2018.)

**Assertion**
Ref	Expression
cshweqdif2	⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉) ∧ (𝑁 ∈ ℤ ∧ 𝑀 ∈ ℤ)) → ((𝑊 cyclShift 𝑁) = (𝑈 cyclShift 𝑀) → (𝑈 cyclShift (𝑀 − 𝑁)) = 𝑊))

**Proof of Theorem cshweqdif2**
Step	Hyp	Ref	Expression
1		simpr 484	. . . . . . . . 9 ⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉) → 𝑈 ∈ Word 𝑉)
2	1	adantr 480	. . . . . . . 8 ⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉) ∧ (𝑁 ∈ ℤ ∧ 𝑀 ∈ ℤ)) → 𝑈 ∈ Word 𝑉)
3		zsubcl 12564	. . . . . . . . . 10 ⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑀 − 𝑁) ∈ ℤ)
4	3	ancoms 458	. . . . . . . . 9 ⊢ ((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℤ) → (𝑀 − 𝑁) ∈ ℤ)
5	4	adantl 481	. . . . . . . 8 ⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉) ∧ (𝑁 ∈ ℤ ∧ 𝑀 ∈ ℤ)) → (𝑀 − 𝑁) ∈ ℤ)
6		simpr 484	. . . . . . . . 9 ⊢ ((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℤ) → 𝑀 ∈ ℤ)
7	6	adantl 481	. . . . . . . 8 ⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉) ∧ (𝑁 ∈ ℤ ∧ 𝑀 ∈ ℤ)) → 𝑀 ∈ ℤ)
8	2, 5, 7	3jca 1129	. . . . . . 7 ⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉) ∧ (𝑁 ∈ ℤ ∧ 𝑀 ∈ ℤ)) → (𝑈 ∈ Word 𝑉 ∧ (𝑀 − 𝑁) ∈ ℤ ∧ 𝑀 ∈ ℤ))
9	8	adantr 480	. . . . . 6 ⊢ ((((𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉) ∧ (𝑁 ∈ ℤ ∧ 𝑀 ∈ ℤ)) ∧ (𝑊 cyclShift 𝑁) = (𝑈 cyclShift 𝑀)) → (𝑈 ∈ Word 𝑉 ∧ (𝑀 − 𝑁) ∈ ℤ ∧ 𝑀 ∈ ℤ))
10		3cshw 14775	. . . . . 6 ⊢ ((𝑈 ∈ Word 𝑉 ∧ (𝑀 − 𝑁) ∈ ℤ ∧ 𝑀 ∈ ℤ) → (𝑈 cyclShift (𝑀 − 𝑁)) = (((𝑈 cyclShift 𝑀) cyclShift (𝑀 − 𝑁)) cyclShift ((♯‘𝑈) − 𝑀)))
11	9, 10	syl 17	. . . . 5 ⊢ ((((𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉) ∧ (𝑁 ∈ ℤ ∧ 𝑀 ∈ ℤ)) ∧ (𝑊 cyclShift 𝑁) = (𝑈 cyclShift 𝑀)) → (𝑈 cyclShift (𝑀 − 𝑁)) = (((𝑈 cyclShift 𝑀) cyclShift (𝑀 − 𝑁)) cyclShift ((♯‘𝑈) − 𝑀)))
12		simpl 482	. . . . . . . . . 10 ⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉) ∧ (𝑁 ∈ ℤ ∧ 𝑀 ∈ ℤ)) → (𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉))
13	12	ancomd 461	. . . . . . . . 9 ⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉) ∧ (𝑁 ∈ ℤ ∧ 𝑀 ∈ ℤ)) → (𝑈 ∈ Word 𝑉 ∧ 𝑊 ∈ Word 𝑉))
14	13	adantr 480	. . . . . . . 8 ⊢ ((((𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉) ∧ (𝑁 ∈ ℤ ∧ 𝑀 ∈ ℤ)) ∧ (𝑊 cyclShift 𝑁) = (𝑈 cyclShift 𝑀)) → (𝑈 ∈ Word 𝑉 ∧ 𝑊 ∈ Word 𝑉))
15		simpr 484	. . . . . . . . . 10 ⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉) ∧ (𝑁 ∈ ℤ ∧ 𝑀 ∈ ℤ)) → (𝑁 ∈ ℤ ∧ 𝑀 ∈ ℤ))
16	15	ancomd 461	. . . . . . . . 9 ⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉) ∧ (𝑁 ∈ ℤ ∧ 𝑀 ∈ ℤ)) → (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ))
17	16	adantr 480	. . . . . . . 8 ⊢ ((((𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉) ∧ (𝑁 ∈ ℤ ∧ 𝑀 ∈ ℤ)) ∧ (𝑊 cyclShift 𝑁) = (𝑈 cyclShift 𝑀)) → (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ))
18		simpr 484	. . . . . . . . 9 ⊢ ((((𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉) ∧ (𝑁 ∈ ℤ ∧ 𝑀 ∈ ℤ)) ∧ (𝑊 cyclShift 𝑁) = (𝑈 cyclShift 𝑀)) → (𝑊 cyclShift 𝑁) = (𝑈 cyclShift 𝑀))
19	18	eqcomd 2743	. . . . . . . 8 ⊢ ((((𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉) ∧ (𝑁 ∈ ℤ ∧ 𝑀 ∈ ℤ)) ∧ (𝑊 cyclShift 𝑁) = (𝑈 cyclShift 𝑀)) → (𝑈 cyclShift 𝑀) = (𝑊 cyclShift 𝑁))
20		cshwleneq 14774	. . . . . . . 8 ⊢ (((𝑈 ∈ Word 𝑉 ∧ 𝑊 ∈ Word 𝑉) ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝑈 cyclShift 𝑀) = (𝑊 cyclShift 𝑁)) → (♯‘𝑈) = (♯‘𝑊))
21	14, 17, 19, 20	syl3anc 1374	. . . . . . 7 ⊢ ((((𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉) ∧ (𝑁 ∈ ℤ ∧ 𝑀 ∈ ℤ)) ∧ (𝑊 cyclShift 𝑁) = (𝑈 cyclShift 𝑀)) → (♯‘𝑈) = (♯‘𝑊))
22	21	oveq1d 7377	. . . . . 6 ⊢ ((((𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉) ∧ (𝑁 ∈ ℤ ∧ 𝑀 ∈ ℤ)) ∧ (𝑊 cyclShift 𝑁) = (𝑈 cyclShift 𝑀)) → ((♯‘𝑈) − 𝑀) = ((♯‘𝑊) − 𝑀))
23	22	oveq2d 7378	. . . . 5 ⊢ ((((𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉) ∧ (𝑁 ∈ ℤ ∧ 𝑀 ∈ ℤ)) ∧ (𝑊 cyclShift 𝑁) = (𝑈 cyclShift 𝑀)) → (((𝑈 cyclShift 𝑀) cyclShift (𝑀 − 𝑁)) cyclShift ((♯‘𝑈) − 𝑀)) = (((𝑈 cyclShift 𝑀) cyclShift (𝑀 − 𝑁)) cyclShift ((♯‘𝑊) − 𝑀)))
24	11, 23	eqtrd 2772	. . . 4 ⊢ ((((𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉) ∧ (𝑁 ∈ ℤ ∧ 𝑀 ∈ ℤ)) ∧ (𝑊 cyclShift 𝑁) = (𝑈 cyclShift 𝑀)) → (𝑈 cyclShift (𝑀 − 𝑁)) = (((𝑈 cyclShift 𝑀) cyclShift (𝑀 − 𝑁)) cyclShift ((♯‘𝑊) − 𝑀)))
25	19	oveq1d 7377	. . . . . 6 ⊢ ((((𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉) ∧ (𝑁 ∈ ℤ ∧ 𝑀 ∈ ℤ)) ∧ (𝑊 cyclShift 𝑁) = (𝑈 cyclShift 𝑀)) → ((𝑈 cyclShift 𝑀) cyclShift (𝑀 − 𝑁)) = ((𝑊 cyclShift 𝑁) cyclShift (𝑀 − 𝑁)))
26		simpl 482	. . . . . . . . . 10 ⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉) → 𝑊 ∈ Word 𝑉)
27	26	adantr 480	. . . . . . . . 9 ⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉) ∧ (𝑁 ∈ ℤ ∧ 𝑀 ∈ ℤ)) → 𝑊 ∈ Word 𝑉)
28		simpl 482	. . . . . . . . . 10 ⊢ ((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℤ) → 𝑁 ∈ ℤ)
29	28	adantl 481	. . . . . . . . 9 ⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉) ∧ (𝑁 ∈ ℤ ∧ 𝑀 ∈ ℤ)) → 𝑁 ∈ ℤ)
30	27, 29, 5	3jca 1129	. . . . . . . 8 ⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉) ∧ (𝑁 ∈ ℤ ∧ 𝑀 ∈ ℤ)) → (𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ ℤ ∧ (𝑀 − 𝑁) ∈ ℤ))
31	30	adantr 480	. . . . . . 7 ⊢ ((((𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉) ∧ (𝑁 ∈ ℤ ∧ 𝑀 ∈ ℤ)) ∧ (𝑊 cyclShift 𝑁) = (𝑈 cyclShift 𝑀)) → (𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ ℤ ∧ (𝑀 − 𝑁) ∈ ℤ))
32		2cshw 14770	. . . . . . 7 ⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ ℤ ∧ (𝑀 − 𝑁) ∈ ℤ) → ((𝑊 cyclShift 𝑁) cyclShift (𝑀 − 𝑁)) = (𝑊 cyclShift (𝑁 + (𝑀 − 𝑁))))
33	31, 32	syl 17	. . . . . 6 ⊢ ((((𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉) ∧ (𝑁 ∈ ℤ ∧ 𝑀 ∈ ℤ)) ∧ (𝑊 cyclShift 𝑁) = (𝑈 cyclShift 𝑀)) → ((𝑊 cyclShift 𝑁) cyclShift (𝑀 − 𝑁)) = (𝑊 cyclShift (𝑁 + (𝑀 − 𝑁))))
34		zcn 12524	. . . . . . . . . . 11 ⊢ (𝑁 ∈ ℤ → 𝑁 ∈ ℂ)
35		zcn 12524	. . . . . . . . . . 11 ⊢ (𝑀 ∈ ℤ → 𝑀 ∈ ℂ)
36	34, 35	anim12i 614	. . . . . . . . . 10 ⊢ ((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℤ) → (𝑁 ∈ ℂ ∧ 𝑀 ∈ ℂ))
37	36	adantl 481	. . . . . . . . 9 ⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉) ∧ (𝑁 ∈ ℤ ∧ 𝑀 ∈ ℤ)) → (𝑁 ∈ ℂ ∧ 𝑀 ∈ ℂ))
38	37	adantr 480	. . . . . . . 8 ⊢ ((((𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉) ∧ (𝑁 ∈ ℤ ∧ 𝑀 ∈ ℤ)) ∧ (𝑊 cyclShift 𝑁) = (𝑈 cyclShift 𝑀)) → (𝑁 ∈ ℂ ∧ 𝑀 ∈ ℂ))
39		pncan3 11396	. . . . . . . 8 ⊢ ((𝑁 ∈ ℂ ∧ 𝑀 ∈ ℂ) → (𝑁 + (𝑀 − 𝑁)) = 𝑀)
40	38, 39	syl 17	. . . . . . 7 ⊢ ((((𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉) ∧ (𝑁 ∈ ℤ ∧ 𝑀 ∈ ℤ)) ∧ (𝑊 cyclShift 𝑁) = (𝑈 cyclShift 𝑀)) → (𝑁 + (𝑀 − 𝑁)) = 𝑀)
41	40	oveq2d 7378	. . . . . 6 ⊢ ((((𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉) ∧ (𝑁 ∈ ℤ ∧ 𝑀 ∈ ℤ)) ∧ (𝑊 cyclShift 𝑁) = (𝑈 cyclShift 𝑀)) → (𝑊 cyclShift (𝑁 + (𝑀 − 𝑁))) = (𝑊 cyclShift 𝑀))
42	25, 33, 41	3eqtrd 2776	. . . . 5 ⊢ ((((𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉) ∧ (𝑁 ∈ ℤ ∧ 𝑀 ∈ ℤ)) ∧ (𝑊 cyclShift 𝑁) = (𝑈 cyclShift 𝑀)) → ((𝑈 cyclShift 𝑀) cyclShift (𝑀 − 𝑁)) = (𝑊 cyclShift 𝑀))
43	42	oveq1d 7377	. . . 4 ⊢ ((((𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉) ∧ (𝑁 ∈ ℤ ∧ 𝑀 ∈ ℤ)) ∧ (𝑊 cyclShift 𝑁) = (𝑈 cyclShift 𝑀)) → (((𝑈 cyclShift 𝑀) cyclShift (𝑀 − 𝑁)) cyclShift ((♯‘𝑊) − 𝑀)) = ((𝑊 cyclShift 𝑀) cyclShift ((♯‘𝑊) − 𝑀)))
44		lencl 14490	. . . . . . . . . 10 ⊢ (𝑊 ∈ Word 𝑉 → (♯‘𝑊) ∈ ℕ₀)
45	44	nn0zd 12544	. . . . . . . . 9 ⊢ (𝑊 ∈ Word 𝑉 → (♯‘𝑊) ∈ ℤ)
46	45	adantr 480	. . . . . . . 8 ⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉) → (♯‘𝑊) ∈ ℤ)
47		zsubcl 12564	. . . . . . . 8 ⊢ (((♯‘𝑊) ∈ ℤ ∧ 𝑀 ∈ ℤ) → ((♯‘𝑊) − 𝑀) ∈ ℤ)
48	46, 6, 47	syl2an 597	. . . . . . 7 ⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉) ∧ (𝑁 ∈ ℤ ∧ 𝑀 ∈ ℤ)) → ((♯‘𝑊) − 𝑀) ∈ ℤ)
49	27, 7, 48	3jca 1129	. . . . . 6 ⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉) ∧ (𝑁 ∈ ℤ ∧ 𝑀 ∈ ℤ)) → (𝑊 ∈ Word 𝑉 ∧ 𝑀 ∈ ℤ ∧ ((♯‘𝑊) − 𝑀) ∈ ℤ))
50	49	adantr 480	. . . . 5 ⊢ ((((𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉) ∧ (𝑁 ∈ ℤ ∧ 𝑀 ∈ ℤ)) ∧ (𝑊 cyclShift 𝑁) = (𝑈 cyclShift 𝑀)) → (𝑊 ∈ Word 𝑉 ∧ 𝑀 ∈ ℤ ∧ ((♯‘𝑊) − 𝑀) ∈ ℤ))
51		2cshw 14770	. . . . 5 ⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑀 ∈ ℤ ∧ ((♯‘𝑊) − 𝑀) ∈ ℤ) → ((𝑊 cyclShift 𝑀) cyclShift ((♯‘𝑊) − 𝑀)) = (𝑊 cyclShift (𝑀 + ((♯‘𝑊) − 𝑀))))
52	50, 51	syl 17	. . . 4 ⊢ ((((𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉) ∧ (𝑁 ∈ ℤ ∧ 𝑀 ∈ ℤ)) ∧ (𝑊 cyclShift 𝑁) = (𝑈 cyclShift 𝑀)) → ((𝑊 cyclShift 𝑀) cyclShift ((♯‘𝑊) − 𝑀)) = (𝑊 cyclShift (𝑀 + ((♯‘𝑊) − 𝑀))))
53	24, 43, 52	3eqtrd 2776	. . 3 ⊢ ((((𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉) ∧ (𝑁 ∈ ℤ ∧ 𝑀 ∈ ℤ)) ∧ (𝑊 cyclShift 𝑁) = (𝑈 cyclShift 𝑀)) → (𝑈 cyclShift (𝑀 − 𝑁)) = (𝑊 cyclShift (𝑀 + ((♯‘𝑊) − 𝑀))))
54	44	nn0cnd 12495	. . . . . . . . 9 ⊢ (𝑊 ∈ Word 𝑉 → (♯‘𝑊) ∈ ℂ)
55	54	adantr 480	. . . . . . . 8 ⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉) → (♯‘𝑊) ∈ ℂ)
56	35	adantl 481	. . . . . . . 8 ⊢ ((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℤ) → 𝑀 ∈ ℂ)
57	55, 56	anim12i 614	. . . . . . 7 ⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉) ∧ (𝑁 ∈ ℤ ∧ 𝑀 ∈ ℤ)) → ((♯‘𝑊) ∈ ℂ ∧ 𝑀 ∈ ℂ))
58	57	ancomd 461	. . . . . 6 ⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉) ∧ (𝑁 ∈ ℤ ∧ 𝑀 ∈ ℤ)) → (𝑀 ∈ ℂ ∧ (♯‘𝑊) ∈ ℂ))
59	58	adantr 480	. . . . 5 ⊢ ((((𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉) ∧ (𝑁 ∈ ℤ ∧ 𝑀 ∈ ℤ)) ∧ (𝑊 cyclShift 𝑁) = (𝑈 cyclShift 𝑀)) → (𝑀 ∈ ℂ ∧ (♯‘𝑊) ∈ ℂ))
60		pncan3 11396	. . . . 5 ⊢ ((𝑀 ∈ ℂ ∧ (♯‘𝑊) ∈ ℂ) → (𝑀 + ((♯‘𝑊) − 𝑀)) = (♯‘𝑊))
61	59, 60	syl 17	. . . 4 ⊢ ((((𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉) ∧ (𝑁 ∈ ℤ ∧ 𝑀 ∈ ℤ)) ∧ (𝑊 cyclShift 𝑁) = (𝑈 cyclShift 𝑀)) → (𝑀 + ((♯‘𝑊) − 𝑀)) = (♯‘𝑊))
62	61	oveq2d 7378	. . 3 ⊢ ((((𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉) ∧ (𝑁 ∈ ℤ ∧ 𝑀 ∈ ℤ)) ∧ (𝑊 cyclShift 𝑁) = (𝑈 cyclShift 𝑀)) → (𝑊 cyclShift (𝑀 + ((♯‘𝑊) − 𝑀))) = (𝑊 cyclShift (♯‘𝑊)))
63		cshwn 14754	. . . . 5 ⊢ (𝑊 ∈ Word 𝑉 → (𝑊 cyclShift (♯‘𝑊)) = 𝑊)
64	27, 63	syl 17	. . . 4 ⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉) ∧ (𝑁 ∈ ℤ ∧ 𝑀 ∈ ℤ)) → (𝑊 cyclShift (♯‘𝑊)) = 𝑊)
65	64	adantr 480	. . 3 ⊢ ((((𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉) ∧ (𝑁 ∈ ℤ ∧ 𝑀 ∈ ℤ)) ∧ (𝑊 cyclShift 𝑁) = (𝑈 cyclShift 𝑀)) → (𝑊 cyclShift (♯‘𝑊)) = 𝑊)
66	53, 62, 65	3eqtrd 2776	. 2 ⊢ ((((𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉) ∧ (𝑁 ∈ ℤ ∧ 𝑀 ∈ ℤ)) ∧ (𝑊 cyclShift 𝑁) = (𝑈 cyclShift 𝑀)) → (𝑈 cyclShift (𝑀 − 𝑁)) = 𝑊)
67	66	ex 412	1 ⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉) ∧ (𝑁 ∈ ℤ ∧ 𝑀 ∈ ℤ)) → ((𝑊 cyclShift 𝑁) = (𝑈 cyclShift 𝑀) → (𝑈 cyclShift (𝑀 − 𝑁)) = 𝑊))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ∧ wa 395 ∧ w3a 1087 = wceq 1542 ∈ wcel 2114 ‘cfv 6494 (class class class)co 7362 ℂcc 11031 + caddc 11036 − cmin 11372 ℤcz 12519 ♯chash 14287 Word cword 14470 cyclShift ccsh 14745

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1797 ax-4 1811 ax-5 1912 ax-6 1969 ax-7 2010 ax-8 2116 ax-9 2124 ax-10 2147 ax-11 2163 ax-12 2185 ax-ext 2709 ax-rep 5213 ax-sep 5232 ax-nul 5242 ax-pow 5304 ax-pr 5372 ax-un 7684 ax-cnex 11089 ax-resscn 11090 ax-1cn 11091 ax-icn 11092 ax-addcl 11093 ax-addrcl 11094 ax-mulcl 11095 ax-mulrcl 11096 ax-mulcom 11097 ax-addass 11098 ax-mulass 11099 ax-distr 11100 ax-i2m1 11101 ax-1ne0 11102 ax-1rid 11103 ax-rnegex 11104 ax-rrecex 11105 ax-cnre 11106 ax-pre-lttri 11107 ax-pre-lttrn 11108 ax-pre-ltadd 11109 ax-pre-mulgt0 11110 ax-pre-sup 11111

This theorem depends on definitions: df-bi 207 df-an 396 df-or 849 df-3or 1088 df-3an 1089 df-tru 1545 df-fal 1555 df-ex 1782 df-nf 1786 df-sb 2069 df-mo 2540 df-eu 2570 df-clab 2716 df-cleq 2729 df-clel 2812 df-nfc 2886 df-ne 2934 df-nel 3038 df-ral 3053 df-rex 3063 df-rmo 3343 df-reu 3344 df-rab 3391 df-v 3432 df-sbc 3730 df-csb 3839 df-dif 3893 df-un 3895 df-in 3897 df-ss 3907 df-pss 3910 df-nul 4275 df-if 4468 df-pw 4544 df-sn 4569 df-pr 4571 df-op 4575 df-uni 4852 df-int 4891 df-iun 4936 df-br 5087 df-opab 5149 df-mpt 5168 df-tr 5194 df-id 5521 df-eprel 5526 df-po 5534 df-so 5535 df-fr 5579 df-we 5581 df-xp 5632 df-rel 5633 df-cnv 5634 df-co 5635 df-dm 5636 df-rn 5637 df-res 5638 df-ima 5639 df-pred 6261 df-ord 6322 df-on 6323 df-lim 6324 df-suc 6325 df-iota 6450 df-fun 6496 df-fn 6497 df-f 6498 df-f1 6499 df-fo 6500 df-f1o 6501 df-fv 6502 df-riota 7319 df-ov 7365 df-oprab 7366 df-mpo 7367 df-om 7813 df-1st 7937 df-2nd 7938 df-frecs 8226 df-wrecs 8257 df-recs 8306 df-rdg 8344 df-1o 8400 df-er 8638 df-en 8889 df-dom 8890 df-sdom 8891 df-fin 8892 df-sup 9350 df-inf 9351 df-card 9858 df-pnf 11176 df-mnf 11177 df-xr 11178 df-ltxr 11179 df-le 11180 df-sub 11374 df-neg 11375 df-div 11803 df-nn 12170 df-2 12239 df-n0 12433 df-z 12520 df-uz 12784 df-rp 12938 df-fz 13457 df-fzo 13604 df-fl 13746 df-mod 13824 df-hash 14288 df-word 14471 df-concat 14528 df-substr 14599 df-pfx 14629 df-csh 14746

This theorem is referenced by: cshweqdifid 14777

W3C validator