Definition df-lininds 42231

Description: Define the relation between a module and its linearly independent subsets. (Contributed by AV, 12-Apr-2019.) (Revised by AV, 24-Apr-2019.) (Revised by AV, 30-Jul-2019.)

Assertion

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 ) ) ) ) }

Distinct variable group:   f, m, s, x

Detailed syntax breakdown of Definition df-lininds

Step	Hyp	Ref	Expression
1		clininds 42229	. 2 class linIndS
2		vs	. . . . . 6 setvar s
3	2	cv 1482	. . . . 5 class s
4		vm	. . . . . . . 8 setvar m
5	4	cv 1482	. . . . . . 7 class m
6		cbs 15857	. . . . . . 7 class Base
7	5, 6	cfv 5888	. . . . . 6 class ( Base ` m )
8	7	cpw 4158	. . . . 5 class ~P ( Base ` m )
9	3, 8	wcel 1990	. . . 4 wff s e. ~P ( Base ` m )
10		vf	. . . . . . . . 9 setvar f
11	10	cv 1482	. . . . . . . 8 class f
12		csca 15944	. . . . . . . . . 10 class Scalar
13	5, 12	cfv 5888	. . . . . . . . 9 class (Scalar ` m )
14		c0g 16100	. . . . . . . . 9 class 0g
15	13, 14	cfv 5888	. . . . . . . 8 class ( 0g ` (Scalar ` m ) )
16		cfsupp 8275	. . . . . . . 8 class finSupp
17	11, 15, 16	wbr 4653	. . . . . . 7 wff f finSupp ( 0g ` (Scalar ` m ) )
18		clinc 42193	. . . . . . . . . 10 class linC
19	5, 18	cfv 5888	. . . . . . . . 9 class ( linC ` m )
20	11, 3, 19	co 6650	. . . . . . . 8 class ( f ( linC ` m ) s )
21	5, 14	cfv 5888	. . . . . . . 8 class ( 0g ` m )
22	20, 21	wceq 1483	. . . . . . 7 wff ( f ( linC ` m ) s ) = ( 0g ` m )
23	17, 22	wa 384	. . . . . 6 wff ( f finSupp ( 0g ` (Scalar ` m ) ) /\ ( f ( linC ` m ) s ) = ( 0g ` m ) )
24		vx	. . . . . . . . . 10 setvar x
25	24	cv 1482	. . . . . . . . 9 class x
26	25, 11	cfv 5888	. . . . . . . 8 class ( f ` x )
27	26, 15	wceq 1483	. . . . . . 7 wff ( f ` x ) = ( 0g ` (Scalar ` m ) )
28	27, 24, 3	wral 2912	. . . . . 6 wff A. x e. s ( f ` x ) = ( 0g ` (Scalar ` m ) )
29	23, 28	wi 4	. . . . 5 wff ( ( f finSupp ( 0g ` (Scalar ` m ) ) /\ ( f ( linC ` m ) s ) = ( 0g ` m ) ) -> A. x e. s ( f ` x ) = ( 0g ` (Scalar ` m ) ) )
30	13, 6	cfv 5888	. . . . . 6 class ( Base ` (Scalar ` m ) )
31		cmap 7857	. . . . . 6 class ^m
32	30, 3, 31	co 6650	. . . . 5 class ( ( Base ` (Scalar ` m ) ) ^m s )
33	29, 10, 32	wral 2912	. . . 4 wff 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 ) ) )
34	9, 33	wa 384	. . 3 wff ( 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 ) ) ) )
35	34, 2, 4	copab 4712	. 2 class { <. 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 ) ) ) ) }
36	1, 35	wceq 1483	1 wff 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 ) ) ) ) }

This definition is referenced by:  rellininds  42232  islininds  42235