Theorem islbs5

Description: An equivalent formulation of the basis predicate in a vector space, using a function F for generating the base. (Contributed by Thierry Arnoux, 20-Feb-2025)

	Ref	Expression
Hypotheses	islbs5.b	⊢ 𝐵 = ( Base ‘ 𝑊 )
	islbs5.k	⊢ 𝐾 = ( Base ‘ 𝑆 )
	islbs5.r	⊢ 𝑆 = ( Scalar ‘ 𝑊 )
	islbs5.t	⊢ · = ( ·𝑠 ‘ 𝑊 )
	islbs5.z	⊢ 𝑂 = ( 0g ‘ 𝑊 )
	islbs5.y	⊢ 0 = ( 0g ‘ 𝑆 )
	islbs5.j	⊢ 𝐽 = ( LBasis ‘ 𝑊 )
	islbs5.n	⊢ 𝑁 = ( LSpan ‘ 𝑊 )
	islbs5.w	⊢ ( 𝜑 → 𝑊 ∈ LMod )
	islbs5.s	⊢ ( 𝜑 → 𝑆 ∈ NzRing )
	islbs5.i	⊢ ( 𝜑 → 𝐼 ∈ 𝑉 )
	islbs5.f	⊢ ( 𝜑 → 𝐹 : 𝐼 –1-1→ 𝐵 )
Assertion	islbs5	⊢ ( 𝜑 → ( ran 𝐹 ∈ ( LBasis ‘ 𝑊 ) ↔ ( ∀ 𝑎 ∈ ( 𝐾 ↑m 𝐼 ) ( ( 𝑎 finSupp 0 ∧ ( 𝑊 Σg ( 𝑎 ∘f · 𝐹 ) ) = 𝑂 ) → 𝑎 = ( 𝐼 × { 0 } ) ) ∧ ( 𝑁 ‘ ran 𝐹 ) = 𝐵 ) ) )

Proof

