lshpkrlem2

Description: Lemma for lshpkrex . The value of tentative functional G is a scalar. (Contributed by NM, 16-Jul-2014)

	Ref	Expression
Hypotheses	lshpkrlem.v	$⊢ V = {Base}_{W}$
	lshpkrlem.a	$⊢ \underset{˙}{+} = +_{W}$
	lshpkrlem.n	$⊢ N = LSpan (W)$
	lshpkrlem.p	$⊢ \underset{˙}{\oplus} = LSSum (W)$
	lshpkrlem.h	$⊢ H = LSHyp (W)$
	lshpkrlem.w	$⊢ φ \to W \in LVec$
	lshpkrlem.u	$⊢ φ \to U \in H$
	lshpkrlem.z	$⊢ φ \to Z \in V$
	lshpkrlem.x	$⊢ φ \to X \in V$
	lshpkrlem.e	$⊢ φ \to U \underset{˙}{\oplus} N (\{Z\}) = V$
	lshpkrlem.d	$⊢ D = Scalar (W)$
	lshpkrlem.k	$⊢ K = {Base}_{D}$
	lshpkrlem.t	$⊢ \underset{˙}{\cdot} = \cdot_{W}$
	lshpkrlem.o	$⊢ \underset{˙}{0} = 0_{D}$
	lshpkrlem.g	$⊢ G = (x \in V ⟼ (ι k \in K \| \exists y \in U x = y \underset{˙}{+} (k \underset{˙}{\cdot} Z)))$
Assertion	lshpkrlem2	$⊢ φ \to G (X) \in K$

Proof

Step	Hyp	Ref	Expression
1		lshpkrlem.v	$⊢ V = {Base}_{W}$
2		lshpkrlem.a	$⊢ \underset{˙}{+} = +_{W}$
3		lshpkrlem.n	$⊢ N = LSpan (W)$
4		lshpkrlem.p	$⊢ \underset{˙}{\oplus} = LSSum (W)$
5		lshpkrlem.h	$⊢ H = LSHyp (W)$
6		lshpkrlem.w	$⊢ φ \to W \in LVec$
7		lshpkrlem.u	$⊢ φ \to U \in H$
8		lshpkrlem.z	$⊢ φ \to Z \in V$
9		lshpkrlem.x	$⊢ φ \to X \in V$
10		lshpkrlem.e	$⊢ φ \to U \underset{˙}{\oplus} N (\{Z\}) = V$
11		lshpkrlem.d	$⊢ D = Scalar (W)$
12		lshpkrlem.k	$⊢ K = {Base}_{D}$
13		lshpkrlem.t	$⊢ \underset{˙}{\cdot} = \cdot_{W}$
14		lshpkrlem.o	$⊢ \underset{˙}{0} = 0_{D}$
15		lshpkrlem.g	$⊢ G = (x \in V ⟼ (ι k \in K \| \exists y \in U x = y \underset{˙}{+} (k \underset{˙}{\cdot} Z)))$
16		eqeq1	$⊢ x = X \to (x = y \underset{˙}{+} (k \underset{˙}{\cdot} Z) \leftrightarrow X = y \underset{˙}{+} (k \underset{˙}{\cdot} Z))$
17	16	rexbidv	$⊢ x = X \to (\exists y \in U x = y \underset{˙}{+} (k \underset{˙}{\cdot} Z) \leftrightarrow \exists y \in U X = y \underset{˙}{+} (k \underset{˙}{\cdot} Z))$
18	17	riotabidv	$⊢ x = X \to (ι k \in K \| \exists y \in U x = y \underset{˙}{+} (k \underset{˙}{\cdot} Z)) = (ι k \in K \| \exists y \in U X = y \underset{˙}{+} (k \underset{˙}{\cdot} Z))$
19		riotaex	$⊢ (ι k \in K \| \exists y \in U X = y \underset{˙}{+} (k \underset{˙}{\cdot} Z)) \in V$
20	18 15 19	fvmpt	$⊢ X \in V \to G (X) = (ι k \in K \| \exists y \in U X = y \underset{˙}{+} (k \underset{˙}{\cdot} Z))$
21	9 20	syl	$⊢ φ \to G (X) = (ι k \in K \| \exists y \in U X = y \underset{˙}{+} (k \underset{˙}{\cdot} Z))$
22	1 2 3 4 5 6 7 8 9 10 11 12 13	lshpsmreu	$⊢ φ \to \exists! k \in K \exists y \in U X = y \underset{˙}{+} (k \underset{˙}{\cdot} Z)$
23		riotacl	$⊢ \exists! k \in K \exists y \in U X = y \underset{˙}{+} (k \underset{˙}{\cdot} Z) \to (ι k \in K \| \exists y \in U X = y \underset{˙}{+} (k \underset{˙}{\cdot} Z)) \in K$
24	22 23	syl	$⊢ φ \to (ι k \in K \| \exists y \in U X = y \underset{˙}{+} (k \underset{˙}{\cdot} Z)) \in K$
25	21 24	eqeltrd	$⊢ φ \to G (X) \in K$

Metamath Proof Explorer

Theorem lshpkrlem2

Proof