# Metamath Proof Explorer

## Theorem pwsgrp

Description: A structure power of a group is a group. (Contributed by Mario Carneiro, 11-Jan-2015)

Ref Expression
Hypothesis pwsgrp.y ${⊢}{Y}={R}{↑}_{𝑠}{I}$
Assertion pwsgrp ${⊢}\left({R}\in \mathrm{Grp}\wedge {I}\in {V}\right)\to {Y}\in \mathrm{Grp}$

### Proof

Step Hyp Ref Expression
1 pwsgrp.y ${⊢}{Y}={R}{↑}_{𝑠}{I}$
2 eqid ${⊢}\mathrm{Scalar}\left({R}\right)=\mathrm{Scalar}\left({R}\right)$
3 1 2 pwsval ${⊢}\left({R}\in \mathrm{Grp}\wedge {I}\in {V}\right)\to {Y}=\mathrm{Scalar}\left({R}\right){⨉}_{𝑠}\left({I}×\left\{{R}\right\}\right)$
4 eqid ${⊢}\mathrm{Scalar}\left({R}\right){⨉}_{𝑠}\left({I}×\left\{{R}\right\}\right)=\mathrm{Scalar}\left({R}\right){⨉}_{𝑠}\left({I}×\left\{{R}\right\}\right)$
5 simpr ${⊢}\left({R}\in \mathrm{Grp}\wedge {I}\in {V}\right)\to {I}\in {V}$
6 fvexd ${⊢}\left({R}\in \mathrm{Grp}\wedge {I}\in {V}\right)\to \mathrm{Scalar}\left({R}\right)\in \mathrm{V}$
7 fconst6g ${⊢}{R}\in \mathrm{Grp}\to \left({I}×\left\{{R}\right\}\right):{I}⟶\mathrm{Grp}$
8 7 adantr ${⊢}\left({R}\in \mathrm{Grp}\wedge {I}\in {V}\right)\to \left({I}×\left\{{R}\right\}\right):{I}⟶\mathrm{Grp}$
9 4 5 6 8 prdsgrpd ${⊢}\left({R}\in \mathrm{Grp}\wedge {I}\in {V}\right)\to \mathrm{Scalar}\left({R}\right){⨉}_{𝑠}\left({I}×\left\{{R}\right\}\right)\in \mathrm{Grp}$
10 3 9 eqeltrd ${⊢}\left({R}\in \mathrm{Grp}\wedge {I}\in {V}\right)\to {Y}\in \mathrm{Grp}$