Metamath Proof Explorer


Theorem hdmap14lem14

Description: Part of proof of part 14 in Baer p. 50 line 3. (Contributed by NM, 6-Jun-2015)

Ref Expression
Hypotheses hdmap14lem12.h H = LHyp K
hdmap14lem12.u U = DVecH K W
hdmap14lem12.v V = Base U
hdmap14lem12.t · ˙ = U
hdmap14lem12.r R = Scalar U
hdmap14lem12.b B = Base R
hdmap14lem12.c C = LCDual K W
hdmap14lem12.e ˙ = C
hdmap14lem12.s S = HDMap K W
hdmap14lem12.k φ K HL W H
hdmap14lem12.f φ F B
hdmap14lem12.p P = Scalar C
hdmap14lem12.a A = Base P
Assertion hdmap14lem14 φ ∃! g A x V S F · ˙ x = g ˙ S x

Proof

Step Hyp Ref Expression
1 hdmap14lem12.h H = LHyp K
2 hdmap14lem12.u U = DVecH K W
3 hdmap14lem12.v V = Base U
4 hdmap14lem12.t · ˙ = U
5 hdmap14lem12.r R = Scalar U
6 hdmap14lem12.b B = Base R
7 hdmap14lem12.c C = LCDual K W
8 hdmap14lem12.e ˙ = C
9 hdmap14lem12.s S = HDMap K W
10 hdmap14lem12.k φ K HL W H
11 hdmap14lem12.f φ F B
12 hdmap14lem12.p P = Scalar C
13 hdmap14lem12.a A = Base P
14 eqid 0 U = 0 U
15 1 2 3 14 10 dvh1dim φ y V y 0 U
16 10 3ad2ant1 φ y V y 0 U K HL W H
17 3simpc φ y V y 0 U y V y 0 U
18 eldifsn y V 0 U y V y 0 U
19 17 18 sylibr φ y V y 0 U y V 0 U
20 11 3ad2ant1 φ y V y 0 U F B
21 1 2 3 4 14 5 6 7 8 12 13 9 16 19 20 hdmap14lem7 φ y V y 0 U ∃! g A S F · ˙ y = g ˙ S y
22 simpl1 φ y V y 0 U g A φ
23 22 10 syl φ y V y 0 U g A K HL W H
24 22 11 syl φ y V y 0 U g A F B
25 19 adantr φ y V y 0 U g A y V 0 U
26 simpr φ y V y 0 U g A g A
27 1 2 3 4 5 6 7 8 9 23 24 12 13 14 25 26 hdmap14lem13 φ y V y 0 U g A S F · ˙ y = g ˙ S y x V S F · ˙ x = g ˙ S x
28 27 reubidva φ y V y 0 U ∃! g A S F · ˙ y = g ˙ S y ∃! g A x V S F · ˙ x = g ˙ S x
29 21 28 mpbid φ y V y 0 U ∃! g A x V S F · ˙ x = g ˙ S x
30 29 rexlimdv3a φ y V y 0 U ∃! g A x V S F · ˙ x = g ˙ S x
31 15 30 mpd φ ∃! g A x V S F · ˙ x = g ˙ S x