pjimai - Hilbert Space Explorer

	Hilbert Space Explorer		< Previous Next > Nearby theorems
Mirrors > Home > HSE Home > Th. List > pjimai		Structured version Visualization version GIF version

Theorem pjimai 32146

Description: The image of a projection. Lemma 5 in Daniel Lehmann, "A presentation of Quantum Logic based on an and then connective", https://doi.org/10.48550/arXiv.quant-ph/0701113. (Contributed by NM, 20-Jan-2007.) (New usage is discouraged.)

**Hypotheses**
Ref	Expression
pjima.1	⊢ 𝐴 ∈ S_ℋ
pjima.2	⊢ 𝐵 ∈ C_ℋ

**Assertion**
Ref	Expression
pjimai	⊢ ((proj_ℎ‘𝐵) “ 𝐴) = ((𝐴 +_ℋ (⊥‘𝐵)) ∩ 𝐵)

Proof of Theorem pjimai Dummy variables 𝑣 𝑢 𝑤 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		pjima.2	. . . . . . . . 9 ⊢ 𝐵 ∈ C_ℋ
2		pjima.1	. . . . . . . . . 10 ⊢ 𝐴 ∈ S_ℋ
3	2	sheli 31184	. . . . . . . . 9 ⊢ (𝑣 ∈ 𝐴 → 𝑣 ∈ ℋ)
4		pjeq 31369	. . . . . . . . 9 ⊢ ((𝐵 ∈ C_ℋ ∧ 𝑣 ∈ ℋ) → (((proj_ℎ‘𝐵)‘𝑣) = 𝑢 ↔ (𝑢 ∈ 𝐵 ∧ ∃𝑤 ∈ (⊥‘𝐵)𝑣 = (𝑢 +_ℎ 𝑤))))
5	1, 3, 4	sylancr 587	. . . . . . . 8 ⊢ (𝑣 ∈ 𝐴 → (((proj_ℎ‘𝐵)‘𝑣) = 𝑢 ↔ (𝑢 ∈ 𝐵 ∧ ∃𝑤 ∈ (⊥‘𝐵)𝑣 = (𝑢 +_ℎ 𝑤))))
6		ibar 528	. . . . . . . . 9 ⊢ (𝑢 ∈ 𝐵 → (∃𝑤 ∈ (⊥‘𝐵)𝑣 = (𝑢 +_ℎ 𝑤) ↔ (𝑢 ∈ 𝐵 ∧ ∃𝑤 ∈ (⊥‘𝐵)𝑣 = (𝑢 +_ℎ 𝑤))))
7	6	bicomd 223	. . . . . . . 8 ⊢ (𝑢 ∈ 𝐵 → ((𝑢 ∈ 𝐵 ∧ ∃𝑤 ∈ (⊥‘𝐵)𝑣 = (𝑢 +_ℎ 𝑤)) ↔ ∃𝑤 ∈ (⊥‘𝐵)𝑣 = (𝑢 +_ℎ 𝑤)))
8	5, 7	sylan9bbr 510	. . . . . . 7 ⊢ ((𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐴) → (((proj_ℎ‘𝐵)‘𝑣) = 𝑢 ↔ ∃𝑤 ∈ (⊥‘𝐵)𝑣 = (𝑢 +_ℎ 𝑤)))
9	1	cheli 31202	. . . . . . . . . . 11 ⊢ (𝑢 ∈ 𝐵 → 𝑢 ∈ ℋ)
10	1	choccli 31277	. . . . . . . . . . . 12 ⊢ (⊥‘𝐵) ∈ C_ℋ
11	10	cheli 31202	. . . . . . . . . . 11 ⊢ (𝑤 ∈ (⊥‘𝐵) → 𝑤 ∈ ℋ)
12		hvsubadd 31047	. . . . . . . . . . . . 13 ⊢ ((𝑣 ∈ ℋ ∧ 𝑤 ∈ ℋ ∧ 𝑢 ∈ ℋ) → ((𝑣 −_ℎ 𝑤) = 𝑢 ↔ (𝑤 +_ℎ 𝑢) = 𝑣))
13	12	3comr 1125	. . . . . . . . . . . 12 ⊢ ((𝑢 ∈ ℋ ∧ 𝑣 ∈ ℋ ∧ 𝑤 ∈ ℋ) → ((𝑣 −_ℎ 𝑤) = 𝑢 ↔ (𝑤 +_ℎ 𝑢) = 𝑣))
14		ax-hvcom 30971	. . . . . . . . . . . . . 14 ⊢ ((𝑢 ∈ ℋ ∧ 𝑤 ∈ ℋ) → (𝑢 +_ℎ 𝑤) = (𝑤 +_ℎ 𝑢))
15	14	3adant2 1131	. . . . . . . . . . . . 13 ⊢ ((𝑢 ∈ ℋ ∧ 𝑣 ∈ ℋ ∧ 𝑤 ∈ ℋ) → (𝑢 +_ℎ 𝑤) = (𝑤 +_ℎ 𝑢))
16	15	eqeq1d 2732	. . . . . . . . . . . 12 ⊢ ((𝑢 ∈ ℋ ∧ 𝑣 ∈ ℋ ∧ 𝑤 ∈ ℋ) → ((𝑢 +_ℎ 𝑤) = 𝑣 ↔ (𝑤 +_ℎ 𝑢) = 𝑣))
17	13, 16	bitr4d 282	. . . . . . . . . . 11 ⊢ ((𝑢 ∈ ℋ ∧ 𝑣 ∈ ℋ ∧ 𝑤 ∈ ℋ) → ((𝑣 −_ℎ 𝑤) = 𝑢 ↔ (𝑢 +_ℎ 𝑤) = 𝑣))
18	9, 3, 11, 17	syl3an 1160	. . . . . . . . . 10 ⊢ ((𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐴 ∧ 𝑤 ∈ (⊥‘𝐵)) → ((𝑣 −_ℎ 𝑤) = 𝑢 ↔ (𝑢 +_ℎ 𝑤) = 𝑣))
19		eqcom 2737	. . . . . . . . . 10 ⊢ (𝑢 = (𝑣 −_ℎ 𝑤) ↔ (𝑣 −_ℎ 𝑤) = 𝑢)
20		eqcom 2737	. . . . . . . . . 10 ⊢ (𝑣 = (𝑢 +_ℎ 𝑤) ↔ (𝑢 +_ℎ 𝑤) = 𝑣)
21	18, 19, 20	3bitr4g 314	. . . . . . . . 9 ⊢ ((𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐴 ∧ 𝑤 ∈ (⊥‘𝐵)) → (𝑢 = (𝑣 −_ℎ 𝑤) ↔ 𝑣 = (𝑢 +_ℎ 𝑤)))
22	21	3expa 1118	. . . . . . . 8 ⊢ (((𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐴) ∧ 𝑤 ∈ (⊥‘𝐵)) → (𝑢 = (𝑣 −_ℎ 𝑤) ↔ 𝑣 = (𝑢 +_ℎ 𝑤)))
23	22	rexbidva 3152	. . . . . . 7 ⊢ ((𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐴) → (∃𝑤 ∈ (⊥‘𝐵)𝑢 = (𝑣 −_ℎ 𝑤) ↔ ∃𝑤 ∈ (⊥‘𝐵)𝑣 = (𝑢 +_ℎ 𝑤)))
24	8, 23	bitr4d 282	. . . . . 6 ⊢ ((𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐴) → (((proj_ℎ‘𝐵)‘𝑣) = 𝑢 ↔ ∃𝑤 ∈ (⊥‘𝐵)𝑢 = (𝑣 −_ℎ 𝑤)))
25	24	rexbidva 3152	. . . . 5 ⊢ (𝑢 ∈ 𝐵 → (∃𝑣 ∈ 𝐴 ((proj_ℎ‘𝐵)‘𝑣) = 𝑢 ↔ ∃𝑣 ∈ 𝐴 ∃𝑤 ∈ (⊥‘𝐵)𝑢 = (𝑣 −_ℎ 𝑤)))
26	1	pjfni 31671	. . . . . 6 ⊢ (proj_ℎ‘𝐵) Fn ℋ
27	2	shssii 31183	. . . . . 6 ⊢ 𝐴 ⊆ ℋ
28		fvelimab 6889	. . . . . 6 ⊢ (((proj_ℎ‘𝐵) Fn ℋ ∧ 𝐴 ⊆ ℋ) → (𝑢 ∈ ((proj_ℎ‘𝐵) “ 𝐴) ↔ ∃𝑣 ∈ 𝐴 ((proj_ℎ‘𝐵)‘𝑣) = 𝑢))
29	26, 27, 28	mp2an 692	. . . . 5 ⊢ (𝑢 ∈ ((proj_ℎ‘𝐵) “ 𝐴) ↔ ∃𝑣 ∈ 𝐴 ((proj_ℎ‘𝐵)‘𝑣) = 𝑢)
30	10	chshii 31197	. . . . . 6 ⊢ (⊥‘𝐵) ∈ S_ℋ
31		shsel3 31285	. . . . . 6 ⊢ ((𝐴 ∈ S_ℋ ∧ (⊥‘𝐵) ∈ S_ℋ ) → (𝑢 ∈ (𝐴 +_ℋ (⊥‘𝐵)) ↔ ∃𝑣 ∈ 𝐴 ∃𝑤 ∈ (⊥‘𝐵)𝑢 = (𝑣 −_ℎ 𝑤)))
32	2, 30, 31	mp2an 692	. . . . 5 ⊢ (𝑢 ∈ (𝐴 +_ℋ (⊥‘𝐵)) ↔ ∃𝑣 ∈ 𝐴 ∃𝑤 ∈ (⊥‘𝐵)𝑢 = (𝑣 −_ℎ 𝑤))
33	25, 29, 32	3bitr4g 314	. . . 4 ⊢ (𝑢 ∈ 𝐵 → (𝑢 ∈ ((proj_ℎ‘𝐵) “ 𝐴) ↔ 𝑢 ∈ (𝐴 +_ℋ (⊥‘𝐵))))
34	33	pm5.32ri 575	. . 3 ⊢ ((𝑢 ∈ ((proj_ℎ‘𝐵) “ 𝐴) ∧ 𝑢 ∈ 𝐵) ↔ (𝑢 ∈ (𝐴 +_ℋ (⊥‘𝐵)) ∧ 𝑢 ∈ 𝐵))
35		imassrn 6017	. . . . . 6 ⊢ ((proj_ℎ‘𝐵) “ 𝐴) ⊆ ran (proj_ℎ‘𝐵)
36	1	pjrni 31672	. . . . . 6 ⊢ ran (proj_ℎ‘𝐵) = 𝐵
37	35, 36	sseqtri 3981	. . . . 5 ⊢ ((proj_ℎ‘𝐵) “ 𝐴) ⊆ 𝐵
38	37	sseli 3928	. . . 4 ⊢ (𝑢 ∈ ((proj_ℎ‘𝐵) “ 𝐴) → 𝑢 ∈ 𝐵)
39	38	pm4.71i 559	. . 3 ⊢ (𝑢 ∈ ((proj_ℎ‘𝐵) “ 𝐴) ↔ (𝑢 ∈ ((proj_ℎ‘𝐵) “ 𝐴) ∧ 𝑢 ∈ 𝐵))
40		elin 3916	. . 3 ⊢ (𝑢 ∈ ((𝐴 +_ℋ (⊥‘𝐵)) ∩ 𝐵) ↔ (𝑢 ∈ (𝐴 +_ℋ (⊥‘𝐵)) ∧ 𝑢 ∈ 𝐵))
41	34, 39, 40	3bitr4i 303	. 2 ⊢ (𝑢 ∈ ((proj_ℎ‘𝐵) “ 𝐴) ↔ 𝑢 ∈ ((𝐴 +_ℋ (⊥‘𝐵)) ∩ 𝐵))
42	41	eqriv 2727	1 ⊢ ((proj_ℎ‘𝐵) “ 𝐴) = ((𝐴 +_ℋ (⊥‘𝐵)) ∩ 𝐵)

