Theorem minmar1cl

Description: Closure of the row replacement function for square matrices: The matrix for a minor is a matrix. (Contributed by AV, 13-Feb-2019)

	Ref	Expression
Hypotheses	minmar1cl.a	⊢ 𝐴 = ( 𝑁 Mat 𝑅 )
	minmar1cl.b	⊢ 𝐵 = ( Base ‘ 𝐴 )
Assertion	minmar1cl	⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝐾 ∈ 𝑁 ∧ 𝐿 ∈ 𝑁 ) ) → ( 𝐾 ( ( 𝑁 minMatR1 𝑅 ) ‘ 𝑀 ) 𝐿 ) ∈ 𝐵 )

Proof

Step	Hyp	Ref	Expression
1		minmar1cl.a	⊢ 𝐴 = ( 𝑁 Mat 𝑅 )
2		minmar1cl.b	⊢ 𝐵 = ( Base ‘ 𝐴 )
3		eqid	⊢ ( 1r ‘ 𝑅 ) = ( 1r ‘ 𝑅 )
4	1 2 3	minmar1marrep	⊢ ( ( 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ) → ( ( 𝑁 minMatR1 𝑅 ) ‘ 𝑀 ) = ( 𝑀 ( 𝑁 matRRep 𝑅 ) ( 1r ‘ 𝑅 ) ) )
5	4	adantr	⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝐾 ∈ 𝑁 ∧ 𝐿 ∈ 𝑁 ) ) → ( ( 𝑁 minMatR1 𝑅 ) ‘ 𝑀 ) = ( 𝑀 ( 𝑁 matRRep 𝑅 ) ( 1r ‘ 𝑅 ) ) )
6	5	oveqd	⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝐾 ∈ 𝑁 ∧ 𝐿 ∈ 𝑁 ) ) → ( 𝐾 ( ( 𝑁 minMatR1 𝑅 ) ‘ 𝑀 ) 𝐿 ) = ( 𝐾 ( 𝑀 ( 𝑁 matRRep 𝑅 ) ( 1r ‘ 𝑅 ) ) 𝐿 ) )
7		simpl	⊢ ( ( 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ) → 𝑅 ∈ Ring )
8		simpr	⊢ ( ( 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ) → 𝑀 ∈ 𝐵 )
9		eqid	⊢ ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 )
10	9 3	ringidcl	⊢ ( 𝑅 ∈ Ring → ( 1r ‘ 𝑅 ) ∈ ( Base ‘ 𝑅 ) )
11	10	adantr	⊢ ( ( 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ) → ( 1r ‘ 𝑅 ) ∈ ( Base ‘ 𝑅 ) )
12	7 8 11	3jca	⊢ ( ( 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ) → ( 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ∧ ( 1r ‘ 𝑅 ) ∈ ( Base ‘ 𝑅 ) ) )
13	1 2	marrepcl	⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ∧ ( 1r ‘ 𝑅 ) ∈ ( Base ‘ 𝑅 ) ) ∧ ( 𝐾 ∈ 𝑁 ∧ 𝐿 ∈ 𝑁 ) ) → ( 𝐾 ( 𝑀 ( 𝑁 matRRep 𝑅 ) ( 1r ‘ 𝑅 ) ) 𝐿 ) ∈ 𝐵 )
14	12 13	sylan	⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝐾 ∈ 𝑁 ∧ 𝐿 ∈ 𝑁 ) ) → ( 𝐾 ( 𝑀 ( 𝑁 matRRep 𝑅 ) ( 1r ‘ 𝑅 ) ) 𝐿 ) ∈ 𝐵 )
15	6 14	eqeltrd	⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝐾 ∈ 𝑁 ∧ 𝐿 ∈ 𝑁 ) ) → ( 𝐾 ( ( 𝑁 minMatR1 𝑅 ) ‘ 𝑀 ) 𝐿 ) ∈ 𝐵 )