Theorem lindslininds

Description: Equivalence of definitions df-linds and df-lininds for (linear) independence for (left) modules. (Contributed by AV, 26-Apr-2019) (Proof shortened by AV, 30-Jul-2019)

	Ref	Expression
Assertion	lindslininds	⊢ ( ( 𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod ) → ( 𝑆 linIndS 𝑀 ↔ 𝑆 ∈ ( LIndS ‘ 𝑀 ) ) )

Proof

Step	Hyp	Ref	Expression
1		eqid	⊢ ( Scalar ‘ 𝑀 ) = ( Scalar ‘ 𝑀 )
2		eqid	⊢ ( Base ‘ ( Scalar ‘ 𝑀 ) ) = ( Base ‘ ( Scalar ‘ 𝑀 ) )
3		eqid	⊢ ( 0g ‘ ( Scalar ‘ 𝑀 ) ) = ( 0g ‘ ( Scalar ‘ 𝑀 ) )
4		eqid	⊢ ( 0g ‘ 𝑀 ) = ( 0g ‘ 𝑀 )
5	1 2 3 4	lindslinindsimp1	⊢ ( ( 𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod ) → ( ( 𝑆 ∈ 𝒫 ( Base ‘ 𝑀 ) ∧ ∀ 𝑓 ∈ ( ( Base ‘ ( Scalar ‘ 𝑀 ) ) ↑m 𝑆 ) ( ( 𝑓 finSupp ( 0g ‘ ( Scalar ‘ 𝑀 ) ) ∧ ( 𝑓 ( linC ‘ 𝑀 ) 𝑆 ) = ( 0g ‘ 𝑀 ) ) → ∀ 𝑥 ∈ 𝑆 ( 𝑓 ‘ 𝑥 ) = ( 0g ‘ ( Scalar ‘ 𝑀 ) ) ) ) → ( 𝑆 ⊆ ( Base ‘ 𝑀 ) ∧ ∀ 𝑠 ∈ 𝑆 ∀ 𝑔 ∈ ( ( Base ‘ ( Scalar ‘ 𝑀 ) ) ∖ { ( 0g ‘ ( Scalar ‘ 𝑀 ) ) } ) ¬ ( 𝑔 ( ·𝑠 ‘ 𝑀 ) 𝑠 ) ∈ ( ( LSpan ‘ 𝑀 ) ‘ ( 𝑆 ∖ { 𝑠 } ) ) ) ) )
6	1 2 3 4	lindslinindsimp2	⊢ ( ( 𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod ) → ( ( 𝑆 ⊆ ( Base ‘ 𝑀 ) ∧ ∀ 𝑠 ∈ 𝑆 ∀ 𝑔 ∈ ( ( Base ‘ ( Scalar ‘ 𝑀 ) ) ∖ { ( 0g ‘ ( Scalar ‘ 𝑀 ) ) } ) ¬ ( 𝑔 ( ·𝑠 ‘ 𝑀 ) 𝑠 ) ∈ ( ( LSpan ‘ 𝑀 ) ‘ ( 𝑆 ∖ { 𝑠 } ) ) ) → ( 𝑆 ∈ 𝒫 ( Base ‘ 𝑀 ) ∧ ∀ 𝑓 ∈ ( ( Base ‘ ( Scalar ‘ 𝑀 ) ) ↑m 𝑆 ) ( ( 𝑓 finSupp ( 0g ‘ ( Scalar ‘ 𝑀 ) ) ∧ ( 𝑓 ( linC ‘ 𝑀 ) 𝑆 ) = ( 0g ‘ 𝑀 ) ) → ∀ 𝑥 ∈ 𝑆 ( 𝑓 ‘ 𝑥 ) = ( 0g ‘ ( Scalar ‘ 𝑀 ) ) ) ) ) )
7	5 6	impbid	⊢ ( ( 𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod ) → ( ( 𝑆 ∈ 𝒫 ( Base ‘ 𝑀 ) ∧ ∀ 𝑓 ∈ ( ( Base ‘ ( Scalar ‘ 𝑀 ) ) ↑m 𝑆 ) ( ( 𝑓 finSupp ( 0g ‘ ( Scalar ‘ 𝑀 ) ) ∧ ( 𝑓 ( linC ‘ 𝑀 ) 𝑆 ) = ( 0g ‘ 𝑀 ) ) → ∀ 𝑥 ∈ 𝑆 ( 𝑓 ‘ 𝑥 ) = ( 0g ‘ ( Scalar ‘ 𝑀 ) ) ) ) ↔ ( 𝑆 ⊆ ( Base ‘ 𝑀 ) ∧ ∀ 𝑠 ∈ 𝑆 ∀ 𝑔 ∈ ( ( Base ‘ ( Scalar ‘ 𝑀 ) ) ∖ { ( 0g ‘ ( Scalar ‘ 𝑀 ) ) } ) ¬ ( 𝑔 ( ·𝑠 ‘ 𝑀 ) 𝑠 ) ∈ ( ( LSpan ‘ 𝑀 ) ‘ ( 𝑆 ∖ { 𝑠 } ) ) ) ) )
8		eqid	⊢ ( Base ‘ 𝑀 ) = ( Base ‘ 𝑀 )
9	8 4 1 2 3	islininds	⊢ ( ( 𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod ) → ( 𝑆 linIndS 𝑀 ↔ ( 𝑆 ∈ 𝒫 ( Base ‘ 𝑀 ) ∧ ∀ 𝑓 ∈ ( ( Base ‘ ( Scalar ‘ 𝑀 ) ) ↑m 𝑆 ) ( ( 𝑓 finSupp ( 0g ‘ ( Scalar ‘ 𝑀 ) ) ∧ ( 𝑓 ( linC ‘ 𝑀 ) 𝑆 ) = ( 0g ‘ 𝑀 ) ) → ∀ 𝑥 ∈ 𝑆 ( 𝑓 ‘ 𝑥 ) = ( 0g ‘ ( Scalar ‘ 𝑀 ) ) ) ) ) )
10		eqid	⊢ ( ·𝑠 ‘ 𝑀 ) = ( ·𝑠 ‘ 𝑀 )
11		eqid	⊢ ( LSpan ‘ 𝑀 ) = ( LSpan ‘ 𝑀 )
12	8 10 11 1 2 3	islinds2	⊢ ( 𝑀 ∈ LMod → ( 𝑆 ∈ ( LIndS ‘ 𝑀 ) ↔ ( 𝑆 ⊆ ( Base ‘ 𝑀 ) ∧ ∀ 𝑠 ∈ 𝑆 ∀ 𝑔 ∈ ( ( Base ‘ ( Scalar ‘ 𝑀 ) ) ∖ { ( 0g ‘ ( Scalar ‘ 𝑀 ) ) } ) ¬ ( 𝑔 ( ·𝑠 ‘ 𝑀 ) 𝑠 ) ∈ ( ( LSpan ‘ 𝑀 ) ‘ ( 𝑆 ∖ { 𝑠 } ) ) ) ) )
13	12	adantl	⊢ ( ( 𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod ) → ( 𝑆 ∈ ( LIndS ‘ 𝑀 ) ↔ ( 𝑆 ⊆ ( Base ‘ 𝑀 ) ∧ ∀ 𝑠 ∈ 𝑆 ∀ 𝑔 ∈ ( ( Base ‘ ( Scalar ‘ 𝑀 ) ) ∖ { ( 0g ‘ ( Scalar ‘ 𝑀 ) ) } ) ¬ ( 𝑔 ( ·𝑠 ‘ 𝑀 ) 𝑠 ) ∈ ( ( LSpan ‘ 𝑀 ) ‘ ( 𝑆 ∖ { 𝑠 } ) ) ) ) )
14	7 9 13	3bitr4d	⊢ ( ( 𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod ) → ( 𝑆 linIndS 𝑀 ↔ 𝑆 ∈ ( LIndS ‘ 𝑀 ) ) )