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 )