Quantum Logic Explorer		< Previous   Next > Nearby theorems
Mirrors  >  Home  >  QLE Home  >  Th. List  >  dp32		Unicode version

---

Theorem dp32 1194

Description: Part of theorem from Alan Day and Doug Pickering, "A note on the Arguesian lattice identity," Studia Sci. Math. Hungar. 19:303-305 (1982). (3)=>(2)

Hypotheses

Ref	Expression
dp32.1	c0 a1 a2 b1 b2
dp32.2	c1 a0 a2 b0 b2
dp32.3	c2 a0 a1 b0 b1
dp32.4	a0 b0 a1 b1 a2 b2

Assertion

Ref	Expression
dp32	a0 a1 c2 c0 c1 b0 b1 c2 c0 c1

---

Proof of Theorem dp32

Step	Hyp	Ref	Expression
1		dp32.1	. . . 4 c0 a1 a2 b1 b2
2		dp32.2	. . . 4 c1 a0 a2 b0 b2
3		dp32.3	. . . 4 c2 a0 a1 b0 b1
4		dp32.4	. . . 4 a0 b0 a1 b1 a2 b2
5	1, 2, 3, 4	dp53 1168	. . 3 a0 b0 b1 c2 c0 c1
6		ancom 74	. . . . 5 a1 a2 b1 b2 b1 b2 a1 a2
7	1, 6	tr 62	. . . 4 c0 b1 b2 a1 a2
8		ancom 74	. . . . 5 a0 a2 b0 b2 b0 b2 a0 a2
9	2, 8	tr 62	. . . 4 c1 b0 b2 a0 a2
10		ancom 74	. . . . 5 a0 a1 b0 b1 b0 b1 a0 a1
11	3, 10	tr 62	. . . 4 c2 b0 b1 a0 a1
12		orcom 73	. . . . . . 7 a0 b0 b0 a0
13		orcom 73	. . . . . . 7 a1 b1 b1 a1
14	12, 13	2an 79	. . . . . 6 a0 b0 a1 b1 b0 a0 b1 a1
15		orcom 73	. . . . . 6 a2 b2 b2 a2
16	14, 15	2an 79	. . . . 5 a0 b0 a1 b1 a2 b2 b0 a0 b1 a1 b2 a2
17	4, 16	tr 62	. . . 4 b0 a0 b1 a1 b2 a2
18	7, 9, 11, 17	dp53 1168	. . 3 b0 a0 a1 c2 c0 c1
19	5, 18	ler2an 173	. 2 a0 b0 b1 c2 c0 c1 b0 a0 a1 c2 c0 c1
20		leao1 162	. . . 4 a0 a1 c2 c0 c1 a0 b0 b1 c2 c0 c1
21	20	mldual2i 1125	. . 3 a0 b0 b1 c2 c0 c1 b0 a0 a1 c2 c0 c1 a0 b0 b1 c2 c0 c1 b0 a0 a1 c2 c0 c1
22		ancom 74	. . . . 5 a0 b0 b1 c2 c0 c1 b0 b0 a0 b0 b1 c2 c0 c1
23		mldual 1122	. . . . 5 b0 a0 b0 b1 c2 c0 c1 b0 a0 b0 b1 c2 c0 c1
24		leao2 163	. . . . . . . . . . 11 b0 a0 a0 a1
25		leao1 162	. . . . . . . . . . 11 b0 a0 b0 b1
26	24, 25	ler2an 173	. . . . . . . . . 10 b0 a0 a0 a1 b0 b1
27	3	cm 61	. . . . . . . . . 10 a0 a1 b0 b1 c2
28	26, 27	lbtr 139	. . . . . . . . 9 b0 a0 c2
29		leao2 163	. . . . . . . . . . . 12 b0 a0 a0 a2
30		leao1 162	. . . . . . . . . . . 12 b0 a0 b0 b2
31	29, 30	ler2an 173	. . . . . . . . . . 11 b0 a0 a0 a2 b0 b2
32	2	cm 61	. . . . . . . . . . 11 a0 a2 b0 b2 c1
33	31, 32	lbtr 139	. . . . . . . . . 10 b0 a0 c1
34	33	lerr 150	. . . . . . . . 9 b0 a0 c0 c1
35	28, 34	ler2an 173	. . . . . . . 8 b0 a0 c2 c0 c1
36	35	lerr 150	. . . . . . 7 b0 a0 b1 c2 c0 c1
37	36	ml2i 1123	. . . . . 6 b0 a0 b0 b1 c2 c0 c1 b0 a0 b0 b1 c2 c0 c1
38		lea 160	. . . . . . . 8 b0 a0 b0
39	38	df-le2 131	. . . . . . 7 b0 a0 b0 b0
40	39	ran 78	. . . . . 6 b0 a0 b0 b1 c2 c0 c1 b0 b1 c2 c0 c1
41	37, 40	tr 62	. . . . 5 b0 a0 b0 b1 c2 c0 c1 b0 b1 c2 c0 c1
42	22, 23, 41	3tr 65	. . . 4 a0 b0 b1 c2 c0 c1 b0 b0 b1 c2 c0 c1
43	42	ror 71	. . 3 a0 b0 b1 c2 c0 c1 b0 a0 a1 c2 c0 c1 b0 b1 c2 c0 c1 a0 a1 c2 c0 c1
44		orcom 73	. . 3 b0 b1 c2 c0 c1 a0 a1 c2 c0 c1 a0 a1 c2 c0 c1 b0 b1 c2 c0 c1
45	21, 43, 44	3tr 65	. 2 a0 b0 b1 c2 c0 c1 b0 a0 a1 c2 c0 c1 a0 a1 c2 c0 c1 b0 b1 c2 c0 c1
46	19, 45	lbtr 139	1 a0 a1 c2 c0 c1 b0 b1 c2 c0 c1

Colors of variables: term

Syntax hints:   wb 1   wle 2   wo 6   wa 7

This theorem was proved from axioms:  ax-a1 30  ax-a2 31  ax-a3 32  ax-a4 33  ax-a5 34  ax-r1 35  ax-r2 36  ax-r4 37  ax-r5 38  ax-ml 1120  ax-arg 1151

This theorem depends on definitions:  df-a 40  df-t 41  df-f 42  df-le1 130  df-le2 131

This theorem is referenced by:  dp23  1195

Copyright terms: Public domain

W3C validator