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 eqtrid ⊢φ→A= M⋅1
19 5 nn0cnd ⊢φ→M∈ℂ
20 19 mulridd ⊢φ→ 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 eqtrid ⊢φ→B= N⋅1
31 6 nn0cnd ⊢φ→N∈ℂ
32 31 mulridd ⊢φ→ 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→ifi∈0..^AA⁡iB⁡i−A=K
72 35 71 mpteq12dva ⊢φ→i∈0..^A+B⟼ifi∈0..^AA⁡iB⁡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⟼ifi∈0..^AA⁡iB⁡i−A
81 76 79 80 mp2an ⊢A++B=i∈0..^A+B⟼ifi∈0..^AA⁡iB⁡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