matring

Description: Existence of the matrix ring, see also the statement in Lang p. 504: "For a given integer n > 0 the set of square n x n matrices form a ring." (Contributed by Stefan O'Rear, 5-Sep-2015)

		Ref	Expression
	Hypothesis	matassa.a	$⊢ A = N Mat R$
	Assertion	matring	$⊢ (N \in Fin \land R \in Ring) \to A \in Ring$

Proof

Step	Hyp	Ref	Expression
1		matassa.a	$⊢ A = N Mat R$
2		eqid	$⊢ {Base}_{R} = {Base}_{R}$
3	1 2	matbas2	$⊢ (N \in Fin \land R \in Ring) \to {Base}_{R}^{(N \times N)} = {Base}_{A}$
4		eqidd	$⊢ (N \in Fin \land R \in Ring) \to +_{A} = +_{A}$
5		eqid	$⊢ R maMul ⟨N, N, N⟩ = R maMul ⟨N, N, N⟩$
6	1 5	matmulr	$⊢ (N \in Fin \land R \in Ring) \to R maMul ⟨N, N, N⟩ = \cdot_{A}$
7	1	matgrp	$⊢ (N \in Fin \land R \in Ring) \to A \in Grp$
8		simp1r	$⊢ ((N \in Fin \land R \in Ring) \land x \in ({Base}_{R}^{(N \times N)}) \land y \in ({Base}_{R}^{(N \times N)})) \to R \in Ring$
9		simp1l	$⊢ ((N \in Fin \land R \in Ring) \land x \in ({Base}_{R}^{(N \times N)}) \land y \in ({Base}_{R}^{(N \times N)})) \to N \in Fin$
10		simp2	$⊢ ((N \in Fin \land R \in Ring) \land x \in ({Base}_{R}^{(N \times N)}) \land y \in ({Base}_{R}^{(N \times N)})) \to x \in ({Base}_{R}^{(N \times N)})$
11		simp3	$⊢ ((N \in Fin \land R \in Ring) \land x \in ({Base}_{R}^{(N \times N)}) \land y \in ({Base}_{R}^{(N \times N)})) \to y \in ({Base}_{R}^{(N \times N)})$
12	2 8 5 9 9 9 10 11	mamucl	$⊢ ((N \in Fin \land R \in Ring) \land x \in ({Base}_{R}^{(N \times N)}) \land y \in ({Base}_{R}^{(N \times N)})) \to x (R maMul ⟨N, N, N⟩) y \in ({Base}_{R}^{(N \times N)})$
13		simplr	$⊢ ((N \in Fin \land R \in Ring) \land (x \in ({Base}_{R}^{(N \times N)}) \land y \in ({Base}_{R}^{(N \times N)}) \land z \in ({Base}_{R}^{(N \times N)}))) \to R \in Ring$
14		simpll	$⊢ ((N \in Fin \land R \in Ring) \land (x \in ({Base}_{R}^{(N \times N)}) \land y \in ({Base}_{R}^{(N \times N)}) \land z \in ({Base}_{R}^{(N \times N)}))) \to N \in Fin$
15		simpr1	$⊢ ((N \in Fin \land R \in Ring) \land (x \in ({Base}_{R}^{(N \times N)}) \land y \in ({Base}_{R}^{(N \times N)}) \land z \in ({Base}_{R}^{(N \times N)}))) \to x \in ({Base}_{R}^{(N \times N)})$
16		simpr2	$⊢ ((N \in Fin \land R \in Ring) \land (x \in ({Base}_{R}^{(N \times N)}) \land y \in ({Base}_{R}^{(N \times N)}) \land z \in ({Base}_{R}^{(N \times N)}))) \to y \in ({Base}_{R}^{(N \times N)})$
17		simpr3	$⊢ ((N \in Fin \land R \in Ring) \land (x \in ({Base}_{R}^{(N \times N)}) \land y \in ({Base}_{R}^{(N \times N)}) \land z \in ({Base}_{R}^{(N \times N)}))) \to z \in ({Base}_{R}^{(N \times N)})$
18	2 13 14 14 14 14 15 16 17 5 5 5 5	mamuass	$⊢ ((N \in Fin \land R \in Ring) \land (x \in ({Base}_{R}^{(N \times N)}) \land y \in ({Base}_{R}^{(N \times N)}) \land z \in ({Base}_{R}^{(N \times N)}))) \to (x (R maMul ⟨N, N, N⟩) y) (R maMul ⟨N, N, N⟩) z = x (R maMul ⟨N, N, N⟩) (y (R maMul ⟨N, N, N⟩) z)$
19		eqid	$⊢ +_{R} = +_{R}$
20	2 13 5 14 14 14 19 15 16 17	mamudir	$⊢ ((N \in Fin \land R \in Ring) \land (x \in ({Base}_{R}^{(N \times N)}) \land y \in ({Base}_{R}^{(N \times N)}) \land z \in ({Base}_{R}^{(N \times N)}))) \to x (R maMul ⟨N, N, N⟩) (y {+_{R}}_{f} z) = (x (R maMul ⟨N, N, N⟩) y) {+_{R}}_{f} (x (R maMul ⟨N, N, N⟩) z)$
21	3	adantr	$⊢ ((N \in Fin \land R \in Ring) \land (x \in ({Base}_{R}^{(N \times N)}) \land y \in ({Base}_{R}^{(N \times N)}) \land z \in ({Base}_{R}^{(N \times N)}))) \to {Base}_{R}^{(N \times N)} = {Base}_{A}$
22	16 21	eleqtrd	$⊢ ((N \in Fin \land R \in Ring) \land (x \in ({Base}_{R}^{(N \times N)}) \land y \in ({Base}_{R}^{(N \times N)}) \land z \in ({Base}_{R}^{(N \times N)}))) \to y \in {Base}_{A}$
23	17 21	eleqtrd	$⊢ ((N \in Fin \land R \in Ring) \land (x \in ({Base}_{R}^{(N \times N)}) \land y \in ({Base}_{R}^{(N \times N)}) \land z \in ({Base}_{R}^{(N \times N)}))) \to z \in {Base}_{A}$
24		eqid	$⊢ {Base}_{A} = {Base}_{A}$
25		eqid	$⊢ +_{A} = +_{A}$
26	1 24 25 19	matplusg2	$⊢ (y \in {Base}_{A} \land z \in {Base}_{A}) \to y +_{A} z = y {+_{R}}_{f} z$
27	22 23 26	syl2anc	$⊢ ((N \in Fin \land R \in Ring) \land (x \in ({Base}_{R}^{(N \times N)}) \land y \in ({Base}_{R}^{(N \times N)}) \land z \in ({Base}_{R}^{(N \times N)}))) \to y +_{A} z = y {+_{R}}_{f} z$
28	27	oveq2d	$⊢ ((N \in Fin \land R \in Ring) \land (x \in ({Base}_{R}^{(N \times N)}) \land y \in ({Base}_{R}^{(N \times N)}) \land z \in ({Base}_{R}^{(N \times N)}))) \to x (R maMul ⟨N, N, N⟩) (y +_{A} z) = x (R maMul ⟨N, N, N⟩) (y {+_{R}}_{f} z)$
29	2 13 5 14 14 14 15 16	mamucl	$⊢ ((N \in Fin \land R \in Ring) \land (x \in ({Base}_{R}^{(N \times N)}) \land y \in ({Base}_{R}^{(N \times N)}) \land z \in ({Base}_{R}^{(N \times N)}))) \to x (R maMul ⟨N, N, N⟩) y \in ({Base}_{R}^{(N \times N)})$
30	29 21	eleqtrd	$⊢ ((N \in Fin \land R \in Ring) \land (x \in ({Base}_{R}^{(N \times N)}) \land y \in ({Base}_{R}^{(N \times N)}) \land z \in ({Base}_{R}^{(N \times N)}))) \to x (R maMul ⟨N, N, N⟩) y \in {Base}_{A}$
31	2 13 5 14 14 14 15 17	mamucl	$⊢ ((N \in Fin \land R \in Ring) \land (x \in ({Base}_{R}^{(N \times N)}) \land y \in ({Base}_{R}^{(N \times N)}) \land z \in ({Base}_{R}^{(N \times N)}))) \to x (R maMul ⟨N, N, N⟩) z \in ({Base}_{R}^{(N \times N)})$
32	31 21	eleqtrd	$⊢ ((N \in Fin \land R \in Ring) \land (x \in ({Base}_{R}^{(N \times N)}) \land y \in ({Base}_{R}^{(N \times N)}) \land z \in ({Base}_{R}^{(N \times N)}))) \to x (R maMul ⟨N, N, N⟩) z \in {Base}_{A}$
33	1 24 25 19	matplusg2	$⊢ (x (R maMul ⟨N, N, N⟩) y \in {Base}_{A} \land x (R maMul ⟨N, N, N⟩) z \in {Base}_{A}) \to (x (R maMul ⟨N, N, N⟩) y) +_{A} (x (R maMul ⟨N, N, N⟩) z) = (x (R maMul ⟨N, N, N⟩) y) {+_{R}}_{f} (x (R maMul ⟨N, N, N⟩) z)$
34	30 32 33	syl2anc	$⊢ ((N \in Fin \land R \in Ring) \land (x \in ({Base}_{R}^{(N \times N)}) \land y \in ({Base}_{R}^{(N \times N)}) \land z \in ({Base}_{R}^{(N \times N)}))) \to (x (R maMul ⟨N, N, N⟩) y) +_{A} (x (R maMul ⟨N, N, N⟩) z) = (x (R maMul ⟨N, N, N⟩) y) {+_{R}}_{f} (x (R maMul ⟨N, N, N⟩) z)$
35	20 28 34	3eqtr4d	$⊢ ((N \in Fin \land R \in Ring) \land (x \in ({Base}_{R}^{(N \times N)}) \land y \in ({Base}_{R}^{(N \times N)}) \land z \in ({Base}_{R}^{(N \times N)}))) \to x (R maMul ⟨N, N, N⟩) (y +_{A} z) = (x (R maMul ⟨N, N, N⟩) y) +_{A} (x (R maMul ⟨N, N, N⟩) z)$
36	2 13 5 14 14 14 19 15 16 17	mamudi	$⊢ ((N \in Fin \land R \in Ring) \land (x \in ({Base}_{R}^{(N \times N)}) \land y \in ({Base}_{R}^{(N \times N)}) \land z \in ({Base}_{R}^{(N \times N)}))) \to (x {+_{R}}_{f} y) (R maMul ⟨N, N, N⟩) z = (x (R maMul ⟨N, N, N⟩) z) {+_{R}}_{f} (y (R maMul ⟨N, N, N⟩) z)$
37	15 21	eleqtrd	$⊢ ((N \in Fin \land R \in Ring) \land (x \in ({Base}_{R}^{(N \times N)}) \land y \in ({Base}_{R}^{(N \times N)}) \land z \in ({Base}_{R}^{(N \times N)}))) \to x \in {Base}_{A}$
38	1 24 25 19	matplusg2	$⊢ (x \in {Base}_{A} \land y \in {Base}_{A}) \to x +_{A} y = x {+_{R}}_{f} y$
39	37 22 38	syl2anc	$⊢ ((N \in Fin \land R \in Ring) \land (x \in ({Base}_{R}^{(N \times N)}) \land y \in ({Base}_{R}^{(N \times N)}) \land z \in ({Base}_{R}^{(N \times N)}))) \to x +_{A} y = x {+_{R}}_{f} y$
40	39	oveq1d	$⊢ ((N \in Fin \land R \in Ring) \land (x \in ({Base}_{R}^{(N \times N)}) \land y \in ({Base}_{R}^{(N \times N)}) \land z \in ({Base}_{R}^{(N \times N)}))) \to (x +_{A} y) (R maMul ⟨N, N, N⟩) z = (x {+_{R}}_{f} y) (R maMul ⟨N, N, N⟩) z$
41	2 13 5 14 14 14 16 17	mamucl	$⊢ ((N \in Fin \land R \in Ring) \land (x \in ({Base}_{R}^{(N \times N)}) \land y \in ({Base}_{R}^{(N \times N)}) \land z \in ({Base}_{R}^{(N \times N)}))) \to y (R maMul ⟨N, N, N⟩) z \in ({Base}_{R}^{(N \times N)})$
42	41 21	eleqtrd	$⊢ ((N \in Fin \land R \in Ring) \land (x \in ({Base}_{R}^{(N \times N)}) \land y \in ({Base}_{R}^{(N \times N)}) \land z \in ({Base}_{R}^{(N \times N)}))) \to y (R maMul ⟨N, N, N⟩) z \in {Base}_{A}$
43	1 24 25 19	matplusg2	$⊢ (x (R maMul ⟨N, N, N⟩) z \in {Base}_{A} \land y (R maMul ⟨N, N, N⟩) z \in {Base}_{A}) \to (x (R maMul ⟨N, N, N⟩) z) +_{A} (y (R maMul ⟨N, N, N⟩) z) = (x (R maMul ⟨N, N, N⟩) z) {+_{R}}_{f} (y (R maMul ⟨N, N, N⟩) z)$
44	32 42 43	syl2anc	$⊢ ((N \in Fin \land R \in Ring) \land (x \in ({Base}_{R}^{(N \times N)}) \land y \in ({Base}_{R}^{(N \times N)}) \land z \in ({Base}_{R}^{(N \times N)}))) \to (x (R maMul ⟨N, N, N⟩) z) +_{A} (y (R maMul ⟨N, N, N⟩) z) = (x (R maMul ⟨N, N, N⟩) z) {+_{R}}_{f} (y (R maMul ⟨N, N, N⟩) z)$
45	36 40 44	3eqtr4d	$⊢ ((N \in Fin \land R \in Ring) \land (x \in ({Base}_{R}^{(N \times N)}) \land y \in ({Base}_{R}^{(N \times N)}) \land z \in ({Base}_{R}^{(N \times N)}))) \to (x +_{A} y) (R maMul ⟨N, N, N⟩) z = (x (R maMul ⟨N, N, N⟩) z) +_{A} (y (R maMul ⟨N, N, N⟩) z)$
46		simpr	$⊢ (N \in Fin \land R \in Ring) \to R \in Ring$
47		eqid	$⊢ 1_{R} = 1_{R}$
48		eqid	$⊢ 0_{R} = 0_{R}$
49		eqid	$⊢ (a \in N, b \in N ⟼ if (a = b, 1_{R}, 0_{R})) = (a \in N, b \in N ⟼ if (a = b, 1_{R}, 0_{R}))$
50		simpl	$⊢ (N \in Fin \land R \in Ring) \to N \in Fin$
51	2 46 47 48 49 50	mamumat1cl	$⊢ (N \in Fin \land R \in Ring) \to (a \in N, b \in N ⟼ if (a = b, 1_{R}, 0_{R})) \in ({Base}_{R}^{(N \times N)})$
52		simplr	$⊢ ((N \in Fin \land R \in Ring) \land x \in ({Base}_{R}^{(N \times N)})) \to R \in Ring$
53		simpll	$⊢ ((N \in Fin \land R \in Ring) \land x \in ({Base}_{R}^{(N \times N)})) \to N \in Fin$
54		simpr	$⊢ ((N \in Fin \land R \in Ring) \land x \in ({Base}_{R}^{(N \times N)})) \to x \in ({Base}_{R}^{(N \times N)})$
55	2 52 47 48 49 53 53 5 54	mamulid	$⊢ ((N \in Fin \land R \in Ring) \land x \in ({Base}_{R}^{(N \times N)})) \to (a \in N, b \in N ⟼ if (a = b, 1_{R}, 0_{R})) (R maMul ⟨N, N, N⟩) x = x$
56	2 52 47 48 49 53 53 5 54	mamurid	$⊢ ((N \in Fin \land R \in Ring) \land x \in ({Base}_{R}^{(N \times N)})) \to x (R maMul ⟨N, N, N⟩) (a \in N, b \in N ⟼ if (a = b, 1_{R}, 0_{R})) = x$
57	3 4 6 7 12 18 35 45 51 55 56	isringd	$⊢ (N \in Fin \land R \in Ring) \to A \in Ring$

Metamath Proof Explorer

Theorem matring

Proof