Description: Foulis-Holland Theorem. If any 2 pairs in a triple of orthomodular lattice elements commute, the triple is distributive. Second of two parts. Theorem 5 of Kalmbach p. 25. (Contributed by NM, 7-Aug-2004) (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 | fh2i | |- ( B i^i ( A vH C ) ) = ( ( B i^i A ) vH ( B i^i C ) ) |
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 | 2 1 3 | 3pm3.2i | |- ( B e. CH /\ A e. CH /\ C e. CH ) |
7 | 4 5 | pm3.2i | |- ( A C_H B /\ A C_H C ) |
8 | fh2 | |- ( ( ( B e. CH /\ A e. CH /\ C e. CH ) /\ ( A C_H B /\ A C_H C ) ) -> ( B i^i ( A vH C ) ) = ( ( B i^i A ) vH ( B i^i C ) ) ) |
|
9 | 6 7 8 | mp2an | |- ( B i^i ( A vH C ) ) = ( ( B i^i A ) vH ( B i^i C ) ) |