Theorem lindflbs

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

	Ref	Expression
Hypotheses	lindflbs.b	⊢ 𝐵 = ( Base ‘ 𝑊 )
	lindflbs.k	⊢ 𝐾 = ( Base ‘ 𝐹 )
	lindflbs.r	⊢ 𝑆 = ( Scalar ‘ 𝑊 )
	lindflbs.t	⊢ · = ( ·𝑠 ‘ 𝑊 )
	lindflbs.z	⊢ 𝑂 = ( 0g ‘ 𝑊 )
	lindflbs.y	⊢ 0 = ( 0g ‘ 𝑆 )
	lindflbs.n	⊢ 𝑁 = ( LSpan ‘ 𝑊 )
	lindflbs.1	⊢ ( 𝜑 → 𝑊 ∈ LMod )
	lindflbs.2	⊢ ( 𝜑 → 𝑆 ∈ NzRing )
	lindflbs.3	⊢ ( 𝜑 → 𝐼 ∈ 𝑉 )
	lindflbs.4	⊢ ( 𝜑 → 𝐹 : 𝐼 –1-1→ 𝐵 )
Assertion	lindflbs	⊢ ( 𝜑 → ( ran 𝐹 ∈ ( LBasis ‘ 𝑊 ) ↔ ( 𝐹 LIndF 𝑊 ∧ ( 𝑁 ‘ ran 𝐹 ) = 𝐵 ) ) )

Proof

Step	Hyp	Ref	Expression
1		lindflbs.b	⊢ 𝐵 = ( Base ‘ 𝑊 )
2		lindflbs.k	⊢ 𝐾 = ( Base ‘ 𝐹 )
3		lindflbs.r	⊢ 𝑆 = ( Scalar ‘ 𝑊 )
4		lindflbs.t	⊢ · = ( ·𝑠 ‘ 𝑊 )
5		lindflbs.z	⊢ 𝑂 = ( 0g ‘ 𝑊 )
6		lindflbs.y	⊢ 0 = ( 0g ‘ 𝑆 )
7		lindflbs.n	⊢ 𝑁 = ( LSpan ‘ 𝑊 )
8		lindflbs.1	⊢ ( 𝜑 → 𝑊 ∈ LMod )
9		lindflbs.2	⊢ ( 𝜑 → 𝑆 ∈ NzRing )
10		lindflbs.3	⊢ ( 𝜑 → 𝐼 ∈ 𝑉 )
11		lindflbs.4	⊢ ( 𝜑 → 𝐹 : 𝐼 –1-1→ 𝐵 )
12		eqid	⊢ ( LBasis ‘ 𝑊 ) = ( LBasis ‘ 𝑊 )
13	1 12 7	islbs4	⊢ ( ran 𝐹 ∈ ( LBasis ‘ 𝑊 ) ↔ ( ran 𝐹 ∈ ( LIndS ‘ 𝑊 ) ∧ ( 𝑁 ‘ ran 𝐹 ) = 𝐵 ) )
14		ssv	⊢ ran 𝐹 ⊆ V
15		f1ssr	⊢ ( ( 𝐹 : 𝐼 –1-1→ 𝐵 ∧ ran 𝐹 ⊆ V ) → 𝐹 : 𝐼 –1-1→ V )
16	11 14 15	sylancl	⊢ ( 𝜑 → 𝐹 : 𝐼 –1-1→ V )
17		f1dm	⊢ ( 𝐹 : 𝐼 –1-1→ 𝐵 → dom 𝐹 = 𝐼 )
18		f1eq2	⊢ ( dom 𝐹 = 𝐼 → ( 𝐹 : dom 𝐹 –1-1→ V ↔ 𝐹 : 𝐼 –1-1→ V ) )
19	11 17 18	3syl	⊢ ( 𝜑 → ( 𝐹 : dom 𝐹 –1-1→ V ↔ 𝐹 : 𝐼 –1-1→ V ) )
20	16 19	mpbird	⊢ ( 𝜑 → 𝐹 : dom 𝐹 –1-1→ V )
21	3	islindf3	⊢ ( ( 𝑊 ∈ LMod ∧ 𝑆 ∈ NzRing ) → ( 𝐹 LIndF 𝑊 ↔ ( 𝐹 : dom 𝐹 –1-1→ V ∧ ran 𝐹 ∈ ( LIndS ‘ 𝑊 ) ) ) )
22	8 9 21	syl2anc	⊢ ( 𝜑 → ( 𝐹 LIndF 𝑊 ↔ ( 𝐹 : dom 𝐹 –1-1→ V ∧ ran 𝐹 ∈ ( LIndS ‘ 𝑊 ) ) ) )
23	20 22	mpbirand	⊢ ( 𝜑 → ( 𝐹 LIndF 𝑊 ↔ ran 𝐹 ∈ ( LIndS ‘ 𝑊 ) ) )
24	23	anbi1d	⊢ ( 𝜑 → ( ( 𝐹 LIndF 𝑊 ∧ ( 𝑁 ‘ ran 𝐹 ) = 𝐵 ) ↔ ( ran 𝐹 ∈ ( LIndS ‘ 𝑊 ) ∧ ( 𝑁 ‘ ran 𝐹 ) = 𝐵 ) ) )
25	13 24	bitr4id	⊢ ( 𝜑 → ( ran 𝐹 ∈ ( LBasis ‘ 𝑊 ) ↔ ( 𝐹 LIndF 𝑊 ∧ ( 𝑁 ‘ ran 𝐹 ) = 𝐵 ) ) )