Theorem 5oalem5

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

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

Proof

Step	Hyp	Ref	Expression
1		5oalem5.1	⊢ 𝐴 ∈ Sℋ
2		5oalem5.2	⊢ 𝐵 ∈ Sℋ
3		5oalem5.3	⊢ 𝐶 ∈ Sℋ
4		5oalem5.4	⊢ 𝐷 ∈ Sℋ
5		5oalem5.5	⊢ 𝐹 ∈ Sℋ
6		5oalem5.6	⊢ 𝐺 ∈ Sℋ
7		5oalem5.7	⊢ 𝑅 ∈ Sℋ
8		5oalem5.8	⊢ 𝑆 ∈ Sℋ
9		simpr	⊢ ( ( ( 𝑓 ∈ 𝐹 ∧ 𝑔 ∈ 𝐺 ) ∧ ( 𝑣 ∈ 𝑅 ∧ 𝑢 ∈ 𝑆 ) ) → ( 𝑣 ∈ 𝑅 ∧ 𝑢 ∈ 𝑆 ) )
10	9	anim2i	⊢ ( ( ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ∧ ( 𝑧 ∈ 𝐶 ∧ 𝑤 ∈ 𝐷 ) ) ∧ ( ( 𝑓 ∈ 𝐹 ∧ 𝑔 ∈ 𝐺 ) ∧ ( 𝑣 ∈ 𝑅 ∧ 𝑢 ∈ 𝑆 ) ) ) → ( ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ∧ ( 𝑧 ∈ 𝐶 ∧ 𝑤 ∈ 𝐷 ) ) ∧ ( 𝑣 ∈ 𝑅 ∧ 𝑢 ∈ 𝑆 ) ) )
11		simpl	⊢ ( ( ( ( 𝑥 +ℎ 𝑦 ) = ( 𝑣 +ℎ 𝑢 ) ∧ ( 𝑧 +ℎ 𝑤 ) = ( 𝑣 +ℎ 𝑢 ) ) ∧ ( 𝑓 +ℎ 𝑔 ) = ( 𝑣 +ℎ 𝑢 ) ) → ( ( 𝑥 +ℎ 𝑦 ) = ( 𝑣 +ℎ 𝑢 ) ∧ ( 𝑧 +ℎ 𝑤 ) = ( 𝑣 +ℎ 𝑢 ) ) )
12	1 2 3 4 7 8	5oalem4	⊢ ( ( ( ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ∧ ( 𝑧 ∈ 𝐶 ∧ 𝑤 ∈ 𝐷 ) ) ∧ ( 𝑣 ∈ 𝑅 ∧ 𝑢 ∈ 𝑆 ) ) ∧ ( ( 𝑥 +ℎ 𝑦 ) = ( 𝑣 +ℎ 𝑢 ) ∧ ( 𝑧 +ℎ 𝑤 ) = ( 𝑣 +ℎ 𝑢 ) ) ) → ( 𝑥 −ℎ 𝑧 ) ∈ ( ( ( 𝐴 +ℋ 𝐶 ) ∩ ( 𝐵 +ℋ 𝐷 ) ) ∩ ( ( ( 𝐴 +ℋ 𝑅 ) ∩ ( 𝐵 +ℋ 𝑆 ) ) +ℋ ( ( 𝐶 +ℋ 𝑅 ) ∩ ( 𝐷 +ℋ 𝑆 ) ) ) ) )
13	10 11 12	syl2an	⊢ ( ( ( ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ∧ ( 𝑧 ∈ 𝐶 ∧ 𝑤 ∈ 𝐷 ) ) ∧ ( ( 𝑓 ∈ 𝐹 ∧ 𝑔 ∈ 𝐺 ) ∧ ( 𝑣 ∈ 𝑅 ∧ 𝑢 ∈ 𝑆 ) ) ) ∧ ( ( ( 𝑥 +ℎ 𝑦 ) = ( 𝑣 +ℎ 𝑢 ) ∧ ( 𝑧 +ℎ 𝑤 ) = ( 𝑣 +ℎ 𝑢 ) ) ∧ ( 𝑓 +ℎ 𝑔 ) = ( 𝑣 +ℎ 𝑢 ) ) ) → ( 𝑥 −ℎ 𝑧 ) ∈ ( ( ( 𝐴 +ℋ 𝐶 ) ∩ ( 𝐵 +ℋ 𝐷 ) ) ∩ ( ( ( 𝐴 +ℋ 𝑅 ) ∩ ( 𝐵 +ℋ 𝑆 ) ) +ℋ ( ( 𝐶 +ℋ 𝑅 ) ∩ ( 𝐷 +ℋ 𝑆 ) ) ) ) )
14	1	sheli	⊢ ( 𝑥 ∈ 𝐴 → 𝑥 ∈ ℋ )
15	14	adantr	⊢ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) → 𝑥 ∈ ℋ )
16	3	sheli	⊢ ( 𝑧 ∈ 𝐶 → 𝑧 ∈ ℋ )
17	16	adantr	⊢ ( ( 𝑧 ∈ 𝐶 ∧ 𝑤 ∈ 𝐷 ) → 𝑧 ∈ ℋ )
18	15 17	anim12i	⊢ ( ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ∧ ( 𝑧 ∈ 𝐶 ∧ 𝑤 ∈ 𝐷 ) ) → ( 𝑥 ∈ ℋ ∧ 𝑧 ∈ ℋ ) )
19	5	sheli	⊢ ( 𝑓 ∈ 𝐹 → 𝑓 ∈ ℋ )
20	19	adantr	⊢ ( ( 𝑓 ∈ 𝐹 ∧ 𝑔 ∈ 𝐺 ) → 𝑓 ∈ ℋ )
21		hvsubsub4	⊢ ( ( ( 𝑥 ∈ ℋ ∧ 𝑓 ∈ ℋ ) ∧ ( 𝑧 ∈ ℋ ∧ 𝑓 ∈ ℋ ) ) → ( ( 𝑥 −ℎ 𝑓 ) −ℎ ( 𝑧 −ℎ 𝑓 ) ) = ( ( 𝑥 −ℎ 𝑧 ) −ℎ ( 𝑓 −ℎ 𝑓 ) ) )
22	21	anandirs	⊢ ( ( ( 𝑥 ∈ ℋ ∧ 𝑧 ∈ ℋ ) ∧ 𝑓 ∈ ℋ ) → ( ( 𝑥 −ℎ 𝑓 ) −ℎ ( 𝑧 −ℎ 𝑓 ) ) = ( ( 𝑥 −ℎ 𝑧 ) −ℎ ( 𝑓 −ℎ 𝑓 ) ) )
23		hvsubid	⊢ ( 𝑓 ∈ ℋ → ( 𝑓 −ℎ 𝑓 ) = 0ℎ )
24	23	oveq2d	⊢ ( 𝑓 ∈ ℋ → ( ( 𝑥 −ℎ 𝑧 ) −ℎ ( 𝑓 −ℎ 𝑓 ) ) = ( ( 𝑥 −ℎ 𝑧 ) −ℎ 0ℎ ) )
25		hvsubcl	⊢ ( ( 𝑥 ∈ ℋ ∧ 𝑧 ∈ ℋ ) → ( 𝑥 −ℎ 𝑧 ) ∈ ℋ )
26		hvsub0	⊢ ( ( 𝑥 −ℎ 𝑧 ) ∈ ℋ → ( ( 𝑥 −ℎ 𝑧 ) −ℎ 0ℎ ) = ( 𝑥 −ℎ 𝑧 ) )
27	25 26	syl	⊢ ( ( 𝑥 ∈ ℋ ∧ 𝑧 ∈ ℋ ) → ( ( 𝑥 −ℎ 𝑧 ) −ℎ 0ℎ ) = ( 𝑥 −ℎ 𝑧 ) )
28	24 27	sylan9eqr	⊢ ( ( ( 𝑥 ∈ ℋ ∧ 𝑧 ∈ ℋ ) ∧ 𝑓 ∈ ℋ ) → ( ( 𝑥 −ℎ 𝑧 ) −ℎ ( 𝑓 −ℎ 𝑓 ) ) = ( 𝑥 −ℎ 𝑧 ) )
29	22 28	eqtrd	⊢ ( ( ( 𝑥 ∈ ℋ ∧ 𝑧 ∈ ℋ ) ∧ 𝑓 ∈ ℋ ) → ( ( 𝑥 −ℎ 𝑓 ) −ℎ ( 𝑧 −ℎ 𝑓 ) ) = ( 𝑥 −ℎ 𝑧 ) )
30	18 20 29	syl2an	⊢ ( ( ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ∧ ( 𝑧 ∈ 𝐶 ∧ 𝑤 ∈ 𝐷 ) ) ∧ ( 𝑓 ∈ 𝐹 ∧ 𝑔 ∈ 𝐺 ) ) → ( ( 𝑥 −ℎ 𝑓 ) −ℎ ( 𝑧 −ℎ 𝑓 ) ) = ( 𝑥 −ℎ 𝑧 ) )
31	30	adantrr	⊢ ( ( ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ∧ ( 𝑧 ∈ 𝐶 ∧ 𝑤 ∈ 𝐷 ) ) ∧ ( ( 𝑓 ∈ 𝐹 ∧ 𝑔 ∈ 𝐺 ) ∧ ( 𝑣 ∈ 𝑅 ∧ 𝑢 ∈ 𝑆 ) ) ) → ( ( 𝑥 −ℎ 𝑓 ) −ℎ ( 𝑧 −ℎ 𝑓 ) ) = ( 𝑥 −ℎ 𝑧 ) )
32	31	adantr	⊢ ( ( ( ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ∧ ( 𝑧 ∈ 𝐶 ∧ 𝑤 ∈ 𝐷 ) ) ∧ ( ( 𝑓 ∈ 𝐹 ∧ 𝑔 ∈ 𝐺 ) ∧ ( 𝑣 ∈ 𝑅 ∧ 𝑢 ∈ 𝑆 ) ) ) ∧ ( ( ( 𝑥 +ℎ 𝑦 ) = ( 𝑣 +ℎ 𝑢 ) ∧ ( 𝑧 +ℎ 𝑤 ) = ( 𝑣 +ℎ 𝑢 ) ) ∧ ( 𝑓 +ℎ 𝑔 ) = ( 𝑣 +ℎ 𝑢 ) ) ) → ( ( 𝑥 −ℎ 𝑓 ) −ℎ ( 𝑧 −ℎ 𝑓 ) ) = ( 𝑥 −ℎ 𝑧 ) )
33		simpl	⊢ ( ( ( 𝑓 ∈ 𝐹 ∧ 𝑔 ∈ 𝐺 ) ∧ ( 𝑣 ∈ 𝑅 ∧ 𝑢 ∈ 𝑆 ) ) → ( 𝑓 ∈ 𝐹 ∧ 𝑔 ∈ 𝐺 ) )
34	33	anim2i	⊢ ( ( ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ∧ ( 𝑧 ∈ 𝐶 ∧ 𝑤 ∈ 𝐷 ) ) ∧ ( ( 𝑓 ∈ 𝐹 ∧ 𝑔 ∈ 𝐺 ) ∧ ( 𝑣 ∈ 𝑅 ∧ 𝑢 ∈ 𝑆 ) ) ) → ( ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ∧ ( 𝑧 ∈ 𝐶 ∧ 𝑤 ∈ 𝐷 ) ) ∧ ( 𝑓 ∈ 𝐹 ∧ 𝑔 ∈ 𝐺 ) ) )
35		anandir	⊢ ( ( ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ∧ ( 𝑧 ∈ 𝐶 ∧ 𝑤 ∈ 𝐷 ) ) ∧ ( 𝑓 ∈ 𝐹 ∧ 𝑔 ∈ 𝐺 ) ) ↔ ( ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ∧ ( 𝑓 ∈ 𝐹 ∧ 𝑔 ∈ 𝐺 ) ) ∧ ( ( 𝑧 ∈ 𝐶 ∧ 𝑤 ∈ 𝐷 ) ∧ ( 𝑓 ∈ 𝐹 ∧ 𝑔 ∈ 𝐺 ) ) ) )
36	34 35	sylib	⊢ ( ( ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ∧ ( 𝑧 ∈ 𝐶 ∧ 𝑤 ∈ 𝐷 ) ) ∧ ( ( 𝑓 ∈ 𝐹 ∧ 𝑔 ∈ 𝐺 ) ∧ ( 𝑣 ∈ 𝑅 ∧ 𝑢 ∈ 𝑆 ) ) ) → ( ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ∧ ( 𝑓 ∈ 𝐹 ∧ 𝑔 ∈ 𝐺 ) ) ∧ ( ( 𝑧 ∈ 𝐶 ∧ 𝑤 ∈ 𝐷 ) ∧ ( 𝑓 ∈ 𝐹 ∧ 𝑔 ∈ 𝐺 ) ) ) )
37		simprr	⊢ ( ( ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ∧ ( 𝑧 ∈ 𝐶 ∧ 𝑤 ∈ 𝐷 ) ) ∧ ( ( 𝑓 ∈ 𝐹 ∧ 𝑔 ∈ 𝐺 ) ∧ ( 𝑣 ∈ 𝑅 ∧ 𝑢 ∈ 𝑆 ) ) ) → ( 𝑣 ∈ 𝑅 ∧ 𝑢 ∈ 𝑆 ) )
38	36 37	jca	⊢ ( ( ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ∧ ( 𝑧 ∈ 𝐶 ∧ 𝑤 ∈ 𝐷 ) ) ∧ ( ( 𝑓 ∈ 𝐹 ∧ 𝑔 ∈ 𝐺 ) ∧ ( 𝑣 ∈ 𝑅 ∧ 𝑢 ∈ 𝑆 ) ) ) → ( ( ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ∧ ( 𝑓 ∈ 𝐹 ∧ 𝑔 ∈ 𝐺 ) ) ∧ ( ( 𝑧 ∈ 𝐶 ∧ 𝑤 ∈ 𝐷 ) ∧ ( 𝑓 ∈ 𝐹 ∧ 𝑔 ∈ 𝐺 ) ) ) ∧ ( 𝑣 ∈ 𝑅 ∧ 𝑢 ∈ 𝑆 ) ) )
39		simpl	⊢ ( ( ( 𝑥 +ℎ 𝑦 ) = ( 𝑣 +ℎ 𝑢 ) ∧ ( 𝑧 +ℎ 𝑤 ) = ( 𝑣 +ℎ 𝑢 ) ) → ( 𝑥 +ℎ 𝑦 ) = ( 𝑣 +ℎ 𝑢 ) )
40	39	anim1i	⊢ ( ( ( ( 𝑥 +ℎ 𝑦 ) = ( 𝑣 +ℎ 𝑢 ) ∧ ( 𝑧 +ℎ 𝑤 ) = ( 𝑣 +ℎ 𝑢 ) ) ∧ ( 𝑓 +ℎ 𝑔 ) = ( 𝑣 +ℎ 𝑢 ) ) → ( ( 𝑥 +ℎ 𝑦 ) = ( 𝑣 +ℎ 𝑢 ) ∧ ( 𝑓 +ℎ 𝑔 ) = ( 𝑣 +ℎ 𝑢 ) ) )
41		simpr	⊢ ( ( ( 𝑥 +ℎ 𝑦 ) = ( 𝑣 +ℎ 𝑢 ) ∧ ( 𝑧 +ℎ 𝑤 ) = ( 𝑣 +ℎ 𝑢 ) ) → ( 𝑧 +ℎ 𝑤 ) = ( 𝑣 +ℎ 𝑢 ) )
42	41	anim1i	⊢ ( ( ( ( 𝑥 +ℎ 𝑦 ) = ( 𝑣 +ℎ 𝑢 ) ∧ ( 𝑧 +ℎ 𝑤 ) = ( 𝑣 +ℎ 𝑢 ) ) ∧ ( 𝑓 +ℎ 𝑔 ) = ( 𝑣 +ℎ 𝑢 ) ) → ( ( 𝑧 +ℎ 𝑤 ) = ( 𝑣 +ℎ 𝑢 ) ∧ ( 𝑓 +ℎ 𝑔 ) = ( 𝑣 +ℎ 𝑢 ) ) )
43	40 42	jca	⊢ ( ( ( ( 𝑥 +ℎ 𝑦 ) = ( 𝑣 +ℎ 𝑢 ) ∧ ( 𝑧 +ℎ 𝑤 ) = ( 𝑣 +ℎ 𝑢 ) ) ∧ ( 𝑓 +ℎ 𝑔 ) = ( 𝑣 +ℎ 𝑢 ) ) → ( ( ( 𝑥 +ℎ 𝑦 ) = ( 𝑣 +ℎ 𝑢 ) ∧ ( 𝑓 +ℎ 𝑔 ) = ( 𝑣 +ℎ 𝑢 ) ) ∧ ( ( 𝑧 +ℎ 𝑤 ) = ( 𝑣 +ℎ 𝑢 ) ∧ ( 𝑓 +ℎ 𝑔 ) = ( 𝑣 +ℎ 𝑢 ) ) ) )
44		anandir	⊢ ( ( ( ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ∧ ( 𝑓 ∈ 𝐹 ∧ 𝑔 ∈ 𝐺 ) ) ∧ ( ( 𝑧 ∈ 𝐶 ∧ 𝑤 ∈ 𝐷 ) ∧ ( 𝑓 ∈ 𝐹 ∧ 𝑔 ∈ 𝐺 ) ) ) ∧ ( 𝑣 ∈ 𝑅 ∧ 𝑢 ∈ 𝑆 ) ) ↔ ( ( ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ∧ ( 𝑓 ∈ 𝐹 ∧ 𝑔 ∈ 𝐺 ) ) ∧ ( 𝑣 ∈ 𝑅 ∧ 𝑢 ∈ 𝑆 ) ) ∧ ( ( ( 𝑧 ∈ 𝐶 ∧ 𝑤 ∈ 𝐷 ) ∧ ( 𝑓 ∈ 𝐹 ∧ 𝑔 ∈ 𝐺 ) ) ∧ ( 𝑣 ∈ 𝑅 ∧ 𝑢 ∈ 𝑆 ) ) ) )
45	1 2 5 6 7 8	5oalem4	⊢ ( ( ( ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ∧ ( 𝑓 ∈ 𝐹 ∧ 𝑔 ∈ 𝐺 ) ) ∧ ( 𝑣 ∈ 𝑅 ∧ 𝑢 ∈ 𝑆 ) ) ∧ ( ( 𝑥 +ℎ 𝑦 ) = ( 𝑣 +ℎ 𝑢 ) ∧ ( 𝑓 +ℎ 𝑔 ) = ( 𝑣 +ℎ 𝑢 ) ) ) → ( 𝑥 −ℎ 𝑓 ) ∈ ( ( ( 𝐴 +ℋ 𝐹 ) ∩ ( 𝐵 +ℋ 𝐺 ) ) ∩ ( ( ( 𝐴 +ℋ 𝑅 ) ∩ ( 𝐵 +ℋ 𝑆 ) ) +ℋ ( ( 𝐹 +ℋ 𝑅 ) ∩ ( 𝐺 +ℋ 𝑆 ) ) ) ) )
46	3 4 5 6 7 8	5oalem4	⊢ ( ( ( ( ( 𝑧 ∈ 𝐶 ∧ 𝑤 ∈ 𝐷 ) ∧ ( 𝑓 ∈ 𝐹 ∧ 𝑔 ∈ 𝐺 ) ) ∧ ( 𝑣 ∈ 𝑅 ∧ 𝑢 ∈ 𝑆 ) ) ∧ ( ( 𝑧 +ℎ 𝑤 ) = ( 𝑣 +ℎ 𝑢 ) ∧ ( 𝑓 +ℎ 𝑔 ) = ( 𝑣 +ℎ 𝑢 ) ) ) → ( 𝑧 −ℎ 𝑓 ) ∈ ( ( ( 𝐶 +ℋ 𝐹 ) ∩ ( 𝐷 +ℋ 𝐺 ) ) ∩ ( ( ( 𝐶 +ℋ 𝑅 ) ∩ ( 𝐷 +ℋ 𝑆 ) ) +ℋ ( ( 𝐹 +ℋ 𝑅 ) ∩ ( 𝐺 +ℋ 𝑆 ) ) ) ) )
47	45 46	anim12i	⊢ ( ( ( ( ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ∧ ( 𝑓 ∈ 𝐹 ∧ 𝑔 ∈ 𝐺 ) ) ∧ ( 𝑣 ∈ 𝑅 ∧ 𝑢 ∈ 𝑆 ) ) ∧ ( ( 𝑥 +ℎ 𝑦 ) = ( 𝑣 +ℎ 𝑢 ) ∧ ( 𝑓 +ℎ 𝑔 ) = ( 𝑣 +ℎ 𝑢 ) ) ) ∧ ( ( ( ( 𝑧 ∈ 𝐶 ∧ 𝑤 ∈ 𝐷 ) ∧ ( 𝑓 ∈ 𝐹 ∧ 𝑔 ∈ 𝐺 ) ) ∧ ( 𝑣 ∈ 𝑅 ∧ 𝑢 ∈ 𝑆 ) ) ∧ ( ( 𝑧 +ℎ 𝑤 ) = ( 𝑣 +ℎ 𝑢 ) ∧ ( 𝑓 +ℎ 𝑔 ) = ( 𝑣 +ℎ 𝑢 ) ) ) ) → ( ( 𝑥 −ℎ 𝑓 ) ∈ ( ( ( 𝐴 +ℋ 𝐹 ) ∩ ( 𝐵 +ℋ 𝐺 ) ) ∩ ( ( ( 𝐴 +ℋ 𝑅 ) ∩ ( 𝐵 +ℋ 𝑆 ) ) +ℋ ( ( 𝐹 +ℋ 𝑅 ) ∩ ( 𝐺 +ℋ 𝑆 ) ) ) ) ∧ ( 𝑧 −ℎ 𝑓 ) ∈ ( ( ( 𝐶 +ℋ 𝐹 ) ∩ ( 𝐷 +ℋ 𝐺 ) ) ∩ ( ( ( 𝐶 +ℋ 𝑅 ) ∩ ( 𝐷 +ℋ 𝑆 ) ) +ℋ ( ( 𝐹 +ℋ 𝑅 ) ∩ ( 𝐺 +ℋ 𝑆 ) ) ) ) ) )
48	47	an4s	⊢ ( ( ( ( ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ∧ ( 𝑓 ∈ 𝐹 ∧ 𝑔 ∈ 𝐺 ) ) ∧ ( 𝑣 ∈ 𝑅 ∧ 𝑢 ∈ 𝑆 ) ) ∧ ( ( ( 𝑧 ∈ 𝐶 ∧ 𝑤 ∈ 𝐷 ) ∧ ( 𝑓 ∈ 𝐹 ∧ 𝑔 ∈ 𝐺 ) ) ∧ ( 𝑣 ∈ 𝑅 ∧ 𝑢 ∈ 𝑆 ) ) ) ∧ ( ( ( 𝑥 +ℎ 𝑦 ) = ( 𝑣 +ℎ 𝑢 ) ∧ ( 𝑓 +ℎ 𝑔 ) = ( 𝑣 +ℎ 𝑢 ) ) ∧ ( ( 𝑧 +ℎ 𝑤 ) = ( 𝑣 +ℎ 𝑢 ) ∧ ( 𝑓 +ℎ 𝑔 ) = ( 𝑣 +ℎ 𝑢 ) ) ) ) → ( ( 𝑥 −ℎ 𝑓 ) ∈ ( ( ( 𝐴 +ℋ 𝐹 ) ∩ ( 𝐵 +ℋ 𝐺 ) ) ∩ ( ( ( 𝐴 +ℋ 𝑅 ) ∩ ( 𝐵 +ℋ 𝑆 ) ) +ℋ ( ( 𝐹 +ℋ 𝑅 ) ∩ ( 𝐺 +ℋ 𝑆 ) ) ) ) ∧ ( 𝑧 −ℎ 𝑓 ) ∈ ( ( ( 𝐶 +ℋ 𝐹 ) ∩ ( 𝐷 +ℋ 𝐺 ) ) ∩ ( ( ( 𝐶 +ℋ 𝑅 ) ∩ ( 𝐷 +ℋ 𝑆 ) ) +ℋ ( ( 𝐹 +ℋ 𝑅 ) ∩ ( 𝐺 +ℋ 𝑆 ) ) ) ) ) )
49	44 48	sylanb	⊢ ( ( ( ( ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ∧ ( 𝑓 ∈ 𝐹 ∧ 𝑔 ∈ 𝐺 ) ) ∧ ( ( 𝑧 ∈ 𝐶 ∧ 𝑤 ∈ 𝐷 ) ∧ ( 𝑓 ∈ 𝐹 ∧ 𝑔 ∈ 𝐺 ) ) ) ∧ ( 𝑣 ∈ 𝑅 ∧ 𝑢 ∈ 𝑆 ) ) ∧ ( ( ( 𝑥 +ℎ 𝑦 ) = ( 𝑣 +ℎ 𝑢 ) ∧ ( 𝑓 +ℎ 𝑔 ) = ( 𝑣 +ℎ 𝑢 ) ) ∧ ( ( 𝑧 +ℎ 𝑤 ) = ( 𝑣 +ℎ 𝑢 ) ∧ ( 𝑓 +ℎ 𝑔 ) = ( 𝑣 +ℎ 𝑢 ) ) ) ) → ( ( 𝑥 −ℎ 𝑓 ) ∈ ( ( ( 𝐴 +ℋ 𝐹 ) ∩ ( 𝐵 +ℋ 𝐺 ) ) ∩ ( ( ( 𝐴 +ℋ 𝑅 ) ∩ ( 𝐵 +ℋ 𝑆 ) ) +ℋ ( ( 𝐹 +ℋ 𝑅 ) ∩ ( 𝐺 +ℋ 𝑆 ) ) ) ) ∧ ( 𝑧 −ℎ 𝑓 ) ∈ ( ( ( 𝐶 +ℋ 𝐹 ) ∩ ( 𝐷 +ℋ 𝐺 ) ) ∩ ( ( ( 𝐶 +ℋ 𝑅 ) ∩ ( 𝐷 +ℋ 𝑆 ) ) +ℋ ( ( 𝐹 +ℋ 𝑅 ) ∩ ( 𝐺 +ℋ 𝑆 ) ) ) ) ) )
50	38 43 49	syl2an	⊢ ( ( ( ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ∧ ( 𝑧 ∈ 𝐶 ∧ 𝑤 ∈ 𝐷 ) ) ∧ ( ( 𝑓 ∈ 𝐹 ∧ 𝑔 ∈ 𝐺 ) ∧ ( 𝑣 ∈ 𝑅 ∧ 𝑢 ∈ 𝑆 ) ) ) ∧ ( ( ( 𝑥 +ℎ 𝑦 ) = ( 𝑣 +ℎ 𝑢 ) ∧ ( 𝑧 +ℎ 𝑤 ) = ( 𝑣 +ℎ 𝑢 ) ) ∧ ( 𝑓 +ℎ 𝑔 ) = ( 𝑣 +ℎ 𝑢 ) ) ) → ( ( 𝑥 −ℎ 𝑓 ) ∈ ( ( ( 𝐴 +ℋ 𝐹 ) ∩ ( 𝐵 +ℋ 𝐺 ) ) ∩ ( ( ( 𝐴 +ℋ 𝑅 ) ∩ ( 𝐵 +ℋ 𝑆 ) ) +ℋ ( ( 𝐹 +ℋ 𝑅 ) ∩ ( 𝐺 +ℋ 𝑆 ) ) ) ) ∧ ( 𝑧 −ℎ 𝑓 ) ∈ ( ( ( 𝐶 +ℋ 𝐹 ) ∩ ( 𝐷 +ℋ 𝐺 ) ) ∩ ( ( ( 𝐶 +ℋ 𝑅 ) ∩ ( 𝐷 +ℋ 𝑆 ) ) +ℋ ( ( 𝐹 +ℋ 𝑅 ) ∩ ( 𝐺 +ℋ 𝑆 ) ) ) ) ) )
51	1 5	shscli	⊢ ( 𝐴 +ℋ 𝐹 ) ∈ Sℋ
52	2 6	shscli	⊢ ( 𝐵 +ℋ 𝐺 ) ∈ Sℋ
53	51 52	shincli	⊢ ( ( 𝐴 +ℋ 𝐹 ) ∩ ( 𝐵 +ℋ 𝐺 ) ) ∈ Sℋ
54	1 7	shscli	⊢ ( 𝐴 +ℋ 𝑅 ) ∈ Sℋ
55	2 8	shscli	⊢ ( 𝐵 +ℋ 𝑆 ) ∈ Sℋ
56	54 55	shincli	⊢ ( ( 𝐴 +ℋ 𝑅 ) ∩ ( 𝐵 +ℋ 𝑆 ) ) ∈ Sℋ
57	5 7	shscli	⊢ ( 𝐹 +ℋ 𝑅 ) ∈ Sℋ
58	6 8	shscli	⊢ ( 𝐺 +ℋ 𝑆 ) ∈ Sℋ
59	57 58	shincli	⊢ ( ( 𝐹 +ℋ 𝑅 ) ∩ ( 𝐺 +ℋ 𝑆 ) ) ∈ Sℋ
60	56 59	shscli	⊢ ( ( ( 𝐴 +ℋ 𝑅 ) ∩ ( 𝐵 +ℋ 𝑆 ) ) +ℋ ( ( 𝐹 +ℋ 𝑅 ) ∩ ( 𝐺 +ℋ 𝑆 ) ) ) ∈ Sℋ
61	53 60	shincli	⊢ ( ( ( 𝐴 +ℋ 𝐹 ) ∩ ( 𝐵 +ℋ 𝐺 ) ) ∩ ( ( ( 𝐴 +ℋ 𝑅 ) ∩ ( 𝐵 +ℋ 𝑆 ) ) +ℋ ( ( 𝐹 +ℋ 𝑅 ) ∩ ( 𝐺 +ℋ 𝑆 ) ) ) ) ∈ Sℋ
62	3 5	shscli	⊢ ( 𝐶 +ℋ 𝐹 ) ∈ Sℋ
63	4 6	shscli	⊢ ( 𝐷 +ℋ 𝐺 ) ∈ Sℋ
64	62 63	shincli	⊢ ( ( 𝐶 +ℋ 𝐹 ) ∩ ( 𝐷 +ℋ 𝐺 ) ) ∈ Sℋ
65	3 7	shscli	⊢ ( 𝐶 +ℋ 𝑅 ) ∈ Sℋ
66	4 8	shscli	⊢ ( 𝐷 +ℋ 𝑆 ) ∈ Sℋ
67	65 66	shincli	⊢ ( ( 𝐶 +ℋ 𝑅 ) ∩ ( 𝐷 +ℋ 𝑆 ) ) ∈ Sℋ
68	67 59	shscli	⊢ ( ( ( 𝐶 +ℋ 𝑅 ) ∩ ( 𝐷 +ℋ 𝑆 ) ) +ℋ ( ( 𝐹 +ℋ 𝑅 ) ∩ ( 𝐺 +ℋ 𝑆 ) ) ) ∈ Sℋ
69	64 68	shincli	⊢ ( ( ( 𝐶 +ℋ 𝐹 ) ∩ ( 𝐷 +ℋ 𝐺 ) ) ∩ ( ( ( 𝐶 +ℋ 𝑅 ) ∩ ( 𝐷 +ℋ 𝑆 ) ) +ℋ ( ( 𝐹 +ℋ 𝑅 ) ∩ ( 𝐺 +ℋ 𝑆 ) ) ) ) ∈ Sℋ
70	61 69	shsvsi	⊢ ( ( ( 𝑥 −ℎ 𝑓 ) ∈ ( ( ( 𝐴 +ℋ 𝐹 ) ∩ ( 𝐵 +ℋ 𝐺 ) ) ∩ ( ( ( 𝐴 +ℋ 𝑅 ) ∩ ( 𝐵 +ℋ 𝑆 ) ) +ℋ ( ( 𝐹 +ℋ 𝑅 ) ∩ ( 𝐺 +ℋ 𝑆 ) ) ) ) ∧ ( 𝑧 −ℎ 𝑓 ) ∈ ( ( ( 𝐶 +ℋ 𝐹 ) ∩ ( 𝐷 +ℋ 𝐺 ) ) ∩ ( ( ( 𝐶 +ℋ 𝑅 ) ∩ ( 𝐷 +ℋ 𝑆 ) ) +ℋ ( ( 𝐹 +ℋ 𝑅 ) ∩ ( 𝐺 +ℋ 𝑆 ) ) ) ) ) → ( ( 𝑥 −ℎ 𝑓 ) −ℎ ( 𝑧 −ℎ 𝑓 ) ) ∈ ( ( ( ( 𝐴 +ℋ 𝐹 ) ∩ ( 𝐵 +ℋ 𝐺 ) ) ∩ ( ( ( 𝐴 +ℋ 𝑅 ) ∩ ( 𝐵 +ℋ 𝑆 ) ) +ℋ ( ( 𝐹 +ℋ 𝑅 ) ∩ ( 𝐺 +ℋ 𝑆 ) ) ) ) +ℋ ( ( ( 𝐶 +ℋ 𝐹 ) ∩ ( 𝐷 +ℋ 𝐺 ) ) ∩ ( ( ( 𝐶 +ℋ 𝑅 ) ∩ ( 𝐷 +ℋ 𝑆 ) ) +ℋ ( ( 𝐹 +ℋ 𝑅 ) ∩ ( 𝐺 +ℋ 𝑆 ) ) ) ) ) )
71	50 70	syl	⊢ ( ( ( ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ∧ ( 𝑧 ∈ 𝐶 ∧ 𝑤 ∈ 𝐷 ) ) ∧ ( ( 𝑓 ∈ 𝐹 ∧ 𝑔 ∈ 𝐺 ) ∧ ( 𝑣 ∈ 𝑅 ∧ 𝑢 ∈ 𝑆 ) ) ) ∧ ( ( ( 𝑥 +ℎ 𝑦 ) = ( 𝑣 +ℎ 𝑢 ) ∧ ( 𝑧 +ℎ 𝑤 ) = ( 𝑣 +ℎ 𝑢 ) ) ∧ ( 𝑓 +ℎ 𝑔 ) = ( 𝑣 +ℎ 𝑢 ) ) ) → ( ( 𝑥 −ℎ 𝑓 ) −ℎ ( 𝑧 −ℎ 𝑓 ) ) ∈ ( ( ( ( 𝐴 +ℋ 𝐹 ) ∩ ( 𝐵 +ℋ 𝐺 ) ) ∩ ( ( ( 𝐴 +ℋ 𝑅 ) ∩ ( 𝐵 +ℋ 𝑆 ) ) +ℋ ( ( 𝐹 +ℋ 𝑅 ) ∩ ( 𝐺 +ℋ 𝑆 ) ) ) ) +ℋ ( ( ( 𝐶 +ℋ 𝐹 ) ∩ ( 𝐷 +ℋ 𝐺 ) ) ∩ ( ( ( 𝐶 +ℋ 𝑅 ) ∩ ( 𝐷 +ℋ 𝑆 ) ) +ℋ ( ( 𝐹 +ℋ 𝑅 ) ∩ ( 𝐺 +ℋ 𝑆 ) ) ) ) ) )
72	32 71	eqeltrrd	⊢ ( ( ( ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ∧ ( 𝑧 ∈ 𝐶 ∧ 𝑤 ∈ 𝐷 ) ) ∧ ( ( 𝑓 ∈ 𝐹 ∧ 𝑔 ∈ 𝐺 ) ∧ ( 𝑣 ∈ 𝑅 ∧ 𝑢 ∈ 𝑆 ) ) ) ∧ ( ( ( 𝑥 +ℎ 𝑦 ) = ( 𝑣 +ℎ 𝑢 ) ∧ ( 𝑧 +ℎ 𝑤 ) = ( 𝑣 +ℎ 𝑢 ) ) ∧ ( 𝑓 +ℎ 𝑔 ) = ( 𝑣 +ℎ 𝑢 ) ) ) → ( 𝑥 −ℎ 𝑧 ) ∈ ( ( ( ( 𝐴 +ℋ 𝐹 ) ∩ ( 𝐵 +ℋ 𝐺 ) ) ∩ ( ( ( 𝐴 +ℋ 𝑅 ) ∩ ( 𝐵 +ℋ 𝑆 ) ) +ℋ ( ( 𝐹 +ℋ 𝑅 ) ∩ ( 𝐺 +ℋ 𝑆 ) ) ) ) +ℋ ( ( ( 𝐶 +ℋ 𝐹 ) ∩ ( 𝐷 +ℋ 𝐺 ) ) ∩ ( ( ( 𝐶 +ℋ 𝑅 ) ∩ ( 𝐷 +ℋ 𝑆 ) ) +ℋ ( ( 𝐹 +ℋ 𝑅 ) ∩ ( 𝐺 +ℋ 𝑆 ) ) ) ) ) )
73	13 72	elind	⊢ ( ( ( ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ∧ ( 𝑧 ∈ 𝐶 ∧ 𝑤 ∈ 𝐷 ) ) ∧ ( ( 𝑓 ∈ 𝐹 ∧ 𝑔 ∈ 𝐺 ) ∧ ( 𝑣 ∈ 𝑅 ∧ 𝑢 ∈ 𝑆 ) ) ) ∧ ( ( ( 𝑥 +ℎ 𝑦 ) = ( 𝑣 +ℎ 𝑢 ) ∧ ( 𝑧 +ℎ 𝑤 ) = ( 𝑣 +ℎ 𝑢 ) ) ∧ ( 𝑓 +ℎ 𝑔 ) = ( 𝑣 +ℎ 𝑢 ) ) ) → ( 𝑥 −ℎ 𝑧 ) ∈ ( ( ( ( 𝐴 +ℋ 𝐶 ) ∩ ( 𝐵 +ℋ 𝐷 ) ) ∩ ( ( ( 𝐴 +ℋ 𝑅 ) ∩ ( 𝐵 +ℋ 𝑆 ) ) +ℋ ( ( 𝐶 +ℋ 𝑅 ) ∩ ( 𝐷 +ℋ 𝑆 ) ) ) ) ∩ ( ( ( ( 𝐴 +ℋ 𝐹 ) ∩ ( 𝐵 +ℋ 𝐺 ) ) ∩ ( ( ( 𝐴 +ℋ 𝑅 ) ∩ ( 𝐵 +ℋ 𝑆 ) ) +ℋ ( ( 𝐹 +ℋ 𝑅 ) ∩ ( 𝐺 +ℋ 𝑆 ) ) ) ) +ℋ ( ( ( 𝐶 +ℋ 𝐹 ) ∩ ( 𝐷 +ℋ 𝐺 ) ) ∩ ( ( ( 𝐶 +ℋ 𝑅 ) ∩ ( 𝐷 +ℋ 𝑆 ) ) +ℋ ( ( 𝐹 +ℋ 𝑅 ) ∩ ( 𝐺 +ℋ 𝑆 ) ) ) ) ) ) )