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 𝐻 = ( LHyp ‘ 𝐾 )
hlhillvec.u 𝑈 = ( ( HLHil ‘ 𝐾 ) ‘ 𝑊 )
hlhillvec.k ( 𝜑 → ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) )
hlhildrng.r 𝑅 = ( Scalar ‘ 𝑈 )
hlhilsrng.l 𝐿 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 )
hlhilsrng.s 𝑆 = ( Scalar ‘ 𝐿 )
hlhilsrng.b 𝐵 = ( Base ‘ 𝑆 )
hlhilsrng.p + = ( +g𝑆 )
hlhilsrng.t · = ( .r𝑆 )
hlhilsrng.g 𝐺 = ( ( HGMap ‘ 𝐾 ) ‘ 𝑊 )
Assertion hlhilsrnglem ( 𝜑𝑅 ∈ *-Ring )

Proof

Step Hyp Ref Expression
1 hlhillvec.h 𝐻 = ( LHyp ‘ 𝐾 )
2 hlhillvec.u 𝑈 = ( ( HLHil ‘ 𝐾 ) ‘ 𝑊 )
3 hlhillvec.k ( 𝜑 → ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) )
4 hlhildrng.r 𝑅 = ( Scalar ‘ 𝑈 )
5 hlhilsrng.l 𝐿 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 )
6 hlhilsrng.s 𝑆 = ( Scalar ‘ 𝐿 )
7 hlhilsrng.b 𝐵 = ( Base ‘ 𝑆 )
8 hlhilsrng.p + = ( +g𝑆 )
9 hlhilsrng.t · = ( .r𝑆 )
10 hlhilsrng.g 𝐺 = ( ( HGMap ‘ 𝐾 ) ‘ 𝑊 )
11 1 5 6 2 4 3 7 hlhilsbase2 ( 𝜑𝐵 = ( Base ‘ 𝑅 ) )
12 1 5 6 2 4 3 8 hlhilsplus2 ( 𝜑+ = ( +g𝑅 ) )
13 1 5 6 2 4 3 9 hlhilsmul2 ( 𝜑· = ( .r𝑅 ) )
14 1 2 4 10 3 hlhilnvl ( 𝜑𝐺 = ( *𝑟𝑅 ) )
15 1 2 3 4 hlhildrng ( 𝜑𝑅 ∈ DivRing )
16 drngring ( 𝑅 ∈ DivRing → 𝑅 ∈ Ring )
17 15 16 syl ( 𝜑𝑅 ∈ Ring )
18 3 adantr ( ( 𝜑𝑥𝐵 ) → ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) )
19 simpr ( ( 𝜑𝑥𝐵 ) → 𝑥𝐵 )
20 1 5 6 7 10 18 19 hgmapcl ( ( 𝜑𝑥𝐵 ) → ( 𝐺𝑥 ) ∈ 𝐵 )
21 3 3ad2ant1 ( ( 𝜑𝑥𝐵𝑦𝐵 ) → ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) )
22 simp2 ( ( 𝜑𝑥𝐵𝑦𝐵 ) → 𝑥𝐵 )
23 simp3 ( ( 𝜑𝑥𝐵𝑦𝐵 ) → 𝑦𝐵 )
24 1 5 6 7 8 10 21 22 23 hgmapadd ( ( 𝜑𝑥𝐵𝑦𝐵 ) → ( 𝐺 ‘ ( 𝑥 + 𝑦 ) ) = ( ( 𝐺𝑥 ) + ( 𝐺𝑦 ) ) )
25 1 5 6 7 9 10 21 22 23 hgmapmul ( ( 𝜑𝑥𝐵𝑦𝐵 ) → ( 𝐺 ‘ ( 𝑥 · 𝑦 ) ) = ( ( 𝐺𝑦 ) · ( 𝐺𝑥 ) ) )
26 1 5 6 7 10 18 19 hgmapvv ( ( 𝜑𝑥𝐵 ) → ( 𝐺 ‘ ( 𝐺𝑥 ) ) = 𝑥 )
27 11 12 13 14 17 20 24 25 26 issrngd ( 𝜑𝑅 ∈ *-Ring )