scmate

Description: An entry of an N x N scalar matrix over the ring R . (Contributed by AV, 18-Dec-2019)

	Ref	Expression
Hypotheses	scmatmat.a	$⊢ A = N Mat R$
	scmatmat.b	$⊢ B = {Base}_{A}$
	scmatmat.s	$⊢ S = N ScMat R$
	scmate.k	$⊢ K = {Base}_{R}$
	scmate.0	$⊢ \underset{˙}{0} = 0_{R}$
Assertion	scmate	$⊢ ((N \in Fin \land R \in Ring \land M \in S) \land (I \in N \land J \in N)) \to \exists c \in K I M J = if (I = J, c, \underset{˙}{0})$

Proof

Step	Hyp	Ref	Expression
1		scmatmat.a	$⊢ A = N Mat R$
2		scmatmat.b	$⊢ B = {Base}_{A}$
3		scmatmat.s	$⊢ S = N ScMat R$
4		scmate.k	$⊢ K = {Base}_{R}$
5		scmate.0	$⊢ \underset{˙}{0} = 0_{R}$
6		eqid	$⊢ 1_{A} = 1_{A}$
7		eqid	$⊢ \cdot_{A} = \cdot_{A}$
8	4 1 2 6 7 3	scmatscmid	$⊢ (N \in Fin \land R \in Ring \land M \in S) \to \exists c \in K M = c \cdot_{A} 1_{A}$
9		oveq	$⊢ M = c \cdot_{A} 1_{A} \to I M J = I (c \cdot_{A} 1_{A}) J$
10		simpll1	$⊢ (((N \in Fin \land R \in Ring \land M \in S) \land (I \in N \land J \in N)) \land c \in K) \to N \in Fin$
11		simpll2	$⊢ (((N \in Fin \land R \in Ring \land M \in S) \land (I \in N \land J \in N)) \land c \in K) \to R \in Ring$
12		simpr	$⊢ (((N \in Fin \land R \in Ring \land M \in S) \land (I \in N \land J \in N)) \land c \in K) \to c \in K$
13		simplr	$⊢ (((N \in Fin \land R \in Ring \land M \in S) \land (I \in N \land J \in N)) \land c \in K) \to (I \in N \land J \in N)$
14	1 4 5 6 7	scmatscmide	$⊢ ((N \in Fin \land R \in Ring \land c \in K) \land (I \in N \land J \in N)) \to I (c \cdot_{A} 1_{A}) J = if (I = J, c, \underset{˙}{0})$
15	10 11 12 13 14	syl31anc	$⊢ (((N \in Fin \land R \in Ring \land M \in S) \land (I \in N \land J \in N)) \land c \in K) \to I (c \cdot_{A} 1_{A}) J = if (I = J, c, \underset{˙}{0})$
16	9 15	sylan9eqr	$⊢ ((((N \in Fin \land R \in Ring \land M \in S) \land (I \in N \land J \in N)) \land c \in K) \land M = c \cdot_{A} 1_{A}) \to I M J = if (I = J, c, \underset{˙}{0})$
17	16	ex	$⊢ (((N \in Fin \land R \in Ring \land M \in S) \land (I \in N \land J \in N)) \land c \in K) \to (M = c \cdot_{A} 1_{A} \to I M J = if (I = J, c, \underset{˙}{0}))$
18	17	reximdva	$⊢ ((N \in Fin \land R \in Ring \land M \in S) \land (I \in N \land J \in N)) \to (\exists c \in K M = c \cdot_{A} 1_{A} \to \exists c \in K I M J = if (I = J, c, \underset{˙}{0}))$
19	18	ex	$⊢ (N \in Fin \land R \in Ring \land M \in S) \to ((I \in N \land J \in N) \to (\exists c \in K M = c \cdot_{A} 1_{A} \to \exists c \in K I M J = if (I = J, c, \underset{˙}{0})))$
20	8 19	mpid	$⊢ (N \in Fin \land R \in Ring \land M \in S) \to ((I \in N \land J \in N) \to \exists c \in K I M J = if (I = J, c, \underset{˙}{0}))$
21	20	imp	$⊢ ((N \in Fin \land R \in Ring \land M \in S) \land (I \in N \land J \in N)) \to \exists c \in K I M J = if (I = J, c, \underset{˙}{0})$

Metamath Proof Explorer

Theorem scmate

Proof