Metamath Proof Explorer

Theorem chocunii

Description: Lemma for uniqueness part of Projection Theorem. Theorem 3.7(i) of Beran p. 102 (uniqueness part). (Contributed by NM, 23-Oct-1999) (Proof shortened by Mario Carneiro, 15-May-2014) (New usage is discouraged.)

Ref Expression
Hypothesis chocuni.1 ⊢H∈Cℋ
Assertion chocunii ⊢A∈H∧B∈⊥⁡H∧C∈H∧D∈⊥⁡H→R=A+ℎB∧R=C+ℎD→A=C∧B=D

Proof

Step Hyp Ref Expression
1 chocuni.1 ⊢H∈Cℋ
2 1 chshii ⊢H∈Sℋ
3 2 a1i ⊢A∈H∧B∈⊥⁡H∧C∈H∧D∈⊥⁡H∧R=A+ℎB∧R=C+ℎD→H∈Sℋ
4 shocsh ⊢H∈Sℋ→⊥⁡H∈Sℋ
5 2 4 mp1i ⊢A∈H∧B∈⊥⁡H∧C∈H∧D∈⊥⁡H∧R=A+ℎB∧R=C+ℎD→⊥⁡H∈Sℋ
6 ocin ⊢H∈Sℋ→H∩⊥⁡H=0ℋ
7 2 6 mp1i ⊢A∈H∧B∈⊥⁡H∧C∈H∧D∈⊥⁡H∧R=A+ℎB∧R=C+ℎD→H∩⊥⁡H=0ℋ
8 simplll ⊢A∈H∧B∈⊥⁡H∧C∈H∧D∈⊥⁡H∧R=A+ℎB∧R=C+ℎD→A∈H
9 simpllr ⊢A∈H∧B∈⊥⁡H∧C∈H∧D∈⊥⁡H∧R=A+ℎB∧R=C+ℎD→B∈⊥⁡H
10 simplrl ⊢A∈H∧B∈⊥⁡H∧C∈H∧D∈⊥⁡H∧R=A+ℎB∧R=C+ℎD→C∈H
11 simplrr ⊢A∈H∧B∈⊥⁡H∧C∈H∧D∈⊥⁡H∧R=A+ℎB∧R=C+ℎD→D∈⊥⁡H
12 eqtr2 ⊢R=A+ℎB∧R=C+ℎD→A+ℎB=C+ℎD
13 12 adantl ⊢A∈H∧B∈⊥⁡H∧C∈H∧D∈⊥⁡H∧R=A+ℎB∧R=C+ℎD→A+ℎB=C+ℎD
14 3 5 7 8 9 10 11 13 shuni ⊢A∈H∧B∈⊥⁡H∧C∈H∧D∈⊥⁡H∧R=A+ℎB∧R=C+ℎD→A=C∧B=D
15 14 ex ⊢A∈H∧B∈⊥⁡H∧C∈H∧D∈⊥⁡H→R=A+ℎB∧R=C+ℎD→A=C∧B=D