Theorem matscaOLD

Description: Obsolete proof of matsca as of 12-Nov-2024. The matrix ring has the same scalars as its underlying linear structure. (Contributed by Stefan O'Rear, 4-Sep-2015) (Proof modification is discouraged.) (New usage is discouraged.)

	Ref	Expression
Hypotheses	matbas.a	|- A = ( N Mat R )
	matbas.g	|- G = ( R freeLMod ( N X. N ) )
Assertion	matscaOLD	|- ( ( N e. Fin /\ R e. V ) -> ( Scalar ` G ) = ( Scalar ` A ) )

Proof

Step	Hyp	Ref	Expression
1		matbas.a	|- A = ( N Mat R )
2		matbas.g	|- G = ( R freeLMod ( N X. N ) )
3		scaid	|- Scalar = Slot ( Scalar ` ndx )
4		3re	|- 3 e. RR
5		3lt5	|- 3 < 5
6	4 5	gtneii	|- 5 =/= 3
7		scandx	|- ( Scalar ` ndx ) = 5
8		mulrndx	|- ( .r ` ndx ) = 3
9	7 8	neeq12i	|- ( ( Scalar ` ndx ) =/= ( .r ` ndx ) <-> 5 =/= 3 )
10	6 9	mpbir	|- ( Scalar ` ndx ) =/= ( .r ` ndx )
11	3 10	setsnid	|- ( Scalar ` G ) = ( Scalar ` ( G sSet <. ( .r ` ndx ) , ( R maMul <. N , N , N >. ) >. ) )
12		eqid	|- ( R maMul <. N , N , N >. ) = ( R maMul <. N , N , N >. )
13	1 2 12	matval	|- ( ( N e. Fin /\ R e. V ) -> A = ( G sSet <. ( .r ` ndx ) , ( R maMul <. N , N , N >. ) >. ) )
14	13	fveq2d	|- ( ( N e. Fin /\ R e. V ) -> ( Scalar ` A ) = ( Scalar ` ( G sSet <. ( .r ` ndx ) , ( R maMul <. N , N , N >. ) >. ) ) )
15	11 14	eqtr4id	|- ( ( N e. Fin /\ R e. V ) -> ( Scalar ` G ) = ( Scalar ` A ) )