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