prjspnval2 - Mathbox for Steven Nguyen

	Mathbox for Steven Nguyen		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > Mathboxes > prjspnval2		Structured version Visualization version GIF version

Theorem prjspnval2 42776

Description: Value of the n-dimensional projective space function, expanded. (Contributed by Steven Nguyen, 15-Jul-2023.)

**Hypotheses**
Ref	Expression
prjspnval2.e	⊢ ∼ = {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) ∧ ∃𝑙 ∈ 𝑆 𝑥 = (𝑙 · 𝑦))}
prjspnval2.w	⊢ 𝑊 = (𝐾 freeLMod (0...𝑁))
prjspnval2.b	⊢ 𝐵 = ((Base‘𝑊) ∖ {(0_g‘𝑊)})
prjspnval2.s	⊢ 𝑆 = (Base‘𝐾)
prjspnval2.x	⊢ · = ( ·_𝑠 ‘𝑊)

**Assertion**
Ref	Expression
prjspnval2	⊢ ((𝑁 ∈ ℕ₀ ∧ 𝐾 ∈ DivRing) → (𝑁ℙ𝕣𝕠𝕛_n𝐾) = (𝐵 / ∼ ))

Distinct variable groups: 𝑊,𝑙,𝑥,𝑦 𝑥,𝐾,𝑦 𝑆,𝑙 Allowed substitution hints: 𝐵(𝑥,𝑦,𝑙) ∼ (𝑥,𝑦,𝑙) 𝑆(𝑥,𝑦) · (𝑥,𝑦,𝑙) 𝐾(𝑙) 𝑁(𝑥,𝑦,𝑙)

