Metamath Proof Explorer


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 ( ( ( ( 𝑥𝐵𝑦𝑅 ) ∧ 𝑣 = ( 𝑥 + 𝑦 ) ) ∧ ( ( 𝑧𝐶𝑤𝑆 ) ∧ 𝑣 = ( 𝑧 + 𝑤 ) ) ) → ( ( ( 𝑥 ∈ ℋ ∧ 𝑦 ∈ ℋ ) ∧ 𝑣 ∈ ℋ ) ∧ ( 𝑧 ∈ ℋ ∧ 𝑤 ∈ ℋ ) ) )