scmatval

Description: The set of N x N scalar matrices over (a ring) R . (Contributed by AV, 18-Dec-2019)

	Ref	Expression
Hypotheses	scmatval.k	$⊢ K = {Base}_{R}$
	scmatval.a	$⊢ A = N Mat R$
	scmatval.b	$⊢ B = {Base}_{A}$
	scmatval.1	$⊢ \underset{˙}{1} = 1_{A}$
	scmatval.t	$⊢ \underset{˙}{\cdot} = \cdot_{A}$
	scmatval.s	$⊢ S = N ScMat R$
Assertion	scmatval	$⊢ (N \in Fin \land R \in V) \to S = \{m \in B \| \exists c \in K m = c \underset{˙}{\cdot} \underset{˙}{1}\}$

Proof

Step	Hyp	Ref	Expression
1		scmatval.k	$⊢ K = {Base}_{R}$
2		scmatval.a	$⊢ A = N Mat R$
3		scmatval.b	$⊢ B = {Base}_{A}$
4		scmatval.1	$⊢ \underset{˙}{1} = 1_{A}$
5		scmatval.t	$⊢ \underset{˙}{\cdot} = \cdot_{A}$
6		scmatval.s	$⊢ S = N ScMat R$
7		df-scmat	$⊢ ScMat = (n \in Fin, r \in V ⟼ ⦋ (n Mat r) / a ⦌ \{m \in {Base}_{a} \| \exists c \in {Base}_{r} m = c \cdot_{a} 1_{a}\})$
8	7	a1i	$⊢ (N \in Fin \land R \in V) \to ScMat = (n \in Fin, r \in V ⟼ ⦋ (n Mat r) / a ⦌ \{m \in {Base}_{a} \| \exists c \in {Base}_{r} m = c \cdot_{a} 1_{a}\})$
9		ovexd	$⊢ ((N \in Fin \land R \in V) \land (n = N \land r = R)) \to n Mat r \in V$
10		fveq2	$⊢ a = n Mat r \to {Base}_{a} = {Base}_{(n Mat r)}$
11		fveq2	$⊢ a = n Mat r \to \cdot_{a} = \cdot_{(n Mat r)}$
12		eqidd	$⊢ a = n Mat r \to c = c$
13		fveq2	$⊢ a = n Mat r \to 1_{a} = 1_{(n Mat r)}$
14	11 12 13	oveq123d	$⊢ a = n Mat r \to c \cdot_{a} 1_{a} = c \cdot_{(n Mat r)} 1_{(n Mat r)}$
15	14	eqeq2d	$⊢ a = n Mat r \to (m = c \cdot_{a} 1_{a} \leftrightarrow m = c \cdot_{(n Mat r)} 1_{(n Mat r)})$
16	15	rexbidv	$⊢ a = n Mat r \to (\exists c \in {Base}_{r} m = c \cdot_{a} 1_{a} \leftrightarrow \exists c \in {Base}_{r} m = c \cdot_{(n Mat r)} 1_{(n Mat r)})$
17	10 16	rabeqbidv	$⊢ a = n Mat r \to \{m \in {Base}_{a} \| \exists c \in {Base}_{r} m = c \cdot_{a} 1_{a}\} = \{m \in {Base}_{(n Mat r)} \| \exists c \in {Base}_{r} m = c \cdot_{(n Mat r)} 1_{(n Mat r)}\}$
18	17	adantl	$⊢ (((N \in Fin \land R \in V) \land (n = N \land r = R)) \land a = n Mat r) \to \{m \in {Base}_{a} \| \exists c \in {Base}_{r} m = c \cdot_{a} 1_{a}\} = \{m \in {Base}_{(n Mat r)} \| \exists c \in {Base}_{r} m = c \cdot_{(n Mat r)} 1_{(n Mat r)}\}$
19	9 18	csbied	$⊢ ((N \in Fin \land R \in V) \land (n = N \land r = R)) \to ⦋ (n Mat r) / a ⦌ \{m \in {Base}_{a} \| \exists c \in {Base}_{r} m = c \cdot_{a} 1_{a}\} = \{m \in {Base}_{(n Mat r)} \| \exists c \in {Base}_{r} m = c \cdot_{(n Mat r)} 1_{(n Mat r)}\}$
20		oveq12	$⊢ (n = N \land r = R) \to n Mat r = N Mat R$
21	20	fveq2d	$⊢ (n = N \land r = R) \to {Base}_{(n Mat r)} = {Base}_{(N Mat R)}$
22	2	fveq2i	$⊢ {Base}_{A} = {Base}_{(N Mat R)}$
23	3 22	eqtri	$⊢ B = {Base}_{(N Mat R)}$
24	21 23	eqtr4di	$⊢ (n = N \land r = R) \to {Base}_{(n Mat r)} = B$
25		fveq2	$⊢ r = R \to {Base}_{r} = {Base}_{R}$
26	25 1	eqtr4di	$⊢ r = R \to {Base}_{r} = K$
27	26	adantl	$⊢ (n = N \land r = R) \to {Base}_{r} = K$
28	20	fveq2d	$⊢ (n = N \land r = R) \to \cdot_{(n Mat r)} = \cdot_{(N Mat R)}$
29	2	fveq2i	$⊢ \cdot_{A} = \cdot_{(N Mat R)}$
30	5 29	eqtri	$⊢ \underset{˙}{\cdot} = \cdot_{(N Mat R)}$
31	28 30	eqtr4di	$⊢ (n = N \land r = R) \to \cdot_{(n Mat r)} = \underset{˙}{\cdot}$
32		eqidd	$⊢ (n = N \land r = R) \to c = c$
33	20	fveq2d	$⊢ (n = N \land r = R) \to 1_{(n Mat r)} = 1_{(N Mat R)}$
34	2	fveq2i	$⊢ 1_{A} = 1_{(N Mat R)}$
35	4 34	eqtri	$⊢ \underset{˙}{1} = 1_{(N Mat R)}$
36	33 35	eqtr4di	$⊢ (n = N \land r = R) \to 1_{(n Mat r)} = \underset{˙}{1}$
37	31 32 36	oveq123d	$⊢ (n = N \land r = R) \to c \cdot_{(n Mat r)} 1_{(n Mat r)} = c \underset{˙}{\cdot} \underset{˙}{1}$
38	37	eqeq2d	$⊢ (n = N \land r = R) \to (m = c \cdot_{(n Mat r)} 1_{(n Mat r)} \leftrightarrow m = c \underset{˙}{\cdot} \underset{˙}{1})$
39	27 38	rexeqbidv	$⊢ (n = N \land r = R) \to (\exists c \in {Base}_{r} m = c \cdot_{(n Mat r)} 1_{(n Mat r)} \leftrightarrow \exists c \in K m = c \underset{˙}{\cdot} \underset{˙}{1})$
40	24 39	rabeqbidv	$⊢ (n = N \land r = R) \to \{m \in {Base}_{(n Mat r)} \| \exists c \in {Base}_{r} m = c \cdot_{(n Mat r)} 1_{(n Mat r)}\} = \{m \in B \| \exists c \in K m = c \underset{˙}{\cdot} \underset{˙}{1}\}$
41	40	adantl	$⊢ ((N \in Fin \land R \in V) \land (n = N \land r = R)) \to \{m \in {Base}_{(n Mat r)} \| \exists c \in {Base}_{r} m = c \cdot_{(n Mat r)} 1_{(n Mat r)}\} = \{m \in B \| \exists c \in K m = c \underset{˙}{\cdot} \underset{˙}{1}\}$
42	19 41	eqtrd	$⊢ ((N \in Fin \land R \in V) \land (n = N \land r = R)) \to ⦋ (n Mat r) / a ⦌ \{m \in {Base}_{a} \| \exists c \in {Base}_{r} m = c \cdot_{a} 1_{a}\} = \{m \in B \| \exists c \in K m = c \underset{˙}{\cdot} \underset{˙}{1}\}$
43		simpl	$⊢ (N \in Fin \land R \in V) \to N \in Fin$
44		elex	$⊢ R \in V \to R \in V$
45	44	adantl	$⊢ (N \in Fin \land R \in V) \to R \in V$
46	3	fvexi	$⊢ B \in V$
47	46	rabex	$⊢ \{m \in B \| \exists c \in K m = c \underset{˙}{\cdot} \underset{˙}{1}\} \in V$
48	47	a1i	$⊢ (N \in Fin \land R \in V) \to \{m \in B \| \exists c \in K m = c \underset{˙}{\cdot} \underset{˙}{1}\} \in V$
49	8 42 43 45 48	ovmpod	$⊢ (N \in Fin \land R \in V) \to N ScMat R = \{m \in B \| \exists c \in K m = c \underset{˙}{\cdot} \underset{˙}{1}\}$
50	6 49	eqtrid	$⊢ (N \in Fin \land R \in V) \to S = \{m \in B \| \exists c \in K m = c \underset{˙}{\cdot} \underset{˙}{1}\}$

Metamath Proof Explorer

Theorem scmatval

Proof