ellspds

Description: Variation on ellspd . (Contributed by Thierry Arnoux, 18-May-2023)

	Ref	Expression
Hypotheses	ellspds.n	$⊢ N = LSpan (M)$
	ellspds.v	$⊢ B = {Base}_{M}$
	ellspds.k	$⊢ K = {Base}_{S}$
	ellspds.s	$⊢ S = Scalar (M)$
	ellspds.z	$⊢ \underset{˙}{0} = 0_{S}$
	ellspds.t	$⊢ \underset{˙}{\cdot} = \cdot_{M}$
	ellspds.m	$⊢ φ \to M \in LMod$
	ellspds.1	$⊢ φ \to V \subseteq B$
Assertion	ellspds	$⊢ φ \to (X \in N (V) \leftrightarrow \exists a \in (K^{V}) ({finSupp}_{\underset{˙}{0}} (a) \land X = \underset{v \in V}{\sum_{M}} (a (v) \underset{˙}{\cdot} v)))$

Proof

Step	Hyp	Ref	Expression
1		ellspds.n	$⊢ N = LSpan (M)$
2		ellspds.v	$⊢ B = {Base}_{M}$
3		ellspds.k	$⊢ K = {Base}_{S}$
4		ellspds.s	$⊢ S = Scalar (M)$
5		ellspds.z	$⊢ \underset{˙}{0} = 0_{S}$
6		ellspds.t	$⊢ \underset{˙}{\cdot} = \cdot_{M}$
7		ellspds.m	$⊢ φ \to M \in LMod$
8		ellspds.1	$⊢ φ \to V \subseteq B$
9		f1oi	$⊢ ({I ↾}_{V}) : V \underset{1-1 onto}{⟶} V$
10		f1of	$⊢ ({I ↾}_{V}) : V \underset{1-1 onto}{⟶} V \to ({I ↾}_{V}) : V ⟶ V$
11	9 10	mp1i	$⊢ φ \to ({I ↾}_{V}) : V ⟶ V$
12	11 8	fssd	$⊢ φ \to ({I ↾}_{V}) : V ⟶ B$
13	2	fvexi	$⊢ B \in V$
14	13	a1i	$⊢ φ \to B \in V$
15	14 8	ssexd	$⊢ φ \to V \in V$
16	1 2 3 4 5 6 12 7 15	ellspd	$⊢ φ \to (X \in N (({I ↾}_{V}) [V]) \leftrightarrow \exists a \in (K^{V}) ({finSupp}_{\underset{˙}{0}} (a) \land X = \sum_{M} (a {\underset{˙}{\cdot}}_{f} ({I ↾}_{V}))))$
17		ssid	$⊢ V \subseteq V$
18		resiima	$⊢ V \subseteq V \to ({I ↾}_{V}) [V] = V$
19	17 18	mp1i	$⊢ φ \to ({I ↾}_{V}) [V] = V$
20	19	fveq2d	$⊢ φ \to N (({I ↾}_{V}) [V]) = N (V)$
21	20	eleq2d	$⊢ φ \to (X \in N (({I ↾}_{V}) [V]) \leftrightarrow X \in N (V))$
22		elmapfn	$⊢ a \in (K^{V}) \to a Fn V$
23	22	adantl	$⊢ (φ \land a \in (K^{V})) \to a Fn V$
24	9 10	mp1i	$⊢ (φ \land a \in (K^{V})) \to ({I ↾}_{V}) : V ⟶ V$
25	24	ffnd	$⊢ (φ \land a \in (K^{V})) \to ({I ↾}_{V}) Fn V$
26	15	adantr	$⊢ (φ \land a \in (K^{V})) \to V \in V$
27		inidm	$⊢ V \cap V = V$
28		eqidd	$⊢ ((φ \land a \in (K^{V})) \land v \in V) \to a (v) = a (v)$
29		fvresi	$⊢ v \in V \to ({I ↾}_{V}) (v) = v$
30	29	adantl	$⊢ ((φ \land a \in (K^{V})) \land v \in V) \to ({I ↾}_{V}) (v) = v$
31	23 25 26 26 27 28 30	offval	$⊢ (φ \land a \in (K^{V})) \to a {\underset{˙}{\cdot}}_{f} ({I ↾}_{V}) = (v \in V ⟼ a (v) \underset{˙}{\cdot} v)$
32	31	oveq2d	$⊢ (φ \land a \in (K^{V})) \to \sum_{M} (a {\underset{˙}{\cdot}}_{f} ({I ↾}_{V})) = \underset{v \in V}{\sum_{M}} (a (v) \underset{˙}{\cdot} v)$
33	32	eqeq2d	$⊢ (φ \land a \in (K^{V})) \to (X = \sum_{M} (a {\underset{˙}{\cdot}}_{f} ({I ↾}_{V})) \leftrightarrow X = \underset{v \in V}{\sum_{M}} (a (v) \underset{˙}{\cdot} v))$
34	33	anbi2d	$⊢ (φ \land a \in (K^{V})) \to (({finSupp}_{\underset{˙}{0}} (a) \land X = \sum_{M} (a {\underset{˙}{\cdot}}_{f} ({I ↾}_{V}))) \leftrightarrow ({finSupp}_{\underset{˙}{0}} (a) \land X = \underset{v \in V}{\sum_{M}} (a (v) \underset{˙}{\cdot} v)))$
35	34	rexbidva	$⊢ φ \to (\exists a \in (K^{V}) ({finSupp}_{\underset{˙}{0}} (a) \land X = \sum_{M} (a {\underset{˙}{\cdot}}_{f} ({I ↾}_{V}))) \leftrightarrow \exists a \in (K^{V}) ({finSupp}_{\underset{˙}{0}} (a) \land X = \underset{v \in V}{\sum_{M}} (a (v) \underset{˙}{\cdot} v)))$
36	16 21 35	3bitr3d	$⊢ φ \to (X \in N (V) \leftrightarrow \exists a \in (K^{V}) ({finSupp}_{\underset{˙}{0}} (a) \land X = \underset{v \in V}{\sum_{M}} (a (v) \underset{˙}{\cdot} v)))$

Metamath Proof Explorer

Theorem ellspds

Proof