Step |
Hyp |
Ref |
Expression |
1 |
|
dib1dim.b |
|- B = ( Base ` K ) |
2 |
|
dib1dim.h |
|- H = ( LHyp ` K ) |
3 |
|
dib1dim.t |
|- T = ( ( LTrn ` K ) ` W ) |
4 |
|
dib1dim.r |
|- R = ( ( trL ` K ) ` W ) |
5 |
|
dib1dim.e |
|- E = ( ( TEndo ` K ) ` W ) |
6 |
|
dib1dim.o |
|- O = ( h e. T |-> ( _I |` B ) ) |
7 |
|
dib1dim.i |
|- I = ( ( DIsoB ` K ) ` W ) |
8 |
|
simpl |
|- ( ( ( K e. HL /\ W e. H ) /\ F e. T ) -> ( K e. HL /\ W e. H ) ) |
9 |
1 2 3 4
|
trlcl |
|- ( ( ( K e. HL /\ W e. H ) /\ F e. T ) -> ( R ` F ) e. B ) |
10 |
|
eqid |
|- ( le ` K ) = ( le ` K ) |
11 |
10 2 3 4
|
trlle |
|- ( ( ( K e. HL /\ W e. H ) /\ F e. T ) -> ( R ` F ) ( le ` K ) W ) |
12 |
|
eqid |
|- ( ( DIsoA ` K ) ` W ) = ( ( DIsoA ` K ) ` W ) |
13 |
1 10 2 3 6 12 7
|
dibval2 |
|- ( ( ( K e. HL /\ W e. H ) /\ ( ( R ` F ) e. B /\ ( R ` F ) ( le ` K ) W ) ) -> ( I ` ( R ` F ) ) = ( ( ( ( DIsoA ` K ) ` W ) ` ( R ` F ) ) X. { O } ) ) |
14 |
8 9 11 13
|
syl12anc |
|- ( ( ( K e. HL /\ W e. H ) /\ F e. T ) -> ( I ` ( R ` F ) ) = ( ( ( ( DIsoA ` K ) ` W ) ` ( R ` F ) ) X. { O } ) ) |
15 |
|
relxp |
|- Rel ( ( ( ( DIsoA ` K ) ` W ) ` ( R ` F ) ) X. { O } ) |
16 |
|
opelxp |
|- ( <. f , t >. e. ( ( ( ( DIsoA ` K ) ` W ) ` ( R ` F ) ) X. { O } ) <-> ( f e. ( ( ( DIsoA ` K ) ` W ) ` ( R ` F ) ) /\ t e. { O } ) ) |
17 |
2 3 4 5 12
|
dia1dim |
|- ( ( ( K e. HL /\ W e. H ) /\ F e. T ) -> ( ( ( DIsoA ` K ) ` W ) ` ( R ` F ) ) = { f | E. s e. E f = ( s ` F ) } ) |
18 |
17
|
abeq2d |
|- ( ( ( K e. HL /\ W e. H ) /\ F e. T ) -> ( f e. ( ( ( DIsoA ` K ) ` W ) ` ( R ` F ) ) <-> E. s e. E f = ( s ` F ) ) ) |
19 |
18
|
anbi1d |
|- ( ( ( K e. HL /\ W e. H ) /\ F e. T ) -> ( ( f e. ( ( ( DIsoA ` K ) ` W ) ` ( R ` F ) ) /\ t e. { O } ) <-> ( E. s e. E f = ( s ` F ) /\ t e. { O } ) ) ) |
20 |
2 3 5
|
tendocl |
|- ( ( ( K e. HL /\ W e. H ) /\ s e. E /\ F e. T ) -> ( s ` F ) e. T ) |
21 |
20
|
3expa |
|- ( ( ( ( K e. HL /\ W e. H ) /\ s e. E ) /\ F e. T ) -> ( s ` F ) e. T ) |
22 |
21
|
an32s |
|- ( ( ( ( K e. HL /\ W e. H ) /\ F e. T ) /\ s e. E ) -> ( s ` F ) e. T ) |
23 |
1 2 3 5 6
|
tendo0cl |
|- ( ( K e. HL /\ W e. H ) -> O e. E ) |
24 |
23
|
ad2antrr |
|- ( ( ( ( K e. HL /\ W e. H ) /\ F e. T ) /\ s e. E ) -> O e. E ) |
25 |
22 24
|
jca |
|- ( ( ( ( K e. HL /\ W e. H ) /\ F e. T ) /\ s e. E ) -> ( ( s ` F ) e. T /\ O e. E ) ) |
26 |
|
eleq1 |
|- ( f = ( s ` F ) -> ( f e. T <-> ( s ` F ) e. T ) ) |
27 |
|
eleq1 |
|- ( t = O -> ( t e. E <-> O e. E ) ) |
28 |
26 27
|
bi2anan9 |
|- ( ( f = ( s ` F ) /\ t = O ) -> ( ( f e. T /\ t e. E ) <-> ( ( s ` F ) e. T /\ O e. E ) ) ) |
29 |
25 28
|
syl5ibrcom |
|- ( ( ( ( K e. HL /\ W e. H ) /\ F e. T ) /\ s e. E ) -> ( ( f = ( s ` F ) /\ t = O ) -> ( f e. T /\ t e. E ) ) ) |
30 |
29
|
rexlimdva |
|- ( ( ( K e. HL /\ W e. H ) /\ F e. T ) -> ( E. s e. E ( f = ( s ` F ) /\ t = O ) -> ( f e. T /\ t e. E ) ) ) |
31 |
30
|
pm4.71rd |
|- ( ( ( K e. HL /\ W e. H ) /\ F e. T ) -> ( E. s e. E ( f = ( s ` F ) /\ t = O ) <-> ( ( f e. T /\ t e. E ) /\ E. s e. E ( f = ( s ` F ) /\ t = O ) ) ) ) |
32 |
|
velsn |
|- ( t e. { O } <-> t = O ) |
33 |
32
|
anbi2i |
|- ( ( E. s e. E f = ( s ` F ) /\ t e. { O } ) <-> ( E. s e. E f = ( s ` F ) /\ t = O ) ) |
34 |
|
r19.41v |
|- ( E. s e. E ( f = ( s ` F ) /\ t = O ) <-> ( E. s e. E f = ( s ` F ) /\ t = O ) ) |
35 |
33 34
|
bitr4i |
|- ( ( E. s e. E f = ( s ` F ) /\ t e. { O } ) <-> E. s e. E ( f = ( s ` F ) /\ t = O ) ) |
36 |
|
df-3an |
|- ( ( f e. T /\ t e. E /\ E. s e. E ( f = ( s ` F ) /\ t = O ) ) <-> ( ( f e. T /\ t e. E ) /\ E. s e. E ( f = ( s ` F ) /\ t = O ) ) ) |
37 |
31 35 36
|
3bitr4g |
|- ( ( ( K e. HL /\ W e. H ) /\ F e. T ) -> ( ( E. s e. E f = ( s ` F ) /\ t e. { O } ) <-> ( f e. T /\ t e. E /\ E. s e. E ( f = ( s ` F ) /\ t = O ) ) ) ) |
38 |
19 37
|
bitrd |
|- ( ( ( K e. HL /\ W e. H ) /\ F e. T ) -> ( ( f e. ( ( ( DIsoA ` K ) ` W ) ` ( R ` F ) ) /\ t e. { O } ) <-> ( f e. T /\ t e. E /\ E. s e. E ( f = ( s ` F ) /\ t = O ) ) ) ) |
39 |
16 38
|
syl5bb |
|- ( ( ( K e. HL /\ W e. H ) /\ F e. T ) -> ( <. f , t >. e. ( ( ( ( DIsoA ` K ) ` W ) ` ( R ` F ) ) X. { O } ) <-> ( f e. T /\ t e. E /\ E. s e. E ( f = ( s ` F ) /\ t = O ) ) ) ) |
40 |
15 39
|
opabbi2dv |
|- ( ( ( K e. HL /\ W e. H ) /\ F e. T ) -> ( ( ( ( DIsoA ` K ) ` W ) ` ( R ` F ) ) X. { O } ) = { <. f , t >. | ( f e. T /\ t e. E /\ E. s e. E ( f = ( s ` F ) /\ t = O ) ) } ) |
41 |
14 40
|
eqtrd |
|- ( ( ( K e. HL /\ W e. H ) /\ F e. T ) -> ( I ` ( R ` F ) ) = { <. f , t >. | ( f e. T /\ t e. E /\ E. s e. E ( f = ( s ` F ) /\ t = O ) ) } ) |
42 |
|
eqeq1 |
|- ( g = <. f , t >. -> ( g = <. ( s ` F ) , O >. <-> <. f , t >. = <. ( s ` F ) , O >. ) ) |
43 |
|
vex |
|- f e. _V |
44 |
|
vex |
|- t e. _V |
45 |
43 44
|
opth |
|- ( <. f , t >. = <. ( s ` F ) , O >. <-> ( f = ( s ` F ) /\ t = O ) ) |
46 |
42 45
|
syl6bb |
|- ( g = <. f , t >. -> ( g = <. ( s ` F ) , O >. <-> ( f = ( s ` F ) /\ t = O ) ) ) |
47 |
46
|
rexbidv |
|- ( g = <. f , t >. -> ( E. s e. E g = <. ( s ` F ) , O >. <-> E. s e. E ( f = ( s ` F ) /\ t = O ) ) ) |
48 |
47
|
rabxp |
|- { g e. ( T X. E ) | E. s e. E g = <. ( s ` F ) , O >. } = { <. f , t >. | ( f e. T /\ t e. E /\ E. s e. E ( f = ( s ` F ) /\ t = O ) ) } |
49 |
41 48
|
eqtr4di |
|- ( ( ( K e. HL /\ W e. H ) /\ F e. T ) -> ( I ` ( R ` F ) ) = { g e. ( T X. E ) | E. s e. E g = <. ( s ` F ) , O >. } ) |