Metamath Proof Explorer


Theorem 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 + ˙ = + W
lshpkrlem.n N = LSpan W
lshpkrlem.p ˙ = LSSum W
lshpkrlem.h H = LSHyp W
lshpkrlem.w φ W LVec
lshpkrlem.u φ U H
lshpkrlem.z φ Z V
lshpkrlem.x φ X V
lshpkrlem.e φ U ˙ N Z = V
lshpkrlem.d D = Scalar W
lshpkrlem.k K = Base D
lshpkrlem.t · ˙ = W
lshpkrlem.o 0 ˙ = 0 D
lshpkrlem.g G = x V ι k K | y U x = y + ˙ k · ˙ Z
Assertion lshpkrlem2 φ G X K

Proof

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