Metamath Proof Explorer

Theorem hlhilphllem

Description: Lemma for hlhil . (Contributed by NM, 23-Jun-2015)

Ref Expression
Hypotheses hlhilphl.h 
|- H = ( LHyp ` K )
hlhilphllem.u 
|- U = ( ( HLHil ` K ) ` W )
hlhilphl.k 
|- ( ph -> ( K e. HL /\ W e. H ) )
hlhilphllem.f 
|- F = ( Scalar ` U )
hlhilphllem.l 
|- L = ( ( DVecH ` K ) ` W )
hlhilphllem.v 
|- V = ( Base ` L )
hlhilphllem.a 
|- .+ = ( +g ` L )
hlhilphllem.s 
|- .x. = ( .s ` L )
hlhilphllem.r 
|- R = ( Scalar ` L )
hlhilphllem.b 
|- B = ( Base ` R )
hlhilphllem.p 
|- .+^ = ( +g ` R )
hlhilphllem.t 
|- .X. = ( .r ` R )
hlhilphllem.q 
|- Q = ( 0g ` R )
hlhilphllem.z 
|- .0. = ( 0g ` L )
hlhilphllem.i 
|- ., = ( .i ` U )
hlhilphllem.j 
|- J = ( ( HDMap ` K ) ` W )
hlhilphllem.g 
|- G = ( ( HGMap ` K ) ` W )
hlhilphllem.e 
|- E = ( x e. V , y e. V |-> ( ( J ` y ) ` x ) )
Assertion hlhilphllem 
|- ( ph -> U e. PreHil )

Proof

Step Hyp Ref Expression
1 hlhilphl.h 
 |-  H = ( LHyp ` K )
2 hlhilphllem.u 
 |-  U = ( ( HLHil ` K ) ` W )
3 hlhilphl.k 
 |-  ( ph -> ( K e. HL /\ W e. H ) )
4 hlhilphllem.f 
 |-  F = ( Scalar ` U )
5 hlhilphllem.l 
 |-  L = ( ( DVecH ` K ) ` W )
6 hlhilphllem.v 
 |-  V = ( Base ` L )
7 hlhilphllem.a 
 |-  .+ = ( +g ` L )
8 hlhilphllem.s 
 |-  .x. = ( .s ` L )
9 hlhilphllem.r 
 |-  R = ( Scalar ` L )
10 hlhilphllem.b 
 |-  B = ( Base ` R )
11 hlhilphllem.p 
 |-  .+^ = ( +g ` R )
12 hlhilphllem.t 
 |-  .X. = ( .r ` R )
13 hlhilphllem.q 
 |-  Q = ( 0g ` R )
14 hlhilphllem.z 
 |-  .0. = ( 0g ` L )
15 hlhilphllem.i 
 |-  ., = ( .i ` U )
16 hlhilphllem.j 
 |-  J = ( ( HDMap ` K ) ` W )
17 hlhilphllem.g 
 |-  G = ( ( HGMap ` K ) ` W )
18 hlhilphllem.e 
 |-  E = ( x e. V , y e. V |-> ( ( J ` y ) ` x ) )
19 1 2 3 5 6 hlhilbase 
 |-  ( ph -> V = ( Base ` U ) )
20 1 2 3 5 7 hlhilplus 
 |-  ( ph -> .+ = ( +g ` U ) )
21 1 5 8 2 3 hlhilvsca 
 |-  ( ph -> .x. = ( .s ` U ) )
22 15 a1i 
 |-  ( ph -> ., = ( .i ` U ) )
23 1 5 2 3 14 hlhil0 
 |-  ( ph -> .0. = ( 0g ` U ) )
24 4 a1i 
 |-  ( ph -> F = ( Scalar ` U ) )
25 1 5 9 2 4 3 10 hlhilsbase2 
 |-  ( ph -> B = ( Base ` F ) )
26 1 5 9 2 4 3 11 hlhilsplus2 
 |-  ( ph -> .+^ = ( +g ` F ) )
27 1 5 9 2 4 3 12 hlhilsmul2 
 |-  ( ph -> .X. = ( .r ` F ) )
28 1 2 4 17 3 hlhilnvl 
 |-  ( ph -> G = ( *r ` F ) )
29 1 5 9 2 4 3 13 hlhils0 
 |-  ( ph -> Q = ( 0g ` F ) )
30 1 2 3 hlhillvec 
 |-  ( ph -> U e. LVec )
31 1 2 3 4 hlhilsrng 
 |-  ( ph -> F e. *Ring )
32 3 3ad2ant1 
 |-  ( ( ph /\ a e. V /\ b e. V ) -> ( K e. HL /\ W e. H ) )
33 simp2 
 |-  ( ( ph /\ a e. V /\ b e. V ) -> a e. V )
34 simp3 
 |-  ( ( ph /\ a e. V /\ b e. V ) -> b e. V )
35 1 5 6 16 2 32 15 33 34 hlhilipval 
 |-  ( ( ph /\ a e. V /\ b e. V ) -> ( a ., b ) = ( ( J ` b ) ` a ) )
36 1 5 6 9 10 16 32 33 34 hdmapipcl 
 |-  ( ( ph /\ a e. V /\ b e. V ) -> ( ( J ` b ) ` a ) e. B )
37 35 36 eqeltrd 
 |-  ( ( ph /\ a e. V /\ b e. V ) -> ( a ., b ) e. B )
38 3 3ad2ant1 
 |-  ( ( ph /\ d e. B /\ ( a e. V /\ b e. V /\ c e. V ) ) -> ( K e. HL /\ W e. H ) )
39 simp31 
 |-  ( ( ph /\ d e. B /\ ( a e. V /\ b e. V /\ c e. V ) ) -> a e. V )
40 simp32 
 |-  ( ( ph /\ d e. B /\ ( a e. V /\ b e. V /\ c e. V ) ) -> b e. V )
41 simp33 
 |-  ( ( ph /\ d e. B /\ ( a e. V /\ b e. V /\ c e. V ) ) -> c e. V )
42 simp2 
 |-  ( ( ph /\ d e. B /\ ( a e. V /\ b e. V /\ c e. V ) ) -> d e. B )
43 1 5 6 7 8 9 10 11 12 16 38 39 40 41 42 hdmapln1 
 |-  ( ( ph /\ d e. B /\ ( a e. V /\ b e. V /\ c e. V ) ) -> ( ( J ` c ) ` ( ( d .x. a ) .+ b ) ) = ( ( d .X. ( ( J ` c ) ` a ) ) .+^ ( ( J ` c ) ` b ) ) )
44 1 5 3 dvhlmod 
 |-  ( ph -> L e. LMod )
45 44 3ad2ant1 
 |-  ( ( ph /\ d e. B /\ ( a e. V /\ b e. V /\ c e. V ) ) -> L e. LMod )
46 6 9 8 10 lmodvscl 
 |-  ( ( L e. LMod /\ d e. B /\ a e. V ) -> ( d .x. a ) e. V )
47 45 42 39 46 syl3anc 
 |-  ( ( ph /\ d e. B /\ ( a e. V /\ b e. V /\ c e. V ) ) -> ( d .x. a ) e. V )
48 6 7 lmodvacl 
 |-  ( ( L e. LMod /\ ( d .x. a ) e. V /\ b e. V ) -> ( ( d .x. a ) .+ b ) e. V )
49 45 47 40 48 syl3anc 
 |-  ( ( ph /\ d e. B /\ ( a e. V /\ b e. V /\ c e. V ) ) -> ( ( d .x. a ) .+ b ) e. V )
50 1 5 6 16 2 38 15 49 41 hlhilipval 
 |-  ( ( ph /\ d e. B /\ ( a e. V /\ b e. V /\ c e. V ) ) -> ( ( ( d .x. a ) .+ b ) ., c ) = ( ( J ` c ) ` ( ( d .x. a ) .+ b ) ) )
51 1 5 6 16 2 38 15 39 41 hlhilipval 
 |-  ( ( ph /\ d e. B /\ ( a e. V /\ b e. V /\ c e. V ) ) -> ( a ., c ) = ( ( J ` c ) ` a ) )
52 51 oveq2d 
 |-  ( ( ph /\ d e. B /\ ( a e. V /\ b e. V /\ c e. V ) ) -> ( d .X. ( a ., c ) ) = ( d .X. ( ( J ` c ) ` a ) ) )
53 1 5 6 16 2 38 15 40 41 hlhilipval 
 |-  ( ( ph /\ d e. B /\ ( a e. V /\ b e. V /\ c e. V ) ) -> ( b ., c ) = ( ( J ` c ) ` b ) )
54 52 53 oveq12d 
 |-  ( ( ph /\ d e. B /\ ( a e. V /\ b e. V /\ c e. V ) ) -> ( ( d .X. ( a ., c ) ) .+^ ( b ., c ) ) = ( ( d .X. ( ( J ` c ) ` a ) ) .+^ ( ( J ` c ) ` b ) ) )
55 43 50 54 3eqtr4d 
 |-  ( ( ph /\ d e. B /\ ( a e. V /\ b e. V /\ c e. V ) ) -> ( ( ( d .x. a ) .+ b ) ., c ) = ( ( d .X. ( a ., c ) ) .+^ ( b ., c ) ) )
56 3 adantr 
 |-  ( ( ph /\ a e. V ) -> ( K e. HL /\ W e. H ) )
57 simpr 
 |-  ( ( ph /\ a e. V ) -> a e. V )
58 1 5 6 16 2 56 15 57 57 hlhilipval 
 |-  ( ( ph /\ a e. V ) -> ( a ., a ) = ( ( J ` a ) ` a ) )
59 58 eqeq1d 
 |-  ( ( ph /\ a e. V ) -> ( ( a ., a ) = Q <-> ( ( J ` a ) ` a ) = Q ) )
60 1 5 6 14 9 13 16 56 57 hdmapip0 
 |-  ( ( ph /\ a e. V ) -> ( ( ( J ` a ) ` a ) = Q <-> a = .0. ) )
61 59 60 bitrd 
 |-  ( ( ph /\ a e. V ) -> ( ( a ., a ) = Q <-> a = .0. ) )
62 61 biimp3a 
 |-  ( ( ph /\ a e. V /\ ( a ., a ) = Q ) -> a = .0. )
63 1 5 6 16 17 32 33 34 hdmapg 
 |-  ( ( ph /\ a e. V /\ b e. V ) -> ( G ` ( ( J ` b ) ` a ) ) = ( ( J ` a ) ` b ) )
64 35 fveq2d 
 |-  ( ( ph /\ a e. V /\ b e. V ) -> ( G ` ( a ., b ) ) = ( G ` ( ( J ` b ) ` a ) ) )
65 1 5 6 16 2 32 15 34 33 hlhilipval 
 |-  ( ( ph /\ a e. V /\ b e. V ) -> ( b ., a ) = ( ( J ` a ) ` b ) )
66 63 64 65 3eqtr4d 
 |-  ( ( ph /\ a e. V /\ b e. V ) -> ( G ` ( a ., b ) ) = ( b ., a ) )
67 19 20 21 22 23 24 25 26 27 28 29 30 31 37 55 62 66 isphld 
 |-  ( ph -> U e. PreHil )