Theorem oa8todual 951

Description: Conventional to dual 8-variable OA law.

Hypothesis

Ref

Expression

oa8to5.1

(((a_|_ v b_|_) ^ (c_|_ v d_|_)) ^ ((e_|_ v f_|_) ^ (g_|_ v h_|_))) =< (b_|_ v (a_|_ ^ (c_|_ v ((((a_|_ v c_|_) ^ (b_|_ v d_|_)) ^ (((a_|_ v g_|_) ^ (b_|_ v h_|_)) v ((c_|_ v g_|_) ^ (d_|_ v h_|_)))) ^ ((((a_|_ v e_|_) ^ (b_|_ v f_|_)) ^ (((a_|_ v g_|_) ^ (b_|_ v h_|_)) v ((e_|_ v g_|_) ^ (f_|_ v h_|_)))) v (((c_|_ v e_|_) ^ (d_|_ v f_|_)) ^ (((c_|_ v g_|_) ^ (d_|_ v h_|_)) v ((e_|_ v g_|_) ^ (f_|_ v h_|_)))))))))

Assertion

Ref	Expression
oa8todual	(b ^ (a v (c ^ ((((a ^ c) v (b ^ d)) v (((a ^ g) v (b ^ h)) ^ ((c ^ g) v (d ^ h)))) v ((((a ^ e) v (b ^ f)) v (((a ^ g) v (b ^ h)) ^ ((e ^ g) v (f ^ h)))) ^ (((c ^ e) v (d ^ f)) v (((c ^ g) v (d ^ h)) ^ ((e ^ g) v (f ^ h))))))))) =< (((a ^ b) v (c ^ d)) v ((e ^ f) v (g ^ h)))

Proof of Theorem oa8todual

