Theorem gomaex3 924

Description: Proof of Mayet Example 3 from 6-variable Godowski equation. R. Mayet, "Equational bases for some varieties of orthomodular lattices related to states", Algebra Universalis 23 (1986), 167-195. (Contributed by NM, 27-May-2000.)

Hypotheses

Ref	Expression
gomaex3.1	a ≤ b⊥
gomaex3.2	b ≤ c⊥
gomaex3.3	c ≤ d⊥
gomaex3.5	e ≤ f⊥
gomaex3.6	f ≤ a⊥
gomaex3.8	(((i →2 g) ∩ (g →2 y)) ∩ (((y →2 w) ∩ (w →2 n)) ∩ ((n →2 k) ∩ (k →2 i)))) ≤ (g →2 i)
gomaex3.9	p = ((a ∪ b) →1 (d ∪ e)⊥ )⊥
gomaex3.10	q = ((e ∪ f) →1 (b ∪ c)⊥ )⊥
gomaex3.11	r = ((p⊥ →1 q)⊥ ∩ (c ∪ d))
gomaex3.12	g = a
gomaex3.14	i = c
gomaex3.16	k = r
gomaex3.18	n = (p⊥ →1 q)⊥
gomaex3.20	w = q⊥
gomaex3.22	y = (e ∪ f)⊥

Assertion

Ref	Expression
gomaex3	(((a ∪ b) ∩ (d ∪ e)⊥ ) ∩ ((((a ∪ b) →1 (d ∪ e)⊥ ) →1 ((e ∪ f) →1 (b ∪ c)⊥ )⊥ )⊥ →1 (c ∪ d))) ≤ ((b ∪ c) ∪ (e ∪ f)⊥ )

Proof of Theorem gomaex3

