Metamath Proof Explorer

Theorem lmatcl

Description: Closure of the literal matrix. (Contributed by Thierry Arnoux, 12-Sep-2020)

Ref Expression
Hypotheses lmatfval.m ⊢ 𝑀 = ( litMat ‘ 𝑊 )
lmatfval.n ⊢ ( 𝜑 → 𝑁 ∈ ℕ )
lmatfval.w ⊢ ( 𝜑 → 𝑊 ∈ Word Word 𝑉 )
lmatfval.1 ⊢ ( 𝜑 → ( ♯ ‘ 𝑊 ) = 𝑁 )
lmatfval.2 ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑁 ) ) → ( ♯ ‘ ( 𝑊 ‘ 𝑖 ) ) = 𝑁 )
lmatcl.b ⊢ 𝑉 = ( Base ‘ 𝑅 )
lmatcl.1 ⊢ 𝑂 = ( ( 1 ... 𝑁 ) Mat 𝑅 )
lmatcl.2 ⊢ 𝑃 = ( Base ‘ 𝑂 )
lmatcl.r ⊢ ( 𝜑 → 𝑅 ∈ 𝑋 )
Assertion lmatcl ( 𝜑 → 𝑀 ∈ 𝑃 )

Proof

Step Hyp Ref Expression
1 lmatfval.m ⊢ 𝑀 = ( litMat ‘ 𝑊 )
2 lmatfval.n ⊢ ( 𝜑 → 𝑁 ∈ ℕ )
3 lmatfval.w ⊢ ( 𝜑 → 𝑊 ∈ Word Word 𝑉 )
4 lmatfval.1 ⊢ ( 𝜑 → ( ♯ ‘ 𝑊 ) = 𝑁 )
5 lmatfval.2 ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑁 ) ) → ( ♯ ‘ ( 𝑊 ‘ 𝑖 ) ) = 𝑁 )
6 lmatcl.b ⊢ 𝑉 = ( Base ‘ 𝑅 )
7 lmatcl.1 ⊢ 𝑂 = ( ( 1 ... 𝑁 ) Mat 𝑅 )
8 lmatcl.2 ⊢ 𝑃 = ( Base ‘ 𝑂 )
9 lmatcl.r ⊢ ( 𝜑 → 𝑅 ∈ 𝑋 )
10 lmatval ⊢ ( 𝑊 ∈ Word Word 𝑉 → ( litMat ‘ 𝑊 ) = ( 𝑘 ∈ ( 1 ... ( ♯ ‘ 𝑊 ) ) , 𝑗 ∈ ( 1 ... ( ♯ ‘ ( 𝑊 ‘ 0 ) ) ) ↦ ( ( 𝑊 ‘ ( 𝑘 − 1 ) ) ‘ ( 𝑗 − 1 ) ) ) )
11 3 10 syl ⊢ ( 𝜑 → ( litMat ‘ 𝑊 ) = ( 𝑘 ∈ ( 1 ... ( ♯ ‘ 𝑊 ) ) , 𝑗 ∈ ( 1 ... ( ♯ ‘ ( 𝑊 ‘ 0 ) ) ) ↦ ( ( 𝑊 ‘ ( 𝑘 − 1 ) ) ‘ ( 𝑗 − 1 ) ) ) )
12 1 11 syl5eq ⊢ ( 𝜑 → 𝑀 = ( 𝑘 ∈ ( 1 ... ( ♯ ‘ 𝑊 ) ) , 𝑗 ∈ ( 1 ... ( ♯ ‘ ( 𝑊 ‘ 0 ) ) ) ↦ ( ( 𝑊 ‘ ( 𝑘 − 1 ) ) ‘ ( 𝑗 − 1 ) ) ) )
13 4 oveq2d ⊢ ( 𝜑 → ( 1 ... ( ♯ ‘ 𝑊 ) ) = ( 1 ... 𝑁 ) )
14 lbfzo0 ⊢ ( 0 ∈ ( 0 ..^ 𝑁 ) ↔ 𝑁 ∈ ℕ )
15 2 14 sylibr ⊢ ( 𝜑 → 0 ∈ ( 0 ..^ 𝑁 ) )
16 0nn0 ⊢ 0 ∈ ℕ0
17 16 a1i ⊢ ( 𝜑 → 0 ∈ ℕ0 )
18 simpr ⊢ ( ( 𝜑 ∧ 𝑖 = 0 ) → 𝑖 = 0 )
19 18 eleq1d ⊢ ( ( 𝜑 ∧ 𝑖 = 0 ) → ( 𝑖 ∈ ( 0 ..^ 𝑁 ) ↔ 0 ∈ ( 0 ..^ 𝑁 ) ) )
20 18 fveq2d ⊢ ( ( 𝜑 ∧ 𝑖 = 0 ) → ( 𝑊 ‘ 𝑖 ) = ( 𝑊 ‘ 0 ) )
21 20 fveqeq2d ⊢ ( ( 𝜑 ∧ 𝑖 = 0 ) → ( ( ♯ ‘ ( 𝑊 ‘ 𝑖 ) ) = 𝑁 ↔ ( ♯ ‘ ( 𝑊 ‘ 0 ) ) = 𝑁 ) )
22 19 21 imbi12d ⊢ ( ( 𝜑 ∧ 𝑖 = 0 ) → ( ( 𝑖 ∈ ( 0 ..^ 𝑁 ) → ( ♯ ‘ ( 𝑊 ‘ 𝑖 ) ) = 𝑁 ) ↔ ( 0 ∈ ( 0 ..^ 𝑁 ) → ( ♯ ‘ ( 𝑊 ‘ 0 ) ) = 𝑁 ) ) )
23 5 ex ⊢ ( 𝜑 → ( 𝑖 ∈ ( 0 ..^ 𝑁 ) → ( ♯ ‘ ( 𝑊 ‘ 𝑖 ) ) = 𝑁 ) )
24 17 22 23 vtocld ⊢ ( 𝜑 → ( 0 ∈ ( 0 ..^ 𝑁 ) → ( ♯ ‘ ( 𝑊 ‘ 0 ) ) = 𝑁 ) )
25 15 24 mpd ⊢ ( 𝜑 → ( ♯ ‘ ( 𝑊 ‘ 0 ) ) = 𝑁 )
26 25 oveq2d ⊢ ( 𝜑 → ( 1 ... ( ♯ ‘ ( 𝑊 ‘ 0 ) ) ) = ( 1 ... 𝑁 ) )
27 eqidd ⊢ ( 𝜑 → ( ( 𝑊 ‘ ( 𝑘 − 1 ) ) ‘ ( 𝑗 − 1 ) ) = ( ( 𝑊 ‘ ( 𝑘 − 1 ) ) ‘ ( 𝑗 − 1 ) ) )
28 13 26 27 mpoeq123dv ⊢ ( 𝜑 → ( 𝑘 ∈ ( 1 ... ( ♯ ‘ 𝑊 ) ) , 𝑗 ∈ ( 1 ... ( ♯ ‘ ( 𝑊 ‘ 0 ) ) ) ↦ ( ( 𝑊 ‘ ( 𝑘 − 1 ) ) ‘ ( 𝑗 − 1 ) ) ) = ( 𝑘 ∈ ( 1 ... 𝑁 ) , 𝑗 ∈ ( 1 ... 𝑁 ) ↦ ( ( 𝑊 ‘ ( 𝑘 − 1 ) ) ‘ ( 𝑗 − 1 ) ) ) )
29 12 28 eqtrd ⊢ ( 𝜑 → 𝑀 = ( 𝑘 ∈ ( 1 ... 𝑁 ) , 𝑗 ∈ ( 1 ... 𝑁 ) ↦ ( ( 𝑊 ‘ ( 𝑘 − 1 ) ) ‘ ( 𝑗 − 1 ) ) ) )
30 fzfid ⊢ ( 𝜑 → ( 1 ... 𝑁 ) ∈ Fin )
31 3 3ad2ant1 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 1 ... 𝑁 ) ∧ 𝑗 ∈ ( 1 ... 𝑁 ) ) → 𝑊 ∈ Word Word 𝑉 )
32 simp2 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 1 ... 𝑁 ) ∧ 𝑗 ∈ ( 1 ... 𝑁 ) ) → 𝑘 ∈ ( 1 ... 𝑁 ) )
33 fz1fzo0m1 ⊢ ( 𝑘 ∈ ( 1 ... 𝑁 ) → ( 𝑘 − 1 ) ∈ ( 0 ..^ 𝑁 ) )
34 32 33 syl ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 1 ... 𝑁 ) ∧ 𝑗 ∈ ( 1 ... 𝑁 ) ) → ( 𝑘 − 1 ) ∈ ( 0 ..^ 𝑁 ) )
35 4 3ad2ant1 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 1 ... 𝑁 ) ∧ 𝑗 ∈ ( 1 ... 𝑁 ) ) → ( ♯ ‘ 𝑊 ) = 𝑁 )
36 35 oveq2d ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 1 ... 𝑁 ) ∧ 𝑗 ∈ ( 1 ... 𝑁 ) ) → ( 0 ..^ ( ♯ ‘ 𝑊 ) ) = ( 0 ..^ 𝑁 ) )
37 34 36 eleqtrrd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 1 ... 𝑁 ) ∧ 𝑗 ∈ ( 1 ... 𝑁 ) ) → ( 𝑘 − 1 ) ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) )
38 wrdsymbcl ⊢ ( ( 𝑊 ∈ Word Word 𝑉 ∧ ( 𝑘 − 1 ) ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ) → ( 𝑊 ‘ ( 𝑘 − 1 ) ) ∈ Word 𝑉 )
39 31 37 38 syl2anc ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 1 ... 𝑁 ) ∧ 𝑗 ∈ ( 1 ... 𝑁 ) ) → ( 𝑊 ‘ ( 𝑘 − 1 ) ) ∈ Word 𝑉 )
40 simp3 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 1 ... 𝑁 ) ∧ 𝑗 ∈ ( 1 ... 𝑁 ) ) → 𝑗 ∈ ( 1 ... 𝑁 ) )
41 fz1fzo0m1 ⊢ ( 𝑗 ∈ ( 1 ... 𝑁 ) → ( 𝑗 − 1 ) ∈ ( 0 ..^ 𝑁 ) )
42 40 41 syl ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 1 ... 𝑁 ) ∧ 𝑗 ∈ ( 1 ... 𝑁 ) ) → ( 𝑗 − 1 ) ∈ ( 0 ..^ 𝑁 ) )
43 ovexd ⊢ ( 𝜑 → ( 𝑘 − 1 ) ∈ V )
44 simpr ⊢ ( ( 𝜑 ∧ 𝑖 = ( 𝑘 − 1 ) ) → 𝑖 = ( 𝑘 − 1 ) )
45 eqidd ⊢ ( ( 𝜑 ∧ 𝑖 = ( 𝑘 − 1 ) ) → ( 0 ..^ 𝑁 ) = ( 0 ..^ 𝑁 ) )
46 44 45 eleq12d ⊢ ( ( 𝜑 ∧ 𝑖 = ( 𝑘 − 1 ) ) → ( 𝑖 ∈ ( 0 ..^ 𝑁 ) ↔ ( 𝑘 − 1 ) ∈ ( 0 ..^ 𝑁 ) ) )
47 44 fveq2d ⊢ ( ( 𝜑 ∧ 𝑖 = ( 𝑘 − 1 ) ) → ( 𝑊 ‘ 𝑖 ) = ( 𝑊 ‘ ( 𝑘 − 1 ) ) )
48 47 fveqeq2d ⊢ ( ( 𝜑 ∧ 𝑖 = ( 𝑘 − 1 ) ) → ( ( ♯ ‘ ( 𝑊 ‘ 𝑖 ) ) = 𝑁 ↔ ( ♯ ‘ ( 𝑊 ‘ ( 𝑘 − 1 ) ) ) = 𝑁 ) )
49 46 48 imbi12d ⊢ ( ( 𝜑 ∧ 𝑖 = ( 𝑘 − 1 ) ) → ( ( 𝑖 ∈ ( 0 ..^ 𝑁 ) → ( ♯ ‘ ( 𝑊 ‘ 𝑖 ) ) = 𝑁 ) ↔ ( ( 𝑘 − 1 ) ∈ ( 0 ..^ 𝑁 ) → ( ♯ ‘ ( 𝑊 ‘ ( 𝑘 − 1 ) ) ) = 𝑁 ) ) )
50 43 49 23 vtocld ⊢ ( 𝜑 → ( ( 𝑘 − 1 ) ∈ ( 0 ..^ 𝑁 ) → ( ♯ ‘ ( 𝑊 ‘ ( 𝑘 − 1 ) ) ) = 𝑁 ) )
51 50 imp ⊢ ( ( 𝜑 ∧ ( 𝑘 − 1 ) ∈ ( 0 ..^ 𝑁 ) ) → ( ♯ ‘ ( 𝑊 ‘ ( 𝑘 − 1 ) ) ) = 𝑁 )
52 33 51 sylan2 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 1 ... 𝑁 ) ) → ( ♯ ‘ ( 𝑊 ‘ ( 𝑘 − 1 ) ) ) = 𝑁 )
53 52 3adant3 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 1 ... 𝑁 ) ∧ 𝑗 ∈ ( 1 ... 𝑁 ) ) → ( ♯ ‘ ( 𝑊 ‘ ( 𝑘 − 1 ) ) ) = 𝑁 )
54 53 oveq2d ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 1 ... 𝑁 ) ∧ 𝑗 ∈ ( 1 ... 𝑁 ) ) → ( 0 ..^ ( ♯ ‘ ( 𝑊 ‘ ( 𝑘 − 1 ) ) ) ) = ( 0 ..^ 𝑁 ) )
55 42 54 eleqtrrd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 1 ... 𝑁 ) ∧ 𝑗 ∈ ( 1 ... 𝑁 ) ) → ( 𝑗 − 1 ) ∈ ( 0 ..^ ( ♯ ‘ ( 𝑊 ‘ ( 𝑘 − 1 ) ) ) ) )
56 wrdsymbcl ⊢ ( ( ( 𝑊 ‘ ( 𝑘 − 1 ) ) ∈ Word 𝑉 ∧ ( 𝑗 − 1 ) ∈ ( 0 ..^ ( ♯ ‘ ( 𝑊 ‘ ( 𝑘 − 1 ) ) ) ) ) → ( ( 𝑊 ‘ ( 𝑘 − 1 ) ) ‘ ( 𝑗 − 1 ) ) ∈ 𝑉 )
57 39 55 56 syl2anc ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 1 ... 𝑁 ) ∧ 𝑗 ∈ ( 1 ... 𝑁 ) ) → ( ( 𝑊 ‘ ( 𝑘 − 1 ) ) ‘ ( 𝑗 − 1 ) ) ∈ 𝑉 )
58 7 6 8 30 9 57 matbas2d ⊢ ( 𝜑 → ( 𝑘 ∈ ( 1 ... 𝑁 ) , 𝑗 ∈ ( 1 ... 𝑁 ) ↦ ( ( 𝑊 ‘ ( 𝑘 − 1 ) ) ‘ ( 𝑗 − 1 ) ) ) ∈ 𝑃 )
59 29 58 eqeltrd ⊢ ( 𝜑 → 𝑀 ∈ 𝑃 )