Theorem 5oalem1

Description: Lemma for orthoarguesian law 5OA. (Contributed by NM, 1-Apr-2000) (New usage is discouraged.)

	Ref	Expression
Hypotheses	5oalem1.1	⊢ 𝐴 ∈ Sℋ
	5oalem1.2	⊢ 𝐵 ∈ Sℋ
	5oalem1.3	⊢ 𝐶 ∈ Sℋ
	5oalem1.4	⊢ 𝑅 ∈ Sℋ
Assertion	5oalem1	⊢ ( ( ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑣 = ( 𝑥 +ℎ 𝑦 ) ) ∧ ( 𝑧 ∈ 𝐶 ∧ ( 𝑥 −ℎ 𝑧 ) ∈ 𝑅 ) ) → 𝑣 ∈ ( 𝐵 +ℋ ( 𝐴 ∩ ( 𝐶 +ℋ 𝑅 ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		5oalem1.1	⊢ 𝐴 ∈ Sℋ
2		5oalem1.2	⊢ 𝐵 ∈ Sℋ
3		5oalem1.3	⊢ 𝐶 ∈ Sℋ
4		5oalem1.4	⊢ 𝑅 ∈ Sℋ
5		simplll	⊢ ( ( ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑣 = ( 𝑥 +ℎ 𝑦 ) ) ∧ ( 𝑧 ∈ 𝐶 ∧ ( 𝑥 −ℎ 𝑧 ) ∈ 𝑅 ) ) → 𝑥 ∈ 𝐴 )
6	1	sheli	⊢ ( 𝑥 ∈ 𝐴 → 𝑥 ∈ ℋ )
7	6	ad2antrr	⊢ ( ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑣 = ( 𝑥 +ℎ 𝑦 ) ) → 𝑥 ∈ ℋ )
8	3	sheli	⊢ ( 𝑧 ∈ 𝐶 → 𝑧 ∈ ℋ )
9	8	adantr	⊢ ( ( 𝑧 ∈ 𝐶 ∧ ( 𝑥 −ℎ 𝑧 ) ∈ 𝑅 ) → 𝑧 ∈ ℋ )
10		hvaddsub12	⊢ ( ( 𝑥 ∈ ℋ ∧ 𝑧 ∈ ℋ ∧ 𝑧 ∈ ℋ ) → ( 𝑥 +ℎ ( 𝑧 −ℎ 𝑧 ) ) = ( 𝑧 +ℎ ( 𝑥 −ℎ 𝑧 ) ) )
11	10	3anidm23	⊢ ( ( 𝑥 ∈ ℋ ∧ 𝑧 ∈ ℋ ) → ( 𝑥 +ℎ ( 𝑧 −ℎ 𝑧 ) ) = ( 𝑧 +ℎ ( 𝑥 −ℎ 𝑧 ) ) )
12		hvsubid	⊢ ( 𝑧 ∈ ℋ → ( 𝑧 −ℎ 𝑧 ) = 0ℎ )
13	12	oveq2d	⊢ ( 𝑧 ∈ ℋ → ( 𝑥 +ℎ ( 𝑧 −ℎ 𝑧 ) ) = ( 𝑥 +ℎ 0ℎ ) )
14		ax-hvaddid	⊢ ( 𝑥 ∈ ℋ → ( 𝑥 +ℎ 0ℎ ) = 𝑥 )
15	13 14	sylan9eqr	⊢ ( ( 𝑥 ∈ ℋ ∧ 𝑧 ∈ ℋ ) → ( 𝑥 +ℎ ( 𝑧 −ℎ 𝑧 ) ) = 𝑥 )
16	11 15	eqtr3d	⊢ ( ( 𝑥 ∈ ℋ ∧ 𝑧 ∈ ℋ ) → ( 𝑧 +ℎ ( 𝑥 −ℎ 𝑧 ) ) = 𝑥 )
17	7 9 16	syl2an	⊢ ( ( ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑣 = ( 𝑥 +ℎ 𝑦 ) ) ∧ ( 𝑧 ∈ 𝐶 ∧ ( 𝑥 −ℎ 𝑧 ) ∈ 𝑅 ) ) → ( 𝑧 +ℎ ( 𝑥 −ℎ 𝑧 ) ) = 𝑥 )
18	3 4	shsvai	⊢ ( ( 𝑧 ∈ 𝐶 ∧ ( 𝑥 −ℎ 𝑧 ) ∈ 𝑅 ) → ( 𝑧 +ℎ ( 𝑥 −ℎ 𝑧 ) ) ∈ ( 𝐶 +ℋ 𝑅 ) )
19	18	adantl	⊢ ( ( ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑣 = ( 𝑥 +ℎ 𝑦 ) ) ∧ ( 𝑧 ∈ 𝐶 ∧ ( 𝑥 −ℎ 𝑧 ) ∈ 𝑅 ) ) → ( 𝑧 +ℎ ( 𝑥 −ℎ 𝑧 ) ) ∈ ( 𝐶 +ℋ 𝑅 ) )
20	17 19	eqeltrrd	⊢ ( ( ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑣 = ( 𝑥 +ℎ 𝑦 ) ) ∧ ( 𝑧 ∈ 𝐶 ∧ ( 𝑥 −ℎ 𝑧 ) ∈ 𝑅 ) ) → 𝑥 ∈ ( 𝐶 +ℋ 𝑅 ) )
21	5 20	elind	⊢ ( ( ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑣 = ( 𝑥 +ℎ 𝑦 ) ) ∧ ( 𝑧 ∈ 𝐶 ∧ ( 𝑥 −ℎ 𝑧 ) ∈ 𝑅 ) ) → 𝑥 ∈ ( 𝐴 ∩ ( 𝐶 +ℋ 𝑅 ) ) )
22		simpllr	⊢ ( ( ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑣 = ( 𝑥 +ℎ 𝑦 ) ) ∧ ( 𝑧 ∈ 𝐶 ∧ ( 𝑥 −ℎ 𝑧 ) ∈ 𝑅 ) ) → 𝑦 ∈ 𝐵 )
23	3 4	shscli	⊢ ( 𝐶 +ℋ 𝑅 ) ∈ Sℋ
24	1 23	shincli	⊢ ( 𝐴 ∩ ( 𝐶 +ℋ 𝑅 ) ) ∈ Sℋ
25	24 2	shsvai	⊢ ( ( 𝑥 ∈ ( 𝐴 ∩ ( 𝐶 +ℋ 𝑅 ) ) ∧ 𝑦 ∈ 𝐵 ) → ( 𝑥 +ℎ 𝑦 ) ∈ ( ( 𝐴 ∩ ( 𝐶 +ℋ 𝑅 ) ) +ℋ 𝐵 ) )
26	24 2	shscomi	⊢ ( ( 𝐴 ∩ ( 𝐶 +ℋ 𝑅 ) ) +ℋ 𝐵 ) = ( 𝐵 +ℋ ( 𝐴 ∩ ( 𝐶 +ℋ 𝑅 ) ) )
27	25 26	eleqtrdi	⊢ ( ( 𝑥 ∈ ( 𝐴 ∩ ( 𝐶 +ℋ 𝑅 ) ) ∧ 𝑦 ∈ 𝐵 ) → ( 𝑥 +ℎ 𝑦 ) ∈ ( 𝐵 +ℋ ( 𝐴 ∩ ( 𝐶 +ℋ 𝑅 ) ) ) )
28	21 22 27	syl2anc	⊢ ( ( ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑣 = ( 𝑥 +ℎ 𝑦 ) ) ∧ ( 𝑧 ∈ 𝐶 ∧ ( 𝑥 −ℎ 𝑧 ) ∈ 𝑅 ) ) → ( 𝑥 +ℎ 𝑦 ) ∈ ( 𝐵 +ℋ ( 𝐴 ∩ ( 𝐶 +ℋ 𝑅 ) ) ) )
29		eleq1	⊢ ( 𝑣 = ( 𝑥 +ℎ 𝑦 ) → ( 𝑣 ∈ ( 𝐵 +ℋ ( 𝐴 ∩ ( 𝐶 +ℋ 𝑅 ) ) ) ↔ ( 𝑥 +ℎ 𝑦 ) ∈ ( 𝐵 +ℋ ( 𝐴 ∩ ( 𝐶 +ℋ 𝑅 ) ) ) ) )
30	29	ad2antlr	⊢ ( ( ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑣 = ( 𝑥 +ℎ 𝑦 ) ) ∧ ( 𝑧 ∈ 𝐶 ∧ ( 𝑥 −ℎ 𝑧 ) ∈ 𝑅 ) ) → ( 𝑣 ∈ ( 𝐵 +ℋ ( 𝐴 ∩ ( 𝐶 +ℋ 𝑅 ) ) ) ↔ ( 𝑥 +ℎ 𝑦 ) ∈ ( 𝐵 +ℋ ( 𝐴 ∩ ( 𝐶 +ℋ 𝑅 ) ) ) ) )
31	28 30	mpbird	⊢ ( ( ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑣 = ( 𝑥 +ℎ 𝑦 ) ) ∧ ( 𝑧 ∈ 𝐶 ∧ ( 𝑥 −ℎ 𝑧 ) ∈ 𝑅 ) ) → 𝑣 ∈ ( 𝐵 +ℋ ( 𝐴 ∩ ( 𝐶 +ℋ 𝑅 ) ) ) )