Metamath Proof Explorer

Theorem 5oalem7

Description: Lemma for orthoarguesian law 5OA. (Contributed by NM, 4-May-2000) TODO: replace uses of ee4anv with 4exdistrv as in 3oalem3 . (New usage is discouraged.)

Ref Expression
Hypotheses 5oalem5.1 
|- A e. SH
5oalem5.2 
|- B e. SH
5oalem5.3 
|- C e. SH
5oalem5.4 
|- D e. SH
5oalem5.5 
|- F e. SH
5oalem5.6 
|- G e. SH
5oalem5.7 
|- R e. SH
5oalem5.8 
|- S e. SH
Assertion 5oalem7 
|- ( ( ( A +H B ) i^i ( C +H D ) ) i^i ( ( F +H G ) i^i ( R +H S ) ) ) C_ ( B +H ( A i^i ( C +H ( ( ( ( A +H C ) i^i ( B +H D ) ) i^i ( ( ( A +H R ) i^i ( B +H S ) ) +H ( ( C +H R ) i^i ( D +H S ) ) ) ) i^i ( ( ( ( A +H F ) i^i ( B +H G ) ) i^i ( ( ( A +H R ) i^i ( B +H S ) ) +H ( ( F +H R ) i^i ( G +H S ) ) ) ) +H ( ( ( C +H F ) i^i ( D +H G ) ) i^i ( ( ( C +H R ) i^i ( D +H S ) ) +H ( ( F +H R ) i^i ( G +H S ) ) ) ) ) ) ) ) )

Proof

Step Hyp Ref Expression
1 5oalem5.1 
 |-  A e. SH
2 5oalem5.2 
 |-  B e. SH
3 5oalem5.3 
 |-  C e. SH
4 5oalem5.4 
 |-  D e. SH
5 5oalem5.5 
 |-  F e. SH
6 5oalem5.6 
 |-  G e. SH
7 5oalem5.7 
 |-  R e. SH
8 5oalem5.8 
 |-  S e. SH
9 ee4anv 
 |-  ( E. x E. y E. f E. g ( E. z E. w ( ( ( x e. A /\ y e. B ) /\ h = ( x +h y ) ) /\ ( ( z e. C /\ w e. D ) /\ h = ( z +h w ) ) ) /\ E. v E. u ( ( ( f e. F /\ g e. G ) /\ h = ( f +h g ) ) /\ ( ( v e. R /\ u e. S ) /\ h = ( v +h u ) ) ) ) <-> ( E. x E. y E. z E. w ( ( ( x e. A /\ y e. B ) /\ h = ( x +h y ) ) /\ ( ( z e. C /\ w e. D ) /\ h = ( z +h w ) ) ) /\ E. f E. g E. v E. u ( ( ( f e. F /\ g e. G ) /\ h = ( f +h g ) ) /\ ( ( v e. R /\ u e. S ) /\ h = ( v +h u ) ) ) ) )
10 exrot4 
 |-  ( E. z E. w E. f E. g E. v E. u ( ( ( ( x e. A /\ y e. B ) /\ h = ( x +h y ) ) /\ ( ( z e. C /\ w e. D ) /\ h = ( z +h w ) ) ) /\ ( ( ( f e. F /\ g e. G ) /\ h = ( f +h g ) ) /\ ( ( v e. R /\ u e. S ) /\ h = ( v +h u ) ) ) ) <-> E. f E. g E. z E. w E. v E. u ( ( ( ( x e. A /\ y e. B ) /\ h = ( x +h y ) ) /\ ( ( z e. C /\ w e. D ) /\ h = ( z +h w ) ) ) /\ ( ( ( f e. F /\ g e. G ) /\ h = ( f +h g ) ) /\ ( ( v e. R /\ u e. S ) /\ h = ( v +h u ) ) ) ) )
11 ee4anv 
 |-  ( E. z E. w E. v E. u ( ( ( ( x e. A /\ y e. B ) /\ h = ( x +h y ) ) /\ ( ( z e. C /\ w e. D ) /\ h = ( z +h w ) ) ) /\ ( ( ( f e. F /\ g e. G ) /\ h = ( f +h g ) ) /\ ( ( v e. R /\ u e. S ) /\ h = ( v +h u ) ) ) ) <-> ( E. z E. w ( ( ( x e. A /\ y e. B ) /\ h = ( x +h y ) ) /\ ( ( z e. C /\ w e. D ) /\ h = ( z +h w ) ) ) /\ E. v E. u ( ( ( f e. F /\ g e. G ) /\ h = ( f +h g ) ) /\ ( ( v e. R /\ u e. S ) /\ h = ( v +h u ) ) ) ) )
