Metamath Proof Explorer

Theorem 5oai

Description: Orthoarguesian law 5OA. This 8-variable inference is called 5OA because it can be converted to a 5-variable equation (see Quantum Logic Explorer). (Contributed by NM, 5-May-2000) (New usage is discouraged.)

Ref Expression
Hypotheses 5oa.1 
|- A e. CH
5oa.2 
|- B e. CH
5oa.3 
|- C e. CH
5oa.4 
|- D e. CH
5oa.5 
|- F e. CH
5oa.6 
|- G e. CH
5oa.7 
|- R e. CH
5oa.8 
|- S e. CH
5oa.9 
|- A C_ ( _|_ ` B )
5oa.10 
|- C C_ ( _|_ ` D )
5oa.11 
|- F C_ ( _|_ ` G )
5oa.12 
|- R C_ ( _|_ ` S )
Assertion 5oai 
|- ( ( ( A vH B ) i^i ( C vH D ) ) i^i ( ( F vH G ) i^i ( R vH S ) ) ) C_ ( B vH ( A i^i ( C vH ( ( ( ( A vH C ) i^i ( B vH D ) ) i^i ( ( ( A vH R ) i^i ( B vH S ) ) vH ( ( C vH R ) i^i ( D vH S ) ) ) ) i^i ( ( ( ( A vH F ) i^i ( B vH G ) ) i^i ( ( ( A vH R ) i^i ( B vH S ) ) vH ( ( F vH R ) i^i ( G vH S ) ) ) ) vH ( ( ( C vH F ) i^i ( D vH G ) ) i^i ( ( ( C vH R ) i^i ( D vH S ) ) vH ( ( F vH R ) i^i ( G vH S ) ) ) ) ) ) ) ) )

Proof

Step Hyp Ref Expression
1 5oa.1 
 |-  A e. CH
2 5oa.2 
 |-  B e. CH
3 5oa.3 
 |-  C e. CH
4 5oa.4 
 |-  D e. CH
5 5oa.5 
 |-  F e. CH
6 5oa.6 
 |-  G e. CH
7 5oa.7 
 |-  R e. CH
8 5oa.8 
 |-  S e. CH
9 5oa.9 
 |-  A C_ ( _|_ ` B )
10 5oa.10 
 |-  C C_ ( _|_ ` D )
11 5oa.11 
 |-  F C_ ( _|_ ` G )
12 5oa.12 
 |-  R C_ ( _|_ ` S )
13 1 2 osumi 
 |-  ( A C_ ( _|_ ` B ) -> ( A +H B ) = ( A vH B ) )
14 9 13 ax-mp 
 |-  ( A +H B ) = ( A vH B )
15 3 4 osumi 
 |-  ( C C_ ( _|_ ` D ) -> ( C +H D ) = ( C vH D ) )
16 10 15 ax-mp 
 |-  ( C +H D ) = ( C vH D )
17 14 16 ineq12i 
 |-  ( ( A +H B ) i^i ( C +H D ) ) = ( ( A vH B ) i^i ( C vH D ) )
18 5 6 osumi 
 |-  ( F C_ ( _|_ ` G ) -> ( F +H G ) = ( F vH G ) )
19 11 18 ax-mp 
 |-  ( F +H G ) = ( F vH G )
20 7 8 osumi 
 |-  ( R C_ ( _|_ ` S ) -> ( R +H S ) = ( R vH S ) )
21 12 20 ax-mp 
 |-  ( R +H S ) = ( R vH S )
22 19 21 ineq12i 
 |-  ( ( F +H G ) i^i ( R +H S ) ) = ( ( F vH G ) i^i ( R vH S ) )
23 17 22 ineq12i 
 |-  ( ( ( A +H B ) i^i ( C +H D ) ) i^i ( ( F +H G ) i^i ( R +H S ) ) ) = ( ( ( A vH B ) i^i ( C vH D ) ) i^i ( ( F vH G ) i^i ( R vH S ) ) )
24 1 chshii 
 |-  A e. SH
25 2 chshii 
 |-  B e. SH
26 3 chshii 
 |-  C e. SH
27 4 chshii 
 |-  D e. SH
28 5 chshii 
 |-  F e. SH
29 6 chshii 
 |-  G e. SH
30 7 chshii 
 |-  R e. SH
31 8 chshii 
 |-  S e. SH
32 24 25 26 27 28 29 30 31 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 ) ) ) ) ) ) ) ) )
33 23 32 eqsstrri 
 |-  ( ( ( A vH B ) i^i ( C vH D ) ) i^i ( ( F vH G ) i^i ( R vH 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 ) ) ) ) ) ) ) ) )
34 24 26 shscli 
 |-  ( A +H C ) e. SH
35 25 27 shscli 
 |-  ( B +H D ) e. SH
36 34 35 shincli 
 |-  ( ( A +H C ) i^i ( B +H D ) ) e. SH
37 24 30 shscli 
 |-  ( A +H R ) e. SH
38 25 31 shscli 
 |-  ( B +H S ) e. SH
39 37 38 shincli 
 |-  ( ( A +H R ) i^i ( B +H S ) ) e. SH
40 26 30 shscli 
 |-  ( C +H R ) e. SH
41 27 31 shscli 
 |-  ( D +H S ) e. SH
42 40 41 shincli 
 |-  ( ( C +H R ) i^i ( D +H S ) ) e. SH
43 39 42 shscli 
 |-  ( ( ( A +H R ) i^i ( B +H S ) ) +H ( ( C +H R ) i^i ( D +H S ) ) ) e. SH
