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 
|- A e. CH
fh1.2 
|- B e. CH
fh1.3 
|- C e. CH
fh1.4 
|- A C_H B
fh1.5 
|- A C_H C
Assertion fh4i 
|- ( B vH ( A i^i C ) ) = ( ( B vH A ) i^i ( B vH C ) )

Proof

Step Hyp Ref Expression
1 fh1.1 
 |-  A e. CH
2 fh1.2 
 |-  B e. CH
3 fh1.3 
 |-  C e. CH
4 fh1.4 
 |-  A C_H B
5 fh1.5 
 |-  A C_H C
6 1 choccli 
 |-  ( _|_ ` A ) e. CH
7 2 choccli 
 |-  ( _|_ ` B ) e. CH
8 3 choccli 
 |-  ( _|_ ` C ) e. CH
9 1 2 4 cmcm3ii 
 |-  ( _|_ ` A ) C_H B
10 6 2 9 cmcm2ii 
 |-  ( _|_ ` A ) C_H ( _|_ ` B )
11 1 3 5 cmcm3ii 
 |-  ( _|_ ` A ) C_H C
12 6 3 11 cmcm2ii 
 |-  ( _|_ ` A ) C_H ( _|_ ` C )
13 6 7 8 10 12 fh2i 
 |-  ( ( _|_ ` B ) i^i ( ( _|_ ` A ) vH ( _|_ ` C ) ) ) = ( ( ( _|_ ` B ) i^i ( _|_ ` A ) ) vH ( ( _|_ ` B ) i^i ( _|_ ` C ) ) )
14 1 3 chdmm1i 
 |-  ( _|_ ` ( A i^i C ) ) = ( ( _|_ ` A ) vH ( _|_ ` C ) )
15 14 ineq2i 
 |-  ( ( _|_ ` B ) i^i ( _|_ ` ( A i^i C ) ) ) = ( ( _|_ ` B ) i^i ( ( _|_ ` A ) vH ( _|_ ` C ) ) )
16 2 1 chdmj1i 
 |-  ( _|_ ` ( B vH A ) ) = ( ( _|_ ` B ) i^i ( _|_ ` A ) )
17 2 3 chdmj1i 
 |-  ( _|_ ` ( B vH C ) ) = ( ( _|_ ` B ) i^i ( _|_ ` C ) )
18 16 17 oveq12i 
 |-  ( ( _|_ ` ( B vH A ) ) vH ( _|_ ` ( B vH C ) ) ) = ( ( ( _|_ ` B ) i^i ( _|_ ` A ) ) vH ( ( _|_ ` B ) i^i ( _|_ ` C ) ) )
19 13 15 18 3eqtr4ri 
 |-  ( ( _|_ ` ( B vH A ) ) vH ( _|_ ` ( B vH C ) ) ) = ( ( _|_ ` B ) i^i ( _|_ ` ( A i^i C ) ) )
20 2 1 chjcli 
 |-  ( B vH A ) e. CH
21 2 3 chjcli 
 |-  ( B vH C ) e. CH
22 20 21 chdmm1i 
 |-  ( _|_ ` ( ( B vH A ) i^i ( B vH C ) ) ) = ( ( _|_ ` ( B vH A ) ) vH ( _|_ ` ( B vH C ) ) )
23 1 3 chincli 
 |-  ( A i^i C ) e. CH
24 2 23 chdmj1i 
 |-  ( _|_ ` ( B vH ( A i^i C ) ) ) = ( ( _|_ ` B ) i^i ( _|_ ` ( A i^i C ) ) )
25 19 22 24 3eqtr4i 
 |-  ( _|_ ` ( ( B vH A ) i^i ( B vH C ) ) ) = ( _|_ ` ( B vH ( A i^i C ) ) )
26 2 23 chjcli 
 |-  ( B vH ( A i^i C ) ) e. CH
27 20 21 chincli 
 |-  ( ( B vH A ) i^i ( B vH C ) ) e. CH
28 26 27 chcon3i 
 |-  ( ( B vH ( A i^i C ) ) = ( ( B vH A ) i^i ( B vH C ) ) <-> ( _|_ ` ( ( B vH A ) i^i ( B vH C ) ) ) = ( _|_ ` ( B vH ( A i^i C ) ) ) )
29 25 28 mpbir 
 |-  ( B vH ( A i^i C ) ) = ( ( B vH A ) i^i ( B vH C ) )