Metamath Proof Explorer

Theorem 3oalem2

Description: Lemma for 3OA (weak) orthoarguesian law. (Contributed by NM, 19-Oct-1999) (New usage is discouraged.)

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

Proof

Step Hyp Ref Expression
1 3oalem1.1 
 |-  B e. CH
2 3oalem1.2 
 |-  C e. CH
3 3oalem1.3 
 |-  R e. CH
4 3oalem1.4 
 |-  S e. CH
5 simplll 
 |-  ( ( ( ( x e. B /\ y e. R ) /\ v = ( x +h y ) ) /\ ( ( z e. C /\ w e. S ) /\ v = ( z +h w ) ) ) -> x e. B )
6 simpllr 
 |-  ( ( ( ( x e. B /\ y e. R ) /\ v = ( x +h y ) ) /\ ( ( z e. C /\ w e. S ) /\ v = ( z +h w ) ) ) -> y e. R )
7 1 2 3 4 3oalem1 
 |-  ( ( ( ( x e. B /\ y e. R ) /\ v = ( x +h y ) ) /\ ( ( z e. C /\ w e. S ) /\ v = ( z +h w ) ) ) -> ( ( ( x e. ~H /\ y e. ~H ) /\ v e. ~H ) /\ ( z e. ~H /\ w e. ~H ) ) )
8 hvaddsub12 
 |-  ( ( y e. ~H /\ w e. ~H /\ w e. ~H ) -> ( y +h ( w -h w ) ) = ( w +h ( y -h w ) ) )
9 8 3anidm23 
 |-  ( ( y e. ~H /\ w e. ~H ) -> ( y +h ( w -h w ) ) = ( w +h ( y -h w ) ) )
10 hvsubid 
 |-  ( w e. ~H -> ( w -h w ) = 0h )
11 10 oveq2d 
 |-  ( w e. ~H -> ( y +h ( w -h w ) ) = ( y +h 0h ) )
12 ax-hvaddid 
 |-  ( y e. ~H -> ( y +h 0h ) = y )
13 11 12 sylan9eqr 
 |-  ( ( y e. ~H /\ w e. ~H ) -> ( y +h ( w -h w ) ) = y )
14 9 13 eqtr3d 
 |-  ( ( y e. ~H /\ w e. ~H ) -> ( w +h ( y -h w ) ) = y )
15 14 ad2ant2l 
 |-  ( ( ( x e. ~H /\ y e. ~H ) /\ ( z e. ~H /\ w e. ~H ) ) -> ( w +h ( y -h w ) ) = y )
16 15 adantlr 
 |-  ( ( ( ( x e. ~H /\ y e. ~H ) /\ v e. ~H ) /\ ( z e. ~H /\ w e. ~H ) ) -> ( w +h ( y -h w ) ) = y )
17 7 16 syl 
 |-  ( ( ( ( x e. B /\ y e. R ) /\ v = ( x +h y ) ) /\ ( ( z e. C /\ w e. S ) /\ v = ( z +h w ) ) ) -> ( w +h ( y -h w ) ) = y )
18 simprlr 
 |-  ( ( ( ( x e. B /\ y e. R ) /\ v = ( x +h y ) ) /\ ( ( z e. C /\ w e. S ) /\ v = ( z +h w ) ) ) -> w e. S )
19 eqtr2 
 |-  ( ( v = ( x +h y ) /\ v = ( z +h w ) ) -> ( x +h y ) = ( z +h w ) )
20 19 oveq1d 
 |-  ( ( v = ( x +h y ) /\ v = ( z +h w ) ) -> ( ( x +h y ) -h ( x +h w ) ) = ( ( z +h w ) -h ( x +h w ) ) )
21 20 ad2ant2l 
 |-  ( ( ( ( x e. B /\ y e. R ) /\ v = ( x +h y ) ) /\ ( ( z e. C /\ w e. S ) /\ v = ( z +h w ) ) ) -> ( ( x +h y ) -h ( x +h w ) ) = ( ( z +h w ) -h ( x +h w ) ) )
22 simpl 
 |-  ( ( x e. ~H /\ y e. ~H ) -> x e. ~H )
