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 0 ˙ = 0 R
Assertion pws0g R Mnd I V I × 0 ˙ = 0 Y

Proof

Step Hyp Ref Expression
1 pwsmnd.y Y = R 𝑠 I
2 pws0g.z 0 ˙ = 0 R
3 eqid Scalar R 𝑠 I × R = Scalar R 𝑠 I × R
4 simpr R Mnd I V I V
5 fvexd R Mnd I V Scalar R V
6 fconst6g R Mnd I × R : I Mnd
7 6 adantr R Mnd I V I × R : I Mnd
8 3 4 5 7 prds0g R Mnd I V 0 𝑔 I × R = 0 Scalar R 𝑠 I × R
9 elex R Mnd R V
10 9 ad2antrr R Mnd I V x I R V
11 fconstmpt I × R = x I R
12 11 a1i R Mnd I V I × R = x I R
13 fn0g 0 𝑔 Fn V
14 13 a1i R Mnd I V 0 𝑔 Fn V
15 dffn5 0 𝑔 Fn V 0 𝑔 = r V 0 r
16 14 15 sylib R Mnd I V 0 𝑔 = r V 0 r
17 fveq2 r = R 0 r = 0 R
18 17 2 syl6eqr r = R 0 r = 0 ˙
19 10 12 16 18 fmptco R Mnd I V 0 𝑔 I × R = x I 0 ˙
20 fconstmpt I × 0 ˙ = x I 0 ˙
21 19 20 syl6reqr R Mnd I V I × 0 ˙ = 0 𝑔 I × R
22 eqid Scalar R = Scalar R
23 1 22 pwsval R Mnd I V Y = Scalar R 𝑠 I × R
24 23 fveq2d R Mnd I V 0 Y = 0 Scalar R 𝑠 I × R
25 8 21 24 3eqtr4d R Mnd I V I × 0 ˙ = 0 Y