44 36 43 shincli 
 |-  ( ( ( 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 ) ) ) ) e. SH
45 24 28 shscli 
 |-  ( A +H F ) e. SH
46 25 29 shscli 
 |-  ( B +H G ) e. SH
47 45 46 shincli 
 |-  ( ( A +H F ) i^i ( B +H G ) ) e. SH
48 28 30 shscli 
 |-  ( F +H R ) e. SH
49 29 31 shscli 
 |-  ( G +H S ) e. SH
50 48 49 shincli 
 |-  ( ( F +H R ) i^i ( G +H S ) ) e. SH
51 39 50 shscli 
 |-  ( ( ( A +H R ) i^i ( B +H S ) ) +H ( ( F +H R ) i^i ( G +H S ) ) ) e. SH
52 47 51 shincli 
 |-  ( ( ( 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 ) ) ) ) e. SH
53 26 28 shscli 
 |-  ( C +H F ) e. SH
54 27 29 shscli 
 |-  ( D +H G ) e. SH
55 53 54 shincli 
 |-  ( ( C +H F ) i^i ( D +H G ) ) e. SH
56 42 50 shscli 
 |-  ( ( ( C +H R ) i^i ( D +H S ) ) +H ( ( F +H R ) i^i ( G +H S ) ) ) e. SH
57 55 56 shincli 
 |-  ( ( ( 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 ) ) ) ) e. SH
58 52 57 shscli 
 |-  ( ( ( ( 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 ) ) ) ) ) e. SH
59 44 58 shincli 
 |-  ( ( ( ( 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 ) ) ) ) ) ) e. SH
60 26 59 shscli 
 |-  ( 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 ) ) ) ) ) ) ) e. SH
61 24 60 shincli 
 |-  ( 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 ) ) ) ) ) ) ) ) e. SH
62 25 61 shsleji 
 |-  ( 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 ) ) ) ) ) ) ) ) ) C_ ( B vH ( 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 ) ) ) ) ) ) ) ) )
63 26 59 shsleji 
 |-  ( 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 ) ) ) ) ) ) ) C_ ( C vH ( ( ( ( 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 ) ) ) ) ) ) )
64 1 3 chsleji 
 |-  ( A +H C ) C_ ( A vH C )
65 2 4 chsleji 
 |-  ( B +H D ) C_ ( B vH D )
66 ss2in 
 |-  ( ( ( A +H C ) C_ ( A vH C ) /\ ( B +H D ) C_ ( B vH D ) ) -> ( ( A +H C ) i^i ( B +H D ) ) C_ ( ( A vH C ) i^i ( B vH D ) ) )
67 64 65 66 mp2an 
 |-  ( ( A +H C ) i^i ( B +H D ) ) C_ ( ( A vH C ) i^i ( B vH D ) )
68 39 42 shsleji 
 |-  ( ( ( A +H R ) i^i ( B +H S ) ) +H ( ( C +H R ) i^i ( D +H S ) ) ) C_ ( ( ( A +H R ) i^i ( B +H S ) ) vH ( ( C +H R ) i^i ( D +H S ) ) )
69 3 7 chsleji 
 |-  ( C +H R ) C_ ( C vH R )
70 4 8 chsleji 
 |-  ( D +H S ) C_ ( D vH S )
71 ss2in 
 |-  ( ( ( C +H R ) C_ ( C vH R ) /\ ( D +H S ) C_ ( D vH S ) ) -> ( ( C +H R ) i^i ( D +H S ) ) C_ ( ( C vH R ) i^i ( D vH S ) ) )
72 69 70 71 mp2an 
 |-  ( ( C +H R ) i^i ( D +H S ) ) C_ ( ( C vH R ) i^i ( D vH S ) )
73 26 30 shjshcli 
 |-  ( C vH R ) e. SH
74 27 31 shjshcli 
 |-  ( D vH S ) e. SH
75 73 74 shincli 
 |-  ( ( C vH R ) i^i ( D vH S ) ) e. SH
76 42 75 39 shlej2i 
 |-  ( ( ( C +H R ) i^i ( D +H S ) ) C_ ( ( C vH R ) i^i ( D vH S ) ) -> ( ( ( A +H R ) i^i ( B +H S ) ) vH ( ( C +H R ) i^i ( D +H S ) ) ) C_ ( ( ( A +H R ) i^i ( B +H S ) ) vH ( ( C vH R ) i^i ( D vH S ) ) ) )
77 72 76 ax-mp 
 |-  ( ( ( A +H R ) i^i ( B +H S ) ) vH ( ( C +H R ) i^i ( D +H S ) ) ) C_ ( ( ( A +H R ) i^i ( B +H S ) ) vH ( ( C vH R ) i^i ( D vH S ) ) )
78 1 7 chsleji 
 |-  ( A +H R ) C_ ( A vH R )
79 2 8 chsleji 
 |-  ( B +H S ) C_ ( B vH S )
80 ss2in 
 |-  ( ( ( A +H R ) C_ ( A vH R ) /\ ( B +H S ) C_ ( B vH S ) ) -> ( ( A +H R ) i^i ( B +H S ) ) C_ ( ( A vH R ) i^i ( B vH S ) ) )
81 78 79 80 mp2an 
 |-  ( ( A +H R ) i^i ( B +H S ) ) C_ ( ( A vH R ) i^i ( B vH S ) )
