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 \in LMod \land I \in V) \to Y \in LMod$

Step	Hyp	Ref	Expression
1		pwslmod.y	$⊢ Y = R ↑_{𝑠} I$
2		eqid	$⊢ Scalar (R) = Scalar (R)$
3	1 2	pwsval	$⊢ (R \in LMod \land I \in V) \to Y = Scalar (R) ⨉_{𝑠} (I \times \{R\})$
4		eqid	$⊢ Scalar (R) ⨉_{𝑠} (I \times \{R\}) = Scalar (R) ⨉_{𝑠} (I \times \{R\})$
5	2	lmodring	$⊢ R \in LMod \to Scalar (R) \in Ring$
6	5	adantr	$⊢ (R \in LMod \land I \in V) \to Scalar (R) \in Ring$
7		simpr	$⊢ (R \in LMod \land I \in V) \to I \in V$
8		fconst6g	$⊢ R \in LMod \to (I \times \{R\}) : I ⟶ LMod$
9	8	adantr	$⊢ (R \in LMod \land I \in V) \to (I \times \{R\}) : I ⟶ LMod$
10		fvconst2g	$⊢ (R \in LMod \land x \in I) \to (I \times \{R\}) (x) = R$
11	10	adantlr	$⊢ ((R \in LMod \land I \in V) \land x \in I) \to (I \times \{R\}) (x) = R$
12	11	fveq2d	$⊢ ((R \in LMod \land I \in V) \land x \in I) \to Scalar ((I \times \{R\}) (x)) = Scalar (R)$
13	4 6 7 9 12	prdslmodd	$⊢ (R \in LMod \land I \in V) \to Scalar (R) ⨉_{𝑠} (I \times \{R\}) \in LMod$
14	3 13	eqeltrd	$⊢ (R \in LMod \land I \in V) \to Y \in LMod$

Metamath Proof Explorer