Theorem baerlem5a

Description: An equality that holds when X , Y , Z are independent (non-colinear) vectors. First equation of part (5) in Baer p. 46. (Contributed by NM, 10-Apr-2015)

	Ref	Expression
Hypotheses	baerlem3.v	|- V = ( Base ` W )
	baerlem3.m	|- .- = ( -g ` W )
	baerlem3.o	|- .0. = ( 0g ` W )
	baerlem3.s	|- .(+) = ( LSSum ` W )
	baerlem3.n	|- N = ( LSpan ` W )
	baerlem3.w	|- ( ph -> W e. LVec )
	baerlem3.x	|- ( ph -> X e. V )
	baerlem3.c	|- ( ph -> -. X e. ( N ` { Y , Z } ) )
	baerlem3.d	|- ( ph -> ( N ` { Y } ) =/= ( N ` { Z } ) )
	baerlem3.y	|- ( ph -> Y e. ( V \ { .0. } ) )
	baerlem3.z	|- ( ph -> Z e. ( V \ { .0. } ) )
	baerlem5a.p	|- .+ = ( +g ` W )
Assertion	baerlem5a	|- ( ph -> ( N ` { ( X .- ( Y .+ Z ) ) } ) = ( ( ( N ` { ( X .- Y ) } ) .(+) ( N ` { Z } ) ) i^i ( ( N ` { ( X .- Z ) } ) .(+) ( N ` { Y } ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		baerlem3.v	|- V = ( Base ` W )
2		baerlem3.m	|- .- = ( -g ` W )
3		baerlem3.o	|- .0. = ( 0g ` W )
4		baerlem3.s	|- .(+) = ( LSSum ` W )
5		baerlem3.n	|- N = ( LSpan ` W )
6		baerlem3.w	|- ( ph -> W e. LVec )
7		baerlem3.x	|- ( ph -> X e. V )
8		baerlem3.c	|- ( ph -> -. X e. ( N ` { Y , Z } ) )
9		baerlem3.d	|- ( ph -> ( N ` { Y } ) =/= ( N ` { Z } ) )
10		baerlem3.y	|- ( ph -> Y e. ( V \ { .0. } ) )
11		baerlem3.z	|- ( ph -> Z e. ( V \ { .0. } ) )
12		baerlem5a.p	|- .+ = ( +g ` W )
13		eqid	|- ( .s ` W ) = ( .s ` W )
14		eqid	|- ( Scalar ` W ) = ( Scalar ` W )
15		eqid	|- ( Base ` ( Scalar ` W ) ) = ( Base ` ( Scalar ` W ) )
16		eqid	|- ( +g ` ( Scalar ` W ) ) = ( +g ` ( Scalar ` W ) )
17		eqid	|- ( -g ` ( Scalar ` W ) ) = ( -g ` ( Scalar ` W ) )
18		eqid	|- ( 0g ` ( Scalar ` W ) ) = ( 0g ` ( Scalar ` W ) )
19		eqid	|- ( invg ` ( Scalar ` W ) ) = ( invg ` ( Scalar ` W ) )
20	1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19	baerlem5alem2	|- ( ph -> ( N ` { ( X .- ( Y .+ Z ) ) } ) = ( ( ( N ` { ( X .- Y ) } ) .(+) ( N ` { Z } ) ) i^i ( ( N ` { ( X .- Z ) } ) .(+) ( N ` { Y } ) ) ) )