Theorem ressascl

Description: The lifting of scalars is invariant between subalgebras and superalgebras. (Contributed by Mario Carneiro, 9-Mar-2015)

	Ref	Expression
Hypotheses	ressascl.a	$$⊢A=\mathrm{algSc}\left(W\right)$$
	ressascl.x	$$⊢X=W{\upharpoonright }_{𝑠}S$$
Assertion	ressascl	$$⊢S\in \mathrm{SubRing}\left(W\right)\to A=\mathrm{algSc}\left(X\right)$$

Proof

Step	Hyp	Ref	Expression
1		ressascl.a	$$⊢A=\mathrm{algSc}\left(W\right)$$
2		ressascl.x	$$⊢X=W{\upharpoonright }_{𝑠}S$$
3		eqid	$$⊢\mathrm{Scalar}\left(W\right)=\mathrm{Scalar}\left(W\right)$$
4	2 3	resssca	$$⊢S\in \mathrm{SubRing}\left(W\right)\to \mathrm{Scalar}\left(W\right)=\mathrm{Scalar}\left(X\right)$$
5	4	fveq2d	$$⊢S\in \mathrm{SubRing}\left(W\right)\to {\mathrm{Base}}_{\mathrm{Scalar}\left(W\right)}={\mathrm{Base}}_{\mathrm{Scalar}\left(X\right)}$$
6		eqid	$$⊢{\cdot }_W={\cdot }_W$$
7	2 6	ressvsca	$$⊢S\in \mathrm{SubRing}\left(W\right)\to {\cdot }_W={\cdot }_X$$
8		eqidd	$$⊢S\in \mathrm{SubRing}\left(W\right)\to x=x$$
9		eqid	$$⊢1_W=1_W$$
10	2 9	subrg1	$$⊢S\in \mathrm{SubRing}\left(W\right)\to 1_W=1_X$$
11	7 8 10	oveq123d	$$⊢S\in \mathrm{SubRing}\left(W\right)\to x{\cdot }_W{1}_W=x{\cdot }_X{1}_X$$
12	5 11	mpteq12dv	$$⊢S\in \mathrm{SubRing}\left(W\right)\to \left(x\in {\mathrm{Base}}_{\mathrm{Scalar}\left(W\right)}⟼x{\cdot }_W{1}_W\right)=\left(x\in {\mathrm{Base}}_{\mathrm{Scalar}\left(X\right)}⟼x{\cdot }_X{1}_X\right)$$
13		eqid	$$⊢{\mathrm{Base}}_{\mathrm{Scalar}\left(W\right)}={\mathrm{Base}}_{\mathrm{Scalar}\left(W\right)}$$
14	1 3 13 6 9	asclfval	$$⊢A=\left(x\in {\mathrm{Base}}_{\mathrm{Scalar}\left(W\right)}⟼x{\cdot }_W{1}_W\right)$$
15		eqid	$$⊢\mathrm{algSc}\left(X\right)=\mathrm{algSc}\left(X\right)$$
16		eqid	$$⊢\mathrm{Scalar}\left(X\right)=\mathrm{Scalar}\left(X\right)$$
17		eqid	$$⊢{\mathrm{Base}}_{\mathrm{Scalar}\left(X\right)}={\mathrm{Base}}_{\mathrm{Scalar}\left(X\right)}$$
18		eqid	$$⊢{\cdot }_X={\cdot }_X$$
19		eqid	$$⊢1_X=1_X$$
20	15 16 17 18 19	asclfval	$$⊢\mathrm{algSc}\left(X\right)=\left(x\in {\mathrm{Base}}_{\mathrm{Scalar}\left(X\right)}⟼x{\cdot }_X{1}_X\right)$$
21	12 14 20	3eqtr4g	$$⊢S\in \mathrm{SubRing}\left(W\right)\to A=\mathrm{algSc}\left(X\right)$$