Metamath Proof Explorer

Theorem pjpreeq

Description: Equality with a projection. This version of pjeq does not assume the Axiom of Choice via pjhth . (Contributed by Mario Carneiro, 15-May-2014) (New usage is discouraged.)

Ref Expression
Assertion pjpreeq 
|- ( ( H e. CH /\ A e. ( H +H ( _|_ ` H ) ) ) -> ( ( ( projh ` H ) ` A ) = B <-> ( B e. H /\ E. x e. ( _|_ ` H ) A = ( B +h x ) ) ) )

Proof

Step Hyp Ref Expression
1 chsh 
 |-  ( H e. CH -> H e. SH )
2 shocsh 
 |-  ( H e. SH -> ( _|_ ` H ) e. SH )
3 shsel 
 |-  ( ( H e. SH /\ ( _|_ ` H ) e. SH ) -> ( A e. ( H +H ( _|_ ` H ) ) <-> E. y e. H E. x e. ( _|_ ` H ) A = ( y +h x ) ) )
4 1 2 3 syl2anc2 
 |-  ( H e. CH -> ( A e. ( H +H ( _|_ ` H ) ) <-> E. y e. H E. x e. ( _|_ ` H ) A = ( y +h x ) ) )
5 4 biimpa 
 |-  ( ( H e. CH /\ A e. ( H +H ( _|_ ` H ) ) ) -> E. y e. H E. x e. ( _|_ ` H ) A = ( y +h x ) )
6 1 2 syl 
 |-  ( H e. CH -> ( _|_ ` H ) e. SH )
7 ocin 
 |-  ( H e. SH -> ( H i^i ( _|_ ` H ) ) = 0H )
8 1 7 syl 
 |-  ( H e. CH -> ( H i^i ( _|_ ` H ) ) = 0H )
9 pjhthmo 
 |-  ( ( H e. SH /\ ( _|_ ` H ) e. SH /\ ( H i^i ( _|_ ` H ) ) = 0H ) -> E* y ( y e. H /\ E. x e. ( _|_ ` H ) A = ( y +h x ) ) )
10 1 6 8 9 syl3anc 
 |-  ( H e. CH -> E* y ( y e. H /\ E. x e. ( _|_ ` H ) A = ( y +h x ) ) )
11 10 adantr 
 |-  ( ( H e. CH /\ A e. ( H +H ( _|_ ` H ) ) ) -> E* y ( y e. H /\ E. x e. ( _|_ ` H ) A = ( y +h x ) ) )
12 reu5 
 |-  ( E! y e. H E. x e. ( _|_ ` H ) A = ( y +h x ) <-> ( E. y e. H E. x e. ( _|_ ` H ) A = ( y +h x ) /\ E* y e. H E. x e. ( _|_ ` H ) A = ( y +h x ) ) )
13 df-rmo 
 |-  ( E* y e. H E. x e. ( _|_ ` H ) A = ( y +h x ) <-> E* y ( y e. H /\ E. x e. ( _|_ ` H ) A = ( y +h x ) ) )
14 13 anbi2i 
 |-  ( ( E. y e. H E. x e. ( _|_ ` H ) A = ( y +h x ) /\ E* y e. H E. x e. ( _|_ ` H ) A = ( y +h x ) ) <-> ( E. y e. H E. x e. ( _|_ ` H ) A = ( y +h x ) /\ E* y ( y e. H /\ E. x e. ( _|_ ` H ) A = ( y +h x ) ) ) )
15 12 14 bitri 
 |-  ( E! y e. H E. x e. ( _|_ ` H ) A = ( y +h x ) <-> ( E. y e. H E. x e. ( _|_ ` H ) A = ( y +h x ) /\ E* y ( y e. H /\ E. x e. ( _|_ ` H ) A = ( y +h x ) ) ) )
16 5 11 15 sylanbrc 
 |-  ( ( H e. CH /\ A e. ( H +H ( _|_ ` H ) ) ) -> E! y e. H E. x e. ( _|_ ` H ) A = ( y +h x ) )
17 riotacl 
 |-  ( E! y e. H E. x e. ( _|_ ` H ) A = ( y +h x ) -> ( iota_ y e. H E. x e. ( _|_ ` H ) A = ( y +h x ) ) e. H )
18 16 17 syl 
 |-  ( ( H e. CH /\ A e. ( H +H ( _|_ ` H ) ) ) -> ( iota_ y e. H E. x e. ( _|_ ` H ) A = ( y +h x ) ) e. H )
19 eleq1 
 |-  ( ( iota_ y e. H E. x e. ( _|_ ` H ) A = ( y +h x ) ) = B -> ( ( iota_ y e. H E. x e. ( _|_ ` H ) A = ( y +h x ) ) e. H <-> B e. H ) )
20 18 19 syl5ibcom 
 |-  ( ( H e. CH /\ A e. ( H +H ( _|_ ` H ) ) ) -> ( ( iota_ y e. H E. x e. ( _|_ ` H ) A = ( y +h x ) ) = B -> B e. H ) )
21 20 pm4.71rd 
 |-  ( ( H e. CH /\ A e. ( H +H ( _|_ ` H ) ) ) -> ( ( iota_ y e. H E. x e. ( _|_ ` H ) A = ( y +h x ) ) = B <-> ( B e. H /\ ( iota_ y e. H E. x e. ( _|_ ` H ) A = ( y +h x ) ) = B ) ) )