82 24 30 shjshcli 
 |-  ( A vH R ) e. SH
83 25 31 shjshcli 
 |-  ( B vH S ) e. SH
84 82 83 shincli 
 |-  ( ( A vH R ) i^i ( B vH S ) ) e. SH
85 39 84 75 shlej1i 
 |-  ( ( ( A +H R ) i^i ( B +H S ) ) C_ ( ( A vH R ) i^i ( B vH S ) ) -> ( ( ( A +H R ) i^i ( B +H S ) ) vH ( ( C vH R ) i^i ( D vH S ) ) ) C_ ( ( ( A vH R ) i^i ( B vH S ) ) vH ( ( C vH R ) i^i ( D vH S ) ) ) )
86 81 85 ax-mp 
 |-  ( ( ( A +H R ) i^i ( B +H S ) ) vH ( ( C vH R ) i^i ( D vH S ) ) ) C_ ( ( ( A vH R ) i^i ( B vH S ) ) vH ( ( C vH R ) i^i ( D vH S ) ) )
87 77 86 sstri 
 |-  ( ( ( A +H R ) i^i ( B +H S ) ) vH ( ( C +H R ) i^i ( D +H S ) ) ) C_ ( ( ( A vH R ) i^i ( B vH S ) ) vH ( ( C vH R ) i^i ( D vH S ) ) )
88 68 87 sstri 
 |-  ( ( ( A +H R ) i^i ( B +H S ) ) +H ( ( C +H R ) i^i ( D +H S ) ) ) C_ ( ( ( A vH R ) i^i ( B vH S ) ) vH ( ( C vH R ) i^i ( D vH S ) ) )
89 ss2in 
 |-  ( ( ( ( A +H C ) i^i ( B +H D ) ) C_ ( ( A vH C ) i^i ( B vH D ) ) /\ ( ( ( A +H R ) i^i ( B +H S ) ) +H ( ( C +H R ) i^i ( D +H S ) ) ) C_ ( ( ( A vH R ) i^i ( B vH S ) ) vH ( ( C vH R ) i^i ( D vH S ) ) ) ) -> ( ( ( 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 ) ) ) ) C_ ( ( ( A vH C ) i^i ( B vH D ) ) i^i ( ( ( A vH R ) i^i ( B vH S ) ) vH ( ( C vH R ) i^i ( D vH S ) ) ) ) )
90 67 88 89 mp2an 
 |-  ( ( ( 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 ) ) ) ) C_ ( ( ( A vH C ) i^i ( B vH D ) ) i^i ( ( ( A vH R ) i^i ( B vH S ) ) vH ( ( C vH R ) i^i ( D vH S ) ) ) )
91 52 57 shsleji 
 |-  ( ( ( ( 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 ) ) ) ) ) C_ ( ( ( ( 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 ) ) ) ) vH ( ( ( 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 ) ) ) ) )
92 3 5 chsleji 
 |-  ( C +H F ) C_ ( C vH F )
93 4 6 chsleji 
 |-  ( D +H G ) C_ ( D vH G )
94 ss2in 
 |-  ( ( ( C +H F ) C_ ( C vH F ) /\ ( D +H G ) C_ ( D vH G ) ) -> ( ( C +H F ) i^i ( D +H G ) ) C_ ( ( C vH F ) i^i ( D vH G ) ) )
95 92 93 94 mp2an 
 |-  ( ( C +H F ) i^i ( D +H G ) ) C_ ( ( C vH F ) i^i ( D vH G ) )
96 42 50 shsleji 
 |-  ( ( ( C +H R ) i^i ( D +H S ) ) +H ( ( F +H R ) i^i ( G +H S ) ) ) C_ ( ( ( C +H R ) i^i ( D +H S ) ) vH ( ( F +H R ) i^i ( G +H S ) ) )
97 5 7 chsleji 
 |-  ( F +H R ) C_ ( F vH R )
98 6 8 chsleji 
 |-  ( G +H S ) C_ ( G vH S )
99 ss2in 
 |-  ( ( ( F +H R ) C_ ( F vH R ) /\ ( G +H S ) C_ ( G vH S ) ) -> ( ( F +H R ) i^i ( G +H S ) ) C_ ( ( F vH R ) i^i ( G vH S ) ) )
100 97 98 99 mp2an 
 |-  ( ( F +H R ) i^i ( G +H S ) ) C_ ( ( F vH R ) i^i ( G vH S ) )
101 28 30 shjshcli 
 |-  ( F vH R ) e. SH
102 29 31 shjshcli 
 |-  ( G vH S ) e. SH
103 101 102 shincli 
 |-  ( ( F vH R ) i^i ( G vH S ) ) e. SH
104 50 103 42 shlej2i 
 |-  ( ( ( F +H R ) i^i ( G +H S ) ) C_ ( ( F vH R ) i^i ( G vH S ) ) -> ( ( ( C +H R ) i^i ( D +H S ) ) vH ( ( F +H R ) i^i ( G +H S ) ) ) C_ ( ( ( C +H R ) i^i ( D +H S ) ) vH ( ( F vH R ) i^i ( G vH S ) ) ) )
105 100 104 ax-mp 
 |-  ( ( ( C +H R ) i^i ( D +H S ) ) vH ( ( F +H R ) i^i ( G +H S ) ) ) C_ ( ( ( C +H R ) i^i ( D +H S ) ) vH ( ( F vH R ) i^i ( G vH S ) ) )
