Step |
Hyp |
Ref |
Expression |
1 |
|
tendo0.b |
|- B = ( Base ` K ) |
2 |
|
tendo0.h |
|- H = ( LHyp ` K ) |
3 |
|
tendo0.t |
|- T = ( ( LTrn ` K ) ` W ) |
4 |
|
tendo0.e |
|- E = ( ( TEndo ` K ) ` W ) |
5 |
|
tendo0.o |
|- O = ( f e. T |-> ( _I |` B ) ) |
6 |
|
eqid |
|- ( le ` K ) = ( le ` K ) |
7 |
|
eqid |
|- ( ( trL ` K ) ` W ) = ( ( trL ` K ) ` W ) |
8 |
|
id |
|- ( ( K e. HL /\ W e. H ) -> ( K e. HL /\ W e. H ) ) |
9 |
1 2 3
|
idltrn |
|- ( ( K e. HL /\ W e. H ) -> ( _I |` B ) e. T ) |
10 |
9
|
adantr |
|- ( ( ( K e. HL /\ W e. H ) /\ g e. T ) -> ( _I |` B ) e. T ) |
11 |
5
|
tendo0cbv |
|- O = ( g e. T |-> ( _I |` B ) ) |
12 |
10 11
|
fmptd |
|- ( ( K e. HL /\ W e. H ) -> O : T --> T ) |
13 |
1 2 3 4 5
|
tendo0co2 |
|- ( ( ( K e. HL /\ W e. H ) /\ g e. T /\ h e. T ) -> ( O ` ( g o. h ) ) = ( ( O ` g ) o. ( O ` h ) ) ) |
14 |
1 2 3 4 5 6 7
|
tendo0tp |
|- ( ( ( K e. HL /\ W e. H ) /\ g e. T ) -> ( ( ( trL ` K ) ` W ) ` ( O ` g ) ) ( le ` K ) ( ( ( trL ` K ) ` W ) ` g ) ) |
15 |
6 2 3 7 4 8 12 13 14
|
istendod |
|- ( ( K e. HL /\ W e. H ) -> O e. E ) |