Theorem matbas

Description: The matrix ring has the same base set as its underlying group. (Contributed by Stefan O'Rear, 4-Sep-2015)

	Ref	Expression
Hypotheses	matbas.a	$$⊢A=N\mathrm{Mat}R$$
	matbas.g	$$⊢G=R\mathrm{freeLMod}\left(N\times N\right)$$
Assertion	matbas	$$⊢\left(N\in \mathrm{Fin}\wedge R\in V\right)\to {\mathrm{Base}}_G={\mathrm{Base}}_A$$

Proof

Step	Hyp	Ref	Expression
1		matbas.a	$$⊢A=N\mathrm{Mat}R$$
2		matbas.g	$$⊢G=R\mathrm{freeLMod}\left(N\times N\right)$$
3		baseid	$$⊢\mathrm{Base}=\mathrm{Slot}{\mathrm{Base}}_{\mathrm{ndx}}$$
4		basendxnmulrndx	$$⊢{\mathrm{Base}}_{\mathrm{ndx}}\ne {\cdot }_{\mathrm{ndx}}$$
5	3 4	setsnid	$$⊢{\mathrm{Base}}_G={\mathrm{Base}}_{\left(G\mathrm{sSet}⟨{\cdot }_{\mathrm{ndx}},R\mathrm{maMul}⟨N,N,N⟩⟩\right)}$$
6		eqid	$$⊢R\mathrm{maMul}⟨N,N,N⟩=R\mathrm{maMul}⟨N,N,N⟩$$
7	1 2 6	matval	$$⊢\left(N\in \mathrm{Fin}\wedge R\in V\right)\to A=G\mathrm{sSet}⟨{\cdot }_{\mathrm{ndx}},R\mathrm{maMul}⟨N,N,N⟩⟩$$
8	7	fveq2d	$$⊢\left(N\in \mathrm{Fin}\wedge R\in V\right)\to {\mathrm{Base}}_A={\mathrm{Base}}_{\left(G\mathrm{sSet}⟨{\cdot }_{\mathrm{ndx}},R\mathrm{maMul}⟨N,N,N⟩⟩\right)}$$
9	5 8	eqtr4id	$$⊢\left(N\in \mathrm{Fin}\wedge R\in V\right)\to {\mathrm{Base}}_G={\mathrm{Base}}_A$$