![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > qusaddvallem | Structured version Visualization version GIF version |
Description: Value of an operation defined on a quotient structure. (Contributed by Mario Carneiro, 24-Feb-2015.) |
Ref | Expression |
---|---|
qusaddf.u | โข (๐ โ ๐ = (๐ /s โผ )) |
qusaddf.v | โข (๐ โ ๐ = (Baseโ๐ )) |
qusaddf.r | โข (๐ โ โผ Er ๐) |
qusaddf.z | โข (๐ โ ๐ โ ๐) |
qusaddf.e | โข (๐ โ ((๐ โผ ๐ โง ๐ โผ ๐) โ (๐ ยท ๐) โผ (๐ ยท ๐))) |
qusaddf.c | โข ((๐ โง (๐ โ ๐ โง ๐ โ ๐)) โ (๐ ยท ๐) โ ๐) |
qusaddflem.f | โข ๐น = (๐ฅ โ ๐ โฆ [๐ฅ] โผ ) |
qusaddflem.g | โข (๐ โ โ = โช ๐ โ ๐ โช ๐ โ ๐ {โจโจ(๐นโ๐), (๐นโ๐)โฉ, (๐นโ(๐ ยท ๐))โฉ}) |
Ref | Expression |
---|---|
qusaddvallem | โข ((๐ โง ๐ โ ๐ โง ๐ โ ๐) โ ([๐] โผ โ [๐] โผ ) = [(๐ ยท ๐)] โผ ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | qusaddf.u | . . . 4 โข (๐ โ ๐ = (๐ /s โผ )) | |
2 | qusaddf.v | . . . 4 โข (๐ โ ๐ = (Baseโ๐ )) | |
3 | qusaddflem.f | . . . 4 โข ๐น = (๐ฅ โ ๐ โฆ [๐ฅ] โผ ) | |
4 | qusaddf.r | . . . . 5 โข (๐ โ โผ Er ๐) | |
5 | fvex 6903 | . . . . . 6 โข (Baseโ๐ ) โ V | |
6 | 2, 5 | eqeltrdi 2839 | . . . . 5 โข (๐ โ ๐ โ V) |
7 | erex 8729 | . . . . 5 โข ( โผ Er ๐ โ (๐ โ V โ โผ โ V)) | |
8 | 4, 6, 7 | sylc 65 | . . . 4 โข (๐ โ โผ โ V) |
9 | qusaddf.z | . . . 4 โข (๐ โ ๐ โ ๐) | |
10 | 1, 2, 3, 8, 9 | quslem 17493 | . . 3 โข (๐ โ ๐น:๐โontoโ(๐ / โผ )) |
11 | qusaddf.c | . . . 4 โข ((๐ โง (๐ โ ๐ โง ๐ โ ๐)) โ (๐ ยท ๐) โ ๐) | |
12 | qusaddf.e | . . . 4 โข (๐ โ ((๐ โผ ๐ โง ๐ โผ ๐) โ (๐ ยท ๐) โผ (๐ ยท ๐))) | |
13 | 4, 6, 3, 11, 12 | ercpbl 17499 | . . 3 โข ((๐ โง (๐ โ ๐ โง ๐ โ ๐) โง (๐ โ ๐ โง ๐ โ ๐)) โ (((๐นโ๐) = (๐นโ๐) โง (๐นโ๐) = (๐นโ๐)) โ (๐นโ(๐ ยท ๐)) = (๐นโ(๐ ยท ๐)))) |
14 | qusaddflem.g | . . 3 โข (๐ โ โ = โช ๐ โ ๐ โช ๐ โ ๐ {โจโจ(๐นโ๐), (๐นโ๐)โฉ, (๐นโ(๐ ยท ๐))โฉ}) | |
15 | 10, 13, 14 | imasaddvallem 17479 | . 2 โข ((๐ โง ๐ โ ๐ โง ๐ โ ๐) โ ((๐นโ๐) โ (๐นโ๐)) = (๐นโ(๐ ยท ๐))) |
16 | 4 | 3ad2ant1 1131 | . . . 4 โข ((๐ โง ๐ โ ๐ โง ๐ โ ๐) โ โผ Er ๐) |
17 | 6 | 3ad2ant1 1131 | . . . 4 โข ((๐ โง ๐ โ ๐ โง ๐ โ ๐) โ ๐ โ V) |
18 | 16, 17, 3 | divsfval 17497 | . . 3 โข ((๐ โง ๐ โ ๐ โง ๐ โ ๐) โ (๐นโ๐) = [๐] โผ ) |
19 | 16, 17, 3 | divsfval 17497 | . . 3 โข ((๐ โง ๐ โ ๐ โง ๐ โ ๐) โ (๐นโ๐) = [๐] โผ ) |
20 | 18, 19 | oveq12d 7429 | . 2 โข ((๐ โง ๐ โ ๐ โง ๐ โ ๐) โ ((๐นโ๐) โ (๐นโ๐)) = ([๐] โผ โ [๐] โผ )) |
21 | 16, 17, 3 | divsfval 17497 | . 2 โข ((๐ โง ๐ โ ๐ โง ๐ โ ๐) โ (๐นโ(๐ ยท ๐)) = [(๐ ยท ๐)] โผ ) |
22 | 15, 20, 21 | 3eqtr3d 2778 | 1 โข ((๐ โง ๐ โ ๐ โง ๐ โ ๐) โ ([๐] โผ โ [๐] โผ ) = [(๐ ยท ๐)] โผ ) |
Colors of variables: wff setvar class |
Syntax hints: โ wi 4 โง wa 394 โง w3a 1085 = wceq 1539 โ wcel 2104 Vcvv 3472 {csn 4627 โจcop 4633 โช ciun 4996 class class class wbr 5147 โฆ cmpt 5230 โcfv 6542 (class class class)co 7411 Er wer 8702 [cec 8703 / cqs 8704 Basecbs 17148 /s cqus 17455 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1911 ax-6 1969 ax-7 2009 ax-8 2106 ax-9 2114 ax-10 2135 ax-11 2152 ax-12 2169 ax-ext 2701 ax-sep 5298 ax-nul 5305 ax-pow 5362 ax-pr 5426 ax-un 7727 |
This theorem depends on definitions: df-bi 206 df-an 395 df-or 844 df-3an 1087 df-tru 1542 df-fal 1552 df-ex 1780 df-nf 1784 df-sb 2066 df-mo 2532 df-eu 2561 df-clab 2708 df-cleq 2722 df-clel 2808 df-nfc 2883 df-ne 2939 df-ral 3060 df-rex 3069 df-rab 3431 df-v 3474 df-sbc 3777 df-csb 3893 df-dif 3950 df-un 3952 df-in 3954 df-ss 3964 df-nul 4322 df-if 4528 df-pw 4603 df-sn 4628 df-pr 4630 df-op 4634 df-uni 4908 df-iun 4998 df-br 5148 df-opab 5210 df-mpt 5231 df-id 5573 df-xp 5681 df-rel 5682 df-cnv 5683 df-co 5684 df-dm 5685 df-rn 5686 df-res 5687 df-ima 5688 df-iota 6494 df-fun 6544 df-fn 6545 df-f 6546 df-fo 6548 df-fv 6550 df-ov 7414 df-er 8705 df-ec 8707 df-qs 8711 |
This theorem is referenced by: qusaddval 17503 qusmulval 17505 |
Copyright terms: Public domain | W3C validator |