Theorem hdmapinvlem2

Description: Line 28 in Baer p. 110, 0 = f(w,u). (Contributed by NM, 11-Jun-2015)

	Ref	Expression
Hypotheses	hdmapinvlem1.h	|- H = ( LHyp ` K )
	hdmapinvlem1.e	|- E = <. ( _I |` ( Base ` K ) ) , ( _I |` ( ( LTrn ` K ) ` W ) ) >.
	hdmapinvlem1.o	|- O = ( ( ocH ` K ) ` W )
	hdmapinvlem1.u	|- U = ( ( DVecH ` K ) ` W )
	hdmapinvlem1.v	|- V = ( Base ` U )
	hdmapinvlem1.r	|- R = ( Scalar ` U )
	hdmapinvlem1.b	|- B = ( Base ` R )
	hdmapinvlem1.t	|- .x. = ( .r ` R )
	hdmapinvlem1.z	|- .0. = ( 0g ` R )
	hdmapinvlem1.s	|- S = ( ( HDMap ` K ) ` W )
	hdmapinvlem1.k	|- ( ph -> ( K e. HL /\ W e. H ) )
	hdmapinvlem1.c	|- ( ph -> C e. ( O ` { E } ) )
Assertion	hdmapinvlem2	|- ( ph -> ( ( S ` C ) ` E ) = .0. )

Proof

Step	Hyp	Ref	Expression
1		hdmapinvlem1.h	|- H = ( LHyp ` K )
2		hdmapinvlem1.e	|- E = <. ( _I |` ( Base ` K ) ) , ( _I |` ( ( LTrn ` K ) ` W ) ) >.
3		hdmapinvlem1.o	|- O = ( ( ocH ` K ) ` W )
4		hdmapinvlem1.u	|- U = ( ( DVecH ` K ) ` W )
5		hdmapinvlem1.v	|- V = ( Base ` U )
6		hdmapinvlem1.r	|- R = ( Scalar ` U )
7		hdmapinvlem1.b	|- B = ( Base ` R )
8		hdmapinvlem1.t	|- .x. = ( .r ` R )
9		hdmapinvlem1.z	|- .0. = ( 0g ` R )
10		hdmapinvlem1.s	|- S = ( ( HDMap ` K ) ` W )
11		hdmapinvlem1.k	|- ( ph -> ( K e. HL /\ W e. H ) )
12		hdmapinvlem1.c	|- ( ph -> C e. ( O ` { E } ) )
13	1 2 3 4 5 6 7 8 9 10 11 12	hdmapinvlem1	|- ( ph -> ( ( S ` E ) ` C ) = .0. )
14		eqid	|- ( Base ` K ) = ( Base ` K )
15		eqid	|- ( ( LTrn ` K ) ` W ) = ( ( LTrn ` K ) ` W )
16		eqid	|- ( 0g ` U ) = ( 0g ` U )
17	1 14 15 4 5 16 2 11	dvheveccl	|- ( ph -> E e. ( V \ { ( 0g ` U ) } ) )
18	17	eldifad	|- ( ph -> E e. V )
19	18	snssd	|- ( ph -> { E } C_ V )
20	1 4 5 3	dochssv	|- ( ( ( K e. HL /\ W e. H ) /\ { E } C_ V ) -> ( O ` { E } ) C_ V )
21	11 19 20	syl2anc	|- ( ph -> ( O ` { E } ) C_ V )
22	21 12	sseldd	|- ( ph -> C e. V )
23	1 4 5 6 9 10 11 18 22	hdmapip0com	|- ( ph -> ( ( ( S ` E ) ` C ) = .0. <-> ( ( S ` C ) ` E ) = .0. ) )
24	13 23	mpbid	|- ( ph -> ( ( S ` C ) ` E ) = .0. )