Step |
Hyp |
Ref |
Expression |
1 |
|
tendoicl.h |
|- H = ( LHyp ` K ) |
2 |
|
tendoicl.t |
|- T = ( ( LTrn ` K ) ` W ) |
3 |
|
tendoicl.e |
|- E = ( ( TEndo ` K ) ` W ) |
4 |
|
tendoicl.i |
|- I = ( s e. E |-> ( f e. T |-> `' ( s ` f ) ) ) |
5 |
|
tendoi.b |
|- B = ( Base ` K ) |
6 |
|
tendoi.p |
|- P = ( s e. E , t e. E |-> ( f e. T |-> ( ( s ` f ) o. ( t ` f ) ) ) ) |
7 |
|
tendoi.o |
|- O = ( f e. T |-> ( _I |` B ) ) |
8 |
|
simpl |
|- ( ( ( K e. HL /\ W e. H ) /\ S e. E ) -> ( K e. HL /\ W e. H ) ) |
9 |
1 2 3 4
|
tendoicl |
|- ( ( ( K e. HL /\ W e. H ) /\ S e. E ) -> ( I ` S ) e. E ) |
10 |
|
simpr |
|- ( ( ( K e. HL /\ W e. H ) /\ S e. E ) -> S e. E ) |
11 |
1 2 3 6
|
tendoplcl |
|- ( ( ( K e. HL /\ W e. H ) /\ ( I ` S ) e. E /\ S e. E ) -> ( ( I ` S ) P S ) e. E ) |
12 |
8 9 10 11
|
syl3anc |
|- ( ( ( K e. HL /\ W e. H ) /\ S e. E ) -> ( ( I ` S ) P S ) e. E ) |
13 |
5 1 2 3 7
|
tendo0cl |
|- ( ( K e. HL /\ W e. H ) -> O e. E ) |
14 |
13
|
adantr |
|- ( ( ( K e. HL /\ W e. H ) /\ S e. E ) -> O e. E ) |
15 |
4 2
|
tendoi2 |
|- ( ( S e. E /\ g e. T ) -> ( ( I ` S ) ` g ) = `' ( S ` g ) ) |
16 |
15
|
adantll |
|- ( ( ( ( K e. HL /\ W e. H ) /\ S e. E ) /\ g e. T ) -> ( ( I ` S ) ` g ) = `' ( S ` g ) ) |
17 |
16
|
coeq1d |
|- ( ( ( ( K e. HL /\ W e. H ) /\ S e. E ) /\ g e. T ) -> ( ( ( I ` S ) ` g ) o. ( S ` g ) ) = ( `' ( S ` g ) o. ( S ` g ) ) ) |
18 |
|
simpll |
|- ( ( ( ( K e. HL /\ W e. H ) /\ S e. E ) /\ g e. T ) -> ( K e. HL /\ W e. H ) ) |
19 |
1 2 3
|
tendocl |
|- ( ( ( K e. HL /\ W e. H ) /\ S e. E /\ g e. T ) -> ( S ` g ) e. T ) |
20 |
19
|
3expa |
|- ( ( ( ( K e. HL /\ W e. H ) /\ S e. E ) /\ g e. T ) -> ( S ` g ) e. T ) |
21 |
5 1 2
|
ltrn1o |
|- ( ( ( K e. HL /\ W e. H ) /\ ( S ` g ) e. T ) -> ( S ` g ) : B -1-1-onto-> B ) |
22 |
18 20 21
|
syl2anc |
|- ( ( ( ( K e. HL /\ W e. H ) /\ S e. E ) /\ g e. T ) -> ( S ` g ) : B -1-1-onto-> B ) |
23 |
|
f1ococnv1 |
|- ( ( S ` g ) : B -1-1-onto-> B -> ( `' ( S ` g ) o. ( S ` g ) ) = ( _I |` B ) ) |
24 |
22 23
|
syl |
|- ( ( ( ( K e. HL /\ W e. H ) /\ S e. E ) /\ g e. T ) -> ( `' ( S ` g ) o. ( S ` g ) ) = ( _I |` B ) ) |
25 |
17 24
|
eqtrd |
|- ( ( ( ( K e. HL /\ W e. H ) /\ S e. E ) /\ g e. T ) -> ( ( ( I ` S ) ` g ) o. ( S ` g ) ) = ( _I |` B ) ) |
26 |
9
|
adantr |
|- ( ( ( ( K e. HL /\ W e. H ) /\ S e. E ) /\ g e. T ) -> ( I ` S ) e. E ) |
27 |
|
simplr |
|- ( ( ( ( K e. HL /\ W e. H ) /\ S e. E ) /\ g e. T ) -> S e. E ) |
28 |
|
simpr |
|- ( ( ( ( K e. HL /\ W e. H ) /\ S e. E ) /\ g e. T ) -> g e. T ) |
29 |
6 2
|
tendopl2 |
|- ( ( ( I ` S ) e. E /\ S e. E /\ g e. T ) -> ( ( ( I ` S ) P S ) ` g ) = ( ( ( I ` S ) ` g ) o. ( S ` g ) ) ) |
30 |
26 27 28 29
|
syl3anc |
|- ( ( ( ( K e. HL /\ W e. H ) /\ S e. E ) /\ g e. T ) -> ( ( ( I ` S ) P S ) ` g ) = ( ( ( I ` S ) ` g ) o. ( S ` g ) ) ) |
31 |
7 5
|
tendo02 |
|- ( g e. T -> ( O ` g ) = ( _I |` B ) ) |
32 |
31
|
adantl |
|- ( ( ( ( K e. HL /\ W e. H ) /\ S e. E ) /\ g e. T ) -> ( O ` g ) = ( _I |` B ) ) |
33 |
25 30 32
|
3eqtr4d |
|- ( ( ( ( K e. HL /\ W e. H ) /\ S e. E ) /\ g e. T ) -> ( ( ( I ` S ) P S ) ` g ) = ( O ` g ) ) |
34 |
33
|
ralrimiva |
|- ( ( ( K e. HL /\ W e. H ) /\ S e. E ) -> A. g e. T ( ( ( I ` S ) P S ) ` g ) = ( O ` g ) ) |
35 |
1 2 3
|
tendoeq1 |
|- ( ( ( K e. HL /\ W e. H ) /\ ( ( ( I ` S ) P S ) e. E /\ O e. E ) /\ A. g e. T ( ( ( I ` S ) P S ) ` g ) = ( O ` g ) ) -> ( ( I ` S ) P S ) = O ) |
36 |
8 12 14 34 35
|
syl121anc |
|- ( ( ( K e. HL /\ W e. H ) /\ S e. E ) -> ( ( I ` S ) P S ) = O ) |