This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem ccatalpha

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)

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

Proof

Step Hyp Ref Expression
1 ccatfval ⊢ ( ( 𝐴 ∈ Word V ∧ 𝐵 ∈ Word V ) → ( 𝐴 ++ 𝐵 ) = ( 𝑥 ∈ ( 0 ..^ ( ( ♯ ‘ 𝐴 ) + ( ♯ ‘ 𝐵 ) ) ) ↦ if ( 𝑥 ∈ ( 0 ..^ ( ♯ ‘ 𝐴 ) ) , ( 𝐴 ‘ 𝑥 ) , ( 𝐵 ‘ ( 𝑥 − ( ♯ ‘ 𝐴 ) ) ) ) ) )
2 1 eleq1d ⊢ ( ( 𝐴 ∈ Word V ∧ 𝐵 ∈ Word V ) → ( ( 𝐴 ++ 𝐵 ) ∈ Word 𝑆 ↔ ( 𝑥 ∈ ( 0 ..^ ( ( ♯ ‘ 𝐴 ) + ( ♯ ‘ 𝐵 ) ) ) ↦ if ( 𝑥 ∈ ( 0 ..^ ( ♯ ‘ 𝐴 ) ) , ( 𝐴 ‘ 𝑥 ) , ( 𝐵 ‘ ( 𝑥 − ( ♯ ‘ 𝐴 ) ) ) ) ) ∈ Word 𝑆 ) )
3 wrdf ⊢ ( ( 𝑥 ∈ ( 0 ..^ ( ( ♯ ‘ 𝐴 ) + ( ♯ ‘ 𝐵 ) ) ) ↦ if ( 𝑥 ∈ ( 0 ..^ ( ♯ ‘ 𝐴 ) ) , ( 𝐴 ‘ 𝑥 ) , ( 𝐵 ‘ ( 𝑥 − ( ♯ ‘ 𝐴 ) ) ) ) ) ∈ Word 𝑆 → ( 𝑥 ∈ ( 0 ..^ ( ( ♯ ‘ 𝐴 ) + ( ♯ ‘ 𝐵 ) ) ) ↦ if ( 𝑥 ∈ ( 0 ..^ ( ♯ ‘ 𝐴 ) ) , ( 𝐴 ‘ 𝑥 ) , ( 𝐵 ‘ ( 𝑥 − ( ♯ ‘ 𝐴 ) ) ) ) ) : ( 0 ..^ ( ♯ ‘ ( 𝑥 ∈ ( 0 ..^ ( ( ♯ ‘ 𝐴 ) + ( ♯ ‘ 𝐵 ) ) ) ↦ if ( 𝑥 ∈ ( 0 ..^ ( ♯ ‘ 𝐴 ) ) , ( 𝐴 ‘ 𝑥 ) , ( 𝐵 ‘ ( 𝑥 − ( ♯ ‘ 𝐴 ) ) ) ) ) ) ) ⟶ 𝑆 )
4 funmpt ⊢ Fun ( 𝑥 ∈ ( 0 ..^ ( ( ♯ ‘ 𝐴 ) + ( ♯ ‘ 𝐵 ) ) ) ↦ if ( 𝑥 ∈ ( 0 ..^ ( ♯ ‘ 𝐴 ) ) , ( 𝐴 ‘ 𝑥 ) , ( 𝐵 ‘ ( 𝑥 − ( ♯ ‘ 𝐴 ) ) ) ) )
5 fzofi ⊢ ( 0 ..^ ( ( ♯ ‘ 𝐴 ) + ( ♯ ‘ 𝐵 ) ) ) ∈ Fin
6 mptfi ⊢ ( ( 0 ..^ ( ( ♯ ‘ 𝐴 ) + ( ♯ ‘ 𝐵 ) ) ) ∈ Fin → ( 𝑥 ∈ ( 0 ..^ ( ( ♯ ‘ 𝐴 ) + ( ♯ ‘ 𝐵 ) ) ) ↦ if ( 𝑥 ∈ ( 0 ..^ ( ♯ ‘ 𝐴 ) ) , ( 𝐴 ‘ 𝑥 ) , ( 𝐵 ‘ ( 𝑥 − ( ♯ ‘ 𝐴 ) ) ) ) ) ∈ Fin )
7 5 6 ax-mp ⊢ ( 𝑥 ∈ ( 0 ..^ ( ( ♯ ‘ 𝐴 ) + ( ♯ ‘ 𝐵 ) ) ) ↦ if ( 𝑥 ∈ ( 0 ..^ ( ♯ ‘ 𝐴 ) ) , ( 𝐴 ‘ 𝑥 ) , ( 𝐵 ‘ ( 𝑥 − ( ♯ ‘ 𝐴 ) ) ) ) ) ∈ Fin
8 hashfun ⊢ ( ( 𝑥 ∈ ( 0 ..^ ( ( ♯ ‘ 𝐴 ) + ( ♯ ‘ 𝐵 ) ) ) ↦ if ( 𝑥 ∈ ( 0 ..^ ( ♯ ‘ 𝐴 ) ) , ( 𝐴 ‘ 𝑥 ) , ( 𝐵 ‘ ( 𝑥 − ( ♯ ‘ 𝐴 ) ) ) ) ) ∈ Fin → ( Fun ( 𝑥 ∈ ( 0 ..^ ( ( ♯ ‘ 𝐴 ) + ( ♯ ‘ 𝐵 ) ) ) ↦ if ( 𝑥 ∈ ( 0 ..^ ( ♯ ‘ 𝐴 ) ) , ( 𝐴 ‘ 𝑥 ) , ( 𝐵 ‘ ( 𝑥 − ( ♯ ‘ 𝐴 ) ) ) ) ) ↔ ( ♯ ‘ ( 𝑥 ∈ ( 0 ..^ ( ( ♯ ‘ 𝐴 ) + ( ♯ ‘ 𝐵 ) ) ) ↦ if ( 𝑥 ∈ ( 0 ..^ ( ♯ ‘ 𝐴 ) ) , ( 𝐴 ‘ 𝑥 ) , ( 𝐵 ‘ ( 𝑥 − ( ♯ ‘ 𝐴 ) ) ) ) ) ) = ( ♯ ‘ dom ( 𝑥 ∈ ( 0 ..^ ( ( ♯ ‘ 𝐴 ) + ( ♯ ‘ 𝐵 ) ) ) ↦ if ( 𝑥 ∈ ( 0 ..^ ( ♯ ‘ 𝐴 ) ) , ( 𝐴 ‘ 𝑥 ) , ( 𝐵 ‘ ( 𝑥 − ( ♯ ‘ 𝐴 ) ) ) ) ) ) ) )
9 7 8 mp1i ⊢ ( ( 𝐴 ∈ Word V ∧ 𝐵 ∈ Word V ) → ( Fun ( 𝑥 ∈ ( 0 ..^ ( ( ♯ ‘ 𝐴 ) + ( ♯ ‘ 𝐵 ) ) ) ↦ if ( 𝑥 ∈ ( 0 ..^ ( ♯ ‘ 𝐴 ) ) , ( 𝐴 ‘ 𝑥 ) , ( 𝐵 ‘ ( 𝑥 − ( ♯ ‘ 𝐴 ) ) ) ) ) ↔ ( ♯ ‘ ( 𝑥 ∈ ( 0 ..^ ( ( ♯ ‘ 𝐴 ) + ( ♯ ‘ 𝐵 ) ) ) ↦ if ( 𝑥 ∈ ( 0 ..^ ( ♯ ‘ 𝐴 ) ) , ( 𝐴 ‘ 𝑥 ) , ( 𝐵 ‘ ( 𝑥 − ( ♯ ‘ 𝐴 ) ) ) ) ) ) = ( ♯ ‘ dom ( 𝑥 ∈ ( 0 ..^ ( ( ♯ ‘ 𝐴 ) + ( ♯ ‘ 𝐵 ) ) ) ↦ if ( 𝑥 ∈ ( 0 ..^ ( ♯ ‘ 𝐴 ) ) , ( 𝐴 ‘ 𝑥 ) , ( 𝐵 ‘ ( 𝑥 − ( ♯ ‘ 𝐴 ) ) ) ) ) ) ) )
10 4 9 mpbii ⊢ ( ( 𝐴 ∈ Word V ∧ 𝐵 ∈ Word V ) → ( ♯ ‘ ( 𝑥 ∈ ( 0 ..^ ( ( ♯ ‘ 𝐴 ) + ( ♯ ‘ 𝐵 ) ) ) ↦ if ( 𝑥 ∈ ( 0 ..^ ( ♯ ‘ 𝐴 ) ) , ( 𝐴 ‘ 𝑥 ) , ( 𝐵 ‘ ( 𝑥 − ( ♯ ‘ 𝐴 ) ) ) ) ) ) = ( ♯ ‘ dom ( 𝑥 ∈ ( 0 ..^ ( ( ♯ ‘ 𝐴 ) + ( ♯ ‘ 𝐵 ) ) ) ↦ if ( 𝑥 ∈ ( 0 ..^ ( ♯ ‘ 𝐴 ) ) , ( 𝐴 ‘ 𝑥 ) , ( 𝐵 ‘ ( 𝑥 − ( ♯ ‘ 𝐴 ) ) ) ) ) ) )
11 dmmptg ⊢ ( ∀ 𝑥 ∈ ( 0 ..^ ( ( ♯ ‘ 𝐴 ) + ( ♯ ‘ 𝐵 ) ) ) if ( 𝑥 ∈ ( 0 ..^ ( ♯ ‘ 𝐴 ) ) , ( 𝐴 ‘ 𝑥 ) , ( 𝐵 ‘ ( 𝑥 − ( ♯ ‘ 𝐴 ) ) ) ) ∈ V → dom ( 𝑥 ∈ ( 0 ..^ ( ( ♯ ‘ 𝐴 ) + ( ♯ ‘ 𝐵 ) ) ) ↦ if ( 𝑥 ∈ ( 0 ..^ ( ♯ ‘ 𝐴 ) ) , ( 𝐴 ‘ 𝑥 ) , ( 𝐵 ‘ ( 𝑥 − ( ♯ ‘ 𝐴 ) ) ) ) ) = ( 0 ..^ ( ( ♯ ‘ 𝐴 ) + ( ♯ ‘ 𝐵 ) ) ) )
12 fvex ⊢ ( 𝐴 ‘ 𝑥 ) ∈ V
13 fvex ⊢ ( 𝐵 ‘ ( 𝑥 − ( ♯ ‘ 𝐴 ) ) ) ∈ V
14 12 13 ifex ⊢ if ( 𝑥 ∈ ( 0 ..^ ( ♯ ‘ 𝐴 ) ) , ( 𝐴 ‘ 𝑥 ) , ( 𝐵 ‘ ( 𝑥 − ( ♯ ‘ 𝐴 ) ) ) ) ∈ V
15 14 a1i ⊢ ( 𝑥 ∈ ( 0 ..^ ( ( ♯ ‘ 𝐴 ) + ( ♯ ‘ 𝐵 ) ) ) → if ( 𝑥 ∈ ( 0 ..^ ( ♯ ‘ 𝐴 ) ) , ( 𝐴 ‘ 𝑥 ) , ( 𝐵 ‘ ( 𝑥 − ( ♯ ‘ 𝐴 ) ) ) ) ∈ V )
16 11 15 mprg ⊢ dom ( 𝑥 ∈ ( 0 ..^ ( ( ♯ ‘ 𝐴 ) + ( ♯ ‘ 𝐵 ) ) ) ↦ if ( 𝑥 ∈ ( 0 ..^ ( ♯ ‘ 𝐴 ) ) , ( 𝐴 ‘ 𝑥 ) , ( 𝐵 ‘ ( 𝑥 − ( ♯ ‘ 𝐴 ) ) ) ) ) = ( 0 ..^ ( ( ♯ ‘ 𝐴 ) + ( ♯ ‘ 𝐵 ) ) )
17 16 fveq2i ⊢ ( ♯ ‘ dom ( 𝑥 ∈ ( 0 ..^ ( ( ♯ ‘ 𝐴 ) + ( ♯ ‘ 𝐵 ) ) ) ↦ if ( 𝑥 ∈ ( 0 ..^ ( ♯ ‘ 𝐴 ) ) , ( 𝐴 ‘ 𝑥 ) , ( 𝐵 ‘ ( 𝑥 − ( ♯ ‘ 𝐴 ) ) ) ) ) ) = ( ♯ ‘ ( 0 ..^ ( ( ♯ ‘ 𝐴 ) + ( ♯ ‘ 𝐵 ) ) ) )
18 lencl ⊢ ( 𝐴 ∈ Word V → ( ♯ ‘ 𝐴 ) ∈ ℕ0 )
19 lencl ⊢ ( 𝐵 ∈ Word V → ( ♯ ‘ 𝐵 ) ∈ ℕ0 )
20 nn0addcl ⊢ ( ( ( ♯ ‘ 𝐴 ) ∈ ℕ0 ∧ ( ♯ ‘ 𝐵 ) ∈ ℕ0 ) → ( ( ♯ ‘ 𝐴 ) + ( ♯ ‘ 𝐵 ) ) ∈ ℕ0 )
21 18 19 20 syl2an ⊢ ( ( 𝐴 ∈ Word V ∧ 𝐵 ∈ Word V ) → ( ( ♯ ‘ 𝐴 ) + ( ♯ ‘ 𝐵 ) ) ∈ ℕ0 )
22 hashfzo0 ⊢ ( ( ( ♯ ‘ 𝐴 ) + ( ♯ ‘ 𝐵 ) ) ∈ ℕ0 → ( ♯ ‘ ( 0 ..^ ( ( ♯ ‘ 𝐴 ) + ( ♯ ‘ 𝐵 ) ) ) ) = ( ( ♯ ‘ 𝐴 ) + ( ♯ ‘ 𝐵 ) ) )
23 21 22 syl ⊢ ( ( 𝐴 ∈ Word V ∧ 𝐵 ∈ Word V ) → ( ♯ ‘ ( 0 ..^ ( ( ♯ ‘ 𝐴 ) + ( ♯ ‘ 𝐵 ) ) ) ) = ( ( ♯ ‘ 𝐴 ) + ( ♯ ‘ 𝐵 ) ) )
24 17 23 eqtrid ⊢ ( ( 𝐴 ∈ Word V ∧ 𝐵 ∈ Word V ) → ( ♯ ‘ dom ( 𝑥 ∈ ( 0 ..^ ( ( ♯ ‘ 𝐴 ) + ( ♯ ‘ 𝐵 ) ) ) ↦ if ( 𝑥 ∈ ( 0 ..^ ( ♯ ‘ 𝐴 ) ) , ( 𝐴 ‘ 𝑥 ) , ( 𝐵 ‘ ( 𝑥 − ( ♯ ‘ 𝐴 ) ) ) ) ) ) = ( ( ♯ ‘ 𝐴 ) + ( ♯ ‘ 𝐵 ) ) )
25 10 24 eqtrd ⊢ ( ( 𝐴 ∈ Word V ∧ 𝐵 ∈ Word V ) → ( ♯ ‘ ( 𝑥 ∈ ( 0 ..^ ( ( ♯ ‘ 𝐴 ) + ( ♯ ‘ 𝐵 ) ) ) ↦ if ( 𝑥 ∈ ( 0 ..^ ( ♯ ‘ 𝐴 ) ) , ( 𝐴 ‘ 𝑥 ) , ( 𝐵 ‘ ( 𝑥 − ( ♯ ‘ 𝐴 ) ) ) ) ) ) = ( ( ♯ ‘ 𝐴 ) + ( ♯ ‘ 𝐵 ) ) )
26 25 oveq2d ⊢ ( ( 𝐴 ∈ Word V ∧ 𝐵 ∈ Word V ) → ( 0 ..^ ( ♯ ‘ ( 𝑥 ∈ ( 0 ..^ ( ( ♯ ‘ 𝐴 ) + ( ♯ ‘ 𝐵 ) ) ) ↦ if ( 𝑥 ∈ ( 0 ..^ ( ♯ ‘ 𝐴 ) ) , ( 𝐴 ‘ 𝑥 ) , ( 𝐵 ‘ ( 𝑥 − ( ♯ ‘ 𝐴 ) ) ) ) ) ) ) = ( 0 ..^ ( ( ♯ ‘ 𝐴 ) + ( ♯ ‘ 𝐵 ) ) ) )
27 26 feq2d ⊢ ( ( 𝐴 ∈ Word V ∧ 𝐵 ∈ Word V ) → ( ( 𝑥 ∈ ( 0 ..^ ( ( ♯ ‘ 𝐴 ) + ( ♯ ‘ 𝐵 ) ) ) ↦ if ( 𝑥 ∈ ( 0 ..^ ( ♯ ‘ 𝐴 ) ) , ( 𝐴 ‘ 𝑥 ) , ( 𝐵 ‘ ( 𝑥 − ( ♯ ‘ 𝐴 ) ) ) ) ) : ( 0 ..^ ( ♯ ‘ ( 𝑥 ∈ ( 0 ..^ ( ( ♯ ‘ 𝐴 ) + ( ♯ ‘ 𝐵 ) ) ) ↦ if ( 𝑥 ∈ ( 0 ..^ ( ♯ ‘ 𝐴 ) ) , ( 𝐴 ‘ 𝑥 ) , ( 𝐵 ‘ ( 𝑥 − ( ♯ ‘ 𝐴 ) ) ) ) ) ) ) ⟶ 𝑆 ↔ ( 𝑥 ∈ ( 0 ..^ ( ( ♯ ‘ 𝐴 ) + ( ♯ ‘ 𝐵 ) ) ) ↦ if ( 𝑥 ∈ ( 0 ..^ ( ♯ ‘ 𝐴 ) ) , ( 𝐴 ‘ 𝑥 ) , ( 𝐵 ‘ ( 𝑥 − ( ♯ ‘ 𝐴 ) ) ) ) ) : ( 0 ..^ ( ( ♯ ‘ 𝐴 ) + ( ♯ ‘ 𝐵 ) ) ) ⟶ 𝑆 ) )
28 eqid ⊢ ( 𝑥 ∈ ( 0 ..^ ( ( ♯ ‘ 𝐴 ) + ( ♯ ‘ 𝐵 ) ) ) ↦ if ( 𝑥 ∈ ( 0 ..^ ( ♯ ‘ 𝐴 ) ) , ( 𝐴 ‘ 𝑥 ) , ( 𝐵 ‘ ( 𝑥 − ( ♯ ‘ 𝐴 ) ) ) ) ) = ( 𝑥 ∈ ( 0 ..^ ( ( ♯ ‘ 𝐴 ) + ( ♯ ‘ 𝐵 ) ) ) ↦ if ( 𝑥 ∈ ( 0 ..^ ( ♯ ‘ 𝐴 ) ) , ( 𝐴 ‘ 𝑥 ) , ( 𝐵 ‘ ( 𝑥 − ( ♯ ‘ 𝐴 ) ) ) ) )
29 28 fmpt ⊢ ( ∀ 𝑥 ∈ ( 0 ..^ ( ( ♯ ‘ 𝐴 ) + ( ♯ ‘ 𝐵 ) ) ) if ( 𝑥 ∈ ( 0 ..^ ( ♯ ‘ 𝐴 ) ) , ( 𝐴 ‘ 𝑥 ) , ( 𝐵 ‘ ( 𝑥 − ( ♯ ‘ 𝐴 ) ) ) ) ∈ 𝑆 ↔ ( 𝑥 ∈ ( 0 ..^ ( ( ♯ ‘ 𝐴 ) + ( ♯ ‘ 𝐵 ) ) ) ↦ if ( 𝑥 ∈ ( 0 ..^ ( ♯ ‘ 𝐴 ) ) , ( 𝐴 ‘ 𝑥 ) , ( 𝐵 ‘ ( 𝑥 − ( ♯ ‘ 𝐴 ) ) ) ) ) : ( 0 ..^ ( ( ♯ ‘ 𝐴 ) + ( ♯ ‘ 𝐵 ) ) ) ⟶ 𝑆 )
30 simpl ⊢ ( ( 𝐴 ∈ Word V ∧ 𝐵 ∈ Word V ) → 𝐴 ∈ Word V )
31 nn0cn ⊢ ( ( ♯ ‘ 𝐴 ) ∈ ℕ0 → ( ♯ ‘ 𝐴 ) ∈ ℂ )
32 nn0cn ⊢ ( ( ♯ ‘ 𝐵 ) ∈ ℕ0 → ( ♯ ‘ 𝐵 ) ∈ ℂ )
33 addcom ⊢ ( ( ( ♯ ‘ 𝐴 ) ∈ ℂ ∧ ( ♯ ‘ 𝐵 ) ∈ ℂ ) → ( ( ♯ ‘ 𝐴 ) + ( ♯ ‘ 𝐵 ) ) = ( ( ♯ ‘ 𝐵 ) + ( ♯ ‘ 𝐴 ) ) )
34 31 32 33 syl2an ⊢ ( ( ( ♯ ‘ 𝐴 ) ∈ ℕ0 ∧ ( ♯ ‘ 𝐵 ) ∈ ℕ0 ) → ( ( ♯ ‘ 𝐴 ) + ( ♯ ‘ 𝐵 ) ) = ( ( ♯ ‘ 𝐵 ) + ( ♯ ‘ 𝐴 ) ) )
35 nn0z ⊢ ( ( ♯ ‘ 𝐴 ) ∈ ℕ0 → ( ♯ ‘ 𝐴 ) ∈ ℤ )
36 35 anim1ci ⊢ ( ( ( ♯ ‘ 𝐴 ) ∈ ℕ0 ∧ ( ♯ ‘ 𝐵 ) ∈ ℕ0 ) → ( ( ♯ ‘ 𝐵 ) ∈ ℕ0 ∧ ( ♯ ‘ 𝐴 ) ∈ ℤ ) )
37 nn0pzuz ⊢ ( ( ( ♯ ‘ 𝐵 ) ∈ ℕ0 ∧ ( ♯ ‘ 𝐴 ) ∈ ℤ ) → ( ( ♯ ‘ 𝐵 ) + ( ♯ ‘ 𝐴 ) ) ∈ ( ℤ≥ ‘ ( ♯ ‘ 𝐴 ) ) )
38 36 37 syl ⊢ ( ( ( ♯ ‘ 𝐴 ) ∈ ℕ0 ∧ ( ♯ ‘ 𝐵 ) ∈ ℕ0 ) → ( ( ♯ ‘ 𝐵 ) + ( ♯ ‘ 𝐴 ) ) ∈ ( ℤ≥ ‘ ( ♯ ‘ 𝐴 ) ) )
39 34 38 eqeltrd ⊢ ( ( ( ♯ ‘ 𝐴 ) ∈ ℕ0 ∧ ( ♯ ‘ 𝐵 ) ∈ ℕ0 ) → ( ( ♯ ‘ 𝐴 ) + ( ♯ ‘ 𝐵 ) ) ∈ ( ℤ≥ ‘ ( ♯ ‘ 𝐴 ) ) )
40 18 19 39 syl2an ⊢ ( ( 𝐴 ∈ Word V ∧ 𝐵 ∈ Word V ) → ( ( ♯ ‘ 𝐴 ) + ( ♯ ‘ 𝐵 ) ) ∈ ( ℤ≥ ‘ ( ♯ ‘ 𝐴 ) ) )
41 fzoss2 ⊢ ( ( ( ♯ ‘ 𝐴 ) + ( ♯ ‘ 𝐵 ) ) ∈ ( ℤ≥ ‘ ( ♯ ‘ 𝐴 ) ) → ( 0 ..^ ( ♯ ‘ 𝐴 ) ) ⊆ ( 0 ..^ ( ( ♯ ‘ 𝐴 ) + ( ♯ ‘ 𝐵 ) ) ) )
42 40 41 syl ⊢ ( ( 𝐴 ∈ Word V ∧ 𝐵 ∈ Word V ) → ( 0 ..^ ( ♯ ‘ 𝐴 ) ) ⊆ ( 0 ..^ ( ( ♯ ‘ 𝐴 ) + ( ♯ ‘ 𝐵 ) ) ) )
43 42 sselda ⊢ ( ( ( 𝐴 ∈ Word V ∧ 𝐵 ∈ Word V ) ∧ 𝑦 ∈ ( 0 ..^ ( ♯ ‘ 𝐴 ) ) ) → 𝑦 ∈ ( 0 ..^ ( ( ♯ ‘ 𝐴 ) + ( ♯ ‘ 𝐵 ) ) ) )
44 eleq1 ⊢ ( 𝑥 = 𝑦 → ( 𝑥 ∈ ( 0 ..^ ( ♯ ‘ 𝐴 ) ) ↔ 𝑦 ∈ ( 0 ..^ ( ♯ ‘ 𝐴 ) ) ) )
45 fveq2 ⊢ ( 𝑥 = 𝑦 → ( 𝐴 ‘ 𝑥 ) = ( 𝐴 ‘ 𝑦 ) )
46 fvoveq1 ⊢ ( 𝑥 = 𝑦 → ( 𝐵 ‘ ( 𝑥 − ( ♯ ‘ 𝐴 ) ) ) = ( 𝐵 ‘ ( 𝑦 − ( ♯ ‘ 𝐴 ) ) ) )
47 44 45 46 ifbieq12d ⊢ ( 𝑥 = 𝑦 → if ( 𝑥 ∈ ( 0 ..^ ( ♯ ‘ 𝐴 ) ) , ( 𝐴 ‘ 𝑥 ) , ( 𝐵 ‘ ( 𝑥 − ( ♯ ‘ 𝐴 ) ) ) ) = if ( 𝑦 ∈ ( 0 ..^ ( ♯ ‘ 𝐴 ) ) , ( 𝐴 ‘ 𝑦 ) , ( 𝐵 ‘ ( 𝑦 − ( ♯ ‘ 𝐴 ) ) ) ) )
48 47 eleq1d ⊢ ( 𝑥 = 𝑦 → ( if ( 𝑥 ∈ ( 0 ..^ ( ♯ ‘ 𝐴 ) ) , ( 𝐴 ‘ 𝑥 ) , ( 𝐵 ‘ ( 𝑥 − ( ♯ ‘ 𝐴 ) ) ) ) ∈ 𝑆 ↔ if ( 𝑦 ∈ ( 0 ..^ ( ♯ ‘ 𝐴 ) ) , ( 𝐴 ‘ 𝑦 ) , ( 𝐵 ‘ ( 𝑦 − ( ♯ ‘ 𝐴 ) ) ) ) ∈ 𝑆 ) )
49 48 rspcv ⊢ ( 𝑦 ∈ ( 0 ..^ ( ( ♯ ‘ 𝐴 ) + ( ♯ ‘ 𝐵 ) ) ) → ( ∀ 𝑥 ∈ ( 0 ..^ ( ( ♯ ‘ 𝐴 ) + ( ♯ ‘ 𝐵 ) ) ) if ( 𝑥 ∈ ( 0 ..^ ( ♯ ‘ 𝐴 ) ) , ( 𝐴 ‘ 𝑥 ) , ( 𝐵 ‘ ( 𝑥 − ( ♯ ‘ 𝐴 ) ) ) ) ∈ 𝑆 → if ( 𝑦 ∈ ( 0 ..^ ( ♯ ‘ 𝐴 ) ) , ( 𝐴 ‘ 𝑦 ) , ( 𝐵 ‘ ( 𝑦 − ( ♯ ‘ 𝐴 ) ) ) ) ∈ 𝑆 ) )
50 43 49 syl ⊢ ( ( ( 𝐴 ∈ Word V ∧ 𝐵 ∈ Word V ) ∧ 𝑦 ∈ ( 0 ..^ ( ♯ ‘ 𝐴 ) ) ) → ( ∀ 𝑥 ∈ ( 0 ..^ ( ( ♯ ‘ 𝐴 ) + ( ♯ ‘ 𝐵 ) ) ) if ( 𝑥 ∈ ( 0 ..^ ( ♯ ‘ 𝐴 ) ) , ( 𝐴 ‘ 𝑥 ) , ( 𝐵 ‘ ( 𝑥 − ( ♯ ‘ 𝐴 ) ) ) ) ∈ 𝑆 → if ( 𝑦 ∈ ( 0 ..^ ( ♯ ‘ 𝐴 ) ) , ( 𝐴 ‘ 𝑦 ) , ( 𝐵 ‘ ( 𝑦 − ( ♯ ‘ 𝐴 ) ) ) ) ∈ 𝑆 ) )
51 iftrue ⊢ ( 𝑦 ∈ ( 0 ..^ ( ♯ ‘ 𝐴 ) ) → if ( 𝑦 ∈ ( 0 ..^ ( ♯ ‘ 𝐴 ) ) , ( 𝐴 ‘ 𝑦 ) , ( 𝐵 ‘ ( 𝑦 − ( ♯ ‘ 𝐴 ) ) ) ) = ( 𝐴 ‘ 𝑦 ) )
52 51 adantl ⊢ ( ( ( 𝐴 ∈ Word V ∧ 𝐵 ∈ Word V ) ∧ 𝑦 ∈ ( 0 ..^ ( ♯ ‘ 𝐴 ) ) ) → if ( 𝑦 ∈ ( 0 ..^ ( ♯ ‘ 𝐴 ) ) , ( 𝐴 ‘ 𝑦 ) , ( 𝐵 ‘ ( 𝑦 − ( ♯ ‘ 𝐴 ) ) ) ) = ( 𝐴 ‘ 𝑦 ) )
53 52 eleq1d ⊢ ( ( ( 𝐴 ∈ Word V ∧ 𝐵 ∈ Word V ) ∧ 𝑦 ∈ ( 0 ..^ ( ♯ ‘ 𝐴 ) ) ) → ( if ( 𝑦 ∈ ( 0 ..^ ( ♯ ‘ 𝐴 ) ) , ( 𝐴 ‘ 𝑦 ) , ( 𝐵 ‘ ( 𝑦 − ( ♯ ‘ 𝐴 ) ) ) ) ∈ 𝑆 ↔ ( 𝐴 ‘ 𝑦 ) ∈ 𝑆 ) )
54 50 53 sylibd ⊢ ( ( ( 𝐴 ∈ Word V ∧ 𝐵 ∈ Word V ) ∧ 𝑦 ∈ ( 0 ..^ ( ♯ ‘ 𝐴 ) ) ) → ( ∀ 𝑥 ∈ ( 0 ..^ ( ( ♯ ‘ 𝐴 ) + ( ♯ ‘ 𝐵 ) ) ) if ( 𝑥 ∈ ( 0 ..^ ( ♯ ‘ 𝐴 ) ) , ( 𝐴 ‘ 𝑥 ) , ( 𝐵 ‘ ( 𝑥 − ( ♯ ‘ 𝐴 ) ) ) ) ∈ 𝑆 → ( 𝐴 ‘ 𝑦 ) ∈ 𝑆 ) )
55 54 impancom ⊢ ( ( ( 𝐴 ∈ Word V ∧ 𝐵 ∈ Word V ) ∧ ∀ 𝑥 ∈ ( 0 ..^ ( ( ♯ ‘ 𝐴 ) + ( ♯ ‘ 𝐵 ) ) ) if ( 𝑥 ∈ ( 0 ..^ ( ♯ ‘ 𝐴 ) ) , ( 𝐴 ‘ 𝑥 ) , ( 𝐵 ‘ ( 𝑥 − ( ♯ ‘ 𝐴 ) ) ) ) ∈ 𝑆 ) → ( 𝑦 ∈ ( 0 ..^ ( ♯ ‘ 𝐴 ) ) → ( 𝐴 ‘ 𝑦 ) ∈ 𝑆 ) )
56 55 ralrimiv ⊢ ( ( ( 𝐴 ∈ Word V ∧ 𝐵 ∈ Word V ) ∧ ∀ 𝑥 ∈ ( 0 ..^ ( ( ♯ ‘ 𝐴 ) + ( ♯ ‘ 𝐵 ) ) ) if ( 𝑥 ∈ ( 0 ..^ ( ♯ ‘ 𝐴 ) ) , ( 𝐴 ‘ 𝑥 ) , ( 𝐵 ‘ ( 𝑥 − ( ♯ ‘ 𝐴 ) ) ) ) ∈ 𝑆 ) → ∀ 𝑦 ∈ ( 0 ..^ ( ♯ ‘ 𝐴 ) ) ( 𝐴 ‘ 𝑦 ) ∈ 𝑆 )
57 iswrdsymb ⊢ ( ( 𝐴 ∈ Word V ∧ ∀ 𝑦 ∈ ( 0 ..^ ( ♯ ‘ 𝐴 ) ) ( 𝐴 ‘ 𝑦 ) ∈ 𝑆 ) → 𝐴 ∈ Word 𝑆 )
58 30 56 57 syl2an2r ⊢ ( ( ( 𝐴 ∈ Word V ∧ 𝐵 ∈ Word V ) ∧ ∀ 𝑥 ∈ ( 0 ..^ ( ( ♯ ‘ 𝐴 ) + ( ♯ ‘ 𝐵 ) ) ) if ( 𝑥 ∈ ( 0 ..^ ( ♯ ‘ 𝐴 ) ) , ( 𝐴 ‘ 𝑥 ) , ( 𝐵 ‘ ( 𝑥 − ( ♯ ‘ 𝐴 ) ) ) ) ∈ 𝑆 ) → 𝐴 ∈ Word 𝑆 )
59 simpr ⊢ ( ( 𝐴 ∈ Word V ∧ 𝐵 ∈ Word V ) → 𝐵 ∈ Word V )
60 simpr ⊢ ( ( ( 𝐴 ∈ Word V ∧ 𝐵 ∈ Word V ) ∧ 𝑦 ∈ ( 0 ..^ ( ♯ ‘ 𝐵 ) ) ) → 𝑦 ∈ ( 0 ..^ ( ♯ ‘ 𝐵 ) ) )
61 18 adantr ⊢ ( ( 𝐴 ∈ Word V ∧ 𝐵 ∈ Word V ) → ( ♯ ‘ 𝐴 ) ∈ ℕ0 )
62 61 adantr ⊢ ( ( ( 𝐴 ∈ Word V ∧ 𝐵 ∈ Word V ) ∧ 𝑦 ∈ ( 0 ..^ ( ♯ ‘ 𝐵 ) ) ) → ( ♯ ‘ 𝐴 ) ∈ ℕ0 )
63 elincfzoext ⊢ ( ( 𝑦 ∈ ( 0 ..^ ( ♯ ‘ 𝐵 ) ) ∧ ( ♯ ‘ 𝐴 ) ∈ ℕ0 ) → ( 𝑦 + ( ♯ ‘ 𝐴 ) ) ∈ ( 0 ..^ ( ( ♯ ‘ 𝐵 ) + ( ♯ ‘ 𝐴 ) ) ) )
64 60 62 63 syl2anc ⊢ ( ( ( 𝐴 ∈ Word V ∧ 𝐵 ∈ Word V ) ∧ 𝑦 ∈ ( 0 ..^ ( ♯ ‘ 𝐵 ) ) ) → ( 𝑦 + ( ♯ ‘ 𝐴 ) ) ∈ ( 0 ..^ ( ( ♯ ‘ 𝐵 ) + ( ♯ ‘ 𝐴 ) ) ) )
65 18 nn0cnd ⊢ ( 𝐴 ∈ Word V → ( ♯ ‘ 𝐴 ) ∈ ℂ )
66 19 nn0cnd ⊢ ( 𝐵 ∈ Word V → ( ♯ ‘ 𝐵 ) ∈ ℂ )
67 65 66 33 syl2an ⊢ ( ( 𝐴 ∈ Word V ∧ 𝐵 ∈ Word V ) → ( ( ♯ ‘ 𝐴 ) + ( ♯ ‘ 𝐵 ) ) = ( ( ♯ ‘ 𝐵 ) + ( ♯ ‘ 𝐴 ) ) )
68 67 oveq2d ⊢ ( ( 𝐴 ∈ Word V ∧ 𝐵 ∈ Word V ) → ( 0 ..^ ( ( ♯ ‘ 𝐴 ) + ( ♯ ‘ 𝐵 ) ) ) = ( 0 ..^ ( ( ♯ ‘ 𝐵 ) + ( ♯ ‘ 𝐴 ) ) ) )
69 68 eleq2d ⊢ ( ( 𝐴 ∈ Word V ∧ 𝐵 ∈ Word V ) → ( ( 𝑦 + ( ♯ ‘ 𝐴 ) ) ∈ ( 0 ..^ ( ( ♯ ‘ 𝐴 ) + ( ♯ ‘ 𝐵 ) ) ) ↔ ( 𝑦 + ( ♯ ‘ 𝐴 ) ) ∈ ( 0 ..^ ( ( ♯ ‘ 𝐵 ) + ( ♯ ‘ 𝐴 ) ) ) ) )
70 69 adantr ⊢ ( ( ( 𝐴 ∈ Word V ∧ 𝐵 ∈ Word V ) ∧ 𝑦 ∈ ( 0 ..^ ( ♯ ‘ 𝐵 ) ) ) → ( ( 𝑦 + ( ♯ ‘ 𝐴 ) ) ∈ ( 0 ..^ ( ( ♯ ‘ 𝐴 ) + ( ♯ ‘ 𝐵 ) ) ) ↔ ( 𝑦 + ( ♯ ‘ 𝐴 ) ) ∈ ( 0 ..^ ( ( ♯ ‘ 𝐵 ) + ( ♯ ‘ 𝐴 ) ) ) ) )
71 64 70 mpbird ⊢ ( ( ( 𝐴 ∈ Word V ∧ 𝐵 ∈ Word V ) ∧ 𝑦 ∈ ( 0 ..^ ( ♯ ‘ 𝐵 ) ) ) → ( 𝑦 + ( ♯ ‘ 𝐴 ) ) ∈ ( 0 ..^ ( ( ♯ ‘ 𝐴 ) + ( ♯ ‘ 𝐵 ) ) ) )
72 eleq1 ⊢ ( 𝑥 = ( 𝑦 + ( ♯ ‘ 𝐴 ) ) → ( 𝑥 ∈ ( 0 ..^ ( ♯ ‘ 𝐴 ) ) ↔ ( 𝑦 + ( ♯ ‘ 𝐴 ) ) ∈ ( 0 ..^ ( ♯ ‘ 𝐴 ) ) ) )
73 fveq2 ⊢ ( 𝑥 = ( 𝑦 + ( ♯ ‘ 𝐴 ) ) → ( 𝐴 ‘ 𝑥 ) = ( 𝐴 ‘ ( 𝑦 + ( ♯ ‘ 𝐴 ) ) ) )
74 fvoveq1 ⊢ ( 𝑥 = ( 𝑦 + ( ♯ ‘ 𝐴 ) ) → ( 𝐵 ‘ ( 𝑥 − ( ♯ ‘ 𝐴 ) ) ) = ( 𝐵 ‘ ( ( 𝑦 + ( ♯ ‘ 𝐴 ) ) − ( ♯ ‘ 𝐴 ) ) ) )
75 72 73 74 ifbieq12d ⊢ ( 𝑥 = ( 𝑦 + ( ♯ ‘ 𝐴 ) ) → if ( 𝑥 ∈ ( 0 ..^ ( ♯ ‘ 𝐴 ) ) , ( 𝐴 ‘ 𝑥 ) , ( 𝐵 ‘ ( 𝑥 − ( ♯ ‘ 𝐴 ) ) ) ) = if ( ( 𝑦 + ( ♯ ‘ 𝐴 ) ) ∈ ( 0 ..^ ( ♯ ‘ 𝐴 ) ) , ( 𝐴 ‘ ( 𝑦 + ( ♯ ‘ 𝐴 ) ) ) , ( 𝐵 ‘ ( ( 𝑦 + ( ♯ ‘ 𝐴 ) ) − ( ♯ ‘ 𝐴 ) ) ) ) )
76 75 eleq1d ⊢ ( 𝑥 = ( 𝑦 + ( ♯ ‘ 𝐴 ) ) → ( if ( 𝑥 ∈ ( 0 ..^ ( ♯ ‘ 𝐴 ) ) , ( 𝐴 ‘ 𝑥 ) , ( 𝐵 ‘ ( 𝑥 − ( ♯ ‘ 𝐴 ) ) ) ) ∈ 𝑆 ↔ if ( ( 𝑦 + ( ♯ ‘ 𝐴 ) ) ∈ ( 0 ..^ ( ♯ ‘ 𝐴 ) ) , ( 𝐴 ‘ ( 𝑦 + ( ♯ ‘ 𝐴 ) ) ) , ( 𝐵 ‘ ( ( 𝑦 + ( ♯ ‘ 𝐴 ) ) − ( ♯ ‘ 𝐴 ) ) ) ) ∈ 𝑆 ) )
77 76 rspcv ⊢ ( ( 𝑦 + ( ♯ ‘ 𝐴 ) ) ∈ ( 0 ..^ ( ( ♯ ‘ 𝐴 ) + ( ♯ ‘ 𝐵 ) ) ) → ( ∀ 𝑥 ∈ ( 0 ..^ ( ( ♯ ‘ 𝐴 ) + ( ♯ ‘ 𝐵 ) ) ) if ( 𝑥 ∈ ( 0 ..^ ( ♯ ‘ 𝐴 ) ) , ( 𝐴 ‘ 𝑥 ) , ( 𝐵 ‘ ( 𝑥 − ( ♯ ‘ 𝐴 ) ) ) ) ∈ 𝑆 → if ( ( 𝑦 + ( ♯ ‘ 𝐴 ) ) ∈ ( 0 ..^ ( ♯ ‘ 𝐴 ) ) , ( 𝐴 ‘ ( 𝑦 + ( ♯ ‘ 𝐴 ) ) ) , ( 𝐵 ‘ ( ( 𝑦 + ( ♯ ‘ 𝐴 ) ) − ( ♯ ‘ 𝐴 ) ) ) ) ∈ 𝑆 ) )
78 71 77 syl ⊢ ( ( ( 𝐴 ∈ Word V ∧ 𝐵 ∈ Word V ) ∧ 𝑦 ∈ ( 0 ..^ ( ♯ ‘ 𝐵 ) ) ) → ( ∀ 𝑥 ∈ ( 0 ..^ ( ( ♯ ‘ 𝐴 ) + ( ♯ ‘ 𝐵 ) ) ) if ( 𝑥 ∈ ( 0 ..^ ( ♯ ‘ 𝐴 ) ) , ( 𝐴 ‘ 𝑥 ) , ( 𝐵 ‘ ( 𝑥 − ( ♯ ‘ 𝐴 ) ) ) ) ∈ 𝑆 → if ( ( 𝑦 + ( ♯ ‘ 𝐴 ) ) ∈ ( 0 ..^ ( ♯ ‘ 𝐴 ) ) , ( 𝐴 ‘ ( 𝑦 + ( ♯ ‘ 𝐴 ) ) ) , ( 𝐵 ‘ ( ( 𝑦 + ( ♯ ‘ 𝐴 ) ) − ( ♯ ‘ 𝐴 ) ) ) ) ∈ 𝑆 ) )
79 18 nn0red ⊢ ( 𝐴 ∈ Word V → ( ♯ ‘ 𝐴 ) ∈ ℝ )
80 79 adantr ⊢ ( ( 𝐴 ∈ Word V ∧ 𝐵 ∈ Word V ) → ( ♯ ‘ 𝐴 ) ∈ ℝ )
81 80 adantr ⊢ ( ( ( 𝐴 ∈ Word V ∧ 𝐵 ∈ Word V ) ∧ 𝑦 ∈ ( 0 ..^ ( ♯ ‘ 𝐵 ) ) ) → ( ♯ ‘ 𝐴 ) ∈ ℝ )
82 elfzoelz ⊢ ( 𝑦 ∈ ( 0 ..^ ( ♯ ‘ 𝐵 ) ) → 𝑦 ∈ ℤ )
83 82 zred ⊢ ( 𝑦 ∈ ( 0 ..^ ( ♯ ‘ 𝐵 ) ) → 𝑦 ∈ ℝ )
84 83 adantr ⊢ ( ( 𝑦 ∈ ( 0 ..^ ( ♯ ‘ 𝐵 ) ) ∧ ( 𝐴 ∈ Word V ∧ 𝐵 ∈ Word V ) ) → 𝑦 ∈ ℝ )
85 80 adantl ⊢ ( ( 𝑦 ∈ ( 0 ..^ ( ♯ ‘ 𝐵 ) ) ∧ ( 𝐴 ∈ Word V ∧ 𝐵 ∈ Word V ) ) → ( ♯ ‘ 𝐴 ) ∈ ℝ )
86 84 85 readdcld ⊢ ( ( 𝑦 ∈ ( 0 ..^ ( ♯ ‘ 𝐵 ) ) ∧ ( 𝐴 ∈ Word V ∧ 𝐵 ∈ Word V ) ) → ( 𝑦 + ( ♯ ‘ 𝐴 ) ) ∈ ℝ )
87 86 ancoms ⊢ ( ( ( 𝐴 ∈ Word V ∧ 𝐵 ∈ Word V ) ∧ 𝑦 ∈ ( 0 ..^ ( ♯ ‘ 𝐵 ) ) ) → ( 𝑦 + ( ♯ ‘ 𝐴 ) ) ∈ ℝ )
88 elfzole1 ⊢ ( 𝑦 ∈ ( 0 ..^ ( ♯ ‘ 𝐵 ) ) → 0 ≤ 𝑦 )
89 88 adantl ⊢ ( ( ( 𝐴 ∈ Word V ∧ 𝐵 ∈ Word V ) ∧ 𝑦 ∈ ( 0 ..^ ( ♯ ‘ 𝐵 ) ) ) → 0 ≤ 𝑦 )
90 addge02 ⊢ ( ( ( ♯ ‘ 𝐴 ) ∈ ℝ ∧ 𝑦 ∈ ℝ ) → ( 0 ≤ 𝑦 ↔ ( ♯ ‘ 𝐴 ) ≤ ( 𝑦 + ( ♯ ‘ 𝐴 ) ) ) )
91 80 83 90 syl2an ⊢ ( ( ( 𝐴 ∈ Word V ∧ 𝐵 ∈ Word V ) ∧ 𝑦 ∈ ( 0 ..^ ( ♯ ‘ 𝐵 ) ) ) → ( 0 ≤ 𝑦 ↔ ( ♯ ‘ 𝐴 ) ≤ ( 𝑦 + ( ♯ ‘ 𝐴 ) ) ) )
92 89 91 mpbid ⊢ ( ( ( 𝐴 ∈ Word V ∧ 𝐵 ∈ Word V ) ∧ 𝑦 ∈ ( 0 ..^ ( ♯ ‘ 𝐵 ) ) ) → ( ♯ ‘ 𝐴 ) ≤ ( 𝑦 + ( ♯ ‘ 𝐴 ) ) )
93 81 87 92 lensymd ⊢ ( ( ( 𝐴 ∈ Word V ∧ 𝐵 ∈ Word V ) ∧ 𝑦 ∈ ( 0 ..^ ( ♯ ‘ 𝐵 ) ) ) → ¬ ( 𝑦 + ( ♯ ‘ 𝐴 ) ) < ( ♯ ‘ 𝐴 ) )
94 93 intn3an3d ⊢ ( ( ( 𝐴 ∈ Word V ∧ 𝐵 ∈ Word V ) ∧ 𝑦 ∈ ( 0 ..^ ( ♯ ‘ 𝐵 ) ) ) → ¬ ( ( 𝑦 + ( ♯ ‘ 𝐴 ) ) ∈ ℕ0 ∧ ( ♯ ‘ 𝐴 ) ∈ ℕ ∧ ( 𝑦 + ( ♯ ‘ 𝐴 ) ) < ( ♯ ‘ 𝐴 ) ) )
95 elfzo0 ⊢ ( ( 𝑦 + ( ♯ ‘ 𝐴 ) ) ∈ ( 0 ..^ ( ♯ ‘ 𝐴 ) ) ↔ ( ( 𝑦 + ( ♯ ‘ 𝐴 ) ) ∈ ℕ0 ∧ ( ♯ ‘ 𝐴 ) ∈ ℕ ∧ ( 𝑦 + ( ♯ ‘ 𝐴 ) ) < ( ♯ ‘ 𝐴 ) ) )
96 94 95 sylnibr ⊢ ( ( ( 𝐴 ∈ Word V ∧ 𝐵 ∈ Word V ) ∧ 𝑦 ∈ ( 0 ..^ ( ♯ ‘ 𝐵 ) ) ) → ¬ ( 𝑦 + ( ♯ ‘ 𝐴 ) ) ∈ ( 0 ..^ ( ♯ ‘ 𝐴 ) ) )
97 96 iffalsed ⊢ ( ( ( 𝐴 ∈ Word V ∧ 𝐵 ∈ Word V ) ∧ 𝑦 ∈ ( 0 ..^ ( ♯ ‘ 𝐵 ) ) ) → if ( ( 𝑦 + ( ♯ ‘ 𝐴 ) ) ∈ ( 0 ..^ ( ♯ ‘ 𝐴 ) ) , ( 𝐴 ‘ ( 𝑦 + ( ♯ ‘ 𝐴 ) ) ) , ( 𝐵 ‘ ( ( 𝑦 + ( ♯ ‘ 𝐴 ) ) − ( ♯ ‘ 𝐴 ) ) ) ) = ( 𝐵 ‘ ( ( 𝑦 + ( ♯ ‘ 𝐴 ) ) − ( ♯ ‘ 𝐴 ) ) ) )
98 97 eleq1d ⊢ ( ( ( 𝐴 ∈ Word V ∧ 𝐵 ∈ Word V ) ∧ 𝑦 ∈ ( 0 ..^ ( ♯ ‘ 𝐵 ) ) ) → ( if ( ( 𝑦 + ( ♯ ‘ 𝐴 ) ) ∈ ( 0 ..^ ( ♯ ‘ 𝐴 ) ) , ( 𝐴 ‘ ( 𝑦 + ( ♯ ‘ 𝐴 ) ) ) , ( 𝐵 ‘ ( ( 𝑦 + ( ♯ ‘ 𝐴 ) ) − ( ♯ ‘ 𝐴 ) ) ) ) ∈ 𝑆 ↔ ( 𝐵 ‘ ( ( 𝑦 + ( ♯ ‘ 𝐴 ) ) − ( ♯ ‘ 𝐴 ) ) ) ∈ 𝑆 ) )
99 82 zcnd ⊢ ( 𝑦 ∈ ( 0 ..^ ( ♯ ‘ 𝐵 ) ) → 𝑦 ∈ ℂ )
100 65 adantr ⊢ ( ( 𝐴 ∈ Word V ∧ 𝐵 ∈ Word V ) → ( ♯ ‘ 𝐴 ) ∈ ℂ )
101 pncan ⊢ ( ( 𝑦 ∈ ℂ ∧ ( ♯ ‘ 𝐴 ) ∈ ℂ ) → ( ( 𝑦 + ( ♯ ‘ 𝐴 ) ) − ( ♯ ‘ 𝐴 ) ) = 𝑦 )
102 99 100 101 syl2anr ⊢ ( ( ( 𝐴 ∈ Word V ∧ 𝐵 ∈ Word V ) ∧ 𝑦 ∈ ( 0 ..^ ( ♯ ‘ 𝐵 ) ) ) → ( ( 𝑦 + ( ♯ ‘ 𝐴 ) ) − ( ♯ ‘ 𝐴 ) ) = 𝑦 )
103 102 fveq2d ⊢ ( ( ( 𝐴 ∈ Word V ∧ 𝐵 ∈ Word V ) ∧ 𝑦 ∈ ( 0 ..^ ( ♯ ‘ 𝐵 ) ) ) → ( 𝐵 ‘ ( ( 𝑦 + ( ♯ ‘ 𝐴 ) ) − ( ♯ ‘ 𝐴 ) ) ) = ( 𝐵 ‘ 𝑦 ) )
104 103 eleq1d ⊢ ( ( ( 𝐴 ∈ Word V ∧ 𝐵 ∈ Word V ) ∧ 𝑦 ∈ ( 0 ..^ ( ♯ ‘ 𝐵 ) ) ) → ( ( 𝐵 ‘ ( ( 𝑦 + ( ♯ ‘ 𝐴 ) ) − ( ♯ ‘ 𝐴 ) ) ) ∈ 𝑆 ↔ ( 𝐵 ‘ 𝑦 ) ∈ 𝑆 ) )
105 104 biimpd ⊢ ( ( ( 𝐴 ∈ Word V ∧ 𝐵 ∈ Word V ) ∧ 𝑦 ∈ ( 0 ..^ ( ♯ ‘ 𝐵 ) ) ) → ( ( 𝐵 ‘ ( ( 𝑦 + ( ♯ ‘ 𝐴 ) ) − ( ♯ ‘ 𝐴 ) ) ) ∈ 𝑆 → ( 𝐵 ‘ 𝑦 ) ∈ 𝑆 ) )
106 98 105 sylbid ⊢ ( ( ( 𝐴 ∈ Word V ∧ 𝐵 ∈ Word V ) ∧ 𝑦 ∈ ( 0 ..^ ( ♯ ‘ 𝐵 ) ) ) → ( if ( ( 𝑦 + ( ♯ ‘ 𝐴 ) ) ∈ ( 0 ..^ ( ♯ ‘ 𝐴 ) ) , ( 𝐴 ‘ ( 𝑦 + ( ♯ ‘ 𝐴 ) ) ) , ( 𝐵 ‘ ( ( 𝑦 + ( ♯ ‘ 𝐴 ) ) − ( ♯ ‘ 𝐴 ) ) ) ) ∈ 𝑆 → ( 𝐵 ‘ 𝑦 ) ∈ 𝑆 ) )
107 78 106 syld ⊢ ( ( ( 𝐴 ∈ Word V ∧ 𝐵 ∈ Word V ) ∧ 𝑦 ∈ ( 0 ..^ ( ♯ ‘ 𝐵 ) ) ) → ( ∀ 𝑥 ∈ ( 0 ..^ ( ( ♯ ‘ 𝐴 ) + ( ♯ ‘ 𝐵 ) ) ) if ( 𝑥 ∈ ( 0 ..^ ( ♯ ‘ 𝐴 ) ) , ( 𝐴 ‘ 𝑥 ) , ( 𝐵 ‘ ( 𝑥 − ( ♯ ‘ 𝐴 ) ) ) ) ∈ 𝑆 → ( 𝐵 ‘ 𝑦 ) ∈ 𝑆 ) )
108 107 impancom ⊢ ( ( ( 𝐴 ∈ Word V ∧ 𝐵 ∈ Word V ) ∧ ∀ 𝑥 ∈ ( 0 ..^ ( ( ♯ ‘ 𝐴 ) + ( ♯ ‘ 𝐵 ) ) ) if ( 𝑥 ∈ ( 0 ..^ ( ♯ ‘ 𝐴 ) ) , ( 𝐴 ‘ 𝑥 ) , ( 𝐵 ‘ ( 𝑥 − ( ♯ ‘ 𝐴 ) ) ) ) ∈ 𝑆 ) → ( 𝑦 ∈ ( 0 ..^ ( ♯ ‘ 𝐵 ) ) → ( 𝐵 ‘ 𝑦 ) ∈ 𝑆 ) )
109 108 ralrimiv ⊢ ( ( ( 𝐴 ∈ Word V ∧ 𝐵 ∈ Word V ) ∧ ∀ 𝑥 ∈ ( 0 ..^ ( ( ♯ ‘ 𝐴 ) + ( ♯ ‘ 𝐵 ) ) ) if ( 𝑥 ∈ ( 0 ..^ ( ♯ ‘ 𝐴 ) ) , ( 𝐴 ‘ 𝑥 ) , ( 𝐵 ‘ ( 𝑥 − ( ♯ ‘ 𝐴 ) ) ) ) ∈ 𝑆 ) → ∀ 𝑦 ∈ ( 0 ..^ ( ♯ ‘ 𝐵 ) ) ( 𝐵 ‘ 𝑦 ) ∈ 𝑆 )
110 iswrdsymb ⊢ ( ( 𝐵 ∈ Word V ∧ ∀ 𝑦 ∈ ( 0 ..^ ( ♯ ‘ 𝐵 ) ) ( 𝐵 ‘ 𝑦 ) ∈ 𝑆 ) → 𝐵 ∈ Word 𝑆 )
111 59 109 110 syl2an2r ⊢ ( ( ( 𝐴 ∈ Word V ∧ 𝐵 ∈ Word V ) ∧ ∀ 𝑥 ∈ ( 0 ..^ ( ( ♯ ‘ 𝐴 ) + ( ♯ ‘ 𝐵 ) ) ) if ( 𝑥 ∈ ( 0 ..^ ( ♯ ‘ 𝐴 ) ) , ( 𝐴 ‘ 𝑥 ) , ( 𝐵 ‘ ( 𝑥 − ( ♯ ‘ 𝐴 ) ) ) ) ∈ 𝑆 ) → 𝐵 ∈ Word 𝑆 )
112 58 111 jca ⊢ ( ( ( 𝐴 ∈ Word V ∧ 𝐵 ∈ Word V ) ∧ ∀ 𝑥 ∈ ( 0 ..^ ( ( ♯ ‘ 𝐴 ) + ( ♯ ‘ 𝐵 ) ) ) if ( 𝑥 ∈ ( 0 ..^ ( ♯ ‘ 𝐴 ) ) , ( 𝐴 ‘ 𝑥 ) , ( 𝐵 ‘ ( 𝑥 − ( ♯ ‘ 𝐴 ) ) ) ) ∈ 𝑆 ) → ( 𝐴 ∈ Word 𝑆 ∧ 𝐵 ∈ Word 𝑆 ) )
113 112 ex ⊢ ( ( 𝐴 ∈ Word V ∧ 𝐵 ∈ Word V ) → ( ∀ 𝑥 ∈ ( 0 ..^ ( ( ♯ ‘ 𝐴 ) + ( ♯ ‘ 𝐵 ) ) ) if ( 𝑥 ∈ ( 0 ..^ ( ♯ ‘ 𝐴 ) ) , ( 𝐴 ‘ 𝑥 ) , ( 𝐵 ‘ ( 𝑥 − ( ♯ ‘ 𝐴 ) ) ) ) ∈ 𝑆 → ( 𝐴 ∈ Word 𝑆 ∧ 𝐵 ∈ Word 𝑆 ) ) )
114 29 113 biimtrrid ⊢ ( ( 𝐴 ∈ Word V ∧ 𝐵 ∈ Word V ) → ( ( 𝑥 ∈ ( 0 ..^ ( ( ♯ ‘ 𝐴 ) + ( ♯ ‘ 𝐵 ) ) ) ↦ if ( 𝑥 ∈ ( 0 ..^ ( ♯ ‘ 𝐴 ) ) , ( 𝐴 ‘ 𝑥 ) , ( 𝐵 ‘ ( 𝑥 − ( ♯ ‘ 𝐴 ) ) ) ) ) : ( 0 ..^ ( ( ♯ ‘ 𝐴 ) + ( ♯ ‘ 𝐵 ) ) ) ⟶ 𝑆 → ( 𝐴 ∈ Word 𝑆 ∧ 𝐵 ∈ Word 𝑆 ) ) )
115 27 114 sylbid ⊢ ( ( 𝐴 ∈ Word V ∧ 𝐵 ∈ Word V ) → ( ( 𝑥 ∈ ( 0 ..^ ( ( ♯ ‘ 𝐴 ) + ( ♯ ‘ 𝐵 ) ) ) ↦ if ( 𝑥 ∈ ( 0 ..^ ( ♯ ‘ 𝐴 ) ) , ( 𝐴 ‘ 𝑥 ) , ( 𝐵 ‘ ( 𝑥 − ( ♯ ‘ 𝐴 ) ) ) ) ) : ( 0 ..^ ( ♯ ‘ ( 𝑥 ∈ ( 0 ..^ ( ( ♯ ‘ 𝐴 ) + ( ♯ ‘ 𝐵 ) ) ) ↦ if ( 𝑥 ∈ ( 0 ..^ ( ♯ ‘ 𝐴 ) ) , ( 𝐴 ‘ 𝑥 ) , ( 𝐵 ‘ ( 𝑥 − ( ♯ ‘ 𝐴 ) ) ) ) ) ) ) ⟶ 𝑆 → ( 𝐴 ∈ Word 𝑆 ∧ 𝐵 ∈ Word 𝑆 ) ) )
116 3 115 syl5 ⊢ ( ( 𝐴 ∈ Word V ∧ 𝐵 ∈ Word V ) → ( ( 𝑥 ∈ ( 0 ..^ ( ( ♯ ‘ 𝐴 ) + ( ♯ ‘ 𝐵 ) ) ) ↦ if ( 𝑥 ∈ ( 0 ..^ ( ♯ ‘ 𝐴 ) ) , ( 𝐴 ‘ 𝑥 ) , ( 𝐵 ‘ ( 𝑥 − ( ♯ ‘ 𝐴 ) ) ) ) ) ∈ Word 𝑆 → ( 𝐴 ∈ Word 𝑆 ∧ 𝐵 ∈ Word 𝑆 ) ) )
117 2 116 sylbid ⊢ ( ( 𝐴 ∈ Word V ∧ 𝐵 ∈ Word V ) → ( ( 𝐴 ++ 𝐵 ) ∈ Word 𝑆 → ( 𝐴 ∈ Word 𝑆 ∧ 𝐵 ∈ Word 𝑆 ) ) )
118 ccatcl ⊢ ( ( 𝐴 ∈ Word 𝑆 ∧ 𝐵 ∈ Word 𝑆 ) → ( 𝐴 ++ 𝐵 ) ∈ Word 𝑆 )
119 117 118 impbid1 ⊢ ( ( 𝐴 ∈ Word V ∧ 𝐵 ∈ Word V ) → ( ( 𝐴 ++ 𝐵 ) ∈ Word 𝑆 ↔ ( 𝐴 ∈ Word 𝑆 ∧ 𝐵 ∈ Word 𝑆 ) ) )