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		simpr	$⊢ (N \in Fin \land R \in CRing) \to R \in CRing$
15	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$
16		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$
17		eqid	$⊢ \cdot_{R} = \cdot_{R}$
18		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}$
19		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)})$
20		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)})$
21	2 15 7 16 16 16 17 18 19 20	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)$
22	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}$
23	19 22	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}$
24		eqid	$⊢ {Base}_{A} = {Base}_{A}$
25		eqid	$⊢ \cdot_{A} = \cdot_{A}$
26		eqid	$⊢ N \times N = N \times N$
27	1 24 2 25 17 26	matvsca2	$⊢ (x \in {Base}_{R} \land y \in {Base}_{A}) \to x \cdot_{A} y = ((N \times N) \times \{x\}) {\cdot_{R}}_{f} y$
28	18 23 27	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$
29	28	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$
30	2 15 7 16 16 16 19 20	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)})$
31	30 22	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}$
32	1 24 2 25 17 26	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)$
33	18 31 32	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)$
34	21 29 33	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)$
35		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$
36	35 2 17 7 16 16 16 19 18 20	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)$
37	20 22	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}$
38	1 24 2 25 17 26	matvsca2	$⊢ (x \in {Base}_{R} \land z \in {Base}_{A}) \to x \cdot_{A} z = ((N \times N) \times \{x\}) {\cdot_{R}}_{f} z$
39	18 37 38	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$
40	39	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)$
41	36 40 33	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)$
42	3 4 5 6 8 11 13 14 34 41	isassad	$⊢ (N \in Fin \land R \in CRing) \to A \in AssAlg$

Metamath Proof Explorer

Theorem matassa

Proof