Theorem go2n6 881

Description: 12-variable Godowski equation derived from 6-variable one. The last hypothesis is the 6-variable Godowski equation.

Hypotheses

Ref	Expression
go2n6.1	g =< h_|_
go2n6.2	h =< i_|_
go2n6.3	i =< j_|_
go2n6.4	j =< k_|_
go2n6.5	k =< m_|_
go2n6.6	m =< n_|_
go2n6.7	n =< u_|_
go2n6.8	u =< w_|_
go2n6.9	w =< x_|_
go2n6.10	x =< y_|_
go2n6.11	y =< z_|_
go2n6.12	z =< g_|_
go2n6.13	(((i ->2 g) ^ (g ->2 y)) ^ (((y ->2 w) ^ (w ->2 n)) ^ ((n ->2 k) ^ (k ->2 i)))) =< (g ->2 i)

Assertion

Ref	Expression
go2n6	(((g v h) ^ (i v j)) ^ (((k v m) ^ (n v u)) ^ ((w v x) ^ (y v z)))) =< (h v i)

Proof of Theorem go2n6

Step	Hyp	Ref	Expression
1		anass 69	. . . . . . . . . 10 (((w v x) ^ (n v u)) ^ ((k v m) ^ (i v j))) = ((w v x) ^ ((n v u) ^ ((k v m) ^ (i v j))))
2		ancom 68	. . . . . . . . . . . . 13 ((k v m) ^ (i v j)) = ((i v j) ^ (k v m))
3	2	lan 70	. . . . . . . . . . . 12 ((n v u) ^ ((k v m) ^ (i v j))) = ((n v u) ^ ((i v j) ^ (k v m)))
4		ancom 68	. . . . . . . . . . . 12 ((n v u) ^ ((i v j) ^ (k v m))) = (((i v j) ^ (k v m)) ^ (n v u))
5		anass 69	. . . . . . . . . . . 12 (((i v j) ^ (k v m)) ^ (n v u)) = ((i v j) ^ ((k v m) ^ (n v u)))
6	3, 4, 5	3tr 62	. . . . . . . . . . 11 ((n v u) ^ ((k v m) ^ (i v j))) = ((i v j) ^ ((k v m) ^ (n v u)))
7	6	lan 70	. . . . . . . . . 10 ((w v x) ^ ((n v u) ^ ((k v m) ^ (i v j)))) = ((w v x) ^ ((i v j) ^ ((k v m) ^ (n v u))))
8		ancom 68	. . . . . . . . . 10 ((w v x) ^ ((i v j) ^ ((k v m) ^ (n v u)))) = (((i v j) ^ ((k v m) ^ (n v u))) ^ (w v x))
9	1, 7, 8	3tr 62	. . . . . . . . 9 (((w v x) ^ (n v u)) ^ ((k v m) ^ (i v j))) = (((i v j) ^ ((k v m) ^ (n v u))) ^ (w v x))
10	9	ran 71	. . . . . . . 8 ((((w v x) ^ (n v u)) ^ ((k v m) ^ (i v j))) ^ (y v z)) = ((((i v j) ^ ((k v m) ^ (n v u))) ^ (w v x)) ^ (y v z))
11		anass 69	. . . . . . . 8 ((((i v j) ^ ((k v m) ^ (n v u))) ^ (w v x)) ^ (y v z)) = (((i v j) ^ ((k v m) ^ (n v u))) ^ ((w v x) ^ (y v z)))
12	10, 11	ax-r2 35	. . . . . . 7 ((((w v x) ^ (n v u)) ^ ((k v m) ^ (i v j))) ^ (y v z)) = (((i v j) ^ ((k v m) ^ (n v u))) ^ ((w v x) ^ (y v z)))
13	12	ax-r1 34	. . . . . 6 (((i v j) ^ ((k v m) ^ (n v u))) ^ ((w v x) ^ (y v z))) = ((((w v x) ^ (n v u)) ^ ((k v m) ^ (i v j))) ^ (y v z))
14		anass 69	. . . . . 6 (((i v j) ^ ((k v m) ^ (n v u))) ^ ((w v x) ^ (y v z))) = ((i v j) ^ (((k v m) ^ (n v u)) ^ ((w v x) ^ (y v z))))
15		ancom 68	. . . . . 6 ((((w v x) ^ (n v u)) ^ ((k v m) ^ (i v j))) ^ (y v z)) = ((y v z) ^ (((w v x) ^ (n v u)) ^ ((k v m) ^ (i v j))))
16	13, 14, 15	3tr2 61	. . . . 5 ((i v j) ^ (((k v m) ^ (n v u)) ^ ((w v x) ^ (y v z)))) = ((y v z) ^ (((w v x) ^ (n v u)) ^ ((k v m) ^ (i v j))))
17	16	lan 70	. . . 4 ((g v h) ^ ((i v j) ^ (((k v m) ^ (n v u)) ^ ((w v x) ^ (y v z))))) = ((g v h) ^ ((y v z) ^ (((w v x) ^ (n v u)) ^ ((k v m) ^ (i v j)))))
18		anass 69	. . . 4 (((g v h) ^ (i v j)) ^ (((k v m) ^ (n v u)) ^ ((w v x) ^ (y v z)))) = ((g v h) ^ ((i v j) ^ (((k v m) ^ (n v u)) ^ ((w v x) ^ (y v z)))))
19		anass 69	. . . 4 (((g v h) ^ (y v z)) ^ (((w v x) ^ (n v u)) ^ ((k v m) ^ (i v j)))) = ((g v h) ^ ((y v z) ^ (((w v x) ^ (n v u)) ^ ((k v m) ^ (i v j)))))
20	17, 18, 19	3tr1 60	. . 3 (((g v h) ^ (i v j)) ^ (((k v m) ^ (n v u)) ^ ((w v x) ^ (y v z)))) = (((g v h) ^ (y v z)) ^ (((w v x) ^ (n v u)) ^ ((k v m) ^ (i v j))))
21	20, 19	ax-r2 35	. 2 (((g v h) ^ (i v j)) ^ (((k v m) ^ (n v u)) ^ ((w v x) ^ (y v z)))) = ((g v h) ^ ((y v z) ^ (((w v x) ^ (n v u)) ^ ((k v m) ^ (i v j)))))
22		go2n6.1	. . 3 g =< h_|_
23		go2n6.2	. . 3 h =< i_|_
24		anass 69	. . . . 5 (((i ->2 g) ^ (g ->2 y)) ^ (((y ->2 w) ^ (w ->2 n)) ^ ((n ->2 k) ^ (k ->2 i)))) = ((i ->2 g) ^ ((g ->2 y) ^ (((y ->2 w) ^ (w ->2 n)) ^ ((n ->2 k) ^ (k ->2 i)))))
25	24	ax-r1 34	. . . 4 ((i ->2 g) ^ ((g ->2 y) ^ (((y ->2 w) ^ (w ->2 n)) ^ ((n ->2 k) ^ (k ->2 i))))) = (((i ->2 g) ^ (g ->2 y)) ^ (((y ->2 w) ^ (w ->2 n)) ^ ((n ->2 k) ^ (k ->2 i))))
26		go2n6.13	. . . 4 (((i ->2 g) ^ (g ->2 y)) ^ (((y ->2 w) ^ (w ->2 n)) ^ ((n ->2 k) ^ (k ->2 i)))) =< (g ->2 i)
27	25, 26	bltr 130	. . 3 ((i ->2 g) ^ ((g ->2 y) ^ (((y ->2 w) ^ (w ->2 n)) ^ ((n ->2 k) ^ (k ->2 i))))) =< (g ->2 i)
28		go2n6.11	. . . . 5 y =< z_|_
29		go2n6.12	. . . . 5 z =< g_|_
30	28, 29	govar2 877	. . . 4 (y v z) =< (g ->2 y)
31		go2n6.9	. . . . . . 7 w =< x_|_
32		go2n6.10	. . . . . . 7 x =< y_|_
33	31, 32	govar2 877	. . . . . 6 (w v x) =< (y ->2 w)
34		go2n6.7	. . . . . . 7 n =< u_|_
35		go2n6.8	. . . . . . 7 u =< w_|_
36	34, 35	govar2 877	. . . . . 6 (n v u) =< (w ->2 n)
37	33, 36	le2an 161	. . . . 5 ((w v x) ^ (n v u)) =< ((y ->2 w) ^ (w ->2 n))
38		go2n6.5	. . . . . . 7 k =< m_|_
39		go2n6.6	. . . . . . 7 m =< n_|_
40	38, 39	govar2 877	. . . . . 6 (k v m) =< (n ->2 k)
41		go2n6.3	. . . . . . 7 i =< j_|_
42		go2n6.4	. . . . . . 7 j =< k_|_
43	41, 42	govar2 877	. . . . . 6 (i v j) =< (k ->2 i)
44	40, 43	le2an 161	. . . . 5 ((k v m) ^ (i v j)) =< ((n ->2 k) ^ (k ->2 i))
45	37, 44	le2an 161	. . . 4 (((w v x) ^ (n v u)) ^ ((k v m) ^ (i v j))) =< (((y ->2 w) ^ (w ->2 n)) ^ ((n ->2 k) ^ (k ->2 i)))
46	30, 45	le2an 161	. . 3 ((y v z) ^ (((w v x) ^ (n v u)) ^ ((k v m) ^ (i v j)))) =< ((g ->2 y) ^ (((y ->2 w) ^ (w ->2 n)) ^ ((n ->2 k) ^ (k ->2 i))))
47	22, 23, 27, 46	gon2n 878	. 2 ((g v h) ^ ((y v z) ^ (((w v