Metamath Proof Explorer

Theorem hlhilhillem

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 ) )
hlhilphllem.o 
|- O = ( ocv ` U )
hlhilphllem.c 
|- C = ( ClSubSp ` U )
Assertion hlhilhillem 
|- ( ph -> U e. Hil )

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 hlhilphllem.o 
 |-  O = ( ocv ` U )
20 hlhilphllem.c 
 |-  C = ( ClSubSp ` U )
21 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 hlhilphllem 
 |-  ( ph -> U e. PreHil )
22 3 adantr 
 |-  ( ( ph /\ x e. C ) -> ( K e. HL /\ W e. H ) )
23 eqid 
 |-  ( ( ocH ` K ) ` W ) = ( ( ocH ` K ) ` W )
24 eqid 
 |-  ( ( DIsoH ` K ) ` W ) = ( ( DIsoH ` K ) ` W )
25 1 24 2 20 3 hlhillcs 
 |-  ( ph -> C = ran ( ( DIsoH ` K ) ` W ) )
26 25 eleq2d 
 |-  ( ph -> ( x e. C <-> x e. ran ( ( DIsoH ` K ) ` W ) ) )
27 26 biimpa 
 |-  ( ( ph /\ x e. C ) -> x e. ran ( ( DIsoH ` K ) ` W ) )
28 1 5 24 6 dihrnss 
 |-  ( ( ( K e. HL /\ W e. H ) /\ x e. ran ( ( DIsoH ` K ) ` W ) ) -> x C_ V )
29 3 28 sylan 
 |-  ( ( ph /\ x e. ran ( ( DIsoH ` K ) ` W ) ) -> x C_ V )
30 27 29 syldan 
 |-  ( ( ph /\ x e. C ) -> x C_ V )
31 1 5 2 22 6 23 19 30 hlhilocv 
 |-  ( ( ph /\ x e. C ) -> ( O ` x ) = ( ( ( ocH ` K ) ` W ) ` x ) )
32 31 oveq2d 
 |-  ( ( ph /\ x e. C ) -> ( x ( LSSum ` L ) ( O ` x ) ) = ( x ( LSSum ` L ) ( ( ( ocH ` K ) ` W ) ` x ) ) )
33 eqid 
 |-  ( LSSum ` L ) = ( LSSum ` L )
34 1 5 2 3 33 hlhillsm 
 |-  ( ph -> ( LSSum ` L ) = ( LSSum ` U ) )
35 34 adantr 
 |-  ( ( ph /\ x e. C ) -> ( LSSum ` L ) = ( LSSum ` U ) )
36 35 oveqd 
 |-  ( ( ph /\ x e. C ) -> ( x ( LSSum ` L ) ( O ` x ) ) = ( x ( LSSum ` U ) ( O ` x ) ) )
37 eqid 
 |-  ( LSubSp ` L ) = ( LSubSp ` L )
38 3 adantr 
 |-  ( ( ph /\ x e. ran ( ( DIsoH ` K ) ` W ) ) -> ( K e. HL /\ W e. H ) )
39 1 5 24 37 dihrnlss 
 |-  ( ( ( K e. HL /\ W e. H ) /\ x e. ran ( ( DIsoH ` K ) ` W ) ) -> x e. ( LSubSp ` L ) )
40 3 39 sylan 
 |-  ( ( ph /\ x e. ran ( ( DIsoH ` K ) ` W ) ) -> x e. ( LSubSp ` L ) )
41 1 24 5 6 23 38 29 dochoccl 
 |-  ( ( ph /\ x e. ran ( ( DIsoH ` K ) ` W ) ) -> ( x e. ran ( ( DIsoH ` K ) ` W ) <-> ( ( ( ocH ` K ) ` W ) ` ( ( ( ocH ` K ) ` W ) ` x ) ) = x ) )
42 41 biimpd 
 |-  ( ( ph /\ x e. ran ( ( DIsoH ` K ) ` W ) ) -> ( x e. ran ( ( DIsoH ` K ) ` W ) -> ( ( ( ocH ` K ) ` W ) ` ( ( ( ocH ` K ) ` W ) ` x ) ) = x ) )
43 42 ex 
 |-  ( ph -> ( x e. ran ( ( DIsoH ` K ) ` W ) -> ( x e. ran ( ( DIsoH ` K ) ` W ) -> ( ( ( ocH ` K ) ` W ) ` ( ( ( ocH ` K ) ` W ) ` x ) ) = x ) ) )
44 43 pm2.43d 
 |-  ( ph -> ( x e. ran ( ( DIsoH ` K ) ` W ) -> ( ( ( ocH ` K ) ` W ) ` ( ( ( ocH ` K ) ` W ) ` x ) ) = x ) )
45 44 imp 
 |-  ( ( ph /\ x e. ran ( ( DIsoH ` K ) ` W ) ) -> ( ( ( ocH ` K ) ` W ) ` ( ( ( ocH ` K ) ` W ) ` x ) ) = x )
46 1 23 5 6 37 33 38 40 45 dochexmid 
 |-  ( ( ph /\ x e. ran ( ( DIsoH ` K ) ` W ) ) -> ( x ( LSSum ` L ) ( ( ( ocH ` K ) ` W ) ` x ) ) = V )
47 27 46 syldan 
 |-  ( ( ph /\ x e. C ) -> ( x ( LSSum ` L ) ( ( ( ocH ` K ) ` W ) ` x ) ) = V )
48 32 36 47 3eqtr3d 
 |-  ( ( ph /\ x e. C ) -> ( x ( LSSum ` U ) ( O ` x ) ) = V )
49 1 2 3 5 6 hlhilbase 
 |-  ( ph -> V = ( Base ` U ) )
50 49 adantr 
 |-  ( ( ph /\ x e. C ) -> V = ( Base ` U ) )
51 48 50 eqtrd 
 |-  ( ( ph /\ x e. C ) -> ( x ( LSSum ` U ) ( O ` x ) ) = ( Base ` U ) )
52 51 ralrimiva 
 |-  ( ph -> A. x e. C ( x ( LSSum ` U ) ( O ` x ) ) = ( Base ` U ) )
53 eqid 
 |-  ( Base ` U ) = ( Base ` U )
54 eqid 
 |-  ( LSSum ` U ) = ( LSSum ` U )
55 53 54 19 20 ishil2 
 |-  ( U e. Hil <-> ( U e. PreHil /\ A. x e. C ( x ( LSSum ` U ) ( O ` x ) ) = ( Base ` U ) ) )
56 21 52 55 sylanbrc 
 |-  ( ph -> U e. Hil )