Metamath Proof Explorer


Theorem hlhilsrnglem

Description: Lemma for hlhilsrng . (Contributed by NM, 21-Jun-2015) (Revised by Mario Carneiro, 28-Jun-2015)

Ref Expression
Hypotheses hlhillvec.h
|- H = ( LHyp ` K )
hlhillvec.u
|- U = ( ( HLHil ` K ) ` W )
hlhillvec.k
|- ( ph -> ( K e. HL /\ W e. H ) )
hlhildrng.r
|- R = ( Scalar ` U )
hlhilsrng.l
|- L = ( ( DVecH ` K ) ` W )
hlhilsrng.s
|- S = ( Scalar ` L )
hlhilsrng.b
|- B = ( Base ` S )
hlhilsrng.p
|- .+ = ( +g ` S )
hlhilsrng.t
|- .x. = ( .r ` S )
hlhilsrng.g
|- G = ( ( HGMap ` K ) ` W )
Assertion hlhilsrnglem
|- ( ph -> R e. *Ring )

Proof

Step Hyp Ref Expression
1 hlhillvec.h
 |-  H = ( LHyp ` K )
2 hlhillvec.u
 |-  U = ( ( HLHil ` K ) ` W )
3 hlhillvec.k
 |-  ( ph -> ( K e. HL /\ W e. H ) )
4 hlhildrng.r
 |-  R = ( Scalar ` U )
5 hlhilsrng.l
 |-  L = ( ( DVecH ` K ) ` W )
6 hlhilsrng.s
 |-  S = ( Scalar ` L )
7 hlhilsrng.b
 |-  B = ( Base ` S )
8 hlhilsrng.p
 |-  .+ = ( +g ` S )
9 hlhilsrng.t
 |-  .x. = ( .r ` S )
10 hlhilsrng.g
 |-  G = ( ( HGMap ` K ) ` W )
11 1 5 6 2 4 3 7 hlhilsbase2
 |-  ( ph -> B = ( Base ` R ) )
12 1 5 6 2 4 3 8 hlhilsplus2
 |-  ( ph -> .+ = ( +g ` R ) )
13 1 5 6 2 4 3 9 hlhilsmul2
 |-  ( ph -> .x. = ( .r ` R ) )
14 1 2 4 10 3 hlhilnvl
 |-  ( ph -> G = ( *r ` R ) )
15 1 2 3 4 hlhildrng
 |-  ( ph -> R e. DivRing )
16 drngring
 |-  ( R e. DivRing -> R e. Ring )
17 15 16 syl
 |-  ( ph -> R e. Ring )
18 3 adantr
 |-  ( ( ph /\ x e. B ) -> ( K e. HL /\ W e. H ) )
19 simpr
 |-  ( ( ph /\ x e. B ) -> x e. B )
20 1 5 6 7 10 18 19 hgmapcl
 |-  ( ( ph /\ x e. B ) -> ( G ` x ) e. B )
21 3 3ad2ant1
 |-  ( ( ph /\ x e. B /\ y e. B ) -> ( K e. HL /\ W e. H ) )
22 simp2
 |-  ( ( ph /\ x e. B /\ y e. B ) -> x e. B )
23 simp3
 |-  ( ( ph /\ x e. B /\ y e. B ) -> y e. B )
24 1 5 6 7 8 10 21 22 23 hgmapadd
 |-  ( ( ph /\ x e. B /\ y e. B ) -> ( G ` ( x .+ y ) ) = ( ( G ` x ) .+ ( G ` y ) ) )
25 1 5 6 7 9 10 21 22 23 hgmapmul
 |-  ( ( ph /\ x e. B /\ y e. B ) -> ( G ` ( x .x. y ) ) = ( ( G ` y ) .x. ( G ` x ) ) )
26 1 5 6 7 10 18 19 hgmapvv
 |-  ( ( ph /\ x e. B ) -> ( G ` ( G ` x ) ) = x )
27 11 12 13 14 17 20 24 25 26 issrngd
 |-  ( ph -> R e. *Ring )