Theorem 5oalem7

Description: Lemma for orthoarguesian law 5OA. (Contributed by NM, 4-May-2000) TODO: replace uses of ee4anv with 4exdistrv as in 3oalem3 . (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	5oalem7	⊢ ( ( ( 𝐴 +ℋ 𝐵 ) ∩ ( 𝐶 +ℋ 𝐷 ) ) ∩ ( ( 𝐹 +ℋ 𝐺 ) ∩ ( 𝑅 +ℋ 𝑆 ) ) ) ⊆ ( 𝐵 +ℋ ( 𝐴 ∩ ( 𝐶 +ℋ ( ( ( ( 𝐴 +ℋ 𝐶 ) ∩ ( 𝐵 +ℋ 𝐷 ) ) ∩ ( ( ( 𝐴 +ℋ 𝑅 ) ∩ ( 𝐵 +ℋ 𝑆 ) ) +ℋ ( ( 𝐶 +ℋ 𝑅 ) ∩ ( 𝐷 +ℋ 𝑆 ) ) ) ) ∩ ( ( ( ( 𝐴 +ℋ 𝐹 ) ∩ ( 𝐵 +ℋ 𝐺 ) ) ∩ ( ( ( 𝐴 +ℋ 𝑅 ) ∩ ( 𝐵 +ℋ 𝑆 ) ) +ℋ ( ( 𝐹 +ℋ 𝑅 ) ∩ ( 𝐺 +ℋ 𝑆 ) ) ) ) +ℋ ( ( ( 𝐶 +ℋ 𝐹 ) ∩ ( 𝐷 +ℋ 𝐺 ) ) ∩ ( ( ( 𝐶 +ℋ 𝑅 ) ∩ ( 𝐷 +ℋ 𝑆 ) ) +ℋ ( ( 𝐹 +ℋ 𝑅 ) ∩ ( 𝐺 +ℋ 𝑆 ) ) ) ) ) ) ) ) )

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		ee4anv	⊢ ( ∃ 𝑥 ∃ 𝑦 ∃ 𝑓 ∃ 𝑔 ( ∃ 𝑧 ∃ 𝑤 ( ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ∧ ℎ = ( 𝑥 +ℎ 𝑦 ) ) ∧ ( ( 𝑧 ∈ 𝐶 ∧ 𝑤 ∈ 𝐷 ) ∧ ℎ = ( 𝑧 +ℎ 𝑤 ) ) ) ∧ ∃ 𝑣 ∃ 𝑢 ( ( ( 𝑓 ∈ 𝐹 ∧ 𝑔 ∈ 𝐺 ) ∧ ℎ = ( 𝑓 +ℎ 𝑔 ) ) ∧ ( ( 𝑣 ∈ 𝑅 ∧ 𝑢 ∈ 𝑆 ) ∧ ℎ = ( 𝑣 +ℎ 𝑢 ) ) ) ) ↔ ( ∃ 𝑥 ∃ 𝑦 ∃ 𝑧 ∃ 𝑤 ( ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ∧ ℎ = ( 𝑥 +ℎ 𝑦 ) ) ∧ ( ( 𝑧 ∈ 𝐶 ∧ 𝑤 ∈ 𝐷 ) ∧ ℎ = ( 𝑧 +ℎ 𝑤 ) ) ) ∧ ∃ 𝑓 ∃ 𝑔 ∃ 𝑣 ∃ 𝑢 ( ( ( 𝑓 ∈ 𝐹 ∧ 𝑔 ∈ 𝐺 ) ∧ ℎ = ( 𝑓 +ℎ 𝑔 ) ) ∧ ( ( 𝑣 ∈ 𝑅 ∧ 𝑢 ∈ 𝑆 ) ∧ ℎ = ( 𝑣 +ℎ 𝑢 ) ) ) ) )
10		exrot4	⊢ ( ∃ 𝑧 ∃ 𝑤 ∃ 𝑓 ∃ 𝑔 ∃ 𝑣 ∃ 𝑢 ( ( ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ∧ ℎ = ( 𝑥 +ℎ 𝑦 ) ) ∧ ( ( 𝑧 ∈ 𝐶 ∧ 𝑤 ∈ 𝐷 ) ∧ ℎ = ( 𝑧 +ℎ 𝑤 ) ) ) ∧ ( ( ( 𝑓 ∈ 𝐹 ∧ 𝑔 ∈ 𝐺 ) ∧ ℎ = ( 𝑓 +ℎ 𝑔 ) ) ∧ ( ( 𝑣 ∈ 𝑅 ∧ 𝑢 ∈ 𝑆 ) ∧ ℎ = ( 𝑣 +ℎ 𝑢 ) ) ) ) ↔ ∃ 𝑓 ∃ 𝑔 ∃ 𝑧 ∃ 𝑤 ∃ 𝑣 ∃ 𝑢 ( ( ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ∧ ℎ = ( 𝑥 +ℎ 𝑦 ) ) ∧ ( ( 𝑧 ∈ 𝐶 ∧ 𝑤 ∈ 𝐷 ) ∧ ℎ = ( 𝑧 +ℎ 𝑤 ) ) ) ∧ ( ( ( 𝑓 ∈ 𝐹 ∧ 𝑔 ∈ 𝐺 ) ∧ ℎ = ( 𝑓 +ℎ 𝑔 ) ) ∧ ( ( 𝑣 ∈ 𝑅 ∧ 𝑢 ∈ 𝑆 ) ∧ ℎ = ( 𝑣 +ℎ 𝑢 ) ) ) ) )
11		ee4anv	⊢ ( ∃ 𝑧 ∃ 𝑤 ∃ 𝑣 ∃ 𝑢 ( ( ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ∧ ℎ = ( 𝑥 +ℎ 𝑦 ) ) ∧ ( ( 𝑧 ∈ 𝐶 ∧ 𝑤 ∈ 𝐷 ) ∧ ℎ = ( 𝑧 +ℎ 𝑤 ) ) ) ∧ ( ( ( 𝑓 ∈ 𝐹 ∧ 𝑔 ∈ 𝐺 ) ∧ ℎ = ( 𝑓 +ℎ 𝑔 ) ) ∧ ( ( 𝑣 ∈ 𝑅 ∧ 𝑢 ∈ 𝑆 ) ∧ ℎ = ( 𝑣 +ℎ 𝑢 ) ) ) ) ↔ ( ∃ 𝑧 ∃ 𝑤 ( ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ∧ ℎ = ( 𝑥 +ℎ 𝑦 ) ) ∧ ( ( 𝑧 ∈ 𝐶 ∧ 𝑤 ∈ 𝐷 ) ∧ ℎ = ( 𝑧 +ℎ 𝑤 ) ) ) ∧ ∃ 𝑣 ∃ 𝑢 ( ( ( 𝑓 ∈ 𝐹 ∧ 𝑔 ∈ 𝐺 ) ∧ ℎ = ( 𝑓 +ℎ 𝑔 ) ) ∧ ( ( 𝑣 ∈ 𝑅 ∧ 𝑢 ∈ 𝑆 ) ∧ ℎ = ( 𝑣 +ℎ 𝑢 ) ) ) ) )
12	11	2exbii	⊢ ( ∃ 𝑓 ∃ 𝑔 ∃ 𝑧 ∃ 𝑤 ∃ 𝑣 ∃ 𝑢 ( ( ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ∧ ℎ = ( 𝑥 +ℎ 𝑦 ) ) ∧ ( ( 𝑧 ∈ 𝐶 ∧ 𝑤 ∈ 𝐷 ) ∧ ℎ = ( 𝑧 +ℎ 𝑤 ) ) ) ∧ ( ( ( 𝑓 ∈ 𝐹 ∧ 𝑔 ∈ 𝐺 ) ∧ ℎ = ( 𝑓 +ℎ 𝑔 ) ) ∧ ( ( 𝑣 ∈ 𝑅 ∧ 𝑢 ∈ 𝑆 ) ∧ ℎ = ( 𝑣 +ℎ 𝑢 ) ) ) ) ↔ ∃ 𝑓 ∃ 𝑔 ( ∃ 𝑧 ∃ 𝑤 ( ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ∧ ℎ = ( 𝑥 +ℎ 𝑦 ) ) ∧ ( ( 𝑧 ∈ 𝐶 ∧ 𝑤 ∈ 𝐷 ) ∧ ℎ = ( 𝑧 +ℎ 𝑤 ) ) ) ∧ ∃ 𝑣 ∃ 𝑢 ( ( ( 𝑓 ∈ 𝐹 ∧ 𝑔 ∈ 𝐺 ) ∧ ℎ = ( 𝑓 +ℎ 𝑔 ) ) ∧ ( ( 𝑣 ∈ 𝑅 ∧ 𝑢 ∈ 𝑆 ) ∧ ℎ = ( 𝑣 +ℎ 𝑢 ) ) ) ) )
13	10 12	bitri	⊢ ( ∃ 𝑧 ∃ 𝑤 ∃ 𝑓 ∃ 𝑔 ∃ 𝑣 ∃ 𝑢 ( ( ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ∧ ℎ = ( 𝑥 +ℎ 𝑦 ) ) ∧ ( ( 𝑧 ∈ 𝐶 ∧ 𝑤 ∈ 𝐷 ) ∧ ℎ = ( 𝑧 +ℎ 𝑤 ) ) ) ∧ ( ( ( 𝑓 ∈ 𝐹 ∧ 𝑔 ∈ 𝐺 ) ∧ ℎ = ( 𝑓 +ℎ 𝑔 ) ) ∧ ( ( 𝑣 ∈ 𝑅 ∧ 𝑢 ∈ 𝑆 ) ∧ ℎ = ( 𝑣 +ℎ 𝑢 ) ) ) ) ↔ ∃ 𝑓 ∃ 𝑔 ( ∃ 𝑧 ∃ 𝑤 ( ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ∧ ℎ = ( 𝑥 +ℎ 𝑦 ) ) ∧ ( ( 𝑧 ∈ 𝐶 ∧ 𝑤 ∈ 𝐷 ) ∧ ℎ = ( 𝑧 +ℎ 𝑤 ) ) ) ∧ ∃ 𝑣 ∃ 𝑢 ( ( ( 𝑓 ∈ 𝐹 ∧ 𝑔 ∈ 𝐺 ) ∧ ℎ = ( 𝑓 +ℎ 𝑔 ) ) ∧ ( ( 𝑣 ∈ 𝑅 ∧ 𝑢 ∈ 𝑆 ) ∧ ℎ = ( 𝑣 +ℎ 𝑢 ) ) ) ) )
14	13	2exbii	⊢ ( ∃ 𝑥 ∃ 𝑦 ∃ 𝑧 ∃ 𝑤 ∃ 𝑓 ∃ 𝑔 ∃ 𝑣 ∃ 𝑢 ( ( ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ∧ ℎ = ( 𝑥 +ℎ 𝑦 ) ) ∧ ( ( 𝑧 ∈ 𝐶 ∧ 𝑤 ∈ 𝐷 ) ∧ ℎ = ( 𝑧 +ℎ 𝑤 ) ) ) ∧ ( ( ( 𝑓 ∈ 𝐹 ∧ 𝑔 ∈ 𝐺 ) ∧ ℎ = ( 𝑓 +ℎ 𝑔 ) ) ∧ ( ( 𝑣 ∈ 𝑅 ∧ 𝑢 ∈ 𝑆 ) ∧ ℎ = ( 𝑣 +ℎ 𝑢 ) ) ) ) ↔ ∃ 𝑥 ∃ 𝑦 ∃ 𝑓 ∃ 𝑔 ( ∃ 𝑧 ∃ 𝑤 ( ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ∧ ℎ = ( 𝑥 +ℎ 𝑦 ) ) ∧ ( ( 𝑧 ∈ 𝐶 ∧ 𝑤 ∈ 𝐷 ) ∧ ℎ = ( 𝑧 +ℎ 𝑤 ) ) ) ∧ ∃ 𝑣 ∃ 𝑢 ( ( ( 𝑓 ∈ 𝐹 ∧ 𝑔 ∈ 𝐺 ) ∧ ℎ = ( 𝑓 +ℎ 𝑔 ) ) ∧ ( ( 𝑣 ∈ 𝑅 ∧ 𝑢 ∈ 𝑆 ) ∧ ℎ = ( 𝑣 +ℎ 𝑢 ) ) ) ) )
15		elin	⊢ ( ℎ ∈ ( ( ( 𝐴 +ℋ 𝐵 ) ∩ ( 𝐶 +ℋ 𝐷 ) ) ∩ ( ( 𝐹 +ℋ 𝐺 ) ∩ ( 𝑅 +ℋ 𝑆 ) ) ) ↔ ( ℎ ∈ ( ( 𝐴 +ℋ 𝐵 ) ∩ ( 𝐶 +ℋ 𝐷 ) ) ∧ ℎ ∈ ( ( 𝐹 +ℋ 𝐺 ) ∩ ( 𝑅 +ℋ 𝑆 ) ) ) )
16	1 2	shseli	⊢ ( ℎ ∈ ( 𝐴 +ℋ 𝐵 ) ↔ ∃ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 ℎ = ( 𝑥 +ℎ 𝑦 ) )
17		r2ex	⊢ ( ∃ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 ℎ = ( 𝑥 +ℎ 𝑦 ) ↔ ∃ 𝑥 ∃ 𝑦 ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ∧ ℎ = ( 𝑥 +ℎ 𝑦 ) ) )
18	16 17	bitri	⊢ ( ℎ ∈ ( 𝐴 +ℋ 𝐵 ) ↔ ∃ 𝑥 ∃ 𝑦 ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ∧ ℎ = ( 𝑥 +ℎ 𝑦 ) ) )
19	3 4	shseli	⊢ ( ℎ ∈ ( 𝐶 +ℋ 𝐷 ) ↔ ∃ 𝑧 ∈ 𝐶 ∃ 𝑤 ∈ 𝐷 ℎ = ( 𝑧 +ℎ 𝑤 ) )
20		r2ex	⊢ ( ∃ 𝑧 ∈ 𝐶 ∃ 𝑤 ∈ 𝐷 ℎ = ( 𝑧 +ℎ 𝑤 ) ↔ ∃ 𝑧 ∃ 𝑤 ( ( 𝑧 ∈ 𝐶 ∧ 𝑤 ∈ 𝐷 ) ∧ ℎ = ( 𝑧 +ℎ 𝑤 ) ) )
21	19 20	bitri	⊢ ( ℎ ∈ ( 𝐶 +ℋ 𝐷 ) ↔ ∃ 𝑧 ∃ 𝑤 ( ( 𝑧 ∈ 𝐶 ∧ 𝑤 ∈ 𝐷 ) ∧ ℎ = ( 𝑧 +ℎ 𝑤 ) ) )
22	18 21	anbi12i	⊢ ( ( ℎ ∈ ( 𝐴 +ℋ 𝐵 ) ∧ ℎ ∈ ( 𝐶 +ℋ 𝐷 ) ) ↔ ( ∃ 𝑥 ∃ 𝑦 ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ∧ ℎ = ( 𝑥 +ℎ 𝑦 ) ) ∧ ∃ 𝑧 ∃ 𝑤 ( ( 𝑧 ∈ 𝐶 ∧ 𝑤 ∈ 𝐷 ) ∧ ℎ = ( 𝑧 +ℎ 𝑤 ) ) ) )
23		elin	⊢ ( ℎ ∈ ( ( 𝐴 +ℋ 𝐵 ) ∩ ( 𝐶 +ℋ 𝐷 ) ) ↔ ( ℎ ∈ ( 𝐴 +ℋ 𝐵 ) ∧ ℎ ∈ ( 𝐶 +ℋ 𝐷 ) ) )
24		ee4anv	⊢ ( ∃ 𝑥 ∃ 𝑦 ∃ 𝑧 ∃ 𝑤 ( ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ∧ ℎ = ( 𝑥 +ℎ 𝑦 ) ) ∧ ( ( 𝑧 ∈ 𝐶 ∧ 𝑤 ∈ 𝐷 ) ∧ ℎ = ( 𝑧 +ℎ 𝑤 ) ) ) ↔ ( ∃ 𝑥 ∃ 𝑦 ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ∧ ℎ = ( 𝑥 +ℎ 𝑦 ) ) ∧ ∃ 𝑧 ∃ 𝑤 ( ( 𝑧 ∈ 𝐶 ∧ 𝑤 ∈ 𝐷 ) ∧ ℎ = ( 𝑧 +ℎ 𝑤 ) ) ) )
25	22 23 24	3bitr4ri	⊢ ( ∃ 𝑥 ∃ 𝑦 ∃ 𝑧 ∃ 𝑤 ( ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ∧ ℎ = ( 𝑥 +ℎ 𝑦 ) ) ∧ ( ( 𝑧 ∈ 𝐶 ∧ 𝑤 ∈ 𝐷 ) ∧ ℎ = ( 𝑧 +ℎ 𝑤 ) ) ) ↔ ℎ ∈ ( ( 𝐴 +ℋ 𝐵 ) ∩ ( 𝐶 +ℋ 𝐷 ) ) )
26	5 6	shseli	⊢ ( ℎ ∈ ( 𝐹 +ℋ 𝐺 ) ↔ ∃ 𝑓 ∈ 𝐹 ∃ 𝑔 ∈ 𝐺 ℎ = ( 𝑓 +ℎ 𝑔 ) )
27		r2ex	⊢ ( ∃ 𝑓 ∈ 𝐹 ∃ 𝑔 ∈ 𝐺 ℎ = ( 𝑓 +ℎ 𝑔 ) ↔ ∃ 𝑓 ∃ 𝑔 ( ( 𝑓 ∈ 𝐹 ∧ 𝑔 ∈ 𝐺 ) ∧ ℎ = ( 𝑓 +ℎ 𝑔 ) ) )
28	26 27	bitri	⊢ ( ℎ ∈ ( 𝐹 +ℋ 𝐺 ) ↔ ∃ 𝑓 ∃ 𝑔 ( ( 𝑓 ∈ 𝐹 ∧ 𝑔 ∈ 𝐺 ) ∧ ℎ = ( 𝑓 +ℎ 𝑔 ) ) )
29	7 8	shseli	⊢ ( ℎ ∈ ( 𝑅 +ℋ 𝑆 ) ↔ ∃ 𝑣 ∈ 𝑅 ∃ 𝑢 ∈ 𝑆 ℎ = ( 𝑣 +ℎ 𝑢 ) )
30		r2ex	⊢ ( ∃ 𝑣 ∈ 𝑅 ∃ 𝑢 ∈ 𝑆 ℎ = ( 𝑣 +ℎ 𝑢 ) ↔ ∃ 𝑣 ∃ 𝑢 ( ( 𝑣 ∈ 𝑅 ∧ 𝑢 ∈ 𝑆 ) ∧ ℎ = ( 𝑣 +ℎ 𝑢 ) ) )
31	29 30	bitri	⊢ ( ℎ ∈ ( 𝑅 +ℋ 𝑆 ) ↔ ∃ 𝑣 ∃ 𝑢 ( ( 𝑣 ∈ 𝑅 ∧ 𝑢 ∈ 𝑆 ) ∧ ℎ = ( 𝑣 +ℎ 𝑢 ) ) )
32	28 31	anbi12i	⊢ ( ( ℎ ∈ ( 𝐹 +ℋ 𝐺 ) ∧ ℎ ∈ ( 𝑅 +ℋ 𝑆 ) ) ↔ ( ∃ 𝑓 ∃ 𝑔 ( ( 𝑓 ∈ 𝐹 ∧ 𝑔 ∈ 𝐺 ) ∧ ℎ = ( 𝑓 +ℎ 𝑔 ) ) ∧ ∃ 𝑣 ∃ 𝑢 ( ( 𝑣 ∈ 𝑅 ∧ 𝑢 ∈ 𝑆 ) ∧ ℎ = ( 𝑣 +ℎ 𝑢 ) ) ) )
33		elin	⊢ ( ℎ ∈ ( ( 𝐹 +ℋ 𝐺 ) ∩ ( 𝑅 +ℋ 𝑆 ) ) ↔ ( ℎ ∈ ( 𝐹 +ℋ 𝐺 ) ∧ ℎ ∈ ( 𝑅 +ℋ 𝑆 ) ) )
34		ee4anv	⊢ ( ∃ 𝑓 ∃ 𝑔 ∃ 𝑣 ∃ 𝑢 ( ( ( 𝑓 ∈ 𝐹 ∧ 𝑔 ∈ 𝐺 ) ∧ ℎ = ( 𝑓 +ℎ 𝑔 ) ) ∧ ( ( 𝑣 ∈ 𝑅 ∧ 𝑢 ∈ 𝑆 ) ∧ ℎ = ( 𝑣 +ℎ 𝑢 ) ) ) ↔ ( ∃ 𝑓 ∃ 𝑔 ( ( 𝑓 ∈ 𝐹 ∧ 𝑔 ∈ 𝐺 ) ∧ ℎ = ( 𝑓 +ℎ 𝑔 ) ) ∧ ∃ 𝑣 ∃ 𝑢 ( ( 𝑣 ∈ 𝑅 ∧ 𝑢 ∈ 𝑆 ) ∧ ℎ = ( 𝑣 +ℎ 𝑢 ) ) ) )
35	32 33 34	3bitr4ri	⊢ ( ∃ 𝑓 ∃ 𝑔 ∃ 𝑣 ∃ 𝑢 ( ( ( 𝑓 ∈ 𝐹 ∧ 𝑔 ∈ 𝐺 ) ∧ ℎ = ( 𝑓 +ℎ 𝑔 ) ) ∧ ( ( 𝑣 ∈ 𝑅 ∧ 𝑢 ∈ 𝑆 ) ∧ ℎ = ( 𝑣 +ℎ 𝑢 ) ) ) ↔ ℎ ∈ ( ( 𝐹 +ℋ 𝐺 ) ∩ ( 𝑅 +ℋ 𝑆 ) ) )
36	25 35	anbi12i	⊢ ( ( ∃ 𝑥 ∃ 𝑦 ∃ 𝑧 ∃ 𝑤 ( ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ∧ ℎ = ( 𝑥 +ℎ 𝑦 ) ) ∧ ( ( 𝑧 ∈ 𝐶 ∧ 𝑤 ∈ 𝐷 ) ∧ ℎ = ( 𝑧 +ℎ 𝑤 ) ) ) ∧ ∃ 𝑓 ∃ 𝑔 ∃ 𝑣 ∃ 𝑢 ( ( ( 𝑓 ∈ 𝐹 ∧ 𝑔 ∈ 𝐺 ) ∧ ℎ = ( 𝑓 +ℎ 𝑔 ) ) ∧ ( ( 𝑣 ∈ 𝑅 ∧ 𝑢 ∈ 𝑆 ) ∧ ℎ = ( 𝑣 +ℎ 𝑢 ) ) ) ) ↔ ( ℎ ∈ ( ( 𝐴 +ℋ 𝐵 ) ∩ ( 𝐶 +ℋ 𝐷 ) ) ∧ ℎ ∈ ( ( 𝐹 +ℋ 𝐺 ) ∩ ( 𝑅 +ℋ 𝑆 ) ) ) )
37	15 36	bitr4i	⊢ ( ℎ ∈ ( ( ( 𝐴 +ℋ 𝐵 ) ∩ ( 𝐶 +ℋ 𝐷 ) ) ∩ ( ( 𝐹 +ℋ 𝐺 ) ∩ ( 𝑅 +ℋ 𝑆 ) ) ) ↔ ( ∃ 𝑥 ∃ 𝑦 ∃ 𝑧 ∃ 𝑤 ( ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ∧ ℎ = ( 𝑥 +ℎ 𝑦 ) ) ∧ ( ( 𝑧 ∈ 𝐶 ∧ 𝑤 ∈ 𝐷 ) ∧ ℎ = ( 𝑧 +ℎ 𝑤 ) ) ) ∧ ∃ 𝑓 ∃ 𝑔 ∃ 𝑣 ∃ 𝑢 ( ( ( 𝑓 ∈ 𝐹 ∧ 𝑔 ∈ 𝐺 ) ∧ ℎ = ( 𝑓 +ℎ 𝑔 ) ) ∧ ( ( 𝑣 ∈ 𝑅 ∧ 𝑢 ∈ 𝑆 ) ∧ ℎ = ( 𝑣 +ℎ 𝑢 ) ) ) ) )
38	9 14 37	3bitr4ri	⊢ ( ℎ ∈ ( ( ( 𝐴 +ℋ 𝐵 ) ∩ ( 𝐶 +ℋ 𝐷 ) ) ∩ ( ( 𝐹 +ℋ 𝐺 ) ∩ ( 𝑅 +ℋ 𝑆 ) ) ) ↔ ∃ 𝑥 ∃ 𝑦 ∃ 𝑧 ∃ 𝑤 ∃ 𝑓 ∃ 𝑔 ∃ 𝑣 ∃ 𝑢 ( ( ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ∧ ℎ = ( 𝑥 +ℎ 𝑦 ) ) ∧ ( ( 𝑧 ∈ 𝐶 ∧ 𝑤 ∈ 𝐷 ) ∧ ℎ = ( 𝑧 +ℎ 𝑤 ) ) ) ∧ ( ( ( 𝑓 ∈ 𝐹 ∧ 𝑔 ∈ 𝐺 ) ∧ ℎ = ( 𝑓 +ℎ 𝑔 ) ) ∧ ( ( 𝑣 ∈ 𝑅 ∧ 𝑢 ∈ 𝑆 ) ∧ ℎ = ( 𝑣 +ℎ 𝑢 ) ) ) ) )
39	1 2 3 4 5 6 7 8	5oalem6	⊢ ( ( ( ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ∧ ℎ = ( 𝑥 +ℎ 𝑦 ) ) ∧ ( ( 𝑧 ∈ 𝐶 ∧ 𝑤 ∈ 𝐷 ) ∧ ℎ = ( 𝑧 +ℎ 𝑤 ) ) ) ∧ ( ( ( 𝑓 ∈ 𝐹 ∧ 𝑔 ∈ 𝐺 ) ∧ ℎ = ( 𝑓 +ℎ 𝑔 ) ) ∧ ( ( 𝑣 ∈ 𝑅 ∧ 𝑢 ∈ 𝑆 ) ∧ ℎ = ( 𝑣 +ℎ 𝑢 ) ) ) ) → ℎ ∈ ( 𝐵 +ℋ ( 𝐴 ∩ ( 𝐶 +ℋ ( ( ( ( 𝐴 +ℋ 𝐶 ) ∩ ( 𝐵 +ℋ 𝐷 ) ) ∩ ( ( ( 𝐴 +ℋ 𝑅 ) ∩ ( 𝐵 +ℋ 𝑆 ) ) +ℋ ( ( 𝐶 +ℋ 𝑅 ) ∩ ( 𝐷 +ℋ 𝑆 ) ) ) ) ∩ ( ( ( ( 𝐴 +ℋ 𝐹 ) ∩ ( 𝐵 +ℋ 𝐺 ) ) ∩ ( ( ( 𝐴 +ℋ 𝑅 ) ∩ ( 𝐵 +ℋ 𝑆 ) ) +ℋ ( ( 𝐹 +ℋ 𝑅 ) ∩ ( 𝐺 +ℋ 𝑆 ) ) ) ) +ℋ ( ( ( 𝐶 +ℋ 𝐹 ) ∩ ( 𝐷 +ℋ 𝐺 ) ) ∩ ( ( ( 𝐶 +ℋ 𝑅 ) ∩ ( 𝐷 +ℋ 𝑆 ) ) +ℋ ( ( 𝐹 +ℋ 𝑅 ) ∩ ( 𝐺 +ℋ 𝑆 ) ) ) ) ) ) ) ) ) )
40	39	exlimivv	⊢ ( ∃ 𝑣 ∃ 𝑢 ( ( ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ∧ ℎ = ( 𝑥 +ℎ 𝑦 ) ) ∧ ( ( 𝑧 ∈ 𝐶 ∧ 𝑤 ∈ 𝐷 ) ∧ ℎ = ( 𝑧 +ℎ 𝑤 ) ) ) ∧ ( ( ( 𝑓 ∈ 𝐹 ∧ 𝑔 ∈ 𝐺 ) ∧ ℎ = ( 𝑓 +ℎ 𝑔 ) ) ∧ ( ( 𝑣 ∈ 𝑅 ∧ 𝑢 ∈ 𝑆 ) ∧ ℎ = ( 𝑣 +ℎ 𝑢 ) ) ) ) → ℎ ∈ ( 𝐵 +ℋ ( 𝐴 ∩ ( 𝐶 +ℋ ( ( ( ( 𝐴 +ℋ 𝐶 ) ∩ ( 𝐵 +ℋ 𝐷 ) ) ∩ ( ( ( 𝐴 +ℋ 𝑅 ) ∩ ( 𝐵 +ℋ 𝑆 ) ) +ℋ ( ( 𝐶 +ℋ 𝑅 ) ∩ ( 𝐷 +ℋ 𝑆 ) ) ) ) ∩ ( ( ( ( 𝐴 +ℋ 𝐹 ) ∩ ( 𝐵 +ℋ 𝐺 ) ) ∩ ( ( ( 𝐴 +ℋ 𝑅 ) ∩ ( 𝐵 +ℋ 𝑆 ) ) +ℋ ( ( 𝐹 +ℋ 𝑅 ) ∩ ( 𝐺 +ℋ 𝑆 ) ) ) ) +ℋ ( ( ( 𝐶 +ℋ 𝐹 ) ∩ ( 𝐷 +ℋ 𝐺 ) ) ∩ ( ( ( 𝐶 +ℋ 𝑅 ) ∩ ( 𝐷 +ℋ 𝑆 ) ) +ℋ ( ( 𝐹 +ℋ 𝑅 ) ∩ ( 𝐺 +ℋ 𝑆 ) ) ) ) ) ) ) ) ) )
41	40	exlimivv	⊢ ( ∃ 𝑓 ∃ 𝑔 ∃ 𝑣 ∃ 𝑢 ( ( ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ∧ ℎ = ( 𝑥 +ℎ 𝑦 ) ) ∧ ( ( 𝑧 ∈ 𝐶 ∧ 𝑤 ∈ 𝐷 ) ∧ ℎ = ( 𝑧 +ℎ 𝑤 ) ) ) ∧ ( ( ( 𝑓 ∈ 𝐹 ∧ 𝑔 ∈ 𝐺 ) ∧ ℎ = ( 𝑓 +ℎ 𝑔 ) ) ∧ ( ( 𝑣 ∈ 𝑅 ∧ 𝑢 ∈ 𝑆 ) ∧ ℎ = ( 𝑣 +ℎ 𝑢 ) ) ) ) → ℎ ∈ ( 𝐵 +ℋ ( 𝐴 ∩ ( 𝐶 +ℋ ( ( ( ( 𝐴 +ℋ 𝐶 ) ∩ ( 𝐵 +ℋ 𝐷 ) ) ∩ ( ( ( 𝐴 +ℋ 𝑅 ) ∩ ( 𝐵 +ℋ 𝑆 ) ) +ℋ ( ( 𝐶 +ℋ 𝑅 ) ∩ ( 𝐷 +ℋ 𝑆 ) ) ) ) ∩ ( ( ( ( 𝐴 +ℋ 𝐹 ) ∩ ( 𝐵 +ℋ 𝐺 ) ) ∩ ( ( ( 𝐴 +ℋ 𝑅 ) ∩ ( 𝐵 +ℋ 𝑆 ) ) +ℋ ( ( 𝐹 +ℋ 𝑅 ) ∩ ( 𝐺 +ℋ 𝑆 ) ) ) ) +ℋ ( ( ( 𝐶 +ℋ 𝐹 ) ∩ ( 𝐷 +ℋ 𝐺 ) ) ∩ ( ( ( 𝐶 +ℋ 𝑅 ) ∩ ( 𝐷 +ℋ 𝑆 ) ) +ℋ ( ( 𝐹 +ℋ 𝑅 ) ∩ ( 𝐺 +ℋ 𝑆 ) ) ) ) ) ) ) ) ) )
42	41	exlimivv	⊢ ( ∃ 𝑧 ∃ 𝑤 ∃ 𝑓 ∃ 𝑔 ∃ 𝑣 ∃ 𝑢 ( ( ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ∧ ℎ = ( 𝑥 +ℎ 𝑦 ) ) ∧ ( ( 𝑧 ∈ 𝐶 ∧ 𝑤 ∈ 𝐷 ) ∧ ℎ = ( 𝑧 +ℎ 𝑤 ) ) ) ∧ ( ( ( 𝑓 ∈ 𝐹 ∧ 𝑔 ∈ 𝐺 ) ∧ ℎ = ( 𝑓 +ℎ 𝑔 ) ) ∧ ( ( 𝑣 ∈ 𝑅 ∧ 𝑢 ∈ 𝑆 ) ∧ ℎ = ( 𝑣 +ℎ 𝑢 ) ) ) ) → ℎ ∈ ( 𝐵 +ℋ ( 𝐴 ∩ ( 𝐶 +ℋ ( ( ( ( 𝐴 +ℋ 𝐶 ) ∩ ( 𝐵 +ℋ 𝐷 ) ) ∩ ( ( ( 𝐴 +ℋ 𝑅 ) ∩ ( 𝐵 +ℋ 𝑆 ) ) +ℋ ( ( 𝐶 +ℋ 𝑅 ) ∩ ( 𝐷 +ℋ 𝑆 ) ) ) ) ∩ ( ( ( ( 𝐴 +ℋ 𝐹 ) ∩ ( 𝐵 +ℋ 𝐺 ) ) ∩ ( ( ( 𝐴 +ℋ 𝑅 ) ∩ ( 𝐵 +ℋ 𝑆 ) ) +ℋ ( ( 𝐹 +ℋ 𝑅 ) ∩ ( 𝐺 +ℋ 𝑆 ) ) ) ) +ℋ ( ( ( 𝐶 +ℋ 𝐹 ) ∩ ( 𝐷 +ℋ 𝐺 ) ) ∩ ( ( ( 𝐶 +ℋ 𝑅 ) ∩ ( 𝐷 +ℋ 𝑆 ) ) +ℋ ( ( 𝐹 +ℋ 𝑅 ) ∩ ( 𝐺 +ℋ 𝑆 ) ) ) ) ) ) ) ) ) )
43	42	exlimivv	⊢ ( ∃ 𝑥 ∃ 𝑦 ∃ 𝑧 ∃ 𝑤 ∃ 𝑓 ∃ 𝑔 ∃ 𝑣 ∃ 𝑢 ( ( ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ∧ ℎ = ( 𝑥 +ℎ 𝑦 ) ) ∧ ( ( 𝑧 ∈ 𝐶 ∧ 𝑤 ∈ 𝐷 ) ∧ ℎ = ( 𝑧 +ℎ 𝑤 ) ) ) ∧ ( ( ( 𝑓 ∈ 𝐹 ∧ 𝑔 ∈ 𝐺 ) ∧ ℎ = ( 𝑓 +ℎ 𝑔 ) ) ∧ ( ( 𝑣 ∈ 𝑅 ∧ 𝑢 ∈ 𝑆 ) ∧ ℎ = ( 𝑣 +ℎ 𝑢 ) ) ) ) → ℎ ∈ ( 𝐵 +ℋ ( 𝐴 ∩ ( 𝐶 +ℋ ( ( ( ( 𝐴 +ℋ 𝐶 ) ∩ ( 𝐵 +ℋ 𝐷 ) ) ∩ ( ( ( 𝐴 +ℋ 𝑅 ) ∩ ( 𝐵 +ℋ 𝑆 ) ) +ℋ ( ( 𝐶 +ℋ 𝑅 ) ∩ ( 𝐷 +ℋ 𝑆 ) ) ) ) ∩ ( ( ( ( 𝐴 +ℋ 𝐹 ) ∩ ( 𝐵 +ℋ 𝐺 ) ) ∩ ( ( ( 𝐴 +ℋ 𝑅 ) ∩ ( 𝐵 +ℋ 𝑆 ) ) +ℋ ( ( 𝐹 +ℋ 𝑅 ) ∩ ( 𝐺 +ℋ 𝑆 ) ) ) ) +ℋ ( ( ( 𝐶 +ℋ 𝐹 ) ∩ ( 𝐷 +ℋ 𝐺 ) ) ∩ ( ( ( 𝐶 +ℋ 𝑅 ) ∩ ( 𝐷 +ℋ 𝑆 ) ) +ℋ ( ( 𝐹 +ℋ 𝑅 ) ∩ ( 𝐺 +ℋ 𝑆 ) ) ) ) ) ) ) ) ) )
44	38 43	sylbi	⊢ ( ℎ ∈ ( ( ( 𝐴 +ℋ 𝐵 ) ∩ ( 𝐶 +ℋ 𝐷 ) ) ∩ ( ( 𝐹 +ℋ 𝐺 ) ∩ ( 𝑅 +ℋ 𝑆 ) ) ) → ℎ ∈ ( 𝐵 +ℋ ( 𝐴 ∩ ( 𝐶 +ℋ ( ( ( ( 𝐴 +ℋ 𝐶 ) ∩ ( 𝐵 +ℋ 𝐷 ) ) ∩ ( ( ( 𝐴 +ℋ 𝑅 ) ∩ ( 𝐵 +ℋ 𝑆 ) ) +ℋ ( ( 𝐶 +ℋ 𝑅 ) ∩ ( 𝐷 +ℋ 𝑆 ) ) ) ) ∩ ( ( ( ( 𝐴 +ℋ 𝐹 ) ∩ ( 𝐵 +ℋ 𝐺 ) ) ∩ ( ( ( 𝐴 +ℋ 𝑅 ) ∩ ( 𝐵 +ℋ 𝑆 ) ) +ℋ ( ( 𝐹 +ℋ 𝑅 ) ∩ ( 𝐺 +ℋ 𝑆 ) ) ) ) +ℋ ( ( ( 𝐶 +ℋ 𝐹 ) ∩ ( 𝐷 +ℋ 𝐺 ) ) ∩ ( ( ( 𝐶 +ℋ 𝑅 ) ∩ ( 𝐷 +ℋ 𝑆 ) ) +ℋ ( ( 𝐹 +ℋ 𝑅 ) ∩ ( 𝐺 +ℋ 𝑆 ) ) ) ) ) ) ) ) ) )
45	44	ssriv	⊢ ( ( ( 𝐴 +ℋ 𝐵 ) ∩ ( 𝐶 +ℋ 𝐷 ) ) ∩ ( ( 𝐹 +ℋ 𝐺 ) ∩ ( 𝑅 +ℋ 𝑆 ) ) ) ⊆ ( 𝐵 +ℋ ( 𝐴 ∩ ( 𝐶 +ℋ ( ( ( ( 𝐴 +ℋ 𝐶 ) ∩ ( 𝐵 +ℋ 𝐷 ) ) ∩ ( ( ( 𝐴 +ℋ 𝑅 ) ∩ ( 𝐵 +ℋ 𝑆 ) ) +ℋ ( ( 𝐶 +ℋ 𝑅 ) ∩ ( 𝐷 +ℋ 𝑆 ) ) ) ) ∩ ( ( ( ( 𝐴 +ℋ 𝐹 ) ∩ ( 𝐵 +ℋ 𝐺 ) ) ∩ ( ( ( 𝐴 +ℋ 𝑅 ) ∩ ( 𝐵 +ℋ 𝑆 ) ) +ℋ ( ( 𝐹 +ℋ 𝑅 ) ∩ ( 𝐺 +ℋ 𝑆 ) ) ) ) +ℋ ( ( ( 𝐶 +ℋ 𝐹 ) ∩ ( 𝐷 +ℋ 𝐺 ) ) ∩ ( ( ( 𝐶 +ℋ 𝑅 ) ∩ ( 𝐷 +ℋ 𝑆 ) ) +ℋ ( ( 𝐹 +ℋ 𝑅 ) ∩ ( 𝐺 +ℋ 𝑆 ) ) ) ) ) ) ) ) )