mat1scmat

Description: A 1-dimensional matrix over a ring is always a scalar matrix (and therefore, by scmatdmat , also a diagonal matrix). (Contributed by AV, 21-Dec-2019)

	Ref	Expression
Hypotheses	mat1scmat.a	$⊢ A = N Mat R$
	mat1scmat.b	$⊢ B = {Base}_{A}$
Assertion	mat1scmat	$⊢ (N \in V \land \|N\| = 1 \land R \in Ring) \to (M \in B \to M \in (N ScMat R))$

Proof

Step	Hyp	Ref	Expression
1		mat1scmat.a	$⊢ A = N Mat R$
2		mat1scmat.b	$⊢ B = {Base}_{A}$
3		hash1snb	$⊢ N \in V \to (\|N\| = 1 \leftrightarrow \exists e N = \{e\})$
4		simpr	$⊢ (R \in Ring \land M \in {Base}_{(\{e\} Mat R)}) \to M \in {Base}_{(\{e\} Mat R)}$
5		eqid	$⊢ \{e\} Mat R = \{e\} Mat R$
6		eqid	$⊢ {Base}_{R} = {Base}_{R}$
7		eqid	$⊢ ⟨e, e⟩ = ⟨e, e⟩$
8	5 6 7	mat1dimelbas	$⊢ (R \in Ring \land e \in V) \to (M \in {Base}_{(\{e\} Mat R)} \leftrightarrow \exists c \in {Base}_{R} M = \{⟨⟨e, e⟩, c⟩\})$
9	8	elvd	$⊢ R \in Ring \to (M \in {Base}_{(\{e\} Mat R)} \leftrightarrow \exists c \in {Base}_{R} M = \{⟨⟨e, e⟩, c⟩\})$
10		simpr	$⊢ ((R \in Ring \land c \in {Base}_{R}) \land M = \{⟨⟨e, e⟩, c⟩\}) \to M = \{⟨⟨e, e⟩, c⟩\}$
11		vex	$⊢ e \in V$
12	11	a1i	$⊢ c \in {Base}_{R} \to e \in V$
13	5 6 7	mat1dimid	$⊢ (R \in Ring \land e \in V) \to 1_{(\{e\} Mat R)} = \{⟨⟨e, e⟩, 1_{R}⟩\}$
14	12 13	sylan2	$⊢ (R \in Ring \land c \in {Base}_{R}) \to 1_{(\{e\} Mat R)} = \{⟨⟨e, e⟩, 1_{R}⟩\}$
15	14	oveq2d	$⊢ (R \in Ring \land c \in {Base}_{R}) \to c \cdot_{(\{e\} Mat R)} 1_{(\{e\} Mat R)} = c \cdot_{(\{e\} Mat R)} \{⟨⟨e, e⟩, 1_{R}⟩\}$
16		simpl	$⊢ (R \in Ring \land c \in {Base}_{R}) \to R \in Ring$
17	16 11	jctir	$⊢ (R \in Ring \land c \in {Base}_{R}) \to (R \in Ring \land e \in V)$
18		simpr	$⊢ (R \in Ring \land c \in {Base}_{R}) \to c \in {Base}_{R}$
19		eqid	$⊢ 1_{R} = 1_{R}$
20	6 19	ringidcl	$⊢ R \in Ring \to 1_{R} \in {Base}_{R}$
21	20	adantr	$⊢ (R \in Ring \land c \in {Base}_{R}) \to 1_{R} \in {Base}_{R}$
22	5 6 7	mat1dimscm	$⊢ ((R \in Ring \land e \in V) \land (c \in {Base}_{R} \land 1_{R} \in {Base}_{R})) \to c \cdot_{(\{e\} Mat R)} \{⟨⟨e, e⟩, 1_{R}⟩\} = \{⟨⟨e, e⟩, c \cdot_{R} 1_{R}⟩\}$
23	17 18 21 22	syl12anc	$⊢ (R \in Ring \land c \in {Base}_{R}) \to c \cdot_{(\{e\} Mat R)} \{⟨⟨e, e⟩, 1_{R}⟩\} = \{⟨⟨e, e⟩, c \cdot_{R} 1_{R}⟩\}$
24		eqid	$⊢ \cdot_{R} = \cdot_{R}$
25	6 24 19	ringridm	$⊢ (R \in Ring \land c \in {Base}_{R}) \to c \cdot_{R} 1_{R} = c$
26	25	opeq2d	$⊢ (R \in Ring \land c \in {Base}_{R}) \to ⟨⟨e, e⟩, c \cdot_{R} 1_{R}⟩ = ⟨⟨e, e⟩, c⟩$
27	26	sneqd	$⊢ (R \in Ring \land c \in {Base}_{R}) \to \{⟨⟨e, e⟩, c \cdot_{R} 1_{R}⟩\} = \{⟨⟨e, e⟩, c⟩\}$
28	15 23 27	3eqtrrd	$⊢ (R \in Ring \land c \in {Base}_{R}) \to \{⟨⟨e, e⟩, c⟩\} = c \cdot_{(\{e\} Mat R)} 1_{(\{e\} Mat R)}$
29	28	adantr	$⊢ ((R \in Ring \land c \in {Base}_{R}) \land M = \{⟨⟨e, e⟩, c⟩\}) \to \{⟨⟨e, e⟩, c⟩\} = c \cdot_{(\{e\} Mat R)} 1_{(\{e\} Mat R)}$
30	10 29	eqtrd	$⊢ ((R \in Ring \land c \in {Base}_{R}) \land M = \{⟨⟨e, e⟩, c⟩\}) \to M = c \cdot_{(\{e\} Mat R)} 1_{(\{e\} Mat R)}$
31	30	ex	$⊢ (R \in Ring \land c \in {Base}_{R}) \to (M = \{⟨⟨e, e⟩, c⟩\} \to M = c \cdot_{(\{e\} Mat R)} 1_{(\{e\} Mat R)})$
32	31	reximdva	$⊢ R \in Ring \to (\exists c \in {Base}_{R} M = \{⟨⟨e, e⟩, c⟩\} \to \exists c \in {Base}_{R} M = c \cdot_{(\{e\} Mat R)} 1_{(\{e\} Mat R)})$
33	9 32	sylbid	$⊢ R \in Ring \to (M \in {Base}_{(\{e\} Mat R)} \to \exists c \in {Base}_{R} M = c \cdot_{(\{e\} Mat R)} 1_{(\{e\} Mat R)})$
34	33	imp	$⊢ (R \in Ring \land M \in {Base}_{(\{e\} Mat R)}) \to \exists c \in {Base}_{R} M = c \cdot_{(\{e\} Mat R)} 1_{(\{e\} Mat R)}$
35		snfi	$⊢ \{e\} \in Fin$
36		simpl	$⊢ (R \in Ring \land M \in {Base}_{(\{e\} Mat R)}) \to R \in Ring$
37		eqid	$⊢ {Base}_{(\{e\} Mat R)} = {Base}_{(\{e\} Mat R)}$
38		eqid	$⊢ 1_{(\{e\} Mat R)} = 1_{(\{e\} Mat R)}$
39		eqid	$⊢ \cdot_{(\{e\} Mat R)} = \cdot_{(\{e\} Mat R)}$
40		eqid	$⊢ \{e\} ScMat R = \{e\} ScMat R$
41	6 5 37 38 39 40	scmatel	$⊢ (\{e\} \in Fin \land R \in Ring) \to (M \in (\{e\} ScMat R) \leftrightarrow (M \in {Base}_{(\{e\} Mat R)} \land \exists c \in {Base}_{R} M = c \cdot_{(\{e\} Mat R)} 1_{(\{e\} Mat R)}))$
42	35 36 41	sylancr	$⊢ (R \in Ring \land M \in {Base}_{(\{e\} Mat R)}) \to (M \in (\{e\} ScMat R) \leftrightarrow (M \in {Base}_{(\{e\} Mat R)} \land \exists c \in {Base}_{R} M = c \cdot_{(\{e\} Mat R)} 1_{(\{e\} Mat R)}))$
43	4 34 42	mpbir2and	$⊢ (R \in Ring \land M \in {Base}_{(\{e\} Mat R)}) \to M \in (\{e\} ScMat R)$
44	43	ex	$⊢ R \in Ring \to (M \in {Base}_{(\{e\} Mat R)} \to M \in (\{e\} ScMat R))$
45	1	fveq2i	$⊢ {Base}_{A} = {Base}_{(N Mat R)}$
46	2 45	eqtri	$⊢ B = {Base}_{(N Mat R)}$
47		fvoveq1	$⊢ N = \{e\} \to {Base}_{(N Mat R)} = {Base}_{(\{e\} Mat R)}$
48	46 47	eqtrid	$⊢ N = \{e\} \to B = {Base}_{(\{e\} Mat R)}$
49	48	eleq2d	$⊢ N = \{e\} \to (M \in B \leftrightarrow M \in {Base}_{(\{e\} Mat R)})$
50		oveq1	$⊢ N = \{e\} \to N ScMat R = \{e\} ScMat R$
51	50	eleq2d	$⊢ N = \{e\} \to (M \in (N ScMat R) \leftrightarrow M \in (\{e\} ScMat R))$
52	49 51	imbi12d	$⊢ N = \{e\} \to ((M \in B \to M \in (N ScMat R)) \leftrightarrow (M \in {Base}_{(\{e\} Mat R)} \to M \in (\{e\} ScMat R)))$
53	44 52	imbitrrid	$⊢ N = \{e\} \to (R \in Ring \to (M \in B \to M \in (N ScMat R)))$
54	53	exlimiv	$⊢ \exists e N = \{e\} \to (R \in Ring \to (M \in B \to M \in (N ScMat R)))$
55	3 54	syl6bi	$⊢ N \in V \to (\|N\| = 1 \to (R \in Ring \to (M \in B \to M \in (N ScMat R))))$
56	55	3imp	$⊢ (N \in V \land \|N\| = 1 \land R \in Ring) \to (M \in B \to M \in (N ScMat R))$

Metamath Proof Explorer

Theorem mat1scmat

Proof