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

Metamath Proof Explorer

Theorem frlmbasfsupp

Description: Elements of the free module are finitely supported. (Contributed by Stefan O'Rear, 3-Feb-2015) (Revised by Thierry Arnoux, 21-Jun-2019) (Proof shortened by AV, 20-Jul-2019)

		Ref	Expression
	Hypotheses	frlmval.f	$⊢ F = R freeLMod I$
		frlmbasfsupp.z	$⊢ \underset{˙}{0} = 0_{R}$
		frlmbasfsupp.b	$⊢ B = {Base}_{F}$
	Assertion	frlmbasfsupp	$⊢ (I \in W \land X \in B) \to {finSupp}_{\underset{˙}{0}} (X)$

Proof

Step	Hyp	Ref	Expression
1		frlmval.f	$⊢ F = R freeLMod I$
2		frlmbasfsupp.z	$⊢ \underset{˙}{0} = 0_{R}$
3		frlmbasfsupp.b	$⊢ B = {Base}_{F}$
4		simpr	$⊢ (I \in W \land X \in B) \to X \in B$
5	1 3	frlmrcl	$⊢ X \in B \to R \in V$
6		simpl	$⊢ (I \in W \land X \in B) \to I \in W$
7		eqid	$⊢ {Base}_{R} = {Base}_{R}$
8	1 7 2 3	frlmelbas	$⊢ (R \in V \land I \in W) \to (X \in B \leftrightarrow (X \in ({Base}_{R}^{I}) \land {finSupp}_{\underset{˙}{0}} (X)))$
9	5 6 8	syl2an2	$⊢ (I \in W \land X \in B) \to (X \in B \leftrightarrow (X \in ({Base}_{R}^{I}) \land {finSupp}_{\underset{˙}{0}} (X)))$
10	4 9	mpbid	$⊢ (I \in W \land X \in B) \to (X \in ({Base}_{R}^{I}) \land {finSupp}_{\underset{˙}{0}} (X))$
11	10	simprd	$⊢ (I \in W \land X \in B) \to {finSupp}_{\underset{˙}{0}} (X)$