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=\mathrm{LHyp}\left(K\right)$$
	hlhillvec.u	$$⊢U=\mathrm{HLHil}\left(K\right)\left(W\right)$$
	hlhillvec.k	$$⊢\phi \to \left(K\in \mathrm{HL}\wedge W\in H\right)$$
	hlhildrng.r	$$⊢R=\mathrm{Scalar}\left(U\right)$$
	hlhilsrng.l	$$⊢L=\mathrm{DVecH}\left(K\right)\left(W\right)$$
	hlhilsrng.s	$$⊢S=\mathrm{Scalar}\left(L\right)$$
	hlhilsrng.b	$$⊢B={\mathrm{Base}}_S$$
	hlhilsrng.p	$$⊢\underset{\dot{}}{+}={+}_S$$
	hlhilsrng.t	$$⊢\underset{\dot{}}{·}={\cdot }_S$$
	hlhilsrng.g	$$⊢G=\mathrm{HGMap}\left(K\right)\left(W\right)$$
Assertion	hlhilsrnglem	$$⊢\phi \to R\in \mathrm{*-Ring}$$

Proof

Step	Hyp	Ref	Expression
1		hlhillvec.h	$$⊢H=\mathrm{LHyp}\left(K\right)$$
2		hlhillvec.u	$$⊢U=\mathrm{HLHil}\left(K\right)\left(W\right)$$
3		hlhillvec.k	$$⊢\phi \to \left(K\in \mathrm{HL}\wedge W\in H\right)$$
4		hlhildrng.r	$$⊢R=\mathrm{Scalar}\left(U\right)$$
5		hlhilsrng.l	$$⊢L=\mathrm{DVecH}\left(K\right)\left(W\right)$$
6		hlhilsrng.s	$$⊢S=\mathrm{Scalar}\left(L\right)$$
7		hlhilsrng.b	$$⊢B={\mathrm{Base}}_S$$
8		hlhilsrng.p	$$⊢\underset{\dot{}}{+}={+}_S$$
9		hlhilsrng.t	$$⊢\underset{\dot{}}{·}={\cdot }_S$$
10		hlhilsrng.g	$$⊢G=\mathrm{HGMap}\left(K\right)\left(W\right)$$
11	1 5 6 2 4 3 7	hlhilsbase2	$$⊢\phi \to B={\mathrm{Base}}_R$$
12	1 5 6 2 4 3 8	hlhilsplus2	$$⊢\phi \to \underset{\dot{}}{+}={+}_R$$
13	1 5 6 2 4 3 9	hlhilsmul2	$$⊢\phi \to \underset{\dot{}}{·}={\cdot }_R$$
14	1 2 4 10 3	hlhilnvl	$$⊢\phi \to G={\mathrm{*}}_R$$
15	1 2 3 4	hlhildrng	$$⊢\phi \to R\in \mathrm{DivRing}$$
16		drngring	$$⊢R\in \mathrm{DivRing}\to R\in \mathrm{Ring}$$
17	15 16	syl	$$⊢\phi \to R\in \mathrm{Ring}$$
18	3	adantr	$$⊢\left(\phi \wedge x\in B\right)\to \left(K\in \mathrm{HL}\wedge W\in H\right)$$
19		simpr	$$⊢\left(\phi \wedge x\in B\right)\to x\in B$$
20	1 5 6 7 10 18 19	hgmapcl	$$⊢\left(\phi \wedge x\in B\right)\to G\left(x\right)\in B$$
21	3	3ad2ant1	$$⊢\left(\phi \wedge x\in B\wedge y\in B\right)\to \left(K\in \mathrm{HL}\wedge W\in H\right)$$
22		simp2	$$⊢\left(\phi \wedge x\in B\wedge y\in B\right)\to x\in B$$
23		simp3	$$⊢\left(\phi \wedge x\in B\wedge y\in B\right)\to y\in B$$
24	1 5 6 7 8 10 21 22 23	hgmapadd	$$⊢\left(\phi \wedge x\in B\wedge y\in B\right)\to G\left(x\underset{\dot{}}{+}y\right)=G\left(x\right)\underset{\dot{}}{+}G\left(y\right)$$
25	1 5 6 7 9 10 21 22 23	hgmapmul	$$⊢\left(\phi \wedge x\in B\wedge y\in B\right)\to G\left(x\underset{\dot{}}{·}y\right)=G\left(y\right)\underset{\dot{}}{·}G\left(x\right)$$
26	1 5 6 7 10 18 19	hgmapvv	$$⊢\left(\phi \wedge x\in B\right)\to G\left(G\left(x\right)\right)=x$$
27	11 12 13 14 17 20 24 25 26	issrngd	$$⊢\phi \to R\in \mathrm{*-Ring}$$