Theorem smadiadetg0

Description: Lemma for smadiadetr : version of smadiadetg with all hypotheses defining class variables removed, i.e. all class variables defined in the hypotheses replaced in the theorem by their definition. (Contributed by AV, 15-Feb-2019)

	Ref	Expression
Hypothesis	smadiadetg0.r	|- R e. CRing
Assertion	smadiadetg0	|- ( ( M e. ( Base ` ( N Mat R ) ) /\ K e. N /\ S e. ( Base ` R ) ) -> ( ( N maDet R ) ` ( K ( M ( N matRRep R ) S ) K ) ) = ( S ( .r ` R ) ( ( ( N \ { K } ) maDet R ) ` ( K ( ( N subMat R ) ` M ) K ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		smadiadetg0.r	|- R e. CRing
2		eqid	|- ( N Mat R ) = ( N Mat R )
3		eqid	|- ( Base ` ( N Mat R ) ) = ( Base ` ( N Mat R ) )
4		eqid	|- ( N maDet R ) = ( N maDet R )
5		eqid	|- ( ( N \ { K } ) maDet R ) = ( ( N \ { K } ) maDet R )
6		eqid	|- ( .r ` R ) = ( .r ` R )
7	2 3 1 4 5 6	smadiadetg	|- ( ( M e. ( Base ` ( N Mat R ) ) /\ K e. N /\ S e. ( Base ` R ) ) -> ( ( N maDet R ) ` ( K ( M ( N matRRep R ) S ) K ) ) = ( S ( .r ` R ) ( ( ( N \ { K } ) maDet R ) ` ( K ( ( N subMat R ) ` M ) K ) ) ) )