Proof of Theorem sralemOLD
| Step | Hyp | Ref
| Expression |
| 1 | | sralemOLD.1 |
. . . . . 6
⊢ 𝐸 = Slot 𝑁 |
| 2 | | sralemOLD.2 |
. . . . . 6
⊢ 𝑁 ∈ ℕ |
| 3 | 1, 2 | ndxid 17234 |
. . . . 5
⊢ 𝐸 = Slot (𝐸‘ndx) |
| 4 | | sralemOLD.3 |
. . . . . . 7
⊢ (𝑁 < 5 ∨ 8 < 𝑁) |
| 5 | 2 | nnrei 12275 |
. . . . . . . . . 10
⊢ 𝑁 ∈ ℝ |
| 6 | | 5re 12353 |
. . . . . . . . . 10
⊢ 5 ∈
ℝ |
| 7 | 5, 6 | ltnei 11385 |
. . . . . . . . 9
⊢ (𝑁 < 5 → 5 ≠ 𝑁) |
| 8 | 7 | necomd 2996 |
. . . . . . . 8
⊢ (𝑁 < 5 → 𝑁 ≠ 5) |
| 9 | | 5lt8 12460 |
. . . . . . . . . 10
⊢ 5 <
8 |
| 10 | | 8re 12362 |
. . . . . . . . . . 11
⊢ 8 ∈
ℝ |
| 11 | 6, 10, 5 | lttri 11387 |
. . . . . . . . . 10
⊢ ((5 <
8 ∧ 8 < 𝑁) → 5
< 𝑁) |
| 12 | 9, 11 | mpan 690 |
. . . . . . . . 9
⊢ (8 <
𝑁 → 5 < 𝑁) |
| 13 | 6, 5 | ltnei 11385 |
. . . . . . . . 9
⊢ (5 <
𝑁 → 𝑁 ≠ 5) |
| 14 | 12, 13 | syl 17 |
. . . . . . . 8
⊢ (8 <
𝑁 → 𝑁 ≠ 5) |
| 15 | 8, 14 | jaoi 858 |
. . . . . . 7
⊢ ((𝑁 < 5 ∨ 8 < 𝑁) → 𝑁 ≠ 5) |
| 16 | 4, 15 | ax-mp 5 |
. . . . . 6
⊢ 𝑁 ≠ 5 |
| 17 | 1, 2 | ndxarg 17233 |
. . . . . . 7
⊢ (𝐸‘ndx) = 𝑁 |
| 18 | | scandx 17358 |
. . . . . . 7
⊢
(Scalar‘ndx) = 5 |
| 19 | 17, 18 | neeq12i 3007 |
. . . . . 6
⊢ ((𝐸‘ndx) ≠
(Scalar‘ndx) ↔ 𝑁
≠ 5) |
| 20 | 16, 19 | mpbir 231 |
. . . . 5
⊢ (𝐸‘ndx) ≠
(Scalar‘ndx) |
| 21 | 3, 20 | setsnid 17245 |
. . . 4
⊢ (𝐸‘𝑊) = (𝐸‘(𝑊 sSet 〈(Scalar‘ndx), (𝑊 ↾s 𝑆)〉)) |
| 22 | | 5lt6 12447 |
. . . . . . . . . . 11
⊢ 5 <
6 |
| 23 | | 6re 12356 |
. . . . . . . . . . . 12
⊢ 6 ∈
ℝ |
| 24 | 5, 6, 23 | lttri 11387 |
. . . . . . . . . . 11
⊢ ((𝑁 < 5 ∧ 5 < 6) →
𝑁 < 6) |
| 25 | 22, 24 | mpan2 691 |
. . . . . . . . . 10
⊢ (𝑁 < 5 → 𝑁 < 6) |
| 26 | 5, 23 | ltnei 11385 |
. . . . . . . . . 10
⊢ (𝑁 < 6 → 6 ≠ 𝑁) |
| 27 | 25, 26 | syl 17 |
. . . . . . . . 9
⊢ (𝑁 < 5 → 6 ≠ 𝑁) |
| 28 | 27 | necomd 2996 |
. . . . . . . 8
⊢ (𝑁 < 5 → 𝑁 ≠ 6) |
| 29 | | 6lt8 12459 |
. . . . . . . . . 10
⊢ 6 <
8 |
| 30 | 23, 10, 5 | lttri 11387 |
. . . . . . . . . 10
⊢ ((6 <
8 ∧ 8 < 𝑁) → 6
< 𝑁) |
| 31 | 29, 30 | mpan 690 |
. . . . . . . . 9
⊢ (8 <
𝑁 → 6 < 𝑁) |
| 32 | 23, 5 | ltnei 11385 |
. . . . . . . . 9
⊢ (6 <
𝑁 → 𝑁 ≠ 6) |
| 33 | 31, 32 | syl 17 |
. . . . . . . 8
⊢ (8 <
𝑁 → 𝑁 ≠ 6) |
| 34 | 28, 33 | jaoi 858 |
. . . . . . 7
⊢ ((𝑁 < 5 ∨ 8 < 𝑁) → 𝑁 ≠ 6) |
| 35 | 4, 34 | ax-mp 5 |
. . . . . 6
⊢ 𝑁 ≠ 6 |
| 36 | | vscandx 17363 |
. . . . . . 7
⊢ (
·𝑠 ‘ndx) = 6 |
| 37 | 17, 36 | neeq12i 3007 |
. . . . . 6
⊢ ((𝐸‘ndx) ≠ (
·𝑠 ‘ndx) ↔ 𝑁 ≠ 6) |
| 38 | 35, 37 | mpbir 231 |
. . . . 5
⊢ (𝐸‘ndx) ≠ (
·𝑠 ‘ndx) |
| 39 | 3, 38 | setsnid 17245 |
. . . 4
⊢ (𝐸‘(𝑊 sSet 〈(Scalar‘ndx), (𝑊 ↾s 𝑆)〉)) = (𝐸‘((𝑊 sSet 〈(Scalar‘ndx), (𝑊 ↾s 𝑆)〉) sSet 〈(
·𝑠 ‘ndx), (.r‘𝑊)〉)) |
| 40 | 5, 6, 10 | lttri 11387 |
. . . . . . . . . . 11
⊢ ((𝑁 < 5 ∧ 5 < 8) →
𝑁 < 8) |
| 41 | 9, 40 | mpan2 691 |
. . . . . . . . . 10
⊢ (𝑁 < 5 → 𝑁 < 8) |
| 42 | 5, 10 | ltnei 11385 |
. . . . . . . . . 10
⊢ (𝑁 < 8 → 8 ≠ 𝑁) |
| 43 | 41, 42 | syl 17 |
. . . . . . . . 9
⊢ (𝑁 < 5 → 8 ≠ 𝑁) |
| 44 | 43 | necomd 2996 |
. . . . . . . 8
⊢ (𝑁 < 5 → 𝑁 ≠ 8) |
| 45 | 10, 5 | ltnei 11385 |
. . . . . . . 8
⊢ (8 <
𝑁 → 𝑁 ≠ 8) |
| 46 | 44, 45 | jaoi 858 |
. . . . . . 7
⊢ ((𝑁 < 5 ∨ 8 < 𝑁) → 𝑁 ≠ 8) |
| 47 | 4, 46 | ax-mp 5 |
. . . . . 6
⊢ 𝑁 ≠ 8 |
| 48 | | ipndx 17374 |
. . . . . . 7
⊢
(·𝑖‘ndx) = 8 |
| 49 | 17, 48 | neeq12i 3007 |
. . . . . 6
⊢ ((𝐸‘ndx) ≠
(·𝑖‘ndx) ↔ 𝑁 ≠ 8) |
| 50 | 47, 49 | mpbir 231 |
. . . . 5
⊢ (𝐸‘ndx) ≠
(·𝑖‘ndx) |
| 51 | 3, 50 | setsnid 17245 |
. . . 4
⊢ (𝐸‘((𝑊 sSet 〈(Scalar‘ndx), (𝑊 ↾s 𝑆)〉) sSet 〈(
·𝑠 ‘ndx), (.r‘𝑊)〉)) = (𝐸‘(((𝑊 sSet 〈(Scalar‘ndx), (𝑊 ↾s 𝑆)〉) sSet 〈(
·𝑠 ‘ndx), (.r‘𝑊)〉) sSet
〈(·𝑖‘ndx),
(.r‘𝑊)〉)) |
| 52 | 21, 39, 51 | 3eqtri 2769 |
. . 3
⊢ (𝐸‘𝑊) = (𝐸‘(((𝑊 sSet 〈(Scalar‘ndx), (𝑊 ↾s 𝑆)〉) sSet 〈(
·𝑠 ‘ndx), (.r‘𝑊)〉) sSet
〈(·𝑖‘ndx),
(.r‘𝑊)〉)) |
| 53 | | srapart.a |
. . . . . 6
⊢ (𝜑 → 𝐴 = ((subringAlg ‘𝑊)‘𝑆)) |
| 54 | 53 | adantl 481 |
. . . . 5
⊢ ((𝑊 ∈ V ∧ 𝜑) → 𝐴 = ((subringAlg ‘𝑊)‘𝑆)) |
| 55 | | srapart.s |
. . . . . 6
⊢ (𝜑 → 𝑆 ⊆ (Base‘𝑊)) |
| 56 | | sraval 21174 |
. . . . . 6
⊢ ((𝑊 ∈ V ∧ 𝑆 ⊆ (Base‘𝑊)) → ((subringAlg
‘𝑊)‘𝑆) = (((𝑊 sSet 〈(Scalar‘ndx), (𝑊 ↾s 𝑆)〉) sSet 〈(
·𝑠 ‘ndx), (.r‘𝑊)〉) sSet
〈(·𝑖‘ndx),
(.r‘𝑊)〉)) |
| 57 | 55, 56 | sylan2 593 |
. . . . 5
⊢ ((𝑊 ∈ V ∧ 𝜑) → ((subringAlg ‘𝑊)‘𝑆) = (((𝑊 sSet 〈(Scalar‘ndx), (𝑊 ↾s 𝑆)〉) sSet 〈(
·𝑠 ‘ndx), (.r‘𝑊)〉) sSet
〈(·𝑖‘ndx),
(.r‘𝑊)〉)) |
| 58 | 54, 57 | eqtrd 2777 |
. . . 4
⊢ ((𝑊 ∈ V ∧ 𝜑) → 𝐴 = (((𝑊 sSet 〈(Scalar‘ndx), (𝑊 ↾s 𝑆)〉) sSet 〈(
·𝑠 ‘ndx), (.r‘𝑊)〉) sSet
〈(·𝑖‘ndx),
(.r‘𝑊)〉)) |
| 59 | 58 | fveq2d 6910 |
. . 3
⊢ ((𝑊 ∈ V ∧ 𝜑) → (𝐸‘𝐴) = (𝐸‘(((𝑊 sSet 〈(Scalar‘ndx), (𝑊 ↾s 𝑆)〉) sSet 〈(
·𝑠 ‘ndx), (.r‘𝑊)〉) sSet
〈(·𝑖‘ndx),
(.r‘𝑊)〉))) |
| 60 | 52, 59 | eqtr4id 2796 |
. 2
⊢ ((𝑊 ∈ V ∧ 𝜑) → (𝐸‘𝑊) = (𝐸‘𝐴)) |
| 61 | 1 | str0 17226 |
. . 3
⊢ ∅ =
(𝐸‘∅) |
| 62 | | fvprc 6898 |
. . . 4
⊢ (¬
𝑊 ∈ V → (𝐸‘𝑊) = ∅) |
| 63 | 62 | adantr 480 |
. . 3
⊢ ((¬
𝑊 ∈ V ∧ 𝜑) → (𝐸‘𝑊) = ∅) |
| 64 | | fv2prc 6951 |
. . . . 5
⊢ (¬
𝑊 ∈ V →
((subringAlg ‘𝑊)‘𝑆) = ∅) |
| 65 | 53, 64 | sylan9eqr 2799 |
. . . 4
⊢ ((¬
𝑊 ∈ V ∧ 𝜑) → 𝐴 = ∅) |
| 66 | 65 | fveq2d 6910 |
. . 3
⊢ ((¬
𝑊 ∈ V ∧ 𝜑) → (𝐸‘𝐴) = (𝐸‘∅)) |
| 67 | 61, 63, 66 | 3eqtr4a 2803 |
. 2
⊢ ((¬
𝑊 ∈ V ∧ 𝜑) → (𝐸‘𝑊) = (𝐸‘𝐴)) |
| 68 | 60, 67 | pm2.61ian 812 |
1
⊢ (𝜑 → (𝐸‘𝑊) = (𝐸‘𝐴)) |