Theorem 3oalem1

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

	Ref	Expression
Hypotheses	3oalem1.1	⊢ 𝐵 ∈ Cℋ
	3oalem1.2	⊢ 𝐶 ∈ Cℋ
	3oalem1.3	⊢ 𝑅 ∈ Cℋ
	3oalem1.4	⊢ 𝑆 ∈ Cℋ
Assertion	3oalem1	⊢ ( ( ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝑅 ) ∧ 𝑣 = ( 𝑥 +ℎ 𝑦 ) ) ∧ ( ( 𝑧 ∈ 𝐶 ∧ 𝑤 ∈ 𝑆 ) ∧ 𝑣 = ( 𝑧 +ℎ 𝑤 ) ) ) → ( ( ( 𝑥 ∈ ℋ ∧ 𝑦 ∈ ℋ ) ∧ 𝑣 ∈ ℋ ) ∧ ( 𝑧 ∈ ℋ ∧ 𝑤 ∈ ℋ ) ) )

Proof

Step	Hyp	Ref	Expression
1		3oalem1.1	⊢ 𝐵 ∈ Cℋ
2		3oalem1.2	⊢ 𝐶 ∈ Cℋ
3		3oalem1.3	⊢ 𝑅 ∈ Cℋ
4		3oalem1.4	⊢ 𝑆 ∈ Cℋ
5	1	cheli	⊢ ( 𝑥 ∈ 𝐵 → 𝑥 ∈ ℋ )
6	3	cheli	⊢ ( 𝑦 ∈ 𝑅 → 𝑦 ∈ ℋ )
7	5 6	anim12i	⊢ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝑅 ) → ( 𝑥 ∈ ℋ ∧ 𝑦 ∈ ℋ ) )
8		hvaddcl	⊢ ( ( 𝑥 ∈ ℋ ∧ 𝑦 ∈ ℋ ) → ( 𝑥 +ℎ 𝑦 ) ∈ ℋ )
9		eleq1	⊢ ( 𝑣 = ( 𝑥 +ℎ 𝑦 ) → ( 𝑣 ∈ ℋ ↔ ( 𝑥 +ℎ 𝑦 ) ∈ ℋ ) )
10	8 9	syl5ibrcom	⊢ ( ( 𝑥 ∈ ℋ ∧ 𝑦 ∈ ℋ ) → ( 𝑣 = ( 𝑥 +ℎ 𝑦 ) → 𝑣 ∈ ℋ ) )
11	10	imdistani	⊢ ( ( ( 𝑥 ∈ ℋ ∧ 𝑦 ∈ ℋ ) ∧ 𝑣 = ( 𝑥 +ℎ 𝑦 ) ) → ( ( 𝑥 ∈ ℋ ∧ 𝑦 ∈ ℋ ) ∧ 𝑣 ∈ ℋ ) )
12	7 11	sylan	⊢ ( ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝑅 ) ∧ 𝑣 = ( 𝑥 +ℎ 𝑦 ) ) → ( ( 𝑥 ∈ ℋ ∧ 𝑦 ∈ ℋ ) ∧ 𝑣 ∈ ℋ ) )
13	2	cheli	⊢ ( 𝑧 ∈ 𝐶 → 𝑧 ∈ ℋ )
14	4	cheli	⊢ ( 𝑤 ∈ 𝑆 → 𝑤 ∈ ℋ )
15	13 14	anim12i	⊢ ( ( 𝑧 ∈ 𝐶 ∧ 𝑤 ∈ 𝑆 ) → ( 𝑧 ∈ ℋ ∧ 𝑤 ∈ ℋ ) )
16	15	adantr	⊢ ( ( ( 𝑧 ∈ 𝐶 ∧ 𝑤 ∈ 𝑆 ) ∧ 𝑣 = ( 𝑧 +ℎ 𝑤 ) ) → ( 𝑧 ∈ ℋ ∧ 𝑤 ∈ ℋ ) )
17	12 16	anim12i	⊢ ( ( ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝑅 ) ∧ 𝑣 = ( 𝑥 +ℎ 𝑦 ) ) ∧ ( ( 𝑧 ∈ 𝐶 ∧ 𝑤 ∈ 𝑆 ) ∧ 𝑣 = ( 𝑧 +ℎ 𝑤 ) ) ) → ( ( ( 𝑥 ∈ ℋ ∧ 𝑦 ∈ ℋ ) ∧ 𝑣 ∈ ℋ ) ∧ ( 𝑧 ∈ ℋ ∧ 𝑤 ∈ ℋ ) ) )