Metamath Proof Explorer

Theorem dibelval3

Description: Member of the partial isomorphism B. (Contributed by NM, 26-Feb-2014)

Ref Expression
Hypotheses dibval3.b 
|- B = ( Base ` K )
dibval3.l 
|- .<_ = ( le ` K )
dibval3.h 
|- H = ( LHyp ` K )
dibval3.t 
|- T = ( ( LTrn ` K ) ` W )
dibval3.r 
|- R = ( ( trL ` K ) ` W )
dibval3.o 
|- .0. = ( g e. T |-> ( _I |` B ) )
dibval3.i 
|- I = ( ( DIsoB ` K ) ` W )
Assertion dibelval3 
|- ( ( ( K e. V /\ W e. H ) /\ ( X e. B /\ X .<_ W ) ) -> ( Y e. ( I ` X ) <-> E. f e. T ( Y = <. f , .0. >. /\ ( R ` f ) .<_ X ) ) )

Proof

Step Hyp Ref Expression
1 dibval3.b 
 |-  B = ( Base ` K )
2 dibval3.l 
 |-  .<_ = ( le ` K )
3 dibval3.h 
 |-  H = ( LHyp ` K )
4 dibval3.t 
 |-  T = ( ( LTrn ` K ) ` W )
5 dibval3.r 
 |-  R = ( ( trL ` K ) ` W )
6 dibval3.o 
 |-  .0. = ( g e. T |-> ( _I |` B ) )
7 dibval3.i 
 |-  I = ( ( DIsoB ` K ) ` W )
8 eqid 
 |-  ( ( DIsoA ` K ) ` W ) = ( ( DIsoA ` K ) ` W )
9 1 2 3 4 6 8 7 dibval2 
 |-  ( ( ( K e. V /\ W e. H ) /\ ( X e. B /\ X .<_ W ) ) -> ( I ` X ) = ( ( ( ( DIsoA ` K ) ` W ) ` X ) X. { .0. } ) )
10 9 eleq2d 
 |-  ( ( ( K e. V /\ W e. H ) /\ ( X e. B /\ X .<_ W ) ) -> ( Y e. ( I ` X ) <-> Y e. ( ( ( ( DIsoA ` K ) ` W ) ` X ) X. { .0. } ) ) )
11 1 2 3 4 5 8 diaelval 
 |-  ( ( ( K e. V /\ W e. H ) /\ ( X e. B /\ X .<_ W ) ) -> ( f e. ( ( ( DIsoA ` K ) ` W ) ` X ) <-> ( f e. T /\ ( R ` f ) .<_ X ) ) )
12 11 anbi1d 
 |-  ( ( ( K e. V /\ W e. H ) /\ ( X e. B /\ X .<_ W ) ) -> ( ( f e. ( ( ( DIsoA ` K ) ` W ) ` X ) /\ Y = <. f , .0. >. ) <-> ( ( f e. T /\ ( R ` f ) .<_ X ) /\ Y = <. f , .0. >. ) ) )
13 an13 
 |-  ( ( Y = <. f , s >. /\ ( f e. ( ( ( DIsoA ` K ) ` W ) ` X ) /\ s e. { .0. } ) ) <-> ( s e. { .0. } /\ ( f e. ( ( ( DIsoA ` K ) ` W ) ` X ) /\ Y = <. f , s >. ) ) )
14 velsn 
 |-  ( s e. { .0. } <-> s = .0. )
15 14 anbi1i 
 |-  ( ( s e. { .0. } /\ ( f e. ( ( ( DIsoA ` K ) ` W ) ` X ) /\ Y = <. f , s >. ) ) <-> ( s = .0. /\ ( f e. ( ( ( DIsoA ` K ) ` W ) ` X ) /\ Y = <. f , s >. ) ) )
16 13 15 bitri 
 |-  ( ( Y = <. f , s >. /\ ( f e. ( ( ( DIsoA ` K ) ` W ) ` X ) /\ s e. { .0. } ) ) <-> ( s = .0. /\ ( f e. ( ( ( DIsoA ` K ) ` W ) ` X ) /\ Y = <. f , s >. ) ) )
17 16 exbii 
 |-  ( E. s ( Y = <. f , s >. /\ ( f e. ( ( ( DIsoA ` K ) ` W ) ` X ) /\ s e. { .0. } ) ) <-> E. s ( s = .0. /\ ( f e. ( ( ( DIsoA ` K ) ` W ) ` X ) /\ Y = <. f , s >. ) ) )
