Theorem swrdccat3blem 11230

Description: Lemma for swrdccat3b 11231. (Contributed by AV, 30-May-2018.)

Hypothesis

Ref	Expression
swrdccatin2.l	⊢ 𝐿 = (♯‘𝐴)

Assertion

Ref	Expression
swrdccat3blem	⊢ ((((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ 𝑀 ∈ (0...(𝐿 + (♯‘𝐵)))) ∧ (𝐿 + (♯‘𝐵)) ≤ 𝐿) → if(𝐿 ≤ 𝑀, (𝐵 substr ⟨(𝑀 − 𝐿), (♯‘𝐵)⟩), ((𝐴 substr ⟨𝑀, 𝐿⟩) ++ 𝐵)) = (𝐴 substr ⟨𝑀, (𝐿 + (♯‘𝐵))⟩))

Proof of Theorem swrdccat3blem

Step	Hyp	Ref	Expression
1		lencl 11035	. . . . . . . 8 ⊢ (𝐵 ∈ Word 𝑉 → (♯‘𝐵) ∈ ℕ0)
2		nn0le0eq0 9358	. . . . . . . . 9 ⊢ ((♯‘𝐵) ∈ ℕ0 → ((♯‘𝐵) ≤ 0 ↔ (♯‘𝐵) = 0))
3	2	biimpd 144	. . . . . . . 8 ⊢ ((♯‘𝐵) ∈ ℕ0 → ((♯‘𝐵) ≤ 0 → (♯‘𝐵) = 0))
4	1, 3	syl 14	. . . . . . 7 ⊢ (𝐵 ∈ Word 𝑉 → ((♯‘𝐵) ≤ 0 → (♯‘𝐵) = 0))
5	4	adantl 277	. . . . . 6 ⊢ ((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) → ((♯‘𝐵) ≤ 0 → (♯‘𝐵) = 0))
6		wrdfin 11050	. . . . . . . . . . . 12 ⊢ (𝐵 ∈ Word 𝑉 → 𝐵 ∈ Fin)
7		fihasheq0 10975	. . . . . . . . . . . 12 ⊢ (𝐵 ∈ Fin → ((♯‘𝐵) = 0 ↔ 𝐵 = ∅))
8	6, 7	syl 14	. . . . . . . . . . 11 ⊢ (𝐵 ∈ Word 𝑉 → ((♯‘𝐵) = 0 ↔ 𝐵 = ∅))
9	8	biimpd 144	. . . . . . . . . 10 ⊢ (𝐵 ∈ Word 𝑉 → ((♯‘𝐵) = 0 → 𝐵 = ∅))
10	9	adantl 277	. . . . . . . . 9 ⊢ ((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) → ((♯‘𝐵) = 0 → 𝐵 = ∅))
11	10	imp 124	. . . . . . . 8 ⊢ (((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ (♯‘𝐵) = 0) → 𝐵 = ∅)
12		lencl 11035	. . . . . . . . . . . . . . . 16 ⊢ (𝐴 ∈ Word 𝑉 → (♯‘𝐴) ∈ ℕ0)
13		swrdccatin2.l	. . . . . . . . . . . . . . . . . . 19 ⊢ 𝐿 = (♯‘𝐴)
14	13	eqcomi 2211	. . . . . . . . . . . . . . . . . 18 ⊢ (♯‘𝐴) = 𝐿
15	14	eleq1i 2273	. . . . . . . . . . . . . . . . 17 ⊢ ((♯‘𝐴) ∈ ℕ0 ↔ 𝐿 ∈ ℕ0)
16		nn0re 9339	. . . . . . . . . . . . . . . . . 18 ⊢ (𝐿 ∈ ℕ0 → 𝐿 ∈ ℝ)
17		elfz2nn0 10269	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑀 ∈ (0...(𝐿 + 0)) ↔ (𝑀 ∈ ℕ0 ∧ (𝐿 + 0) ∈ ℕ0 ∧ 𝑀 ≤ (𝐿 + 0)))
18		recn 8093	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝐿 ∈ ℝ → 𝐿 ∈ ℂ)
19	18	addridd 8256	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝐿 ∈ ℝ → (𝐿 + 0) = 𝐿)
20	19	breq2d 4071	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝐿 ∈ ℝ → (𝑀 ≤ (𝐿 + 0) ↔ 𝑀 ≤ 𝐿))
21		nn0re 9339	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (𝑀 ∈ ℕ0 → 𝑀 ∈ ℝ)
22	21	anim1i 340	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((𝑀 ∈ ℕ0 ∧ 𝐿 ∈ ℝ) → (𝑀 ∈ ℝ ∧ 𝐿 ∈ ℝ))
23	22	ancoms 268	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((𝐿 ∈ ℝ ∧ 𝑀 ∈ ℕ0) → (𝑀 ∈ ℝ ∧ 𝐿 ∈ ℝ))
24		letri3 8188	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((𝑀 ∈ ℝ ∧ 𝐿 ∈ ℝ) → (𝑀 = 𝐿 ↔ (𝑀 ≤ 𝐿 ∧ 𝐿 ≤ 𝑀)))
25	23, 24	syl 14	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝐿 ∈ ℝ ∧ 𝑀 ∈ ℕ0) → (𝑀 = 𝐿 ↔ (𝑀 ≤ 𝐿 ∧ 𝐿 ≤ 𝑀)))
26	25	biimprd 158	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝐿 ∈ ℝ ∧ 𝑀 ∈ ℕ0) → ((𝑀 ≤ 𝐿 ∧ 𝐿 ≤ 𝑀) → 𝑀 = 𝐿))
27	26	exp4b 367	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝐿 ∈ ℝ → (𝑀 ∈ ℕ0 → (𝑀 ≤ 𝐿 → (𝐿 ≤ 𝑀 → 𝑀 = 𝐿))))
28	27	com23 78	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝐿 ∈ ℝ → (𝑀 ≤ 𝐿 → (𝑀 ∈ ℕ0 → (𝐿 ≤ 𝑀 → 𝑀 = 𝐿))))
29	20, 28	sylbid 150	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝐿 ∈ ℝ → (𝑀 ≤ (𝐿 + 0) → (𝑀 ∈ ℕ0 → (𝐿 ≤ 𝑀 → 𝑀 = 𝐿))))
30	29	com3l 81	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑀 ≤ (𝐿 + 0) → (𝑀 ∈ ℕ0 → (𝐿 ∈ ℝ → (𝐿 ≤ 𝑀 → 𝑀 = 𝐿))))
31	30	impcom 125	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑀 ∈ ℕ0 ∧ 𝑀 ≤ (𝐿 + 0)) → (𝐿 ∈ ℝ → (𝐿 ≤ 𝑀 → 𝑀 = 𝐿)))
32	31	3adant2 1019	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑀 ∈ ℕ0 ∧ (𝐿 + 0) ∈ ℕ0 ∧ 𝑀 ≤ (𝐿 + 0)) → (𝐿 ∈ ℝ → (𝐿 ≤ 𝑀 → 𝑀 = 𝐿)))
33	32	com12 30	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝐿 ∈ ℝ → ((𝑀 ∈ ℕ0 ∧ (𝐿 + 0) ∈ ℕ0 ∧ 𝑀 ≤ (𝐿 + 0)) → (𝐿 ≤ 𝑀 → 𝑀 = 𝐿)))
34	17, 33	biimtrid 152	. . . . . . . . . . . . . . . . . 18 ⊢ (𝐿 ∈ ℝ → (𝑀 ∈ (0...(𝐿 + 0)) → (𝐿 ≤ 𝑀 → 𝑀 = 𝐿)))
35	16, 34	syl 14	. . . . . . . . . . . . . . . . 17 ⊢ (𝐿 ∈ ℕ0 → (𝑀 ∈ (0...(𝐿 + 0)) → (𝐿 ≤ 𝑀 → 𝑀 = 𝐿)))
36	15, 35	sylbi 121	. . . . . . . . . . . . . . . 16 ⊢ ((♯‘𝐴) ∈ ℕ0 → (𝑀 ∈ (0...(𝐿 + 0)) → (𝐿 ≤ 𝑀 → 𝑀 = 𝐿)))
37	12, 36	syl 14	. . . . . . . . . . . . . . 15 ⊢ (𝐴 ∈ Word 𝑉 → (𝑀 ∈ (0...(𝐿 + 0)) → (𝐿 ≤ 𝑀 → 𝑀 = 𝐿)))
38	37	imp 124	. . . . . . . . . . . . . 14 ⊢ ((𝐴 ∈ Word 𝑉 ∧ 𝑀 ∈ (0...(𝐿 + 0))) → (𝐿 ≤ 𝑀 → 𝑀 = 𝐿))
39		0ex 4187	. . . . . . . . . . . . . . . . . . 19 ⊢ ∅ ∈ V
40		0z 9418	. . . . . . . . . . . . . . . . . . 19 ⊢ 0 ∈ ℤ
41		swrd00g 11140	. . . . . . . . . . . . . . . . . . 19 ⊢ ((∅ ∈ V ∧ 0 ∈ ℤ) → (∅ substr ⟨0, 0⟩) = ∅)
42	39, 40, 41	mp2an 426	. . . . . . . . . . . . . . . . . 18 ⊢ (∅ substr ⟨0, 0⟩) = ∅
43	13, 12	eqeltrid 2294	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝐴 ∈ Word 𝑉 → 𝐿 ∈ ℕ0)
44	43	nn0zd 9528	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝐴 ∈ Word 𝑉 → 𝐿 ∈ ℤ)
45		swrd00g 11140	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝐴 ∈ Word 𝑉 ∧ 𝐿 ∈ ℤ) → (𝐴 substr ⟨𝐿, 𝐿⟩) = ∅)
46	44, 45	mpdan 421	. . . . . . . . . . . . . . . . . 18 ⊢ (𝐴 ∈ Word 𝑉 → (𝐴 substr ⟨𝐿, 𝐿⟩) = ∅)
47	42, 46	eqtr4id 2259	. . . . . . . . . . . . . . . . 17 ⊢ (𝐴 ∈ Word 𝑉 → (∅ substr ⟨0, 0⟩) = (𝐴 substr ⟨𝐿, 𝐿⟩))
48		nn0cn 9340	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝐿 ∈ ℕ0 → 𝐿 ∈ ℂ)
49	48	subidd 8406	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝐿 ∈ ℕ0 → (𝐿 − 𝐿) = 0)
50	49	opeq1d 3839	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝐿 ∈ ℕ0 → ⟨(𝐿 − 𝐿), 0⟩ = ⟨0, 0⟩)
51	50	oveq2d 5983	. . . . . . . . . . . . . . . . . 18 ⊢ (𝐿 ∈ ℕ0 → (∅ substr ⟨(𝐿 − 𝐿), 0⟩) = (∅ substr ⟨0, 0⟩))
52	43, 51	syl 14	. . . . . . . . . . . . . . . . 17 ⊢ (𝐴 ∈ Word 𝑉 → (∅ substr ⟨(𝐿 − 𝐿), 0⟩) = (∅ substr ⟨0, 0⟩))
53	48	addridd 8256	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝐿 ∈ ℕ0 → (𝐿 + 0) = 𝐿)
54	53	opeq2d 3840	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝐿 ∈ ℕ0 → ⟨𝐿, (𝐿 + 0)⟩ = ⟨𝐿, 𝐿⟩)
55	54	oveq2d 5983	. . . . . . . . . . . . . . . . . 18 ⊢ (𝐿 ∈ ℕ0 → (𝐴 substr ⟨𝐿, (𝐿 + 0)⟩) = (𝐴 substr ⟨𝐿, 𝐿⟩))
56	43, 55	syl 14	. . . . . . . . . . . . . . . . 17 ⊢ (𝐴 ∈ Word 𝑉 → (𝐴 substr ⟨𝐿, (𝐿 + 0)⟩) = (𝐴 substr ⟨𝐿, 𝐿⟩))
57	47, 52, 56	3eqtr4d 2250	. . . . . . . . . . . . . . . 16 ⊢ (𝐴 ∈ Word 𝑉 → (∅ substr ⟨(𝐿 − 𝐿), 0⟩) = (𝐴 substr ⟨𝐿, (𝐿 + 0)⟩))
58		oveq1 5974	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑀 = 𝐿 → (𝑀 − 𝐿) = (𝐿 − 𝐿))
59	58	opeq1d 3839	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑀 = 𝐿 → ⟨(𝑀 − 𝐿), 0⟩ = ⟨(𝐿 − 𝐿), 0⟩)
60	59	oveq2d 5983	. . . . . . . . . . . . . . . . 17 ⊢ (𝑀 = 𝐿 → (∅ substr ⟨(𝑀 − 𝐿), 0⟩) = (∅ substr ⟨(𝐿 − 𝐿), 0⟩))
61		opeq1 3833	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑀 = 𝐿 → ⟨𝑀, (𝐿 + 0)⟩ = ⟨𝐿, (𝐿 + 0)⟩)
62	61	oveq2d 5983	. . . . . . . . . . . . . . . . 17 ⊢ (𝑀 = 𝐿 → (𝐴 substr ⟨𝑀, (𝐿 + 0)⟩) = (𝐴 substr ⟨𝐿, (𝐿 + 0)⟩))
63	60, 62	eqeq12d 2222	. . . . . . . . . . . . . . . 16 ⊢ (𝑀 = 𝐿 → ((∅ substr ⟨(𝑀 − 𝐿), 0⟩) = (𝐴 substr ⟨𝑀, (𝐿 + 0)⟩) ↔ (∅ substr ⟨(𝐿 − 𝐿), 0⟩) = (𝐴 substr ⟨𝐿, (𝐿 + 0)⟩)))
64	57, 63	syl5ibrcom 157	. . . . . . . . . . . . . . 15 ⊢ (𝐴 ∈ Word 𝑉 → (𝑀 = 𝐿 → (∅ substr ⟨(𝑀 − 𝐿), 0⟩) = (𝐴 substr ⟨𝑀, (𝐿 + 0)⟩)))
65	64	adantr 276	. . . . . . . . . . . . . 14 ⊢ ((𝐴 ∈ Word 𝑉 ∧ 𝑀 ∈ (0...(𝐿 + 0))) → (𝑀 = 𝐿 → (∅ substr ⟨(𝑀 − 𝐿), 0⟩) = (𝐴 substr ⟨𝑀, (𝐿 + 0)⟩)))
66	38, 65	syld 45	. . . . . . . . . . . . 13 ⊢ ((𝐴 ∈ Word 𝑉 ∧ 𝑀 ∈ (0...(𝐿 + 0))) → (𝐿 ≤ 𝑀 → (∅ substr ⟨(𝑀 − 𝐿), 0⟩) = (𝐴 substr ⟨𝑀, (𝐿 + 0)⟩)))
67	66	imp 124	. . . . . . . . . . . 12 ⊢ (((𝐴 ∈ Word 𝑉 ∧ 𝑀 ∈ (0...(𝐿 + 0))) ∧ 𝐿 ≤ 𝑀) → (∅ substr ⟨(𝑀 − 𝐿), 0⟩) = (𝐴 substr ⟨𝑀, (𝐿 + 0)⟩))
68		simpl 109	. . . . . . . . . . . . . . . 16 ⊢ ((𝐴 ∈ Word 𝑉 ∧ 𝑀 ∈ (0...(𝐿 + 0))) → 𝐴 ∈ Word 𝑉)
69		elfzelz 10182	. . . . . . . . . . . . . . . . 17 ⊢ (𝑀 ∈ (0...(𝐿 + 0)) → 𝑀 ∈ ℤ)
70	69	adantl 277	. . . . . . . . . . . . . . . 16 ⊢ ((𝐴 ∈ Word 𝑉 ∧ 𝑀 ∈ (0...(𝐿 + 0))) → 𝑀 ∈ ℤ)
71	44	adantr 276	. . . . . . . . . . . . . . . 16 ⊢ ((𝐴 ∈ Word 𝑉 ∧ 𝑀 ∈ (0...(𝐿 + 0))) → 𝐿 ∈ ℤ)
72		swrdclg 11141	. . . . . . . . . . . . . . . 16 ⊢ ((𝐴 ∈ Word 𝑉 ∧ 𝑀 ∈ ℤ ∧ 𝐿 ∈ ℤ) → (𝐴 substr ⟨𝑀, 𝐿⟩) ∈ Word 𝑉)
73	68, 70, 71, 72	syl3anc 1250	. . . . . . . . . . . . . . 15 ⊢ ((𝐴 ∈ Word 𝑉 ∧ 𝑀 ∈ (0...(𝐿 + 0))) → (𝐴 substr ⟨𝑀, 𝐿⟩) ∈ Word 𝑉)
74		ccatrid 11101	. . . . . . . . . . . . . . 15 ⊢ ((𝐴 substr ⟨𝑀, 𝐿⟩) ∈ Word 𝑉 → ((𝐴 substr ⟨𝑀, 𝐿⟩) ++ ∅) = (𝐴 substr ⟨𝑀, 𝐿⟩))
75	73, 74	syl 14	. . . . . . . . . . . . . 14 ⊢ ((𝐴 ∈ Word 𝑉 ∧ 𝑀 ∈ (0...(𝐿 + 0))) → ((𝐴 substr ⟨𝑀, 𝐿⟩) ++ ∅) = (𝐴 substr ⟨𝑀, 𝐿⟩))
76	15, 48	sylbi 121	. . . . . . . . . . . . . . . . . . 19 ⊢ ((♯‘𝐴) ∈ ℕ0 → 𝐿 ∈ ℂ)
77	12, 76	syl 14	. . . . . . . . . . . . . . . . . 18 ⊢ (𝐴 ∈ Word 𝑉 → 𝐿 ∈ ℂ)
78		addrid 8245	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝐿 ∈ ℂ → (𝐿 + 0) = 𝐿)
79	78	eqcomd 2213	. . . . . . . . . . . . . . . . . 18 ⊢ (𝐿 ∈ ℂ → 𝐿 = (𝐿 + 0))
80	77, 79	syl 14	. . . . . . . . . . . . . . . . 17 ⊢ (𝐴 ∈ Word 𝑉 → 𝐿 = (𝐿 + 0))
81	80	opeq2d 3840	. . . . . . . . . . . . . . . 16 ⊢ (𝐴 ∈ Word 𝑉 → ⟨𝑀, 𝐿⟩ = ⟨𝑀, (𝐿 + 0)⟩)
82	81	oveq2d 5983	. . . . . . . . . . . . . . 15 ⊢ (𝐴 ∈ Word 𝑉 → (𝐴 substr ⟨𝑀, 𝐿⟩) = (𝐴 substr ⟨𝑀, (𝐿 + 0)⟩))
83	82	adantr 276	. . . . . . . . . . . . . 14 ⊢ ((𝐴 ∈ Word 𝑉 ∧ 𝑀 ∈ (0...(𝐿 + 0))) → (𝐴 substr ⟨𝑀, 𝐿⟩) = (𝐴 substr ⟨𝑀, (𝐿 + 0)⟩))
84	75, 83	eqtrd 2240	. . . . . . . . . . . . 13 ⊢ ((𝐴 ∈ Word 𝑉 ∧ 𝑀 ∈ (0...(𝐿 + 0))) → ((𝐴 substr ⟨𝑀, 𝐿⟩) ++ ∅) = (𝐴 substr ⟨𝑀, (𝐿 + 0)⟩))
85	84	adantr 276	. . . . . . . . . . . 12 ⊢ (((𝐴 ∈ Word 𝑉 ∧ 𝑀 ∈ (0...(𝐿 + 0))) ∧ ¬ 𝐿 ≤ 𝑀) → ((𝐴 substr ⟨𝑀, 𝐿⟩) ++ ∅) = (𝐴 substr ⟨𝑀, (𝐿 + 0)⟩))
86		zdcle 9484	. . . . . . . . . . . . 13 ⊢ ((𝐿 ∈ ℤ ∧ 𝑀 ∈ ℤ) → DECID 𝐿 ≤ 𝑀)
87	44, 69, 86	syl2an 289	. . . . . . . . . . . 12 ⊢ ((𝐴 ∈ Word 𝑉 ∧ 𝑀 ∈ (0...(𝐿 + 0))) → DECID 𝐿 ≤ 𝑀)
88	67, 85, 87	ifeqdadc 3612	. . . . . . . . . . 11 ⊢ ((𝐴 ∈ Word 𝑉 ∧ 𝑀 ∈ (0...(𝐿 + 0))) → if(𝐿 ≤ 𝑀, (∅ substr ⟨(𝑀 − 𝐿), 0⟩), ((𝐴 substr ⟨𝑀, 𝐿⟩) ++ ∅)) = (𝐴 substr ⟨𝑀, (𝐿 + 0)⟩))
89	88	ex 115	. . . . . . . . . 10 ⊢ (𝐴 ∈ Word 𝑉 → (𝑀 ∈ (0...(𝐿 + 0)) → if(𝐿 ≤ 𝑀, (∅ substr ⟨(𝑀 − 𝐿), 0⟩), ((𝐴 substr ⟨𝑀, 𝐿⟩) ++ ∅)) = (𝐴 substr ⟨𝑀, (𝐿 + 0)⟩)))
90	89	ad3antrrr 492	. . . . . . . . 9 ⊢ ((((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ (♯‘𝐵) = 0) ∧ 𝐵 = ∅) → (𝑀 ∈ (0...(𝐿 + 0)) → if(𝐿 ≤ 𝑀, (∅ substr ⟨(𝑀 − 𝐿), 0⟩), ((𝐴 substr ⟨𝑀, 𝐿⟩) ++ ∅)) = (𝐴 substr ⟨𝑀, (𝐿 + 0)⟩)))
91		oveq2 5975	. . . . . . . . . . . . . 14 ⊢ ((♯‘𝐵) = 0 → (𝐿 + (♯‘𝐵)) = (𝐿 + 0))
92	91	oveq2d 5983	. . . . . . . . . . . . 13 ⊢ ((♯‘𝐵) = 0 → (0...(𝐿 + (♯‘𝐵))) = (0...(𝐿 + 0)))
93	92	eleq2d 2277	. . . . . . . . . . . 12 ⊢ ((♯‘𝐵) = 0 → (𝑀 ∈ (0...(𝐿 + (♯‘𝐵))) ↔ 𝑀 ∈ (0...(𝐿 + 0))))
94	93	adantr 276	. . . . . . . . . . 11 ⊢ (((♯‘𝐵) = 0 ∧ 𝐵 = ∅) → (𝑀 ∈ (0...(𝐿 + (♯‘𝐵))) ↔ 𝑀 ∈ (0...(𝐿 + 0))))
95		simpr 110	. . . . . . . . . . . . . 14 ⊢ (((♯‘𝐵) = 0 ∧ 𝐵 = ∅) → 𝐵 = ∅)
96		opeq2 3834	. . . . . . . . . . . . . . 15 ⊢ ((♯‘𝐵) = 0 → ⟨(𝑀 − 𝐿), (♯‘𝐵)⟩ = ⟨(𝑀 − 𝐿), 0⟩)
97	96	adantr 276	. . . . . . . . . . . . . 14 ⊢ (((♯‘𝐵) = 0 ∧ 𝐵 = ∅) → ⟨(𝑀 − 𝐿), (♯‘𝐵)⟩ = ⟨(𝑀 − 𝐿), 0⟩)
98	95, 97	oveq12d 5985	. . . . . . . . . . . . 13 ⊢ (((♯‘𝐵) = 0 ∧ 𝐵 = ∅) → (𝐵 substr ⟨(𝑀 − 𝐿), (♯‘𝐵)⟩) = (∅ substr ⟨(𝑀 − 𝐿), 0⟩))
99		oveq2 5975	. . . . . . . . . . . . . 14 ⊢ (𝐵 = ∅ → ((𝐴 substr ⟨𝑀, 𝐿⟩) ++ 𝐵) = ((𝐴 substr ⟨𝑀, 𝐿⟩) ++ ∅))
100	99	adantl 277	. . . . . . . . . . . . 13 ⊢ (((♯‘𝐵) = 0 ∧ 𝐵 = ∅) → ((𝐴 substr ⟨𝑀, 𝐿⟩) ++ 𝐵) = ((𝐴 substr ⟨𝑀, 𝐿⟩) ++ ∅))
101	98, 100	ifeq12d 3599	. . . . . . . . . . . 12 ⊢ (((♯‘𝐵) = 0 ∧ 𝐵 = ∅) → if(𝐿 ≤ 𝑀, (𝐵 substr ⟨(𝑀 − 𝐿), (♯‘𝐵)⟩), ((𝐴 substr ⟨𝑀, 𝐿⟩) ++ 𝐵)) = if(𝐿 ≤ 𝑀, (∅ substr ⟨(𝑀 − 𝐿), 0⟩), ((𝐴 substr ⟨𝑀, 𝐿⟩) ++ ∅)))
102	91	opeq2d 3840	. . . . . . . . . . . . . 14 ⊢ ((♯‘𝐵) = 0 → ⟨𝑀, (𝐿 + (♯‘𝐵))⟩ = ⟨𝑀, (𝐿 + 0)⟩)
103	102	oveq2d 5983	. . . . . . . . . . . . 13 ⊢ ((♯‘𝐵) = 0 → (𝐴 substr ⟨𝑀, (𝐿 + (♯‘𝐵))⟩) = (𝐴 substr ⟨𝑀, (𝐿 + 0)⟩))
104	103	adantr 276	. . . . . . . . . . . 12 ⊢ (((♯‘𝐵) = 0 ∧ 𝐵 = ∅) → (𝐴 substr ⟨𝑀, (𝐿 + (♯‘𝐵))⟩) = (𝐴 substr ⟨𝑀, (𝐿 + 0)⟩))
105	101, 104	eqeq12d 2222	. . . . . . . . . . 11 ⊢ (((♯‘𝐵) = 0 ∧ 𝐵 = ∅) → (if(𝐿 ≤ 𝑀, (𝐵 substr ⟨(𝑀 − 𝐿), (♯‘𝐵)⟩), ((𝐴 substr ⟨𝑀, 𝐿⟩) ++ 𝐵)) = (𝐴 substr ⟨𝑀, (𝐿 + (♯‘𝐵))⟩) ↔ if(𝐿 ≤ 𝑀, (∅ substr ⟨(𝑀 − 𝐿), 0⟩), ((𝐴 substr ⟨𝑀, 𝐿⟩) ++ ∅)) = (𝐴 substr ⟨𝑀, (𝐿 + 0)⟩)))
106	94, 105	imbi12d 234	. . . . . . . . . 10 ⊢ (((♯‘𝐵) = 0 ∧ 𝐵 = ∅) → ((𝑀 ∈ (0...(𝐿 + (♯‘𝐵))) → if(𝐿 ≤ 𝑀, (𝐵 substr ⟨(𝑀 − 𝐿), (♯‘𝐵)⟩), ((𝐴 substr ⟨𝑀, 𝐿⟩) ++ 𝐵)) = (𝐴 substr ⟨𝑀, (𝐿 + (♯‘𝐵))⟩)) ↔ (𝑀 ∈ (0...(𝐿 + 0)) → if(𝐿 ≤ 𝑀, (∅ substr ⟨(𝑀 − 𝐿), 0⟩), ((𝐴 substr ⟨𝑀, 𝐿⟩) ++ ∅)) = (𝐴 substr ⟨𝑀, (𝐿 + 0)⟩))))
107	106	adantll 476	. . . . . . . . 9 ⊢ ((((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ (♯‘𝐵) = 0) ∧ 𝐵 = ∅) → ((𝑀 ∈ (0...(𝐿 + (♯‘𝐵))) → if(𝐿 ≤ 𝑀, (𝐵 substr ⟨(𝑀 − 𝐿), (♯‘𝐵)⟩), ((𝐴 substr ⟨𝑀, 𝐿⟩) ++ 𝐵)) = (𝐴 substr ⟨𝑀, (𝐿 + (♯‘𝐵))⟩)) ↔ (𝑀 ∈ (0...(𝐿 + 0)) → if(𝐿 ≤ 𝑀, (∅ substr ⟨(𝑀 − 𝐿), 0⟩), ((𝐴 substr ⟨𝑀, 𝐿⟩) ++ ∅)) = (𝐴 substr ⟨𝑀, (𝐿 + 0)⟩))))
108	90, 107	mpbird 167	. . . . . . . 8 ⊢ ((((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ (♯‘𝐵) = 0) ∧ 𝐵 = ∅) → (𝑀 ∈ (0...(𝐿 + (♯‘𝐵))) → if(𝐿 ≤ 𝑀, (𝐵 substr ⟨(𝑀 − 𝐿), (♯‘𝐵)⟩), ((𝐴 substr ⟨𝑀, 𝐿⟩) ++ 𝐵)) = (𝐴 substr ⟨𝑀, (𝐿 + (♯‘𝐵))⟩)))
109	11, 108	mpdan 421	. . . . . . 7 ⊢ (((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ (♯‘𝐵) = 0) → (𝑀 ∈ (0...(𝐿 + (♯‘𝐵))) → if(𝐿 ≤ 𝑀, (𝐵 substr ⟨(𝑀 − 𝐿), (♯‘𝐵)⟩), ((𝐴 substr ⟨𝑀, 𝐿⟩) ++ 𝐵)) = (𝐴 substr ⟨𝑀, (𝐿 + (♯‘𝐵))⟩)))
110	109	ex 115	. . . . . 6 ⊢ ((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) → ((♯‘𝐵) = 0 → (𝑀 ∈ (0...(𝐿 + (♯‘𝐵))) → if(𝐿 ≤ 𝑀, (𝐵 substr ⟨(𝑀 − 𝐿), (♯‘𝐵)⟩), ((𝐴 substr ⟨𝑀, 𝐿⟩) ++ 𝐵)) = (𝐴 substr ⟨𝑀, (𝐿 + (♯‘𝐵))⟩))))
111	5, 110	syld 45	. . . . 5 ⊢ ((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) → ((♯‘𝐵) ≤ 0 → (𝑀 ∈ (0...(𝐿 + (♯‘𝐵))) → if(𝐿 ≤ 𝑀, (𝐵 substr ⟨(𝑀 − 𝐿), (♯‘𝐵)⟩), ((𝐴 substr ⟨𝑀, 𝐿⟩) ++ 𝐵)) = (𝐴 substr ⟨𝑀, (𝐿 + (♯‘𝐵))⟩))))
112	111	com23 78	. . . 4 ⊢ ((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) → (𝑀 ∈ (0...(𝐿 + (♯‘𝐵))) → ((♯‘𝐵) ≤ 0 → if(𝐿 ≤ 𝑀, (𝐵 substr ⟨(𝑀 − 𝐿), (♯‘𝐵)⟩), ((𝐴 substr ⟨𝑀, 𝐿⟩) ++ 𝐵)) = (𝐴 substr ⟨𝑀, (𝐿 + (♯‘𝐵))⟩))))
113	112	imp 124	. . 3 ⊢ (((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ 𝑀 ∈ (0...(𝐿 + (♯‘𝐵)))) → ((♯‘𝐵) ≤ 0 → if(𝐿 ≤ 𝑀, (𝐵 substr ⟨(𝑀 − 𝐿), (♯‘𝐵)⟩), ((𝐴 substr ⟨𝑀, 𝐿⟩) ++ 𝐵)) = (𝐴 substr ⟨𝑀, (𝐿 + (♯‘𝐵))⟩)))
114	113	adantr 276	. 2 ⊢ ((((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ 𝑀 ∈ (0...(𝐿 + (♯‘𝐵)))) ∧ (𝐿 + (♯‘𝐵)) ≤ 𝐿) → ((♯‘𝐵) ≤ 0 → if(𝐿 ≤ 𝑀, (𝐵 substr ⟨(𝑀 − 𝐿), (♯‘𝐵)⟩), ((𝐴 substr ⟨𝑀, 𝐿⟩) ++ 𝐵)) = (𝐴 substr ⟨𝑀, (𝐿 + (♯‘𝐵))⟩)))
115	13	eleq1i 2273	. . . . . . . 8 ⊢ (𝐿 ∈ ℕ0 ↔ (♯‘𝐴) ∈ ℕ0)
116	115, 16	sylbir 135	. . . . . . 7 ⊢ ((♯‘𝐴) ∈ ℕ0 → 𝐿 ∈ ℝ)
117	12, 116	syl 14	. . . . . 6 ⊢ (𝐴 ∈ Word 𝑉 → 𝐿 ∈ ℝ)
118	1	nn0red 9384	. . . . . 6 ⊢ (𝐵 ∈ Word 𝑉 → (♯‘𝐵) ∈ ℝ)
119		leaddle0 8585	. . . . . 6 ⊢ ((𝐿 ∈ ℝ ∧ (♯‘𝐵) ∈ ℝ) → ((𝐿 + (♯‘𝐵)) ≤ 𝐿 ↔ (♯‘𝐵) ≤ 0))
120	117, 118, 119	syl2an 289	. . . . 5 ⊢ ((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) → ((𝐿 + (♯‘𝐵)) ≤ 𝐿 ↔ (♯‘𝐵) ≤ 0))
121		pm2.24 622	. . . . 5 ⊢ ((♯‘𝐵) ≤ 0 → (¬ (♯‘𝐵) ≤ 0 → if(𝐿 ≤ 𝑀, (𝐵 substr ⟨(𝑀 − 𝐿), (♯‘𝐵)⟩), ((𝐴 substr ⟨𝑀, 𝐿⟩) ++ 𝐵)) = (𝐴 substr ⟨𝑀, (𝐿 + (♯‘𝐵))⟩)))
122	120, 121	biimtrdi 163	. . . 4 ⊢ ((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) → ((𝐿 + (♯‘𝐵)) ≤ 𝐿 → (¬ (♯‘𝐵) ≤ 0 → if(𝐿 ≤ 𝑀, (𝐵 substr ⟨(𝑀 − 𝐿), (♯‘𝐵)⟩), ((𝐴 substr ⟨𝑀, 𝐿⟩) ++ 𝐵)) = (𝐴 substr ⟨𝑀, (𝐿 + (♯‘𝐵))⟩))))
123	122	adantr 276	. . 3 ⊢ (((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ 𝑀 ∈ (0...(𝐿 + (♯‘𝐵)))) → ((𝐿 + (♯‘𝐵)) ≤ 𝐿 → (¬ (♯‘𝐵) ≤ 0 → if(𝐿 ≤ 𝑀, (𝐵 substr ⟨(𝑀 − 𝐿), (♯‘𝐵)⟩), ((𝐴 substr ⟨𝑀, 𝐿⟩) ++ 𝐵)) = (𝐴 substr ⟨𝑀, (𝐿 + (♯‘𝐵))⟩))))
124	123	imp 124	. 2 ⊢ ((((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ 𝑀 ∈ (0...(𝐿 + (♯‘𝐵)))) ∧ (𝐿 + (♯‘𝐵)) ≤ 𝐿) → (¬ (♯‘𝐵) ≤ 0 → if(𝐿 ≤ 𝑀, (𝐵 substr ⟨(𝑀 − 𝐿), (♯‘𝐵)⟩), ((𝐴 substr ⟨𝑀, 𝐿⟩) ++ 𝐵)) = (𝐴 substr ⟨𝑀, (𝐿 + (♯‘𝐵))⟩)))
125	1	ad3antlr 493	. . . . 5 ⊢ ((((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ 𝑀 ∈ (0...(𝐿 + (♯‘𝐵)))) ∧ (𝐿 + (♯‘𝐵)) ≤ 𝐿) → (♯‘𝐵) ∈ ℕ0)
126	125	nn0zd 9528	. . . 4 ⊢ ((((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ 𝑀 ∈ (0...(𝐿 + (♯‘𝐵)))) ∧ (𝐿 + (♯‘𝐵)) ≤ 𝐿) → (♯‘𝐵) ∈ ℤ)
127		zdcle 9484	. . . 4 ⊢ (((♯‘𝐵) ∈ ℤ ∧ 0 ∈ ℤ) → DECID (♯‘𝐵) ≤ 0)
128	126, 40, 127	sylancl 413	. . 3 ⊢ ((((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ 𝑀 ∈ (0...(𝐿 + (♯‘𝐵)))) ∧ (𝐿 + (♯‘𝐵)) ≤ 𝐿) → DECID (♯‘𝐵) ≤ 0)
129		exmiddc 838	. . 3 ⊢ (DECID (♯‘𝐵) ≤ 0 → ((♯‘𝐵) ≤ 0 ∨ ¬ (♯‘𝐵) ≤ 0))
130	128, 129	syl 14	. 2 ⊢ ((((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ 𝑀 ∈ (0...(𝐿 + (♯‘𝐵)))) ∧ (𝐿 + (♯‘𝐵)) ≤ 𝐿) → ((♯‘𝐵) ≤ 0 ∨ ¬ (♯‘𝐵) ≤ 0))
131	114, 124, 130	mpjaod 720	1 ⊢ ((((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ 𝑀 ∈ (0...(𝐿 + (♯‘𝐵)))) ∧ (𝐿 + (♯‘𝐵)) ≤ 𝐿) → if(𝐿 ≤ 𝑀, (𝐵 substr ⟨(𝑀 − 𝐿), (♯‘𝐵)⟩), ((𝐴 substr ⟨𝑀, 𝐿⟩) ++ 𝐵)) = (𝐴 substr ⟨𝑀, (𝐿 + (♯‘𝐵))⟩))

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 104   ↔ wb 105   ∨ wo 710  DECID wdc 836   ∧ w3a 981   = wceq 1373   ∈ wcel 2178  Vcvv 2776  ∅c0 3468  ifcif 3579  ⟨cop 3646   class class class wbr 4059  ‘cfv 5290  (class class class)co 5967  Fincfn 6850  ℂcc 7958  ℝcr 7959  0cc0 7960   + caddc 7963   ≤ cle 8143   − cmin 8278  ℕ₀cn0 9330  ℤcz 9407  ...cfz 10165  ♯chash 10957  Word cword 11031   ++ cconcat 11084   substr csubstr 11136

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-in1 615  ax-in2 616  ax-io 711  ax-5 1471  ax-7 1472  ax-gen 1473  ax-ie1 1517  ax-ie2 1518  ax-8 1528  ax-10 1529  ax-11 1530  ax-i12 1531  ax-bndl 1533  ax-4 1534  ax-17 1550  ax-i9 1554  ax-ial 1558  ax-i5r 1559  ax-13 2180  ax-14 2181  ax-ext 2189  ax-coll 4175  ax-sep 4178  ax-nul 4186  ax-pow 4234  ax-pr 4269  ax-un 4498  ax-setind 4603  ax-iinf 4654  ax-cnex 8051  ax-resscn 8052  ax-1cn 8053  ax-1re 8054  ax-icn 8055  ax-addcl 8056  ax-addrcl 8057  ax-mulcl 8058  ax-addcom 8060  ax-addass 8062  ax-distr 8064  ax-i2m1 8065  ax-0lt1 8066  ax-0id 8068  ax-rnegex 8069  ax-cnre 8071  ax-pre-ltirr 8072  ax-pre-ltwlin 8073  ax-pre-lttrn 8074  ax-pre-apti 8075  ax-pre-ltadd 8076

This theorem depends on definitions:  df-bi 117  df-dc 837  df-3or 982  df-3an 983  df-tru 1376  df-fal 1379  df-nf 1485  df-sb 1787  df-eu 2058  df-mo 2059  df-clab 2194  df-cleq 2200  df-clel 2203  df-nfc 2339  df-ne 2379  df-nel 2474  df-ral 2491  df-rex 2492  df-reu 2493  df-rab 2495  df-v 2778  df-sbc 3006  df-csb 3102  df-dif 3176  df-un 3178  df-in 3180  df-ss 3187  df-nul 3469  df-if 3580  df-pw 3628  df-sn 3649  df-pr 3650  df-op 3652  df-uni 3865  df-int 3900  df-iun 3943  df-br 4060  df-opab 4122  df-mpt 4123  df-tr 4159  df-id 4358  df-iord 4431  df-on 4433  df-ilim 4434  df-suc 4436  df-iom 4657  df-xp 4699  df-rel 4700  df-cnv 4701  df-co 4702  df-dm 4703  df-rn 4704  df-res 4705  df-ima 4706  df-iota 5251  df-fun 5292  df-fn 5293  df-f 5294  df-f1 5295  df-fo 5296  df-f1o 5297  df-fv 5298  df-riota 5922  df-ov 5970  df-oprab 5971  df-mpo 5972  df-1st 6249  df-2nd 6250  df-recs 6414  df-frec 6500  df-1o 6525  df-er 6643  df-en 6851  df-dom 6852  df-fin 6853  df-pnf 8144  df-mnf 8145  df-xr 8146  df-ltxr 8147  df-le 8148  df-sub 8280  df-neg 8281  df-inn 9072  df-n0 9331  df-z 9408  df-uz 9684  df-fz 10166  df-fzo 10300  df-ihash 10958  df-word 11032  df-concat 11085  df-substr 11137

This theorem is referenced by:  swrdccat3b  11231