Description: Foulis-Holland Theorem. If any 2 pairs in a triple of orthomodular lattice elements commute, the triple is distributive. First 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 | fh1i | |- ( A i^i ( B vH C ) ) = ( ( A i^i B ) vH ( A 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 | 1 2 3 | 3pm3.2i | |- ( A e. CH /\ B e. CH /\ C e. CH ) |
| 7 | 4 5 | pm3.2i | |- ( A C_H B /\ A C_H C ) |
| 8 | fh1 | |- ( ( ( A e. CH /\ B e. CH /\ C e. CH ) /\ ( A C_H B /\ A C_H C ) ) -> ( A i^i ( B vH C ) ) = ( ( A i^i B ) vH ( A i^i C ) ) ) |
|
| 9 | 6 7 8 | mp2an | |- ( A i^i ( B vH C ) ) = ( ( A i^i B ) vH ( A i^i C ) ) |