| Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
| Mirrors > Home > MPE Home > Th. List > qusval | Structured version Visualization version GIF version | ||
| Description: Value of a quotient structure. (Contributed by Mario Carneiro, 23-Feb-2015.) |
| Ref | Expression |
|---|---|
| qusval.u | ⊢ (𝜑 → 𝑈 = (𝑅 /s ∼ )) |
| qusval.v | ⊢ (𝜑 → 𝑉 = (Base‘𝑅)) |
| qusval.f | ⊢ 𝐹 = (𝑥 ∈ 𝑉 ↦ [𝑥] ∼ ) |
| qusval.e | ⊢ (𝜑 → ∼ ∈ 𝑊) |
| qusval.r | ⊢ (𝜑 → 𝑅 ∈ 𝑍) |
| Ref | Expression |
|---|---|
| qusval | ⊢ (𝜑 → 𝑈 = (𝐹 “s 𝑅)) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | qusval.u | . 2 ⊢ (𝜑 → 𝑈 = (𝑅 /s ∼ )) | |
| 2 | df-qus 17553 | . . . 4 ⊢ /s = (𝑟 ∈ V, 𝑒 ∈ V ↦ ((𝑥 ∈ (Base‘𝑟) ↦ [𝑥]𝑒) “s 𝑟)) | |
| 3 | 2 | a1i 11 | . . 3 ⊢ (𝜑 → /s = (𝑟 ∈ V, 𝑒 ∈ V ↦ ((𝑥 ∈ (Base‘𝑟) ↦ [𝑥]𝑒) “s 𝑟))) |
| 4 | simprl 782 | . . . . . . . 8 ⊢ ((𝜑 ∧ (𝑟 = 𝑅 ∧ 𝑒 = ∼ )) → 𝑟 = 𝑅) | |
| 5 | 4 | fveq2d 6875 | . . . . . . 7 ⊢ ((𝜑 ∧ (𝑟 = 𝑅 ∧ 𝑒 = ∼ )) → (Base‘𝑟) = (Base‘𝑅)) |
| 6 | qusval.v | . . . . . . . 8 ⊢ (𝜑 → 𝑉 = (Base‘𝑅)) | |
| 7 | 6 | adantr 485 | . . . . . . 7 ⊢ ((𝜑 ∧ (𝑟 = 𝑅 ∧ 𝑒 = ∼ )) → 𝑉 = (Base‘𝑅)) |
| 8 | 5, 7 | eqtr4d 2803 | . . . . . 6 ⊢ ((𝜑 ∧ (𝑟 = 𝑅 ∧ 𝑒 = ∼ )) → (Base‘𝑟) = 𝑉) |
| 9 | eceq2 8724 | . . . . . . 7 ⊢ (𝑒 = ∼ → [𝑥]𝑒 = [𝑥] ∼ ) | |
| 10 | 9 | ad2antll 741 | . . . . . 6 ⊢ ((𝜑 ∧ (𝑟 = 𝑅 ∧ 𝑒 = ∼ )) → [𝑥]𝑒 = [𝑥] ∼ ) |
| 11 | 8, 10 | mpteq12dv 5192 | . . . . 5 ⊢ ((𝜑 ∧ (𝑟 = 𝑅 ∧ 𝑒 = ∼ )) → (𝑥 ∈ (Base‘𝑟) ↦ [𝑥]𝑒) = (𝑥 ∈ 𝑉 ↦ [𝑥] ∼ )) |
| 12 | qusval.f | . . . . 5 ⊢ 𝐹 = (𝑥 ∈ 𝑉 ↦ [𝑥] ∼ ) | |
| 13 | 11, 12 | eqtr4di 2818 | . . . 4 ⊢ ((𝜑 ∧ (𝑟 = 𝑅 ∧ 𝑒 = ∼ )) → (𝑥 ∈ (Base‘𝑟) ↦ [𝑥]𝑒) = 𝐹) |
| 14 | 13, 4 | oveq12d 7418 | . . 3 ⊢ ((𝜑 ∧ (𝑟 = 𝑅 ∧ 𝑒 = ∼ )) → ((𝑥 ∈ (Base‘𝑟) ↦ [𝑥]𝑒) “s 𝑟) = (𝐹 “s 𝑅)) |
| 15 | qusval.r | . . . 4 ⊢ (𝜑 → 𝑅 ∈ 𝑍) | |
| 16 | 15 | elexd 3480 | . . 3 ⊢ (𝜑 → 𝑅 ∈ V) |
| 17 | qusval.e | . . . 4 ⊢ (𝜑 → ∼ ∈ 𝑊) | |
| 18 | 17 | elexd 3480 | . . 3 ⊢ (𝜑 → ∼ ∈ V) |
| 19 | ovexd 7435 | . . 3 ⊢ (𝜑 → (𝐹 “s 𝑅) ∈ V) | |
| 20 | 3, 14, 16, 18, 19 | ovmpod 7552 | . 2 ⊢ (𝜑 → (𝑅 /s ∼ ) = (𝐹 “s 𝑅)) |
| 21 | 1, 20 | eqtrd 2800 | 1 ⊢ (𝜑 → 𝑈 = (𝐹 “s 𝑅)) |
| Colors of variables: wff setvar class |
| Syntax hints: → wi 4 ∧ wa 400 = wceq 1563 ∈ wcel 2145 Vcvv 3457 ↦ cmpt 5186 ‘cfv 6525 (class class class)co 7400 ∈ cmpo 7402 [cec 8680 Basecbs 17259 “s cimas 17548 /s cqus 17549 |
| 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 5251 ax-nul 5261 ax-pr 5395 |
| 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 4869 df-br 5106 df-opab 5168 df-mpt 5187 df-id 5547 df-xp 5658 df-rel 5659 df-cnv 5660 df-co 5661 df-dm 5662 df-rn 5663 df-res 5664 df-ima 5665 df-iota 6481 df-fun 6527 df-fv 6533 df-ov 7403 df-oprab 7404 df-mpo 7405 df-ec 8684 df-qus 17553 |
| This theorem is referenced by: qusin 17588 qusbas 17589 quss 17590 qusaddval 17597 qusaddf 17598 qusmulval 17599 qusmulf 17600 qusgrp2 19115 qusrng 20249 qusring2 20407 qustps 23840 qustgpopn 24238 qustgplem 24239 qustgphaus 24241 qusvsval 33587 quslmod 33593 quslmhm 33594 |
| Copyright terms: Public domain | W3C validator |