matassa

Description: Existence of the matrix algebra, see also the statement in Lang p. 505: "Then Mat_n(R) is an algebra over R" . (Contributed by Stefan O'Rear, 5-Sep-2015)

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

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 CRing) \to {Base}_{R}^{(N \times N)} = {Base}_{A}$
4	1	matsca2	$⊢ (N \in Fin \land R \in CRing) \to R = Scalar (A)$
5		eqidd	$⊢ (N \in Fin \land R \in CRing) \to {Base}_{R} = {Base}_{R}$
6		eqidd	$⊢ (N \in Fin \land R \in CRing) \to \cdot_{A} = \cdot_{A}$
7		eqid	$⊢ R maMul ⟨N, N, N⟩ = R maMul ⟨N, N, N⟩$
8	1 7	matmulr	$⊢ (N \in Fin \land R \in CRing) \to R maMul ⟨N, N, N⟩ = \cdot_{A}$
9		crngring	$⊢ R \in CRing \to R \in Ring$
10	1	matlmod	$⊢ (N \in Fin \land R \in Ring) \to A \in LMod$
11	9 10	sylan2	$⊢ (N \in Fin \land R \in CRing) \to A \in LMod$
12	1	matring	$⊢ (N \in Fin \land R \in Ring) \to A \in Ring$
13	9 12	sylan2	$⊢ (N \in Fin \land R \in CRing) \to A \in Ring$
14	9	ad2antlr	$⊢ ((N \in Fin \land R \in CRing) \land (x \in {Base}_{R} \land y \in ({Base}_{R}^{(N \times N)}) \land z \in ({Base}_{R}^{(N \times N)}))) \to R \in Ring$
15		simpll	$⊢ ((N \in Fin \land R \in CRing) \land (x \in {Base}_{R} \land y \in ({Base}_{R}^{(N \times N)}) \land z \in ({Base}_{R}^{(N \times N)}))) \to N \in Fin$
16		eqid	$⊢ \cdot_{R} = \cdot_{R}$
17		simpr1	$⊢ ((N \in Fin \land R \in CRing) \land (x \in {Base}_{R} \land y \in ({Base}_{R}^{(N \times N)}) \land z \in ({Base}_{R}^{(N \times N)}))) \to x \in {Base}_{R}$
18		simpr2	$⊢ ((N \in Fin \land R \in CRing) \land (x \in {Base}_{R} \land y \in ({Base}_{R}^{(N \times N)}) \land z \in ({Base}_{R}^{(N \times N)}))) \to y \in ({Base}_{R}^{(N \times N)})$
19		simpr3	$⊢ ((N \in Fin \land R \in CRing) \land (x \in {Base}_{R} \land y \in ({Base}_{R}^{(N \times N)}) \land z \in ({Base}_{R}^{(N \times N)}))) \to z \in ({Base}_{R}^{(N \times N)})$
20	2 14 7 15 15 15 16 17 18 19	mamuvs1	$⊢ ((N \in Fin \land R \in CRing) \land (x \in {Base}_{R} \land y \in ({Base}_{R}^{(N \times N)}) \land z \in ({Base}_{R}^{(N \times N)}))) \to (((N \times N) \times \{x\}) {\cdot_{R}}_{f} y) (R maMul ⟨N, N, N⟩) z = ((N \times N) \times \{x\}) {\cdot_{R}}_{f} (y (R maMul ⟨N, N, N⟩) z)$
21	3	adantr	$⊢ ((N \in Fin \land R \in CRing) \land (x \in {Base}_{R} \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	18 21	eleqtrd	$⊢ ((N \in Fin \land R \in CRing) \land (x \in {Base}_{R} \land y \in ({Base}_{R}^{(N \times N)}) \land z \in ({Base}_{R}^{(N \times N)}))) \to y \in {Base}_{A}$
23		eqid	$⊢ {Base}_{A} = {Base}_{A}$
24		eqid	$⊢ \cdot_{A} = \cdot_{A}$
25		eqid	$⊢ N \times N = N \times N$
26	1 23 2 24 16 25	matvsca2	$⊢ (x \in {Base}_{R} \land y \in {Base}_{A}) \to x \cdot_{A} y = ((N \times N) \times \{x\}) {\cdot_{R}}_{f} y$
27	17 22 26	syl2anc	$⊢ ((N \in Fin \land R \in CRing) \land (x \in {Base}_{R} \land y \in ({Base}_{R}^{(N \times N)}) \land z \in ({Base}_{R}^{(N \times N)}))) \to x \cdot_{A} y = ((N \times N) \times \{x\}) {\cdot_{R}}_{f} y$
28	27	oveq1d	$⊢ ((N \in Fin \land R \in CRing) \land (x \in {Base}_{R} \land y \in ({Base}_{R}^{(N \times N)}) \land z \in ({Base}_{R}^{(N \times N)}))) \to (x \cdot_{A} y) (R maMul ⟨N, N, N⟩) z = (((N \times N) \times \{x\}) {\cdot_{R}}_{f} y) (R maMul ⟨N, N, N⟩) z$
29	2 14 7 15 15 15 18 19	mamucl	$⊢ ((N \in Fin \land R \in CRing) \land (x \in {Base}_{R} \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)})$
30	29 21	eleqtrd	$⊢ ((N \in Fin \land R \in CRing) \land (x \in {Base}_{R} \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}$
31	1 23 2 24 16 25	matvsca2	$⊢ (x \in {Base}_{R} \land y (R maMul ⟨N, N, N⟩) z \in {Base}_{A}) \to x \cdot_{A} (y (R maMul ⟨N, N, N⟩) z) = ((N \times N) \times \{x\}) {\cdot_{R}}_{f} (y (R maMul ⟨N, N, N⟩) z)$
32	17 30 31	syl2anc	$⊢ ((N \in Fin \land R \in CRing) \land (x \in {Base}_{R} \land y \in ({Base}_{R}^{(N \times N)}) \land z \in ({Base}_{R}^{(N \times N)}))) \to x \cdot_{A} (y (R maMul ⟨N, N, N⟩) z) = ((N \times N) \times \{x\}) {\cdot_{R}}_{f} (y (R maMul ⟨N, N, N⟩) z)$
33	20 28 32	3eqtr4d	$⊢ ((N \in Fin \land R \in CRing) \land (x \in {Base}_{R} \land y \in ({Base}_{R}^{(N \times N)}) \land z \in ({Base}_{R}^{(N \times N)}))) \to (x \cdot_{A} y) (R maMul ⟨N, N, N⟩) z = x \cdot_{A} (y (R maMul ⟨N, N, N⟩) z)$
34		simplr	$⊢ ((N \in Fin \land R \in CRing) \land (x \in {Base}_{R} \land y \in ({Base}_{R}^{(N \times N)}) \land z \in ({Base}_{R}^{(N \times N)}))) \to R \in CRing$
35	34 2 16 7 15 15 15 18 17 19	mamuvs2	$⊢ ((N \in Fin \land R \in CRing) \land (x \in {Base}_{R} \land y \in ({Base}_{R}^{(N \times N)}) \land z \in ({Base}_{R}^{(N \times N)}))) \to y (R maMul ⟨N, N, N⟩) (((N \times N) \times \{x\}) {\cdot_{R}}_{f} z) = ((N \times N) \times \{x\}) {\cdot_{R}}_{f} (y (R maMul ⟨N, N, N⟩) z)$
36	19 21	eleqtrd	$⊢ ((N \in Fin \land R \in CRing) \land (x \in {Base}_{R} \land y \in ({Base}_{R}^{(N \times N)}) \land z \in ({Base}_{R}^{(N \times N)}))) \to z \in {Base}_{A}$
37	1 23 2 24 16 25	matvsca2	$⊢ (x \in {Base}_{R} \land z \in {Base}_{A}) \to x \cdot_{A} z = ((N \times N) \times \{x\}) {\cdot_{R}}_{f} z$
38	17 36 37	syl2anc	$⊢ ((N \in Fin \land R \in CRing) \land (x \in {Base}_{R} \land y \in ({Base}_{R}^{(N \times N)}) \land z \in ({Base}_{R}^{(N \times N)}))) \to x \cdot_{A} z = ((N \times N) \times \{x\}) {\cdot_{R}}_{f} z$
39	38	oveq2d	$⊢ ((N \in Fin \land R \in CRing) \land (x \in {Base}_{R} \land y \in ({Base}_{R}^{(N \times N)}) \land z \in ({Base}_{R}^{(N \times N)}))) \to y (R maMul ⟨N, N, N⟩) (x \cdot_{A} z) = y (R maMul ⟨N, N, N⟩) (((N \times N) \times \{x\}) {\cdot_{R}}_{f} z)$
40	35 39 32	3eqtr4d	$⊢ ((N \in Fin \land R \in CRing) \land (x \in {Base}_{R} \land y \in ({Base}_{R}^{(N \times N)}) \land z \in ({Base}_{R}^{(N \times N)}))) \to y (R maMul ⟨N, N, N⟩) (x \cdot_{A} z) = x \cdot_{A} (y (R maMul ⟨N, N, N⟩) z)$
41	3 4 5 6 8 11 13 33 40	isassad	$⊢ (N \in Fin \land R \in CRing) \to A \in AssAlg$

Metamath Proof Explorer

Theorem matassa

Proof