Theorem srasca

Description: The set of scalars of a subring algebra. (Contributed by Stefan O'Rear, 27-Nov-2014) (Revised by Mario Carneiro, 4-Oct-2015) (Revised by Thierry Arnoux, 16-Jun-2019)

	Ref	Expression
Hypotheses	srapart.a	$$⊢\phi \to A=\mathrm{subringAlg}\left(W\right)\left(S\right)$$
	srapart.s	$$⊢\phi \to S\subseteq {\mathrm{Base}}_W$$
Assertion	srasca	$$⊢\phi \to W{\upharpoonright }_{𝑠}S=\mathrm{Scalar}\left(A\right)$$

Proof

Step	Hyp	Ref	Expression
1		srapart.a	$$⊢\phi \to A=\mathrm{subringAlg}\left(W\right)\left(S\right)$$
2		srapart.s	$$⊢\phi \to S\subseteq {\mathrm{Base}}_W$$
3		scaid	$$⊢\mathrm{Scalar}=\mathrm{Slot}\mathrm{Scalar}\left(\mathrm{ndx}\right)$$
4		5re	$$⊢5\in ℝ$$
5		5lt6	$$⊢5<6$$
6	4 5	ltneii	$$⊢5\ne 6$$
7		scandx	$$⊢\mathrm{Scalar}\left(\mathrm{ndx}\right)=5$$
8		vscandx	$$⊢{\cdot }_{\mathrm{ndx}}=6$$
9	7 8	neeq12i	$$⊢\mathrm{Scalar}\left(\mathrm{ndx}\right)\ne {\cdot }_{\mathrm{ndx}}\leftrightarrow 5\ne 6$$
10	6 9	mpbir	$$⊢\mathrm{Scalar}\left(\mathrm{ndx}\right)\ne {\cdot }_{\mathrm{ndx}}$$
11	3 10	setsnid	$$⊢\mathrm{Scalar}\left(W\mathrm{sSet}⟨\mathrm{Scalar}\left(\mathrm{ndx}\right),W{\upharpoonright }_{𝑠}S⟩\right)=\mathrm{Scalar}\left(\left(W\mathrm{sSet}⟨\mathrm{Scalar}\left(\mathrm{ndx}\right),W{\upharpoonright }_{𝑠}S⟩\right)\mathrm{sSet}⟨{\cdot }_{\mathrm{ndx}},{\cdot }_W⟩\right)$$
12		5lt8	$$⊢5<8$$
13	4 12	ltneii	$$⊢5\ne 8$$
14		ipndx	$$⊢{\cdot }_{𝑖}\left(\mathrm{ndx}\right)=8$$
15	7 14	neeq12i	$$⊢\mathrm{Scalar}\left(\mathrm{ndx}\right)\ne {\cdot }_{𝑖}\left(\mathrm{ndx}\right)\leftrightarrow 5\ne 8$$
16	13 15	mpbir	$$⊢\mathrm{Scalar}\left(\mathrm{ndx}\right)\ne {\cdot }_{𝑖}\left(\mathrm{ndx}\right)$$
17	3 16	setsnid	$$⊢\mathrm{Scalar}\left(\left(W\mathrm{sSet}⟨\mathrm{Scalar}\left(\mathrm{ndx}\right),W{\upharpoonright }_{𝑠}S⟩\right)\mathrm{sSet}⟨{\cdot }_{\mathrm{ndx}},{\cdot }_W⟩\right)=\mathrm{Scalar}\left(\left(\left(W\mathrm{sSet}⟨\mathrm{Scalar}\left(\mathrm{ndx}\right),W{\upharpoonright }_{𝑠}S⟩\right)\mathrm{sSet}⟨{\cdot }_{\mathrm{ndx}},{\cdot }_W⟩\right)\mathrm{sSet}⟨{\cdot }_{𝑖}\left(\mathrm{ndx}\right),{\cdot }_W⟩\right)$$
18	11 17	eqtri	$$⊢\mathrm{Scalar}\left(W\mathrm{sSet}⟨\mathrm{Scalar}\left(\mathrm{ndx}\right),W{\upharpoonright }_{𝑠}S⟩\right)=\mathrm{Scalar}\left(\left(\left(W\mathrm{sSet}⟨\mathrm{Scalar}\left(\mathrm{ndx}\right),W{\upharpoonright }_{𝑠}S⟩\right)\mathrm{sSet}⟨{\cdot }_{\mathrm{ndx}},{\cdot }_W⟩\right)\mathrm{sSet}⟨{\cdot }_{𝑖}\left(\mathrm{ndx}\right),{\cdot }_W⟩\right)$$
19		ovexd	$$⊢\phi \to W{\upharpoonright }_{𝑠}S\in \mathrm{V}$$
20	3	setsid	$$⊢\left(W\in \mathrm{V}\wedge W{\upharpoonright }_{𝑠}S\in \mathrm{V}\right)\to W{\upharpoonright }_{𝑠}S=\mathrm{Scalar}\left(W\mathrm{sSet}⟨\mathrm{Scalar}\left(\mathrm{ndx}\right),W{\upharpoonright }_{𝑠}S⟩\right)$$
21	19 20	sylan2	$$⊢\left(W\in \mathrm{V}\wedge \phi \right)\to W{\upharpoonright }_{𝑠}S=\mathrm{Scalar}\left(W\mathrm{sSet}⟨\mathrm{Scalar}\left(\mathrm{ndx}\right),W{\upharpoonright }_{𝑠}S⟩\right)$$
22	1	adantl	$$⊢\left(W\in \mathrm{V}\wedge \phi \right)\to A=\mathrm{subringAlg}\left(W\right)\left(S\right)$$
23		sraval	$$⊢\left(W\in \mathrm{V}\wedge S\subseteq {\mathrm{Base}}_W\right)\to \mathrm{subringAlg}\left(W\right)\left(S\right)=\left(\left(W\mathrm{sSet}⟨\mathrm{Scalar}\left(\mathrm{ndx}\right),W{\upharpoonright }_{𝑠}S⟩\right)\mathrm{sSet}⟨{\cdot }_{\mathrm{ndx}},{\cdot }_W⟩\right)\mathrm{sSet}⟨{\cdot }_{𝑖}\left(\mathrm{ndx}\right),{\cdot }_W⟩$$
24	2 23	sylan2	$$⊢\left(W\in \mathrm{V}\wedge \phi \right)\to \mathrm{subringAlg}\left(W\right)\left(S\right)=\left(\left(W\mathrm{sSet}⟨\mathrm{Scalar}\left(\mathrm{ndx}\right),W{\upharpoonright }_{𝑠}S⟩\right)\mathrm{sSet}⟨{\cdot }_{\mathrm{ndx}},{\cdot }_W⟩\right)\mathrm{sSet}⟨{\cdot }_{𝑖}\left(\mathrm{ndx}\right),{\cdot }_W⟩$$
25	22 24	eqtrd	$$⊢\left(W\in \mathrm{V}\wedge \phi \right)\to A=\left(\left(W\mathrm{sSet}⟨\mathrm{Scalar}\left(\mathrm{ndx}\right),W{\upharpoonright }_{𝑠}S⟩\right)\mathrm{sSet}⟨{\cdot }_{\mathrm{ndx}},{\cdot }_W⟩\right)\mathrm{sSet}⟨{\cdot }_{𝑖}\left(\mathrm{ndx}\right),{\cdot }_W⟩$$
26	25	fveq2d	$$⊢\left(W\in \mathrm{V}\wedge \phi \right)\to \mathrm{Scalar}\left(A\right)=\mathrm{Scalar}\left(\left(\left(W\mathrm{sSet}⟨\mathrm{Scalar}\left(\mathrm{ndx}\right),W{\upharpoonright }_{𝑠}S⟩\right)\mathrm{sSet}⟨{\cdot }_{\mathrm{ndx}},{\cdot }_W⟩\right)\mathrm{sSet}⟨{\cdot }_{𝑖}\left(\mathrm{ndx}\right),{\cdot }_W⟩\right)$$
27	18 21 26	3eqtr4a	$$⊢\left(W\in \mathrm{V}\wedge \phi \right)\to W{\upharpoonright }_{𝑠}S=\mathrm{Scalar}\left(A\right)$$
28	3	str0	$$⊢\varnothing =\mathrm{Scalar}\left(\varnothing \right)$$
29		reldmress	$$⊢\mathrm{Rel}\mathrm{dom}{\upharpoonright }_{𝑠}$$
30	29	ovprc1	$$⊢\neg W\in \mathrm{V}\to W{\upharpoonright }_{𝑠}S=\varnothing$$
31	30	adantr	$$⊢\left(\neg W\in \mathrm{V}\wedge \phi \right)\to W{\upharpoonright }_{𝑠}S=\varnothing$$
32		fv2prc	$$⊢\neg W\in \mathrm{V}\to \mathrm{subringAlg}\left(W\right)\left(S\right)=\varnothing$$
33	1 32	sylan9eqr	$$⊢\left(\neg W\in \mathrm{V}\wedge \phi \right)\to A=\varnothing$$
34	33	fveq2d	$$⊢\left(\neg W\in \mathrm{V}\wedge \phi \right)\to \mathrm{Scalar}\left(A\right)=\mathrm{Scalar}\left(\varnothing \right)$$
35	28 31 34	3eqtr4a	$$⊢\left(\neg W\in \mathrm{V}\wedge \phi \right)\to W{\upharpoonright }_{𝑠}S=\mathrm{Scalar}\left(A\right)$$
36	27 35	pm2.61ian	$$⊢\phi \to W{\upharpoonright }_{𝑠}S=\mathrm{Scalar}\left(A\right)$$