Theorem lco0 48273

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.)

Assertion

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

Proof of Theorem lco0

Dummy variables 𝑣 𝑤 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		0elpw 5362	. . 3 ⊢ ∅ ∈ 𝒫 (Base‘𝑀)
2		eqid 2735	. . . 4 ⊢ (Base‘𝑀) = (Base‘𝑀)
3		eqid 2735	. . . 4 ⊢ (Scalar‘𝑀) = (Scalar‘𝑀)
4		eqid 2735	. . . 4 ⊢ (Base‘(Scalar‘𝑀)) = (Base‘(Scalar‘𝑀))
5	2, 3, 4	lcoop 48257	. . 3 ⊢ ((𝑀 ∈ Mnd ∧ ∅ ∈ 𝒫 (Base‘𝑀)) → (𝑀 LinCo ∅) = {𝑣 ∈ (Base‘𝑀) ∣ ∃𝑤 ∈ ((Base‘(Scalar‘𝑀)) ↑m ∅)(𝑤 finSupp (0g‘(Scalar‘𝑀)) ∧ 𝑣 = (𝑤( linC ‘𝑀)∅))})
6	1, 5	mpan2 691	. 2 ⊢ (𝑀 ∈ Mnd → (𝑀 LinCo ∅) = {𝑣 ∈ (Base‘𝑀) ∣ ∃𝑤 ∈ ((Base‘(Scalar‘𝑀)) ↑m ∅)(𝑤 finSupp (0g‘(Scalar‘𝑀)) ∧ 𝑣 = (𝑤( linC ‘𝑀)∅))})
7		fvex 6920	. . . . . . 7 ⊢ (Base‘(Scalar‘𝑀)) ∈ V
8		map0e 8921	. . . . . . 7 ⊢ ((Base‘(Scalar‘𝑀)) ∈ V → ((Base‘(Scalar‘𝑀)) ↑m ∅) = 1o)
9	7, 8	mp1i 13	. . . . . 6 ⊢ ((𝑀 ∈ Mnd ∧ 𝑣 ∈ (Base‘𝑀)) → ((Base‘(Scalar‘𝑀)) ↑m ∅) = 1o)
10		df1o2 8512	. . . . . 6 ⊢ 1o = {∅}
11	9, 10	eqtrdi 2791	. . . . 5 ⊢ ((𝑀 ∈ Mnd ∧ 𝑣 ∈ (Base‘𝑀)) → ((Base‘(Scalar‘𝑀)) ↑m ∅) = {∅})
12	11	rexeqdv 3325	. . . 4 ⊢ ((𝑀 ∈ Mnd ∧ 𝑣 ∈ (Base‘𝑀)) → (∃𝑤 ∈ ((Base‘(Scalar‘𝑀)) ↑m ∅)(𝑤 finSupp (0g‘(Scalar‘𝑀)) ∧ 𝑣 = (𝑤( linC ‘𝑀)∅)) ↔ ∃𝑤 ∈ {∅} (𝑤 finSupp (0g‘(Scalar‘𝑀)) ∧ 𝑣 = (𝑤( linC ‘𝑀)∅))))
13		lincval0 48261	. . . . . . . 8 ⊢ (𝑀 ∈ Mnd → (∅( linC ‘𝑀)∅) = (0g‘𝑀))
14	13	adantr 480	. . . . . . 7 ⊢ ((𝑀 ∈ Mnd ∧ 𝑣 ∈ (Base‘𝑀)) → (∅( linC ‘𝑀)∅) = (0g‘𝑀))
15	14	eqeq2d 2746	. . . . . 6 ⊢ ((𝑀 ∈ Mnd ∧ 𝑣 ∈ (Base‘𝑀)) → (𝑣 = (∅( linC ‘𝑀)∅) ↔ 𝑣 = (0g‘𝑀)))
16	15	anbi2d 630	. . . . 5 ⊢ ((𝑀 ∈ Mnd ∧ 𝑣 ∈ (Base‘𝑀)) → ((∅ ∈ Fin ∧ 𝑣 = (∅( linC ‘𝑀)∅)) ↔ (∅ ∈ Fin ∧ 𝑣 = (0g‘𝑀))))
17		0ex 5313	. . . . . 6 ⊢ ∅ ∈ V
18		breq1 5151	. . . . . . . . 9 ⊢ (𝑤 = ∅ → (𝑤 finSupp (0g‘(Scalar‘𝑀)) ↔ ∅ finSupp (0g‘(Scalar‘𝑀))))
19		fvex 6920	. . . . . . . . . . 11 ⊢ (0g‘(Scalar‘𝑀)) ∈ V
20		0fsupp 9428	. . . . . . . . . . 11 ⊢ ((0g‘(Scalar‘𝑀)) ∈ V → ∅ finSupp (0g‘(Scalar‘𝑀)))
21	19, 20	ax-mp 5	. . . . . . . . . 10 ⊢ ∅ finSupp (0g‘(Scalar‘𝑀))
22		0fi 9081	. . . . . . . . . 10 ⊢ ∅ ∈ Fin
23	21, 22	2th 264	. . . . . . . . 9 ⊢ (∅ finSupp (0g‘(Scalar‘𝑀)) ↔ ∅ ∈ Fin)
24	18, 23	bitrdi 287	. . . . . . . 8 ⊢ (𝑤 = ∅ → (𝑤 finSupp (0g‘(Scalar‘𝑀)) ↔ ∅ ∈ Fin))
25		oveq1 7438	. . . . . . . . 9 ⊢ (𝑤 = ∅ → (𝑤( linC ‘𝑀)∅) = (∅( linC ‘𝑀)∅))
26	25	eqeq2d 2746	. . . . . . . 8 ⊢ (𝑤 = ∅ → (𝑣 = (𝑤( linC ‘𝑀)∅) ↔ 𝑣 = (∅( linC ‘𝑀)∅)))
27	24, 26	anbi12d 632	. . . . . . 7 ⊢ (𝑤 = ∅ → ((𝑤 finSupp (0g‘(Scalar‘𝑀)) ∧ 𝑣 = (𝑤( linC ‘𝑀)∅)) ↔ (∅ ∈ Fin ∧ 𝑣 = (∅( linC ‘𝑀)∅))))
28	27	rexsng 4681	. . . . . 6 ⊢ (∅ ∈ V → (∃𝑤 ∈ {∅} (𝑤 finSupp (0g‘(Scalar‘𝑀)) ∧ 𝑣 = (𝑤( linC ‘𝑀)∅)) ↔ (∅ ∈ Fin ∧ 𝑣 = (∅( linC ‘𝑀)∅))))
29	17, 28	mp1i 13	. . . . 5 ⊢ ((𝑀 ∈ Mnd ∧ 𝑣 ∈ (Base‘𝑀)) → (∃𝑤 ∈ {∅} (𝑤 finSupp (0g‘(Scalar‘𝑀)) ∧ 𝑣 = (𝑤( linC ‘𝑀)∅)) ↔ (∅ ∈ Fin ∧ 𝑣 = (∅( linC ‘𝑀)∅))))
30	22	a1i 11	. . . . . 6 ⊢ ((𝑀 ∈ Mnd ∧ 𝑣 ∈ (Base‘𝑀)) → ∅ ∈ Fin)
31	30	biantrurd 532	. . . . 5 ⊢ ((𝑀 ∈ Mnd ∧ 𝑣 ∈ (Base‘𝑀)) → (𝑣 = (0g‘𝑀) ↔ (∅ ∈ Fin ∧ 𝑣 = (0g‘𝑀))))
32	16, 29, 31	3bitr4d 311	. . . 4 ⊢ ((𝑀 ∈ Mnd ∧ 𝑣 ∈ (Base‘𝑀)) → (∃𝑤 ∈ {∅} (𝑤 finSupp (0g‘(Scalar‘𝑀)) ∧ 𝑣 = (𝑤( linC ‘𝑀)∅)) ↔ 𝑣 = (0g‘𝑀)))
33	12, 32	bitrd 279	. . 3 ⊢ ((𝑀 ∈ Mnd ∧ 𝑣 ∈ (Base‘𝑀)) → (∃𝑤 ∈ ((Base‘(Scalar‘𝑀)) ↑m ∅)(𝑤 finSupp (0g‘(Scalar‘𝑀)) ∧ 𝑣 = (𝑤( linC ‘𝑀)∅)) ↔ 𝑣 = (0g‘𝑀)))
34	33	rabbidva 3440	. 2 ⊢ (𝑀 ∈ Mnd → {𝑣 ∈ (Base‘𝑀) ∣ ∃𝑤 ∈ ((Base‘(Scalar‘𝑀)) ↑m ∅)(𝑤 finSupp (0g‘(Scalar‘𝑀)) ∧ 𝑣 = (𝑤( linC ‘𝑀)∅))} = {𝑣 ∈ (Base‘𝑀) ∣ 𝑣 = (0g‘𝑀)})
35		eqid 2735	. . . 4 ⊢ (0g‘𝑀) = (0g‘𝑀)
36	2, 35	mndidcl 18775	. . 3 ⊢ (𝑀 ∈ Mnd → (0g‘𝑀) ∈ (Base‘𝑀))
37		rabsn 4726	. . 3 ⊢ ((0g‘𝑀) ∈ (Base‘𝑀) → {𝑣 ∈ (Base‘𝑀) ∣ 𝑣 = (0g‘𝑀)} = {(0g‘𝑀)})
38	36, 37	syl 17	. 2 ⊢ (𝑀 ∈ Mnd → {𝑣 ∈ (Base‘𝑀) ∣ 𝑣 = (0g‘𝑀)} = {(0g‘𝑀)})
39	6, 34, 38	3eqtrd 2779	1 ⊢ (𝑀 ∈ Mnd → (𝑀 LinCo ∅) = {(0g‘𝑀)})

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395   = wceq 1537   ∈ wcel 2106  ∃wrex 3068  {crab 3433  Vcvv 3478  ∅c0 4339  𝒫 cpw 4605  {csn 4631   class class class wbr 5148  ‘cfv 6563  (class class class)co 7431  1_oc1o 8498   ↑_m cmap 8865  Fincfn 8984   finSupp cfsupp 9399  Basecbs 17245  Scalarcsca 17301  0_gc0g 17486  Mndcmnd 18760   linC clinc 48250   LinCo clinco 48251

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005  ax-8 2108  ax-9 2116  ax-10 2139  ax-11 2155  ax-12 2175  ax-ext 2706  ax-rep 5285  ax-sep 5302  ax-nul 5312  ax-pow 5371  ax-pr 5438  ax-un 7754

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1540  df-fal 1550  df-ex 1777  df-nf 1781  df-sb 2063  df-mo 2538  df-eu 2567  df-clab 2713  df-cleq 2727  df-clel 2814  df-nfc 2890  df-ne 2939  df-ral 3060  df-rex 3069  df-rmo 3378  df-reu 3379  df-rab 3434  df-v 3480  df-sbc 3792  df-csb 3909  df-dif 3966  df-un 3968  df-in 3970  df-ss 3980  df-pss 3983  df-nul 4340  df-if 4532  df-pw 4607  df-sn 4632  df-pr 4634  df-op 4638  df-uni 4913  df-iun 4998  df-br 5149  df-opab 5211  df-mpt 5232  df-tr 5266  df-id 5583  df-eprel 5589  df-po 5597  df-so 5598  df-fr 5641  df-we 5643  df-xp 5695  df-rel 5696  df-cnv 5697  df-co 5698  df-dm 5699  df-rn 5700  df-res 5701  df-ima 5702  df-pred 6323  df-ord 6389  df-on 6390  df-lim 6391  df-suc 6392  df-iota 6516  df-fun 6565  df-fn 6566  df-f 6567  df-f1 6568  df-fo 6569  df-f1o 6570  df-fv 6571  df-riota 7388  df-ov 7434  df-oprab 7435  df-mpo 7436  df-om 7888  df-1st 8013  df-2nd 8014  df-supp 8185  df-frecs 8305  df-wrecs 8336  df-recs 8410  df-rdg 8449  df-1o 8505  df-map 8867  df-en 8985  df-fin 8988  df-fsupp 9400  df-seq 14040  df-0g 17488  df-gsum 17489  df-mgm 18666  df-sgrp 18745  df-mnd 18761  df-linc 48252  df-lco 48253

This theorem is referenced by:  lcoel0  48274