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