Theorem 3oalem2 29434

Description: Lemma for 3OA (weak) orthoarguesian law. (Contributed by NM, 19-Oct-1999.) (New usage is discouraged.)

Hypotheses

Ref	Expression
3oalem1.1	⊢ 𝐵 ∈ Cℋ
3oalem1.2	⊢ 𝐶 ∈ Cℋ
3oalem1.3	⊢ 𝑅 ∈ Cℋ
3oalem1.4	⊢ 𝑆 ∈ Cℋ

Assertion

Ref	Expression
3oalem2	⊢ ((((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝑅) ∧ 𝑣 = (𝑥 +ℎ 𝑦)) ∧ ((𝑧 ∈ 𝐶 ∧ 𝑤 ∈ 𝑆) ∧ 𝑣 = (𝑧 +ℎ 𝑤))) → 𝑣 ∈ (𝐵 +ℋ (𝑅 ∩ (𝑆 +ℋ ((𝐵 +ℋ 𝐶) ∩ (𝑅 +ℋ 𝑆))))))

Distinct variable groups:   𝑥,𝑦,𝑧,𝑤,𝑣,𝐵   𝑥,𝐶,𝑦,𝑧,𝑤,𝑣   𝑥,𝑅,𝑦,𝑧,𝑤,𝑣   𝑥,𝑆,𝑦,𝑧,𝑤,𝑣

Proof of Theorem 3oalem2

