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	⊢ 𝑅 ∈ CRing
Assertion	smadiadetg0	⊢ ( ( 𝑀 ∈ ( Base ‘ ( 𝑁 Mat 𝑅 ) ) ∧ 𝐾 ∈ 𝑁 ∧ 𝑆 ∈ ( Base ‘ 𝑅 ) ) → ( ( 𝑁 maDet 𝑅 ) ‘ ( 𝐾 ( 𝑀 ( 𝑁 matRRep 𝑅 ) 𝑆 ) 𝐾 ) ) = ( 𝑆 ( .r ‘ 𝑅 ) ( ( ( 𝑁 ∖ { 𝐾 } ) maDet 𝑅 ) ‘ ( 𝐾 ( ( 𝑁 subMat 𝑅 ) ‘ 𝑀 ) 𝐾 ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		smadiadetg0.r	⊢ 𝑅 ∈ CRing
2		eqid	⊢ ( 𝑁 Mat 𝑅 ) = ( 𝑁 Mat 𝑅 )
3		eqid	⊢ ( Base ‘ ( 𝑁 Mat 𝑅 ) ) = ( Base ‘ ( 𝑁 Mat 𝑅 ) )
4		eqid	⊢ ( 𝑁 maDet 𝑅 ) = ( 𝑁 maDet 𝑅 )
5		eqid	⊢ ( ( 𝑁 ∖ { 𝐾 } ) maDet 𝑅 ) = ( ( 𝑁 ∖ { 𝐾 } ) maDet 𝑅 )
6		eqid	⊢ ( .r ‘ 𝑅 ) = ( .r ‘ 𝑅 )
7	2 3 1 4 5 6	smadiadetg	⊢ ( ( 𝑀 ∈ ( Base ‘ ( 𝑁 Mat 𝑅 ) ) ∧ 𝐾 ∈ 𝑁 ∧ 𝑆 ∈ ( Base ‘ 𝑅 ) ) → ( ( 𝑁 maDet 𝑅 ) ‘ ( 𝐾 ( 𝑀 ( 𝑁 matRRep 𝑅 ) 𝑆 ) 𝐾 ) ) = ( 𝑆 ( .r ‘ 𝑅 ) ( ( ( 𝑁 ∖ { 𝐾 } ) maDet 𝑅 ) ‘ ( 𝐾 ( ( 𝑁 subMat 𝑅 ) ‘ 𝑀 ) 𝐾 ) ) ) )