frlmlss

Description: The base set of the free module is a subspace of the power module. (Contributed by Stefan O'Rear, 1-Feb-2015)

	Ref	Expression
Hypotheses	frlmval.f	$⊢ F = R freeLMod I$
	frlmpws.b	$⊢ B = {Base}_{F}$
	frlmlss.u	$⊢ U = LSubSp (ringLMod (R) ↑_{𝑠} I)$
Assertion	frlmlss	$⊢ (R \in Ring \land I \in W) \to B \in U$

Proof

Step	Hyp	Ref	Expression
1		frlmval.f	$⊢ F = R freeLMod I$
2		frlmpws.b	$⊢ B = {Base}_{F}$
3		frlmlss.u	$⊢ U = LSubSp (ringLMod (R) ↑_{𝑠} I)$
4	1	frlmval	$⊢ (R \in Ring \land I \in W) \to F = R \oplus_{m} (I \times \{ringLMod (R)\})$
5	4	fveq2d	$⊢ (R \in Ring \land I \in W) \to {Base}_{F} = {Base}_{(R \oplus_{m} (I \times \{ringLMod (R)\}))}$
6	2 5	eqtrid	$⊢ (R \in Ring \land I \in W) \to B = {Base}_{(R \oplus_{m} (I \times \{ringLMod (R)\}))}$
7		simpr	$⊢ (R \in Ring \land I \in W) \to I \in W$
8		simpl	$⊢ (R \in Ring \land I \in W) \to R \in Ring$
9		rlmlmod	$⊢ R \in Ring \to ringLMod (R) \in LMod$
10	9	adantr	$⊢ (R \in Ring \land I \in W) \to ringLMod (R) \in LMod$
11		fconst6g	$⊢ ringLMod (R) \in LMod \to (I \times \{ringLMod (R)\}) : I ⟶ LMod$
12	10 11	syl	$⊢ (R \in Ring \land I \in W) \to (I \times \{ringLMod (R)\}) : I ⟶ LMod$
13		fvex	$⊢ ringLMod (R) \in V$
14	13	fvconst2	$⊢ i \in I \to (I \times \{ringLMod (R)\}) (i) = ringLMod (R)$
15	14	adantl	$⊢ ((R \in Ring \land I \in W) \land i \in I) \to (I \times \{ringLMod (R)\}) (i) = ringLMod (R)$
16	15	fveq2d	$⊢ ((R \in Ring \land I \in W) \land i \in I) \to Scalar ((I \times \{ringLMod (R)\}) (i)) = Scalar (ringLMod (R))$
17		rlmsca	$⊢ R \in Ring \to R = Scalar (ringLMod (R))$
18	17	ad2antrr	$⊢ ((R \in Ring \land I \in W) \land i \in I) \to R = Scalar (ringLMod (R))$
19	16 18	eqtr4d	$⊢ ((R \in Ring \land I \in W) \land i \in I) \to Scalar ((I \times \{ringLMod (R)\}) (i)) = R$
20		eqid	$⊢ R ⨉_{𝑠} (I \times \{ringLMod (R)\}) = R ⨉_{𝑠} (I \times \{ringLMod (R)\})$
21		eqid	$⊢ LSubSp (R ⨉_{𝑠} (I \times \{ringLMod (R)\})) = LSubSp (R ⨉_{𝑠} (I \times \{ringLMod (R)\}))$
22		eqid	$⊢ {Base}_{(R \oplus_{m} (I \times \{ringLMod (R)\}))} = {Base}_{(R \oplus_{m} (I \times \{ringLMod (R)\}))}$
23	7 8 12 19 20 21 22	dsmmlss	$⊢ (R \in Ring \land I \in W) \to {Base}_{(R \oplus_{m} (I \times \{ringLMod (R)\}))} \in LSubSp (R ⨉_{𝑠} (I \times \{ringLMod (R)\}))$
24		eqid	$⊢ ringLMod (R) ↑_{𝑠} I = ringLMod (R) ↑_{𝑠} I$
25		eqid	$⊢ Scalar (ringLMod (R)) = Scalar (ringLMod (R))$
26	24 25	pwsval	$⊢ (ringLMod (R) \in V \land I \in W) \to ringLMod (R) ↑_{𝑠} I = Scalar (ringLMod (R)) ⨉_{𝑠} (I \times \{ringLMod (R)\})$
27	13 26	mpan	$⊢ I \in W \to ringLMod (R) ↑_{𝑠} I = Scalar (ringLMod (R)) ⨉_{𝑠} (I \times \{ringLMod (R)\})$
28	27	adantl	$⊢ (R \in Ring \land I \in W) \to ringLMod (R) ↑_{𝑠} I = Scalar (ringLMod (R)) ⨉_{𝑠} (I \times \{ringLMod (R)\})$
29	17	eqcomd	$⊢ R \in Ring \to Scalar (ringLMod (R)) = R$
30	29	adantr	$⊢ (R \in Ring \land I \in W) \to Scalar (ringLMod (R)) = R$
31	30	oveq1d	$⊢ (R \in Ring \land I \in W) \to Scalar (ringLMod (R)) ⨉_{𝑠} (I \times \{ringLMod (R)\}) = R ⨉_{𝑠} (I \times \{ringLMod (R)\})$
32	28 31	eqtr2d	$⊢ (R \in Ring \land I \in W) \to R ⨉_{𝑠} (I \times \{ringLMod (R)\}) = ringLMod (R) ↑_{𝑠} I$
33	32	fveq2d	$⊢ (R \in Ring \land I \in W) \to LSubSp (R ⨉_{𝑠} (I \times \{ringLMod (R)\})) = LSubSp (ringLMod (R) ↑_{𝑠} I)$
34	33 3	eqtr4di	$⊢ (R \in Ring \land I \in W) \to LSubSp (R ⨉_{𝑠} (I \times \{ringLMod (R)\})) = U$
35	23 34	eleqtrd	$⊢ (R \in Ring \land I \in W) \to {Base}_{(R \oplus_{m} (I \times \{ringLMod (R)\}))} \in U$
36	6 35	eqeltrd	$⊢ (R \in Ring \land I \in W) \to B \in U$

Metamath Proof Explorer

Theorem frlmlss

Proof