Theorem drgextlsp

Description: The scalar field is a subspace of a subring algebra. (Contributed by Thierry Arnoux, 17-Jul-2023)

	Ref	Expression
Hypotheses	drgext.b	$$⊢B=\mathrm{subringAlg}\left(E\right)\left(U\right)$$
	drgext.1	$$⊢\phi \to E\in \mathrm{DivRing}$$
	drgext.2	$$⊢\phi \to U\in \mathrm{SubRing}\left(E\right)$$
	drgext.f	$$⊢F=E{\upharpoonright }_{𝑠}U$$
	drgext.3	$$⊢\phi \to F\in \mathrm{DivRing}$$
Assertion	drgextlsp	$$⊢\phi \to U\in \mathrm{LSubSp}\left(B\right)$$

Proof

Step	Hyp	Ref	Expression
1		drgext.b	$$⊢B=\mathrm{subringAlg}\left(E\right)\left(U\right)$$
2		drgext.1	$$⊢\phi \to E\in \mathrm{DivRing}$$
3		drgext.2	$$⊢\phi \to U\in \mathrm{SubRing}\left(E\right)$$
4		drgext.f	$$⊢F=E{\upharpoonright }_{𝑠}U$$
5		drgext.3	$$⊢\phi \to F\in \mathrm{DivRing}$$
6		eqidd	$$⊢\phi \to \mathrm{Scalar}\left(B\right)=\mathrm{Scalar}\left(B\right)$$
7		eqidd	$$⊢\phi \to {\mathrm{Base}}_{\mathrm{Scalar}\left(B\right)}={\mathrm{Base}}_{\mathrm{Scalar}\left(B\right)}$$
8		eqidd	$$⊢\phi \to {\mathrm{Base}}_B={\mathrm{Base}}_B$$
9		eqidd	$$⊢\phi \to {+}_B={+}_B$$
10		eqidd	$$⊢\phi \to {\cdot }_B={\cdot }_B$$
11		eqidd	$$⊢\phi \to \mathrm{LSubSp}\left(B\right)=\mathrm{LSubSp}\left(B\right)$$
12		eqid	$$⊢{\mathrm{Base}}_E={\mathrm{Base}}_E$$
13	12	subrgss	$$⊢U\in \mathrm{SubRing}\left(E\right)\to U\subseteq {\mathrm{Base}}_E$$
14	3 13	syl	$$⊢\phi \to U\subseteq {\mathrm{Base}}_E$$
15	1	a1i	$$⊢\phi \to B=\mathrm{subringAlg}\left(E\right)\left(U\right)$$
16	15 14	srabase	$$⊢\phi \to {\mathrm{Base}}_E={\mathrm{Base}}_B$$
17	14 16	sseqtrd	$$⊢\phi \to U\subseteq {\mathrm{Base}}_B$$
18		eqid	$$⊢1_E=1_E$$
19	18	subrg1cl	$$⊢U\in \mathrm{SubRing}\left(E\right)\to 1_E\in U$$
20		ne0i	$$⊢1_E\in U\to U\ne \varnothing$$
21	3 19 20	3syl	$$⊢\phi \to U\ne \varnothing$$
22		drnggrp	$$⊢F\in \mathrm{DivRing}\to F\in \mathrm{Grp}$$
23	5 22	syl	$$⊢\phi \to F\in \mathrm{Grp}$$
24	23	adantr	$$⊢\left(\phi \wedge \left(x\in {\mathrm{Base}}_{\mathrm{Scalar}\left(B\right)}\wedge a\in U\wedge b\in U\right)\right)\to F\in \mathrm{Grp}$$
25	15 14	sravsca	$$⊢\phi \to {\cdot }_E={\cdot }_B$$
26		eqid	$$⊢{\cdot }_E={\cdot }_E$$
27	4 26	ressmulr	$$⊢U\in \mathrm{SubRing}\left(E\right)\to {\cdot }_E={\cdot }_F$$
28	3 27	syl	$$⊢\phi \to {\cdot }_E={\cdot }_F$$
29	25 28	eqtr3d	$$⊢\phi \to {\cdot }_B={\cdot }_F$$
30	29	oveqdr	$$⊢\left(\phi \wedge \left(x\in {\mathrm{Base}}_{\mathrm{Scalar}\left(B\right)}\wedge a\in U\wedge b\in U\right)\right)\to x{\cdot }_{B}a=x{\cdot }_{F}a$$
31		drngring	$$⊢F\in \mathrm{DivRing}\to F\in \mathrm{Ring}$$
32	5 31	syl	$$⊢\phi \to F\in \mathrm{Ring}$$
33	32	adantr	$$⊢\left(\phi \wedge \left(x\in {\mathrm{Base}}_{\mathrm{Scalar}\left(B\right)}\wedge a\in U\wedge b\in U\right)\right)\to F\in \mathrm{Ring}$$
34		simpr1	$$⊢\left(\phi \wedge \left(x\in {\mathrm{Base}}_{\mathrm{Scalar}\left(B\right)}\wedge a\in U\wedge b\in U\right)\right)\to x\in {\mathrm{Base}}_{\mathrm{Scalar}\left(B\right)}$$
35	15 14	srasca	$$⊢\phi \to E{\upharpoonright }_{𝑠}U=\mathrm{Scalar}\left(B\right)$$
36	4 35	syl5eq	$$⊢\phi \to F=\mathrm{Scalar}\left(B\right)$$
37	36	fveq2d	$$⊢\phi \to {\mathrm{Base}}_F={\mathrm{Base}}_{\mathrm{Scalar}\left(B\right)}$$
38	37	adantr	$$⊢\left(\phi \wedge \left(x\in {\mathrm{Base}}_{\mathrm{Scalar}\left(B\right)}\wedge a\in U\wedge b\in U\right)\right)\to {\mathrm{Base}}_F={\mathrm{Base}}_{\mathrm{Scalar}\left(B\right)}$$
39	34 38	eleqtrrd	$$⊢\left(\phi \wedge \left(x\in {\mathrm{Base}}_{\mathrm{Scalar}\left(B\right)}\wedge a\in U\wedge b\in U\right)\right)\to x\in {\mathrm{Base}}_F$$
40		simpr2	$$⊢\left(\phi \wedge \left(x\in {\mathrm{Base}}_{\mathrm{Scalar}\left(B\right)}\wedge a\in U\wedge b\in U\right)\right)\to a\in U$$
41	4 12	ressbas2	$$⊢U\subseteq {\mathrm{Base}}_E\to U={\mathrm{Base}}_F$$
42	14 41	syl	$$⊢\phi \to U={\mathrm{Base}}_F$$
43	42	adantr	$$⊢\left(\phi \wedge \left(x\in {\mathrm{Base}}_{\mathrm{Scalar}\left(B\right)}\wedge a\in U\wedge b\in U\right)\right)\to U={\mathrm{Base}}_F$$
44	40 43	eleqtrd	$$⊢\left(\phi \wedge \left(x\in {\mathrm{Base}}_{\mathrm{Scalar}\left(B\right)}\wedge a\in U\wedge b\in U\right)\right)\to a\in {\mathrm{Base}}_F$$
45		eqid	$$⊢{\mathrm{Base}}_F={\mathrm{Base}}_F$$
46		eqid	$$⊢{\cdot }_F={\cdot }_F$$
47	45 46	ringcl	$$⊢\left(F\in \mathrm{Ring}\wedge x\in {\mathrm{Base}}_F\wedge a\in {\mathrm{Base}}_F\right)\to x{\cdot }_{F}a\in {\mathrm{Base}}_F$$
48	33 39 44 47	syl3anc	$$⊢\left(\phi \wedge \left(x\in {\mathrm{Base}}_{\mathrm{Scalar}\left(B\right)}\wedge a\in U\wedge b\in U\right)\right)\to x{\cdot }_{F}a\in {\mathrm{Base}}_F$$
49	30 48	eqeltrd	$$⊢\left(\phi \wedge \left(x\in {\mathrm{Base}}_{\mathrm{Scalar}\left(B\right)}\wedge a\in U\wedge b\in U\right)\right)\to x{\cdot }_{B}a\in {\mathrm{Base}}_F$$
50		simpr3	$$⊢\left(\phi \wedge \left(x\in {\mathrm{Base}}_{\mathrm{Scalar}\left(B\right)}\wedge a\in U\wedge b\in U\right)\right)\to b\in U$$
51	50 43	eleqtrd	$$⊢\left(\phi \wedge \left(x\in {\mathrm{Base}}_{\mathrm{Scalar}\left(B\right)}\wedge a\in U\wedge b\in U\right)\right)\to b\in {\mathrm{Base}}_F$$
52		eqid	$$⊢{+}_F={+}_F$$
53	45 52	grpcl	$$⊢\left(F\in \mathrm{Grp}\wedge x{\cdot }_{B}a\in {\mathrm{Base}}_F\wedge b\in {\mathrm{Base}}_F\right)\to \left(x{\cdot }_{B}a\right){+}_{F}b\in {\mathrm{Base}}_F$$
54	24 49 51 53	syl3anc	$$⊢\left(\phi \wedge \left(x\in {\mathrm{Base}}_{\mathrm{Scalar}\left(B\right)}\wedge a\in U\wedge b\in U\right)\right)\to \left(x{\cdot }_{B}a\right){+}_{F}b\in {\mathrm{Base}}_F$$
55	15 14	sraaddg	$$⊢\phi \to {+}_E={+}_B$$
56		eqid	$$⊢{+}_E={+}_E$$
57	4 56	ressplusg	$$⊢U\in \mathrm{SubRing}\left(E\right)\to {+}_E={+}_F$$
58	3 57	syl	$$⊢\phi \to {+}_E={+}_F$$
59	55 58	eqtr3d	$$⊢\phi \to {+}_B={+}_F$$
60	59	adantr	$$⊢\left(\phi \wedge \left(x\in {\mathrm{Base}}_{\mathrm{Scalar}\left(B\right)}\wedge a\in U\wedge b\in U\right)\right)\to {+}_B={+}_F$$
61	60	oveqd	$$⊢\left(\phi \wedge \left(x\in {\mathrm{Base}}_{\mathrm{Scalar}\left(B\right)}\wedge a\in U\wedge b\in U\right)\right)\to \left(x{\cdot }_{B}a\right){+}_{B}b=\left(x{\cdot }_{B}a\right){+}_{F}b$$
62	54 61 43	3eltr4d	$$⊢\left(\phi \wedge \left(x\in {\mathrm{Base}}_{\mathrm{Scalar}\left(B\right)}\wedge a\in U\wedge b\in U\right)\right)\to \left(x{\cdot }_{B}a\right){+}_{B}b\in U$$
63	6 7 8 9 10 11 17 21 62	islssd	$$⊢\phi \to U\in \mathrm{LSubSp}\left(B\right)$$