Metamath Proof Explorer

Theorem lindflbs

Description: Conditions for an independent family to be a basis. (Contributed by Thierry Arnoux, 21-Jul-2023)

Ref Expression
Hypotheses lindflbs.b ⊢ B = Base W
lindflbs.k ⊢ K = Base F
lindflbs.r ⊢ S = Scalar ⁡ W
lindflbs.t ⊢ · ˙ = ⋅ W
lindflbs.z ⊢ O = 0 W
lindflbs.y ⊢ 0 ˙ = 0 S
lindflbs.n ⊢ N = LSpan ⁡ W
lindflbs.1 ⊢ φ → W ∈ LMod
lindflbs.2 ⊢ φ → S ∈ NzRing
lindflbs.3 ⊢ φ → I ∈ V
lindflbs.4 ⊢ φ → F : I ⟶ 1-1 B
Assertion lindflbs ⊢ φ → ran ⁡ F ∈ LBasis ⁡ W ↔ F LIndF W ∧ N ⁡ ran ⁡ F = B

Proof

Step Hyp Ref Expression
1 lindflbs.b ⊢ B = Base W
2 lindflbs.k ⊢ K = Base F
3 lindflbs.r ⊢ S = Scalar ⁡ W
4 lindflbs.t ⊢ · ˙ = ⋅ W
5 lindflbs.z ⊢ O = 0 W
6 lindflbs.y ⊢ 0 ˙ = 0 S
7 lindflbs.n ⊢ N = LSpan ⁡ W
8 lindflbs.1 ⊢ φ → W ∈ LMod
9 lindflbs.2 ⊢ φ → S ∈ NzRing
10 lindflbs.3 ⊢ φ → I ∈ V
11 lindflbs.4 ⊢ φ → F : I ⟶ 1-1 B
12 eqid ⊢ LBasis ⁡ W = LBasis ⁡ W
13 1 12 7 islbs4 ⊢ ran ⁡ F ∈ LBasis ⁡ W ↔ ran ⁡ F ∈ LIndS ⁡ W ∧ N ⁡ ran ⁡ F = B
14 ssv ⊢ ran ⁡ F ⊆ V
15 f1ssr ⊢ F : I ⟶ 1-1 B ∧ ran ⁡ F ⊆ V → F : I ⟶ 1-1 V
16 11 14 15 sylancl ⊢ φ → F : I ⟶ 1-1 V
17 f1dm ⊢ F : I ⟶ 1-1 B → dom ⁡ F = I
18 f1eq2 ⊢ dom ⁡ F = I → F : dom ⁡ F ⟶ 1-1 V ↔ F : I ⟶ 1-1 V
19 11 17 18 3syl ⊢ φ → F : dom ⁡ F ⟶ 1-1 V ↔ F : I ⟶ 1-1 V
20 16 19 mpbird ⊢ φ → F : dom ⁡ F ⟶ 1-1 V
21 3 islindf3 ⊢ W ∈ LMod ∧ S ∈ NzRing → F LIndF W ↔ F : dom ⁡ F ⟶ 1-1 V ∧ ran ⁡ F ∈ LIndS ⁡ W
22 8 9 21 syl2anc ⊢ φ → F LIndF W ↔ F : dom ⁡ F ⟶ 1-1 V ∧ ran ⁡ F ∈ LIndS ⁡ W
23 20 22 mpbirand ⊢ φ → F LIndF W ↔ ran ⁡ F ∈ LIndS ⁡ W
24 23 anbi1d ⊢ φ → F LIndF W ∧ N ⁡ ran ⁡ F = B ↔ ran ⁡ F ∈ LIndS ⁡ W ∧ N ⁡ ran ⁡ F = B
25 13 24 bitr4id ⊢ φ → ran ⁡ F ∈ LBasis ⁡ W ↔ F LIndF W ∧ N ⁡ ran ⁡ F = B