![]() |
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 16632 | . . . 4 ⊢ /s = (𝑟 ∈ V, 𝑒 ∈ V ↦ ((𝑥 ∈ (Base‘𝑟) ↦ [𝑥]𝑒) “s 𝑟)) | |
3 | 2 | a1i 11 | . . 3 ⊢ (𝜑 → /s = (𝑟 ∈ V, 𝑒 ∈ V ↦ ((𝑥 ∈ (Base‘𝑟) ↦ [𝑥]𝑒) “s 𝑟))) |
4 | simprl 758 | . . . . . . . 8 ⊢ ((𝜑 ∧ (𝑟 = 𝑅 ∧ 𝑒 = ∼ )) → 𝑟 = 𝑅) | |
5 | 4 | fveq2d 6497 | . . . . . . 7 ⊢ ((𝜑 ∧ (𝑟 = 𝑅 ∧ 𝑒 = ∼ )) → (Base‘𝑟) = (Base‘𝑅)) |
6 | qusval.v | . . . . . . . 8 ⊢ (𝜑 → 𝑉 = (Base‘𝑅)) | |
7 | 6 | adantr 473 | . . . . . . 7 ⊢ ((𝜑 ∧ (𝑟 = 𝑅 ∧ 𝑒 = ∼ )) → 𝑉 = (Base‘𝑅)) |
8 | 5, 7 | eqtr4d 2811 | . . . . . 6 ⊢ ((𝜑 ∧ (𝑟 = 𝑅 ∧ 𝑒 = ∼ )) → (Base‘𝑟) = 𝑉) |
9 | eceq2 8123 | . . . . . . 7 ⊢ (𝑒 = ∼ → [𝑥]𝑒 = [𝑥] ∼ ) | |
10 | 9 | ad2antll 716 | . . . . . 6 ⊢ ((𝜑 ∧ (𝑟 = 𝑅 ∧ 𝑒 = ∼ )) → [𝑥]𝑒 = [𝑥] ∼ ) |
11 | 8, 10 | mpteq12dv 5006 | . . . . 5 ⊢ ((𝜑 ∧ (𝑟 = 𝑅 ∧ 𝑒 = ∼ )) → (𝑥 ∈ (Base‘𝑟) ↦ [𝑥]𝑒) = (𝑥 ∈ 𝑉 ↦ [𝑥] ∼ )) |
12 | qusval.f | . . . . 5 ⊢ 𝐹 = (𝑥 ∈ 𝑉 ↦ [𝑥] ∼ ) | |
13 | 11, 12 | syl6eqr 2826 | . . . 4 ⊢ ((𝜑 ∧ (𝑟 = 𝑅 ∧ 𝑒 = ∼ )) → (𝑥 ∈ (Base‘𝑟) ↦ [𝑥]𝑒) = 𝐹) |
14 | 13, 4 | oveq12d 6988 | . . 3 ⊢ ((𝜑 ∧ (𝑟 = 𝑅 ∧ 𝑒 = ∼ )) → ((𝑥 ∈ (Base‘𝑟) ↦ [𝑥]𝑒) “s 𝑟) = (𝐹 “s 𝑅)) |
15 | qusval.r | . . . 4 ⊢ (𝜑 → 𝑅 ∈ 𝑍) | |
16 | 15 | elexd 3429 | . . 3 ⊢ (𝜑 → 𝑅 ∈ V) |
17 | qusval.e | . . . 4 ⊢ (𝜑 → ∼ ∈ 𝑊) | |
18 | 17 | elexd 3429 | . . 3 ⊢ (𝜑 → ∼ ∈ V) |
19 | ovexd 7004 | . . 3 ⊢ (𝜑 → (𝐹 “s 𝑅) ∈ V) | |
20 | 3, 14, 16, 18, 19 | ovmpod 7112 | . 2 ⊢ (𝜑 → (𝑅 /s ∼ ) = (𝐹 “s 𝑅)) |
21 | 1, 20 | eqtrd 2808 | 1 ⊢ (𝜑 → 𝑈 = (𝐹 “s 𝑅)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 387 = wceq 1507 ∈ wcel 2050 Vcvv 3409 ↦ cmpt 5002 ‘cfv 6182 (class class class)co 6970 ∈ cmpo 6972 [cec 8081 Basecbs 16333 “s cimas 16627 /s cqus 16628 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1758 ax-4 1772 ax-5 1869 ax-6 1928 ax-7 1965 ax-8 2052 ax-9 2059 ax-10 2079 ax-11 2093 ax-12 2106 ax-13 2301 ax-ext 2744 ax-sep 5054 ax-nul 5061 ax-pr 5180 |
This theorem depends on definitions: df-bi 199 df-an 388 df-or 834 df-3an 1070 df-tru 1510 df-ex 1743 df-nf 1747 df-sb 2016 df-mo 2547 df-eu 2584 df-clab 2753 df-cleq 2765 df-clel 2840 df-nfc 2912 df-ral 3087 df-rex 3088 df-rab 3091 df-v 3411 df-sbc 3676 df-dif 3826 df-un 3828 df-in 3830 df-ss 3837 df-nul 4173 df-if 4345 df-sn 4436 df-pr 4438 df-op 4442 df-uni 4707 df-br 4924 df-opab 4986 df-mpt 5003 df-id 5306 df-xp 5407 df-rel 5408 df-cnv 5409 df-co 5410 df-dm 5411 df-rn 5412 df-res 5413 df-ima 5414 df-iota 6146 df-fun 6184 df-fv 6190 df-ov 6973 df-oprab 6974 df-mpo 6975 df-ec 8085 df-qus 16632 |
This theorem is referenced by: qusin 16667 qusbas 16668 quss 16669 qusaddval 16676 qusaddf 16677 qusmulval 16678 qusmulf 16679 qusgrp2 17998 qusring2 19087 qustps 22028 qustgpopn 22425 qustgplem 22426 qustgphaus 22428 qusscaval 30600 quslmod 30602 quslmhm 30603 |
Copyright terms: Public domain | W3C validator |