Metamath Proof Explorer

Theorem hdmap14lem10

Description: Part of proof of part 14 in Baer p. 49 line 38. (Contributed by NM, 3-Jun-2015)

Ref Expression
Hypotheses hdmap14lem8.h 
|- H = ( LHyp ` K )
hdmap14lem8.u 
|- U = ( ( DVecH ` K ) ` W )
hdmap14lem8.v 
|- V = ( Base ` U )
hdmap14lem8.q 
|- .+ = ( +g ` U )
hdmap14lem8.t 
|- .x. = ( .s ` U )
hdmap14lem8.o 
|- .0. = ( 0g ` U )
hdmap14lem8.n 
|- N = ( LSpan ` U )
hdmap14lem8.r 
|- R = ( Scalar ` U )
hdmap14lem8.b 
|- B = ( Base ` R )
hdmap14lem8.c 
|- C = ( ( LCDual ` K ) ` W )
hdmap14lem8.d 
|- .+b = ( +g ` C )
hdmap14lem8.e 
|- .xb = ( .s ` C )
hdmap14lem8.p 
|- P = ( Scalar ` C )
hdmap14lem8.a 
|- A = ( Base ` P )
hdmap14lem8.s 
|- S = ( ( HDMap ` K ) ` W )
hdmap14lem8.k 
|- ( ph -> ( K e. HL /\ W e. H ) )
hdmap14lem8.x 
|- ( ph -> X e. ( V \ { .0. } ) )
hdmap14lem8.y 
|- ( ph -> Y e. ( V \ { .0. } ) )
hdmap14lem8.f 
|- ( ph -> F e. B )
hdmap14lem8.g 
|- ( ph -> G e. A )
hdmap14lem8.i 
|- ( ph -> I e. A )
hdmap14lem8.xx 
|- ( ph -> ( S ` ( F .x. X ) ) = ( G .xb ( S ` X ) ) )
hdmap14lem8.yy 
|- ( ph -> ( S ` ( F .x. Y ) ) = ( I .xb ( S ` Y ) ) )
hdmap14lem8.ne 
|- ( ph -> ( N ` { X } ) =/= ( N ` { Y } ) )
Assertion hdmap14lem10 
|- ( ph -> G = I )

Proof

Step Hyp Ref Expression
1 hdmap14lem8.h 
 |-  H = ( LHyp ` K )
2 hdmap14lem8.u 
 |-  U = ( ( DVecH ` K ) ` W )
3 hdmap14lem8.v 
 |-  V = ( Base ` U )
4 hdmap14lem8.q 
 |-  .+ = ( +g ` U )
5 hdmap14lem8.t 
 |-  .x. = ( .s ` U )
6 hdmap14lem8.o 
 |-  .0. = ( 0g ` U )
7 hdmap14lem8.n 
 |-  N = ( LSpan ` U )
8 hdmap14lem8.r 
 |-  R = ( Scalar ` U )
9 hdmap14lem8.b 
 |-  B = ( Base ` R )
10 hdmap14lem8.c 
 |-  C = ( ( LCDual ` K ) ` W )
11 hdmap14lem8.d 
 |-  .+b = ( +g ` C )
12 hdmap14lem8.e 
 |-  .xb = ( .s ` C )
13 hdmap14lem8.p 
 |-  P = ( Scalar ` C )
14 hdmap14lem8.a 
 |-  A = ( Base ` P )
15 hdmap14lem8.s 
 |-  S = ( ( HDMap ` K ) ` W )
16 hdmap14lem8.k 
 |-  ( ph -> ( K e. HL /\ W e. H ) )
17 hdmap14lem8.x 
 |-  ( ph -> X e. ( V \ { .0. } ) )
18 hdmap14lem8.y 
 |-  ( ph -> Y e. ( V \ { .0. } ) )
19 hdmap14lem8.f 
 |-  ( ph -> F e. B )
20 hdmap14lem8.g 
 |-  ( ph -> G e. A )
21 hdmap14lem8.i 
 |-  ( ph -> I e. A )
22 hdmap14lem8.xx 
 |-  ( ph -> ( S ` ( F .x. X ) ) = ( G .xb ( S ` X ) ) )
23 hdmap14lem8.yy 
 |-  ( ph -> ( S ` ( F .x. Y ) ) = ( I .xb ( S ` Y ) ) )
24 hdmap14lem8.ne 
 |-  ( ph -> ( N ` { X } ) =/= ( N ` { Y } ) )
