![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > rngqiprngimfv | Structured version Visualization version GIF version |
Description: The value of the function πΉ at an element of (the base set of) a non-unital ring. (Contributed by AV, 24-Feb-2025.) |
Ref | Expression |
---|---|
rng2idlring.r | β’ (π β π β Rng) |
rng2idlring.i | β’ (π β πΌ β (2Idealβπ )) |
rng2idlring.j | β’ π½ = (π βΎs πΌ) |
rng2idlring.u | β’ (π β π½ β Ring) |
rng2idlring.b | β’ π΅ = (Baseβπ ) |
rng2idlring.t | β’ Β· = (.rβπ ) |
rng2idlring.1 | β’ 1 = (1rβπ½) |
rngqiprngim.g | β’ βΌ = (π ~QG πΌ) |
rngqiprngim.q | β’ π = (π /s βΌ ) |
rngqiprngim.c | β’ πΆ = (Baseβπ) |
rngqiprngim.p | β’ π = (π Γs π½) |
rngqiprngim.f | β’ πΉ = (π₯ β π΅ β¦ β¨[π₯] βΌ , ( 1 Β· π₯)β©) |
Ref | Expression |
---|---|
rngqiprngimfv | β’ ((π β§ π΄ β π΅) β (πΉβπ΄) = β¨[π΄] βΌ , ( 1 Β· π΄)β©) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | rngqiprngim.f | . . 3 β’ πΉ = (π₯ β π΅ β¦ β¨[π₯] βΌ , ( 1 Β· π₯)β©) | |
2 | 1 | a1i 11 | . 2 β’ ((π β§ π΄ β π΅) β πΉ = (π₯ β π΅ β¦ β¨[π₯] βΌ , ( 1 Β· π₯)β©)) |
3 | eceq1 8756 | . . . 4 β’ (π₯ = π΄ β [π₯] βΌ = [π΄] βΌ ) | |
4 | oveq2 7421 | . . . 4 β’ (π₯ = π΄ β ( 1 Β· π₯) = ( 1 Β· π΄)) | |
5 | 3, 4 | opeq12d 4878 | . . 3 β’ (π₯ = π΄ β β¨[π₯] βΌ , ( 1 Β· π₯)β© = β¨[π΄] βΌ , ( 1 Β· π΄)β©) |
6 | 5 | adantl 480 | . 2 β’ (((π β§ π΄ β π΅) β§ π₯ = π΄) β β¨[π₯] βΌ , ( 1 Β· π₯)β© = β¨[π΄] βΌ , ( 1 Β· π΄)β©) |
7 | simpr 483 | . 2 β’ ((π β§ π΄ β π΅) β π΄ β π΅) | |
8 | opex 5461 | . . 3 β’ β¨[π΄] βΌ , ( 1 Β· π΄)β© β V | |
9 | 8 | a1i 11 | . 2 β’ ((π β§ π΄ β π΅) β β¨[π΄] βΌ , ( 1 Β· π΄)β© β V) |
10 | 2, 6, 7, 9 | fvmptd 7005 | 1 β’ ((π β§ π΄ β π΅) β (πΉβπ΄) = β¨[π΄] βΌ , ( 1 Β· π΄)β©) |
Colors of variables: wff setvar class |
Syntax hints: β wi 4 β§ wa 394 = wceq 1533 β wcel 2098 Vcvv 3463 β¨cop 4631 β¦ cmpt 5227 βcfv 6543 (class class class)co 7413 [cec 8716 Basecbs 17174 βΎs cress 17203 .rcmulr 17228 /s cqus 17481 Γs cxps 17482 ~QG cqg 19076 Rngcrng 20091 1rcur 20120 Ringcrg 20172 2Idealc2idl 21142 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1789 ax-4 1803 ax-5 1905 ax-6 1963 ax-7 2003 ax-8 2100 ax-9 2108 ax-10 2129 ax-11 2146 ax-12 2166 ax-ext 2696 ax-sep 5295 ax-nul 5302 ax-pr 5424 |
This theorem depends on definitions: df-bi 206 df-an 395 df-or 846 df-3an 1086 df-tru 1536 df-fal 1546 df-ex 1774 df-nf 1778 df-sb 2060 df-mo 2528 df-eu 2557 df-clab 2703 df-cleq 2717 df-clel 2802 df-nfc 2877 df-ral 3052 df-rex 3061 df-rab 3420 df-v 3465 df-sbc 3771 df-csb 3887 df-dif 3944 df-un 3946 df-in 3948 df-ss 3958 df-nul 4320 df-if 4526 df-sn 4626 df-pr 4628 df-op 4632 df-uni 4905 df-br 5145 df-opab 5207 df-mpt 5228 df-id 5571 df-xp 5679 df-rel 5680 df-cnv 5681 df-co 5682 df-dm 5683 df-rn 5684 df-res 5685 df-ima 5686 df-iota 6495 df-fun 6545 df-fv 6551 df-ov 7416 df-ec 8720 |
This theorem is referenced by: rngqiprngghm 21188 rngqiprngimf1 21189 rngqiprngimfo 21190 rngqiprnglin 21191 rngqiprngfu 21206 |
Copyright terms: Public domain | W3C validator |