22 shsss 
 |-  ( ( H e. SH /\ ( _|_ ` H ) e. SH ) -> ( H +H ( _|_ ` H ) ) C_ ~H )
23 1 2 22 syl2anc2 
 |-  ( H e. CH -> ( H +H ( _|_ ` H ) ) C_ ~H )
24 23 sselda 
 |-  ( ( H e. CH /\ A e. ( H +H ( _|_ ` H ) ) ) -> A e. ~H )
25 pjhval 
 |-  ( ( H e. CH /\ A e. ~H ) -> ( ( projh ` H ) ` A ) = ( iota_ y e. H E. x e. ( _|_ ` H ) A = ( y +h x ) ) )
26 24 25 syldan 
 |-  ( ( H e. CH /\ A e. ( H +H ( _|_ ` H ) ) ) -> ( ( projh ` H ) ` A ) = ( iota_ y e. H E. x e. ( _|_ ` H ) A = ( y +h x ) ) )
27 26 eqeq1d 
 |-  ( ( H e. CH /\ A e. ( H +H ( _|_ ` H ) ) ) -> ( ( ( projh ` H ) ` A ) = B <-> ( iota_ y e. H E. x e. ( _|_ ` H ) A = ( y +h x ) ) = B ) )
28 id 
 |-  ( B e. H -> B e. H )
29 oveq1 
 |-  ( y = B -> ( y +h x ) = ( B +h x ) )
30 29 eqeq2d 
 |-  ( y = B -> ( A = ( y +h x ) <-> A = ( B +h x ) ) )
31 30 rexbidv 
 |-  ( y = B -> ( E. x e. ( _|_ ` H ) A = ( y +h x ) <-> E. x e. ( _|_ ` H ) A = ( B +h x ) ) )
32 31 riota2 
 |-  ( ( B e. H /\ E! y e. H E. x e. ( _|_ ` H ) A = ( y +h x ) ) -> ( E. x e. ( _|_ ` H ) A = ( B +h x ) <-> ( iota_ y e. H E. x e. ( _|_ ` H ) A = ( y +h x ) ) = B ) )
33 28 16 32 syl2anr 
 |-  ( ( ( H e. CH /\ A e. ( H +H ( _|_ ` H ) ) ) /\ B e. H ) -> ( E. x e. ( _|_ ` H ) A = ( B +h x ) <-> ( iota_ y e. H E. x e. ( _|_ ` H ) A = ( y +h x ) ) = B ) )
34 33 pm5.32da 
 |-  ( ( H e. CH /\ A e. ( H +H ( _|_ ` H ) ) ) -> ( ( B e. H /\ E. x e. ( _|_ ` H ) A = ( B +h x ) ) <-> ( B e. H /\ ( iota_ y e. H E. x e. ( _|_ ` H ) A = ( y +h x ) ) = B ) ) )
35 21 27 34 3bitr4d 
 |-  ( ( H e. CH /\ A e. ( H +H ( _|_ ` H ) ) ) -> ( ( ( projh ` H ) ` A ) = B <-> ( B e. H /\ E. x e. ( _|_ ` H ) A = ( B +h x ) ) ) )