Step	Hyp	Ref	Expression
1		simplll 773	. . 3 ⊢ ((((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝑅) ∧ 𝑣 = (𝑥 +ℎ 𝑦)) ∧ ((𝑧 ∈ 𝐶 ∧ 𝑤 ∈ 𝑆) ∧ 𝑣 = (𝑧 +ℎ 𝑤))) → 𝑥 ∈ 𝐵)
2		simpllr 774	. . . 4 ⊢ ((((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝑅) ∧ 𝑣 = (𝑥 +ℎ 𝑦)) ∧ ((𝑧 ∈ 𝐶 ∧ 𝑤 ∈ 𝑆) ∧ 𝑣 = (𝑧 +ℎ 𝑤))) → 𝑦 ∈ 𝑅)
3		3oalem1.1	. . . . . . 7 ⊢ 𝐵 ∈ Cℋ
4		3oalem1.2	. . . . . . 7 ⊢ 𝐶 ∈ Cℋ
5		3oalem1.3	. . . . . . 7 ⊢ 𝑅 ∈ Cℋ
6		3oalem1.4	. . . . . . 7 ⊢ 𝑆 ∈ Cℋ
7	3, 4, 5, 6	3oalem1 29433	. . . . . 6 ⊢ ((((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝑅) ∧ 𝑣 = (𝑥 +ℎ 𝑦)) ∧ ((𝑧 ∈ 𝐶 ∧ 𝑤 ∈ 𝑆) ∧ 𝑣 = (𝑧 +ℎ 𝑤))) → (((𝑥 ∈ ℋ ∧ 𝑦 ∈ ℋ) ∧ 𝑣 ∈ ℋ) ∧ (𝑧 ∈ ℋ ∧ 𝑤 ∈ ℋ)))
8		hvaddsub12 28809	. . . . . . . . . 10 ⊢ ((𝑦 ∈ ℋ ∧ 𝑤 ∈ ℋ ∧ 𝑤 ∈ ℋ) → (𝑦 +ℎ (𝑤 −ℎ 𝑤)) = (𝑤 +ℎ (𝑦 −ℎ 𝑤)))
9	8	3anidm23 1417	. . . . . . . . 9 ⊢ ((𝑦 ∈ ℋ ∧ 𝑤 ∈ ℋ) → (𝑦 +ℎ (𝑤 −ℎ 𝑤)) = (𝑤 +ℎ (𝑦 −ℎ 𝑤)))
10		hvsubid 28797	. . . . . . . . . . 11 ⊢ (𝑤 ∈ ℋ → (𝑤 −ℎ 𝑤) = 0ℎ)
11	10	oveq2d 7166	. . . . . . . . . 10 ⊢ (𝑤 ∈ ℋ → (𝑦 +ℎ (𝑤 −ℎ 𝑤)) = (𝑦 +ℎ 0ℎ))
12		ax-hvaddid 28775	. . . . . . . . . 10 ⊢ (𝑦 ∈ ℋ → (𝑦 +ℎ 0ℎ) = 𝑦)
13	11, 12	sylan9eqr 2878	. . . . . . . . 9 ⊢ ((𝑦 ∈ ℋ ∧ 𝑤 ∈ ℋ) → (𝑦 +ℎ (𝑤 −ℎ 𝑤)) = 𝑦)
14	9, 13	eqtr3d 2858	. . . . . . . 8 ⊢ ((𝑦 ∈ ℋ ∧ 𝑤 ∈ ℋ) → (𝑤 +ℎ (𝑦 −ℎ 𝑤)) = 𝑦)
15	14	ad2ant2l 744	. . . . . . 7 ⊢ (((𝑥 ∈ ℋ ∧ 𝑦 ∈ ℋ) ∧ (𝑧 ∈ ℋ ∧ 𝑤 ∈ ℋ)) → (𝑤 +ℎ (𝑦 −ℎ 𝑤)) = 𝑦)
16	15	adantlr 713	. . . . . 6 ⊢ ((((𝑥 ∈ ℋ ∧ 𝑦 ∈ ℋ) ∧ 𝑣 ∈ ℋ) ∧ (𝑧 ∈ ℋ ∧ 𝑤 ∈ ℋ)) → (𝑤 +ℎ (𝑦 −ℎ 𝑤)) = 𝑦)
17	7, 16	syl 17	. . . . 5 ⊢ ((((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝑅) ∧ 𝑣 = (𝑥 +ℎ 𝑦)) ∧ ((𝑧 ∈ 𝐶 ∧ 𝑤 ∈ 𝑆) ∧ 𝑣 = (𝑧 +ℎ 𝑤))) → (𝑤 +ℎ (𝑦 −ℎ 𝑤)) = 𝑦)
18		simprlr 778	. . . . . 6 ⊢ ((((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝑅) ∧ 𝑣 = (𝑥 +ℎ 𝑦)) ∧ ((𝑧 ∈ 𝐶 ∧ 𝑤 ∈ 𝑆) ∧ 𝑣 = (𝑧 +ℎ 𝑤))) → 𝑤 ∈ 𝑆)
19		eqtr2 2842	. . . . . . . . . . 11 ⊢ ((𝑣 = (𝑥 +ℎ 𝑦) ∧ 𝑣 = (𝑧 +ℎ 𝑤)) → (𝑥 +ℎ 𝑦) = (𝑧 +ℎ 𝑤))
20	19	oveq1d 7165	. . . . . . . . . 10 ⊢ ((𝑣 = (𝑥 +ℎ 𝑦) ∧ 𝑣 = (𝑧 +ℎ 𝑤)) → ((𝑥 +ℎ 𝑦) −ℎ (𝑥 +ℎ 𝑤)) = ((𝑧 +ℎ 𝑤) −ℎ (𝑥 +ℎ 𝑤)))
21	20	ad2ant2l 744	. . . . . . . . 9 ⊢ ((((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝑅) ∧ 𝑣 = (𝑥 +ℎ 𝑦)) ∧ ((𝑧 ∈ 𝐶 ∧ 𝑤 ∈ 𝑆) ∧ 𝑣 = (𝑧 +ℎ 𝑤))) → ((𝑥 +ℎ 𝑦) −ℎ (𝑥 +ℎ 𝑤)) = ((𝑧 +ℎ 𝑤) −ℎ (𝑥 +ℎ 𝑤)))
22		simpl 485	. . . . . . . . . . . . . 14 ⊢ ((𝑥 ∈ ℋ ∧ 𝑦 ∈ ℋ) → 𝑥 ∈ ℋ)
23	22	anim1i 616	. . . . . . . . . . . . 13 ⊢ (((𝑥 ∈ ℋ ∧ 𝑦 ∈ ℋ) ∧ 𝑤 ∈ ℋ) → (𝑥 ∈ ℋ ∧ 𝑤 ∈ ℋ))
24		hvsub4 28808	. . . . . . . . . . . . 13 ⊢ (((𝑥 ∈ ℋ ∧ 𝑦 ∈ ℋ) ∧ (𝑥 ∈ ℋ ∧ 𝑤 ∈ ℋ)) → ((𝑥 +ℎ 𝑦) −ℎ (𝑥 +ℎ 𝑤)) = ((𝑥 −ℎ 𝑥) +ℎ (𝑦 −ℎ 𝑤)))
25	23, 24	syldan 593	. . . . . . . . . . . 12 ⊢ (((𝑥 ∈ ℋ ∧ 𝑦 ∈ ℋ) ∧ 𝑤 ∈ ℋ) → ((𝑥 +ℎ 𝑦) −ℎ (𝑥 +ℎ 𝑤)) = ((𝑥 −ℎ 𝑥) +ℎ (𝑦 −ℎ 𝑤)))
26		hvsubid 28797	. . . . . . . . . . . . . 14 ⊢ (𝑥 ∈ ℋ → (𝑥 −ℎ 𝑥) = 0ℎ)
27	26	ad2antrr 724	. . . . . . . . . . . . 13 ⊢ (((𝑥 ∈ ℋ ∧ 𝑦 ∈ ℋ) ∧ 𝑤 ∈ ℋ) → (𝑥 −ℎ 𝑥) = 0ℎ)
28	27	oveq1d 7165	. . . . . . . . . . . 12 ⊢ (((𝑥 ∈ ℋ ∧ 𝑦 ∈ ℋ) ∧ 𝑤 ∈ ℋ) → ((𝑥 −ℎ 𝑥) +ℎ (𝑦 −ℎ 𝑤)) = (0ℎ +ℎ (𝑦 −ℎ 𝑤)))
29		hvsubcl 28788	. . . . . . . . . . . . . 14 ⊢ ((𝑦 ∈ ℋ ∧ 𝑤 ∈ ℋ) → (𝑦 −ℎ 𝑤) ∈ ℋ)
30		hvaddid2 28794	. . . . . . . . . . . . . 14 ⊢ ((𝑦 −ℎ 𝑤) ∈ ℋ → (0ℎ +ℎ (𝑦 −ℎ 𝑤)) = (𝑦 −ℎ 𝑤))
31	29, 30	syl 17	. . . . . . . . . . . . 13 ⊢ ((𝑦 ∈ ℋ ∧ 𝑤 ∈ ℋ) → (0ℎ +ℎ (𝑦 −ℎ 𝑤)) = (𝑦 −ℎ 𝑤))
32	31	adantll 712	. . . . . . . . . . . 12 ⊢ (((𝑥 ∈ ℋ ∧ 𝑦 ∈ ℋ) ∧ 𝑤 ∈ ℋ) → (0ℎ +ℎ (𝑦 −ℎ 𝑤)) = (𝑦 −ℎ 𝑤))
33	25, 28, 32	3eqtrd 2860	. . . . . . . . . . 11 ⊢ (((𝑥 ∈ ℋ ∧ 𝑦 ∈ ℋ) ∧ 𝑤 ∈ ℋ) → ((𝑥 +ℎ 𝑦) −ℎ (𝑥 +ℎ 𝑤)) = (𝑦 −ℎ 𝑤))
34	33	ad2ant2rl 747	. . . . . . . . . 10 ⊢ ((((𝑥 ∈ ℋ ∧ 𝑦 ∈ ℋ) ∧ 𝑣 ∈ ℋ) ∧ (𝑧 ∈ ℋ ∧ 𝑤 ∈ ℋ)) → ((𝑥 +ℎ 𝑦) −ℎ (𝑥 +ℎ 𝑤)) = (𝑦 −ℎ 𝑤))
35	7, 34	syl 17	. . . . . . . . 9 ⊢ ((((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝑅) ∧ 𝑣 = (𝑥 +ℎ 𝑦)) ∧ ((𝑧 ∈ 𝐶 ∧ 𝑤 ∈ 𝑆) ∧ 𝑣 = (𝑧 +ℎ 𝑤))) → ((𝑥 +ℎ 𝑦) −ℎ (𝑥 +ℎ 𝑤)) = (𝑦 −ℎ 𝑤))
36		simpr 487	. . . . . . . . . . . . . 14 ⊢ ((𝑥 ∈ ℋ ∧ (𝑧 ∈ ℋ ∧ 𝑤 ∈ ℋ)) → (𝑧 ∈ ℋ ∧ 𝑤 ∈ ℋ))
37		simpr 487	. . . . . . . . . . . . . . 15 ⊢ ((𝑧 ∈ ℋ ∧ 𝑤 ∈ ℋ) → 𝑤 ∈ ℋ)
38	37	anim2i 618	. . . . . . . . . . . . . 14 ⊢ ((𝑥 ∈ ℋ ∧ (𝑧 ∈ ℋ ∧ 𝑤 ∈ ℋ)) → (𝑥 ∈ ℋ ∧ 𝑤 ∈ ℋ))
39		hvsub4 28808	. . . . . . . . . . . . . 14 ⊢ (((𝑧 ∈ ℋ ∧ 𝑤 ∈ ℋ) ∧ (𝑥 ∈ ℋ ∧ 𝑤 ∈ ℋ)) → ((𝑧 +ℎ 𝑤) −ℎ (𝑥 +ℎ 𝑤)) = ((𝑧 −ℎ 𝑥) +ℎ (𝑤 −ℎ 𝑤)))
40	36, 38, 39	syl2anc 586	. . . . . . . . . . . . 13 ⊢ ((𝑥 ∈ ℋ ∧ (𝑧 ∈ ℋ ∧ 𝑤 ∈ ℋ)) → ((𝑧 +ℎ 𝑤) −ℎ (𝑥 +ℎ 𝑤)) = ((𝑧 −ℎ 𝑥) +ℎ (𝑤 −ℎ 𝑤)))
41	10	ad2antll 727	. . . . . . . . . . . . . 14 ⊢ ((𝑥 ∈ ℋ ∧ (𝑧 ∈ ℋ ∧ 𝑤 ∈ ℋ)) → (𝑤 −ℎ 𝑤) = 0ℎ)
42	41	oveq2d 7166	. . . . . . . . . . . . 13 ⊢ ((𝑥 ∈ ℋ ∧ (𝑧 ∈ ℋ ∧ 𝑤 ∈ ℋ)) → ((𝑧 −ℎ 𝑥) +ℎ (𝑤 −ℎ 𝑤)) = ((𝑧 −ℎ 𝑥) +ℎ 0ℎ))
43		hvsubcl 28788	. . . . . . . . . . . . . . . 16 ⊢ ((𝑧 ∈ ℋ ∧ 𝑥 ∈ ℋ) → (𝑧 −ℎ 𝑥) ∈ ℋ)
44		ax-hvaddid 28775	. . . . . . . . . . . . . . . 16 ⊢ ((𝑧 −ℎ 𝑥) ∈ ℋ → ((𝑧 −ℎ 𝑥) +ℎ 0ℎ) = (𝑧 −ℎ 𝑥))
45	43, 44	syl 17	. . . . . . . . . . . . . . 15 ⊢ ((𝑧 ∈ ℋ ∧ 𝑥 ∈ ℋ) → ((𝑧 −ℎ 𝑥) +ℎ 0ℎ) = (𝑧 −ℎ 𝑥))
46	45	ancoms 461	. . . . . . . . . . . . . 14 ⊢ ((𝑥 ∈ ℋ ∧ 𝑧 ∈ ℋ) → ((𝑧 −ℎ 𝑥) +ℎ 0ℎ) = (𝑧 −ℎ 𝑥))
47	46	adantrr 715	. . . . . . . . . . . . 13 ⊢ ((𝑥 ∈ ℋ ∧ (𝑧 ∈ ℋ ∧ 𝑤 ∈ ℋ)) → ((𝑧 −ℎ 𝑥) +ℎ 0ℎ) = (𝑧 −ℎ 𝑥))
48	40, 42, 47	3eqtrd 2860	. . . . . . . . . . . 12 ⊢ ((𝑥 ∈ ℋ ∧ (𝑧 ∈ ℋ ∧ 𝑤 ∈ ℋ)) → ((𝑧 +ℎ 𝑤) −ℎ (𝑥 +ℎ 𝑤)) = (𝑧 −ℎ 𝑥))
49	48	adantlr 713	. . . . . . . . . . 11 ⊢ (((𝑥 ∈ ℋ ∧ 𝑦 ∈ ℋ) ∧ (𝑧 ∈ ℋ ∧ 𝑤 ∈ ℋ)) → ((𝑧 +ℎ 𝑤) −ℎ (𝑥 +ℎ 𝑤)) = (𝑧 −ℎ 𝑥))
50	49	adantlr 713	. . . . . . . . . 10 ⊢ ((((𝑥 ∈ ℋ ∧ 𝑦 ∈ ℋ) ∧ 𝑣 ∈ ℋ) ∧ (𝑧 ∈ ℋ ∧ 𝑤 ∈ ℋ)) → ((𝑧 +ℎ 𝑤) −ℎ (𝑥 +ℎ 𝑤)) = (𝑧 −ℎ 𝑥))
51	7, 50	syl 17	. . . . . . . . 9 ⊢ ((((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝑅) ∧ 𝑣 = (𝑥 +ℎ 𝑦)) ∧ ((𝑧 ∈ 𝐶 ∧ 𝑤 ∈ 𝑆) ∧ 𝑣 = (𝑧 +ℎ 𝑤))) → ((𝑧 +ℎ 𝑤) −ℎ (𝑥 +ℎ 𝑤)) = (𝑧 −ℎ 𝑥))
52	21, 35, 51	3eqtr3d 2864	. . . . . . . 8 ⊢ ((((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝑅) ∧ 𝑣 = (𝑥 +ℎ 𝑦)) ∧ ((𝑧 ∈ 𝐶 ∧ 𝑤 ∈ 𝑆) ∧ 𝑣 = (𝑧 +ℎ 𝑤))) → (𝑦 −ℎ 𝑤) = (𝑧 −ℎ 𝑥))
53		simpll 765	. . . . . . . . 9 ⊢ (((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝑅) ∧ 𝑣 = (𝑥 +ℎ 𝑦)) → 𝑥 ∈ 𝐵)
54		simpll 765	. . . . . . . . 9 ⊢ (((𝑧 ∈ 𝐶 ∧ 𝑤 ∈ 𝑆) ∧ 𝑣 = (𝑧 +ℎ 𝑤)) → 𝑧 ∈ 𝐶)
55	4	chshii 28998	. . . . . . . . . . . 12 ⊢ 𝐶 ∈ Sℋ
56	3	chshii 28998	. . . . . . . . . . . 12 ⊢ 𝐵 ∈ Sℋ
57	55, 56	shsvsi 29138	. . . . . . . . . . 11 ⊢ ((𝑧 ∈ 𝐶 ∧ 𝑥 ∈ 𝐵) → (𝑧 −ℎ 𝑥) ∈ (𝐶 +ℋ 𝐵))
58	57	ancoms 461	. . . . . . . . . 10 ⊢ ((𝑥 ∈ 𝐵 ∧ 𝑧 ∈ 𝐶) → (𝑧 −ℎ 𝑥) ∈ (𝐶 +ℋ 𝐵))
59	56, 55	shscomi 29134	. . . . . . . . . 10 ⊢ (𝐵 +ℋ 𝐶) = (𝐶 +ℋ 𝐵)
60	58, 59	eleqtrrdi 2924	. . . . . . . . 9 ⊢ ((𝑥 ∈ 𝐵 ∧ 𝑧 ∈ 𝐶) → (𝑧 −ℎ 𝑥) ∈ (𝐵 +ℋ 𝐶))
61	53, 54, 60	syl2an 597	. . . . . . . 8 ⊢ ((((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝑅) ∧ 𝑣 = (𝑥 +ℎ 𝑦)) ∧ ((𝑧 ∈ 𝐶 ∧ 𝑤 ∈ 𝑆) ∧ 𝑣 = (𝑧 +ℎ 𝑤))) → (𝑧 −ℎ 𝑥) ∈ (𝐵 +ℋ 𝐶))
62	52, 61	eqeltrd 2913	. . . . . . 7 ⊢ ((((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝑅) ∧ 𝑣 = (𝑥 +ℎ 𝑦)) ∧ ((𝑧 ∈ 𝐶 ∧ 𝑤 ∈ 𝑆) ∧ 𝑣 = (𝑧 +ℎ 𝑤))) → (𝑦 −ℎ 𝑤) ∈ (𝐵 +ℋ 𝐶))
63		simplr 767	. . . . . . . 8 ⊢ (((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝑅) ∧ 𝑣 = (𝑥 +ℎ 𝑦)) → 𝑦 ∈ 𝑅)
64		simplr 767	. . . . . . . 8 ⊢ (((𝑧 ∈ 𝐶 ∧ 𝑤 ∈ 𝑆) ∧ 𝑣 = (𝑧 +ℎ 𝑤)) → 𝑤 ∈ 𝑆)
65	5	chshii 28998	. . . . . . . . 9 ⊢ 𝑅 ∈ Sℋ
66	6	chshii 28998	. . . . . . . . 9 ⊢ 𝑆 ∈ Sℋ
67	65, 66	shsvsi 29138	. . . . . . . 8 ⊢ ((𝑦 ∈ 𝑅 ∧ 𝑤 ∈ 𝑆) → (𝑦 −ℎ 𝑤) ∈ (𝑅 +ℋ 𝑆))
68	63, 64, 67	syl2an 597	. . . . . . 7 ⊢ ((((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝑅) ∧ 𝑣 = (𝑥 +ℎ 𝑦)) ∧ ((𝑧 ∈ 𝐶 ∧ 𝑤 ∈ 𝑆) ∧ 𝑣 = (𝑧 +ℎ 𝑤))) → (𝑦 −ℎ 𝑤) ∈ (𝑅 +ℋ 𝑆))
69	62, 68	elind 4170	. . . . . 6 ⊢ ((((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝑅) ∧ 𝑣 = (𝑥 +ℎ 𝑦)) ∧ ((𝑧 ∈ 𝐶 ∧ 𝑤 ∈ 𝑆) ∧ 𝑣 = (𝑧 +ℎ 𝑤))) → (𝑦 −ℎ 𝑤) ∈ ((𝐵 +ℋ 𝐶) ∩ (𝑅 +ℋ 𝑆)))
70	56, 55	shscli 29088	. . . . . . . 8 ⊢ (𝐵 +ℋ 𝐶) ∈ Sℋ
71	65, 66	shscli 29088	. . . . . . . 8 ⊢ (𝑅 +ℋ 𝑆) ∈ Sℋ
72	70, 71	shincli 29133	. . . . . . 7 ⊢ ((𝐵 +ℋ 𝐶) ∩ (𝑅 +ℋ 𝑆)) ∈ Sℋ
73	66, 72	shsvai 29135	. . . . . 6 ⊢ ((𝑤 ∈ 𝑆 ∧ (𝑦 −ℎ 𝑤) ∈ ((𝐵 +ℋ 𝐶) ∩ (𝑅 +ℋ 𝑆))) → (𝑤 +ℎ (𝑦 −ℎ 𝑤)) ∈ (𝑆 +ℋ ((𝐵 +ℋ 𝐶) ∩ (𝑅 +ℋ 𝑆))))
74	18, 69, 73	syl2anc 586	. . . . 5 ⊢ ((((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝑅) ∧ 𝑣 = (𝑥 +ℎ 𝑦)) ∧ ((𝑧 ∈ 𝐶 ∧ 𝑤 ∈ 𝑆) ∧ 𝑣 = (𝑧 +ℎ 𝑤))) → (𝑤 +ℎ (𝑦 −ℎ 𝑤)) ∈ (𝑆 +ℋ ((𝐵 +ℋ 𝐶) ∩ (𝑅 +ℋ 𝑆))))
75	17, 74	eqeltrrd 2914	. . . 4 ⊢ ((((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝑅) ∧ 𝑣 = (𝑥 +ℎ 𝑦)) ∧ ((𝑧 ∈ 𝐶 ∧ 𝑤 ∈ 𝑆) ∧ 𝑣 = (𝑧 +ℎ 𝑤))) → 𝑦 ∈ (𝑆 +ℋ ((𝐵 +ℋ 𝐶) ∩ (𝑅 +ℋ 𝑆))))
76	2, 75	elind 4170	. . 3 ⊢ ((((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝑅) ∧ 𝑣 = (𝑥 +ℎ 𝑦)) ∧ ((𝑧 ∈ 𝐶 ∧ 𝑤 ∈ 𝑆) ∧ 𝑣 = (𝑧 +ℎ 𝑤))) → 𝑦 ∈ (𝑅 ∩ (𝑆 +ℋ ((𝐵 +ℋ 𝐶) ∩ (𝑅 +ℋ 𝑆)))))
77	66, 72	shscli 29088	. . . . 5 ⊢ (𝑆 +ℋ ((𝐵 +ℋ 𝐶) ∩ (𝑅 +ℋ 𝑆))) ∈ Sℋ
78	65, 77	shincli 29133	. . . 4 ⊢ (𝑅 ∩ (𝑆 +ℋ ((𝐵 +ℋ 𝐶) ∩ (𝑅 +ℋ 𝑆)))) ∈ Sℋ
79	56, 78	shsvai 29135	. . 3 ⊢ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ (𝑅 ∩ (𝑆 +ℋ ((𝐵 +ℋ 𝐶) ∩ (𝑅 +ℋ 𝑆))))) → (𝑥 +ℎ 𝑦) ∈ (𝐵 +ℋ (𝑅 ∩ (𝑆 +ℋ ((𝐵 +ℋ 𝐶) ∩ (𝑅 +ℋ 𝑆))))))
80	1, 76, 79	syl2anc 586	. 2 ⊢ ((((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝑅) ∧ 𝑣 = (𝑥 +ℎ 𝑦)) ∧ ((𝑧 ∈ 𝐶 ∧ 𝑤 ∈ 𝑆) ∧ 𝑣 = (𝑧 +ℎ 𝑤))) → (𝑥 +ℎ 𝑦) ∈ (𝐵 +ℋ (𝑅 ∩ (𝑆 +ℋ ((𝐵 +ℋ 𝐶) ∩ (𝑅 +ℋ 𝑆))))))
81		eleq1 2900	. . 3 ⊢ (𝑣 = (𝑥 +ℎ 𝑦) → (𝑣 ∈ (𝐵 +ℋ (𝑅 ∩ (𝑆 +ℋ ((𝐵 +ℋ 𝐶) ∩ (𝑅 +ℋ 𝑆))))) ↔ (𝑥 +ℎ 𝑦) ∈ (𝐵 +ℋ (𝑅 ∩ (𝑆 +ℋ ((𝐵 +ℋ 𝐶) ∩ (𝑅 +ℋ 𝑆)))))))
82	81	ad2antlr 725	. 2 ⊢ ((((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝑅) ∧ 𝑣 = (𝑥 +ℎ 𝑦)) ∧ ((𝑧 ∈ 𝐶 ∧ 𝑤 ∈ 𝑆) ∧ 𝑣 = (𝑧 +ℎ 𝑤))) → (𝑣 ∈ (𝐵 +ℋ (𝑅 ∩ (𝑆 +ℋ ((𝐵 +ℋ 𝐶) ∩ (𝑅 +ℋ 𝑆))))) ↔ (𝑥 +ℎ 𝑦) ∈ (𝐵 +ℋ (𝑅 ∩ (𝑆 +ℋ ((𝐵 +ℋ 𝐶) ∩ (𝑅 +ℋ 𝑆)))))))
83	80, 82	mpbird 259	1 ⊢ ((((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝑅) ∧ 𝑣 = (𝑥 +ℎ 𝑦)) ∧ ((𝑧 ∈ 𝐶 ∧ 𝑤 ∈ 𝑆) ∧ 𝑣 = (𝑧 +ℎ 𝑤))) → 𝑣 ∈ (𝐵 +ℋ (𝑅 ∩ (𝑆 +ℋ ((𝐵 +ℋ 𝐶) ∩ (𝑅 +ℋ 𝑆))))))