Step	Hyp	Ref	Expression
1		df-i1 44	. . . 4 ((((a ∪ b) →1 (d ∪ e)⊥ ) →1 ((e ∪ f) →1 (b ∪ c)⊥ )⊥ )⊥ →1 (c ∪ d)) = ((((a ∪ b) →1 (d ∪ e)⊥ ) →1 ((e ∪ f) →1 (b ∪ c)⊥ )⊥ )⊥ ⊥ ∪ ((((a ∪ b) →1 (d ∪ e)⊥ ) →1 ((e ∪ f) →1 (b ∪ c)⊥ )⊥ )⊥ ∩ (c ∪ d)))
2		ax-a2 31	. . . . . 6 (r ∪ (p⊥ →1 q)) = ((p⊥ →1 q) ∪ r)
3		gomaex3.9	. . . . . . . . . 10 p = ((a ∪ b) →1 (d ∪ e)⊥ )⊥
4	3	con2 67	. . . . . . . . 9 p⊥ = ((a ∪ b) →1 (d ∪ e)⊥ )
5		gomaex3.10	. . . . . . . . 9 q = ((e ∪ f) →1 (b ∪ c)⊥ )⊥
6	4, 5	ud1lem0ab 257	. . . . . . . 8 (p⊥ →1 q) = (((a ∪ b) →1 (d ∪ e)⊥ ) →1 ((e ∪ f) →1 (b ∪ c)⊥ )⊥ )
7		ax-a1 30	. . . . . . . 8 (((a ∪ b) →1 (d ∪ e)⊥ ) →1 ((e ∪ f) →1 (b ∪ c)⊥ )⊥ ) = (((a ∪ b) →1 (d ∪ e)⊥ ) →1 ((e ∪ f) →1 (b ∪ c)⊥ )⊥ )⊥ ⊥
8	6, 7	ax-r2 36	. . . . . . 7 (p⊥ →1 q) = (((a ∪ b) →1 (d ∪ e)⊥ ) →1 ((e ∪ f) →1 (b ∪ c)⊥ )⊥ )⊥ ⊥
9		gomaex3.11	. . . . . . . 8 r = ((p⊥ →1 q)⊥ ∩ (c ∪ d))
10	6	ax-r4 37	. . . . . . . . 9 (p⊥ →1 q)⊥ = (((a ∪ b) →1 (d ∪ e)⊥ ) →1 ((e ∪ f) →1 (b ∪ c)⊥ )⊥ )⊥
11	10	ran 78	. . . . . . . 8 ((p⊥ →1 q)⊥ ∩ (c ∪ d)) = ((((a ∪ b) →1 (d ∪ e)⊥ ) →1 ((e ∪ f) →1 (b ∪ c)⊥ )⊥ )⊥ ∩ (c ∪ d))
12	9, 11	ax-r2 36	. . . . . . 7 r = ((((a ∪ b) →1 (d ∪ e)⊥ ) →1 ((e ∪ f) →1 (b ∪ c)⊥ )⊥ )⊥ ∩ (c ∪ d))
13	8, 12	2or 72	. . . . . 6 ((p⊥ →1 q) ∪ r) = ((((a ∪ b) →1 (d ∪ e)⊥ ) →1 ((e ∪ f) →1 (b ∪ c)⊥ )⊥ )⊥ ⊥ ∪ ((((a ∪ b) →1 (d ∪ e)⊥ ) →1 ((e ∪ f) →1 (b ∪ c)⊥ )⊥ )⊥ ∩ (c ∪ d)))
14	2, 13	ax-r2 36	. . . . 5 (r ∪ (p⊥ →1 q)) = ((((a ∪ b) →1 (d ∪ e)⊥ ) →1 ((e ∪ f) →1 (b ∪ c)⊥ )⊥ )⊥ ⊥ ∪ ((((a ∪ b) →1 (d ∪ e)⊥ ) →1 ((e ∪ f) →1 (b ∪ c)⊥ )⊥ )⊥ ∩ (c ∪ d)))
15	14	ax-r1 35	. . . 4 ((((a ∪ b) →1 (d ∪ e)⊥ ) →1 ((e ∪ f) →1 (b ∪ c)⊥ )⊥ )⊥ ⊥ ∪ ((((a ∪ b) →1 (d ∪ e)⊥ ) →1 ((e ∪ f) →1 (b ∪ c)⊥ )⊥ )⊥ ∩ (c ∪ d))) = (r ∪ (p⊥ →1 q))
16	1, 15	ax-r2 36	. . 3 ((((a ∪ b) →1 (d ∪ e)⊥ ) →1 ((e ∪ f) →1 (b ∪ c)⊥ )⊥ )⊥ →1 (c ∪ d)) = (r ∪ (p⊥ →1 q))
17	16	lan 77	. 2 (((a ∪ b) ∩ (d ∪ e)⊥ ) ∩ ((((a ∪ b) →1 (d ∪ e)⊥ ) →1 ((e ∪ f) →1 (b ∪ c)⊥ )⊥ )⊥ →1 (c ∪ d))) = (((a ∪ b) ∩ (d ∪ e)⊥ ) ∩ (r ∪ (p⊥ →1 q)))
18		gomaex3.1	. . 3 a ≤ b⊥
19		gomaex3.2	. . 3 b ≤ c⊥
20		gomaex3.3	. . 3 c ≤ d⊥
21		gomaex3.5	. . 3 e ≤ f⊥
22		gomaex3.6	. . 3 f ≤ a⊥
23		gomaex3.8	. . 3 (((i →2 g) ∩ (g →2 y)) ∩ (((y →2 w) ∩ (w →2 n)) ∩ ((n →2 k) ∩ (k →2 i)))) ≤ (g →2 i)
24		gomaex3.12	. . 3 g = a
25		id 59	. . 3 b = b
26		gomaex3.14	. . 3 i = c
27		id 59	. . 3 (c ∪ d)⊥ = (c ∪ d)⊥
28		gomaex3.16	. . 3 k = r
29		id 59	. . 3 (p⊥ →1 q) = (p⊥ →1 q)
30		gomaex3.18	. . 3 n = (p⊥ →1 q)⊥
31		id 59	. . 3 (p⊥ ∩ q) = (p⊥ ∩ q)
32		gomaex3.20	. . 3 w = q⊥
33		id 59	. . 3 q = q
34		gomaex3.22	. . 3 y = (e ∪ f)⊥
35		id 59	. . 3 f = f
36	18, 19, 20, 21, 22, 23, 3, 5, 9, 24, 25, 26, 27, 28, 29, 30, 31, 32, 33, 34, 35	gomaex3lem10 923	. 2 (((a ∪ b) ∩ (d ∪ e)⊥ ) ∩ (r ∪ (p⊥ →1 q))) ≤ ((b ∪ c) ∪ (e ∪ f)⊥ )
37	17, 36	bltr 138	1 (((a ∪ b) ∩ (d ∪ e)⊥ ) ∩ ((((a ∪ b) →1 (d ∪ e)⊥ ) →1 ((e ∪ f) →1 (b ∪ c)⊥ )⊥ )⊥ →1 (c ∪ d))) ≤ ((b ∪ c) ∪ (e ∪ f)⊥ )

Syntax hints:   = wb 1   ≤ wle 2  ^⊥ wn 4   ∪ wo 6   ∩ wa 7   →₁ wi1 12   →₂ wi2 13

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-i1 44  df-i2 45  df-le1 130  df-le2 131  df-c1 132  df-c2 133

This theorem is referenced by: (None)