Metamath Proof Explorer


Definition df-lininds

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)

Ref Expression
Assertion df-lininds linIndS=sm|s𝒫BasemfBaseScalarmsfinSupp0ScalarmfflinCms=0mxsfx=0Scalarm

Detailed syntax breakdown

Step Hyp Ref Expression
0 clininds classlinIndS
1 vs setvars
2 vm setvarm
3 1 cv setvars
4 cbs classBase
5 2 cv setvarm
6 5 4 cfv classBasem
7 6 cpw class𝒫Basem
8 3 7 wcel wffs𝒫Basem
9 vf setvarf
10 csca classScalar
11 5 10 cfv classScalarm
12 11 4 cfv classBaseScalarm
13 cmap class𝑚
14 12 3 13 co classBaseScalarms
15 9 cv setvarf
16 cfsupp classfinSupp
17 c0g class0𝑔
18 11 17 cfv class0Scalarm
19 15 18 16 wbr wfffinSupp0Scalarmf
20 clinc classlinC
21 5 20 cfv classlinCm
22 15 3 21 co classflinCms
23 5 17 cfv class0m
24 22 23 wceq wffflinCms=0m
25 19 24 wa wfffinSupp0ScalarmfflinCms=0m
26 vx setvarx
27 26 cv setvarx
28 27 15 cfv classfx
29 28 18 wceq wfffx=0Scalarm
30 29 26 3 wral wffxsfx=0Scalarm
31 25 30 wi wfffinSupp0ScalarmfflinCms=0mxsfx=0Scalarm
32 31 9 14 wral wfffBaseScalarmsfinSupp0ScalarmfflinCms=0mxsfx=0Scalarm
33 8 32 wa wffs𝒫BasemfBaseScalarmsfinSupp0ScalarmfflinCms=0mxsfx=0Scalarm
34 33 1 2 copab classsm|s𝒫BasemfBaseScalarmsfinSupp0ScalarmfflinCms=0mxsfx=0Scalarm
35 0 34 wceq wfflinIndS=sm|s𝒫BasemfBaseScalarmsfinSupp0ScalarmfflinCms=0mxsfx=0Scalarm