Mathbox for Steven Nguyen |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > Mathboxes > prjspner | Structured version Visualization version GIF version |
Description: The relation used to define ℙ𝕣𝕠𝕛 (and indirectly ℙ𝕣𝕠𝕛n through df-prjspn 39986) is an equivalence relation. This is a lemma that converts the equivalence relation used in results like prjspertr 39976 and prjspersym 39978 (see prjspnerlem 39988). Several theorems are covered in one thanks to the theorems around df-er 8305. (Contributed by SN, 14-Aug-2023.) |
Ref | Expression |
---|---|
prjspner.e | ⊢ ∼ = {〈𝑥, 𝑦〉 ∣ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) ∧ ∃𝑙 ∈ 𝑆 𝑥 = (𝑙 · 𝑦))} |
prjspner.w | ⊢ 𝑊 = (𝐾 freeLMod (0...𝑁)) |
prjspner.b | ⊢ 𝐵 = ((Base‘𝑊) ∖ {(0g‘𝑊)}) |
prjspner.s | ⊢ 𝑆 = (Base‘𝐾) |
prjspner.x | ⊢ · = ( ·𝑠 ‘𝑊) |
prjspner.k | ⊢ (𝜑 → 𝐾 ∈ DivRing) |
Ref | Expression |
---|---|
prjspner | ⊢ (𝜑 → ∼ Er 𝐵) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | prjspner.k | . . . 4 ⊢ (𝜑 → 𝐾 ∈ DivRing) | |
2 | ovexd 7191 | . . . 4 ⊢ (𝜑 → (0...𝑁) ∈ V) | |
3 | prjspner.w | . . . . 5 ⊢ 𝑊 = (𝐾 freeLMod (0...𝑁)) | |
4 | 3 | frlmlvec 20539 | . . . 4 ⊢ ((𝐾 ∈ DivRing ∧ (0...𝑁) ∈ V) → 𝑊 ∈ LVec) |
5 | 1, 2, 4 | syl2anc 587 | . . 3 ⊢ (𝜑 → 𝑊 ∈ LVec) |
6 | eqid 2758 | . . . 4 ⊢ {〈𝑥, 𝑦〉 ∣ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) ∧ ∃𝑙 ∈ (Base‘(Scalar‘𝑊))𝑥 = (𝑙 · 𝑦))} = {〈𝑥, 𝑦〉 ∣ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) ∧ ∃𝑙 ∈ (Base‘(Scalar‘𝑊))𝑥 = (𝑙 · 𝑦))} | |
7 | prjspner.b | . . . 4 ⊢ 𝐵 = ((Base‘𝑊) ∖ {(0g‘𝑊)}) | |
8 | eqid 2758 | . . . 4 ⊢ (Scalar‘𝑊) = (Scalar‘𝑊) | |
9 | prjspner.x | . . . 4 ⊢ · = ( ·𝑠 ‘𝑊) | |
10 | eqid 2758 | . . . 4 ⊢ (Base‘(Scalar‘𝑊)) = (Base‘(Scalar‘𝑊)) | |
11 | 6, 7, 8, 9, 10 | prjsper 39979 | . . 3 ⊢ (𝑊 ∈ LVec → {〈𝑥, 𝑦〉 ∣ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) ∧ ∃𝑙 ∈ (Base‘(Scalar‘𝑊))𝑥 = (𝑙 · 𝑦))} Er 𝐵) |
12 | 5, 11 | syl 17 | . 2 ⊢ (𝜑 → {〈𝑥, 𝑦〉 ∣ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) ∧ ∃𝑙 ∈ (Base‘(Scalar‘𝑊))𝑥 = (𝑙 · 𝑦))} Er 𝐵) |
13 | prjspner.e | . . . 4 ⊢ ∼ = {〈𝑥, 𝑦〉 ∣ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) ∧ ∃𝑙 ∈ 𝑆 𝑥 = (𝑙 · 𝑦))} | |
14 | prjspner.s | . . . 4 ⊢ 𝑆 = (Base‘𝐾) | |
15 | 13, 3, 7, 14, 9 | prjspnerlem 39988 | . . 3 ⊢ (𝐾 ∈ DivRing → ∼ = {〈𝑥, 𝑦〉 ∣ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) ∧ ∃𝑙 ∈ (Base‘(Scalar‘𝑊))𝑥 = (𝑙 · 𝑦))}) |
16 | ereq1 8312 | . . 3 ⊢ ( ∼ = {〈𝑥, 𝑦〉 ∣ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) ∧ ∃𝑙 ∈ (Base‘(Scalar‘𝑊))𝑥 = (𝑙 · 𝑦))} → ( ∼ Er 𝐵 ↔ {〈𝑥, 𝑦〉 ∣ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) ∧ ∃𝑙 ∈ (Base‘(Scalar‘𝑊))𝑥 = (𝑙 · 𝑦))} Er 𝐵)) | |
17 | 1, 15, 16 | 3syl 18 | . 2 ⊢ (𝜑 → ( ∼ Er 𝐵 ↔ {〈𝑥, 𝑦〉 ∣ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) ∧ ∃𝑙 ∈ (Base‘(Scalar‘𝑊))𝑥 = (𝑙 · 𝑦))} Er 𝐵)) |
18 | 12, 17 | mpbird 260 | 1 ⊢ (𝜑 → ∼ Er 𝐵) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 209 ∧ wa 399 = wceq 1538 ∈ wcel 2111 ∃wrex 3071 Vcvv 3409 ∖ cdif 3857 {csn 4525 {copab 5098 ‘cfv 6340 (class class class)co 7156 Er wer 8302 0cc0 10588 ...cfz 12952 Basecbs 16554 Scalarcsca 16639 ·𝑠 cvsca 16640 0gc0g 16784 DivRingcdr 19583 LVecclvec 19955 freeLMod cfrlm 20524 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1797 ax-4 1811 ax-5 1911 ax-6 1970 ax-7 2015 ax-8 2113 ax-9 2121 ax-10 2142 ax-11 2158 ax-12 2175 ax-ext 2729 ax-rep 5160 ax-sep 5173 ax-nul 5180 ax-pow 5238 ax-pr 5302 ax-un 7465 ax-cnex 10644 ax-resscn 10645 ax-1cn 10646 ax-icn 10647 ax-addcl 10648 ax-addrcl 10649 ax-mulcl 10650 ax-mulrcl 10651 ax-mulcom 10652 ax-addass 10653 ax-mulass 10654 ax-distr 10655 ax-i2m1 10656 ax-1ne0 10657 ax-1rid 10658 ax-rnegex 10659 ax-rrecex 10660 ax-cnre 10661 ax-pre-lttri 10662 ax-pre-lttrn 10663 ax-pre-ltadd 10664 ax-pre-mulgt0 10665 |
This theorem depends on definitions: df-bi 210 df-an 400 df-or 845 df-3or 1085 df-3an 1086 df-tru 1541 df-fal 1551 df-ex 1782 df-nf 1786 df-sb 2070 df-mo 2557 df-eu 2588 df-clab 2736 df-cleq 2750 df-clel 2830 df-nfc 2901 df-ne 2952 df-nel 3056 df-ral 3075 df-rex 3076 df-reu 3077 df-rmo 3078 df-rab 3079 df-v 3411 df-sbc 3699 df-csb 3808 df-dif 3863 df-un 3865 df-in 3867 df-ss 3877 df-pss 3879 df-nul 4228 df-if 4424 df-pw 4499 df-sn 4526 df-pr 4528 df-tp 4530 df-op 4532 df-uni 4802 df-iun 4888 df-br 5037 df-opab 5099 df-mpt 5117 df-tr 5143 df-id 5434 df-eprel 5439 df-po 5447 df-so 5448 df-fr 5487 df-we 5489 df-xp 5534 df-rel 5535 df-cnv 5536 df-co 5537 df-dm 5538 df-rn 5539 df-res 5540 df-ima 5541 df-pred 6131 df-ord 6177 df-on 6178 df-lim 6179 df-suc 6180 df-iota 6299 df-fun 6342 df-fn 6343 df-f 6344 df-f1 6345 df-fo 6346 df-f1o 6347 df-fv 6348 df-riota 7114 df-ov 7159 df-oprab 7160 df-mpo 7161 df-om 7586 df-1st 7699 df-2nd 7700 df-tpos 7908 df-wrecs 7963 df-recs 8024 df-rdg 8062 df-1o 8118 df-er 8305 df-map 8424 df-ixp 8493 df-en 8541 df-dom 8542 df-sdom 8543 df-fin 8544 df-sup 8952 df-pnf 10728 df-mnf 10729 df-xr 10730 df-ltxr 10731 df-le 10732 df-sub 10923 df-neg 10924 df-nn 11688 df-2 11750 df-3 11751 df-4 11752 df-5 11753 df-6 11754 df-7 11755 df-8 11756 df-9 11757 df-n0 11948 df-z 12034 df-dec 12151 df-uz 12296 df-fz 12953 df-struct 16556 df-ndx 16557 df-slot 16558 df-base 16560 df-sets 16561 df-ress 16562 df-plusg 16649 df-mulr 16650 df-sca 16652 df-vsca 16653 df-ip 16654 df-tset 16655 df-ple 16656 df-ds 16658 df-hom 16660 df-cco 16661 df-0g 16786 df-prds 16792 df-pws 16794 df-mgm 17931 df-sgrp 17980 df-mnd 17991 df-grp 18185 df-minusg 18186 df-sbg 18187 df-subg 18356 df-mgp 19321 df-ur 19333 df-ring 19380 df-oppr 19457 df-dvdsr 19475 df-unit 19476 df-invr 19506 df-drng 19585 df-subrg 19614 df-lmod 19717 df-lss 19785 df-lvec 19956 df-sra 20025 df-rgmod 20026 df-dsmm 20510 df-frlm 20525 |
This theorem is referenced by: prjspner01 39994 prjspner1 39995 |
Copyright terms: Public domain | W3C validator |