Step |
Hyp |
Ref |
Expression |
1 |
|
hdmap12c.h |
|- H = ( LHyp ` K ) |
2 |
|
hdmap12c.u |
|- U = ( ( DVecH ` K ) ` W ) |
3 |
|
hdmap12c.v |
|- V = ( Base ` U ) |
4 |
|
hdmap12c.m |
|- .- = ( -g ` U ) |
5 |
|
hdmap12c.c |
|- C = ( ( LCDual ` K ) ` W ) |
6 |
|
hdmap12c.n |
|- N = ( -g ` C ) |
7 |
|
hdmap12c.s |
|- S = ( ( HDMap ` K ) ` W ) |
8 |
|
hdmap12c.k |
|- ( ph -> ( K e. HL /\ W e. H ) ) |
9 |
|
hdmap12c.x |
|- ( ph -> X e. V ) |
10 |
|
hdmap12c.y |
|- ( ph -> Y e. V ) |
11 |
|
eqid |
|- ( +g ` U ) = ( +g ` U ) |
12 |
|
eqid |
|- ( invg ` U ) = ( invg ` U ) |
13 |
3 11 12 4
|
grpsubval |
|- ( ( X e. V /\ Y e. V ) -> ( X .- Y ) = ( X ( +g ` U ) ( ( invg ` U ) ` Y ) ) ) |
14 |
9 10 13
|
syl2anc |
|- ( ph -> ( X .- Y ) = ( X ( +g ` U ) ( ( invg ` U ) ` Y ) ) ) |
15 |
14
|
fveq2d |
|- ( ph -> ( S ` ( X .- Y ) ) = ( S ` ( X ( +g ` U ) ( ( invg ` U ) ` Y ) ) ) ) |
16 |
|
eqid |
|- ( +g ` C ) = ( +g ` C ) |
17 |
1 2 8
|
dvhlmod |
|- ( ph -> U e. LMod ) |
18 |
3 12
|
lmodvnegcl |
|- ( ( U e. LMod /\ Y e. V ) -> ( ( invg ` U ) ` Y ) e. V ) |
19 |
17 10 18
|
syl2anc |
|- ( ph -> ( ( invg ` U ) ` Y ) e. V ) |
20 |
1 2 3 11 5 16 7 8 9 19
|
hdmapadd |
|- ( ph -> ( S ` ( X ( +g ` U ) ( ( invg ` U ) ` Y ) ) ) = ( ( S ` X ) ( +g ` C ) ( S ` ( ( invg ` U ) ` Y ) ) ) ) |
21 |
|
eqid |
|- ( invg ` C ) = ( invg ` C ) |
22 |
1 2 3 12 5 21 7 8 10
|
hdmapneg |
|- ( ph -> ( S ` ( ( invg ` U ) ` Y ) ) = ( ( invg ` C ) ` ( S ` Y ) ) ) |
23 |
22
|
oveq2d |
|- ( ph -> ( ( S ` X ) ( +g ` C ) ( S ` ( ( invg ` U ) ` Y ) ) ) = ( ( S ` X ) ( +g ` C ) ( ( invg ` C ) ` ( S ` Y ) ) ) ) |
24 |
15 20 23
|
3eqtrd |
|- ( ph -> ( S ` ( X .- Y ) ) = ( ( S ` X ) ( +g ` C ) ( ( invg ` C ) ` ( S ` Y ) ) ) ) |
25 |
|
eqid |
|- ( Base ` C ) = ( Base ` C ) |
26 |
1 2 3 5 25 7 8 9
|
hdmapcl |
|- ( ph -> ( S ` X ) e. ( Base ` C ) ) |
27 |
1 2 3 5 25 7 8 10
|
hdmapcl |
|- ( ph -> ( S ` Y ) e. ( Base ` C ) ) |
28 |
25 16 21 6
|
grpsubval |
|- ( ( ( S ` X ) e. ( Base ` C ) /\ ( S ` Y ) e. ( Base ` C ) ) -> ( ( S ` X ) N ( S ` Y ) ) = ( ( S ` X ) ( +g ` C ) ( ( invg ` C ) ` ( S ` Y ) ) ) ) |
29 |
26 27 28
|
syl2anc |
|- ( ph -> ( ( S ` X ) N ( S ` Y ) ) = ( ( S ` X ) ( +g ` C ) ( ( invg ` C ) ` ( S ` Y ) ) ) ) |
30 |
24 29
|
eqtr4d |
|- ( ph -> ( S ` ( X .- Y ) ) = ( ( S ` X ) N ( S ` Y ) ) ) |