Mathbox for Norm Megill < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  mapdh8 Unicode version

Theorem mapdh8 30668
 Description: Part (8) in [Baer] p. 48. Given a reference vector , the value of function at a vector is independent of the choice of auxiliary vectors and . Unlike Baer's, our version does not require , , and to be independent, and also is defined for all and that are not colinear with or . We do this to make the definition of Baer's sigma function more straightforward. (This part eliminates .) (Contributed by NM, 13-May-2015.)
Hypotheses
Ref Expression
mapdh8a.h
mapdh8a.u
mapdh8a.v
mapdh8a.s
mapdh8a.o
mapdh8a.n
mapdh8a.c LCDual
mapdh8a.d
mapdh8a.r
mapdh8a.q
mapdh8a.j
mapdh8a.m mapd
mapdh8a.i
mapdh8a.k
mapdh8h.f
mapdh8h.mn
mapdh8i.x
mapdh8i.y
mapdh8i.z
mapdh8i.xy
mapdh8i.xz
mapdh8i.yt
mapdh8i.zt
mapdh8.t
Assertion
Ref Expression
mapdh8
Distinct variable groups:   ,,   ,,   ,   ,,   ,,   ,   ,,   ,,   ,,   ,   ,,   ,   ,,   ,   ,,   ,,   ,,   ,   ,
Allowed substitution hints:   ()   ()   ()   ()   (,)   (,)   ()   (,)

Proof of Theorem mapdh8
StepHypRef Expression
1 mapdh8a.q . . . . . 6
2 mapdh8a.i . . . . . 6
3 mapdh8a.o . . . . . 6
4 mapdh8i.y . . . . . 6
5 fvex 5391 . . . . . . 7
65a1i 12 . . . . . 6
71, 2, 3, 4, 6mapdhval0 30604 . . . . 5
8 mapdh8i.z . . . . . 6
9 fvex 5391 . . . . . . 7
109a1i 12 . . . . . 6
111, 2, 3, 8, 10mapdhval0 30604 . . . . 5
127, 11eqtr4d 2288 . . . 4
14 oteq3 3707 . . . . 5
1514fveq2d 5381 . . . 4
17 oteq3 3707 . . . . 5
1817fveq2d 5381 . . . 4
2013, 16, 193eqtr4d 2295 . 2
21 mapdh8a.h . . 3
22 mapdh8a.u . . 3
23 mapdh8a.v . . 3
24 mapdh8a.s . . 3
25 mapdh8a.n . . 3
26 mapdh8a.c . . 3 LCDual
27 mapdh8a.d . . 3
28 mapdh8a.r . . 3
29 mapdh8a.j . . 3
30 mapdh8a.m . . 3 mapd
31 mapdh8a.k . . . 4
33 mapdh8h.f . . . 4
35 mapdh8h.mn . . . 4
37 mapdh8i.x . . . 4
41 mapdh8i.xy . . . 4
43 mapdh8i.xz . . . 4