Metamath Proof Explorer


Theorem mapdh6eN

Description: Lemmma for mapdh6N . Part (6) in Baer p. 47 line 38. (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 mapdh6eN φIXFw+˙Y+˙Z=IXFw+˙Y˙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 3 5 14 dvhlmod φULMod
27 24 eldifad φwV
28 22 eldifad φYV
29 6 18 lmodvacl ULModwVYVw+˙YV
30 26 27 28 29 syl3anc φw+˙YV
31 3 5 14 dvhlvec φULVec
32 17 eldifad φXV
33 6 9 31 27 32 28 25 lspindpi φNwNXNwNY
34 33 simprd φNwNY
35 6 18 8 9 26 27 28 34 lmodindp1 φw+˙Y0˙
36 eldifsn w+˙YV0˙w+˙YVw+˙Y0˙
37 30 35 36 sylanbrc φw+˙YV0˙
38 23 eldifad φZV
39 6 9 31 32 28 38 20 lspindpi φNXNYNXNZ
40 39 simpld φNXNY
41 6 18 8 9 31 17 22 23 24 21 40 25 mapdindp3 φNXNw+˙Y
42 6 18 8 9 31 17 22 23 24 21 40 25 mapdindp4 φ¬ZNXw+˙Y
43 6 8 9 31 17 30 38 41 42 lspindp1 φNZNw+˙Y¬XNZw+˙Y
44 43 simprd φ¬XNZw+˙Y
45 prcom w+˙YZ=Zw+˙Y
46 45 fveq2i Nw+˙YZ=NZw+˙Y
47 46 eleq2i XNw+˙YZXNZw+˙Y
48 44 47 sylnibr φ¬XNw+˙YZ
49 6 9 31 38 32 30 42 lspindpi φNZNXNZNw+˙Y
50 49 simprd φNZNw+˙Y
51 50 necomd φNw+˙YNZ
52 eqidd φIXFw+˙Y=IXFw+˙Y
53 eqidd φIXFZ=IXFZ
54 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 37 23 48 51 52 53 mapdh6aN φIXFw+˙Y+˙Z=IXFw+˙Y˙IXFZ