Theorem 4oadist 1023

Description: OA Distributive law. This is equivalent to the 6-variable OA law, as shown by theorem d6oa 977.

Hypotheses

Ref	Expression
4oa.1	e = (((a ^ c) v ((a ->1 d) ^ (c ->1 d))) ^ ((b ^ c) v ((b ->1 d) ^ (c ->1 d))))
4oa.2	f = (((a ^ b) v ((a ->1 d) ^ (b ->1 d))) v e)
4oadist.1	h =< (a ->1 d)
4oadist.2	j =< f
4oadist.3	k =< f
4oadist.4	(h ^ (b ->1 d)) =< k

Assertion

Ref	Expression
4oadist	(h ^ (j v k)) = ((h ^ j) v (h ^ k))

Proof of Theorem 4oadist

Step	Hyp	Ref	Expression
1		4oadist.2	. . . . . . . . . 10 j =< f
2		4oadist.3	. . . . . . . . . 10 k =< f
3	1, 2	le2or 160	. . . . . . . . 9 (j v k) =< (f v f)
4		oridm 102	. . . . . . . . 9 (f v f) = f
5	3, 4	lbtr 131	. . . . . . . 8 (j v k) =< f
6	5	lelan 159	. . . . . . 7 (h ^ (j v k)) =< (h ^ f)
7	6	df2le2 128	. . . . . 6 ((h ^ (j v k)) ^ (h ^ f)) = (h ^ (j v k))
8	7	ax-r1 34	. . . . 5 (h ^ (j v k)) = ((h ^ (j v k)) ^ (h ^ f))
9		4oa.2	. . . . . . . . 9 f = (((a ^ b) v ((a ->1 d) ^ (b ->1 d))) v e)
10		or32 75	. . . . . . . . 9 (((a ^ b) v ((a ->1 d) ^ (b ->1 d))) v e) = (((a ^ b) v e) v ((a ->1 d) ^ (b ->1 d)))
11	9, 10	ax-r2 35	. . . . . . . 8 f = (((a ^ b) v e) v ((a ->1 d) ^ (b ->1 d)))
12	11	lan 70	. . . . . . 7 (h ^ f) = (h ^ (((a ^ b) v e) v ((a ->1 d) ^ (b ->1 d))))
13		4oa.1	. . . . . . . 8 e = (((a ^ c) v ((a ->1 d) ^ (c ->1 d))) ^ ((b ^ c) v ((b ->1 d) ^ (c ->1 d))))
14		leo 150	. . . . . . . . 9 ((a ^ b) v e) =< (((a ^ b) v e) v ((a ->1 d) ^ (b ->1 d)))
15	11	ax-r1 34	. . . . . . . . 9 (((a ^ b) v e) v ((a ->1 d) ^ (b ->1 d))) = f
16	14, 15	lbtr 131	. . . . . . . 8 ((a ^ b) v e) =< f
17		4oadist.1	. . . . . . . 8 h =< (a ->1 d)
18	13, 9, 16, 17	4oagen1b 1022	. . . . . . 7 (h ^ (((a ^ b) v e) v ((a ->1 d) ^ (b ->1 d)))) = (h ^ (b ->1 d))
19	12, 18	ax-r2 35	. . . . . 6 (h ^ f) = (h ^ (b ->1 d))
20	19	lan 70	. . . . 5 ((h ^ (j v k)) ^ (h ^ f)) = ((h ^ (j v k)) ^ (h ^ (b ->1 d)))
21	8, 20	ax-r2 35	. . . 4 (h ^ (j v k)) = ((h ^ (j v k)) ^ (h ^ (b ->1 d)))
22		lear 153	. . . . 5 ((h ^ (j v k)) ^ (h ^ (b ->1 d))) =< (h ^ (b ->1 d))
23		4oadist.4	. . . . . . . . 9 (h ^ (b ->1 d)) =< k
24	23	df2le2 128	. . . . . . . 8 ((h ^ (b ->1 d)) ^ k) = (h ^ (b ->1 d))
25	24	ax-r1 34	. . . . . . 7 (h ^ (b ->1 d)) = ((h ^ (b ->1 d)) ^ k)
26		an32 76	. . . . . . 7 ((h ^ (b ->1 d)) ^ k) = ((h ^ k) ^ (b ->1 d))
27	25, 26	ax-r2 35	. . . . . 6 (h ^ (b ->1 d)) = ((h ^ k) ^ (b ->1 d))
28		lea 152	. . . . . 6 ((h ^ k) ^ (b ->1 d)) =< (h ^ k)
29	27, 28	bltr 130	. . . . 5 (h ^ (b ->1 d)) =< (h ^ k)
30	22, 29	letr 129	. . . 4 ((h ^ (j v k)) ^ (h ^ (b ->1 d))) =< (h ^ k)
31	21, 30	bltr 130	. . 3 (h ^ (j v k)) =< (h ^ k)
32		leor 151	. . 3 (h ^ k) =< ((h ^ j) v (h ^ k))
33	31, 32	letr 129	. 2 (h ^ (j v k)) =< ((h ^ j) v (h ^ k))
34		ledi 166	. 2 ((h ^ j) v (h ^ k)) =< (h ^ (j v k))
35	33, 34	lebi 137	1 (h ^ (j v k)) = ((h ^ j) v (h ^ k))

Syntax hints:   = wb 1   =< wle 2   v wo 6   ^ wa 7   ->1 wi1 13

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  ax-4oa 1012

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

metamath.org