Theorem cshw1s2 30906

Description: Cyclically shifting a length 2 word swaps its symbols. (Contributed by Thierry Arnoux, 19-Sep-2023.)

Assertion

Ref	Expression
cshw1s2	⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) → (⟨“𝐴𝐵”⟩ cyclShift 1) = ⟨“𝐵𝐴”⟩)

Proof of Theorem cshw1s2

Dummy variable 𝑖 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		s2len 14419	. . . . . . . 8 ⊢ (♯‘⟨“𝐴𝐵”⟩) = 2
2	1	oveq2i 7202	. . . . . . 7 ⊢ (1 mod (♯‘⟨“𝐴𝐵”⟩)) = (1 mod 2)
3		1re 10798	. . . . . . . 8 ⊢ 1 ∈ ℝ
4		2rp 12556	. . . . . . . 8 ⊢ 2 ∈ ℝ+
5		0le1 11320	. . . . . . . 8 ⊢ 0 ≤ 1
6		1lt2 11966	. . . . . . . 8 ⊢ 1 < 2
7		modid 13434	. . . . . . . 8 ⊢ (((1 ∈ ℝ ∧ 2 ∈ ℝ+) ∧ (0 ≤ 1 ∧ 1 < 2)) → (1 mod 2) = 1)
8	3, 4, 5, 6, 7	mp4an 693	. . . . . . 7 ⊢ (1 mod 2) = 1
9	2, 8	eqtri 2759	. . . . . 6 ⊢ (1 mod (♯‘⟨“𝐴𝐵”⟩)) = 1
10	9, 1	opeq12i 4775	. . . . 5 ⊢ ⟨(1 mod (♯‘⟨“𝐴𝐵”⟩)), (♯‘⟨“𝐴𝐵”⟩)⟩ = ⟨1, 2⟩
11	10	oveq2i 7202	. . . 4 ⊢ (⟨“𝐴𝐵”⟩ substr ⟨(1 mod (♯‘⟨“𝐴𝐵”⟩)), (♯‘⟨“𝐴𝐵”⟩)⟩) = (⟨“𝐴𝐵”⟩ substr ⟨1, 2⟩)
12		s2cl 14408	. . . . . 6 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) → ⟨“𝐴𝐵”⟩ ∈ Word 𝑉)
13		tpid2g 4673	. . . . . . . . 9 ⊢ (1 ∈ ℝ → 1 ∈ {0, 1, 2})
14	3, 13	ax-mp 5	. . . . . . . 8 ⊢ 1 ∈ {0, 1, 2}
15		fz0tp 13178	. . . . . . . 8 ⊢ (0...2) = {0, 1, 2}
16	14, 15	eleqtrri 2830	. . . . . . 7 ⊢ 1 ∈ (0...2)
17		tpid3g 4674	. . . . . . . . . 10 ⊢ (2 ∈ ℝ+ → 2 ∈ {0, 1, 2})
18	4, 17	ax-mp 5	. . . . . . . . 9 ⊢ 2 ∈ {0, 1, 2}
19	18, 15	eleqtrri 2830	. . . . . . . 8 ⊢ 2 ∈ (0...2)
20	1	oveq2i 7202	. . . . . . . 8 ⊢ (0...(♯‘⟨“𝐴𝐵”⟩)) = (0...2)
21	19, 20	eleqtrri 2830	. . . . . . 7 ⊢ 2 ∈ (0...(♯‘⟨“𝐴𝐵”⟩))
22		swrdval2 14176	. . . . . . 7 ⊢ ((⟨“𝐴𝐵”⟩ ∈ Word 𝑉 ∧ 1 ∈ (0...2) ∧ 2 ∈ (0...(♯‘⟨“𝐴𝐵”⟩))) → (⟨“𝐴𝐵”⟩ substr ⟨1, 2⟩) = (𝑖 ∈ (0..^(2 − 1)) ↦ (⟨“𝐴𝐵”⟩‘(𝑖 + 1))))
23	16, 21, 22	mp3an23 1455	. . . . . 6 ⊢ (⟨“𝐴𝐵”⟩ ∈ Word 𝑉 → (⟨“𝐴𝐵”⟩ substr ⟨1, 2⟩) = (𝑖 ∈ (0..^(2 − 1)) ↦ (⟨“𝐴𝐵”⟩‘(𝑖 + 1))))
24	12, 23	syl 17	. . . . 5 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) → (⟨“𝐴𝐵”⟩ substr ⟨1, 2⟩) = (𝑖 ∈ (0..^(2 − 1)) ↦ (⟨“𝐴𝐵”⟩‘(𝑖 + 1))))
25		2m1e1 11921	. . . . . . . . 9 ⊢ (2 − 1) = 1
26	25	oveq2i 7202	. . . . . . . 8 ⊢ (0..^(2 − 1)) = (0..^1)
27		fzo01 13289	. . . . . . . 8 ⊢ (0..^1) = {0}
28	26, 27	eqtri 2759	. . . . . . 7 ⊢ (0..^(2 − 1)) = {0}
29	28	a1i 11	. . . . . 6 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) → (0..^(2 − 1)) = {0})
30		simpr 488	. . . . . . . . . . . 12 ⊢ (((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) ∧ 𝑖 ∈ (0..^(2 − 1))) → 𝑖 ∈ (0..^(2 − 1)))
31	30, 28	eleqtrdi 2841	. . . . . . . . . . 11 ⊢ (((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) ∧ 𝑖 ∈ (0..^(2 − 1))) → 𝑖 ∈ {0})
32		elsni 4544	. . . . . . . . . . 11 ⊢ (𝑖 ∈ {0} → 𝑖 = 0)
33	31, 32	syl 17	. . . . . . . . . 10 ⊢ (((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) ∧ 𝑖 ∈ (0..^(2 − 1))) → 𝑖 = 0)
34	33	oveq1d 7206	. . . . . . . . 9 ⊢ (((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) ∧ 𝑖 ∈ (0..^(2 − 1))) → (𝑖 + 1) = (0 + 1))
35		0p1e1 11917	. . . . . . . . 9 ⊢ (0 + 1) = 1
36	34, 35	eqtrdi 2787	. . . . . . . 8 ⊢ (((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) ∧ 𝑖 ∈ (0..^(2 − 1))) → (𝑖 + 1) = 1)
37	36	fveq2d 6699	. . . . . . 7 ⊢ (((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) ∧ 𝑖 ∈ (0..^(2 − 1))) → (⟨“𝐴𝐵”⟩‘(𝑖 + 1)) = (⟨“𝐴𝐵”⟩‘1))
38		s2fv1 14418	. . . . . . . 8 ⊢ (𝐵 ∈ 𝑉 → (⟨“𝐴𝐵”⟩‘1) = 𝐵)
39	38	ad2antlr 727	. . . . . . 7 ⊢ (((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) ∧ 𝑖 ∈ (0..^(2 − 1))) → (⟨“𝐴𝐵”⟩‘1) = 𝐵)
40	37, 39	eqtrd 2771	. . . . . 6 ⊢ (((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) ∧ 𝑖 ∈ (0..^(2 − 1))) → (⟨“𝐴𝐵”⟩‘(𝑖 + 1)) = 𝐵)
41	29, 40	mpteq12dva 5124	. . . . 5 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) → (𝑖 ∈ (0..^(2 − 1)) ↦ (⟨“𝐴𝐵”⟩‘(𝑖 + 1))) = (𝑖 ∈ {0} ↦ 𝐵))
42		fconstmpt 5596	. . . . . 6 ⊢ ({0} × {𝐵}) = (𝑖 ∈ {0} ↦ 𝐵)
43		0nn0 12070	. . . . . . . 8 ⊢ 0 ∈ ℕ0
44		simpr 488	. . . . . . . 8 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) → 𝐵 ∈ 𝑉)
45		xpsng 6932	. . . . . . . 8 ⊢ ((0 ∈ ℕ0 ∧ 𝐵 ∈ 𝑉) → ({0} × {𝐵}) = {⟨0, 𝐵⟩})
46	43, 44, 45	sylancr 590	. . . . . . 7 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) → ({0} × {𝐵}) = {⟨0, 𝐵⟩})
47		s1val 14120	. . . . . . . 8 ⊢ (𝐵 ∈ 𝑉 → ⟨“𝐵”⟩ = {⟨0, 𝐵⟩})
48	47	adantl 485	. . . . . . 7 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) → ⟨“𝐵”⟩ = {⟨0, 𝐵⟩})
49	46, 48	eqtr4d 2774	. . . . . 6 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) → ({0} × {𝐵}) = ⟨“𝐵”⟩)
50	42, 49	eqtr3id 2785	. . . . 5 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) → (𝑖 ∈ {0} ↦ 𝐵) = ⟨“𝐵”⟩)
51	24, 41, 50	3eqtrd 2775	. . . 4 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) → (⟨“𝐴𝐵”⟩ substr ⟨1, 2⟩) = ⟨“𝐵”⟩)
52	11, 51	syl5eq 2783	. . 3 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) → (⟨“𝐴𝐵”⟩ substr ⟨(1 mod (♯‘⟨“𝐴𝐵”⟩)), (♯‘⟨“𝐴𝐵”⟩)⟩) = ⟨“𝐵”⟩)
53	9	oveq2i 7202	. . . 4 ⊢ (⟨“𝐴𝐵”⟩ prefix (1 mod (♯‘⟨“𝐴𝐵”⟩))) = (⟨“𝐴𝐵”⟩ prefix 1)
54		pfx1s2 30887	. . . 4 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) → (⟨“𝐴𝐵”⟩ prefix 1) = ⟨“𝐴”⟩)
55	53, 54	syl5eq 2783	. . 3 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) → (⟨“𝐴𝐵”⟩ prefix (1 mod (♯‘⟨“𝐴𝐵”⟩))) = ⟨“𝐴”⟩)
56	52, 55	oveq12d 7209	. 2 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) → ((⟨“𝐴𝐵”⟩ substr ⟨(1 mod (♯‘⟨“𝐴𝐵”⟩)), (♯‘⟨“𝐴𝐵”⟩)⟩) ++ (⟨“𝐴𝐵”⟩ prefix (1 mod (♯‘⟨“𝐴𝐵”⟩)))) = (⟨“𝐵”⟩ ++ ⟨“𝐴”⟩))
57		1z 12172	. . 3 ⊢ 1 ∈ ℤ
58		cshword 14321	. . 3 ⊢ ((⟨“𝐴𝐵”⟩ ∈ Word 𝑉 ∧ 1 ∈ ℤ) → (⟨“𝐴𝐵”⟩ cyclShift 1) = ((⟨“𝐴𝐵”⟩ substr ⟨(1 mod (♯‘⟨“𝐴𝐵”⟩)), (♯‘⟨“𝐴𝐵”⟩)⟩) ++ (⟨“𝐴𝐵”⟩ prefix (1 mod (♯‘⟨“𝐴𝐵”⟩)))))
59	12, 57, 58	sylancl 589	. 2 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) → (⟨“𝐴𝐵”⟩ cyclShift 1) = ((⟨“𝐴𝐵”⟩ substr ⟨(1 mod (♯‘⟨“𝐴𝐵”⟩)), (♯‘⟨“𝐴𝐵”⟩)⟩) ++ (⟨“𝐴𝐵”⟩ prefix (1 mod (♯‘⟨“𝐴𝐵”⟩)))))
60		df-s2 14378	. . 3 ⊢ ⟨“𝐵𝐴”⟩ = (⟨“𝐵”⟩ ++ ⟨“𝐴”⟩)
61	60	a1i 11	. 2 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) → ⟨“𝐵𝐴”⟩ = (⟨“𝐵”⟩ ++ ⟨“𝐴”⟩))
62	56, 59, 61	3eqtr4d 2781	1 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) → (⟨“𝐴𝐵”⟩ cyclShift 1) = ⟨“𝐵𝐴”⟩)

