lmatcl

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

	Ref	Expression
Hypotheses	lmatfval.m	$⊢ M = litMat (W)$
	lmatfval.n	$⊢ φ \to N \in ℕ$
	lmatfval.w	$⊢ φ \to W \in Word Word V$
	lmatfval.1	$⊢ φ \to \|W\| = N$
	lmatfval.2	$⊢ (φ \land i \in (0 ..^N)) \to \|W (i)\| = N$
	lmatcl.b	$⊢ V = {Base}_{R}$
	lmatcl.1	$⊢ O = (1 \dots N) Mat R$
	lmatcl.2	$⊢ P = {Base}_{O}$
	lmatcl.r	$⊢ φ \to R \in X$
Assertion	lmatcl	$⊢ φ \to M \in P$

Proof

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

Metamath Proof Explorer

Theorem lmatcl

Proof