Theorem lco0

Description: The set of empty linear combinations over a monoid is the singleton with the identity element of the monoid. (Contributed by AV, 12-Apr-2019)

	Ref	Expression
Assertion	lco0	⊢ ( 𝑀 ∈ Mnd → ( 𝑀 LinCo ∅ ) = { ( 0g ‘ 𝑀 ) } )

Proof

Step	Hyp	Ref	Expression
1		0elpw	⊢ ∅ ∈ 𝒫 ( Base ‘ 𝑀 )
2		eqid	⊢ ( Base ‘ 𝑀 ) = ( Base ‘ 𝑀 )
3		eqid	⊢ ( Scalar ‘ 𝑀 ) = ( Scalar ‘ 𝑀 )
4		eqid	⊢ ( Base ‘ ( Scalar ‘ 𝑀 ) ) = ( Base ‘ ( Scalar ‘ 𝑀 ) )
5	2 3 4	lcoop	⊢ ( ( 𝑀 ∈ Mnd ∧ ∅ ∈ 𝒫 ( Base ‘ 𝑀 ) ) → ( 𝑀 LinCo ∅ ) = { 𝑣 ∈ ( Base ‘ 𝑀 ) ∣ ∃ 𝑤 ∈ ( ( Base ‘ ( Scalar ‘ 𝑀 ) ) ↑m ∅ ) ( 𝑤 finSupp ( 0g ‘ ( Scalar ‘ 𝑀 ) ) ∧ 𝑣 = ( 𝑤 ( linC ‘ 𝑀 ) ∅ ) ) } )
6	1 5	mpan2	⊢ ( 𝑀 ∈ Mnd → ( 𝑀 LinCo ∅ ) = { 𝑣 ∈ ( Base ‘ 𝑀 ) ∣ ∃ 𝑤 ∈ ( ( Base ‘ ( Scalar ‘ 𝑀 ) ) ↑m ∅ ) ( 𝑤 finSupp ( 0g ‘ ( Scalar ‘ 𝑀 ) ) ∧ 𝑣 = ( 𝑤 ( linC ‘ 𝑀 ) ∅ ) ) } )
7		fvex	⊢ ( Base ‘ ( Scalar ‘ 𝑀 ) ) ∈ V
8		map0e	⊢ ( ( Base ‘ ( Scalar ‘ 𝑀 ) ) ∈ V → ( ( Base ‘ ( Scalar ‘ 𝑀 ) ) ↑m ∅ ) = 1o )
9	7 8	mp1i	⊢ ( ( 𝑀 ∈ Mnd ∧ 𝑣 ∈ ( Base ‘ 𝑀 ) ) → ( ( Base ‘ ( Scalar ‘ 𝑀 ) ) ↑m ∅ ) = 1o )
10		df1o2	⊢ 1o = { ∅ }
11	9 10	eqtrdi	⊢ ( ( 𝑀 ∈ Mnd ∧ 𝑣 ∈ ( Base ‘ 𝑀 ) ) → ( ( Base ‘ ( Scalar ‘ 𝑀 ) ) ↑m ∅ ) = { ∅ } )
12	11	rexeqdv	⊢ ( ( 𝑀 ∈ Mnd ∧ 𝑣 ∈ ( Base ‘ 𝑀 ) ) → ( ∃ 𝑤 ∈ ( ( Base ‘ ( Scalar ‘ 𝑀 ) ) ↑m ∅ ) ( 𝑤 finSupp ( 0g ‘ ( Scalar ‘ 𝑀 ) ) ∧ 𝑣 = ( 𝑤 ( linC ‘ 𝑀 ) ∅ ) ) ↔ ∃ 𝑤 ∈ { ∅ } ( 𝑤 finSupp ( 0g ‘ ( Scalar ‘ 𝑀 ) ) ∧ 𝑣 = ( 𝑤 ( linC ‘ 𝑀 ) ∅ ) ) ) )
13		lincval0	⊢ ( 𝑀 ∈ Mnd → ( ∅ ( linC ‘ 𝑀 ) ∅ ) = ( 0g ‘ 𝑀 ) )
14	13	adantr	⊢ ( ( 𝑀 ∈ Mnd ∧ 𝑣 ∈ ( Base ‘ 𝑀 ) ) → ( ∅ ( linC ‘ 𝑀 ) ∅ ) = ( 0g ‘ 𝑀 ) )
15	14	eqeq2d	⊢ ( ( 𝑀 ∈ Mnd ∧ 𝑣 ∈ ( Base ‘ 𝑀 ) ) → ( 𝑣 = ( ∅ ( linC ‘ 𝑀 ) ∅ ) ↔ 𝑣 = ( 0g ‘ 𝑀 ) ) )
16	15	anbi2d	⊢ ( ( 𝑀 ∈ Mnd ∧ 𝑣 ∈ ( Base ‘ 𝑀 ) ) → ( ( ∅ ∈ Fin ∧ 𝑣 = ( ∅ ( linC ‘ 𝑀 ) ∅ ) ) ↔ ( ∅ ∈ Fin ∧ 𝑣 = ( 0g ‘ 𝑀 ) ) ) )
17		0ex	⊢ ∅ ∈ V
18		breq1	⊢ ( 𝑤 = ∅ → ( 𝑤 finSupp ( 0g ‘ ( Scalar ‘ 𝑀 ) ) ↔ ∅ finSupp ( 0g ‘ ( Scalar ‘ 𝑀 ) ) ) )
19		fvex	⊢ ( 0g ‘ ( Scalar ‘ 𝑀 ) ) ∈ V
20		0fsupp	⊢ ( ( 0g ‘ ( Scalar ‘ 𝑀 ) ) ∈ V → ∅ finSupp ( 0g ‘ ( Scalar ‘ 𝑀 ) ) )
21	19 20	ax-mp	⊢ ∅ finSupp ( 0g ‘ ( Scalar ‘ 𝑀 ) )
22		0fin	⊢ ∅ ∈ Fin
23	21 22	2th	⊢ ( ∅ finSupp ( 0g ‘ ( Scalar ‘ 𝑀 ) ) ↔ ∅ ∈ Fin )
24	18 23	bitrdi	⊢ ( 𝑤 = ∅ → ( 𝑤 finSupp ( 0g ‘ ( Scalar ‘ 𝑀 ) ) ↔ ∅ ∈ Fin ) )
25		oveq1	⊢ ( 𝑤 = ∅ → ( 𝑤 ( linC ‘ 𝑀 ) ∅ ) = ( ∅ ( linC ‘ 𝑀 ) ∅ ) )
26	25	eqeq2d	⊢ ( 𝑤 = ∅ → ( 𝑣 = ( 𝑤 ( linC ‘ 𝑀 ) ∅ ) ↔ 𝑣 = ( ∅ ( linC ‘ 𝑀 ) ∅ ) ) )
27	24 26	anbi12d	⊢ ( 𝑤 = ∅ → ( ( 𝑤 finSupp ( 0g ‘ ( Scalar ‘ 𝑀 ) ) ∧ 𝑣 = ( 𝑤 ( linC ‘ 𝑀 ) ∅ ) ) ↔ ( ∅ ∈ Fin ∧ 𝑣 = ( ∅ ( linC ‘ 𝑀 ) ∅ ) ) ) )
28	27	rexsng	⊢ ( ∅ ∈ V → ( ∃ 𝑤 ∈ { ∅ } ( 𝑤 finSupp ( 0g ‘ ( Scalar ‘ 𝑀 ) ) ∧ 𝑣 = ( 𝑤 ( linC ‘ 𝑀 ) ∅ ) ) ↔ ( ∅ ∈ Fin ∧ 𝑣 = ( ∅ ( linC ‘ 𝑀 ) ∅ ) ) ) )
29	17 28	mp1i	⊢ ( ( 𝑀 ∈ Mnd ∧ 𝑣 ∈ ( Base ‘ 𝑀 ) ) → ( ∃ 𝑤 ∈ { ∅ } ( 𝑤 finSupp ( 0g ‘ ( Scalar ‘ 𝑀 ) ) ∧ 𝑣 = ( 𝑤 ( linC ‘ 𝑀 ) ∅ ) ) ↔ ( ∅ ∈ Fin ∧ 𝑣 = ( ∅ ( linC ‘ 𝑀 ) ∅ ) ) ) )
30	22	a1i	⊢ ( ( 𝑀 ∈ Mnd ∧ 𝑣 ∈ ( Base ‘ 𝑀 ) ) → ∅ ∈ Fin )
31	30	biantrurd	⊢ ( ( 𝑀 ∈ Mnd ∧ 𝑣 ∈ ( Base ‘ 𝑀 ) ) → ( 𝑣 = ( 0g ‘ 𝑀 ) ↔ ( ∅ ∈ Fin ∧ 𝑣 = ( 0g ‘ 𝑀 ) ) ) )
32	16 29 31	3bitr4d	⊢ ( ( 𝑀 ∈ Mnd ∧ 𝑣 ∈ ( Base ‘ 𝑀 ) ) → ( ∃ 𝑤 ∈ { ∅ } ( 𝑤 finSupp ( 0g ‘ ( Scalar ‘ 𝑀 ) ) ∧ 𝑣 = ( 𝑤 ( linC ‘ 𝑀 ) ∅ ) ) ↔ 𝑣 = ( 0g ‘ 𝑀 ) ) )
33	12 32	bitrd	⊢ ( ( 𝑀 ∈ Mnd ∧ 𝑣 ∈ ( Base ‘ 𝑀 ) ) → ( ∃ 𝑤 ∈ ( ( Base ‘ ( Scalar ‘ 𝑀 ) ) ↑m ∅ ) ( 𝑤 finSupp ( 0g ‘ ( Scalar ‘ 𝑀 ) ) ∧ 𝑣 = ( 𝑤 ( linC ‘ 𝑀 ) ∅ ) ) ↔ 𝑣 = ( 0g ‘ 𝑀 ) ) )
34	33	rabbidva	⊢ ( 𝑀 ∈ Mnd → { 𝑣 ∈ ( Base ‘ 𝑀 ) ∣ ∃ 𝑤 ∈ ( ( Base ‘ ( Scalar ‘ 𝑀 ) ) ↑m ∅ ) ( 𝑤 finSupp ( 0g ‘ ( Scalar ‘ 𝑀 ) ) ∧ 𝑣 = ( 𝑤 ( linC ‘ 𝑀 ) ∅ ) ) } = { 𝑣 ∈ ( Base ‘ 𝑀 ) ∣ 𝑣 = ( 0g ‘ 𝑀 ) } )
35		eqid	⊢ ( 0g ‘ 𝑀 ) = ( 0g ‘ 𝑀 )
36	2 35	mndidcl	⊢ ( 𝑀 ∈ Mnd → ( 0g ‘ 𝑀 ) ∈ ( Base ‘ 𝑀 ) )
37		rabsn	⊢ ( ( 0g ‘ 𝑀 ) ∈ ( Base ‘ 𝑀 ) → { 𝑣 ∈ ( Base ‘ 𝑀 ) ∣ 𝑣 = ( 0g ‘ 𝑀 ) } = { ( 0g ‘ 𝑀 ) } )
38	36 37	syl	⊢ ( 𝑀 ∈ Mnd → { 𝑣 ∈ ( Base ‘ 𝑀 ) ∣ 𝑣 = ( 0g ‘ 𝑀 ) } = { ( 0g ‘ 𝑀 ) } )
39	6 34 38	3eqtrd	⊢ ( 𝑀 ∈ Mnd → ( 𝑀 LinCo ∅ ) = { ( 0g ‘ 𝑀 ) } )