Metamath Proof Explorer

Theorem rellininds

Description: The class defining the relation between a module and its linearly independent subsets is a relation. (Contributed by AV, 13-Apr-2019)

		Ref	Expression
	Assertion	rellininds	\|- Rel linIndS

Proof

Step	Hyp	Ref	Expression
1		df-lininds	\|- linIndS = { <. s , m >. \| ( s e. ~P ( Base ` m ) /\ A. f e. ( ( Base ` ( Scalar ` m ) ) ^m s ) ( ( f finSupp ( 0g ` ( Scalar ` m ) ) /\ ( f ( linC ` m ) s ) = ( 0g ` m ) ) -> A. x e. s ( f ` x ) = ( 0g ` ( Scalar ` m ) ) ) ) }
2	1	relopabiv	\|- Rel linIndS

Step

Hyp

Ref

Expression

df-lininds

 |-  linIndS = { <. s , m >. | ( s e. ~P ( Base ` m ) /\ A. f e. ( ( Base ` ( Scalar ` m ) ) ^m s ) ( ( f finSupp ( 0g ` ( Scalar ` m ) ) /\ ( f ( linC ` m ) s ) = ( 0g ` m ) ) -> A. x e. s ( f ` x ) = ( 0g ` ( Scalar ` m ) ) ) ) }

relopabiv

 |-  Rel linIndS