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