MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  ccatalpha Structured version   Visualization version   GIF version

Theorem ccatalpha 13756
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.
StepHypRef Expression
1 ccatfval 13736 . . . 4 ((𝐴 ∈ Word V ∧ 𝐵 ∈ Word V) → (𝐴 ++ 𝐵) = (𝑥 ∈ (0..^((♯‘𝐴) + (♯‘𝐵))) ↦ if(𝑥 ∈ (0..^(♯‘𝐴)), (𝐴𝑥), (𝐵‘(𝑥 − (♯‘𝐴))))))
21eleq1d 2850 . . 3 ((𝐴 ∈ Word V ∧ 𝐵 ∈ Word V) → ((𝐴 ++ 𝐵) ∈ Word 𝑆 ↔ (𝑥 ∈ (0..^((♯‘𝐴) + (♯‘𝐵))) ↦ if(𝑥 ∈ (0..^(♯‘𝐴)), (𝐴𝑥), (𝐵‘(𝑥 − (♯‘𝐴))))) ∈ Word 𝑆))
3 wrdf 13677 . . . 4 ((𝑥 ∈ (0..^((♯‘𝐴) + (♯‘𝐵))) ↦ if(𝑥 ∈ (0..^(♯‘𝐴)), (𝐴𝑥), (𝐵‘(𝑥 − (♯‘𝐴))))) ∈ Word 𝑆 → (𝑥 ∈ (0..^((♯‘𝐴) + (♯‘𝐵))) ↦ if(𝑥 ∈ (0..^(♯‘𝐴)), (𝐴𝑥), (𝐵‘(𝑥 − (♯‘𝐴))))):(0..^(♯‘(𝑥 ∈ (0..^((♯‘𝐴) + (♯‘𝐵))) ↦ if(𝑥 ∈ (0..^(♯‘𝐴)), (𝐴𝑥), (𝐵‘(𝑥 − (♯‘𝐴)))))))⟶𝑆)
4 funmpt 6226 . . . . . . . . 9 Fun (𝑥 ∈ (0..^((♯‘𝐴) + (♯‘𝐵))) ↦ if(𝑥 ∈ (0..^(♯‘𝐴)), (𝐴𝑥), (𝐵‘(𝑥 − (♯‘𝐴)))))
5 fzofi 13157 . . . . . . . . . . 11 (0..^((♯‘𝐴) + (♯‘𝐵))) ∈ Fin
6 mptfi 8618 . . . . . . . . . . 11 ((0..^((♯‘𝐴) + (♯‘𝐵))) ∈ Fin → (𝑥 ∈ (0..^((♯‘𝐴) + (♯‘𝐵))) ↦ if(𝑥 ∈ (0..^(♯‘𝐴)), (𝐴𝑥), (𝐵‘(𝑥 − (♯‘𝐴))))) ∈ Fin)
75, 6ax-mp 5 . . . . . . . . . 10 (𝑥 ∈ (0..^((♯‘𝐴) + (♯‘𝐵))) ↦ if(𝑥 ∈ (0..^(♯‘𝐴)), (𝐴𝑥), (𝐵‘(𝑥 − (♯‘𝐴))))) ∈ Fin
8 hashfun 13611 . . . . . . . . . 10 ((𝑥 ∈ (0..^((♯‘𝐴) + (♯‘𝐵))) ↦ if(𝑥 ∈ (0..^(♯‘𝐴)), (𝐴𝑥), (𝐵‘(𝑥 − (♯‘𝐴))))) ∈ Fin → (Fun (𝑥 ∈ (0..^((♯‘𝐴) + (♯‘𝐵))) ↦ if(𝑥 ∈ (0..^(♯‘𝐴)), (𝐴𝑥), (𝐵‘(𝑥 − (♯‘𝐴))))) ↔ (♯‘(𝑥 ∈ (0..^((♯‘𝐴) + (♯‘𝐵))) ↦ if(𝑥 ∈ (0..^(♯‘𝐴)), (𝐴𝑥), (𝐵‘(𝑥 − (♯‘𝐴)))))) = (♯‘dom (𝑥 ∈ (0..^((♯‘𝐴) + (♯‘𝐵))) ↦ if(𝑥 ∈ (0..^(♯‘𝐴)), (𝐴𝑥), (𝐵‘(𝑥 − (♯‘𝐴))))))))
97, 8mp1i 13 . . . . . . . . 9 ((𝐴 ∈ Word V ∧ 𝐵 ∈ Word V) → (Fun (𝑥 ∈ (0..^((♯‘𝐴) + (♯‘𝐵))) ↦ if(𝑥 ∈ (0..^(♯‘𝐴)), (𝐴𝑥), (𝐵‘(𝑥 − (♯‘𝐴))))) ↔ (♯‘(𝑥 ∈ (0..^((♯‘𝐴) + (♯‘𝐵))) ↦ if(𝑥 ∈ (0..^(♯‘𝐴)), (𝐴𝑥), (𝐵‘(𝑥 − (♯‘𝐴)))))) = (♯‘dom (𝑥 ∈ (0..^((♯‘𝐴) + (♯‘𝐵))) ↦ if(𝑥 ∈ (0..^(♯‘𝐴)), (𝐴𝑥), (𝐵‘(𝑥 − (♯‘𝐴))))))))
104, 9mpbii 225 . . . . . . . 8 ((𝐴 ∈ Word V ∧ 𝐵 ∈ Word V) → (♯‘(𝑥 ∈ (0..^((♯‘𝐴) + (♯‘𝐵))) ↦ if(𝑥 ∈ (0..^(♯‘𝐴)), (𝐴𝑥), (𝐵‘(𝑥 − (♯‘𝐴)))))) = (♯‘dom (𝑥 ∈ (0..^((♯‘𝐴) + (♯‘𝐵))) ↦ if(𝑥 ∈ (0..^(♯‘𝐴)), (𝐴𝑥), (𝐵‘(𝑥 − (♯‘𝐴)))))))
11 dmmptg 5935 . . . . . . . . . . 11 (∀𝑥 ∈ (0..^((♯‘𝐴) + (♯‘𝐵)))if(𝑥 ∈ (0..^(♯‘𝐴)), (𝐴𝑥), (𝐵‘(𝑥 − (♯‘𝐴)))) ∈ V → dom (𝑥 ∈ (0..^((♯‘𝐴) + (♯‘𝐵))) ↦ if(𝑥 ∈ (0..^(♯‘𝐴)), (𝐴𝑥), (𝐵‘(𝑥 − (♯‘𝐴))))) = (0..^((♯‘𝐴) + (♯‘𝐵))))
12 fvex 6512 . . . . . . . . . . . . 13 (𝐴𝑥) ∈ V
13 fvex 6512 . . . . . . . . . . . . 13 (𝐵‘(𝑥 − (♯‘𝐴))) ∈ V
1412, 13ifex 4398 . . . . . . . . . . . 12 if(𝑥 ∈ (0..^(♯‘𝐴)), (𝐴𝑥), (𝐵‘(𝑥 − (♯‘𝐴)))) ∈ V
1514a1i 11 . . . . . . . . . . 11 (𝑥 ∈ (0..^((♯‘𝐴) + (♯‘𝐵))) → if(𝑥 ∈ (0..^(♯‘𝐴)), (𝐴𝑥), (𝐵‘(𝑥 − (♯‘𝐴)))) ∈ V)
1611, 15mprg 3102 . . . . . . . . . 10 dom (𝑥 ∈ (0..^((♯‘𝐴) + (♯‘𝐵))) ↦ if(𝑥 ∈ (0..^(♯‘𝐴)), (𝐴𝑥), (𝐵‘(𝑥 − (♯‘𝐴))))) = (0..^((♯‘𝐴) + (♯‘𝐵)))
1716fveq2i 6502 . . . . . . . . 9 (♯‘dom (𝑥 ∈ (0..^((♯‘𝐴) + (♯‘𝐵))) ↦ if(𝑥 ∈ (0..^(♯‘𝐴)), (𝐴𝑥), (𝐵‘(𝑥 − (♯‘𝐴)))))) = (♯‘(0..^((♯‘𝐴) + (♯‘𝐵))))
18 lencl 13694 . . . . . . . . . . 11 (𝐴 ∈ Word V → (♯‘𝐴) ∈ ℕ0)
19 lencl 13694 . . . . . . . . . . 11 (𝐵 ∈ Word V → (♯‘𝐵) ∈ ℕ0)
20 nn0addcl 11744 . . . . . . . . . . 11 (((♯‘𝐴) ∈ ℕ0 ∧ (♯‘𝐵) ∈ ℕ0) → ((♯‘𝐴) + (♯‘𝐵)) ∈ ℕ0)
2118, 19, 20syl2an 586 . . . . . . . . . 10 ((𝐴 ∈ Word V ∧ 𝐵 ∈ Word V) → ((♯‘𝐴) + (♯‘𝐵)) ∈ ℕ0)
22 hashfzo0 13604 . . . . . . . . . 10 (((♯‘𝐴) + (♯‘𝐵)) ∈ ℕ0 → (♯‘(0..^((♯‘𝐴) + (♯‘𝐵)))) = ((♯‘𝐴) + (♯‘𝐵)))
2321, 22syl 17 . . . . . . . . 9 ((𝐴 ∈ Word V ∧ 𝐵 ∈ Word V) → (♯‘(0..^((♯‘𝐴) + (♯‘𝐵)))) = ((♯‘𝐴) + (♯‘𝐵)))
2417, 23syl5eq 2826 . . . . . . . 8 ((𝐴 ∈ Word V ∧ 𝐵 ∈ Word V) → (♯‘dom (𝑥 ∈ (0..^((♯‘𝐴) + (♯‘𝐵))) ↦ if(𝑥 ∈ (0..^(♯‘𝐴)), (𝐴𝑥), (𝐵‘(𝑥 − (♯‘𝐴)))))) = ((♯‘𝐴) + (♯‘𝐵)))
2510, 24eqtrd 2814 . . . . . . 7 ((𝐴 ∈ Word V ∧ 𝐵 ∈ Word V) → (♯‘(𝑥 ∈ (0..^((♯‘𝐴) + (♯‘𝐵))) ↦ if(𝑥 ∈ (0..^(♯‘𝐴)), (𝐴𝑥), (𝐵‘(𝑥 − (♯‘𝐴)))))) = ((♯‘𝐴) + (♯‘𝐵)))
2625oveq2d 6992 . . . . . 6 ((𝐴 ∈ Word V ∧ 𝐵 ∈ Word V) → (0..^(♯‘(𝑥 ∈ (0..^((♯‘𝐴) + (♯‘𝐵))) ↦ if(𝑥 ∈ (0..^(♯‘𝐴)), (𝐴𝑥), (𝐵‘(𝑥 − (♯‘𝐴))))))) = (0..^((♯‘𝐴) + (♯‘𝐵))))
2726feq2d 6330 . . . . 5 ((𝐴 ∈ Word V ∧ 𝐵 ∈ Word V) → ((𝑥 ∈ (0..^((♯‘𝐴) + (♯‘𝐵))) ↦ if(𝑥 ∈ (0..^(♯‘𝐴)), (𝐴𝑥), (𝐵‘(𝑥 − (♯‘𝐴))))):(0..^(♯‘(𝑥 ∈ (0..^((♯‘𝐴) + (♯‘𝐵))) ↦ if(𝑥 ∈ (0..^(♯‘𝐴)), (𝐴𝑥), (𝐵‘(𝑥 − (♯‘𝐴)))))))⟶𝑆 ↔ (𝑥 ∈ (0..^((♯‘𝐴) + (♯‘𝐵))) ↦ if(𝑥 ∈ (0..^(♯‘𝐴)), (𝐴𝑥), (𝐵‘(𝑥 − (♯‘𝐴))))):(0..^((♯‘𝐴) + (♯‘𝐵)))⟶𝑆))
28 eqid 2778 . . . . . . 7 (𝑥 ∈ (0..^((♯‘𝐴) + (♯‘𝐵))) ↦ if(𝑥 ∈ (0..^(♯‘𝐴)), (𝐴𝑥), (𝐵‘(𝑥 − (♯‘𝐴))))) = (𝑥 ∈ (0..^((♯‘𝐴) + (♯‘𝐵))) ↦ if(𝑥 ∈ (0..^(♯‘𝐴)), (𝐴𝑥), (𝐵‘(𝑥 − (♯‘𝐴)))))
2928fmpt 6697 . . . . . 6 (∀𝑥 ∈ (0..^((♯‘𝐴) + (♯‘𝐵)))if(𝑥 ∈ (0..^(♯‘𝐴)), (𝐴𝑥), (𝐵‘(𝑥 − (♯‘𝐴)))) ∈ 𝑆 ↔ (𝑥 ∈ (0..^((♯‘𝐴) + (♯‘𝐵))) ↦ if(𝑥 ∈ (0..^(♯‘𝐴)), (𝐴𝑥), (𝐵‘(𝑥 − (♯‘𝐴))))):(0..^((♯‘𝐴) + (♯‘𝐵)))⟶𝑆)
30 simpl 475 . . . . . . . . 9 ((𝐴 ∈ Word V ∧ 𝐵 ∈ Word V) → 𝐴 ∈ Word V)
31 nn0cn 11718 . . . . . . . . . . . . . . . . . 18 ((♯‘𝐴) ∈ ℕ0 → (♯‘𝐴) ∈ ℂ)
32 nn0cn 11718 . . . . . . . . . . . . . . . . . 18 ((♯‘𝐵) ∈ ℕ0 → (♯‘𝐵) ∈ ℂ)
33 addcom 10626 . . . . . . . . . . . . . . . . . 18 (((♯‘𝐴) ∈ ℂ ∧ (♯‘𝐵) ∈ ℂ) → ((♯‘𝐴) + (♯‘𝐵)) = ((♯‘𝐵) + (♯‘𝐴)))
3431, 32, 33syl2an 586 . . . . . . . . . . . . . . . . 17 (((♯‘𝐴) ∈ ℕ0 ∧ (♯‘𝐵) ∈ ℕ0) → ((♯‘𝐴) + (♯‘𝐵)) = ((♯‘𝐵) + (♯‘𝐴)))
35 nn0z 11818 . . . . . . . . . . . . . . . . . . 19 ((♯‘𝐴) ∈ ℕ0 → (♯‘𝐴) ∈ ℤ)
3635anim1ci 606 . . . . . . . . . . . . . . . . . 18 (((♯‘𝐴) ∈ ℕ0 ∧ (♯‘𝐵) ∈ ℕ0) → ((♯‘𝐵) ∈ ℕ0 ∧ (♯‘𝐴) ∈ ℤ))
37 nn0pzuz 12119 . . . . . . . . . . . . . . . . . 18 (((♯‘𝐵) ∈ ℕ0 ∧ (♯‘𝐴) ∈ ℤ) → ((♯‘𝐵) + (♯‘𝐴)) ∈ (ℤ‘(♯‘𝐴)))
3836, 37syl 17 . . . . . . . . . . . . . . . . 17 (((♯‘𝐴) ∈ ℕ0 ∧ (♯‘𝐵) ∈ ℕ0) → ((♯‘𝐵) + (♯‘𝐴)) ∈ (ℤ‘(♯‘𝐴)))
3934, 38eqeltrd 2866 . . . . . . . . . . . . . . . 16 (((♯‘𝐴) ∈ ℕ0 ∧ (♯‘𝐵) ∈ ℕ0) → ((♯‘𝐴) + (♯‘𝐵)) ∈ (ℤ‘(♯‘𝐴)))
4018, 19, 39syl2an 586 . . . . . . . . . . . . . . 15 ((𝐴 ∈ Word V ∧ 𝐵 ∈ Word V) → ((♯‘𝐴) + (♯‘𝐵)) ∈ (ℤ‘(♯‘𝐴)))
41 fzoss2 12880 . . . . . . . . . . . . . . 15 (((♯‘𝐴) + (♯‘𝐵)) ∈ (ℤ‘(♯‘𝐴)) → (0..^(♯‘𝐴)) ⊆ (0..^((♯‘𝐴) + (♯‘𝐵))))
4240, 41syl 17 . . . . . . . . . . . . . 14 ((𝐴 ∈ Word V ∧ 𝐵 ∈ Word V) → (0..^(♯‘𝐴)) ⊆ (0..^((♯‘𝐴) + (♯‘𝐵))))
4342sselda 3858 . . . . . . . . . . . . 13 (((𝐴 ∈ Word V ∧ 𝐵 ∈ Word V) ∧ 𝑦 ∈ (0..^(♯‘𝐴))) → 𝑦 ∈ (0..^((♯‘𝐴) + (♯‘𝐵))))
44 eleq1 2853 . . . . . . . . . . . . . . . 16 (𝑥 = 𝑦 → (𝑥 ∈ (0..^(♯‘𝐴)) ↔ 𝑦 ∈ (0..^(♯‘𝐴))))
45 fveq2 6499 . . . . . . . . . . . . . . . 16 (𝑥 = 𝑦 → (𝐴𝑥) = (𝐴𝑦))
46 fvoveq1 6999 . . . . . . . . . . . . . . . 16 (𝑥 = 𝑦 → (𝐵‘(𝑥 − (♯‘𝐴))) = (𝐵‘(𝑦 − (♯‘𝐴))))
4744, 45, 46ifbieq12d 4377 . . . . . . . . . . . . . . 15 (𝑥 = 𝑦 → if(𝑥 ∈ (0..^(♯‘𝐴)), (𝐴𝑥), (𝐵‘(𝑥 − (♯‘𝐴)))) = if(𝑦 ∈ (0..^(♯‘𝐴)), (𝐴𝑦), (𝐵‘(𝑦 − (♯‘𝐴)))))
4847eleq1d 2850 . . . . . . . . . . . . . 14 (𝑥 = 𝑦 → (if(𝑥 ∈ (0..^(♯‘𝐴)), (𝐴𝑥), (𝐵‘(𝑥 − (♯‘𝐴)))) ∈ 𝑆 ↔ if(𝑦 ∈ (0..^(♯‘𝐴)), (𝐴𝑦), (𝐵‘(𝑦 − (♯‘𝐴)))) ∈ 𝑆))
4948rspcv 3531 . . . . . . . . . . . . 13 (𝑦 ∈ (0..^((♯‘𝐴) + (♯‘𝐵))) → (∀𝑥 ∈ (0..^((♯‘𝐴) + (♯‘𝐵)))if(𝑥 ∈ (0..^(♯‘𝐴)), (𝐴𝑥), (𝐵‘(𝑥 − (♯‘𝐴)))) ∈ 𝑆 → if(𝑦 ∈ (0..^(♯‘𝐴)), (𝐴𝑦), (𝐵‘(𝑦 − (♯‘𝐴)))) ∈ 𝑆))
5043, 49syl 17 . . . . . . . . . . . 12 (((𝐴 ∈ Word V ∧ 𝐵 ∈ Word V) ∧ 𝑦 ∈ (0..^(♯‘𝐴))) → (∀𝑥 ∈ (0..^((♯‘𝐴) + (♯‘𝐵)))if(𝑥 ∈ (0..^(♯‘𝐴)), (𝐴𝑥), (𝐵‘(𝑥 − (♯‘𝐴)))) ∈ 𝑆 → if(𝑦 ∈ (0..^(♯‘𝐴)), (𝐴𝑦), (𝐵‘(𝑦 − (♯‘𝐴)))) ∈ 𝑆))
51 iftrue 4356 . . . . . . . . . . . . . 14 (𝑦 ∈ (0..^(♯‘𝐴)) → if(𝑦 ∈ (0..^(♯‘𝐴)), (𝐴𝑦), (𝐵‘(𝑦 − (♯‘𝐴)))) = (𝐴𝑦))
5251adantl 474 . . . . . . . . . . . . 13 (((𝐴 ∈ Word V ∧ 𝐵 ∈ Word V) ∧ 𝑦 ∈ (0..^(♯‘𝐴))) → if(𝑦 ∈ (0..^(♯‘𝐴)), (𝐴𝑦), (𝐵‘(𝑦 − (♯‘𝐴)))) = (𝐴𝑦))
5352eleq1d 2850 . . . . . . . . . . . 12 (((𝐴 ∈ Word V ∧ 𝐵 ∈ Word V) ∧ 𝑦 ∈ (0..^(♯‘𝐴))) → (if(𝑦 ∈ (0..^(♯‘𝐴)), (𝐴𝑦), (𝐵‘(𝑦 − (♯‘𝐴)))) ∈ 𝑆 ↔ (𝐴𝑦) ∈ 𝑆))
5450, 53sylibd 231 . . . . . . . . . . 11 (((𝐴 ∈ Word V ∧ 𝐵 ∈ Word V) ∧ 𝑦 ∈ (0..^(♯‘𝐴))) → (∀𝑥 ∈ (0..^((♯‘𝐴) + (♯‘𝐵)))if(𝑥 ∈ (0..^(♯‘𝐴)), (𝐴𝑥), (𝐵‘(𝑥 − (♯‘𝐴)))) ∈ 𝑆 → (𝐴𝑦) ∈ 𝑆))
5554impancom 444 . . . . . . . . . 10 (((𝐴 ∈ Word V ∧ 𝐵 ∈ Word V) ∧ ∀𝑥 ∈ (0..^((♯‘𝐴) + (♯‘𝐵)))if(𝑥 ∈ (0..^(♯‘𝐴)), (𝐴𝑥), (𝐵‘(𝑥 − (♯‘𝐴)))) ∈ 𝑆) → (𝑦 ∈ (0..^(♯‘𝐴)) → (𝐴𝑦) ∈ 𝑆))
5655ralrimiv 3131 . . . . . . . . 9 (((𝐴 ∈ Word V ∧ 𝐵 ∈ Word V) ∧ ∀𝑥 ∈ (0..^((♯‘𝐴) + (♯‘𝐵)))if(𝑥 ∈ (0..^(♯‘𝐴)), (𝐴𝑥), (𝐵‘(𝑥 − (♯‘𝐴)))) ∈ 𝑆) → ∀𝑦 ∈ (0..^(♯‘𝐴))(𝐴𝑦) ∈ 𝑆)
57 iswrdsymb 13692 . . . . . . . . 9 ((𝐴 ∈ Word V ∧ ∀𝑦 ∈ (0..^(♯‘𝐴))(𝐴𝑦) ∈ 𝑆) → 𝐴 ∈ Word 𝑆)
5830, 56, 57syl2an2r 672 . . . . . . . 8 (((𝐴 ∈ Word V ∧ 𝐵 ∈ Word V) ∧ ∀𝑥 ∈ (0..^((♯‘𝐴) + (♯‘𝐵)))if(𝑥 ∈ (0..^(♯‘𝐴)), (𝐴𝑥), (𝐵‘(𝑥 − (♯‘𝐴)))) ∈ 𝑆) → 𝐴 ∈ Word 𝑆)
59 simpr 477 . . . . . . . . 9 ((𝐴 ∈ Word V ∧ 𝐵 ∈ Word V) → 𝐵 ∈ Word V)
60 simpr 477 . . . . . . . . . . . . . . 15 (((𝐴 ∈ Word V ∧ 𝐵 ∈ Word V) ∧ 𝑦 ∈ (0..^(♯‘𝐵))) → 𝑦 ∈ (0..^(♯‘𝐵)))
6118adantr 473 . . . . . . . . . . . . . . . 16 ((𝐴 ∈ Word V ∧ 𝐵 ∈ Word V) → (♯‘𝐴) ∈ ℕ0)
6261adantr 473 . . . . . . . . . . . . . . 15 (((𝐴 ∈ Word V ∧ 𝐵 ∈ Word V) ∧ 𝑦 ∈ (0..^(♯‘𝐵))) → (♯‘𝐴) ∈ ℕ0)
63 elincfzoext 12910 . . . . . . . . . . . . . . 15 ((𝑦 ∈ (0..^(♯‘𝐵)) ∧ (♯‘𝐴) ∈ ℕ0) → (𝑦 + (♯‘𝐴)) ∈ (0..^((♯‘𝐵) + (♯‘𝐴))))
6460, 62, 63syl2anc 576 . . . . . . . . . . . . . 14 (((𝐴 ∈ Word V ∧ 𝐵 ∈ Word V) ∧ 𝑦 ∈ (0..^(♯‘𝐵))) → (𝑦 + (♯‘𝐴)) ∈ (0..^((♯‘𝐵) + (♯‘𝐴))))
6518nn0cnd 11769 . . . . . . . . . . . . . . . . . 18 (𝐴 ∈ Word V → (♯‘𝐴) ∈ ℂ)
6619nn0cnd 11769 . . . . . . . . . . . . . . . . . 18 (𝐵 ∈ Word V → (♯‘𝐵) ∈ ℂ)
6765, 66, 33syl2an 586 . . . . . . . . . . . . . . . . 17 ((𝐴 ∈ Word V ∧ 𝐵 ∈ Word V) → ((♯‘𝐴) + (♯‘𝐵)) = ((♯‘𝐵) + (♯‘𝐴)))
6867oveq2d 6992 . . . . . . . . . . . . . . . 16 ((𝐴 ∈ Word V ∧ 𝐵 ∈ Word V) → (0..^((♯‘𝐴) + (♯‘𝐵))) = (0..^((♯‘𝐵) + (♯‘𝐴))))
6968eleq2d 2851 . . . . . . . . . . . . . . 15 ((𝐴 ∈ Word V ∧ 𝐵 ∈ Word V) → ((𝑦 + (♯‘𝐴)) ∈ (0..^((♯‘𝐴) + (♯‘𝐵))) ↔ (𝑦 + (♯‘𝐴)) ∈ (0..^((♯‘𝐵) + (♯‘𝐴)))))
7069adantr 473 . . . . . . . . . . . . . 14 (((𝐴 ∈ Word V ∧ 𝐵 ∈ Word V) ∧ 𝑦 ∈ (0..^(♯‘𝐵))) → ((𝑦 + (♯‘𝐴)) ∈ (0..^((♯‘𝐴) + (♯‘𝐵))) ↔ (𝑦 + (♯‘𝐴)) ∈ (0..^((♯‘𝐵) + (♯‘𝐴)))))
7164, 70mpbird 249 . . . . . . . . . . . . 13 (((𝐴 ∈ Word V ∧ 𝐵 ∈ Word V) ∧ 𝑦 ∈ (0..^(♯‘𝐵))) → (𝑦 + (♯‘𝐴)) ∈ (0..^((♯‘𝐴) + (♯‘𝐵))))
72 eleq1 2853 . . . . . . . . . . . . . . . 16 (𝑥 = (𝑦 + (♯‘𝐴)) → (𝑥 ∈ (0..^(♯‘𝐴)) ↔ (𝑦 + (♯‘𝐴)) ∈ (0..^(♯‘𝐴))))
73 fveq2 6499 . . . . . . . . . . . . . . . 16 (𝑥 = (𝑦 + (♯‘𝐴)) → (𝐴𝑥) = (𝐴‘(𝑦 + (♯‘𝐴))))
74 fvoveq1 6999 . . . . . . . . . . . . . . . 16 (𝑥 = (𝑦 + (♯‘𝐴)) → (𝐵‘(𝑥 − (♯‘𝐴))) = (𝐵‘((𝑦 + (♯‘𝐴)) − (♯‘𝐴))))
7572, 73, 74ifbieq12d 4377 . . . . . . . . . . . . . . 15 (𝑥 = (𝑦 + (♯‘𝐴)) → if(𝑥 ∈ (0..^(♯‘𝐴)), (𝐴𝑥), (𝐵‘(𝑥 − (♯‘𝐴)))) = if((𝑦 + (♯‘𝐴)) ∈ (0..^(♯‘𝐴)), (𝐴‘(𝑦 + (♯‘𝐴))), (𝐵‘((𝑦 + (♯‘𝐴)) − (♯‘𝐴)))))
7675eleq1d 2850 . . . . . . . . . . . . . 14 (𝑥 = (𝑦 + (♯‘𝐴)) → (if(𝑥 ∈ (0..^(♯‘𝐴)), (𝐴𝑥), (𝐵‘(𝑥 − (♯‘𝐴)))) ∈ 𝑆 ↔ if((𝑦 + (♯‘𝐴)) ∈ (0..^(♯‘𝐴)), (𝐴‘(𝑦 + (♯‘𝐴))), (𝐵‘((𝑦 + (♯‘𝐴)) − (♯‘𝐴)))) ∈ 𝑆))
7776rspcv 3531 . . . . . . . . . . . . 13 ((𝑦 + (♯‘𝐴)) ∈ (0..^((♯‘𝐴) + (♯‘𝐵))) → (∀𝑥 ∈ (0..^((♯‘𝐴) + (♯‘𝐵)))if(𝑥 ∈ (0..^(♯‘𝐴)), (𝐴𝑥), (𝐵‘(𝑥 − (♯‘𝐴)))) ∈ 𝑆 → if((𝑦 + (♯‘𝐴)) ∈ (0..^(♯‘𝐴)), (𝐴‘(𝑦 + (♯‘𝐴))), (𝐵‘((𝑦 + (♯‘𝐴)) − (♯‘𝐴)))) ∈ 𝑆))
7871, 77syl 17 . . . . . . . . . . . 12 (((𝐴 ∈ Word V ∧ 𝐵 ∈ Word V) ∧ 𝑦 ∈ (0..^(♯‘𝐵))) → (∀𝑥 ∈ (0..^((♯‘𝐴) + (♯‘𝐵)))if(𝑥 ∈ (0..^(♯‘𝐴)), (𝐴𝑥), (𝐵‘(𝑥 − (♯‘𝐴)))) ∈ 𝑆 → if((𝑦 + (♯‘𝐴)) ∈ (0..^(♯‘𝐴)), (𝐴‘(𝑦 + (♯‘𝐴))), (𝐵‘((𝑦 + (♯‘𝐴)) − (♯‘𝐴)))) ∈ 𝑆))
7918nn0red 11768 . . . . . . . . . . . . . . . . . . . 20 (𝐴 ∈ Word V → (♯‘𝐴) ∈ ℝ)
8079adantr 473 . . . . . . . . . . . . . . . . . . 19 ((𝐴 ∈ Word V ∧ 𝐵 ∈ Word V) → (♯‘𝐴) ∈ ℝ)
8180adantr 473 . . . . . . . . . . . . . . . . . 18 (((𝐴 ∈ Word V ∧ 𝐵 ∈ Word V) ∧ 𝑦 ∈ (0..^(♯‘𝐵))) → (♯‘𝐴) ∈ ℝ)
82 elfzoelz 12854 . . . . . . . . . . . . . . . . . . . . . 22 (𝑦 ∈ (0..^(♯‘𝐵)) → 𝑦 ∈ ℤ)
8382zred 11900 . . . . . . . . . . . . . . . . . . . . 21 (𝑦 ∈ (0..^(♯‘𝐵)) → 𝑦 ∈ ℝ)
8483adantr 473 . . . . . . . . . . . . . . . . . . . 20 ((𝑦 ∈ (0..^(♯‘𝐵)) ∧ (𝐴 ∈ Word V ∧ 𝐵 ∈ Word V)) → 𝑦 ∈ ℝ)
8580adantl 474 . . . . . . . . . . . . . . . . . . . 20 ((𝑦 ∈ (0..^(♯‘𝐵)) ∧ (𝐴 ∈ Word V ∧ 𝐵 ∈ Word V)) → (♯‘𝐴) ∈ ℝ)
8684, 85readdcld 10469 . . . . . . . . . . . . . . . . . . 19 ((𝑦 ∈ (0..^(♯‘𝐵)) ∧ (𝐴 ∈ Word V ∧ 𝐵 ∈ Word V)) → (𝑦 + (♯‘𝐴)) ∈ ℝ)
8786ancoms 451 . . . . . . . . . . . . . . . . . 18 (((𝐴 ∈ Word V ∧ 𝐵 ∈ Word V) ∧ 𝑦 ∈ (0..^(♯‘𝐵))) → (𝑦 + (♯‘𝐴)) ∈ ℝ)
88 elfzole1 12862 . . . . . . . . . . . . . . . . . . . 20 (𝑦 ∈ (0..^(♯‘𝐵)) → 0 ≤ 𝑦)
8988adantl 474 . . . . . . . . . . . . . . . . . . 19 (((𝐴 ∈ Word V ∧ 𝐵 ∈ Word V) ∧ 𝑦 ∈ (0..^(♯‘𝐵))) → 0 ≤ 𝑦)
90 addge02 10952 . . . . . . . . . . . . . . . . . . . 20 (((♯‘𝐴) ∈ ℝ ∧ 𝑦 ∈ ℝ) → (0 ≤ 𝑦 ↔ (♯‘𝐴) ≤ (𝑦 + (♯‘𝐴))))
9180, 83, 90syl2an 586 . . . . . . . . . . . . . . . . . . 19 (((𝐴 ∈ Word V ∧ 𝐵 ∈ Word V) ∧ 𝑦 ∈ (0..^(♯‘𝐵))) → (0 ≤ 𝑦 ↔ (♯‘𝐴) ≤ (𝑦 + (♯‘𝐴))))
9289, 91mpbid 224 . . . . . . . . . . . . . . . . . 18 (((𝐴 ∈ Word V ∧ 𝐵 ∈ Word V) ∧ 𝑦 ∈ (0..^(♯‘𝐵))) → (♯‘𝐴) ≤ (𝑦 + (♯‘𝐴)))
9381, 87, 92lensymd 10591 . . . . . . . . . . . . . . . . 17 (((𝐴 ∈ Word V ∧ 𝐵 ∈ Word V) ∧ 𝑦 ∈ (0..^(♯‘𝐵))) → ¬ (𝑦 + (♯‘𝐴)) < (♯‘𝐴))
9493intn3an3d 1460 . . . . . . . . . . . . . . . 16 (((𝐴 ∈ Word V ∧ 𝐵 ∈ Word V) ∧ 𝑦 ∈ (0..^(♯‘𝐵))) → ¬ ((𝑦 + (♯‘𝐴)) ∈ ℕ0 ∧ (♯‘𝐴) ∈ ℕ ∧ (𝑦 + (♯‘𝐴)) < (♯‘𝐴)))
95 elfzo0 12893 . . . . . . . . . . . . . . . 16 ((𝑦 + (♯‘𝐴)) ∈ (0..^(♯‘𝐴)) ↔ ((𝑦 + (♯‘𝐴)) ∈ ℕ0 ∧ (♯‘𝐴) ∈ ℕ ∧ (𝑦 + (♯‘𝐴)) < (♯‘𝐴)))
9694, 95sylnibr 321 . . . . . . . . . . . . . . 15 (((𝐴 ∈ Word V ∧ 𝐵 ∈ Word V) ∧ 𝑦 ∈ (0..^(♯‘𝐵))) → ¬ (𝑦 + (♯‘𝐴)) ∈ (0..^(♯‘𝐴)))
9796iffalsed 4361 . . . . . . . . . . . . . 14 (((𝐴 ∈ Word V ∧ 𝐵 ∈ Word V) ∧ 𝑦 ∈ (0..^(♯‘𝐵))) → if((𝑦 + (♯‘𝐴)) ∈ (0..^(♯‘𝐴)), (𝐴‘(𝑦 + (♯‘𝐴))), (𝐵‘((𝑦 + (♯‘𝐴)) − (♯‘𝐴)))) = (𝐵‘((𝑦 + (♯‘𝐴)) − (♯‘𝐴))))
9897eleq1d 2850 . . . . . . . . . . . . 13 (((𝐴 ∈ Word V ∧ 𝐵 ∈ Word V) ∧ 𝑦 ∈ (0..^(♯‘𝐵))) → (if((𝑦 + (♯‘𝐴)) ∈ (0..^(♯‘𝐴)), (𝐴‘(𝑦 + (♯‘𝐴))), (𝐵‘((𝑦 + (♯‘𝐴)) − (♯‘𝐴)))) ∈ 𝑆 ↔ (𝐵‘((𝑦 + (♯‘𝐴)) − (♯‘𝐴))) ∈ 𝑆))
9982zcnd 11901 . . . . . . . . . . . . . . . . 17 (𝑦 ∈ (0..^(♯‘𝐵)) → 𝑦 ∈ ℂ)
10065adantr 473 . . . . . . . . . . . . . . . . 17 ((𝐴 ∈ Word V ∧ 𝐵 ∈ Word V) → (♯‘𝐴) ∈ ℂ)
101 pncan 10692 . . . . . . . . . . . . . . . . 17 ((𝑦 ∈ ℂ ∧ (♯‘𝐴) ∈ ℂ) → ((𝑦 + (♯‘𝐴)) − (♯‘𝐴)) = 𝑦)
10299, 100, 101syl2anr 587 . . . . . . . . . . . . . . . 16 (((𝐴 ∈ Word V ∧ 𝐵 ∈ Word V) ∧ 𝑦 ∈ (0..^(♯‘𝐵))) → ((𝑦 + (♯‘𝐴)) − (♯‘𝐴)) = 𝑦)
103102fveq2d 6503 . . . . . . . . . . . . . . 15 (((𝐴 ∈ Word V ∧ 𝐵 ∈ Word V) ∧ 𝑦 ∈ (0..^(♯‘𝐵))) → (𝐵‘((𝑦 + (♯‘𝐴)) − (♯‘𝐴))) = (𝐵𝑦))
104103eleq1d 2850 . . . . . . . . . . . . . 14 (((𝐴 ∈ Word V ∧ 𝐵 ∈ Word V) ∧ 𝑦 ∈ (0..^(♯‘𝐵))) → ((𝐵‘((𝑦 + (♯‘𝐴)) − (♯‘𝐴))) ∈ 𝑆 ↔ (𝐵𝑦) ∈ 𝑆))
105104biimpd 221 . . . . . . . . . . . . 13 (((𝐴 ∈ Word V ∧ 𝐵 ∈ Word V) ∧ 𝑦 ∈ (0..^(♯‘𝐵))) → ((𝐵‘((𝑦 + (♯‘𝐴)) − (♯‘𝐴))) ∈ 𝑆 → (𝐵𝑦) ∈ 𝑆))
10698, 105sylbid 232 . . . . . . . . . . . 12 (((𝐴 ∈ Word V ∧ 𝐵 ∈ Word V) ∧ 𝑦 ∈ (0..^(♯‘𝐵))) → (if((𝑦 + (♯‘𝐴)) ∈ (0..^(♯‘𝐴)), (𝐴‘(𝑦 + (♯‘𝐴))), (𝐵‘((𝑦 + (♯‘𝐴)) − (♯‘𝐴)))) ∈ 𝑆 → (𝐵𝑦) ∈ 𝑆))
10778, 106syld 47 . . . . . . . . . . 11 (((𝐴 ∈ Word V ∧ 𝐵 ∈ Word V) ∧ 𝑦 ∈ (0..^(♯‘𝐵))) → (∀𝑥 ∈ (0..^((♯‘𝐴) + (♯‘𝐵)))if(𝑥 ∈ (0..^(♯‘𝐴)), (𝐴𝑥), (𝐵‘(𝑥 − (♯‘𝐴)))) ∈ 𝑆 → (𝐵𝑦) ∈ 𝑆))
108107impancom 444 . . . . . . . . . 10 (((𝐴 ∈ Word V ∧ 𝐵 ∈ Word V) ∧ ∀𝑥 ∈ (0..^((♯‘𝐴) + (♯‘𝐵)))if(𝑥 ∈ (0..^(♯‘𝐴)), (𝐴𝑥), (𝐵‘(𝑥 − (♯‘𝐴)))) ∈ 𝑆) → (𝑦 ∈ (0..^(♯‘𝐵)) → (𝐵𝑦) ∈ 𝑆))
109108ralrimiv 3131 . . . . . . . . 9 (((𝐴 ∈ Word V ∧ 𝐵 ∈ Word V) ∧ ∀𝑥 ∈ (0..^((♯‘𝐴) + (♯‘𝐵)))if(𝑥 ∈ (0..^(♯‘𝐴)), (𝐴𝑥), (𝐵‘(𝑥 − (♯‘𝐴)))) ∈ 𝑆) → ∀𝑦 ∈ (0..^(♯‘𝐵))(𝐵𝑦) ∈ 𝑆)
110 iswrdsymb 13692 . . . . . . . . 9 ((𝐵 ∈ Word V ∧ ∀𝑦 ∈ (0..^(♯‘𝐵))(𝐵𝑦) ∈ 𝑆) → 𝐵 ∈ Word 𝑆)
11159, 109, 110syl2an2r 672 . . . . . . . 8 (((𝐴 ∈ Word V ∧ 𝐵 ∈ Word V) ∧ ∀𝑥 ∈ (0..^((♯‘𝐴) + (♯‘𝐵)))if(𝑥 ∈ (0..^(♯‘𝐴)), (𝐴𝑥), (𝐵‘(𝑥 − (♯‘𝐴)))) ∈ 𝑆) → 𝐵 ∈ Word 𝑆)
11258, 111jca 504 . . . . . . 7 (((𝐴 ∈ Word V ∧ 𝐵 ∈ Word V) ∧ ∀𝑥 ∈ (0..^((♯‘𝐴) + (♯‘𝐵)))if(𝑥 ∈ (0..^(♯‘𝐴)), (𝐴𝑥), (𝐵‘(𝑥 − (♯‘𝐴)))) ∈ 𝑆) → (𝐴 ∈ Word 𝑆𝐵 ∈ Word 𝑆))
113112ex 405 . . . . . 6 ((𝐴 ∈ Word V ∧ 𝐵 ∈ Word V) → (∀𝑥 ∈ (0..^((♯‘𝐴) + (♯‘𝐵)))if(𝑥 ∈ (0..^(♯‘𝐴)), (𝐴𝑥), (𝐵‘(𝑥 − (♯‘𝐴)))) ∈ 𝑆 → (𝐴 ∈ Word 𝑆𝐵 ∈ Word 𝑆)))
11429, 113syl5bir 235 . . . . 5 ((𝐴 ∈ Word V ∧ 𝐵 ∈ Word V) → ((𝑥 ∈ (0..^((♯‘𝐴) + (♯‘𝐵))) ↦ if(𝑥 ∈ (0..^(♯‘𝐴)), (𝐴𝑥), (𝐵‘(𝑥 − (♯‘𝐴))))):(0..^((♯‘𝐴) + (♯‘𝐵)))⟶𝑆 → (𝐴 ∈ Word 𝑆𝐵 ∈ Word 𝑆)))
11527, 114sylbid 232 . . . 4 ((𝐴 ∈ Word V ∧ 𝐵 ∈ Word V) → ((𝑥 ∈ (0..^((♯‘𝐴) + (♯‘𝐵))) ↦ if(𝑥 ∈ (0..^(♯‘𝐴)), (𝐴𝑥), (𝐵‘(𝑥 − (♯‘𝐴))))):(0..^(♯‘(𝑥 ∈ (0..^((♯‘𝐴) + (♯‘𝐵))) ↦ if(𝑥 ∈ (0..^(♯‘𝐴)), (𝐴𝑥), (𝐵‘(𝑥 − (♯‘𝐴)))))))⟶𝑆 → (𝐴 ∈ Word 𝑆𝐵 ∈ Word 𝑆)))
1163, 115syl5 34 . . 3 ((𝐴 ∈ Word V ∧ 𝐵 ∈ Word V) → ((𝑥 ∈ (0..^((♯‘𝐴) + (♯‘𝐵))) ↦ if(𝑥 ∈ (0..^(♯‘𝐴)), (𝐴𝑥), (𝐵‘(𝑥 − (♯‘𝐴))))) ∈ Word 𝑆 → (𝐴 ∈ Word 𝑆𝐵 ∈ Word 𝑆)))
1172, 116sylbid 232 . 2 ((𝐴 ∈ Word V ∧ 𝐵 ∈ Word V) → ((𝐴 ++ 𝐵) ∈ Word 𝑆 → (𝐴 ∈ Word 𝑆𝐵 ∈ Word 𝑆)))
118 ccatcl 13737 . 2 ((𝐴 ∈ Word 𝑆𝐵 ∈ Word 𝑆) → (𝐴 ++ 𝐵) ∈ Word 𝑆)
119117, 118impbid1 217 1 ((𝐴 ∈ Word V ∧ 𝐵 ∈ Word V) → ((𝐴 ++ 𝐵) ∈ Word 𝑆 ↔ (𝐴 ∈ Word 𝑆𝐵 ∈ Word 𝑆)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 198  wa 387  w3a 1068   = wceq 1507  wcel 2050  wral 3088  Vcvv 3415  wss 3829  ifcif 4350   class class class wbr 4929  cmpt 5008  dom cdm 5407  Fun wfun 6182  wf 6184  cfv 6188  (class class class)co 6976  Fincfn 8306  cc 10333  cr 10334  0cc0 10335   + caddc 10338   < clt 10474  cle 10475  cmin 10670  cn 11439  0cn0 11707  cz 11793  cuz 12058  ..^cfzo 12849  chash 13505  Word cword 13672   ++ cconcat 13733
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1758  ax-4 1772  ax-5 1869  ax-6 1928  ax-7 1965  ax-8 2052  ax-9 2059  ax-10 2079  ax-11 2093  ax-12 2106  ax-13 2301  ax-ext 2750  ax-rep 5049  ax-sep 5060  ax-nul 5067  ax-pow 5119  ax-pr 5186  ax-un 7279  ax-cnex 10391  ax-resscn 10392  ax-1cn 10393  ax-icn 10394  ax-addcl 10395  ax-addrcl 10396  ax-mulcl 10397  ax-mulrcl 10398  ax-mulcom 10399  ax-addass 10400  ax-mulass 10401  ax-distr 10402  ax-i2m1 10403  ax-1ne0 10404  ax-1rid 10405  ax-rnegex 10406  ax-rrecex 10407  ax-cnre 10408  ax-pre-lttri 10409  ax-pre-lttrn 10410  ax-pre-ltadd 10411  ax-pre-mulgt0 10412
This theorem depends on definitions:  df-bi 199  df-an 388  df-or 834  df-3or 1069  df-3an 1070  df-tru 1510  df-ex 1743  df-nf 1747  df-sb 2016  df-mo 2547  df-eu 2584  df-clab 2759  df-cleq 2771  df-clel 2846  df-nfc 2918  df-ne 2968  df-nel 3074  df-ral 3093  df-rex 3094  df-reu 3095  df-rmo 3096  df-rab 3097  df-v 3417  df-sbc 3682  df-csb 3787  df-dif 3832  df-un 3834  df-in 3836  df-ss 3843  df-pss 3845  df-nul 4179  df-if 4351  df-pw 4424  df-sn 4442  df-pr 4444  df-tp 4446  df-op 4448  df-uni 4713  df-int 4750  df-iun 4794  df-br 4930  df-opab 4992  df-mpt 5009  df-tr 5031  df-id 5312  df-eprel 5317  df-po 5326  df-so 5327  df-fr 5366  df-we 5368  df-xp 5413  df-rel 5414  df-cnv 5415  df-co 5416  df-dm 5417  df-rn 5418  df-res 5419  df-ima 5420  df-pred 5986  df-ord 6032  df-on 6033  df-lim 6034  df-suc 6035  df-iota 6152  df-fun 6190  df-fn 6191  df-f 6192  df-f1 6193  df-fo 6194  df-f1o 6195  df-fv 6196  df-riota 6937  df-ov 6979  df-oprab 6980  df-mpo 6981  df-om 7397  df-1st 7501  df-2nd 7502  df-wrecs 7750  df-recs 7812  df-rdg 7850  df-1o 7905  df-oadd 7909  df-er 8089  df-en 8307  df-dom 8308  df-sdom 8309  df-fin 8310  df-dju 9124  df-card 9162  df-pnf 10476  df-mnf 10477  df-xr 10478  df-ltxr 10479  df-le 10480  df-sub 10672  df-neg 10673  df-nn 11440  df-2 11503  df-n0 11708  df-xnn0 11780  df-z 11794  df-uz 12059  df-fz 12709  df-fzo 12850  df-hash 13506  df-word 13673  df-concat 13734
This theorem is referenced by:  ccatrcl1  13757  ccats1alpha  13782  clwwlkwwlksb  27577
  Copyright terms: Public domain W3C validator