Step |
Hyp |
Ref |
Expression |
1 |
|
dvhop.b |
|- B = ( Base ` K ) |
2 |
|
dvhop.h |
|- H = ( LHyp ` K ) |
3 |
|
dvhop.t |
|- T = ( ( LTrn ` K ) ` W ) |
4 |
|
dvhop.e |
|- E = ( ( TEndo ` K ) ` W ) |
5 |
|
dvhop.p |
|- P = ( a e. E , b e. E |-> ( c e. T |-> ( ( a ` c ) o. ( b ` c ) ) ) ) |
6 |
|
dvhop.a |
|- A = ( f e. ( T X. E ) , g e. ( T X. E ) |-> <. ( ( 1st ` f ) o. ( 1st ` g ) ) , ( ( 2nd ` f ) P ( 2nd ` g ) ) >. ) |
7 |
|
dvhop.s |
|- S = ( s e. E , f e. ( T X. E ) |-> <. ( s ` ( 1st ` f ) ) , ( s o. ( 2nd ` f ) ) >. ) |
8 |
|
dvhop.o |
|- O = ( c e. T |-> ( _I |` B ) ) |
9 |
|
simprr |
|- ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ U e. E ) ) -> U e. E ) |
10 |
1 2 3
|
idltrn |
|- ( ( K e. HL /\ W e. H ) -> ( _I |` B ) e. T ) |
11 |
10
|
adantr |
|- ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ U e. E ) ) -> ( _I |` B ) e. T ) |
12 |
2 3 4
|
tendoidcl |
|- ( ( K e. HL /\ W e. H ) -> ( _I |` T ) e. E ) |
13 |
12
|
adantr |
|- ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ U e. E ) ) -> ( _I |` T ) e. E ) |
14 |
7
|
dvhopspN |
|- ( ( U e. E /\ ( ( _I |` B ) e. T /\ ( _I |` T ) e. E ) ) -> ( U S <. ( _I |` B ) , ( _I |` T ) >. ) = <. ( U ` ( _I |` B ) ) , ( U o. ( _I |` T ) ) >. ) |
15 |
9 11 13 14
|
syl12anc |
|- ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ U e. E ) ) -> ( U S <. ( _I |` B ) , ( _I |` T ) >. ) = <. ( U ` ( _I |` B ) ) , ( U o. ( _I |` T ) ) >. ) |
16 |
1 2 4
|
tendoid |
|- ( ( ( K e. HL /\ W e. H ) /\ U e. E ) -> ( U ` ( _I |` B ) ) = ( _I |` B ) ) |
17 |
16
|
adantrl |
|- ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ U e. E ) ) -> ( U ` ( _I |` B ) ) = ( _I |` B ) ) |
18 |
2 3 4
|
tendo1mulr |
|- ( ( ( K e. HL /\ W e. H ) /\ U e. E ) -> ( U o. ( _I |` T ) ) = U ) |
19 |
18
|
adantrl |
|- ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ U e. E ) ) -> ( U o. ( _I |` T ) ) = U ) |
20 |
17 19
|
opeq12d |
|- ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ U e. E ) ) -> <. ( U ` ( _I |` B ) ) , ( U o. ( _I |` T ) ) >. = <. ( _I |` B ) , U >. ) |
21 |
15 20
|
eqtrd |
|- ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ U e. E ) ) -> ( U S <. ( _I |` B ) , ( _I |` T ) >. ) = <. ( _I |` B ) , U >. ) |
22 |
21
|
oveq2d |
|- ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ U e. E ) ) -> ( <. F , O >. A ( U S <. ( _I |` B ) , ( _I |` T ) >. ) ) = ( <. F , O >. A <. ( _I |` B ) , U >. ) ) |
23 |
|
simprl |
|- ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ U e. E ) ) -> F e. T ) |
24 |
1 2 3 4 8
|
tendo0cl |
|- ( ( K e. HL /\ W e. H ) -> O e. E ) |
25 |
24
|
adantr |
|- ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ U e. E ) ) -> O e. E ) |
26 |
6
|
dvhopaddN |
|- ( ( ( F e. T /\ O e. E ) /\ ( ( _I |` B ) e. T /\ U e. E ) ) -> ( <. F , O >. A <. ( _I |` B ) , U >. ) = <. ( F o. ( _I |` B ) ) , ( O P U ) >. ) |
27 |
23 25 11 9 26
|
syl22anc |
|- ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ U e. E ) ) -> ( <. F , O >. A <. ( _I |` B ) , U >. ) = <. ( F o. ( _I |` B ) ) , ( O P U ) >. ) |
28 |
1 2 3
|
ltrn1o |
|- ( ( ( K e. HL /\ W e. H ) /\ F e. T ) -> F : B -1-1-onto-> B ) |
29 |
28
|
adantrr |
|- ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ U e. E ) ) -> F : B -1-1-onto-> B ) |
30 |
|
f1of |
|- ( F : B -1-1-onto-> B -> F : B --> B ) |
31 |
|
fcoi1 |
|- ( F : B --> B -> ( F o. ( _I |` B ) ) = F ) |
32 |
29 30 31
|
3syl |
|- ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ U e. E ) ) -> ( F o. ( _I |` B ) ) = F ) |
33 |
1 2 3 4 8 5
|
tendo0pl |
|- ( ( ( K e. HL /\ W e. H ) /\ U e. E ) -> ( O P U ) = U ) |
34 |
33
|
adantrl |
|- ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ U e. E ) ) -> ( O P U ) = U ) |
35 |
32 34
|
opeq12d |
|- ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ U e. E ) ) -> <. ( F o. ( _I |` B ) ) , ( O P U ) >. = <. F , U >. ) |
36 |
22 27 35
|
3eqtrrd |
|- ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ U e. E ) ) -> <. F , U >. = ( <. F , O >. A ( U S <. ( _I |` B ) , ( _I |` T ) >. ) ) ) |