Metamath Proof Explorer

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 ⊢ ( 𝜑 → 𝐴 = ( ( subringAlg ‘ 𝑊 ) ‘ 𝑆 ) )
srapart.s ⊢ ( 𝜑 → 𝑆 ⊆ ( Base ‘ 𝑊 ) )
sralem.1 ⊢ 𝐸 = Slot 𝑁
sralem.2 ⊢ 𝑁 ∈ ℕ
sralem.3 ⊢ ( 𝑁 < 5 ∨ 8 < 𝑁 )
Assertion sralem ( 𝜑 → ( 𝐸 ‘ 𝑊 ) = ( 𝐸 ‘ 𝐴 ) )

Proof

Step Hyp Ref Expression
1 srapart.a ⊢ ( 𝜑 → 𝐴 = ( ( subringAlg ‘ 𝑊 ) ‘ 𝑆 ) )
2 srapart.s ⊢ ( 𝜑 → 𝑆 ⊆ ( Base ‘ 𝑊 ) )
3 sralem.1 ⊢ 𝐸 = Slot 𝑁
4 sralem.2 ⊢ 𝑁 ∈ ℕ
5 sralem.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 ⊢ ( 𝜑 → ( 𝐸 ‘ 𝑊 ) = ( 𝐸 ‘ 𝐴 ) )