23 22 anim1i 
 |-  ( ( ( x e. ~H /\ y e. ~H ) /\ w e. ~H ) -> ( x e. ~H /\ w e. ~H ) )
24 hvsub4 
 |-  ( ( ( x e. ~H /\ y e. ~H ) /\ ( x e. ~H /\ w e. ~H ) ) -> ( ( x +h y ) -h ( x +h w ) ) = ( ( x -h x ) +h ( y -h w ) ) )
25 23 24 syldan 
 |-  ( ( ( x e. ~H /\ y e. ~H ) /\ w e. ~H ) -> ( ( x +h y ) -h ( x +h w ) ) = ( ( x -h x ) +h ( y -h w ) ) )
26 hvsubid 
 |-  ( x e. ~H -> ( x -h x ) = 0h )
27 26 ad2antrr 
 |-  ( ( ( x e. ~H /\ y e. ~H ) /\ w e. ~H ) -> ( x -h x ) = 0h )
28 27 oveq1d 
 |-  ( ( ( x e. ~H /\ y e. ~H ) /\ w e. ~H ) -> ( ( x -h x ) +h ( y -h w ) ) = ( 0h +h ( y -h w ) ) )
29 hvsubcl 
 |-  ( ( y e. ~H /\ w e. ~H ) -> ( y -h w ) e. ~H )
30 hvaddlid 
 |-  ( ( y -h w ) e. ~H -> ( 0h +h ( y -h w ) ) = ( y -h w ) )
31 29 30 syl 
 |-  ( ( y e. ~H /\ w e. ~H ) -> ( 0h +h ( y -h w ) ) = ( y -h w ) )
32 31 adantll 
 |-  ( ( ( x e. ~H /\ y e. ~H ) /\ w e. ~H ) -> ( 0h +h ( y -h w ) ) = ( y -h w ) )
33 25 28 32 3eqtrd 
 |-  ( ( ( x e. ~H /\ y e. ~H ) /\ w e. ~H ) -> ( ( x +h y ) -h ( x +h w ) ) = ( y -h w ) )
34 33 ad2ant2rl 
 |-  ( ( ( ( x e. ~H /\ y e. ~H ) /\ v e. ~H ) /\ ( z e. ~H /\ w e. ~H ) ) -> ( ( x +h y ) -h ( x +h w ) ) = ( y -h w ) )
35 7 34 syl 
 |-  ( ( ( ( x e. B /\ y e. R ) /\ v = ( x +h y ) ) /\ ( ( z e. C /\ w e. S ) /\ v = ( z +h w ) ) ) -> ( ( x +h y ) -h ( x +h w ) ) = ( y -h w ) )
36 simpr 
 |-  ( ( x e. ~H /\ ( z e. ~H /\ w e. ~H ) ) -> ( z e. ~H /\ w e. ~H ) )
37 simpr 
 |-  ( ( z e. ~H /\ w e. ~H ) -> w e. ~H )
38 37 anim2i 
 |-  ( ( x e. ~H /\ ( z e. ~H /\ w e. ~H ) ) -> ( x e. ~H /\ w e. ~H ) )
39 hvsub4 
 |-  ( ( ( z e. ~H /\ w e. ~H ) /\ ( x e. ~H /\ w e. ~H ) ) -> ( ( z +h w ) -h ( x +h w ) ) = ( ( z -h x ) +h ( w -h w ) ) )
40 36 38 39 syl2anc 
 |-  ( ( x e. ~H /\ ( z e. ~H /\ w e. ~H ) ) -> ( ( z +h w ) -h ( x +h w ) ) = ( ( z -h x ) +h ( w -h w ) ) )
41 10 ad2antll 
 |-  ( ( x e. ~H /\ ( z e. ~H /\ w e. ~H ) ) -> ( w -h w ) = 0h )
42 41 oveq2d 
 |-  ( ( x e. ~H /\ ( z e. ~H /\ w e. ~H ) ) -> ( ( z -h x ) +h ( w -h w ) ) = ( ( z -h x ) +h 0h ) )
43 hvsubcl 
 |-  ( ( z e. ~H /\ x e. ~H ) -> ( z -h x ) e. ~H )
