Theorem testmod2expanded 1216

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

Assertion

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

Proof of Theorem testmod2expanded

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

Syntax hints:   = wb 1   ∪ wo 6   ∩ wa 7

This theorem was proved from 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 theorem depends on definitions:  df-a 40  df-t 41  df-f 42  df-le1 130  df-le2 131

This theorem is referenced by: (None)