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 |
|
tendo0pl.p |
|- P = ( s e. E , t e. E |-> ( f e. T |-> ( ( s ` f ) o. ( t ` f ) ) ) ) |
7 |
|
simpl |
|- ( ( ( K e. HL /\ W e. H ) /\ S e. E ) -> ( K e. HL /\ W e. H ) ) |
8 |
1 2 3 4 5
|
tendo0cl |
|- ( ( K e. HL /\ W e. H ) -> O e. E ) |
9 |
8
|
adantr |
|- ( ( ( K e. HL /\ W e. H ) /\ S e. E ) -> O e. E ) |
10 |
|
simpr |
|- ( ( ( K e. HL /\ W e. H ) /\ S e. E ) -> S e. E ) |
11 |
2 3 4 6
|
tendoplcl |
|- ( ( ( K e. HL /\ W e. H ) /\ O e. E /\ S e. E ) -> ( O P S ) e. E ) |
12 |
7 9 10 11
|
syl3anc |
|- ( ( ( K e. HL /\ W e. H ) /\ S e. E ) -> ( O P S ) e. E ) |
13 |
|
simpll |
|- ( ( ( ( K e. HL /\ W e. H ) /\ S e. E ) /\ g e. T ) -> ( K e. HL /\ W e. H ) ) |
14 |
13 8
|
syl |
|- ( ( ( ( K e. HL /\ W e. H ) /\ S e. E ) /\ g e. T ) -> O e. E ) |
15 |
|
simplr |
|- ( ( ( ( K e. HL /\ W e. H ) /\ S e. E ) /\ g e. T ) -> S e. E ) |
16 |
|
simpr |
|- ( ( ( ( K e. HL /\ W e. H ) /\ S e. E ) /\ g e. T ) -> g e. T ) |
17 |
6 3
|
tendopl2 |
|- ( ( O e. E /\ S e. E /\ g e. T ) -> ( ( O P S ) ` g ) = ( ( O ` g ) o. ( S ` g ) ) ) |
18 |
14 15 16 17
|
syl3anc |
|- ( ( ( ( K e. HL /\ W e. H ) /\ S e. E ) /\ g e. T ) -> ( ( O P S ) ` g ) = ( ( O ` g ) o. ( S ` g ) ) ) |
19 |
5 1
|
tendo02 |
|- ( g e. T -> ( O ` g ) = ( _I |` B ) ) |
20 |
19
|
adantl |
|- ( ( ( ( K e. HL /\ W e. H ) /\ S e. E ) /\ g e. T ) -> ( O ` g ) = ( _I |` B ) ) |
21 |
20
|
coeq1d |
|- ( ( ( ( K e. HL /\ W e. H ) /\ S e. E ) /\ g e. T ) -> ( ( O ` g ) o. ( S ` g ) ) = ( ( _I |` B ) o. ( S ` g ) ) ) |
22 |
2 3 4
|
tendocl |
|- ( ( ( K e. HL /\ W e. H ) /\ S e. E /\ g e. T ) -> ( S ` g ) e. T ) |
23 |
22
|
3expa |
|- ( ( ( ( K e. HL /\ W e. H ) /\ S e. E ) /\ g e. T ) -> ( S ` g ) e. T ) |
24 |
1 2 3
|
ltrn1o |
|- ( ( ( K e. HL /\ W e. H ) /\ ( S ` g ) e. T ) -> ( S ` g ) : B -1-1-onto-> B ) |
25 |
13 23 24
|
syl2anc |
|- ( ( ( ( K e. HL /\ W e. H ) /\ S e. E ) /\ g e. T ) -> ( S ` g ) : B -1-1-onto-> B ) |
26 |
|
f1of |
|- ( ( S ` g ) : B -1-1-onto-> B -> ( S ` g ) : B --> B ) |
27 |
|
fcoi2 |
|- ( ( S ` g ) : B --> B -> ( ( _I |` B ) o. ( S ` g ) ) = ( S ` g ) ) |
28 |
25 26 27
|
3syl |
|- ( ( ( ( K e. HL /\ W e. H ) /\ S e. E ) /\ g e. T ) -> ( ( _I |` B ) o. ( S ` g ) ) = ( S ` g ) ) |
29 |
18 21 28
|
3eqtrd |
|- ( ( ( ( K e. HL /\ W e. H ) /\ S e. E ) /\ g e. T ) -> ( ( O P S ) ` g ) = ( S ` g ) ) |
30 |
29
|
ralrimiva |
|- ( ( ( K e. HL /\ W e. H ) /\ S e. E ) -> A. g e. T ( ( O P S ) ` g ) = ( S ` g ) ) |
31 |
2 3 4
|
tendoeq1 |
|- ( ( ( K e. HL /\ W e. H ) /\ ( ( O P S ) e. E /\ S e. E ) /\ A. g e. T ( ( O P S ) ` g ) = ( S ` g ) ) -> ( O P S ) = S ) |
32 |
7 12 10 30 31
|
syl121anc |
|- ( ( ( K e. HL /\ W e. H ) /\ S e. E ) -> ( O P S ) = S ) |