Metamath Proof Explorer

Theorem 5oalem2

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

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

Proof

Step Hyp Ref Expression
1 5oalem2.1 ⊢ 𝐴 ∈ Sℋ
2 5oalem2.2 ⊢ 𝐵 ∈ Sℋ
3 5oalem2.3 ⊢ 𝐶 ∈ Sℋ
4 5oalem2.4 ⊢ 𝐷 ∈ Sℋ
5 1 3 shsvsi ⊢ ( ( 𝑥 ∈ 𝐴 ∧ 𝑧 ∈ 𝐶 ) → ( 𝑥 −ℎ 𝑧 ) ∈ ( 𝐴 +ℋ 𝐶 ) )
6 5 ad2ant2r ⊢ ( ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ∧ ( 𝑧 ∈ 𝐶 ∧ 𝑤 ∈ 𝐷 ) ) → ( 𝑥 −ℎ 𝑧 ) ∈ ( 𝐴 +ℋ 𝐶 ) )
7 6 adantr ⊢ ( ( ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ∧ ( 𝑧 ∈ 𝐶 ∧ 𝑤 ∈ 𝐷 ) ) ∧ ( 𝑥 +ℎ 𝑦 ) = ( 𝑧 +ℎ 𝑤 ) ) → ( 𝑥 −ℎ 𝑧 ) ∈ ( 𝐴 +ℋ 𝐶 ) )
8 4 2 shsvsi ⊢ ( ( 𝑤 ∈ 𝐷 ∧ 𝑦 ∈ 𝐵 ) → ( 𝑤 −ℎ 𝑦 ) ∈ ( 𝐷 +ℋ 𝐵 ) )
9 8 ancoms ⊢ ( ( 𝑦 ∈ 𝐵 ∧ 𝑤 ∈ 𝐷 ) → ( 𝑤 −ℎ 𝑦 ) ∈ ( 𝐷 +ℋ 𝐵 ) )
10 2 4 shscomi ⊢ ( 𝐵 +ℋ 𝐷 ) = ( 𝐷 +ℋ 𝐵 )
11 9 10 eleqtrrdi ⊢ ( ( 𝑦 ∈ 𝐵 ∧ 𝑤 ∈ 𝐷 ) → ( 𝑤 −ℎ 𝑦 ) ∈ ( 𝐵 +ℋ 𝐷 ) )
12 11 ad2ant2l ⊢ ( ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ∧ ( 𝑧 ∈ 𝐶 ∧ 𝑤 ∈ 𝐷 ) ) → ( 𝑤 −ℎ 𝑦 ) ∈ ( 𝐵 +ℋ 𝐷 ) )
13 12 adantr ⊢ ( ( ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ∧ ( 𝑧 ∈ 𝐶 ∧ 𝑤 ∈ 𝐷 ) ) ∧ ( 𝑥 +ℎ 𝑦 ) = ( 𝑧 +ℎ 𝑤 ) ) → ( 𝑤 −ℎ 𝑦 ) ∈ ( 𝐵 +ℋ 𝐷 ) )
14 1 sheli ⊢ ( 𝑥 ∈ 𝐴 → 𝑥 ∈ ℋ )
15 2 sheli ⊢ ( 𝑦 ∈ 𝐵 → 𝑦 ∈ ℋ )
16 14 15 anim12i ⊢ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) → ( 𝑥 ∈ ℋ ∧ 𝑦 ∈ ℋ ) )
17 3 sheli ⊢ ( 𝑧 ∈ 𝐶 → 𝑧 ∈ ℋ )
18 4 sheli ⊢ ( 𝑤 ∈ 𝐷 → 𝑤 ∈ ℋ )
19 17 18 anim12i ⊢ ( ( 𝑧 ∈ 𝐶 ∧ 𝑤 ∈ 𝐷 ) → ( 𝑧 ∈ ℋ ∧ 𝑤 ∈ ℋ ) )
20 16 19 anim12i ⊢ ( ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ∧ ( 𝑧 ∈ 𝐶 ∧ 𝑤 ∈ 𝐷 ) ) → ( ( 𝑥 ∈ ℋ ∧ 𝑦 ∈ ℋ ) ∧ ( 𝑧 ∈ ℋ ∧ 𝑤 ∈ ℋ ) ) )
21 oveq1 ⊢ ( ( 𝑥 +ℎ 𝑦 ) = ( 𝑧 +ℎ 𝑤 ) → ( ( 𝑥 +ℎ 𝑦 ) −ℎ ( 𝑧 +ℎ 𝑦 ) ) = ( ( 𝑧 +ℎ 𝑤 ) −ℎ ( 𝑧 +ℎ 𝑦 ) ) )
22 21 adantl ⊢ ( ( ( ( 𝑥 ∈ ℋ ∧ 𝑦 ∈ ℋ ) ∧ ( 𝑧 ∈ ℋ ∧ 𝑤 ∈ ℋ ) ) ∧ ( 𝑥 +ℎ 𝑦 ) = ( 𝑧 +ℎ 𝑤 ) ) → ( ( 𝑥 +ℎ 𝑦 ) −ℎ ( 𝑧 +ℎ 𝑦 ) ) = ( ( 𝑧 +ℎ 𝑤 ) −ℎ ( 𝑧 +ℎ 𝑦 ) ) )
23 simpr ⊢ ( ( 𝑥 ∈ ℋ ∧ 𝑦 ∈ ℋ ) → 𝑦 ∈ ℋ )
24 23 anim2i ⊢ ( ( 𝑧 ∈ ℋ ∧ ( 𝑥 ∈ ℋ ∧ 𝑦 ∈ ℋ ) ) → ( 𝑧 ∈ ℋ ∧ 𝑦 ∈ ℋ ) )
25 24 ancoms ⊢ ( ( ( 𝑥 ∈ ℋ ∧ 𝑦 ∈ ℋ ) ∧ 𝑧 ∈ ℋ ) → ( 𝑧 ∈ ℋ ∧ 𝑦 ∈ ℋ ) )
26 hvsub4 ⊢ ( ( ( 𝑥 ∈ ℋ ∧ 𝑦 ∈ ℋ ) ∧ ( 𝑧 ∈ ℋ ∧ 𝑦 ∈ ℋ ) ) → ( ( 𝑥 +ℎ 𝑦 ) −ℎ ( 𝑧 +ℎ 𝑦 ) ) = ( ( 𝑥 −ℎ 𝑧 ) +ℎ ( 𝑦 −ℎ 𝑦 ) ) )
27 25 26 syldan ⊢ ( ( ( 𝑥 ∈ ℋ ∧ 𝑦 ∈ ℋ ) ∧ 𝑧 ∈ ℋ ) → ( ( 𝑥 +ℎ 𝑦 ) −ℎ ( 𝑧 +ℎ 𝑦 ) ) = ( ( 𝑥 −ℎ 𝑧 ) +ℎ ( 𝑦 −ℎ 𝑦 ) ) )
28 hvsubid ⊢ ( 𝑦 ∈ ℋ → ( 𝑦 −ℎ 𝑦 ) = 0ℎ )
29 28 oveq2d ⊢ ( 𝑦 ∈ ℋ → ( ( 𝑥 −ℎ 𝑧 ) +ℎ ( 𝑦 −ℎ 𝑦 ) ) = ( ( 𝑥 −ℎ 𝑧 ) +ℎ 0ℎ ) )
30 29 ad2antlr ⊢ ( ( ( 𝑥 ∈ ℋ ∧ 𝑦 ∈ ℋ ) ∧ 𝑧 ∈ ℋ ) → ( ( 𝑥 −ℎ 𝑧 ) +ℎ ( 𝑦 −ℎ 𝑦 ) ) = ( ( 𝑥 −ℎ 𝑧 ) +ℎ 0ℎ ) )
31 hvsubcl ⊢ ( ( 𝑥 ∈ ℋ ∧ 𝑧 ∈ ℋ ) → ( 𝑥 −ℎ 𝑧 ) ∈ ℋ )
32 ax-hvaddid ⊢ ( ( 𝑥 −ℎ 𝑧 ) ∈ ℋ → ( ( 𝑥 −ℎ 𝑧 ) +ℎ 0ℎ ) = ( 𝑥 −ℎ 𝑧 ) )
33 31 32 syl ⊢ ( ( 𝑥 ∈ ℋ ∧ 𝑧 ∈ ℋ ) → ( ( 𝑥 −ℎ 𝑧 ) +ℎ 0ℎ ) = ( 𝑥 −ℎ 𝑧 ) )
34 33 adantlr ⊢ ( ( ( 𝑥 ∈ ℋ ∧ 𝑦 ∈ ℋ ) ∧ 𝑧 ∈ ℋ ) → ( ( 𝑥 −ℎ 𝑧 ) +ℎ 0ℎ ) = ( 𝑥 −ℎ 𝑧 ) )
35 27 30 34 3eqtrd ⊢ ( ( ( 𝑥 ∈ ℋ ∧ 𝑦 ∈ ℋ ) ∧ 𝑧 ∈ ℋ ) → ( ( 𝑥 +ℎ 𝑦 ) −ℎ ( 𝑧 +ℎ 𝑦 ) ) = ( 𝑥 −ℎ 𝑧 ) )
36 35 adantrr ⊢ ( ( ( 𝑥 ∈ ℋ ∧ 𝑦 ∈ ℋ ) ∧ ( 𝑧 ∈ ℋ ∧ 𝑤 ∈ ℋ ) ) → ( ( 𝑥 +ℎ 𝑦 ) −ℎ ( 𝑧 +ℎ 𝑦 ) ) = ( 𝑥 −ℎ 𝑧 ) )
37 36 adantr ⊢ ( ( ( ( 𝑥 ∈ ℋ ∧ 𝑦 ∈ ℋ ) ∧ ( 𝑧 ∈ ℋ ∧ 𝑤 ∈ ℋ ) ) ∧ ( 𝑥 +ℎ 𝑦 ) = ( 𝑧 +ℎ 𝑤 ) ) → ( ( 𝑥 +ℎ 𝑦 ) −ℎ ( 𝑧 +ℎ 𝑦 ) ) = ( 𝑥 −ℎ 𝑧 ) )
38 simpr ⊢ ( ( 𝑦 ∈ ℋ ∧ ( 𝑧 ∈ ℋ ∧ 𝑤 ∈ ℋ ) ) → ( 𝑧 ∈ ℋ ∧ 𝑤 ∈ ℋ ) )
39 simpl ⊢ ( ( 𝑧 ∈ ℋ ∧ 𝑤 ∈ ℋ ) → 𝑧 ∈ ℋ )
40 39 anim1i ⊢ ( ( ( 𝑧 ∈ ℋ ∧ 𝑤 ∈ ℋ ) ∧ 𝑦 ∈ ℋ ) → ( 𝑧 ∈ ℋ ∧ 𝑦 ∈ ℋ ) )
41 40 ancoms ⊢ ( ( 𝑦 ∈ ℋ ∧ ( 𝑧 ∈ ℋ ∧ 𝑤 ∈ ℋ ) ) → ( 𝑧 ∈ ℋ ∧ 𝑦 ∈ ℋ ) )
42 hvsub4 ⊢ ( ( ( 𝑧 ∈ ℋ ∧ 𝑤 ∈ ℋ ) ∧ ( 𝑧 ∈ ℋ ∧ 𝑦 ∈ ℋ ) ) → ( ( 𝑧 +ℎ 𝑤 ) −ℎ ( 𝑧 +ℎ 𝑦 ) ) = ( ( 𝑧 −ℎ 𝑧 ) +ℎ ( 𝑤 −ℎ 𝑦 ) ) )
43 38 41 42 syl2anc ⊢ ( ( 𝑦 ∈ ℋ ∧ ( 𝑧 ∈ ℋ ∧ 𝑤 ∈ ℋ ) ) → ( ( 𝑧 +ℎ 𝑤 ) −ℎ ( 𝑧 +ℎ 𝑦 ) ) = ( ( 𝑧 −ℎ 𝑧 ) +ℎ ( 𝑤 −ℎ 𝑦 ) ) )
44 hvsubid ⊢ ( 𝑧 ∈ ℋ → ( 𝑧 −ℎ 𝑧 ) = 0ℎ )
45 44 oveq1d ⊢ ( 𝑧 ∈ ℋ → ( ( 𝑧 −ℎ 𝑧 ) +ℎ ( 𝑤 −ℎ 𝑦 ) ) = ( 0ℎ +ℎ ( 𝑤 −ℎ 𝑦 ) ) )
46 45 ad2antrl ⊢ ( ( 𝑦 ∈ ℋ ∧ ( 𝑧 ∈ ℋ ∧ 𝑤 ∈ ℋ ) ) → ( ( 𝑧 −ℎ 𝑧 ) +ℎ ( 𝑤 −ℎ 𝑦 ) ) = ( 0ℎ +ℎ ( 𝑤 −ℎ 𝑦 ) ) )
47 hvsubcl ⊢ ( ( 𝑤 ∈ ℋ ∧ 𝑦 ∈ ℋ ) → ( 𝑤 −ℎ 𝑦 ) ∈ ℋ )
48 hvaddid2 ⊢ ( ( 𝑤 −ℎ 𝑦 ) ∈ ℋ → ( 0ℎ +ℎ ( 𝑤 −ℎ 𝑦 ) ) = ( 𝑤 −ℎ 𝑦 ) )
49 47 48 syl ⊢ ( ( 𝑤 ∈ ℋ ∧ 𝑦 ∈ ℋ ) → ( 0ℎ +ℎ ( 𝑤 −ℎ 𝑦 ) ) = ( 𝑤 −ℎ 𝑦 ) )
50 49 ancoms ⊢ ( ( 𝑦 ∈ ℋ ∧ 𝑤 ∈ ℋ ) → ( 0ℎ +ℎ ( 𝑤 −ℎ 𝑦 ) ) = ( 𝑤 −ℎ 𝑦 ) )
51 50 adantrl ⊢ ( ( 𝑦 ∈ ℋ ∧ ( 𝑧 ∈ ℋ ∧ 𝑤 ∈ ℋ ) ) → ( 0ℎ +ℎ ( 𝑤 −ℎ 𝑦 ) ) = ( 𝑤 −ℎ 𝑦 ) )
52 43 46 51 3eqtrd ⊢ ( ( 𝑦 ∈ ℋ ∧ ( 𝑧 ∈ ℋ ∧ 𝑤 ∈ ℋ ) ) → ( ( 𝑧 +ℎ 𝑤 ) −ℎ ( 𝑧 +ℎ 𝑦 ) ) = ( 𝑤 −ℎ 𝑦 ) )
53 52 adantll ⊢ ( ( ( 𝑥 ∈ ℋ ∧ 𝑦 ∈ ℋ ) ∧ ( 𝑧 ∈ ℋ ∧ 𝑤 ∈ ℋ ) ) → ( ( 𝑧 +ℎ 𝑤 ) −ℎ ( 𝑧 +ℎ 𝑦 ) ) = ( 𝑤 −ℎ 𝑦 ) )
54 53 adantr ⊢ ( ( ( ( 𝑥 ∈ ℋ ∧ 𝑦 ∈ ℋ ) ∧ ( 𝑧 ∈ ℋ ∧ 𝑤 ∈ ℋ ) ) ∧ ( 𝑥 +ℎ 𝑦 ) = ( 𝑧 +ℎ 𝑤 ) ) → ( ( 𝑧 +ℎ 𝑤 ) −ℎ ( 𝑧 +ℎ 𝑦 ) ) = ( 𝑤 −ℎ 𝑦 ) )
55 22 37 54 3eqtr3d ⊢ ( ( ( ( 𝑥 ∈ ℋ ∧ 𝑦 ∈ ℋ ) ∧ ( 𝑧 ∈ ℋ ∧ 𝑤 ∈ ℋ ) ) ∧ ( 𝑥 +ℎ 𝑦 ) = ( 𝑧 +ℎ 𝑤 ) ) → ( 𝑥 −ℎ 𝑧 ) = ( 𝑤 −ℎ 𝑦 ) )
56 55 eleq1d ⊢ ( ( ( ( 𝑥 ∈ ℋ ∧ 𝑦 ∈ ℋ ) ∧ ( 𝑧 ∈ ℋ ∧ 𝑤 ∈ ℋ ) ) ∧ ( 𝑥 +ℎ 𝑦 ) = ( 𝑧 +ℎ 𝑤 ) ) → ( ( 𝑥 −ℎ 𝑧 ) ∈ ( 𝐵 +ℋ 𝐷 ) ↔ ( 𝑤 −ℎ 𝑦 ) ∈ ( 𝐵 +ℋ 𝐷 ) ) )
57 20 56 sylan ⊢ ( ( ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ∧ ( 𝑧 ∈ 𝐶 ∧ 𝑤 ∈ 𝐷 ) ) ∧ ( 𝑥 +ℎ 𝑦 ) = ( 𝑧 +ℎ 𝑤 ) ) → ( ( 𝑥 −ℎ 𝑧 ) ∈ ( 𝐵 +ℋ 𝐷 ) ↔ ( 𝑤 −ℎ 𝑦 ) ∈ ( 𝐵 +ℋ 𝐷 ) ) )
58 13 57 mpbird ⊢ ( ( ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ∧ ( 𝑧 ∈ 𝐶 ∧ 𝑤 ∈ 𝐷 ) ) ∧ ( 𝑥 +ℎ 𝑦 ) = ( 𝑧 +ℎ 𝑤 ) ) → ( 𝑥 −ℎ 𝑧 ) ∈ ( 𝐵 +ℋ 𝐷 ) )
59 7 58 elind ⊢ ( ( ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ∧ ( 𝑧 ∈ 𝐶 ∧ 𝑤 ∈ 𝐷 ) ) ∧ ( 𝑥 +ℎ 𝑦 ) = ( 𝑧 +ℎ 𝑤 ) ) → ( 𝑥 −ℎ 𝑧 ) ∈ ( ( 𝐴 +ℋ 𝐶 ) ∩ ( 𝐵 +ℋ 𝐷 ) ) )