Metamath Proof Explorer

Theorem 3oalem6

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 3oalem6 ( 𝐵 +ℋ ( 𝑅 ∩ ( 𝑆 +ℋ ( ( 𝐵 +ℋ 𝐶 ) ∩ ( 𝑅 +ℋ 𝑆 ) ) ) ) ) ⊆ ( 𝐵 ∨ℋ ( 𝑅 ∩ ( 𝑆 ∨ℋ ( ( 𝐵 ∨ℋ 𝐶 ) ∩ ( 𝑅 ∨ℋ 𝑆 ) ) ) ) )

Proof

Step Hyp Ref Expression
1 3oa.1 ⊢ 𝐴 ∈ Cℋ
2 3oa.2 ⊢ 𝐵 ∈ Cℋ
3 3oa.3 ⊢ 𝐶 ∈ Cℋ
4 3oa.4 ⊢ 𝑅 = ( ( ⊥ ‘ 𝐵 ) ∩ ( 𝐵 ∨ℋ 𝐴 ) )
5 3oa.5 ⊢ 𝑆 = ( ( ⊥ ‘ 𝐶 ) ∩ ( 𝐶 ∨ℋ 𝐴 ) )
6 2 chshii ⊢ 𝐵 ∈ Sℋ
7 2 choccli ⊢ ( ⊥ ‘ 𝐵 ) ∈ Cℋ
8 2 1 chjcli ⊢ ( 𝐵 ∨ℋ 𝐴 ) ∈ Cℋ
9 7 8 chincli ⊢ ( ( ⊥ ‘ 𝐵 ) ∩ ( 𝐵 ∨ℋ 𝐴 ) ) ∈ Cℋ
10 4 9 eqeltri ⊢ 𝑅 ∈ Cℋ
11 10 chshii ⊢ 𝑅 ∈ Sℋ
12 3 choccli ⊢ ( ⊥ ‘ 𝐶 ) ∈ Cℋ
13 3 1 chjcli ⊢ ( 𝐶 ∨ℋ 𝐴 ) ∈ Cℋ
14 12 13 chincli ⊢ ( ( ⊥ ‘ 𝐶 ) ∩ ( 𝐶 ∨ℋ 𝐴 ) ) ∈ Cℋ
15 5 14 eqeltri ⊢ 𝑆 ∈ Cℋ
16 15 chshii ⊢ 𝑆 ∈ Sℋ
17 3 chshii ⊢ 𝐶 ∈ Sℋ
18 6 17 shscli ⊢ ( 𝐵 +ℋ 𝐶 ) ∈ Sℋ
19 11 16 shscli ⊢ ( 𝑅 +ℋ 𝑆 ) ∈ Sℋ
20 18 19 shincli ⊢ ( ( 𝐵 +ℋ 𝐶 ) ∩ ( 𝑅 +ℋ 𝑆 ) ) ∈ Sℋ
21 16 20 shscli ⊢ ( 𝑆 +ℋ ( ( 𝐵 +ℋ 𝐶 ) ∩ ( 𝑅 +ℋ 𝑆 ) ) ) ∈ Sℋ
22 11 21 shincli ⊢ ( 𝑅 ∩ ( 𝑆 +ℋ ( ( 𝐵 +ℋ 𝐶 ) ∩ ( 𝑅 +ℋ 𝑆 ) ) ) ) ∈ Sℋ
23 6 22 shsleji ⊢ ( 𝐵 +ℋ ( 𝑅 ∩ ( 𝑆 +ℋ ( ( 𝐵 +ℋ 𝐶 ) ∩ ( 𝑅 +ℋ 𝑆 ) ) ) ) ) ⊆ ( 𝐵 ∨ℋ ( 𝑅 ∩ ( 𝑆 +ℋ ( ( 𝐵 +ℋ 𝐶 ) ∩ ( 𝑅 +ℋ 𝑆 ) ) ) ) )
24 16 20 shsleji ⊢ ( 𝑆 +ℋ ( ( 𝐵 +ℋ 𝐶 ) ∩ ( 𝑅 +ℋ 𝑆 ) ) ) ⊆ ( 𝑆 ∨ℋ ( ( 𝐵 +ℋ 𝐶 ) ∩ ( 𝑅 +ℋ 𝑆 ) ) )
25 2 3 chsleji ⊢ ( 𝐵 +ℋ 𝐶 ) ⊆ ( 𝐵 ∨ℋ 𝐶 )
26 ssrin ⊢ ( ( 𝐵 +ℋ 𝐶 ) ⊆ ( 𝐵 ∨ℋ 𝐶 ) → ( ( 𝐵 +ℋ 𝐶 ) ∩ ( 𝑅 +ℋ 𝑆 ) ) ⊆ ( ( 𝐵 ∨ℋ 𝐶 ) ∩ ( 𝑅 +ℋ 𝑆 ) ) )
27 25 26 ax-mp ⊢ ( ( 𝐵 +ℋ 𝐶 ) ∩ ( 𝑅 +ℋ 𝑆 ) ) ⊆ ( ( 𝐵 ∨ℋ 𝐶 ) ∩ ( 𝑅 +ℋ 𝑆 ) )
28 10 15 chsleji ⊢ ( 𝑅 +ℋ 𝑆 ) ⊆ ( 𝑅 ∨ℋ 𝑆 )
29 sslin ⊢ ( ( 𝑅 +ℋ 𝑆 ) ⊆ ( 𝑅 ∨ℋ 𝑆 ) → ( ( 𝐵 ∨ℋ 𝐶 ) ∩ ( 𝑅 +ℋ 𝑆 ) ) ⊆ ( ( 𝐵 ∨ℋ 𝐶 ) ∩ ( 𝑅 ∨ℋ 𝑆 ) ) )
30 28 29 ax-mp ⊢ ( ( 𝐵 ∨ℋ 𝐶 ) ∩ ( 𝑅 +ℋ 𝑆 ) ) ⊆ ( ( 𝐵 ∨ℋ 𝐶 ) ∩ ( 𝑅 ∨ℋ 𝑆 ) )
31 27 30 sstri ⊢ ( ( 𝐵 +ℋ 𝐶 ) ∩ ( 𝑅 +ℋ 𝑆 ) ) ⊆ ( ( 𝐵 ∨ℋ 𝐶 ) ∩ ( 𝑅 ∨ℋ 𝑆 ) )
32 2 3 chjcli ⊢ ( 𝐵 ∨ℋ 𝐶 ) ∈ Cℋ
33 10 15 chjcli ⊢ ( 𝑅 ∨ℋ 𝑆 ) ∈ Cℋ
34 32 33 chincli ⊢ ( ( 𝐵 ∨ℋ 𝐶 ) ∩ ( 𝑅 ∨ℋ 𝑆 ) ) ∈ Cℋ
35 34 chshii ⊢ ( ( 𝐵 ∨ℋ 𝐶 ) ∩ ( 𝑅 ∨ℋ 𝑆 ) ) ∈ Sℋ
36 20 35 16 shlej2i ⊢ ( ( ( 𝐵 +ℋ 𝐶 ) ∩ ( 𝑅 +ℋ 𝑆 ) ) ⊆ ( ( 𝐵 ∨ℋ 𝐶 ) ∩ ( 𝑅 ∨ℋ 𝑆 ) ) → ( 𝑆 ∨ℋ ( ( 𝐵 +ℋ 𝐶 ) ∩ ( 𝑅 +ℋ 𝑆 ) ) ) ⊆ ( 𝑆 ∨ℋ ( ( 𝐵 ∨ℋ 𝐶 ) ∩ ( 𝑅 ∨ℋ 𝑆 ) ) ) )
37 31 36 ax-mp ⊢ ( 𝑆 ∨ℋ ( ( 𝐵 +ℋ 𝐶 ) ∩ ( 𝑅 +ℋ 𝑆 ) ) ) ⊆ ( 𝑆 ∨ℋ ( ( 𝐵 ∨ℋ 𝐶 ) ∩ ( 𝑅 ∨ℋ 𝑆 ) ) )
38 24 37 sstri ⊢ ( 𝑆 +ℋ ( ( 𝐵 +ℋ 𝐶 ) ∩ ( 𝑅 +ℋ 𝑆 ) ) ) ⊆ ( 𝑆 ∨ℋ ( ( 𝐵 ∨ℋ 𝐶 ) ∩ ( 𝑅 ∨ℋ 𝑆 ) ) )
39 sslin ⊢ ( ( 𝑆 +ℋ ( ( 𝐵 +ℋ 𝐶 ) ∩ ( 𝑅 +ℋ 𝑆 ) ) ) ⊆ ( 𝑆 ∨ℋ ( ( 𝐵 ∨ℋ 𝐶 ) ∩ ( 𝑅 ∨ℋ 𝑆 ) ) ) → ( 𝑅 ∩ ( 𝑆 +ℋ ( ( 𝐵 +ℋ 𝐶 ) ∩ ( 𝑅 +ℋ 𝑆 ) ) ) ) ⊆ ( 𝑅 ∩ ( 𝑆 ∨ℋ ( ( 𝐵 ∨ℋ 𝐶 ) ∩ ( 𝑅 ∨ℋ 𝑆 ) ) ) ) )
40 38 39 ax-mp ⊢ ( 𝑅 ∩ ( 𝑆 +ℋ ( ( 𝐵 +ℋ 𝐶 ) ∩ ( 𝑅 +ℋ 𝑆 ) ) ) ) ⊆ ( 𝑅 ∩ ( 𝑆 ∨ℋ ( ( 𝐵 ∨ℋ 𝐶 ) ∩ ( 𝑅 ∨ℋ 𝑆 ) ) ) )
41 15 34 chjcli ⊢ ( 𝑆 ∨ℋ ( ( 𝐵 ∨ℋ 𝐶 ) ∩ ( 𝑅 ∨ℋ 𝑆 ) ) ) ∈ Cℋ
42 10 41 chincli ⊢ ( 𝑅 ∩ ( 𝑆 ∨ℋ ( ( 𝐵 ∨ℋ 𝐶 ) ∩ ( 𝑅 ∨ℋ 𝑆 ) ) ) ) ∈ Cℋ
43 42 chshii ⊢ ( 𝑅 ∩ ( 𝑆 ∨ℋ ( ( 𝐵 ∨ℋ 𝐶 ) ∩ ( 𝑅 ∨ℋ 𝑆 ) ) ) ) ∈ Sℋ
44 22 43 6 shlej2i ⊢ ( ( 𝑅 ∩ ( 𝑆 +ℋ ( ( 𝐵 +ℋ 𝐶 ) ∩ ( 𝑅 +ℋ 𝑆 ) ) ) ) ⊆ ( 𝑅 ∩ ( 𝑆 ∨ℋ ( ( 𝐵 ∨ℋ 𝐶 ) ∩ ( 𝑅 ∨ℋ 𝑆 ) ) ) ) → ( 𝐵 ∨ℋ ( 𝑅 ∩ ( 𝑆 +ℋ ( ( 𝐵 +ℋ 𝐶 ) ∩ ( 𝑅 +ℋ 𝑆 ) ) ) ) ) ⊆ ( 𝐵 ∨ℋ ( 𝑅 ∩ ( 𝑆 ∨ℋ ( ( 𝐵 ∨ℋ 𝐶 ) ∩ ( 𝑅 ∨ℋ 𝑆 ) ) ) ) ) )
45 40 44 ax-mp ⊢ ( 𝐵 ∨ℋ ( 𝑅 ∩ ( 𝑆 +ℋ ( ( 𝐵 +ℋ 𝐶 ) ∩ ( 𝑅 +ℋ 𝑆 ) ) ) ) ) ⊆ ( 𝐵 ∨ℋ ( 𝑅 ∩ ( 𝑆 ∨ℋ ( ( 𝐵 ∨ℋ 𝐶 ) ∩ ( 𝑅 ∨ℋ 𝑆 ) ) ) ) )
46 23 45 sstri ⊢ ( 𝐵 +ℋ ( 𝑅 ∩ ( 𝑆 +ℋ ( ( 𝐵 +ℋ 𝐶 ) ∩ ( 𝑅 +ℋ 𝑆 ) ) ) ) ) ⊆ ( 𝐵 ∨ℋ ( 𝑅 ∩ ( 𝑆 ∨ℋ ( ( 𝐵 ∨ℋ 𝐶 ) ∩ ( 𝑅 ∨ℋ 𝑆 ) ) ) ) )