Theorem scmatid

Description: The identity matrix is a scalar matrix. (Contributed by AV, 20-Aug-2019) (Revised by AV, 18-Dec-2019)

	Ref	Expression
Hypotheses	scmatid.a	⊢ 𝐴 = ( 𝑁 Mat 𝑅 )
	scmatid.b	⊢ 𝐵 = ( Base ‘ 𝐴 )
	scmatid.e	⊢ 𝐸 = ( Base ‘ 𝑅 )
	scmatid.0	⊢ 0 = ( 0g ‘ 𝑅 )
	scmatid.s	⊢ 𝑆 = ( 𝑁 ScMat 𝑅 )
Assertion	scmatid	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → ( 1r ‘ 𝐴 ) ∈ 𝑆 )

Proof

Step	Hyp	Ref	Expression
1		scmatid.a	⊢ 𝐴 = ( 𝑁 Mat 𝑅 )
2		scmatid.b	⊢ 𝐵 = ( Base ‘ 𝐴 )
3		scmatid.e	⊢ 𝐸 = ( Base ‘ 𝑅 )
4		scmatid.0	⊢ 0 = ( 0g ‘ 𝑅 )
5		scmatid.s	⊢ 𝑆 = ( 𝑁 ScMat 𝑅 )
6	1	matring	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → 𝐴 ∈ Ring )
7		eqid	⊢ ( 1r ‘ 𝐴 ) = ( 1r ‘ 𝐴 )
8	2 7	ringidcl	⊢ ( 𝐴 ∈ Ring → ( 1r ‘ 𝐴 ) ∈ 𝐵 )
9	6 8	syl	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → ( 1r ‘ 𝐴 ) ∈ 𝐵 )
10	1	matsca2	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → 𝑅 = ( Scalar ‘ 𝐴 ) )
11	10	eqcomd	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → ( Scalar ‘ 𝐴 ) = 𝑅 )
12	11	fveq2d	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → ( 1r ‘ ( Scalar ‘ 𝐴 ) ) = ( 1r ‘ 𝑅 ) )
13		eqid	⊢ ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 )
14		eqid	⊢ ( 1r ‘ 𝑅 ) = ( 1r ‘ 𝑅 )
15	13 14	ringidcl	⊢ ( 𝑅 ∈ Ring → ( 1r ‘ 𝑅 ) ∈ ( Base ‘ 𝑅 ) )
16	15	adantl	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → ( 1r ‘ 𝑅 ) ∈ ( Base ‘ 𝑅 ) )
17	12 16	eqeltrd	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → ( 1r ‘ ( Scalar ‘ 𝐴 ) ) ∈ ( Base ‘ 𝑅 ) )
18		oveq1	⊢ ( 𝑐 = ( 1r ‘ ( Scalar ‘ 𝐴 ) ) → ( 𝑐 ( ·𝑠 ‘ 𝐴 ) ( 1r ‘ 𝐴 ) ) = ( ( 1r ‘ ( Scalar ‘ 𝐴 ) ) ( ·𝑠 ‘ 𝐴 ) ( 1r ‘ 𝐴 ) ) )
19	18	eqeq2d	⊢ ( 𝑐 = ( 1r ‘ ( Scalar ‘ 𝐴 ) ) → ( ( 1r ‘ 𝐴 ) = ( 𝑐 ( ·𝑠 ‘ 𝐴 ) ( 1r ‘ 𝐴 ) ) ↔ ( 1r ‘ 𝐴 ) = ( ( 1r ‘ ( Scalar ‘ 𝐴 ) ) ( ·𝑠 ‘ 𝐴 ) ( 1r ‘ 𝐴 ) ) ) )
20	19	adantl	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ 𝑐 = ( 1r ‘ ( Scalar ‘ 𝐴 ) ) ) → ( ( 1r ‘ 𝐴 ) = ( 𝑐 ( ·𝑠 ‘ 𝐴 ) ( 1r ‘ 𝐴 ) ) ↔ ( 1r ‘ 𝐴 ) = ( ( 1r ‘ ( Scalar ‘ 𝐴 ) ) ( ·𝑠 ‘ 𝐴 ) ( 1r ‘ 𝐴 ) ) ) )
21	1	matlmod	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → 𝐴 ∈ LMod )
22		eqid	⊢ ( Scalar ‘ 𝐴 ) = ( Scalar ‘ 𝐴 )
23		eqid	⊢ ( ·𝑠 ‘ 𝐴 ) = ( ·𝑠 ‘ 𝐴 )
24		eqid	⊢ ( 1r ‘ ( Scalar ‘ 𝐴 ) ) = ( 1r ‘ ( Scalar ‘ 𝐴 ) )
25	2 22 23 24	lmodvs1	⊢ ( ( 𝐴 ∈ LMod ∧ ( 1r ‘ 𝐴 ) ∈ 𝐵 ) → ( ( 1r ‘ ( Scalar ‘ 𝐴 ) ) ( ·𝑠 ‘ 𝐴 ) ( 1r ‘ 𝐴 ) ) = ( 1r ‘ 𝐴 ) )
26	21 9 25	syl2anc	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → ( ( 1r ‘ ( Scalar ‘ 𝐴 ) ) ( ·𝑠 ‘ 𝐴 ) ( 1r ‘ 𝐴 ) ) = ( 1r ‘ 𝐴 ) )
27	26	eqcomd	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → ( 1r ‘ 𝐴 ) = ( ( 1r ‘ ( Scalar ‘ 𝐴 ) ) ( ·𝑠 ‘ 𝐴 ) ( 1r ‘ 𝐴 ) ) )
28	17 20 27	rspcedvd	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → ∃ 𝑐 ∈ ( Base ‘ 𝑅 ) ( 1r ‘ 𝐴 ) = ( 𝑐 ( ·𝑠 ‘ 𝐴 ) ( 1r ‘ 𝐴 ) ) )
29	13 1 2 7 23 5	scmatel	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → ( ( 1r ‘ 𝐴 ) ∈ 𝑆 ↔ ( ( 1r ‘ 𝐴 ) ∈ 𝐵 ∧ ∃ 𝑐 ∈ ( Base ‘ 𝑅 ) ( 1r ‘ 𝐴 ) = ( 𝑐 ( ·𝑠 ‘ 𝐴 ) ( 1r ‘ 𝐴 ) ) ) ) )
30	9 28 29	mpbir2and	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → ( 1r ‘ 𝐴 ) ∈ 𝑆 )