Theorem 3oai

Description: 3OA (weak) orthoarguesian law. Equation IV of GodowskiGreechie p. 249. (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	3oai	⊢ ( ( 𝐵 ∨ℋ 𝑅 ) ∩ ( 𝐶 ∨ℋ 𝑆 ) ) ⊆ ( 𝐵 ∨ℋ ( 𝑅 ∩ ( 𝑆 ∨ℋ ( ( 𝐵 ∨ℋ 𝐶 ) ∩ ( 𝑅 ∨ℋ 𝑆 ) ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		3oa.1	⊢ 𝐴 ∈ Cℋ
2		3oa.2	⊢ 𝐵 ∈ Cℋ
3		3oa.3	⊢ 𝐶 ∈ Cℋ
4		3oa.4	⊢ 𝑅 = ( ( ⊥ ‘ 𝐵 ) ∩ ( 𝐵 ∨ℋ 𝐴 ) )
5		3oa.5	⊢ 𝑆 = ( ( ⊥ ‘ 𝐶 ) ∩ ( 𝐶 ∨ℋ 𝐴 ) )
6	1 2 3 4 5	3oalem5	⊢ ( ( 𝐵 +ℋ 𝑅 ) ∩ ( 𝐶 +ℋ 𝑆 ) ) = ( ( 𝐵 ∨ℋ 𝑅 ) ∩ ( 𝐶 ∨ℋ 𝑆 ) )
7	2	choccli	⊢ ( ⊥ ‘ 𝐵 ) ∈ Cℋ
8	2 1	chjcli	⊢ ( 𝐵 ∨ℋ 𝐴 ) ∈ Cℋ
9	7 8	chincli	⊢ ( ( ⊥ ‘ 𝐵 ) ∩ ( 𝐵 ∨ℋ 𝐴 ) ) ∈ Cℋ
10	4 9	eqeltri	⊢ 𝑅 ∈ Cℋ
11	3	choccli	⊢ ( ⊥ ‘ 𝐶 ) ∈ Cℋ
12	3 1	chjcli	⊢ ( 𝐶 ∨ℋ 𝐴 ) ∈ Cℋ
13	11 12	chincli	⊢ ( ( ⊥ ‘ 𝐶 ) ∩ ( 𝐶 ∨ℋ 𝐴 ) ) ∈ Cℋ
14	5 13	eqeltri	⊢ 𝑆 ∈ Cℋ
15	2 3 10 14	3oalem3	⊢ ( ( 𝐵 +ℋ 𝑅 ) ∩ ( 𝐶 +ℋ 𝑆 ) ) ⊆ ( 𝐵 +ℋ ( 𝑅 ∩ ( 𝑆 +ℋ ( ( 𝐵 +ℋ 𝐶 ) ∩ ( 𝑅 +ℋ 𝑆 ) ) ) ) )
16	1 2 3 4 5	3oalem6	⊢ ( 𝐵 +ℋ ( 𝑅 ∩ ( 𝑆 +ℋ ( ( 𝐵 +ℋ 𝐶 ) ∩ ( 𝑅 +ℋ 𝑆 ) ) ) ) ) ⊆ ( 𝐵 ∨ℋ ( 𝑅 ∩ ( 𝑆 ∨ℋ ( ( 𝐵 ∨ℋ 𝐶 ) ∩ ( 𝑅 ∨ℋ 𝑆 ) ) ) ) )
17	15 16	sstri	⊢ ( ( 𝐵 +ℋ 𝑅 ) ∩ ( 𝐶 +ℋ 𝑆 ) ) ⊆ ( 𝐵 ∨ℋ ( 𝑅 ∩ ( 𝑆 ∨ℋ ( ( 𝐵 ∨ℋ 𝐶 ) ∩ ( 𝑅 ∨ℋ 𝑆 ) ) ) ) )
18	6 17	eqsstrri	⊢ ( ( 𝐵 ∨ℋ 𝑅 ) ∩ ( 𝐶 ∨ℋ 𝑆 ) ) ⊆ ( 𝐵 ∨ℋ ( 𝑅 ∩ ( 𝑆 ∨ℋ ( ( 𝐵 ∨ℋ 𝐶 ) ∩ ( 𝑅 ∨ℋ 𝑆 ) ) ) ) )