ccatalpha - Intuitionistic Logic Explorer

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

Theorem ccatalpha 11161

Description: A concatenation of two arbitrary words is a word over an alphabet iff the symbols of both words belong to the alphabet. (Contributed by AV, 28-Feb-2021.)

**Assertion**
Ref	Expression
ccatalpha	⊢ ((𝐴 ∈ Word V ∧ 𝐵 ∈ Word V) → ((𝐴 ++ 𝐵) ∈ Word 𝑆 ↔ (𝐴 ∈ Word 𝑆 ∧ 𝐵 ∈ Word 𝑆)))

Proof of Theorem ccatalpha Dummy variables 𝑥 𝑦 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		wrdfin 11103	. . . . 5 ⊢ (𝐴 ∈ Word V → 𝐴 ∈ Fin)
2		wrdfin 11103	. . . . 5 ⊢ (𝐵 ∈ Word V → 𝐵 ∈ Fin)
3		ccatfvalfi 11140	. . . . 5 ⊢ ((𝐴 ∈ Fin ∧ 𝐵 ∈ Fin) → (𝐴 ++ 𝐵) = (𝑥 ∈ (0..^((♯‘𝐴) + (♯‘𝐵))) ↦ if(𝑥 ∈ (0..^(♯‘𝐴)), (𝐴‘𝑥), (𝐵‘(𝑥 − (♯‘𝐴))))))
4	1, 2, 3	syl2an 289	. . . 4 ⊢ ((𝐴 ∈ Word V ∧ 𝐵 ∈ Word V) → (𝐴 ++ 𝐵) = (𝑥 ∈ (0..^((♯‘𝐴) + (♯‘𝐵))) ↦ if(𝑥 ∈ (0..^(♯‘𝐴)), (𝐴‘𝑥), (𝐵‘(𝑥 − (♯‘𝐴))))))
5	4	eleq1d 2298	. . 3 ⊢ ((𝐴 ∈ Word V ∧ 𝐵 ∈ Word V) → ((𝐴 ++ 𝐵) ∈ Word 𝑆 ↔ (𝑥 ∈ (0..^((♯‘𝐴) + (♯‘𝐵))) ↦ if(𝑥 ∈ (0..^(♯‘𝐴)), (𝐴‘𝑥), (𝐵‘(𝑥 − (♯‘𝐴))))) ∈ Word 𝑆))
6		wrdf 11090	. . . 4 ⊢ ((𝑥 ∈ (0..^((♯‘𝐴) + (♯‘𝐵))) ↦ if(𝑥 ∈ (0..^(♯‘𝐴)), (𝐴‘𝑥), (𝐵‘(𝑥 − (♯‘𝐴))))) ∈ Word 𝑆 → (𝑥 ∈ (0..^((♯‘𝐴) + (♯‘𝐵))) ↦ if(𝑥 ∈ (0..^(♯‘𝐴)), (𝐴‘𝑥), (𝐵‘(𝑥 − (♯‘𝐴))))):(0..^(♯‘(𝑥 ∈ (0..^((♯‘𝐴) + (♯‘𝐵))) ↦ if(𝑥 ∈ (0..^(♯‘𝐴)), (𝐴‘𝑥), (𝐵‘(𝑥 − (♯‘𝐴)))))))⟶𝑆)
7		funmpt 5356	. . . . . . . . . . 11 ⊢ Fun (𝑥 ∈ (0..^((♯‘𝐴) + (♯‘𝐵))) ↦ if(𝑥 ∈ (0..^(♯‘𝐴)), (𝐴‘𝑥), (𝐵‘(𝑥 − (♯‘𝐴)))))
8	7	a1i 9	. . . . . . . . . 10 ⊢ ((𝐴 ∈ Word V ∧ 𝐵 ∈ Word V) → Fun (𝑥 ∈ (0..^((♯‘𝐴) + (♯‘𝐵))) ↦ if(𝑥 ∈ (0..^(♯‘𝐴)), (𝐴‘𝑥), (𝐵‘(𝑥 − (♯‘𝐴))))))
9	8	funfnd 5349	. . . . . . . . 9 ⊢ ((𝐴 ∈ Word V ∧ 𝐵 ∈ Word V) → (𝑥 ∈ (0..^((♯‘𝐴) + (♯‘𝐵))) ↦ if(𝑥 ∈ (0..^(♯‘𝐴)), (𝐴‘𝑥), (𝐵‘(𝑥 − (♯‘𝐴))))) Fn dom (𝑥 ∈ (0..^((♯‘𝐴) + (♯‘𝐵))) ↦ if(𝑥 ∈ (0..^(♯‘𝐴)), (𝐴‘𝑥), (𝐵‘(𝑥 − (♯‘𝐴))))))
10		eqid 2229	. . . . . . . . . . 11 ⊢ (𝑥 ∈ (0..^((♯‘𝐴) + (♯‘𝐵))) ↦ if(𝑥 ∈ (0..^(♯‘𝐴)), (𝐴‘𝑥), (𝐵‘(𝑥 − (♯‘𝐴))))) = (𝑥 ∈ (0..^((♯‘𝐴) + (♯‘𝐵))) ↦ if(𝑥 ∈ (0..^(♯‘𝐴)), (𝐴‘𝑥), (𝐵‘(𝑥 − (♯‘𝐴)))))
11		fvexg 5648	. . . . . . . . . . . . 13 ⊢ ((𝐴 ∈ Word V ∧ 𝑥 ∈ (0..^((♯‘𝐴) + (♯‘𝐵)))) → (𝐴‘𝑥) ∈ V)
12	11	adantlr 477	. . . . . . . . . . . 12 ⊢ (((𝐴 ∈ Word V ∧ 𝐵 ∈ Word V) ∧ 𝑥 ∈ (0..^((♯‘𝐴) + (♯‘𝐵)))) → (𝐴‘𝑥) ∈ V)
13		simplr 528	. . . . . . . . . . . . 13 ⊢ (((𝐴 ∈ Word V ∧ 𝐵 ∈ Word V) ∧ 𝑥 ∈ (0..^((♯‘𝐴) + (♯‘𝐵)))) → 𝐵 ∈ Word V)
14		elfzoelz 10355	. . . . . . . . . . . . . . 15 ⊢ (𝑥 ∈ (0..^((♯‘𝐴) + (♯‘𝐵))) → 𝑥 ∈ ℤ)
15	14	adantl 277	. . . . . . . . . . . . . 14 ⊢ (((𝐴 ∈ Word V ∧ 𝐵 ∈ Word V) ∧ 𝑥 ∈ (0..^((♯‘𝐴) + (♯‘𝐵)))) → 𝑥 ∈ ℤ)
16		simpll 527	. . . . . . . . . . . . . . 15 ⊢ (((𝐴 ∈ Word V ∧ 𝐵 ∈ Word V) ∧ 𝑥 ∈ (0..^((♯‘𝐴) + (♯‘𝐵)))) → 𝐴 ∈ Word V)
17		lencl 11088	. . . . . . . . . . . . . . . 16 ⊢ (𝐴 ∈ Word V → (♯‘𝐴) ∈ ℕ₀)
18	17	nn0zd 9578	. . . . . . . . . . . . . . 15 ⊢ (𝐴 ∈ Word V → (♯‘𝐴) ∈ ℤ)
19	16, 18	syl 14	. . . . . . . . . . . . . 14 ⊢ (((𝐴 ∈ Word V ∧ 𝐵 ∈ Word V) ∧ 𝑥 ∈ (0..^((♯‘𝐴) + (♯‘𝐵)))) → (♯‘𝐴) ∈ ℤ)
20	15, 19	zsubcld 9585	. . . . . . . . . . . . 13 ⊢ (((𝐴 ∈ Word V ∧ 𝐵 ∈ Word V) ∧ 𝑥 ∈ (0..^((♯‘𝐴) + (♯‘𝐵)))) → (𝑥 − (♯‘𝐴)) ∈ ℤ)
21		fvexg 5648	. . . . . . . . . . . . 13 ⊢ ((𝐵 ∈ Word V ∧ (𝑥 − (♯‘𝐴)) ∈ ℤ) → (𝐵‘(𝑥 − (♯‘𝐴))) ∈ V)
22	13, 20, 21	syl2anc 411	. . . . . . . . . . . 12 ⊢ (((𝐴 ∈ Word V ∧ 𝐵 ∈ Word V) ∧ 𝑥 ∈ (0..^((♯‘𝐴) + (♯‘𝐵)))) → (𝐵‘(𝑥 − (♯‘𝐴))) ∈ V)
23	12, 22	ifexd 4575	. . . . . . . . . . 11 ⊢ (((𝐴 ∈ Word V ∧ 𝐵 ∈ Word V) ∧ 𝑥 ∈ (0..^((♯‘𝐴) + (♯‘𝐵)))) → if(𝑥 ∈ (0..^(♯‘𝐴)), (𝐴‘𝑥), (𝐵‘(𝑥 − (♯‘𝐴)))) ∈ V)
24	10, 23	dmmptd 5454	. . . . . . . . . 10 ⊢ ((𝐴 ∈ Word V ∧ 𝐵 ∈ Word V) → dom (𝑥 ∈ (0..^((♯‘𝐴) + (♯‘𝐵))) ↦ if(𝑥 ∈ (0..^(♯‘𝐴)), (𝐴‘𝑥), (𝐵‘(𝑥 − (♯‘𝐴))))) = (0..^((♯‘𝐴) + (♯‘𝐵))))
25		0z 9468	. . . . . . . . . . 11 ⊢ 0 ∈ ℤ
26	17	adantr 276	. . . . . . . . . . . . 13 ⊢ ((𝐴 ∈ Word V ∧ 𝐵 ∈ Word V) → (♯‘𝐴) ∈ ℕ₀)
27		lencl 11088	. . . . . . . . . . . . . 14 ⊢ (𝐵 ∈ Word V → (♯‘𝐵) ∈ ℕ₀)
28	27	adantl 277	. . . . . . . . . . . . 13 ⊢ ((𝐴 ∈ Word V ∧ 𝐵 ∈ Word V) → (♯‘𝐵) ∈ ℕ₀)
29	26, 28	nn0addcld 9437	. . . . . . . . . . . 12 ⊢ ((𝐴 ∈ Word V ∧ 𝐵 ∈ Word V) → ((♯‘𝐴) + (♯‘𝐵)) ∈ ℕ₀)
30	29	nn0zd 9578	. . . . . . . . . . 11 ⊢ ((𝐴 ∈ Word V ∧ 𝐵 ∈ Word V) → ((♯‘𝐴) + (♯‘𝐵)) ∈ ℤ)
31		fzofig 10666	. . . . . . . . . . 11 ⊢ ((0 ∈ ℤ ∧ ((♯‘𝐴) + (♯‘𝐵)) ∈ ℤ) → (0..^((♯‘𝐴) + (♯‘𝐵))) ∈ Fin)
32	25, 30, 31	sylancr 414	. . . . . . . . . 10 ⊢ ((𝐴 ∈ Word V ∧ 𝐵 ∈ Word V) → (0..^((♯‘𝐴) + (♯‘𝐵))) ∈ Fin)
33	24, 32	eqeltrd 2306	. . . . . . . . 9 ⊢ ((𝐴 ∈ Word V ∧ 𝐵 ∈ Word V) → dom (𝑥 ∈ (0..^((♯‘𝐴) + (♯‘𝐵))) ↦ if(𝑥 ∈ (0..^(♯‘𝐴)), (𝐴‘𝑥), (𝐵‘(𝑥 − (♯‘𝐴))))) ∈ Fin)
34		fihashfn 11034	. . . . . . . . 9 ⊢ (((𝑥 ∈ (0..^((♯‘𝐴) + (♯‘𝐵))) ↦ if(𝑥 ∈ (0..^(♯‘𝐴)), (𝐴‘𝑥), (𝐵‘(𝑥 − (♯‘𝐴))))) Fn dom (𝑥 ∈ (0..^((♯‘𝐴) + (♯‘𝐵))) ↦ if(𝑥 ∈ (0..^(♯‘𝐴)), (𝐴‘𝑥), (𝐵‘(𝑥 − (♯‘𝐴))))) ∧ dom (𝑥 ∈ (0..^((♯‘𝐴) + (♯‘𝐵))) ↦ if(𝑥 ∈ (0..^(♯‘𝐴)), (𝐴‘𝑥), (𝐵‘(𝑥 − (♯‘𝐴))))) ∈ Fin) → (♯‘(𝑥 ∈ (0..^((♯‘𝐴) + (♯‘𝐵))) ↦ if(𝑥 ∈ (0..^(♯‘𝐴)), (𝐴‘𝑥), (𝐵‘(𝑥 − (♯‘𝐴)))))) = (♯‘dom (𝑥 ∈ (0..^((♯‘𝐴) + (♯‘𝐵))) ↦ if(𝑥 ∈ (0..^(♯‘𝐴)), (𝐴‘𝑥), (𝐵‘(𝑥 − (♯‘𝐴)))))))
35	9, 33, 34	syl2anc 411	. . . . . . . 8 ⊢ ((𝐴 ∈ Word V ∧ 𝐵 ∈ Word V) → (♯‘(𝑥 ∈ (0..^((♯‘𝐴) + (♯‘𝐵))) ↦ if(𝑥 ∈ (0..^(♯‘𝐴)), (𝐴‘𝑥), (𝐵‘(𝑥 − (♯‘𝐴)))))) = (♯‘dom (𝑥 ∈ (0..^((♯‘𝐴) + (♯‘𝐵))) ↦ if(𝑥 ∈ (0..^(♯‘𝐴)), (𝐴‘𝑥), (𝐵‘(𝑥 − (♯‘𝐴)))))))
36	24	fveq2d 5633	. . . . . . . 8 ⊢ ((𝐴 ∈ Word V ∧ 𝐵 ∈ Word V) → (♯‘dom (𝑥 ∈ (0..^((♯‘𝐴) + (♯‘𝐵))) ↦ if(𝑥 ∈ (0..^(♯‘𝐴)), (𝐴‘𝑥), (𝐵‘(𝑥 − (♯‘𝐴)))))) = (♯‘(0..^((♯‘𝐴) + (♯‘𝐵)))))
37		nn0addcl 9415	. . . . . . . . . 10 ⊢ (((♯‘𝐴) ∈ ℕ₀ ∧ (♯‘𝐵) ∈ ℕ₀) → ((♯‘𝐴) + (♯‘𝐵)) ∈ ℕ₀)
38	17, 27, 37	syl2an 289	. . . . . . . . 9 ⊢ ((𝐴 ∈ Word V ∧ 𝐵 ∈ Word V) → ((♯‘𝐴) + (♯‘𝐵)) ∈ ℕ₀)
39		hashfzo0 11058	. . . . . . . . 9 ⊢ (((♯‘𝐴) + (♯‘𝐵)) ∈ ℕ₀ → (♯‘(0..^((♯‘𝐴) + (♯‘𝐵)))) = ((♯‘𝐴) + (♯‘𝐵)))
40	38, 39	syl 14	. . . . . . . 8 ⊢ ((𝐴 ∈ Word V ∧ 𝐵 ∈ Word V) → (♯‘(0..^((♯‘𝐴) + (♯‘𝐵)))) = ((♯‘𝐴) + (♯‘𝐵)))
41	35, 36, 40	3eqtrd 2266	. . . . . . 7 ⊢ ((𝐴 ∈ Word V ∧ 𝐵 ∈ Word V) → (♯‘(𝑥 ∈ (0..^((♯‘𝐴) + (♯‘𝐵))) ↦ if(𝑥 ∈ (0..^(♯‘𝐴)), (𝐴‘𝑥), (𝐵‘(𝑥 − (♯‘𝐴)))))) = ((♯‘𝐴) + (♯‘𝐵)))
42	41	oveq2d 6023	. . . . . 6 ⊢ ((𝐴 ∈ Word V ∧ 𝐵 ∈ Word V) → (0..^(♯‘(𝑥 ∈ (0..^((♯‘𝐴) + (♯‘𝐵))) ↦ if(𝑥 ∈ (0..^(♯‘𝐴)), (𝐴‘𝑥), (𝐵‘(𝑥 − (♯‘𝐴))))))) = (0..^((♯‘𝐴) + (♯‘𝐵))))
43	42	feq2d 5461	. . . . 5 ⊢ ((𝐴 ∈ Word V ∧ 𝐵 ∈ Word V) → ((𝑥 ∈ (0..^((♯‘𝐴) + (♯‘𝐵))) ↦ if(𝑥 ∈ (0..^(♯‘𝐴)), (𝐴‘𝑥), (𝐵‘(𝑥 − (♯‘𝐴))))):(0..^(♯‘(𝑥 ∈ (0..^((♯‘𝐴) + (♯‘𝐵))) ↦ if(𝑥 ∈ (0..^(♯‘𝐴)), (𝐴‘𝑥), (𝐵‘(𝑥 − (♯‘𝐴)))))))⟶𝑆 ↔ (𝑥 ∈ (0..^((♯‘𝐴) + (♯‘𝐵))) ↦ if(𝑥 ∈ (0..^(♯‘𝐴)), (𝐴‘𝑥), (𝐵‘(𝑥 − (♯‘𝐴))))):(0..^((♯‘𝐴) + (♯‘𝐵)))⟶𝑆))
44	10	fmpt 5787	. . . . . 6 ⊢ (∀𝑥 ∈ (0..^((♯‘𝐴) + (♯‘𝐵)))if(𝑥 ∈ (0..^(♯‘𝐴)), (𝐴‘𝑥), (𝐵‘(𝑥 − (♯‘𝐴)))) ∈ 𝑆 ↔ (𝑥 ∈ (0..^((♯‘𝐴) + (♯‘𝐵))) ↦ if(𝑥 ∈ (0..^(♯‘𝐴)), (𝐴‘𝑥), (𝐵‘(𝑥 − (♯‘𝐴))))):(0..^((♯‘𝐴) + (♯‘𝐵)))⟶𝑆)
45		simpl 109	. . . . . . . . 9 ⊢ ((𝐴 ∈ Word V ∧ 𝐵 ∈ Word V) → 𝐴 ∈ Word V)
46		nn0cn 9390	. . . . . . . . . . . . . . . . . 18 ⊢ ((♯‘𝐴) ∈ ℕ₀ → (♯‘𝐴) ∈ ℂ)
47		nn0cn 9390	. . . . . . . . . . . . . . . . . 18 ⊢ ((♯‘𝐵) ∈ ℕ₀ → (♯‘𝐵) ∈ ℂ)
48		addcom 8294	. . . . . . . . . . . . . . . . . 18 ⊢ (((♯‘𝐴) ∈ ℂ ∧ (♯‘𝐵) ∈ ℂ) → ((♯‘𝐴) + (♯‘𝐵)) = ((♯‘𝐵) + (♯‘𝐴)))
49	46, 47, 48	syl2an 289	. . . . . . . . . . . . . . . . 17 ⊢ (((♯‘𝐴) ∈ ℕ₀ ∧ (♯‘𝐵) ∈ ℕ₀) → ((♯‘𝐴) + (♯‘𝐵)) = ((♯‘𝐵) + (♯‘𝐴)))
50		nn0z 9477	. . . . . . . . . . . . . . . . . . 19 ⊢ ((♯‘𝐴) ∈ ℕ₀ → (♯‘𝐴) ∈ ℤ)
51	50	anim1ci 341	. . . . . . . . . . . . . . . . . 18 ⊢ (((♯‘𝐴) ∈ ℕ₀ ∧ (♯‘𝐵) ∈ ℕ₀) → ((♯‘𝐵) ∈ ℕ₀ ∧ (♯‘𝐴) ∈ ℤ))
52		nn0pzuz 9794	. . . . . . . . . . . . . . . . . 18 ⊢ (((♯‘𝐵) ∈ ℕ₀ ∧ (♯‘𝐴) ∈ ℤ) → ((♯‘𝐵) + (♯‘𝐴)) ∈ (ℤ_≥‘(♯‘𝐴)))
53	51, 52	syl 14	. . . . . . . . . . . . . . . . 17 ⊢ (((♯‘𝐴) ∈ ℕ₀ ∧ (♯‘𝐵) ∈ ℕ₀) → ((♯‘𝐵) + (♯‘𝐴)) ∈ (ℤ_≥‘(♯‘𝐴)))
54	49, 53	eqeltrd 2306	. . . . . . . . . . . . . . . 16 ⊢ (((♯‘𝐴) ∈ ℕ₀ ∧ (♯‘𝐵) ∈ ℕ₀) → ((♯‘𝐴) + (♯‘𝐵)) ∈ (ℤ_≥‘(♯‘𝐴)))
55	17, 27, 54	syl2an 289	. . . . . . . . . . . . . . 15 ⊢ ((𝐴 ∈ Word V ∧ 𝐵 ∈ Word V) → ((♯‘𝐴) + (♯‘𝐵)) ∈ (ℤ_≥‘(♯‘𝐴)))
56		fzoss2 10382	. . . . . . . . . . . . . . 15 ⊢ (((♯‘𝐴) + (♯‘𝐵)) ∈ (ℤ_≥‘(♯‘𝐴)) → (0..^(♯‘𝐴)) ⊆ (0..^((♯‘𝐴) + (♯‘𝐵))))
57	55, 56	syl 14	. . . . . . . . . . . . . 14 ⊢ ((𝐴 ∈ Word V ∧ 𝐵 ∈ Word V) → (0..^(♯‘𝐴)) ⊆ (0..^((♯‘𝐴) + (♯‘𝐵))))
58	57	sselda 3224	. . . . . . . . . . . . 13 ⊢ (((𝐴 ∈ Word V ∧ 𝐵 ∈ Word V) ∧ 𝑦 ∈ (0..^(♯‘𝐴))) → 𝑦 ∈ (0..^((♯‘𝐴) + (♯‘𝐵))))
59		eleq1 2292	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 = 𝑦 → (𝑥 ∈ (0..^(♯‘𝐴)) ↔ 𝑦 ∈ (0..^(♯‘𝐴))))
60		fveq2 5629	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 = 𝑦 → (𝐴‘𝑥) = (𝐴‘𝑦))
61		fvoveq1 6030	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 = 𝑦 → (𝐵‘(𝑥 − (♯‘𝐴))) = (𝐵‘(𝑦 − (♯‘𝐴))))
62	59, 60, 61	ifbieq12d 3629	. . . . . . . . . . . . . . 15 ⊢ (𝑥 = 𝑦 → if(𝑥 ∈ (0..^(♯‘𝐴)), (𝐴‘𝑥), (𝐵‘(𝑥 − (♯‘𝐴)))) = if(𝑦 ∈ (0..^(♯‘𝐴)), (𝐴‘𝑦), (𝐵‘(𝑦 − (♯‘𝐴)))))
63	62	eleq1d 2298	. . . . . . . . . . . . . 14 ⊢ (𝑥 = 𝑦 → (if(𝑥 ∈ (0..^(♯‘𝐴)), (𝐴‘𝑥), (𝐵‘(𝑥 − (♯‘𝐴)))) ∈ 𝑆 ↔ if(𝑦 ∈ (0..^(♯‘𝐴)), (𝐴‘𝑦), (𝐵‘(𝑦 − (♯‘𝐴)))) ∈ 𝑆))
64	63	rspcv 2903	. . . . . . . . . . . . 13 ⊢ (𝑦 ∈ (0..^((♯‘𝐴) + (♯‘𝐵))) → (∀𝑥 ∈ (0..^((♯‘𝐴) + (♯‘𝐵)))if(𝑥 ∈ (0..^(♯‘𝐴)), (𝐴‘𝑥), (𝐵‘(𝑥 − (♯‘𝐴)))) ∈ 𝑆 → if(𝑦 ∈ (0..^(♯‘𝐴)), (𝐴‘𝑦), (𝐵‘(𝑦 − (♯‘𝐴)))) ∈ 𝑆))
65	58, 64	syl 14	. . . . . . . . . . . 12 ⊢ (((𝐴 ∈ Word V ∧ 𝐵 ∈ Word V) ∧ 𝑦 ∈ (0..^(♯‘𝐴))) → (∀𝑥 ∈ (0..^((♯‘𝐴) + (♯‘𝐵)))if(𝑥 ∈ (0..^(♯‘𝐴)), (𝐴‘𝑥), (𝐵‘(𝑥 − (♯‘𝐴)))) ∈ 𝑆 → if(𝑦 ∈ (0..^(♯‘𝐴)), (𝐴‘𝑦), (𝐵‘(𝑦 − (♯‘𝐴)))) ∈ 𝑆))
66		iftrue 3607	. . . . . . . . . . . . . 14 ⊢ (𝑦 ∈ (0..^(♯‘𝐴)) → if(𝑦 ∈ (0..^(♯‘𝐴)), (𝐴‘𝑦), (𝐵‘(𝑦 − (♯‘𝐴)))) = (𝐴‘𝑦))
67	66	adantl 277	. . . . . . . . . . . . 13 ⊢ (((𝐴 ∈ Word V ∧ 𝐵 ∈ Word V) ∧ 𝑦 ∈ (0..^(♯‘𝐴))) → if(𝑦 ∈ (0..^(♯‘𝐴)), (𝐴‘𝑦), (𝐵‘(𝑦 − (♯‘𝐴)))) = (𝐴‘𝑦))
68	67	eleq1d 2298	. . . . . . . . . . . 12 ⊢ (((𝐴 ∈ Word V ∧ 𝐵 ∈ Word V) ∧ 𝑦 ∈ (0..^(♯‘𝐴))) → (if(𝑦 ∈ (0..^(♯‘𝐴)), (𝐴‘𝑦), (𝐵‘(𝑦 − (♯‘𝐴)))) ∈ 𝑆 ↔ (𝐴‘𝑦) ∈ 𝑆))
69	65, 68	sylibd 149	. . . . . . . . . . 11 ⊢ (((𝐴 ∈ Word V ∧ 𝐵 ∈ Word V) ∧ 𝑦 ∈ (0..^(♯‘𝐴))) → (∀𝑥 ∈ (0..^((♯‘𝐴) + (♯‘𝐵)))if(𝑥 ∈ (0..^(♯‘𝐴)), (𝐴‘𝑥), (𝐵‘(𝑥 − (♯‘𝐴)))) ∈ 𝑆 → (𝐴‘𝑦) ∈ 𝑆))
70	69	impancom 260	. . . . . . . . . 10 ⊢ (((𝐴 ∈ Word V ∧ 𝐵 ∈ Word V) ∧ ∀𝑥 ∈ (0..^((♯‘𝐴) + (♯‘𝐵)))if(𝑥 ∈ (0..^(♯‘𝐴)), (𝐴‘𝑥), (𝐵‘(𝑥 − (♯‘𝐴)))) ∈ 𝑆) → (𝑦 ∈ (0..^(♯‘𝐴)) → (𝐴‘𝑦) ∈ 𝑆))
71	70	ralrimiv 2602	. . . . . . . . 9 ⊢ (((𝐴 ∈ Word V ∧ 𝐵 ∈ Word V) ∧ ∀𝑥 ∈ (0..^((♯‘𝐴) + (♯‘𝐵)))if(𝑥 ∈ (0..^(♯‘𝐴)), (𝐴‘𝑥), (𝐵‘(𝑥 − (♯‘𝐴)))) ∈ 𝑆) → ∀𝑦 ∈ (0..^(♯‘𝐴))(𝐴‘𝑦) ∈ 𝑆)
72		iswrdsymb 11102	. . . . . . . . 9 ⊢ ((𝐴 ∈ Word V ∧ ∀𝑦 ∈ (0..^(♯‘𝐴))(𝐴‘𝑦) ∈ 𝑆) → 𝐴 ∈ Word 𝑆)
73	45, 71, 72	syl2an2r 597	. . . . . . . 8 ⊢ (((𝐴 ∈ Word V ∧ 𝐵 ∈ Word V) ∧ ∀𝑥 ∈ (0..^((♯‘𝐴) + (♯‘𝐵)))if(𝑥 ∈ (0..^(♯‘𝐴)), (𝐴‘𝑥), (𝐵‘(𝑥 − (♯‘𝐴)))) ∈ 𝑆) → 𝐴 ∈ Word 𝑆)
74		simpr 110	. . . . . . . . 9 ⊢ ((𝐴 ∈ Word V ∧ 𝐵 ∈ Word V) → 𝐵 ∈ Word V)
75		simpr 110	. . . . . . . . . . . . . . 15 ⊢ (((𝐴 ∈ Word V ∧ 𝐵 ∈ Word V) ∧ 𝑦 ∈ (0..^(♯‘𝐵))) → 𝑦 ∈ (0..^(♯‘𝐵)))
76	26	adantr 276	. . . . . . . . . . . . . . 15 ⊢ (((𝐴 ∈ Word V ∧ 𝐵 ∈ Word V) ∧ 𝑦 ∈ (0..^(♯‘𝐵))) → (♯‘𝐴) ∈ ℕ₀)
77		elincfzoext 10411	. . . . . . . . . . . . . . 15 ⊢ ((𝑦 ∈ (0..^(♯‘𝐵)) ∧ (♯‘𝐴) ∈ ℕ₀) → (𝑦 + (♯‘𝐴)) ∈ (0..^((♯‘𝐵) + (♯‘𝐴))))
78	75, 76, 77	syl2anc 411	. . . . . . . . . . . . . 14 ⊢ (((𝐴 ∈ Word V ∧ 𝐵 ∈ Word V) ∧ 𝑦 ∈ (0..^(♯‘𝐵))) → (𝑦 + (♯‘𝐴)) ∈ (0..^((♯‘𝐵) + (♯‘𝐴))))
79	17	nn0cnd 9435	. . . . . . . . . . . . . . . . . 18 ⊢ (𝐴 ∈ Word V → (♯‘𝐴) ∈ ℂ)
80	27	nn0cnd 9435	. . . . . . . . . . . . . . . . . 18 ⊢ (𝐵 ∈ Word V → (♯‘𝐵) ∈ ℂ)
81	79, 80, 48	syl2an 289	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐴 ∈ Word V ∧ 𝐵 ∈ Word V) → ((♯‘𝐴) + (♯‘𝐵)) = ((♯‘𝐵) + (♯‘𝐴)))
82	81	oveq2d 6023	. . . . . . . . . . . . . . . 16 ⊢ ((𝐴 ∈ Word V ∧ 𝐵 ∈ Word V) → (0..^((♯‘𝐴) + (♯‘𝐵))) = (0..^((♯‘𝐵) + (♯‘𝐴))))
83	82	eleq2d 2299	. . . . . . . . . . . . . . 15 ⊢ ((𝐴 ∈ Word V ∧ 𝐵 ∈ Word V) → ((𝑦 + (♯‘𝐴)) ∈ (0..^((♯‘𝐴) + (♯‘𝐵))) ↔ (𝑦 + (♯‘𝐴)) ∈ (0..^((♯‘𝐵) + (♯‘𝐴)))))
84	83	adantr 276	. . . . . . . . . . . . . 14 ⊢ (((𝐴 ∈ Word V ∧ 𝐵 ∈ Word V) ∧ 𝑦 ∈ (0..^(♯‘𝐵))) → ((𝑦 + (♯‘𝐴)) ∈ (0..^((♯‘𝐴) + (♯‘𝐵))) ↔ (𝑦 + (♯‘𝐴)) ∈ (0..^((♯‘𝐵) + (♯‘𝐴)))))
85	78, 84	mpbird 167	. . . . . . . . . . . . 13 ⊢ (((𝐴 ∈ Word V ∧ 𝐵 ∈ Word V) ∧ 𝑦 ∈ (0..^(♯‘𝐵))) → (𝑦 + (♯‘𝐴)) ∈ (0..^((♯‘𝐴) + (♯‘𝐵))))
86		eleq1 2292	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 = (𝑦 + (♯‘𝐴)) → (𝑥 ∈ (0..^(♯‘𝐴)) ↔ (𝑦 + (♯‘𝐴)) ∈ (0..^(♯‘𝐴))))
87		fveq2 5629	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 = (𝑦 + (♯‘𝐴)) → (𝐴‘𝑥) = (𝐴‘(𝑦 + (♯‘𝐴))))
88		fvoveq1 6030	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 = (𝑦 + (♯‘𝐴)) → (𝐵‘(𝑥 − (♯‘𝐴))) = (𝐵‘((𝑦 + (♯‘𝐴)) − (♯‘𝐴))))
89	86, 87, 88	ifbieq12d 3629	. . . . . . . . . . . . . . 15 ⊢ (𝑥 = (𝑦 + (♯‘𝐴)) → if(𝑥 ∈ (0..^(♯‘𝐴)), (𝐴‘𝑥), (𝐵‘(𝑥 − (♯‘𝐴)))) = if((𝑦 + (♯‘𝐴)) ∈ (0..^(♯‘𝐴)), (𝐴‘(𝑦 + (♯‘𝐴))), (𝐵‘((𝑦 + (♯‘𝐴)) − (♯‘𝐴)))))
90	89	eleq1d 2298	. . . . . . . . . . . . . 14 ⊢ (𝑥 = (𝑦 + (♯‘𝐴)) → (if(𝑥 ∈ (0..^(♯‘𝐴)), (𝐴‘𝑥), (𝐵‘(𝑥 − (♯‘𝐴)))) ∈ 𝑆 ↔ if((𝑦 + (♯‘𝐴)) ∈ (0..^(♯‘𝐴)), (𝐴‘(𝑦 + (♯‘𝐴))), (𝐵‘((𝑦 + (♯‘𝐴)) − (♯‘𝐴)))) ∈ 𝑆))
91	90	rspcv 2903	. . . . . . . . . . . . 13 ⊢ ((𝑦 + (♯‘𝐴)) ∈ (0..^((♯‘𝐴) + (♯‘𝐵))) → (∀𝑥 ∈ (0..^((♯‘𝐴) + (♯‘𝐵)))if(𝑥 ∈ (0..^(♯‘𝐴)), (𝐴‘𝑥), (𝐵‘(𝑥 − (♯‘𝐴)))) ∈ 𝑆 → if((𝑦 + (♯‘𝐴)) ∈ (0..^(♯‘𝐴)), (𝐴‘(𝑦 + (♯‘𝐴))), (𝐵‘((𝑦 + (♯‘𝐴)) − (♯‘𝐴)))) ∈ 𝑆))
92	85, 91	syl 14	. . . . . . . . . . . 12 ⊢ (((𝐴 ∈ Word V ∧ 𝐵 ∈ Word V) ∧ 𝑦 ∈ (0..^(♯‘𝐵))) → (∀𝑥 ∈ (0..^((♯‘𝐴) + (♯‘𝐵)))if(𝑥 ∈ (0..^(♯‘𝐴)), (𝐴‘𝑥), (𝐵‘(𝑥 − (♯‘𝐴)))) ∈ 𝑆 → if((𝑦 + (♯‘𝐴)) ∈ (0..^(♯‘𝐴)), (𝐴‘(𝑦 + (♯‘𝐴))), (𝐵‘((𝑦 + (♯‘𝐴)) − (♯‘𝐴)))) ∈ 𝑆))
93	17	nn0red 9434	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝐴 ∈ Word V → (♯‘𝐴) ∈ ℝ)
94	93	adantr 276	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝐴 ∈ Word V ∧ 𝐵 ∈ Word V) → (♯‘𝐴) ∈ ℝ)
95	94	adantr 276	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝐴 ∈ Word V ∧ 𝐵 ∈ Word V) ∧ 𝑦 ∈ (0..^(♯‘𝐵))) → (♯‘𝐴) ∈ ℝ)
96		elfzoelz 10355	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑦 ∈ (0..^(♯‘𝐵)) → 𝑦 ∈ ℤ)
97	96	zred 9580	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑦 ∈ (0..^(♯‘𝐵)) → 𝑦 ∈ ℝ)
98	97	adantr 276	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑦 ∈ (0..^(♯‘𝐵)) ∧ (𝐴 ∈ Word V ∧ 𝐵 ∈ Word V)) → 𝑦 ∈ ℝ)
99	94	adantl 277	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑦 ∈ (0..^(♯‘𝐵)) ∧ (𝐴 ∈ Word V ∧ 𝐵 ∈ Word V)) → (♯‘𝐴) ∈ ℝ)
100	98, 99	readdcld 8187	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑦 ∈ (0..^(♯‘𝐵)) ∧ (𝐴 ∈ Word V ∧ 𝐵 ∈ Word V)) → (𝑦 + (♯‘𝐴)) ∈ ℝ)
101	100	ancoms 268	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝐴 ∈ Word V ∧ 𝐵 ∈ Word V) ∧ 𝑦 ∈ (0..^(♯‘𝐵))) → (𝑦 + (♯‘𝐴)) ∈ ℝ)
102		elfzole1 10364	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑦 ∈ (0..^(♯‘𝐵)) → 0 ≤ 𝑦)
103	102	adantl 277	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝐴 ∈ Word V ∧ 𝐵 ∈ Word V) ∧ 𝑦 ∈ (0..^(♯‘𝐵))) → 0 ≤ 𝑦)
104		addge02 8631	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((♯‘𝐴) ∈ ℝ ∧ 𝑦 ∈ ℝ) → (0 ≤ 𝑦 ↔ (♯‘𝐴) ≤ (𝑦 + (♯‘𝐴))))
105	94, 97, 104	syl2an 289	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝐴 ∈ Word V ∧ 𝐵 ∈ Word V) ∧ 𝑦 ∈ (0..^(♯‘𝐵))) → (0 ≤ 𝑦 ↔ (♯‘𝐴) ≤ (𝑦 + (♯‘𝐴))))
106	103, 105	mpbid 147	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝐴 ∈ Word V ∧ 𝐵 ∈ Word V) ∧ 𝑦 ∈ (0..^(♯‘𝐵))) → (♯‘𝐴) ≤ (𝑦 + (♯‘𝐴)))
107	95, 101, 106	lensymd 8279	. . . . . . . . . . . . . . . . 17 ⊢ (((𝐴 ∈ Word V ∧ 𝐵 ∈ Word V) ∧ 𝑦 ∈ (0..^(♯‘𝐵))) → ¬ (𝑦 + (♯‘𝐴)) < (♯‘𝐴))
108	107	intn3an3d 1392	. . . . . . . . . . . . . . . 16 ⊢ (((𝐴 ∈ Word V ∧ 𝐵 ∈ Word V) ∧ 𝑦 ∈ (0..^(♯‘𝐵))) → ¬ ((𝑦 + (♯‘𝐴)) ∈ ℕ₀ ∧ (♯‘𝐴) ∈ ℕ ∧ (𝑦 + (♯‘𝐴)) < (♯‘𝐴)))
109		elfzo0 10394	. . . . . . . . . . . . . . . 16 ⊢ ((𝑦 + (♯‘𝐴)) ∈ (0..^(♯‘𝐴)) ↔ ((𝑦 + (♯‘𝐴)) ∈ ℕ₀ ∧ (♯‘𝐴) ∈ ℕ ∧ (𝑦 + (♯‘𝐴)) < (♯‘𝐴)))
110	108, 109	sylnibr 681	. . . . . . . . . . . . . . 15 ⊢ (((𝐴 ∈ Word V ∧ 𝐵 ∈ Word V) ∧ 𝑦 ∈ (0..^(♯‘𝐵))) → ¬ (𝑦 + (♯‘𝐴)) ∈ (0..^(♯‘𝐴)))
111	110	iffalsed 3612	. . . . . . . . . . . . . 14 ⊢ (((𝐴 ∈ Word V ∧ 𝐵 ∈ Word V) ∧ 𝑦 ∈ (0..^(♯‘𝐵))) → if((𝑦 + (♯‘𝐴)) ∈ (0..^(♯‘𝐴)), (𝐴‘(𝑦 + (♯‘𝐴))), (𝐵‘((𝑦 + (♯‘𝐴)) − (♯‘𝐴)))) = (𝐵‘((𝑦 + (♯‘𝐴)) − (♯‘𝐴))))
112	111	eleq1d 2298	. . . . . . . . . . . . 13 ⊢ (((𝐴 ∈ Word V ∧ 𝐵 ∈ Word V) ∧ 𝑦 ∈ (0..^(♯‘𝐵))) → (if((𝑦 + (♯‘𝐴)) ∈ (0..^(♯‘𝐴)), (𝐴‘(𝑦 + (♯‘𝐴))), (𝐵‘((𝑦 + (♯‘𝐴)) − (♯‘𝐴)))) ∈ 𝑆 ↔ (𝐵‘((𝑦 + (♯‘𝐴)) − (♯‘𝐴))) ∈ 𝑆))
113	96	zcnd 9581	. . . . . . . . . . . . . . . . 17 ⊢ (𝑦 ∈ (0..^(♯‘𝐵)) → 𝑦 ∈ ℂ)
114	79	adantr 276	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐴 ∈ Word V ∧ 𝐵 ∈ Word V) → (♯‘𝐴) ∈ ℂ)
115		pncan 8363	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑦 ∈ ℂ ∧ (♯‘𝐴) ∈ ℂ) → ((𝑦 + (♯‘𝐴)) − (♯‘𝐴)) = 𝑦)
116	113, 114, 115	syl2anr 290	. . . . . . . . . . . . . . . 16 ⊢ (((𝐴 ∈ Word V ∧ 𝐵 ∈ Word V) ∧ 𝑦 ∈ (0..^(♯‘𝐵))) → ((𝑦 + (♯‘𝐴)) − (♯‘𝐴)) = 𝑦)
117	116	fveq2d 5633	. . . . . . . . . . . . . . 15 ⊢ (((𝐴 ∈ Word V ∧ 𝐵 ∈ Word V) ∧ 𝑦 ∈ (0..^(♯‘𝐵))) → (𝐵‘((𝑦 + (♯‘𝐴)) − (♯‘𝐴))) = (𝐵‘𝑦))
118	117	eleq1d 2298	. . . . . . . . . . . . . 14 ⊢ (((𝐴 ∈ Word V ∧ 𝐵 ∈ Word V) ∧ 𝑦 ∈ (0..^(♯‘𝐵))) → ((𝐵‘((𝑦 + (♯‘𝐴)) − (♯‘𝐴))) ∈ 𝑆 ↔ (𝐵‘𝑦) ∈ 𝑆))
119	118	biimpd 144	. . . . . . . . . . . . 13 ⊢ (((𝐴 ∈ Word V ∧ 𝐵 ∈ Word V) ∧ 𝑦 ∈ (0..^(♯‘𝐵))) → ((𝐵‘((𝑦 + (♯‘𝐴)) − (♯‘𝐴))) ∈ 𝑆 → (𝐵‘𝑦) ∈ 𝑆))
120	112, 119	sylbid 150	. . . . . . . . . . . 12 ⊢ (((𝐴 ∈ Word V ∧ 𝐵 ∈ Word V) ∧ 𝑦 ∈ (0..^(♯‘𝐵))) → (if((𝑦 + (♯‘𝐴)) ∈ (0..^(♯‘𝐴)), (𝐴‘(𝑦 + (♯‘𝐴))), (𝐵‘((𝑦 + (♯‘𝐴)) − (♯‘𝐴)))) ∈ 𝑆 → (𝐵‘𝑦) ∈ 𝑆))
121	92, 120	syld 45	. . . . . . . . . . 11 ⊢ (((𝐴 ∈ Word V ∧ 𝐵 ∈ Word V) ∧ 𝑦 ∈ (0..^(♯‘𝐵))) → (∀𝑥 ∈ (0..^((♯‘𝐴) + (♯‘𝐵)))if(𝑥 ∈ (0..^(♯‘𝐴)), (𝐴‘𝑥), (𝐵‘(𝑥 − (♯‘𝐴)))) ∈ 𝑆 → (𝐵‘𝑦) ∈ 𝑆))
122	121	impancom 260	. . . . . . . . . 10 ⊢ (((𝐴 ∈ Word V ∧ 𝐵 ∈ Word V) ∧ ∀𝑥 ∈ (0..^((♯‘𝐴) + (♯‘𝐵)))if(𝑥 ∈ (0..^(♯‘𝐴)), (𝐴‘𝑥), (𝐵‘(𝑥 − (♯‘𝐴)))) ∈ 𝑆) → (𝑦 ∈ (0..^(♯‘𝐵)) → (𝐵‘𝑦) ∈ 𝑆))
123	122	ralrimiv 2602	. . . . . . . . 9 ⊢ (((𝐴 ∈ Word V ∧ 𝐵 ∈ Word V) ∧ ∀𝑥 ∈ (0..^((♯‘𝐴) + (♯‘𝐵)))if(𝑥 ∈ (0..^(♯‘𝐴)), (𝐴‘𝑥), (𝐵‘(𝑥 − (♯‘𝐴)))) ∈ 𝑆) → ∀𝑦 ∈ (0..^(♯‘𝐵))(𝐵‘𝑦) ∈ 𝑆)
124		iswrdsymb 11102	. . . . . . . . 9 ⊢ ((𝐵 ∈ Word V ∧ ∀𝑦 ∈ (0..^(♯‘𝐵))(𝐵‘𝑦) ∈ 𝑆) → 𝐵 ∈ Word 𝑆)
125	74, 123, 124	syl2an2r 597	. . . . . . . 8 ⊢ (((𝐴 ∈ Word V ∧ 𝐵 ∈ Word V) ∧ ∀𝑥 ∈ (0..^((♯‘𝐴) + (♯‘𝐵)))if(𝑥 ∈ (0..^(♯‘𝐴)), (𝐴‘𝑥), (𝐵‘(𝑥 − (♯‘𝐴)))) ∈ 𝑆) → 𝐵 ∈ Word 𝑆)
126	73, 125	jca 306	. . . . . . 7 ⊢ (((𝐴 ∈ Word V ∧ 𝐵 ∈ Word V) ∧ ∀𝑥 ∈ (0..^((♯‘𝐴) + (♯‘𝐵)))if(𝑥 ∈ (0..^(♯‘𝐴)), (𝐴‘𝑥), (𝐵‘(𝑥 − (♯‘𝐴)))) ∈ 𝑆) → (𝐴 ∈ Word 𝑆 ∧ 𝐵 ∈ Word 𝑆))
127	126	ex 115	. . . . . 6 ⊢ ((𝐴 ∈ Word V ∧ 𝐵 ∈ Word V) → (∀𝑥 ∈ (0..^((♯‘𝐴) + (♯‘𝐵)))if(𝑥 ∈ (0..^(♯‘𝐴)), (𝐴‘𝑥), (𝐵‘(𝑥 − (♯‘𝐴)))) ∈ 𝑆 → (𝐴 ∈ Word 𝑆 ∧ 𝐵 ∈ Word 𝑆)))
128	44, 127	biimtrrid 153	. . . . 5 ⊢ ((𝐴 ∈ Word V ∧ 𝐵 ∈ Word V) → ((𝑥 ∈ (0..^((♯‘𝐴) + (♯‘𝐵))) ↦ if(𝑥 ∈ (0..^(♯‘𝐴)), (𝐴‘𝑥), (𝐵‘(𝑥 − (♯‘𝐴))))):(0..^((♯‘𝐴) + (♯‘𝐵)))⟶𝑆 → (𝐴 ∈ Word 𝑆 ∧ 𝐵 ∈ Word 𝑆)))
129	43, 128	sylbid 150	. . . 4 ⊢ ((𝐴 ∈ Word V ∧ 𝐵 ∈ Word V) → ((𝑥 ∈ (0..^((♯‘𝐴) + (♯‘𝐵))) ↦ if(𝑥 ∈ (0..^(♯‘𝐴)), (𝐴‘𝑥), (𝐵‘(𝑥 − (♯‘𝐴))))):(0..^(♯‘(𝑥 ∈ (0..^((♯‘𝐴) + (♯‘𝐵))) ↦ if(𝑥 ∈ (0..^(♯‘𝐴)), (𝐴‘𝑥), (𝐵‘(𝑥 − (♯‘𝐴)))))))⟶𝑆 → (𝐴 ∈ Word 𝑆 ∧ 𝐵 ∈ Word 𝑆)))
130	6, 129	syl5 32	. . 3 ⊢ ((𝐴 ∈ Word V ∧ 𝐵 ∈ Word V) → ((𝑥 ∈ (0..^((♯‘𝐴) + (♯‘𝐵))) ↦ if(𝑥 ∈ (0..^(♯‘𝐴)), (𝐴‘𝑥), (𝐵‘(𝑥 − (♯‘𝐴))))) ∈ Word 𝑆 → (𝐴 ∈ Word 𝑆 ∧ 𝐵 ∈ Word 𝑆)))
131	5, 130	sylbid 150	. 2 ⊢ ((𝐴 ∈ Word V ∧ 𝐵 ∈ Word V) → ((𝐴 ++ 𝐵) ∈ Word 𝑆 → (𝐴 ∈ Word 𝑆 ∧ 𝐵 ∈ Word 𝑆)))
132		ccatcl 11141	. 2 ⊢ ((𝐴 ∈ Word 𝑆 ∧ 𝐵 ∈ Word 𝑆) → (𝐴 ++ 𝐵) ∈ Word 𝑆)
133	131, 132	impbid1 142	1 ⊢ ((𝐴 ∈ Word V ∧ 𝐵 ∈ Word V) → ((𝐴 ++ 𝐵) ∈ Word 𝑆 ↔ (𝐴 ∈ Word 𝑆 ∧ 𝐵 ∈ Word 𝑆)))

