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 syl5bir ( ( 𝐴 ∈ 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 𝑆 ) ) )