44 ax-hvaddid 
 |-  ( ( z -h x ) e. ~H -> ( ( z -h x ) +h 0h ) = ( z -h x ) )
45 43 44 syl 
 |-  ( ( z e. ~H /\ x e. ~H ) -> ( ( z -h x ) +h 0h ) = ( z -h x ) )
46 45 ancoms 
 |-  ( ( x e. ~H /\ z e. ~H ) -> ( ( z -h x ) +h 0h ) = ( z -h x ) )
47 46 adantrr 
 |-  ( ( x e. ~H /\ ( z e. ~H /\ w e. ~H ) ) -> ( ( z -h x ) +h 0h ) = ( z -h x ) )
48 40 42 47 3eqtrd 
 |-  ( ( x e. ~H /\ ( z e. ~H /\ w e. ~H ) ) -> ( ( z +h w ) -h ( x +h w ) ) = ( z -h x ) )
49 48 adantlr 
 |-  ( ( ( x e. ~H /\ y e. ~H ) /\ ( z e. ~H /\ w e. ~H ) ) -> ( ( z +h w ) -h ( x +h w ) ) = ( z -h x ) )
50 49 adantlr 
 |-  ( ( ( ( x e. ~H /\ y e. ~H ) /\ v e. ~H ) /\ ( z e. ~H /\ w e. ~H ) ) -> ( ( z +h w ) -h ( x +h w ) ) = ( z -h x ) )
51 7 50 syl 
 |-  ( ( ( ( x e. B /\ y e. R ) /\ v = ( x +h y ) ) /\ ( ( z e. C /\ w e. S ) /\ v = ( z +h w ) ) ) -> ( ( z +h w ) -h ( x +h w ) ) = ( z -h x ) )
52 21 35 51 3eqtr3d 
 |-  ( ( ( ( x e. B /\ y e. R ) /\ v = ( x +h y ) ) /\ ( ( z e. C /\ w e. S ) /\ v = ( z +h w ) ) ) -> ( y -h w ) = ( z -h x ) )
53 simpll 
 |-  ( ( ( x e. B /\ y e. R ) /\ v = ( x +h y ) ) -> x e. B )
54 simpll 
 |-  ( ( ( z e. C /\ w e. S ) /\ v = ( z +h w ) ) -> z e. C )
55 2 chshii 
 |-  C e. SH
56 1 chshii 
 |-  B e. SH
57 55 56 shsvsi 
 |-  ( ( z e. C /\ x e. B ) -> ( z -h x ) e. ( C +H B ) )
58 57 ancoms 
 |-  ( ( x e. B /\ z e. C ) -> ( z -h x ) e. ( C +H B ) )
59 56 55 shscomi 
 |-  ( B +H C ) = ( C +H B )
60 58 59 eleqtrrdi 
 |-  ( ( x e. B /\ z e. C ) -> ( z -h x ) e. ( B +H C ) )
61 53 54 60 syl2an 
 |-  ( ( ( ( x e. B /\ y e. R ) /\ v = ( x +h y ) ) /\ ( ( z e. C /\ w e. S ) /\ v = ( z +h w ) ) ) -> ( z -h x ) e. ( B +H C ) )
62 52 61 eqeltrd 
 |-  ( ( ( ( x e. B /\ y e. R ) /\ v = ( x +h y ) ) /\ ( ( z e. C /\ w e. S ) /\ v = ( z +h w ) ) ) -> ( y -h w ) e. ( B +H C ) )
63 simplr 
 |-  ( ( ( x e. B /\ y e. R ) /\ v = ( x +h y ) ) -> y e. R )
64 simplr 
 |-  ( ( ( z e. C /\ w e. S ) /\ v = ( z +h w ) ) -> w e. S )
65 3 chshii 
 |-  R e. SH
66 4 chshii 
 |-  S e. SH
67 65 66 shsvsi 
 |-  ( ( y e. R /\ w e. S ) -> ( y -h w ) e. ( R +H S ) )
68 63 64 67 syl2an 
 |-  ( ( ( ( x e. B /\ y e. R ) /\ v = ( x +h y ) ) /\ ( ( z e. C /\ w e. S ) /\ v = ( z +h w ) ) ) -> ( y -h w ) e. ( R +H S ) )
