Theorem sralemOLD

Description: Obsolete version of sralem as of 29-Oct-2024. Lemma for srabase and similar theorems. (Contributed by Mario Carneiro, 4-Oct-2015) (Revised by Thierry Arnoux, 16-Jun-2019) (Proof modification is discouraged.) (New usage is discouraged.)

	Ref	Expression
Hypotheses	srapart.a	⊢ ( 𝜑 → 𝐴 = ( ( subringAlg ‘ 𝑊 ) ‘ 𝑆 ) )
	srapart.s	⊢ ( 𝜑 → 𝑆 ⊆ ( Base ‘ 𝑊 ) )
	sralemOLD.1	⊢ 𝐸 = Slot 𝑁
	sralemOLD.2	⊢ 𝑁 ∈ ℕ
	sralemOLD.3	⊢ ( 𝑁 < 5 ∨ 8 < 𝑁 )
Assertion	sralemOLD	⊢ ( 𝜑 → ( 𝐸 ‘ 𝑊 ) = ( 𝐸 ‘ 𝐴 ) )

Proof

Step	Hyp	Ref	Expression
1		srapart.a	⊢ ( 𝜑 → 𝐴 = ( ( subringAlg ‘ 𝑊 ) ‘ 𝑆 ) )
2		srapart.s	⊢ ( 𝜑 → 𝑆 ⊆ ( Base ‘ 𝑊 ) )
3		sralemOLD.1	⊢ 𝐸 = Slot 𝑁
4		sralemOLD.2	⊢ 𝑁 ∈ ℕ
5		sralemOLD.3	⊢ ( 𝑁 < 5 ∨ 8 < 𝑁 )
6	3 4	ndxid	⊢ 𝐸 = Slot ( 𝐸 ‘ ndx )
7	4	nnrei	⊢ 𝑁 ∈ ℝ
8		5re	⊢ 5 ∈ ℝ
9	7 8	ltnei	⊢ ( 𝑁 < 5 → 5 ≠ 𝑁 )
10	9	necomd	⊢ ( 𝑁 < 5 → 𝑁 ≠ 5 )
11		5lt8	⊢ 5 < 8
12		8re	⊢ 8 ∈ ℝ
13	8 12 7	lttri	⊢ ( ( 5 < 8 ∧ 8 < 𝑁 ) → 5 < 𝑁 )
14	11 13	mpan	⊢ ( 8 < 𝑁 → 5 < 𝑁 )
15	8 7	ltnei	⊢ ( 5 < 𝑁 → 𝑁 ≠ 5 )
16	14 15	syl	⊢ ( 8 < 𝑁 → 𝑁 ≠ 5 )
17	10 16	jaoi	⊢ ( ( 𝑁 < 5 ∨ 8 < 𝑁 ) → 𝑁 ≠ 5 )
18	5 17	ax-mp	⊢ 𝑁 ≠ 5
19	3 4	ndxarg	⊢ ( 𝐸 ‘ ndx ) = 𝑁
20		scandx	⊢ ( Scalar ‘ ndx ) = 5
21	19 20	neeq12i	⊢ ( ( 𝐸 ‘ ndx ) ≠ ( Scalar ‘ ndx ) ↔ 𝑁 ≠ 5 )
22	18 21	mpbir	⊢ ( 𝐸 ‘ ndx ) ≠ ( Scalar ‘ ndx )
23	6 22	setsnid	⊢ ( 𝐸 ‘ 𝑊 ) = ( 𝐸 ‘ ( 𝑊 sSet ⟨ ( Scalar ‘ ndx ) , ( 𝑊 ↾s 𝑆 ) ⟩ ) )
24		5lt6	⊢ 5 < 6
25		6re	⊢ 6 ∈ ℝ
26	7 8 25	lttri	⊢ ( ( 𝑁 < 5 ∧ 5 < 6 ) → 𝑁 < 6 )
27	24 26	mpan2	⊢ ( 𝑁 < 5 → 𝑁 < 6 )
28	7 25	ltnei	⊢ ( 𝑁 < 6 → 6 ≠ 𝑁 )
29	27 28	syl	⊢ ( 𝑁 < 5 → 6 ≠ 𝑁 )
30	29	necomd	⊢ ( 𝑁 < 5 → 𝑁 ≠ 6 )
31		6lt8	⊢ 6 < 8
32	25 12 7	lttri	⊢ ( ( 6 < 8 ∧ 8 < 𝑁 ) → 6 < 𝑁 )
33	31 32	mpan	⊢ ( 8 < 𝑁 → 6 < 𝑁 )
34	25 7	ltnei	⊢ ( 6 < 𝑁 → 𝑁 ≠ 6 )
35	33 34	syl	⊢ ( 8 < 𝑁 → 𝑁 ≠ 6 )
36	30 35	jaoi	⊢ ( ( 𝑁 < 5 ∨ 8 < 𝑁 ) → 𝑁 ≠ 6 )
37	5 36	ax-mp	⊢ 𝑁 ≠ 6
38		vscandx	⊢ ( ·𝑠 ‘ ndx ) = 6
39	19 38	neeq12i	⊢ ( ( 𝐸 ‘ ndx ) ≠ ( ·𝑠 ‘ ndx ) ↔ 𝑁 ≠ 6 )
40	37 39	mpbir	⊢ ( 𝐸 ‘ ndx ) ≠ ( ·𝑠 ‘ ndx )
41	6 40	setsnid	⊢ ( 𝐸 ‘ ( 𝑊 sSet ⟨ ( Scalar ‘ ndx ) , ( 𝑊 ↾s 𝑆 ) ⟩ ) ) = ( 𝐸 ‘ ( ( 𝑊 sSet ⟨ ( Scalar ‘ ndx ) , ( 𝑊 ↾s 𝑆 ) ⟩ ) sSet ⟨ ( ·𝑠 ‘ ndx ) , ( .r ‘ 𝑊 ) ⟩ ) )
42	7 8 12	lttri	⊢ ( ( 𝑁 < 5 ∧ 5 < 8 ) → 𝑁 < 8 )
43	11 42	mpan2	⊢ ( 𝑁 < 5 → 𝑁 < 8 )
44	7 12	ltnei	⊢ ( 𝑁 < 8 → 8 ≠ 𝑁 )
45	43 44	syl	⊢ ( 𝑁 < 5 → 8 ≠ 𝑁 )
46	45	necomd	⊢ ( 𝑁 < 5 → 𝑁 ≠ 8 )
47	12 7	ltnei	⊢ ( 8 < 𝑁 → 𝑁 ≠ 8 )
48	46 47	jaoi	⊢ ( ( 𝑁 < 5 ∨ 8 < 𝑁 ) → 𝑁 ≠ 8 )
49	5 48	ax-mp	⊢ 𝑁 ≠ 8
50		ipndx	⊢ ( ·𝑖 ‘ ndx ) = 8
51	19 50	neeq12i	⊢ ( ( 𝐸 ‘ ndx ) ≠ ( ·𝑖 ‘ ndx ) ↔ 𝑁 ≠ 8 )
52	49 51	mpbir	⊢ ( 𝐸 ‘ ndx ) ≠ ( ·𝑖 ‘ ndx )
53	6 52	setsnid	⊢ ( 𝐸 ‘ ( ( 𝑊 sSet ⟨ ( Scalar ‘ ndx ) , ( 𝑊 ↾s 𝑆 ) ⟩ ) sSet ⟨ ( ·𝑠 ‘ ndx ) , ( .r ‘ 𝑊 ) ⟩ ) ) = ( 𝐸 ‘ ( ( ( 𝑊 sSet ⟨ ( Scalar ‘ ndx ) , ( 𝑊 ↾s 𝑆 ) ⟩ ) sSet ⟨ ( ·𝑠 ‘ ndx ) , ( .r ‘ 𝑊 ) ⟩ ) sSet ⟨ ( ·𝑖 ‘ ndx ) , ( .r ‘ 𝑊 ) ⟩ ) )
54	23 41 53	3eqtri	⊢ ( 𝐸 ‘ 𝑊 ) = ( 𝐸 ‘ ( ( ( 𝑊 sSet ⟨ ( Scalar ‘ ndx ) , ( 𝑊 ↾s 𝑆 ) ⟩ ) sSet ⟨ ( ·𝑠 ‘ ndx ) , ( .r ‘ 𝑊 ) ⟩ ) sSet ⟨ ( ·𝑖 ‘ ndx ) , ( .r ‘ 𝑊 ) ⟩ ) )
55	1	adantl	⊢ ( ( 𝑊 ∈ V ∧ 𝜑 ) → 𝐴 = ( ( subringAlg ‘ 𝑊 ) ‘ 𝑆 ) )
56		sraval	⊢ ( ( 𝑊 ∈ V ∧ 𝑆 ⊆ ( Base ‘ 𝑊 ) ) → ( ( subringAlg ‘ 𝑊 ) ‘ 𝑆 ) = ( ( ( 𝑊 sSet ⟨ ( Scalar ‘ ndx ) , ( 𝑊 ↾s 𝑆 ) ⟩ ) sSet ⟨ ( ·𝑠 ‘ ndx ) , ( .r ‘ 𝑊 ) ⟩ ) sSet ⟨ ( ·𝑖 ‘ ndx ) , ( .r ‘ 𝑊 ) ⟩ ) )
57	2 56	sylan2	⊢ ( ( 𝑊 ∈ V ∧ 𝜑 ) → ( ( subringAlg ‘ 𝑊 ) ‘ 𝑆 ) = ( ( ( 𝑊 sSet ⟨ ( Scalar ‘ ndx ) , ( 𝑊 ↾s 𝑆 ) ⟩ ) sSet ⟨ ( ·𝑠 ‘ ndx ) , ( .r ‘ 𝑊 ) ⟩ ) sSet ⟨ ( ·𝑖 ‘ ndx ) , ( .r ‘ 𝑊 ) ⟩ ) )
58	55 57	eqtrd	⊢ ( ( 𝑊 ∈ V ∧ 𝜑 ) → 𝐴 = ( ( ( 𝑊 sSet ⟨ ( Scalar ‘ ndx ) , ( 𝑊 ↾s 𝑆 ) ⟩ ) sSet ⟨ ( ·𝑠 ‘ ndx ) , ( .r ‘ 𝑊 ) ⟩ ) sSet ⟨ ( ·𝑖 ‘ ndx ) , ( .r ‘ 𝑊 ) ⟩ ) )
59	58	fveq2d	⊢ ( ( 𝑊 ∈ V ∧ 𝜑 ) → ( 𝐸 ‘ 𝐴 ) = ( 𝐸 ‘ ( ( ( 𝑊 sSet ⟨ ( Scalar ‘ ndx ) , ( 𝑊 ↾s 𝑆 ) ⟩ ) sSet ⟨ ( ·𝑠 ‘ ndx ) , ( .r ‘ 𝑊 ) ⟩ ) sSet ⟨ ( ·𝑖 ‘ ndx ) , ( .r ‘ 𝑊 ) ⟩ ) ) )
60	54 59	eqtr4id	⊢ ( ( 𝑊 ∈ V ∧ 𝜑 ) → ( 𝐸 ‘ 𝑊 ) = ( 𝐸 ‘ 𝐴 ) )
61	3	str0	⊢ ∅ = ( 𝐸 ‘ ∅ )
62		fvprc	⊢ ( ¬ 𝑊 ∈ V → ( 𝐸 ‘ 𝑊 ) = ∅ )
63	62	adantr	⊢ ( ( ¬ 𝑊 ∈ V ∧ 𝜑 ) → ( 𝐸 ‘ 𝑊 ) = ∅ )
64		fv2prc	⊢ ( ¬ 𝑊 ∈ V → ( ( subringAlg ‘ 𝑊 ) ‘ 𝑆 ) = ∅ )
65	1 64	sylan9eqr	⊢ ( ( ¬ 𝑊 ∈ V ∧ 𝜑 ) → 𝐴 = ∅ )
66	65	fveq2d	⊢ ( ( ¬ 𝑊 ∈ V ∧ 𝜑 ) → ( 𝐸 ‘ 𝐴 ) = ( 𝐸 ‘ ∅ ) )
67	61 63 66	3eqtr4a	⊢ ( ( ¬ 𝑊 ∈ V ∧ 𝜑 ) → ( 𝐸 ‘ 𝑊 ) = ( 𝐸 ‘ 𝐴 ) )
68	60 67	pm2.61ian	⊢ ( 𝜑 → ( 𝐸 ‘ 𝑊 ) = ( 𝐸 ‘ 𝐴 ) )