Metamath Proof Explorer

Theorem dihwN

Description: Value of isomorphism H at the fiducial hyperplane W . (Contributed by NM, 25-Aug-2014) (New usage is discouraged.)

Ref Expression
Hypotheses dihw.b 
|- B = ( Base ` K )
dihw.h 
|- H = ( LHyp ` K )
dihw.t 
|- T = ( ( LTrn ` K ) ` W )
dihw.o 
|- .0. = ( f e. T |-> ( _I |` B ) )
dihw.i 
|- I = ( ( DIsoH ` K ) ` W )
dihw.k 
|- ( ph -> ( K e. HL /\ W e. H ) )
Assertion dihwN 
|- ( ph -> ( I ` W ) = ( T X. { .0. } ) )

Proof

Step Hyp Ref Expression
1 dihw.b 
 |-  B = ( Base ` K )
2 dihw.h 
 |-  H = ( LHyp ` K )
3 dihw.t 
 |-  T = ( ( LTrn ` K ) ` W )
4 dihw.o 
 |-  .0. = ( f e. T |-> ( _I |` B ) )
5 dihw.i 
 |-  I = ( ( DIsoH ` K ) ` W )
6 dihw.k 
 |-  ( ph -> ( K e. HL /\ W e. H ) )
7 6 simprd 
 |-  ( ph -> W e. H )
8 1 2 lhpbase 
 |-  ( W e. H -> W e. B )
9 7 8 syl 
 |-  ( ph -> W e. B )
10 6 simpld 
 |-  ( ph -> K e. HL )
11 10 hllatd 
 |-  ( ph -> K e. Lat )
12 eqid 
 |-  ( le ` K ) = ( le ` K )
13 1 12 latref 
 |-  ( ( K e. Lat /\ W e. B ) -> W ( le ` K ) W )
14 11 9 13 syl2anc 
 |-  ( ph -> W ( le ` K ) W )
15 9 14 jca 
 |-  ( ph -> ( W e. B /\ W ( le ` K ) W ) )
16 eqid 
 |-  ( ( DIsoB ` K ) ` W ) = ( ( DIsoB ` K ) ` W )
17 1 12 2 5 16 dihvalb 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( W e. B /\ W ( le ` K ) W ) ) -> ( I ` W ) = ( ( ( DIsoB ` K ) ` W ) ` W ) )
18 6 15 17 syl2anc 
 |-  ( ph -> ( I ` W ) = ( ( ( DIsoB ` K ) ` W ) ` W ) )
19 eqid 
 |-  ( ( DIsoA ` K ) ` W ) = ( ( DIsoA ` K ) ` W )
20 1 12 2 3 4 19 16 dibval2 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( W e. B /\ W ( le ` K ) W ) ) -> ( ( ( DIsoB ` K ) ` W ) ` W ) = ( ( ( ( DIsoA ` K ) ` W ) ` W ) X. { .0. } ) )
21 6 15 20 syl2anc 
 |-  ( ph -> ( ( ( DIsoB ` K ) ` W ) ` W ) = ( ( ( ( DIsoA ` K ) ` W ) ` W ) X. { .0. } ) )
22 eqid 
 |-  ( ( trL ` K ) ` W ) = ( ( trL ` K ) ` W )
23 1 12 2 3 22 19 diaval 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( W e. B /\ W ( le ` K ) W ) ) -> ( ( ( DIsoA ` K ) ` W ) ` W ) = { g e. T | ( ( ( trL ` K ) ` W ) ` g ) ( le ` K ) W } )
24 6 15 23 syl2anc 
 |-  ( ph -> ( ( ( DIsoA ` K ) ` W ) ` W ) = { g e. T | ( ( ( trL ` K ) ` W ) ` g ) ( le ` K ) W } )
25 12 2 3 22 trlle 
 |-  ( ( ( K e. HL /\ W e. H ) /\ g e. T ) -> ( ( ( trL ` K ) ` W ) ` g ) ( le ` K ) W )
26 6 25 sylan 
 |-  ( ( ph /\ g e. T ) -> ( ( ( trL ` K ) ` W ) ` g ) ( le ` K ) W )
27 26 ralrimiva 
 |-  ( ph -> A. g e. T ( ( ( trL ` K ) ` W ) ` g ) ( le ` K ) W )
28 rabid2 
 |-  ( T = { g e. T | ( ( ( trL ` K ) ` W ) ` g ) ( le ` K ) W } <-> A. g e. T ( ( ( trL ` K ) ` W ) ` g ) ( le ` K ) W )
29 27 28 sylibr 
 |-  ( ph -> T = { g e. T | ( ( ( trL ` K ) ` W ) ` g ) ( le ` K ) W } )
30 24 29 eqtr4d 
 |-  ( ph -> ( ( ( DIsoA ` K ) ` W ) ` W ) = T )
31 30 xpeq1d 
 |-  ( ph -> ( ( ( ( DIsoA ` K ) ` W ) ` W ) X. { .0. } ) = ( T X. { .0. } ) )
32 18 21 31 3eqtrd 
 |-  ( ph -> ( I ` W ) = ( T X. { .0. } ) )