Metamath Proof Explorer


Theorem ccatmulgnn0dir

Description: Concatenation of words follow the rule mulgnn0dir (although applying mulgnn0dir would require S to be a set). In this case A is <" K "> to the power M in the free monoid. (Contributed by Thierry Arnoux, 5-Oct-2018)

Ref Expression
Hypotheses ccatmulgnn0dir.a 𝐴 = ( ( 0 ..^ 𝑀 ) × { 𝐾 } )
ccatmulgnn0dir.b 𝐵 = ( ( 0 ..^ 𝑁 ) × { 𝐾 } )
ccatmulgnn0dir.c 𝐶 = ( ( 0 ..^ ( 𝑀 + 𝑁 ) ) × { 𝐾 } )
ccatmulgnn0dir.k ( 𝜑𝐾𝑆 )
ccatmulgnn0dir.m ( 𝜑𝑀 ∈ ℕ0 )
ccatmulgnn0dir.n ( 𝜑𝑁 ∈ ℕ0 )
Assertion ccatmulgnn0dir ( 𝜑 → ( 𝐴 ++ 𝐵 ) = 𝐶 )

Proof

Step Hyp Ref Expression
1 ccatmulgnn0dir.a 𝐴 = ( ( 0 ..^ 𝑀 ) × { 𝐾 } )
2 ccatmulgnn0dir.b 𝐵 = ( ( 0 ..^ 𝑁 ) × { 𝐾 } )
3 ccatmulgnn0dir.c 𝐶 = ( ( 0 ..^ ( 𝑀 + 𝑁 ) ) × { 𝐾 } )
4 ccatmulgnn0dir.k ( 𝜑𝐾𝑆 )
5 ccatmulgnn0dir.m ( 𝜑𝑀 ∈ ℕ0 )
6 ccatmulgnn0dir.n ( 𝜑𝑁 ∈ ℕ0 )
7 1 fveq2i ( ♯ ‘ 𝐴 ) = ( ♯ ‘ ( ( 0 ..^ 𝑀 ) × { 𝐾 } ) )
8 fzofi ( 0 ..^ 𝑀 ) ∈ Fin
9 snfi { 𝐾 } ∈ Fin
10 hashxp ( ( ( 0 ..^ 𝑀 ) ∈ Fin ∧ { 𝐾 } ∈ Fin ) → ( ♯ ‘ ( ( 0 ..^ 𝑀 ) × { 𝐾 } ) ) = ( ( ♯ ‘ ( 0 ..^ 𝑀 ) ) · ( ♯ ‘ { 𝐾 } ) ) )
11 8 9 10 mp2an ( ♯ ‘ ( ( 0 ..^ 𝑀 ) × { 𝐾 } ) ) = ( ( ♯ ‘ ( 0 ..^ 𝑀 ) ) · ( ♯ ‘ { 𝐾 } ) )
12 7 11 eqtri ( ♯ ‘ 𝐴 ) = ( ( ♯ ‘ ( 0 ..^ 𝑀 ) ) · ( ♯ ‘ { 𝐾 } ) )
13 hashfzo0 ( 𝑀 ∈ ℕ0 → ( ♯ ‘ ( 0 ..^ 𝑀 ) ) = 𝑀 )
14 5 13 syl ( 𝜑 → ( ♯ ‘ ( 0 ..^ 𝑀 ) ) = 𝑀 )
15 hashsng ( 𝐾𝑆 → ( ♯ ‘ { 𝐾 } ) = 1 )
16 4 15 syl ( 𝜑 → ( ♯ ‘ { 𝐾 } ) = 1 )
17 14 16 oveq12d ( 𝜑 → ( ( ♯ ‘ ( 0 ..^ 𝑀 ) ) · ( ♯ ‘ { 𝐾 } ) ) = ( 𝑀 · 1 ) )
18 12 17 syl5eq ( 𝜑 → ( ♯ ‘ 𝐴 ) = ( 𝑀 · 1 ) )
19 5 nn0cnd ( 𝜑𝑀 ∈ ℂ )
20 19 mulid1d ( 𝜑 → ( 𝑀 · 1 ) = 𝑀 )
21 18 20 eqtrd ( 𝜑 → ( ♯ ‘ 𝐴 ) = 𝑀 )
22 2 fveq2i ( ♯ ‘ 𝐵 ) = ( ♯ ‘ ( ( 0 ..^ 𝑁 ) × { 𝐾 } ) )
23 fzofi ( 0 ..^ 𝑁 ) ∈ Fin
24 hashxp ( ( ( 0 ..^ 𝑁 ) ∈ Fin ∧ { 𝐾 } ∈ Fin ) → ( ♯ ‘ ( ( 0 ..^ 𝑁 ) × { 𝐾 } ) ) = ( ( ♯ ‘ ( 0 ..^ 𝑁 ) ) · ( ♯ ‘ { 𝐾 } ) ) )
25 23 9 24 mp2an ( ♯ ‘ ( ( 0 ..^ 𝑁 ) × { 𝐾 } ) ) = ( ( ♯ ‘ ( 0 ..^ 𝑁 ) ) · ( ♯ ‘ { 𝐾 } ) )
26 22 25 eqtri ( ♯ ‘ 𝐵 ) = ( ( ♯ ‘ ( 0 ..^ 𝑁 ) ) · ( ♯ ‘ { 𝐾 } ) )
27 hashfzo0 ( 𝑁 ∈ ℕ0 → ( ♯ ‘ ( 0 ..^ 𝑁 ) ) = 𝑁 )
28 6 27 syl ( 𝜑 → ( ♯ ‘ ( 0 ..^ 𝑁 ) ) = 𝑁 )
29 28 16 oveq12d ( 𝜑 → ( ( ♯ ‘ ( 0 ..^ 𝑁 ) ) · ( ♯ ‘ { 𝐾 } ) ) = ( 𝑁 · 1 ) )
30 26 29 syl5eq ( 𝜑 → ( ♯ ‘ 𝐵 ) = ( 𝑁 · 1 ) )
31 6 nn0cnd ( 𝜑𝑁 ∈ ℂ )
32 31 mulid1d ( 𝜑 → ( 𝑁 · 1 ) = 𝑁 )
33 30 32 eqtrd ( 𝜑 → ( ♯ ‘ 𝐵 ) = 𝑁 )
34 21 33 oveq12d ( 𝜑 → ( ( ♯ ‘ 𝐴 ) + ( ♯ ‘ 𝐵 ) ) = ( 𝑀 + 𝑁 ) )
35 34 oveq2d ( 𝜑 → ( 0 ..^ ( ( ♯ ‘ 𝐴 ) + ( ♯ ‘ 𝐵 ) ) ) = ( 0 ..^ ( 𝑀 + 𝑁 ) ) )
36 simpll ( ( ( 𝜑𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝐴 ) + ( ♯ ‘ 𝐵 ) ) ) ) ∧ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝐴 ) ) ) → 𝜑 )
37 simpr ( ( ( 𝜑𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝐴 ) + ( ♯ ‘ 𝐵 ) ) ) ) ∧ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝐴 ) ) ) → 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝐴 ) ) )
38 21 oveq2d ( 𝜑 → ( 0 ..^ ( ♯ ‘ 𝐴 ) ) = ( 0 ..^ 𝑀 ) )
39 36 38 syl ( ( ( 𝜑𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝐴 ) + ( ♯ ‘ 𝐵 ) ) ) ) ∧ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝐴 ) ) ) → ( 0 ..^ ( ♯ ‘ 𝐴 ) ) = ( 0 ..^ 𝑀 ) )
40 37 39 eleqtrd ( ( ( 𝜑𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝐴 ) + ( ♯ ‘ 𝐵 ) ) ) ) ∧ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝐴 ) ) ) → 𝑖 ∈ ( 0 ..^ 𝑀 ) )
41 fconstg ( 𝐾𝑆 → ( ( 0 ..^ 𝑀 ) × { 𝐾 } ) : ( 0 ..^ 𝑀 ) ⟶ { 𝐾 } )
42 4 41 syl ( 𝜑 → ( ( 0 ..^ 𝑀 ) × { 𝐾 } ) : ( 0 ..^ 𝑀 ) ⟶ { 𝐾 } )
43 1 a1i ( 𝜑𝐴 = ( ( 0 ..^ 𝑀 ) × { 𝐾 } ) )
44 43 feq1d ( 𝜑 → ( 𝐴 : ( 0 ..^ 𝑀 ) ⟶ { 𝐾 } ↔ ( ( 0 ..^ 𝑀 ) × { 𝐾 } ) : ( 0 ..^ 𝑀 ) ⟶ { 𝐾 } ) )
45 42 44 mpbird ( 𝜑𝐴 : ( 0 ..^ 𝑀 ) ⟶ { 𝐾 } )
46 fvconst ( ( 𝐴 : ( 0 ..^ 𝑀 ) ⟶ { 𝐾 } ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝐴𝑖 ) = 𝐾 )
47 45 46 sylan ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝐴𝑖 ) = 𝐾 )
48 36 40 47 syl2anc ( ( ( 𝜑𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝐴 ) + ( ♯ ‘ 𝐵 ) ) ) ) ∧ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝐴 ) ) ) → ( 𝐴𝑖 ) = 𝐾 )
49 simpll ( ( ( 𝜑𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝐴 ) + ( ♯ ‘ 𝐵 ) ) ) ) ∧ ¬ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝐴 ) ) ) → 𝜑 )
50 simplr ( ( ( 𝜑𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝐴 ) + ( ♯ ‘ 𝐵 ) ) ) ) ∧ ¬ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝐴 ) ) ) → 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝐴 ) + ( ♯ ‘ 𝐵 ) ) ) )
51 simpr ( ( ( 𝜑𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝐴 ) + ( ♯ ‘ 𝐵 ) ) ) ) ∧ ¬ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝐴 ) ) ) → ¬ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝐴 ) ) )
52 21 5 eqeltrd ( 𝜑 → ( ♯ ‘ 𝐴 ) ∈ ℕ0 )
53 49 52 syl ( ( ( 𝜑𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝐴 ) + ( ♯ ‘ 𝐵 ) ) ) ) ∧ ¬ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝐴 ) ) ) → ( ♯ ‘ 𝐴 ) ∈ ℕ0 )
54 53 nn0zd ( ( ( 𝜑𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝐴 ) + ( ♯ ‘ 𝐵 ) ) ) ) ∧ ¬ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝐴 ) ) ) → ( ♯ ‘ 𝐴 ) ∈ ℤ )
55 33 6 eqeltrd ( 𝜑 → ( ♯ ‘ 𝐵 ) ∈ ℕ0 )
56 49 55 syl ( ( ( 𝜑𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝐴 ) + ( ♯ ‘ 𝐵 ) ) ) ) ∧ ¬ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝐴 ) ) ) → ( ♯ ‘ 𝐵 ) ∈ ℕ0 )
57 56 nn0zd ( ( ( 𝜑𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝐴 ) + ( ♯ ‘ 𝐵 ) ) ) ) ∧ ¬ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝐴 ) ) ) → ( ♯ ‘ 𝐵 ) ∈ ℤ )
58 fzocatel ( ( ( 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝐴 ) + ( ♯ ‘ 𝐵 ) ) ) ∧ ¬ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝐴 ) ) ) ∧ ( ( ♯ ‘ 𝐴 ) ∈ ℤ ∧ ( ♯ ‘ 𝐵 ) ∈ ℤ ) ) → ( 𝑖 − ( ♯ ‘ 𝐴 ) ) ∈ ( 0 ..^ ( ♯ ‘ 𝐵 ) ) )
59 50 51 54 57 58 syl22anc ( ( ( 𝜑𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝐴 ) + ( ♯ ‘ 𝐵 ) ) ) ) ∧ ¬ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝐴 ) ) ) → ( 𝑖 − ( ♯ ‘ 𝐴 ) ) ∈ ( 0 ..^ ( ♯ ‘ 𝐵 ) ) )
60 33 oveq2d ( 𝜑 → ( 0 ..^ ( ♯ ‘ 𝐵 ) ) = ( 0 ..^ 𝑁 ) )
61 49 60 syl ( ( ( 𝜑𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝐴 ) + ( ♯ ‘ 𝐵 ) ) ) ) ∧ ¬ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝐴 ) ) ) → ( 0 ..^ ( ♯ ‘ 𝐵 ) ) = ( 0 ..^ 𝑁 ) )
62 59 61 eleqtrd ( ( ( 𝜑𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝐴 ) + ( ♯ ‘ 𝐵 ) ) ) ) ∧ ¬ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝐴 ) ) ) → ( 𝑖 − ( ♯ ‘ 𝐴 ) ) ∈ ( 0 ..^ 𝑁 ) )
63 fconstg ( 𝐾𝑆 → ( ( 0 ..^ 𝑁 ) × { 𝐾 } ) : ( 0 ..^ 𝑁 ) ⟶ { 𝐾 } )
64 4 63 syl ( 𝜑 → ( ( 0 ..^ 𝑁 ) × { 𝐾 } ) : ( 0 ..^ 𝑁 ) ⟶ { 𝐾 } )
65 2 a1i ( 𝜑𝐵 = ( ( 0 ..^ 𝑁 ) × { 𝐾 } ) )
66 65 feq1d ( 𝜑 → ( 𝐵 : ( 0 ..^ 𝑁 ) ⟶ { 𝐾 } ↔ ( ( 0 ..^ 𝑁 ) × { 𝐾 } ) : ( 0 ..^ 𝑁 ) ⟶ { 𝐾 } ) )
67 64 66 mpbird ( 𝜑𝐵 : ( 0 ..^ 𝑁 ) ⟶ { 𝐾 } )
68 fvconst ( ( 𝐵 : ( 0 ..^ 𝑁 ) ⟶ { 𝐾 } ∧ ( 𝑖 − ( ♯ ‘ 𝐴 ) ) ∈ ( 0 ..^ 𝑁 ) ) → ( 𝐵 ‘ ( 𝑖 − ( ♯ ‘ 𝐴 ) ) ) = 𝐾 )
69 67 68 sylan ( ( 𝜑 ∧ ( 𝑖 − ( ♯ ‘ 𝐴 ) ) ∈ ( 0 ..^ 𝑁 ) ) → ( 𝐵 ‘ ( 𝑖 − ( ♯ ‘ 𝐴 ) ) ) = 𝐾 )
70 49 62 69 syl2anc ( ( ( 𝜑𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝐴 ) + ( ♯ ‘ 𝐵 ) ) ) ) ∧ ¬ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝐴 ) ) ) → ( 𝐵 ‘ ( 𝑖 − ( ♯ ‘ 𝐴 ) ) ) = 𝐾 )
71 48 70 ifeqda ( ( 𝜑𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝐴 ) + ( ♯ ‘ 𝐵 ) ) ) ) → if ( 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝐴 ) ) , ( 𝐴𝑖 ) , ( 𝐵 ‘ ( 𝑖 − ( ♯ ‘ 𝐴 ) ) ) ) = 𝐾 )
72 35 71 mpteq12dva ( 𝜑 → ( 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝐴 ) + ( ♯ ‘ 𝐵 ) ) ) ↦ if ( 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝐴 ) ) , ( 𝐴𝑖 ) , ( 𝐵 ‘ ( 𝑖 − ( ♯ ‘ 𝐴 ) ) ) ) ) = ( 𝑖 ∈ ( 0 ..^ ( 𝑀 + 𝑁 ) ) ↦ 𝐾 ) )
73 ovex ( 0 ..^ 𝑀 ) ∈ V
74 snex { 𝐾 } ∈ V
75 73 74 xpex ( ( 0 ..^ 𝑀 ) × { 𝐾 } ) ∈ V
76 1 75 eqeltri 𝐴 ∈ V
77 ovex ( 0 ..^ 𝑁 ) ∈ V
78 77 74 xpex ( ( 0 ..^ 𝑁 ) × { 𝐾 } ) ∈ V
79 2 78 eqeltri 𝐵 ∈ V
80 ccatfval ( ( 𝐴 ∈ V ∧ 𝐵 ∈ V ) → ( 𝐴 ++ 𝐵 ) = ( 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝐴 ) + ( ♯ ‘ 𝐵 ) ) ) ↦ if ( 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝐴 ) ) , ( 𝐴𝑖 ) , ( 𝐵 ‘ ( 𝑖 − ( ♯ ‘ 𝐴 ) ) ) ) ) )
81 76 79 80 mp2an ( 𝐴 ++ 𝐵 ) = ( 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝐴 ) + ( ♯ ‘ 𝐵 ) ) ) ↦ if ( 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝐴 ) ) , ( 𝐴𝑖 ) , ( 𝐵 ‘ ( 𝑖 − ( ♯ ‘ 𝐴 ) ) ) ) )
82 fconstmpt ( ( 0 ..^ ( 𝑀 + 𝑁 ) ) × { 𝐾 } ) = ( 𝑖 ∈ ( 0 ..^ ( 𝑀 + 𝑁 ) ) ↦ 𝐾 )
83 3 82 eqtri 𝐶 = ( 𝑖 ∈ ( 0 ..^ ( 𝑀 + 𝑁 ) ) ↦ 𝐾 )
84 72 81 83 3eqtr4g ( 𝜑 → ( 𝐴 ++ 𝐵 ) = 𝐶 )