Step	Hyp	Ref	Expression
1		islbs5.b	⊢ 𝐵 = ( Base ‘ 𝑊 )
2		islbs5.k	⊢ 𝐾 = ( Base ‘ 𝑆 )
3		islbs5.r	⊢ 𝑆 = ( Scalar ‘ 𝑊 )
4		islbs5.t	⊢ · = ( ·𝑠 ‘ 𝑊 )
5		islbs5.z	⊢ 𝑂 = ( 0g ‘ 𝑊 )
6		islbs5.y	⊢ 0 = ( 0g ‘ 𝑆 )
7		islbs5.j	⊢ 𝐽 = ( LBasis ‘ 𝑊 )
8		islbs5.n	⊢ 𝑁 = ( LSpan ‘ 𝑊 )
9		islbs5.w	⊢ ( 𝜑 → 𝑊 ∈ LMod )
10		islbs5.s	⊢ ( 𝜑 → 𝑆 ∈ NzRing )
11		islbs5.i	⊢ ( 𝜑 → 𝐼 ∈ 𝑉 )
12		islbs5.f	⊢ ( 𝜑 → 𝐹 : 𝐼 –1-1→ 𝐵 )
13		eqid	⊢ ( Base ‘ 𝐹 ) = ( Base ‘ 𝐹 )
14	1 13 3 4 5 6 8 9 10 11 12	lindflbs	⊢ ( 𝜑 → ( ran 𝐹 ∈ ( LBasis ‘ 𝑊 ) ↔ ( 𝐹 LIndF 𝑊 ∧ ( 𝑁 ‘ ran 𝐹 ) = 𝐵 ) ) )
15		f1f	⊢ ( 𝐹 : 𝐼 –1-1→ 𝐵 → 𝐹 : 𝐼 ⟶ 𝐵 )
16	12 15	syl	⊢ ( 𝜑 → 𝐹 : 𝐼 ⟶ 𝐵 )
17		eqid	⊢ ( Base ‘ ( 𝑆 freeLMod 𝐼 ) ) = ( Base ‘ ( 𝑆 freeLMod 𝐼 ) )
18	1 3 4 5 6 17	islindf4	⊢ ( ( 𝑊 ∈ LMod ∧ 𝐼 ∈ 𝑉 ∧ 𝐹 : 𝐼 ⟶ 𝐵 ) → ( 𝐹 LIndF 𝑊 ↔ ∀ 𝑎 ∈ ( Base ‘ ( 𝑆 freeLMod 𝐼 ) ) ( ( 𝑊 Σg ( 𝑎 ∘f · 𝐹 ) ) = 𝑂 → 𝑎 = ( 𝐼 × { 0 } ) ) ) )
19	9 11 16 18	syl3anc	⊢ ( 𝜑 → ( 𝐹 LIndF 𝑊 ↔ ∀ 𝑎 ∈ ( Base ‘ ( 𝑆 freeLMod 𝐼 ) ) ( ( 𝑊 Σg ( 𝑎 ∘f · 𝐹 ) ) = 𝑂 → 𝑎 = ( 𝐼 × { 0 } ) ) ) )
20	10	elexd	⊢ ( 𝜑 → 𝑆 ∈ V )
21		eqid	⊢ ( 𝑆 freeLMod 𝐼 ) = ( 𝑆 freeLMod 𝐼 )
22	21 2 6 17	frlmelbas	⊢ ( ( 𝑆 ∈ V ∧ 𝐼 ∈ 𝑉 ) → ( 𝑎 ∈ ( Base ‘ ( 𝑆 freeLMod 𝐼 ) ) ↔ ( 𝑎 ∈ ( 𝐾 ↑m 𝐼 ) ∧ 𝑎 finSupp 0 ) ) )
23	20 11 22	syl2anc	⊢ ( 𝜑 → ( 𝑎 ∈ ( Base ‘ ( 𝑆 freeLMod 𝐼 ) ) ↔ ( 𝑎 ∈ ( 𝐾 ↑m 𝐼 ) ∧ 𝑎 finSupp 0 ) ) )
24	23	imbi1d	⊢ ( 𝜑 → ( ( 𝑎 ∈ ( Base ‘ ( 𝑆 freeLMod 𝐼 ) ) → ( ( 𝑊 Σg ( 𝑎 ∘f · 𝐹 ) ) = 𝑂 → 𝑎 = ( 𝐼 × { 0 } ) ) ) ↔ ( ( 𝑎 ∈ ( 𝐾 ↑m 𝐼 ) ∧ 𝑎 finSupp 0 ) → ( ( 𝑊 Σg ( 𝑎 ∘f · 𝐹 ) ) = 𝑂 → 𝑎 = ( 𝐼 × { 0 } ) ) ) ) )
25		impexp	⊢ ( ( ( 𝑎 ∈ ( 𝐾 ↑m 𝐼 ) ∧ 𝑎 finSupp 0 ) → ( ( 𝑊 Σg ( 𝑎 ∘f · 𝐹 ) ) = 𝑂 → 𝑎 = ( 𝐼 × { 0 } ) ) ) ↔ ( 𝑎 ∈ ( 𝐾 ↑m 𝐼 ) → ( 𝑎 finSupp 0 → ( ( 𝑊 Σg ( 𝑎 ∘f · 𝐹 ) ) = 𝑂 → 𝑎 = ( 𝐼 × { 0 } ) ) ) ) )
26		impexp	⊢ ( ( ( 𝑎 finSupp 0 ∧ ( 𝑊 Σg ( 𝑎 ∘f · 𝐹 ) ) = 𝑂 ) → 𝑎 = ( 𝐼 × { 0 } ) ) ↔ ( 𝑎 finSupp 0 → ( ( 𝑊 Σg ( 𝑎 ∘f · 𝐹 ) ) = 𝑂 → 𝑎 = ( 𝐼 × { 0 } ) ) ) )
27	26	a1i	⊢ ( 𝜑 → ( ( ( 𝑎 finSupp 0 ∧ ( 𝑊 Σg ( 𝑎 ∘f · 𝐹 ) ) = 𝑂 ) → 𝑎 = ( 𝐼 × { 0 } ) ) ↔ ( 𝑎 finSupp 0 → ( ( 𝑊 Σg ( 𝑎 ∘f · 𝐹 ) ) = 𝑂 → 𝑎 = ( 𝐼 × { 0 } ) ) ) ) )
28	27	bicomd	⊢ ( 𝜑 → ( ( 𝑎 finSupp 0 → ( ( 𝑊 Σg ( 𝑎 ∘f · 𝐹 ) ) = 𝑂 → 𝑎 = ( 𝐼 × { 0 } ) ) ) ↔ ( ( 𝑎 finSupp 0 ∧ ( 𝑊 Σg ( 𝑎 ∘f · 𝐹 ) ) = 𝑂 ) → 𝑎 = ( 𝐼 × { 0 } ) ) ) )
29	28	imbi2d	⊢ ( 𝜑 → ( ( 𝑎 ∈ ( 𝐾 ↑m 𝐼 ) → ( 𝑎 finSupp 0 → ( ( 𝑊 Σg ( 𝑎 ∘f · 𝐹 ) ) = 𝑂 → 𝑎 = ( 𝐼 × { 0 } ) ) ) ) ↔ ( 𝑎 ∈ ( 𝐾 ↑m 𝐼 ) → ( ( 𝑎 finSupp 0 ∧ ( 𝑊 Σg ( 𝑎 ∘f · 𝐹 ) ) = 𝑂 ) → 𝑎 = ( 𝐼 × { 0 } ) ) ) ) )
30	25 29	bitrid	⊢ ( 𝜑 → ( ( ( 𝑎 ∈ ( 𝐾 ↑m 𝐼 ) ∧ 𝑎 finSupp 0 ) → ( ( 𝑊 Σg ( 𝑎 ∘f · 𝐹 ) ) = 𝑂 → 𝑎 = ( 𝐼 × { 0 } ) ) ) ↔ ( 𝑎 ∈ ( 𝐾 ↑m 𝐼 ) → ( ( 𝑎 finSupp 0 ∧ ( 𝑊 Σg ( 𝑎 ∘f · 𝐹 ) ) = 𝑂 ) → 𝑎 = ( 𝐼 × { 0 } ) ) ) ) )
31	24 30	bitrd	⊢ ( 𝜑 → ( ( 𝑎 ∈ ( Base ‘ ( 𝑆 freeLMod 𝐼 ) ) → ( ( 𝑊 Σg ( 𝑎 ∘f · 𝐹 ) ) = 𝑂 → 𝑎 = ( 𝐼 × { 0 } ) ) ) ↔ ( 𝑎 ∈ ( 𝐾 ↑m 𝐼 ) → ( ( 𝑎 finSupp 0 ∧ ( 𝑊 Σg ( 𝑎 ∘f · 𝐹 ) ) = 𝑂 ) → 𝑎 = ( 𝐼 × { 0 } ) ) ) ) )
32	31	ralbidv2	⊢ ( 𝜑 → ( ∀ 𝑎 ∈ ( Base ‘ ( 𝑆 freeLMod 𝐼 ) ) ( ( 𝑊 Σg ( 𝑎 ∘f · 𝐹 ) ) = 𝑂 → 𝑎 = ( 𝐼 × { 0 } ) ) ↔ ∀ 𝑎 ∈ ( 𝐾 ↑m 𝐼 ) ( ( 𝑎 finSupp 0 ∧ ( 𝑊 Σg ( 𝑎 ∘f · 𝐹 ) ) = 𝑂 ) → 𝑎 = ( 𝐼 × { 0 } ) ) ) )
33	19 32	bitrd	⊢ ( 𝜑 → ( 𝐹 LIndF 𝑊 ↔ ∀ 𝑎 ∈ ( 𝐾 ↑m 𝐼 ) ( ( 𝑎 finSupp 0 ∧ ( 𝑊 Σg ( 𝑎 ∘f · 𝐹 ) ) = 𝑂 ) → 𝑎 = ( 𝐼 × { 0 } ) ) ) )
34	33	anbi1d	⊢ ( 𝜑 → ( ( 𝐹 LIndF 𝑊 ∧ ( 𝑁 ‘ ran 𝐹 ) = 𝐵 ) ↔ ( ∀ 𝑎 ∈ ( 𝐾 ↑m 𝐼 ) ( ( 𝑎 finSupp 0 ∧ ( 𝑊 Σg ( 𝑎 ∘f · 𝐹 ) ) = 𝑂 ) → 𝑎 = ( 𝐼 × { 0 } ) ) ∧ ( 𝑁 ‘ ran 𝐹 ) = 𝐵 ) ) )
35	14 34	bitrd	⊢ ( 𝜑 → ( ran 𝐹 ∈ ( LBasis ‘ 𝑊 ) ↔ ( ∀ 𝑎 ∈ ( 𝐾 ↑m 𝐼 ) ( ( 𝑎 finSupp 0 ∧ ( 𝑊 Σg ( 𝑎 ∘f · 𝐹 ) ) = 𝑂 ) → 𝑎 = ( 𝐼 × { 0 } ) ) ∧ ( 𝑁 ‘ ran 𝐹 ) = 𝐵 ) ) )