Metamath Proof Explorer

Theorem hdmap14lem11

Description: Part of proof of part 14 in Baer p. 50 line 3. (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 ) ) )
Assertion hdmap14lem11 
|- ( 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 17 eldifad 
 |-  ( ph -> X e. V )
25 18 eldifad 
 |-  ( ph -> Y e. V )
26 1 2 3 7 16 24 25 dvh3dim 
 |-  ( ph -> E. z e. V -. z e. ( N ` { X , Y } ) )
27 eqid 
 |-  ( LSpan ` C ) = ( LSpan ` C )
28 16 3ad2ant1 
 |-  ( ( ph /\ z e. V /\ -. z e. ( N ` { X , Y } ) ) -> ( K e. HL /\ W e. H ) )
29 simp2 
 |-  ( ( ph /\ z e. V /\ -. z e. ( N ` { X , Y } ) ) -> z e. V )
30 19 3ad2ant1 
 |-  ( ( ph /\ z e. V /\ -. z e. ( N ` { X , Y } ) ) -> F e. B )
31 1 2 3 5 8 9 10 12 27 13 14 15 28 29 30 hdmap14lem2a 
 |-  ( ( ph /\ z e. V /\ -. z e. ( N ` { X , Y } ) ) -> E. g e. A ( S ` ( F .x. z ) ) = ( g .xb ( S ` z ) ) )
32 simp11 
 |-  ( ( ( ph /\ z e. V /\ -. z e. ( N ` { X , Y } ) ) /\ g e. A /\ ( S ` ( F .x. z ) ) = ( g .xb ( S ` z ) ) ) -> ph )
33 32 16 syl 
 |-  ( ( ( ph /\ z e. V /\ -. z e. ( N ` { X , Y } ) ) /\ g e. A /\ ( S ` ( F .x. z ) ) = ( g .xb ( S ` z ) ) ) -> ( K e. HL /\ W e. H ) )
34 eqid 
 |-  ( LSubSp ` U ) = ( LSubSp ` U )
35 1 2 16 dvhlmod 
 |-  ( ph -> U e. LMod )
36 32 35 syl 
 |-  ( ( ( ph /\ z e. V /\ -. z e. ( N ` { X , Y } ) ) /\ g e. A /\ ( S ` ( F .x. z ) ) = ( g .xb ( S ` z ) ) ) -> U e. LMod )
37 3 34 7 35 24 25 lspprcl 
 |-  ( ph -> ( N ` { X , Y } ) e. ( LSubSp ` U ) )
38 32 37 syl 
 |-  ( ( ( ph /\ z e. V /\ -. z e. ( N ` { X , Y } ) ) /\ g e. A /\ ( S ` ( F .x. z ) ) = ( g .xb ( S ` z ) ) ) -> ( N ` { X , Y } ) e. ( LSubSp ` U ) )
39 simp12 
 |-  ( ( ( ph /\ z e. V /\ -. z e. ( N ` { X , Y } ) ) /\ g e. A /\ ( S ` ( F .x. z ) ) = ( g .xb ( S ` z ) ) ) -> z e. V )
