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 ⊢ A = 0 ..^ M × K
ccatmulgnn0dir.b ⊢ B = 0 ..^ N × K
ccatmulgnn0dir.c ⊢ C = 0 ..^ M + N × K
ccatmulgnn0dir.k ⊢ φ → K ∈ S
ccatmulgnn0dir.m ⊢ φ → M ∈ ℕ 0
ccatmulgnn0dir.n ⊢ φ → N ∈ ℕ 0
Assertion ccatmulgnn0dir ⊢ φ → A ++ B = C

Proof

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