Theorem 3oalem1

Description: Lemma for 3OA (weak) orthoarguesian law. (Contributed by NM, 19-Oct-1999) (New usage is discouraged.)

	Ref	Expression
Hypotheses	3oalem1.1	|- B e. CH
	3oalem1.2	|- C e. CH
	3oalem1.3	|- R e. CH
	3oalem1.4	|- S e. CH
Assertion	3oalem1	|- ( ( ( ( x e. B /\ y e. R ) /\ v = ( x +h y ) ) /\ ( ( z e. C /\ w e. S ) /\ v = ( z +h w ) ) ) -> ( ( ( x e. ~H /\ y e. ~H ) /\ v e. ~H ) /\ ( z e. ~H /\ w e. ~H ) ) )

Proof

Step	Hyp	Ref	Expression
1		3oalem1.1	|- B e. CH
2		3oalem1.2	|- C e. CH
3		3oalem1.3	|- R e. CH
4		3oalem1.4	|- S e. CH
5	1	cheli	|- ( x e. B -> x e. ~H )
6	3	cheli	|- ( y e. R -> y e. ~H )
7	5 6	anim12i	|- ( ( x e. B /\ y e. R ) -> ( x e. ~H /\ y e. ~H ) )
8		hvaddcl	|- ( ( x e. ~H /\ y e. ~H ) -> ( x +h y ) e. ~H )
9		eleq1	|- ( v = ( x +h y ) -> ( v e. ~H <-> ( x +h y ) e. ~H ) )
10	8 9	syl5ibrcom	|- ( ( x e. ~H /\ y e. ~H ) -> ( v = ( x +h y ) -> v e. ~H ) )
11	10	imdistani	|- ( ( ( x e. ~H /\ y e. ~H ) /\ v = ( x +h y ) ) -> ( ( x e. ~H /\ y e. ~H ) /\ v e. ~H ) )
12	7 11	sylan	|- ( ( ( x e. B /\ y e. R ) /\ v = ( x +h y ) ) -> ( ( x e. ~H /\ y e. ~H ) /\ v e. ~H ) )
13	2	cheli	|- ( z e. C -> z e. ~H )
14	4	cheli	|- ( w e. S -> w e. ~H )
15	13 14	anim12i	|- ( ( z e. C /\ w e. S ) -> ( z e. ~H /\ w e. ~H ) )
16	15	adantr	|- ( ( ( z e. C /\ w e. S ) /\ v = ( z +h w ) ) -> ( z e. ~H /\ w e. ~H ) )
17	12 16	anim12i	|- ( ( ( ( x e. B /\ y e. R ) /\ v = ( x +h y ) ) /\ ( ( z e. C /\ w e. S ) /\ v = ( z +h w ) ) ) -> ( ( ( x e. ~H /\ y e. ~H ) /\ v e. ~H ) /\ ( z e. ~H /\ w e. ~H ) ) )