Metamath Proof Explorer


Theorem hdmap14lem4

Description: Simplify ( A \ { Q } ) in hdmap14lem3 to provide a slightly simpler definition later. TODO: Use hdmap14lem4a if that one is also used directly elsewhere. Otherwise, merge hdmap14lem4a into this one. (Contributed by NM, 31-May-2015)

Ref Expression
Hypotheses hdmap14lem1.h H = LHyp K
hdmap14lem1.u U = DVecH K W
hdmap14lem1.v V = Base U
hdmap14lem1.t · ˙ = U
hdmap14lem3.o 0 ˙ = 0 U
hdmap14lem1.r R = Scalar U
hdmap14lem1.b B = Base R
hdmap14lem1.z Z = 0 R
hdmap14lem1.c C = LCDual K W
hdmap14lem2.e ˙ = C
hdmap14lem1.l L = LSpan C
hdmap14lem2.p P = Scalar C
hdmap14lem2.a A = Base P
hdmap14lem2.q Q = 0 P
hdmap14lem1.s S = HDMap K W
hdmap14lem1.k φ K HL W H
hdmap14lem3.x φ X V 0 ˙
hdmap14lem1.f φ F B Z
Assertion hdmap14lem4 φ ∃! g A S F · ˙ X = g ˙ S X

Proof

Step Hyp Ref Expression
1 hdmap14lem1.h H = LHyp K
2 hdmap14lem1.u U = DVecH K W
3 hdmap14lem1.v V = Base U
4 hdmap14lem1.t · ˙ = U
5 hdmap14lem3.o 0 ˙ = 0 U
6 hdmap14lem1.r R = Scalar U
7 hdmap14lem1.b B = Base R
8 hdmap14lem1.z Z = 0 R
9 hdmap14lem1.c C = LCDual K W
10 hdmap14lem2.e ˙ = C
11 hdmap14lem1.l L = LSpan C
12 hdmap14lem2.p P = Scalar C
13 hdmap14lem2.a A = Base P
14 hdmap14lem2.q Q = 0 P
15 hdmap14lem1.s S = HDMap K W
16 hdmap14lem1.k φ K HL W H
17 hdmap14lem3.x φ X V 0 ˙
18 hdmap14lem1.f φ F B Z
19 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 hdmap14lem3 φ ∃! g A Q S F · ˙ X = g ˙ S X
20 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 hdmap14lem4a φ ∃! g A Q S F · ˙ X = g ˙ S X ∃! g A S F · ˙ X = g ˙ S X
21 19 20 mpbid φ ∃! g A S F · ˙ X = g ˙ S X