This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ⊢ 𝑌 = ( 𝑅 ↑s 𝐼 )
Assertion pwsgrp ( ( 𝑅 ∈ Grp ∧ 𝐼 ∈ 𝑉 ) → 𝑌 ∈ Grp )

Proof

Step Hyp Ref Expression
1 pwsgrp.y ⊢ 𝑌 = ( 𝑅 ↑s 𝐼 )
2 eqid ⊢ ( Scalar ‘ 𝑅 ) = ( Scalar ‘ 𝑅 )
3 1 2 pwsval ⊢ ( ( 𝑅 ∈ Grp ∧ 𝐼 ∈ 𝑉 ) → 𝑌 = ( ( Scalar ‘ 𝑅 ) Xs ( 𝐼 × { 𝑅 } ) ) )
4 eqid ⊢ ( ( Scalar ‘ 𝑅 ) Xs ( 𝐼 × { 𝑅 } ) ) = ( ( Scalar ‘ 𝑅 ) Xs ( 𝐼 × { 𝑅 } ) )
5 simpr ⊢ ( ( 𝑅 ∈ Grp ∧ 𝐼 ∈ 𝑉 ) → 𝐼 ∈ 𝑉 )
6 fvexd ⊢ ( ( 𝑅 ∈ Grp ∧ 𝐼 ∈ 𝑉 ) → ( Scalar ‘ 𝑅 ) ∈ V )
7 fconst6g ⊢ ( 𝑅 ∈ Grp → ( 𝐼 × { 𝑅 } ) : 𝐼 ⟶ Grp )
8 7 adantr ⊢ ( ( 𝑅 ∈ Grp ∧ 𝐼 ∈ 𝑉 ) → ( 𝐼 × { 𝑅 } ) : 𝐼 ⟶ Grp )
9 4 5 6 8 prdsgrpd ⊢ ( ( 𝑅 ∈ Grp ∧ 𝐼 ∈ 𝑉 ) → ( ( Scalar ‘ 𝑅 ) Xs ( 𝐼 × { 𝑅 } ) ) ∈ Grp )
10 3 9 eqeltrd ⊢ ( ( 𝑅 ∈ Grp ∧ 𝐼 ∈ 𝑉 ) → 𝑌 ∈ Grp )