40 simp13 
 |-  ( ( ( ph /\ z e. V /\ -. z e. ( N ` { X , Y } ) ) /\ g e. A /\ ( S ` ( F .x. z ) ) = ( g .xb ( S ` z ) ) ) -> -. z e. ( N ` { X , Y } ) )
41 6 34 36 38 39 40 lssneln0 
 |-  ( ( ( ph /\ z e. V /\ -. z e. ( N ` { X , Y } ) ) /\ g e. A /\ ( S ` ( F .x. z ) ) = ( g .xb ( S ` z ) ) ) -> z e. ( V \ { .0. } ) )
42 32 17 syl 
 |-  ( ( ( ph /\ z e. V /\ -. z e. ( N ` { X , Y } ) ) /\ g e. A /\ ( S ` ( F .x. z ) ) = ( g .xb ( S ` z ) ) ) -> X e. ( V \ { .0. } ) )
43 32 19 syl 
 |-  ( ( ( ph /\ z e. V /\ -. z e. ( N ` { X , Y } ) ) /\ g e. A /\ ( S ` ( F .x. z ) ) = ( g .xb ( S ` z ) ) ) -> F e. B )
44 simp2 
 |-  ( ( ( ph /\ z e. V /\ -. z e. ( N ` { X , Y } ) ) /\ g e. A /\ ( S ` ( F .x. z ) ) = ( g .xb ( S ` z ) ) ) -> g e. A )
45 32 20 syl 
 |-  ( ( ( ph /\ z e. V /\ -. z e. ( N ` { X , Y } ) ) /\ g e. A /\ ( S ` ( F .x. z ) ) = ( g .xb ( S ` z ) ) ) -> G e. A )
46 simp3 
 |-  ( ( ( ph /\ z e. V /\ -. z e. ( N ` { X , Y } ) ) /\ g e. A /\ ( S ` ( F .x. z ) ) = ( g .xb ( S ` z ) ) ) -> ( S ` ( F .x. z ) ) = ( g .xb ( S ` z ) ) )
47 32 22 syl 
 |-  ( ( ( ph /\ z e. V /\ -. z e. ( N ` { X , Y } ) ) /\ g e. A /\ ( S ` ( F .x. z ) ) = ( g .xb ( S ` z ) ) ) -> ( S ` ( F .x. X ) ) = ( G .xb ( S ` X ) ) )
48 1 2 16 dvhlvec 
 |-  ( ph -> U e. LVec )
49 32 48 syl 
 |-  ( ( ( ph /\ z e. V /\ -. z e. ( N ` { X , Y } ) ) /\ g e. A /\ ( S ` ( F .x. z ) ) = ( g .xb ( S ` z ) ) ) -> U e. LVec )
50 32 24 syl 
 |-  ( ( ( ph /\ z e. V /\ -. z e. ( N ` { X , Y } ) ) /\ g e. A /\ ( S ` ( F .x. z ) ) = ( g .xb ( S ` z ) ) ) -> X e. V )
51 32 25 syl 
 |-  ( ( ( ph /\ z e. V /\ -. z e. ( N ` { X , Y } ) ) /\ g e. A /\ ( S ` ( F .x. z ) ) = ( g .xb ( S ` z ) ) ) -> Y e. V )
52 3 7 49 39 50 51 40 lspindpi 
 |-  ( ( ( ph /\ z e. V /\ -. z e. ( N ` { X , Y } ) ) /\ g e. A /\ ( S ` ( F .x. z ) ) = ( g .xb ( S ` z ) ) ) -> ( ( N ` { z } ) =/= ( N ` { X } ) /\ ( N ` { z } ) =/= ( N ` { Y } ) ) )
53 52 simpld 
 |-  ( ( ( ph /\ z e. V /\ -. z e. ( N ` { X , Y } ) ) /\ g e. A /\ ( S ` ( F .x. z ) ) = ( g .xb ( S ` z ) ) ) -> ( N ` { z } ) =/= ( N ` { X } ) )
54 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 33 41 42 43 44 45 46 47 53 hdmap14lem10 
 |-  ( ( ( ph /\ z e. V /\ -. z e. ( N ` { X , Y } ) ) /\ g e. A /\ ( S ` ( F .x. z ) ) = ( g .xb ( S ` z ) ) ) -> g = G )
55 32 18 syl 
 |-  ( ( ( ph /\ z e. V /\ -. z e. ( N ` { X , Y } ) ) /\ g e. A /\ ( S ` ( F .x. z ) ) = ( g .xb ( S ` z ) ) ) -> Y e. ( V \ { .0. } ) )
56 32 21 syl 
 |-  ( ( ( ph /\ z e. V /\ -. z e. ( N ` { X , Y } ) ) /\ g e. A /\ ( S ` ( F .x. z ) ) = ( g .xb ( S ` z ) ) ) -> I e. A )
57 32 23 syl 
 |-  ( ( ( ph /\ z e. V /\ -. z e. ( N ` { X , Y } ) ) /\ g e. A /\ ( S ` ( F .x. z ) ) = ( g .xb ( S ` z ) ) ) -> ( S ` ( F .x. Y ) ) = ( I .xb ( S ` Y ) ) )
58 52 simprd 
 |-  ( ( ( ph /\ z e. V /\ -. z e. ( N ` { X , Y } ) ) /\ g e. A /\ ( S ` ( F .x. z ) ) = ( g .xb ( S ` z ) ) ) -> ( N ` { z } ) =/= ( N ` { Y } ) )
59 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 33 41 55 43 44 56 46 57 58 hdmap14lem10 
 |-  ( ( ( ph /\ z e. V /\ -. z e. ( N ` { X , Y } ) ) /\ g e. A /\ ( S ` ( F .x. z ) ) = ( g .xb ( S ` z ) ) ) -> g = I )
60 54 59 eqtr3d 
 |-  ( ( ( ph /\ z e. V /\ -. z e. ( N ` { X , Y } ) ) /\ g e. A /\ ( S ` ( F .x. z ) ) = ( g .xb ( S ` z ) ) ) -> G = I )
61 60 rexlimdv3a 
 |-  ( ( ph /\ z e. V /\ -. z e. ( N ` { X , Y } ) ) -> ( E. g e. A ( S ` ( F .x. z ) ) = ( g .xb ( S ` z ) ) -> G = I ) )
62 31 61 mpd 
 |-  ( ( ph /\ z e. V /\ -. z e. ( N ` { X , Y } ) ) -> G = I )
63 62 rexlimdv3a 
 |-  ( ph -> ( E. z e. V -. z e. ( N ` { X , Y } ) -> G = I ) )
64 26 63 mpd 
 |-  ( ph -> G = I )