matsc

Description: The identity matrix multiplied with a scalar. (Contributed by Stefan O'Rear, 16-Jul-2018)

	Ref	Expression
Hypotheses	matsc.a	$⊢ A = N Mat R$
	matsc.k	$⊢ K = {Base}_{R}$
	matsc.m	$⊢ \underset{˙}{\cdot} = \cdot_{A}$
	matsc.z	$⊢ \underset{˙}{0} = 0_{R}$
Assertion	matsc	$⊢ (N \in Fin \land R \in Ring \land L \in K) \to L \underset{˙}{\cdot} 1_{A} = (i \in N, j \in N ⟼ if (i = j, L, \underset{˙}{0}))$

Proof

Step	Hyp	Ref	Expression
1		matsc.a	$⊢ A = N Mat R$
2		matsc.k	$⊢ K = {Base}_{R}$
3		matsc.m	$⊢ \underset{˙}{\cdot} = \cdot_{A}$
4		matsc.z	$⊢ \underset{˙}{0} = 0_{R}$
5		simp3	$⊢ (N \in Fin \land R \in Ring \land L \in K) \to L \in K$
6		3simpa	$⊢ (N \in Fin \land R \in Ring \land L \in K) \to (N \in Fin \land R \in Ring)$
7	1	matring	$⊢ (N \in Fin \land R \in Ring) \to A \in Ring$
8		eqid	$⊢ {Base}_{A} = {Base}_{A}$
9		eqid	$⊢ 1_{A} = 1_{A}$
10	8 9	ringidcl	$⊢ A \in Ring \to 1_{A} \in {Base}_{A}$
11	6 7 10	3syl	$⊢ (N \in Fin \land R \in Ring \land L \in K) \to 1_{A} \in {Base}_{A}$
12		eqid	$⊢ \cdot_{R} = \cdot_{R}$
13		eqid	$⊢ N \times N = N \times N$
14	1 8 2 3 12 13	matvsca2	$⊢ (L \in K \land 1_{A} \in {Base}_{A}) \to L \underset{˙}{\cdot} 1_{A} = ((N \times N) \times \{L\}) {\cdot_{R}}_{f} 1_{A}$
15	5 11 14	syl2anc	$⊢ (N \in Fin \land R \in Ring \land L \in K) \to L \underset{˙}{\cdot} 1_{A} = ((N \times N) \times \{L\}) {\cdot_{R}}_{f} 1_{A}$
16		simp1	$⊢ (N \in Fin \land R \in Ring \land L \in K) \to N \in Fin$
17		simp13	$⊢ ((N \in Fin \land R \in Ring \land L \in K) \land i \in N \land j \in N) \to L \in K$
18		fvex	$⊢ 1_{R} \in V$
19	4	fvexi	$⊢ \underset{˙}{0} \in V$
20	18 19	ifex	$⊢ if (i = j, 1_{R}, \underset{˙}{0}) \in V$
21	20	a1i	$⊢ ((N \in Fin \land R \in Ring \land L \in K) \land i \in N \land j \in N) \to if (i = j, 1_{R}, \underset{˙}{0}) \in V$
22		fconstmpo	$⊢ (N \times N) \times \{L\} = (i \in N, j \in N ⟼ L)$
23	22	a1i	$⊢ (N \in Fin \land R \in Ring \land L \in K) \to (N \times N) \times \{L\} = (i \in N, j \in N ⟼ L)$
24		eqid	$⊢ 1_{R} = 1_{R}$
25	1 24 4	mat1	$⊢ (N \in Fin \land R \in Ring) \to 1_{A} = (i \in N, j \in N ⟼ if (i = j, 1_{R}, \underset{˙}{0}))$
26	25	3adant3	$⊢ (N \in Fin \land R \in Ring \land L \in K) \to 1_{A} = (i \in N, j \in N ⟼ if (i = j, 1_{R}, \underset{˙}{0}))$
27	16 16 17 21 23 26	offval22	$⊢ (N \in Fin \land R \in Ring \land L \in K) \to ((N \times N) \times \{L\}) {\cdot_{R}}_{f} 1_{A} = (i \in N, j \in N ⟼ L \cdot_{R} if (i = j, 1_{R}, \underset{˙}{0}))$
28		ovif2	$⊢ L \cdot_{R} if (i = j, 1_{R}, \underset{˙}{0}) = if (i = j, L \cdot_{R} 1_{R}, L \cdot_{R} \underset{˙}{0})$
29	2 12 24	ringridm	$⊢ (R \in Ring \land L \in K) \to L \cdot_{R} 1_{R} = L$
30	29	3adant1	$⊢ (N \in Fin \land R \in Ring \land L \in K) \to L \cdot_{R} 1_{R} = L$
31	2 12 4	ringrz	$⊢ (R \in Ring \land L \in K) \to L \cdot_{R} \underset{˙}{0} = \underset{˙}{0}$
32	31	3adant1	$⊢ (N \in Fin \land R \in Ring \land L \in K) \to L \cdot_{R} \underset{˙}{0} = \underset{˙}{0}$
33	30 32	ifeq12d	$⊢ (N \in Fin \land R \in Ring \land L \in K) \to if (i = j, L \cdot_{R} 1_{R}, L \cdot_{R} \underset{˙}{0}) = if (i = j, L, \underset{˙}{0})$
34	28 33	eqtrid	$⊢ (N \in Fin \land R \in Ring \land L \in K) \to L \cdot_{R} if (i = j, 1_{R}, \underset{˙}{0}) = if (i = j, L, \underset{˙}{0})$
35	34	mpoeq3dv	$⊢ (N \in Fin \land R \in Ring \land L \in K) \to (i \in N, j \in N ⟼ L \cdot_{R} if (i = j, 1_{R}, \underset{˙}{0})) = (i \in N, j \in N ⟼ if (i = j, L, \underset{˙}{0}))$
36	15 27 35	3eqtrd	$⊢ (N \in Fin \land R \in Ring \land L \in K) \to L \underset{˙}{\cdot} 1_{A} = (i \in N, j \in N ⟼ if (i = j, L, \underset{˙}{0}))$

Metamath Proof Explorer

Theorem matsc

Proof