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 ) )
13 12 adantl 
 |-  ( ( ( ( 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 ) )
14 3 5 7 8 9 10 11 13 shuni 
 |-  ( ( ( ( A e. H /\ B e. ( _|_ ` H ) ) /\ ( C e. H /\ D e. ( _|_ ` H ) ) ) /\ ( R = ( A +h B ) /\ R = ( C +h D ) ) ) -> ( A = C /\ B = D ) )
15 14 ex 
 |-  ( ( ( A e. H /\ B e. ( _|_ ` H ) ) /\ ( C e. H /\ D e. ( _|_ ` H ) ) ) -> ( ( R = ( A +h B ) /\ R = ( C +h D ) ) -> ( A = C /\ B = D ) ) )