smatvscl

Description: Closure of the scalar multiplication in the ring of scalar matrices. ( matvscl analog.) (Contributed by AV, 24-Dec-2019)

	Ref	Expression
Hypotheses	smatvscl.k	$⊢ K = {Base}_{R}$
	smatvscl.a	$⊢ A = N Mat R$
	smatvscl.s	$⊢ S = N ScMat R$
	smatvscl.t	$⊢ \underset{˙}{*} = \cdot_{A}$
Assertion	smatvscl	$⊢ ((N \in Fin \land R \in Ring) \land (C \in K \land X \in S)) \to C \underset{˙}{*} X \in S$

Proof

Step	Hyp	Ref	Expression
1		smatvscl.k	$⊢ K = {Base}_{R}$
2		smatvscl.a	$⊢ A = N Mat R$
3		smatvscl.s	$⊢ S = N ScMat R$
4		smatvscl.t	$⊢ \underset{˙}{*} = \cdot_{A}$
5		eqid	$⊢ {Base}_{R} = {Base}_{R}$
6		eqid	$⊢ {Base}_{A} = {Base}_{A}$
7		eqid	$⊢ 1_{A} = 1_{A}$
8	5 2 6 7 4 3	scmatel	$⊢ (N \in Fin \land R \in Ring) \to (X \in S \leftrightarrow (X \in {Base}_{A} \land \exists c \in {Base}_{R} X = c \underset{˙}{*} 1_{A}))$
9		oveq2	$⊢ X = c \underset{˙}{} 1_{A} \to C \underset{˙}{} X = C \underset{˙}{} (c \underset{˙}{} 1_{A})$
10	9	adantl	$⊢ (((((N \in Fin \land R \in Ring) \land C \in K) \land X \in {Base}_{A}) \land c \in {Base}_{R}) \land X = c \underset{˙}{} 1_{A}) \to C \underset{˙}{} X = C \underset{˙}{} (c \underset{˙}{} 1_{A})$
11	2	matlmod	$⊢ (N \in Fin \land R \in Ring) \to A \in LMod$
12	11	ad3antrrr	$⊢ ((((N \in Fin \land R \in Ring) \land C \in K) \land X \in {Base}_{A}) \land c \in {Base}_{R}) \to A \in LMod$
13	2	matsca2	$⊢ (N \in Fin \land R \in Ring) \to R = Scalar (A)$
14	13	fveq2d	$⊢ (N \in Fin \land R \in Ring) \to {Base}_{R} = {Base}_{Scalar (A)}$
15	1 14	eqtrid	$⊢ (N \in Fin \land R \in Ring) \to K = {Base}_{Scalar (A)}$
16	15	eleq2d	$⊢ (N \in Fin \land R \in Ring) \to (C \in K \leftrightarrow C \in {Base}_{Scalar (A)})$
17	16	biimpa	$⊢ ((N \in Fin \land R \in Ring) \land C \in K) \to C \in {Base}_{Scalar (A)}$
18	17	ad2antrr	$⊢ ((((N \in Fin \land R \in Ring) \land C \in K) \land X \in {Base}_{A}) \land c \in {Base}_{R}) \to C \in {Base}_{Scalar (A)}$
19	13	ad2antrr	$⊢ (((N \in Fin \land R \in Ring) \land C \in K) \land X \in {Base}_{A}) \to R = Scalar (A)$
20	19	fveq2d	$⊢ (((N \in Fin \land R \in Ring) \land C \in K) \land X \in {Base}_{A}) \to {Base}_{R} = {Base}_{Scalar (A)}$
21	20	eleq2d	$⊢ (((N \in Fin \land R \in Ring) \land C \in K) \land X \in {Base}_{A}) \to (c \in {Base}_{R} \leftrightarrow c \in {Base}_{Scalar (A)})$
22	21	biimpa	$⊢ ((((N \in Fin \land R \in Ring) \land C \in K) \land X \in {Base}_{A}) \land c \in {Base}_{R}) \to c \in {Base}_{Scalar (A)}$
23	2	matring	$⊢ (N \in Fin \land R \in Ring) \to A \in Ring$
24	6 7	ringidcl	$⊢ A \in Ring \to 1_{A} \in {Base}_{A}$
25	23 24	syl	$⊢ (N \in Fin \land R \in Ring) \to 1_{A} \in {Base}_{A}$
26	25	ad3antrrr	$⊢ ((((N \in Fin \land R \in Ring) \land C \in K) \land X \in {Base}_{A}) \land c \in {Base}_{R}) \to 1_{A} \in {Base}_{A}$
27		eqid	$⊢ Scalar (A) = Scalar (A)$
28		eqid	$⊢ {Base}_{Scalar (A)} = {Base}_{Scalar (A)}$
29		eqid	$⊢ \cdot_{Scalar (A)} = \cdot_{Scalar (A)}$
30	6 27 4 28 29	lmodvsass	$⊢ (A \in LMod \land (C \in {Base}_{Scalar (A)} \land c \in {Base}_{Scalar (A)} \land 1_{A} \in {Base}_{A})) \to (C \cdot_{Scalar (A)} c) \underset{˙}{} 1_{A} = C \underset{˙}{} (c \underset{˙}{*} 1_{A})$
31	12 18 22 26 30	syl13anc	$⊢ ((((N \in Fin \land R \in Ring) \land C \in K) \land X \in {Base}_{A}) \land c \in {Base}_{R}) \to (C \cdot_{Scalar (A)} c) \underset{˙}{} 1_{A} = C \underset{˙}{} (c \underset{˙}{*} 1_{A})$
32	31	eqcomd	$⊢ ((((N \in Fin \land R \in Ring) \land C \in K) \land X \in {Base}_{A}) \land c \in {Base}_{R}) \to C \underset{˙}{} (c \underset{˙}{} 1_{A}) = (C \cdot_{Scalar (A)} c) \underset{˙}{*} 1_{A}$
33		simplll	$⊢ ((((N \in Fin \land R \in Ring) \land C \in K) \land X \in {Base}_{A}) \land c \in {Base}_{R}) \to (N \in Fin \land R \in Ring)$
34	13	adantr	$⊢ ((N \in Fin \land R \in Ring) \land C \in K) \to R = Scalar (A)$
35	34	eqcomd	$⊢ ((N \in Fin \land R \in Ring) \land C \in K) \to Scalar (A) = R$
36	35	ad2antrr	$⊢ ((((N \in Fin \land R \in Ring) \land C \in K) \land X \in {Base}_{A}) \land c \in {Base}_{R}) \to Scalar (A) = R$
37	36	fveq2d	$⊢ ((((N \in Fin \land R \in Ring) \land C \in K) \land X \in {Base}_{A}) \land c \in {Base}_{R}) \to \cdot_{Scalar (A)} = \cdot_{R}$
38	37	oveqd	$⊢ ((((N \in Fin \land R \in Ring) \land C \in K) \land X \in {Base}_{A}) \land c \in {Base}_{R}) \to C \cdot_{Scalar (A)} c = C \cdot_{R} c$
39		simp-4r	$⊢ ((((N \in Fin \land R \in Ring) \land C \in K) \land X \in {Base}_{A}) \land c \in {Base}_{R}) \to R \in Ring$
40		simpllr	$⊢ ((((N \in Fin \land R \in Ring) \land C \in K) \land X \in {Base}_{A}) \land c \in {Base}_{R}) \to C \in K$
41	1	eqcomi	$⊢ {Base}_{R} = K$
42	41	eleq2i	$⊢ c \in {Base}_{R} \leftrightarrow c \in K$
43	42	biimpi	$⊢ c \in {Base}_{R} \to c \in K$
44	43	adantl	$⊢ ((((N \in Fin \land R \in Ring) \land C \in K) \land X \in {Base}_{A}) \land c \in {Base}_{R}) \to c \in K$
45		eqid	$⊢ \cdot_{R} = \cdot_{R}$
46	1 45	ringcl	$⊢ (R \in Ring \land C \in K \land c \in K) \to C \cdot_{R} c \in K$
47	39 40 44 46	syl3anc	$⊢ ((((N \in Fin \land R \in Ring) \land C \in K) \land X \in {Base}_{A}) \land c \in {Base}_{R}) \to C \cdot_{R} c \in K$
48	38 47	eqeltrd	$⊢ ((((N \in Fin \land R \in Ring) \land C \in K) \land X \in {Base}_{A}) \land c \in {Base}_{R}) \to C \cdot_{Scalar (A)} c \in K$
49	1 2 6 4	matvscl	$⊢ ((N \in Fin \land R \in Ring) \land (C \cdot_{Scalar (A)} c \in K \land 1_{A} \in {Base}_{A})) \to (C \cdot_{Scalar (A)} c) \underset{˙}{*} 1_{A} \in {Base}_{A}$
50	33 48 26 49	syl12anc	$⊢ ((((N \in Fin \land R \in Ring) \land C \in K) \land X \in {Base}_{A}) \land c \in {Base}_{R}) \to (C \cdot_{Scalar (A)} c) \underset{˙}{*} 1_{A} \in {Base}_{A}$
51		oveq1	$⊢ C \cdot_{Scalar (A)} c = e \to (C \cdot_{Scalar (A)} c) \underset{˙}{} 1_{A} = e \underset{˙}{} 1_{A}$
52	51	eqcoms	$⊢ e = C \cdot_{Scalar (A)} c \to (C \cdot_{Scalar (A)} c) \underset{˙}{} 1_{A} = e \underset{˙}{} 1_{A}$
53	52	adantl	$⊢ (((((N \in Fin \land R \in Ring) \land C \in K) \land X \in {Base}_{A}) \land c \in {Base}_{R}) \land e = C \cdot_{Scalar (A)} c) \to (C \cdot_{Scalar (A)} c) \underset{˙}{} 1_{A} = e \underset{˙}{} 1_{A}$
54	48 53	rspcedeq2vd	$⊢ ((((N \in Fin \land R \in Ring) \land C \in K) \land X \in {Base}_{A}) \land c \in {Base}_{R}) \to \exists e \in K (C \cdot_{Scalar (A)} c) \underset{˙}{} 1_{A} = e \underset{˙}{} 1_{A}$
55	1 2 6 7 4 3	scmatel	$⊢ (N \in Fin \land R \in Ring) \to ((C \cdot_{Scalar (A)} c) \underset{˙}{} 1_{A} \in S \leftrightarrow ((C \cdot_{Scalar (A)} c) \underset{˙}{} 1_{A} \in {Base}_{A} \land \exists e \in K (C \cdot_{Scalar (A)} c) \underset{˙}{} 1_{A} = e \underset{˙}{} 1_{A}))$
56	55	ad3antrrr	$⊢ ((((N \in Fin \land R \in Ring) \land C \in K) \land X \in {Base}_{A}) \land c \in {Base}_{R}) \to ((C \cdot_{Scalar (A)} c) \underset{˙}{} 1_{A} \in S \leftrightarrow ((C \cdot_{Scalar (A)} c) \underset{˙}{} 1_{A} \in {Base}_{A} \land \exists e \in K (C \cdot_{Scalar (A)} c) \underset{˙}{} 1_{A} = e \underset{˙}{} 1_{A}))$
57	50 54 56	mpbir2and	$⊢ ((((N \in Fin \land R \in Ring) \land C \in K) \land X \in {Base}_{A}) \land c \in {Base}_{R}) \to (C \cdot_{Scalar (A)} c) \underset{˙}{*} 1_{A} \in S$
58	32 57	eqeltrd	$⊢ ((((N \in Fin \land R \in Ring) \land C \in K) \land X \in {Base}_{A}) \land c \in {Base}_{R}) \to C \underset{˙}{} (c \underset{˙}{} 1_{A}) \in S$
59	58	adantr	$⊢ (((((N \in Fin \land R \in Ring) \land C \in K) \land X \in {Base}_{A}) \land c \in {Base}_{R}) \land X = c \underset{˙}{} 1_{A}) \to C \underset{˙}{} (c \underset{˙}{*} 1_{A}) \in S$
60	10 59	eqeltrd	$⊢ (((((N \in Fin \land R \in Ring) \land C \in K) \land X \in {Base}_{A}) \land c \in {Base}_{R}) \land X = c \underset{˙}{} 1_{A}) \to C \underset{˙}{} X \in S$
61	60	rexlimdva2	$⊢ (((N \in Fin \land R \in Ring) \land C \in K) \land X \in {Base}_{A}) \to (\exists c \in {Base}_{R} X = c \underset{˙}{} 1_{A} \to C \underset{˙}{} X \in S)$
62	61	expimpd	$⊢ ((N \in Fin \land R \in Ring) \land C \in K) \to ((X \in {Base}_{A} \land \exists c \in {Base}_{R} X = c \underset{˙}{} 1_{A}) \to C \underset{˙}{} X \in S)$
63	62	ex	$⊢ (N \in Fin \land R \in Ring) \to (C \in K \to ((X \in {Base}_{A} \land \exists c \in {Base}_{R} X = c \underset{˙}{} 1_{A}) \to C \underset{˙}{} X \in S))$
64	63	com23	$⊢ (N \in Fin \land R \in Ring) \to ((X \in {Base}_{A} \land \exists c \in {Base}_{R} X = c \underset{˙}{} 1_{A}) \to (C \in K \to C \underset{˙}{} X \in S))$
65	8 64	sylbid	$⊢ (N \in Fin \land R \in Ring) \to (X \in S \to (C \in K \to C \underset{˙}{*} X \in S))$
66	65	com23	$⊢ (N \in Fin \land R \in Ring) \to (C \in K \to (X \in S \to C \underset{˙}{*} X \in S))$
67	66	imp32	$⊢ ((N \in Fin \land R \in Ring) \land (C \in K \land X \in S)) \to C \underset{˙}{*} X \in S$

Metamath Proof Explorer

Theorem smatvscl

Proof