Metamath Proof Explorer

Theorem 3oalem5

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 3oalem5
`|- ( ( B +H R ) i^i ( C +H S ) ) = ( ( B vH R ) i^i ( C 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 4 3oalem4
` |-  R C_ ( _|_ ` B )`
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 2 osumi
` |-  ( R C_ ( _|_ ` B ) -> ( R +H B ) = ( R vH B ) )`
12 6 11 ax-mp
` |-  ( R +H B ) = ( R vH B )`
13 2 chshii
` |-  B e. SH`
14 10 chshii
` |-  R e. SH`
15 13 14 shscomi
` |-  ( B +H R ) = ( R +H B )`
16 2 10 chjcomi
` |-  ( B vH R ) = ( R vH B )`
17 12 15 16 3eqtr4i
` |-  ( B +H R ) = ( B vH R )`
18 5 3oalem4
` |-  S C_ ( _|_ ` C )`
19 3 choccli
` |-  ( _|_ ` C ) e. CH`
20 3 1 chjcli
` |-  ( C vH A ) e. CH`
21 19 20 chincli
` |-  ( ( _|_ ` C ) i^i ( C vH A ) ) e. CH`
22 5 21 eqeltri
` |-  S e. CH`
23 22 3 osumi
` |-  ( S C_ ( _|_ ` C ) -> ( S +H C ) = ( S vH C ) )`
24 18 23 ax-mp
` |-  ( S +H C ) = ( S vH C )`
25 3 chshii
` |-  C e. SH`
26 22 chshii
` |-  S e. SH`
27 25 26 shscomi
` |-  ( C +H S ) = ( S +H C )`
28 3 22 chjcomi
` |-  ( C vH S ) = ( S vH C )`
29 24 27 28 3eqtr4i
` |-  ( C +H S ) = ( C vH S )`
30 17 29 ineq12i
` |-  ( ( B +H R ) i^i ( C +H S ) ) = ( ( B vH R ) i^i ( C vH S ) )`