Metamath Proof Explorer


Theorem ledi

Description: An ortholattice is distributive in one ordering direction. (Contributed by NM, 14-Jun-2006) (New usage is discouraged.)

Ref Expression
Assertion ledi A C B C C C A B A C A B C

Proof

Step Hyp Ref Expression
1 ineq1 A = if A C A 0 A B = if A C A 0 B
2 ineq1 A = if A C A 0 A C = if A C A 0 C
3 1 2 oveq12d A = if A C A 0 A B A C = if A C A 0 B if A C A 0 C
4 ineq1 A = if A C A 0 A B C = if A C A 0 B C
5 3 4 sseq12d A = if A C A 0 A B A C A B C if A C A 0 B if A C A 0 C if A C A 0 B C
6 ineq2 B = if B C B 0 if A C A 0 B = if A C A 0 if B C B 0
7 6 oveq1d B = if B C B 0 if A C A 0 B if A C A 0 C = if A C A 0 if B C B 0 if A C A 0 C
8 oveq1 B = if B C B 0 B C = if B C B 0 C
9 8 ineq2d B = if B C B 0 if A C A 0 B C = if A C A 0 if B C B 0 C
10 7 9 sseq12d B = if B C B 0 if A C A 0 B if A C A 0 C if A C A 0 B C if A C A 0 if B C B 0 if A C A 0 C if A C A 0 if B C B 0 C
11 ineq2 C = if C C C 0 if A C A 0 C = if A C A 0 if C C C 0
12 11 oveq2d C = if C C C 0 if A C A 0 if B C B 0 if A C A 0 C = if A C A 0 if B C B 0 if A C A 0 if C C C 0
13 oveq2 C = if C C C 0 if B C B 0 C = if B C B 0 if C C C 0
14 13 ineq2d C = if C C C 0 if A C A 0 if B C B 0 C = if A C A 0 if B C B 0 if C C C 0
15 12 14 sseq12d C = if C C C 0 if A C A 0 if B C B 0 if A C A 0 C if A C A 0 if B C B 0 C if A C A 0 if B C B 0 if A C A 0 if C C C 0 if A C A 0 if B C B 0 if C C C 0
16 h0elch 0 C
17 16 elimel if A C A 0 C
18 16 elimel if B C B 0 C
19 16 elimel if C C C 0 C
20 17 18 19 ledii if A C A 0 if B C B 0 if A C A 0 if C C C 0 if A C A 0 if B C B 0 if C C C 0
21 5 10 15 20 dedth3h A C B C C C A B A C A B C