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

Theorem dvhopN 31851
 Description: Decompose a vector expressed as an ordered pair into the sum of two components, the first from the translation group vector base of and the other from the one-dimensional vector subspace . Part of Lemma M of [Crawley] p. 121, line 18. We represent their e, sigma, f by , , . We swapped the order of vector sum (their juxtaposition i.e. composition) to show first. Note that and are the zero and one of the division ring , and is the zero of the translation group. is the scalar product. (Contributed by NM, 21-Nov-2013.) (New usage is discouraged.)
Hypotheses
Ref Expression
dvhop.b
dvhop.h
dvhop.t
dvhop.e
dvhop.p
dvhop.a
dvhop.s
dvhop.o
Assertion
Ref Expression
dvhopN
Distinct variable groups:   ,   ,,,,,   ,   ,   ,,   ,,,,,,   ,,,
Allowed substitution hints:   (,,,,,)   (,,,,)   (,,,)   (,,,,,)   (,,,,,)   ()   (,,,,,)   (,,,,)   (,,,,)   (,,,,,)   (,,)

Proof of Theorem dvhopN
StepHypRef Expression
1 simprr 734 . . . . 5
2 dvhop.b . . . . . . 7
3 dvhop.h . . . . . . 7
4 dvhop.t . . . . . . 7
52, 3, 4idltrn 30884 . . . . . 6
65adantr 452 . . . . 5
7 dvhop.e . . . . . . 7
83, 4, 7tendoidcl 31503 . . . . . 6
98adantr 452 . . . . 5
10 dvhop.s . . . . . 6
1110dvhopspN 31850 . . . . 5
121, 6, 9, 11syl12anc 1182 . . . 4
132, 3, 7tendoid 31507 . . . . . 6
1413adantrl 697 . . . . 5
153, 4, 7tendo1mulr 31505 . . . . . 6
1615adantrl 697 . . . . 5
1714, 16opeq12d 3984 . . . 4
1812, 17eqtrd 2467 . . 3
1918oveq2d 6089 . 2
20 simprl 733 . . 3
21 dvhop.o . . . . 5
222, 3, 4, 7, 21tendo0cl 31524 . . . 4
24 dvhop.a . . . 4