106 42 75 103 shlej1i 
 |-  ( ( ( C +H R ) i^i ( D +H S ) ) C_ ( ( C vH R ) i^i ( D vH S ) ) -> ( ( ( C +H R ) i^i ( D +H S ) ) vH ( ( F vH R ) i^i ( G vH S ) ) ) C_ ( ( ( C vH R ) i^i ( D vH S ) ) vH ( ( F vH R ) i^i ( G vH S ) ) ) )
107 72 106 ax-mp 
 |-  ( ( ( C +H R ) i^i ( D +H S ) ) vH ( ( F vH R ) i^i ( G vH S ) ) ) C_ ( ( ( C vH R ) i^i ( D vH S ) ) vH ( ( F vH R ) i^i ( G vH S ) ) )
108 105 107 sstri 
 |-  ( ( ( C +H R ) i^i ( D +H S ) ) vH ( ( F +H R ) i^i ( G +H S ) ) ) C_ ( ( ( C vH R ) i^i ( D vH S ) ) vH ( ( F vH R ) i^i ( G vH S ) ) )
109 96 108 sstri 
 |-  ( ( ( C +H R ) i^i ( D +H S ) ) +H ( ( F +H R ) i^i ( G +H S ) ) ) C_ ( ( ( C vH R ) i^i ( D vH S ) ) vH ( ( F vH R ) i^i ( G vH S ) ) )
110 ss2in 
 |-  ( ( ( ( C +H F ) i^i ( D +H G ) ) C_ ( ( C vH F ) i^i ( D vH G ) ) /\ ( ( ( C +H R ) i^i ( D +H S ) ) +H ( ( F +H R ) i^i ( G +H S ) ) ) C_ ( ( ( C vH R ) i^i ( D vH S ) ) vH ( ( F vH R ) i^i ( G vH S ) ) ) ) -> ( ( ( 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 ) ) ) ) C_ ( ( ( C vH F ) i^i ( D vH G ) ) i^i ( ( ( C vH R ) i^i ( D vH S ) ) vH ( ( F vH R ) i^i ( G vH S ) ) ) ) )
111 95 109 110 mp2an 
 |-  ( ( ( 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 ) ) ) ) C_ ( ( ( C vH F ) i^i ( D vH G ) ) i^i ( ( ( C vH R ) i^i ( D vH S ) ) vH ( ( F vH R ) i^i ( G vH S ) ) ) )
112 3 5 chjcli 
 |-  ( C vH F ) e. CH
113 4 6 chjcli 
 |-  ( D vH G ) e. CH
114 112 113 chincli 
 |-  ( ( C vH F ) i^i ( D vH G ) ) e. CH
115 114 chshii 
 |-  ( ( C vH F ) i^i ( D vH G ) ) e. SH
116 75 103 shjshcli 
 |-  ( ( ( C vH R ) i^i ( D vH S ) ) vH ( ( F vH R ) i^i ( G vH S ) ) ) e. SH
117 115 116 shincli 
 |-  ( ( ( C vH F ) i^i ( D vH G ) ) i^i ( ( ( C vH R ) i^i ( D vH S ) ) vH ( ( F vH R ) i^i ( G vH S ) ) ) ) e. SH
118 57 117 52 shlej2i 
 |-  ( ( ( ( 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 ) ) ) ) C_ ( ( ( C vH F ) i^i ( D vH G ) ) i^i ( ( ( C vH R ) i^i ( D vH S ) ) vH ( ( F vH R ) i^i ( G vH S ) ) ) ) -> ( ( ( ( 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 ) ) ) ) vH ( ( ( 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 ) ) ) ) ) C_ ( ( ( ( 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 ) ) ) ) vH ( ( ( C vH F ) i^i ( D vH G ) ) i^i ( ( ( C vH R ) i^i ( D vH S ) ) vH ( ( F vH R ) i^i ( G vH S ) ) ) ) ) )
119 111 118 ax-mp 
 |-  ( ( ( ( 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 ) ) ) ) vH ( ( ( 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 ) ) ) ) ) C_ ( ( ( ( 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 ) ) ) ) vH ( ( ( C vH F ) i^i ( D vH G ) ) i^i ( ( ( C vH R ) i^i ( D vH S ) ) vH ( ( F vH R ) i^i ( G vH S ) ) ) ) )
120 1 5 chsleji 
 |-  ( A +H F ) C_ ( A vH F )
121 2 6 chsleji 
 |-  ( B +H G ) C_ ( B vH G )
122 ss2in 
 |-  ( ( ( A +H F ) C_ ( A vH F ) /\ ( B +H G ) C_ ( B vH G ) ) -> ( ( A +H F ) i^i ( B +H G ) ) C_ ( ( A vH F ) i^i ( B vH G ) ) )
123 120 121 122 mp2an 
 |-  ( ( A +H F ) i^i ( B +H G ) ) C_ ( ( A vH F ) i^i ( B vH G ) )
124 39 50 shsleji 
 |-  ( ( ( A +H R ) i^i ( B +H S ) ) +H ( ( F +H R ) i^i ( G +H S ) ) ) C_ ( ( ( A +H R ) i^i ( B +H S ) ) vH ( ( F +H R ) i^i ( G +H S ) ) )
125 50 103 39 shlej2i 
 |-  ( ( ( F +H R ) i^i ( G +H S ) ) C_ ( ( F vH R ) i^i ( G vH S ) ) -> ( ( ( A +H R ) i^i ( B +H S ) ) vH ( ( F +H R ) i^i ( G +H S ) ) ) C_ ( ( ( A +H R ) i^i ( B +H S ) ) vH ( ( F vH R ) i^i ( G vH S ) ) ) )
