Metamath Proof Explorer

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 \in CRing$
	Assertion	smadiadetg0	$⊢ (M \in {Base}_{(N Mat R)} \land K \in N \land S \in {Base}_{R}) \to (N maDet R) (K (M (N matRRep R) S) K) = S \cdot_{R} ((N ∖ \{K\}) maDet R) (K (N subMat R) (M) K)$

Proof

Step	Hyp	Ref	Expression
1		smadiadetg0.r	$⊢ R \in 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	$⊢ \cdot_{R} = \cdot_{R}$
7	2 3 1 4 5 6	smadiadetg	$⊢ (M \in {Base}_{(N Mat R)} \land K \in N \land S \in {Base}_{R}) \to (N maDet R) (K (M (N matRRep R) S) K) = S \cdot_{R} ((N ∖ \{K\}) maDet R) (K (N subMat R) (M) K)$