Metamath Proof Explorer

Theorem islinindfis

Description: The property of being a linearly independent finite subset. (Contributed by AV, 27-Apr-2019)

Ref Expression
Hypotheses islininds.b ⊢ 𝐵 = ( Base ‘ 𝑀 )
islininds.z ⊢ 𝑍 = ( 0g ‘ 𝑀 )
islininds.r ⊢ 𝑅 = ( Scalar ‘ 𝑀 )
islininds.e ⊢ 𝐸 = ( Base ‘ 𝑅 )
islininds.0 ⊢ 0 = ( 0g ‘ 𝑅 )
Assertion islinindfis ( ( 𝑆 ∈ Fin ∧ 𝑀 ∈ 𝑊 ) → ( 𝑆 linIndS 𝑀 ↔ ( 𝑆 ∈ 𝒫 𝐵 ∧ ∀ 𝑓 ∈ ( 𝐸 ↑m 𝑆 ) ( ( 𝑓 ( 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 1 2 3 4 5 islininds ⊢ ( ( 𝑆 ∈ Fin ∧ 𝑀 ∈ 𝑊 ) → ( 𝑆 linIndS 𝑀 ↔ ( 𝑆 ∈ 𝒫 𝐵 ∧ ∀ 𝑓 ∈ ( 𝐸 ↑m 𝑆 ) ( ( 𝑓 finSupp 0 ∧ ( 𝑓 ( linC ‘ 𝑀 ) 𝑆 ) = 𝑍 ) → ∀ 𝑥 ∈ 𝑆 ( 𝑓 ‘ 𝑥 ) = 0 ) ) ) )
7 pm4.79 ⊢ ( ( ( 𝑓 finSupp 0 → ∀ 𝑥 ∈ 𝑆 ( 𝑓 ‘ 𝑥 ) = 0 ) ∨ ( ( 𝑓 ( linC ‘ 𝑀 ) 𝑆 ) = 𝑍 → ∀ 𝑥 ∈ 𝑆 ( 𝑓 ‘ 𝑥 ) = 0 ) ) ↔ ( ( 𝑓 finSupp 0 ∧ ( 𝑓 ( linC ‘ 𝑀 ) 𝑆 ) = 𝑍 ) → ∀ 𝑥 ∈ 𝑆 ( 𝑓 ‘ 𝑥 ) = 0 ) )
8 elmapi ⊢ ( 𝑓 ∈ ( 𝐸 ↑m 𝑆 ) → 𝑓 : 𝑆 ⟶ 𝐸 )
9 8 adantl ⊢ ( ( ( 𝑆 ∈ Fin ∧ 𝑀 ∈ 𝑊 ) ∧ 𝑓 ∈ ( 𝐸 ↑m 𝑆 ) ) → 𝑓 : 𝑆 ⟶ 𝐸 )
10 simpll ⊢ ( ( ( 𝑆 ∈ Fin ∧ 𝑀 ∈ 𝑊 ) ∧ 𝑓 ∈ ( 𝐸 ↑m 𝑆 ) ) → 𝑆 ∈ Fin )
11 5 fvexi ⊢ 0 ∈ V
12 11 a1i ⊢ ( ( ( 𝑆 ∈ Fin ∧ 𝑀 ∈ 𝑊 ) ∧ 𝑓 ∈ ( 𝐸 ↑m 𝑆 ) ) → 0 ∈ V )
13 9 10 12 fdmfifsupp ⊢ ( ( ( 𝑆 ∈ Fin ∧ 𝑀 ∈ 𝑊 ) ∧ 𝑓 ∈ ( 𝐸 ↑m 𝑆 ) ) → 𝑓 finSupp 0 )
14 13 adantr ⊢ ( ( ( ( 𝑆 ∈ Fin ∧ 𝑀 ∈ 𝑊 ) ∧ 𝑓 ∈ ( 𝐸 ↑m 𝑆 ) ) ∧ ( 𝑓 ( linC ‘ 𝑀 ) 𝑆 ) = 𝑍 ) → 𝑓 finSupp 0 )
15 14 imim1i ⊢ ( ( 𝑓 finSupp 0 → ∀ 𝑥 ∈ 𝑆 ( 𝑓 ‘ 𝑥 ) = 0 ) → ( ( ( ( 𝑆 ∈ Fin ∧ 𝑀 ∈ 𝑊 ) ∧ 𝑓 ∈ ( 𝐸 ↑m 𝑆 ) ) ∧ ( 𝑓 ( linC ‘ 𝑀 ) 𝑆 ) = 𝑍 ) → ∀ 𝑥 ∈ 𝑆 ( 𝑓 ‘ 𝑥 ) = 0 ) )
16 15 expd ⊢ ( ( 𝑓 finSupp 0 → ∀ 𝑥 ∈ 𝑆 ( 𝑓 ‘ 𝑥 ) = 0 ) → ( ( ( 𝑆 ∈ Fin ∧ 𝑀 ∈ 𝑊 ) ∧ 𝑓 ∈ ( 𝐸 ↑m 𝑆 ) ) → ( ( 𝑓 ( linC ‘ 𝑀 ) 𝑆 ) = 𝑍 → ∀ 𝑥 ∈ 𝑆 ( 𝑓 ‘ 𝑥 ) = 0 ) ) )
17 ax-1 ⊢ ( ( ( 𝑓 ( linC ‘ 𝑀 ) 𝑆 ) = 𝑍 → ∀ 𝑥 ∈ 𝑆 ( 𝑓 ‘ 𝑥 ) = 0 ) → ( ( ( 𝑆 ∈ Fin ∧ 𝑀 ∈ 𝑊 ) ∧ 𝑓 ∈ ( 𝐸 ↑m 𝑆 ) ) → ( ( 𝑓 ( linC ‘ 𝑀 ) 𝑆 ) = 𝑍 → ∀ 𝑥 ∈ 𝑆 ( 𝑓 ‘ 𝑥 ) = 0 ) ) )
18 16 17 jaoi ⊢ ( ( ( 𝑓 finSupp 0 → ∀ 𝑥 ∈ 𝑆 ( 𝑓 ‘ 𝑥 ) = 0 ) ∨ ( ( 𝑓 ( linC ‘ 𝑀 ) 𝑆 ) = 𝑍 → ∀ 𝑥 ∈ 𝑆 ( 𝑓 ‘ 𝑥 ) = 0 ) ) → ( ( ( 𝑆 ∈ Fin ∧ 𝑀 ∈ 𝑊 ) ∧ 𝑓 ∈ ( 𝐸 ↑m 𝑆 ) ) → ( ( 𝑓 ( linC ‘ 𝑀 ) 𝑆 ) = 𝑍 → ∀ 𝑥 ∈ 𝑆 ( 𝑓 ‘ 𝑥 ) = 0 ) ) )
19 7 18 sylbir ⊢ ( ( ( 𝑓 finSupp 0 ∧ ( 𝑓 ( linC ‘ 𝑀 ) 𝑆 ) = 𝑍 ) → ∀ 𝑥 ∈ 𝑆 ( 𝑓 ‘ 𝑥 ) = 0 ) → ( ( ( 𝑆 ∈ Fin ∧ 𝑀 ∈ 𝑊 ) ∧ 𝑓 ∈ ( 𝐸 ↑m 𝑆 ) ) → ( ( 𝑓 ( linC ‘ 𝑀 ) 𝑆 ) = 𝑍 → ∀ 𝑥 ∈ 𝑆 ( 𝑓 ‘ 𝑥 ) = 0 ) ) )
20 19 com12 ⊢ ( ( ( 𝑆 ∈ Fin ∧ 𝑀 ∈ 𝑊 ) ∧ 𝑓 ∈ ( 𝐸 ↑m 𝑆 ) ) → ( ( ( 𝑓 finSupp 0 ∧ ( 𝑓 ( linC ‘ 𝑀 ) 𝑆 ) = 𝑍 ) → ∀ 𝑥 ∈ 𝑆 ( 𝑓 ‘ 𝑥 ) = 0 ) → ( ( 𝑓 ( linC ‘ 𝑀 ) 𝑆 ) = 𝑍 → ∀ 𝑥 ∈ 𝑆 ( 𝑓 ‘ 𝑥 ) = 0 ) ) )
21 pm3.42 ⊢ ( ( ( 𝑓 ( linC ‘ 𝑀 ) 𝑆 ) = 𝑍 → ∀ 𝑥 ∈ 𝑆 ( 𝑓 ‘ 𝑥 ) = 0 ) → ( ( 𝑓 finSupp 0 ∧ ( 𝑓 ( linC ‘ 𝑀 ) 𝑆 ) = 𝑍 ) → ∀ 𝑥 ∈ 𝑆 ( 𝑓 ‘ 𝑥 ) = 0 ) )
22 20 21 impbid1 ⊢ ( ( ( 𝑆 ∈ Fin ∧ 𝑀 ∈ 𝑊 ) ∧ 𝑓 ∈ ( 𝐸 ↑m 𝑆 ) ) → ( ( ( 𝑓 finSupp 0 ∧ ( 𝑓 ( linC ‘ 𝑀 ) 𝑆 ) = 𝑍 ) → ∀ 𝑥 ∈ 𝑆 ( 𝑓 ‘ 𝑥 ) = 0 ) ↔ ( ( 𝑓 ( linC ‘ 𝑀 ) 𝑆 ) = 𝑍 → ∀ 𝑥 ∈ 𝑆 ( 𝑓 ‘ 𝑥 ) = 0 ) ) )
23 22 ralbidva ⊢ ( ( 𝑆 ∈ Fin ∧ 𝑀 ∈ 𝑊 ) → ( ∀ 𝑓 ∈ ( 𝐸 ↑m 𝑆 ) ( ( 𝑓 finSupp 0 ∧ ( 𝑓 ( linC ‘ 𝑀 ) 𝑆 ) = 𝑍 ) → ∀ 𝑥 ∈ 𝑆 ( 𝑓 ‘ 𝑥 ) = 0 ) ↔ ∀ 𝑓 ∈ ( 𝐸 ↑m 𝑆 ) ( ( 𝑓 ( linC ‘ 𝑀 ) 𝑆 ) = 𝑍 → ∀ 𝑥 ∈ 𝑆 ( 𝑓 ‘ 𝑥 ) = 0 ) ) )
24 23 anbi2d ⊢ ( ( 𝑆 ∈ Fin ∧ 𝑀 ∈ 𝑊 ) → ( ( 𝑆 ∈ 𝒫 𝐵 ∧ ∀ 𝑓 ∈ ( 𝐸 ↑m 𝑆 ) ( ( 𝑓 finSupp 0 ∧ ( 𝑓 ( linC ‘ 𝑀 ) 𝑆 ) = 𝑍 ) → ∀ 𝑥 ∈ 𝑆 ( 𝑓 ‘ 𝑥 ) = 0 ) ) ↔ ( 𝑆 ∈ 𝒫 𝐵 ∧ ∀ 𝑓 ∈ ( 𝐸 ↑m 𝑆 ) ( ( 𝑓 ( linC ‘ 𝑀 ) 𝑆 ) = 𝑍 → ∀ 𝑥 ∈ 𝑆 ( 𝑓 ‘ 𝑥 ) = 0 ) ) ) )
25 6 24 bitrd ⊢ ( ( 𝑆 ∈ Fin ∧ 𝑀 ∈ 𝑊 ) → ( 𝑆 linIndS 𝑀 ↔ ( 𝑆 ∈ 𝒫 𝐵 ∧ ∀ 𝑓 ∈ ( 𝐸 ↑m 𝑆 ) ( ( 𝑓 ( linC ‘ 𝑀 ) 𝑆 ) = 𝑍 → ∀ 𝑥 ∈ 𝑆 ( 𝑓 ‘ 𝑥 ) = 0 ) ) ) )