Proof of Theorem sralem
Step | Hyp | Ref
| Expression |
1 | | srapart.a |
. . . . . 6
⊢ (𝜑 → 𝐴 = ((subringAlg ‘𝑊)‘𝑆)) |
2 | 1 | adantl 482 |
. . . . 5
⊢ ((𝑊 ∈ V ∧ 𝜑) → 𝐴 = ((subringAlg ‘𝑊)‘𝑆)) |
3 | | srapart.s |
. . . . . 6
⊢ (𝜑 → 𝑆 ⊆ (Base‘𝑊)) |
4 | | sraval 19626 |
. . . . . 6
⊢ ((𝑊 ∈ V ∧ 𝑆 ⊆ (Base‘𝑊)) → ((subringAlg
‘𝑊)‘𝑆) = (((𝑊 sSet 〈(Scalar‘ndx), (𝑊 ↾s 𝑆)〉) sSet 〈(
·𝑠 ‘ndx), (.r‘𝑊)〉) sSet
〈(·𝑖‘ndx),
(.r‘𝑊)〉)) |
5 | 3, 4 | sylan2 592 |
. . . . 5
⊢ ((𝑊 ∈ V ∧ 𝜑) → ((subringAlg ‘𝑊)‘𝑆) = (((𝑊 sSet 〈(Scalar‘ndx), (𝑊 ↾s 𝑆)〉) sSet 〈(
·𝑠 ‘ndx), (.r‘𝑊)〉) sSet
〈(·𝑖‘ndx),
(.r‘𝑊)〉)) |
6 | 2, 5 | eqtrd 2829 |
. . . 4
⊢ ((𝑊 ∈ V ∧ 𝜑) → 𝐴 = (((𝑊 sSet 〈(Scalar‘ndx), (𝑊 ↾s 𝑆)〉) sSet 〈(
·𝑠 ‘ndx), (.r‘𝑊)〉) sSet
〈(·𝑖‘ndx),
(.r‘𝑊)〉)) |
7 | 6 | fveq2d 6534 |
. . 3
⊢ ((𝑊 ∈ V ∧ 𝜑) → (𝐸‘𝐴) = (𝐸‘(((𝑊 sSet 〈(Scalar‘ndx), (𝑊 ↾s 𝑆)〉) sSet 〈(
·𝑠 ‘ndx), (.r‘𝑊)〉) sSet
〈(·𝑖‘ndx),
(.r‘𝑊)〉))) |
8 | | sralem.1 |
. . . . . 6
⊢ 𝐸 = Slot 𝑁 |
9 | | sralem.2 |
. . . . . 6
⊢ 𝑁 ∈ ℕ |
10 | 8, 9 | ndxid 16326 |
. . . . 5
⊢ 𝐸 = Slot (𝐸‘ndx) |
11 | | sralem.3 |
. . . . . . 7
⊢ (𝑁 < 5 ∨ 8 < 𝑁) |
12 | 9 | nnrei 11484 |
. . . . . . . . . 10
⊢ 𝑁 ∈ ℝ |
13 | | 5re 11561 |
. . . . . . . . . 10
⊢ 5 ∈
ℝ |
14 | 12, 13 | ltnei 10600 |
. . . . . . . . 9
⊢ (𝑁 < 5 → 5 ≠ 𝑁) |
15 | 14 | necomd 3037 |
. . . . . . . 8
⊢ (𝑁 < 5 → 𝑁 ≠ 5) |
16 | | 5lt8 11668 |
. . . . . . . . . 10
⊢ 5 <
8 |
17 | | 8re 11570 |
. . . . . . . . . . 11
⊢ 8 ∈
ℝ |
18 | 13, 17, 12 | lttri 10602 |
. . . . . . . . . 10
⊢ ((5 <
8 ∧ 8 < 𝑁) → 5
< 𝑁) |
19 | 16, 18 | mpan 686 |
. . . . . . . . 9
⊢ (8 <
𝑁 → 5 < 𝑁) |
20 | 13, 12 | ltnei 10600 |
. . . . . . . . 9
⊢ (5 <
𝑁 → 𝑁 ≠ 5) |
21 | 19, 20 | syl 17 |
. . . . . . . 8
⊢ (8 <
𝑁 → 𝑁 ≠ 5) |
22 | 15, 21 | jaoi 852 |
. . . . . . 7
⊢ ((𝑁 < 5 ∨ 8 < 𝑁) → 𝑁 ≠ 5) |
23 | 11, 22 | ax-mp 5 |
. . . . . 6
⊢ 𝑁 ≠ 5 |
24 | 8, 9 | ndxarg 16325 |
. . . . . . 7
⊢ (𝐸‘ndx) = 𝑁 |
25 | | scandx 16449 |
. . . . . . 7
⊢
(Scalar‘ndx) = 5 |
26 | 24, 25 | neeq12i 3048 |
. . . . . 6
⊢ ((𝐸‘ndx) ≠
(Scalar‘ndx) ↔ 𝑁
≠ 5) |
27 | 23, 26 | mpbir 232 |
. . . . 5
⊢ (𝐸‘ndx) ≠
(Scalar‘ndx) |
28 | 10, 27 | setsnid 16356 |
. . . 4
⊢ (𝐸‘𝑊) = (𝐸‘(𝑊 sSet 〈(Scalar‘ndx), (𝑊 ↾s 𝑆)〉)) |
29 | | 5lt6 11655 |
. . . . . . . . . . 11
⊢ 5 <
6 |
30 | | 6re 11564 |
. . . . . . . . . . . 12
⊢ 6 ∈
ℝ |
31 | 12, 13, 30 | lttri 10602 |
. . . . . . . . . . 11
⊢ ((𝑁 < 5 ∧ 5 < 6) →
𝑁 < 6) |
32 | 29, 31 | mpan2 687 |
. . . . . . . . . 10
⊢ (𝑁 < 5 → 𝑁 < 6) |
33 | 12, 30 | ltnei 10600 |
. . . . . . . . . 10
⊢ (𝑁 < 6 → 6 ≠ 𝑁) |
34 | 32, 33 | syl 17 |
. . . . . . . . 9
⊢ (𝑁 < 5 → 6 ≠ 𝑁) |
35 | 34 | necomd 3037 |
. . . . . . . 8
⊢ (𝑁 < 5 → 𝑁 ≠ 6) |
36 | | 6lt8 11667 |
. . . . . . . . . 10
⊢ 6 <
8 |
37 | 30, 17, 12 | lttri 10602 |
. . . . . . . . . 10
⊢ ((6 <
8 ∧ 8 < 𝑁) → 6
< 𝑁) |
38 | 36, 37 | mpan 686 |
. . . . . . . . 9
⊢ (8 <
𝑁 → 6 < 𝑁) |
39 | 30, 12 | ltnei 10600 |
. . . . . . . . 9
⊢ (6 <
𝑁 → 𝑁 ≠ 6) |
40 | 38, 39 | syl 17 |
. . . . . . . 8
⊢ (8 <
𝑁 → 𝑁 ≠ 6) |
41 | 35, 40 | jaoi 852 |
. . . . . . 7
⊢ ((𝑁 < 5 ∨ 8 < 𝑁) → 𝑁 ≠ 6) |
42 | 11, 41 | ax-mp 5 |
. . . . . 6
⊢ 𝑁 ≠ 6 |
43 | | vscandx 16451 |
. . . . . . 7
⊢ (
·𝑠 ‘ndx) = 6 |
44 | 24, 43 | neeq12i 3048 |
. . . . . 6
⊢ ((𝐸‘ndx) ≠ (
·𝑠 ‘ndx) ↔ 𝑁 ≠ 6) |
45 | 42, 44 | mpbir 232 |
. . . . 5
⊢ (𝐸‘ndx) ≠ (
·𝑠 ‘ndx) |
46 | 10, 45 | setsnid 16356 |
. . . 4
⊢ (𝐸‘(𝑊 sSet 〈(Scalar‘ndx), (𝑊 ↾s 𝑆)〉)) = (𝐸‘((𝑊 sSet 〈(Scalar‘ndx), (𝑊 ↾s 𝑆)〉) sSet 〈(
·𝑠 ‘ndx), (.r‘𝑊)〉)) |
47 | 12, 13, 17 | lttri 10602 |
. . . . . . . . . . 11
⊢ ((𝑁 < 5 ∧ 5 < 8) →
𝑁 < 8) |
48 | 16, 47 | mpan2 687 |
. . . . . . . . . 10
⊢ (𝑁 < 5 → 𝑁 < 8) |
49 | 12, 17 | ltnei 10600 |
. . . . . . . . . 10
⊢ (𝑁 < 8 → 8 ≠ 𝑁) |
50 | 48, 49 | syl 17 |
. . . . . . . . 9
⊢ (𝑁 < 5 → 8 ≠ 𝑁) |
51 | 50 | necomd 3037 |
. . . . . . . 8
⊢ (𝑁 < 5 → 𝑁 ≠ 8) |
52 | 17, 12 | ltnei 10600 |
. . . . . . . 8
⊢ (8 <
𝑁 → 𝑁 ≠ 8) |
53 | 51, 52 | jaoi 852 |
. . . . . . 7
⊢ ((𝑁 < 5 ∨ 8 < 𝑁) → 𝑁 ≠ 8) |
54 | 11, 53 | ax-mp 5 |
. . . . . 6
⊢ 𝑁 ≠ 8 |
55 | | ipndx 16458 |
. . . . . . 7
⊢
(·𝑖‘ndx) = 8 |
56 | 24, 55 | neeq12i 3048 |
. . . . . 6
⊢ ((𝐸‘ndx) ≠
(·𝑖‘ndx) ↔ 𝑁 ≠ 8) |
57 | 54, 56 | mpbir 232 |
. . . . 5
⊢ (𝐸‘ndx) ≠
(·𝑖‘ndx) |
58 | 10, 57 | setsnid 16356 |
. . . 4
⊢ (𝐸‘((𝑊 sSet 〈(Scalar‘ndx), (𝑊 ↾s 𝑆)〉) sSet 〈(
·𝑠 ‘ndx), (.r‘𝑊)〉)) = (𝐸‘(((𝑊 sSet 〈(Scalar‘ndx), (𝑊 ↾s 𝑆)〉) sSet 〈(
·𝑠 ‘ndx), (.r‘𝑊)〉) sSet
〈(·𝑖‘ndx),
(.r‘𝑊)〉)) |
59 | 28, 46, 58 | 3eqtri 2821 |
. . 3
⊢ (𝐸‘𝑊) = (𝐸‘(((𝑊 sSet 〈(Scalar‘ndx), (𝑊 ↾s 𝑆)〉) sSet 〈(
·𝑠 ‘ndx), (.r‘𝑊)〉) sSet
〈(·𝑖‘ndx),
(.r‘𝑊)〉)) |
60 | 7, 59 | syl6reqr 2848 |
. 2
⊢ ((𝑊 ∈ V ∧ 𝜑) → (𝐸‘𝑊) = (𝐸‘𝐴)) |
61 | 8 | str0 16352 |
. . 3
⊢ ∅ =
(𝐸‘∅) |
62 | | fvprc 6523 |
. . . 4
⊢ (¬
𝑊 ∈ V → (𝐸‘𝑊) = ∅) |
63 | 62 | adantr 481 |
. . 3
⊢ ((¬
𝑊 ∈ V ∧ 𝜑) → (𝐸‘𝑊) = ∅) |
64 | | fv2prc 6570 |
. . . . 5
⊢ (¬
𝑊 ∈ V →
((subringAlg ‘𝑊)‘𝑆) = ∅) |
65 | 1, 64 | sylan9eqr 2851 |
. . . 4
⊢ ((¬
𝑊 ∈ V ∧ 𝜑) → 𝐴 = ∅) |
66 | 65 | fveq2d 6534 |
. . 3
⊢ ((¬
𝑊 ∈ V ∧ 𝜑) → (𝐸‘𝐴) = (𝐸‘∅)) |
67 | 61, 63, 66 | 3eqtr4a 2855 |
. 2
⊢ ((¬
𝑊 ∈ V ∧ 𝜑) → (𝐸‘𝑊) = (𝐸‘𝐴)) |
68 | 60, 67 | pm2.61ian 808 |
1
⊢ (𝜑 → (𝐸‘𝑊) = (𝐸‘𝐴)) |