Proof of Theorem sraipg
Step | Hyp | Ref
| Expression |
1 | | srapart.ex |
. . . . 5
⊢ (𝜑 → 𝑊 ∈ 𝑋) |
2 | | scaslid 12629 |
. . . . . . 7
⊢ (Scalar =
Slot (Scalar‘ndx) ∧ (Scalar‘ndx) ∈
ℕ) |
3 | 2 | simpri 113 |
. . . . . 6
⊢
(Scalar‘ndx) ∈ ℕ |
4 | 3 | a1i 9 |
. . . . 5
⊢ (𝜑 → (Scalar‘ndx) ∈
ℕ) |
5 | | basfn 12537 |
. . . . . . . 8
⊢ Base Fn
V |
6 | 1 | elexd 2764 |
. . . . . . . 8
⊢ (𝜑 → 𝑊 ∈ V) |
7 | | funfvex 5546 |
. . . . . . . . 9
⊢ ((Fun
Base ∧ 𝑊 ∈ dom
Base) → (Base‘𝑊)
∈ V) |
8 | 7 | funfni 5330 |
. . . . . . . 8
⊢ ((Base Fn
V ∧ 𝑊 ∈ V) →
(Base‘𝑊) ∈
V) |
9 | 5, 6, 8 | sylancr 414 |
. . . . . . 7
⊢ (𝜑 → (Base‘𝑊) ∈ V) |
10 | | srapart.s |
. . . . . . 7
⊢ (𝜑 → 𝑆 ⊆ (Base‘𝑊)) |
11 | 9, 10 | ssexd 4157 |
. . . . . 6
⊢ (𝜑 → 𝑆 ∈ V) |
12 | | ressex 12542 |
. . . . . 6
⊢ ((𝑊 ∈ 𝑋 ∧ 𝑆 ∈ V) → (𝑊 ↾s 𝑆) ∈ V) |
13 | 1, 11, 12 | syl2anc 411 |
. . . . 5
⊢ (𝜑 → (𝑊 ↾s 𝑆) ∈ V) |
14 | | setsex 12511 |
. . . . 5
⊢ ((𝑊 ∈ 𝑋 ∧ (Scalar‘ndx) ∈ ℕ
∧ (𝑊
↾s 𝑆)
∈ V) → (𝑊 sSet
〈(Scalar‘ndx), (𝑊 ↾s 𝑆)〉) ∈ V) |
15 | 1, 4, 13, 14 | syl3anc 1248 |
. . . 4
⊢ (𝜑 → (𝑊 sSet 〈(Scalar‘ndx), (𝑊 ↾s 𝑆)〉) ∈
V) |
16 | | vscaslid 12639 |
. . . . . 6
⊢ (
·𝑠 = Slot (
·𝑠 ‘ndx) ∧ (
·𝑠 ‘ndx) ∈
ℕ) |
17 | 16 | simpri 113 |
. . . . 5
⊢ (
·𝑠 ‘ndx) ∈ ℕ |
18 | 17 | a1i 9 |
. . . 4
⊢ (𝜑 → (
·𝑠 ‘ndx) ∈
ℕ) |
19 | | mulrslid 12608 |
. . . . . 6
⊢
(.r = Slot (.r‘ndx) ∧
(.r‘ndx) ∈ ℕ) |
20 | 19 | slotex 12506 |
. . . . 5
⊢ (𝑊 ∈ 𝑋 → (.r‘𝑊) ∈ V) |
21 | 1, 20 | syl 14 |
. . . 4
⊢ (𝜑 → (.r‘𝑊) ∈ V) |
22 | | setsex 12511 |
. . . 4
⊢ (((𝑊 sSet 〈(Scalar‘ndx),
(𝑊 ↾s
𝑆)〉) ∈ V ∧ (
·𝑠 ‘ndx) ∈ ℕ ∧
(.r‘𝑊)
∈ V) → ((𝑊 sSet
〈(Scalar‘ndx), (𝑊 ↾s 𝑆)〉) sSet 〈(
·𝑠 ‘ndx), (.r‘𝑊)〉) ∈
V) |
23 | 15, 18, 21, 22 | syl3anc 1248 |
. . 3
⊢ (𝜑 → ((𝑊 sSet 〈(Scalar‘ndx), (𝑊 ↾s 𝑆)〉) sSet 〈(
·𝑠 ‘ndx), (.r‘𝑊)〉) ∈
V) |
24 | | ipslid 12647 |
. . . 4
⊢
(·𝑖 = Slot
(·𝑖‘ndx) ∧
(·𝑖‘ndx) ∈
ℕ) |
25 | 24 | setsslid 12530 |
. . 3
⊢ ((((𝑊 sSet 〈(Scalar‘ndx),
(𝑊 ↾s
𝑆)〉) sSet 〈(
·𝑠 ‘ndx), (.r‘𝑊)〉) ∈ V ∧
(.r‘𝑊)
∈ V) → (.r‘𝑊) =
(·𝑖‘(((𝑊 sSet 〈(Scalar‘ndx), (𝑊 ↾s 𝑆)〉) sSet 〈(
·𝑠 ‘ndx), (.r‘𝑊)〉) sSet
〈(·𝑖‘ndx),
(.r‘𝑊)〉))) |
26 | 23, 21, 25 | syl2anc 411 |
. 2
⊢ (𝜑 → (.r‘𝑊) =
(·𝑖‘(((𝑊 sSet 〈(Scalar‘ndx), (𝑊 ↾s 𝑆)〉) sSet 〈(
·𝑠 ‘ndx), (.r‘𝑊)〉) sSet
〈(·𝑖‘ndx),
(.r‘𝑊)〉))) |
27 | | srapart.a |
. . . 4
⊢ (𝜑 → 𝐴 = ((subringAlg ‘𝑊)‘𝑆)) |
28 | | sraval 13713 |
. . . . 5
⊢ ((𝑊 ∈ V ∧ 𝑆 ⊆ (Base‘𝑊)) → ((subringAlg
‘𝑊)‘𝑆) = (((𝑊 sSet 〈(Scalar‘ndx), (𝑊 ↾s 𝑆)〉) sSet 〈(
·𝑠 ‘ndx), (.r‘𝑊)〉) sSet
〈(·𝑖‘ndx),
(.r‘𝑊)〉)) |
29 | 6, 10, 28 | syl2anc 411 |
. . . 4
⊢ (𝜑 → ((subringAlg ‘𝑊)‘𝑆) = (((𝑊 sSet 〈(Scalar‘ndx), (𝑊 ↾s 𝑆)〉) sSet 〈(
·𝑠 ‘ndx), (.r‘𝑊)〉) sSet
〈(·𝑖‘ndx),
(.r‘𝑊)〉)) |
30 | 27, 29 | eqtrd 2221 |
. . 3
⊢ (𝜑 → 𝐴 = (((𝑊 sSet 〈(Scalar‘ndx), (𝑊 ↾s 𝑆)〉) sSet 〈(
·𝑠 ‘ndx), (.r‘𝑊)〉) sSet
〈(·𝑖‘ndx),
(.r‘𝑊)〉)) |
31 | 30 | fveq2d 5533 |
. 2
⊢ (𝜑 →
(·𝑖‘𝐴) =
(·𝑖‘(((𝑊 sSet 〈(Scalar‘ndx), (𝑊 ↾s 𝑆)〉) sSet 〈(
·𝑠 ‘ndx), (.r‘𝑊)〉) sSet
〈(·𝑖‘ndx),
(.r‘𝑊)〉))) |
32 | 26, 31 | eqtr4d 2224 |
1
⊢ (𝜑 → (.r‘𝑊) =
(·𝑖‘𝐴)) |