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