Theorem linindscl

Description: A linearly independent set is a subset of (the base set of) a module. (Contributed by AV, 13-Apr-2019)

	Ref	Expression
Assertion	linindscl	⊢ ( 𝑆 linIndS 𝑀 → 𝑆 ∈ 𝒫 ( Base ‘ 𝑀 ) )

Proof

Step	Hyp	Ref	Expression
1		eqid	⊢ ( Base ‘ 𝑀 ) = ( Base ‘ 𝑀 )
2		eqid	⊢ ( 0g ‘ 𝑀 ) = ( 0g ‘ 𝑀 )
3		eqid	⊢ ( Scalar ‘ 𝑀 ) = ( Scalar ‘ 𝑀 )
4		eqid	⊢ ( Base ‘ ( Scalar ‘ 𝑀 ) ) = ( Base ‘ ( Scalar ‘ 𝑀 ) )
5		eqid	⊢ ( 0g ‘ ( Scalar ‘ 𝑀 ) ) = ( 0g ‘ ( Scalar ‘ 𝑀 ) )
6	1 2 3 4 5	linindsi	⊢ ( 𝑆 linIndS 𝑀 → ( 𝑆 ∈ 𝒫 ( Base ‘ 𝑀 ) ∧ ∀ 𝑓 ∈ ( ( Base ‘ ( Scalar ‘ 𝑀 ) ) ↑m 𝑆 ) ( ( 𝑓 finSupp ( 0g ‘ ( Scalar ‘ 𝑀 ) ) ∧ ( 𝑓 ( linC ‘ 𝑀 ) 𝑆 ) = ( 0g ‘ 𝑀 ) ) → ∀ 𝑥 ∈ 𝑆 ( 𝑓 ‘ 𝑥 ) = ( 0g ‘ ( Scalar ‘ 𝑀 ) ) ) ) )
7	6	simpld	⊢ ( 𝑆 linIndS 𝑀 → 𝑆 ∈ 𝒫 ( Base ‘ 𝑀 ) )