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 ( ( 𝐻 ∈ Cℋ ∧ 𝐴 ∈ ( 𝐻 +ℋ ( ⊥ ‘ 𝐻 ) ) ) → ( ( ( projℎ ‘ 𝐻 ) ‘ 𝐴 ) = 𝐵 ↔ ( 𝐵 ∈ 𝐻 ∧ ∃ 𝑥 ∈ ( ⊥ ‘ 𝐻 ) 𝐴 = ( 𝐵 +ℎ 𝑥 ) ) ) )

Proof

Step Hyp Ref Expression
1 chsh ⊢ ( 𝐻 ∈ Cℋ → 𝐻 ∈ Sℋ )
2 shocsh ⊢ ( 𝐻 ∈ Sℋ → ( ⊥ ‘ 𝐻 ) ∈ Sℋ )
3 shsel ⊢ ( ( 𝐻 ∈ Sℋ ∧ ( ⊥ ‘ 𝐻 ) ∈ Sℋ ) → ( 𝐴 ∈ ( 𝐻 +ℋ ( ⊥ ‘ 𝐻 ) ) ↔ ∃ 𝑦 ∈ 𝐻 ∃ 𝑥 ∈ ( ⊥ ‘ 𝐻 ) 𝐴 = ( 𝑦 +ℎ 𝑥 ) ) )
4 1 2 3 syl2anc2 ⊢ ( 𝐻 ∈ Cℋ → ( 𝐴 ∈ ( 𝐻 +ℋ ( ⊥ ‘ 𝐻 ) ) ↔ ∃ 𝑦 ∈ 𝐻 ∃ 𝑥 ∈ ( ⊥ ‘ 𝐻 ) 𝐴 = ( 𝑦 +ℎ 𝑥 ) ) )
5 4 biimpa ⊢ ( ( 𝐻 ∈ Cℋ ∧ 𝐴 ∈ ( 𝐻 +ℋ ( ⊥ ‘ 𝐻 ) ) ) → ∃ 𝑦 ∈ 𝐻 ∃ 𝑥 ∈ ( ⊥ ‘ 𝐻 ) 𝐴 = ( 𝑦 +ℎ 𝑥 ) )
6 1 2 syl ⊢ ( 𝐻 ∈ Cℋ → ( ⊥ ‘ 𝐻 ) ∈ Sℋ )
7 ocin ⊢ ( 𝐻 ∈ Sℋ → ( 𝐻 ∩ ( ⊥ ‘ 𝐻 ) ) = 0ℋ )
8 1 7 syl ⊢ ( 𝐻 ∈ Cℋ → ( 𝐻 ∩ ( ⊥ ‘ 𝐻 ) ) = 0ℋ )
9 pjhthmo ⊢ ( ( 𝐻 ∈ Sℋ ∧ ( ⊥ ‘ 𝐻 ) ∈ Sℋ ∧ ( 𝐻 ∩ ( ⊥ ‘ 𝐻 ) ) = 0ℋ ) → ∃* 𝑦 ( 𝑦 ∈ 𝐻 ∧ ∃ 𝑥 ∈ ( ⊥ ‘ 𝐻 ) 𝐴 = ( 𝑦 +ℎ 𝑥 ) ) )
10 1 6 8 9 syl3anc ⊢ ( 𝐻 ∈ Cℋ → ∃* 𝑦 ( 𝑦 ∈ 𝐻 ∧ ∃ 𝑥 ∈ ( ⊥ ‘ 𝐻 ) 𝐴 = ( 𝑦 +ℎ 𝑥 ) ) )
11 10 adantr ⊢ ( ( 𝐻 ∈ Cℋ ∧ 𝐴 ∈ ( 𝐻 +ℋ ( ⊥ ‘ 𝐻 ) ) ) → ∃* 𝑦 ( 𝑦 ∈ 𝐻 ∧ ∃ 𝑥 ∈ ( ⊥ ‘ 𝐻 ) 𝐴 = ( 𝑦 +ℎ 𝑥 ) ) )
12 reu5 ⊢ ( ∃! 𝑦 ∈ 𝐻 ∃ 𝑥 ∈ ( ⊥ ‘ 𝐻 ) 𝐴 = ( 𝑦 +ℎ 𝑥 ) ↔ ( ∃ 𝑦 ∈ 𝐻 ∃ 𝑥 ∈ ( ⊥ ‘ 𝐻 ) 𝐴 = ( 𝑦 +ℎ 𝑥 ) ∧ ∃* 𝑦 ∈ 𝐻 ∃ 𝑥 ∈ ( ⊥ ‘ 𝐻 ) 𝐴 = ( 𝑦 +ℎ 𝑥 ) ) )
13 df-rmo ⊢ ( ∃* 𝑦 ∈ 𝐻 ∃ 𝑥 ∈ ( ⊥ ‘ 𝐻 ) 𝐴 = ( 𝑦 +ℎ 𝑥 ) ↔ ∃* 𝑦 ( 𝑦 ∈ 𝐻 ∧ ∃ 𝑥 ∈ ( ⊥ ‘ 𝐻 ) 𝐴 = ( 𝑦 +ℎ 𝑥 ) ) )
14 13 anbi2i ⊢ ( ( ∃ 𝑦 ∈ 𝐻 ∃ 𝑥 ∈ ( ⊥ ‘ 𝐻 ) 𝐴 = ( 𝑦 +ℎ 𝑥 ) ∧ ∃* 𝑦 ∈ 𝐻 ∃ 𝑥 ∈ ( ⊥ ‘ 𝐻 ) 𝐴 = ( 𝑦 +ℎ 𝑥 ) ) ↔ ( ∃ 𝑦 ∈ 𝐻 ∃ 𝑥 ∈ ( ⊥ ‘ 𝐻 ) 𝐴 = ( 𝑦 +ℎ 𝑥 ) ∧ ∃* 𝑦 ( 𝑦 ∈ 𝐻 ∧ ∃ 𝑥 ∈ ( ⊥ ‘ 𝐻 ) 𝐴 = ( 𝑦 +ℎ 𝑥 ) ) ) )
15 12 14 bitri ⊢ ( ∃! 𝑦 ∈ 𝐻 ∃ 𝑥 ∈ ( ⊥ ‘ 𝐻 ) 𝐴 = ( 𝑦 +ℎ 𝑥 ) ↔ ( ∃ 𝑦 ∈ 𝐻 ∃ 𝑥 ∈ ( ⊥ ‘ 𝐻 ) 𝐴 = ( 𝑦 +ℎ 𝑥 ) ∧ ∃* 𝑦 ( 𝑦 ∈ 𝐻 ∧ ∃ 𝑥 ∈ ( ⊥ ‘ 𝐻 ) 𝐴 = ( 𝑦 +ℎ 𝑥 ) ) ) )
16 5 11 15 sylanbrc ⊢ ( ( 𝐻 ∈ Cℋ ∧ 𝐴 ∈ ( 𝐻 +ℋ ( ⊥ ‘ 𝐻 ) ) ) → ∃! 𝑦 ∈ 𝐻 ∃ 𝑥 ∈ ( ⊥ ‘ 𝐻 ) 𝐴 = ( 𝑦 +ℎ 𝑥 ) )
17 riotacl ⊢ ( ∃! 𝑦 ∈ 𝐻 ∃ 𝑥 ∈ ( ⊥ ‘ 𝐻 ) 𝐴 = ( 𝑦 +ℎ 𝑥 ) → ( ℩ 𝑦 ∈ 𝐻 ∃ 𝑥 ∈ ( ⊥ ‘ 𝐻 ) 𝐴 = ( 𝑦 +ℎ 𝑥 ) ) ∈ 𝐻 )
18 16 17 syl ⊢ ( ( 𝐻 ∈ Cℋ ∧ 𝐴 ∈ ( 𝐻 +ℋ ( ⊥ ‘ 𝐻 ) ) ) → ( ℩ 𝑦 ∈ 𝐻 ∃ 𝑥 ∈ ( ⊥ ‘ 𝐻 ) 𝐴 = ( 𝑦 +ℎ 𝑥 ) ) ∈ 𝐻 )
19 eleq1 ⊢ ( ( ℩ 𝑦 ∈ 𝐻 ∃ 𝑥 ∈ ( ⊥ ‘ 𝐻 ) 𝐴 = ( 𝑦 +ℎ 𝑥 ) ) = 𝐵 → ( ( ℩ 𝑦 ∈ 𝐻 ∃ 𝑥 ∈ ( ⊥ ‘ 𝐻 ) 𝐴 = ( 𝑦 +ℎ 𝑥 ) ) ∈ 𝐻 ↔ 𝐵 ∈ 𝐻 ) )
20 18 19 syl5ibcom ⊢ ( ( 𝐻 ∈ Cℋ ∧ 𝐴 ∈ ( 𝐻 +ℋ ( ⊥ ‘ 𝐻 ) ) ) → ( ( ℩ 𝑦 ∈ 𝐻 ∃ 𝑥 ∈ ( ⊥ ‘ 𝐻 ) 𝐴 = ( 𝑦 +ℎ 𝑥 ) ) = 𝐵 → 𝐵 ∈ 𝐻 ) )
21 20 pm4.71rd ⊢ ( ( 𝐻 ∈ Cℋ ∧ 𝐴 ∈ ( 𝐻 +ℋ ( ⊥ ‘ 𝐻 ) ) ) → ( ( ℩ 𝑦 ∈ 𝐻 ∃ 𝑥 ∈ ( ⊥ ‘ 𝐻 ) 𝐴 = ( 𝑦 +ℎ 𝑥 ) ) = 𝐵 ↔ ( 𝐵 ∈ 𝐻 ∧ ( ℩ 𝑦 ∈ 𝐻 ∃ 𝑥 ∈ ( ⊥ ‘ 𝐻 ) 𝐴 = ( 𝑦 +ℎ 𝑥 ) ) = 𝐵 ) ) )
22 shsss ⊢ ( ( 𝐻 ∈ Sℋ ∧ ( ⊥ ‘ 𝐻 ) ∈ Sℋ ) → ( 𝐻 +ℋ ( ⊥ ‘ 𝐻 ) ) ⊆ ℋ )
23 1 2 22 syl2anc2 ⊢ ( 𝐻 ∈ Cℋ → ( 𝐻 +ℋ ( ⊥ ‘ 𝐻 ) ) ⊆ ℋ )
24 23 sselda ⊢ ( ( 𝐻 ∈ Cℋ ∧ 𝐴 ∈ ( 𝐻 +ℋ ( ⊥ ‘ 𝐻 ) ) ) → 𝐴 ∈ ℋ )
25 pjhval ⊢ ( ( 𝐻 ∈ Cℋ ∧ 𝐴 ∈ ℋ ) → ( ( projℎ ‘ 𝐻 ) ‘ 𝐴 ) = ( ℩ 𝑦 ∈ 𝐻 ∃ 𝑥 ∈ ( ⊥ ‘ 𝐻 ) 𝐴 = ( 𝑦 +ℎ 𝑥 ) ) )
26 24 25 syldan ⊢ ( ( 𝐻 ∈ Cℋ ∧ 𝐴 ∈ ( 𝐻 +ℋ ( ⊥ ‘ 𝐻 ) ) ) → ( ( projℎ ‘ 𝐻 ) ‘ 𝐴 ) = ( ℩ 𝑦 ∈ 𝐻 ∃ 𝑥 ∈ ( ⊥ ‘ 𝐻 ) 𝐴 = ( 𝑦 +ℎ 𝑥 ) ) )
27 26 eqeq1d ⊢ ( ( 𝐻 ∈ Cℋ ∧ 𝐴 ∈ ( 𝐻 +ℋ ( ⊥ ‘ 𝐻 ) ) ) → ( ( ( projℎ ‘ 𝐻 ) ‘ 𝐴 ) = 𝐵 ↔ ( ℩ 𝑦 ∈ 𝐻 ∃ 𝑥 ∈ ( ⊥ ‘ 𝐻 ) 𝐴 = ( 𝑦 +ℎ 𝑥 ) ) = 𝐵 ) )
28 id ⊢ ( 𝐵 ∈ 𝐻 → 𝐵 ∈ 𝐻 )
29 oveq1 ⊢ ( 𝑦 = 𝐵 → ( 𝑦 +ℎ 𝑥 ) = ( 𝐵 +ℎ 𝑥 ) )
30 29 eqeq2d ⊢ ( 𝑦 = 𝐵 → ( 𝐴 = ( 𝑦 +ℎ 𝑥 ) ↔ 𝐴 = ( 𝐵 +ℎ 𝑥 ) ) )
31 30 rexbidv ⊢ ( 𝑦 = 𝐵 → ( ∃ 𝑥 ∈ ( ⊥ ‘ 𝐻 ) 𝐴 = ( 𝑦 +ℎ 𝑥 ) ↔ ∃ 𝑥 ∈ ( ⊥ ‘ 𝐻 ) 𝐴 = ( 𝐵 +ℎ 𝑥 ) ) )
32 31 riota2 ⊢ ( ( 𝐵 ∈ 𝐻 ∧ ∃! 𝑦 ∈ 𝐻 ∃ 𝑥 ∈ ( ⊥ ‘ 𝐻 ) 𝐴 = ( 𝑦 +ℎ 𝑥 ) ) → ( ∃ 𝑥 ∈ ( ⊥ ‘ 𝐻 ) 𝐴 = ( 𝐵 +ℎ 𝑥 ) ↔ ( ℩ 𝑦 ∈ 𝐻 ∃ 𝑥 ∈ ( ⊥ ‘ 𝐻 ) 𝐴 = ( 𝑦 +ℎ 𝑥 ) ) = 𝐵 ) )
33 28 16 32 syl2anr ⊢ ( ( ( 𝐻 ∈ Cℋ ∧ 𝐴 ∈ ( 𝐻 +ℋ ( ⊥ ‘ 𝐻 ) ) ) ∧ 𝐵 ∈ 𝐻 ) → ( ∃ 𝑥 ∈ ( ⊥ ‘ 𝐻 ) 𝐴 = ( 𝐵 +ℎ 𝑥 ) ↔ ( ℩ 𝑦 ∈ 𝐻 ∃ 𝑥 ∈ ( ⊥ ‘ 𝐻 ) 𝐴 = ( 𝑦 +ℎ 𝑥 ) ) = 𝐵 ) )
34 33 pm5.32da ⊢ ( ( 𝐻 ∈ Cℋ ∧ 𝐴 ∈ ( 𝐻 +ℋ ( ⊥ ‘ 𝐻 ) ) ) → ( ( 𝐵 ∈ 𝐻 ∧ ∃ 𝑥 ∈ ( ⊥ ‘ 𝐻 ) 𝐴 = ( 𝐵 +ℎ 𝑥 ) ) ↔ ( 𝐵 ∈ 𝐻 ∧ ( ℩ 𝑦 ∈ 𝐻 ∃ 𝑥 ∈ ( ⊥ ‘ 𝐻 ) 𝐴 = ( 𝑦 +ℎ 𝑥 ) ) = 𝐵 ) ) )
35 21 27 34 3bitr4d ⊢ ( ( 𝐻 ∈ Cℋ ∧ 𝐴 ∈ ( 𝐻 +ℋ ( ⊥ ‘ 𝐻 ) ) ) → ( ( ( projℎ ‘ 𝐻 ) ‘ 𝐴 ) = 𝐵 ↔ ( 𝐵 ∈ 𝐻 ∧ ∃ 𝑥 ∈ ( ⊥ ‘ 𝐻 ) 𝐴 = ( 𝐵 +ℎ 𝑥 ) ) ) )