12 11 2exbii 
 |-  ( E. f E. g E. z E. w E. v E. u ( ( ( ( x e. A /\ y e. B ) /\ h = ( x +h y ) ) /\ ( ( z e. C /\ w e. D ) /\ h = ( z +h w ) ) ) /\ ( ( ( f e. F /\ g e. G ) /\ h = ( f +h g ) ) /\ ( ( v e. R /\ u e. S ) /\ h = ( v +h u ) ) ) ) <-> E. f E. g ( E. z E. w ( ( ( x e. A /\ y e. B ) /\ h = ( x +h y ) ) /\ ( ( z e. C /\ w e. D ) /\ h = ( z +h w ) ) ) /\ E. v E. u ( ( ( f e. F /\ g e. G ) /\ h = ( f +h g ) ) /\ ( ( v e. R /\ u e. S ) /\ h = ( v +h u ) ) ) ) )
13 10 12 bitri 
 |-  ( E. z E. w E. f E. g E. v E. u ( ( ( ( x e. A /\ y e. B ) /\ h = ( x +h y ) ) /\ ( ( z e. C /\ w e. D ) /\ h = ( z +h w ) ) ) /\ ( ( ( f e. F /\ g e. G ) /\ h = ( f +h g ) ) /\ ( ( v e. R /\ u e. S ) /\ h = ( v +h u ) ) ) ) <-> E. f E. g ( E. z E. w ( ( ( x e. A /\ y e. B ) /\ h = ( x +h y ) ) /\ ( ( z e. C /\ w e. D ) /\ h = ( z +h w ) ) ) /\ E. v E. u ( ( ( f e. F /\ g e. G ) /\ h = ( f +h g ) ) /\ ( ( v e. R /\ u e. S ) /\ h = ( v +h u ) ) ) ) )
14 13 2exbii 
 |-  ( E. x E. y E. z E. w E. f E. g E. v E. u ( ( ( ( x e. A /\ y e. B ) /\ h = ( x +h y ) ) /\ ( ( z e. C /\ w e. D ) /\ h = ( z +h w ) ) ) /\ ( ( ( f e. F /\ g e. G ) /\ h = ( f +h g ) ) /\ ( ( v e. R /\ u e. S ) /\ h = ( v +h u ) ) ) ) <-> E. x E. y E. f E. g ( E. z E. w ( ( ( x e. A /\ y e. B ) /\ h = ( x +h y ) ) /\ ( ( z e. C /\ w e. D ) /\ h = ( z +h w ) ) ) /\ E. v E. u ( ( ( f e. F /\ g e. G ) /\ h = ( f +h g ) ) /\ ( ( v e. R /\ u e. S ) /\ h = ( v +h u ) ) ) ) )
15 elin 
 |-  ( h e. ( ( ( A +H B ) i^i ( C +H D ) ) i^i ( ( F +H G ) i^i ( R +H S ) ) ) <-> ( h e. ( ( A +H B ) i^i ( C +H D ) ) /\ h e. ( ( F +H G ) i^i ( R +H S ) ) ) )
16 1 2 shseli 
 |-  ( h e. ( A +H B ) <-> E. x e. A E. y e. B h = ( x +h y ) )
17 r2ex 
 |-  ( E. x e. A E. y e. B h = ( x +h y ) <-> E. x E. y ( ( x e. A /\ y e. B ) /\ h = ( x +h y ) ) )
18 16 17 bitri 
 |-  ( h e. ( A +H B ) <-> E. x E. y ( ( x e. A /\ y e. B ) /\ h = ( x +h y ) ) )
19 3 4 shseli 
 |-  ( h e. ( C +H D ) <-> E. z e. C E. w e. D h = ( z +h w ) )
20 r2ex 
 |-  ( E. z e. C E. w e. D h = ( z +h w ) <-> E. z E. w ( ( z e. C /\ w e. D ) /\ h = ( z +h w ) ) )
21 19 20 bitri 
 |-  ( h e. ( C +H D ) <-> E. z E. w ( ( z e. C /\ w e. D ) /\ h = ( z +h w ) ) )
