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

Metamath Proof Explorer

Theorem pwslmod

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

Ref Expression
Hypothesis pwslmod.y ⊢ 𝑌 = ( 𝑅 ↑s 𝐼 )
Assertion pwslmod ( ( 𝑅 ∈ LMod ∧ 𝐼 ∈ 𝑉 ) → 𝑌 ∈ LMod )

Proof

Step Hyp Ref Expression
1 pwslmod.y ⊢ 𝑌 = ( 𝑅 ↑s 𝐼 )
2 eqid ⊢ ( Scalar ‘ 𝑅 ) = ( Scalar ‘ 𝑅 )
3 1 2 pwsval ⊢ ( ( 𝑅 ∈ LMod ∧ 𝐼 ∈ 𝑉 ) → 𝑌 = ( ( Scalar ‘ 𝑅 ) Xs ( 𝐼 × { 𝑅 } ) ) )
4 eqid ⊢ ( ( Scalar ‘ 𝑅 ) Xs ( 𝐼 × { 𝑅 } ) ) = ( ( Scalar ‘ 𝑅 ) Xs ( 𝐼 × { 𝑅 } ) )
5 2 lmodring ⊢ ( 𝑅 ∈ LMod → ( Scalar ‘ 𝑅 ) ∈ Ring )
6 5 adantr ⊢ ( ( 𝑅 ∈ LMod ∧ 𝐼 ∈ 𝑉 ) → ( Scalar ‘ 𝑅 ) ∈ Ring )
7 simpr ⊢ ( ( 𝑅 ∈ LMod ∧ 𝐼 ∈ 𝑉 ) → 𝐼 ∈ 𝑉 )
8 fconst6g ⊢ ( 𝑅 ∈ LMod → ( 𝐼 × { 𝑅 } ) : 𝐼 ⟶ LMod )
9 8 adantr ⊢ ( ( 𝑅 ∈ LMod ∧ 𝐼 ∈ 𝑉 ) → ( 𝐼 × { 𝑅 } ) : 𝐼 ⟶ LMod )
10 fvconst2g ⊢ ( ( 𝑅 ∈ LMod ∧ 𝑥 ∈ 𝐼 ) → ( ( 𝐼 × { 𝑅 } ) ‘ 𝑥 ) = 𝑅 )
11 10 adantlr ⊢ ( ( ( 𝑅 ∈ LMod ∧ 𝐼 ∈ 𝑉 ) ∧ 𝑥 ∈ 𝐼 ) → ( ( 𝐼 × { 𝑅 } ) ‘ 𝑥 ) = 𝑅 )
12 11 fveq2d ⊢ ( ( ( 𝑅 ∈ LMod ∧ 𝐼 ∈ 𝑉 ) ∧ 𝑥 ∈ 𝐼 ) → ( Scalar ‘ ( ( 𝐼 × { 𝑅 } ) ‘ 𝑥 ) ) = ( Scalar ‘ 𝑅 ) )
13 4 6 7 9 12 prdslmodd ⊢ ( ( 𝑅 ∈ LMod ∧ 𝐼 ∈ 𝑉 ) → ( ( Scalar ‘ 𝑅 ) Xs ( 𝐼 × { 𝑅 } ) ) ∈ LMod )
14 3 13 eqeltrd ⊢ ( ( 𝑅 ∈ LMod ∧ 𝐼 ∈ 𝑉 ) → 𝑌 ∈ LMod )