Step	Hyp	Ref	Expression
1		oa8to5.1	. . 3 (((a_|_ v b_|_) ^ (c_|_ v d_|_)) ^ ((e_|_ v f_|_) ^ (g_|_ v h_|_))) =< (b_|_ v (a_|_ ^ (c_|_ v ((((a_|_ v c_|_) ^ (b_|_ v d_|_)) ^ (((a_|_ v g_|_) ^ (b_|_ v h_|_)) v ((c_|_ v g_|_) ^ (d_|_ v h_|_)))) ^ ((((a_|_ v e_|_) ^ (b_|_ v f_|_)) ^ (((a_|_ v g_|_) ^ (b_|_ v h_|_)) v ((e_|_ v g_|_) ^ (f_|_ v h_|_)))) v (((c_|_ v e_|_) ^ (d_|_ v f_|_)) ^ (((c_|_ v g_|_) ^ (d_|_ v h_|_)) v ((e_|_ v g_|_) ^ (f_|_ v h_|_)))))))))
2	1	lecon 146	. 2 (b_|_ v (a_|_ ^ (c_|_ v ((((a_|_ v c_|_) ^ (b_|_ v d_|_)) ^ (((a_|_ v g_|_) ^ (b_|_ v h_|_)) v ((c_|_ v g_|_) ^ (d_|_ v h_|_)))) ^ ((((a_|_ v e_|_) ^ (b_|_ v f_|_)) ^ (((a_|_ v g_|_) ^ (b_|_ v h_|_)) v ((e_|_ v g_|_) ^ (f_|_ v h_|_)))) v (((c_|_ v e_|_) ^ (d_|_ v f_|_)) ^ (((c_|_ v g_|_) ^ (d_|_ v h_|_)) v ((e_|_ v g_|_) ^ (f_|_ v h_|_)))))))))_|_ =< (((a_|_ v b_|_) ^ (c_|_ v d_|_)) ^ ((e_|_ v f_|_) ^ (g_|_ v h_|_)))_|_
3		ax-a1 29	. . . 4 b = b_|__|_
4		ax-a1 29	. . . . . 6 a = a_|__|_
5		ax-a1 29	. . . . . . . 8 c = c_|__|_
6		df-a 39	. . . . . . . . . . . . . 14 (a ^ c) = (a_|_ v c_|_)_|_
7		df-a 39	. . . . . . . . . . . . . 14 (b ^ d) = (b_|_ v d_|_)_|_
8	6, 7	2or 67	. . . . . . . . . . . . 13 ((a ^ c) v (b ^ d)) = ((a_|_ v c_|_)_|_ v (b_|_ v d_|_)_|_)
9		oran3 85	. . . . . . . . . . . . 13 ((a_|_ v c_|_)_|_ v (b_|_ v d_|_)_|_) = ((a_|_ v c_|_) ^ (b_|_ v d_|_))_|_
10	8, 9	ax-r2 35	. . . . . . . . . . . 12 ((a ^ c) v (b ^ d)) = ((a_|_ v c_|_) ^ (b_|_ v d_|_))_|_
11		df-a 39	. . . . . . . . . . . . . . . 16 (a ^ g) = (a_|_ v g_|_)_|_
12		df-a 39	. . . . . . . . . . . . . . . 16 (b ^ h) = (b_|_ v h_|_)_|_
13	11, 12	2or 67	. . . . . . . . . . . . . . 15 ((a ^ g) v (b ^ h)) = ((a_|_ v g_|_)_|_ v (b_|_ v h_|_)_|_)
14		oran3 85	. . . . . . . . . . . . . . 15 ((a_|_ v g_|_)_|_ v (b_|_ v h_|_)_|_) = ((a_|_ v g_|_) ^ (b_|_ v h_|_))_|_
15	13, 14	ax-r2 35	. . . . . . . . . . . . . 14 ((a ^ g) v (b ^ h)) = ((a_|_ v g_|_) ^ (b_|_ v h_|_))_|_
16		df-a 39	. . . . . . . . . . . . . . . 16 (c ^ g) = (c_|_ v g_|_)_|_
17		df-a 39	. . . . . . . . . . . . . . . 16 (d ^ h) = (d_|_ v h_|_)_|_
18	16, 17	2or 67	. . . . . . . . . . . . . . 15 ((c ^ g) v (d ^ h)) = ((c_|_ v g_|_)_|_ v (d_|_ v h_|_)_|_)
19		oran3 85	. . . . . . . . . . . . . . 15 ((c_|_ v g_|_)_|_ v (d_|_ v h_|_)_|_) = ((c_|_ v g_|_) ^ (d_|_ v h_|_))_|_
20	18, 19	ax-r2 35	. . . . . . . . . . . . . 14 ((c ^ g) v (d ^ h)) = ((c_|_ v g_|_) ^ (d_|_ v h_|_))_|_
21	15, 20	2an 72	. . . . . . . . . . . . 13 (((a ^ g) v (b ^ h)) ^ ((c ^ g) v (d ^ h))) = (((a_|_ v g_|_) ^ (b_|_ v h_|_))_|_ ^ ((c_|_ v g_|_) ^ (d_|_ v h_|_))_|_)
22		anor3 82	. . . . . . . . . . . . 13 (((a_|_ v g_|_) ^ (b_|_ v h_|_))_|_ ^ ((c_|_ v g_|_) ^ (d_|_ v h_|_))_|_) = (((a_|_ v g_|_) ^ (b_|_ v h_|_)) v ((c_|_ v g_|_) ^ (d_|_ v h_|_)))_|_
23	21, 22	ax-r2 35	. . . . . . . . . . . 12 (((a ^ g) v (b ^ h)) ^ ((c ^ g) v (d ^ h))) = (((a_|_ v g_|_) ^ (b_|_ v h_|_)) v ((c_|_ v g_|_) ^ (d_|_ v h_|_)))_|_
24	10, 23	2or 67	. . . . . . . . . . 11 (((a ^ c) v (b ^ d)) v (((a ^ g) v (b ^ h)) ^ ((c ^ g) v (d ^ h)))) = (((a_|_ v c_|_) ^ (b_|_ v d_|_))_|_ v (((a_|_ v g_|_) ^ (b_|_ v h_|_)) v ((c_|_ v g_|_) ^ (d_|_ v h_|_)))_|_)
25		oran3 85	. . . . . . . . . . 11 (((a_|_ v c_|_) ^ (b_|_ v d_|_))_|_ v (((a_|_ v g_|_) ^ (b_|_ v h_|_)) v ((c_|_ v g_|_) ^ (d_|_ v h_|_)))_|_) = (((a_|_ v c_|_) ^ (b_|_ v d_|_)) ^ (((a_|_ v g_|_) ^ (b_|_ v h_|_)) v ((c_|_ v g_|_) ^ (d_|_ v h_|_))))_|_
26	24, 25	ax-r2 35	. . . . . . . . . 10 (((a ^ c) v (b ^ d)) v (((a ^ g) v (b ^ h)) ^ ((c ^ g) v (d ^ h)))) = (((a_|_ v c_|_) ^ (b_|_ v d_|_)) ^ (((a_|_ v g_|_) ^ (b_|_ v h_|_)) v ((c_|_ v g_|_) ^ (d_|_ v h_|_))))_|_
27		df-a 39	. . . . . . . . . . . . . . . 16 (a ^ e) = (a_|_ v e_|_)_|_
28		df-a 39	. . . . . . . . . . . . . . . 16 (b ^ f) = (b_|_ v f_|_)_|_
29	27, 28	2or 67	. . . . . . . . . . . . . . 15 ((a ^ e) v (b ^ f)) = ((a_|_ v e_|_)_|_ v (b_|_ v f_|_)_|_)
30		oran3 85	. . . . . . . . . . . . . . 15 ((a_|_ v e_|_)_|_ v (b_|_ v f_|_)_|_) = ((a_|_ v e_|_) ^ (b_|_ v f_|_))_|_
31	29, 30	ax-r2 35	. . . . . . . . . . . . . 14 ((a ^ e) v (b ^ f)) = ((a_|_ v e_|_) ^ (b_|_ v f_|_))_|_
32		df-a 39	. . . . . . . . . . . . . . . . . 18 (e ^ g) = (e_|_ v g_|_)_|_
33		df-a 39	. . . . . . . . . . . . . . . . . 18 (f ^ h) = (f_|_ v h_|_)_|_
34	32, 33	2or 67	. . . . . . . . . . . . . . . . 17 ((e ^ g) v (f ^ h)) = ((e_|_ v g_|_)_|_ v (f_|_ v h_|_)_|_)
35		oran3 85	. . . . . . . . . . . . . . . . 17 ((e_|_ v g_|_)_|_ v (f_|_ v h_|_)_|_) = ((e_|_ v g_|_) ^ (f_|_ v h_|_))_|_
36	34, 35	ax-r2 35	. . . . . . . . . . . . . . . 16 ((e ^ g) v (f ^ h)) = ((e_|_ v g_|_) ^ (f_|_ v h_|_))_|_
37	15, 36	2an 72	. . . . . . . . . . . . . . 15 (((a ^ g) v (b ^ h)) ^ ((e ^ g) v (f ^ h))) = (((a_|_ v g_|_) ^ (b_|_ v h_|_))_|_ ^ ((e_|_ v g_|_) ^ (f_|_ v h_|_))