Metamath Proof Explorer

Theorem pjhtheu2

Description: Uniqueness of y for the projection theorem. (Contributed by NM, 6-Nov-1999) (Revised by Mario Carneiro, 15-May-2014) (New usage is discouraged.)

Ref Expression
Assertion pjhtheu2 ( ( 𝐻 ∈ Cℋ ∧ 𝐴 ∈ ℋ ) → ∃! 𝑦 ∈ ( ⊥ ‘ 𝐻 ) ∃ 𝑥 ∈ 𝐻 𝐴 = ( 𝑥 +ℎ 𝑦 ) )

Proof

Step Hyp Ref Expression
1 choccl ⊢ ( 𝐻 ∈ Cℋ → ( ⊥ ‘ 𝐻 ) ∈ Cℋ )
2 pjhtheu ⊢ ( ( ( ⊥ ‘ 𝐻 ) ∈ Cℋ ∧ 𝐴 ∈ ℋ ) → ∃! 𝑦 ∈ ( ⊥ ‘ 𝐻 ) ∃ 𝑥 ∈ ( ⊥ ‘ ( ⊥ ‘ 𝐻 ) ) 𝐴 = ( 𝑦 +ℎ 𝑥 ) )
3 1 2 sylan ⊢ ( ( 𝐻 ∈ Cℋ ∧ 𝐴 ∈ ℋ ) → ∃! 𝑦 ∈ ( ⊥ ‘ 𝐻 ) ∃ 𝑥 ∈ ( ⊥ ‘ ( ⊥ ‘ 𝐻 ) ) 𝐴 = ( 𝑦 +ℎ 𝑥 ) )
4 simpll ⊢ ( ( ( 𝐻 ∈ Cℋ ∧ 𝐴 ∈ ℋ ) ∧ 𝑦 ∈ ( ⊥ ‘ 𝐻 ) ) → 𝐻 ∈ Cℋ )
5 ococ ⊢ ( 𝐻 ∈ Cℋ → ( ⊥ ‘ ( ⊥ ‘ 𝐻 ) ) = 𝐻 )
6 4 5 syl ⊢ ( ( ( 𝐻 ∈ Cℋ ∧ 𝐴 ∈ ℋ ) ∧ 𝑦 ∈ ( ⊥ ‘ 𝐻 ) ) → ( ⊥ ‘ ( ⊥ ‘ 𝐻 ) ) = 𝐻 )
7 6 rexeqdv ⊢ ( ( ( 𝐻 ∈ Cℋ ∧ 𝐴 ∈ ℋ ) ∧ 𝑦 ∈ ( ⊥ ‘ 𝐻 ) ) → ( ∃ 𝑥 ∈ ( ⊥ ‘ ( ⊥ ‘ 𝐻 ) ) 𝐴 = ( 𝑦 +ℎ 𝑥 ) ↔ ∃ 𝑥 ∈ 𝐻 𝐴 = ( 𝑦 +ℎ 𝑥 ) ) )
8 1 adantr ⊢ ( ( 𝐻 ∈ Cℋ ∧ 𝐴 ∈ ℋ ) → ( ⊥ ‘ 𝐻 ) ∈ Cℋ )
9 chel ⊢ ( ( ( ⊥ ‘ 𝐻 ) ∈ Cℋ ∧ 𝑦 ∈ ( ⊥ ‘ 𝐻 ) ) → 𝑦 ∈ ℋ )
10 8 9 sylan ⊢ ( ( ( 𝐻 ∈ Cℋ ∧ 𝐴 ∈ ℋ ) ∧ 𝑦 ∈ ( ⊥ ‘ 𝐻 ) ) → 𝑦 ∈ ℋ )
11 10 adantr ⊢ ( ( ( ( 𝐻 ∈ Cℋ ∧ 𝐴 ∈ ℋ ) ∧ 𝑦 ∈ ( ⊥ ‘ 𝐻 ) ) ∧ 𝑥 ∈ 𝐻 ) → 𝑦 ∈ ℋ )
12 chel ⊢ ( ( 𝐻 ∈ Cℋ ∧ 𝑥 ∈ 𝐻 ) → 𝑥 ∈ ℋ )
13 4 12 sylan ⊢ ( ( ( ( 𝐻 ∈ Cℋ ∧ 𝐴 ∈ ℋ ) ∧ 𝑦 ∈ ( ⊥ ‘ 𝐻 ) ) ∧ 𝑥 ∈ 𝐻 ) → 𝑥 ∈ ℋ )
14 ax-hvcom ⊢ ( ( 𝑦 ∈ ℋ ∧ 𝑥 ∈ ℋ ) → ( 𝑦 +ℎ 𝑥 ) = ( 𝑥 +ℎ 𝑦 ) )
15 11 13 14 syl2anc ⊢ ( ( ( ( 𝐻 ∈ Cℋ ∧ 𝐴 ∈ ℋ ) ∧ 𝑦 ∈ ( ⊥ ‘ 𝐻 ) ) ∧ 𝑥 ∈ 𝐻 ) → ( 𝑦 +ℎ 𝑥 ) = ( 𝑥 +ℎ 𝑦 ) )
16 15 eqeq2d ⊢ ( ( ( ( 𝐻 ∈ Cℋ ∧ 𝐴 ∈ ℋ ) ∧ 𝑦 ∈ ( ⊥ ‘ 𝐻 ) ) ∧ 𝑥 ∈ 𝐻 ) → ( 𝐴 = ( 𝑦 +ℎ 𝑥 ) ↔ 𝐴 = ( 𝑥 +ℎ 𝑦 ) ) )
17 16 rexbidva ⊢ ( ( ( 𝐻 ∈ Cℋ ∧ 𝐴 ∈ ℋ ) ∧ 𝑦 ∈ ( ⊥ ‘ 𝐻 ) ) → ( ∃ 𝑥 ∈ 𝐻 𝐴 = ( 𝑦 +ℎ 𝑥 ) ↔ ∃ 𝑥 ∈ 𝐻 𝐴 = ( 𝑥 +ℎ 𝑦 ) ) )
18 7 17 bitrd ⊢ ( ( ( 𝐻 ∈ Cℋ ∧ 𝐴 ∈ ℋ ) ∧ 𝑦 ∈ ( ⊥ ‘ 𝐻 ) ) → ( ∃ 𝑥 ∈ ( ⊥ ‘ ( ⊥ ‘ 𝐻 ) ) 𝐴 = ( 𝑦 +ℎ 𝑥 ) ↔ ∃ 𝑥 ∈ 𝐻 𝐴 = ( 𝑥 +ℎ 𝑦 ) ) )
19 18 reubidva ⊢ ( ( 𝐻 ∈ Cℋ ∧ 𝐴 ∈ ℋ ) → ( ∃! 𝑦 ∈ ( ⊥ ‘ 𝐻 ) ∃ 𝑥 ∈ ( ⊥ ‘ ( ⊥ ‘ 𝐻 ) ) 𝐴 = ( 𝑦 +ℎ 𝑥 ) ↔ ∃! 𝑦 ∈ ( ⊥ ‘ 𝐻 ) ∃ 𝑥 ∈ 𝐻 𝐴 = ( 𝑥 +ℎ 𝑦 ) ) )
20 3 19 mpbid ⊢ ( ( 𝐻 ∈ Cℋ ∧ 𝐴 ∈ ℋ ) → ∃! 𝑦 ∈ ( ⊥ ‘ 𝐻 ) ∃ 𝑥 ∈ 𝐻 𝐴 = ( 𝑥 +ℎ 𝑦 ) )