Metamath Proof Explorer


Theorem lshpkrlem3

Description: Lemma for lshpkrex . Defining property of GX . (Contributed by NM, 15-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 lshpkrlem3 φ z U X = z + ˙ G X · ˙ Z

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 1 2 3 4 5 6 7 8 9 10 11 12 13 lshpsmreu φ ∃! l K z U X = z + ˙ l · ˙ Z
17 riotasbc ∃! l K z U X = z + ˙ l · ˙ Z [˙ ι l K | z U X = z + ˙ l · ˙ Z / l]˙ z U X = z + ˙ l · ˙ Z
18 16 17 syl φ [˙ ι l K | z U X = z + ˙ l · ˙ Z / l]˙ z U X = z + ˙ l · ˙ Z
19 eqeq1 x = X x = z + ˙ l · ˙ Z X = z + ˙ l · ˙ Z
20 19 rexbidv x = X z U x = z + ˙ l · ˙ Z z U X = z + ˙ l · ˙ Z
21 20 riotabidv x = X ι l K | z U x = z + ˙ l · ˙ Z = ι l K | z U X = z + ˙ l · ˙ Z
22 oveq1 k = l k · ˙ Z = l · ˙ Z
23 22 oveq2d k = l y + ˙ k · ˙ Z = y + ˙ l · ˙ Z
24 23 eqeq2d k = l x = y + ˙ k · ˙ Z x = y + ˙ l · ˙ Z
25 24 rexbidv k = l y U x = y + ˙ k · ˙ Z y U x = y + ˙ l · ˙ Z
26 oveq1 y = z y + ˙ l · ˙ Z = z + ˙ l · ˙ Z
27 26 eqeq2d y = z x = y + ˙ l · ˙ Z x = z + ˙ l · ˙ Z
28 27 cbvrexvw y U x = y + ˙ l · ˙ Z z U x = z + ˙ l · ˙ Z
29 25 28 bitrdi k = l y U x = y + ˙ k · ˙ Z z U x = z + ˙ l · ˙ Z
30 29 cbvriotavw ι k K | y U x = y + ˙ k · ˙ Z = ι l K | z U x = z + ˙ l · ˙ Z
31 30 mpteq2i x V ι k K | y U x = y + ˙ k · ˙ Z = x V ι l K | z U x = z + ˙ l · ˙ Z
32 15 31 eqtri G = x V ι l K | z U x = z + ˙ l · ˙ Z
33 riotaex ι l K | z U X = z + ˙ l · ˙ Z V
34 21 32 33 fvmpt X V G X = ι l K | z U X = z + ˙ l · ˙ Z
35 dfsbcq G X = ι l K | z U X = z + ˙ l · ˙ Z [˙ G X / l]˙ z U X = z + ˙ l · ˙ Z [˙ ι l K | z U X = z + ˙ l · ˙ Z / l]˙ z U X = z + ˙ l · ˙ Z
36 9 34 35 3syl φ [˙ G X / l]˙ z U X = z + ˙ l · ˙ Z [˙ ι l K | z U X = z + ˙ l · ˙ Z / l]˙ z U X = z + ˙ l · ˙ Z
37 18 36 mpbird φ [˙ G X / l]˙ z U X = z + ˙ l · ˙ Z
38 fvex G X V
39 oveq1 l = G X l · ˙ Z = G X · ˙ Z
40 39 oveq2d l = G X z + ˙ l · ˙ Z = z + ˙ G X · ˙ Z
41 40 eqeq2d l = G X X = z + ˙ l · ˙ Z X = z + ˙ G X · ˙ Z
42 41 rexbidv l = G X z U X = z + ˙ l · ˙ Z z U X = z + ˙ G X · ˙ Z
43 38 42 sbcie [˙ G X / l]˙ z U X = z + ˙ l · ˙ Z z U X = z + ˙ G X · ˙ Z
44 37 43 sylib φ z U X = z + ˙ G X · ˙ Z