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 )