126 100 125 ax-mp 
 |-  ( ( ( A +H R ) i^i ( B +H S ) ) vH ( ( F +H R ) i^i ( G +H S ) ) ) C_ ( ( ( A +H R ) i^i ( B +H S ) ) vH ( ( F vH R ) i^i ( G vH S ) ) )
127 39 84 103 shlej1i 
 |-  ( ( ( A +H R ) i^i ( B +H S ) ) C_ ( ( A vH R ) i^i ( B vH S ) ) -> ( ( ( A +H R ) i^i ( B +H S ) ) vH ( ( F vH R ) i^i ( G vH S ) ) ) C_ ( ( ( A vH R ) i^i ( B vH S ) ) vH ( ( F vH R ) i^i ( G vH S ) ) ) )
128 81 127 ax-mp 
 |-  ( ( ( A +H R ) i^i ( B +H S ) ) vH ( ( F vH R ) i^i ( G vH S ) ) ) C_ ( ( ( A vH R ) i^i ( B vH S ) ) vH ( ( F vH R ) i^i ( G vH S ) ) )
129 126 128 sstri 
 |-  ( ( ( A +H R ) i^i ( B +H S ) ) vH ( ( F +H R ) i^i ( G +H S ) ) ) C_ ( ( ( A vH R ) i^i ( B vH S ) ) vH ( ( F vH R ) i^i ( G vH S ) ) )
130 124 129 sstri 
 |-  ( ( ( A +H R ) i^i ( B +H S ) ) +H ( ( F +H R ) i^i ( G +H S ) ) ) C_ ( ( ( A vH R ) i^i ( B vH S ) ) vH ( ( F vH R ) i^i ( G vH S ) ) )
131 ss2in 
 |-  ( ( ( ( A +H F ) i^i ( B +H G ) ) C_ ( ( A vH F ) i^i ( B vH G ) ) /\ ( ( ( A +H R ) i^i ( B +H S ) ) +H ( ( F +H R ) i^i ( G +H S ) ) ) C_ ( ( ( A vH R ) i^i ( B vH S ) ) vH ( ( F vH R ) i^i ( G vH S ) ) ) ) -> ( ( ( 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 ) ) ) ) C_ ( ( ( A vH F ) i^i ( B vH G ) ) i^i ( ( ( A vH R ) i^i ( B vH S ) ) vH ( ( F vH R ) i^i ( G vH S ) ) ) ) )
132 123 130 131 mp2an 
 |-  ( ( ( 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 ) ) ) ) C_ ( ( ( A vH F ) i^i ( B vH G ) ) i^i ( ( ( A vH R ) i^i ( B vH S ) ) vH ( ( F vH R ) i^i ( G vH S ) ) ) )
133 1 5 chjcli 
 |-  ( A vH F ) e. CH
134 2 6 chjcli 
 |-  ( B vH G ) e. CH
135 133 134 chincli 
 |-  ( ( A vH F ) i^i ( B vH G ) ) e. CH
136 135 chshii 
 |-  ( ( A vH F ) i^i ( B vH G ) ) e. SH
137 84 103 shjshcli 
 |-  ( ( ( A vH R ) i^i ( B vH S ) ) vH ( ( F vH R ) i^i ( G vH S ) ) ) e. SH
138 136 137 shincli 
 |-  ( ( ( A vH F ) i^i ( B vH G ) ) i^i ( ( ( A vH R ) i^i ( B vH S ) ) vH ( ( F vH R ) i^i ( G vH S ) ) ) ) e. SH
139 52 138 117 shlej1i 
 |-  ( ( ( ( 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 ) ) ) ) C_ ( ( ( A vH F ) i^i ( B vH G ) ) i^i ( ( ( A vH R ) i^i ( B vH S ) ) vH ( ( F vH R ) i^i ( G vH S ) ) ) ) -> ( ( ( ( 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 ) ) ) ) vH ( ( ( C vH F ) i^i ( D vH G ) ) i^i ( ( ( C vH R ) i^i ( D vH S ) ) vH ( ( F vH R ) i^i ( G vH S ) ) ) ) ) C_ ( ( ( ( A vH F ) i^i ( B vH G ) ) i^i ( ( ( A vH R ) i^i ( B vH S ) ) vH ( ( F vH R ) i^i ( G vH S ) ) ) ) vH ( ( ( C vH F ) i^i ( D vH G ) ) i^i ( ( ( C vH R ) i^i ( D vH S ) ) vH ( ( F vH R ) i^i ( G vH S ) ) ) ) ) )
140 132 139 ax-mp 
 |-  ( ( ( ( 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 ) ) ) ) vH ( ( ( C vH F ) i^i ( D vH G ) ) i^i ( ( ( C vH R ) i^i ( D vH S ) ) vH ( ( F vH R ) i^i ( G vH S ) ) ) ) ) C_ ( ( ( ( A vH F ) i^i ( B vH G ) ) i^i ( ( ( A vH R ) i^i ( B vH S ) ) vH ( ( F vH R ) i^i ( G vH S ) ) ) ) vH ( ( ( C vH F ) i^i ( D vH G ) ) i^i ( ( ( C vH R ) i^i ( D vH S ) ) vH ( ( F vH R ) i^i ( G vH S ) ) ) ) )
