Step | Hyp | Ref
| Expression |
1 | | xpsval.t |
. 2
⊢ 𝑇 = (𝑅 ×s 𝑆) |
2 | | xpsval.1 |
. . . 4
⊢ (𝜑 → 𝑅 ∈ 𝑉) |
3 | | elex 3212 |
. . . 4
⊢ (𝑅 ∈ 𝑉 → 𝑅 ∈ V) |
4 | 2, 3 | syl 17 |
. . 3
⊢ (𝜑 → 𝑅 ∈ V) |
5 | | xpsval.2 |
. . . 4
⊢ (𝜑 → 𝑆 ∈ 𝑊) |
6 | | elex 3212 |
. . . 4
⊢ (𝑆 ∈ 𝑊 → 𝑆 ∈ V) |
7 | 5, 6 | syl 17 |
. . 3
⊢ (𝜑 → 𝑆 ∈ V) |
8 | | fveq2 6191 |
. . . . . . . . 9
⊢ (𝑟 = 𝑅 → (Base‘𝑟) = (Base‘𝑅)) |
9 | | xpsval.x |
. . . . . . . . 9
⊢ 𝑋 = (Base‘𝑅) |
10 | 8, 9 | syl6eqr 2674 |
. . . . . . . 8
⊢ (𝑟 = 𝑅 → (Base‘𝑟) = 𝑋) |
11 | | fveq2 6191 |
. . . . . . . . 9
⊢ (𝑠 = 𝑆 → (Base‘𝑠) = (Base‘𝑆)) |
12 | | xpsval.y |
. . . . . . . . 9
⊢ 𝑌 = (Base‘𝑆) |
13 | 11, 12 | syl6eqr 2674 |
. . . . . . . 8
⊢ (𝑠 = 𝑆 → (Base‘𝑠) = 𝑌) |
14 | | mpt2eq12 6715 |
. . . . . . . 8
⊢
(((Base‘𝑟) =
𝑋 ∧ (Base‘𝑠) = 𝑌) → (𝑥 ∈ (Base‘𝑟), 𝑦 ∈ (Base‘𝑠) ↦ ◡({𝑥} +𝑐 {𝑦})) = (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦}))) |
15 | 10, 13, 14 | syl2an 494 |
. . . . . . 7
⊢ ((𝑟 = 𝑅 ∧ 𝑠 = 𝑆) → (𝑥 ∈ (Base‘𝑟), 𝑦 ∈ (Base‘𝑠) ↦ ◡({𝑥} +𝑐 {𝑦})) = (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦}))) |
16 | | xpsval.f |
. . . . . . 7
⊢ 𝐹 = (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦})) |
17 | 15, 16 | syl6eqr 2674 |
. . . . . 6
⊢ ((𝑟 = 𝑅 ∧ 𝑠 = 𝑆) → (𝑥 ∈ (Base‘𝑟), 𝑦 ∈ (Base‘𝑠) ↦ ◡({𝑥} +𝑐 {𝑦})) = 𝐹) |
18 | 17 | cnveqd 5298 |
. . . . 5
⊢ ((𝑟 = 𝑅 ∧ 𝑠 = 𝑆) → ◡(𝑥 ∈ (Base‘𝑟), 𝑦 ∈ (Base‘𝑠) ↦ ◡({𝑥} +𝑐 {𝑦})) = ◡𝐹) |
19 | | fveq2 6191 |
. . . . . . . . 9
⊢ (𝑟 = 𝑅 → (Scalar‘𝑟) = (Scalar‘𝑅)) |
20 | 19 | adantr 481 |
. . . . . . . 8
⊢ ((𝑟 = 𝑅 ∧ 𝑠 = 𝑆) → (Scalar‘𝑟) = (Scalar‘𝑅)) |
21 | | xpsval.k |
. . . . . . . 8
⊢ 𝐺 = (Scalar‘𝑅) |
22 | 20, 21 | syl6eqr 2674 |
. . . . . . 7
⊢ ((𝑟 = 𝑅 ∧ 𝑠 = 𝑆) → (Scalar‘𝑟) = 𝐺) |
23 | | sneq 4187 |
. . . . . . . . 9
⊢ (𝑟 = 𝑅 → {𝑟} = {𝑅}) |
24 | | sneq 4187 |
. . . . . . . . 9
⊢ (𝑠 = 𝑆 → {𝑠} = {𝑆}) |
25 | 23, 24 | oveqan12d 6669 |
. . . . . . . 8
⊢ ((𝑟 = 𝑅 ∧ 𝑠 = 𝑆) → ({𝑟} +𝑐 {𝑠}) = ({𝑅} +𝑐 {𝑆})) |
26 | 25 | cnveqd 5298 |
. . . . . . 7
⊢ ((𝑟 = 𝑅 ∧ 𝑠 = 𝑆) → ◡({𝑟} +𝑐 {𝑠}) = ◡({𝑅} +𝑐 {𝑆})) |
27 | 22, 26 | oveq12d 6668 |
. . . . . 6
⊢ ((𝑟 = 𝑅 ∧ 𝑠 = 𝑆) → ((Scalar‘𝑟)Xs◡({𝑟} +𝑐 {𝑠})) = (𝐺Xs◡({𝑅} +𝑐 {𝑆}))) |
28 | | xpsval.u |
. . . . . 6
⊢ 𝑈 = (𝐺Xs◡({𝑅} +𝑐 {𝑆})) |
29 | 27, 28 | syl6eqr 2674 |
. . . . 5
⊢ ((𝑟 = 𝑅 ∧ 𝑠 = 𝑆) → ((Scalar‘𝑟)Xs◡({𝑟} +𝑐 {𝑠})) = 𝑈) |
30 | 18, 29 | oveq12d 6668 |
. . . 4
⊢ ((𝑟 = 𝑅 ∧ 𝑠 = 𝑆) → (◡(𝑥 ∈ (Base‘𝑟), 𝑦 ∈ (Base‘𝑠) ↦ ◡({𝑥} +𝑐 {𝑦})) “s
((Scalar‘𝑟)Xs◡({𝑟} +𝑐 {𝑠}))) = (◡𝐹 “s 𝑈)) |
31 | | df-xps 16170 |
. . . 4
⊢
×s = (𝑟 ∈ V, 𝑠 ∈ V ↦ (◡(𝑥 ∈ (Base‘𝑟), 𝑦 ∈ (Base‘𝑠) ↦ ◡({𝑥} +𝑐 {𝑦})) “s
((Scalar‘𝑟)Xs◡({𝑟} +𝑐 {𝑠})))) |
32 | | ovex 6678 |
. . . 4
⊢ (◡𝐹 “s 𝑈) ∈ V |
33 | 30, 31, 32 | ovmpt2a 6791 |
. . 3
⊢ ((𝑅 ∈ V ∧ 𝑆 ∈ V) → (𝑅 ×s
𝑆) = (◡𝐹 “s 𝑈)) |
34 | 4, 7, 33 | syl2anc 693 |
. 2
⊢ (𝜑 → (𝑅 ×s 𝑆) = (◡𝐹 “s 𝑈)) |
35 | 1, 34 | syl5eq 2668 |
1
⊢ (𝜑 → 𝑇 = (◡𝐹 “s 𝑈)) |