matdim

Description: Dimension of the space of square matrices. (Contributed by Thierry Arnoux, 20-May-2023)

	Ref	Expression
Hypotheses	matdim.a	$⊢ A = I Mat R$
	matdim.n	$⊢ N = \|I\|$
Assertion	matdim	$⊢ (I \in Fin \land R \in DivRing) \to \dim (A) = N \cdot N$

Proof

Step	Hyp	Ref	Expression
1		matdim.a	$⊢ A = I Mat R$
2		matdim.n	$⊢ N = \|I\|$
3		simpr	$⊢ (I \in Fin \land R \in DivRing) \to R \in DivRing$
4		simpl	$⊢ (I \in Fin \land R \in DivRing) \to I \in Fin$
5		xpfi	$⊢ (I \in Fin \land I \in Fin) \to I \times I \in Fin$
6	4 4 5	syl2anc	$⊢ (I \in Fin \land R \in DivRing) \to I \times I \in Fin$
7		eqid	$⊢ R freeLMod (I \times I) = R freeLMod (I \times I)$
8	7	frlmdim	$⊢ (R \in DivRing \land I \times I \in Fin) \to \dim (R freeLMod (I \times I)) = \|I \times I\|$
9	3 6 8	syl2anc	$⊢ (I \in Fin \land R \in DivRing) \to \dim (R freeLMod (I \times I)) = \|I \times I\|$
10	1 7	matbas	$⊢ (I \in Fin \land R \in DivRing) \to {Base}_{(R freeLMod (I \times I))} = {Base}_{A}$
11	10	eqcomd	$⊢ (I \in Fin \land R \in DivRing) \to {Base}_{A} = {Base}_{(R freeLMod (I \times I))}$
12		eqidd	$⊢ (I \in Fin \land R \in DivRing) \to {Base}_{A} = {Base}_{A}$
13		ssidd	$⊢ (I \in Fin \land R \in DivRing) \to {Base}_{A} \subseteq {Base}_{A}$
14	1 7	matplusg	$⊢ (I \in Fin \land R \in DivRing) \to +_{(R freeLMod (I \times I))} = +_{A}$
15	14	oveqdr	$⊢ ((I \in Fin \land R \in DivRing) \land (x \in {Base}_{A} \land y \in {Base}_{A})) \to x +_{(R freeLMod (I \times I))} y = x +_{A} y$
16	7	frlmlvec	$⊢ (R \in DivRing \land I \times I \in Fin) \to R freeLMod (I \times I) \in LVec$
17	3 6 16	syl2anc	$⊢ (I \in Fin \land R \in DivRing) \to R freeLMod (I \times I) \in LVec$
18		lveclmod	$⊢ R freeLMod (I \times I) \in LVec \to R freeLMod (I \times I) \in LMod$
19	17 18	syl	$⊢ (I \in Fin \land R \in DivRing) \to R freeLMod (I \times I) \in LMod$
20	19	adantr	$⊢ ((I \in Fin \land R \in DivRing) \land (x \in {Base}_{Scalar (A)} \land y \in {Base}_{A})) \to R freeLMod (I \times I) \in LMod$
21		simprl	$⊢ ((I \in Fin \land R \in DivRing) \land (x \in {Base}_{Scalar (A)} \land y \in {Base}_{A})) \to x \in {Base}_{Scalar (A)}$
22	1 7	matsca	$⊢ (I \in Fin \land R \in DivRing) \to Scalar (R freeLMod (I \times I)) = Scalar (A)$
23	22	fveq2d	$⊢ (I \in Fin \land R \in DivRing) \to {Base}_{Scalar (R freeLMod (I \times I))} = {Base}_{Scalar (A)}$
24	23	eqcomd	$⊢ (I \in Fin \land R \in DivRing) \to {Base}_{Scalar (A)} = {Base}_{Scalar (R freeLMod (I \times I))}$
25	24	adantr	$⊢ ((I \in Fin \land R \in DivRing) \land (x \in {Base}_{Scalar (A)} \land y \in {Base}_{A})) \to {Base}_{Scalar (A)} = {Base}_{Scalar (R freeLMod (I \times I))}$
26	21 25	eleqtrd	$⊢ ((I \in Fin \land R \in DivRing) \land (x \in {Base}_{Scalar (A)} \land y \in {Base}_{A})) \to x \in {Base}_{Scalar (R freeLMod (I \times I))}$
27		simprr	$⊢ ((I \in Fin \land R \in DivRing) \land (x \in {Base}_{Scalar (A)} \land y \in {Base}_{A})) \to y \in {Base}_{A}$
28	11	adantr	$⊢ ((I \in Fin \land R \in DivRing) \land (x \in {Base}_{Scalar (A)} \land y \in {Base}_{A})) \to {Base}_{A} = {Base}_{(R freeLMod (I \times I))}$
29	27 28	eleqtrd	$⊢ ((I \in Fin \land R \in DivRing) \land (x \in {Base}_{Scalar (A)} \land y \in {Base}_{A})) \to y \in {Base}_{(R freeLMod (I \times I))}$
30		eqid	$⊢ {Base}_{(R freeLMod (I \times I))} = {Base}_{(R freeLMod (I \times I))}$
31		eqid	$⊢ Scalar (R freeLMod (I \times I)) = Scalar (R freeLMod (I \times I))$
32		eqid	$⊢ \cdot_{(R freeLMod (I \times I))} = \cdot_{(R freeLMod (I \times I))}$
33		eqid	$⊢ {Base}_{Scalar (R freeLMod (I \times I))} = {Base}_{Scalar (R freeLMod (I \times I))}$
34	30 31 32 33	lmodvscl	$⊢ (R freeLMod (I \times I) \in LMod \land x \in {Base}_{Scalar (R freeLMod (I \times I))} \land y \in {Base}_{(R freeLMod (I \times I))}) \to x \cdot_{(R freeLMod (I \times I))} y \in {Base}_{(R freeLMod (I \times I))}$
35	20 26 29 34	syl3anc	$⊢ ((I \in Fin \land R \in DivRing) \land (x \in {Base}_{Scalar (A)} \land y \in {Base}_{A})) \to x \cdot_{(R freeLMod (I \times I))} y \in {Base}_{(R freeLMod (I \times I))}$
36	35 28	eleqtrrd	$⊢ ((I \in Fin \land R \in DivRing) \land (x \in {Base}_{Scalar (A)} \land y \in {Base}_{A})) \to x \cdot_{(R freeLMod (I \times I))} y \in {Base}_{A}$
37	1 7	matvsca	$⊢ (I \in Fin \land R \in DivRing) \to \cdot_{(R freeLMod (I \times I))} = \cdot_{A}$
38	37	oveqdr	$⊢ ((I \in Fin \land R \in DivRing) \land (x \in {Base}_{Scalar (A)} \land y \in {Base}_{A})) \to x \cdot_{(R freeLMod (I \times I))} y = x \cdot_{A} y$
39		eqid	$⊢ Scalar (A) = Scalar (A)$
40		eqidd	$⊢ (I \in Fin \land R \in DivRing) \to {Base}_{Scalar (A)} = {Base}_{Scalar (A)}$
41	22	fveq2d	$⊢ (I \in Fin \land R \in DivRing) \to +_{Scalar (R freeLMod (I \times I))} = +_{Scalar (A)}$
42	41	oveqdr	$⊢ ((I \in Fin \land R \in DivRing) \land (x \in {Base}_{Scalar (A)} \land y \in {Base}_{Scalar (A)})) \to x +_{Scalar (R freeLMod (I \times I))} y = x +_{Scalar (A)} y$
43		drngring	$⊢ R \in DivRing \to R \in Ring$
44	1	matlmod	$⊢ (I \in Fin \land R \in Ring) \to A \in LMod$
45	43 44	sylan2	$⊢ (I \in Fin \land R \in DivRing) \to A \in LMod$
46	1	matsca2	$⊢ (I \in Fin \land R \in DivRing) \to R = Scalar (A)$
47	46 3	eqeltrrd	$⊢ (I \in Fin \land R \in DivRing) \to Scalar (A) \in DivRing$
48	39	islvec	$⊢ A \in LVec \leftrightarrow (A \in LMod \land Scalar (A) \in DivRing)$
49	45 47 48	sylanbrc	$⊢ (I \in Fin \land R \in DivRing) \to A \in LVec$
50	11 12 13 15 36 38 31 39 24 40 42 17 49	dimpropd	$⊢ (I \in Fin \land R \in DivRing) \to \dim (R freeLMod (I \times I)) = \dim (A)$
51		hashxp	$⊢ (I \in Fin \land I \in Fin) \to \|I \times I\| = \|I\| \|I\|$
52	4 4 51	syl2anc	$⊢ (I \in Fin \land R \in DivRing) \to \|I \times I\| = \|I\| \|I\|$
53	9 50 52	3eqtr3d	$⊢ (I \in Fin \land R \in DivRing) \to \dim (A) = \|I\| \|I\|$
54	2 2	oveq12i	$⊢ N \cdot N = \|I\| \|I\|$
55	53 54	eqtr4di	$⊢ (I \in Fin \land R \in DivRing) \to \dim (A) = N \cdot N$

Metamath Proof Explorer

Theorem matdim

Proof