Metamath Proof Explorer


Theorem pws1

Description: Value of the ring unit in a structure power. (Contributed by Mario Carneiro, 11-Mar-2015)

Ref Expression
Hypotheses pws1.y Y=R𝑠I
pws1.o 1˙=1R
Assertion pws1 RRingIVI×1˙=1Y

Proof

Step Hyp Ref Expression
1 pws1.y Y=R𝑠I
2 pws1.o 1˙=1R
3 eqid ScalarR=ScalarR
4 1 3 pwsval RRingIVY=ScalarR𝑠I×R
5 4 fveq2d RRingIV1Y=1ScalarR𝑠I×R
6 eqid ScalarR𝑠I×R=ScalarR𝑠I×R
7 simpr RRingIVIV
8 fvexd RRingIVScalarRV
9 fconst6g RRingI×R:IRing
10 9 adantr RRingIVI×R:IRing
11 6 7 8 10 prds1 RRingIV1rI×R=1ScalarR𝑠I×R
12 fn0g 0𝑔FnV
13 fnmgp mulGrpFnV
14 ssv ranmulGrpV
15 14 a1i RRingIVranmulGrpV
16 fnco 0𝑔FnVmulGrpFnVranmulGrpV0𝑔mulGrpFnV
17 12 13 15 16 mp3an12i RRingIV0𝑔mulGrpFnV
18 df-ur 1r=0𝑔mulGrp
19 18 fneq1i 1rFnV0𝑔mulGrpFnV
20 17 19 sylibr RRingIV1rFnV
21 elex RRingRV
22 21 adantr RRingIVRV
23 fcoconst 1rFnVRV1rI×R=I×1R
24 20 22 23 syl2anc RRingIV1rI×R=I×1R
25 2 sneqi 1˙=1R
26 25 xpeq2i I×1˙=I×1R
27 24 26 eqtr4di RRingIV1rI×R=I×1˙
28 5 11 27 3eqtr2rd RRingIVI×1˙=1Y