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	$⊢ B = {Base}_{W}$
	islbs5.k	$⊢ K = {Base}_{S}$
	islbs5.r	$⊢ S = Scalar (W)$
	islbs5.t	$⊢ \underset{˙}{\cdot} = \cdot_{W}$
	islbs5.z	$⊢ O = 0_{W}$
	islbs5.y	$⊢ \underset{˙}{0} = 0_{S}$
	islbs5.j	$⊢ J = LBasis (W)$
	islbs5.n	$⊢ N = LSpan (W)$
	islbs5.w	$⊢ φ \to W \in LMod$
	islbs5.s	$⊢ φ \to S \in NzRing$
	islbs5.i	$⊢ φ \to I \in V$
	islbs5.f	$⊢ φ \to F : I \underset{1-1}{⟶} B$
Assertion	islbs5	$⊢ φ \to (ran F \in LBasis (W) \leftrightarrow (\forall a \in (K^{I}) (({finSupp}_{\underset{˙}{0}} (a) \land \sum_{W} (a {\underset{˙}{\cdot}}_{f} F) = O) \to a = I \times \{\underset{˙}{0}\}) \land N (ran F) = B))$

Proof

Step	Hyp	Ref	Expression
1		islbs5.b	$⊢ B = {Base}_{W}$
2		islbs5.k	$⊢ K = {Base}_{S}$
3		islbs5.r	$⊢ S = Scalar (W)$
4		islbs5.t	$⊢ \underset{˙}{\cdot} = \cdot_{W}$
5		islbs5.z	$⊢ O = 0_{W}$
6		islbs5.y	$⊢ \underset{˙}{0} = 0_{S}$
7		islbs5.j	$⊢ J = LBasis (W)$
8		islbs5.n	$⊢ N = LSpan (W)$
9		islbs5.w	$⊢ φ \to W \in LMod$
10		islbs5.s	$⊢ φ \to S \in NzRing$
11		islbs5.i	$⊢ φ \to I \in V$
12		islbs5.f	$⊢ φ \to F : I \underset{1-1}{⟶} B$
13		eqid	$⊢ {Base}_{F} = {Base}_{F}$
14	1 13 3 4 5 6 8 9 10 11 12	lindflbs	$⊢ φ \to (ran F \in LBasis (W) \leftrightarrow (F LIndF W \land N (ran F) = B))$
15		f1f	$⊢ F : I \underset{1-1}{⟶} B \to F : I ⟶ B$
16	12 15	syl	$⊢ φ \to F : I ⟶ B$
17		eqid	$⊢ {Base}_{(S freeLMod I)} = {Base}_{(S freeLMod I)}$
18	1 3 4 5 6 17	islindf4	$⊢ (W \in LMod \land I \in V \land F : I ⟶ B) \to (F LIndF W \leftrightarrow \forall a \in {Base}_{(S freeLMod I)} (\sum_{W} (a {\underset{˙}{\cdot}}_{f} F) = O \to a = I \times \{\underset{˙}{0}\}))$
19	9 11 16 18	syl3anc	$⊢ φ \to (F LIndF W \leftrightarrow \forall a \in {Base}_{(S freeLMod I)} (\sum_{W} (a {\underset{˙}{\cdot}}_{f} F) = O \to a = I \times \{\underset{˙}{0}\}))$
20	10	elexd	$⊢ φ \to S \in V$
21		eqid	$⊢ S freeLMod I = S freeLMod I$
22	21 2 6 17	frlmelbas	$⊢ (S \in V \land I \in V) \to (a \in {Base}_{(S freeLMod I)} \leftrightarrow (a \in (K^{I}) \land {finSupp}_{\underset{˙}{0}} (a)))$
23	20 11 22	syl2anc	$⊢ φ \to (a \in {Base}_{(S freeLMod I)} \leftrightarrow (a \in (K^{I}) \land {finSupp}_{\underset{˙}{0}} (a)))$
24	23	imbi1d	$⊢ φ \to ((a \in {Base}_{(S freeLMod I)} \to (\sum_{W} (a {\underset{˙}{\cdot}}_{f} F) = O \to a = I \times \{\underset{˙}{0}\})) \leftrightarrow ((a \in (K^{I}) \land {finSupp}_{\underset{˙}{0}} (a)) \to (\sum_{W} (a {\underset{˙}{\cdot}}_{f} F) = O \to a = I \times \{\underset{˙}{0}\})))$
25		impexp	$⊢ ((a \in (K^{I}) \land {finSupp}_{\underset{˙}{0}} (a)) \to (\sum_{W} (a {\underset{˙}{\cdot}}_{f} F) = O \to a = I \times \{\underset{˙}{0}\})) \leftrightarrow (a \in (K^{I}) \to ({finSupp}_{\underset{˙}{0}} (a) \to (\sum_{W} (a {\underset{˙}{\cdot}}_{f} F) = O \to a = I \times \{\underset{˙}{0}\})))$
26		impexp	$⊢ (({finSupp}_{\underset{˙}{0}} (a) \land \sum_{W} (a {\underset{˙}{\cdot}}_{f} F) = O) \to a = I \times \{\underset{˙}{0}\}) \leftrightarrow ({finSupp}_{\underset{˙}{0}} (a) \to (\sum_{W} (a {\underset{˙}{\cdot}}_{f} F) = O \to a = I \times \{\underset{˙}{0}\}))$
27	26	a1i	$⊢ φ \to ((({finSupp}_{\underset{˙}{0}} (a) \land \sum_{W} (a {\underset{˙}{\cdot}}_{f} F) = O) \to a = I \times \{\underset{˙}{0}\}) \leftrightarrow ({finSupp}_{\underset{˙}{0}} (a) \to (\sum_{W} (a {\underset{˙}{\cdot}}_{f} F) = O \to a = I \times \{\underset{˙}{0}\})))$
28	27	bicomd	$⊢ φ \to (({finSupp}_{\underset{˙}{0}} (a) \to (\sum_{W} (a {\underset{˙}{\cdot}}_{f} F) = O \to a = I \times \{\underset{˙}{0}\})) \leftrightarrow (({finSupp}_{\underset{˙}{0}} (a) \land \sum_{W} (a {\underset{˙}{\cdot}}_{f} F) = O) \to a = I \times \{\underset{˙}{0}\}))$
29	28	imbi2d	$⊢ φ \to ((a \in (K^{I}) \to ({finSupp}_{\underset{˙}{0}} (a) \to (\sum_{W} (a {\underset{˙}{\cdot}}_{f} F) = O \to a = I \times \{\underset{˙}{0}\}))) \leftrightarrow (a \in (K^{I}) \to (({finSupp}_{\underset{˙}{0}} (a) \land \sum_{W} (a {\underset{˙}{\cdot}}_{f} F) = O) \to a = I \times \{\underset{˙}{0}\})))$
30	25 29	bitrid	$⊢ φ \to (((a \in (K^{I}) \land {finSupp}_{\underset{˙}{0}} (a)) \to (\sum_{W} (a {\underset{˙}{\cdot}}_{f} F) = O \to a = I \times \{\underset{˙}{0}\})) \leftrightarrow (a \in (K^{I}) \to (({finSupp}_{\underset{˙}{0}} (a) \land \sum_{W} (a {\underset{˙}{\cdot}}_{f} F) = O) \to a = I \times \{\underset{˙}{0}\})))$
31	24 30	bitrd	$⊢ φ \to ((a \in {Base}_{(S freeLMod I)} \to (\sum_{W} (a {\underset{˙}{\cdot}}_{f} F) = O \to a = I \times \{\underset{˙}{0}\})) \leftrightarrow (a \in (K^{I}) \to (({finSupp}_{\underset{˙}{0}} (a) \land \sum_{W} (a {\underset{˙}{\cdot}}_{f} F) = O) \to a = I \times \{\underset{˙}{0}\})))$
32	31	ralbidv2	$⊢ φ \to (\forall a \in {Base}_{(S freeLMod I)} (\sum_{W} (a {\underset{˙}{\cdot}}_{f} F) = O \to a = I \times \{\underset{˙}{0}\}) \leftrightarrow \forall a \in (K^{I}) (({finSupp}_{\underset{˙}{0}} (a) \land \sum_{W} (a {\underset{˙}{\cdot}}_{f} F) = O) \to a = I \times \{\underset{˙}{0}\}))$
33	19 32	bitrd	$⊢ φ \to (F LIndF W \leftrightarrow \forall a \in (K^{I}) (({finSupp}_{\underset{˙}{0}} (a) \land \sum_{W} (a {\underset{˙}{\cdot}}_{f} F) = O) \to a = I \times \{\underset{˙}{0}\}))$
34	33	anbi1d	$⊢ φ \to ((F LIndF W \land N (ran F) = B) \leftrightarrow (\forall a \in (K^{I}) (({finSupp}_{\underset{˙}{0}} (a) \land \sum_{W} (a {\underset{˙}{\cdot}}_{f} F) = O) \to a = I \times \{\underset{˙}{0}\}) \land N (ran F) = B))$
35	14 34	bitrd	$⊢ φ \to (ran F \in LBasis (W) \leftrightarrow (\forall a \in (K^{I}) (({finSupp}_{\underset{˙}{0}} (a) \land \sum_{W} (a {\underset{˙}{\cdot}}_{f} F) = O) \to a = I \times \{\underset{˙}{0}\}) \land N (ran F) = B))$

Metamath Proof Explorer

Theorem islbs5

Proof