Proof of Theorem sralemg
Step | Hyp | Ref
| Expression |
1 | | srapart.ex |
. . . 4
⊢ (𝜑 → 𝑊 ∈ 𝑋) |
2 | | basfn 12534 |
. . . . . . 7
⊢ Base Fn
V |
3 | 1 | elexd 2762 |
. . . . . . 7
⊢ (𝜑 → 𝑊 ∈ V) |
4 | | funfvex 5544 |
. . . . . . . 8
⊢ ((Fun
Base ∧ 𝑊 ∈ dom
Base) → (Base‘𝑊)
∈ V) |
5 | 4 | funfni 5328 |
. . . . . . 7
⊢ ((Base Fn
V ∧ 𝑊 ∈ V) →
(Base‘𝑊) ∈
V) |
6 | 2, 3, 5 | sylancr 414 |
. . . . . 6
⊢ (𝜑 → (Base‘𝑊) ∈ V) |
7 | | srapart.s |
. . . . . 6
⊢ (𝜑 → 𝑆 ⊆ (Base‘𝑊)) |
8 | 6, 7 | ssexd 4155 |
. . . . 5
⊢ (𝜑 → 𝑆 ∈ V) |
9 | | ressex 12539 |
. . . . 5
⊢ ((𝑊 ∈ 𝑋 ∧ 𝑆 ∈ V) → (𝑊 ↾s 𝑆) ∈ V) |
10 | 1, 8, 9 | syl2anc 411 |
. . . 4
⊢ (𝜑 → (𝑊 ↾s 𝑆) ∈ V) |
11 | | sralemg.1 |
. . . . 5
⊢ (𝐸 = Slot (𝐸‘ndx) ∧ (𝐸‘ndx) ∈ ℕ) |
12 | | sralem.2 |
. . . . . 6
⊢
(Scalar‘ndx) ≠ (𝐸‘ndx) |
13 | 12 | necomi 2442 |
. . . . 5
⊢ (𝐸‘ndx) ≠
(Scalar‘ndx) |
14 | | scaslid 12626 |
. . . . . 6
⊢ (Scalar =
Slot (Scalar‘ndx) ∧ (Scalar‘ndx) ∈
ℕ) |
15 | 14 | simpri 113 |
. . . . 5
⊢
(Scalar‘ndx) ∈ ℕ |
16 | 11, 13, 15 | setsslnid 12528 |
. . . 4
⊢ ((𝑊 ∈ 𝑋 ∧ (𝑊 ↾s 𝑆) ∈ V) → (𝐸‘𝑊) = (𝐸‘(𝑊 sSet 〈(Scalar‘ndx), (𝑊 ↾s 𝑆)〉))) |
17 | 1, 10, 16 | syl2anc 411 |
. . 3
⊢ (𝜑 → (𝐸‘𝑊) = (𝐸‘(𝑊 sSet 〈(Scalar‘ndx), (𝑊 ↾s 𝑆)〉))) |
18 | 15 | a1i 9 |
. . . . 5
⊢ (𝜑 → (Scalar‘ndx) ∈
ℕ) |
19 | | setsex 12508 |
. . . . 5
⊢ ((𝑊 ∈ 𝑋 ∧ (Scalar‘ndx) ∈ ℕ
∧ (𝑊
↾s 𝑆)
∈ V) → (𝑊 sSet
〈(Scalar‘ndx), (𝑊 ↾s 𝑆)〉) ∈ V) |
20 | 1, 18, 10, 19 | syl3anc 1248 |
. . . 4
⊢ (𝜑 → (𝑊 sSet 〈(Scalar‘ndx), (𝑊 ↾s 𝑆)〉) ∈
V) |
21 | | mulrslid 12605 |
. . . . . 6
⊢
(.r = Slot (.r‘ndx) ∧
(.r‘ndx) ∈ ℕ) |
22 | 21 | slotex 12503 |
. . . . 5
⊢ (𝑊 ∈ 𝑋 → (.r‘𝑊) ∈ V) |
23 | 1, 22 | syl 14 |
. . . 4
⊢ (𝜑 → (.r‘𝑊) ∈ V) |
24 | | sralem.3 |
. . . . . 6
⊢ (
·𝑠 ‘ndx) ≠ (𝐸‘ndx) |
25 | 24 | necomi 2442 |
. . . . 5
⊢ (𝐸‘ndx) ≠ (
·𝑠 ‘ndx) |
26 | | vscaslid 12636 |
. . . . . 6
⊢ (
·𝑠 = Slot (
·𝑠 ‘ndx) ∧ (
·𝑠 ‘ndx) ∈
ℕ) |
27 | 26 | simpri 113 |
. . . . 5
⊢ (
·𝑠 ‘ndx) ∈ ℕ |
28 | 11, 25, 27 | setsslnid 12528 |
. . . 4
⊢ (((𝑊 sSet 〈(Scalar‘ndx),
(𝑊 ↾s
𝑆)〉) ∈ V ∧
(.r‘𝑊)
∈ V) → (𝐸‘(𝑊 sSet 〈(Scalar‘ndx), (𝑊 ↾s 𝑆)〉)) = (𝐸‘((𝑊 sSet 〈(Scalar‘ndx), (𝑊 ↾s 𝑆)〉) sSet 〈(
·𝑠 ‘ndx), (.r‘𝑊)〉))) |
29 | 20, 23, 28 | syl2anc 411 |
. . 3
⊢ (𝜑 → (𝐸‘(𝑊 sSet 〈(Scalar‘ndx), (𝑊 ↾s 𝑆)〉)) = (𝐸‘((𝑊 sSet 〈(Scalar‘ndx), (𝑊 ↾s 𝑆)〉) sSet 〈(
·𝑠 ‘ndx), (.r‘𝑊)〉))) |
30 | 27 | a1i 9 |
. . . . 5
⊢ (𝜑 → (
·𝑠 ‘ndx) ∈
ℕ) |
31 | | setsex 12508 |
. . . . 5
⊢ (((𝑊 sSet 〈(Scalar‘ndx),
(𝑊 ↾s
𝑆)〉) ∈ V ∧ (
·𝑠 ‘ndx) ∈ ℕ ∧
(.r‘𝑊)
∈ V) → ((𝑊 sSet
〈(Scalar‘ndx), (𝑊 ↾s 𝑆)〉) sSet 〈(
·𝑠 ‘ndx), (.r‘𝑊)〉) ∈
V) |
32 | 20, 30, 23, 31 | syl3anc 1248 |
. . . 4
⊢ (𝜑 → ((𝑊 sSet 〈(Scalar‘ndx), (𝑊 ↾s 𝑆)〉) sSet 〈(
·𝑠 ‘ndx), (.r‘𝑊)〉) ∈
V) |
33 | | sralem.4 |
. . . . . 6
⊢
(·𝑖‘ndx) ≠ (𝐸‘ndx) |
34 | 33 | necomi 2442 |
. . . . 5
⊢ (𝐸‘ndx) ≠
(·𝑖‘ndx) |
35 | | ipslid 12644 |
. . . . . 6
⊢
(·𝑖 = Slot
(·𝑖‘ndx) ∧
(·𝑖‘ndx) ∈
ℕ) |
36 | 35 | simpri 113 |
. . . . 5
⊢
(·𝑖‘ndx) ∈
ℕ |
37 | 11, 34, 36 | setsslnid 12528 |
. . . 4
⊢ ((((𝑊 sSet 〈(Scalar‘ndx),
(𝑊 ↾s
𝑆)〉) sSet 〈(
·𝑠 ‘ndx), (.r‘𝑊)〉) ∈ V ∧
(.r‘𝑊)
∈ V) → (𝐸‘((𝑊 sSet 〈(Scalar‘ndx), (𝑊 ↾s 𝑆)〉) sSet 〈(
·𝑠 ‘ndx), (.r‘𝑊)〉)) = (𝐸‘(((𝑊 sSet 〈(Scalar‘ndx), (𝑊 ↾s 𝑆)〉) sSet 〈(
·𝑠 ‘ndx), (.r‘𝑊)〉) sSet
〈(·𝑖‘ndx),
(.r‘𝑊)〉))) |
38 | 32, 23, 37 | syl2anc 411 |
. . 3
⊢ (𝜑 → (𝐸‘((𝑊 sSet 〈(Scalar‘ndx), (𝑊 ↾s 𝑆)〉) sSet 〈(
·𝑠 ‘ndx), (.r‘𝑊)〉)) = (𝐸‘(((𝑊 sSet 〈(Scalar‘ndx), (𝑊 ↾s 𝑆)〉) sSet 〈(
·𝑠 ‘ndx), (.r‘𝑊)〉) sSet
〈(·𝑖‘ndx),
(.r‘𝑊)〉))) |
39 | 17, 29, 38 | 3eqtrd 2224 |
. 2
⊢ (𝜑 → (𝐸‘𝑊) = (𝐸‘(((𝑊 sSet 〈(Scalar‘ndx), (𝑊 ↾s 𝑆)〉) sSet 〈(
·𝑠 ‘ndx), (.r‘𝑊)〉) sSet
〈(·𝑖‘ndx),
(.r‘𝑊)〉))) |
40 | | srapart.a |
. . . 4
⊢ (𝜑 → 𝐴 = ((subringAlg ‘𝑊)‘𝑆)) |
41 | | sraval 13683 |
. . . . 5
⊢ ((𝑊 ∈ 𝑋 ∧ 𝑆 ⊆ (Base‘𝑊)) → ((subringAlg ‘𝑊)‘𝑆) = (((𝑊 sSet 〈(Scalar‘ndx), (𝑊 ↾s 𝑆)〉) sSet 〈(
·𝑠 ‘ndx), (.r‘𝑊)〉) sSet
〈(·𝑖‘ndx),
(.r‘𝑊)〉)) |
42 | 1, 7, 41 | syl2anc 411 |
. . . 4
⊢ (𝜑 → ((subringAlg ‘𝑊)‘𝑆) = (((𝑊 sSet 〈(Scalar‘ndx), (𝑊 ↾s 𝑆)〉) sSet 〈(
·𝑠 ‘ndx), (.r‘𝑊)〉) sSet
〈(·𝑖‘ndx),
(.r‘𝑊)〉)) |
43 | 40, 42 | eqtrd 2220 |
. . 3
⊢ (𝜑 → 𝐴 = (((𝑊 sSet 〈(Scalar‘ndx), (𝑊 ↾s 𝑆)〉) sSet 〈(
·𝑠 ‘ndx), (.r‘𝑊)〉) sSet
〈(·𝑖‘ndx),
(.r‘𝑊)〉)) |
44 | 43 | fveq2d 5531 |
. 2
⊢ (𝜑 → (𝐸‘𝐴) = (𝐸‘(((𝑊 sSet 〈(Scalar‘ndx), (𝑊 ↾s 𝑆)〉) sSet 〈(
·𝑠 ‘ndx), (.r‘𝑊)〉) sSet
〈(·𝑖‘ndx),
(.r‘𝑊)〉))) |
45 | 39, 44 | eqtr4d 2223 |
1
⊢ (𝜑 → (𝐸‘𝑊) = (𝐸‘𝐴)) |