Step |
Hyp |
Ref |
Expression |
1 |
|
dvhfvadd.h |
|- H = ( LHyp ` K ) |
2 |
|
dvhfvadd.t |
|- T = ( ( LTrn ` K ) ` W ) |
3 |
|
dvhfvadd.e |
|- E = ( ( TEndo ` K ) ` W ) |
4 |
|
dvhfvadd.u |
|- U = ( ( DVecH ` K ) ` W ) |
5 |
|
dvhfvadd.f |
|- D = ( Scalar ` U ) |
6 |
|
dvhfvadd.p |
|- .+^ = ( +g ` D ) |
7 |
|
dvhfvadd.a |
|- .+b = ( f e. ( T X. E ) , g e. ( T X. E ) |-> <. ( ( 1st ` f ) o. ( 1st ` g ) ) , ( ( 2nd ` f ) .+^ ( 2nd ` g ) ) >. ) |
8 |
|
dvhfvadd.s |
|- .+ = ( +g ` U ) |
9 |
|
eqid |
|- ( ( EDRing ` K ) ` W ) = ( ( EDRing ` K ) ` W ) |
10 |
1 2 3 9 4
|
dvhset |
|- ( ( K e. HL /\ W e. H ) -> U = ( { <. ( Base ` ndx ) , ( T X. E ) >. , <. ( +g ` ndx ) , ( f e. ( T X. E ) , g e. ( T X. E ) |-> <. ( ( 1st ` f ) o. ( 1st ` g ) ) , ( h e. T |-> ( ( ( 2nd ` f ) ` h ) o. ( ( 2nd ` g ) ` h ) ) ) >. ) >. , <. ( Scalar ` ndx ) , ( ( EDRing ` K ) ` W ) >. } u. { <. ( .s ` ndx ) , ( s e. E , f e. ( T X. E ) |-> <. ( s ` ( 1st ` f ) ) , ( s o. ( 2nd ` f ) ) >. ) >. } ) ) |
11 |
10
|
fveq2d |
|- ( ( K e. HL /\ W e. H ) -> ( +g ` U ) = ( +g ` ( { <. ( Base ` ndx ) , ( T X. E ) >. , <. ( +g ` ndx ) , ( f e. ( T X. E ) , g e. ( T X. E ) |-> <. ( ( 1st ` f ) o. ( 1st ` g ) ) , ( h e. T |-> ( ( ( 2nd ` f ) ` h ) o. ( ( 2nd ` g ) ` h ) ) ) >. ) >. , <. ( Scalar ` ndx ) , ( ( EDRing ` K ) ` W ) >. } u. { <. ( .s ` ndx ) , ( s e. E , f e. ( T X. E ) |-> <. ( s ` ( 1st ` f ) ) , ( s o. ( 2nd ` f ) ) >. ) >. } ) ) ) |
12 |
1 9 4 5
|
dvhsca |
|- ( ( K e. HL /\ W e. H ) -> D = ( ( EDRing ` K ) ` W ) ) |
13 |
12
|
fveq2d |
|- ( ( K e. HL /\ W e. H ) -> ( +g ` D ) = ( +g ` ( ( EDRing ` K ) ` W ) ) ) |
14 |
6 13
|
syl5eq |
|- ( ( K e. HL /\ W e. H ) -> .+^ = ( +g ` ( ( EDRing ` K ) ` W ) ) ) |
15 |
14
|
oveqd |
|- ( ( K e. HL /\ W e. H ) -> ( ( 2nd ` f ) .+^ ( 2nd ` g ) ) = ( ( 2nd ` f ) ( +g ` ( ( EDRing ` K ) ` W ) ) ( 2nd ` g ) ) ) |
16 |
15
|
3ad2ant1 |
|- ( ( ( K e. HL /\ W e. H ) /\ f e. ( T X. E ) /\ g e. ( T X. E ) ) -> ( ( 2nd ` f ) .+^ ( 2nd ` g ) ) = ( ( 2nd ` f ) ( +g ` ( ( EDRing ` K ) ` W ) ) ( 2nd ` g ) ) ) |
17 |
|
xp2nd |
|- ( f e. ( T X. E ) -> ( 2nd ` f ) e. E ) |
18 |
|
xp2nd |
|- ( g e. ( T X. E ) -> ( 2nd ` g ) e. E ) |
19 |
17 18
|
anim12i |
|- ( ( f e. ( T X. E ) /\ g e. ( T X. E ) ) -> ( ( 2nd ` f ) e. E /\ ( 2nd ` g ) e. E ) ) |
20 |
|
eqid |
|- ( +g ` ( ( EDRing ` K ) ` W ) ) = ( +g ` ( ( EDRing ` K ) ` W ) ) |
21 |
1 2 3 9 20
|
erngplus |
|- ( ( ( K e. HL /\ W e. H ) /\ ( ( 2nd ` f ) e. E /\ ( 2nd ` g ) e. E ) ) -> ( ( 2nd ` f ) ( +g ` ( ( EDRing ` K ) ` W ) ) ( 2nd ` g ) ) = ( h e. T |-> ( ( ( 2nd ` f ) ` h ) o. ( ( 2nd ` g ) ` h ) ) ) ) |
22 |
19 21
|
sylan2 |
|- ( ( ( K e. HL /\ W e. H ) /\ ( f e. ( T X. E ) /\ g e. ( T X. E ) ) ) -> ( ( 2nd ` f ) ( +g ` ( ( EDRing ` K ) ` W ) ) ( 2nd ` g ) ) = ( h e. T |-> ( ( ( 2nd ` f ) ` h ) o. ( ( 2nd ` g ) ` h ) ) ) ) |
23 |
22
|
3impb |
|- ( ( ( K e. HL /\ W e. H ) /\ f e. ( T X. E ) /\ g e. ( T X. E ) ) -> ( ( 2nd ` f ) ( +g ` ( ( EDRing ` K ) ` W ) ) ( 2nd ` g ) ) = ( h e. T |-> ( ( ( 2nd ` f ) ` h ) o. ( ( 2nd ` g ) ` h ) ) ) ) |
24 |
16 23
|
eqtrd |
|- ( ( ( K e. HL /\ W e. H ) /\ f e. ( T X. E ) /\ g e. ( T X. E ) ) -> ( ( 2nd ` f ) .+^ ( 2nd ` g ) ) = ( h e. T |-> ( ( ( 2nd ` f ) ` h ) o. ( ( 2nd ` g ) ` h ) ) ) ) |
25 |
24
|
opeq2d |
|- ( ( ( K e. HL /\ W e. H ) /\ f e. ( T X. E ) /\ g e. ( T X. E ) ) -> <. ( ( 1st ` f ) o. ( 1st ` g ) ) , ( ( 2nd ` f ) .+^ ( 2nd ` g ) ) >. = <. ( ( 1st ` f ) o. ( 1st ` g ) ) , ( h e. T |-> ( ( ( 2nd ` f ) ` h ) o. ( ( 2nd ` g ) ` h ) ) ) >. ) |
26 |
25
|
mpoeq3dva |
|- ( ( K e. HL /\ W e. H ) -> ( f e. ( T X. E ) , g e. ( T X. E ) |-> <. ( ( 1st ` f ) o. ( 1st ` g ) ) , ( ( 2nd ` f ) .+^ ( 2nd ` g ) ) >. ) = ( f e. ( T X. E ) , g e. ( T X. E ) |-> <. ( ( 1st ` f ) o. ( 1st ` g ) ) , ( h e. T |-> ( ( ( 2nd ` f ) ` h ) o. ( ( 2nd ` g ) ` h ) ) ) >. ) ) |
27 |
2
|
fvexi |
|- T e. _V |
28 |
3
|
fvexi |
|- E e. _V |
29 |
27 28
|
xpex |
|- ( T X. E ) e. _V |
30 |
29 29
|
mpoex |
|- ( f e. ( T X. E ) , g e. ( T X. E ) |-> <. ( ( 1st ` f ) o. ( 1st ` g ) ) , ( h e. T |-> ( ( ( 2nd ` f ) ` h ) o. ( ( 2nd ` g ) ` h ) ) ) >. ) e. _V |
31 |
|
eqid |
|- ( { <. ( Base ` ndx ) , ( T X. E ) >. , <. ( +g ` ndx ) , ( f e. ( T X. E ) , g e. ( T X. E ) |-> <. ( ( 1st ` f ) o. ( 1st ` g ) ) , ( h e. T |-> ( ( ( 2nd ` f ) ` h ) o. ( ( 2nd ` g ) ` h ) ) ) >. ) >. , <. ( Scalar ` ndx ) , ( ( EDRing ` K ) ` W ) >. } u. { <. ( .s ` ndx ) , ( s e. E , f e. ( T X. E ) |-> <. ( s ` ( 1st ` f ) ) , ( s o. ( 2nd ` f ) ) >. ) >. } ) = ( { <. ( Base ` ndx ) , ( T X. E ) >. , <. ( +g ` ndx ) , ( f e. ( T X. E ) , g e. ( T X. E ) |-> <. ( ( 1st ` f ) o. ( 1st ` g ) ) , ( h e. T |-> ( ( ( 2nd ` f ) ` h ) o. ( ( 2nd ` g ) ` h ) ) ) >. ) >. , <. ( Scalar ` ndx ) , ( ( EDRing ` K ) ` W ) >. } u. { <. ( .s ` ndx ) , ( s e. E , f e. ( T X. E ) |-> <. ( s ` ( 1st ` f ) ) , ( s o. ( 2nd ` f ) ) >. ) >. } ) |
32 |
31
|
lmodplusg |
|- ( ( f e. ( T X. E ) , g e. ( T X. E ) |-> <. ( ( 1st ` f ) o. ( 1st ` g ) ) , ( h e. T |-> ( ( ( 2nd ` f ) ` h ) o. ( ( 2nd ` g ) ` h ) ) ) >. ) e. _V -> ( f e. ( T X. E ) , g e. ( T X. E ) |-> <. ( ( 1st ` f ) o. ( 1st ` g ) ) , ( h e. T |-> ( ( ( 2nd ` f ) ` h ) o. ( ( 2nd ` g ) ` h ) ) ) >. ) = ( +g ` ( { <. ( Base ` ndx ) , ( T X. E ) >. , <. ( +g ` ndx ) , ( f e. ( T X. E ) , g e. ( T X. E ) |-> <. ( ( 1st ` f ) o. ( 1st ` g ) ) , ( h e. T |-> ( ( ( 2nd ` f ) ` h ) o. ( ( 2nd ` g ) ` h ) ) ) >. ) >. , <. ( Scalar ` ndx ) , ( ( EDRing ` K ) ` W ) >. } u. { <. ( .s ` ndx ) , ( s e. E , f e. ( T X. E ) |-> <. ( s ` ( 1st ` f ) ) , ( s o. ( 2nd ` f ) ) >. ) >. } ) ) ) |
33 |
30 32
|
ax-mp |
|- ( f e. ( T X. E ) , g e. ( T X. E ) |-> <. ( ( 1st ` f ) o. ( 1st ` g ) ) , ( h e. T |-> ( ( ( 2nd ` f ) ` h ) o. ( ( 2nd ` g ) ` h ) ) ) >. ) = ( +g ` ( { <. ( Base ` ndx ) , ( T X. E ) >. , <. ( +g ` ndx ) , ( f e. ( T X. E ) , g e. ( T X. E ) |-> <. ( ( 1st ` f ) o. ( 1st ` g ) ) , ( h e. T |-> ( ( ( 2nd ` f ) ` h ) o. ( ( 2nd ` g ) ` h ) ) ) >. ) >. , <. ( Scalar ` ndx ) , ( ( EDRing ` K ) ` W ) >. } u. { <. ( .s ` ndx ) , ( s e. E , f e. ( T X. E ) |-> <. ( s ` ( 1st ` f ) ) , ( s o. ( 2nd ` f ) ) >. ) >. } ) ) |
34 |
26 33
|
eqtr2di |
|- ( ( K e. HL /\ W e. H ) -> ( +g ` ( { <. ( Base ` ndx ) , ( T X. E ) >. , <. ( +g ` ndx ) , ( f e. ( T X. E ) , g e. ( T X. E ) |-> <. ( ( 1st ` f ) o. ( 1st ` g ) ) , ( h e. T |-> ( ( ( 2nd ` f ) ` h ) o. ( ( 2nd ` g ) ` h ) ) ) >. ) >. , <. ( Scalar ` ndx ) , ( ( EDRing ` K ) ` W ) >. } u. { <. ( .s ` ndx ) , ( s e. E , f e. ( T X. E ) |-> <. ( s ` ( 1st ` f ) ) , ( s o. ( 2nd ` f ) ) >. ) >. } ) ) = ( f e. ( T X. E ) , g e. ( T X. E ) |-> <. ( ( 1st ` f ) o. ( 1st ` g ) ) , ( ( 2nd ` f ) .+^ ( 2nd ` g ) ) >. ) ) |
35 |
11 34
|
eqtrd |
|- ( ( K e. HL /\ W e. H ) -> ( +g ` U ) = ( f e. ( T X. E ) , g e. ( T X. E ) |-> <. ( ( 1st ` f ) o. ( 1st ` g ) ) , ( ( 2nd ` f ) .+^ ( 2nd ` g ) ) >. ) ) |
36 |
35 8 7
|
3eqtr4g |
|- ( ( K e. HL /\ W e. H ) -> .+ = .+b ) |