lcoval

Description: The value of a linear combination. (Contributed by AV, 5-Apr-2019) (Revised by AV, 28-Jul-2019)

	Ref	Expression
Hypotheses	lcoop.b	$⊢ B = {Base}_{M}$
	lcoop.s	$⊢ S = Scalar (M)$
	lcoop.r	$⊢ R = {Base}_{S}$
Assertion	lcoval	$⊢ (M \in X \land V \in 𝒫 B) \to (C \in (M LinCo V) \leftrightarrow (C \in B \land \exists s \in (R^{V}) ({finSupp}_{0_{S}} (s) \land C = s linC (M) V)))$

Step	Hyp	Ref	Expression
1		lcoop.b	$⊢ B = {Base}_{M}$
2		lcoop.s	$⊢ S = Scalar (M)$
3		lcoop.r	$⊢ R = {Base}_{S}$
4	1 2 3	lcoop	$⊢ (M \in X \land V \in 𝒫 B) \to M LinCo V = \{c \in B \| \exists s \in (R^{V}) ({finSupp}_{0_{S}} (s) \land c = s linC (M) V)\}$
5	4	eleq2d	$⊢ (M \in X \land V \in 𝒫 B) \to (C \in (M LinCo V) \leftrightarrow C \in \{c \in B \| \exists s \in (R^{V}) ({finSupp}_{0_{S}} (s) \land c = s linC (M) V)\})$
6		eqeq1	$⊢ c = C \to (c = s linC (M) V \leftrightarrow C = s linC (M) V)$
7	6	anbi2d	$⊢ c = C \to (({finSupp}_{0_{S}} (s) \land c = s linC (M) V) \leftrightarrow ({finSupp}_{0_{S}} (s) \land C = s linC (M) V))$
8	7	rexbidv	$⊢ c = C \to (\exists s \in (R^{V}) ({finSupp}_{0_{S}} (s) \land c = s linC (M) V) \leftrightarrow \exists s \in (R^{V}) ({finSupp}_{0_{S}} (s) \land C = s linC (M) V))$
9	8	elrab	$⊢ C \in \{c \in B \| \exists s \in (R^{V}) ({finSupp}_{0_{S}} (s) \land c = s linC (M) V)\} \leftrightarrow (C \in B \land \exists s \in (R^{V}) ({finSupp}_{0_{S}} (s) \land C = s linC (M) V))$
10	5 9	bitrdi	$⊢ (M \in X \land V \in 𝒫 B) \to (C \in (M LinCo V) \leftrightarrow (C \in B \land \exists s \in (R^{V}) ({finSupp}_{0_{S}} (s) \land C = s linC (M) V)))$

Metamath Proof Explorer