Metamath Proof Explorer

Theorem 3oai

Description: 3OA (weak) orthoarguesian law. Equation IV of GodowskiGreechie p. 249. (Contributed by NM, 19-Oct-1999) (New usage is discouraged.)

Ref Expression
Hypotheses 3oa.1 
|- A e. CH
3oa.2 
|- B e. CH
3oa.3 
|- C e. CH
3oa.4 
|- R = ( ( _|_ ` B ) i^i ( B vH A ) )
3oa.5 
|- S = ( ( _|_ ` C ) i^i ( C vH A ) )
Assertion 3oai 
|- ( ( B vH R ) i^i ( C vH S ) ) C_ ( B vH ( R i^i ( S vH ( ( B vH C ) i^i ( R vH S ) ) ) ) )

Proof

Step Hyp Ref Expression
1 3oa.1 
 |-  A e. CH
2 3oa.2 
 |-  B e. CH
3 3oa.3 
 |-  C e. CH
4 3oa.4 
 |-  R = ( ( _|_ ` B ) i^i ( B vH A ) )
5 3oa.5 
 |-  S = ( ( _|_ ` C ) i^i ( C vH A ) )
6 1 2 3 4 5 3oalem5 
 |-  ( ( B +H R ) i^i ( C +H S ) ) = ( ( B vH R ) i^i ( C vH S ) )
7 2 choccli 
 |-  ( _|_ ` B ) e. CH
8 2 1 chjcli 
 |-  ( B vH A ) e. CH
9 7 8 chincli 
 |-  ( ( _|_ ` B ) i^i ( B vH A ) ) e. CH
10 4 9 eqeltri 
 |-  R e. CH
11 3 choccli 
 |-  ( _|_ ` C ) e. CH
12 3 1 chjcli 
 |-  ( C vH A ) e. CH
13 11 12 chincli 
 |-  ( ( _|_ ` C ) i^i ( C vH A ) ) e. CH
14 5 13 eqeltri 
 |-  S e. CH
15 2 3 10 14 3oalem3 
 |-  ( ( B +H R ) i^i ( C +H S ) ) C_ ( B +H ( R i^i ( S +H ( ( B +H C ) i^i ( R +H S ) ) ) ) )
16 1 2 3 4 5 3oalem6 
 |-  ( B +H ( R i^i ( S +H ( ( B +H C ) i^i ( R +H S ) ) ) ) ) C_ ( B vH ( R i^i ( S vH ( ( B vH C ) i^i ( R vH S ) ) ) ) )
17 15 16 sstri 
 |-  ( ( B +H R ) i^i ( C +H S ) ) C_ ( B vH ( R i^i ( S vH ( ( B vH C ) i^i ( R vH S ) ) ) ) )
18 6 17 eqsstrri 
 |-  ( ( B vH R ) i^i ( C vH S ) ) C_ ( B vH ( R i^i ( S vH ( ( B vH C ) i^i ( R vH S ) ) ) ) )