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 ssv ⊢ ran ⁡ F ⊆ V
13 f1ssr ⊢ F : I ⟶ 1-1 B ∧ ran ⁡ F ⊆ V → F : I ⟶ 1-1 V
14 11 12 13 sylancl ⊢ φ → F : I ⟶ 1-1 V
15 f1dm ⊢ F : I ⟶ 1-1 B → dom ⁡ F = I
16 f1eq2 ⊢ dom ⁡ F = I → F : dom ⁡ F ⟶ 1-1 V ↔ F : I ⟶ 1-1 V
17 11 15 16 3syl ⊢ φ → F : dom ⁡ F ⟶ 1-1 V ↔ F : I ⟶ 1-1 V
18 14 17 mpbird ⊢ φ → F : dom ⁡ F ⟶ 1-1 V
19 3 islindf3 ⊢ W ∈ LMod ∧ S ∈ NzRing → F LIndF W ↔ F : dom ⁡ F ⟶ 1-1 V ∧ ran ⁡ F ∈ LIndS ⁡ W
20 8 9 19 syl2anc ⊢ φ → F LIndF W ↔ F : dom ⁡ F ⟶ 1-1 V ∧ ran ⁡ F ∈ LIndS ⁡ W
21 18 20 mpbirand ⊢ φ → F LIndF W ↔ ran ⁡ F ∈ LIndS ⁡ W
22 21 anbi1d ⊢ φ → F LIndF W ∧ N ⁡ ran ⁡ F = B ↔ ran ⁡ F ∈ LIndS ⁡ W ∧ N ⁡ ran ⁡ F = B
23 eqid ⊢ LBasis ⁡ W = LBasis ⁡ W
24 1 23 7 islbs4 ⊢ ran ⁡ F ∈ LBasis ⁡ W ↔ ran ⁡ F ∈ LIndS ⁡ W ∧ N ⁡ ran ⁡ F = B
25 22 24 syl6rbbr ⊢ φ → ran ⁡ F ∈ LBasis ⁡ W ↔ F LIndF W ∧ N ⁡ ran ⁡ F = B