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 φ K HL W H
hlhildrng.r R = Scalar U
hlhilsrng.l L = DVecH K W
hlhilsrng.s S = Scalar L
hlhilsrng.b B = Base S
hlhilsrng.p + ˙ = + S
hlhilsrng.t · ˙ = S
hlhilsrng.g G = HGMap K W
Assertion hlhilsrnglem φ R *-Ring

Proof

Step Hyp Ref Expression
1 hlhillvec.h H = LHyp K
2 hlhillvec.u U = HLHil K W
3 hlhillvec.k φ K HL W 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 + ˙ = + S
9 hlhilsrng.t · ˙ = S
10 hlhilsrng.g G = HGMap K W
11 1 5 6 2 4 3 7 hlhilsbase2 φ B = Base R
12 1 5 6 2 4 3 8 hlhilsplus2 φ + ˙ = + R
13 1 5 6 2 4 3 9 hlhilsmul2 φ · ˙ = R
14 1 2 4 10 3 hlhilnvl φ G = * R
15 1 2 3 4 hlhildrng φ R DivRing
16 drngring R DivRing R Ring
17 15 16 syl φ R Ring
18 3 adantr φ x B K HL W H
19 simpr φ x B x B
20 1 5 6 7 10 18 19 hgmapcl φ x B G x B
21 3 3ad2ant1 φ x B y B K HL W H
22 simp2 φ x B y B x B
23 simp3 φ x B y B y B
24 1 5 6 7 8 10 21 22 23 hgmapadd φ x B y B G x + ˙ y = G x + ˙ G y
25 1 5 6 7 9 10 21 22 23 hgmapmul φ x B y B G x · ˙ y = G y · ˙ G x
26 1 5 6 7 10 18 19 hgmapvv φ x B G G x = x
27 11 12 13 14 17 20 24 25 26 issrngd φ R *-Ring