Metamath Proof Explorer

Theorem fh4i

Description: Variation of the Foulis-Holland Theorem. (Contributed by NM, 16-Jan-2005) (New usage is discouraged.)

Ref Expression
Hypotheses fh1.1 ⊢ 𝐴 ∈ Cℋ
fh1.2 ⊢ 𝐵 ∈ Cℋ
fh1.3 ⊢ 𝐶 ∈ Cℋ
fh1.4 ⊢ 𝐴 𝐶ℋ 𝐵
fh1.5 ⊢ 𝐴 𝐶ℋ 𝐶
Assertion fh4i ( 𝐵 ∨ℋ ( 𝐴 ∩ 𝐶 ) ) = ( ( 𝐵 ∨ℋ 𝐴 ) ∩ ( 𝐵 ∨ℋ 𝐶 ) )

Proof

Step Hyp Ref Expression
1 fh1.1 ⊢ 𝐴 ∈ Cℋ
2 fh1.2 ⊢ 𝐵 ∈ Cℋ
3 fh1.3 ⊢ 𝐶 ∈ Cℋ
4 fh1.4 ⊢ 𝐴 𝐶ℋ 𝐵
5 fh1.5 ⊢ 𝐴 𝐶ℋ 𝐶
6 1 choccli ⊢ ( ⊥ ‘ 𝐴 ) ∈ Cℋ
7 2 choccli ⊢ ( ⊥ ‘ 𝐵 ) ∈ Cℋ
8 3 choccli ⊢ ( ⊥ ‘ 𝐶 ) ∈ Cℋ
9 1 2 4 cmcm3ii ⊢ ( ⊥ ‘ 𝐴 ) 𝐶ℋ 𝐵
10 6 2 9 cmcm2ii ⊢ ( ⊥ ‘ 𝐴 ) 𝐶ℋ ( ⊥ ‘ 𝐵 )
11 1 3 5 cmcm3ii ⊢ ( ⊥ ‘ 𝐴 ) 𝐶ℋ 𝐶
12 6 3 11 cmcm2ii ⊢ ( ⊥ ‘ 𝐴 ) 𝐶ℋ ( ⊥ ‘ 𝐶 )
13 6 7 8 10 12 fh2i ⊢ ( ( ⊥ ‘ 𝐵 ) ∩ ( ( ⊥ ‘ 𝐴 ) ∨ℋ ( ⊥ ‘ 𝐶 ) ) ) = ( ( ( ⊥ ‘ 𝐵 ) ∩ ( ⊥ ‘ 𝐴 ) ) ∨ℋ ( ( ⊥ ‘ 𝐵 ) ∩ ( ⊥ ‘ 𝐶 ) ) )
14 1 3 chdmm1i ⊢ ( ⊥ ‘ ( 𝐴 ∩ 𝐶 ) ) = ( ( ⊥ ‘ 𝐴 ) ∨ℋ ( ⊥ ‘ 𝐶 ) )
15 14 ineq2i ⊢ ( ( ⊥ ‘ 𝐵 ) ∩ ( ⊥ ‘ ( 𝐴 ∩ 𝐶 ) ) ) = ( ( ⊥ ‘ 𝐵 ) ∩ ( ( ⊥ ‘ 𝐴 ) ∨ℋ ( ⊥ ‘ 𝐶 ) ) )
16 2 1 chdmj1i ⊢ ( ⊥ ‘ ( 𝐵 ∨ℋ 𝐴 ) ) = ( ( ⊥ ‘ 𝐵 ) ∩ ( ⊥ ‘ 𝐴 ) )
17 2 3 chdmj1i ⊢ ( ⊥ ‘ ( 𝐵 ∨ℋ 𝐶 ) ) = ( ( ⊥ ‘ 𝐵 ) ∩ ( ⊥ ‘ 𝐶 ) )
18 16 17 oveq12i ⊢ ( ( ⊥ ‘ ( 𝐵 ∨ℋ 𝐴 ) ) ∨ℋ ( ⊥ ‘ ( 𝐵 ∨ℋ 𝐶 ) ) ) = ( ( ( ⊥ ‘ 𝐵 ) ∩ ( ⊥ ‘ 𝐴 ) ) ∨ℋ ( ( ⊥ ‘ 𝐵 ) ∩ ( ⊥ ‘ 𝐶 ) ) )
19 13 15 18 3eqtr4ri ⊢ ( ( ⊥ ‘ ( 𝐵 ∨ℋ 𝐴 ) ) ∨ℋ ( ⊥ ‘ ( 𝐵 ∨ℋ 𝐶 ) ) ) = ( ( ⊥ ‘ 𝐵 ) ∩ ( ⊥ ‘ ( 𝐴 ∩ 𝐶 ) ) )
20 2 1 chjcli ⊢ ( 𝐵 ∨ℋ 𝐴 ) ∈ Cℋ
21 2 3 chjcli ⊢ ( 𝐵 ∨ℋ 𝐶 ) ∈ Cℋ
22 20 21 chdmm1i ⊢ ( ⊥ ‘ ( ( 𝐵 ∨ℋ 𝐴 ) ∩ ( 𝐵 ∨ℋ 𝐶 ) ) ) = ( ( ⊥ ‘ ( 𝐵 ∨ℋ 𝐴 ) ) ∨ℋ ( ⊥ ‘ ( 𝐵 ∨ℋ 𝐶 ) ) )
23 1 3 chincli ⊢ ( 𝐴 ∩ 𝐶 ) ∈ Cℋ
24 2 23 chdmj1i ⊢ ( ⊥ ‘ ( 𝐵 ∨ℋ ( 𝐴 ∩ 𝐶 ) ) ) = ( ( ⊥ ‘ 𝐵 ) ∩ ( ⊥ ‘ ( 𝐴 ∩ 𝐶 ) ) )
25 19 22 24 3eqtr4i ⊢ ( ⊥ ‘ ( ( 𝐵 ∨ℋ 𝐴 ) ∩ ( 𝐵 ∨ℋ 𝐶 ) ) ) = ( ⊥ ‘ ( 𝐵 ∨ℋ ( 𝐴 ∩ 𝐶 ) ) )
26 2 23 chjcli ⊢ ( 𝐵 ∨ℋ ( 𝐴 ∩ 𝐶 ) ) ∈ Cℋ
27 20 21 chincli ⊢ ( ( 𝐵 ∨ℋ 𝐴 ) ∩ ( 𝐵 ∨ℋ 𝐶 ) ) ∈ Cℋ
28 26 27 chcon3i ⊢ ( ( 𝐵 ∨ℋ ( 𝐴 ∩ 𝐶 ) ) = ( ( 𝐵 ∨ℋ 𝐴 ) ∩ ( 𝐵 ∨ℋ 𝐶 ) ) ↔ ( ⊥ ‘ ( ( 𝐵 ∨ℋ 𝐴 ) ∩ ( 𝐵 ∨ℋ 𝐶 ) ) ) = ( ⊥ ‘ ( 𝐵 ∨ℋ ( 𝐴 ∩ 𝐶 ) ) ) )
29 25 28 mpbir ⊢ ( 𝐵 ∨ℋ ( 𝐴 ∩ 𝐶 ) ) = ( ( 𝐵 ∨ℋ 𝐴 ) ∩ ( 𝐵 ∨ℋ 𝐶 ) )