Metamath Proof Explorer

Theorem lmatcl

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

Ref Expression
Hypotheses lmatfval.m ⊢ M = litMat ⁡ W
lmatfval.n ⊢ φ → N ∈ ℕ
lmatfval.w ⊢ φ → W ∈ Word Word V
lmatfval.1 ⊢ φ → W = N
lmatfval.2 ⊢ φ ∧ i ∈ 0 ..^ N → W ⁡ i = N
lmatcl.b ⊢ V = Base R
lmatcl.1 ⊢ O = 1 … N Mat R
lmatcl.2 ⊢ P = Base O
lmatcl.r ⊢ φ → R ∈ X
Assertion lmatcl ⊢ φ → M ∈ P

Proof

Step Hyp Ref Expression
1 lmatfval.m ⊢ M = litMat ⁡ W
2 lmatfval.n ⊢ φ → N ∈ ℕ
3 lmatfval.w ⊢ φ → W ∈ Word Word V
4 lmatfval.1 ⊢ φ → W = N
5 lmatfval.2 ⊢ φ ∧ i ∈ 0 ..^ N → W ⁡ i = N
6 lmatcl.b ⊢ V = Base R
7 lmatcl.1 ⊢ O = 1 … N Mat R
8 lmatcl.2 ⊢ P = Base O
9 lmatcl.r ⊢ φ → R ∈ X
10 lmatval ⊢ W ∈ Word Word V → litMat ⁡ W = k ∈ 1 … W , j ∈ 1 … W ⁡ 0 ⟼ W ⁡ k − 1 ⁡ j − 1
11 3 10 syl ⊢ φ → litMat ⁡ W = k ∈ 1 … W , j ∈ 1 … W ⁡ 0 ⟼ W ⁡ k − 1 ⁡ j − 1
12 1 11 syl5eq ⊢ φ → M = k ∈ 1 … W , j ∈ 1 … W ⁡ 0 ⟼ W ⁡ k − 1 ⁡ j − 1
13 4 oveq2d ⊢ φ → 1 … W = 1 … N
14 lbfzo0 ⊢ 0 ∈ 0 ..^ N ↔ N ∈ ℕ
15 2 14 sylibr ⊢ φ → 0 ∈ 0 ..^ N
16 0nn0 ⊢ 0 ∈ ℕ 0
17 16 a1i ⊢ φ → 0 ∈ ℕ 0
18 simpr ⊢ φ ∧ i = 0 → i = 0
19 18 eleq1d ⊢ φ ∧ i = 0 → i ∈ 0 ..^ N ↔ 0 ∈ 0 ..^ N
20 18 fveq2d ⊢ φ ∧ i = 0 → W ⁡ i = W ⁡ 0
21 20 fveqeq2d ⊢ φ ∧ i = 0 → W ⁡ i = N ↔ W ⁡ 0 = N
22 19 21 imbi12d ⊢ φ ∧ i = 0 → i ∈ 0 ..^ N → W ⁡ i = N ↔ 0 ∈ 0 ..^ N → W ⁡ 0 = N
23 5 ex ⊢ φ → i ∈ 0 ..^ N → W ⁡ i = N
24 17 22 23 vtocld ⊢ φ → 0 ∈ 0 ..^ N → W ⁡ 0 = N
25 15 24 mpd ⊢ φ → W ⁡ 0 = N
26 25 oveq2d ⊢ φ → 1 … W ⁡ 0 = 1 … N
27 eqidd ⊢ φ → W ⁡ k − 1 ⁡ j − 1 = W ⁡ k − 1 ⁡ j − 1
28 13 26 27 mpoeq123dv ⊢ φ → k ∈ 1 … W , j ∈ 1 … W ⁡ 0 ⟼ W ⁡ k − 1 ⁡ j − 1 = k ∈ 1 … N , j ∈ 1 … N ⟼ W ⁡ k − 1 ⁡ j − 1
29 12 28 eqtrd ⊢ φ → M = k ∈ 1 … N , j ∈ 1 … N ⟼ W ⁡ k − 1 ⁡ j − 1
30 fzfid ⊢ φ → 1 … N ∈ Fin
31 3 3ad2ant1 ⊢ φ ∧ k ∈ 1 … N ∧ j ∈ 1 … N → W ∈ Word Word V
32 simp2 ⊢ φ ∧ k ∈ 1 … N ∧ j ∈ 1 … N → k ∈ 1 … N
33 fz1fzo0m1 ⊢ k ∈ 1 … N → k − 1 ∈ 0 ..^ N
34 32 33 syl ⊢ φ ∧ k ∈ 1 … N ∧ j ∈ 1 … N → k − 1 ∈ 0 ..^ N
35 4 3ad2ant1 ⊢ φ ∧ k ∈ 1 … N ∧ j ∈ 1 … N → W = N
36 35 oveq2d ⊢ φ ∧ k ∈ 1 … N ∧ j ∈ 1 … N → 0 ..^ W = 0 ..^ N
37 34 36 eleqtrrd ⊢ φ ∧ k ∈ 1 … N ∧ j ∈ 1 … N → k − 1 ∈ 0 ..^ W
38 wrdsymbcl ⊢ W ∈ Word Word V ∧ k − 1 ∈ 0 ..^ W → W ⁡ k − 1 ∈ Word V
39 31 37 38 syl2anc ⊢ φ ∧ k ∈ 1 … N ∧ j ∈ 1 … N → W ⁡ k − 1 ∈ Word V
40 simp3 ⊢ φ ∧ k ∈ 1 … N ∧ j ∈ 1 … N → j ∈ 1 … N
41 fz1fzo0m1 ⊢ j ∈ 1 … N → j − 1 ∈ 0 ..^ N
42 40 41 syl ⊢ φ ∧ k ∈ 1 … N ∧ j ∈ 1 … N → j − 1 ∈ 0 ..^ N
43 ovexd ⊢ φ → k − 1 ∈ V
44 simpr ⊢ φ ∧ i = k − 1 → i = k − 1
45 eqidd ⊢ φ ∧ i = k − 1 → 0 ..^ N = 0 ..^ N
46 44 45 eleq12d ⊢ φ ∧ i = k − 1 → i ∈ 0 ..^ N ↔ k − 1 ∈ 0 ..^ N
47 44 fveq2d ⊢ φ ∧ i = k − 1 → W ⁡ i = W ⁡ k − 1
48 47 fveqeq2d ⊢ φ ∧ i = k − 1 → W ⁡ i = N ↔ W ⁡ k − 1 = N
49 46 48 imbi12d ⊢ φ ∧ i = k − 1 → i ∈ 0 ..^ N → W ⁡ i = N ↔ k − 1 ∈ 0 ..^ N → W ⁡ k − 1 = N
50 43 49 23 vtocld ⊢ φ → k − 1 ∈ 0 ..^ N → W ⁡ k − 1 = N
51 50 imp ⊢ φ ∧ k − 1 ∈ 0 ..^ N → W ⁡ k − 1 = N
52 33 51 sylan2 ⊢ φ ∧ k ∈ 1 … N → W ⁡ k − 1 = N
53 52 3adant3 ⊢ φ ∧ k ∈ 1 … N ∧ j ∈ 1 … N → W ⁡ k − 1 = N
54 53 oveq2d ⊢ φ ∧ k ∈ 1 … N ∧ j ∈ 1 … N → 0 ..^ W ⁡ k − 1 = 0 ..^ N
55 42 54 eleqtrrd ⊢ φ ∧ k ∈ 1 … N ∧ j ∈ 1 … N → j − 1 ∈ 0 ..^ W ⁡ k − 1
56 wrdsymbcl ⊢ W ⁡ k − 1 ∈ Word V ∧ j − 1 ∈ 0 ..^ W ⁡ k − 1 → W ⁡ k − 1 ⁡ j − 1 ∈ V
57 39 55 56 syl2anc ⊢ φ ∧ k ∈ 1 … N ∧ j ∈ 1 … N → W ⁡ k − 1 ⁡ j − 1 ∈ V
58 7 6 8 30 9 57 matbas2d ⊢ φ → k ∈ 1 … N , j ∈ 1 … N ⟼ W ⁡ k − 1 ⁡ j − 1 ∈ P
59 29 58 eqeltrd ⊢ φ → M ∈ P