| 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 17551 | . . . 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 5191 | . . . . 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 5185 ‘cfv 6525 (class class class)co 7400 ∈ cmpo 7402 [cec 8680 Basecbs 17257 “s cimas 17546 /s cqus 17547 |
| 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-mpt 5186 df-id 5546 df-xp 5657 df-rel 5658 df-cnv 5659 df-co 5660 df-dm 5661 df-rn 5662 df-res 5663 df-ima 5664 df-iota 6481 df-fun 6527 df-fv 6533 df-ov 7403 df-oprab 7404 df-mpo 7405 df-ec 8684 df-qus 17551 |
| This theorem is referenced by: qusin 17586 qusbas 17587 quss 17588 qusaddval 17595 qusaddf 17596 qusmulval 17597 qusmulf 17598 qusgrp2 19112 qusrng 20246 qusring2 20404 qustps 23836 qustgpopn 24234 qustgplem 24235 qustgphaus 24237 qusvsval 33582 quslmod 33588 quslmhm 33589 |
| Copyright terms: Public domain | W3C validator |