Metamath Proof Explorer


Theorem mapdh6N

Description: Part (6) of Baer p. 47 line 6. Note that we use -. X e. ( N{ Y , Z } ) which is equivalent to Baer's "Fx i^i (Fy + Fz)" by lspdisjb . TODO: If disjoint variable conditions with I and ph become a problem later, use cbv* theorems on I variables here to get rid of them. Maybe reorder hypotheses in lemmas to the more consistent order of this theorem, so they can be shared with this theorem. TODO: may be deleted (with its lemmas), if not needed, in view of hdmap1l6 . (Contributed by NM, 1-May-2015) (New usage is discouraged.)

Ref Expression
Hypotheses mapdh6.h H=LHypK
mapdh6.u U=DVecHKW
mapdh6.v V=BaseU
mapdh6.p +˙=+U
mapdh6.s -˙=-U
mapdh6.o 0˙=0U
mapdh6.n N=LSpanU
mapdh6.c C=LCDualKW
mapdh6.d D=BaseC
mapdh6.a ˙=+C
mapdh6.r R=-C
mapdh6.q Q=0C
mapdh6.j J=LSpanC
mapdh6.m M=mapdKW
mapdh6.i I=xVif2ndx=0˙QιhD|MN2ndx=JhMN1st1stx-˙2ndx=J2nd1stxRh
mapdh6.k φKHLWH
mapdh6.f φFD
mapdh6.x φXV0˙
mapdh6.y φYV
mapdh6.z φZV
mapdh6.xn φ¬XNYZ
mapdh6.mn φMNX=JF
Assertion mapdh6N φIXFY+˙Z=IXFY˙IXFZ

Proof

Step Hyp Ref Expression
1 mapdh6.h H=LHypK
2 mapdh6.u U=DVecHKW
3 mapdh6.v V=BaseU
4 mapdh6.p +˙=+U
5 mapdh6.s -˙=-U
6 mapdh6.o 0˙=0U
7 mapdh6.n N=LSpanU
8 mapdh6.c C=LCDualKW
9 mapdh6.d D=BaseC
10 mapdh6.a ˙=+C
11 mapdh6.r R=-C
12 mapdh6.q Q=0C
13 mapdh6.j J=LSpanC
14 mapdh6.m M=mapdKW
15 mapdh6.i I=xVif2ndx=0˙QιhD|MN2ndx=JhMN1st1stx-˙2ndx=J2nd1stxRh
16 mapdh6.k φKHLWH
17 mapdh6.f φFD
18 mapdh6.x φXV0˙
19 mapdh6.y φYV
20 mapdh6.z φZV
21 mapdh6.xn φ¬XNYZ
22 mapdh6.mn φMNX=JF
23 12 15 1 14 2 3 5 6 7 8 9 11 13 16 17 22 18 4 10 19 20 21 mapdh6kN φIXFY+˙Z=IXFY˙IXFZ