Metamath Proof Explorer

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 𝐹 ) = 𝐵 ) ) )