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