This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ⊢ 𝐻 ∈ Cℋ
Assertion chocunii ( ( ( 𝐴 ∈ 𝐻 ∧ 𝐵 ∈ ( ⊥ ‘ 𝐻 ) ) ∧ ( 𝐶 ∈ 𝐻 ∧ 𝐷 ∈ ( ⊥ ‘ 𝐻 ) ) ) → ( ( 𝑅 = ( 𝐴 +ℎ 𝐵 ) ∧ 𝑅 = ( 𝐶 +ℎ 𝐷 ) ) → ( 𝐴 = 𝐶 ∧ 𝐵 = 𝐷 ) ) )

Proof

Step Hyp Ref Expression
1 chocuni.1 ⊢ 𝐻 ∈ Cℋ
2 1 chshii ⊢ 𝐻 ∈ Sℋ
3 2 a1i ⊢ ( ( ( ( 𝐴 ∈ 𝐻 ∧ 𝐵 ∈ ( ⊥ ‘ 𝐻 ) ) ∧ ( 𝐶 ∈ 𝐻 ∧ 𝐷 ∈ ( ⊥ ‘ 𝐻 ) ) ) ∧ ( 𝑅 = ( 𝐴 +ℎ 𝐵 ) ∧ 𝑅 = ( 𝐶 +ℎ 𝐷 ) ) ) → 𝐻 ∈ Sℋ )
4 shocsh ⊢ ( 𝐻 ∈ Sℋ → ( ⊥ ‘ 𝐻 ) ∈ Sℋ )
5 2 4 mp1i ⊢ ( ( ( ( 𝐴 ∈ 𝐻 ∧ 𝐵 ∈ ( ⊥ ‘ 𝐻 ) ) ∧ ( 𝐶 ∈ 𝐻 ∧ 𝐷 ∈ ( ⊥ ‘ 𝐻 ) ) ) ∧ ( 𝑅 = ( 𝐴 +ℎ 𝐵 ) ∧ 𝑅 = ( 𝐶 +ℎ 𝐷 ) ) ) → ( ⊥ ‘ 𝐻 ) ∈ Sℋ )
6 ocin ⊢ ( 𝐻 ∈ Sℋ → ( 𝐻 ∩ ( ⊥ ‘ 𝐻 ) ) = 0ℋ )
7 2 6 mp1i ⊢ ( ( ( ( 𝐴 ∈ 𝐻 ∧ 𝐵 ∈ ( ⊥ ‘ 𝐻 ) ) ∧ ( 𝐶 ∈ 𝐻 ∧ 𝐷 ∈ ( ⊥ ‘ 𝐻 ) ) ) ∧ ( 𝑅 = ( 𝐴 +ℎ 𝐵 ) ∧ 𝑅 = ( 𝐶 +ℎ 𝐷 ) ) ) → ( 𝐻 ∩ ( ⊥ ‘ 𝐻 ) ) = 0ℋ )
8 simplll ⊢ ( ( ( ( 𝐴 ∈ 𝐻 ∧ 𝐵 ∈ ( ⊥ ‘ 𝐻 ) ) ∧ ( 𝐶 ∈ 𝐻 ∧ 𝐷 ∈ ( ⊥ ‘ 𝐻 ) ) ) ∧ ( 𝑅 = ( 𝐴 +ℎ 𝐵 ) ∧ 𝑅 = ( 𝐶 +ℎ 𝐷 ) ) ) → 𝐴 ∈ 𝐻 )
9 simpllr ⊢ ( ( ( ( 𝐴 ∈ 𝐻 ∧ 𝐵 ∈ ( ⊥ ‘ 𝐻 ) ) ∧ ( 𝐶 ∈ 𝐻 ∧ 𝐷 ∈ ( ⊥ ‘ 𝐻 ) ) ) ∧ ( 𝑅 = ( 𝐴 +ℎ 𝐵 ) ∧ 𝑅 = ( 𝐶 +ℎ 𝐷 ) ) ) → 𝐵 ∈ ( ⊥ ‘ 𝐻 ) )
10 simplrl ⊢ ( ( ( ( 𝐴 ∈ 𝐻 ∧ 𝐵 ∈ ( ⊥ ‘ 𝐻 ) ) ∧ ( 𝐶 ∈ 𝐻 ∧ 𝐷 ∈ ( ⊥ ‘ 𝐻 ) ) ) ∧ ( 𝑅 = ( 𝐴 +ℎ 𝐵 ) ∧ 𝑅 = ( 𝐶 +ℎ 𝐷 ) ) ) → 𝐶 ∈ 𝐻 )
11 simplrr ⊢ ( ( ( ( 𝐴 ∈ 𝐻 ∧ 𝐵 ∈ ( ⊥ ‘ 𝐻 ) ) ∧ ( 𝐶 ∈ 𝐻 ∧ 𝐷 ∈ ( ⊥ ‘ 𝐻 ) ) ) ∧ ( 𝑅 = ( 𝐴 +ℎ 𝐵 ) ∧ 𝑅 = ( 𝐶 +ℎ 𝐷 ) ) ) → 𝐷 ∈ ( ⊥ ‘ 𝐻 ) )
12 eqtr2 ⊢ ( ( 𝑅 = ( 𝐴 +ℎ 𝐵 ) ∧ 𝑅 = ( 𝐶 +ℎ 𝐷 ) ) → ( 𝐴 +ℎ 𝐵 ) = ( 𝐶 +ℎ 𝐷 ) )
13 12 adantl ⊢ ( ( ( ( 𝐴 ∈ 𝐻 ∧ 𝐵 ∈ ( ⊥ ‘ 𝐻 ) ) ∧ ( 𝐶 ∈ 𝐻 ∧ 𝐷 ∈ ( ⊥ ‘ 𝐻 ) ) ) ∧ ( 𝑅 = ( 𝐴 +ℎ 𝐵 ) ∧ 𝑅 = ( 𝐶 +ℎ 𝐷 ) ) ) → ( 𝐴 +ℎ 𝐵 ) = ( 𝐶 +ℎ 𝐷 ) )
14 3 5 7 8 9 10 11 13 shuni ⊢ ( ( ( ( 𝐴 ∈ 𝐻 ∧ 𝐵 ∈ ( ⊥ ‘ 𝐻 ) ) ∧ ( 𝐶 ∈ 𝐻 ∧ 𝐷 ∈ ( ⊥ ‘ 𝐻 ) ) ) ∧ ( 𝑅 = ( 𝐴 +ℎ 𝐵 ) ∧ 𝑅 = ( 𝐶 +ℎ 𝐷 ) ) ) → ( 𝐴 = 𝐶 ∧ 𝐵 = 𝐷 ) )
15 14 ex ⊢ ( ( ( 𝐴 ∈ 𝐻 ∧ 𝐵 ∈ ( ⊥ ‘ 𝐻 ) ) ∧ ( 𝐶 ∈ 𝐻 ∧ 𝐷 ∈ ( ⊥ ‘ 𝐻 ) ) ) → ( ( 𝑅 = ( 𝐴 +ℎ 𝐵 ) ∧ 𝑅 = ( 𝐶 +ℎ 𝐷 ) ) → ( 𝐴 = 𝐶 ∧ 𝐵 = 𝐷 ) ) )