# 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 e. CH`
Assertion chocunii
`|- ( ( ( A e. H /\ B e. ( _|_ ` H ) ) /\ ( C e. H /\ D e. ( _|_ ` H ) ) ) -> ( ( R = ( A +h B ) /\ R = ( C +h D ) ) -> ( A = C /\ B = D ) ) )`

### Proof

Step Hyp Ref Expression
1 chocuni.1
` |-  H e. CH`
2 1 chshii
` |-  H e. SH`
3 2 a1i
` |-  ( ( ( ( A e. H /\ B e. ( _|_ ` H ) ) /\ ( C e. H /\ D e. ( _|_ ` H ) ) ) /\ ( R = ( A +h B ) /\ R = ( C +h D ) ) ) -> H e. SH )`
4 shocsh
` |-  ( H e. SH -> ( _|_ ` H ) e. SH )`
5 2 4 mp1i
` |-  ( ( ( ( A e. H /\ B e. ( _|_ ` H ) ) /\ ( C e. H /\ D e. ( _|_ ` H ) ) ) /\ ( R = ( A +h B ) /\ R = ( C +h D ) ) ) -> ( _|_ ` H ) e. SH )`
6 ocin
` |-  ( H e. SH -> ( H i^i ( _|_ ` H ) ) = 0H )`
7 2 6 mp1i
` |-  ( ( ( ( A e. H /\ B e. ( _|_ ` H ) ) /\ ( C e. H /\ D e. ( _|_ ` H ) ) ) /\ ( R = ( A +h B ) /\ R = ( C +h D ) ) ) -> ( H i^i ( _|_ ` H ) ) = 0H )`
8 simplll
` |-  ( ( ( ( A e. H /\ B e. ( _|_ ` H ) ) /\ ( C e. H /\ D e. ( _|_ ` H ) ) ) /\ ( R = ( A +h B ) /\ R = ( C +h D ) ) ) -> A e. H )`
9 simpllr
` |-  ( ( ( ( A e. H /\ B e. ( _|_ ` H ) ) /\ ( C e. H /\ D e. ( _|_ ` H ) ) ) /\ ( R = ( A +h B ) /\ R = ( C +h D ) ) ) -> B e. ( _|_ ` H ) )`
10 simplrl
` |-  ( ( ( ( A e. H /\ B e. ( _|_ ` H ) ) /\ ( C e. H /\ D e. ( _|_ ` H ) ) ) /\ ( R = ( A +h B ) /\ R = ( C +h D ) ) ) -> C e. H )`
11 simplrr
` |-  ( ( ( ( A e. H /\ B e. ( _|_ ` H ) ) /\ ( C e. H /\ D e. ( _|_ ` H ) ) ) /\ ( R = ( A +h B ) /\ R = ( C +h D ) ) ) -> D e. ( _|_ ` H ) )`
12 eqtr2
` |-  ( ( R = ( A +h B ) /\ R = ( C +h D ) ) -> ( A +h B ) = ( C +h D ) )`
` |-  ( ( ( ( A e. H /\ B e. ( _|_ ` H ) ) /\ ( C e. H /\ D e. ( _|_ ` H ) ) ) /\ ( R = ( A +h B ) /\ R = ( C +h D ) ) ) -> ( A +h B ) = ( C +h D ) )`
` |-  ( ( ( ( A e. H /\ B e. ( _|_ ` H ) ) /\ ( C e. H /\ D e. ( _|_ ` H ) ) ) /\ ( R = ( A +h B ) /\ R = ( C +h D ) ) ) -> ( A = C /\ B = D ) )`
` |-  ( ( ( A e. H /\ B e. ( _|_ ` H ) ) /\ ( C e. H /\ D e. ( _|_ ` H ) ) ) -> ( ( R = ( A +h B ) /\ R = ( C +h D ) ) -> ( A = C /\ B = D ) ) )`