Theorem 3oalem3

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

	Ref	Expression
Hypotheses	3oalem1.1	⊢ 𝐵 ∈ Cℋ
	3oalem1.2	⊢ 𝐶 ∈ Cℋ
	3oalem1.3	⊢ 𝑅 ∈ Cℋ
	3oalem1.4	⊢ 𝑆 ∈ Cℋ
Assertion	3oalem3	⊢ ( ( 𝐵 +ℋ 𝑅 ) ∩ ( 𝐶 +ℋ 𝑆 ) ) ⊆ ( 𝐵 +ℋ ( 𝑅 ∩ ( 𝑆 +ℋ ( ( 𝐵 +ℋ 𝐶 ) ∩ ( 𝑅 +ℋ 𝑆 ) ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		3oalem1.1	⊢ 𝐵 ∈ Cℋ
2		3oalem1.2	⊢ 𝐶 ∈ Cℋ
3		3oalem1.3	⊢ 𝑅 ∈ Cℋ
4		3oalem1.4	⊢ 𝑆 ∈ Cℋ
5	1 3	chseli	⊢ ( 𝑣 ∈ ( 𝐵 +ℋ 𝑅 ) ↔ ∃ 𝑥 ∈ 𝐵 ∃ 𝑦 ∈ 𝑅 𝑣 = ( 𝑥 +ℎ 𝑦 ) )
6		r2ex	⊢ ( ∃ 𝑥 ∈ 𝐵 ∃ 𝑦 ∈ 𝑅 𝑣 = ( 𝑥 +ℎ 𝑦 ) ↔ ∃ 𝑥 ∃ 𝑦 ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝑅 ) ∧ 𝑣 = ( 𝑥 +ℎ 𝑦 ) ) )
7	5 6	bitri	⊢ ( 𝑣 ∈ ( 𝐵 +ℋ 𝑅 ) ↔ ∃ 𝑥 ∃ 𝑦 ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝑅 ) ∧ 𝑣 = ( 𝑥 +ℎ 𝑦 ) ) )
8	2 4	chseli	⊢ ( 𝑣 ∈ ( 𝐶 +ℋ 𝑆 ) ↔ ∃ 𝑧 ∈ 𝐶 ∃ 𝑤 ∈ 𝑆 𝑣 = ( 𝑧 +ℎ 𝑤 ) )
9		r2ex	⊢ ( ∃ 𝑧 ∈ 𝐶 ∃ 𝑤 ∈ 𝑆 𝑣 = ( 𝑧 +ℎ 𝑤 ) ↔ ∃ 𝑧 ∃ 𝑤 ( ( 𝑧 ∈ 𝐶 ∧ 𝑤 ∈ 𝑆 ) ∧ 𝑣 = ( 𝑧 +ℎ 𝑤 ) ) )
10	8 9	bitri	⊢ ( 𝑣 ∈ ( 𝐶 +ℋ 𝑆 ) ↔ ∃ 𝑧 ∃ 𝑤 ( ( 𝑧 ∈ 𝐶 ∧ 𝑤 ∈ 𝑆 ) ∧ 𝑣 = ( 𝑧 +ℎ 𝑤 ) ) )
11	7 10	anbi12i	⊢ ( ( 𝑣 ∈ ( 𝐵 +ℋ 𝑅 ) ∧ 𝑣 ∈ ( 𝐶 +ℋ 𝑆 ) ) ↔ ( ∃ 𝑥 ∃ 𝑦 ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝑅 ) ∧ 𝑣 = ( 𝑥 +ℎ 𝑦 ) ) ∧ ∃ 𝑧 ∃ 𝑤 ( ( 𝑧 ∈ 𝐶 ∧ 𝑤 ∈ 𝑆 ) ∧ 𝑣 = ( 𝑧 +ℎ 𝑤 ) ) ) )
12		elin	⊢ ( 𝑣 ∈ ( ( 𝐵 +ℋ 𝑅 ) ∩ ( 𝐶 +ℋ 𝑆 ) ) ↔ ( 𝑣 ∈ ( 𝐵 +ℋ 𝑅 ) ∧ 𝑣 ∈ ( 𝐶 +ℋ 𝑆 ) ) )
13		4exdistrv	⊢ ( ∃ 𝑥 ∃ 𝑧 ∃ 𝑦 ∃ 𝑤 ( ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝑅 ) ∧ 𝑣 = ( 𝑥 +ℎ 𝑦 ) ) ∧ ( ( 𝑧 ∈ 𝐶 ∧ 𝑤 ∈ 𝑆 ) ∧ 𝑣 = ( 𝑧 +ℎ 𝑤 ) ) ) ↔ ( ∃ 𝑥 ∃ 𝑦 ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝑅 ) ∧ 𝑣 = ( 𝑥 +ℎ 𝑦 ) ) ∧ ∃ 𝑧 ∃ 𝑤 ( ( 𝑧 ∈ 𝐶 ∧ 𝑤 ∈ 𝑆 ) ∧ 𝑣 = ( 𝑧 +ℎ 𝑤 ) ) ) )
14	11 12 13	3bitr4i	⊢ ( 𝑣 ∈ ( ( 𝐵 +ℋ 𝑅 ) ∩ ( 𝐶 +ℋ 𝑆 ) ) ↔ ∃ 𝑥 ∃ 𝑧 ∃ 𝑦 ∃ 𝑤 ( ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝑅 ) ∧ 𝑣 = ( 𝑥 +ℎ 𝑦 ) ) ∧ ( ( 𝑧 ∈ 𝐶 ∧ 𝑤 ∈ 𝑆 ) ∧ 𝑣 = ( 𝑧 +ℎ 𝑤 ) ) ) )
15	1 2 3 4	3oalem2	⊢ ( ( ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝑅 ) ∧ 𝑣 = ( 𝑥 +ℎ 𝑦 ) ) ∧ ( ( 𝑧 ∈ 𝐶 ∧ 𝑤 ∈ 𝑆 ) ∧ 𝑣 = ( 𝑧 +ℎ 𝑤 ) ) ) → 𝑣 ∈ ( 𝐵 +ℋ ( 𝑅 ∩ ( 𝑆 +ℋ ( ( 𝐵 +ℋ 𝐶 ) ∩ ( 𝑅 +ℋ 𝑆 ) ) ) ) ) )
16	15	exlimivv	⊢ ( ∃ 𝑦 ∃ 𝑤 ( ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝑅 ) ∧ 𝑣 = ( 𝑥 +ℎ 𝑦 ) ) ∧ ( ( 𝑧 ∈ 𝐶 ∧ 𝑤 ∈ 𝑆 ) ∧ 𝑣 = ( 𝑧 +ℎ 𝑤 ) ) ) → 𝑣 ∈ ( 𝐵 +ℋ ( 𝑅 ∩ ( 𝑆 +ℋ ( ( 𝐵 +ℋ 𝐶 ) ∩ ( 𝑅 +ℋ 𝑆 ) ) ) ) ) )
17	16	exlimivv	⊢ ( ∃ 𝑥 ∃ 𝑧 ∃ 𝑦 ∃ 𝑤 ( ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝑅 ) ∧ 𝑣 = ( 𝑥 +ℎ 𝑦 ) ) ∧ ( ( 𝑧 ∈ 𝐶 ∧ 𝑤 ∈ 𝑆 ) ∧ 𝑣 = ( 𝑧 +ℎ 𝑤 ) ) ) → 𝑣 ∈ ( 𝐵 +ℋ ( 𝑅 ∩ ( 𝑆 +ℋ ( ( 𝐵 +ℋ 𝐶 ) ∩ ( 𝑅 +ℋ 𝑆 ) ) ) ) ) )
18	14 17	sylbi	⊢ ( 𝑣 ∈ ( ( 𝐵 +ℋ 𝑅 ) ∩ ( 𝐶 +ℋ 𝑆 ) ) → 𝑣 ∈ ( 𝐵 +ℋ ( 𝑅 ∩ ( 𝑆 +ℋ ( ( 𝐵 +ℋ 𝐶 ) ∩ ( 𝑅 +ℋ 𝑆 ) ) ) ) ) )
19	18	ssriv	⊢ ( ( 𝐵 +ℋ 𝑅 ) ∩ ( 𝐶 +ℋ 𝑆 ) ) ⊆ ( 𝐵 +ℋ ( 𝑅 ∩ ( 𝑆 +ℋ ( ( 𝐵 +ℋ 𝐶 ) ∩ ( 𝑅 +ℋ 𝑆 ) ) ) ) )