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 ⊢ Y = R ↑ 𝑠 I
Assertion pwslmod ⊢ R ∈ LMod ∧ I ∈ V → Y ∈ LMod

Proof

Step Hyp Ref Expression
1 pwslmod.y ⊢ Y = R ↑ 𝑠 I
2 eqid ⊢ Scalar ⁡ R = Scalar ⁡ R
3 1 2 pwsval ⊢ R ∈ LMod ∧ I ∈ V → Y = Scalar ⁡ R ⨉ 𝑠 I × R
4 eqid ⊢ Scalar ⁡ R ⨉ 𝑠 I × R = Scalar ⁡ R ⨉ 𝑠 I × R
5 2 lmodring ⊢ R ∈ LMod → Scalar ⁡ R ∈ Ring
6 5 adantr ⊢ R ∈ LMod ∧ I ∈ V → Scalar ⁡ R ∈ Ring
7 simpr ⊢ R ∈ LMod ∧ I ∈ V → I ∈ V
8 fconst6g ⊢ R ∈ LMod → I × R : I ⟶ LMod
9 8 adantr ⊢ R ∈ LMod ∧ I ∈ V → I × R : I ⟶ LMod
10 fvconst2g ⊢ R ∈ LMod ∧ x ∈ I → I × R ⁡ x = R
11 10 adantlr ⊢ R ∈ LMod ∧ I ∈ V ∧ x ∈ I → I × R ⁡ x = R
12 11 fveq2d ⊢ R ∈ LMod ∧ I ∈ V ∧ x ∈ I → Scalar ⁡ I × R ⁡ x = Scalar ⁡ R
13 4 6 7 9 12 prdslmodd ⊢ R ∈ LMod ∧ I ∈ V → Scalar ⁡ R ⨉ 𝑠 I × R ∈ LMod
14 3 13 eqeltrd ⊢ R ∈ LMod ∧ I ∈ V → Y ∈ LMod