Step |
Hyp |
Ref |
Expression |
1 |
|
tgrpset.h |
|- H = ( LHyp ` K ) |
2 |
|
tgrpset.t |
|- T = ( ( LTrn ` K ) ` W ) |
3 |
|
tgrpset.g |
|- G = ( ( TGrp ` K ) ` W ) |
4 |
|
tgrp.o |
|- .+ = ( +g ` G ) |
5 |
1 2 3 4
|
tgrpopr |
|- ( ( K e. V /\ W e. H ) -> .+ = ( f e. T , g e. T |-> ( f o. g ) ) ) |
6 |
5
|
3adant3 |
|- ( ( K e. V /\ W e. H /\ ( X e. T /\ Y e. T ) ) -> .+ = ( f e. T , g e. T |-> ( f o. g ) ) ) |
7 |
6
|
oveqd |
|- ( ( K e. V /\ W e. H /\ ( X e. T /\ Y e. T ) ) -> ( X .+ Y ) = ( X ( f e. T , g e. T |-> ( f o. g ) ) Y ) ) |
8 |
|
simp3l |
|- ( ( K e. V /\ W e. H /\ ( X e. T /\ Y e. T ) ) -> X e. T ) |
9 |
|
simp3r |
|- ( ( K e. V /\ W e. H /\ ( X e. T /\ Y e. T ) ) -> Y e. T ) |
10 |
|
coexg |
|- ( ( X e. T /\ Y e. T ) -> ( X o. Y ) e. _V ) |
11 |
10
|
3ad2ant3 |
|- ( ( K e. V /\ W e. H /\ ( X e. T /\ Y e. T ) ) -> ( X o. Y ) e. _V ) |
12 |
|
coeq1 |
|- ( f = X -> ( f o. g ) = ( X o. g ) ) |
13 |
|
coeq2 |
|- ( g = Y -> ( X o. g ) = ( X o. Y ) ) |
14 |
|
eqid |
|- ( f e. T , g e. T |-> ( f o. g ) ) = ( f e. T , g e. T |-> ( f o. g ) ) |
15 |
12 13 14
|
ovmpog |
|- ( ( X e. T /\ Y e. T /\ ( X o. Y ) e. _V ) -> ( X ( f e. T , g e. T |-> ( f o. g ) ) Y ) = ( X o. Y ) ) |
16 |
8 9 11 15
|
syl3anc |
|- ( ( K e. V /\ W e. H /\ ( X e. T /\ Y e. T ) ) -> ( X ( f e. T , g e. T |-> ( f o. g ) ) Y ) = ( X o. Y ) ) |
17 |
7 16
|
eqtrd |
|- ( ( K e. V /\ W e. H /\ ( X e. T /\ Y e. T ) ) -> ( X .+ Y ) = ( X o. Y ) ) |