Colors of variables: wff set class

Syntax hints: → wi 4 ∧ wa 104 ↔ wb 105 ∧ w3a 1002 = wceq 1395 ∈ wcel 2200 ∀wral 2508 Vcvv 2799 ⊆ wss 3197 ifcif 3602 class class class wbr 4083 ↦ cmpt 4145 dom cdm 4719 Fun wfun 5312 Fn wfn 5313 ⟶wf 5314 ‘cfv 5318 (class class class)co 6007 Fincfn 6895 ℂcc 8008 ℝcr 8009 0cc0 8010 + caddc 8013 < clt 8192 ≤ cle 8193 − cmin 8328 ℕcn 9121 ℕ₀cn0 9380 ℤcz 9457 ℤ_≥cuz 9733 ..^cfzo 10350 ♯chash 11009 Word cword 11084 ++ cconcat 11138

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 617 ax-in2 618 ax-io 714 ax-5 1493 ax-7 1494 ax-gen 1495 ax-ie1 1539 ax-ie2 1540 ax-8 1550 ax-10 1551 ax-11 1552 ax-i12 1553 ax-bndl 1555 ax-4 1556 ax-17 1572 ax-i9 1576 ax-ial 1580 ax-i5r 1581 ax-13 2202 ax-14 2203 ax-ext 2211 ax-coll 4199 ax-sep 4202 ax-nul 4210 ax-pow 4258 ax-pr 4293 ax-un 4524 ax-setind 4629 ax-iinf 4680 ax-cnex 8101 ax-resscn 8102 ax-1cn 8103 ax-1re 8104 ax-icn 8105 ax-addcl 8106 ax-addrcl 8107 ax-mulcl 8108 ax-addcom 8110 ax-addass 8112 ax-distr 8114 ax-i2m1 8115 ax-0lt1 8116 ax-0id 8118 ax-rnegex 8119 ax-cnre 8121 ax-pre-ltirr 8122 ax-pre-ltwlin 8123 ax-pre-lttrn 8124 ax-pre-apti 8125 ax-pre-ltadd 8126

