Theorem testmod2 1215

Description: A modular law experiment. (Contributed by NM, 21-Apr-2012.)

Assertion

Ref	Expression
testmod2	((a ∪ b) ∩ (a ∪ (c ∪ d))) = (a ∪ (b ∩ (((a ∪ c) ∩ (b ∪ d)) ∪ (d ∩ ((a ∪ c) ∪ ((b ∪ c) ∩ (d ∪ a)))))))

Proof of Theorem testmod2

Step	Hyp	Ref	Expression
1		orass 75	. . . . 5 ((a ∪ c) ∪ d) = (a ∪ (c ∪ d))
2	1	lan 77	. . . 4 ((a ∪ b) ∩ ((a ∪ c) ∪ d)) = ((a ∪ b) ∩ (a ∪ (c ∪ d)))
3	2	cm 61	. . 3 ((a ∪ b) ∩ (a ∪ (c ∪ d))) = ((a ∪ b) ∩ ((a ∪ c) ∪ d))
4		leo 158	. . . . 5 a ≤ (a ∪ c)
5	4	ler 149	. . . 4 a ≤ ((a ∪ c) ∪ d)
6	5	mlduali 1128	. . 3 ((a ∪ b) ∩ ((a ∪ c) ∪ d)) = (a ∪ (b ∩ ((a ∪ c) ∪ d)))
7	3, 6	tr 62	. 2 ((a ∪ b) ∩ (a ∪ (c ∪ d))) = (a ∪ (b ∩ ((a ∪ c) ∪ d)))
8		leo 158	. . . . . . . . 9 b ≤ (b ∪ d)
9		leor 159	. . . . . . . . 9 b ≤ ((a ∪ c) ∪ b)
10	8, 9	ler2an 173	. . . . . . . 8 b ≤ ((b ∪ d) ∩ ((a ∪ c) ∪ b))
11	10	df2le2 136	. . . . . . 7 (b ∩ ((b ∪ d) ∩ ((a ∪ c) ∪ b))) = b
12	11	ran 78	. . . . . 6 ((b ∩ ((b ∪ d) ∩ ((a ∪ c) ∪ b))) ∩ ((a ∪ c) ∪ d)) = (b ∩ ((a ∪ c) ∪ d))
13	12	cm 61	. . . . 5 (b ∩ ((a ∪ c) ∪ d)) = ((b ∩ ((b ∪ d) ∩ ((a ∪ c) ∪ b))) ∩ ((a ∪ c) ∪ d))
14		anass 76	. . . . 5 ((b ∩ ((b ∪ d) ∩ ((a ∪ c) ∪ b))) ∩ ((a ∪ c) ∪ d)) = (b ∩ (((b ∪ d) ∩ ((a ∪ c) ∪ b)) ∩ ((a ∪ c) ∪ d)))
15	13, 14	tr 62	. . . 4 (b ∩ ((a ∪ c) ∪ d)) = (b ∩ (((b ∪ d) ∩ ((a ∪ c) ∪ b)) ∩ ((a ∪ c) ∪ d)))
16		an32 83	. . . . . . . . . 10 (((b ∪ d) ∩ ((a ∪ c) ∪ b)) ∩ ((a ∪ c) ∪ d)) = (((b ∪ d) ∩ ((a ∪ c) ∪ d)) ∩ ((a ∪ c) ∪ b))
17		leor 159	. . . . . . . . . . . . 13 d ≤ (b ∪ d)
18	17	mldual2i 1127	. . . . . . . . . . . 12 ((b ∪ d) ∩ ((a ∪ c) ∪ d)) = (((b ∪ d) ∩ (a ∪ c)) ∪ d)
19		ancom 74	. . . . . . . . . . . . 13 ((b ∪ d) ∩ (a ∪ c)) = ((a ∪ c) ∩ (b ∪ d))
20	19	ror 71	. . . . . . . . . . . 12 (((b ∪ d) ∩ (a ∪ c)) ∪ d) = (((a ∪ c) ∩ (b ∪ d)) ∪ d)
21	18, 20	tr 62	. . . . . . . . . . 11 ((b ∪ d) ∩ ((a ∪ c) ∪ d)) = (((a ∪ c) ∩ (b ∪ d)) ∪ d)
22	21	ran 78	. . . . . . . . . 10 (((b ∪ d) ∩ ((a ∪ c) ∪ d)) ∩ ((a ∪ c) ∪ b)) = ((((a ∪ c) ∩ (b ∪ d)) ∪ d) ∩ ((a ∪ c) ∪ b))
23	16, 22	tr 62	. . . . . . . . 9 (((b ∪ d) ∩ ((a ∪ c) ∪ b)) ∩ ((a ∪ c) ∪ d)) = ((((a ∪ c) ∩ (b ∪ d)) ∪ d) ∩ ((a ∪ c) ∪ b))
24		lea 160	. . . . . . . . . . . . 13 ((a ∪ c) ∩ (b ∪ d)) ≤ (a ∪ c)
25	24	leror 152	. . . . . . . . . . . 12 (((a ∪ c) ∩ (b ∪ d)) ∪ d) ≤ ((a ∪ c) ∪ d)
26	25	df2le2 136	. . . . . . . . . . 11 ((((a ∪ c) ∩ (b ∪ d)) ∪ d) ∩ ((a ∪ c) ∪ d)) = (((a ∪ c) ∩ (b ∪ d)) ∪ d)
27	26	ran 78	. . . . . . . . . 10 (((((a ∪ c) ∩ (b ∪ d)) ∪ d) ∩ ((a ∪ c) ∪ d)) ∩ ((a ∪ c) ∪ b)) = ((((a ∪ c) ∩ (b ∪ d)) ∪ d) ∩ ((a ∪ c) ∪ b))
28	27	cm 61	. . . . . . . . 9 ((((a ∪ c) ∩ (b ∪ d)) ∪ d) ∩ ((a ∪ c) ∪ b)) = (((((a ∪ c) ∩ (b ∪ d)) ∪ d) ∩ ((a ∪ c) ∪ d)) ∩ ((a ∪ c) ∪ b))
29	23, 28	tr 62	. . . . . . . 8 (((b ∪ d) ∩ ((a ∪ c) ∪ b)) ∩ ((a ∪ c) ∪ d)) = (((((a ∪ c) ∩ (b ∪ d)) ∪ d) ∩ ((a ∪ c) ∪ d)) ∩ ((a ∪ c) ∪ b))
30		anass 76	. . . . . . . 8 (((((a ∪ c) ∩ (b ∪ d)) ∪ d) ∩ ((a ∪ c) ∪ d)) ∩ ((a ∪ c) ∪ b)) = ((((a ∪ c) ∩ (b ∪ d)) ∪ d) ∩ (((a ∪ c) ∪ d) ∩ ((a ∪ c) ∪ b)))
31	29, 30	tr 62	. . . . . . 7 (((b ∪ d) ∩ ((a ∪ c) ∪ b)) ∩ ((a ∪ c) ∪ d)) = ((((a ∪ c) ∩ (b ∪ d)) ∪ d) ∩ (((a ∪ c) ∪ d) ∩ ((a ∪ c) ∪ b)))
32		l42modlem1 1149	. . . . . . . . 9 (((a ∪ c) ∪ d) ∩ ((a ∪ c) ∪ b)) = ((a ∪ c) ∪ ((a ∪ d) ∩ (c ∪ b)))
33		orcom 73	. . . . . . . . . . . 12 (a ∪ d) = (d ∪ a)
34		orcom 73	. . . . . . . . . . . 12 (c ∪ b) = (b ∪ c)
35	33, 34	2an 79	. . . . . . . . . . 11 ((a ∪ d) ∩ (c ∪ b)) = ((d ∪ a) ∩ (b ∪ c))
36		ancom 74	. . . . . . . . . . 11 ((d ∪ a) ∩ (b ∪ c)) = ((b ∪ c) ∩ (d ∪ a))
37	35, 36	tr 62	. . . . . . . . . 10 ((a ∪ d) ∩ (c ∪ b)) = ((b ∪ c) ∩ (d ∪ a))
38	37	lor 70	. . . . . . . . 9 ((a ∪ c) ∪ ((a ∪ d) ∩ (c ∪ b))) = ((a ∪ c) ∪ ((b ∪ c) ∩ (d ∪ a)))
39	32, 38	tr 62	. . . . . . . 8 (((a ∪ c) ∪ d) ∩ ((a ∪ c) ∪ b)) = ((a ∪ c) ∪ ((b ∪ c) ∩ (d ∪ a)))
40	39	lan 77	. . . . . . 7 ((((a ∪ c) ∩ (b ∪ d)) ∪ d) ∩ (((a ∪ c) ∪ d) ∩ ((a ∪ c) ∪ b))) = ((((a ∪ c) ∩ (b ∪ d)) ∪ d) ∩ ((a ∪ c) ∪ ((b ∪ c) ∩ (d ∪ a))))
41	31, 40	tr 62	. . . . . 6 (((b ∪ d) ∩ ((a ∪ c) ∪ b)) ∩ ((a ∪ c) ∪ d)) = ((((a ∪ c) ∩ (b ∪ d)) ∪ d) ∩ ((a ∪ c) ∪ ((b ∪ c) ∩ (d ∪ a))))
42		leao1 162	. . . . . . 7 ((a ∪ c) ∩ (b ∪ d)) ≤ ((a ∪ c) ∪ ((b ∪ c) ∩ (d ∪ a)))
43	42	mlduali 1128	. . . . . 6 ((((a ∪ c) ∩ (b ∪ d)) ∪ d) ∩ ((a ∪ c) ∪ ((b ∪ c) ∩ (d ∪ a)))) = (((a ∪ c) ∩ (b ∪ d)) ∪ (d ∩ ((a ∪ c) ∪ ((b ∪ c) ∩ (d ∪ a)))))
44	41, 43	tr 62	. . . . 5 (((b ∪ d) ∩ ((a ∪ c) ∪ b)) ∩ ((a ∪ c) ∪ d)) = (((a ∪ c) ∩ (b ∪ d)) ∪ (d ∩ ((a ∪ c) ∪ ((b ∪ c) ∩ (d ∪ a)))))
45	44	lan 77	. . . 4 (b ∩ (((b ∪ d) ∩ ((a ∪ c) ∪ b)) ∩ ((a ∪ c) ∪ d))) = (b ∩ (((a ∪ c) ∩ (b ∪ d)) ∪ (d ∩ ((a ∪ c) ∪ ((b ∪ c) ∩ (d ∪ a))))))
46	15, 45	tr 62	. . 3 (b ∩ ((a ∪ c) ∪ d)) = (b ∩ (((a ∪ c) ∩ (b ∪ d)) ∪ (d ∩ ((a ∪ c) ∪ ((b ∪ c) ∩ (d ∪ a))))))
47	46	lor 70	. 2 (a ∪ (b ∩ ((a ∪ c) ∪ d))) = (a ∪ (b ∩ (((a ∪ c) ∩ (b ∪ d)) ∪ (d ∩ ((a ∪ c) ∪ ((b ∪ c) ∩ (d ∪ a)))))))
48	7, 47	tr 62	1 ((a ∪ b) ∩ (a ∪ (c ∪ d))) = (a ∪ (b ∩ (((a ∪ c) ∩ (b ∪ d)) ∪ (d ∩ ((a ∪ c) ∪ ((b ∪ c) ∩ (d ∪ a)))))))

This proof depends on syntax axioms:   = wb 1   ∪ wo 6   ∩ wa 7

This proof depends on axioms:  ax-a1 30  ax-a2 31  ax-a3 32  ax-a5 34  ax-r1 35  ax-r2 36  ax-r4 37  ax-r5 38  ax-ml 1122

This proof depends on definitions:  df-a 40  df-t 41  df-f 42  df-le1 130  df-le2 131

This theorem is used by: (None)