18 4 fvexi 
 |-  T e. _V
19 18 mptex 
 |-  ( g e. T |-> ( _I |` B ) ) e. _V
20 6 19 eqeltri 
 |-  .0. e. _V
21 opeq2 
 |-  ( s = .0. -> <. f , s >. = <. f , .0. >. )
22 21 eqeq2d 
 |-  ( s = .0. -> ( Y = <. f , s >. <-> Y = <. f , .0. >. ) )
23 22 anbi2d 
 |-  ( s = .0. -> ( ( f e. ( ( ( DIsoA ` K ) ` W ) ` X ) /\ Y = <. f , s >. ) <-> ( f e. ( ( ( DIsoA ` K ) ` W ) ` X ) /\ Y = <. f , .0. >. ) ) )
24 20 23 ceqsexv 
 |-  ( E. s ( s = .0. /\ ( f e. ( ( ( DIsoA ` K ) ` W ) ` X ) /\ Y = <. f , s >. ) ) <-> ( f e. ( ( ( DIsoA ` K ) ` W ) ` X ) /\ Y = <. f , .0. >. ) )
25 17 24 bitri 
 |-  ( E. s ( Y = <. f , s >. /\ ( f e. ( ( ( DIsoA ` K ) ` W ) ` X ) /\ s e. { .0. } ) ) <-> ( f e. ( ( ( DIsoA ` K ) ` W ) ` X ) /\ Y = <. f , .0. >. ) )
26 anass 
 |-  ( ( ( f e. T /\ Y = <. f , .0. >. ) /\ ( R ` f ) .<_ X ) <-> ( f e. T /\ ( Y = <. f , .0. >. /\ ( R ` f ) .<_ X ) ) )
27 an32 
 |-  ( ( ( f e. T /\ Y = <. f , .0. >. ) /\ ( R ` f ) .<_ X ) <-> ( ( f e. T /\ ( R ` f ) .<_ X ) /\ Y = <. f , .0. >. ) )
28 26 27 bitr3i 
 |-  ( ( f e. T /\ ( Y = <. f , .0. >. /\ ( R ` f ) .<_ X ) ) <-> ( ( f e. T /\ ( R ` f ) .<_ X ) /\ Y = <. f , .0. >. ) )
29 12 25 28 3bitr4g 
 |-  ( ( ( K e. V /\ W e. H ) /\ ( X e. B /\ X .<_ W ) ) -> ( E. s ( Y = <. f , s >. /\ ( f e. ( ( ( DIsoA ` K ) ` W ) ` X ) /\ s e. { .0. } ) ) <-> ( f e. T /\ ( Y = <. f , .0. >. /\ ( R ` f ) .<_ X ) ) ) )
30 29 exbidv 
 |-  ( ( ( K e. V /\ W e. H ) /\ ( X e. B /\ X .<_ W ) ) -> ( E. f E. s ( Y = <. f , s >. /\ ( f e. ( ( ( DIsoA ` K ) ` W ) ` X ) /\ s e. { .0. } ) ) <-> E. f ( f e. T /\ ( Y = <. f , .0. >. /\ ( R ` f ) .<_ X ) ) ) )
31 elxp 
 |-  ( Y e. ( ( ( ( DIsoA ` K ) ` W ) ` X ) X. { .0. } ) <-> E. f E. s ( Y = <. f , s >. /\ ( f e. ( ( ( DIsoA ` K ) ` W ) ` X ) /\ s e. { .0. } ) ) )
32 df-rex 
 |-  ( E. f e. T ( Y = <. f , .0. >. /\ ( R ` f ) .<_ X ) <-> E. f ( f e. T /\ ( Y = <. f , .0. >. /\ ( R ` f ) .<_ X ) ) )
33 30 31 32 3bitr4g 
 |-  ( ( ( K e. V /\ W e. H ) /\ ( X e. B /\ X .<_ W ) ) -> ( Y e. ( ( ( ( DIsoA ` K ) ` W ) ` X ) X. { .0. } ) <-> E. f e. T ( Y = <. f , .0. >. /\ ( R ` f ) .<_ X ) ) )
34 10 33 bitrd 
 |-  ( ( ( K e. V /\ W e. H ) /\ ( X e. B /\ X .<_ W ) ) -> ( Y e. ( I ` X ) <-> E. f e. T ( Y = <. f , .0. >. /\ ( R ` f ) .<_ X ) ) )