69 62 68 elind 
 |-  ( ( ( ( x e. B /\ y e. R ) /\ v = ( x +h y ) ) /\ ( ( z e. C /\ w e. S ) /\ v = ( z +h w ) ) ) -> ( y -h w ) e. ( ( B +H C ) i^i ( R +H S ) ) )
70 56 55 shscli 
 |-  ( B +H C ) e. SH
71 65 66 shscli 
 |-  ( R +H S ) e. SH
72 70 71 shincli 
 |-  ( ( B +H C ) i^i ( R +H S ) ) e. SH
73 66 72 shsvai 
 |-  ( ( w e. S /\ ( y -h w ) e. ( ( B +H C ) i^i ( R +H S ) ) ) -> ( w +h ( y -h w ) ) e. ( S +H ( ( B +H C ) i^i ( R +H S ) ) ) )
74 18 69 73 syl2anc 
 |-  ( ( ( ( x e. B /\ y e. R ) /\ v = ( x +h y ) ) /\ ( ( z e. C /\ w e. S ) /\ v = ( z +h w ) ) ) -> ( w +h ( y -h w ) ) e. ( S +H ( ( B +H C ) i^i ( R +H S ) ) ) )
75 17 74 eqeltrrd 
 |-  ( ( ( ( x e. B /\ y e. R ) /\ v = ( x +h y ) ) /\ ( ( z e. C /\ w e. S ) /\ v = ( z +h w ) ) ) -> y e. ( S +H ( ( B +H C ) i^i ( R +H S ) ) ) )
76 6 75 elind 
 |-  ( ( ( ( x e. B /\ y e. R ) /\ v = ( x +h y ) ) /\ ( ( z e. C /\ w e. S ) /\ v = ( z +h w ) ) ) -> y e. ( R i^i ( S +H ( ( B +H C ) i^i ( R +H S ) ) ) ) )
77 66 72 shscli 
 |-  ( S +H ( ( B +H C ) i^i ( R +H S ) ) ) e. SH
78 65 77 shincli 
 |-  ( R i^i ( S +H ( ( B +H C ) i^i ( R +H S ) ) ) ) e. SH
79 56 78 shsvai 
 |-  ( ( x e. B /\ y e. ( R i^i ( S +H ( ( B +H C ) i^i ( R +H S ) ) ) ) ) -> ( x +h y ) e. ( B +H ( R i^i ( S +H ( ( B +H C ) i^i ( R +H S ) ) ) ) ) )
80 5 76 79 syl2anc 
 |-  ( ( ( ( x e. B /\ y e. R ) /\ v = ( x +h y ) ) /\ ( ( z e. C /\ w e. S ) /\ v = ( z +h w ) ) ) -> ( x +h y ) e. ( B +H ( R i^i ( S +H ( ( B +H C ) i^i ( R +H S ) ) ) ) ) )
81 eleq1 
 |-  ( v = ( x +h y ) -> ( v e. ( B +H ( R i^i ( S +H ( ( B +H C ) i^i ( R +H S ) ) ) ) ) <-> ( x +h y ) e. ( B +H ( R i^i ( S +H ( ( B +H C ) i^i ( R +H S ) ) ) ) ) ) )
82 81 ad2antlr 
 |-  ( ( ( ( x e. B /\ y e. R ) /\ v = ( x +h y ) ) /\ ( ( z e. C /\ w e. S ) /\ v = ( z +h w ) ) ) -> ( v e. ( B +H ( R i^i ( S +H ( ( B +H C ) i^i ( R +H S ) ) ) ) ) <-> ( x +h y ) e. ( B +H ( R i^i ( S +H ( ( B +H C ) i^i ( R +H S ) ) ) ) ) ) )
83 80 82 mpbird 
 |-  ( ( ( ( x e. B /\ y e. R ) /\ v = ( x +h y ) ) /\ ( ( z e. C /\ w e. S ) /\ v = ( z +h w ) ) ) -> v e. ( B +H ( R i^i ( S +H ( ( B +H C ) i^i ( R +H S ) ) ) ) ) )