d1mat2pmat

Description: The transformation of a matrix of dimenson 1. (Contributed by AV, 4-Aug-2019)

	Ref	Expression
Hypotheses	d1mat2pmat.t	$⊢ T = N matToPolyMat R$
	d1mat2pmat.b	$⊢ B = {Base}_{(N Mat R)}$
	d1mat2pmat.p	$⊢ P = {Poly}_{1} (R)$
	d1mat2pmat.s	$⊢ S = algSc (P)$
Assertion	d1mat2pmat	$⊢ (R \in V \land (N = \{A\} \land A \in V) \land M \in B) \to T (M) = \{⟨⟨A, A⟩, S (A M A)⟩\}$

Proof

Step	Hyp	Ref	Expression
1		d1mat2pmat.t	$⊢ T = N matToPolyMat R$
2		d1mat2pmat.b	$⊢ B = {Base}_{(N Mat R)}$
3		d1mat2pmat.p	$⊢ P = {Poly}_{1} (R)$
4		d1mat2pmat.s	$⊢ S = algSc (P)$
5		snfi	$⊢ \{A\} \in Fin$
6		eleq1	$⊢ N = \{A\} \to (N \in Fin \leftrightarrow \{A\} \in Fin)$
7	5 6	mpbiri	$⊢ N = \{A\} \to N \in Fin$
8	7	adantr	$⊢ (N = \{A\} \land A \in V) \to N \in Fin$
9	8	3ad2ant2	$⊢ (R \in V \land (N = \{A\} \land A \in V) \land M \in B) \to N \in Fin$
10		simp1	$⊢ (R \in V \land (N = \{A\} \land A \in V) \land M \in B) \to R \in V$
11		simp3	$⊢ (R \in V \land (N = \{A\} \land A \in V) \land M \in B) \to M \in B$
12		eqid	$⊢ N Mat R = N Mat R$
13	1 12 2 3 4	mat2pmatval	$⊢ (N \in Fin \land R \in V \land M \in B) \to T (M) = (i \in N, j \in N ⟼ S (i M j))$
14	9 10 11 13	syl3anc	$⊢ (R \in V \land (N = \{A\} \land A \in V) \land M \in B) \to T (M) = (i \in N, j \in N ⟼ S (i M j))$
15		id	$⊢ A \in V \to A \in V$
16		fvexd	$⊢ A \in V \to S (A M A) \in V$
17	15 15 16	3jca	$⊢ A \in V \to (A \in V \land A \in V \land S (A M A) \in V)$
18	17	adantl	$⊢ (N = \{A\} \land A \in V) \to (A \in V \land A \in V \land S (A M A) \in V)$
19	18	3ad2ant2	$⊢ (R \in V \land (N = \{A\} \land A \in V) \land M \in B) \to (A \in V \land A \in V \land S (A M A) \in V)$
20		eqid	$⊢ (i \in \{A\}, j \in \{A\} ⟼ S (i M j)) = (i \in \{A\}, j \in \{A\} ⟼ S (i M j))$
21		fvoveq1	$⊢ i = A \to S (i M j) = S (A M j)$
22		oveq2	$⊢ j = A \to A M j = A M A$
23	22	fveq2d	$⊢ j = A \to S (A M j) = S (A M A)$
24	20 21 23	mposn	$⊢ (A \in V \land A \in V \land S (A M A) \in V) \to (i \in \{A\}, j \in \{A\} ⟼ S (i M j)) = \{⟨⟨A, A⟩, S (A M A)⟩\}$
25	19 24	syl	$⊢ (R \in V \land (N = \{A\} \land A \in V) \land M \in B) \to (i \in \{A\}, j \in \{A\} ⟼ S (i M j)) = \{⟨⟨A, A⟩, S (A M A)⟩\}$
26		mpoeq12	$⊢ (N = \{A\} \land N = \{A\}) \to (i \in N, j \in N ⟼ S (i M j)) = (i \in \{A\}, j \in \{A\} ⟼ S (i M j))$
27	26	eqeq1d	$⊢ (N = \{A\} \land N = \{A\}) \to ((i \in N, j \in N ⟼ S (i M j)) = \{⟨⟨A, A⟩, S (A M A)⟩\} \leftrightarrow (i \in \{A\}, j \in \{A\} ⟼ S (i M j)) = \{⟨⟨A, A⟩, S (A M A)⟩\})$
28	27	anidms	$⊢ N = \{A\} \to ((i \in N, j \in N ⟼ S (i M j)) = \{⟨⟨A, A⟩, S (A M A)⟩\} \leftrightarrow (i \in \{A\}, j \in \{A\} ⟼ S (i M j)) = \{⟨⟨A, A⟩, S (A M A)⟩\})$
29	28	adantr	$⊢ (N = \{A\} \land A \in V) \to ((i \in N, j \in N ⟼ S (i M j)) = \{⟨⟨A, A⟩, S (A M A)⟩\} \leftrightarrow (i \in \{A\}, j \in \{A\} ⟼ S (i M j)) = \{⟨⟨A, A⟩, S (A M A)⟩\})$
30	29	3ad2ant2	$⊢ (R \in V \land (N = \{A\} \land A \in V) \land M \in B) \to ((i \in N, j \in N ⟼ S (i M j)) = \{⟨⟨A, A⟩, S (A M A)⟩\} \leftrightarrow (i \in \{A\}, j \in \{A\} ⟼ S (i M j)) = \{⟨⟨A, A⟩, S (A M A)⟩\})$
31	25 30	mpbird	$⊢ (R \in V \land (N = \{A\} \land A \in V) \land M \in B) \to (i \in N, j \in N ⟼ S (i M j)) = \{⟨⟨A, A⟩, S (A M A)⟩\}$
32	14 31	eqtrd	$⊢ (R \in V \land (N = \{A\} \land A \in V) \land M \in B) \to T (M) = \{⟨⟨A, A⟩, S (A M A)⟩\}$

Metamath Proof Explorer

Theorem d1mat2pmat

Proof