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 14726

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 12514	. . . . . . . . . 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 1128	. . . . . . 7 ⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉) ∧ (𝑁 ∈ ℤ ∧ 𝑀 ∈ ℤ)) → (𝑈 ∈ Word 𝑉 ∧ (𝑀 − 𝑁) ∈ ℤ ∧ 𝑀 ∈ ℤ))
9	8	adantr 480	. . . . . 6 ⊢ ((((𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉) ∧ (𝑁 ∈ ℤ ∧ 𝑀 ∈ ℤ)) ∧ (𝑊 cyclShift 𝑁) = (𝑈 cyclShift 𝑀)) → (𝑈 ∈ Word 𝑉 ∧ (𝑀 − 𝑁) ∈ ℤ ∧ 𝑀 ∈ ℤ))
10		3cshw 14725	. . . . . 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 2737	. . . . . . . 8 ⊢ ((((𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉) ∧ (𝑁 ∈ ℤ ∧ 𝑀 ∈ ℤ)) ∧ (𝑊 cyclShift 𝑁) = (𝑈 cyclShift 𝑀)) → (𝑈 cyclShift 𝑀) = (𝑊 cyclShift 𝑁))
20		cshwleneq 14724	. . . . . . . 8 ⊢ (((𝑈 ∈ Word 𝑉 ∧ 𝑊 ∈ Word 𝑉) ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝑈 cyclShift 𝑀) = (𝑊 cyclShift 𝑁)) → (♯‘𝑈) = (♯‘𝑊))
21	14, 17, 19, 20	syl3anc 1373	. . . . . . 7 ⊢ ((((𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉) ∧ (𝑁 ∈ ℤ ∧ 𝑀 ∈ ℤ)) ∧ (𝑊 cyclShift 𝑁) = (𝑈 cyclShift 𝑀)) → (♯‘𝑈) = (♯‘𝑊))
22	21	oveq1d 7361	. . . . . 6 ⊢ ((((𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉) ∧ (𝑁 ∈ ℤ ∧ 𝑀 ∈ ℤ)) ∧ (𝑊 cyclShift 𝑁) = (𝑈 cyclShift 𝑀)) → ((♯‘𝑈) − 𝑀) = ((♯‘𝑊) − 𝑀))
23	22	oveq2d 7362	. . . . 5 ⊢ ((((𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉) ∧ (𝑁 ∈ ℤ ∧ 𝑀 ∈ ℤ)) ∧ (𝑊 cyclShift 𝑁) = (𝑈 cyclShift 𝑀)) → (((𝑈 cyclShift 𝑀) cyclShift (𝑀 − 𝑁)) cyclShift ((♯‘𝑈) − 𝑀)) = (((𝑈 cyclShift 𝑀) cyclShift (𝑀 − 𝑁)) cyclShift ((♯‘𝑊) − 𝑀)))
24	11, 23	eqtrd 2766	. . . 4 ⊢ ((((𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉) ∧ (𝑁 ∈ ℤ ∧ 𝑀 ∈ ℤ)) ∧ (𝑊 cyclShift 𝑁) = (𝑈 cyclShift 𝑀)) → (𝑈 cyclShift (𝑀 − 𝑁)) = (((𝑈 cyclShift 𝑀) cyclShift (𝑀 − 𝑁)) cyclShift ((♯‘𝑊) − 𝑀)))
25	19	oveq1d 7361	. . . . . 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 1128	. . . . . . . 8 ⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉) ∧ (𝑁 ∈ ℤ ∧ 𝑀 ∈ ℤ)) → (𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ ℤ ∧ (𝑀 − 𝑁) ∈ ℤ))
31	30	adantr 480	. . . . . . 7 ⊢ ((((𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉) ∧ (𝑁 ∈ ℤ ∧ 𝑀 ∈ ℤ)) ∧ (𝑊 cyclShift 𝑁) = (𝑈 cyclShift 𝑀)) → (𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ ℤ ∧ (𝑀 − 𝑁) ∈ ℤ))
32		2cshw 14720	. . . . . . 7 ⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ ℤ ∧ (𝑀 − 𝑁) ∈ ℤ) → ((𝑊 cyclShift 𝑁) cyclShift (𝑀 − 𝑁)) = (𝑊 cyclShift (𝑁 + (𝑀 − 𝑁))))
33	31, 32	syl 17	. . . . . 6 ⊢ ((((𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉) ∧ (𝑁 ∈ ℤ ∧ 𝑀 ∈ ℤ)) ∧ (𝑊 cyclShift 𝑁) = (𝑈 cyclShift 𝑀)) → ((𝑊 cyclShift 𝑁) cyclShift (𝑀 − 𝑁)) = (𝑊 cyclShift (𝑁 + (𝑀 − 𝑁))))
34		zcn 12473	. . . . . . . . . . 11 ⊢ (𝑁 ∈ ℤ → 𝑁 ∈ ℂ)
35		zcn 12473	. . . . . . . . . . 11 ⊢ (𝑀 ∈ ℤ → 𝑀 ∈ ℂ)
36	34, 35	anim12i 613	. . . . . . . . . 10 ⊢ ((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℤ) → (𝑁 ∈ ℂ ∧ 𝑀 ∈ ℂ))
37	36	adantl 481	. . . . . . . . 9 ⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉) ∧ (𝑁 ∈ ℤ ∧ 𝑀 ∈ ℤ)) → (𝑁 ∈ ℂ ∧ 𝑀 ∈ ℂ))
38	37	adantr 480	. . . . . . . 8 ⊢ ((((𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉) ∧ (𝑁 ∈ ℤ ∧ 𝑀 ∈ ℤ)) ∧ (𝑊 cyclShift 𝑁) = (𝑈 cyclShift 𝑀)) → (𝑁 ∈ ℂ ∧ 𝑀 ∈ ℂ))
39		pncan3 11368	. . . . . . . 8 ⊢ ((𝑁 ∈ ℂ ∧ 𝑀 ∈ ℂ) → (𝑁 + (𝑀 − 𝑁)) = 𝑀)
40	38, 39	syl 17	. . . . . . 7 ⊢ ((((𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉) ∧ (𝑁 ∈ ℤ ∧ 𝑀 ∈ ℤ)) ∧ (𝑊 cyclShift 𝑁) = (𝑈 cyclShift 𝑀)) → (𝑁 + (𝑀 − 𝑁)) = 𝑀)
41	40	oveq2d 7362	. . . . . 6 ⊢ ((((𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉) ∧ (𝑁 ∈ ℤ ∧ 𝑀 ∈ ℤ)) ∧ (𝑊 cyclShift 𝑁) = (𝑈 cyclShift 𝑀)) → (𝑊 cyclShift (𝑁 + (𝑀 − 𝑁))) = (𝑊 cyclShift 𝑀))
42	25, 33, 41	3eqtrd 2770	. . . . 5 ⊢ ((((𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉) ∧ (𝑁 ∈ ℤ ∧ 𝑀 ∈ ℤ)) ∧ (𝑊 cyclShift 𝑁) = (𝑈 cyclShift 𝑀)) → ((𝑈 cyclShift 𝑀) cyclShift (𝑀 − 𝑁)) = (𝑊 cyclShift 𝑀))
43	42	oveq1d 7361	. . . 4 ⊢ ((((𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉) ∧ (𝑁 ∈ ℤ ∧ 𝑀 ∈ ℤ)) ∧ (𝑊 cyclShift 𝑁) = (𝑈 cyclShift 𝑀)) → (((𝑈 cyclShift 𝑀) cyclShift (𝑀 − 𝑁)) cyclShift ((♯‘𝑊) − 𝑀)) = ((𝑊 cyclShift 𝑀) cyclShift ((♯‘𝑊) − 𝑀)))
44		lencl 14440	. . . . . . . . . 10 ⊢ (𝑊 ∈ Word 𝑉 → (♯‘𝑊) ∈ ℕ₀)
45	44	nn0zd 12494	. . . . . . . . 9 ⊢ (𝑊 ∈ Word 𝑉 → (♯‘𝑊) ∈ ℤ)
46	45	adantr 480	. . . . . . . 8 ⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉) → (♯‘𝑊) ∈ ℤ)
47		zsubcl 12514	. . . . . . . 8 ⊢ (((♯‘𝑊) ∈ ℤ ∧ 𝑀 ∈ ℤ) → ((♯‘𝑊) − 𝑀) ∈ ℤ)
48	46, 6, 47	syl2an 596	. . . . . . 7 ⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉) ∧ (𝑁 ∈ ℤ ∧ 𝑀 ∈ ℤ)) → ((♯‘𝑊) − 𝑀) ∈ ℤ)
49	27, 7, 48	3jca 1128	. . . . . 6 ⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉) ∧ (𝑁 ∈ ℤ ∧ 𝑀 ∈ ℤ)) → (𝑊 ∈ Word 𝑉 ∧ 𝑀 ∈ ℤ ∧ ((♯‘𝑊) − 𝑀) ∈ ℤ))
50	49	adantr 480	. . . . 5 ⊢ ((((𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉) ∧ (𝑁 ∈ ℤ ∧ 𝑀 ∈ ℤ)) ∧ (𝑊 cyclShift 𝑁) = (𝑈 cyclShift 𝑀)) → (𝑊 ∈ Word 𝑉 ∧ 𝑀 ∈ ℤ ∧ ((♯‘𝑊) − 𝑀) ∈ ℤ))
51		2cshw 14720	. . . . 5 ⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑀 ∈ ℤ ∧ ((♯‘𝑊) − 𝑀) ∈ ℤ) → ((𝑊 cyclShift 𝑀) cyclShift ((♯‘𝑊) − 𝑀)) = (𝑊 cyclShift (𝑀 + ((♯‘𝑊) − 𝑀))))
52	50, 51	syl 17	. . . 4 ⊢ ((((𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉) ∧ (𝑁 ∈ ℤ ∧ 𝑀 ∈ ℤ)) ∧ (𝑊 cyclShift 𝑁) = (𝑈 cyclShift 𝑀)) → ((𝑊 cyclShift 𝑀) cyclShift ((♯‘𝑊) − 𝑀)) = (𝑊 cyclShift (𝑀 + ((♯‘𝑊) − 𝑀))))
53	24, 43, 52	3eqtrd 2770	. . 3 ⊢ ((((𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉) ∧ (𝑁 ∈ ℤ ∧ 𝑀 ∈ ℤ)) ∧ (𝑊 cyclShift 𝑁) = (𝑈 cyclShift 𝑀)) → (𝑈 cyclShift (𝑀 − 𝑁)) = (𝑊 cyclShift (𝑀 + ((♯‘𝑊) − 𝑀))))
54	44	nn0cnd 12444	. . . . . . . . 9 ⊢ (𝑊 ∈ Word 𝑉 → (♯‘𝑊) ∈ ℂ)
55	54	adantr 480	. . . . . . . 8 ⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉) → (♯‘𝑊) ∈ ℂ)
56	35	adantl 481	. . . . . . . 8 ⊢ ((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℤ) → 𝑀 ∈ ℂ)
57	55, 56	anim12i 613	. . . . . . 7 ⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉) ∧ (𝑁 ∈ ℤ ∧ 𝑀 ∈ ℤ)) → ((♯‘𝑊) ∈ ℂ ∧ 𝑀 ∈ ℂ))
58	57	ancomd 461	. . . . . 6 ⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉) ∧ (𝑁 ∈ ℤ ∧ 𝑀 ∈ ℤ)) → (𝑀 ∈ ℂ ∧ (♯‘𝑊) ∈ ℂ))
59	58	adantr 480	. . . . 5 ⊢ ((((𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉) ∧ (𝑁 ∈ ℤ ∧ 𝑀 ∈ ℤ)) ∧ (𝑊 cyclShift 𝑁) = (𝑈 cyclShift 𝑀)) → (𝑀 ∈ ℂ ∧ (♯‘𝑊) ∈ ℂ))
60		pncan3 11368	. . . . 5 ⊢ ((𝑀 ∈ ℂ ∧ (♯‘𝑊) ∈ ℂ) → (𝑀 + ((♯‘𝑊) − 𝑀)) = (♯‘𝑊))
61	59, 60	syl 17	. . . 4 ⊢ ((((𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉) ∧ (𝑁 ∈ ℤ ∧ 𝑀 ∈ ℤ)) ∧ (𝑊 cyclShift 𝑁) = (𝑈 cyclShift 𝑀)) → (𝑀 + ((♯‘𝑊) − 𝑀)) = (♯‘𝑊))
62	61	oveq2d 7362	. . 3 ⊢ ((((𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉) ∧ (𝑁 ∈ ℤ ∧ 𝑀 ∈ ℤ)) ∧ (𝑊 cyclShift 𝑁) = (𝑈 cyclShift 𝑀)) → (𝑊 cyclShift (𝑀 + ((♯‘𝑊) − 𝑀))) = (𝑊 cyclShift (♯‘𝑊)))
63		cshwn 14704	. . . . 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 2770	. 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 1086 = wceq 1541 ∈ wcel 2111 ‘cfv 6481 (class class class)co 7346 ℂcc 11004 + caddc 11009 − cmin 11344 ℤcz 12468 ♯chash 14237 Word cword 14420 cyclShift ccsh 14695

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1796 ax-4 1810 ax-5 1911 ax-6 1968 ax-7 2009 ax-8 2113 ax-9 2121 ax-10 2144 ax-11 2160 ax-12 2180 ax-ext 2703 ax-rep 5215 ax-sep 5232 ax-nul 5242 ax-pow 5301 ax-pr 5368 ax-un 7668 ax-cnex 11062 ax-resscn 11063 ax-1cn 11064 ax-icn 11065 ax-addcl 11066 ax-addrcl 11067 ax-mulcl 11068 ax-mulrcl 11069 ax-mulcom 11070 ax-addass 11071 ax-mulass 11072 ax-distr 11073 ax-i2m1 11074 ax-1ne0 11075 ax-1rid 11076 ax-rnegex 11077 ax-rrecex 11078 ax-cnre 11079 ax-pre-lttri 11080 ax-pre-lttrn 11081 ax-pre-ltadd 11082 ax-pre-mulgt0 11083 ax-pre-sup 11084

