Theorem 3oalem5

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

	Ref	Expression
Hypotheses	3oa.1	⊢ 𝐴 ∈ Cℋ
	3oa.2	⊢ 𝐵 ∈ Cℋ
	3oa.3	⊢ 𝐶 ∈ Cℋ
	3oa.4	⊢ 𝑅 = ( ( ⊥ ‘ 𝐵 ) ∩ ( 𝐵 ∨ℋ 𝐴 ) )
	3oa.5	⊢ 𝑆 = ( ( ⊥ ‘ 𝐶 ) ∩ ( 𝐶 ∨ℋ 𝐴 ) )
Assertion	3oalem5	⊢ ( ( 𝐵 +ℋ 𝑅 ) ∩ ( 𝐶 +ℋ 𝑆 ) ) = ( ( 𝐵 ∨ℋ 𝑅 ) ∩ ( 𝐶 ∨ℋ 𝑆 ) )

Proof

Step	Hyp	Ref	Expression
1		3oa.1	⊢ 𝐴 ∈ Cℋ
2		3oa.2	⊢ 𝐵 ∈ Cℋ
3		3oa.3	⊢ 𝐶 ∈ Cℋ
4		3oa.4	⊢ 𝑅 = ( ( ⊥ ‘ 𝐵 ) ∩ ( 𝐵 ∨ℋ 𝐴 ) )
5		3oa.5	⊢ 𝑆 = ( ( ⊥ ‘ 𝐶 ) ∩ ( 𝐶 ∨ℋ 𝐴 ) )
6	4	3oalem4	⊢ 𝑅 ⊆ ( ⊥ ‘ 𝐵 )
7	2	choccli	⊢ ( ⊥ ‘ 𝐵 ) ∈ Cℋ
8	2 1	chjcli	⊢ ( 𝐵 ∨ℋ 𝐴 ) ∈ Cℋ
9	7 8	chincli	⊢ ( ( ⊥ ‘ 𝐵 ) ∩ ( 𝐵 ∨ℋ 𝐴 ) ) ∈ Cℋ
10	4 9	eqeltri	⊢ 𝑅 ∈ Cℋ
11	10 2	osumi	⊢ ( 𝑅 ⊆ ( ⊥ ‘ 𝐵 ) → ( 𝑅 +ℋ 𝐵 ) = ( 𝑅 ∨ℋ 𝐵 ) )
12	6 11	ax-mp	⊢ ( 𝑅 +ℋ 𝐵 ) = ( 𝑅 ∨ℋ 𝐵 )
13	2	chshii	⊢ 𝐵 ∈ Sℋ
14	10	chshii	⊢ 𝑅 ∈ Sℋ
15	13 14	shscomi	⊢ ( 𝐵 +ℋ 𝑅 ) = ( 𝑅 +ℋ 𝐵 )
16	2 10	chjcomi	⊢ ( 𝐵 ∨ℋ 𝑅 ) = ( 𝑅 ∨ℋ 𝐵 )
17	12 15 16	3eqtr4i	⊢ ( 𝐵 +ℋ 𝑅 ) = ( 𝐵 ∨ℋ 𝑅 )
18	5	3oalem4	⊢ 𝑆 ⊆ ( ⊥ ‘ 𝐶 )
19	3	choccli	⊢ ( ⊥ ‘ 𝐶 ) ∈ Cℋ
20	3 1	chjcli	⊢ ( 𝐶 ∨ℋ 𝐴 ) ∈ Cℋ
21	19 20	chincli	⊢ ( ( ⊥ ‘ 𝐶 ) ∩ ( 𝐶 ∨ℋ 𝐴 ) ) ∈ Cℋ
22	5 21	eqeltri	⊢ 𝑆 ∈ Cℋ
23	22 3	osumi	⊢ ( 𝑆 ⊆ ( ⊥ ‘ 𝐶 ) → ( 𝑆 +ℋ 𝐶 ) = ( 𝑆 ∨ℋ 𝐶 ) )
24	18 23	ax-mp	⊢ ( 𝑆 +ℋ 𝐶 ) = ( 𝑆 ∨ℋ 𝐶 )
25	3	chshii	⊢ 𝐶 ∈ Sℋ
26	22	chshii	⊢ 𝑆 ∈ Sℋ
27	25 26	shscomi	⊢ ( 𝐶 +ℋ 𝑆 ) = ( 𝑆 +ℋ 𝐶 )
28	3 22	chjcomi	⊢ ( 𝐶 ∨ℋ 𝑆 ) = ( 𝑆 ∨ℋ 𝐶 )
29	24 27 28	3eqtr4i	⊢ ( 𝐶 +ℋ 𝑆 ) = ( 𝐶 ∨ℋ 𝑆 )
30	17 29	ineq12i	⊢ ( ( 𝐵 +ℋ 𝑅 ) ∩ ( 𝐶 +ℋ 𝑆 ) ) = ( ( 𝐵 ∨ℋ 𝑅 ) ∩ ( 𝐶 ∨ℋ 𝑆 ) )