Proof of Theorem rrxip
Step | Hyp | Ref
| Expression |
1 | | rrxval.r |
. . . 4
⊢ 𝐻 = (ℝ^‘𝐼) |
2 | | rrxbase.b |
. . . 4
⊢ 𝐵 = (Base‘𝐻) |
3 | 1, 2 | rrxprds 23177 |
. . 3
⊢ (𝐼 ∈ 𝑉 → 𝐻 =
(toℂHil‘((ℝfldXs(𝐼 × {((subringAlg
‘ℝfld)‘ℝ)})) ↾s 𝐵))) |
4 | 3 | fveq2d 6195 |
. 2
⊢ (𝐼 ∈ 𝑉 →
(·𝑖‘𝐻) =
(·𝑖‘(toℂHil‘((ℝfldXs(𝐼 × {((subringAlg
‘ℝfld)‘ℝ)})) ↾s 𝐵)))) |
5 | | eqid 2622 |
. . . 4
⊢
(toℂHil‘((ℝfldXs(𝐼 × {((subringAlg
‘ℝfld)‘ℝ)})) ↾s 𝐵)) =
(toℂHil‘((ℝfldXs(𝐼 × {((subringAlg
‘ℝfld)‘ℝ)})) ↾s 𝐵)) |
6 | | eqid 2622 |
. . . 4
⊢
(·𝑖‘((ℝfldXs(𝐼 × {((subringAlg
‘ℝfld)‘ℝ)})) ↾s 𝐵)) =
(·𝑖‘((ℝfldXs(𝐼 × {((subringAlg
‘ℝfld)‘ℝ)})) ↾s 𝐵)) |
7 | 5, 6 | tchip 23024 |
. . 3
⊢
(·𝑖‘((ℝfldXs(𝐼 × {((subringAlg
‘ℝfld)‘ℝ)})) ↾s 𝐵)) =
(·𝑖‘(toℂHil‘((ℝfldXs(𝐼 × {((subringAlg
‘ℝfld)‘ℝ)})) ↾s 𝐵))) |
8 | | fvex 6201 |
. . . . . 6
⊢
(Base‘𝐻)
∈ V |
9 | 2, 8 | eqeltri 2697 |
. . . . 5
⊢ 𝐵 ∈ V |
10 | | eqid 2622 |
. . . . . 6
⊢
((ℝfldXs(𝐼 × {((subringAlg
‘ℝfld)‘ℝ)})) ↾s 𝐵) = ((ℝfldXs(𝐼 × {((subringAlg
‘ℝfld)‘ℝ)})) ↾s 𝐵) |
11 | | eqid 2622 |
. . . . . 6
⊢
(·𝑖‘(ℝfldXs(𝐼 × {((subringAlg
‘ℝfld)‘ℝ)}))) =
(·𝑖‘(ℝfldXs(𝐼 × {((subringAlg
‘ℝfld)‘ℝ)}))) |
12 | 10, 11 | ressip 16033 |
. . . . 5
⊢ (𝐵 ∈ V →
(·𝑖‘(ℝfldXs(𝐼 × {((subringAlg
‘ℝfld)‘ℝ)}))) =
(·𝑖‘((ℝfldXs(𝐼 × {((subringAlg
‘ℝfld)‘ℝ)})) ↾s 𝐵))) |
13 | 9, 12 | ax-mp 5 |
. . . 4
⊢
(·𝑖‘(ℝfldXs(𝐼 × {((subringAlg
‘ℝfld)‘ℝ)}))) =
(·𝑖‘((ℝfldXs(𝐼 × {((subringAlg
‘ℝfld)‘ℝ)})) ↾s 𝐵)) |
14 | | eqid 2622 |
. . . . . 6
⊢
(ℝfldXs(𝐼 × {((subringAlg
‘ℝfld)‘ℝ)})) = (ℝfldXs(𝐼 × {((subringAlg
‘ℝfld)‘ℝ)})) |
15 | | refld 19965 |
. . . . . . 7
⊢
ℝfld ∈ Field |
16 | 15 | a1i 11 |
. . . . . 6
⊢ (𝐼 ∈ 𝑉 → ℝfld ∈
Field) |
17 | | snex 4908 |
. . . . . . 7
⊢
{((subringAlg ‘ℝfld)‘ℝ)} ∈
V |
18 | | xpexg 6960 |
. . . . . . 7
⊢ ((𝐼 ∈ 𝑉 ∧ {((subringAlg
‘ℝfld)‘ℝ)} ∈ V) → (𝐼 × {((subringAlg
‘ℝfld)‘ℝ)}) ∈ V) |
19 | 17, 18 | mpan2 707 |
. . . . . 6
⊢ (𝐼 ∈ 𝑉 → (𝐼 × {((subringAlg
‘ℝfld)‘ℝ)}) ∈ V) |
20 | | eqid 2622 |
. . . . . 6
⊢
(Base‘(ℝfldXs(𝐼 × {((subringAlg
‘ℝfld)‘ℝ)}))) =
(Base‘(ℝfldXs(𝐼 × {((subringAlg
‘ℝfld)‘ℝ)}))) |
21 | | fvex 6201 |
. . . . . . . . 9
⊢
((subringAlg ‘ℝfld)‘ℝ) ∈
V |
22 | 21 | snnz 4309 |
. . . . . . . 8
⊢
{((subringAlg ‘ℝfld)‘ℝ)} ≠
∅ |
23 | | dmxp 5344 |
. . . . . . . 8
⊢
({((subringAlg ‘ℝfld)‘ℝ)} ≠
∅ → dom (𝐼
× {((subringAlg ‘ℝfld)‘ℝ)}) = 𝐼) |
24 | 22, 23 | ax-mp 5 |
. . . . . . 7
⊢ dom
(𝐼 × {((subringAlg
‘ℝfld)‘ℝ)}) = 𝐼 |
25 | 24 | a1i 11 |
. . . . . 6
⊢ (𝐼 ∈ 𝑉 → dom (𝐼 × {((subringAlg
‘ℝfld)‘ℝ)}) = 𝐼) |
26 | 14, 16, 19, 20, 25, 11 | prdsip 16121 |
. . . . 5
⊢ (𝐼 ∈ 𝑉 →
(·𝑖‘(ℝfldXs(𝐼 × {((subringAlg
‘ℝfld)‘ℝ)}))) = (𝑓 ∈
(Base‘(ℝfldXs(𝐼 × {((subringAlg
‘ℝfld)‘ℝ)}))), 𝑔 ∈
(Base‘(ℝfldXs(𝐼 × {((subringAlg
‘ℝfld)‘ℝ)}))) ↦ (ℝfld
Σg (𝑥 ∈ 𝐼 ↦ ((𝑓‘𝑥)(·𝑖‘((𝐼 × {((subringAlg
‘ℝfld)‘ℝ)})‘𝑥))(𝑔‘𝑥)))))) |
27 | 14, 16, 19, 20, 25 | prdsbas 16117 |
. . . . . . 7
⊢ (𝐼 ∈ 𝑉 →
(Base‘(ℝfldXs(𝐼 × {((subringAlg
‘ℝfld)‘ℝ)}))) = X𝑥 ∈
𝐼 (Base‘((𝐼 × {((subringAlg
‘ℝfld)‘ℝ)})‘𝑥))) |
28 | | eqidd 2623 |
. . . . . . . . . . 11
⊢ (𝑥 ∈ 𝐼 → ((subringAlg
‘ℝfld)‘ℝ) = ((subringAlg
‘ℝfld)‘ℝ)) |
29 | | rebase 19952 |
. . . . . . . . . . . . 13
⊢ ℝ =
(Base‘ℝfld) |
30 | 29 | eqimssi 3659 |
. . . . . . . . . . . 12
⊢ ℝ
⊆ (Base‘ℝfld) |
31 | 30 | a1i 11 |
. . . . . . . . . . 11
⊢ (𝑥 ∈ 𝐼 → ℝ ⊆
(Base‘ℝfld)) |
32 | 28, 31 | srabase 19178 |
. . . . . . . . . 10
⊢ (𝑥 ∈ 𝐼 → (Base‘ℝfld) =
(Base‘((subringAlg
‘ℝfld)‘ℝ))) |
33 | 29 | a1i 11 |
. . . . . . . . . 10
⊢ (𝑥 ∈ 𝐼 → ℝ =
(Base‘ℝfld)) |
34 | 21 | fvconst2 6469 |
. . . . . . . . . . 11
⊢ (𝑥 ∈ 𝐼 → ((𝐼 × {((subringAlg
‘ℝfld)‘ℝ)})‘𝑥) = ((subringAlg
‘ℝfld)‘ℝ)) |
35 | 34 | fveq2d 6195 |
. . . . . . . . . 10
⊢ (𝑥 ∈ 𝐼 → (Base‘((𝐼 × {((subringAlg
‘ℝfld)‘ℝ)})‘𝑥)) = (Base‘((subringAlg
‘ℝfld)‘ℝ))) |
36 | 32, 33, 35 | 3eqtr4rd 2667 |
. . . . . . . . 9
⊢ (𝑥 ∈ 𝐼 → (Base‘((𝐼 × {((subringAlg
‘ℝfld)‘ℝ)})‘𝑥)) = ℝ) |
37 | 36 | adantl 482 |
. . . . . . . 8
⊢ ((𝐼 ∈ 𝑉 ∧ 𝑥 ∈ 𝐼) → (Base‘((𝐼 × {((subringAlg
‘ℝfld)‘ℝ)})‘𝑥)) = ℝ) |
38 | 37 | ixpeq2dva 7923 |
. . . . . . 7
⊢ (𝐼 ∈ 𝑉 → X𝑥 ∈ 𝐼 (Base‘((𝐼 × {((subringAlg
‘ℝfld)‘ℝ)})‘𝑥)) = X𝑥 ∈ 𝐼 ℝ) |
39 | | reex 10027 |
. . . . . . . 8
⊢ ℝ
∈ V |
40 | | ixpconstg 7917 |
. . . . . . . 8
⊢ ((𝐼 ∈ 𝑉 ∧ ℝ ∈ V) → X𝑥 ∈
𝐼 ℝ = (ℝ
↑𝑚 𝐼)) |
41 | 39, 40 | mpan2 707 |
. . . . . . 7
⊢ (𝐼 ∈ 𝑉 → X𝑥 ∈ 𝐼 ℝ = (ℝ
↑𝑚 𝐼)) |
42 | 27, 38, 41 | 3eqtrd 2660 |
. . . . . 6
⊢ (𝐼 ∈ 𝑉 →
(Base‘(ℝfldXs(𝐼 × {((subringAlg
‘ℝfld)‘ℝ)}))) = (ℝ
↑𝑚 𝐼)) |
43 | | remulr 19957 |
. . . . . . . . . . 11
⊢ ·
= (.r‘ℝfld) |
44 | 34, 31 | sraip 19183 |
. . . . . . . . . . 11
⊢ (𝑥 ∈ 𝐼 →
(.r‘ℝfld) =
(·𝑖‘((𝐼 × {((subringAlg
‘ℝfld)‘ℝ)})‘𝑥))) |
45 | 43, 44 | syl5req 2669 |
. . . . . . . . . 10
⊢ (𝑥 ∈ 𝐼 →
(·𝑖‘((𝐼 × {((subringAlg
‘ℝfld)‘ℝ)})‘𝑥)) = · ) |
46 | 45 | oveqd 6667 |
. . . . . . . . 9
⊢ (𝑥 ∈ 𝐼 → ((𝑓‘𝑥)(·𝑖‘((𝐼 × {((subringAlg
‘ℝfld)‘ℝ)})‘𝑥))(𝑔‘𝑥)) = ((𝑓‘𝑥) · (𝑔‘𝑥))) |
47 | 46 | mpteq2ia 4740 |
. . . . . . . 8
⊢ (𝑥 ∈ 𝐼 ↦ ((𝑓‘𝑥)(·𝑖‘((𝐼 × {((subringAlg
‘ℝfld)‘ℝ)})‘𝑥))(𝑔‘𝑥))) = (𝑥 ∈ 𝐼 ↦ ((𝑓‘𝑥) · (𝑔‘𝑥))) |
48 | 47 | a1i 11 |
. . . . . . 7
⊢ (𝐼 ∈ 𝑉 → (𝑥 ∈ 𝐼 ↦ ((𝑓‘𝑥)(·𝑖‘((𝐼 × {((subringAlg
‘ℝfld)‘ℝ)})‘𝑥))(𝑔‘𝑥))) = (𝑥 ∈ 𝐼 ↦ ((𝑓‘𝑥) · (𝑔‘𝑥)))) |
49 | 48 | oveq2d 6666 |
. . . . . 6
⊢ (𝐼 ∈ 𝑉 → (ℝfld
Σg (𝑥 ∈ 𝐼 ↦ ((𝑓‘𝑥)(·𝑖‘((𝐼 × {((subringAlg
‘ℝfld)‘ℝ)})‘𝑥))(𝑔‘𝑥)))) = (ℝfld
Σg (𝑥
∈ 𝐼 ↦ ((𝑓‘𝑥) · (𝑔‘𝑥))))) |
50 | 42, 42, 49 | mpt2eq123dv 6717 |
. . . . 5
⊢ (𝐼 ∈ 𝑉 → (𝑓 ∈
(Base‘(ℝfldXs(𝐼 × {((subringAlg
‘ℝfld)‘ℝ)}))), 𝑔 ∈
(Base‘(ℝfldXs(𝐼 × {((subringAlg
‘ℝfld)‘ℝ)}))) ↦ (ℝfld
Σg (𝑥 ∈ 𝐼 ↦ ((𝑓‘𝑥)(·𝑖‘((𝐼 × {((subringAlg
‘ℝfld)‘ℝ)})‘𝑥))(𝑔‘𝑥))))) = (𝑓 ∈ (ℝ ↑𝑚 𝐼), 𝑔 ∈ (ℝ ↑𝑚 𝐼) ↦ (ℝfld
Σg (𝑥
∈ 𝐼 ↦ ((𝑓‘𝑥) · (𝑔‘𝑥)))))) |
51 | 26, 50 | eqtrd 2656 |
. . . 4
⊢ (𝐼 ∈ 𝑉 →
(·𝑖‘(ℝfldXs(𝐼 × {((subringAlg
‘ℝfld)‘ℝ)}))) = (𝑓 ∈ (ℝ ↑𝑚
𝐼), 𝑔 ∈ (ℝ ↑𝑚
𝐼) ↦
(ℝfld Σg (𝑥 ∈ 𝐼 ↦ ((𝑓‘𝑥) · (𝑔‘𝑥)))))) |
52 | 13, 51 | syl5eqr 2670 |
. . 3
⊢ (𝐼 ∈ 𝑉 →
(·𝑖‘((ℝfldXs(𝐼 × {((subringAlg
‘ℝfld)‘ℝ)})) ↾s 𝐵)) = (𝑓 ∈ (ℝ ↑𝑚
𝐼), 𝑔 ∈ (ℝ ↑𝑚
𝐼) ↦
(ℝfld Σg (𝑥 ∈ 𝐼 ↦ ((𝑓‘𝑥) · (𝑔‘𝑥)))))) |
53 | 7, 52 | syl5eqr 2670 |
. 2
⊢ (𝐼 ∈ 𝑉 →
(·𝑖‘(toℂHil‘((ℝfldXs(𝐼 × {((subringAlg
‘ℝfld)‘ℝ)})) ↾s 𝐵))) = (𝑓 ∈ (ℝ ↑𝑚 𝐼), 𝑔 ∈ (ℝ ↑𝑚 𝐼) ↦ (ℝfld
Σg (𝑥 ∈
𝐼 ↦ ((𝑓‘𝑥) · (𝑔‘𝑥)))))) |
54 | 4, 53 | eqtr2d 2657 |
1
⊢ (𝐼 ∈ 𝑉 → (𝑓 ∈ (ℝ ↑𝑚
𝐼), 𝑔 ∈ (ℝ ↑𝑚
𝐼) ↦
(ℝfld Σg (𝑥 ∈ 𝐼 ↦ ((𝑓‘𝑥) · (𝑔‘𝑥))))) =
(·𝑖‘𝐻)) |