This theorem depends on definitions: df-bi 207 df-an 396 df-or 848 df-3or 1087 df-3an 1088 df-tru 1544 df-fal 1554 df-ex 1781 df-nf 1785 df-sb 2068 df-mo 2535 df-eu 2564 df-clab 2710 df-cleq 2723 df-clel 2806 df-nfc 2881 df-ne 2929 df-nel 3033 df-ral 3048 df-rex 3057 df-rmo 3346 df-reu 3347 df-rab 3396 df-v 3438 df-sbc 3737 df-csb 3846 df-dif 3900 df-un 3902 df-in 3904 df-ss 3914 df-pss 3917 df-nul 4281 df-if 4473 df-pw 4549 df-sn 4574 df-pr 4576 df-op 4580 df-uni 4857 df-int 4896 df-iun 4941 df-br 5090 df-opab 5152 df-mpt 5171 df-tr 5197 df-id 5509 df-eprel 5514 df-po 5522 df-so 5523 df-fr 5567 df-we 5569 df-xp 5620 df-rel 5621 df-cnv 5622 df-co 5623 df-dm 5624 df-rn 5625 df-res 5626 df-ima 5627 df-pred 6248 df-ord 6309 df-on 6310 df-lim 6311 df-suc 6312 df-iota 6437 df-fun 6483 df-fn 6484 df-f 6485 df-f1 6486 df-fo 6487 df-f1o 6488 df-fv 6489 df-riota 7303 df-ov 7349 df-oprab 7350 df-mpo 7351 df-om 7797 df-1st 7921 df-2nd 7922 df-frecs 8211 df-wrecs 8242 df-recs 8291 df-rdg 8329 df-1o 8385 df-er 8622 df-en 8870 df-dom 8871 df-sdom 8872 df-fin 8873 df-sup 9326 df-inf 9327 df-card 9832 df-pnf 11148 df-mnf 11149 df-xr 11150 df-ltxr 11151 df-le 11152 df-sub 11346 df-neg 11347 df-div 11775 df-nn 12126 df-2 12188 df-n0 12382 df-z 12469 df-uz 12733 df-rp 12891 df-fz 13408 df-fzo 13555 df-fl 13696 df-mod 13774 df-hash 14238 df-word 14421 df-concat 14478 df-substr 14549 df-pfx 14579 df-csh 14696

This theorem is referenced by: cshweqdifid 14727

W3C validator