Definition df-lindeps

Description: Define the relation between a module and its linearly dependent subsets. (Contributed by AV, 26-Apr-2019)

	Ref	Expression
Assertion	df-lindeps	⊢ linDepS = { ⟨ 𝑠 , 𝑚 ⟩ ∣ ¬ 𝑠 linIndS 𝑚 }

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		clindeps	⊢ linDepS
1		vs	⊢ 𝑠
2		vm	⊢ 𝑚
3	1	cv	⊢ 𝑠
4		clininds	⊢ linIndS
5	2	cv	⊢ 𝑚
6	3 5 4	wbr	⊢ 𝑠 linIndS 𝑚
7	6	wn	⊢ ¬ 𝑠 linIndS 𝑚
8	7 1 2	copab	⊢ { ⟨ 𝑠 , 𝑚 ⟩ ∣ ¬ 𝑠 linIndS 𝑚 }
9	0 8	wceq	⊢ linDepS = { ⟨ 𝑠 , 𝑚 ⟩ ∣ ¬ 𝑠 linIndS 𝑚 }