Metamath Proof Explorer


Theorem mapdh75d

Description: Part (7) of Baer p. 48 line 10 (4 of 6 cases). (Contributed by NM, 2-May-2015)

Ref Expression
Hypotheses mapdh75.h H=LHypK
mapdh75.u U=DVecHKW
mapdh75.v V=BaseU
mapdh75.s -˙=-U
mapdh75.o 0˙=0U
mapdh75.n N=LSpanU
mapdh75.c C=LCDualKW
mapdh75.d D=BaseC
mapdh75.r R=-C
mapdh75.q Q=0C
mapdh75.j J=LSpanC
mapdh75.m M=mapdKW
mapdh75.i I=xVif2ndx=0˙QιhD|MN2ndx=JhMN1st1stx-˙2ndx=J2nd1stxRh
mapdh75.k φKHLWH
mapdh75.f φFD
mapdh75.mn φMNX=JF
mapdh75a φIXFY=G
mapdh75d.b φIXFZ=E
mapdh75d.vw φNYNZ
mapdh75d.un φ¬XNYZ
mapdh75d.x φXV0˙
mapdh75d.y φYV0˙
mapdh75d.z φZV0˙
Assertion mapdh75d φIYGZ=E

Proof

Step Hyp Ref Expression
1 mapdh75.h H=LHypK
2 mapdh75.u U=DVecHKW
3 mapdh75.v V=BaseU
4 mapdh75.s -˙=-U
5 mapdh75.o 0˙=0U
6 mapdh75.n N=LSpanU
7 mapdh75.c C=LCDualKW
8 mapdh75.d D=BaseC
9 mapdh75.r R=-C
10 mapdh75.q Q=0C
11 mapdh75.j J=LSpanC
12 mapdh75.m M=mapdKW
13 mapdh75.i I=xVif2ndx=0˙QιhD|MN2ndx=JhMN1st1stx-˙2ndx=J2nd1stxRh
14 mapdh75.k φKHLWH
15 mapdh75.f φFD
16 mapdh75.mn φMNX=JF
17 mapdh75a φIXFY=G
18 mapdh75d.b φIXFZ=E
19 mapdh75d.vw φNYNZ
20 mapdh75d.un φ¬XNYZ
21 mapdh75d.x φXV0˙
22 mapdh75d.y φYV0˙
23 mapdh75d.z φZV0˙
24 10 13 1 12 2 3 4 5 6 7 8 9 11 14 15 16 21 22 23 20 19 17 18 mapdheq4 φIYGZ=E