Metamath Proof Explorer

Theorem 5oalem1

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

Ref Expression
Hypotheses 5oalem1.1 
|- A e. SH
5oalem1.2 
|- B e. SH
5oalem1.3 
|- C e. SH
5oalem1.4 
|- R e. SH
Assertion 5oalem1 
|- ( ( ( ( x e. A /\ y e. B ) /\ v = ( x +h y ) ) /\ ( z e. C /\ ( x -h z ) e. R ) ) -> v e. ( B +H ( A i^i ( C +H R ) ) ) )

Proof

Step Hyp Ref Expression
1 5oalem1.1 
 |-  A e. SH
2 5oalem1.2 
 |-  B e. SH
3 5oalem1.3 
 |-  C e. SH
4 5oalem1.4 
 |-  R e. SH
5 simplll 
 |-  ( ( ( ( x e. A /\ y e. B ) /\ v = ( x +h y ) ) /\ ( z e. C /\ ( x -h z ) e. R ) ) -> x e. A )
6 1 sheli 
 |-  ( x e. A -> x e. ~H )
7 6 ad2antrr 
 |-  ( ( ( x e. A /\ y e. B ) /\ v = ( x +h y ) ) -> x e. ~H )
8 3 sheli 
 |-  ( z e. C -> z e. ~H )
9 8 adantr 
 |-  ( ( z e. C /\ ( x -h z ) e. R ) -> z e. ~H )
10 hvaddsub12 
 |-  ( ( x e. ~H /\ z e. ~H /\ z e. ~H ) -> ( x +h ( z -h z ) ) = ( z +h ( x -h z ) ) )
11 10 3anidm23 
 |-  ( ( x e. ~H /\ z e. ~H ) -> ( x +h ( z -h z ) ) = ( z +h ( x -h z ) ) )
12 hvsubid 
 |-  ( z e. ~H -> ( z -h z ) = 0h )
13 12 oveq2d 
 |-  ( z e. ~H -> ( x +h ( z -h z ) ) = ( x +h 0h ) )
14 ax-hvaddid 
 |-  ( x e. ~H -> ( x +h 0h ) = x )
15 13 14 sylan9eqr 
 |-  ( ( x e. ~H /\ z e. ~H ) -> ( x +h ( z -h z ) ) = x )
16 11 15 eqtr3d 
 |-  ( ( x e. ~H /\ z e. ~H ) -> ( z +h ( x -h z ) ) = x )
17 7 9 16 syl2an 
 |-  ( ( ( ( x e. A /\ y e. B ) /\ v = ( x +h y ) ) /\ ( z e. C /\ ( x -h z ) e. R ) ) -> ( z +h ( x -h z ) ) = x )
18 3 4 shsvai 
 |-  ( ( z e. C /\ ( x -h z ) e. R ) -> ( z +h ( x -h z ) ) e. ( C +H R ) )
19 18 adantl 
 |-  ( ( ( ( x e. A /\ y e. B ) /\ v = ( x +h y ) ) /\ ( z e. C /\ ( x -h z ) e. R ) ) -> ( z +h ( x -h z ) ) e. ( C +H R ) )
20 17 19 eqeltrrd 
 |-  ( ( ( ( x e. A /\ y e. B ) /\ v = ( x +h y ) ) /\ ( z e. C /\ ( x -h z ) e. R ) ) -> x e. ( C +H R ) )
21 5 20 elind 
 |-  ( ( ( ( x e. A /\ y e. B ) /\ v = ( x +h y ) ) /\ ( z e. C /\ ( x -h z ) e. R ) ) -> x e. ( A i^i ( C +H R ) ) )
22 simpllr 
 |-  ( ( ( ( x e. A /\ y e. B ) /\ v = ( x +h y ) ) /\ ( z e. C /\ ( x -h z ) e. R ) ) -> y e. B )
23 3 4 shscli 
 |-  ( C +H R ) e. SH
24 1 23 shincli 
 |-  ( A i^i ( C +H R ) ) e. SH
25 24 2 shsvai 
 |-  ( ( x e. ( A i^i ( C +H R ) ) /\ y e. B ) -> ( x +h y ) e. ( ( A i^i ( C +H R ) ) +H B ) )
26 24 2 shscomi 
 |-  ( ( A i^i ( C +H R ) ) +H B ) = ( B +H ( A i^i ( C +H R ) ) )
27 25 26 eleqtrdi 
 |-  ( ( x e. ( A i^i ( C +H R ) ) /\ y e. B ) -> ( x +h y ) e. ( B +H ( A i^i ( C +H R ) ) ) )
28 21 22 27 syl2anc 
 |-  ( ( ( ( x e. A /\ y e. B ) /\ v = ( x +h y ) ) /\ ( z e. C /\ ( x -h z ) e. R ) ) -> ( x +h y ) e. ( B +H ( A i^i ( C +H R ) ) ) )
29 eleq1 
 |-  ( v = ( x +h y ) -> ( v e. ( B +H ( A i^i ( C +H R ) ) ) <-> ( x +h y ) e. ( B +H ( A i^i ( C +H R ) ) ) ) )
30 29 ad2antlr 
 |-  ( ( ( ( x e. A /\ y e. B ) /\ v = ( x +h y ) ) /\ ( z e. C /\ ( x -h z ) e. R ) ) -> ( v e. ( B +H ( A i^i ( C +H R ) ) ) <-> ( x +h y ) e. ( B +H ( A i^i ( C +H R ) ) ) ) )
31 28 30 mpbird 
 |-  ( ( ( ( x e. A /\ y e. B ) /\ v = ( x +h y ) ) /\ ( z e. C /\ ( x -h z ) e. R ) ) -> v e. ( B +H ( A i^i ( C +H R ) ) ) )