Theorem sralem

Description: Lemma for srabase and similar theorems. (Contributed 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$$
	sralem.1	$$⊢E=\mathrm{Slot}N$$
	sralem.2	$$⊢N\in \mathbb{N}$$
	sralem.3	$$⊢\left(N<5\vee 8<N\right)$$
Assertion	sralem	$$⊢\phi \to E\left(W\right)=E\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		sralem.1	$$⊢E=\mathrm{Slot}N$$
4		sralem.2	$$⊢N\in \mathbb{N}$$
5		sralem.3	$$⊢\left(N<5\vee 8<N\right)$$
6	3 4	ndxid	$$⊢E=\mathrm{Slot}E\left(\mathrm{ndx}\right)$$
7	4	nnrei	$$⊢N\in ℝ$$
8		5re	$$⊢5\in ℝ$$
9	7 8	ltnei	$$⊢N<5\to 5\ne N$$
10	9	necomd	$$⊢N<5\to N\ne 5$$
11		5lt8	$$⊢5<8$$
12		8re	$$⊢8\in ℝ$$
13	8 12 7	lttri	$$⊢\left(5<8\wedge 8<N\right)\to 5<N$$
14	11 13	mpan	$$⊢8<N\to 5<N$$
15	8 7	ltnei	$$⊢5<N\to N\ne 5$$
16	14 15	syl	$$⊢8<N\to N\ne 5$$
17	10 16	jaoi	$$⊢\left(N<5\vee 8<N\right)\to N\ne 5$$
18	5 17	ax-mp	$$⊢N\ne 5$$
19	3 4	ndxarg	$$⊢E\left(\mathrm{ndx}\right)=N$$
20		scandx	$$⊢\mathrm{Scalar}\left(\mathrm{ndx}\right)=5$$
21	19 20	neeq12i	$$⊢E\left(\mathrm{ndx}\right)\ne \mathrm{Scalar}\left(\mathrm{ndx}\right)\leftrightarrow N\ne 5$$
22	18 21	mpbir	$$⊢E\left(\mathrm{ndx}\right)\ne \mathrm{Scalar}\left(\mathrm{ndx}\right)$$
23	6 22	setsnid	$$⊢E\left(W\right)=E\left(W\mathrm{sSet}⟨\mathrm{Scalar}\left(\mathrm{ndx}\right),W{\upharpoonright }_{𝑠}S⟩\right)$$
24		5lt6	$$⊢5<6$$
25		6re	$$⊢6\in ℝ$$
26	7 8 25	lttri	$$⊢\left(N<5\wedge 5<6\right)\to N<6$$
27	24 26	mpan2	$$⊢N<5\to N<6$$
28	7 25	ltnei	$$⊢N<6\to 6\ne N$$
29	27 28	syl	$$⊢N<5\to 6\ne N$$
30	29	necomd	$$⊢N<5\to N\ne 6$$
31		6lt8	$$⊢6<8$$
32	25 12 7	lttri	$$⊢\left(6<8\wedge 8<N\right)\to 6<N$$
33	31 32	mpan	$$⊢8<N\to 6<N$$
34	25 7	ltnei	$$⊢6<N\to N\ne 6$$
35	33 34	syl	$$⊢8<N\to N\ne 6$$
36	30 35	jaoi	$$⊢\left(N<5\vee 8<N\right)\to N\ne 6$$
37	5 36	ax-mp	$$⊢N\ne 6$$
38		vscandx	$$⊢{\cdot }_{\mathrm{ndx}}=6$$
39	19 38	neeq12i	$$⊢E\left(\mathrm{ndx}\right)\ne {\cdot }_{\mathrm{ndx}}\leftrightarrow N\ne 6$$
40	37 39	mpbir	$$⊢E\left(\mathrm{ndx}\right)\ne {\cdot }_{\mathrm{ndx}}$$
41	6 40	setsnid	$$⊢E\left(W\mathrm{sSet}⟨\mathrm{Scalar}\left(\mathrm{ndx}\right),W{\upharpoonright }_{𝑠}S⟩\right)=E\left(\left(W\mathrm{sSet}⟨\mathrm{Scalar}\left(\mathrm{ndx}\right),W{\upharpoonright }_{𝑠}S⟩\right)\mathrm{sSet}⟨{\cdot }_{\mathrm{ndx}},{\cdot }_W⟩\right)$$
42	7 8 12	lttri	$$⊢\left(N<5\wedge 5<8\right)\to N<8$$
43	11 42	mpan2	$$⊢N<5\to N<8$$
44	7 12	ltnei	$$⊢N<8\to 8\ne N$$
45	43 44	syl	$$⊢N<5\to 8\ne N$$
46	45	necomd	$$⊢N<5\to N\ne 8$$
47	12 7	ltnei	$$⊢8<N\to N\ne 8$$
48	46 47	jaoi	$$⊢\left(N<5\vee 8<N\right)\to N\ne 8$$
49	5 48	ax-mp	$$⊢N\ne 8$$
50		ipndx	$$⊢{\cdot }_{𝑖}\left(\mathrm{ndx}\right)=8$$
51	19 50	neeq12i	$$⊢E\left(\mathrm{ndx}\right)\ne {\cdot }_{𝑖}\left(\mathrm{ndx}\right)\leftrightarrow N\ne 8$$
52	49 51	mpbir	$$⊢E\left(\mathrm{ndx}\right)\ne {\cdot }_{𝑖}\left(\mathrm{ndx}\right)$$
53	6 52	setsnid	$$⊢E\left(\left(W\mathrm{sSet}⟨\mathrm{Scalar}\left(\mathrm{ndx}\right),W{\upharpoonright }_{𝑠}S⟩\right)\mathrm{sSet}⟨{\cdot }_{\mathrm{ndx}},{\cdot }_W⟩\right)=E\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)$$
54	23 41 53	3eqtri	$$⊢E\left(W\right)=E\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)$$
55	1	adantl	$$⊢\left(W\in \mathrm{V}\wedge \phi \right)\to A=\mathrm{subringAlg}\left(W\right)\left(S\right)$$
56		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⟩$$
57	2 56	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⟩$$
58	55 57	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⟩$$
59	58	fveq2d	$$⊢\left(W\in \mathrm{V}\wedge \phi \right)\to E\left(A\right)=E\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)$$
60	54 59	eqtr4id	$$⊢\left(W\in \mathrm{V}\wedge \phi \right)\to E\left(W\right)=E\left(A\right)$$
61	3	str0	$$⊢\varnothing =E\left(\varnothing \right)$$
62		fvprc	$$⊢\neg W\in \mathrm{V}\to E\left(W\right)=\varnothing$$
63	62	adantr	$$⊢\left(\neg W\in \mathrm{V}\wedge \phi \right)\to E\left(W\right)=\varnothing$$
64		fv2prc	$$⊢\neg W\in \mathrm{V}\to \mathrm{subringAlg}\left(W\right)\left(S\right)=\varnothing$$
65	1 64	sylan9eqr	$$⊢\left(\neg W\in \mathrm{V}\wedge \phi \right)\to A=\varnothing$$
66	65	fveq2d	$$⊢\left(\neg W\in \mathrm{V}\wedge \phi \right)\to E\left(A\right)=E\left(\varnothing \right)$$
67	61 63 66	3eqtr4a	$$⊢\left(\neg W\in \mathrm{V}\wedge \phi \right)\to E\left(W\right)=E\left(A\right)$$
68	60 67	pm2.61ian	$$⊢\phi \to E\left(W\right)=E\left(A\right)$$