Theorem gomaex3 904

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.

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 v b) ->1 (d v e)_|_)_|_
gomaex3.10	q = ((e v f) ->1 (b v c)_|_)_|_
gomaex3.11	r = ((p_|_ ->1 q)_|_ ^ (c v 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 v f)_|_

Assertion

Ref	Expression
gomaex3	(((a v b) ^ (d v e)_|_) ^ ((((a v b) ->1 (d v e)_|_) ->1 ((e v f) ->1 (b v c)_|_)_|_)_|_ ->1 (c v d))) =< ((b v c) v (e v f)_|_)

Proof of Theorem gomaex3

Step	Hyp	Ref	Expression
1		df-i1 43	. . . 4 ((((a v b) ->1 (d v e)_|_) ->1 ((e v f) ->1 (b v c)_|_)_|_)_|_ ->1 (c v d)) = ((((a v b) ->1 (d v e)_|_) ->1 ((e v f) ->1 (b v c)_|_)_|_)_|__|_ v ((((a v b) ->1 (d v e)_|_) ->1 ((e v f) ->1 (b v c)_|_)_|_)_|_ ^ (c v d)))
2		ax-a2 30	. . . . . 6 (r v (p_|_ ->1 q)) = ((p_|_ ->1 q) v r)
3		gomaex3.9	. . . . . . . . . 10 p = ((a v b) ->1 (d v e)_|_)_|_
4	3	con2 64	. . . . . . . . 9 p_|_ = ((a v b) ->1 (d v e)_|_)
5		gomaex3.10	. . . . . . . . 9 q = ((e v f) ->1 (b v c)_|_)_|_
6	4, 5	ud1lem0ab 249	. . . . . . . 8 (p_|_ ->1 q) = (((a v b) ->1 (d v e)_|_) ->1 ((e v f) ->1 (b v c)_|_)_|_)
7		ax-a1 29	. . . . . . . 8 (((a v b) ->1 (d v e)_|_) ->1 ((e v f) ->1 (b v c)_|_)_|_) = (((a v b) ->1 (d v e)_|_) ->1 ((e v f) ->1 (b v c)_|_)_|_)_|__|_
8	6, 7	ax-r2 35	. . . . . . 7 (p_|_ ->1 q) = (((a v b) ->1 (d v e)_|_) ->1 ((e v f) ->1 (b v c)_|_)_|_)_|__|_
9		gomaex3.11	. . . . . . . 8 r = ((p_|_ ->1 q)_|_ ^ (c v d))
10	6	ax-r4 36	. . . . . . . . 9 (p_|_ ->1 q)_|_ = (((a v b) ->1 (d v e)_|_) ->1 ((e v f) ->1 (b v c)_|_)_|_)_|_
11	10	ran 71	. . . . . . . 8 ((p_|_ ->1 q)_|_ ^ (c v d)) = ((((a v b) ->1 (d v e)_|_) ->1 ((e v f) ->1 (b v c)_|_)_|_)_|_ ^ (c v d))
12	9, 11	ax-r2 35	. . . . . . 7 r = ((((a v b) ->1 (d v e)_|_) ->1 ((e v f) ->1 (b v c)_|_)_|_)_|_ ^ (c v d))
13	8, 12	2or 67	. . . . . 6 ((p_|_ ->1 q) v r) = ((((a v b) ->1 (d v e)_|_) ->1 ((e v f) ->1 (b v c)_|_)_|_)_|__|_ v ((((a v b) ->1 (d v e)_|_) ->1 ((e v f) ->1 (b v c)_|_)_|_)_|_ ^ (c v d)))
14	2, 13	ax-r2 35	. . . . 5 (r v (p_|_ ->1 q)) = ((((a v b) ->1 (d v e)_|_) ->1 ((e v f) ->1 (b v c)_|_)_|_)_|__|_ v ((((a v b) ->1 (d v e)_|_) ->1 ((e v f) ->1 (b v c)_|_)_|_)_|_ ^ (c v d)))
15	14	ax-r1 34	. . . 4 ((((a v b) ->1 (d v e)_|_) ->1 ((e v f) ->1 (b v c)_|_)_|_)_|__|_ v ((((a v b) ->1 (d v e)_|_) ->1 ((e v f) ->1 (b v c)_|_)_|_)_|_ ^ (c v d))) = (r v (p_|_ ->1 q))
16	1, 15	ax-r2 35	. . 3 ((((a v b) ->1 (d v e)_|_) ->1 ((e v f) ->1 (b v c)_|_)_|_)_|_ ->1 (c v d)) = (r v (p_|_ ->1 q))
17	16	lan 70	. 2 (((a v b) ^ (d v e)_|_) ^ ((((a v b) ->1 (d v e)_|_) ->1 ((e v f) ->1 (b v c)_|_)_|_)_|_ ->1 (c v d))) = (((a v b) ^ (d v e)_|_) ^ (r v (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 58	. . 3 b = b
26		gomaex3.14	. . 3 i = c
27		id 58	. . 3 (c v d)_|_ = (c v d)_|_
28		gomaex3.16	. . 3 k = r
29		id 58	. . 3 (p_|_ ->1 q) = (p_|_ ->1 q)
30		gomaex3.18	. . 3 n = (p_|_ ->1 q)_|_
31		id 58	. . 3 (p_|_ ^ q) = (p_|_ ^ q)
32		gomaex3.20	. . 3 w = q_|_
33		id 58	. . 3 q = q
34		gomaex3.22	. . 3 y = (e v f)_|_
35		id 58	. . 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 903	. 2 (((a v b) ^ (d v e)_|_) ^ (r v (p_|_ ->1 q))) =< ((b v c) v (e v f)_|_)
37	17, 36	bltr 130	1 (((a v b) ^ (d v e)_|_) ^ ((((a v b) ->1 (d v e)_|_) ->1 ((e v f) ->1 (b v c)_|_)_|_)_|_ ->1 (c v d))) =< ((b v c) v (e v f)_|_)

Syntax hints:   = wb 1   =< wle 2  _|_wn 4   v wo 6   ^ wa 7   ->1 wi1 13   ->2 wi2 14

This theorem was proved from axioms:  ax-a1 29  ax-a2 30  ax-a3 31  ax-a4 32  ax-a5 33  ax-r1 34  ax-r2 35  ax-r4 36  ax-r5 37  ax-r3 421

This theorem depends on definitions:  df-b 38  df-a 39  df-t 40  df-f 41  df-i1 43  df-i2 44  df-le1 122  df-le2 123  df-c1 124  df-c2 125

metamath.org