22 18 21 anbi12i 
 |-  ( ( h e. ( A +H B ) /\ h e. ( C +H D ) ) <-> ( E. x E. y ( ( x e. A /\ y e. B ) /\ h = ( x +h y ) ) /\ E. z E. w ( ( z e. C /\ w e. D ) /\ h = ( z +h w ) ) ) )
23 elin 
 |-  ( h e. ( ( A +H B ) i^i ( C +H D ) ) <-> ( h e. ( A +H B ) /\ h e. ( C +H D ) ) )
24 ee4anv 
 |-  ( E. x E. y E. z E. w ( ( ( x e. A /\ y e. B ) /\ h = ( x +h y ) ) /\ ( ( z e. C /\ w e. D ) /\ h = ( z +h w ) ) ) <-> ( E. x E. y ( ( x e. A /\ y e. B ) /\ h = ( x +h y ) ) /\ E. z E. w ( ( z e. C /\ w e. D ) /\ h = ( z +h w ) ) ) )
25 22 23 24 3bitr4ri 
 |-  ( E. x E. y E. z E. w ( ( ( x e. A /\ y e. B ) /\ h = ( x +h y ) ) /\ ( ( z e. C /\ w e. D ) /\ h = ( z +h w ) ) ) <-> h e. ( ( A +H B ) i^i ( C +H D ) ) )
26 5 6 shseli 
 |-  ( h e. ( F +H G ) <-> E. f e. F E. g e. G h = ( f +h g ) )
27 r2ex 
 |-  ( E. f e. F E. g e. G h = ( f +h g ) <-> E. f E. g ( ( f e. F /\ g e. G ) /\ h = ( f +h g ) ) )
28 26 27 bitri 
 |-  ( h e. ( F +H G ) <-> E. f E. g ( ( f e. F /\ g e. G ) /\ h = ( f +h g ) ) )
29 7 8 shseli 
 |-  ( h e. ( R +H S ) <-> E. v e. R E. u e. S h = ( v +h u ) )
30 r2ex 
 |-  ( E. v e. R E. u e. S h = ( v +h u ) <-> E. v E. u ( ( v e. R /\ u e. S ) /\ h = ( v +h u ) ) )
31 29 30 bitri 
 |-  ( h e. ( R +H S ) <-> E. v E. u ( ( v e. R /\ u e. S ) /\ h = ( v +h u ) ) )
32 28 31 anbi12i 
 |-  ( ( h e. ( F +H G ) /\ h e. ( R +H S ) ) <-> ( E. f E. g ( ( f e. F /\ g e. G ) /\ h = ( f +h g ) ) /\ E. v E. u ( ( v e. R /\ u e. S ) /\ h = ( v +h u ) ) ) )
33 elin 
 |-  ( h e. ( ( F +H G ) i^i ( R +H S ) ) <-> ( h e. ( F +H G ) /\ h e. ( R +H S ) ) )
34 ee4anv 
 |-  ( E. f E. g E. v E. u ( ( ( f e. F /\ g e. G ) /\ h = ( f +h g ) ) /\ ( ( v e. R /\ u e. S ) /\ h = ( v +h u ) ) ) <-> ( E. f E. g ( ( f e. F /\ g e. G ) /\ h = ( f +h g ) ) /\ E. v E. u ( ( v e. R /\ u e. S ) /\ h = ( v +h u ) ) ) )
35 32 33 34 3bitr4ri 
 |-  ( E. f E. g E. v E. u ( ( ( f e. F /\ g e. G ) /\ h = ( f +h g ) ) /\ ( ( v e. R /\ u e. S ) /\ h = ( v +h u ) ) ) <-> h e. ( ( F +H G ) i^i ( R +H S ) ) )
36 25 35 anbi12i 
 |-  ( ( E. x E. y E. z E. w ( ( ( x e. A /\ y e. B ) /\ h = ( x +h y ) ) /\ ( ( z e. C /\ w e. D ) /\ h = ( z +h w ) ) ) /\ E. f E. g E. v E. u ( ( ( f e. F /\ g e. G ) /\ h = ( f +h g ) ) /\ ( ( v e. R /\ u e. S ) /\ h = ( v +h u ) ) ) ) <-> ( h e. ( ( A +H B ) i^i ( C +H D ) ) /\ h e. ( ( F +H G ) i^i ( R +H S ) ) ) )
