| Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
| Mirrors > Home > MPE Home > Th. List > pwsval | Structured version Visualization version GIF version | ||
| Description: Value of a structure power. (Contributed by Mario Carneiro, 11-Jan-2015.) |
| Ref | Expression |
|---|---|
| pwsval.y | ⊢ 𝑌 = (𝑅 ↑s 𝐼) |
| pwsval.f | ⊢ 𝐹 = (Scalar‘𝑅) |
| Ref | Expression |
|---|---|
| pwsval | ⊢ ((𝑅 ∈ 𝑉 ∧ 𝐼 ∈ 𝑊) → 𝑌 = (𝐹Xs(𝐼 × {𝑅}))) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | pwsval.y | . 2 ⊢ 𝑌 = (𝑅 ↑s 𝐼) | |
| 2 | elex 3478 | . . 3 ⊢ (𝑅 ∈ 𝑉 → 𝑅 ∈ V) | |
| 3 | elex 3478 | . . 3 ⊢ (𝐼 ∈ 𝑊 → 𝐼 ∈ V) | |
| 4 | simpl 487 | . . . . . . 7 ⊢ ((𝑟 = 𝑅 ∧ 𝑖 = 𝐼) → 𝑟 = 𝑅) | |
| 5 | 4 | fveq2d 6875 | . . . . . 6 ⊢ ((𝑟 = 𝑅 ∧ 𝑖 = 𝐼) → (Scalar‘𝑟) = (Scalar‘𝑅)) |
| 6 | pwsval.f | . . . . . 6 ⊢ 𝐹 = (Scalar‘𝑅) | |
| 7 | 5, 6 | eqtr4di 2818 | . . . . 5 ⊢ ((𝑟 = 𝑅 ∧ 𝑖 = 𝐼) → (Scalar‘𝑟) = 𝐹) |
| 8 | id 23 | . . . . . 6 ⊢ (𝑖 = 𝐼 → 𝑖 = 𝐼) | |
| 9 | sneq 4595 | . . . . . 6 ⊢ (𝑟 = 𝑅 → {𝑟} = {𝑅}) | |
| 10 | xpeq12 5676 | . . . . . 6 ⊢ ((𝑖 = 𝐼 ∧ {𝑟} = {𝑅}) → (𝑖 × {𝑟}) = (𝐼 × {𝑅})) | |
| 11 | 8, 9, 10 | syl2anr 608 | . . . . 5 ⊢ ((𝑟 = 𝑅 ∧ 𝑖 = 𝐼) → (𝑖 × {𝑟}) = (𝐼 × {𝑅})) |
| 12 | 7, 11 | oveq12d 7418 | . . . 4 ⊢ ((𝑟 = 𝑅 ∧ 𝑖 = 𝐼) → ((Scalar‘𝑟)Xs(𝑖 × {𝑟})) = (𝐹Xs(𝐼 × {𝑅}))) |
| 13 | df-pws 17490 | . . . 4 ⊢ ↑s = (𝑟 ∈ V, 𝑖 ∈ V ↦ ((Scalar‘𝑟)Xs(𝑖 × {𝑟}))) | |
| 14 | ovex 7433 | . . . 4 ⊢ (𝐹Xs(𝐼 × {𝑅})) ∈ V | |
| 15 | 12, 13, 14 | ovmpoa 7555 | . . 3 ⊢ ((𝑅 ∈ V ∧ 𝐼 ∈ V) → (𝑅 ↑s 𝐼) = (𝐹Xs(𝐼 × {𝑅}))) |
| 16 | 2, 3, 15 | syl2an 607 | . 2 ⊢ ((𝑅 ∈ 𝑉 ∧ 𝐼 ∈ 𝑊) → (𝑅 ↑s 𝐼) = (𝐹Xs(𝐼 × {𝑅}))) |
| 17 | 1, 16 | eqtrid 2812 | 1 ⊢ ((𝑅 ∈ 𝑉 ∧ 𝐼 ∈ 𝑊) → 𝑌 = (𝐹Xs(𝐼 × {𝑅}))) |
| Colors of variables: wff setvar class |
| Syntax hints: → wi 4 ∧ wa 400 = wceq 1563 ∈ wcel 2145 Vcvv 3457 {csn 4585 × cxp 5649 ‘cfv 6525 (class class class)co 7400 Scalarcsca 17301 Xscprds 17486 ↑s cpws 17487 |
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1818 ax-4 1832 ax-5 1933 ax-6 1990 ax-7 2031 ax-8 2147 ax-9 2155 ax-10 2178 ax-11 2194 ax-12 2215 ax-ext 2737 ax-sep 5250 ax-nul 5260 ax-pr 5394 |
| This theorem depends on definitions: df-bi 210 df-an 401 df-or 861 df-3an 1103 df-tru 1566 df-fal 1576 df-ex 1803 df-nf 1807 df-sb 2094 df-mo 2569 df-eu 2599 df-clab 2744 df-cleq 2757 df-clel 2840 df-nfc 2914 df-ne 2961 df-ral 3080 df-rex 3090 df-rab 3418 df-v 3459 df-sbc 3748 df-dif 3910 df-un 3912 df-in 3914 df-ss 3924 df-nul 4289 df-if 4484 df-sn 4586 df-pr 4588 df-op 4592 df-uni 4868 df-br 5105 df-opab 5167 df-id 5546 df-xp 5657 df-rel 5658 df-cnv 5659 df-co 5660 df-dm 5661 df-iota 6481 df-fun 6527 df-fv 6533 df-ov 7403 df-oprab 7404 df-mpo 7405 df-pws 17490 |
| This theorem is referenced by: pwsbas 17528 pwsplusgval 17532 pwsmulrval 17533 pwsle 17534 pwsvscafval 17536 pwssca 17538 pwsmnd 18818 pws0g 18819 pwspjmhm 18877 pwsgrp 19106 pwsinvg 19107 pwscmn 19921 pwsabl 19922 pwsgsum 20040 pwsring 20393 pws1 20394 pwscrng 20395 pwsmgp 20396 pwslmod 21057 frlmpws 21857 frlmlss 21858 frlmpwsfi 21859 frlmbas 21862 frlmip 21885 pwstps 23744 resspwsds 24486 pwsxms 24646 pwsms 24647 rrxprds 25505 cnpwstotbnd 38303 repwsmet 38340 rrnequiv 38341 |
| Copyright terms: Public domain | W3C validator |