| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | ccatfval 14612 | . . . 4
⊢ ((𝐴 ∈ Word V ∧ 𝐵 ∈ Word V) → (𝐴 ++ 𝐵) = (𝑥 ∈ (0..^((♯‘𝐴) + (♯‘𝐵))) ↦ if(𝑥 ∈
(0..^(♯‘𝐴)),
(𝐴‘𝑥), (𝐵‘(𝑥 − (♯‘𝐴)))))) | 
| 2 | 1 | eleq1d 2825 | . . 3
⊢ ((𝐴 ∈ Word V ∧ 𝐵 ∈ Word V) → ((𝐴 ++ 𝐵) ∈ Word 𝑆 ↔ (𝑥 ∈ (0..^((♯‘𝐴) + (♯‘𝐵))) ↦ if(𝑥 ∈
(0..^(♯‘𝐴)),
(𝐴‘𝑥), (𝐵‘(𝑥 − (♯‘𝐴))))) ∈ Word 𝑆)) | 
| 3 |  | wrdf 14558 | . . . 4
⊢ ((𝑥 ∈
(0..^((♯‘𝐴) +
(♯‘𝐵))) ↦
if(𝑥 ∈
(0..^(♯‘𝐴)),
(𝐴‘𝑥), (𝐵‘(𝑥 − (♯‘𝐴))))) ∈ Word 𝑆 → (𝑥 ∈ (0..^((♯‘𝐴) + (♯‘𝐵))) ↦ if(𝑥 ∈
(0..^(♯‘𝐴)),
(𝐴‘𝑥), (𝐵‘(𝑥 − (♯‘𝐴))))):(0..^(♯‘(𝑥 ∈
(0..^((♯‘𝐴) +
(♯‘𝐵))) ↦
if(𝑥 ∈
(0..^(♯‘𝐴)),
(𝐴‘𝑥), (𝐵‘(𝑥 − (♯‘𝐴)))))))⟶𝑆) | 
| 4 |  | funmpt 6603 | . . . . . . . . 9
⊢ Fun
(𝑥 ∈
(0..^((♯‘𝐴) +
(♯‘𝐵))) ↦
if(𝑥 ∈
(0..^(♯‘𝐴)),
(𝐴‘𝑥), (𝐵‘(𝑥 − (♯‘𝐴))))) | 
| 5 |  | fzofi 14016 | . . . . . . . . . . 11
⊢
(0..^((♯‘𝐴) + (♯‘𝐵))) ∈ Fin | 
| 6 |  | mptfi 9392 | . . . . . . . . . . 11
⊢
((0..^((♯‘𝐴) + (♯‘𝐵))) ∈ Fin → (𝑥 ∈ (0..^((♯‘𝐴) + (♯‘𝐵))) ↦ if(𝑥 ∈
(0..^(♯‘𝐴)),
(𝐴‘𝑥), (𝐵‘(𝑥 − (♯‘𝐴))))) ∈ Fin) | 
| 7 | 5, 6 | ax-mp 5 | . . . . . . . . . 10
⊢ (𝑥 ∈
(0..^((♯‘𝐴) +
(♯‘𝐵))) ↦
if(𝑥 ∈
(0..^(♯‘𝐴)),
(𝐴‘𝑥), (𝐵‘(𝑥 − (♯‘𝐴))))) ∈ Fin | 
| 8 |  | hashfun 14477 | . . . . . . . . . 10
⊢ ((𝑥 ∈
(0..^((♯‘𝐴) +
(♯‘𝐵))) ↦
if(𝑥 ∈
(0..^(♯‘𝐴)),
(𝐴‘𝑥), (𝐵‘(𝑥 − (♯‘𝐴))))) ∈ Fin → (Fun (𝑥 ∈
(0..^((♯‘𝐴) +
(♯‘𝐵))) ↦
if(𝑥 ∈
(0..^(♯‘𝐴)),
(𝐴‘𝑥), (𝐵‘(𝑥 − (♯‘𝐴))))) ↔ (♯‘(𝑥 ∈
(0..^((♯‘𝐴) +
(♯‘𝐵))) ↦
if(𝑥 ∈
(0..^(♯‘𝐴)),
(𝐴‘𝑥), (𝐵‘(𝑥 − (♯‘𝐴)))))) = (♯‘dom (𝑥 ∈
(0..^((♯‘𝐴) +
(♯‘𝐵))) ↦
if(𝑥 ∈
(0..^(♯‘𝐴)),
(𝐴‘𝑥), (𝐵‘(𝑥 − (♯‘𝐴)))))))) | 
| 9 | 7, 8 | mp1i 13 | . . . . . . . . 9
⊢ ((𝐴 ∈ Word V ∧ 𝐵 ∈ Word V) → (Fun
(𝑥 ∈
(0..^((♯‘𝐴) +
(♯‘𝐵))) ↦
if(𝑥 ∈
(0..^(♯‘𝐴)),
(𝐴‘𝑥), (𝐵‘(𝑥 − (♯‘𝐴))))) ↔ (♯‘(𝑥 ∈
(0..^((♯‘𝐴) +
(♯‘𝐵))) ↦
if(𝑥 ∈
(0..^(♯‘𝐴)),
(𝐴‘𝑥), (𝐵‘(𝑥 − (♯‘𝐴)))))) = (♯‘dom (𝑥 ∈
(0..^((♯‘𝐴) +
(♯‘𝐵))) ↦
if(𝑥 ∈
(0..^(♯‘𝐴)),
(𝐴‘𝑥), (𝐵‘(𝑥 − (♯‘𝐴)))))))) | 
| 10 | 4, 9 | mpbii 233 | . . . . . . . 8
⊢ ((𝐴 ∈ Word V ∧ 𝐵 ∈ Word V) →
(♯‘(𝑥 ∈
(0..^((♯‘𝐴) +
(♯‘𝐵))) ↦
if(𝑥 ∈
(0..^(♯‘𝐴)),
(𝐴‘𝑥), (𝐵‘(𝑥 − (♯‘𝐴)))))) = (♯‘dom (𝑥 ∈
(0..^((♯‘𝐴) +
(♯‘𝐵))) ↦
if(𝑥 ∈
(0..^(♯‘𝐴)),
(𝐴‘𝑥), (𝐵‘(𝑥 − (♯‘𝐴))))))) | 
| 11 |  | dmmptg 6261 | . . . . . . . . . . 11
⊢
(∀𝑥 ∈
(0..^((♯‘𝐴) +
(♯‘𝐵)))if(𝑥 ∈
(0..^(♯‘𝐴)),
(𝐴‘𝑥), (𝐵‘(𝑥 − (♯‘𝐴)))) ∈ V → dom (𝑥 ∈ (0..^((♯‘𝐴) + (♯‘𝐵))) ↦ if(𝑥 ∈
(0..^(♯‘𝐴)),
(𝐴‘𝑥), (𝐵‘(𝑥 − (♯‘𝐴))))) = (0..^((♯‘𝐴) + (♯‘𝐵)))) | 
| 12 |  | fvex 6918 | . . . . . . . . . . . . 13
⊢ (𝐴‘𝑥) ∈ V | 
| 13 |  | fvex 6918 | . . . . . . . . . . . . 13
⊢ (𝐵‘(𝑥 − (♯‘𝐴))) ∈ V | 
| 14 | 12, 13 | ifex 4575 | . . . . . . . . . . . 12
⊢ if(𝑥 ∈
(0..^(♯‘𝐴)),
(𝐴‘𝑥), (𝐵‘(𝑥 − (♯‘𝐴)))) ∈ V | 
| 15 | 14 | a1i 11 | . . . . . . . . . . 11
⊢ (𝑥 ∈
(0..^((♯‘𝐴) +
(♯‘𝐵))) →
if(𝑥 ∈
(0..^(♯‘𝐴)),
(𝐴‘𝑥), (𝐵‘(𝑥 − (♯‘𝐴)))) ∈ V) | 
| 16 | 11, 15 | mprg 3066 | . . . . . . . . . 10
⊢ dom
(𝑥 ∈
(0..^((♯‘𝐴) +
(♯‘𝐵))) ↦
if(𝑥 ∈
(0..^(♯‘𝐴)),
(𝐴‘𝑥), (𝐵‘(𝑥 − (♯‘𝐴))))) = (0..^((♯‘𝐴) + (♯‘𝐵))) | 
| 17 | 16 | fveq2i 6908 | . . . . . . . . 9
⊢
(♯‘dom (𝑥 ∈ (0..^((♯‘𝐴) + (♯‘𝐵))) ↦ if(𝑥 ∈
(0..^(♯‘𝐴)),
(𝐴‘𝑥), (𝐵‘(𝑥 − (♯‘𝐴)))))) =
(♯‘(0..^((♯‘𝐴) + (♯‘𝐵)))) | 
| 18 |  | lencl 14572 | . . . . . . . . . . 11
⊢ (𝐴 ∈ Word V →
(♯‘𝐴) ∈
ℕ0) | 
| 19 |  | lencl 14572 | . . . . . . . . . . 11
⊢ (𝐵 ∈ Word V →
(♯‘𝐵) ∈
ℕ0) | 
| 20 |  | nn0addcl 12563 | . . . . . . . . . . 11
⊢
(((♯‘𝐴)
∈ ℕ0 ∧ (♯‘𝐵) ∈ ℕ0) →
((♯‘𝐴) +
(♯‘𝐵)) ∈
ℕ0) | 
| 21 | 18, 19, 20 | syl2an 596 | . . . . . . . . . 10
⊢ ((𝐴 ∈ Word V ∧ 𝐵 ∈ Word V) →
((♯‘𝐴) +
(♯‘𝐵)) ∈
ℕ0) | 
| 22 |  | hashfzo0 14470 | . . . . . . . . . 10
⊢
(((♯‘𝐴)
+ (♯‘𝐵)) ∈
ℕ0 → (♯‘(0..^((♯‘𝐴) + (♯‘𝐵)))) = ((♯‘𝐴) + (♯‘𝐵))) | 
| 23 | 21, 22 | syl 17 | . . . . . . . . 9
⊢ ((𝐴 ∈ Word V ∧ 𝐵 ∈ Word V) →
(♯‘(0..^((♯‘𝐴) + (♯‘𝐵)))) = ((♯‘𝐴) + (♯‘𝐵))) | 
| 24 | 17, 23 | eqtrid 2788 | . . . . . . . 8
⊢ ((𝐴 ∈ Word V ∧ 𝐵 ∈ Word V) →
(♯‘dom (𝑥
∈ (0..^((♯‘𝐴) + (♯‘𝐵))) ↦ if(𝑥 ∈ (0..^(♯‘𝐴)), (𝐴‘𝑥), (𝐵‘(𝑥 − (♯‘𝐴)))))) = ((♯‘𝐴) + (♯‘𝐵))) | 
| 25 | 10, 24 | eqtrd 2776 | . . . . . . 7
⊢ ((𝐴 ∈ Word V ∧ 𝐵 ∈ Word V) →
(♯‘(𝑥 ∈
(0..^((♯‘𝐴) +
(♯‘𝐵))) ↦
if(𝑥 ∈
(0..^(♯‘𝐴)),
(𝐴‘𝑥), (𝐵‘(𝑥 − (♯‘𝐴)))))) = ((♯‘𝐴) + (♯‘𝐵))) | 
| 26 | 25 | oveq2d 7448 | . . . . . 6
⊢ ((𝐴 ∈ Word V ∧ 𝐵 ∈ Word V) →
(0..^(♯‘(𝑥
∈ (0..^((♯‘𝐴) + (♯‘𝐵))) ↦ if(𝑥 ∈ (0..^(♯‘𝐴)), (𝐴‘𝑥), (𝐵‘(𝑥 − (♯‘𝐴))))))) = (0..^((♯‘𝐴) + (♯‘𝐵)))) | 
| 27 | 26 | feq2d 6721 | . . . . 5
⊢ ((𝐴 ∈ Word V ∧ 𝐵 ∈ Word V) → ((𝑥 ∈
(0..^((♯‘𝐴) +
(♯‘𝐵))) ↦
if(𝑥 ∈
(0..^(♯‘𝐴)),
(𝐴‘𝑥), (𝐵‘(𝑥 − (♯‘𝐴))))):(0..^(♯‘(𝑥 ∈
(0..^((♯‘𝐴) +
(♯‘𝐵))) ↦
if(𝑥 ∈
(0..^(♯‘𝐴)),
(𝐴‘𝑥), (𝐵‘(𝑥 − (♯‘𝐴)))))))⟶𝑆 ↔ (𝑥 ∈ (0..^((♯‘𝐴) + (♯‘𝐵))) ↦ if(𝑥 ∈
(0..^(♯‘𝐴)),
(𝐴‘𝑥), (𝐵‘(𝑥 − (♯‘𝐴))))):(0..^((♯‘𝐴) + (♯‘𝐵)))⟶𝑆)) | 
| 28 |  | eqid 2736 | . . . . . . 7
⊢ (𝑥 ∈
(0..^((♯‘𝐴) +
(♯‘𝐵))) ↦
if(𝑥 ∈
(0..^(♯‘𝐴)),
(𝐴‘𝑥), (𝐵‘(𝑥 − (♯‘𝐴))))) = (𝑥 ∈ (0..^((♯‘𝐴) + (♯‘𝐵))) ↦ if(𝑥 ∈
(0..^(♯‘𝐴)),
(𝐴‘𝑥), (𝐵‘(𝑥 − (♯‘𝐴))))) | 
| 29 | 28 | fmpt 7129 | . . . . . 6
⊢
(∀𝑥 ∈
(0..^((♯‘𝐴) +
(♯‘𝐵)))if(𝑥 ∈
(0..^(♯‘𝐴)),
(𝐴‘𝑥), (𝐵‘(𝑥 − (♯‘𝐴)))) ∈ 𝑆 ↔ (𝑥 ∈ (0..^((♯‘𝐴) + (♯‘𝐵))) ↦ if(𝑥 ∈
(0..^(♯‘𝐴)),
(𝐴‘𝑥), (𝐵‘(𝑥 − (♯‘𝐴))))):(0..^((♯‘𝐴) + (♯‘𝐵)))⟶𝑆) | 
| 30 |  | simpl 482 | . . . . . . . . 9
⊢ ((𝐴 ∈ Word V ∧ 𝐵 ∈ Word V) → 𝐴 ∈ Word V) | 
| 31 |  | nn0cn 12538 | . . . . . . . . . . . . . . . . . 18
⊢
((♯‘𝐴)
∈ ℕ0 → (♯‘𝐴) ∈ ℂ) | 
| 32 |  | nn0cn 12538 | . . . . . . . . . . . . . . . . . 18
⊢
((♯‘𝐵)
∈ ℕ0 → (♯‘𝐵) ∈ ℂ) | 
| 33 |  | addcom 11448 | . . . . . . . . . . . . . . . . . 18
⊢
(((♯‘𝐴)
∈ ℂ ∧ (♯‘𝐵) ∈ ℂ) →
((♯‘𝐴) +
(♯‘𝐵)) =
((♯‘𝐵) +
(♯‘𝐴))) | 
| 34 | 31, 32, 33 | syl2an 596 | . . . . . . . . . . . . . . . . 17
⊢
(((♯‘𝐴)
∈ ℕ0 ∧ (♯‘𝐵) ∈ ℕ0) →
((♯‘𝐴) +
(♯‘𝐵)) =
((♯‘𝐵) +
(♯‘𝐴))) | 
| 35 |  | nn0z 12640 | . . . . . . . . . . . . . . . . . . 19
⊢
((♯‘𝐴)
∈ ℕ0 → (♯‘𝐴) ∈ ℤ) | 
| 36 | 35 | anim1ci 616 | . . . . . . . . . . . . . . . . . 18
⊢
(((♯‘𝐴)
∈ ℕ0 ∧ (♯‘𝐵) ∈ ℕ0) →
((♯‘𝐵) ∈
ℕ0 ∧ (♯‘𝐴) ∈ ℤ)) | 
| 37 |  | nn0pzuz 12948 | . . . . . . . . . . . . . . . . . 18
⊢
(((♯‘𝐵)
∈ ℕ0 ∧ (♯‘𝐴) ∈ ℤ) →
((♯‘𝐵) +
(♯‘𝐴)) ∈
(ℤ≥‘(♯‘𝐴))) | 
| 38 | 36, 37 | syl 17 | . . . . . . . . . . . . . . . . 17
⊢
(((♯‘𝐴)
∈ ℕ0 ∧ (♯‘𝐵) ∈ ℕ0) →
((♯‘𝐵) +
(♯‘𝐴)) ∈
(ℤ≥‘(♯‘𝐴))) | 
| 39 | 34, 38 | eqeltrd 2840 | . . . . . . . . . . . . . . . 16
⊢
(((♯‘𝐴)
∈ ℕ0 ∧ (♯‘𝐵) ∈ ℕ0) →
((♯‘𝐴) +
(♯‘𝐵)) ∈
(ℤ≥‘(♯‘𝐴))) | 
| 40 | 18, 19, 39 | syl2an 596 | . . . . . . . . . . . . . . 15
⊢ ((𝐴 ∈ Word V ∧ 𝐵 ∈ Word V) →
((♯‘𝐴) +
(♯‘𝐵)) ∈
(ℤ≥‘(♯‘𝐴))) | 
| 41 |  | fzoss2 13728 | . . . . . . . . . . . . . . 15
⊢
(((♯‘𝐴)
+ (♯‘𝐵)) ∈
(ℤ≥‘(♯‘𝐴)) → (0..^(♯‘𝐴)) ⊆
(0..^((♯‘𝐴) +
(♯‘𝐵)))) | 
| 42 | 40, 41 | syl 17 | . . . . . . . . . . . . . 14
⊢ ((𝐴 ∈ Word V ∧ 𝐵 ∈ Word V) →
(0..^(♯‘𝐴))
⊆ (0..^((♯‘𝐴) + (♯‘𝐵)))) | 
| 43 | 42 | sselda 3982 | . . . . . . . . . . . . 13
⊢ (((𝐴 ∈ Word V ∧ 𝐵 ∈ Word V) ∧ 𝑦 ∈
(0..^(♯‘𝐴)))
→ 𝑦 ∈
(0..^((♯‘𝐴) +
(♯‘𝐵)))) | 
| 44 |  | eleq1 2828 | . . . . . . . . . . . . . . . 16
⊢ (𝑥 = 𝑦 → (𝑥 ∈ (0..^(♯‘𝐴)) ↔ 𝑦 ∈ (0..^(♯‘𝐴)))) | 
| 45 |  | fveq2 6905 | . . . . . . . . . . . . . . . 16
⊢ (𝑥 = 𝑦 → (𝐴‘𝑥) = (𝐴‘𝑦)) | 
| 46 |  | fvoveq1 7455 | . . . . . . . . . . . . . . . 16
⊢ (𝑥 = 𝑦 → (𝐵‘(𝑥 − (♯‘𝐴))) = (𝐵‘(𝑦 − (♯‘𝐴)))) | 
| 47 | 44, 45, 46 | ifbieq12d 4553 | . . . . . . . . . . . . . . 15
⊢ (𝑥 = 𝑦 → if(𝑥 ∈ (0..^(♯‘𝐴)), (𝐴‘𝑥), (𝐵‘(𝑥 − (♯‘𝐴)))) = if(𝑦 ∈ (0..^(♯‘𝐴)), (𝐴‘𝑦), (𝐵‘(𝑦 − (♯‘𝐴))))) | 
| 48 | 47 | eleq1d 2825 | . . . . . . . . . . . . . 14
⊢ (𝑥 = 𝑦 → (if(𝑥 ∈ (0..^(♯‘𝐴)), (𝐴‘𝑥), (𝐵‘(𝑥 − (♯‘𝐴)))) ∈ 𝑆 ↔ if(𝑦 ∈ (0..^(♯‘𝐴)), (𝐴‘𝑦), (𝐵‘(𝑦 − (♯‘𝐴)))) ∈ 𝑆)) | 
| 49 | 48 | rspcv 3617 | . . . . . . . . . . . . 13
⊢ (𝑦 ∈
(0..^((♯‘𝐴) +
(♯‘𝐵))) →
(∀𝑥 ∈
(0..^((♯‘𝐴) +
(♯‘𝐵)))if(𝑥 ∈
(0..^(♯‘𝐴)),
(𝐴‘𝑥), (𝐵‘(𝑥 − (♯‘𝐴)))) ∈ 𝑆 → if(𝑦 ∈ (0..^(♯‘𝐴)), (𝐴‘𝑦), (𝐵‘(𝑦 − (♯‘𝐴)))) ∈ 𝑆)) | 
| 50 | 43, 49 | syl 17 | . . . . . . . . . . . 12
⊢ (((𝐴 ∈ Word V ∧ 𝐵 ∈ Word V) ∧ 𝑦 ∈
(0..^(♯‘𝐴)))
→ (∀𝑥 ∈
(0..^((♯‘𝐴) +
(♯‘𝐵)))if(𝑥 ∈
(0..^(♯‘𝐴)),
(𝐴‘𝑥), (𝐵‘(𝑥 − (♯‘𝐴)))) ∈ 𝑆 → if(𝑦 ∈ (0..^(♯‘𝐴)), (𝐴‘𝑦), (𝐵‘(𝑦 − (♯‘𝐴)))) ∈ 𝑆)) | 
| 51 |  | iftrue 4530 | . . . . . . . . . . . . . 14
⊢ (𝑦 ∈
(0..^(♯‘𝐴))
→ if(𝑦 ∈
(0..^(♯‘𝐴)),
(𝐴‘𝑦), (𝐵‘(𝑦 − (♯‘𝐴)))) = (𝐴‘𝑦)) | 
| 52 | 51 | adantl 481 | . . . . . . . . . . . . 13
⊢ (((𝐴 ∈ Word V ∧ 𝐵 ∈ Word V) ∧ 𝑦 ∈
(0..^(♯‘𝐴)))
→ if(𝑦 ∈
(0..^(♯‘𝐴)),
(𝐴‘𝑦), (𝐵‘(𝑦 − (♯‘𝐴)))) = (𝐴‘𝑦)) | 
| 53 | 52 | eleq1d 2825 | . . . . . . . . . . . 12
⊢ (((𝐴 ∈ Word V ∧ 𝐵 ∈ Word V) ∧ 𝑦 ∈
(0..^(♯‘𝐴)))
→ (if(𝑦 ∈
(0..^(♯‘𝐴)),
(𝐴‘𝑦), (𝐵‘(𝑦 − (♯‘𝐴)))) ∈ 𝑆 ↔ (𝐴‘𝑦) ∈ 𝑆)) | 
| 54 | 50, 53 | sylibd 239 | . . . . . . . . . . 11
⊢ (((𝐴 ∈ Word V ∧ 𝐵 ∈ Word V) ∧ 𝑦 ∈
(0..^(♯‘𝐴)))
→ (∀𝑥 ∈
(0..^((♯‘𝐴) +
(♯‘𝐵)))if(𝑥 ∈
(0..^(♯‘𝐴)),
(𝐴‘𝑥), (𝐵‘(𝑥 − (♯‘𝐴)))) ∈ 𝑆 → (𝐴‘𝑦) ∈ 𝑆)) | 
| 55 | 54 | impancom 451 | . . . . . . . . . 10
⊢ (((𝐴 ∈ Word V ∧ 𝐵 ∈ Word V) ∧
∀𝑥 ∈
(0..^((♯‘𝐴) +
(♯‘𝐵)))if(𝑥 ∈
(0..^(♯‘𝐴)),
(𝐴‘𝑥), (𝐵‘(𝑥 − (♯‘𝐴)))) ∈ 𝑆) → (𝑦 ∈ (0..^(♯‘𝐴)) → (𝐴‘𝑦) ∈ 𝑆)) | 
| 56 | 55 | ralrimiv 3144 | . . . . . . . . 9
⊢ (((𝐴 ∈ Word V ∧ 𝐵 ∈ Word V) ∧
∀𝑥 ∈
(0..^((♯‘𝐴) +
(♯‘𝐵)))if(𝑥 ∈
(0..^(♯‘𝐴)),
(𝐴‘𝑥), (𝐵‘(𝑥 − (♯‘𝐴)))) ∈ 𝑆) → ∀𝑦 ∈ (0..^(♯‘𝐴))(𝐴‘𝑦) ∈ 𝑆) | 
| 57 |  | iswrdsymb 14570 | . . . . . . . . 9
⊢ ((𝐴 ∈ Word V ∧
∀𝑦 ∈
(0..^(♯‘𝐴))(𝐴‘𝑦) ∈ 𝑆) → 𝐴 ∈ Word 𝑆) | 
| 58 | 30, 56, 57 | syl2an2r 685 | . . . . . . . 8
⊢ (((𝐴 ∈ Word V ∧ 𝐵 ∈ Word V) ∧
∀𝑥 ∈
(0..^((♯‘𝐴) +
(♯‘𝐵)))if(𝑥 ∈
(0..^(♯‘𝐴)),
(𝐴‘𝑥), (𝐵‘(𝑥 − (♯‘𝐴)))) ∈ 𝑆) → 𝐴 ∈ Word 𝑆) | 
| 59 |  | simpr 484 | . . . . . . . . 9
⊢ ((𝐴 ∈ Word V ∧ 𝐵 ∈ Word V) → 𝐵 ∈ Word V) | 
| 60 |  | simpr 484 | . . . . . . . . . . . . . . 15
⊢ (((𝐴 ∈ Word V ∧ 𝐵 ∈ Word V) ∧ 𝑦 ∈
(0..^(♯‘𝐵)))
→ 𝑦 ∈
(0..^(♯‘𝐵))) | 
| 61 | 18 | adantr 480 | . . . . . . . . . . . . . . . 16
⊢ ((𝐴 ∈ Word V ∧ 𝐵 ∈ Word V) →
(♯‘𝐴) ∈
ℕ0) | 
| 62 | 61 | adantr 480 | . . . . . . . . . . . . . . 15
⊢ (((𝐴 ∈ Word V ∧ 𝐵 ∈ Word V) ∧ 𝑦 ∈
(0..^(♯‘𝐵)))
→ (♯‘𝐴)
∈ ℕ0) | 
| 63 |  | elincfzoext 13763 | . . . . . . . . . . . . . . 15
⊢ ((𝑦 ∈
(0..^(♯‘𝐵))
∧ (♯‘𝐴)
∈ ℕ0) → (𝑦 + (♯‘𝐴)) ∈ (0..^((♯‘𝐵) + (♯‘𝐴)))) | 
| 64 | 60, 62, 63 | syl2anc 584 | . . . . . . . . . . . . . 14
⊢ (((𝐴 ∈ Word V ∧ 𝐵 ∈ Word V) ∧ 𝑦 ∈
(0..^(♯‘𝐵)))
→ (𝑦 +
(♯‘𝐴)) ∈
(0..^((♯‘𝐵) +
(♯‘𝐴)))) | 
| 65 | 18 | nn0cnd 12591 | . . . . . . . . . . . . . . . . . 18
⊢ (𝐴 ∈ Word V →
(♯‘𝐴) ∈
ℂ) | 
| 66 | 19 | nn0cnd 12591 | . . . . . . . . . . . . . . . . . 18
⊢ (𝐵 ∈ Word V →
(♯‘𝐵) ∈
ℂ) | 
| 67 | 65, 66, 33 | syl2an 596 | . . . . . . . . . . . . . . . . 17
⊢ ((𝐴 ∈ Word V ∧ 𝐵 ∈ Word V) →
((♯‘𝐴) +
(♯‘𝐵)) =
((♯‘𝐵) +
(♯‘𝐴))) | 
| 68 | 67 | oveq2d 7448 | . . . . . . . . . . . . . . . 16
⊢ ((𝐴 ∈ Word V ∧ 𝐵 ∈ Word V) →
(0..^((♯‘𝐴) +
(♯‘𝐵))) =
(0..^((♯‘𝐵) +
(♯‘𝐴)))) | 
| 69 | 68 | eleq2d 2826 | . . . . . . . . . . . . . . 15
⊢ ((𝐴 ∈ Word V ∧ 𝐵 ∈ Word V) → ((𝑦 + (♯‘𝐴)) ∈
(0..^((♯‘𝐴) +
(♯‘𝐵))) ↔
(𝑦 + (♯‘𝐴)) ∈
(0..^((♯‘𝐵) +
(♯‘𝐴))))) | 
| 70 | 69 | adantr 480 | . . . . . . . . . . . . . 14
⊢ (((𝐴 ∈ Word V ∧ 𝐵 ∈ Word V) ∧ 𝑦 ∈
(0..^(♯‘𝐵)))
→ ((𝑦 +
(♯‘𝐴)) ∈
(0..^((♯‘𝐴) +
(♯‘𝐵))) ↔
(𝑦 + (♯‘𝐴)) ∈
(0..^((♯‘𝐵) +
(♯‘𝐴))))) | 
| 71 | 64, 70 | mpbird 257 | . . . . . . . . . . . . 13
⊢ (((𝐴 ∈ Word V ∧ 𝐵 ∈ Word V) ∧ 𝑦 ∈
(0..^(♯‘𝐵)))
→ (𝑦 +
(♯‘𝐴)) ∈
(0..^((♯‘𝐴) +
(♯‘𝐵)))) | 
| 72 |  | eleq1 2828 | . . . . . . . . . . . . . . . 16
⊢ (𝑥 = (𝑦 + (♯‘𝐴)) → (𝑥 ∈ (0..^(♯‘𝐴)) ↔ (𝑦 + (♯‘𝐴)) ∈ (0..^(♯‘𝐴)))) | 
| 73 |  | fveq2 6905 | . . . . . . . . . . . . . . . 16
⊢ (𝑥 = (𝑦 + (♯‘𝐴)) → (𝐴‘𝑥) = (𝐴‘(𝑦 + (♯‘𝐴)))) | 
| 74 |  | fvoveq1 7455 | . . . . . . . . . . . . . . . 16
⊢ (𝑥 = (𝑦 + (♯‘𝐴)) → (𝐵‘(𝑥 − (♯‘𝐴))) = (𝐵‘((𝑦 + (♯‘𝐴)) − (♯‘𝐴)))) | 
| 75 | 72, 73, 74 | ifbieq12d 4553 | . . . . . . . . . . . . . . 15
⊢ (𝑥 = (𝑦 + (♯‘𝐴)) → if(𝑥 ∈ (0..^(♯‘𝐴)), (𝐴‘𝑥), (𝐵‘(𝑥 − (♯‘𝐴)))) = if((𝑦 + (♯‘𝐴)) ∈ (0..^(♯‘𝐴)), (𝐴‘(𝑦 + (♯‘𝐴))), (𝐵‘((𝑦 + (♯‘𝐴)) − (♯‘𝐴))))) | 
| 76 | 75 | eleq1d 2825 | . . . . . . . . . . . . . 14
⊢ (𝑥 = (𝑦 + (♯‘𝐴)) → (if(𝑥 ∈ (0..^(♯‘𝐴)), (𝐴‘𝑥), (𝐵‘(𝑥 − (♯‘𝐴)))) ∈ 𝑆 ↔ if((𝑦 + (♯‘𝐴)) ∈ (0..^(♯‘𝐴)), (𝐴‘(𝑦 + (♯‘𝐴))), (𝐵‘((𝑦 + (♯‘𝐴)) − (♯‘𝐴)))) ∈ 𝑆)) | 
| 77 | 76 | rspcv 3617 | . . . . . . . . . . . . 13
⊢ ((𝑦 + (♯‘𝐴)) ∈
(0..^((♯‘𝐴) +
(♯‘𝐵))) →
(∀𝑥 ∈
(0..^((♯‘𝐴) +
(♯‘𝐵)))if(𝑥 ∈
(0..^(♯‘𝐴)),
(𝐴‘𝑥), (𝐵‘(𝑥 − (♯‘𝐴)))) ∈ 𝑆 → if((𝑦 + (♯‘𝐴)) ∈ (0..^(♯‘𝐴)), (𝐴‘(𝑦 + (♯‘𝐴))), (𝐵‘((𝑦 + (♯‘𝐴)) − (♯‘𝐴)))) ∈ 𝑆)) | 
| 78 | 71, 77 | syl 17 | . . . . . . . . . . . 12
⊢ (((𝐴 ∈ Word V ∧ 𝐵 ∈ Word V) ∧ 𝑦 ∈
(0..^(♯‘𝐵)))
→ (∀𝑥 ∈
(0..^((♯‘𝐴) +
(♯‘𝐵)))if(𝑥 ∈
(0..^(♯‘𝐴)),
(𝐴‘𝑥), (𝐵‘(𝑥 − (♯‘𝐴)))) ∈ 𝑆 → if((𝑦 + (♯‘𝐴)) ∈ (0..^(♯‘𝐴)), (𝐴‘(𝑦 + (♯‘𝐴))), (𝐵‘((𝑦 + (♯‘𝐴)) − (♯‘𝐴)))) ∈ 𝑆)) | 
| 79 | 18 | nn0red 12590 | . . . . . . . . . . . . . . . . . . . 20
⊢ (𝐴 ∈ Word V →
(♯‘𝐴) ∈
ℝ) | 
| 80 | 79 | adantr 480 | . . . . . . . . . . . . . . . . . . 19
⊢ ((𝐴 ∈ Word V ∧ 𝐵 ∈ Word V) →
(♯‘𝐴) ∈
ℝ) | 
| 81 | 80 | adantr 480 | . . . . . . . . . . . . . . . . . 18
⊢ (((𝐴 ∈ Word V ∧ 𝐵 ∈ Word V) ∧ 𝑦 ∈
(0..^(♯‘𝐵)))
→ (♯‘𝐴)
∈ ℝ) | 
| 82 |  | elfzoelz 13700 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑦 ∈
(0..^(♯‘𝐵))
→ 𝑦 ∈
ℤ) | 
| 83 | 82 | zred 12724 | . . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑦 ∈
(0..^(♯‘𝐵))
→ 𝑦 ∈
ℝ) | 
| 84 | 83 | adantr 480 | . . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑦 ∈
(0..^(♯‘𝐵))
∧ (𝐴 ∈ Word V
∧ 𝐵 ∈ Word V))
→ 𝑦 ∈
ℝ) | 
| 85 | 80 | adantl 481 | . . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑦 ∈
(0..^(♯‘𝐵))
∧ (𝐴 ∈ Word V
∧ 𝐵 ∈ Word V))
→ (♯‘𝐴)
∈ ℝ) | 
| 86 | 84, 85 | readdcld 11291 | . . . . . . . . . . . . . . . . . . 19
⊢ ((𝑦 ∈
(0..^(♯‘𝐵))
∧ (𝐴 ∈ Word V
∧ 𝐵 ∈ Word V))
→ (𝑦 +
(♯‘𝐴)) ∈
ℝ) | 
| 87 | 86 | ancoms 458 | . . . . . . . . . . . . . . . . . 18
⊢ (((𝐴 ∈ Word V ∧ 𝐵 ∈ Word V) ∧ 𝑦 ∈
(0..^(♯‘𝐵)))
→ (𝑦 +
(♯‘𝐴)) ∈
ℝ) | 
| 88 |  | elfzole1 13708 | . . . . . . . . . . . . . . . . . . . 20
⊢ (𝑦 ∈
(0..^(♯‘𝐵))
→ 0 ≤ 𝑦) | 
| 89 | 88 | adantl 481 | . . . . . . . . . . . . . . . . . . 19
⊢ (((𝐴 ∈ Word V ∧ 𝐵 ∈ Word V) ∧ 𝑦 ∈
(0..^(♯‘𝐵)))
→ 0 ≤ 𝑦) | 
| 90 |  | addge02 11775 | . . . . . . . . . . . . . . . . . . . 20
⊢
(((♯‘𝐴)
∈ ℝ ∧ 𝑦
∈ ℝ) → (0 ≤ 𝑦 ↔ (♯‘𝐴) ≤ (𝑦 + (♯‘𝐴)))) | 
| 91 | 80, 83, 90 | syl2an 596 | . . . . . . . . . . . . . . . . . . 19
⊢ (((𝐴 ∈ Word V ∧ 𝐵 ∈ Word V) ∧ 𝑦 ∈
(0..^(♯‘𝐵)))
→ (0 ≤ 𝑦 ↔
(♯‘𝐴) ≤
(𝑦 + (♯‘𝐴)))) | 
| 92 | 89, 91 | mpbid 232 | . . . . . . . . . . . . . . . . . 18
⊢ (((𝐴 ∈ Word V ∧ 𝐵 ∈ Word V) ∧ 𝑦 ∈
(0..^(♯‘𝐵)))
→ (♯‘𝐴)
≤ (𝑦 +
(♯‘𝐴))) | 
| 93 | 81, 87, 92 | lensymd 11413 | . . . . . . . . . . . . . . . . 17
⊢ (((𝐴 ∈ Word V ∧ 𝐵 ∈ Word V) ∧ 𝑦 ∈
(0..^(♯‘𝐵)))
→ ¬ (𝑦 +
(♯‘𝐴)) <
(♯‘𝐴)) | 
| 94 | 93 | intn3an3d 1482 | . . . . . . . . . . . . . . . 16
⊢ (((𝐴 ∈ Word V ∧ 𝐵 ∈ Word V) ∧ 𝑦 ∈
(0..^(♯‘𝐵)))
→ ¬ ((𝑦 +
(♯‘𝐴)) ∈
ℕ0 ∧ (♯‘𝐴) ∈ ℕ ∧ (𝑦 + (♯‘𝐴)) < (♯‘𝐴))) | 
| 95 |  | elfzo0 13741 | . . . . . . . . . . . . . . . 16
⊢ ((𝑦 + (♯‘𝐴)) ∈
(0..^(♯‘𝐴))
↔ ((𝑦 +
(♯‘𝐴)) ∈
ℕ0 ∧ (♯‘𝐴) ∈ ℕ ∧ (𝑦 + (♯‘𝐴)) < (♯‘𝐴))) | 
| 96 | 94, 95 | sylnibr 329 | . . . . . . . . . . . . . . 15
⊢ (((𝐴 ∈ Word V ∧ 𝐵 ∈ Word V) ∧ 𝑦 ∈
(0..^(♯‘𝐵)))
→ ¬ (𝑦 +
(♯‘𝐴)) ∈
(0..^(♯‘𝐴))) | 
| 97 | 96 | iffalsed 4535 | . . . . . . . . . . . . . 14
⊢ (((𝐴 ∈ Word V ∧ 𝐵 ∈ Word V) ∧ 𝑦 ∈
(0..^(♯‘𝐵)))
→ if((𝑦 +
(♯‘𝐴)) ∈
(0..^(♯‘𝐴)),
(𝐴‘(𝑦 + (♯‘𝐴))), (𝐵‘((𝑦 + (♯‘𝐴)) − (♯‘𝐴)))) = (𝐵‘((𝑦 + (♯‘𝐴)) − (♯‘𝐴)))) | 
| 98 | 97 | eleq1d 2825 | . . . . . . . . . . . . 13
⊢ (((𝐴 ∈ Word V ∧ 𝐵 ∈ Word V) ∧ 𝑦 ∈
(0..^(♯‘𝐵)))
→ (if((𝑦 +
(♯‘𝐴)) ∈
(0..^(♯‘𝐴)),
(𝐴‘(𝑦 + (♯‘𝐴))), (𝐵‘((𝑦 + (♯‘𝐴)) − (♯‘𝐴)))) ∈ 𝑆 ↔ (𝐵‘((𝑦 + (♯‘𝐴)) − (♯‘𝐴))) ∈ 𝑆)) | 
| 99 | 82 | zcnd 12725 | . . . . . . . . . . . . . . . . 17
⊢ (𝑦 ∈
(0..^(♯‘𝐵))
→ 𝑦 ∈
ℂ) | 
| 100 | 65 | adantr 480 | . . . . . . . . . . . . . . . . 17
⊢ ((𝐴 ∈ Word V ∧ 𝐵 ∈ Word V) →
(♯‘𝐴) ∈
ℂ) | 
| 101 |  | pncan 11515 | . . . . . . . . . . . . . . . . 17
⊢ ((𝑦 ∈ ℂ ∧
(♯‘𝐴) ∈
ℂ) → ((𝑦 +
(♯‘𝐴)) −
(♯‘𝐴)) = 𝑦) | 
| 102 | 99, 100, 101 | syl2anr 597 | . . . . . . . . . . . . . . . 16
⊢ (((𝐴 ∈ Word V ∧ 𝐵 ∈ Word V) ∧ 𝑦 ∈
(0..^(♯‘𝐵)))
→ ((𝑦 +
(♯‘𝐴)) −
(♯‘𝐴)) = 𝑦) | 
| 103 | 102 | fveq2d 6909 | . . . . . . . . . . . . . . 15
⊢ (((𝐴 ∈ Word V ∧ 𝐵 ∈ Word V) ∧ 𝑦 ∈
(0..^(♯‘𝐵)))
→ (𝐵‘((𝑦 + (♯‘𝐴)) − (♯‘𝐴))) = (𝐵‘𝑦)) | 
| 104 | 103 | eleq1d 2825 | . . . . . . . . . . . . . 14
⊢ (((𝐴 ∈ Word V ∧ 𝐵 ∈ Word V) ∧ 𝑦 ∈
(0..^(♯‘𝐵)))
→ ((𝐵‘((𝑦 + (♯‘𝐴)) − (♯‘𝐴))) ∈ 𝑆 ↔ (𝐵‘𝑦) ∈ 𝑆)) | 
| 105 | 104 | biimpd 229 | . . . . . . . . . . . . 13
⊢ (((𝐴 ∈ Word V ∧ 𝐵 ∈ Word V) ∧ 𝑦 ∈
(0..^(♯‘𝐵)))
→ ((𝐵‘((𝑦 + (♯‘𝐴)) − (♯‘𝐴))) ∈ 𝑆 → (𝐵‘𝑦) ∈ 𝑆)) | 
| 106 | 98, 105 | sylbid 240 | . . . . . . . . . . . 12
⊢ (((𝐴 ∈ Word V ∧ 𝐵 ∈ Word V) ∧ 𝑦 ∈
(0..^(♯‘𝐵)))
→ (if((𝑦 +
(♯‘𝐴)) ∈
(0..^(♯‘𝐴)),
(𝐴‘(𝑦 + (♯‘𝐴))), (𝐵‘((𝑦 + (♯‘𝐴)) − (♯‘𝐴)))) ∈ 𝑆 → (𝐵‘𝑦) ∈ 𝑆)) | 
| 107 | 78, 106 | syld 47 | . . . . . . . . . . 11
⊢ (((𝐴 ∈ Word V ∧ 𝐵 ∈ Word V) ∧ 𝑦 ∈
(0..^(♯‘𝐵)))
→ (∀𝑥 ∈
(0..^((♯‘𝐴) +
(♯‘𝐵)))if(𝑥 ∈
(0..^(♯‘𝐴)),
(𝐴‘𝑥), (𝐵‘(𝑥 − (♯‘𝐴)))) ∈ 𝑆 → (𝐵‘𝑦) ∈ 𝑆)) | 
| 108 | 107 | impancom 451 | . . . . . . . . . 10
⊢ (((𝐴 ∈ Word V ∧ 𝐵 ∈ Word V) ∧
∀𝑥 ∈
(0..^((♯‘𝐴) +
(♯‘𝐵)))if(𝑥 ∈
(0..^(♯‘𝐴)),
(𝐴‘𝑥), (𝐵‘(𝑥 − (♯‘𝐴)))) ∈ 𝑆) → (𝑦 ∈ (0..^(♯‘𝐵)) → (𝐵‘𝑦) ∈ 𝑆)) | 
| 109 | 108 | ralrimiv 3144 | . . . . . . . . 9
⊢ (((𝐴 ∈ Word V ∧ 𝐵 ∈ Word V) ∧
∀𝑥 ∈
(0..^((♯‘𝐴) +
(♯‘𝐵)))if(𝑥 ∈
(0..^(♯‘𝐴)),
(𝐴‘𝑥), (𝐵‘(𝑥 − (♯‘𝐴)))) ∈ 𝑆) → ∀𝑦 ∈ (0..^(♯‘𝐵))(𝐵‘𝑦) ∈ 𝑆) | 
| 110 |  | iswrdsymb 14570 | . . . . . . . . 9
⊢ ((𝐵 ∈ Word V ∧
∀𝑦 ∈
(0..^(♯‘𝐵))(𝐵‘𝑦) ∈ 𝑆) → 𝐵 ∈ Word 𝑆) | 
| 111 | 59, 109, 110 | syl2an2r 685 | . . . . . . . 8
⊢ (((𝐴 ∈ Word V ∧ 𝐵 ∈ Word V) ∧
∀𝑥 ∈
(0..^((♯‘𝐴) +
(♯‘𝐵)))if(𝑥 ∈
(0..^(♯‘𝐴)),
(𝐴‘𝑥), (𝐵‘(𝑥 − (♯‘𝐴)))) ∈ 𝑆) → 𝐵 ∈ Word 𝑆) | 
| 112 | 58, 111 | jca 511 | . . . . . . 7
⊢ (((𝐴 ∈ Word V ∧ 𝐵 ∈ Word V) ∧
∀𝑥 ∈
(0..^((♯‘𝐴) +
(♯‘𝐵)))if(𝑥 ∈
(0..^(♯‘𝐴)),
(𝐴‘𝑥), (𝐵‘(𝑥 − (♯‘𝐴)))) ∈ 𝑆) → (𝐴 ∈ Word 𝑆 ∧ 𝐵 ∈ Word 𝑆)) | 
| 113 | 112 | ex 412 | . . . . . 6
⊢ ((𝐴 ∈ Word V ∧ 𝐵 ∈ Word V) →
(∀𝑥 ∈
(0..^((♯‘𝐴) +
(♯‘𝐵)))if(𝑥 ∈
(0..^(♯‘𝐴)),
(𝐴‘𝑥), (𝐵‘(𝑥 − (♯‘𝐴)))) ∈ 𝑆 → (𝐴 ∈ Word 𝑆 ∧ 𝐵 ∈ Word 𝑆))) | 
| 114 | 29, 113 | biimtrrid 243 | . . . . 5
⊢ ((𝐴 ∈ Word V ∧ 𝐵 ∈ Word V) → ((𝑥 ∈
(0..^((♯‘𝐴) +
(♯‘𝐵))) ↦
if(𝑥 ∈
(0..^(♯‘𝐴)),
(𝐴‘𝑥), (𝐵‘(𝑥 − (♯‘𝐴))))):(0..^((♯‘𝐴) + (♯‘𝐵)))⟶𝑆 → (𝐴 ∈ Word 𝑆 ∧ 𝐵 ∈ Word 𝑆))) | 
| 115 | 27, 114 | sylbid 240 | . . . 4
⊢ ((𝐴 ∈ Word V ∧ 𝐵 ∈ Word V) → ((𝑥 ∈
(0..^((♯‘𝐴) +
(♯‘𝐵))) ↦
if(𝑥 ∈
(0..^(♯‘𝐴)),
(𝐴‘𝑥), (𝐵‘(𝑥 − (♯‘𝐴))))):(0..^(♯‘(𝑥 ∈
(0..^((♯‘𝐴) +
(♯‘𝐵))) ↦
if(𝑥 ∈
(0..^(♯‘𝐴)),
(𝐴‘𝑥), (𝐵‘(𝑥 − (♯‘𝐴)))))))⟶𝑆 → (𝐴 ∈ Word 𝑆 ∧ 𝐵 ∈ Word 𝑆))) | 
| 116 | 3, 115 | syl5 34 | . . 3
⊢ ((𝐴 ∈ Word V ∧ 𝐵 ∈ Word V) → ((𝑥 ∈
(0..^((♯‘𝐴) +
(♯‘𝐵))) ↦
if(𝑥 ∈
(0..^(♯‘𝐴)),
(𝐴‘𝑥), (𝐵‘(𝑥 − (♯‘𝐴))))) ∈ Word 𝑆 → (𝐴 ∈ Word 𝑆 ∧ 𝐵 ∈ Word 𝑆))) | 
| 117 | 2, 116 | sylbid 240 | . 2
⊢ ((𝐴 ∈ Word V ∧ 𝐵 ∈ Word V) → ((𝐴 ++ 𝐵) ∈ Word 𝑆 → (𝐴 ∈ Word 𝑆 ∧ 𝐵 ∈ Word 𝑆))) | 
| 118 |  | ccatcl 14613 | . 2
⊢ ((𝐴 ∈ Word 𝑆 ∧ 𝐵 ∈ Word 𝑆) → (𝐴 ++ 𝐵) ∈ Word 𝑆) | 
| 119 | 117, 118 | impbid1 225 | 1
⊢ ((𝐴 ∈ Word V ∧ 𝐵 ∈ Word V) → ((𝐴 ++ 𝐵) ∈ Word 𝑆 ↔ (𝐴 ∈ Word 𝑆 ∧ 𝐵 ∈ Word 𝑆))) |