Syntax hints:   → wi 4   ∧ wa 399   = wceq 1543   ∈ wcel 2112  {csn 4527  {ctp 4531  ⟨cop 4533   class class class wbr 5039   ↦ cmpt 5120   × cxp 5534  ‘cfv 6358  (class class class)co 7191  ℝcr 10693  0cc0 10694  1c1 10695   + caddc 10697   < clt 10832   ≤ cle 10833   − cmin 11027  2c2 11850  ℕ₀cn0 12055  ℤcz 12141  ℝ⁺crp 12551  ...cfz 13060  ..^cfzo 13203   mod cmo 13407  ♯chash 13861  Word cword 14034   ++ cconcat 14090  ⟨“cs1 14117   substr csubstr 14170   prefix cpfx 14200   cyclShift ccsh 14318  ⟨“cs2 14371

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2018  ax-8 2114  ax-9 2122  ax-10 2143  ax-11 2160  ax-12 2177  ax-ext 2708  ax-rep 5164  ax-sep 5177  ax-nul 5184  ax-pow 5243  ax-pr 5307  ax-un 7501  ax-cnex 10750  ax-resscn 10751  ax-1cn 10752  ax-icn 10753  ax-addcl 10754  ax-addrcl 10755  ax-mulcl 10756  ax-mulrcl 10757  ax-mulcom 10758  ax-addass 10759  ax-mulass 10760  ax-distr 10761  ax-i2m1 10762  ax-1ne0 10763  ax-1rid 10764  ax-rnegex 10765  ax-rrecex 10766  ax-cnre 10767  ax-pre-lttri 10768  ax-pre-lttrn 10769  ax-pre-ltadd 10770  ax-pre-mulgt0 10771  ax-pre-sup 10772

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 848  df-3or 1090  df-3an 1091  df-tru 1546  df-fal 1556  df-ex 1788  df-nf 1792  df-sb 2073  df-mo 2539  df-eu 2568  df-clab 2715  df-cleq 2728  df-clel 2809  df-nfc 2879  df-ne 2933  df-nel 3037  df-ral 3056  df-rex 3057  df-reu 3058  df-rmo 3059  df-rab 3060  df-v 3400  df-sbc 3684  df-csb 3799  df-dif 3856  df-un 3858  df-in 3860  df-ss 3870  df-pss 3872  df-nul 4224  df-if 4426  df-pw 4501  df-sn 4528  df-pr 4530  df-tp 4532  df-op 4534  df-uni 4806  df-int 4846  df-iun 4892  df-br 5040  df-opab 5102  df-mpt 5121  df-tr 5147  df-id 5440  df-eprel 5445  df-po 5453  df-so 5454  df-fr 5494  df-we 5496  df-xp 5542  df-rel 5543  df-cnv 5544  df-co 5545  df-dm 5546  df-rn 5547  df-res 5548  df-ima 5549  df-pred 6140  df-ord 6194  df-on 6195  df-lim 6196  df-suc 6197  df-iota 6316  df-fun 6360  df-fn 6361  df-f 6362  df-f1 6363  df-fo 6364  df-f1o 6365  df-fv 6366  df-riota 7148  df-ov 7194  df-oprab 7195  df-mpo 7196  df-om 7623  df-1st 7739  df-2nd 7740  df-wrecs 8025  df-recs 8086  df-rdg 8124  df-1o 8180  df-er 8369  df-en 8605  df-dom 8606  df-sdom 8607  df-fin 8608  df-sup 9036  df-inf 9037  df-card 9520  df-pnf 10834  df-mnf 10835  df-xr 10836  df-ltxr 10837  df-le 10838  df-sub 11029  df-neg 11030  df-div 11455  df-nn 11796  df-2 11858  df-n0 12056  df-xnn0 12128  df-z 12142  df-uz 12404  df-rp 12552  df-fz 13061  df-fzo 13204  df-fl 13332  df-mod 13408  df-hash 13862  df-word 14035  df-concat 14091  df-s1 14118  df-substr 14171  df-pfx 14201  df-csh 14319  df-s2 14378

This theorem is referenced by:  cycpm2tr  31059