scmatscmiddistr

Description: Distributive law for scalar and ring multiplication for scalar matrices expressed as multiplications of a scalar with the identity matrix. (Contributed by AV, 19-Dec-2019)

	Ref	Expression
Hypotheses	scmatscmide.a	$⊢ A = N Mat R$
	scmatscmide.b	$⊢ B = {Base}_{R}$
	scmatscmide.0	$⊢ \underset{˙}{0} = 0_{R}$
	scmatscmide.1	$⊢ \underset{˙}{1} = 1_{A}$
	scmatscmide.m	$⊢ \underset{˙}{*} = \cdot_{A}$
	scmatscmiddistr.t	$⊢ \underset{˙}{\cdot} = \cdot_{R}$
	scmatscmiddistr.m	$⊢ \underset{˙}{\times} = \cdot_{A}$
Assertion	scmatscmiddistr	$⊢ ((N \in Fin \land R \in Ring) \land (S \in B \land T \in B)) \to (S \underset{˙}{} \underset{˙}{1}) \underset{˙}{\times} (T \underset{˙}{} \underset{˙}{1}) = (S \underset{˙}{\cdot} T) \underset{˙}{*} \underset{˙}{1}$

Proof

Step	Hyp	Ref	Expression
1		scmatscmide.a	$⊢ A = N Mat R$
2		scmatscmide.b	$⊢ B = {Base}_{R}$
3		scmatscmide.0	$⊢ \underset{˙}{0} = 0_{R}$
4		scmatscmide.1	$⊢ \underset{˙}{1} = 1_{A}$
5		scmatscmide.m	$⊢ \underset{˙}{*} = \cdot_{A}$
6		scmatscmiddistr.t	$⊢ \underset{˙}{\cdot} = \cdot_{R}$
7		scmatscmiddistr.m	$⊢ \underset{˙}{\times} = \cdot_{A}$
8		simprl	$⊢ ((N \in Fin \land R \in Ring) \land (S \in B \land T \in B)) \to S \in B$
9		eqid	$⊢ {Base}_{A} = {Base}_{A}$
10		eqid	$⊢ N DMat R = N DMat R$
11	1 9 3 10	dmatid	$⊢ (N \in Fin \land R \in Ring) \to 1_{A} \in (N DMat R)$
12	4 11	eqeltrid	$⊢ (N \in Fin \land R \in Ring) \to \underset{˙}{1} \in (N DMat R)$
13	12	adantr	$⊢ ((N \in Fin \land R \in Ring) \land (S \in B \land T \in B)) \to \underset{˙}{1} \in (N DMat R)$
14	8 13	jca	$⊢ ((N \in Fin \land R \in Ring) \land (S \in B \land T \in B)) \to (S \in B \land \underset{˙}{1} \in (N DMat R))$
15	2 1 9 5 10	dmatscmcl	$⊢ ((N \in Fin \land R \in Ring) \land (S \in B \land \underset{˙}{1} \in (N DMat R))) \to S \underset{˙}{*} \underset{˙}{1} \in (N DMat R)$
16	14 15	syldan	$⊢ ((N \in Fin \land R \in Ring) \land (S \in B \land T \in B)) \to S \underset{˙}{*} \underset{˙}{1} \in (N DMat R)$
17		simprr	$⊢ ((N \in Fin \land R \in Ring) \land (S \in B \land T \in B)) \to T \in B$
18	17 13	jca	$⊢ ((N \in Fin \land R \in Ring) \land (S \in B \land T \in B)) \to (T \in B \land \underset{˙}{1} \in (N DMat R))$
19	2 1 9 5 10	dmatscmcl	$⊢ ((N \in Fin \land R \in Ring) \land (T \in B \land \underset{˙}{1} \in (N DMat R))) \to T \underset{˙}{*} \underset{˙}{1} \in (N DMat R)$
20	18 19	syldan	$⊢ ((N \in Fin \land R \in Ring) \land (S \in B \land T \in B)) \to T \underset{˙}{*} \underset{˙}{1} \in (N DMat R)$
21	16 20	jca	$⊢ ((N \in Fin \land R \in Ring) \land (S \in B \land T \in B)) \to (S \underset{˙}{} \underset{˙}{1} \in (N DMat R) \land T \underset{˙}{} \underset{˙}{1} \in (N DMat R))$
22	7	oveqi	$⊢ (S \underset{˙}{} \underset{˙}{1}) \underset{˙}{\times} (T \underset{˙}{} \underset{˙}{1}) = (S \underset{˙}{} \underset{˙}{1}) \cdot_{A} (T \underset{˙}{} \underset{˙}{1})$
23	1 9 3 10	dmatmul	$⊢ ((N \in Fin \land R \in Ring) \land (S \underset{˙}{} \underset{˙}{1} \in (N DMat R) \land T \underset{˙}{} \underset{˙}{1} \in (N DMat R))) \to (S \underset{˙}{} \underset{˙}{1}) \cdot_{A} (T \underset{˙}{} \underset{˙}{1}) = (i \in N, j \in N ⟼ if (i = j, (i (S \underset{˙}{} \underset{˙}{1}) j) \cdot_{R} (i (T \underset{˙}{} \underset{˙}{1}) j), \underset{˙}{0}))$
24	22 23	syl5eq	$⊢ ((N \in Fin \land R \in Ring) \land (S \underset{˙}{} \underset{˙}{1} \in (N DMat R) \land T \underset{˙}{} \underset{˙}{1} \in (N DMat R))) \to (S \underset{˙}{} \underset{˙}{1}) \underset{˙}{\times} (T \underset{˙}{} \underset{˙}{1}) = (i \in N, j \in N ⟼ if (i = j, (i (S \underset{˙}{} \underset{˙}{1}) j) \cdot_{R} (i (T \underset{˙}{} \underset{˙}{1}) j), \underset{˙}{0}))$
25	21 24	syldan	$⊢ ((N \in Fin \land R \in Ring) \land (S \in B \land T \in B)) \to (S \underset{˙}{} \underset{˙}{1}) \underset{˙}{\times} (T \underset{˙}{} \underset{˙}{1}) = (i \in N, j \in N ⟼ if (i = j, (i (S \underset{˙}{} \underset{˙}{1}) j) \cdot_{R} (i (T \underset{˙}{} \underset{˙}{1}) j), \underset{˙}{0}))$
26		simpll	$⊢ ((N \in Fin \land R \in Ring) \land (S \in B \land T \in B)) \to N \in Fin$
27		simplr	$⊢ ((N \in Fin \land R \in Ring) \land (S \in B \land T \in B)) \to R \in Ring$
28	26 27 8	3jca	$⊢ ((N \in Fin \land R \in Ring) \land (S \in B \land T \in B)) \to (N \in Fin \land R \in Ring \land S \in B)$
29	28	3ad2ant1	$⊢ (((N \in Fin \land R \in Ring) \land (S \in B \land T \in B)) \land i \in N \land j \in N) \to (N \in Fin \land R \in Ring \land S \in B)$
30		3simpc	$⊢ (((N \in Fin \land R \in Ring) \land (S \in B \land T \in B)) \land i \in N \land j \in N) \to (i \in N \land j \in N)$
31	1 2 3 4 5	scmatscmide	$⊢ ((N \in Fin \land R \in Ring \land S \in B) \land (i \in N \land j \in N)) \to i (S \underset{˙}{*} \underset{˙}{1}) j = if (i = j, S, \underset{˙}{0})$
32	29 30 31	syl2anc	$⊢ (((N \in Fin \land R \in Ring) \land (S \in B \land T \in B)) \land i \in N \land j \in N) \to i (S \underset{˙}{*} \underset{˙}{1}) j = if (i = j, S, \underset{˙}{0})$
33	26 27 17	3jca	$⊢ ((N \in Fin \land R \in Ring) \land (S \in B \land T \in B)) \to (N \in Fin \land R \in Ring \land T \in B)$
34	33	3ad2ant1	$⊢ (((N \in Fin \land R \in Ring) \land (S \in B \land T \in B)) \land i \in N \land j \in N) \to (N \in Fin \land R \in Ring \land T \in B)$
35	1 2 3 4 5	scmatscmide	$⊢ ((N \in Fin \land R \in Ring \land T \in B) \land (i \in N \land j \in N)) \to i (T \underset{˙}{*} \underset{˙}{1}) j = if (i = j, T, \underset{˙}{0})$
36	34 30 35	syl2anc	$⊢ (((N \in Fin \land R \in Ring) \land (S \in B \land T \in B)) \land i \in N \land j \in N) \to i (T \underset{˙}{*} \underset{˙}{1}) j = if (i = j, T, \underset{˙}{0})$
37	32 36	oveq12d	$⊢ (((N \in Fin \land R \in Ring) \land (S \in B \land T \in B)) \land i \in N \land j \in N) \to (i (S \underset{˙}{} \underset{˙}{1}) j) \cdot_{R} (i (T \underset{˙}{} \underset{˙}{1}) j) = if (i = j, S, \underset{˙}{0}) \cdot_{R} if (i = j, T, \underset{˙}{0})$
38	37	ifeq1d	$⊢ (((N \in Fin \land R \in Ring) \land (S \in B \land T \in B)) \land i \in N \land j \in N) \to if (i = j, (i (S \underset{˙}{} \underset{˙}{1}) j) \cdot_{R} (i (T \underset{˙}{} \underset{˙}{1}) j), \underset{˙}{0}) = if (i = j, if (i = j, S, \underset{˙}{0}) \cdot_{R} if (i = j, T, \underset{˙}{0}), \underset{˙}{0})$
39	38	mpoeq3dva	$⊢ ((N \in Fin \land R \in Ring) \land (S \in B \land T \in B)) \to (i \in N, j \in N ⟼ if (i = j, (i (S \underset{˙}{} \underset{˙}{1}) j) \cdot_{R} (i (T \underset{˙}{} \underset{˙}{1}) j), \underset{˙}{0})) = (i \in N, j \in N ⟼ if (i = j, if (i = j, S, \underset{˙}{0}) \cdot_{R} if (i = j, T, \underset{˙}{0}), \underset{˙}{0}))$
40		iftrue	$⊢ i = j \to if (i = j, S, \underset{˙}{0}) = S$
41		iftrue	$⊢ i = j \to if (i = j, T, \underset{˙}{0}) = T$
42	40 41	oveq12d	$⊢ i = j \to if (i = j, S, \underset{˙}{0}) \cdot_{R} if (i = j, T, \underset{˙}{0}) = S \cdot_{R} T$
43	42	adantl	$⊢ ((((N \in Fin \land R \in Ring) \land (S \in B \land T \in B)) \land i \in N \land j \in N) \land i = j) \to if (i = j, S, \underset{˙}{0}) \cdot_{R} if (i = j, T, \underset{˙}{0}) = S \cdot_{R} T$
44	43	ifeq1da	$⊢ (((N \in Fin \land R \in Ring) \land (S \in B \land T \in B)) \land i \in N \land j \in N) \to if (i = j, if (i = j, S, \underset{˙}{0}) \cdot_{R} if (i = j, T, \underset{˙}{0}), \underset{˙}{0}) = if (i = j, S \cdot_{R} T, \underset{˙}{0})$
45	44	mpoeq3dva	$⊢ ((N \in Fin \land R \in Ring) \land (S \in B \land T \in B)) \to (i \in N, j \in N ⟼ if (i = j, if (i = j, S, \underset{˙}{0}) \cdot_{R} if (i = j, T, \underset{˙}{0}), \underset{˙}{0})) = (i \in N, j \in N ⟼ if (i = j, S \cdot_{R} T, \underset{˙}{0}))$
46		eqidd	$⊢ (((N \in Fin \land R \in Ring) \land (S \in B \land T \in B)) \land (x \in N \land y \in N)) \to (i \in N, j \in N ⟼ if (i = j, S \cdot_{R} T, \underset{˙}{0})) = (i \in N, j \in N ⟼ if (i = j, S \cdot_{R} T, \underset{˙}{0}))$
47		eqeq12	$⊢ (i = x \land j = y) \to (i = j \leftrightarrow x = y)$
48	6	eqcomi	$⊢ \cdot_{R} = \underset{˙}{\cdot}$
49	48	oveqi	$⊢ S \cdot_{R} T = S \underset{˙}{\cdot} T$
50	49	a1i	$⊢ (i = x \land j = y) \to S \cdot_{R} T = S \underset{˙}{\cdot} T$
51	47 50	ifbieq1d	$⊢ (i = x \land j = y) \to if (i = j, S \cdot_{R} T, \underset{˙}{0}) = if (x = y, S \underset{˙}{\cdot} T, \underset{˙}{0})$
52	51	adantl	$⊢ ((((N \in Fin \land R \in Ring) \land (S \in B \land T \in B)) \land (x \in N \land y \in N)) \land (i = x \land j = y)) \to if (i = j, S \cdot_{R} T, \underset{˙}{0}) = if (x = y, S \underset{˙}{\cdot} T, \underset{˙}{0})$
53		simprl	$⊢ (((N \in Fin \land R \in Ring) \land (S \in B \land T \in B)) \land (x \in N \land y \in N)) \to x \in N$
54		simprr	$⊢ (((N \in Fin \land R \in Ring) \land (S \in B \land T \in B)) \land (x \in N \land y \in N)) \to y \in N$
55		ovex	$⊢ S \underset{˙}{\cdot} T \in V$
56	3	fvexi	$⊢ \underset{˙}{0} \in V$
57	55 56	ifex	$⊢ if (x = y, S \underset{˙}{\cdot} T, \underset{˙}{0}) \in V$
58	57	a1i	$⊢ (((N \in Fin \land R \in Ring) \land (S \in B \land T \in B)) \land (x \in N \land y \in N)) \to if (x = y, S \underset{˙}{\cdot} T, \underset{˙}{0}) \in V$
59	46 52 53 54 58	ovmpod	$⊢ (((N \in Fin \land R \in Ring) \land (S \in B \land T \in B)) \land (x \in N \land y \in N)) \to x (i \in N, j \in N ⟼ if (i = j, S \cdot_{R} T, \underset{˙}{0})) y = if (x = y, S \underset{˙}{\cdot} T, \underset{˙}{0})$
60	27 8 17	3jca	$⊢ ((N \in Fin \land R \in Ring) \land (S \in B \land T \in B)) \to (R \in Ring \land S \in B \land T \in B)$
61	2 6	ringcl	$⊢ (R \in Ring \land S \in B \land T \in B) \to S \underset{˙}{\cdot} T \in B$
62	60 61	syl	$⊢ ((N \in Fin \land R \in Ring) \land (S \in B \land T \in B)) \to S \underset{˙}{\cdot} T \in B$
63	26 27 62	3jca	$⊢ ((N \in Fin \land R \in Ring) \land (S \in B \land T \in B)) \to (N \in Fin \land R \in Ring \land S \underset{˙}{\cdot} T \in B)$
64	1 2 3 4 5	scmatscmide	$⊢ ((N \in Fin \land R \in Ring \land S \underset{˙}{\cdot} T \in B) \land (x \in N \land y \in N)) \to x ((S \underset{˙}{\cdot} T) \underset{˙}{*} \underset{˙}{1}) y = if (x = y, S \underset{˙}{\cdot} T, \underset{˙}{0})$
65	63 64	sylan	$⊢ (((N \in Fin \land R \in Ring) \land (S \in B \land T \in B)) \land (x \in N \land y \in N)) \to x ((S \underset{˙}{\cdot} T) \underset{˙}{*} \underset{˙}{1}) y = if (x = y, S \underset{˙}{\cdot} T, \underset{˙}{0})$
66	59 65	eqtr4d	$⊢ (((N \in Fin \land R \in Ring) \land (S \in B \land T \in B)) \land (x \in N \land y \in N)) \to x (i \in N, j \in N ⟼ if (i = j, S \cdot_{R} T, \underset{˙}{0})) y = x ((S \underset{˙}{\cdot} T) \underset{˙}{*} \underset{˙}{1}) y$
67	66	ralrimivva	$⊢ ((N \in Fin \land R \in Ring) \land (S \in B \land T \in B)) \to \forall x \in N \forall y \in N x (i \in N, j \in N ⟼ if (i = j, S \cdot_{R} T, \underset{˙}{0})) y = x ((S \underset{˙}{\cdot} T) \underset{˙}{*} \underset{˙}{1}) y$
68		eqid	$⊢ \cdot_{R} = \cdot_{R}$
69	2 68	ringcl	$⊢ (R \in Ring \land S \in B \land T \in B) \to S \cdot_{R} T \in B$
70	60 69	syl	$⊢ ((N \in Fin \land R \in Ring) \land (S \in B \land T \in B)) \to S \cdot_{R} T \in B$
71	2 3	ring0cl	$⊢ R \in Ring \to \underset{˙}{0} \in B$
72	71	adantl	$⊢ (N \in Fin \land R \in Ring) \to \underset{˙}{0} \in B$
73	72	adantr	$⊢ ((N \in Fin \land R \in Ring) \land (S \in B \land T \in B)) \to \underset{˙}{0} \in B$
74	70 73	ifcld	$⊢ ((N \in Fin \land R \in Ring) \land (S \in B \land T \in B)) \to if (i = j, S \cdot_{R} T, \underset{˙}{0}) \in B$
75	74	3ad2ant1	$⊢ (((N \in Fin \land R \in Ring) \land (S \in B \land T \in B)) \land i \in N \land j \in N) \to if (i = j, S \cdot_{R} T, \underset{˙}{0}) \in B$
76	1 2 9 26 27 75	matbas2d	$⊢ ((N \in Fin \land R \in Ring) \land (S \in B \land T \in B)) \to (i \in N, j \in N ⟼ if (i = j, S \cdot_{R} T, \underset{˙}{0})) \in {Base}_{A}$
77	1	matring	$⊢ (N \in Fin \land R \in Ring) \to A \in Ring$
78	9 4	ringidcl	$⊢ A \in Ring \to \underset{˙}{1} \in {Base}_{A}$
79	77 78	syl	$⊢ (N \in Fin \land R \in Ring) \to \underset{˙}{1} \in {Base}_{A}$
80	79	adantr	$⊢ ((N \in Fin \land R \in Ring) \land (S \in B \land T \in B)) \to \underset{˙}{1} \in {Base}_{A}$
81	62 80	jca	$⊢ ((N \in Fin \land R \in Ring) \land (S \in B \land T \in B)) \to (S \underset{˙}{\cdot} T \in B \land \underset{˙}{1} \in {Base}_{A})$
82	2 1 9 5	matvscl	$⊢ ((N \in Fin \land R \in Ring) \land (S \underset{˙}{\cdot} T \in B \land \underset{˙}{1} \in {Base}_{A})) \to (S \underset{˙}{\cdot} T) \underset{˙}{*} \underset{˙}{1} \in {Base}_{A}$
83	81 82	syldan	$⊢ ((N \in Fin \land R \in Ring) \land (S \in B \land T \in B)) \to (S \underset{˙}{\cdot} T) \underset{˙}{*} \underset{˙}{1} \in {Base}_{A}$
84	1 9	eqmat	$⊢ ((i \in N, j \in N ⟼ if (i = j, S \cdot_{R} T, \underset{˙}{0})) \in {Base}_{A} \land (S \underset{˙}{\cdot} T) \underset{˙}{} \underset{˙}{1} \in {Base}_{A}) \to ((i \in N, j \in N ⟼ if (i = j, S \cdot_{R} T, \underset{˙}{0})) = (S \underset{˙}{\cdot} T) \underset{˙}{} \underset{˙}{1} \leftrightarrow \forall x \in N \forall y \in N x (i \in N, j \in N ⟼ if (i = j, S \cdot_{R} T, \underset{˙}{0})) y = x ((S \underset{˙}{\cdot} T) \underset{˙}{*} \underset{˙}{1}) y)$
85	76 83 84	syl2anc	$⊢ ((N \in Fin \land R \in Ring) \land (S \in B \land T \in B)) \to ((i \in N, j \in N ⟼ if (i = j, S \cdot_{R} T, \underset{˙}{0})) = (S \underset{˙}{\cdot} T) \underset{˙}{} \underset{˙}{1} \leftrightarrow \forall x \in N \forall y \in N x (i \in N, j \in N ⟼ if (i = j, S \cdot_{R} T, \underset{˙}{0})) y = x ((S \underset{˙}{\cdot} T) \underset{˙}{} \underset{˙}{1}) y)$
86	67 85	mpbird	$⊢ ((N \in Fin \land R \in Ring) \land (S \in B \land T \in B)) \to (i \in N, j \in N ⟼ if (i = j, S \cdot_{R} T, \underset{˙}{0})) = (S \underset{˙}{\cdot} T) \underset{˙}{*} \underset{˙}{1}$
87	45 86	eqtrd	$⊢ ((N \in Fin \land R \in Ring) \land (S \in B \land T \in B)) \to (i \in N, j \in N ⟼ if (i = j, if (i = j, S, \underset{˙}{0}) \cdot_{R} if (i = j, T, \underset{˙}{0}), \underset{˙}{0})) = (S \underset{˙}{\cdot} T) \underset{˙}{*} \underset{˙}{1}$
88	39 87	eqtrd	$⊢ ((N \in Fin \land R \in Ring) \land (S \in B \land T \in B)) \to (i \in N, j \in N ⟼ if (i = j, (i (S \underset{˙}{} \underset{˙}{1}) j) \cdot_{R} (i (T \underset{˙}{} \underset{˙}{1}) j), \underset{˙}{0})) = (S \underset{˙}{\cdot} T) \underset{˙}{*} \underset{˙}{1}$
89	25 88	eqtrd	$⊢ ((N \in Fin \land R \in Ring) \land (S \in B \land T \in B)) \to (S \underset{˙}{} \underset{˙}{1}) \underset{˙}{\times} (T \underset{˙}{} \underset{˙}{1}) = (S \underset{˙}{\cdot} T) \underset{˙}{*} \underset{˙}{1}$

Metamath Proof Explorer

Theorem scmatscmiddistr

Proof