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	1	adantl	$$⊢\left(W\in \mathrm{V}\wedge \phi \right)\to A=\mathrm{subringAlg}\left(W\right)\left(S\right)$$
7		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⟩$$
8	2 7	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⟩$$
9	6 8	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⟩$$
10	9	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)$$
11	3 4	ndxid	$$⊢E=\mathrm{Slot}E\left(\mathrm{ndx}\right)$$
12	4	nnrei	$$⊢N\in ℝ$$
13		5re	$$⊢5\in ℝ$$
14	12 13	ltnei	$$⊢N<5\to 5\ne N$$
15	14	necomd	$$⊢N<5\to N\ne 5$$
16		5lt8	$$⊢5<8$$
17		8re	$$⊢8\in ℝ$$
18	13 17 12	lttri	$$⊢\left(5<8\wedge 8<N\right)\to 5<N$$
19	16 18	mpan	$$⊢8<N\to 5<N$$
20	13 12	ltnei	$$⊢5<N\to N\ne 5$$
21	19 20	syl	$$⊢8<N\to N\ne 5$$
22	15 21	jaoi	$$⊢\left(N<5\vee 8<N\right)\to N\ne 5$$
23	5 22	ax-mp	$$⊢N\ne 5$$
24	3 4	ndxarg	$$⊢E\left(\mathrm{ndx}\right)=N$$
25		scandx	$$⊢\mathrm{Scalar}\left(\mathrm{ndx}\right)=5$$
26	24 25	neeq12i	$$⊢E\left(\mathrm{ndx}\right)\ne \mathrm{Scalar}\left(\mathrm{ndx}\right)\leftrightarrow N\ne 5$$
27	23 26	mpbir	$$⊢E\left(\mathrm{ndx}\right)\ne \mathrm{Scalar}\left(\mathrm{ndx}\right)$$
28	11 27	setsnid	$$⊢E\left(W\right)=E\left(W\mathrm{sSet}⟨\mathrm{Scalar}\left(\mathrm{ndx}\right),W{\upharpoonright }_{𝑠}S⟩\right)$$
29		5lt6	$$⊢5<6$$
30		6re	$$⊢6\in ℝ$$
31	12 13 30	lttri	$$⊢\left(N<5\wedge 5<6\right)\to N<6$$
32	29 31	mpan2	$$⊢N<5\to N<6$$
33	12 30	ltnei	$$⊢N<6\to 6\ne N$$
34	32 33	syl	$$⊢N<5\to 6\ne N$$
35	34	necomd	$$⊢N<5\to N\ne 6$$
36		6lt8	$$⊢6<8$$
37	30 17 12	lttri	$$⊢\left(6<8\wedge 8<N\right)\to 6<N$$
38	36 37	mpan	$$⊢8<N\to 6<N$$
39	30 12	ltnei	$$⊢6<N\to N\ne 6$$
40	38 39	syl	$$⊢8<N\to N\ne 6$$
41	35 40	jaoi	$$⊢\left(N<5\vee 8<N\right)\to N\ne 6$$
42	5 41	ax-mp	$$⊢N\ne 6$$
43		vscandx	$$⊢{\cdot }_{\mathrm{ndx}}=6$$
44	24 43	neeq12i	$$⊢E\left(\mathrm{ndx}\right)\ne {\cdot }_{\mathrm{ndx}}\leftrightarrow N\ne 6$$
45	42 44	mpbir	$$⊢E\left(\mathrm{ndx}\right)\ne {\cdot }_{\mathrm{ndx}}$$
46	11 45	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)$$
47	12 13 17	lttri	$$⊢\left(N<5\wedge 5<8\right)\to N<8$$
48	16 47	mpan2	$$⊢N<5\to N<8$$
49	12 17	ltnei	$$⊢N<8\to 8\ne N$$
50	48 49	syl	$$⊢N<5\to 8\ne N$$
51	50	necomd	$$⊢N<5\to N\ne 8$$
52	17 12	ltnei	$$⊢8<N\to N\ne 8$$
53	51 52	jaoi	$$⊢\left(N<5\vee 8<N\right)\to N\ne 8$$
54	5 53	ax-mp	$$⊢N\ne 8$$
55		ipndx	$$⊢{\cdot }_{𝑖}\left(\mathrm{ndx}\right)=8$$
56	24 55	neeq12i	$$⊢E\left(\mathrm{ndx}\right)\ne {\cdot }_{𝑖}\left(\mathrm{ndx}\right)\leftrightarrow N\ne 8$$
57	54 56	mpbir	$$⊢E\left(\mathrm{ndx}\right)\ne {\cdot }_{𝑖}\left(\mathrm{ndx}\right)$$
58	11 57	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)$$
59	28 46 58	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)$$
60	10 59	syl6reqr	$$⊢\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)$$