Metamath Proof Explorer


Theorem mapdh75cN

Description: Part (7) of Baer p. 48 line 10 (3 of 6 cases). (Contributed by NM, 2-May-2015) (New usage is discouraged.)

Ref Expression
Hypotheses mapdh75.h H = LHyp K
mapdh75.u U = DVecH K W
mapdh75.v V = Base U
mapdh75.s - ˙ = - U
mapdh75.o 0 ˙ = 0 U
mapdh75.n N = LSpan U
mapdh75.c C = LCDual K W
mapdh75.d D = Base C
mapdh75.r R = - C
mapdh75.q Q = 0 C
mapdh75.j J = LSpan C
mapdh75.m M = mapd K W
mapdh75.i I = x V if 2 nd x = 0 ˙ Q ι h D | M N 2 nd x = J h M N 1 st 1 st x - ˙ 2 nd x = J 2 nd 1 st x R h
mapdh75.k φ K HL W H
mapdh75.f φ F D
mapdh75.mn φ M N X = J F
mapdh75a φ I X F Y = G
mapdh75c.ne φ N X N Y
mapdh75c.x φ X V 0 ˙
mapdh75c.y φ Y V 0 ˙
Assertion mapdh75cN φ I Y G X = F

Proof

Step Hyp Ref Expression
1 mapdh75.h H = LHyp K
2 mapdh75.u U = DVecH K W
3 mapdh75.v V = Base U
4 mapdh75.s - ˙ = - U
5 mapdh75.o 0 ˙ = 0 U
6 mapdh75.n N = LSpan U
7 mapdh75.c C = LCDual K W
8 mapdh75.d D = Base C
9 mapdh75.r R = - C
10 mapdh75.q Q = 0 C
11 mapdh75.j J = LSpan C
12 mapdh75.m M = mapd K W
13 mapdh75.i I = x V if 2 nd x = 0 ˙ Q ι h D | M N 2 nd x = J h M N 1 st 1 st x - ˙ 2 nd x = J 2 nd 1 st x R h
14 mapdh75.k φ K HL W H
15 mapdh75.f φ F D
16 mapdh75.mn φ M N X = J F
17 mapdh75a φ I X F Y = G
18 mapdh75c.ne φ N X N Y
19 mapdh75c.x φ X V 0 ˙
20 mapdh75c.y φ Y V 0 ˙
21 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 mapdh75e φ I Y G X = F