Theorem 4oadist 1044

Description: OA Distributive law. This is equivalent to the 6-variable OA law, as shown by Theorem d6oa 997. (Contributed by NM, 29-Dec-1998.)

Hypotheses

Ref	Expression
4oa.1	e = (((a ∩ c) ∪ ((a →1 d) ∩ (c →1 d))) ∩ ((b ∩ c) ∪ ((b →1 d) ∩ (c →1 d))))
4oa.2	f = (((a ∩ b) ∪ ((a →1 d) ∩ (b →1 d))) ∪ 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 ∪ k)) = ((h ∩ j) ∪ (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 168	. . . . . . . . 9 (j ∪ k) ≤ (f ∪ f)
4		oridm 110	. . . . . . . . 9 (f ∪ f) = f
5	3, 4	lbtr 139	. . . . . . . 8 (j ∪ k) ≤ f
6	5	lelan 167	. . . . . . 7 (h ∩ (j ∪ k)) ≤ (h ∩ f)
7	6	df2le2 136	. . . . . 6 ((h ∩ (j ∪ k)) ∩ (h ∩ f)) = (h ∩ (j ∪ k))
8	7	ax-r1 35	. . . . 5 (h ∩ (j ∪ k)) = ((h ∩ (j ∪ k)) ∩ (h ∩ f))
9		4oa.2	. . . . . . . . 9 f = (((a ∩ b) ∪ ((a →1 d) ∩ (b →1 d))) ∪ e)
10		or32 82	. . . . . . . . 9 (((a ∩ b) ∪ ((a →1 d) ∩ (b →1 d))) ∪ e) = (((a ∩ b) ∪ e) ∪ ((a →1 d) ∩ (b →1 d)))
11	9, 10	ax-r2 36	. . . . . . . 8 f = (((a ∩ b) ∪ e) ∪ ((a →1 d) ∩ (b →1 d)))
12	11	lan 77	. . . . . . 7 (h ∩ f) = (h ∩ (((a ∩ b) ∪ e) ∪ ((a →1 d) ∩ (b →1 d))))
13		4oa.1	. . . . . . . 8 e = (((a ∩ c) ∪ ((a →1 d) ∩ (c →1 d))) ∩ ((b ∩ c) ∪ ((b →1 d) ∩ (c →1 d))))
14		leo 158	. . . . . . . . 9 ((a ∩ b) ∪ e) ≤ (((a ∩ b) ∪ e) ∪ ((a →1 d) ∩ (b →1 d)))
15	11	ax-r1 35	. . . . . . . . 9 (((a ∩ b) ∪ e) ∪ ((a →1 d) ∩ (b →1 d))) = f
16	14, 15	lbtr 139	. . . . . . . 8 ((a ∩ b) ∪ e) ≤ f
17		4oadist.1	. . . . . . . 8 h ≤ (a →1 d)
18	13, 9, 16, 17	4oagen1b 1043	. . . . . . 7 (h ∩ (((a ∩ b) ∪ e) ∪ ((a →1 d) ∩ (b →1 d)))) = (h ∩ (b →1 d))
19	12, 18	ax-r2 36	. . . . . 6 (h ∩ f) = (h ∩ (b →1 d))
20	19	lan 77	. . . . 5 ((h ∩ (j ∪ k)) ∩ (h ∩ f)) = ((h ∩ (j ∪ k)) ∩ (h ∩ (b →1 d)))
21	8, 20	ax-r2 36	. . . 4 (h ∩ (j ∪ k)) = ((h ∩ (j ∪ k)) ∩ (h ∩ (b →1 d)))
22		lear 161	. . . . 5 ((h ∩ (j ∪ k)) ∩ (h ∩ (b →1 d))) ≤ (h ∩ (b →1 d))
23		4oadist.4	. . . . . . . . 9 (h ∩ (b →1 d)) ≤ k
24	23	df2le2 136	. . . . . . . 8 ((h ∩ (b →1 d)) ∩ k) = (h ∩ (b →1 d))
25	24	ax-r1 35	. . . . . . 7 (h ∩ (b →1 d)) = ((h ∩ (b →1 d)) ∩ k)
26		an32 83	. . . . . . 7 ((h ∩ (b →1 d)) ∩ k) = ((h ∩ k) ∩ (b →1 d))
27	25, 26	ax-r2 36	. . . . . 6 (h ∩ (b →1 d)) = ((h ∩ k) ∩ (b →1 d))
28		lea 160	. . . . . 6 ((h ∩ k) ∩ (b →1 d)) ≤ (h ∩ k)
29	27, 28	bltr 138	. . . . 5 (h ∩ (b →1 d)) ≤ (h ∩ k)
30	22, 29	letr 137	. . . 4 ((h ∩ (j ∪ k)) ∩ (h ∩ (b →1 d))) ≤ (h ∩ k)
31	21, 30	bltr 138	. . 3 (h ∩ (j ∪ k)) ≤ (h ∩ k)
32		leor 159	. . 3 (h ∩ k) ≤ ((h ∩ j) ∪ (h ∩ k))
33	31, 32	letr 137	. 2 (h ∩ (j ∪ k)) ≤ ((h ∩ j) ∪ (h ∩ k))
34		ledi 174	. 2 ((h ∩ j) ∪ (h ∩ k)) ≤ (h ∩ (j ∪ k))
35	33, 34	lebi 145	1 (h ∩ (j ∪ k)) = ((h ∩ j) ∪ (h ∩ k))

This proof depends on syntax axioms:   = wb 1   ≤ wle 2   ∪ wo 6   ∩ wa 7   →₁ wi1 12

This proof depends on axioms:  ax-a1 30  ax-a2 31  ax-a3 32  ax-a4 33  ax-a5 34  ax-r1 35  ax-r2 36  ax-r4 37  ax-r5 38  ax-r3 439  ax-4oa 1033

This proof depends on definitions:  df-b 39  df-a 40  df-t 41  df-f 42  df-i1 44  df-le1 130  df-le2 131  df-c1 132  df-c2 133

This theorem is used by: (None)