Metamath Proof Explorer

Theorem islinindfiss

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

Ref Expression
Hypotheses islininds.b ⊢ B = Base M
islininds.z ⊢ Z = 0 M
islininds.r ⊢ R = Scalar ⁡ M
islininds.e ⊢ E = Base R
islininds.0 ⊢ 0 ˙ = 0 R
Assertion islinindfiss ⊢ M ∈ W ∧ S ∈ Fin ∧ S ∈ 𝒫 B → S linIndS M ↔ ∀ f ∈ E S f linC ⁡ M S = Z → ∀ x ∈ S f ⁡ x = 0 ˙

Proof

Step Hyp Ref Expression
1 islininds.b ⊢ B = Base M
2 islininds.z ⊢ Z = 0 M
3 islininds.r ⊢ R = Scalar ⁡ M
4 islininds.e ⊢ E = Base R
5 islininds.0 ⊢ 0 ˙ = 0 R
6 1 2 3 4 5 islinindfis ⊢ S ∈ Fin ∧ M ∈ W → S linIndS M ↔ S ∈ 𝒫 B ∧ ∀ f ∈ E S f linC ⁡ M S = Z → ∀ x ∈ S f ⁡ x = 0 ˙
7 6 ancoms ⊢ M ∈ W ∧ S ∈ Fin → S linIndS M ↔ S ∈ 𝒫 B ∧ ∀ f ∈ E S f linC ⁡ M S = Z → ∀ x ∈ S f ⁡ x = 0 ˙
8 7 3adant3 ⊢ M ∈ W ∧ S ∈ Fin ∧ S ∈ 𝒫 B → S linIndS M ↔ S ∈ 𝒫 B ∧ ∀ f ∈ E S f linC ⁡ M S = Z → ∀ x ∈ S f ⁡ x = 0 ˙
9 8 3anibar ⊢ M ∈ W ∧ S ∈ Fin ∧ S ∈ 𝒫 B → S linIndS M ↔ ∀ f ∈ E S f linC ⁡ M S = Z → ∀ x ∈ S f ⁡ x = 0 ˙