Metamath Proof Explorer


Theorem mapdh6gN

Description: Lemmma for mapdh6N . Part (6) of Baer p. 47 line 39. (Contributed by NM, 1-May-2015) (New usage is discouraged.)

Ref Expression
Hypotheses mapdh.q Q=0C
mapdh.i I=xVif2ndx=0˙QιhD|MN2ndx=JhMN1st1stx-˙2ndx=J2nd1stxRh
mapdh.h H=LHypK
mapdh.m M=mapdKW
mapdh.u U=DVecHKW
mapdh.v V=BaseU
mapdh.s -˙=-U
mapdhc.o 0˙=0U
mapdh.n N=LSpanU
mapdh.c C=LCDualKW
mapdh.d D=BaseC
mapdh.r R=-C
mapdh.j J=LSpanC
mapdh.k φKHLWH
mapdhc.f φFD
mapdh.mn φMNX=JF
mapdhcl.x φXV0˙
mapdh.p +˙=+U
mapdh.a ˙=+C
mapdh6d.xn φ¬XNYZ
mapdh6d.yz φNY=NZ
mapdh6d.y φYV0˙
mapdh6d.z φZV0˙
mapdh6d.w φwV0˙
mapdh6d.wn φ¬wNXY
Assertion mapdh6gN φIXFw˙IXFY+˙Z=IXFw˙IXFY˙IXFZ

Proof

Step Hyp Ref Expression
1 mapdh.q Q=0C
2 mapdh.i I=xVif2ndx=0˙QιhD|MN2ndx=JhMN1st1stx-˙2ndx=J2nd1stxRh
3 mapdh.h H=LHypK
4 mapdh.m M=mapdKW
5 mapdh.u U=DVecHKW
6 mapdh.v V=BaseU
7 mapdh.s -˙=-U
8 mapdhc.o 0˙=0U
9 mapdh.n N=LSpanU
10 mapdh.c C=LCDualKW
11 mapdh.d D=BaseC
12 mapdh.r R=-C
13 mapdh.j J=LSpanC
14 mapdh.k φKHLWH
15 mapdhc.f φFD
16 mapdh.mn φMNX=JF
17 mapdhcl.x φXV0˙
18 mapdh.p +˙=+U
19 mapdh.a ˙=+C
20 mapdh6d.xn φ¬XNYZ
21 mapdh6d.yz φNY=NZ
22 mapdh6d.y φYV0˙
23 mapdh6d.z φZV0˙
24 mapdh6d.w φwV0˙
25 mapdh6d.wn φ¬wNXY
26 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 mapdh6dN φIXFw+˙Y+˙Z=IXFw˙IXFY+˙Z
27 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 mapdh6eN φIXFw+˙Y+˙Z=IXFw+˙Y˙IXFZ
28 3 5 14 dvhlmod φULMod
29 24 eldifad φwV
30 22 eldifad φYV
31 23 eldifad φZV
32 6 18 lmodass ULModwVYVZVw+˙Y+˙Z=w+˙Y+˙Z
33 28 29 30 31 32 syl13anc φw+˙Y+˙Z=w+˙Y+˙Z
34 33 oteq3d φXFw+˙Y+˙Z=XFw+˙Y+˙Z
35 34 fveq2d φIXFw+˙Y+˙Z=IXFw+˙Y+˙Z
36 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 mapdh6fN φIXFw+˙Y=IXFw˙IXFY
37 36 oveq1d φIXFw+˙Y˙IXFZ=IXFw˙IXFY˙IXFZ
38 27 35 37 3eqtr3d φIXFw+˙Y+˙Z=IXFw˙IXFY˙IXFZ
39 26 38 eqtr3d φIXFw˙IXFY+˙Z=IXFw˙IXFY˙IXFZ