Theorem normlem4

Description: Lemma used to derive properties of norm. Part of Theorem 3.3(ii) of Beran p. 97. (Contributed by NM, 29-Jul-1999) (New usage is discouraged.)

	Ref	Expression
Hypotheses	normlem1.1	|- S e. CC
	normlem1.2	|- F e. ~H
	normlem1.3	|- G e. ~H
	normlem2.4	|- B = -u ( ( ( * ` S ) x. ( F .ih G ) ) + ( S x. ( G .ih F ) ) )
	normlem3.5	|- A = ( G .ih G )
	normlem3.6	|- C = ( F .ih F )
	normlem4.7	|- R e. RR
	normlem4.8	|- ( abs ` S ) = 1
Assertion	normlem4	|- ( ( F -h ( ( S x. R ) .h G ) ) .ih ( F -h ( ( S x. R ) .h G ) ) ) = ( ( ( A x. ( R ^ 2 ) ) + ( B x. R ) ) + C )

Proof

Step	Hyp	Ref	Expression
1		normlem1.1	|- S e. CC
2		normlem1.2	|- F e. ~H
3		normlem1.3	|- G e. ~H
4		normlem2.4	|- B = -u ( ( ( * ` S ) x. ( F .ih G ) ) + ( S x. ( G .ih F ) ) )
5		normlem3.5	|- A = ( G .ih G )
6		normlem3.6	|- C = ( F .ih F )
7		normlem4.7	|- R e. RR
8		normlem4.8	|- ( abs ` S ) = 1
9	1 2 3 7 8	normlem1	|- ( ( F -h ( ( S x. R ) .h G ) ) .ih ( F -h ( ( S x. R ) .h G ) ) ) = ( ( ( F .ih F ) + ( ( ( * ` S ) x. -u R ) x. ( F .ih G ) ) ) + ( ( ( S x. -u R ) x. ( G .ih F ) ) + ( ( R ^ 2 ) x. ( G .ih G ) ) ) )
10	1 2 3 4 5 6 7	normlem3	|- ( ( ( A x. ( R ^ 2 ) ) + ( B x. R ) ) + C ) = ( ( ( F .ih F ) + ( ( ( * ` S ) x. -u R ) x. ( F .ih G ) ) ) + ( ( ( S x. -u R ) x. ( G .ih F ) ) + ( ( R ^ 2 ) x. ( G .ih G ) ) ) )
11	9 10	eqtr4i	|- ( ( F -h ( ( S x. R ) .h G ) ) .ih ( F -h ( ( S x. R ) .h G ) ) ) = ( ( ( A x. ( R ^ 2 ) ) + ( B x. R ) ) + C )