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 14756

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 12547	. . . . . . . . . 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 14755	. . . . . 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 14754	. . . . . . . 8 ⊢ (((𝑈 ∈ Word 𝑉 ∧ 𝑊 ∈ Word 𝑉) ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝑈 cyclShift 𝑀) = (𝑊 cyclShift 𝑁)) → (♯‘𝑈) = (♯‘𝑊))
21	14, 17, 19, 20	syl3anc 1374	. . . . . . 7 ⊢ ((((𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉) ∧ (𝑁 ∈ ℤ ∧ 𝑀 ∈ ℤ)) ∧ (𝑊 cyclShift 𝑁) = (𝑈 cyclShift 𝑀)) → (♯‘𝑈) = (♯‘𝑊))
22	21	oveq1d 7385	. . . . . 6 ⊢ ((((𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉) ∧ (𝑁 ∈ ℤ ∧ 𝑀 ∈ ℤ)) ∧ (𝑊 cyclShift 𝑁) = (𝑈 cyclShift 𝑀)) → ((♯‘𝑈) − 𝑀) = ((♯‘𝑊) − 𝑀))
23	22	oveq2d 7386	. . . . 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 7385	. . . . . 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 14750	. . . . . . 7 ⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ ℤ ∧ (𝑀 − 𝑁) ∈ ℤ) → ((𝑊 cyclShift 𝑁) cyclShift (𝑀 − 𝑁)) = (𝑊 cyclShift (𝑁 + (𝑀 − 𝑁))))
33	31, 32	syl 17	. . . . . 6 ⊢ ((((𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉) ∧ (𝑁 ∈ ℤ ∧ 𝑀 ∈ ℤ)) ∧ (𝑊 cyclShift 𝑁) = (𝑈 cyclShift 𝑀)) → ((𝑊 cyclShift 𝑁) cyclShift (𝑀 − 𝑁)) = (𝑊 cyclShift (𝑁 + (𝑀 − 𝑁))))
34		zcn 12507	. . . . . . . . . . 11 ⊢ (𝑁 ∈ ℤ → 𝑁 ∈ ℂ)
35		zcn 12507	. . . . . . . . . . 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 11402	. . . . . . . 8 ⊢ ((𝑁 ∈ ℂ ∧ 𝑀 ∈ ℂ) → (𝑁 + (𝑀 − 𝑁)) = 𝑀)
40	38, 39	syl 17	. . . . . . 7 ⊢ ((((𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉) ∧ (𝑁 ∈ ℤ ∧ 𝑀 ∈ ℤ)) ∧ (𝑊 cyclShift 𝑁) = (𝑈 cyclShift 𝑀)) → (𝑁 + (𝑀 − 𝑁)) = 𝑀)
41	40	oveq2d 7386	. . . . . 6 ⊢ ((((𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉) ∧ (𝑁 ∈ ℤ ∧ 𝑀 ∈ ℤ)) ∧ (𝑊 cyclShift 𝑁) = (𝑈 cyclShift 𝑀)) → (𝑊 cyclShift (𝑁 + (𝑀 − 𝑁))) = (𝑊 cyclShift 𝑀))
42	25, 33, 41	3eqtrd 2776	. . . . 5 ⊢ ((((𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉) ∧ (𝑁 ∈ ℤ ∧ 𝑀 ∈ ℤ)) ∧ (𝑊 cyclShift 𝑁) = (𝑈 cyclShift 𝑀)) → ((𝑈 cyclShift 𝑀) cyclShift (𝑀 − 𝑁)) = (𝑊 cyclShift 𝑀))
43	42	oveq1d 7385	. . . 4 ⊢ ((((𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉) ∧ (𝑁 ∈ ℤ ∧ 𝑀 ∈ ℤ)) ∧ (𝑊 cyclShift 𝑁) = (𝑈 cyclShift 𝑀)) → (((𝑈 cyclShift 𝑀) cyclShift (𝑀 − 𝑁)) cyclShift ((♯‘𝑊) − 𝑀)) = ((𝑊 cyclShift 𝑀) cyclShift ((♯‘𝑊) − 𝑀)))
44		lencl 14470	. . . . . . . . . 10 ⊢ (𝑊 ∈ Word 𝑉 → (♯‘𝑊) ∈ ℕ₀)
45	44	nn0zd 12527	. . . . . . . . 9 ⊢ (𝑊 ∈ Word 𝑉 → (♯‘𝑊) ∈ ℤ)
46	45	adantr 480	. . . . . . . 8 ⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉) → (♯‘𝑊) ∈ ℤ)
47		zsubcl 12547	. . . . . . . 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 14750	. . . . 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 12478	. . . . . . . . 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 11402	. . . . 5 ⊢ ((𝑀 ∈ ℂ ∧ (♯‘𝑊) ∈ ℂ) → (𝑀 + ((♯‘𝑊) − 𝑀)) = (♯‘𝑊))
61	59, 60	syl 17	. . . 4 ⊢ ((((𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉) ∧ (𝑁 ∈ ℤ ∧ 𝑀 ∈ ℤ)) ∧ (𝑊 cyclShift 𝑁) = (𝑈 cyclShift 𝑀)) → (𝑀 + ((♯‘𝑊) − 𝑀)) = (♯‘𝑊))
62	61	oveq2d 7386	. . 3 ⊢ ((((𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉) ∧ (𝑁 ∈ ℤ ∧ 𝑀 ∈ ℤ)) ∧ (𝑊 cyclShift 𝑁) = (𝑈 cyclShift 𝑀)) → (𝑊 cyclShift (𝑀 + ((♯‘𝑊) − 𝑀))) = (𝑊 cyclShift (♯‘𝑊)))
63		cshwn 14734	. . . . 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 6502 (class class class)co 7370 ℂcc 11038 + caddc 11043 − cmin 11378 ℤcz 12502 ♯chash 14267 Word cword 14450 cyclShift ccsh 14725

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 5226 ax-sep 5245 ax-nul 5255 ax-pow 5314 ax-pr 5381 ax-un 7692 ax-cnex 11096 ax-resscn 11097 ax-1cn 11098 ax-icn 11099 ax-addcl 11100 ax-addrcl 11101 ax-mulcl 11102 ax-mulrcl 11103 ax-mulcom 11104 ax-addass 11105 ax-mulass 11106 ax-distr 11107 ax-i2m1 11108 ax-1ne0 11109 ax-1rid 11110 ax-rnegex 11111 ax-rrecex 11112 ax-cnre 11113 ax-pre-lttri 11114 ax-pre-lttrn 11115 ax-pre-ltadd 11116 ax-pre-mulgt0 11117 ax-pre-sup 11118

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 3352 df-reu 3353 df-rab 3402 df-v 3444 df-sbc 3743 df-csb 3852 df-dif 3906 df-un 3908 df-in 3910 df-ss 3920 df-pss 3923 df-nul 4288 df-if 4482 df-pw 4558 df-sn 4583 df-pr 4585 df-op 4589 df-uni 4866 df-int 4905 df-iun 4950 df-br 5101 df-opab 5163 df-mpt 5182 df-tr 5208 df-id 5529 df-eprel 5534 df-po 5542 df-so 5543 df-fr 5587 df-we 5589 df-xp 5640 df-rel 5641 df-cnv 5642 df-co 5643 df-dm 5644 df-rn 5645 df-res 5646 df-ima 5647 df-pred 6269 df-ord 6330 df-on 6331 df-lim 6332 df-suc 6333 df-iota 6458 df-fun 6504 df-fn 6505 df-f 6506 df-f1 6507 df-fo 6508 df-f1o 6509 df-fv 6510 df-riota 7327 df-ov 7373 df-oprab 7374 df-mpo 7375 df-om 7821 df-1st 7945 df-2nd 7946 df-frecs 8235 df-wrecs 8266 df-recs 8315 df-rdg 8353 df-1o 8409 df-er 8647 df-en 8898 df-dom 8899 df-sdom 8900 df-fin 8901 df-sup 9359 df-inf 9360 df-card 9865 df-pnf 11182 df-mnf 11183 df-xr 11184 df-ltxr 11185 df-le 11186 df-sub 11380 df-neg 11381 df-div 11809 df-nn 12160 df-2 12222 df-n0 12416 df-z 12503 df-uz 12766 df-rp 12920 df-fz 13438 df-fzo 13585 df-fl 13726 df-mod 13804 df-hash 14268 df-word 14451 df-concat 14508 df-substr 14579 df-pfx 14609 df-csh 14726

This theorem is referenced by: cshweqdifid 14757

W3C validator