Syntax hints:   → wi 4   ↔ wb 208   ∧ wa 398   = wceq 1533   ∈ wcel 2110   ∩ cin 3934  (class class class)co 7150   ℋchba 28690   +_ℎ cva 28691  0_ℎc0v 28695   −_ℎ cmv 28696   C_ℋ cch 28700   +_ℋ cph 28702

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1907  ax-6 1966  ax-7 2011  ax-8 2112  ax-9 2120  ax-10 2141  ax-11 2157  ax-12 2173  ax-ext 2793  ax-rep 5182  ax-sep 5195  ax-nul 5202  ax-pow 5258  ax-pr 5321  ax-un 7455  ax-cnex 10587  ax-resscn 10588  ax-1cn 10589  ax-icn 10590  ax-addcl 10591  ax-addrcl 10592  ax-mulcl 10593  ax-mulrcl 10594  ax-mulcom 10595  ax-addass 10596  ax-mulass 10597  ax-distr 10598  ax-i2m1 10599  ax-1ne0 10600  ax-1rid 10601  ax-rnegex 10602  ax-rrecex 10603  ax-cnre 10604  ax-pre-lttri 10605  ax-pre-lttrn 10606  ax-pre-ltadd 10607  ax-hilex 28770  ax-hfvadd 28771  ax-hvcom 28772  ax-hvass 28773  ax-hv0cl 28774  ax-hvaddid 28775  ax-hfvmul 28776  ax-hvmulid 28777  ax-hvdistr1 28779  ax-hvdistr2 28780  ax-hvmul0 28781

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3or 1084  df-3an 1085  df-tru 1536  df-ex 1777  df-nf 1781  df-sb 2066  df-mo 2618  df-eu 2650  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-ne 3017  df-nel 3124  df-ral 3143  df-rex 3144  df-reu 3145  df-rab 3147  df-v 3496  df-sbc 3772  df-csb 3883  df-dif 3938  df-un 3940  df-in 3942  df-ss 3951  df-pss 3953  df-nul 4291  df-if 4467  df-pw 4540  df-sn 4561  df-pr 4563  df-tp 4565  df-op 4567  df-uni 4832  df-int 4869  df-iun 4913  df-br 5059  df-opab 5121  df-mpt 5139  df-tr 5165  df-id 5454  df-eprel 5459  df-po 5468  df-so 5469  df-fr 5508  df-we 5510  df-xp 5555  df-rel 5556  df-cnv 5557  df-co 5558  df-dm 5559  df-rn 5560  df-res 5561  df-ima 5562  df-pred 6142  df-ord 6188  df-on 6189  df-lim 6190  df-suc 6191  df-iota 6308  df-fun 6351  df-fn 6352  df-f 6353  df-f1 6354  df-fo 6355  df-f1o 6356  df-fv 6357  df-riota 7108  df-ov 7153  df-oprab 7154  df-mpo 7155  df-om 7575  df-wrecs 7941  df-recs 8002  df-rdg 8040  df-er 8283  df-map 8402  df-en 8504  df-dom 8505  df-sdom 8506  df-pnf 10671  df-mnf 10672  df-ltxr 10674  df-sub 10866  df-neg 10867  df-nn 11633  df-grpo 28264  df-ablo 28316  df-hvsub 28742  df-hlim 28743  df-sh 28978  df-ch 28992  df-shs 29079

This theorem is referenced by:  3oalem3  29435