Metamath Proof Explorer


Theorem pws0g

Description: Zero in a structure power of a monoid. (Contributed by Mario Carneiro, 11-Jan-2015)

Ref Expression
Hypotheses pwsmnd.y Y=R𝑠I
pws0g.z 0˙=0R
Assertion pws0g RMndIVI×0˙=0Y

Proof

Step Hyp Ref Expression
1 pwsmnd.y Y=R𝑠I
2 pws0g.z 0˙=0R
3 eqid ScalarR𝑠I×R=ScalarR𝑠I×R
4 simpr RMndIVIV
5 fvexd RMndIVScalarRV
6 fconst6g RMndI×R:IMnd
7 6 adantr RMndIVI×R:IMnd
8 3 4 5 7 prds0g RMndIV0𝑔I×R=0ScalarR𝑠I×R
9 fconstmpt I×0˙=xI0˙
10 elex RMndRV
11 10 ad2antrr RMndIVxIRV
12 fconstmpt I×R=xIR
13 12 a1i RMndIVI×R=xIR
14 fn0g 0𝑔FnV
15 14 a1i RMndIV0𝑔FnV
16 dffn5 0𝑔FnV0𝑔=rV0r
17 15 16 sylib RMndIV0𝑔=rV0r
18 fveq2 r=R0r=0R
19 18 2 eqtr4di r=R0r=0˙
20 11 13 17 19 fmptco RMndIV0𝑔I×R=xI0˙
21 9 20 eqtr4id RMndIVI×0˙=0𝑔I×R
22 eqid ScalarR=ScalarR
23 1 22 pwsval RMndIVY=ScalarR𝑠I×R
24 23 fveq2d RMndIV0Y=0ScalarR𝑠I×R
25 8 21 24 3eqtr4d RMndIVI×0˙=0Y