Metamath Proof Explorer

Theorem 3oalem6

Description: Lemma for 3OA (weak) orthoarguesian law. (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 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 ) ) ) ) )

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 2 chshii 
 |-  B e. SH
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 10 chshii 
 |-  R e. SH
12 3 choccli 
 |-  ( _|_ ` C ) e. CH
13 3 1 chjcli 
 |-  ( C vH A ) e. CH
14 12 13 chincli 
 |-  ( ( _|_ ` C ) i^i ( C vH A ) ) e. CH
15 5 14 eqeltri 
 |-  S e. CH
16 15 chshii 
 |-  S e. SH
17 3 chshii 
 |-  C e. SH
18 6 17 shscli 
 |-  ( B +H C ) e. SH
19 11 16 shscli 
 |-  ( R +H S ) e. SH
20 18 19 shincli 
 |-  ( ( B +H C ) i^i ( R +H S ) ) e. SH
21 16 20 shscli 
 |-  ( S +H ( ( B +H C ) i^i ( R +H S ) ) ) e. SH
22 11 21 shincli 
 |-  ( R i^i ( S +H ( ( B +H C ) i^i ( R +H S ) ) ) ) e. SH
23 6 22 shsleji 
 |-  ( B +H ( R i^i ( S +H ( ( B +H C ) i^i ( R +H S ) ) ) ) ) C_ ( B vH ( R i^i ( S +H ( ( B +H C ) i^i ( R +H S ) ) ) ) )
24 16 20 shsleji 
 |-  ( S +H ( ( B +H C ) i^i ( R +H S ) ) ) C_ ( S vH ( ( B +H C ) i^i ( R +H S ) ) )
25 2 3 chsleji 
 |-  ( B +H C ) C_ ( B vH C )
26 ssrin 
 |-  ( ( B +H C ) C_ ( B vH C ) -> ( ( B +H C ) i^i ( R +H S ) ) C_ ( ( B vH C ) i^i ( R +H S ) ) )
27 25 26 ax-mp 
 |-  ( ( B +H C ) i^i ( R +H S ) ) C_ ( ( B vH C ) i^i ( R +H S ) )
28 10 15 chsleji 
 |-  ( R +H S ) C_ ( R vH S )
29 sslin 
 |-  ( ( R +H S ) C_ ( R vH S ) -> ( ( B vH C ) i^i ( R +H S ) ) C_ ( ( B vH C ) i^i ( R vH S ) ) )
30 28 29 ax-mp 
 |-  ( ( B vH C ) i^i ( R +H S ) ) C_ ( ( B vH C ) i^i ( R vH S ) )
31 27 30 sstri 
 |-  ( ( B +H C ) i^i ( R +H S ) ) C_ ( ( B vH C ) i^i ( R vH S ) )
32 2 3 chjcli 
 |-  ( B vH C ) e. CH
33 10 15 chjcli 
 |-  ( R vH S ) e. CH
34 32 33 chincli 
 |-  ( ( B vH C ) i^i ( R vH S ) ) e. CH
35 34 chshii 
 |-  ( ( B vH C ) i^i ( R vH S ) ) e. SH
36 20 35 16 shlej2i 
 |-  ( ( ( B +H C ) i^i ( R +H S ) ) C_ ( ( B vH C ) i^i ( R vH S ) ) -> ( S vH ( ( B +H C ) i^i ( R +H S ) ) ) C_ ( S vH ( ( B vH C ) i^i ( R vH S ) ) ) )
37 31 36 ax-mp 
 |-  ( S vH ( ( B +H C ) i^i ( R +H S ) ) ) C_ ( S vH ( ( B vH C ) i^i ( R vH S ) ) )
38 24 37 sstri 
 |-  ( S +H ( ( B +H C ) i^i ( R +H S ) ) ) C_ ( S vH ( ( B vH C ) i^i ( R vH S ) ) )
39 sslin 
 |-  ( ( S +H ( ( B +H C ) i^i ( R +H S ) ) ) C_ ( S vH ( ( B vH C ) i^i ( R vH S ) ) ) -> ( R i^i ( S +H ( ( B +H C ) i^i ( R +H S ) ) ) ) C_ ( R i^i ( S vH ( ( B vH C ) i^i ( R vH S ) ) ) ) )
40 38 39 ax-mp 
 |-  ( R i^i ( S +H ( ( B +H C ) i^i ( R +H S ) ) ) ) C_ ( R i^i ( S vH ( ( B vH C ) i^i ( R vH S ) ) ) )
41 15 34 chjcli 
 |-  ( S vH ( ( B vH C ) i^i ( R vH S ) ) ) e. CH
42 10 41 chincli 
 |-  ( R i^i ( S vH ( ( B vH C ) i^i ( R vH S ) ) ) ) e. CH
43 42 chshii 
 |-  ( R i^i ( S vH ( ( B vH C ) i^i ( R vH S ) ) ) ) e. SH
44 22 43 6 shlej2i 
 |-  ( ( R i^i ( S +H ( ( B +H C ) i^i ( R +H S ) ) ) ) C_ ( R i^i ( S vH ( ( B vH C ) i^i ( R vH S ) ) ) ) -> ( B vH ( 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 ) ) ) ) ) )
45 40 44 ax-mp 
 |-  ( B vH ( 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 ) ) ) ) )
46 23 45 sstri 
 |-  ( 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 ) ) ) ) )