**Proof of Theorem prjspnval2**
Step	Hyp	Ref	Expression
1		prjspnval 42774	. 2 ⊢ ((𝑁 ∈ ℕ₀ ∧ 𝐾 ∈ DivRing) → (𝑁ℙ𝕣𝕠𝕛_n𝐾) = (ℙ𝕣𝕠𝕛‘(𝐾 freeLMod (0...𝑁))))
2		prjspnval2.w	. . . . 5 ⊢ 𝑊 = (𝐾 freeLMod (0...𝑁))
3	2	fveq2i 6834	. . . 4 ⊢ (ℙ𝕣𝕠𝕛‘𝑊) = (ℙ𝕣𝕠𝕛‘(𝐾 freeLMod (0...𝑁)))
4		ovex 7388	. . . . . . 7 ⊢ (0...𝑁) ∈ V
5	2	frlmlvec 21707	. . . . . . 7 ⊢ ((𝐾 ∈ DivRing ∧ (0...𝑁) ∈ V) → 𝑊 ∈ LVec)
6	4, 5	mpan2 691	. . . . . 6 ⊢ (𝐾 ∈ DivRing → 𝑊 ∈ LVec)
7		prjspnval2.b	. . . . . . 7 ⊢ 𝐵 = ((Base‘𝑊) ∖ {(0_g‘𝑊)})
8		prjspnval2.x	. . . . . . 7 ⊢ · = ( ·_𝑠 ‘𝑊)
9		eqid 2733	. . . . . . 7 ⊢ (Scalar‘𝑊) = (Scalar‘𝑊)
10		eqid 2733	. . . . . . 7 ⊢ (Base‘(Scalar‘𝑊)) = (Base‘(Scalar‘𝑊))
11	7, 8, 9, 10	prjspval 42761	. . . . . 6 ⊢ (𝑊 ∈ LVec → (ℙ𝕣𝕠𝕛‘𝑊) = (𝐵 / {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) ∧ ∃𝑙 ∈ (Base‘(Scalar‘𝑊))𝑥 = (𝑙 · 𝑦))}))
12	6, 11	syl 17	. . . . 5 ⊢ (𝐾 ∈ DivRing → (ℙ𝕣𝕠𝕛‘𝑊) = (𝐵 / {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) ∧ ∃𝑙 ∈ (Base‘(Scalar‘𝑊))𝑥 = (𝑙 · 𝑦))}))
13		prjspnval2.e	. . . . . . 7 ⊢ ∼ = {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) ∧ ∃𝑙 ∈ 𝑆 𝑥 = (𝑙 · 𝑦))}
14		prjspnval2.s	. . . . . . 7 ⊢ 𝑆 = (Base‘𝐾)
15	13, 2, 7, 14, 8	prjspnerlem 42775	. . . . . 6 ⊢ (𝐾 ∈ DivRing → ∼ = {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) ∧ ∃𝑙 ∈ (Base‘(Scalar‘𝑊))𝑥 = (𝑙 · 𝑦))})
16	15	qseq2d 8694	. . . . 5 ⊢ (𝐾 ∈ DivRing → (𝐵 / ∼ ) = (𝐵 / {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) ∧ ∃𝑙 ∈ (Base‘(Scalar‘𝑊))𝑥 = (𝑙 · 𝑦))}))
17	12, 16	eqtr4d 2771	. . . 4 ⊢ (𝐾 ∈ DivRing → (ℙ𝕣𝕠𝕛‘𝑊) = (𝐵 / ∼ ))
18	3, 17	eqtr3id 2782	. . 3 ⊢ (𝐾 ∈ DivRing → (ℙ𝕣𝕠𝕛‘(𝐾 freeLMod (0...𝑁))) = (𝐵 / ∼ ))
19	18	adantl 481	. 2 ⊢ ((𝑁 ∈ ℕ₀ ∧ 𝐾 ∈ DivRing) → (ℙ𝕣𝕠𝕛‘(𝐾 freeLMod (0...𝑁))) = (𝐵 / ∼ ))
20	1, 19	eqtrd 2768	1 ⊢ ((𝑁 ∈ ℕ₀ ∧ 𝐾 ∈ DivRing) → (𝑁ℙ𝕣𝕠𝕛_n𝐾) = (𝐵 / ∼ ))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ∧ wa 395 = wceq 1541 ∈ wcel 2113 ∃wrex 3057 Vcvv 3437 ∖ cdif 3895 {csn 4577 {copab 5157 ‘cfv 6489 (class class class)co 7355 / cqs 8630 0cc0 11017 ℕ₀cn0 12392 ...cfz 13414 Basecbs 17127 Scalarcsca 17171 ·_𝑠 cvsca 17172 0_gc0g 17350 DivRingcdr 20653 LVecclvec 21045 freeLMod cfrlm 21692 ℙ𝕣𝕠𝕛cprjsp 42759 ℙ𝕣𝕠𝕛_ncprjspn 42772

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1796 ax-4 1810 ax-5 1911 ax-6 1968 ax-7 2009 ax-8 2115 ax-9 2123 ax-10 2146 ax-11 2162 ax-12 2182 ax-ext 2705 ax-rep 5221 ax-sep 5238 ax-nul 5248 ax-pow 5307 ax-pr 5374 ax-un 7677 ax-cnex 11073 ax-resscn 11074 ax-1cn 11075 ax-icn 11076 ax-addcl 11077 ax-addrcl 11078 ax-mulcl 11079 ax-mulrcl 11080 ax-mulcom 11081 ax-addass 11082 ax-mulass 11083 ax-distr 11084 ax-i2m1 11085 ax-1ne0 11086 ax-1rid 11087 ax-rnegex 11088 ax-rrecex 11089 ax-cnre 11090 ax-pre-lttri 11091 ax-pre-lttrn 11092 ax-pre-ltadd 11093 ax-pre-mulgt0 11094

This theorem depends on definitions: df-bi 207 df-an 396 df-or 848 df-3or 1087 df-3an 1088 df-tru 1544 df-fal 1554 df-ex 1781 df-nf 1785 df-sb 2068 df-mo 2537 df-eu 2566 df-clab 2712 df-cleq 2725 df-clel 2808 df-nfc 2882 df-ne 2930 df-nel 3034 df-ral 3049 df-rex 3058 df-rmo 3347 df-reu 3348 df-rab 3397 df-v 3439 df-sbc 3738 df-csb 3847 df-dif 3901 df-un 3903 df-in 3905 df-ss 3915 df-pss 3918 df-nul 4283 df-if 4477 df-pw 4553 df-sn 4578 df-pr 4580 df-tp 4582 df-op 4584 df-uni 4861 df-iun 4945 df-br 5096 df-opab 5158 df-mpt 5177 df-tr 5203 df-id 5516 df-eprel 5521 df-po 5529 df-so 5530 df-fr 5574 df-we 5576 df-xp 5627 df-rel 5628 df-cnv 5629 df-co 5630 df-dm 5631 df-rn 5632 df-res 5633 df-ima 5634 df-pred 6256 df-ord 6317 df-on 6318 df-lim 6319 df-suc 6320 df-iota 6445 df-fun 6491 df-fn 6492 df-f 6493 df-f1 6494 df-fo 6495 df-f1o 6496 df-fv 6497 df-riota 7312 df-ov 7358 df-oprab 7359 df-mpo 7360 df-om 7806 df-1st 7930 df-2nd 7931 df-frecs 8220 df-wrecs 8251 df-recs 8300 df-rdg 8338 df-1o 8394 df-er 8631 df-ec 8633 df-qs 8637 df-map 8761 df-ixp 8832 df-en 8880 df-dom 8881 df-sdom 8882 df-fin 8883 df-sup 9337 df-pnf 11159 df-mnf 11160 df-xr 11161 df-ltxr 11162 df-le 11163 df-sub 11357 df-neg 11358 df-nn 12137 df-2 12199 df-3 12200 df-4 12201 df-5 12202 df-6 12203 df-7 12204 df-8 12205 df-9 12206 df-n0 12393 df-z 12480 df-dec 12599 df-uz 12743 df-fz 13415 df-struct 17065 df-sets 17082 df-slot 17100 df-ndx 17112 df-base 17128 df-ress 17149 df-plusg 17181 df-mulr 17182 df-sca 17184 df-vsca 17185 df-ip 17186 df-tset 17187 df-ple 17188 df-ds 17190 df-hom 17192 df-cco 17193 df-0g 17352 df-prds 17358 df-pws 17360 df-mgm 18556 df-sgrp 18635 df-mnd 18651 df-grp 18857 df-minusg 18858 df-sbg 18859 df-subg 19044 df-cmn 19702 df-abl 19703 df-mgp 20067 df-rng 20079 df-ur 20108 df-ring 20161 df-subrg 20494 df-drng 20655 df-lmod 20804 df-lss 20874 df-lvec 21046 df-sra 21116 df-rgmod 21117 df-dsmm 21678 df-frlm 21693 df-prjsp 42760 df-prjspn 42773

This theorem is referenced by: prjspnssbas 42779 prjspnn0 42780 0prjspn 42786

W3C validator