Theorem oago3.21x 872

Description: 4-variable extension of Equation (3.21) of "Equations, states, and lattices..." paper. This shows that it holds in all OMLs, not just 4GO.

Assertion

Ref	Expression
oago3.21x	((((a ->5 b) ^ (b ->5 c)) ^ (c ->5 d)) ^ (d ->5 a)) = (((a == b) ^ (b == c)) ^ (c == d))

Proof of Theorem oago3.21x

Step	Hyp	Ref	Expression
1		i5lei1 339	. . . . . 6 (a ->5 b) =< (a ->1 b)
2		i5lei2 340	. . . . . 6 (b ->5 c) =< (b ->2 c)
3	1, 2	le2an 161	. . . . 5 ((a ->5 b) ^ (b ->5 c)) =< ((a ->1 b) ^ (b ->2 c))
4		i5lei1 339	. . . . 5 (c ->5 d) =< (c ->1 d)
5	3, 4	le2an 161	. . . 4 (((a ->5 b) ^ (b ->5 c)) ^ (c ->5 d)) =< (((a ->1 b) ^ (b ->2 c)) ^ (c ->1 d))
6		i5lei2 340	. . . 4 (d ->5 a) =< (d ->2 a)
7	5, 6	le2an 161	. . 3 ((((a ->5 b) ^ (b ->5 c)) ^ (c ->5 d)) ^ (d ->5 a)) =< ((((a ->1 b) ^ (b ->2 c)) ^ (c ->1 d)) ^ (d ->2 a))
8		mhcor1 870	. . 3 ((((a ->1 b) ^ (b ->2 c)) ^ (c ->1 d)) ^ (d ->2 a)) = (((a == b) ^ (b == c)) ^ (c == d))
9	7, 8	lbtr 131	. 2 ((((a ->5 b) ^ (b ->5 c)) ^ (c ->5 d)) ^ (d ->5 a)) =< (((a == b) ^ (b == c)) ^ (c == d))
10		leid 140	. . . 4 (((a == b) ^ (b == c)) ^ (c == d)) =< (((a == b) ^ (b == c)) ^ (c == d))
11		eqtr4 816	. . . . 5 (((a == b) ^ (b == c)) ^ (c == d)) =< (a == d)
12		bicom 88	. . . . 5 (a == d) = (d == a)
13	11, 12	lbtr 131	. . . 4 (((a == b) ^ (b == c)) ^ (c == d)) =< (d == a)
14	10, 13	ler2an 165	. . 3 (((a == b) ^ (b == c)) ^ (c == d)) =< ((((a == b) ^ (b == c)) ^ (c == d)) ^ (d == a))
15		u5lembi 707	. . . . . . . 8 ((a ->5 b) ^ (b ->5 a)) = (a == b)
16	15	ax-r1 34	. . . . . . 7 (a == b) = ((a ->5 b) ^ (b ->5 a))
17		lea 152	. . . . . . 7 ((a ->5 b) ^ (b ->5 a)) =< (a ->5 b)
18	16, 17	bltr 130	. . . . . 6 (a == b) =< (a ->5 b)
19		u5lembi 707	. . . . . . . 8 ((b ->5 c) ^ (c ->5 b)) = (b == c)
20	19	ax-r1 34	. . . . . . 7 (b == c) = ((b ->5 c) ^ (c ->5 b))
21		lea 152	. . . . . . 7 ((b ->5 c) ^ (c ->5 b)) =< (b ->5 c)
22	20, 21	bltr 130	. . . . . 6 (b == c) =< (b ->5 c)
23	18, 22	le2an 161	. . . . 5 ((a == b) ^ (b == c)) =< ((a ->5 b) ^ (b ->5 c))
24		u5lembi 707	. . . . . . 7 ((c ->5 d) ^ (d ->5 c)) = (c == d)
25	24	ax-r1 34	. . . . . 6 (c == d) = ((c ->5 d) ^ (d ->5 c))
26		lea 152	. . . . . 6 ((c ->5 d) ^ (d ->5 c)) =< (c ->5 d)
27	25, 26	bltr 130	. . . . 5 (c == d) =< (c ->5 d)
28	23, 27	le2an 161	. . . 4 (((a == b) ^ (b == c)) ^ (c == d)) =< (((a ->5 b) ^ (b ->5 c)) ^ (c ->5 d))
29		u5lembi 707	. . . . . 6 ((d ->5 a) ^ (a ->5 d)) = (d == a)
30	29	ax-r1 34	. . . . 5 (d == a) = ((d ->5 a) ^ (a ->5 d))
31		lea 152	. . . . 5 ((d ->5 a) ^ (a ->5 d)) =< (d ->5 a)
32	30, 31	bltr 130	. . . 4 (d == a) =< (d ->5 a)
33	28, 32	le2an 161	. . 3 ((((a == b) ^ (b == c)) ^ (c == d)) ^ (d == a)) =< ((((a ->5 b) ^ (b ->5 c)) ^ (c ->5 d)) ^ (d ->5 a))
34	14, 33	letr 129	. 2 (((a == b) ^ (b == c)) ^ (c == d)) =< ((((a ->5 b) ^ (b ->5 c)) ^ (c ->5 d)) ^ (d ->5 a))
35	9, 34	lebi 137	1 ((((a ->5 b) ^ (b ->5 c)) ^ (c ->5 d)) ^ (d ->5 a)) = (((a == b) ^ (b == c)) ^ (c == d))

Syntax hints:   = wb 1   == tb 5   ^ wa 7   ->1 wi1 13   ->2 wi2 14   ->5 wi5 17

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-i5 47  df-le1 122  df-le2 123  df-c1 124  df-c2 125

metamath.org