37 15 36 bitr4i 
 |-  ( h e. ( ( ( A +H B ) i^i ( C +H D ) ) i^i ( ( F +H G ) i^i ( R +H S ) ) ) <-> ( E. x E. y E. z E. w ( ( ( x e. A /\ y e. B ) /\ h = ( x +h y ) ) /\ ( ( z e. C /\ w e. D ) /\ h = ( z +h w ) ) ) /\ E. f E. g E. v E. u ( ( ( f e. F /\ g e. G ) /\ h = ( f +h g ) ) /\ ( ( v e. R /\ u e. S ) /\ h = ( v +h u ) ) ) ) )
38 9 14 37 3bitr4ri 
 |-  ( h e. ( ( ( A +H B ) i^i ( C +H D ) ) i^i ( ( F +H G ) i^i ( R +H S ) ) ) <-> E. x E. y E. z E. w E. f E. g E. v E. u ( ( ( ( x e. A /\ y e. B ) /\ h = ( x +h y ) ) /\ ( ( z e. C /\ w e. D ) /\ h = ( z +h w ) ) ) /\ ( ( ( f e. F /\ g e. G ) /\ h = ( f +h g ) ) /\ ( ( v e. R /\ u e. S ) /\ h = ( v +h u ) ) ) ) )
39 1 2 3 4 5 6 7 8 5oalem6 
 |-  ( ( ( ( ( x e. A /\ y e. B ) /\ h = ( x +h y ) ) /\ ( ( z e. C /\ w e. D ) /\ h = ( z +h w ) ) ) /\ ( ( ( f e. F /\ g e. G ) /\ h = ( f +h g ) ) /\ ( ( v e. R /\ u e. S ) /\ h = ( v +h u ) ) ) ) -> h e. ( B +H ( A i^i ( C +H ( ( ( ( A +H C ) i^i ( B +H D ) ) i^i ( ( ( A +H R ) i^i ( B +H S ) ) +H ( ( C +H R ) i^i ( D +H S ) ) ) ) i^i ( ( ( ( A +H F ) i^i ( B +H G ) ) i^i ( ( ( A +H R ) i^i ( B +H S ) ) +H ( ( F +H R ) i^i ( G +H S ) ) ) ) +H ( ( ( C +H F ) i^i ( D +H G ) ) i^i ( ( ( C +H R ) i^i ( D +H S ) ) +H ( ( F +H R ) i^i ( G +H S ) ) ) ) ) ) ) ) ) )
40 39 exlimivv 
 |-  ( E. v E. u ( ( ( ( x e. A /\ y e. B ) /\ h = ( x +h y ) ) /\ ( ( z e. C /\ w e. D ) /\ h = ( z +h w ) ) ) /\ ( ( ( f e. F /\ g e. G ) /\ h = ( f +h g ) ) /\ ( ( v e. R /\ u e. S ) /\ h = ( v +h u ) ) ) ) -> h e. ( B +H ( A i^i ( C +H ( ( ( ( A +H C ) i^i ( B +H D ) ) i^i ( ( ( A +H R ) i^i ( B +H S ) ) +H ( ( C +H R ) i^i ( D +H S ) ) ) ) i^i ( ( ( ( A +H F ) i^i ( B +H G ) ) i^i ( ( ( A +H R ) i^i ( B +H S ) ) +H ( ( F +H R ) i^i ( G +H S ) ) ) ) +H ( ( ( C +H F ) i^i ( D +H G ) ) i^i ( ( ( C +H R ) i^i ( D +H S ) ) +H ( ( F +H R ) i^i ( G +H S ) ) ) ) ) ) ) ) ) )
41 40 exlimivv 
 |-  ( E. f E. g E. v E. u ( ( ( ( x e. A /\ y e. B ) /\ h = ( x +h y ) ) /\ ( ( z e. C /\ w e. D ) /\ h = ( z +h w ) ) ) /\ ( ( ( f e. F /\ g e. G ) /\ h = ( f +h g ) ) /\ ( ( v e. R /\ u e. S ) /\ h = ( v +h u ) ) ) ) -> h e. ( B +H ( A i^i ( C +H ( ( ( ( A +H C ) i^i ( B +H D ) ) i^i ( ( ( A +H R ) i^i ( B +H S ) ) +H ( ( C +H R ) i^i ( D +H S ) ) ) ) i^i ( ( ( ( A +H F ) i^i ( B +H G ) ) i^i ( ( ( A +H R ) i^i ( B +H S ) ) +H ( ( F +H R ) i^i ( G +H S ) ) ) ) +H ( ( ( C +H F ) i^i ( D +H G ) ) i^i ( ( ( C +H R ) i^i ( D +H S ) ) +H ( ( F +H R ) i^i ( G +H S ) ) ) ) ) ) ) ) ) )