141 119 140 sstri 
 |-  ( ( ( ( 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 ) ) ) ) vH ( ( ( 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 ) ) ) ) ) C_ ( ( ( ( A vH F ) i^i ( B vH G ) ) i^i ( ( ( A vH R ) i^i ( B vH S ) ) vH ( ( F vH R ) i^i ( G vH S ) ) ) ) vH ( ( ( C vH F ) i^i ( D vH G ) ) i^i ( ( ( C vH R ) i^i ( D vH S ) ) vH ( ( F vH R ) i^i ( G vH S ) ) ) ) )
142 91 141 sstri 
 |-  ( ( ( ( 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 ) ) ) ) ) C_ ( ( ( ( A vH F ) i^i ( B vH G ) ) i^i ( ( ( A vH R ) i^i ( B vH S ) ) vH ( ( F vH R ) i^i ( G vH S ) ) ) ) vH ( ( ( C vH F ) i^i ( D vH G ) ) i^i ( ( ( C vH R ) i^i ( D vH S ) ) vH ( ( F vH R ) i^i ( G vH S ) ) ) ) )
143 ss2in 
 |-  ( ( ( ( ( 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 ) ) ) ) C_ ( ( ( A vH C ) i^i ( B vH D ) ) i^i ( ( ( A vH R ) i^i ( B vH S ) ) vH ( ( C vH R ) i^i ( D vH S ) ) ) ) /\ ( ( ( ( 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 ) ) ) ) ) C_ ( ( ( ( A vH F ) i^i ( B vH G ) ) i^i ( ( ( A vH R ) i^i ( B vH S ) ) vH ( ( F vH R ) i^i ( G vH S ) ) ) ) vH ( ( ( C vH F ) i^i ( D vH G ) ) i^i ( ( ( C vH R ) i^i ( D vH S ) ) vH ( ( F vH R ) i^i ( G vH S ) ) ) ) ) ) -> ( ( ( ( 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 ) ) ) ) ) ) C_ ( ( ( ( A vH C ) i^i ( B vH D ) ) i^i ( ( ( A vH R ) i^i ( B vH S ) ) vH ( ( C vH R ) i^i ( D vH S ) ) ) ) i^i ( ( ( ( A vH F ) i^i ( B vH G ) ) i^i ( ( ( A vH R ) i^i ( B vH S ) ) vH ( ( F vH R ) i^i ( G vH S ) ) ) ) vH ( ( ( C vH F ) i^i ( D vH G ) ) i^i ( ( ( C vH R ) i^i ( D vH S ) ) vH ( ( F vH R ) i^i ( G vH S ) ) ) ) ) ) )
144 90 142 143 mp2an 
 |-  ( ( ( ( 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 ) ) ) ) ) ) C_ ( ( ( ( A vH C ) i^i ( B vH D ) ) i^i ( ( ( A vH R ) i^i ( B vH S ) ) vH ( ( C vH R ) i^i ( D vH S ) ) ) ) i^i ( ( ( ( A vH F ) i^i ( B vH G ) ) i^i ( ( ( A vH R ) i^i ( B vH S ) ) vH ( ( F vH R ) i^i ( G vH S ) ) ) ) vH ( ( ( C vH F ) i^i ( D vH G ) ) i^i ( ( ( C vH R ) i^i ( D vH S ) ) vH ( ( F vH R ) i^i ( G vH S ) ) ) ) ) )
145 1 3 chjcli 
 |-  ( A vH C ) e. CH
146 2 4 chjcli 
 |-  ( B vH D ) e. CH
147 145 146 chincli 
 |-  ( ( A vH C ) i^i ( B vH D ) ) e. CH
148 84 75 shjcli 
 |-  ( ( ( A vH R ) i^i ( B vH S ) ) vH ( ( C vH R ) i^i ( D vH S ) ) ) e. CH
149 147 148 chincli 
 |-  ( ( ( A vH C ) i^i ( B vH D ) ) i^i ( ( ( A vH R ) i^i ( B vH S ) ) vH ( ( C vH R ) i^i ( D vH S ) ) ) ) e. CH
150 149 chshii 
 |-  ( ( ( A vH C ) i^i ( B vH D ) ) i^i ( ( ( A vH R ) i^i ( B vH S ) ) vH ( ( C vH R ) i^i ( D vH S ) ) ) ) e. SH
151 138 117 shjshcli 
 |-  ( ( ( ( A vH F ) i^i ( B vH G ) ) i^i ( ( ( A vH R ) i^i ( B vH S ) ) vH ( ( F vH R ) i^i ( G vH S ) ) ) ) vH ( ( ( C vH F ) i^i ( D vH G ) ) i^i ( ( ( C vH R ) i^i ( D vH S ) ) vH ( ( F vH R ) i^i ( G vH S ) ) ) ) ) e. SH
152 150 151 shincli 
 |-  ( ( ( ( A vH C ) i^i ( B vH D ) ) i^i ( ( ( A vH R ) i^i ( B vH S ) ) vH ( ( C vH R ) i^i ( D vH S ) ) ) ) i^i ( ( ( ( A vH F ) i^i ( B vH G ) ) i^i ( ( ( A vH R ) i^i ( B vH S ) ) vH ( ( F vH R ) i^i ( G vH S ) ) ) ) vH ( ( ( C vH F ) i^i ( D vH G ) ) i^i ( ( ( C vH R ) i^i ( D vH S ) ) vH ( ( F vH R ) i^i ( G vH S ) ) ) ) ) ) e. SH
