Theorem pjimai

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

	Ref	Expression
Hypotheses	pjima.1	⊢ 𝐴 ∈ Sℋ
	pjima.2	⊢ 𝐵 ∈ Cℋ
Assertion	pjimai	⊢ ( ( projℎ ‘ 𝐵 ) “ 𝐴 ) = ( ( 𝐴 +ℋ ( ⊥ ‘ 𝐵 ) ) ∩ 𝐵 )

Proof

Step	Hyp	Ref	Expression
1		pjima.1	⊢ 𝐴 ∈ Sℋ
2		pjima.2	⊢ 𝐵 ∈ Cℋ
3	1	sheli	⊢ ( 𝑣 ∈ 𝐴 → 𝑣 ∈ ℋ )
4		pjeq	⊢ ( ( 𝐵 ∈ Cℋ ∧ 𝑣 ∈ ℋ ) → ( ( ( projℎ ‘ 𝐵 ) ‘ 𝑣 ) = 𝑢 ↔ ( 𝑢 ∈ 𝐵 ∧ ∃ 𝑤 ∈ ( ⊥ ‘ 𝐵 ) 𝑣 = ( 𝑢 +ℎ 𝑤 ) ) ) )
5	2 3 4	sylancr	⊢ ( 𝑣 ∈ 𝐴 → ( ( ( projℎ ‘ 𝐵 ) ‘ 𝑣 ) = 𝑢 ↔ ( 𝑢 ∈ 𝐵 ∧ ∃ 𝑤 ∈ ( ⊥ ‘ 𝐵 ) 𝑣 = ( 𝑢 +ℎ 𝑤 ) ) ) )
6		ibar	⊢ ( 𝑢 ∈ 𝐵 → ( ∃ 𝑤 ∈ ( ⊥ ‘ 𝐵 ) 𝑣 = ( 𝑢 +ℎ 𝑤 ) ↔ ( 𝑢 ∈ 𝐵 ∧ ∃ 𝑤 ∈ ( ⊥ ‘ 𝐵 ) 𝑣 = ( 𝑢 +ℎ 𝑤 ) ) ) )
7	6	bicomd	⊢ ( 𝑢 ∈ 𝐵 → ( ( 𝑢 ∈ 𝐵 ∧ ∃ 𝑤 ∈ ( ⊥ ‘ 𝐵 ) 𝑣 = ( 𝑢 +ℎ 𝑤 ) ) ↔ ∃ 𝑤 ∈ ( ⊥ ‘ 𝐵 ) 𝑣 = ( 𝑢 +ℎ 𝑤 ) ) )
8	5 7	sylan9bbr	⊢ ( ( 𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐴 ) → ( ( ( projℎ ‘ 𝐵 ) ‘ 𝑣 ) = 𝑢 ↔ ∃ 𝑤 ∈ ( ⊥ ‘ 𝐵 ) 𝑣 = ( 𝑢 +ℎ 𝑤 ) ) )
9	2	cheli	⊢ ( 𝑢 ∈ 𝐵 → 𝑢 ∈ ℋ )
10	2	choccli	⊢ ( ⊥ ‘ 𝐵 ) ∈ Cℋ
11	10	cheli	⊢ ( 𝑤 ∈ ( ⊥ ‘ 𝐵 ) → 𝑤 ∈ ℋ )
12		hvsubadd	⊢ ( ( 𝑣 ∈ ℋ ∧ 𝑤 ∈ ℋ ∧ 𝑢 ∈ ℋ ) → ( ( 𝑣 −ℎ 𝑤 ) = 𝑢 ↔ ( 𝑤 +ℎ 𝑢 ) = 𝑣 ) )
13	12	3comr	⊢ ( ( 𝑢 ∈ ℋ ∧ 𝑣 ∈ ℋ ∧ 𝑤 ∈ ℋ ) → ( ( 𝑣 −ℎ 𝑤 ) = 𝑢 ↔ ( 𝑤 +ℎ 𝑢 ) = 𝑣 ) )
14		ax-hvcom	⊢ ( ( 𝑢 ∈ ℋ ∧ 𝑤 ∈ ℋ ) → ( 𝑢 +ℎ 𝑤 ) = ( 𝑤 +ℎ 𝑢 ) )
15	14	3adant2	⊢ ( ( 𝑢 ∈ ℋ ∧ 𝑣 ∈ ℋ ∧ 𝑤 ∈ ℋ ) → ( 𝑢 +ℎ 𝑤 ) = ( 𝑤 +ℎ 𝑢 ) )
16	15	eqeq1d	⊢ ( ( 𝑢 ∈ ℋ ∧ 𝑣 ∈ ℋ ∧ 𝑤 ∈ ℋ ) → ( ( 𝑢 +ℎ 𝑤 ) = 𝑣 ↔ ( 𝑤 +ℎ 𝑢 ) = 𝑣 ) )
17	13 16	bitr4d	⊢ ( ( 𝑢 ∈ ℋ ∧ 𝑣 ∈ ℋ ∧ 𝑤 ∈ ℋ ) → ( ( 𝑣 −ℎ 𝑤 ) = 𝑢 ↔ ( 𝑢 +ℎ 𝑤 ) = 𝑣 ) )
18	9 3 11 17	syl3an	⊢ ( ( 𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐴 ∧ 𝑤 ∈ ( ⊥ ‘ 𝐵 ) ) → ( ( 𝑣 −ℎ 𝑤 ) = 𝑢 ↔ ( 𝑢 +ℎ 𝑤 ) = 𝑣 ) )
19		eqcom	⊢ ( 𝑢 = ( 𝑣 −ℎ 𝑤 ) ↔ ( 𝑣 −ℎ 𝑤 ) = 𝑢 )
20		eqcom	⊢ ( 𝑣 = ( 𝑢 +ℎ 𝑤 ) ↔ ( 𝑢 +ℎ 𝑤 ) = 𝑣 )
21	18 19 20	3bitr4g	⊢ ( ( 𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐴 ∧ 𝑤 ∈ ( ⊥ ‘ 𝐵 ) ) → ( 𝑢 = ( 𝑣 −ℎ 𝑤 ) ↔ 𝑣 = ( 𝑢 +ℎ 𝑤 ) ) )
22	21	3expa	⊢ ( ( ( 𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐴 ) ∧ 𝑤 ∈ ( ⊥ ‘ 𝐵 ) ) → ( 𝑢 = ( 𝑣 −ℎ 𝑤 ) ↔ 𝑣 = ( 𝑢 +ℎ 𝑤 ) ) )
23	22	rexbidva	⊢ ( ( 𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐴 ) → ( ∃ 𝑤 ∈ ( ⊥ ‘ 𝐵 ) 𝑢 = ( 𝑣 −ℎ 𝑤 ) ↔ ∃ 𝑤 ∈ ( ⊥ ‘ 𝐵 ) 𝑣 = ( 𝑢 +ℎ 𝑤 ) ) )
24	8 23	bitr4d	⊢ ( ( 𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐴 ) → ( ( ( projℎ ‘ 𝐵 ) ‘ 𝑣 ) = 𝑢 ↔ ∃ 𝑤 ∈ ( ⊥ ‘ 𝐵 ) 𝑢 = ( 𝑣 −ℎ 𝑤 ) ) )
25	24	rexbidva	⊢ ( 𝑢 ∈ 𝐵 → ( ∃ 𝑣 ∈ 𝐴 ( ( projℎ ‘ 𝐵 ) ‘ 𝑣 ) = 𝑢 ↔ ∃ 𝑣 ∈ 𝐴 ∃ 𝑤 ∈ ( ⊥ ‘ 𝐵 ) 𝑢 = ( 𝑣 −ℎ 𝑤 ) ) )
26	2	pjfni	⊢ ( projℎ ‘ 𝐵 ) Fn ℋ
27	1	shssii	⊢ 𝐴 ⊆ ℋ
28		fvelimab	⊢ ( ( ( projℎ ‘ 𝐵 ) Fn ℋ ∧ 𝐴 ⊆ ℋ ) → ( 𝑢 ∈ ( ( projℎ ‘ 𝐵 ) “ 𝐴 ) ↔ ∃ 𝑣 ∈ 𝐴 ( ( projℎ ‘ 𝐵 ) ‘ 𝑣 ) = 𝑢 ) )
29	26 27 28	mp2an	⊢ ( 𝑢 ∈ ( ( projℎ ‘ 𝐵 ) “ 𝐴 ) ↔ ∃ 𝑣 ∈ 𝐴 ( ( projℎ ‘ 𝐵 ) ‘ 𝑣 ) = 𝑢 )
30	10	chshii	⊢ ( ⊥ ‘ 𝐵 ) ∈ Sℋ
31		shsel3	⊢ ( ( 𝐴 ∈ Sℋ ∧ ( ⊥ ‘ 𝐵 ) ∈ Sℋ ) → ( 𝑢 ∈ ( 𝐴 +ℋ ( ⊥ ‘ 𝐵 ) ) ↔ ∃ 𝑣 ∈ 𝐴 ∃ 𝑤 ∈ ( ⊥ ‘ 𝐵 ) 𝑢 = ( 𝑣 −ℎ 𝑤 ) ) )
32	1 30 31	mp2an	⊢ ( 𝑢 ∈ ( 𝐴 +ℋ ( ⊥ ‘ 𝐵 ) ) ↔ ∃ 𝑣 ∈ 𝐴 ∃ 𝑤 ∈ ( ⊥ ‘ 𝐵 ) 𝑢 = ( 𝑣 −ℎ 𝑤 ) )
33	25 29 32	3bitr4g	⊢ ( 𝑢 ∈ 𝐵 → ( 𝑢 ∈ ( ( projℎ ‘ 𝐵 ) “ 𝐴 ) ↔ 𝑢 ∈ ( 𝐴 +ℋ ( ⊥ ‘ 𝐵 ) ) ) )
34	33	pm5.32ri	⊢ ( ( 𝑢 ∈ ( ( projℎ ‘ 𝐵 ) “ 𝐴 ) ∧ 𝑢 ∈ 𝐵 ) ↔ ( 𝑢 ∈ ( 𝐴 +ℋ ( ⊥ ‘ 𝐵 ) ) ∧ 𝑢 ∈ 𝐵 ) )
35		imassrn	⊢ ( ( projℎ ‘ 𝐵 ) “ 𝐴 ) ⊆ ran ( projℎ ‘ 𝐵 )
36	2	pjrni	⊢ ran ( projℎ ‘ 𝐵 ) = 𝐵
37	35 36	sseqtri	⊢ ( ( projℎ ‘ 𝐵 ) “ 𝐴 ) ⊆ 𝐵
38	37	sseli	⊢ ( 𝑢 ∈ ( ( projℎ ‘ 𝐵 ) “ 𝐴 ) → 𝑢 ∈ 𝐵 )
39	38	pm4.71i	⊢ ( 𝑢 ∈ ( ( projℎ ‘ 𝐵 ) “ 𝐴 ) ↔ ( 𝑢 ∈ ( ( projℎ ‘ 𝐵 ) “ 𝐴 ) ∧ 𝑢 ∈ 𝐵 ) )
40		elin	⊢ ( 𝑢 ∈ ( ( 𝐴 +ℋ ( ⊥ ‘ 𝐵 ) ) ∩ 𝐵 ) ↔ ( 𝑢 ∈ ( 𝐴 +ℋ ( ⊥ ‘ 𝐵 ) ) ∧ 𝑢 ∈ 𝐵 ) )
41	34 39 40	3bitr4i	⊢ ( 𝑢 ∈ ( ( projℎ ‘ 𝐵 ) “ 𝐴 ) ↔ 𝑢 ∈ ( ( 𝐴 +ℋ ( ⊥ ‘ 𝐵 ) ) ∩ 𝐵 ) )
42	41	eqriv	⊢ ( ( projℎ ‘ 𝐵 ) “ 𝐴 ) = ( ( 𝐴 +ℋ ( ⊥ ‘ 𝐵 ) ) ∩ 𝐵 )