Mathbox for Steven Nguyen |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > Mathboxes > prjspnfv01 | Structured version Visualization version GIF version |
Description: Any vector is equivalent to a vector whose zeroth coordinate is 0 or 1 (proof of the value of the zeroth coordinate). (Contributed by SN, 13-Aug-2023.) |
Ref | Expression |
---|---|
prjspnfv01.f | ⊢ 𝐹 = (𝑏 ∈ 𝐵 ↦ if((𝑏‘0) = 0 , 𝑏, ((𝐼‘(𝑏‘0)) · 𝑏))) |
prjspnfv01.b | ⊢ 𝐵 = ((Base‘𝑊) ∖ {(0g‘𝑊)}) |
prjspnfv01.w | ⊢ 𝑊 = (𝐾 freeLMod (0...𝑁)) |
prjspnfv01.t | ⊢ · = ( ·𝑠 ‘𝑊) |
prjspnfv01.0 | ⊢ 0 = (0g‘𝐾) |
prjspnfv01.1 | ⊢ 1 = (1r‘𝐾) |
prjspnfv01.i | ⊢ 𝐼 = (invr‘𝐾) |
prjspnfv01.k | ⊢ (𝜑 → 𝐾 ∈ DivRing) |
prjspnfv01.n | ⊢ (𝜑 → 𝑁 ∈ ℕ0) |
prjspnfv01.x | ⊢ (𝜑 → 𝑋 ∈ 𝐵) |
Ref | Expression |
---|---|
prjspnfv01 | ⊢ (𝜑 → ((𝐹‘𝑋)‘0) = if((𝑋‘0) = 0 , 0 , 1 )) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | prjspnfv01.f | . . . 4 ⊢ 𝐹 = (𝑏 ∈ 𝐵 ↦ if((𝑏‘0) = 0 , 𝑏, ((𝐼‘(𝑏‘0)) · 𝑏))) | |
2 | fveq1 6735 | . . . . . 6 ⊢ (𝑏 = 𝑋 → (𝑏‘0) = (𝑋‘0)) | |
3 | 2 | eqeq1d 2740 | . . . . 5 ⊢ (𝑏 = 𝑋 → ((𝑏‘0) = 0 ↔ (𝑋‘0) = 0 )) |
4 | id 22 | . . . . 5 ⊢ (𝑏 = 𝑋 → 𝑏 = 𝑋) | |
5 | 2 | fveq2d 6740 | . . . . . 6 ⊢ (𝑏 = 𝑋 → (𝐼‘(𝑏‘0)) = (𝐼‘(𝑋‘0))) |
6 | 5, 4 | oveq12d 7250 | . . . . 5 ⊢ (𝑏 = 𝑋 → ((𝐼‘(𝑏‘0)) · 𝑏) = ((𝐼‘(𝑋‘0)) · 𝑋)) |
7 | 3, 4, 6 | ifbieq12d 4482 | . . . 4 ⊢ (𝑏 = 𝑋 → if((𝑏‘0) = 0 , 𝑏, ((𝐼‘(𝑏‘0)) · 𝑏)) = if((𝑋‘0) = 0 , 𝑋, ((𝐼‘(𝑋‘0)) · 𝑋))) |
8 | prjspnfv01.x | . . . 4 ⊢ (𝜑 → 𝑋 ∈ 𝐵) | |
9 | ovexd 7267 | . . . . 5 ⊢ (𝜑 → ((𝐼‘(𝑋‘0)) · 𝑋) ∈ V) | |
10 | 8, 9 | ifexd 4502 | . . . 4 ⊢ (𝜑 → if((𝑋‘0) = 0 , 𝑋, ((𝐼‘(𝑋‘0)) · 𝑋)) ∈ V) |
11 | 1, 7, 8, 10 | fvmptd3 6860 | . . 3 ⊢ (𝜑 → (𝐹‘𝑋) = if((𝑋‘0) = 0 , 𝑋, ((𝐼‘(𝑋‘0)) · 𝑋))) |
12 | 11 | fveq1d 6738 | . 2 ⊢ (𝜑 → ((𝐹‘𝑋)‘0) = (if((𝑋‘0) = 0 , 𝑋, ((𝐼‘(𝑋‘0)) · 𝑋))‘0)) |
13 | iffv 6753 | . . 3 ⊢ (if((𝑋‘0) = 0 , 𝑋, ((𝐼‘(𝑋‘0)) · 𝑋))‘0) = if((𝑋‘0) = 0 , (𝑋‘0), (((𝐼‘(𝑋‘0)) · 𝑋)‘0)) | |
14 | 13 | a1i 11 | . 2 ⊢ (𝜑 → (if((𝑋‘0) = 0 , 𝑋, ((𝐼‘(𝑋‘0)) · 𝑋))‘0) = if((𝑋‘0) = 0 , (𝑋‘0), (((𝐼‘(𝑋‘0)) · 𝑋)‘0))) |
15 | simpr 488 | . . 3 ⊢ ((𝜑 ∧ (𝑋‘0) = 0 ) → (𝑋‘0) = 0 ) | |
16 | prjspnfv01.w | . . . . 5 ⊢ 𝑊 = (𝐾 freeLMod (0...𝑁)) | |
17 | eqid 2738 | . . . . 5 ⊢ (Base‘𝑊) = (Base‘𝑊) | |
18 | eqid 2738 | . . . . 5 ⊢ (Base‘𝐾) = (Base‘𝐾) | |
19 | ovexd 7267 | . . . . 5 ⊢ ((𝜑 ∧ ¬ (𝑋‘0) = 0 ) → (0...𝑁) ∈ V) | |
20 | prjspnfv01.k | . . . . . 6 ⊢ (𝜑 → 𝐾 ∈ DivRing) | |
21 | ovexd 7267 | . . . . . . . 8 ⊢ (𝜑 → (0...𝑁) ∈ V) | |
22 | prjspnfv01.b | . . . . . . . . . 10 ⊢ 𝐵 = ((Base‘𝑊) ∖ {(0g‘𝑊)}) | |
23 | 8, 22 | eleqtrdi 2849 | . . . . . . . . 9 ⊢ (𝜑 → 𝑋 ∈ ((Base‘𝑊) ∖ {(0g‘𝑊)})) |
24 | 23 | eldifad 3893 | . . . . . . . 8 ⊢ (𝜑 → 𝑋 ∈ (Base‘𝑊)) |
25 | 16, 18, 17 | frlmbasf 20750 | . . . . . . . 8 ⊢ (((0...𝑁) ∈ V ∧ 𝑋 ∈ (Base‘𝑊)) → 𝑋:(0...𝑁)⟶(Base‘𝐾)) |
26 | 21, 24, 25 | syl2anc 587 | . . . . . . 7 ⊢ (𝜑 → 𝑋:(0...𝑁)⟶(Base‘𝐾)) |
27 | prjspnfv01.n | . . . . . . . 8 ⊢ (𝜑 → 𝑁 ∈ ℕ0) | |
28 | 0elfz 13234 | . . . . . . . 8 ⊢ (𝑁 ∈ ℕ0 → 0 ∈ (0...𝑁)) | |
29 | 27, 28 | syl 17 | . . . . . . 7 ⊢ (𝜑 → 0 ∈ (0...𝑁)) |
30 | 26, 29 | ffvelrnd 6924 | . . . . . 6 ⊢ (𝜑 → (𝑋‘0) ∈ (Base‘𝐾)) |
31 | neqne 2949 | . . . . . 6 ⊢ (¬ (𝑋‘0) = 0 → (𝑋‘0) ≠ 0 ) | |
32 | prjspnfv01.0 | . . . . . . 7 ⊢ 0 = (0g‘𝐾) | |
33 | prjspnfv01.i | . . . . . . 7 ⊢ 𝐼 = (invr‘𝐾) | |
34 | 18, 32, 33 | drnginvrcl 19812 | . . . . . 6 ⊢ ((𝐾 ∈ DivRing ∧ (𝑋‘0) ∈ (Base‘𝐾) ∧ (𝑋‘0) ≠ 0 ) → (𝐼‘(𝑋‘0)) ∈ (Base‘𝐾)) |
35 | 20, 30, 31, 34 | syl2an3an 1424 | . . . . 5 ⊢ ((𝜑 ∧ ¬ (𝑋‘0) = 0 ) → (𝐼‘(𝑋‘0)) ∈ (Base‘𝐾)) |
36 | 24 | adantr 484 | . . . . 5 ⊢ ((𝜑 ∧ ¬ (𝑋‘0) = 0 ) → 𝑋 ∈ (Base‘𝑊)) |
37 | 29 | adantr 484 | . . . . 5 ⊢ ((𝜑 ∧ ¬ (𝑋‘0) = 0 ) → 0 ∈ (0...𝑁)) |
38 | prjspnfv01.t | . . . . 5 ⊢ · = ( ·𝑠 ‘𝑊) | |
39 | eqid 2738 | . . . . 5 ⊢ (.r‘𝐾) = (.r‘𝐾) | |
40 | 16, 17, 18, 19, 35, 36, 37, 38, 39 | frlmvscaval 20758 | . . . 4 ⊢ ((𝜑 ∧ ¬ (𝑋‘0) = 0 ) → (((𝐼‘(𝑋‘0)) · 𝑋)‘0) = ((𝐼‘(𝑋‘0))(.r‘𝐾)(𝑋‘0))) |
41 | prjspnfv01.1 | . . . . . 6 ⊢ 1 = (1r‘𝐾) | |
42 | 18, 32, 39, 41, 33 | drnginvrl 19814 | . . . . 5 ⊢ ((𝐾 ∈ DivRing ∧ (𝑋‘0) ∈ (Base‘𝐾) ∧ (𝑋‘0) ≠ 0 ) → ((𝐼‘(𝑋‘0))(.r‘𝐾)(𝑋‘0)) = 1 ) |
43 | 20, 30, 31, 42 | syl2an3an 1424 | . . . 4 ⊢ ((𝜑 ∧ ¬ (𝑋‘0) = 0 ) → ((𝐼‘(𝑋‘0))(.r‘𝐾)(𝑋‘0)) = 1 ) |
44 | 40, 43 | eqtrd 2778 | . . 3 ⊢ ((𝜑 ∧ ¬ (𝑋‘0) = 0 ) → (((𝐼‘(𝑋‘0)) · 𝑋)‘0) = 1 ) |
45 | 15, 44 | ifeq12da 4487 | . 2 ⊢ (𝜑 → if((𝑋‘0) = 0 , (𝑋‘0), (((𝐼‘(𝑋‘0)) · 𝑋)‘0)) = if((𝑋‘0) = 0 , 0 , 1 )) |
46 | 12, 14, 45 | 3eqtrd 2782 | 1 ⊢ (𝜑 → ((𝐹‘𝑋)‘0) = if((𝑋‘0) = 0 , 0 , 1 )) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 → wi 4 ∧ wa 399 = wceq 1543 ∈ wcel 2111 ≠ wne 2941 Vcvv 3421 ∖ cdif 3878 ifcif 4454 {csn 4556 ↦ cmpt 5150 ⟶wf 6394 ‘cfv 6398 (class class class)co 7232 0cc0 10754 ℕ0cn0 12115 ...cfz 13120 Basecbs 16788 .rcmulr 16831 ·𝑠 cvsca 16834 0gc0g 16972 1rcur 19544 invrcinvr 19717 DivRingcdr 19795 freeLMod cfrlm 20736 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1803 ax-4 1817 ax-5 1918 ax-6 1976 ax-7 2016 ax-8 2113 ax-9 2121 ax-10 2142 ax-11 2159 ax-12 2176 ax-ext 2709 ax-rep 5194 ax-sep 5207 ax-nul 5214 ax-pow 5273 ax-pr 5337 ax-un 7542 ax-cnex 10810 ax-resscn 10811 ax-1cn 10812 ax-icn 10813 ax-addcl 10814 ax-addrcl 10815 ax-mulcl 10816 ax-mulrcl 10817 ax-mulcom 10818 ax-addass 10819 ax-mulass 10820 ax-distr 10821 ax-i2m1 10822 ax-1ne0 10823 ax-1rid 10824 ax-rnegex 10825 ax-rrecex 10826 ax-cnre 10827 ax-pre-lttri 10828 ax-pre-lttrn 10829 ax-pre-ltadd 10830 ax-pre-mulgt0 10831 |
This theorem depends on definitions: df-bi 210 df-an 400 df-or 848 df-3or 1090 df-3an 1091 df-tru 1546 df-fal 1556 df-ex 1788 df-nf 1792 df-sb 2072 df-mo 2540 df-eu 2569 df-clab 2716 df-cleq 2730 df-clel 2817 df-nfc 2887 df-ne 2942 df-nel 3048 df-ral 3067 df-rex 3068 df-reu 3069 df-rmo 3070 df-rab 3071 df-v 3423 df-sbc 3710 df-csb 3827 df-dif 3884 df-un 3886 df-in 3888 df-ss 3898 df-pss 3900 df-nul 4253 df-if 4455 df-pw 4530 df-sn 4557 df-pr 4559 df-tp 4561 df-op 4563 df-uni 4835 df-iun 4921 df-br 5069 df-opab 5131 df-mpt 5151 df-tr 5177 df-id 5470 df-eprel 5475 df-po 5483 df-so 5484 df-fr 5524 df-we 5526 df-xp 5572 df-rel 5573 df-cnv 5574 df-co 5575 df-dm 5576 df-rn 5577 df-res 5578 df-ima 5579 df-pred 6176 df-ord 6234 df-on 6235 df-lim 6236 df-suc 6237 df-iota 6356 df-fun 6400 df-fn 6401 df-f 6402 df-f1 6403 df-fo 6404 df-f1o 6405 df-fv 6406 df-riota 7189 df-ov 7235 df-oprab 7236 df-mpo 7237 df-of 7488 df-om 7664 df-1st 7780 df-2nd 7781 df-supp 7925 df-tpos 7989 df-wrecs 8068 df-recs 8129 df-rdg 8167 df-1o 8223 df-er 8412 df-map 8531 df-ixp 8600 df-en 8648 df-dom 8649 df-sdom 8650 df-fin 8651 df-fsupp 9011 df-sup 9083 df-pnf 10894 df-mnf 10895 df-xr 10896 df-ltxr 10897 df-le 10898 df-sub 11089 df-neg 11090 df-nn 11856 df-2 11918 df-3 11919 df-4 11920 df-5 11921 df-6 11922 df-7 11923 df-8 11924 df-9 11925 df-n0 12116 df-z 12202 df-dec 12319 df-uz 12464 df-fz 13121 df-struct 16728 df-sets 16745 df-slot 16763 df-ndx 16773 df-base 16789 df-ress 16813 df-plusg 16843 df-mulr 16844 df-sca 16846 df-vsca 16847 df-ip 16848 df-tset 16849 df-ple 16850 df-ds 16852 df-hom 16854 df-cco 16855 df-0g 16974 df-prds 16980 df-pws 16982 df-mgm 18142 df-sgrp 18191 df-mnd 18202 df-grp 18396 df-minusg 18397 df-mgp 19533 df-ur 19545 df-ring 19592 df-oppr 19669 df-dvdsr 19687 df-unit 19688 df-invr 19718 df-drng 19797 df-sra 20237 df-rgmod 20238 df-dsmm 20722 df-frlm 20737 |
This theorem is referenced by: (None) |
Copyright terms: Public domain | W3C validator |