swrdccat3blem - Intuitionistic Logic Explorer

	Intuitionistic Logic Explorer		< Previous Next > Nearby theorems
Mirrors > Home > ILE Home > Th. List > swrdccat3blem		GIF version

Theorem swrdccat3blem 11511

Description: Lemma for swrdccat3b 11512. (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 11308	. . . . . . . 8 ⊢ (𝐵 ∈ Word 𝑉 → (♯‘𝐵) ∈ ℕ₀)
2		nn0le0eq0 9591	. . . . . . . . 9 ⊢ ((♯‘𝐵) ∈ ℕ₀ → ((♯‘𝐵) ≤ 0 ↔ (♯‘𝐵) = 0))
3	2	biimpd 144	. . . . . . . 8 ⊢ ((♯‘𝐵) ∈ ℕ₀ → ((♯‘𝐵) ≤ 0 → (♯‘𝐵) = 0))
4	1, 3	syl 14	. . . . . . 7 ⊢ (𝐵 ∈ Word 𝑉 → ((♯‘𝐵) ≤ 0 → (♯‘𝐵) = 0))
5	4	adantl 277	. . . . . 6 ⊢ ((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) → ((♯‘𝐵) ≤ 0 → (♯‘𝐵) = 0))
6		wrdfin 11323	. . . . . . . . . . . 12 ⊢ (𝐵 ∈ Word 𝑉 → 𝐵 ∈ Fin)
7		fihasheq0 11232	. . . . . . . . . . . 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 11308	. . . . . . . . . . . . . . . 16 ⊢ (𝐴 ∈ Word 𝑉 → (♯‘𝐴) ∈ ℕ₀)
13		swrdccatin2.l	. . . . . . . . . . . . . . . . . . 19 ⊢ 𝐿 = (♯‘𝐴)
14	13	eqcomi 2242	. . . . . . . . . . . . . . . . . 18 ⊢ (♯‘𝐴) = 𝐿
15	14	eleq1i 2304	. . . . . . . . . . . . . . . . 17 ⊢ ((♯‘𝐴) ∈ ℕ₀ ↔ 𝐿 ∈ ℕ₀)
16		nn0re 9572	. . . . . . . . . . . . . . . . . 18 ⊢ (𝐿 ∈ ℕ₀ → 𝐿 ∈ ℝ)
17		elfz2nn0 10519	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑀 ∈ (0...(𝐿 + 0)) ↔ (𝑀 ∈ ℕ₀ ∧ (𝐿 + 0) ∈ ℕ₀ ∧ 𝑀 ≤ (𝐿 + 0)))
18		recn 8312	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝐿 ∈ ℝ → 𝐿 ∈ ℂ)
19	18	addridd 8475	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝐿 ∈ ℝ → (𝐿 + 0) = 𝐿)
20	19	breq2d 4142	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝐿 ∈ ℝ → (𝑀 ≤ (𝐿 + 0) ↔ 𝑀 ≤ 𝐿))
21		nn0re 9572	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (𝑀 ∈ ℕ₀ → 𝑀 ∈ ℝ)
22	21	anim1i 340	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((𝑀 ∈ ℕ₀ ∧ 𝐿 ∈ ℝ) → (𝑀 ∈ ℝ ∧ 𝐿 ∈ ℝ))
23	22	ancoms 268	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((𝐿 ∈ ℝ ∧ 𝑀 ∈ ℕ₀) → (𝑀 ∈ ℝ ∧ 𝐿 ∈ ℝ))
24		letri3 8406	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((𝑀 ∈ ℝ ∧ 𝐿 ∈ ℝ) → (𝑀 = 𝐿 ↔ (𝑀 ≤ 𝐿 ∧ 𝐿 ≤ 𝑀)))
25	23, 24	syl 14	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝐿 ∈ ℝ ∧ 𝑀 ∈ ℕ₀) → (𝑀 = 𝐿 ↔ (𝑀 ≤ 𝐿 ∧ 𝐿 ≤ 𝑀)))
26	25	biimprd 158	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝐿 ∈ ℝ ∧ 𝑀 ∈ ℕ₀) → ((𝑀 ≤ 𝐿 ∧ 𝐿 ≤ 𝑀) → 𝑀 = 𝐿))
27	26	exp4b 367	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝐿 ∈ ℝ → (𝑀 ∈ ℕ₀ → (𝑀 ≤ 𝐿 → (𝐿 ≤ 𝑀 → 𝑀 = 𝐿))))
28	27	com23 78	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝐿 ∈ ℝ → (𝑀 ≤ 𝐿 → (𝑀 ∈ ℕ₀ → (𝐿 ≤ 𝑀 → 𝑀 = 𝐿))))
29	20, 28	sylbid 150	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝐿 ∈ ℝ → (𝑀 ≤ (𝐿 + 0) → (𝑀 ∈ ℕ₀ → (𝐿 ≤ 𝑀 → 𝑀 = 𝐿))))
30	29	com3l 81	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑀 ≤ (𝐿 + 0) → (𝑀 ∈ ℕ₀ → (𝐿 ∈ ℝ → (𝐿 ≤ 𝑀 → 𝑀 = 𝐿))))
31	30	impcom 125	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑀 ∈ ℕ₀ ∧ 𝑀 ≤ (𝐿 + 0)) → (𝐿 ∈ ℝ → (𝐿 ≤ 𝑀 → 𝑀 = 𝐿)))
32	31	3adant2 1047	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑀 ∈ ℕ₀ ∧ (𝐿 + 0) ∈ ℕ₀ ∧ 𝑀 ≤ (𝐿 + 0)) → (𝐿 ∈ ℝ → (𝐿 ≤ 𝑀 → 𝑀 = 𝐿)))
33	32	com12 30	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝐿 ∈ ℝ → ((𝑀 ∈ ℕ₀ ∧ (𝐿 + 0) ∈ ℕ₀ ∧ 𝑀 ≤ (𝐿 + 0)) → (𝐿 ≤ 𝑀 → 𝑀 = 𝐿)))
34	17, 33	biimtrid 152	. . . . . . . . . . . . . . . . . 18 ⊢ (𝐿 ∈ ℝ → (𝑀 ∈ (0...(𝐿 + 0)) → (𝐿 ≤ 𝑀 → 𝑀 = 𝐿)))
35	16, 34	syl 14	. . . . . . . . . . . . . . . . 17 ⊢ (𝐿 ∈ ℕ₀ → (𝑀 ∈ (0...(𝐿 + 0)) → (𝐿 ≤ 𝑀 → 𝑀 = 𝐿)))
36	15, 35	sylbi 121	. . . . . . . . . . . . . . . 16 ⊢ ((♯‘𝐴) ∈ ℕ₀ → (𝑀 ∈ (0...(𝐿 + 0)) → (𝐿 ≤ 𝑀 → 𝑀 = 𝐿)))
37	12, 36	syl 14	. . . . . . . . . . . . . . 15 ⊢ (𝐴 ∈ Word 𝑉 → (𝑀 ∈ (0...(𝐿 + 0)) → (𝐿 ≤ 𝑀 → 𝑀 = 𝐿)))
38	37	imp 124	. . . . . . . . . . . . . 14 ⊢ ((𝐴 ∈ Word 𝑉 ∧ 𝑀 ∈ (0...(𝐿 + 0))) → (𝐿 ≤ 𝑀 → 𝑀 = 𝐿))
39		0ex 4260	. . . . . . . . . . . . . . . . . . 19 ⊢ ∅ ∈ V
40		0z 9655	. . . . . . . . . . . . . . . . . . 19 ⊢ 0 ∈ ℤ
41		swrd00g 11421	. . . . . . . . . . . . . . . . . . 19 ⊢ ((∅ ∈ V ∧ 0 ∈ ℤ) → (∅ substr ⟨0, 0⟩) = ∅)
42	39, 40, 41	mp2an 430	. . . . . . . . . . . . . . . . . 18 ⊢ (∅ substr ⟨0, 0⟩) = ∅
43	13, 12	eqeltrid 2325	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝐴 ∈ Word 𝑉 → 𝐿 ∈ ℕ₀)
44	43	nn0zd 9766	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝐴 ∈ Word 𝑉 → 𝐿 ∈ ℤ)
45		swrd00g 11421	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝐴 ∈ Word 𝑉 ∧ 𝐿 ∈ ℤ) → (𝐴 substr ⟨𝐿, 𝐿⟩) = ∅)
46	44, 45	mpdan 425	. . . . . . . . . . . . . . . . . 18 ⊢ (𝐴 ∈ Word 𝑉 → (𝐴 substr ⟨𝐿, 𝐿⟩) = ∅)
47	42, 46	eqtr4id 2290	. . . . . . . . . . . . . . . . 17 ⊢ (𝐴 ∈ Word 𝑉 → (∅ substr ⟨0, 0⟩) = (𝐴 substr ⟨𝐿, 𝐿⟩))
48		nn0cn 9573	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝐿 ∈ ℕ₀ → 𝐿 ∈ ℂ)
49	48	subidd 8625	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝐿 ∈ ℕ₀ → (𝐿 − 𝐿) = 0)
50	49	opeq1d 3910	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝐿 ∈ ℕ₀ → ⟨(𝐿 − 𝐿), 0⟩ = ⟨0, 0⟩)
51	50	oveq2d 6101	. . . . . . . . . . . . . . . . . 18 ⊢ (𝐿 ∈ ℕ₀ → (∅ substr ⟨(𝐿 − 𝐿), 0⟩) = (∅ substr ⟨0, 0⟩))
52	43, 51	syl 14	. . . . . . . . . . . . . . . . 17 ⊢ (𝐴 ∈ Word 𝑉 → (∅ substr ⟨(𝐿 − 𝐿), 0⟩) = (∅ substr ⟨0, 0⟩))
53	48	addridd 8475	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝐿 ∈ ℕ₀ → (𝐿 + 0) = 𝐿)
54	53	opeq2d 3911	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝐿 ∈ ℕ₀ → ⟨𝐿, (𝐿 + 0)⟩ = ⟨𝐿, 𝐿⟩)
55	54	oveq2d 6101	. . . . . . . . . . . . . . . . . 18 ⊢ (𝐿 ∈ ℕ₀ → (𝐴 substr ⟨𝐿, (𝐿 + 0)⟩) = (𝐴 substr ⟨𝐿, 𝐿⟩))
56	43, 55	syl 14	. . . . . . . . . . . . . . . . 17 ⊢ (𝐴 ∈ Word 𝑉 → (𝐴 substr ⟨𝐿, (𝐿 + 0)⟩) = (𝐴 substr ⟨𝐿, 𝐿⟩))
57	47, 52, 56	3eqtr4d 2281	. . . . . . . . . . . . . . . 16 ⊢ (𝐴 ∈ Word 𝑉 → (∅ substr ⟨(𝐿 − 𝐿), 0⟩) = (𝐴 substr ⟨𝐿, (𝐿 + 0)⟩))
58		oveq1 6092	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑀 = 𝐿 → (𝑀 − 𝐿) = (𝐿 − 𝐿))
59	58	opeq1d 3910	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑀 = 𝐿 → ⟨(𝑀 − 𝐿), 0⟩ = ⟨(𝐿 − 𝐿), 0⟩)
60	59	oveq2d 6101	. . . . . . . . . . . . . . . . 17 ⊢ (𝑀 = 𝐿 → (∅ substr ⟨(𝑀 − 𝐿), 0⟩) = (∅ substr ⟨(𝐿 − 𝐿), 0⟩))
61		opeq1 3904	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑀 = 𝐿 → ⟨𝑀, (𝐿 + 0)⟩ = ⟨𝐿, (𝐿 + 0)⟩)
62	61	oveq2d 6101	. . . . . . . . . . . . . . . . 17 ⊢ (𝑀 = 𝐿 → (𝐴 substr ⟨𝑀, (𝐿 + 0)⟩) = (𝐴 substr ⟨𝐿, (𝐿 + 0)⟩))
63	60, 62	eqeq12d 2253	. . . . . . . . . . . . . . . 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 10428	. . . . . . . . . . . . . . . . 17 ⊢ (𝑀 ∈ (0...(𝐿 + 0)) → 𝑀 ∈ ℤ)
70	69	adantl 277	. . . . . . . . . . . . . . . 16 ⊢ ((𝐴 ∈ Word 𝑉 ∧ 𝑀 ∈ (0...(𝐿 + 0))) → 𝑀 ∈ ℤ)
71	44	adantr 276	. . . . . . . . . . . . . . . 16 ⊢ ((𝐴 ∈ Word 𝑉 ∧ 𝑀 ∈ (0...(𝐿 + 0))) → 𝐿 ∈ ℤ)
72		swrdclg 11422	. . . . . . . . . . . . . . . 16 ⊢ ((𝐴 ∈ Word 𝑉 ∧ 𝑀 ∈ ℤ ∧ 𝐿 ∈ ℤ) → (𝐴 substr ⟨𝑀, 𝐿⟩) ∈ Word 𝑉)
73	68, 70, 71, 72	syl3anc 1278	. . . . . . . . . . . . . . 15 ⊢ ((𝐴 ∈ Word 𝑉 ∧ 𝑀 ∈ (0...(𝐿 + 0))) → (𝐴 substr ⟨𝑀, 𝐿⟩) ∈ Word 𝑉)
74		ccatrid 11375	. . . . . . . . . . . . . . 15 ⊢ ((𝐴 substr ⟨𝑀, 𝐿⟩) ∈ Word 𝑉 → ((𝐴 substr ⟨𝑀, 𝐿⟩) ++ ∅) = (𝐴 substr ⟨𝑀, 𝐿⟩))
75	73, 74	syl 14	. . . . . . . . . . . . . 14 ⊢ ((𝐴 ∈ Word 𝑉 ∧ 𝑀 ∈ (0...(𝐿 + 0))) → ((𝐴 substr ⟨𝑀, 𝐿⟩) ++ ∅) = (𝐴 substr ⟨𝑀, 𝐿⟩))
76	15, 48	sylbi 121	. . . . . . . . . . . . . . . . . . 19 ⊢ ((♯‘𝐴) ∈ ℕ₀ → 𝐿 ∈ ℂ)
77	12, 76	syl 14	. . . . . . . . . . . . . . . . . 18 ⊢ (𝐴 ∈ Word 𝑉 → 𝐿 ∈ ℂ)
78		addrid 8464	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝐿 ∈ ℂ → (𝐿 + 0) = 𝐿)
79	78	eqcomd 2244	. . . . . . . . . . . . . . . . . 18 ⊢ (𝐿 ∈ ℂ → 𝐿 = (𝐿 + 0))
80	77, 79	syl 14	. . . . . . . . . . . . . . . . 17 ⊢ (𝐴 ∈ Word 𝑉 → 𝐿 = (𝐿 + 0))
81	80	opeq2d 3911	. . . . . . . . . . . . . . . 16 ⊢ (𝐴 ∈ Word 𝑉 → ⟨𝑀, 𝐿⟩ = ⟨𝑀, (𝐿 + 0)⟩)
82	81	oveq2d 6101	. . . . . . . . . . . . . . 15 ⊢ (𝐴 ∈ Word 𝑉 → (𝐴 substr ⟨𝑀, 𝐿⟩) = (𝐴 substr ⟨𝑀, (𝐿 + 0)⟩))
83	82	adantr 276	. . . . . . . . . . . . . 14 ⊢ ((𝐴 ∈ Word 𝑉 ∧ 𝑀 ∈ (0...(𝐿 + 0))) → (𝐴 substr ⟨𝑀, 𝐿⟩) = (𝐴 substr ⟨𝑀, (𝐿 + 0)⟩))
84	75, 83	eqtrd 2271	. . . . . . . . . . . . 13 ⊢ ((𝐴 ∈ Word 𝑉 ∧ 𝑀 ∈ (0...(𝐿 + 0))) → ((𝐴 substr ⟨𝑀, 𝐿⟩) ++ ∅) = (𝐴 substr ⟨𝑀, (𝐿 + 0)⟩))
85	84	adantr 276	. . . . . . . . . . . 12 ⊢ (((𝐴 ∈ Word 𝑉 ∧ 𝑀 ∈ (0...(𝐿 + 0))) ∧ ¬ 𝐿 ≤ 𝑀) → ((𝐴 substr ⟨𝑀, 𝐿⟩) ++ ∅) = (𝐴 substr ⟨𝑀, (𝐿 + 0)⟩))
86		zdcle 9721	. . . . . . . . . . . . 13 ⊢ ((𝐿 ∈ ℤ ∧ 𝑀 ∈ ℤ) → DECID 𝐿 ≤ 𝑀)
87	44, 69, 86	syl2an 289	. . . . . . . . . . . 12 ⊢ ((𝐴 ∈ Word 𝑉 ∧ 𝑀 ∈ (0...(𝐿 + 0))) → DECID 𝐿 ≤ 𝑀)
88	67, 85, 87	ifeqdadc 3673	. . . . . . . . . . 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 496	. . . . . . . . 9 ⊢ ((((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ (♯‘𝐵) = 0) ∧ 𝐵 = ∅) → (𝑀 ∈ (0...(𝐿 + 0)) → if(𝐿 ≤ 𝑀, (∅ substr ⟨(𝑀 − 𝐿), 0⟩), ((𝐴 substr ⟨𝑀, 𝐿⟩) ++ ∅)) = (𝐴 substr ⟨𝑀, (𝐿 + 0)⟩)))
91		oveq2 6093	. . . . . . . . . . . . . 14 ⊢ ((♯‘𝐵) = 0 → (𝐿 + (♯‘𝐵)) = (𝐿 + 0))
92	91	oveq2d 6101	. . . . . . . . . . . . 13 ⊢ ((♯‘𝐵) = 0 → (0...(𝐿 + (♯‘𝐵))) = (0...(𝐿 + 0)))
93	92	eleq2d 2308	. . . . . . . . . . . 12 ⊢ ((♯‘𝐵) = 0 → (𝑀 ∈ (0...(𝐿 + (♯‘𝐵))) ↔ 𝑀 ∈ (0...(𝐿 + 0))))
94	93	adantr 276	. . . . . . . . . . 11 ⊢ (((♯‘𝐵) = 0 ∧ 𝐵 = ∅) → (𝑀 ∈ (0...(𝐿 + (♯‘𝐵))) ↔ 𝑀 ∈ (0...(𝐿 + 0))))
95		simpr 110	. . . . . . . . . . . . . 14 ⊢ (((♯‘𝐵) = 0 ∧ 𝐵 = ∅) → 𝐵 = ∅)
96		opeq2 3905	. . . . . . . . . . . . . . 15 ⊢ ((♯‘𝐵) = 0 → ⟨(𝑀 − 𝐿), (♯‘𝐵)⟩ = ⟨(𝑀 − 𝐿), 0⟩)
97	96	adantr 276	. . . . . . . . . . . . . 14 ⊢ (((♯‘𝐵) = 0 ∧ 𝐵 = ∅) → ⟨(𝑀 − 𝐿), (♯‘𝐵)⟩ = ⟨(𝑀 − 𝐿), 0⟩)
98	95, 97	oveq12d 6103	. . . . . . . . . . . . 13 ⊢ (((♯‘𝐵) = 0 ∧ 𝐵 = ∅) → (𝐵 substr ⟨(𝑀 − 𝐿), (♯‘𝐵)⟩) = (∅ substr ⟨(𝑀 − 𝐿), 0⟩))
99		oveq2 6093	. . . . . . . . . . . . . 14 ⊢ (𝐵 = ∅ → ((𝐴 substr ⟨𝑀, 𝐿⟩) ++ 𝐵) = ((𝐴 substr ⟨𝑀, 𝐿⟩) ++ ∅))
100	99	adantl 277	. . . . . . . . . . . . 13 ⊢ (((♯‘𝐵) = 0 ∧ 𝐵 = ∅) → ((𝐴 substr ⟨𝑀, 𝐿⟩) ++ 𝐵) = ((𝐴 substr ⟨𝑀, 𝐿⟩) ++ ∅))
101	98, 100	ifeq12d 3660	. . . . . . . . . . . 12 ⊢ (((♯‘𝐵) = 0 ∧ 𝐵 = ∅) → if(𝐿 ≤ 𝑀, (𝐵 substr ⟨(𝑀 − 𝐿), (♯‘𝐵)⟩), ((𝐴 substr ⟨𝑀, 𝐿⟩) ++ 𝐵)) = if(𝐿 ≤ 𝑀, (∅ substr ⟨(𝑀 − 𝐿), 0⟩), ((𝐴 substr ⟨𝑀, 𝐿⟩) ++ ∅)))
102	91	opeq2d 3911	. . . . . . . . . . . . . 14 ⊢ ((♯‘𝐵) = 0 → ⟨𝑀, (𝐿 + (♯‘𝐵))⟩ = ⟨𝑀, (𝐿 + 0)⟩)
103	102	oveq2d 6101	. . . . . . . . . . . . 13 ⊢ ((♯‘𝐵) = 0 → (𝐴 substr ⟨𝑀, (𝐿 + (♯‘𝐵))⟩) = (𝐴 substr ⟨𝑀, (𝐿 + 0)⟩))
104	103	adantr 276	. . . . . . . . . . . 12 ⊢ (((♯‘𝐵) = 0 ∧ 𝐵 = ∅) → (𝐴 substr ⟨𝑀, (𝐿 + (♯‘𝐵))⟩) = (𝐴 substr ⟨𝑀, (𝐿 + 0)⟩))
105	101, 104	eqeq12d 2253	. . . . . . . . . . 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 480	. . . . . . . . 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 425	. . . . . . 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 2304	. . . . . . . 8 ⊢ (𝐿 ∈ ℕ₀ ↔ (♯‘𝐴) ∈ ℕ₀)
116	115, 16	sylbir 135	. . . . . . 7 ⊢ ((♯‘𝐴) ∈ ℕ₀ → 𝐿 ∈ ℝ)
117	12, 116	syl 14	. . . . . 6 ⊢ (𝐴 ∈ Word 𝑉 → 𝐿 ∈ ℝ)
118	1	nn0red 9621	. . . . . 6 ⊢ (𝐵 ∈ Word 𝑉 → (♯‘𝐵) ∈ ℝ)
119		leaddle0 8805	. . . . . 6 ⊢ ((𝐿 ∈ ℝ ∧ (♯‘𝐵) ∈ ℝ) → ((𝐿 + (♯‘𝐵)) ≤ 𝐿 ↔ (♯‘𝐵) ≤ 0))
120	117, 118, 119	syl2an 289	. . . . 5 ⊢ ((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) → ((𝐿 + (♯‘𝐵)) ≤ 𝐿 ↔ (♯‘𝐵) ≤ 0))
121		pm2.24 630	. . . . 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 497	. . . . 5 ⊢ ((((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ 𝑀 ∈ (0...(𝐿 + (♯‘𝐵)))) ∧ (𝐿 + (♯‘𝐵)) ≤ 𝐿) → (♯‘𝐵) ∈ ℕ₀)
126	125	nn0zd 9766	. . . 4 ⊢ ((((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ 𝑀 ∈ (0...(𝐿 + (♯‘𝐵)))) ∧ (𝐿 + (♯‘𝐵)) ≤ 𝐿) → (♯‘𝐵) ∈ ℤ)
127		zdcle 9721	. . . 4 ⊢ (((♯‘𝐵) ∈ ℤ ∧ 0 ∈ ℤ) → DECID (♯‘𝐵) ≤ 0)
128	126, 40, 127	sylancl 417	. . 3 ⊢ ((((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ 𝑀 ∈ (0...(𝐿 + (♯‘𝐵)))) ∧ (𝐿 + (♯‘𝐵)) ≤ 𝐿) → DECID (♯‘𝐵) ≤ 0)
129		exmiddc 848	. . 3 ⊢ (DECID (♯‘𝐵) ≤ 0 → ((♯‘𝐵) ≤ 0 ∨ ¬ (♯‘𝐵) ≤ 0))
130	128, 129	syl 14	. 2 ⊢ ((((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ 𝑀 ∈ (0...(𝐿 + (♯‘𝐵)))) ∧ (𝐿 + (♯‘𝐵)) ≤ 𝐿) → ((♯‘𝐵) ≤ 0 ∨ ¬ (♯‘𝐵) ≤ 0))
131	114, 124, 130	mpjaod 730	1 ⊢ ((((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ 𝑀 ∈ (0...(𝐿 + (♯‘𝐵)))) ∧ (𝐿 + (♯‘𝐵)) ≤ 𝐿) → if(𝐿 ≤ 𝑀, (𝐵 substr ⟨(𝑀 − 𝐿), (♯‘𝐵)⟩), ((𝐴 substr ⟨𝑀, 𝐿⟩) ++ 𝐵)) = (𝐴 substr ⟨𝑀, (𝐿 + (♯‘𝐵))⟩))

Colors of variables: wff set class

This proof depends on syntax axioms: ¬ wn 3 → wi 4 ∧ wa 104 ↔ wb 105 ∨ wo 720 DECID wdc 846 ∧ w3a 1009 = wceq 1402 ∈ wcel 2209 Vcvv 2821 ∅c0 3520 ifcif 3638 ⟨cop 3712 class class class wbr 4130 ‘cfv 5377 (class class class)co 6085 Fincfn 7022 ℂcc 8177 ℝcr 8178 0cc0 8179 + caddc 8182 ≤ cle 8361 − cmin 8497 ℕ₀cn0 9563 ℤcz 9644 ...cfz 10411 ♯chash 11214 Word cword 11304 ++ cconcat 11358 substr csubstr 11417

This proof depends on axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 106 ax-ia2 107 ax-ia3 108 ax-in1 623 ax-in2 624 ax-io 721 ax-5 1500 ax-7 1501 ax-gen 1502 ax-ie1 1546 ax-ie2 1547 ax-8 1557 ax-10 1558 ax-11 1559 ax-i12 1560 ax-bndl 1562 ax-4 1563 ax-17 1579 ax-i9 1583 ax-ial 1587 ax-i5r 1588 ax-14 2212 ax-ext 2220 ax-coll 4246 ax-sep 4249 ax-nul 4259 ax-pow 4311 ax-pr 4346 ax-un 4578 ax-setind 4684 ax-iinf 4735 ax-cnex 8270 ax-resscn 8271 ax-1cn 8272 ax-1re 8273 ax-icn 8274 ax-addcl 8275 ax-addrcl 8276 ax-mulcl 8277 ax-addcom 8279 ax-addass 8281 ax-distr 8283 ax-i2m1 8284 ax-0lt1 8285 ax-0id 8287 ax-rnegex 8288 ax-cnre 8290 ax-pre-ltirr 8291 ax-pre-ltwlin 8292 ax-pre-lttrn 8293 ax-pre-apti 8294 ax-pre-ltadd 8295

This proof depends on definitions: df-bi 117 df-dc 847 df-3or 1010 df-3an 1011 df-tru 1405 df-fal 1408 df-nf 1514 df-sb 1816 df-eu 2089 df-mo 2090 df-clab 2225 df-cleq 2231 df-clel 2234 df-nfc 2381 df-ne 2421 df-nel 2516 df-ral 2533 df-rex 2534 df-reu 2535 df-rab 2537 df-v 2823 df-sbc 3052 df-csb 3148 df-dif 3222 df-un 3224 df-in 3226 df-ss 3233 df-nul 3521 df-if 3639 df-pw 3690 df-sn 3715 df-pr 3716 df-op 3718 df-uni 3936 df-int 3971 df-iun 4014 df-br 4131 df-opab 4193 df-mpt 4194 df-tr 4230 df-id 4438 df-iord 4511 df-on 4513 df-ilim 4514 df-suc 4516 df-iom 4738 df-xp 4780 df-rel 4781 df-cnv 4782 df-co 4783 df-dm 4784 df-rn 4785 df-res 4786 df-ima 4787 df-iota 5337 df-fun 5379 df-fn 5380 df-f 5381 df-f1 5382 df-fo 5383 df-f1o 5384 df-fv 5385 df-riota 6038 df-ov 6088 df-oprab 6089 df-mpo 6090 df-1st 6374 df-2nd 6375 df-recs 6576 df-frec 6662 df-1o 6687 df-er 6807 df-en 7023 df-dom 7024 df-fin 7025 df-pnf 8362 df-mnf 8363 df-xr 8364 df-ltxr 8365 df-le 8366 df-sub 8499 df-neg 8500 df-inn 9305 df-n0 9564 df-z 9645 df-uz 9922 df-fz 10412 df-fzo 10550 df-ihash 11215 df-word 11305 df-concat 11359 df-substr 11418

This theorem is used by: swrdccat3b 11512

W3C validator