42 41 exlimivv 
 |-  ( E. z E. w E. f E. g E. v E. u ( ( ( ( x e. A /\ y e. B ) /\ h = ( x +h y ) ) /\ ( ( z e. C /\ w e. D ) /\ h = ( z +h w ) ) ) /\ ( ( ( f e. F /\ g e. G ) /\ h = ( f +h g ) ) /\ ( ( v e. R /\ u e. S ) /\ h = ( v +h u ) ) ) ) -> h e. ( B +H ( A i^i ( C +H ( ( ( ( A +H C ) i^i ( B +H D ) ) i^i ( ( ( A +H R ) i^i ( B +H S ) ) +H ( ( C +H R ) i^i ( D +H S ) ) ) ) i^i ( ( ( ( A +H F ) i^i ( B +H G ) ) i^i ( ( ( A +H R ) i^i ( B +H S ) ) +H ( ( F +H R ) i^i ( G +H S ) ) ) ) +H ( ( ( C +H F ) i^i ( D +H G ) ) i^i ( ( ( C +H R ) i^i ( D +H S ) ) +H ( ( F +H R ) i^i ( G +H S ) ) ) ) ) ) ) ) ) )
43 42 exlimivv 
 |-  ( E. x E. y E. z E. w E. f E. g E. v E. u ( ( ( ( x e. A /\ y e. B ) /\ h = ( x +h y ) ) /\ ( ( z e. C /\ w e. D ) /\ h = ( z +h w ) ) ) /\ ( ( ( f e. F /\ g e. G ) /\ h = ( f +h g ) ) /\ ( ( v e. R /\ u e. S ) /\ h = ( v +h u ) ) ) ) -> h e. ( B +H ( A i^i ( C +H ( ( ( ( A +H C ) i^i ( B +H D ) ) i^i ( ( ( A +H R ) i^i ( B +H S ) ) +H ( ( C +H R ) i^i ( D +H S ) ) ) ) i^i ( ( ( ( A +H F ) i^i ( B +H G ) ) i^i ( ( ( A +H R ) i^i ( B +H S ) ) +H ( ( F +H R ) i^i ( G +H S ) ) ) ) +H ( ( ( C +H F ) i^i ( D +H G ) ) i^i ( ( ( C +H R ) i^i ( D +H S ) ) +H ( ( F +H R ) i^i ( G +H S ) ) ) ) ) ) ) ) ) )
44 38 43 sylbi 
 |-  ( h e. ( ( ( A +H B ) i^i ( C +H D ) ) i^i ( ( F +H G ) i^i ( R +H S ) ) ) -> h e. ( B +H ( A i^i ( C +H ( ( ( ( A +H C ) i^i ( B +H D ) ) i^i ( ( ( A +H R ) i^i ( B +H S ) ) +H ( ( C +H R ) i^i ( D +H S ) ) ) ) i^i ( ( ( ( A +H F ) i^i ( B +H G ) ) i^i ( ( ( A +H R ) i^i ( B +H S ) ) +H ( ( F +H R ) i^i ( G +H S ) ) ) ) +H ( ( ( C +H F ) i^i ( D +H G ) ) i^i ( ( ( C +H R ) i^i ( D +H S ) ) +H ( ( F +H R ) i^i ( G +H S ) ) ) ) ) ) ) ) ) )
45 44 ssriv 
 |-  ( ( ( A +H B ) i^i ( C +H D ) ) i^i ( ( F +H G ) i^i ( R +H S ) ) ) C_ ( B +H ( A i^i ( C +H ( ( ( ( A +H C ) i^i ( B +H D ) ) i^i ( ( ( A +H R ) i^i ( B +H S ) ) +H ( ( C +H R ) i^i ( D +H S ) ) ) ) i^i ( ( ( ( A +H F ) i^i ( B +H G ) ) i^i ( ( ( A +H R ) i^i ( B +H S ) ) +H ( ( F +H R ) i^i ( G +H S ) ) ) ) +H ( ( ( C +H F ) i^i ( D +H G ) ) i^i ( ( ( C +H R ) i^i ( D +H S ) ) +H ( ( F +H R ) i^i ( G +H S ) ) ) ) ) ) ) ) )