mat0dimscm

Description: The scalar multiplication in the algebra of matrices with dimension 0. (Contributed by AV, 6-Aug-2019)

		Ref	Expression
	Hypothesis	mat0dim.a	⊢ 𝐴 = ( ∅ Mat 𝑅 )
	Assertion	mat0dimscm	⊢ ( ( 𝑅 ∈ Ring ∧ 𝑋 ∈ ( Base ‘ 𝑅 ) ) → ( 𝑋 ( ·_𝑠 ‘ 𝐴 ) ∅ ) = ∅ )

Proof

Step	Hyp	Ref	Expression
1		mat0dim.a	⊢ 𝐴 = ( ∅ Mat 𝑅 )
2		simpl	⊢ ( ( 𝑅 ∈ Ring ∧ 𝑋 ∈ ( Base ‘ 𝑅 ) ) → 𝑅 ∈ Ring )
3		0fi	⊢ ∅ ∈ Fin
4	1	matlmod	⊢ ( ( ∅ ∈ Fin ∧ 𝑅 ∈ Ring ) → 𝐴 ∈ LMod )
5	3 2 4	sylancr	⊢ ( ( 𝑅 ∈ Ring ∧ 𝑋 ∈ ( Base ‘ 𝑅 ) ) → 𝐴 ∈ LMod )
6	1	matsca2	⊢ ( ( ∅ ∈ Fin ∧ 𝑅 ∈ Ring ) → 𝑅 = ( Scalar ‘ 𝐴 ) )
7	3 6	mpan	⊢ ( 𝑅 ∈ Ring → 𝑅 = ( Scalar ‘ 𝐴 ) )
8	7	fveq2d	⊢ ( 𝑅 ∈ Ring → ( Base ‘ 𝑅 ) = ( Base ‘ ( Scalar ‘ 𝐴 ) ) )
9	8	eleq2d	⊢ ( 𝑅 ∈ Ring → ( 𝑋 ∈ ( Base ‘ 𝑅 ) ↔ 𝑋 ∈ ( Base ‘ ( Scalar ‘ 𝐴 ) ) ) )
10	9	biimpa	⊢ ( ( 𝑅 ∈ Ring ∧ 𝑋 ∈ ( Base ‘ 𝑅 ) ) → 𝑋 ∈ ( Base ‘ ( Scalar ‘ 𝐴 ) ) )
11		0ex	⊢ ∅ ∈ V
12	11	snid	⊢ ∅ ∈ { ∅ }
13	1	fveq2i	⊢ ( Base ‘ 𝐴 ) = ( Base ‘ ( ∅ Mat 𝑅 ) )
14		mat0dimbas0	⊢ ( 𝑅 ∈ Ring → ( Base ‘ ( ∅ Mat 𝑅 ) ) = { ∅ } )
15	13 14	eqtrid	⊢ ( 𝑅 ∈ Ring → ( Base ‘ 𝐴 ) = { ∅ } )
16	12 15	eleqtrrid	⊢ ( 𝑅 ∈ Ring → ∅ ∈ ( Base ‘ 𝐴 ) )
17	16	adantr	⊢ ( ( 𝑅 ∈ Ring ∧ 𝑋 ∈ ( Base ‘ 𝑅 ) ) → ∅ ∈ ( Base ‘ 𝐴 ) )
18		eqid	⊢ ( Base ‘ 𝐴 ) = ( Base ‘ 𝐴 )
19		eqid	⊢ ( Scalar ‘ 𝐴 ) = ( Scalar ‘ 𝐴 )
20		eqid	⊢ ( ·_𝑠 ‘ 𝐴 ) = ( ·_𝑠 ‘ 𝐴 )
21		eqid	⊢ ( Base ‘ ( Scalar ‘ 𝐴 ) ) = ( Base ‘ ( Scalar ‘ 𝐴 ) )
22	18 19 20 21	lmodvscl	⊢ ( ( 𝐴 ∈ LMod ∧ 𝑋 ∈ ( Base ‘ ( Scalar ‘ 𝐴 ) ) ∧ ∅ ∈ ( Base ‘ 𝐴 ) ) → ( 𝑋 ( ·_𝑠 ‘ 𝐴 ) ∅ ) ∈ ( Base ‘ 𝐴 ) )
23	5 10 17 22	syl3anc	⊢ ( ( 𝑅 ∈ Ring ∧ 𝑋 ∈ ( Base ‘ 𝑅 ) ) → ( 𝑋 ( ·_𝑠 ‘ 𝐴 ) ∅ ) ∈ ( Base ‘ 𝐴 ) )
24	15	eleq2d	⊢ ( 𝑅 ∈ Ring → ( ( 𝑋 ( ·_𝑠 ‘ 𝐴 ) ∅ ) ∈ ( Base ‘ 𝐴 ) ↔ ( 𝑋 ( ·_𝑠 ‘ 𝐴 ) ∅ ) ∈ { ∅ } ) )
25		elsni	⊢ ( ( 𝑋 ( ·_𝑠 ‘ 𝐴 ) ∅ ) ∈ { ∅ } → ( 𝑋 ( ·_𝑠 ‘ 𝐴 ) ∅ ) = ∅ )
26	24 25	biimtrdi	⊢ ( 𝑅 ∈ Ring → ( ( 𝑋 ( ·_𝑠 ‘ 𝐴 ) ∅ ) ∈ ( Base ‘ 𝐴 ) → ( 𝑋 ( ·_𝑠 ‘ 𝐴 ) ∅ ) = ∅ ) )
27	2 23 26	sylc	⊢ ( ( 𝑅 ∈ Ring ∧ 𝑋 ∈ ( Base ‘ 𝑅 ) ) → ( 𝑋 ( ·_𝑠 ‘ 𝐴 ) ∅ ) = ∅ )

Metamath Proof Explorer

Theorem mat0dimscm

Proof