25 eqid 
 |-  ( LSpan ` C ) = ( LSpan ` C )
26 1 2 16 dvhlmod 
 |-  ( ph -> U e. LMod )
27 17 eldifad 
 |-  ( ph -> X e. V )
28 18 eldifad 
 |-  ( ph -> Y e. V )
29 3 4 lmodvacl 
 |-  ( ( U e. LMod /\ X e. V /\ Y e. V ) -> ( X .+ Y ) e. V )
30 26 27 28 29 syl3anc 
 |-  ( ph -> ( X .+ Y ) e. V )
31 1 2 3 5 8 9 10 12 25 13 14 15 16 30 19 hdmap14lem2a 
 |-  ( ph -> E. g e. A ( S ` ( F .x. ( X .+ Y ) ) ) = ( g .xb ( S ` ( X .+ Y ) ) ) )
32 16 3ad2ant1 
 |-  ( ( ph /\ g e. A /\ ( S ` ( F .x. ( X .+ Y ) ) ) = ( g .xb ( S ` ( X .+ Y ) ) ) ) -> ( K e. HL /\ W e. H ) )
33 17 3ad2ant1 
 |-  ( ( ph /\ g e. A /\ ( S ` ( F .x. ( X .+ Y ) ) ) = ( g .xb ( S ` ( X .+ Y ) ) ) ) -> X e. ( V \ { .0. } ) )
34 18 3ad2ant1 
 |-  ( ( ph /\ g e. A /\ ( S ` ( F .x. ( X .+ Y ) ) ) = ( g .xb ( S ` ( X .+ Y ) ) ) ) -> Y e. ( V \ { .0. } ) )
35 19 3ad2ant1 
 |-  ( ( ph /\ g e. A /\ ( S ` ( F .x. ( X .+ Y ) ) ) = ( g .xb ( S ` ( X .+ Y ) ) ) ) -> F e. B )
36 20 3ad2ant1 
 |-  ( ( ph /\ g e. A /\ ( S ` ( F .x. ( X .+ Y ) ) ) = ( g .xb ( S ` ( X .+ Y ) ) ) ) -> G e. A )
37 21 3ad2ant1 
 |-  ( ( ph /\ g e. A /\ ( S ` ( F .x. ( X .+ Y ) ) ) = ( g .xb ( S ` ( X .+ Y ) ) ) ) -> I e. A )
38 22 3ad2ant1 
 |-  ( ( ph /\ g e. A /\ ( S ` ( F .x. ( X .+ Y ) ) ) = ( g .xb ( S ` ( X .+ Y ) ) ) ) -> ( S ` ( F .x. X ) ) = ( G .xb ( S ` X ) ) )
39 23 3ad2ant1 
 |-  ( ( ph /\ g e. A /\ ( S ` ( F .x. ( X .+ Y ) ) ) = ( g .xb ( S ` ( X .+ Y ) ) ) ) -> ( S ` ( F .x. Y ) ) = ( I .xb ( S ` Y ) ) )
40 24 3ad2ant1 
 |-  ( ( ph /\ g e. A /\ ( S ` ( F .x. ( X .+ Y ) ) ) = ( g .xb ( S ` ( X .+ Y ) ) ) ) -> ( N ` { X } ) =/= ( N ` { Y } ) )
41 simp2 
 |-  ( ( ph /\ g e. A /\ ( S ` ( F .x. ( X .+ Y ) ) ) = ( g .xb ( S ` ( X .+ Y ) ) ) ) -> g e. A )
42 simp3 
 |-  ( ( ph /\ g e. A /\ ( S ` ( F .x. ( X .+ Y ) ) ) = ( g .xb ( S ` ( X .+ Y ) ) ) ) -> ( S ` ( F .x. ( X .+ Y ) ) ) = ( g .xb ( S ` ( X .+ Y ) ) ) )
43 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 32 33 34 35 36 37 38 39 40 41 42 hdmap14lem9 
 |-  ( ( ph /\ g e. A /\ ( S ` ( F .x. ( X .+ Y ) ) ) = ( g .xb ( S ` ( X .+ Y ) ) ) ) -> G = I )
44 43 rexlimdv3a 
 |-  ( ph -> ( E. g e. A ( S ` ( F .x. ( X .+ Y ) ) ) = ( g .xb ( S ` ( X .+ Y ) ) ) -> G = I ) )
45 31 44 mpd 
 |-  ( ph -> G = I )