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 = { ⟨ 𝑠 , 𝑚 ⟩ ∣ ( 𝑠 ∈ 𝒫 ( Base ‘ 𝑚 ) ∧ ∀ 𝑓 ∈ ( ( Base ‘ ( Scalar ‘ 𝑚 ) ) ↑m 𝑠 ) ( ( 𝑓 finSupp ( 0g ‘ ( Scalar ‘ 𝑚 ) ) ∧ ( 𝑓 ( linC ‘ 𝑚 ) 𝑠 ) = ( 0g𝑚 ) ) → ∀ 𝑥𝑠 ( 𝑓𝑥 ) = ( 0g ‘ ( Scalar ‘ 𝑚 ) ) ) ) }

Detailed syntax breakdown

Step Hyp Ref Expression
0 clininds linIndS
1 vs 𝑠
2 vm 𝑚
3 1 cv 𝑠
4 cbs Base
5 2 cv 𝑚
6 5 4 cfv ( Base ‘ 𝑚 )
7 6 cpw 𝒫 ( Base ‘ 𝑚 )
8 3 7 wcel 𝑠 ∈ 𝒫 ( Base ‘ 𝑚 )
9 vf 𝑓
10 csca Scalar
11 5 10 cfv ( Scalar ‘ 𝑚 )
12 11 4 cfv ( Base ‘ ( Scalar ‘ 𝑚 ) )
13 cmap m
14 12 3 13 co ( ( Base ‘ ( Scalar ‘ 𝑚 ) ) ↑m 𝑠 )
15 9 cv 𝑓
16 cfsupp finSupp
17 c0g 0g
18 11 17 cfv ( 0g ‘ ( Scalar ‘ 𝑚 ) )
19 15 18 16 wbr 𝑓 finSupp ( 0g ‘ ( Scalar ‘ 𝑚 ) )
20 clinc linC
21 5 20 cfv ( linC ‘ 𝑚 )
22 15 3 21 co ( 𝑓 ( linC ‘ 𝑚 ) 𝑠 )
23 5 17 cfv ( 0g𝑚 )
24 22 23 wceq ( 𝑓 ( linC ‘ 𝑚 ) 𝑠 ) = ( 0g𝑚 )
25 19 24 wa ( 𝑓 finSupp ( 0g ‘ ( Scalar ‘ 𝑚 ) ) ∧ ( 𝑓 ( linC ‘ 𝑚 ) 𝑠 ) = ( 0g𝑚 ) )
26 vx 𝑥
27 26 cv 𝑥
28 27 15 cfv ( 𝑓𝑥 )
29 28 18 wceq ( 𝑓𝑥 ) = ( 0g ‘ ( Scalar ‘ 𝑚 ) )
30 29 26 3 wral 𝑥𝑠 ( 𝑓𝑥 ) = ( 0g ‘ ( Scalar ‘ 𝑚 ) )
31 25 30 wi ( ( 𝑓 finSupp ( 0g ‘ ( Scalar ‘ 𝑚 ) ) ∧ ( 𝑓 ( linC ‘ 𝑚 ) 𝑠 ) = ( 0g𝑚 ) ) → ∀ 𝑥𝑠 ( 𝑓𝑥 ) = ( 0g ‘ ( Scalar ‘ 𝑚 ) ) )
32 31 9 14 wral 𝑓 ∈ ( ( Base ‘ ( Scalar ‘ 𝑚 ) ) ↑m 𝑠 ) ( ( 𝑓 finSupp ( 0g ‘ ( Scalar ‘ 𝑚 ) ) ∧ ( 𝑓 ( linC ‘ 𝑚 ) 𝑠 ) = ( 0g𝑚 ) ) → ∀ 𝑥𝑠 ( 𝑓𝑥 ) = ( 0g ‘ ( Scalar ‘ 𝑚 ) ) )
33 8 32 wa ( 𝑠 ∈ 𝒫 ( Base ‘ 𝑚 ) ∧ ∀ 𝑓 ∈ ( ( Base ‘ ( Scalar ‘ 𝑚 ) ) ↑m 𝑠 ) ( ( 𝑓 finSupp ( 0g ‘ ( Scalar ‘ 𝑚 ) ) ∧ ( 𝑓 ( linC ‘ 𝑚 ) 𝑠 ) = ( 0g𝑚 ) ) → ∀ 𝑥𝑠 ( 𝑓𝑥 ) = ( 0g ‘ ( Scalar ‘ 𝑚 ) ) ) )
34 33 1 2 copab { ⟨ 𝑠 , 𝑚 ⟩ ∣ ( 𝑠 ∈ 𝒫 ( Base ‘ 𝑚 ) ∧ ∀ 𝑓 ∈ ( ( Base ‘ ( Scalar ‘ 𝑚 ) ) ↑m 𝑠 ) ( ( 𝑓 finSupp ( 0g ‘ ( Scalar ‘ 𝑚 ) ) ∧ ( 𝑓 ( linC ‘ 𝑚 ) 𝑠 ) = ( 0g𝑚 ) ) → ∀ 𝑥𝑠 ( 𝑓𝑥 ) = ( 0g ‘ ( Scalar ‘ 𝑚 ) ) ) ) }
35 0 34 wceq linIndS = { ⟨ 𝑠 , 𝑚 ⟩ ∣ ( 𝑠 ∈ 𝒫 ( Base ‘ 𝑚 ) ∧ ∀ 𝑓 ∈ ( ( Base ‘ ( Scalar ‘ 𝑚 ) ) ↑m 𝑠 ) ( ( 𝑓 finSupp ( 0g ‘ ( Scalar ‘ 𝑚 ) ) ∧ ( 𝑓 ( linC ‘ 𝑚 ) 𝑠 ) = ( 0g𝑚 ) ) → ∀ 𝑥𝑠 ( 𝑓𝑥 ) = ( 0g ‘ ( Scalar ‘ 𝑚 ) ) ) ) }