Theorem 5oalem3

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	5oalem3	⊢ ( ( ( ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ∧ ( 𝑧 ∈ 𝐶 ∧ 𝑤 ∈ 𝐷 ) ) ∧ ( 𝑓 ∈ 𝐹 ∧ 𝑔 ∈ 𝐺 ) ) ∧ ( ( 𝑥 +ℎ 𝑦 ) = ( 𝑓 +ℎ 𝑔 ) ∧ ( 𝑧 +ℎ 𝑤 ) = ( 𝑓 +ℎ 𝑔 ) ) ) → ( 𝑥 −ℎ 𝑧 ) ∈ ( ( ( 𝐴 +ℋ 𝐹 ) ∩ ( 𝐵 +ℋ 𝐺 ) ) +ℋ ( ( 𝐶 +ℋ 𝐹 ) ∩ ( 𝐷 +ℋ 𝐺 ) ) ) )

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		anandir	⊢ ( ( ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ∧ ( 𝑧 ∈ 𝐶 ∧ 𝑤 ∈ 𝐷 ) ) ∧ ( 𝑓 ∈ 𝐹 ∧ 𝑔 ∈ 𝐺 ) ) ↔ ( ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ∧ ( 𝑓 ∈ 𝐹 ∧ 𝑔 ∈ 𝐺 ) ) ∧ ( ( 𝑧 ∈ 𝐶 ∧ 𝑤 ∈ 𝐷 ) ∧ ( 𝑓 ∈ 𝐹 ∧ 𝑔 ∈ 𝐺 ) ) ) )
8	1 2 5 6	5oalem2	⊢ ( ( ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ∧ ( 𝑓 ∈ 𝐹 ∧ 𝑔 ∈ 𝐺 ) ) ∧ ( 𝑥 +ℎ 𝑦 ) = ( 𝑓 +ℎ 𝑔 ) ) → ( 𝑥 −ℎ 𝑓 ) ∈ ( ( 𝐴 +ℋ 𝐹 ) ∩ ( 𝐵 +ℋ 𝐺 ) ) )
9	3 4 5 6	5oalem2	⊢ ( ( ( ( 𝑧 ∈ 𝐶 ∧ 𝑤 ∈ 𝐷 ) ∧ ( 𝑓 ∈ 𝐹 ∧ 𝑔 ∈ 𝐺 ) ) ∧ ( 𝑧 +ℎ 𝑤 ) = ( 𝑓 +ℎ 𝑔 ) ) → ( 𝑧 −ℎ 𝑓 ) ∈ ( ( 𝐶 +ℋ 𝐹 ) ∩ ( 𝐷 +ℋ 𝐺 ) ) )
10	8 9	anim12i	⊢ ( ( ( ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ∧ ( 𝑓 ∈ 𝐹 ∧ 𝑔 ∈ 𝐺 ) ) ∧ ( 𝑥 +ℎ 𝑦 ) = ( 𝑓 +ℎ 𝑔 ) ) ∧ ( ( ( 𝑧 ∈ 𝐶 ∧ 𝑤 ∈ 𝐷 ) ∧ ( 𝑓 ∈ 𝐹 ∧ 𝑔 ∈ 𝐺 ) ) ∧ ( 𝑧 +ℎ 𝑤 ) = ( 𝑓 +ℎ 𝑔 ) ) ) → ( ( 𝑥 −ℎ 𝑓 ) ∈ ( ( 𝐴 +ℋ 𝐹 ) ∩ ( 𝐵 +ℋ 𝐺 ) ) ∧ ( 𝑧 −ℎ 𝑓 ) ∈ ( ( 𝐶 +ℋ 𝐹 ) ∩ ( 𝐷 +ℋ 𝐺 ) ) ) )
11	10	an4s	⊢ ( ( ( ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ∧ ( 𝑓 ∈ 𝐹 ∧ 𝑔 ∈ 𝐺 ) ) ∧ ( ( 𝑧 ∈ 𝐶 ∧ 𝑤 ∈ 𝐷 ) ∧ ( 𝑓 ∈ 𝐹 ∧ 𝑔 ∈ 𝐺 ) ) ) ∧ ( ( 𝑥 +ℎ 𝑦 ) = ( 𝑓 +ℎ 𝑔 ) ∧ ( 𝑧 +ℎ 𝑤 ) = ( 𝑓 +ℎ 𝑔 ) ) ) → ( ( 𝑥 −ℎ 𝑓 ) ∈ ( ( 𝐴 +ℋ 𝐹 ) ∩ ( 𝐵 +ℋ 𝐺 ) ) ∧ ( 𝑧 −ℎ 𝑓 ) ∈ ( ( 𝐶 +ℋ 𝐹 ) ∩ ( 𝐷 +ℋ 𝐺 ) ) ) )
12	7 11	sylanb	⊢ ( ( ( ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ∧ ( 𝑧 ∈ 𝐶 ∧ 𝑤 ∈ 𝐷 ) ) ∧ ( 𝑓 ∈ 𝐹 ∧ 𝑔 ∈ 𝐺 ) ) ∧ ( ( 𝑥 +ℎ 𝑦 ) = ( 𝑓 +ℎ 𝑔 ) ∧ ( 𝑧 +ℎ 𝑤 ) = ( 𝑓 +ℎ 𝑔 ) ) ) → ( ( 𝑥 −ℎ 𝑓 ) ∈ ( ( 𝐴 +ℋ 𝐹 ) ∩ ( 𝐵 +ℋ 𝐺 ) ) ∧ ( 𝑧 −ℎ 𝑓 ) ∈ ( ( 𝐶 +ℋ 𝐹 ) ∩ ( 𝐷 +ℋ 𝐺 ) ) ) )
13	1 5	shscli	⊢ ( 𝐴 +ℋ 𝐹 ) ∈ Sℋ
14	2 6	shscli	⊢ ( 𝐵 +ℋ 𝐺 ) ∈ Sℋ
15	13 14	shincli	⊢ ( ( 𝐴 +ℋ 𝐹 ) ∩ ( 𝐵 +ℋ 𝐺 ) ) ∈ Sℋ
16	3 5	shscli	⊢ ( 𝐶 +ℋ 𝐹 ) ∈ Sℋ
17	4 6	shscli	⊢ ( 𝐷 +ℋ 𝐺 ) ∈ Sℋ
18	16 17	shincli	⊢ ( ( 𝐶 +ℋ 𝐹 ) ∩ ( 𝐷 +ℋ 𝐺 ) ) ∈ Sℋ
19	15 18	shsvsi	⊢ ( ( ( 𝑥 −ℎ 𝑓 ) ∈ ( ( 𝐴 +ℋ 𝐹 ) ∩ ( 𝐵 +ℋ 𝐺 ) ) ∧ ( 𝑧 −ℎ 𝑓 ) ∈ ( ( 𝐶 +ℋ 𝐹 ) ∩ ( 𝐷 +ℋ 𝐺 ) ) ) → ( ( 𝑥 −ℎ 𝑓 ) −ℎ ( 𝑧 −ℎ 𝑓 ) ) ∈ ( ( ( 𝐴 +ℋ 𝐹 ) ∩ ( 𝐵 +ℋ 𝐺 ) ) +ℋ ( ( 𝐶 +ℋ 𝐹 ) ∩ ( 𝐷 +ℋ 𝐺 ) ) ) )
20	12 19	syl	⊢ ( ( ( ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ∧ ( 𝑧 ∈ 𝐶 ∧ 𝑤 ∈ 𝐷 ) ) ∧ ( 𝑓 ∈ 𝐹 ∧ 𝑔 ∈ 𝐺 ) ) ∧ ( ( 𝑥 +ℎ 𝑦 ) = ( 𝑓 +ℎ 𝑔 ) ∧ ( 𝑧 +ℎ 𝑤 ) = ( 𝑓 +ℎ 𝑔 ) ) ) → ( ( 𝑥 −ℎ 𝑓 ) −ℎ ( 𝑧 −ℎ 𝑓 ) ) ∈ ( ( ( 𝐴 +ℋ 𝐹 ) ∩ ( 𝐵 +ℋ 𝐺 ) ) +ℋ ( ( 𝐶 +ℋ 𝐹 ) ∩ ( 𝐷 +ℋ 𝐺 ) ) ) )
21	1	sheli	⊢ ( 𝑥 ∈ 𝐴 → 𝑥 ∈ ℋ )
22	21	adantr	⊢ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) → 𝑥 ∈ ℋ )
23	3	sheli	⊢ ( 𝑧 ∈ 𝐶 → 𝑧 ∈ ℋ )
24	23	adantr	⊢ ( ( 𝑧 ∈ 𝐶 ∧ 𝑤 ∈ 𝐷 ) → 𝑧 ∈ ℋ )
25	22 24	anim12i	⊢ ( ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ∧ ( 𝑧 ∈ 𝐶 ∧ 𝑤 ∈ 𝐷 ) ) → ( 𝑥 ∈ ℋ ∧ 𝑧 ∈ ℋ ) )
26	5	sheli	⊢ ( 𝑓 ∈ 𝐹 → 𝑓 ∈ ℋ )
27	26	adantr	⊢ ( ( 𝑓 ∈ 𝐹 ∧ 𝑔 ∈ 𝐺 ) → 𝑓 ∈ ℋ )
28		hvsubsub4	⊢ ( ( ( 𝑥 ∈ ℋ ∧ 𝑓 ∈ ℋ ) ∧ ( 𝑧 ∈ ℋ ∧ 𝑓 ∈ ℋ ) ) → ( ( 𝑥 −ℎ 𝑓 ) −ℎ ( 𝑧 −ℎ 𝑓 ) ) = ( ( 𝑥 −ℎ 𝑧 ) −ℎ ( 𝑓 −ℎ 𝑓 ) ) )
29	28	anandirs	⊢ ( ( ( 𝑥 ∈ ℋ ∧ 𝑧 ∈ ℋ ) ∧ 𝑓 ∈ ℋ ) → ( ( 𝑥 −ℎ 𝑓 ) −ℎ ( 𝑧 −ℎ 𝑓 ) ) = ( ( 𝑥 −ℎ 𝑧 ) −ℎ ( 𝑓 −ℎ 𝑓 ) ) )
30		hvsubid	⊢ ( 𝑓 ∈ ℋ → ( 𝑓 −ℎ 𝑓 ) = 0ℎ )
31	30	oveq2d	⊢ ( 𝑓 ∈ ℋ → ( ( 𝑥 −ℎ 𝑧 ) −ℎ ( 𝑓 −ℎ 𝑓 ) ) = ( ( 𝑥 −ℎ 𝑧 ) −ℎ 0ℎ ) )
32		hvsubcl	⊢ ( ( 𝑥 ∈ ℋ ∧ 𝑧 ∈ ℋ ) → ( 𝑥 −ℎ 𝑧 ) ∈ ℋ )
33		hvsub0	⊢ ( ( 𝑥 −ℎ 𝑧 ) ∈ ℋ → ( ( 𝑥 −ℎ 𝑧 ) −ℎ 0ℎ ) = ( 𝑥 −ℎ 𝑧 ) )
34	32 33	syl	⊢ ( ( 𝑥 ∈ ℋ ∧ 𝑧 ∈ ℋ ) → ( ( 𝑥 −ℎ 𝑧 ) −ℎ 0ℎ ) = ( 𝑥 −ℎ 𝑧 ) )
35	31 34	sylan9eqr	⊢ ( ( ( 𝑥 ∈ ℋ ∧ 𝑧 ∈ ℋ ) ∧ 𝑓 ∈ ℋ ) → ( ( 𝑥 −ℎ 𝑧 ) −ℎ ( 𝑓 −ℎ 𝑓 ) ) = ( 𝑥 −ℎ 𝑧 ) )
36	29 35	eqtrd	⊢ ( ( ( 𝑥 ∈ ℋ ∧ 𝑧 ∈ ℋ ) ∧ 𝑓 ∈ ℋ ) → ( ( 𝑥 −ℎ 𝑓 ) −ℎ ( 𝑧 −ℎ 𝑓 ) ) = ( 𝑥 −ℎ 𝑧 ) )
37	25 27 36	syl2an	⊢ ( ( ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ∧ ( 𝑧 ∈ 𝐶 ∧ 𝑤 ∈ 𝐷 ) ) ∧ ( 𝑓 ∈ 𝐹 ∧ 𝑔 ∈ 𝐺 ) ) → ( ( 𝑥 −ℎ 𝑓 ) −ℎ ( 𝑧 −ℎ 𝑓 ) ) = ( 𝑥 −ℎ 𝑧 ) )
38	37	eleq1d	⊢ ( ( ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ∧ ( 𝑧 ∈ 𝐶 ∧ 𝑤 ∈ 𝐷 ) ) ∧ ( 𝑓 ∈ 𝐹 ∧ 𝑔 ∈ 𝐺 ) ) → ( ( ( 𝑥 −ℎ 𝑓 ) −ℎ ( 𝑧 −ℎ 𝑓 ) ) ∈ ( ( ( 𝐴 +ℋ 𝐹 ) ∩ ( 𝐵 +ℋ 𝐺 ) ) +ℋ ( ( 𝐶 +ℋ 𝐹 ) ∩ ( 𝐷 +ℋ 𝐺 ) ) ) ↔ ( 𝑥 −ℎ 𝑧 ) ∈ ( ( ( 𝐴 +ℋ 𝐹 ) ∩ ( 𝐵 +ℋ 𝐺 ) ) +ℋ ( ( 𝐶 +ℋ 𝐹 ) ∩ ( 𝐷 +ℋ 𝐺 ) ) ) ) )
39	38	adantr	⊢ ( ( ( ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ∧ ( 𝑧 ∈ 𝐶 ∧ 𝑤 ∈ 𝐷 ) ) ∧ ( 𝑓 ∈ 𝐹 ∧ 𝑔 ∈ 𝐺 ) ) ∧ ( ( 𝑥 +ℎ 𝑦 ) = ( 𝑓 +ℎ 𝑔 ) ∧ ( 𝑧 +ℎ 𝑤 ) = ( 𝑓 +ℎ 𝑔 ) ) ) → ( ( ( 𝑥 −ℎ 𝑓 ) −ℎ ( 𝑧 −ℎ 𝑓 ) ) ∈ ( ( ( 𝐴 +ℋ 𝐹 ) ∩ ( 𝐵 +ℋ 𝐺 ) ) +ℋ ( ( 𝐶 +ℋ 𝐹 ) ∩ ( 𝐷 +ℋ 𝐺 ) ) ) ↔ ( 𝑥 −ℎ 𝑧 ) ∈ ( ( ( 𝐴 +ℋ 𝐹 ) ∩ ( 𝐵 +ℋ 𝐺 ) ) +ℋ ( ( 𝐶 +ℋ 𝐹 ) ∩ ( 𝐷 +ℋ 𝐺 ) ) ) ) )
40	20 39	mpbid	⊢ ( ( ( ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ∧ ( 𝑧 ∈ 𝐶 ∧ 𝑤 ∈ 𝐷 ) ) ∧ ( 𝑓 ∈ 𝐹 ∧ 𝑔 ∈ 𝐺 ) ) ∧ ( ( 𝑥 +ℎ 𝑦 ) = ( 𝑓 +ℎ 𝑔 ) ∧ ( 𝑧 +ℎ 𝑤 ) = ( 𝑓 +ℎ 𝑔 ) ) ) → ( 𝑥 −ℎ 𝑧 ) ∈ ( ( ( 𝐴 +ℋ 𝐹 ) ∩ ( 𝐵 +ℋ 𝐺 ) ) +ℋ ( ( 𝐶 +ℋ 𝐹 ) ∩ ( 𝐷 +ℋ 𝐺 ) ) ) )