Theorem mhcor1 888

Description: Corollary of Marsden-Herman Lemma. (Contributed by NM, 26-Jun-2003.)

Assertion

Ref	Expression
mhcor1	((((a →1 b) ∩ (b →2 c)) ∩ (c →1 d)) ∩ (d →2 a)) = (((a ≡ b) ∩ (b ≡ c)) ∩ (c ≡ d))

Proof of Theorem mhcor1

Step	Hyp	Ref	Expression
1		anass 76	. . 3 ((((b →2 c) ∩ (c →1 d)) ∩ (a →1 b)) ∩ (d →2 a)) = (((b →2 c) ∩ (c →1 d)) ∩ ((a →1 b) ∩ (d →2 a)))
2		imp3 841	. . . 4 ((b →2 c) ∩ (c →1 d)) = ((b⊥ ∩ c⊥ ) ∪ (c ∩ d))
3		ancom 74	. . . . 5 ((a →1 b) ∩ (d →2 a)) = ((d →2 a) ∩ (a →1 b))
4		imp3 841	. . . . 5 ((d →2 a) ∩ (a →1 b)) = ((d⊥ ∩ a⊥ ) ∪ (a ∩ b))
5	3, 4	ax-r2 36	. . . 4 ((a →1 b) ∩ (d →2 a)) = ((d⊥ ∩ a⊥ ) ∪ (a ∩ b))
6	2, 5	2an 79	. . 3 (((b →2 c) ∩ (c →1 d)) ∩ ((a →1 b) ∩ (d →2 a))) = (((b⊥ ∩ c⊥ ) ∪ (c ∩ d)) ∩ ((d⊥ ∩ a⊥ ) ∪ (a ∩ b)))
7		leao3 164	. . . . . . . . 9 (c ∩ d) ≤ (b ∪ c)
8		oran 87	. . . . . . . . 9 (b ∪ c) = (b⊥ ∩ c⊥ )⊥
9	7, 8	lbtr 139	. . . . . . . 8 (c ∩ d) ≤ (b⊥ ∩ c⊥ )⊥
10	9	lecom 180	. . . . . . 7 (c ∩ d) C (b⊥ ∩ c⊥ )⊥
11	10	comcom7 460	. . . . . 6 (c ∩ d) C (b⊥ ∩ c⊥ )
12	11	comcom 453	. . . . 5 (b⊥ ∩ c⊥ ) C (c ∩ d)
13		leao2 163	. . . . . . . 8 (c ∩ d) ≤ (d ∪ a)
14		oran 87	. . . . . . . 8 (d ∪ a) = (d⊥ ∩ a⊥ )⊥
15	13, 14	lbtr 139	. . . . . . 7 (c ∩ d) ≤ (d⊥ ∩ a⊥ )⊥
16	15	lecom 180	. . . . . 6 (c ∩ d) C (d⊥ ∩ a⊥ )⊥
17	16	comcom7 460	. . . . 5 (c ∩ d) C (d⊥ ∩ a⊥ )
18		leao3 164	. . . . . . . . 9 (a ∩ b) ≤ (d ∪ a)
19	18, 14	lbtr 139	. . . . . . . 8 (a ∩ b) ≤ (d⊥ ∩ a⊥ )⊥
20	19	lecom 180	. . . . . . 7 (a ∩ b) C (d⊥ ∩ a⊥ )⊥
21	20	comcom7 460	. . . . . 6 (a ∩ b) C (d⊥ ∩ a⊥ )
22	21	comcom 453	. . . . 5 (d⊥ ∩ a⊥ ) C (a ∩ b)
23		leao2 163	. . . . . . . 8 (a ∩ b) ≤ (b ∪ c)
24	23, 8	lbtr 139	. . . . . . 7 (a ∩ b) ≤ (b⊥ ∩ c⊥ )⊥
25	24	lecom 180	. . . . . 6 (a ∩ b) C (b⊥ ∩ c⊥ )⊥
26	25	comcom7 460	. . . . 5 (a ∩ b) C (b⊥ ∩ c⊥ )
27	12, 17, 22, 26	mh2 884	. . . 4 (((b⊥ ∩ c⊥ ) ∪ (c ∩ d)) ∩ ((d⊥ ∩ a⊥ ) ∪ (a ∩ b))) = ((((b⊥ ∩ c⊥ ) ∩ (d⊥ ∩ a⊥ )) ∪ ((b⊥ ∩ c⊥ ) ∩ (a ∩ b))) ∪ (((c ∩ d) ∩ (d⊥ ∩ a⊥ )) ∪ ((c ∩ d) ∩ (a ∩ b))))
28		ancom 74	. . . . . . . 8 ((c⊥ ∩ d⊥ ) ∩ (a⊥ ∩ b⊥ )) = ((a⊥ ∩ b⊥ ) ∩ (c⊥ ∩ d⊥ ))
29		ancom 74	. . . . . . . . . 10 (b⊥ ∩ c⊥ ) = (c⊥ ∩ b⊥ )
30	29	ran 78	. . . . . . . . 9 ((b⊥ ∩ c⊥ ) ∩ (d⊥ ∩ a⊥ )) = ((c⊥ ∩ b⊥ ) ∩ (d⊥ ∩ a⊥ ))
31		an4 86	. . . . . . . . 9 ((c⊥ ∩ b⊥ ) ∩ (d⊥ ∩ a⊥ )) = ((c⊥ ∩ d⊥ ) ∩ (b⊥ ∩ a⊥ ))
32		ancom 74	. . . . . . . . . 10 (b⊥ ∩ a⊥ ) = (a⊥ ∩ b⊥ )
33	32	lan 77	. . . . . . . . 9 ((c⊥ ∩ d⊥ ) ∩ (b⊥ ∩ a⊥ )) = ((c⊥ ∩ d⊥ ) ∩ (a⊥ ∩ b⊥ ))
34	30, 31, 33	3tr 65	. . . . . . . 8 ((b⊥ ∩ c⊥ ) ∩ (d⊥ ∩ a⊥ )) = ((c⊥ ∩ d⊥ ) ∩ (a⊥ ∩ b⊥ ))
35		anass 76	. . . . . . . 8 (((a⊥ ∩ b⊥ ) ∩ c⊥ ) ∩ d⊥ ) = ((a⊥ ∩ b⊥ ) ∩ (c⊥ ∩ d⊥ ))
36	28, 34, 35	3tr1 63	. . . . . . 7 ((b⊥ ∩ c⊥ ) ∩ (d⊥ ∩ a⊥ )) = (((a⊥ ∩ b⊥ ) ∩ c⊥ ) ∩ d⊥ )
37		ancom 74	. . . . . . . 8 ((b⊥ ∩ c⊥ ) ∩ (a ∩ b)) = ((a ∩ b) ∩ (b⊥ ∩ c⊥ ))
38		anass 76	. . . . . . . 8 ((a ∩ b) ∩ (b⊥ ∩ c⊥ )) = (a ∩ (b ∩ (b⊥ ∩ c⊥ )))
39		dff 101	. . . . . . . . . . . . 13 0 = (b ∩ b⊥ )
40	39	ran 78	. . . . . . . . . . . 12 (0 ∩ c⊥ ) = ((b ∩ b⊥ ) ∩ c⊥ )
41	40	ax-r1 35	. . . . . . . . . . 11 ((b ∩ b⊥ ) ∩ c⊥ ) = (0 ∩ c⊥ )
42		anass 76	. . . . . . . . . . 11 ((b ∩ b⊥ ) ∩ c⊥ ) = (b ∩ (b⊥ ∩ c⊥ ))
43		an0r 109	. . . . . . . . . . 11 (0 ∩ c⊥ ) = 0
44	41, 42, 43	3tr2 64	. . . . . . . . . 10 (b ∩ (b⊥ ∩ c⊥ )) = 0
45	44	lan 77	. . . . . . . . 9 (a ∩ (b ∩ (b⊥ ∩ c⊥ ))) = (a ∩ 0)
46		an0 108	. . . . . . . . 9 (a ∩ 0) = 0
47	45, 46	ax-r2 36	. . . . . . . 8 (a ∩ (b ∩ (b⊥ ∩ c⊥ ))) = 0
48	37, 38, 47	3tr 65	. . . . . . 7 ((b⊥ ∩ c⊥ ) ∩ (a ∩ b)) = 0
49	36, 48	2or 72	. . . . . 6 (((b⊥ ∩ c⊥ ) ∩ (d⊥ ∩ a⊥ )) ∪ ((b⊥ ∩ c⊥ ) ∩ (a ∩ b))) = ((((a⊥ ∩ b⊥ ) ∩ c⊥ ) ∩ d⊥ ) ∪ 0)
50		or0 102	. . . . . 6 ((((a⊥ ∩ b⊥ ) ∩ c⊥ ) ∩ d⊥ ) ∪ 0) = (((a⊥ ∩ b⊥ ) ∩ c⊥ ) ∩ d⊥ )
51	49, 50	ax-r2 36	. . . . 5 (((b⊥ ∩ c⊥ ) ∩ (d⊥ ∩ a⊥ )) ∪ ((b⊥ ∩ c⊥ ) ∩ (a ∩ b))) = (((a⊥ ∩ b⊥ ) ∩ c⊥ ) ∩ d⊥ )
52		anass 76	. . . . . . . 8 ((c ∩ d) ∩ (d⊥ ∩ a⊥ )) = (c ∩ (d ∩ (d⊥ ∩ a⊥ )))
53		anass 76	. . . . . . . . . . 11 ((d ∩ d⊥ ) ∩ a⊥ ) = (d ∩ (d⊥ ∩ a⊥ ))
54	53	ax-r1 35	. . . . . . . . . 10 (d ∩ (d⊥ ∩ a⊥ )) = ((d ∩ d⊥ ) ∩ a⊥ )
55		an0r 109	. . . . . . . . . . . . 13 (0 ∩ a⊥ ) = 0
56	55	ax-r1 35	. . . . . . . . . . . 12 0 = (0 ∩ a⊥ )
57		dff 101	. . . . . . . . . . . . 13 0 = (d ∩ d⊥ )
58	57	ran 78	. . . . . . . . . . . 12 (0 ∩ a⊥ ) = ((d ∩ d⊥ ) ∩ a⊥ )
59	56, 58	ax-r2 36	. . . . . . . . . . 11 0 = ((d ∩ d⊥ ) ∩ a⊥ )
60	59	ax-r1 35	. . . . . . . . . 10 ((d ∩ d⊥ ) ∩ a⊥ ) = 0
61	54, 60	ax-r2 36	. . . . . . . . 9 (d ∩ (d⊥ ∩ a⊥ )) = 0
62	61	lan 77	. . . . . . . 8 (c ∩ (d ∩ (d⊥ ∩ a⊥ ))) = (c ∩ 0)
63		an0 108	. . . . . . . 8 (c ∩ 0) = 0
64	52, 62, 63	3tr 65	. . . . . . 7 ((c ∩ d) ∩ (d⊥ ∩ a⊥ )) = 0
65		ancom 74	. . . . . . . 8 ((c ∩ d) ∩ (a ∩ b)) = ((a ∩ b) ∩ (c ∩ d))
66		anass 76	. . . . . . . . 9 (((a ∩ b) ∩ c) ∩ d) = ((a ∩ b) ∩ (c ∩ d))
67	66	ax-r1 35	. . . . . . . 8 ((a ∩ b) ∩ (c ∩ d)) = (((a ∩ b) ∩ c) ∩ d)
68	65, 67	ax-r2 36	. . . . . . 7 ((c ∩ d) ∩ (a ∩ b)) = (((a ∩ b) ∩ c) ∩ d)
69	64, 68	2or 72	. . . . . 6 (((c ∩ d) ∩ (d⊥ ∩ a⊥ )) ∪ ((c ∩ d) ∩ (a ∩ b))) = (0 ∪ (((a ∩ b) ∩ c) ∩ d))
70		or0r 103	. . . . . 6 (0 ∪ (((a ∩ b) ∩ c) ∩ d)) = (((a ∩ b) ∩ c) ∩ d)
71	69, 70	ax-r2 36	. . . . 5 (((c ∩ d) ∩ (d⊥ ∩ a⊥ )) ∪ ((c ∩ d) ∩ (a ∩ b))) = (((a ∩ b) ∩ c) ∩ d)
72	51, 71	2or 72	. . . 4 ((((b⊥ ∩ c⊥ ) ∩ (d⊥ ∩ a⊥ )) ∪ ((b⊥ ∩ c⊥ ) ∩ (a ∩ b))) ∪ (((c ∩ d) ∩ (d⊥ ∩ a⊥ )) ∪ ((c ∩ d) ∩ (a ∩ b)))) = ((((a⊥ ∩ b⊥ ) ∩ c⊥ ) ∩ d⊥ ) ∪ (((a ∩ b) ∩ c) ∩ d))
73		ax-a2 31	. . . 4 ((((a⊥ ∩ b⊥ ) ∩ c⊥ ) ∩ d⊥ ) ∪ (((a ∩ b) ∩ c) ∩ d)) = ((((a ∩ b) ∩ c) ∩ d) ∪ (((a⊥ ∩ b⊥ ) ∩ c⊥ ) ∩ d⊥ ))
74	27, 72, 73	3tr 65	. . 3 (((b⊥ ∩ c⊥ ) ∪ (c ∩ d)) ∩ ((d⊥ ∩ a⊥ ) ∪ (a ∩ b))) = ((((a ∩ b) ∩ c) ∩ d) ∪ (((a⊥ ∩ b⊥ ) ∩ c⊥ ) ∩ d⊥ ))
75	1, 6, 74	3tr 65	. 2 ((((b →2 c) ∩ (c →1 d)) ∩ (a →1 b)) ∩ (d →2 a)) = ((((a ∩ b) ∩ c) ∩ d) ∪ (((a⊥ ∩ b⊥ ) ∩ c⊥ ) ∩ d⊥ ))
76		anass 76	. . . 4 (((a →1 b) ∩ (b →2 c)) ∩ (c →1 d)) = ((a →1 b) ∩ ((b →2 c) ∩ (c →1 d)))
77		ancom 74	. . . 4 ((a →1 b) ∩ ((b →2 c) ∩ (c →1 d))) = (((b →2 c) ∩ (c →1 d)) ∩ (a →1 b))
78	76, 77	ax-r2 36	. . 3 (((a →1 b) ∩ (b →2 c)) ∩ (c →1 d)) = (((b →2 c) ∩ (c →1 d)) ∩ (a →1 b))
79	78	ran 78	. 2 ((((a →1 b) ∩ (b →2 c)) ∩ (c →1 d)) ∩ (d →2 a)) = ((((b →2 c) ∩ (c →1 d)) ∩ (a →1 b)) ∩ (d →2 a))
80		bi4 840	. 2 (((a ≡ b) ∩ (b ≡ c)) ∩ (c ≡ d)) = ((((a ∩ b) ∩ c) ∩ d) ∪ (((a⊥ ∩ b⊥ ) ∩ c⊥ ) ∩ d⊥ ))
81	75, 79, 80	3tr1 63	1 ((((a →1 b) ∩ (b →2 c)) ∩ (c →1 d)) ∩ (d →2 a)) = (((a ≡ b) ∩ (b ≡ c)) ∩ (c ≡ d))

Syntax hints:   = wb 1  ^⊥ wn 4   ≡ tb 5   ∪ wo 6   ∩ wa 7  0wf 9   →₁ wi1 12   →₂ wi2 13

This theorem was proved from 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

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

This theorem is referenced by:  oago3.29  889  oago3.21x  890