scmatsubcl

Description: The difference of two scalar matrices is a scalar matrix. (Contributed by AV, 20-Aug-2019) (Revised by AV, 19-Dec-2019)

	Ref	Expression
Hypotheses	scmatid.a	$⊢ A = N Mat R$
	scmatid.b	$⊢ B = {Base}_{A}$
	scmatid.e	$⊢ E = {Base}_{R}$
	scmatid.0	$⊢ \underset{˙}{0} = 0_{R}$
	scmatid.s	$⊢ S = N ScMat R$
Assertion	scmatsubcl	$⊢ ((N \in Fin \land R \in Ring) \land (X \in S \land Y \in S)) \to X -_{A} Y \in S$

Proof

Step	Hyp	Ref	Expression
1		scmatid.a	$⊢ A = N Mat R$
2		scmatid.b	$⊢ B = {Base}_{A}$
3		scmatid.e	$⊢ E = {Base}_{R}$
4		scmatid.0	$⊢ \underset{˙}{0} = 0_{R}$
5		scmatid.s	$⊢ S = N ScMat R$
6		eqid	$⊢ 1_{A} = 1_{A}$
7		eqid	$⊢ \cdot_{A} = \cdot_{A}$
8	3 1 2 6 7 5	scmatscmid	$⊢ (N \in Fin \land R \in Ring \land X \in S) \to \exists c \in E X = c \cdot_{A} 1_{A}$
9	8	3expa	$⊢ ((N \in Fin \land R \in Ring) \land X \in S) \to \exists c \in E X = c \cdot_{A} 1_{A}$
10	9	adantrr	$⊢ ((N \in Fin \land R \in Ring) \land (X \in S \land Y \in S)) \to \exists c \in E X = c \cdot_{A} 1_{A}$
11	3 1 2 6 7 5	scmatscmid	$⊢ (N \in Fin \land R \in Ring \land Y \in S) \to \exists d \in E Y = d \cdot_{A} 1_{A}$
12	11	3expia	$⊢ (N \in Fin \land R \in Ring) \to (Y \in S \to \exists d \in E Y = d \cdot_{A} 1_{A})$
13		oveq12	$⊢ (X = c \cdot_{A} 1_{A} \land Y = d \cdot_{A} 1_{A}) \to X -_{A} Y = (c \cdot_{A} 1_{A}) -_{A} (d \cdot_{A} 1_{A})$
14	13	adantl	$⊢ ((((N \in Fin \land R \in Ring) \land d \in E) \land c \in E) \land (X = c \cdot_{A} 1_{A} \land Y = d \cdot_{A} 1_{A})) \to X -_{A} Y = (c \cdot_{A} 1_{A}) -_{A} (d \cdot_{A} 1_{A})$
15		eqid	$⊢ Scalar (A) = Scalar (A)$
16		eqid	$⊢ {Base}_{Scalar (A)} = {Base}_{Scalar (A)}$
17		eqid	$⊢ -_{A} = -_{A}$
18		eqid	$⊢ -_{Scalar (A)} = -_{Scalar (A)}$
19	1	matlmod	$⊢ (N \in Fin \land R \in Ring) \to A \in LMod$
20	19	ad2antrr	$⊢ (((N \in Fin \land R \in Ring) \land d \in E) \land c \in E) \to A \in LMod$
21	1	matsca2	$⊢ (N \in Fin \land R \in Ring) \to R = Scalar (A)$
22	21	fveq2d	$⊢ (N \in Fin \land R \in Ring) \to {Base}_{R} = {Base}_{Scalar (A)}$
23	3 22	eqtrid	$⊢ (N \in Fin \land R \in Ring) \to E = {Base}_{Scalar (A)}$
24	23	eleq2d	$⊢ (N \in Fin \land R \in Ring) \to (c \in E \leftrightarrow c \in {Base}_{Scalar (A)})$
25	24	biimpd	$⊢ (N \in Fin \land R \in Ring) \to (c \in E \to c \in {Base}_{Scalar (A)})$
26	25	adantr	$⊢ ((N \in Fin \land R \in Ring) \land d \in E) \to (c \in E \to c \in {Base}_{Scalar (A)})$
27	26	imp	$⊢ (((N \in Fin \land R \in Ring) \land d \in E) \land c \in E) \to c \in {Base}_{Scalar (A)}$
28	23	eleq2d	$⊢ (N \in Fin \land R \in Ring) \to (d \in E \leftrightarrow d \in {Base}_{Scalar (A)})$
29	28	biimpa	$⊢ ((N \in Fin \land R \in Ring) \land d \in E) \to d \in {Base}_{Scalar (A)}$
30	29	adantr	$⊢ (((N \in Fin \land R \in Ring) \land d \in E) \land c \in E) \to d \in {Base}_{Scalar (A)}$
31	1	matring	$⊢ (N \in Fin \land R \in Ring) \to A \in Ring$
32	2 6	ringidcl	$⊢ A \in Ring \to 1_{A} \in B$
33	31 32	syl	$⊢ (N \in Fin \land R \in Ring) \to 1_{A} \in B$
34	33	ad2antrr	$⊢ (((N \in Fin \land R \in Ring) \land d \in E) \land c \in E) \to 1_{A} \in B$
35	2 7 15 16 17 18 20 27 30 34	lmodsubdir	$⊢ (((N \in Fin \land R \in Ring) \land d \in E) \land c \in E) \to (c -_{Scalar (A)} d) \cdot_{A} 1_{A} = (c \cdot_{A} 1_{A}) -_{A} (d \cdot_{A} 1_{A})$
36	35	eqcomd	$⊢ (((N \in Fin \land R \in Ring) \land d \in E) \land c \in E) \to (c \cdot_{A} 1_{A}) -_{A} (d \cdot_{A} 1_{A}) = (c -_{Scalar (A)} d) \cdot_{A} 1_{A}$
37		simpll	$⊢ (((N \in Fin \land R \in Ring) \land d \in E) \land c \in E) \to (N \in Fin \land R \in Ring)$
38	21	eqcomd	$⊢ (N \in Fin \land R \in Ring) \to Scalar (A) = R$
39	38	ad2antrr	$⊢ (((N \in Fin \land R \in Ring) \land d \in E) \land c \in E) \to Scalar (A) = R$
40	39	fveq2d	$⊢ (((N \in Fin \land R \in Ring) \land d \in E) \land c \in E) \to -_{Scalar (A)} = -_{R}$
41	40	oveqd	$⊢ (((N \in Fin \land R \in Ring) \land d \in E) \land c \in E) \to c -_{Scalar (A)} d = c -_{R} d$
42		ringgrp	$⊢ R \in Ring \to R \in Grp$
43	42	adantl	$⊢ (N \in Fin \land R \in Ring) \to R \in Grp$
44	43	ad2antrr	$⊢ (((N \in Fin \land R \in Ring) \land d \in E) \land c \in E) \to R \in Grp$
45		simpr	$⊢ (((N \in Fin \land R \in Ring) \land d \in E) \land c \in E) \to c \in E$
46		simplr	$⊢ (((N \in Fin \land R \in Ring) \land d \in E) \land c \in E) \to d \in E$
47		eqid	$⊢ -_{R} = -_{R}$
48	3 47	grpsubcl	$⊢ (R \in Grp \land c \in E \land d \in E) \to c -_{R} d \in E$
49	44 45 46 48	syl3anc	$⊢ (((N \in Fin \land R \in Ring) \land d \in E) \land c \in E) \to c -_{R} d \in E$
50	41 49	eqeltrd	$⊢ (((N \in Fin \land R \in Ring) \land d \in E) \land c \in E) \to c -_{Scalar (A)} d \in E$
51	3 1 2 7	matvscl	$⊢ ((N \in Fin \land R \in Ring) \land (c -_{Scalar (A)} d \in E \land 1_{A} \in B)) \to (c -_{Scalar (A)} d) \cdot_{A} 1_{A} \in B$
52	37 50 34 51	syl12anc	$⊢ (((N \in Fin \land R \in Ring) \land d \in E) \land c \in E) \to (c -_{Scalar (A)} d) \cdot_{A} 1_{A} \in B$
53		oveq1	$⊢ e = c -_{Scalar (A)} d \to e \cdot_{A} 1_{A} = (c -_{Scalar (A)} d) \cdot_{A} 1_{A}$
54	53	eqeq2d	$⊢ e = c -_{Scalar (A)} d \to ((c -_{Scalar (A)} d) \cdot_{A} 1_{A} = e \cdot_{A} 1_{A} \leftrightarrow (c -_{Scalar (A)} d) \cdot_{A} 1_{A} = (c -_{Scalar (A)} d) \cdot_{A} 1_{A})$
55	54	adantl	$⊢ ((((N \in Fin \land R \in Ring) \land d \in E) \land c \in E) \land e = c -_{Scalar (A)} d) \to ((c -_{Scalar (A)} d) \cdot_{A} 1_{A} = e \cdot_{A} 1_{A} \leftrightarrow (c -_{Scalar (A)} d) \cdot_{A} 1_{A} = (c -_{Scalar (A)} d) \cdot_{A} 1_{A})$
56		eqidd	$⊢ (((N \in Fin \land R \in Ring) \land d \in E) \land c \in E) \to (c -_{Scalar (A)} d) \cdot_{A} 1_{A} = (c -_{Scalar (A)} d) \cdot_{A} 1_{A}$
57	50 55 56	rspcedvd	$⊢ (((N \in Fin \land R \in Ring) \land d \in E) \land c \in E) \to \exists e \in E (c -_{Scalar (A)} d) \cdot_{A} 1_{A} = e \cdot_{A} 1_{A}$
58	3 1 2 6 7 5	scmatel	$⊢ (N \in Fin \land R \in Ring) \to ((c -_{Scalar (A)} d) \cdot_{A} 1_{A} \in S \leftrightarrow ((c -_{Scalar (A)} d) \cdot_{A} 1_{A} \in B \land \exists e \in E (c -_{Scalar (A)} d) \cdot_{A} 1_{A} = e \cdot_{A} 1_{A}))$
59	58	ad2antrr	$⊢ (((N \in Fin \land R \in Ring) \land d \in E) \land c \in E) \to ((c -_{Scalar (A)} d) \cdot_{A} 1_{A} \in S \leftrightarrow ((c -_{Scalar (A)} d) \cdot_{A} 1_{A} \in B \land \exists e \in E (c -_{Scalar (A)} d) \cdot_{A} 1_{A} = e \cdot_{A} 1_{A}))$
60	52 57 59	mpbir2and	$⊢ (((N \in Fin \land R \in Ring) \land d \in E) \land c \in E) \to (c -_{Scalar (A)} d) \cdot_{A} 1_{A} \in S$
61	36 60	eqeltrd	$⊢ (((N \in Fin \land R \in Ring) \land d \in E) \land c \in E) \to (c \cdot_{A} 1_{A}) -_{A} (d \cdot_{A} 1_{A}) \in S$
62	61	adantr	$⊢ ((((N \in Fin \land R \in Ring) \land d \in E) \land c \in E) \land (X = c \cdot_{A} 1_{A} \land Y = d \cdot_{A} 1_{A})) \to (c \cdot_{A} 1_{A}) -_{A} (d \cdot_{A} 1_{A}) \in S$
63	14 62	eqeltrd	$⊢ ((((N \in Fin \land R \in Ring) \land d \in E) \land c \in E) \land (X = c \cdot_{A} 1_{A} \land Y = d \cdot_{A} 1_{A})) \to X -_{A} Y \in S$
64	63	exp32	$⊢ (((N \in Fin \land R \in Ring) \land d \in E) \land c \in E) \to (X = c \cdot_{A} 1_{A} \to (Y = d \cdot_{A} 1_{A} \to X -_{A} Y \in S))$
65	64	rexlimdva	$⊢ ((N \in Fin \land R \in Ring) \land d \in E) \to (\exists c \in E X = c \cdot_{A} 1_{A} \to (Y = d \cdot_{A} 1_{A} \to X -_{A} Y \in S))$
66	65	com23	$⊢ ((N \in Fin \land R \in Ring) \land d \in E) \to (Y = d \cdot_{A} 1_{A} \to (\exists c \in E X = c \cdot_{A} 1_{A} \to X -_{A} Y \in S))$
67	66	rexlimdva	$⊢ (N \in Fin \land R \in Ring) \to (\exists d \in E Y = d \cdot_{A} 1_{A} \to (\exists c \in E X = c \cdot_{A} 1_{A} \to X -_{A} Y \in S))$
68	12 67	syldc	$⊢ Y \in S \to ((N \in Fin \land R \in Ring) \to (\exists c \in E X = c \cdot_{A} 1_{A} \to X -_{A} Y \in S))$
69	68	adantl	$⊢ (X \in S \land Y \in S) \to ((N \in Fin \land R \in Ring) \to (\exists c \in E X = c \cdot_{A} 1_{A} \to X -_{A} Y \in S))$
70	69	impcom	$⊢ ((N \in Fin \land R \in Ring) \land (X \in S \land Y \in S)) \to (\exists c \in E X = c \cdot_{A} 1_{A} \to X -_{A} Y \in S)$
71	10 70	mpd	$⊢ ((N \in Fin \land R \in Ring) \land (X \in S \land Y \in S)) \to X -_{A} Y \in S$

Metamath Proof Explorer

Theorem scmatsubcl

Proof