Theorem 5oalem4

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

	Ref	Expression
Hypotheses	5oalem3.1	⊢ 𝐴 ∈ Sℋ
	5oalem3.2	⊢ 𝐵 ∈ Sℋ
	5oalem3.3	⊢ 𝐶 ∈ Sℋ
	5oalem3.4	⊢ 𝐷 ∈ Sℋ
	5oalem3.5	⊢ 𝐹 ∈ Sℋ
	5oalem3.6	⊢ 𝐺 ∈ Sℋ
Assertion	5oalem4	⊢ ( ( ( ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ∧ ( 𝑧 ∈ 𝐶 ∧ 𝑤 ∈ 𝐷 ) ) ∧ ( 𝑓 ∈ 𝐹 ∧ 𝑔 ∈ 𝐺 ) ) ∧ ( ( 𝑥 +ℎ 𝑦 ) = ( 𝑓 +ℎ 𝑔 ) ∧ ( 𝑧 +ℎ 𝑤 ) = ( 𝑓 +ℎ 𝑔 ) ) ) → ( 𝑥 −ℎ 𝑧 ) ∈ ( ( ( 𝐴 +ℋ 𝐶 ) ∩ ( 𝐵 +ℋ 𝐷 ) ) ∩ ( ( ( 𝐴 +ℋ 𝐹 ) ∩ ( 𝐵 +ℋ 𝐺 ) ) +ℋ ( ( 𝐶 +ℋ 𝐹 ) ∩ ( 𝐷 +ℋ 𝐺 ) ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		5oalem3.1	⊢ 𝐴 ∈ Sℋ
2		5oalem3.2	⊢ 𝐵 ∈ Sℋ
3		5oalem3.3	⊢ 𝐶 ∈ Sℋ
4		5oalem3.4	⊢ 𝐷 ∈ Sℋ
5		5oalem3.5	⊢ 𝐹 ∈ Sℋ
6		5oalem3.6	⊢ 𝐺 ∈ Sℋ
7		eqtr3	⊢ ( ( ( 𝑥 +ℎ 𝑦 ) = ( 𝑓 +ℎ 𝑔 ) ∧ ( 𝑧 +ℎ 𝑤 ) = ( 𝑓 +ℎ 𝑔 ) ) → ( 𝑥 +ℎ 𝑦 ) = ( 𝑧 +ℎ 𝑤 ) )
8	1 2 3 4	5oalem2	⊢ ( ( ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ∧ ( 𝑧 ∈ 𝐶 ∧ 𝑤 ∈ 𝐷 ) ) ∧ ( 𝑥 +ℎ 𝑦 ) = ( 𝑧 +ℎ 𝑤 ) ) → ( 𝑥 −ℎ 𝑧 ) ∈ ( ( 𝐴 +ℋ 𝐶 ) ∩ ( 𝐵 +ℋ 𝐷 ) ) )
9	7 8	sylan2	⊢ ( ( ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ∧ ( 𝑧 ∈ 𝐶 ∧ 𝑤 ∈ 𝐷 ) ) ∧ ( ( 𝑥 +ℎ 𝑦 ) = ( 𝑓 +ℎ 𝑔 ) ∧ ( 𝑧 +ℎ 𝑤 ) = ( 𝑓 +ℎ 𝑔 ) ) ) → ( 𝑥 −ℎ 𝑧 ) ∈ ( ( 𝐴 +ℋ 𝐶 ) ∩ ( 𝐵 +ℋ 𝐷 ) ) )
10	9	adantlr	⊢ ( ( ( ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ∧ ( 𝑧 ∈ 𝐶 ∧ 𝑤 ∈ 𝐷 ) ) ∧ ( 𝑓 ∈ 𝐹 ∧ 𝑔 ∈ 𝐺 ) ) ∧ ( ( 𝑥 +ℎ 𝑦 ) = ( 𝑓 +ℎ 𝑔 ) ∧ ( 𝑧 +ℎ 𝑤 ) = ( 𝑓 +ℎ 𝑔 ) ) ) → ( 𝑥 −ℎ 𝑧 ) ∈ ( ( 𝐴 +ℋ 𝐶 ) ∩ ( 𝐵 +ℋ 𝐷 ) ) )
11	1 2 3 4 5 6	5oalem3	⊢ ( ( ( ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ∧ ( 𝑧 ∈ 𝐶 ∧ 𝑤 ∈ 𝐷 ) ) ∧ ( 𝑓 ∈ 𝐹 ∧ 𝑔 ∈ 𝐺 ) ) ∧ ( ( 𝑥 +ℎ 𝑦 ) = ( 𝑓 +ℎ 𝑔 ) ∧ ( 𝑧 +ℎ 𝑤 ) = ( 𝑓 +ℎ 𝑔 ) ) ) → ( 𝑥 −ℎ 𝑧 ) ∈ ( ( ( 𝐴 +ℋ 𝐹 ) ∩ ( 𝐵 +ℋ 𝐺 ) ) +ℋ ( ( 𝐶 +ℋ 𝐹 ) ∩ ( 𝐷 +ℋ 𝐺 ) ) ) )
12	10 11	elind	⊢ ( ( ( ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ∧ ( 𝑧 ∈ 𝐶 ∧ 𝑤 ∈ 𝐷 ) ) ∧ ( 𝑓 ∈ 𝐹 ∧ 𝑔 ∈ 𝐺 ) ) ∧ ( ( 𝑥 +ℎ 𝑦 ) = ( 𝑓 +ℎ 𝑔 ) ∧ ( 𝑧 +ℎ 𝑤 ) = ( 𝑓 +ℎ 𝑔 ) ) ) → ( 𝑥 −ℎ 𝑧 ) ∈ ( ( ( 𝐴 +ℋ 𝐶 ) ∩ ( 𝐵 +ℋ 𝐷 ) ) ∩ ( ( ( 𝐴 +ℋ 𝐹 ) ∩ ( 𝐵 +ℋ 𝐺 ) ) +ℋ ( ( 𝐶 +ℋ 𝐹 ) ∩ ( 𝐷 +ℋ 𝐺 ) ) ) ) )