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ℎ⁡BA=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∈⊥⁡Bv=u+ℎw
5 2 3 4 sylancr ⊢v∈A→projℎ⁡B⁡v=u↔u∈B∧∃w∈⊥⁡Bv=u+ℎw
6 ibar ⊢u∈B→∃w∈⊥⁡Bv=u+ℎw↔u∈B∧∃w∈⊥⁡Bv=u+ℎw
7 6 bicomd ⊢u∈B→u∈B∧∃w∈⊥⁡Bv=u+ℎw↔∃w∈⊥⁡Bv=u+ℎw
8 5 7 sylan9bbr ⊢u∈B∧v∈A→projℎ⁡B⁡v=u↔∃w∈⊥⁡Bv=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∈⊥⁡Bu=v-ℎw↔∃w∈⊥⁡Bv=u+ℎw
24 8 23 bitr4d ⊢u∈B∧v∈A→projℎ⁡B⁡v=u↔∃w∈⊥⁡Bu=v-ℎw
25 24 rexbidva ⊢u∈B→∃v∈Aprojℎ⁡B⁡v=u↔∃v∈A∃w∈⊥⁡Bu=v-ℎw
26 2 pjfni ⊢projℎ⁡BFnℋ
27 1 shssii ⊢A⊆ℋ
28 fvelimab ⊢projℎ⁡BFnℋ∧A⊆ℋ→u∈projℎ⁡BA↔∃v∈Aprojℎ⁡B⁡v=u
29 26 27 28 mp2an ⊢u∈projℎ⁡BA↔∃v∈Aprojℎ⁡B⁡v=u
30 10 chshii ⊢⊥⁡B∈Sℋ
31 shsel3 ⊢A∈Sℋ∧⊥⁡B∈Sℋ→u∈A+ℋ⊥⁡B↔∃v∈A∃w∈⊥⁡Bu=v-ℎw
32 1 30 31 mp2an ⊢u∈A+ℋ⊥⁡B↔∃v∈A∃w∈⊥⁡Bu=v-ℎw
33 25 29 32 3bitr4g ⊢u∈B→u∈projℎ⁡BA↔u∈A+ℋ⊥⁡B
34 33 pm5.32ri ⊢u∈projℎ⁡BA∧u∈B↔u∈A+ℋ⊥⁡B∧u∈B
35 imassrn ⊢projℎ⁡BA⊆ran⁡projℎ⁡B
36 2 pjrni ⊢ran⁡projℎ⁡B=B
37 35 36 sseqtri ⊢projℎ⁡BA⊆B
38 37 sseli ⊢u∈projℎ⁡BA→u∈B
39 38 pm4.71i ⊢u∈projℎ⁡BA↔u∈projℎ⁡BA∧u∈B
40 elin ⊢u∈A+ℋ⊥⁡B∩B↔u∈A+ℋ⊥⁡B∧u∈B
41 34 39 40 3bitr4i ⊢u∈projℎ⁡BA↔u∈A+ℋ⊥⁡B∩B
42 41 eqriv ⊢projℎ⁡BA=A+ℋ⊥⁡B∩B