Proof of Theorem rrxip
Step | Hyp | Ref
| Expression |
1 | | rrxval.r |
. . . 4
⊢ 𝐻 = (ℝ^‘𝐼) |
2 | | rrxbase.b |
. . . 4
⊢ 𝐵 = (Base‘𝐻) |
3 | 1, 2 | rrxprds 24286 |
. . 3
⊢ (𝐼 ∈ 𝑉 → 𝐻 =
(toℂPreHil‘((ℝfldXs(𝐼 × {((subringAlg
‘ℝfld)‘ℝ)})) ↾s 𝐵))) |
4 | 3 | fveq2d 6721 |
. 2
⊢ (𝐼 ∈ 𝑉 →
(·𝑖‘𝐻) =
(·𝑖‘(toℂPreHil‘((ℝfldXs(𝐼 × {((subringAlg
‘ℝfld)‘ℝ)})) ↾s 𝐵)))) |
5 | | eqid 2737 |
. . . 4
⊢
(toℂPreHil‘((ℝfldXs(𝐼 × {((subringAlg
‘ℝfld)‘ℝ)})) ↾s 𝐵)) =
(toℂPreHil‘((ℝfldXs(𝐼 × {((subringAlg
‘ℝfld)‘ℝ)})) ↾s 𝐵)) |
6 | | eqid 2737 |
. . . 4
⊢
(·𝑖‘((ℝfldXs(𝐼 × {((subringAlg
‘ℝfld)‘ℝ)})) ↾s 𝐵)) =
(·𝑖‘((ℝfldXs(𝐼 × {((subringAlg
‘ℝfld)‘ℝ)})) ↾s 𝐵)) |
7 | 5, 6 | tcphip 24122 |
. . 3
⊢
(·𝑖‘((ℝfldXs(𝐼 × {((subringAlg
‘ℝfld)‘ℝ)})) ↾s 𝐵)) =
(·𝑖‘(toℂPreHil‘((ℝfldXs(𝐼 × {((subringAlg
‘ℝfld)‘ℝ)})) ↾s 𝐵))) |
8 | 2 | fvexi 6731 |
. . . . 5
⊢ 𝐵 ∈ V |
9 | | eqid 2737 |
. . . . . 6
⊢
((ℝfldXs(𝐼 × {((subringAlg
‘ℝfld)‘ℝ)})) ↾s 𝐵) = ((ℝfldXs(𝐼 × {((subringAlg
‘ℝfld)‘ℝ)})) ↾s 𝐵) |
10 | | eqid 2737 |
. . . . . 6
⊢
(·𝑖‘(ℝfldXs(𝐼 × {((subringAlg
‘ℝfld)‘ℝ)}))) =
(·𝑖‘(ℝfldXs(𝐼 × {((subringAlg
‘ℝfld)‘ℝ)}))) |
11 | 9, 10 | ressip 16878 |
. . . . 5
⊢ (𝐵 ∈ V →
(·𝑖‘(ℝfldXs(𝐼 × {((subringAlg
‘ℝfld)‘ℝ)}))) =
(·𝑖‘((ℝfldXs(𝐼 × {((subringAlg
‘ℝfld)‘ℝ)})) ↾s 𝐵))) |
12 | 8, 11 | ax-mp 5 |
. . . 4
⊢
(·𝑖‘(ℝfldXs(𝐼 × {((subringAlg
‘ℝfld)‘ℝ)}))) =
(·𝑖‘((ℝfldXs(𝐼 × {((subringAlg
‘ℝfld)‘ℝ)})) ↾s 𝐵)) |
13 | | eqid 2737 |
. . . . . 6
⊢
(ℝfldXs(𝐼 × {((subringAlg
‘ℝfld)‘ℝ)})) = (ℝfldXs(𝐼 × {((subringAlg
‘ℝfld)‘ℝ)})) |
14 | | refld 20581 |
. . . . . . 7
⊢
ℝfld ∈ Field |
15 | 14 | a1i 11 |
. . . . . 6
⊢ (𝐼 ∈ 𝑉 → ℝfld ∈
Field) |
16 | | snex 5324 |
. . . . . . 7
⊢
{((subringAlg ‘ℝfld)‘ℝ)} ∈
V |
17 | | xpexg 7535 |
. . . . . . 7
⊢ ((𝐼 ∈ 𝑉 ∧ {((subringAlg
‘ℝfld)‘ℝ)} ∈ V) → (𝐼 × {((subringAlg
‘ℝfld)‘ℝ)}) ∈ V) |
18 | 16, 17 | mpan2 691 |
. . . . . 6
⊢ (𝐼 ∈ 𝑉 → (𝐼 × {((subringAlg
‘ℝfld)‘ℝ)}) ∈ V) |
19 | | eqid 2737 |
. . . . . 6
⊢
(Base‘(ℝfldXs(𝐼 × {((subringAlg
‘ℝfld)‘ℝ)}))) =
(Base‘(ℝfldXs(𝐼 × {((subringAlg
‘ℝfld)‘ℝ)}))) |
20 | | fvex 6730 |
. . . . . . . . 9
⊢
((subringAlg ‘ℝfld)‘ℝ) ∈
V |
21 | 20 | snnz 4692 |
. . . . . . . 8
⊢
{((subringAlg ‘ℝfld)‘ℝ)} ≠
∅ |
22 | | dmxp 5798 |
. . . . . . . 8
⊢
({((subringAlg ‘ℝfld)‘ℝ)} ≠
∅ → dom (𝐼
× {((subringAlg ‘ℝfld)‘ℝ)}) = 𝐼) |
23 | 21, 22 | ax-mp 5 |
. . . . . . 7
⊢ dom
(𝐼 × {((subringAlg
‘ℝfld)‘ℝ)}) = 𝐼 |
24 | 23 | a1i 11 |
. . . . . 6
⊢ (𝐼 ∈ 𝑉 → dom (𝐼 × {((subringAlg
‘ℝfld)‘ℝ)}) = 𝐼) |
25 | 13, 15, 18, 19, 24, 10 | prdsip 16966 |
. . . . 5
⊢ (𝐼 ∈ 𝑉 →
(·𝑖‘(ℝfldXs(𝐼 × {((subringAlg
‘ℝfld)‘ℝ)}))) = (𝑓 ∈
(Base‘(ℝfldXs(𝐼 × {((subringAlg
‘ℝfld)‘ℝ)}))), 𝑔 ∈
(Base‘(ℝfldXs(𝐼 × {((subringAlg
‘ℝfld)‘ℝ)}))) ↦ (ℝfld
Σg (𝑥 ∈ 𝐼 ↦ ((𝑓‘𝑥)(·𝑖‘((𝐼 × {((subringAlg
‘ℝfld)‘ℝ)})‘𝑥))(𝑔‘𝑥)))))) |
26 | 13, 15, 18, 19, 24 | prdsbas 16962 |
. . . . . . 7
⊢ (𝐼 ∈ 𝑉 →
(Base‘(ℝfldXs(𝐼 × {((subringAlg
‘ℝfld)‘ℝ)}))) = X𝑥 ∈
𝐼 (Base‘((𝐼 × {((subringAlg
‘ℝfld)‘ℝ)})‘𝑥))) |
27 | | eqidd 2738 |
. . . . . . . . . . 11
⊢ (𝑥 ∈ 𝐼 → ((subringAlg
‘ℝfld)‘ℝ) = ((subringAlg
‘ℝfld)‘ℝ)) |
28 | | rebase 20568 |
. . . . . . . . . . . . 13
⊢ ℝ =
(Base‘ℝfld) |
29 | 28 | eqimssi 3959 |
. . . . . . . . . . . 12
⊢ ℝ
⊆ (Base‘ℝfld) |
30 | 29 | a1i 11 |
. . . . . . . . . . 11
⊢ (𝑥 ∈ 𝐼 → ℝ ⊆
(Base‘ℝfld)) |
31 | 27, 30 | srabase 20215 |
. . . . . . . . . 10
⊢ (𝑥 ∈ 𝐼 → (Base‘ℝfld) =
(Base‘((subringAlg
‘ℝfld)‘ℝ))) |
32 | 28 | a1i 11 |
. . . . . . . . . 10
⊢ (𝑥 ∈ 𝐼 → ℝ =
(Base‘ℝfld)) |
33 | 20 | fvconst2 7019 |
. . . . . . . . . . 11
⊢ (𝑥 ∈ 𝐼 → ((𝐼 × {((subringAlg
‘ℝfld)‘ℝ)})‘𝑥) = ((subringAlg
‘ℝfld)‘ℝ)) |
34 | 33 | fveq2d 6721 |
. . . . . . . . . 10
⊢ (𝑥 ∈ 𝐼 → (Base‘((𝐼 × {((subringAlg
‘ℝfld)‘ℝ)})‘𝑥)) = (Base‘((subringAlg
‘ℝfld)‘ℝ))) |
35 | 31, 32, 34 | 3eqtr4rd 2788 |
. . . . . . . . 9
⊢ (𝑥 ∈ 𝐼 → (Base‘((𝐼 × {((subringAlg
‘ℝfld)‘ℝ)})‘𝑥)) = ℝ) |
36 | 35 | adantl 485 |
. . . . . . . 8
⊢ ((𝐼 ∈ 𝑉 ∧ 𝑥 ∈ 𝐼) → (Base‘((𝐼 × {((subringAlg
‘ℝfld)‘ℝ)})‘𝑥)) = ℝ) |
37 | 36 | ixpeq2dva 8593 |
. . . . . . 7
⊢ (𝐼 ∈ 𝑉 → X𝑥 ∈ 𝐼 (Base‘((𝐼 × {((subringAlg
‘ℝfld)‘ℝ)})‘𝑥)) = X𝑥 ∈ 𝐼 ℝ) |
38 | | reex 10820 |
. . . . . . . 8
⊢ ℝ
∈ V |
39 | | ixpconstg 8587 |
. . . . . . . 8
⊢ ((𝐼 ∈ 𝑉 ∧ ℝ ∈ V) → X𝑥 ∈
𝐼 ℝ = (ℝ
↑m 𝐼)) |
40 | 38, 39 | mpan2 691 |
. . . . . . 7
⊢ (𝐼 ∈ 𝑉 → X𝑥 ∈ 𝐼 ℝ = (ℝ ↑m 𝐼)) |
41 | 26, 37, 40 | 3eqtrd 2781 |
. . . . . 6
⊢ (𝐼 ∈ 𝑉 →
(Base‘(ℝfldXs(𝐼 × {((subringAlg
‘ℝfld)‘ℝ)}))) = (ℝ ↑m
𝐼)) |
42 | | remulr 20573 |
. . . . . . . . . . 11
⊢ ·
= (.r‘ℝfld) |
43 | 33, 30 | sraip 20220 |
. . . . . . . . . . 11
⊢ (𝑥 ∈ 𝐼 →
(.r‘ℝfld) =
(·𝑖‘((𝐼 × {((subringAlg
‘ℝfld)‘ℝ)})‘𝑥))) |
44 | 42, 43 | eqtr2id 2791 |
. . . . . . . . . 10
⊢ (𝑥 ∈ 𝐼 →
(·𝑖‘((𝐼 × {((subringAlg
‘ℝfld)‘ℝ)})‘𝑥)) = · ) |
45 | 44 | oveqd 7230 |
. . . . . . . . 9
⊢ (𝑥 ∈ 𝐼 → ((𝑓‘𝑥)(·𝑖‘((𝐼 × {((subringAlg
‘ℝfld)‘ℝ)})‘𝑥))(𝑔‘𝑥)) = ((𝑓‘𝑥) · (𝑔‘𝑥))) |
46 | 45 | mpteq2ia 5146 |
. . . . . . . 8
⊢ (𝑥 ∈ 𝐼 ↦ ((𝑓‘𝑥)(·𝑖‘((𝐼 × {((subringAlg
‘ℝfld)‘ℝ)})‘𝑥))(𝑔‘𝑥))) = (𝑥 ∈ 𝐼 ↦ ((𝑓‘𝑥) · (𝑔‘𝑥))) |
47 | 46 | a1i 11 |
. . . . . . 7
⊢ (𝐼 ∈ 𝑉 → (𝑥 ∈ 𝐼 ↦ ((𝑓‘𝑥)(·𝑖‘((𝐼 × {((subringAlg
‘ℝfld)‘ℝ)})‘𝑥))(𝑔‘𝑥))) = (𝑥 ∈ 𝐼 ↦ ((𝑓‘𝑥) · (𝑔‘𝑥)))) |
48 | 47 | oveq2d 7229 |
. . . . . 6
⊢ (𝐼 ∈ 𝑉 → (ℝfld
Σg (𝑥 ∈ 𝐼 ↦ ((𝑓‘𝑥)(·𝑖‘((𝐼 × {((subringAlg
‘ℝfld)‘ℝ)})‘𝑥))(𝑔‘𝑥)))) = (ℝfld
Σg (𝑥
∈ 𝐼 ↦ ((𝑓‘𝑥) · (𝑔‘𝑥))))) |
49 | 41, 41, 48 | mpoeq123dv 7286 |
. . . . 5
⊢ (𝐼 ∈ 𝑉 → (𝑓 ∈
(Base‘(ℝfldXs(𝐼 × {((subringAlg
‘ℝfld)‘ℝ)}))), 𝑔 ∈
(Base‘(ℝfldXs(𝐼 × {((subringAlg
‘ℝfld)‘ℝ)}))) ↦ (ℝfld
Σg (𝑥 ∈ 𝐼 ↦ ((𝑓‘𝑥)(·𝑖‘((𝐼 × {((subringAlg
‘ℝfld)‘ℝ)})‘𝑥))(𝑔‘𝑥))))) = (𝑓 ∈ (ℝ ↑m 𝐼), 𝑔 ∈ (ℝ ↑m 𝐼) ↦ (ℝfld
Σg (𝑥
∈ 𝐼 ↦ ((𝑓‘𝑥) · (𝑔‘𝑥)))))) |
50 | 25, 49 | eqtrd 2777 |
. . . 4
⊢ (𝐼 ∈ 𝑉 →
(·𝑖‘(ℝfldXs(𝐼 × {((subringAlg
‘ℝfld)‘ℝ)}))) = (𝑓 ∈ (ℝ ↑m 𝐼), 𝑔 ∈ (ℝ ↑m 𝐼) ↦ (ℝfld
Σg (𝑥 ∈ 𝐼 ↦ ((𝑓‘𝑥) · (𝑔‘𝑥)))))) |
51 | 12, 50 | eqtr3id 2792 |
. . 3
⊢ (𝐼 ∈ 𝑉 →
(·𝑖‘((ℝfldXs(𝐼 × {((subringAlg
‘ℝfld)‘ℝ)})) ↾s 𝐵)) = (𝑓 ∈ (ℝ ↑m 𝐼), 𝑔 ∈ (ℝ ↑m 𝐼) ↦ (ℝfld
Σg (𝑥 ∈ 𝐼 ↦ ((𝑓‘𝑥) · (𝑔‘𝑥)))))) |
52 | 7, 51 | eqtr3id 2792 |
. 2
⊢ (𝐼 ∈ 𝑉 →
(·𝑖‘(toℂPreHil‘((ℝfldXs(𝐼 × {((subringAlg
‘ℝfld)‘ℝ)})) ↾s 𝐵))) = (𝑓 ∈ (ℝ ↑m 𝐼), 𝑔
∈ (ℝ ↑m 𝐼)
↦ (ℝfld Σg (𝑥 ∈ 𝐼 ↦ ((𝑓‘𝑥) · (𝑔‘𝑥)))))) |
53 | 4, 52 | eqtr2d 2778 |
1
⊢ (𝐼 ∈ 𝑉 → (𝑓 ∈ (ℝ ↑m 𝐼), 𝑔 ∈ (ℝ ↑m 𝐼) ↦ (ℝfld
Σg (𝑥 ∈ 𝐼 ↦ ((𝑓‘𝑥) · (𝑔‘𝑥))))) =
(·𝑖‘𝐻)) |