This theorem depends on definitions: df-bi 117 df-dc 840 df-3or 1003 df-3an 1004 df-tru 1398 df-fal 1401 df-nf 1507 df-sb 1809 df-eu 2080 df-mo 2081 df-clab 2216 df-cleq 2222 df-clel 2225 df-nfc 2361 df-ne 2401 df-nel 2496 df-ral 2513 df-rex 2514 df-reu 2515 df-rab 2517 df-v 2801 df-sbc 3029 df-csb 3125 df-dif 3199 df-un 3201 df-in 3203 df-ss 3210 df-nul 3492 df-if 3603 df-pw 3651 df-sn 3672 df-pr 3673 df-op 3675 df-uni 3889 df-int 3924 df-iun 3967 df-br 4084 df-opab 4146 df-mpt 4147 df-tr 4183 df-id 4384 df-iord 4457 df-on 4459 df-ilim 4460 df-suc 4462 df-iom 4683 df-xp 4725 df-rel 4726 df-cnv 4727 df-co 4728 df-dm 4729 df-rn 4730 df-res 4731 df-ima 4732 df-iota 5278 df-fun 5320 df-fn 5321 df-f 5322 df-f1 5323 df-fo 5324 df-f1o 5325 df-fv 5326 df-riota 5960 df-ov 6010 df-oprab 6011 df-mpo 6012 df-1st 6292 df-2nd 6293 df-recs 6457 df-frec 6543 df-1o 6568 df-er 6688 df-en 6896 df-dom 6897 df-fin 6898 df-pnf 8194 df-mnf 8195 df-xr 8196 df-ltxr 8197 df-le 8198 df-sub 8330 df-neg 8331 df-inn 9122 df-n0 9381 df-z 9458 df-uz 9734 df-fz 10217 df-fzo 10351 df-ihash 11010 df-word 11085 df-concat 11139

This theorem is referenced by: ccatrcl1 11162

W3C validator