mat1dimcrng

Description: The algebra of matrices with dimension 1 over a commutative ring is a commutative ring. (Contributed by AV, 16-Aug-2019)

	Ref	Expression
Hypotheses	mat1dim.a	$⊢ A = \{E\} Mat R$
	mat1dim.b	$⊢ B = {Base}_{R}$
	mat1dim.o	$⊢ O = ⟨E, E⟩$
Assertion	mat1dimcrng	$⊢ (R \in CRing \land E \in V) \to A \in CRing$

Proof

Step	Hyp	Ref	Expression
1		mat1dim.a	$⊢ A = \{E\} Mat R$
2		mat1dim.b	$⊢ B = {Base}_{R}$
3		mat1dim.o	$⊢ O = ⟨E, E⟩$
4		snfi	$⊢ \{E\} \in Fin$
5		crngring	$⊢ R \in CRing \to R \in Ring$
6	5	adantr	$⊢ (R \in CRing \land E \in V) \to R \in Ring$
7	1	matring	$⊢ (\{E\} \in Fin \land R \in Ring) \to A \in Ring$
8	4 6 7	sylancr	$⊢ (R \in CRing \land E \in V) \to A \in Ring$
9	1 2 3	mat1dimelbas	$⊢ (R \in Ring \land E \in V) \to (x \in {Base}_{A} \leftrightarrow \exists a \in B x = \{⟨O, a⟩\})$
10	1 2 3	mat1dimelbas	$⊢ (R \in Ring \land E \in V) \to (y \in {Base}_{A} \leftrightarrow \exists b \in B y = \{⟨O, b⟩\})$
11	9 10	anbi12d	$⊢ (R \in Ring \land E \in V) \to ((x \in {Base}_{A} \land y \in {Base}_{A}) \leftrightarrow (\exists a \in B x = \{⟨O, a⟩\} \land \exists b \in B y = \{⟨O, b⟩\}))$
12	5 11	sylan	$⊢ (R \in CRing \land E \in V) \to ((x \in {Base}_{A} \land y \in {Base}_{A}) \leftrightarrow (\exists a \in B x = \{⟨O, a⟩\} \land \exists b \in B y = \{⟨O, b⟩\}))$
13		simpll	$⊢ ((R \in CRing \land E \in V) \land (a \in B \land b \in B)) \to R \in CRing$
14		simprl	$⊢ ((R \in CRing \land E \in V) \land (a \in B \land b \in B)) \to a \in B$
15		simprr	$⊢ ((R \in CRing \land E \in V) \land (a \in B \land b \in B)) \to b \in B$
16		eqid	$⊢ \cdot_{R} = \cdot_{R}$
17	2 16	crngcom	$⊢ (R \in CRing \land a \in B \land b \in B) \to a \cdot_{R} b = b \cdot_{R} a$
18	13 14 15 17	syl3anc	$⊢ ((R \in CRing \land E \in V) \land (a \in B \land b \in B)) \to a \cdot_{R} b = b \cdot_{R} a$
19	18	opeq2d	$⊢ ((R \in CRing \land E \in V) \land (a \in B \land b \in B)) \to ⟨O, a \cdot_{R} b⟩ = ⟨O, b \cdot_{R} a⟩$
20	19	sneqd	$⊢ ((R \in CRing \land E \in V) \land (a \in B \land b \in B)) \to \{⟨O, a \cdot_{R} b⟩\} = \{⟨O, b \cdot_{R} a⟩\}$
21	5	anim1i	$⊢ (R \in CRing \land E \in V) \to (R \in Ring \land E \in V)$
22	1 2 3	mat1dimmul	$⊢ ((R \in Ring \land E \in V) \land (a \in B \land b \in B)) \to \{⟨O, a⟩\} \cdot_{A} \{⟨O, b⟩\} = \{⟨O, a \cdot_{R} b⟩\}$
23	21 22	sylan	$⊢ ((R \in CRing \land E \in V) \land (a \in B \land b \in B)) \to \{⟨O, a⟩\} \cdot_{A} \{⟨O, b⟩\} = \{⟨O, a \cdot_{R} b⟩\}$
24		pm3.22	$⊢ (a \in B \land b \in B) \to (b \in B \land a \in B)$
25	1 2 3	mat1dimmul	$⊢ ((R \in Ring \land E \in V) \land (b \in B \land a \in B)) \to \{⟨O, b⟩\} \cdot_{A} \{⟨O, a⟩\} = \{⟨O, b \cdot_{R} a⟩\}$
26	21 24 25	syl2an	$⊢ ((R \in CRing \land E \in V) \land (a \in B \land b \in B)) \to \{⟨O, b⟩\} \cdot_{A} \{⟨O, a⟩\} = \{⟨O, b \cdot_{R} a⟩\}$
27	20 23 26	3eqtr4d	$⊢ ((R \in CRing \land E \in V) \land (a \in B \land b \in B)) \to \{⟨O, a⟩\} \cdot_{A} \{⟨O, b⟩\} = \{⟨O, b⟩\} \cdot_{A} \{⟨O, a⟩\}$
28	27	expr	$⊢ ((R \in CRing \land E \in V) \land a \in B) \to (b \in B \to \{⟨O, a⟩\} \cdot_{A} \{⟨O, b⟩\} = \{⟨O, b⟩\} \cdot_{A} \{⟨O, a⟩\})$
29	28	adantr	$⊢ (((R \in CRing \land E \in V) \land a \in B) \land x = \{⟨O, a⟩\}) \to (b \in B \to \{⟨O, a⟩\} \cdot_{A} \{⟨O, b⟩\} = \{⟨O, b⟩\} \cdot_{A} \{⟨O, a⟩\})$
30	29	imp	$⊢ ((((R \in CRing \land E \in V) \land a \in B) \land x = \{⟨O, a⟩\}) \land b \in B) \to \{⟨O, a⟩\} \cdot_{A} \{⟨O, b⟩\} = \{⟨O, b⟩\} \cdot_{A} \{⟨O, a⟩\}$
31	30	adantr	$⊢ (((((R \in CRing \land E \in V) \land a \in B) \land x = \{⟨O, a⟩\}) \land b \in B) \land y = \{⟨O, b⟩\}) \to \{⟨O, a⟩\} \cdot_{A} \{⟨O, b⟩\} = \{⟨O, b⟩\} \cdot_{A} \{⟨O, a⟩\}$
32		oveq12	$⊢ (x = \{⟨O, a⟩\} \land y = \{⟨O, b⟩\}) \to x \cdot_{A} y = \{⟨O, a⟩\} \cdot_{A} \{⟨O, b⟩\}$
33	32	ad4ant24	$⊢ (((((R \in CRing \land E \in V) \land a \in B) \land x = \{⟨O, a⟩\}) \land b \in B) \land y = \{⟨O, b⟩\}) \to x \cdot_{A} y = \{⟨O, a⟩\} \cdot_{A} \{⟨O, b⟩\}$
34		oveq12	$⊢ (y = \{⟨O, b⟩\} \land x = \{⟨O, a⟩\}) \to y \cdot_{A} x = \{⟨O, b⟩\} \cdot_{A} \{⟨O, a⟩\}$
35	34	expcom	$⊢ x = \{⟨O, a⟩\} \to (y = \{⟨O, b⟩\} \to y \cdot_{A} x = \{⟨O, b⟩\} \cdot_{A} \{⟨O, a⟩\})$
36	35	ad2antlr	$⊢ ((((R \in CRing \land E \in V) \land a \in B) \land x = \{⟨O, a⟩\}) \land b \in B) \to (y = \{⟨O, b⟩\} \to y \cdot_{A} x = \{⟨O, b⟩\} \cdot_{A} \{⟨O, a⟩\})$
37	36	imp	$⊢ (((((R \in CRing \land E \in V) \land a \in B) \land x = \{⟨O, a⟩\}) \land b \in B) \land y = \{⟨O, b⟩\}) \to y \cdot_{A} x = \{⟨O, b⟩\} \cdot_{A} \{⟨O, a⟩\}$
38	31 33 37	3eqtr4d	$⊢ (((((R \in CRing \land E \in V) \land a \in B) \land x = \{⟨O, a⟩\}) \land b \in B) \land y = \{⟨O, b⟩\}) \to x \cdot_{A} y = y \cdot_{A} x$
39	38	rexlimdva2	$⊢ (((R \in CRing \land E \in V) \land a \in B) \land x = \{⟨O, a⟩\}) \to (\exists b \in B y = \{⟨O, b⟩\} \to x \cdot_{A} y = y \cdot_{A} x)$
40	39	rexlimdva2	$⊢ (R \in CRing \land E \in V) \to (\exists a \in B x = \{⟨O, a⟩\} \to (\exists b \in B y = \{⟨O, b⟩\} \to x \cdot_{A} y = y \cdot_{A} x))$
41	40	impd	$⊢ (R \in CRing \land E \in V) \to ((\exists a \in B x = \{⟨O, a⟩\} \land \exists b \in B y = \{⟨O, b⟩\}) \to x \cdot_{A} y = y \cdot_{A} x)$
42	12 41	sylbid	$⊢ (R \in CRing \land E \in V) \to ((x \in {Base}_{A} \land y \in {Base}_{A}) \to x \cdot_{A} y = y \cdot_{A} x)$
43	42	ralrimivv	$⊢ (R \in CRing \land E \in V) \to \forall x \in {Base}_{A} \forall y \in {Base}_{A} x \cdot_{A} y = y \cdot_{A} x$
44		eqid	$⊢ {Base}_{A} = {Base}_{A}$
45		eqid	$⊢ \cdot_{A} = \cdot_{A}$
46	44 45	iscrng2	$⊢ A \in CRing \leftrightarrow (A \in Ring \land \forall x \in {Base}_{A} \forall y \in {Base}_{A} x \cdot_{A} y = y \cdot_{A} x)$
47	8 43 46	sylanbrc	$⊢ (R \in CRing \land E \in V) \to A \in CRing$

Metamath Proof Explorer

Theorem mat1dimcrng

Proof