Theorem e2astlem1 895

Description: Lemma towards a possible proof that E*₂ on p. 23 of Mayet, "Equations holding in Hilbert lattices" IJTP 2006, holds in all OMLs. (Contributed by NM, 25-Jun-2006.)

Hypotheses

Ref	Expression
e2ast.1	a ≤ b⊥
e2ast.2	c ≤ d⊥
e2ast.3	r ≤ a⊥
e2ast.4	a ≤ c⊥
e2ast.5	c ≤ r⊥

Assertion

Ref	Expression
e2astlem1	(((a ∪ b) ∩ (c ∪ d)) ∩ ((a ∪ c) ∪ r)) = ((a ∪ (b ∩ (c ∪ r))) ∩ (c ∪ (d ∩ (a ∪ r))))

Proof of Theorem e2astlem1

Step	Hyp	Ref	Expression
1		anandir 115	. 2 (((a ∪ b) ∩ (c ∪ d)) ∩ ((a ∪ c) ∪ r)) = (((a ∪ b) ∩ ((a ∪ c) ∪ r)) ∩ ((c ∪ d) ∩ ((a ∪ c) ∪ r)))
2		leo 158	. . . . . . 7 a ≤ (a ∪ c)
3	2	ler 149	. . . . . 6 a ≤ ((a ∪ c) ∪ r)
4	3	lecom 180	. . . . 5 a C ((a ∪ c) ∪ r)
5		e2ast.1	. . . . . . 7 a ≤ b⊥
6	5	lecom 180	. . . . . 6 a C b⊥
7	6	comcom7 460	. . . . 5 a C b
8	4, 7	fh2r 474	. . . 4 ((a ∪ b) ∩ ((a ∪ c) ∪ r)) = ((a ∩ ((a ∪ c) ∪ r)) ∪ (b ∩ ((a ∪ c) ∪ r)))
9	3	df2le2 136	. . . . 5 (a ∩ ((a ∪ c) ∪ r)) = a
10		ax-a3 32	. . . . . . 7 ((a ∪ c) ∪ r) = (a ∪ (c ∪ r))
11	10	lan 77	. . . . . 6 (b ∩ ((a ∪ c) ∪ r)) = (b ∩ (a ∪ (c ∪ r)))
12		e2ast.4	. . . . . . . . . . 11 a ≤ c⊥
13	12	lecom 180	. . . . . . . . . 10 a C c⊥
14	13	comcom7 460	. . . . . . . . 9 a C c
15		e2ast.3	. . . . . . . . . . . 12 r ≤ a⊥
16	15	lecom 180	. . . . . . . . . . 11 r C a⊥
17	16	comcom7 460	. . . . . . . . . 10 r C a
18	17	comcom 453	. . . . . . . . 9 a C r
19	14, 18	com2or 483	. . . . . . . 8 a C (c ∪ r)
20	7, 19	fh2 470	. . . . . . 7 (b ∩ (a ∪ (c ∪ r))) = ((b ∩ a) ∪ (b ∩ (c ∪ r)))
21	5	lecon3 157	. . . . . . . . 9 b ≤ a⊥
22	21	ortha 438	. . . . . . . 8 (b ∩ a) = 0
23	22	ax-r5 38	. . . . . . 7 ((b ∩ a) ∪ (b ∩ (c ∪ r))) = (0 ∪ (b ∩ (c ∪ r)))
24	20, 23	ax-r2 36	. . . . . 6 (b ∩ (a ∪ (c ∪ r))) = (0 ∪ (b ∩ (c ∪ r)))
25		or0r 103	. . . . . 6 (0 ∪ (b ∩ (c ∪ r))) = (b ∩ (c ∪ r))
26	11, 24, 25	3tr 65	. . . . 5 (b ∩ ((a ∪ c) ∪ r)) = (b ∩ (c ∪ r))
27	9, 26	2or 72	. . . 4 ((a ∩ ((a ∪ c) ∪ r)) ∪ (b ∩ ((a ∪ c) ∪ r))) = (a ∪ (b ∩ (c ∪ r)))
28	8, 27	ax-r2 36	. . 3 ((a ∪ b) ∩ ((a ∪ c) ∪ r)) = (a ∪ (b ∩ (c ∪ r)))
29		leor 159	. . . . . . 7 c ≤ (a ∪ c)
30	29	ler 149	. . . . . 6 c ≤ ((a ∪ c) ∪ r)
31	30	lecom 180	. . . . 5 c C ((a ∪ c) ∪ r)
32		e2ast.2	. . . . . . 7 c ≤ d⊥
33	32	lecom 180	. . . . . 6 c C d⊥
34	33	comcom7 460	. . . . 5 c C d
35	31, 34	fh2r 474	. . . 4 ((c ∪ d) ∩ ((a ∪ c) ∪ r)) = ((c ∩ ((a ∪ c) ∪ r)) ∪ (d ∩ ((a ∪ c) ∪ r)))
36	30	df2le2 136	. . . . 5 (c ∩ ((a ∪ c) ∪ r)) = c
37		or32 82	. . . . . . 7 ((a ∪ c) ∪ r) = ((a ∪ r) ∪ c)
38	37	lan 77	. . . . . 6 (d ∩ ((a ∪ c) ∪ r)) = (d ∩ ((a ∪ r) ∪ c))
39	14	comcom 453	. . . . . . . 8 c C a
40		e2ast.5	. . . . . . . . . 10 c ≤ r⊥
41	40	lecom 180	. . . . . . . . 9 c C r⊥
42	41	comcom7 460	. . . . . . . 8 c C r
43	39, 42	com2or 483	. . . . . . 7 c C (a ∪ r)
44	34, 43	fh2c 477	. . . . . 6 (d ∩ ((a ∪ r) ∪ c)) = ((d ∩ (a ∪ r)) ∪ (d ∩ c))
45	32	lecon3 157	. . . . . . . . 9 d ≤ c⊥
46	45	ortha 438	. . . . . . . 8 (d ∩ c) = 0
47	46	lor 70	. . . . . . 7 ((d ∩ (a ∪ r)) ∪ (d ∩ c)) = ((d ∩ (a ∪ r)) ∪ 0)
48		or0 102	. . . . . . 7 ((d ∩ (a ∪ r)) ∪ 0) = (d ∩ (a ∪ r))
49	47, 48	ax-r2 36	. . . . . 6 ((d ∩ (a ∪ r)) ∪ (d ∩ c)) = (d ∩ (a ∪ r))
50	38, 44, 49	3tr 65	. . . . 5 (d ∩ ((a ∪ c) ∪ r)) = (d ∩ (a ∪ r))
51	36, 50	2or 72	. . . 4 ((c ∩ ((a ∪ c) ∪ r)) ∪ (d ∩ ((a ∪ c) ∪ r))) = (c ∪ (d ∩ (a ∪ r)))
52	35, 51	ax-r2 36	. . 3 ((c ∪ d) ∩ ((a ∪ c) ∪ r)) = (c ∪ (d ∩ (a ∪ r)))
53	28, 52	2an 79	. 2 (((a ∪ b) ∩ ((a ∪ c) ∪ r)) ∩ ((c ∪ d) ∩ ((a ∪ c) ∪ r))) = ((a ∪ (b ∩ (c ∪ r))) ∩ (c ∪ (d ∩ (a ∪ r))))
54	1, 53	ax-r2 36	1 (((a ∪ b) ∩ (c ∪ d)) ∩ ((a ∪ c) ∪ r)) = ((a ∪ (b ∩ (c ∪ r))) ∩ (c ∪ (d ∩ (a ∪ r))))

Syntax hints:   = wb 1   ≤ wle 2  ^⊥ wn 4   ∪ wo 6   ∩ wa 7  0wf 9

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)