Colors of variables: wff setvar class

Syntax hints: ↔ wb 206 ∧ wa 395 ∧ w3a 1086 = wceq 1541 ∈ wcel 2110 ∃wrex 3054 ∩ cin 3899 ⊆ wss 3900 ran crn 5615 “ cima 5617 Fn wfn 6472 ‘cfv 6477 (class class class)co 7341 ℋchba 30889 +_ℎ cva 30890 −_ℎ cmv 30895 S_ℋ csh 30898 C_ℋ cch 30899 ⊥cort 30900 +_ℋ cph 30901 proj_ℎcpjh 30907

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 2112 ax-9 2120 ax-10 2143 ax-11 2159 ax-12 2179 ax-ext 2702 ax-rep 5215 ax-sep 5232 ax-nul 5242 ax-pow 5301 ax-pr 5368 ax-un 7663 ax-inf2 9526 ax-cc 10318 ax-cnex 11054 ax-resscn 11055 ax-1cn 11056 ax-icn 11057 ax-addcl 11058 ax-addrcl 11059 ax-mulcl 11060 ax-mulrcl 11061 ax-mulcom 11062 ax-addass 11063 ax-mulass 11064 ax-distr 11065 ax-i2m1 11066 ax-1ne0 11067 ax-1rid 11068 ax-rnegex 11069 ax-rrecex 11070 ax-cnre 11071 ax-pre-lttri 11072 ax-pre-lttrn 11073 ax-pre-ltadd 11074 ax-pre-mulgt0 11075 ax-pre-sup 11076 ax-addf 11077 ax-mulf 11078 ax-hilex 30969 ax-hfvadd 30970 ax-hvcom 30971 ax-hvass 30972 ax-hv0cl 30973 ax-hvaddid 30974 ax-hfvmul 30975 ax-hvmulid 30976 ax-hvmulass 30977 ax-hvdistr1 30978 ax-hvdistr2 30979 ax-hvmul0 30980 ax-hfi 31049 ax-his1 31052 ax-his2 31053 ax-his3 31054 ax-his4 31055 ax-hcompl 31172

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 2067 df-mo 2534 df-eu 2563 df-clab 2709 df-cleq 2722 df-clel 2804 df-nfc 2879 df-ne 2927 df-nel 3031 df-ral 3046 df-rex 3055 df-rmo 3344 df-reu 3345 df-rab 3394 df-v 3436 df-sbc 3740 df-csb 3849 df-dif 3903 df-un 3905 df-in 3907 df-ss 3917 df-pss 3920 df-nul 4282 df-if 4474 df-pw 4550 df-sn 4575 df-pr 4577 df-tp 4579 df-op 4581 df-uni 4858 df-int 4896 df-iun 4941 df-iin 4942 df-br 5090 df-opab 5152 df-mpt 5171 df-tr 5197 df-id 5509 df-eprel 5514 df-po 5522 df-so 5523 df-fr 5567 df-se 5568 df-we 5569 df-xp 5620 df-rel 5621 df-cnv 5622 df-co 5623 df-dm 5624 df-rn 5625 df-res 5626 df-ima 5627 df-pred 6244 df-ord 6305 df-on 6306 df-lim 6307 df-suc 6308 df-iota 6433 df-fun 6479 df-fn 6480 df-f 6481 df-f1 6482 df-fo 6483 df-f1o 6484 df-fv 6485 df-isom 6486 df-riota 7298 df-ov 7344 df-oprab 7345 df-mpo 7346 df-of 7605 df-om 7792 df-1st 7916 df-2nd 7917 df-supp 8086 df-frecs 8206 df-wrecs 8237 df-recs 8286 df-rdg 8324 df-1o 8380 df-2o 8381 df-oadd 8384 df-omul 8385 df-er 8617 df-map 8747 df-pm 8748 df-ixp 8817 df-en 8865 df-dom 8866 df-sdom 8867 df-fin 8868 df-fsupp 9241 df-fi 9290 df-sup 9321 df-inf 9322 df-oi 9391 df-card 9824 df-acn 9827 df-pnf 11140 df-mnf 11141 df-xr 11142 df-ltxr 11143 df-le 11144 df-sub 11338 df-neg 11339 df-div 11767 df-nn 12118 df-2 12180 df-3 12181 df-4 12182 df-5 12183 df-6 12184 df-7 12185 df-8 12186 df-9 12187 df-n0 12374 df-z 12461 df-dec 12581 df-uz 12725 df-q 12839 df-rp 12883 df-xneg 13003 df-xadd 13004 df-xmul 13005 df-ioo 13241 df-ico 13243 df-icc 13244 df-fz 13400 df-fzo 13547 df-fl 13688 df-seq 13901 df-exp 13961 df-hash 14230 df-cj 14998 df-re 14999 df-im 15000 df-sqrt 15134 df-abs 15135 df-clim 15387 df-rlim 15388 df-sum 15586 df-struct 17050 df-sets 17067 df-slot 17085 df-ndx 17097 df-base 17113 df-ress 17134 df-plusg 17166 df-mulr 17167 df-starv 17168 df-sca 17169 df-vsca 17170 df-ip 17171 df-tset 17172 df-ple 17173 df-ds 17175 df-unif 17176 df-hom 17177 df-cco 17178 df-rest 17318 df-topn 17319 df-0g 17337 df-gsum 17338 df-topgen 17339 df-pt 17340 df-prds 17343 df-xrs 17398 df-qtop 17403 df-imas 17404 df-xps 17406 df-mre 17480 df-mrc 17481 df-acs 17483 df-mgm 18540 df-sgrp 18619 df-mnd 18635 df-submnd 18684 df-mulg 18973 df-cntz 19222 df-cmn 19687 df-psmet 21276 df-xmet 21277 df-met 21278 df-bl 21279 df-mopn 21280 df-fbas 21281 df-fg 21282 df-cnfld 21285 df-top 22802 df-topon 22819 df-topsp 22841 df-bases 22854 df-cld 22927 df-ntr 22928 df-cls 22929 df-nei 23006 df-cn 23135 df-cnp 23136 df-lm 23137 df-haus 23223 df-tx 23470 df-hmeo 23663 df-fil 23754 df-fm 23846 df-flim 23847 df-flf 23848 df-xms 24228 df-ms 24229 df-tms 24230 df-cfil 25175 df-cau 25176 df-cmet 25177 df-grpo 30463 df-gid 30464 df-ginv 30465 df-gdiv 30466 df-ablo 30515 df-vc 30529 df-nv 30562 df-va 30565 df-ba 30566 df-sm 30567 df-0v 30568 df-vs 30569 df-nmcv 30570 df-ims 30571 df-dip 30671 df-ssp 30692 df-ph 30783 df-cbn 30833 df-hnorm 30938 df-hba 30939 df-hvsub 30941 df-hlim 30942 df-hcau 30943 df-sh 31177 df-ch 31191 df-oc 31222 df-ch0 31223 df-shs 31278 df-pjh 31365

This theorem is referenced by: (None)

W3C validator