153 59 152 26 shlej2i 
 |-  ( ( ( ( ( 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 ) ) ) ) ) ) C_ ( ( ( ( A vH C ) i^i ( B vH D ) ) i^i ( ( ( A vH R ) i^i ( B vH S ) ) vH ( ( C vH R ) i^i ( D vH S ) ) ) ) i^i ( ( ( ( A vH F ) i^i ( B vH G ) ) i^i ( ( ( A vH R ) i^i ( B vH S ) ) vH ( ( F vH R ) i^i ( G vH S ) ) ) ) vH ( ( ( C vH F ) i^i ( D vH G ) ) i^i ( ( ( C vH R ) i^i ( D vH S ) ) vH ( ( F vH R ) i^i ( G vH S ) ) ) ) ) ) -> ( C vH ( ( ( ( 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 ) ) ) ) ) ) ) C_ ( C vH ( ( ( ( A vH C ) i^i ( B vH D ) ) i^i ( ( ( A vH R ) i^i ( B vH S ) ) vH ( ( C vH R ) i^i ( D vH S ) ) ) ) i^i ( ( ( ( A vH F ) i^i ( B vH G ) ) i^i ( ( ( A vH R ) i^i ( B vH S ) ) vH ( ( F vH R ) i^i ( G vH S ) ) ) ) vH ( ( ( C vH F ) i^i ( D vH G ) ) i^i ( ( ( C vH R ) i^i ( D vH S ) ) vH ( ( F vH R ) i^i ( G vH S ) ) ) ) ) ) ) )
154 144 153 ax-mp 
 |-  ( C vH ( ( ( ( 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 ) ) ) ) ) ) ) C_ ( C vH ( ( ( ( A vH C ) i^i ( B vH D ) ) i^i ( ( ( A vH R ) i^i ( B vH S ) ) vH ( ( C vH R ) i^i ( D vH S ) ) ) ) i^i ( ( ( ( A vH F ) i^i ( B vH G ) ) i^i ( ( ( A vH R ) i^i ( B vH S ) ) vH ( ( F vH R ) i^i ( G vH S ) ) ) ) vH ( ( ( C vH F ) i^i ( D vH G ) ) i^i ( ( ( C vH R ) i^i ( D vH S ) ) vH ( ( F vH R ) i^i ( G vH S ) ) ) ) ) ) )
155 63 154 sstri 
 |-  ( 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 ) ) ) ) ) ) ) C_ ( C vH ( ( ( ( A vH C ) i^i ( B vH D ) ) i^i ( ( ( A vH R ) i^i ( B vH S ) ) vH ( ( C vH R ) i^i ( D vH S ) ) ) ) i^i ( ( ( ( A vH F ) i^i ( B vH G ) ) i^i ( ( ( A vH R ) i^i ( B vH S ) ) vH ( ( F vH R ) i^i ( G vH S ) ) ) ) vH ( ( ( C vH F ) i^i ( D vH G ) ) i^i ( ( ( C vH R ) i^i ( D vH S ) ) vH ( ( F vH R ) i^i ( G vH S ) ) ) ) ) ) )
156 sslin 
 |-  ( ( 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 ) ) ) ) ) ) ) C_ ( C vH ( ( ( ( A vH C ) i^i ( B vH D ) ) i^i ( ( ( A vH R ) i^i ( B vH S ) ) vH ( ( C vH R ) i^i ( D vH S ) ) ) ) i^i ( ( ( ( A vH F ) i^i ( B vH G ) ) i^i ( ( ( A vH R ) i^i ( B vH S ) ) vH ( ( F vH R ) i^i ( G vH S ) ) ) ) vH ( ( ( C vH F ) i^i ( D vH G ) ) i^i ( ( ( C vH R ) i^i ( D vH S ) ) vH ( ( F vH R ) i^i ( G vH S ) ) ) ) ) ) ) -> ( 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 ) ) ) ) ) ) ) ) C_ ( A i^i ( C vH ( ( ( ( A vH C ) i^i ( B vH D ) ) i^i ( ( ( A vH R ) i^i ( B vH S ) ) vH ( ( C vH R ) i^i ( D vH S ) ) ) ) i^i ( ( ( ( A vH F ) i^i ( B vH G ) ) i^i ( ( ( A vH R ) i^i ( B vH S ) ) vH ( ( F vH R ) i^i ( G vH S ) ) ) ) vH ( ( ( C vH F ) i^i ( D vH G ) ) i^i ( ( ( C vH R ) i^i ( D vH S ) ) vH ( ( F vH R ) i^i ( G vH S ) ) ) ) ) ) ) ) )
157 155 156 ax-mp 
 |-  ( 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 ) ) ) ) ) ) ) ) C_ ( A i^i ( C vH ( ( ( ( A vH C ) i^i ( B vH D ) ) i^i ( ( ( A vH R ) i^i ( B vH S ) ) vH ( ( C vH R ) i^i ( D vH S ) ) ) ) i^i ( ( ( ( A vH F ) i^i ( B vH G ) ) i^i ( ( ( A vH R ) i^i ( B vH S ) ) vH ( ( F vH R ) i^i ( G vH S ) ) ) ) vH ( ( ( C vH F ) i^i ( D vH G ) ) i^i ( ( ( C vH R ) i^i ( D vH S ) ) vH ( ( F vH R ) i^i ( G vH S ) ) ) ) ) ) ) )
