Metamath Proof Explorer

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 ⊢ A ∈ S ℋ
pjima.2 ⊢ B ∈ C ℋ
Assertion pjimai ⊢ proj ℎ ⁡ B A = A + ℋ ⊥ ⁡ B ∩ B

Proof

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