| Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
| Mirrors > Home > ILE Home > Th. List > 2idlval | GIF version | ||
| Description: Definition of a two-sided ideal. (Contributed by Mario Carneiro, 14-Jun-2015.) |
| Ref | Expression |
|---|---|
| 2idlval.i | ⊢ 𝐼 = (LIdeal‘𝑅) |
| 2idlval.o | ⊢ 𝑂 = (oppr‘𝑅) |
| 2idlval.j | ⊢ 𝐽 = (LIdeal‘𝑂) |
| 2idlval.t | ⊢ 𝑇 = (2Ideal‘𝑅) |
| Ref | Expression |
|---|---|
| 2idlval | ⊢ 𝑇 = (𝐼 ∩ 𝐽) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | 2idlval.t | . . . 4 ⊢ 𝑇 = (2Ideal‘𝑅) | |
| 2 | 1 | 2idlmex 14518 | . . 3 ⊢ (𝑥 ∈ 𝑇 → 𝑅 ∈ V) |
| 3 | elinel1 3393 | . . . 4 ⊢ (𝑥 ∈ (𝐼 ∩ 𝐽) → 𝑥 ∈ 𝐼) | |
| 4 | 2idlval.i | . . . . 5 ⊢ 𝐼 = (LIdeal‘𝑅) | |
| 5 | 4 | lidlmex 14492 | . . . 4 ⊢ (𝑥 ∈ 𝐼 → 𝑅 ∈ V) |
| 6 | 3, 5 | syl 14 | . . 3 ⊢ (𝑥 ∈ (𝐼 ∩ 𝐽) → 𝑅 ∈ V) |
| 7 | lidlex 14490 | . . . . . . . 8 ⊢ (𝑅 ∈ V → (LIdeal‘𝑅) ∈ V) | |
| 8 | 4, 7 | eqeltrid 2318 | . . . . . . 7 ⊢ (𝑅 ∈ V → 𝐼 ∈ V) |
| 9 | inex1g 4225 | . . . . . . 7 ⊢ (𝐼 ∈ V → (𝐼 ∩ 𝐽) ∈ V) | |
| 10 | 8, 9 | syl 14 | . . . . . 6 ⊢ (𝑅 ∈ V → (𝐼 ∩ 𝐽) ∈ V) |
| 11 | fveq2 5639 | . . . . . . . . 9 ⊢ (𝑟 = 𝑅 → (LIdeal‘𝑟) = (LIdeal‘𝑅)) | |
| 12 | 11, 4 | eqtr4di 2282 | . . . . . . . 8 ⊢ (𝑟 = 𝑅 → (LIdeal‘𝑟) = 𝐼) |
| 13 | fveq2 5639 | . . . . . . . . . . 11 ⊢ (𝑟 = 𝑅 → (oppr‘𝑟) = (oppr‘𝑅)) | |
| 14 | 2idlval.o | . . . . . . . . . . 11 ⊢ 𝑂 = (oppr‘𝑅) | |
| 15 | 13, 14 | eqtr4di 2282 | . . . . . . . . . 10 ⊢ (𝑟 = 𝑅 → (oppr‘𝑟) = 𝑂) |
| 16 | 15 | fveq2d 5643 | . . . . . . . . 9 ⊢ (𝑟 = 𝑅 → (LIdeal‘(oppr‘𝑟)) = (LIdeal‘𝑂)) |
| 17 | 2idlval.j | . . . . . . . . 9 ⊢ 𝐽 = (LIdeal‘𝑂) | |
| 18 | 16, 17 | eqtr4di 2282 | . . . . . . . 8 ⊢ (𝑟 = 𝑅 → (LIdeal‘(oppr‘𝑟)) = 𝐽) |
| 19 | 12, 18 | ineq12d 3409 | . . . . . . 7 ⊢ (𝑟 = 𝑅 → ((LIdeal‘𝑟) ∩ (LIdeal‘(oppr‘𝑟))) = (𝐼 ∩ 𝐽)) |
| 20 | df-2idl 14517 | . . . . . . 7 ⊢ 2Ideal = (𝑟 ∈ V ↦ ((LIdeal‘𝑟) ∩ (LIdeal‘(oppr‘𝑟)))) | |
| 21 | 19, 20 | fvmptg 5722 | . . . . . 6 ⊢ ((𝑅 ∈ V ∧ (𝐼 ∩ 𝐽) ∈ V) → (2Ideal‘𝑅) = (𝐼 ∩ 𝐽)) |
| 22 | 10, 21 | mpdan 421 | . . . . 5 ⊢ (𝑅 ∈ V → (2Ideal‘𝑅) = (𝐼 ∩ 𝐽)) |
| 23 | 1, 22 | eqtrid 2276 | . . . 4 ⊢ (𝑅 ∈ V → 𝑇 = (𝐼 ∩ 𝐽)) |
| 24 | 23 | eleq2d 2301 | . . 3 ⊢ (𝑅 ∈ V → (𝑥 ∈ 𝑇 ↔ 𝑥 ∈ (𝐼 ∩ 𝐽))) |
| 25 | 2, 6, 24 | pm5.21nii 711 | . 2 ⊢ (𝑥 ∈ 𝑇 ↔ 𝑥 ∈ (𝐼 ∩ 𝐽)) |
| 26 | 25 | eqriv 2228 | 1 ⊢ 𝑇 = (𝐼 ∩ 𝐽) |
| Colors of variables: wff set class |
| Syntax hints: = wceq 1397 ∈ wcel 2202 Vcvv 2802 ∩ cin 3199 ‘cfv 5326 opprcoppr 14083 LIdealclidl 14484 2Idealc2idl 14516 |
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 106 ax-ia2 107 ax-ia3 108 ax-in1 619 ax-in2 620 ax-io 716 ax-5 1495 ax-7 1496 ax-gen 1497 ax-ie1 1541 ax-ie2 1542 ax-8 1552 ax-10 1553 ax-11 1554 ax-i12 1555 ax-bndl 1557 ax-4 1558 ax-17 1574 ax-i9 1578 ax-ial 1582 ax-i5r 1583 ax-13 2204 ax-14 2205 ax-ext 2213 ax-coll 4204 ax-sep 4207 ax-pow 4264 ax-pr 4299 ax-un 4530 ax-setind 4635 ax-cnex 8123 ax-resscn 8124 ax-1re 8126 ax-addrcl 8129 |
| This theorem depends on definitions: df-bi 117 df-3an 1006 df-tru 1400 df-fal 1403 df-nf 1509 df-sb 1811 df-eu 2082 df-mo 2083 df-clab 2218 df-cleq 2224 df-clel 2227 df-nfc 2363 df-ne 2403 df-ral 2515 df-rex 2516 df-reu 2517 df-rab 2519 df-v 2804 df-sbc 3032 df-csb 3128 df-dif 3202 df-un 3204 df-in 3206 df-ss 3213 df-pw 3654 df-sn 3675 df-pr 3676 df-op 3678 df-uni 3894 df-int 3929 df-iun 3972 df-br 4089 df-opab 4151 df-mpt 4152 df-id 4390 df-xp 4731 df-rel 4732 df-cnv 4733 df-co 4734 df-dm 4735 df-rn 4736 df-res 4737 df-ima 4738 df-iota 5286 df-fun 5328 df-fn 5329 df-f 5330 df-f1 5331 df-fo 5332 df-f1o 5333 df-fv 5334 df-ov 6021 df-oprab 6022 df-mpo 6023 df-inn 9144 df-2 9202 df-3 9203 df-4 9204 df-5 9205 df-6 9206 df-7 9207 df-8 9208 df-ndx 13087 df-slot 13088 df-base 13090 df-sets 13091 df-iress 13092 df-mulr 13176 df-sca 13178 df-vsca 13179 df-ip 13180 df-lssm 14370 df-sra 14452 df-rgmod 14453 df-lidl 14486 df-2idl 14517 |
| This theorem is referenced by: (None) |
| Copyright terms: Public domain | W3C validator |