# Metamath Proof Explorer

## Theorem pws0g

Description: Zero in a product of monoids. (Contributed by Mario Carneiro, 11-Jan-2015)

Ref Expression
Hypotheses pwsmnd.y ${⊢}{Y}={R}{↑}_{𝑠}{I}$
pws0g.z
Assertion pws0g

### Proof

Step Hyp Ref Expression
1 pwsmnd.y ${⊢}{Y}={R}{↑}_{𝑠}{I}$
2 pws0g.z
3 eqid ${⊢}\mathrm{Scalar}\left({R}\right){⨉}_{𝑠}\left({I}×\left\{{R}\right\}\right)=\mathrm{Scalar}\left({R}\right){⨉}_{𝑠}\left({I}×\left\{{R}\right\}\right)$
4 simpr ${⊢}\left({R}\in \mathrm{Mnd}\wedge {I}\in {V}\right)\to {I}\in {V}$
5 fvexd ${⊢}\left({R}\in \mathrm{Mnd}\wedge {I}\in {V}\right)\to \mathrm{Scalar}\left({R}\right)\in \mathrm{V}$
6 fconst6g ${⊢}{R}\in \mathrm{Mnd}\to \left({I}×\left\{{R}\right\}\right):{I}⟶\mathrm{Mnd}$
7 6 adantr ${⊢}\left({R}\in \mathrm{Mnd}\wedge {I}\in {V}\right)\to \left({I}×\left\{{R}\right\}\right):{I}⟶\mathrm{Mnd}$
8 3 4 5 7 prds0g ${⊢}\left({R}\in \mathrm{Mnd}\wedge {I}\in {V}\right)\to {0}_{𝑔}\circ \left({I}×\left\{{R}\right\}\right)={0}_{\left(\mathrm{Scalar}\left({R}\right){⨉}_{𝑠}\left({I}×\left\{{R}\right\}\right)\right)}$
9 elex ${⊢}{R}\in \mathrm{Mnd}\to {R}\in \mathrm{V}$
10 9 ad2antrr ${⊢}\left(\left({R}\in \mathrm{Mnd}\wedge {I}\in {V}\right)\wedge {x}\in {I}\right)\to {R}\in \mathrm{V}$
11 fconstmpt ${⊢}{I}×\left\{{R}\right\}=\left({x}\in {I}⟼{R}\right)$
12 11 a1i ${⊢}\left({R}\in \mathrm{Mnd}\wedge {I}\in {V}\right)\to {I}×\left\{{R}\right\}=\left({x}\in {I}⟼{R}\right)$
13 fn0g ${⊢}{0}_{𝑔}Fn\mathrm{V}$
14 13 a1i ${⊢}\left({R}\in \mathrm{Mnd}\wedge {I}\in {V}\right)\to {0}_{𝑔}Fn\mathrm{V}$
15 dffn5 ${⊢}{0}_{𝑔}Fn\mathrm{V}↔{0}_{𝑔}=\left({r}\in \mathrm{V}⟼{0}_{{r}}\right)$
16 14 15 sylib ${⊢}\left({R}\in \mathrm{Mnd}\wedge {I}\in {V}\right)\to {0}_{𝑔}=\left({r}\in \mathrm{V}⟼{0}_{{r}}\right)$
17 fveq2 ${⊢}{r}={R}\to {0}_{{r}}={0}_{{R}}$
18 17 2 syl6eqr
19 10 12 16 18 fmptco
20 fconstmpt
21 19 20 syl6reqr
22 eqid ${⊢}\mathrm{Scalar}\left({R}\right)=\mathrm{Scalar}\left({R}\right)$
23 1 22 pwsval ${⊢}\left({R}\in \mathrm{Mnd}\wedge {I}\in {V}\right)\to {Y}=\mathrm{Scalar}\left({R}\right){⨉}_{𝑠}\left({I}×\left\{{R}\right\}\right)$
24 23 fveq2d ${⊢}\left({R}\in \mathrm{Mnd}\wedge {I}\in {V}\right)\to {0}_{{Y}}={0}_{\left(\mathrm{Scalar}\left({R}\right){⨉}_{𝑠}\left({I}×\left\{{R}\right\}\right)\right)}$
25 8 21 24 3eqtr4d