Metamath Proof Explorer

Theorem islininds

Description: The property of being a linearly independent subset. (Contributed by AV, 13-Apr-2019) (Revised by AV, 30-Jul-2019)

Ref Expression
Hypotheses islininds.b ⊢ 𝐵 = ( Base ‘ 𝑀 )
islininds.z ⊢ 𝑍 = ( 0g ‘ 𝑀 )
islininds.r ⊢ 𝑅 = ( Scalar ‘ 𝑀 )
islininds.e ⊢ 𝐸 = ( Base ‘ 𝑅 )
islininds.0 ⊢ 0 = ( 0g ‘ 𝑅 )
Assertion islininds ( ( 𝑆 ∈ 𝑉 ∧ 𝑀 ∈ 𝑊 ) → ( 𝑆 linIndS 𝑀 ↔ ( 𝑆 ∈ 𝒫 𝐵 ∧ ∀ 𝑓 ∈ ( 𝐸 ↑m 𝑆 ) ( ( 𝑓 finSupp 0 ∧ ( 𝑓 ( linC ‘ 𝑀 ) 𝑆 ) = 𝑍 ) → ∀ 𝑥 ∈ 𝑆 ( 𝑓 ‘ 𝑥 ) = 0 ) ) ) )

Proof

Step Hyp Ref Expression
1 islininds.b ⊢ 𝐵 = ( Base ‘ 𝑀 )
2 islininds.z ⊢ 𝑍 = ( 0g ‘ 𝑀 )
3 islininds.r ⊢ 𝑅 = ( Scalar ‘ 𝑀 )
4 islininds.e ⊢ 𝐸 = ( Base ‘ 𝑅 )
5 islininds.0 ⊢ 0 = ( 0g ‘ 𝑅 )
6 simpl ⊢ ( ( 𝑠 = 𝑆 ∧ 𝑚 = 𝑀 ) → 𝑠 = 𝑆 )
7 fveq2 ⊢ ( 𝑚 = 𝑀 → ( Base ‘ 𝑚 ) = ( Base ‘ 𝑀 ) )
8 7 1 eqtr4di ⊢ ( 𝑚 = 𝑀 → ( Base ‘ 𝑚 ) = 𝐵 )
9 8 adantl ⊢ ( ( 𝑠 = 𝑆 ∧ 𝑚 = 𝑀 ) → ( Base ‘ 𝑚 ) = 𝐵 )
10 9 pweqd ⊢ ( ( 𝑠 = 𝑆 ∧ 𝑚 = 𝑀 ) → 𝒫 ( Base ‘ 𝑚 ) = 𝒫 𝐵 )
11 6 10 eleq12d ⊢ ( ( 𝑠 = 𝑆 ∧ 𝑚 = 𝑀 ) → ( 𝑠 ∈ 𝒫 ( Base ‘ 𝑚 ) ↔ 𝑆 ∈ 𝒫 𝐵 ) )
12 fveq2 ⊢ ( 𝑚 = 𝑀 → ( Scalar ‘ 𝑚 ) = ( Scalar ‘ 𝑀 ) )
13 12 3 eqtr4di ⊢ ( 𝑚 = 𝑀 → ( Scalar ‘ 𝑚 ) = 𝑅 )
14 13 fveq2d ⊢ ( 𝑚 = 𝑀 → ( Base ‘ ( Scalar ‘ 𝑚 ) ) = ( Base ‘ 𝑅 ) )
15 14 4 eqtr4di ⊢ ( 𝑚 = 𝑀 → ( Base ‘ ( Scalar ‘ 𝑚 ) ) = 𝐸 )
16 15 adantl ⊢ ( ( 𝑠 = 𝑆 ∧ 𝑚 = 𝑀 ) → ( Base ‘ ( Scalar ‘ 𝑚 ) ) = 𝐸 )
17 16 6 oveq12d ⊢ ( ( 𝑠 = 𝑆 ∧ 𝑚 = 𝑀 ) → ( ( Base ‘ ( Scalar ‘ 𝑚 ) ) ↑m 𝑠 ) = ( 𝐸 ↑m 𝑆 ) )
18 12 adantl ⊢ ( ( 𝑠 = 𝑆 ∧ 𝑚 = 𝑀 ) → ( Scalar ‘ 𝑚 ) = ( Scalar ‘ 𝑀 ) )
19 18 3 eqtr4di ⊢ ( ( 𝑠 = 𝑆 ∧ 𝑚 = 𝑀 ) → ( Scalar ‘ 𝑚 ) = 𝑅 )
20 19 fveq2d ⊢ ( ( 𝑠 = 𝑆 ∧ 𝑚 = 𝑀 ) → ( 0g ‘ ( Scalar ‘ 𝑚 ) ) = ( 0g ‘ 𝑅 ) )
21 20 5 eqtr4di ⊢ ( ( 𝑠 = 𝑆 ∧ 𝑚 = 𝑀 ) → ( 0g ‘ ( Scalar ‘ 𝑚 ) ) = 0 )
22 21 breq2d ⊢ ( ( 𝑠 = 𝑆 ∧ 𝑚 = 𝑀 ) → ( 𝑓 finSupp ( 0g ‘ ( Scalar ‘ 𝑚 ) ) ↔ 𝑓 finSupp 0 ) )
23 fveq2 ⊢ ( 𝑚 = 𝑀 → ( linC ‘ 𝑚 ) = ( linC ‘ 𝑀 ) )
24 23 adantl ⊢ ( ( 𝑠 = 𝑆 ∧ 𝑚 = 𝑀 ) → ( linC ‘ 𝑚 ) = ( linC ‘ 𝑀 ) )
25 eqidd ⊢ ( ( 𝑠 = 𝑆 ∧ 𝑚 = 𝑀 ) → 𝑓 = 𝑓 )
26 24 25 6 oveq123d ⊢ ( ( 𝑠 = 𝑆 ∧ 𝑚 = 𝑀 ) → ( 𝑓 ( linC ‘ 𝑚 ) 𝑠 ) = ( 𝑓 ( linC ‘ 𝑀 ) 𝑆 ) )
27 fveq2 ⊢ ( 𝑚 = 𝑀 → ( 0g ‘ 𝑚 ) = ( 0g ‘ 𝑀 ) )
28 27 adantl ⊢ ( ( 𝑠 = 𝑆 ∧ 𝑚 = 𝑀 ) → ( 0g ‘ 𝑚 ) = ( 0g ‘ 𝑀 ) )
29 28 2 eqtr4di ⊢ ( ( 𝑠 = 𝑆 ∧ 𝑚 = 𝑀 ) → ( 0g ‘ 𝑚 ) = 𝑍 )
30 26 29 eqeq12d ⊢ ( ( 𝑠 = 𝑆 ∧ 𝑚 = 𝑀 ) → ( ( 𝑓 ( linC ‘ 𝑚 ) 𝑠 ) = ( 0g ‘ 𝑚 ) ↔ ( 𝑓 ( linC ‘ 𝑀 ) 𝑆 ) = 𝑍 ) )
31 22 30 anbi12d ⊢ ( ( 𝑠 = 𝑆 ∧ 𝑚 = 𝑀 ) → ( ( 𝑓 finSupp ( 0g ‘ ( Scalar ‘ 𝑚 ) ) ∧ ( 𝑓 ( linC ‘ 𝑚 ) 𝑠 ) = ( 0g ‘ 𝑚 ) ) ↔ ( 𝑓 finSupp 0 ∧ ( 𝑓 ( linC ‘ 𝑀 ) 𝑆 ) = 𝑍 ) ) )
32 13 fveq2d ⊢ ( 𝑚 = 𝑀 → ( 0g ‘ ( Scalar ‘ 𝑚 ) ) = ( 0g ‘ 𝑅 ) )
33 32 5 eqtr4di ⊢ ( 𝑚 = 𝑀 → ( 0g ‘ ( Scalar ‘ 𝑚 ) ) = 0 )
34 33 adantl ⊢ ( ( 𝑠 = 𝑆 ∧ 𝑚 = 𝑀 ) → ( 0g ‘ ( Scalar ‘ 𝑚 ) ) = 0 )
35 34 eqeq2d ⊢ ( ( 𝑠 = 𝑆 ∧ 𝑚 = 𝑀 ) → ( ( 𝑓 ‘ 𝑥 ) = ( 0g ‘ ( Scalar ‘ 𝑚 ) ) ↔ ( 𝑓 ‘ 𝑥 ) = 0 ) )
36 6 35 raleqbidv ⊢ ( ( 𝑠 = 𝑆 ∧ 𝑚 = 𝑀 ) → ( ∀ 𝑥 ∈ 𝑠 ( 𝑓 ‘ 𝑥 ) = ( 0g ‘ ( Scalar ‘ 𝑚 ) ) ↔ ∀ 𝑥 ∈ 𝑆 ( 𝑓 ‘ 𝑥 ) = 0 ) )
37 31 36 imbi12d ⊢ ( ( 𝑠 = 𝑆 ∧ 𝑚 = 𝑀 ) → ( ( ( 𝑓 finSupp ( 0g ‘ ( Scalar ‘ 𝑚 ) ) ∧ ( 𝑓 ( linC ‘ 𝑚 ) 𝑠 ) = ( 0g ‘ 𝑚 ) ) → ∀ 𝑥 ∈ 𝑠 ( 𝑓 ‘ 𝑥 ) = ( 0g ‘ ( Scalar ‘ 𝑚 ) ) ) ↔ ( ( 𝑓 finSupp 0 ∧ ( 𝑓 ( linC ‘ 𝑀 ) 𝑆 ) = 𝑍 ) → ∀ 𝑥 ∈ 𝑆 ( 𝑓 ‘ 𝑥 ) = 0 ) ) )
38 17 37 raleqbidv ⊢ ( ( 𝑠 = 𝑆 ∧ 𝑚 = 𝑀 ) → ( ∀ 𝑓 ∈ ( ( Base ‘ ( Scalar ‘ 𝑚 ) ) ↑m 𝑠 ) ( ( 𝑓 finSupp ( 0g ‘ ( Scalar ‘ 𝑚 ) ) ∧ ( 𝑓 ( linC ‘ 𝑚 ) 𝑠 ) = ( 0g ‘ 𝑚 ) ) → ∀ 𝑥 ∈ 𝑠 ( 𝑓 ‘ 𝑥 ) = ( 0g ‘ ( Scalar ‘ 𝑚 ) ) ) ↔ ∀ 𝑓 ∈ ( 𝐸 ↑m 𝑆 ) ( ( 𝑓 finSupp 0 ∧ ( 𝑓 ( linC ‘ 𝑀 ) 𝑆 ) = 𝑍 ) → ∀ 𝑥 ∈ 𝑆 ( 𝑓 ‘ 𝑥 ) = 0 ) ) )
39 11 38 anbi12d ⊢ ( ( 𝑠 = 𝑆 ∧ 𝑚 = 𝑀 ) → ( ( 𝑠 ∈ 𝒫 ( Base ‘ 𝑚 ) ∧ ∀ 𝑓 ∈ ( ( Base ‘ ( Scalar ‘ 𝑚 ) ) ↑m 𝑠 ) ( ( 𝑓 finSupp ( 0g ‘ ( Scalar ‘ 𝑚 ) ) ∧ ( 𝑓 ( linC ‘ 𝑚 ) 𝑠 ) = ( 0g ‘ 𝑚 ) ) → ∀ 𝑥 ∈ 𝑠 ( 𝑓 ‘ 𝑥 ) = ( 0g ‘ ( Scalar ‘ 𝑚 ) ) ) ) ↔ ( 𝑆 ∈ 𝒫 𝐵 ∧ ∀ 𝑓 ∈ ( 𝐸 ↑m 𝑆 ) ( ( 𝑓 finSupp 0 ∧ ( 𝑓 ( linC ‘ 𝑀 ) 𝑆 ) = 𝑍 ) → ∀ 𝑥 ∈ 𝑆 ( 𝑓 ‘ 𝑥 ) = 0 ) ) ) )
40 df-lininds ⊢ linIndS = { ⟨ 𝑠 , 𝑚 ⟩ ∣ ( 𝑠 ∈ 𝒫 ( Base ‘ 𝑚 ) ∧ ∀ 𝑓 ∈ ( ( Base ‘ ( Scalar ‘ 𝑚 ) ) ↑m 𝑠 ) ( ( 𝑓 finSupp ( 0g ‘ ( Scalar ‘ 𝑚 ) ) ∧ ( 𝑓 ( linC ‘ 𝑚 ) 𝑠 ) = ( 0g ‘ 𝑚 ) ) → ∀ 𝑥 ∈ 𝑠 ( 𝑓 ‘ 𝑥 ) = ( 0g ‘ ( Scalar ‘ 𝑚 ) ) ) ) }
41 39 40 brabga ⊢ ( ( 𝑆 ∈ 𝑉 ∧ 𝑀 ∈ 𝑊 ) → ( 𝑆 linIndS 𝑀 ↔ ( 𝑆 ∈ 𝒫 𝐵 ∧ ∀ 𝑓 ∈ ( 𝐸 ↑m 𝑆 ) ( ( 𝑓 finSupp 0 ∧ ( 𝑓 ( linC ‘ 𝑀 ) 𝑆 ) = 𝑍 ) → ∀ 𝑥 ∈ 𝑆 ( 𝑓 ‘ 𝑥 ) = 0 ) ) ) )