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 ) )