Theorem e2ast2 894

Description: Show that the E*₂ derivative on p. 23 of Mayet, "Equations holding in Hilbert lattices" IJTP 2006, holds in all OMLs. (Contributed by NM, 24-Jun-2006.)

Hypotheses

Ref	Expression
e2ast2.1	a ≤ b⊥
e2ast2.2	c ≤ d⊥
e2ast2.3	a ≤ c⊥

Assertion

Ref	Expression
e2ast2	((a ∪ b) ∩ (c ∪ d)) ≤ ((b ∪ d) ∪ (a ∪ c)⊥ )

Proof of Theorem e2ast2

Step	Hyp	Ref	Expression
1		e2ast2.3	. . . 4 a ≤ c⊥
2	1	leror 152	. . 3 (a ∪ b) ≤ (c⊥ ∪ b)
3	1	lecon3 157	. . . 4 c ≤ a⊥
4	3	leror 152	. . 3 (c ∪ d) ≤ (a⊥ ∪ d)
5	2, 4	le2an 169	. 2 ((a ∪ b) ∩ (c ∪ d)) ≤ ((c⊥ ∪ b) ∩ (a⊥ ∪ d))
6		e2ast2.2	. . . . . . . . . . 11 c ≤ d⊥
7	6	lecon3 157	. . . . . . . . . 10 d ≤ c⊥
8	7	lecom 180	. . . . . . . . 9 d C c⊥
9	8	comcom 453	. . . . . . . 8 c⊥ C d
10	1	lecom 180	. . . . . . . . . 10 a C c⊥
11	10	comcom 453	. . . . . . . . 9 c⊥ C a
12	11	comcom2 183	. . . . . . . 8 c⊥ C a⊥
13	9, 12	fh4c 478	. . . . . . 7 (d ∪ (a⊥ ∩ c⊥ )) = ((d ∪ a⊥ ) ∩ (d ∪ c⊥ ))
14	7	df-le2 131	. . . . . . . 8 (d ∪ c⊥ ) = c⊥
15	14	lan 77	. . . . . . 7 ((d ∪ a⊥ ) ∩ (d ∪ c⊥ )) = ((d ∪ a⊥ ) ∩ c⊥ )
16	13, 15	ax-r2 36	. . . . . 6 (d ∪ (a⊥ ∩ c⊥ )) = ((d ∪ a⊥ ) ∩ c⊥ )
17	16	ax-r1 35	. . . . 5 ((d ∪ a⊥ ) ∩ c⊥ ) = (d ∪ (a⊥ ∩ c⊥ ))
18		anor3 90	. . . . . 6 (a⊥ ∩ c⊥ ) = (a ∪ c)⊥
19	18	lor 70	. . . . 5 (d ∪ (a⊥ ∩ c⊥ )) = (d ∪ (a ∪ c)⊥ )
20	17, 19	ax-r2 36	. . . 4 ((d ∪ a⊥ ) ∩ c⊥ ) = (d ∪ (a ∪ c)⊥ )
21	20	lor 70	. . 3 (b ∪ ((d ∪ a⊥ ) ∩ c⊥ )) = (b ∪ (d ∪ (a ∪ c)⊥ ))
22		leao4 165	. . . . . . . . 9 (b ∩ a⊥ ) ≤ (d ∪ a⊥ )
23	22	lecom 180	. . . . . . . 8 (b ∩ a⊥ ) C (d ∪ a⊥ )
24	23	comcom 453	. . . . . . 7 (d ∪ a⊥ ) C (b ∩ a⊥ )
25	9, 12	com2or 483	. . . . . . . 8 c⊥ C (d ∪ a⊥ )
26	25	comcom 453	. . . . . . 7 (d ∪ a⊥ ) C c⊥
27	24, 26	fh4 472	. . . . . 6 ((b ∩ a⊥ ) ∪ ((d ∪ a⊥ ) ∩ c⊥ )) = (((b ∩ a⊥ ) ∪ (d ∪ a⊥ )) ∩ ((b ∩ a⊥ ) ∪ c⊥ ))
28		or32 82	. . . . . . . 8 (((b ∩ a⊥ ) ∪ d) ∪ a⊥ ) = (((b ∩ a⊥ ) ∪ a⊥ ) ∪ d)
29		ax-a3 32	. . . . . . . 8 (((b ∩ a⊥ ) ∪ d) ∪ a⊥ ) = ((b ∩ a⊥ ) ∪ (d ∪ a⊥ ))
30		lear 161	. . . . . . . . . 10 (b ∩ a⊥ ) ≤ a⊥
31	30	df-le2 131	. . . . . . . . 9 ((b ∩ a⊥ ) ∪ a⊥ ) = a⊥
32	31	ax-r5 38	. . . . . . . 8 (((b ∩ a⊥ ) ∪ a⊥ ) ∪ d) = (a⊥ ∪ d)
33	28, 29, 32	3tr2 64	. . . . . . 7 ((b ∩ a⊥ ) ∪ (d ∪ a⊥ )) = (a⊥ ∪ d)
34		e2ast2.1	. . . . . . . . . . 11 a ≤ b⊥
35	34	lecon3 157	. . . . . . . . . 10 b ≤ a⊥
36	35	df2le2 136	. . . . . . . . 9 (b ∩ a⊥ ) = b
37	36	ax-r5 38	. . . . . . . 8 ((b ∩ a⊥ ) ∪ c⊥ ) = (b ∪ c⊥ )
38		ax-a2 31	. . . . . . . 8 (b ∪ c⊥ ) = (c⊥ ∪ b)
39	37, 38	ax-r2 36	. . . . . . 7 ((b ∩ a⊥ ) ∪ c⊥ ) = (c⊥ ∪ b)
40	33, 39	2an 79	. . . . . 6 (((b ∩ a⊥ ) ∪ (d ∪ a⊥ )) ∩ ((b ∩ a⊥ ) ∪ c⊥ )) = ((a⊥ ∪ d) ∩ (c⊥ ∪ b))
41		ancom 74	. . . . . 6 ((a⊥ ∪ d) ∩ (c⊥ ∪ b)) = ((c⊥ ∪ b) ∩ (a⊥ ∪ d))
42	27, 40, 41	3tr 65	. . . . 5 ((b ∩ a⊥ ) ∪ ((d ∪ a⊥ ) ∩ c⊥ )) = ((c⊥ ∪ b) ∩ (a⊥ ∪ d))
43	42	ax-r1 35	. . . 4 ((c⊥ ∪ b) ∩ (a⊥ ∪ d)) = ((b ∩ a⊥ ) ∪ ((d ∪ a⊥ ) ∩ c⊥ ))
44	36	ax-r5 38	. . . 4 ((b ∩ a⊥ ) ∪ ((d ∪ a⊥ ) ∩ c⊥ )) = (b ∪ ((d ∪ a⊥ ) ∩ c⊥ ))
45	43, 44	ax-r2 36	. . 3 ((c⊥ ∪ b) ∩ (a⊥ ∪ d)) = (b ∪ ((d ∪ a⊥ ) ∩ c⊥ ))
46		ax-a3 32	. . 3 ((b ∪ d) ∪ (a ∪ c)⊥ ) = (b ∪ (d ∪ (a ∪ c)⊥ ))
47	21, 45, 46	3tr1 63	. 2 ((c⊥ ∪ b) ∩ (a⊥ ∪ d)) = ((b ∪ d) ∪ (a ∪ c)⊥ )
48	5, 47	lbtr 139	1 ((a ∪ b) ∩ (c ∪ d)) ≤ ((b ∪ d) ∪ (a ∪ c)⊥ )

Syntax hints:   ≤ wle 2  ^⊥ wn 4   ∪ 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-r3 439

This theorem depends on definitions:  df-b 39  df-a 40  df-t 41  df-f 42  df-le1 130  df-le2 131  df-c1 132  df-c2 133

This theorem is referenced by: (None)