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 e. SH
pjima.2 
|- B e. CH
Assertion pjimai 
|- ( ( projh ` B ) " A ) = ( ( A +H ( _|_ ` B ) ) i^i B )

Proof

Step Hyp Ref Expression
1 pjima.1 
 |-  A e. SH
2 pjima.2 
 |-  B e. CH
3 1 sheli 
 |-  ( v e. A -> v e. ~H )
4 pjeq 
 |-  ( ( B e. CH /\ v e. ~H ) -> ( ( ( projh ` B ) ` v ) = u <-> ( u e. B /\ E. w e. ( _|_ ` B ) v = ( u +h w ) ) ) )
5 2 3 4 sylancr 
 |-  ( v e. A -> ( ( ( projh ` B ) ` v ) = u <-> ( u e. B /\ E. w e. ( _|_ ` B ) v = ( u +h w ) ) ) )
6 ibar 
 |-  ( u e. B -> ( E. w e. ( _|_ ` B ) v = ( u +h w ) <-> ( u e. B /\ E. w e. ( _|_ ` B ) v = ( u +h w ) ) ) )
7 6 bicomd 
 |-  ( u e. B -> ( ( u e. B /\ E. w e. ( _|_ ` B ) v = ( u +h w ) ) <-> E. w e. ( _|_ ` B ) v = ( u +h w ) ) )
8 5 7 sylan9bbr 
 |-  ( ( u e. B /\ v e. A ) -> ( ( ( projh ` B ) ` v ) = u <-> E. w e. ( _|_ ` B ) v = ( u +h w ) ) )
9 2 cheli 
 |-  ( u e. B -> u e. ~H )
10 2 choccli 
 |-  ( _|_ ` B ) e. CH
11 10 cheli 
 |-  ( w e. ( _|_ ` B ) -> w e. ~H )
12 hvsubadd 
 |-  ( ( v e. ~H /\ w e. ~H /\ u e. ~H ) -> ( ( v -h w ) = u <-> ( w +h u ) = v ) )
13 12 3comr 
 |-  ( ( u e. ~H /\ v e. ~H /\ w e. ~H ) -> ( ( v -h w ) = u <-> ( w +h u ) = v ) )
14 ax-hvcom 
 |-  ( ( u e. ~H /\ w e. ~H ) -> ( u +h w ) = ( w +h u ) )
15 14 3adant2 
 |-  ( ( u e. ~H /\ v e. ~H /\ w e. ~H ) -> ( u +h w ) = ( w +h u ) )
16 15 eqeq1d 
 |-  ( ( u e. ~H /\ v e. ~H /\ w e. ~H ) -> ( ( u +h w ) = v <-> ( w +h u ) = v ) )
17 13 16 bitr4d 
 |-  ( ( u e. ~H /\ v e. ~H /\ w e. ~H ) -> ( ( v -h w ) = u <-> ( u +h w ) = v ) )
18 9 3 11 17 syl3an 
 |-  ( ( u e. B /\ v e. A /\ w e. ( _|_ ` B ) ) -> ( ( v -h w ) = u <-> ( u +h w ) = v ) )
19 eqcom 
 |-  ( u = ( v -h w ) <-> ( v -h w ) = u )
20 eqcom 
 |-  ( v = ( u +h w ) <-> ( u +h w ) = v )
21 18 19 20 3bitr4g 
 |-  ( ( u e. B /\ v e. A /\ w e. ( _|_ ` B ) ) -> ( u = ( v -h w ) <-> v = ( u +h w ) ) )
22 21 3expa 
 |-  ( ( ( u e. B /\ v e. A ) /\ w e. ( _|_ ` B ) ) -> ( u = ( v -h w ) <-> v = ( u +h w ) ) )
23 22 rexbidva 
 |-  ( ( u e. B /\ v e. A ) -> ( E. w e. ( _|_ ` B ) u = ( v -h w ) <-> E. w e. ( _|_ ` B ) v = ( u +h w ) ) )
24 8 23 bitr4d 
 |-  ( ( u e. B /\ v e. A ) -> ( ( ( projh ` B ) ` v ) = u <-> E. w e. ( _|_ ` B ) u = ( v -h w ) ) )
25 24 rexbidva 
 |-  ( u e. B -> ( E. v e. A ( ( projh ` B ) ` v ) = u <-> E. v e. A E. w e. ( _|_ ` B ) u = ( v -h w ) ) )
26 2 pjfni 
 |-  ( projh ` B ) Fn ~H
27 1 shssii 
 |-  A C_ ~H
28 fvelimab 
 |-  ( ( ( projh ` B ) Fn ~H /\ A C_ ~H ) -> ( u e. ( ( projh ` B ) " A ) <-> E. v e. A ( ( projh ` B ) ` v ) = u ) )
29 26 27 28 mp2an 
 |-  ( u e. ( ( projh ` B ) " A ) <-> E. v e. A ( ( projh ` B ) ` v ) = u )
30 10 chshii 
 |-  ( _|_ ` B ) e. SH
31 shsel3 
 |-  ( ( A e. SH /\ ( _|_ ` B ) e. SH ) -> ( u e. ( A +H ( _|_ ` B ) ) <-> E. v e. A E. w e. ( _|_ ` B ) u = ( v -h w ) ) )
32 1 30 31 mp2an 
 |-  ( u e. ( A +H ( _|_ ` B ) ) <-> E. v e. A E. w e. ( _|_ ` B ) u = ( v -h w ) )
33 25 29 32 3bitr4g 
 |-  ( u e. B -> ( u e. ( ( projh ` B ) " A ) <-> u e. ( A +H ( _|_ ` B ) ) ) )
34 33 pm5.32ri 
 |-  ( ( u e. ( ( projh ` B ) " A ) /\ u e. B ) <-> ( u e. ( A +H ( _|_ ` B ) ) /\ u e. B ) )
35 imassrn 
 |-  ( ( projh ` B ) " A ) C_ ran ( projh ` B )
36 2 pjrni 
 |-  ran ( projh ` B ) = B
37 35 36 sseqtri 
 |-  ( ( projh ` B ) " A ) C_ B
38 37 sseli 
 |-  ( u e. ( ( projh ` B ) " A ) -> u e. B )
39 38 pm4.71i 
 |-  ( u e. ( ( projh ` B ) " A ) <-> ( u e. ( ( projh ` B ) " A ) /\ u e. B ) )
40 elin 
 |-  ( u e. ( ( A +H ( _|_ ` B ) ) i^i B ) <-> ( u e. ( A +H ( _|_ ` B ) ) /\ u e. B ) )
41 34 39 40 3bitr4i 
 |-  ( u e. ( ( projh ` B ) " A ) <-> u e. ( ( A +H ( _|_ ` B ) ) i^i B ) )
42 41 eqriv 
 |-  ( ( projh ` B ) " A ) = ( ( A +H ( _|_ ` B ) ) i^i B )