158 26 152 shjshcli 
 |-  ( C vH ( ( ( ( A vH C ) i^i ( B vH D ) ) i^i ( ( ( A vH R ) i^i ( B vH S ) ) vH ( ( C vH R ) i^i ( D vH S ) ) ) ) i^i ( ( ( ( A vH F ) i^i ( B vH G ) ) i^i ( ( ( A vH R ) i^i ( B vH S ) ) vH ( ( F vH R ) i^i ( G vH S ) ) ) ) vH ( ( ( C vH F ) i^i ( D vH G ) ) i^i ( ( ( C vH R ) i^i ( D vH S ) ) vH ( ( F vH R ) i^i ( G vH S ) ) ) ) ) ) ) e. SH
159 24 158 shincli 
 |-  ( A i^i ( C vH ( ( ( ( A vH C ) i^i ( B vH D ) ) i^i ( ( ( A vH R ) i^i ( B vH S ) ) vH ( ( C vH R ) i^i ( D vH S ) ) ) ) i^i ( ( ( ( A vH F ) i^i ( B vH G ) ) i^i ( ( ( A vH R ) i^i ( B vH S ) ) vH ( ( F vH R ) i^i ( G vH S ) ) ) ) vH ( ( ( C vH F ) i^i ( D vH G ) ) i^i ( ( ( C vH R ) i^i ( D vH S ) ) vH ( ( F vH R ) i^i ( G vH S ) ) ) ) ) ) ) ) e. SH
160 61 159 25 shlej2i 
 |-  ( ( 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 ) ) ) ) ) ) ) ) C_ ( A i^i ( C vH ( ( ( ( A vH C ) i^i ( B vH D ) ) i^i ( ( ( A vH R ) i^i ( B vH S ) ) vH ( ( C vH R ) i^i ( D vH S ) ) ) ) i^i ( ( ( ( A vH F ) i^i ( B vH G ) ) i^i ( ( ( A vH R ) i^i ( B vH S ) ) vH ( ( F vH R ) i^i ( G vH S ) ) ) ) vH ( ( ( C vH F ) i^i ( D vH G ) ) i^i ( ( ( C vH R ) i^i ( D vH S ) ) vH ( ( F vH R ) i^i ( G vH S ) ) ) ) ) ) ) ) -> ( B vH ( 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 ) ) ) ) ) ) ) ) ) C_ ( B vH ( A i^i ( C vH ( ( ( ( A vH C ) i^i ( B vH D ) ) i^i ( ( ( A vH R ) i^i ( B vH S ) ) vH ( ( C vH R ) i^i ( D vH S ) ) ) ) i^i ( ( ( ( A vH F ) i^i ( B vH G ) ) i^i ( ( ( A vH R ) i^i ( B vH S ) ) vH ( ( F vH R ) i^i ( G vH S ) ) ) ) vH ( ( ( C vH F ) i^i ( D vH G ) ) i^i ( ( ( C vH R ) i^i ( D vH S ) ) vH ( ( F vH R ) i^i ( G vH S ) ) ) ) ) ) ) ) ) )
161 157 160 ax-mp 
 |-  ( B vH ( 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 ) ) ) ) ) ) ) ) ) C_ ( B vH ( A i^i ( C vH ( ( ( ( A vH C ) i^i ( B vH D ) ) i^i ( ( ( A vH R ) i^i ( B vH S ) ) vH ( ( C vH R ) i^i ( D vH S ) ) ) ) i^i ( ( ( ( A vH F ) i^i ( B vH G ) ) i^i ( ( ( A vH R ) i^i ( B vH S ) ) vH ( ( F vH R ) i^i ( G vH S ) ) ) ) vH ( ( ( C vH F ) i^i ( D vH G ) ) i^i ( ( ( C vH R ) i^i ( D vH S ) ) vH ( ( F vH R ) i^i ( G vH S ) ) ) ) ) ) ) ) )
162 62 161 sstri 
 |-  ( 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 ) ) ) ) ) ) ) ) ) C_ ( B vH ( A i^i ( C vH ( ( ( ( A vH C ) i^i ( B vH D ) ) i^i ( ( ( A vH R ) i^i ( B vH S ) ) vH ( ( C vH R ) i^i ( D vH S ) ) ) ) i^i ( ( ( ( A vH F ) i^i ( B vH G ) ) i^i ( ( ( A vH R ) i^i ( B vH S ) ) vH ( ( F vH R ) i^i ( G vH S ) ) ) ) vH ( ( ( C vH F ) i^i ( D vH G ) ) i^i ( ( ( C vH R ) i^i ( D vH S ) ) vH ( ( F vH R ) i^i ( G vH S ) ) ) ) ) ) ) ) )
163 33 162 sstri 
 |-  ( ( ( A vH B ) i^i ( C vH D ) ) i^i ( ( F vH G ) i^i ( R vH S ) ) ) C_ ( B vH ( A i^i ( C vH ( ( ( ( A vH C ) i^i ( B vH D ) ) i^i ( ( ( A vH R ) i^i ( B vH S ) ) vH ( ( C vH R ) i^i ( D vH S ) ) ) ) i^i ( ( ( ( A vH F ) i^i ( B vH G ) ) i^i ( ( ( A vH R ) i^i ( B vH S ) ) vH ( ( F vH R ) i^i ( G vH S ) ) ) ) vH ( ( ( C vH F ) i^i ( D vH G ) ) i^i ( ( ( C vH R ) i^i ( D vH S ) ) vH ( ( F vH R ) i^i ( G vH S ) ) ) ) ) ) ) ) )