Metamath Proof Explorer

Theorem 5oalem4

Description: Lemma for orthoarguesian law 5OA. (Contributed by NM, 2-Apr-2000) (New usage is discouraged.)

Ref Expression
Hypotheses 5oalem3.1 
|- A e. SH
5oalem3.2 
|- B e. SH
5oalem3.3 
|- C e. SH
5oalem3.4 
|- D e. SH
5oalem3.5 
|- F e. SH
5oalem3.6 
|- G e. SH
Assertion 5oalem4 
|- ( ( ( ( ( x e. A /\ y e. B ) /\ ( z e. C /\ w e. D ) ) /\ ( f e. F /\ g e. G ) ) /\ ( ( x +h y ) = ( f +h g ) /\ ( z +h w ) = ( f +h g ) ) ) -> ( x -h z ) e. ( ( ( A +H C ) i^i ( B +H D ) ) i^i ( ( ( A +H F ) i^i ( B +H G ) ) +H ( ( C +H F ) i^i ( D +H G ) ) ) ) )

Proof

Step Hyp Ref Expression
1 5oalem3.1 
 |-  A e. SH
2 5oalem3.2 
 |-  B e. SH
3 5oalem3.3 
 |-  C e. SH
4 5oalem3.4 
 |-  D e. SH
5 5oalem3.5 
 |-  F e. SH
6 5oalem3.6 
 |-  G e. SH
7 eqtr3 
 |-  ( ( ( x +h y ) = ( f +h g ) /\ ( z +h w ) = ( f +h g ) ) -> ( x +h y ) = ( z +h w ) )
8 1 2 3 4 5oalem2 
 |-  ( ( ( ( x e. A /\ y e. B ) /\ ( z e. C /\ w e. D ) ) /\ ( x +h y ) = ( z +h w ) ) -> ( x -h z ) e. ( ( A +H C ) i^i ( B +H D ) ) )
9 7 8 sylan2 
 |-  ( ( ( ( x e. A /\ y e. B ) /\ ( z e. C /\ w e. D ) ) /\ ( ( x +h y ) = ( f +h g ) /\ ( z +h w ) = ( f +h g ) ) ) -> ( x -h z ) e. ( ( A +H C ) i^i ( B +H D ) ) )
10 9 adantlr 
 |-  ( ( ( ( ( x e. A /\ y e. B ) /\ ( z e. C /\ w e. D ) ) /\ ( f e. F /\ g e. G ) ) /\ ( ( x +h y ) = ( f +h g ) /\ ( z +h w ) = ( f +h g ) ) ) -> ( x -h z ) e. ( ( A +H C ) i^i ( B +H D ) ) )
11 1 2 3 4 5 6 5oalem3 
 |-  ( ( ( ( ( x e. A /\ y e. B ) /\ ( z e. C /\ w e. D ) ) /\ ( f e. F /\ g e. G ) ) /\ ( ( x +h y ) = ( f +h g ) /\ ( z +h w ) = ( f +h g ) ) ) -> ( x -h z ) e. ( ( ( A +H F ) i^i ( B +H G ) ) +H ( ( C +H F ) i^i ( D +H G ) ) ) )
12 10 11 elind 
 |-  ( ( ( ( ( x e. A /\ y e. B ) /\ ( z e. C /\ w e. D ) ) /\ ( f e. F /\ g e. G ) ) /\ ( ( x +h y ) = ( f +h g ) /\ ( z +h w ) = ( f +h g ) ) ) -> ( x -h z ) e. ( ( ( A +H C ) i^i ( B +H D ) ) i^i ( ( ( A +H F ) i^i ( B +H G ) ) +H ( ( C +H F ) i^i ( D +H G ) ) ) ) )