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 ⊢ H ∈ C ℋ
Assertion pjcompi ⊢ A ∈ H ∧ B ∈ ⊥ ⁡ H → proj ℎ ⁡ H ⁡ A + ℎ B = A

Proof

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