Metamath Proof Explorer

Theorem ldualvsubcl

Description: Closure of vector subtraction in the dual of a vector space. (Contributed by NM, 27-Feb-2015)

Ref Expression
Hypotheses ldualvsubcl.f 
|- F = ( LFnl ` W )
ldualvsubcl.d 
|- D = ( LDual ` W )
ldualvsubcl.m 
|- .- = ( -g ` D )
ldualvsubcl.w 
|- ( ph -> W e. LMod )
ldualvsubcl.g 
|- ( ph -> G e. F )
ldualvsubcl.h 
|- ( ph -> H e. F )
Assertion ldualvsubcl 
|- ( ph -> ( G .- H ) e. F )

Proof

Step Hyp Ref Expression
1 ldualvsubcl.f 
 |-  F = ( LFnl ` W )
2 ldualvsubcl.d 
 |-  D = ( LDual ` W )
3 ldualvsubcl.m 
 |-  .- = ( -g ` D )
4 ldualvsubcl.w 
 |-  ( ph -> W e. LMod )
5 ldualvsubcl.g 
 |-  ( ph -> G e. F )
6 ldualvsubcl.h 
 |-  ( ph -> H e. F )
7 eqid 
 |-  ( Scalar ` W ) = ( Scalar ` W )
8 eqid 
 |-  ( invg ` ( Scalar ` W ) ) = ( invg ` ( Scalar ` W ) )
9 eqid 
 |-  ( 1r ` ( Scalar ` W ) ) = ( 1r ` ( Scalar ` W ) )
10 eqid 
 |-  ( +g ` D ) = ( +g ` D )
11 eqid 
 |-  ( .s ` D ) = ( .s ` D )
12 7 8 9 1 2 10 11 3 4 5 6 ldualvsub 
 |-  ( ph -> ( G .- H ) = ( G ( +g ` D ) ( ( ( invg ` ( Scalar ` W ) ) ` ( 1r ` ( Scalar ` W ) ) ) ( .s ` D ) H ) ) )
13 eqid 
 |-  ( Base ` ( Scalar ` W ) ) = ( Base ` ( Scalar ` W ) )
14 7 lmodring 
 |-  ( W e. LMod -> ( Scalar ` W ) e. Ring )
15 4 14 syl 
 |-  ( ph -> ( Scalar ` W ) e. Ring )
16 ringgrp 
 |-  ( ( Scalar ` W ) e. Ring -> ( Scalar ` W ) e. Grp )
17 15 16 syl 
 |-  ( ph -> ( Scalar ` W ) e. Grp )
18 13 9 ringidcl 
 |-  ( ( Scalar ` W ) e. Ring -> ( 1r ` ( Scalar ` W ) ) e. ( Base ` ( Scalar ` W ) ) )
19 15 18 syl 
 |-  ( ph -> ( 1r ` ( Scalar ` W ) ) e. ( Base ` ( Scalar ` W ) ) )
20 13 8 grpinvcl 
 |-  ( ( ( Scalar ` W ) e. Grp /\ ( 1r ` ( Scalar ` W ) ) e. ( Base ` ( Scalar ` W ) ) ) -> ( ( invg ` ( Scalar ` W ) ) ` ( 1r ` ( Scalar ` W ) ) ) e. ( Base ` ( Scalar ` W ) ) )
21 17 19 20 syl2anc 
 |-  ( ph -> ( ( invg ` ( Scalar ` W ) ) ` ( 1r ` ( Scalar ` W ) ) ) e. ( Base ` ( Scalar ` W ) ) )
22 1 7 13 2 11 4 21 6 ldualvscl 
 |-  ( ph -> ( ( ( invg ` ( Scalar ` W ) ) ` ( 1r ` ( Scalar ` W ) ) ) ( .s ` D ) H ) e. F )
23 1 2 10 4 5 22 ldualvaddcl 
 |-  ( ph -> ( G ( +g ` D ) ( ( ( invg ` ( Scalar ` W ) ) ` ( 1r ` ( Scalar ` W ) ) ) ( .s ` D ) H ) ) e. F )
24 12 23 eqeltrd 
 |-  ( ph -> ( G .- H ) e. F )