Metamath Proof Explorer

Theorem pjcompi

Description: Component of a projection. (Contributed by NM, 31-Oct-1999) (Revised by Mario Carneiro, 19-May-2014) (New usage is discouraged.)

Ref Expression
Hypothesis pjidm.1 ⊢ 𝐻 ∈ Cℋ
Assertion pjcompi ( ( 𝐴 ∈ 𝐻 ∧ 𝐵 ∈ ( ⊥ ‘ 𝐻 ) ) → ( ( projℎ ‘ 𝐻 ) ‘ ( 𝐴 +ℎ 𝐵 ) ) = 𝐴 )

Proof

Step Hyp Ref Expression
1 pjidm.1 ⊢ 𝐻 ∈ Cℋ
2 1 cheli ⊢ ( 𝐴 ∈ 𝐻 → 𝐴 ∈ ℋ )
3 1 choccli ⊢ ( ⊥ ‘ 𝐻 ) ∈ Cℋ
4 3 cheli ⊢ ( 𝐵 ∈ ( ⊥ ‘ 𝐻 ) → 𝐵 ∈ ℋ )
5 hvaddcl ⊢ ( ( 𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ) → ( 𝐴 +ℎ 𝐵 ) ∈ ℋ )
6 2 4 5 syl2an ⊢ ( ( 𝐴 ∈ 𝐻 ∧ 𝐵 ∈ ( ⊥ ‘ 𝐻 ) ) → ( 𝐴 +ℎ 𝐵 ) ∈ ℋ )
7 axpjpj ⊢ ( ( 𝐻 ∈ Cℋ ∧ ( 𝐴 +ℎ 𝐵 ) ∈ ℋ ) → ( 𝐴 +ℎ 𝐵 ) = ( ( ( projℎ ‘ 𝐻 ) ‘ ( 𝐴 +ℎ 𝐵 ) ) +ℎ ( ( projℎ ‘ ( ⊥ ‘ 𝐻 ) ) ‘ ( 𝐴 +ℎ 𝐵 ) ) ) )
8 1 6 7 sylancr ⊢ ( ( 𝐴 ∈ 𝐻 ∧ 𝐵 ∈ ( ⊥ ‘ 𝐻 ) ) → ( 𝐴 +ℎ 𝐵 ) = ( ( ( projℎ ‘ 𝐻 ) ‘ ( 𝐴 +ℎ 𝐵 ) ) +ℎ ( ( projℎ ‘ ( ⊥ ‘ 𝐻 ) ) ‘ ( 𝐴 +ℎ 𝐵 ) ) ) )
9 eqid ⊢ ( 𝐴 +ℎ 𝐵 ) = ( 𝐴 +ℎ 𝐵 )
10 axpjcl ⊢ ( ( 𝐻 ∈ Cℋ ∧ ( 𝐴 +ℎ 𝐵 ) ∈ ℋ ) → ( ( projℎ ‘ 𝐻 ) ‘ ( 𝐴 +ℎ 𝐵 ) ) ∈ 𝐻 )
11 1 6 10 sylancr ⊢ ( ( 𝐴 ∈ 𝐻 ∧ 𝐵 ∈ ( ⊥ ‘ 𝐻 ) ) → ( ( projℎ ‘ 𝐻 ) ‘ ( 𝐴 +ℎ 𝐵 ) ) ∈ 𝐻 )
12 axpjcl ⊢ ( ( ( ⊥ ‘ 𝐻 ) ∈ Cℋ ∧ ( 𝐴 +ℎ 𝐵 ) ∈ ℋ ) → ( ( projℎ ‘ ( ⊥ ‘ 𝐻 ) ) ‘ ( 𝐴 +ℎ 𝐵 ) ) ∈ ( ⊥ ‘ 𝐻 ) )
13 3 6 12 sylancr ⊢ ( ( 𝐴 ∈ 𝐻 ∧ 𝐵 ∈ ( ⊥ ‘ 𝐻 ) ) → ( ( projℎ ‘ ( ⊥ ‘ 𝐻 ) ) ‘ ( 𝐴 +ℎ 𝐵 ) ) ∈ ( ⊥ ‘ 𝐻 ) )
14 simpl ⊢ ( ( 𝐴 ∈ 𝐻 ∧ 𝐵 ∈ ( ⊥ ‘ 𝐻 ) ) → 𝐴 ∈ 𝐻 )
15 simpr ⊢ ( ( 𝐴 ∈ 𝐻 ∧ 𝐵 ∈ ( ⊥ ‘ 𝐻 ) ) → 𝐵 ∈ ( ⊥ ‘ 𝐻 ) )
16 1 chocunii ⊢ ( ( ( ( ( projℎ ‘ 𝐻 ) ‘ ( 𝐴 +ℎ 𝐵 ) ) ∈ 𝐻 ∧ ( ( projℎ ‘ ( ⊥ ‘ 𝐻 ) ) ‘ ( 𝐴 +ℎ 𝐵 ) ) ∈ ( ⊥ ‘ 𝐻 ) ) ∧ ( 𝐴 ∈ 𝐻 ∧ 𝐵 ∈ ( ⊥ ‘ 𝐻 ) ) ) → ( ( ( 𝐴 +ℎ 𝐵 ) = ( ( ( projℎ ‘ 𝐻 ) ‘ ( 𝐴 +ℎ 𝐵 ) ) +ℎ ( ( projℎ ‘ ( ⊥ ‘ 𝐻 ) ) ‘ ( 𝐴 +ℎ 𝐵 ) ) ) ∧ ( 𝐴 +ℎ 𝐵 ) = ( 𝐴 +ℎ 𝐵 ) ) → ( ( ( projℎ ‘ 𝐻 ) ‘ ( 𝐴 +ℎ 𝐵 ) ) = 𝐴 ∧ ( ( projℎ ‘ ( ⊥ ‘ 𝐻 ) ) ‘ ( 𝐴 +ℎ 𝐵 ) ) = 𝐵 ) ) )
17 11 13 14 15 16 syl22anc ⊢ ( ( 𝐴 ∈ 𝐻 ∧ 𝐵 ∈ ( ⊥ ‘ 𝐻 ) ) → ( ( ( 𝐴 +ℎ 𝐵 ) = ( ( ( projℎ ‘ 𝐻 ) ‘ ( 𝐴 +ℎ 𝐵 ) ) +ℎ ( ( projℎ ‘ ( ⊥ ‘ 𝐻 ) ) ‘ ( 𝐴 +ℎ 𝐵 ) ) ) ∧ ( 𝐴 +ℎ 𝐵 ) = ( 𝐴 +ℎ 𝐵 ) ) → ( ( ( projℎ ‘ 𝐻 ) ‘ ( 𝐴 +ℎ 𝐵 ) ) = 𝐴 ∧ ( ( projℎ ‘ ( ⊥ ‘ 𝐻 ) ) ‘ ( 𝐴 +ℎ 𝐵 ) ) = 𝐵 ) ) )
18 9 17 mpan2i ⊢ ( ( 𝐴 ∈ 𝐻 ∧ 𝐵 ∈ ( ⊥ ‘ 𝐻 ) ) → ( ( 𝐴 +ℎ 𝐵 ) = ( ( ( projℎ ‘ 𝐻 ) ‘ ( 𝐴 +ℎ 𝐵 ) ) +ℎ ( ( projℎ ‘ ( ⊥ ‘ 𝐻 ) ) ‘ ( 𝐴 +ℎ 𝐵 ) ) ) → ( ( ( projℎ ‘ 𝐻 ) ‘ ( 𝐴 +ℎ 𝐵 ) ) = 𝐴 ∧ ( ( projℎ ‘ ( ⊥ ‘ 𝐻 ) ) ‘ ( 𝐴 +ℎ 𝐵 ) ) = 𝐵 ) ) )
19 8 18 mpd ⊢ ( ( 𝐴 ∈ 𝐻 ∧ 𝐵 ∈ ( ⊥ ‘ 𝐻 ) ) → ( ( ( projℎ ‘ 𝐻 ) ‘ ( 𝐴 +ℎ 𝐵 ) ) = 𝐴 ∧ ( ( projℎ ‘ ( ⊥ ‘ 𝐻 ) ) ‘ ( 𝐴 +ℎ 𝐵 ) ) = 𝐵 ) )
20 19 simpld ⊢ ( ( 𝐴 ∈ 𝐻 ∧ 𝐵 ∈ ( ⊥ ‘ 𝐻 ) ) → ( ( projℎ ‘ 𝐻 ) ‘ ( 𝐴 +ℎ 𝐵 ) ) = 𝐴 )