Proof of Theorem srasca
Step | Hyp | Ref
| Expression |
1 | | scaid 15837 |
. . . . 5
⊢ Scalar =
Slot (Scalar‘ndx) |
2 | | 5re 10976 |
. . . . . . 7
⊢ 5 ∈
ℝ |
3 | | 5lt6 11081 |
. . . . . . 7
⊢ 5 <
6 |
4 | 2, 3 | ltneii 10029 |
. . . . . 6
⊢ 5 ≠
6 |
5 | | scandx 15836 |
. . . . . . 7
⊢
(Scalar‘ndx) = 5 |
6 | | vscandx 15838 |
. . . . . . 7
⊢ (
·𝑠 ‘ndx) = 6 |
7 | 5, 6 | neeq12i 2848 |
. . . . . 6
⊢
((Scalar‘ndx) ≠ ( ·𝑠
‘ndx) ↔ 5 ≠ 6) |
8 | 4, 7 | mpbir 220 |
. . . . 5
⊢
(Scalar‘ndx) ≠ ( ·𝑠
‘ndx) |
9 | 1, 8 | setsnid 15743 |
. . . 4
⊢
(Scalar‘(𝑊
sSet 〈(Scalar‘ndx), (𝑊 ↾s 𝑆)〉)) = (Scalar‘((𝑊 sSet 〈(Scalar‘ndx),
(𝑊 ↾s
𝑆)〉) sSet 〈(
·𝑠 ‘ndx), (.r‘𝑊)〉)) |
10 | | 5lt8 11094 |
. . . . . . 7
⊢ 5 <
8 |
11 | 2, 10 | ltneii 10029 |
. . . . . 6
⊢ 5 ≠
8 |
12 | | ipndx 15845 |
. . . . . . 7
⊢
(·𝑖‘ndx) = 8 |
13 | 5, 12 | neeq12i 2848 |
. . . . . 6
⊢
((Scalar‘ndx) ≠ (·𝑖‘ndx)
↔ 5 ≠ 8) |
14 | 11, 13 | mpbir 220 |
. . . . 5
⊢
(Scalar‘ndx) ≠
(·𝑖‘ndx) |
15 | 1, 14 | setsnid 15743 |
. . . 4
⊢
(Scalar‘((𝑊
sSet 〈(Scalar‘ndx), (𝑊 ↾s 𝑆)〉) sSet 〈(
·𝑠 ‘ndx), (.r‘𝑊)〉)) =
(Scalar‘(((𝑊 sSet
〈(Scalar‘ndx), (𝑊 ↾s 𝑆)〉) sSet 〈(
·𝑠 ‘ndx), (.r‘𝑊)〉) sSet
〈(·𝑖‘ndx),
(.r‘𝑊)〉)) |
16 | 9, 15 | eqtri 2632 |
. . 3
⊢
(Scalar‘(𝑊
sSet 〈(Scalar‘ndx), (𝑊 ↾s 𝑆)〉)) = (Scalar‘(((𝑊 sSet 〈(Scalar‘ndx),
(𝑊 ↾s
𝑆)〉) sSet 〈(
·𝑠 ‘ndx), (.r‘𝑊)〉) sSet
〈(·𝑖‘ndx),
(.r‘𝑊)〉)) |
17 | | ovex 6577 |
. . . . 5
⊢ (𝑊 ↾s 𝑆) ∈ V |
18 | 17 | a1i 11 |
. . . 4
⊢ (𝜑 → (𝑊 ↾s 𝑆) ∈ V) |
19 | 1 | setsid 15742 |
. . . 4
⊢ ((𝑊 ∈ V ∧ (𝑊 ↾s 𝑆) ∈ V) → (𝑊 ↾s 𝑆) = (Scalar‘(𝑊 sSet 〈(Scalar‘ndx),
(𝑊 ↾s
𝑆)〉))) |
20 | 18, 19 | sylan2 490 |
. . 3
⊢ ((𝑊 ∈ V ∧ 𝜑) → (𝑊 ↾s 𝑆) = (Scalar‘(𝑊 sSet 〈(Scalar‘ndx), (𝑊 ↾s 𝑆)〉))) |
21 | | srapart.a |
. . . . . 6
⊢ (𝜑 → 𝐴 = ((subringAlg ‘𝑊)‘𝑆)) |
22 | 21 | adantl 481 |
. . . . 5
⊢ ((𝑊 ∈ V ∧ 𝜑) → 𝐴 = ((subringAlg ‘𝑊)‘𝑆)) |
23 | | srapart.s |
. . . . . 6
⊢ (𝜑 → 𝑆 ⊆ (Base‘𝑊)) |
24 | | sraval 18997 |
. . . . . 6
⊢ ((𝑊 ∈ V ∧ 𝑆 ⊆ (Base‘𝑊)) → ((subringAlg
‘𝑊)‘𝑆) = (((𝑊 sSet 〈(Scalar‘ndx), (𝑊 ↾s 𝑆)〉) sSet 〈(
·𝑠 ‘ndx), (.r‘𝑊)〉) sSet
〈(·𝑖‘ndx),
(.r‘𝑊)〉)) |
25 | 23, 24 | sylan2 490 |
. . . . 5
⊢ ((𝑊 ∈ V ∧ 𝜑) → ((subringAlg ‘𝑊)‘𝑆) = (((𝑊 sSet 〈(Scalar‘ndx), (𝑊 ↾s 𝑆)〉) sSet 〈(
·𝑠 ‘ndx), (.r‘𝑊)〉) sSet
〈(·𝑖‘ndx),
(.r‘𝑊)〉)) |
26 | 22, 25 | eqtrd 2644 |
. . . 4
⊢ ((𝑊 ∈ V ∧ 𝜑) → 𝐴 = (((𝑊 sSet 〈(Scalar‘ndx), (𝑊 ↾s 𝑆)〉) sSet 〈(
·𝑠 ‘ndx), (.r‘𝑊)〉) sSet
〈(·𝑖‘ndx),
(.r‘𝑊)〉)) |
27 | 26 | fveq2d 6107 |
. . 3
⊢ ((𝑊 ∈ V ∧ 𝜑) → (Scalar‘𝐴) = (Scalar‘(((𝑊 sSet 〈(Scalar‘ndx), (𝑊 ↾s 𝑆)〉) sSet 〈(
·𝑠 ‘ndx), (.r‘𝑊)〉) sSet
〈(·𝑖‘ndx),
(.r‘𝑊)〉))) |
28 | 16, 20, 27 | 3eqtr4a 2670 |
. 2
⊢ ((𝑊 ∈ V ∧ 𝜑) → (𝑊 ↾s 𝑆) = (Scalar‘𝐴)) |
29 | 1 | str0 15739 |
. . 3
⊢ ∅ =
(Scalar‘∅) |
30 | | reldmress 15753 |
. . . . 5
⊢ Rel dom
↾s |
31 | 30 | ovprc1 6582 |
. . . 4
⊢ (¬
𝑊 ∈ V → (𝑊 ↾s 𝑆) = ∅) |
32 | 31 | adantr 480 |
. . 3
⊢ ((¬
𝑊 ∈ V ∧ 𝜑) → (𝑊 ↾s 𝑆) = ∅) |
33 | | fvprc 6097 |
. . . . . . 7
⊢ (¬
𝑊 ∈ V →
(subringAlg ‘𝑊) =
∅) |
34 | 33 | fveq1d 6105 |
. . . . . 6
⊢ (¬
𝑊 ∈ V →
((subringAlg ‘𝑊)‘𝑆) = (∅‘𝑆)) |
35 | | 0fv 6137 |
. . . . . 6
⊢
(∅‘𝑆) =
∅ |
36 | 34, 35 | syl6eq 2660 |
. . . . 5
⊢ (¬
𝑊 ∈ V →
((subringAlg ‘𝑊)‘𝑆) = ∅) |
37 | 21, 36 | sylan9eqr 2666 |
. . . 4
⊢ ((¬
𝑊 ∈ V ∧ 𝜑) → 𝐴 = ∅) |
38 | 37 | fveq2d 6107 |
. . 3
⊢ ((¬
𝑊 ∈ V ∧ 𝜑) → (Scalar‘𝐴) =
(Scalar‘∅)) |
39 | 29, 32, 38 | 3eqtr4a 2670 |
. 2
⊢ ((¬
𝑊 ∈ V ∧ 𝜑) → (𝑊 ↾s 𝑆) = (Scalar‘𝐴)) |
40 | 28, 39 | pm2.61ian 827 |
1
⊢ (𝜑 → (𝑊 ↾s 𝑆) = (Scalar‘𝐴)) |