Quantum Logic Explorer

Quantum Logic Explorer

< Previous Next >
Related theorems
GIF version

Theorem mhcor1 870

Description: Corollary of Marsden-Herman Lemma.

**Assertion**
Ref	Expression
mhcor1	((((a →₁b) ∩ (b →₂c)) ∩ (c →₁d)) ∩ (d →₂a)) = (((a ≡ b) ∩ (b ≡ c)) ∩ (c ≡ d))

**Proof of Theorem mhcor1**
Step	Hyp	Ref	Expression
1		anass 69	. . 3 ((((b →₂c) ∩ (c →₁d)) ∩ (a →₁b)) ∩ (d →₂a)) = (((b →₂c) ∩ (c →₁d)) ∩ ((a →₁b) ∩ (d →₂a)))
2		imp3 823	. . . 4 ((b →₂c) ∩ (c →₁d)) = ((b^⊥ ∩ c^⊥ ) ∪ (c ∩ d))
3		ancom 68	. . . . 5 ((a →₁b) ∩ (d →₂a)) = ((d →₂a) ∩ (a →₁b))
4		imp3 823	. . . . 5 ((d →₂a) ∩ (a →₁b)) = ((d^⊥ ∩ a^⊥ ) ∪ (a ∩ b))
5	3, 4	ax-r2 35	. . . 4 ((a →₁b) ∩ (d →₂a)) = ((d^⊥ ∩ a^⊥ ) ∪ (a ∩ b))
6	2, 5	2an 72	. . 3 (((b →₂c) ∩ (c →₁d)) ∩ ((a →₁b) ∩ (d →₂a))) = (((b^⊥ ∩ c^⊥ ) ∪ (c ∩ d)) ∩ ((d^⊥ ∩ a^⊥ ) ∪ (a ∩ b)))
7		leao3 156	. . . . . . . . 9 (c ∩ d) ≤ (b ∪ c)
8		oran 79	. . . . . . . . 9 (b ∪ c) = (b^⊥ ∩ c^⊥ )^⊥
9	7, 8	lbtr 131	. . . . . . . 8 (c ∩ d) ≤ (b^⊥ ∩ c^⊥ )^⊥
10	9	lecom 172	. . . . . . 7 (c ∩ d) C (b^⊥ ∩ c^⊥ )^⊥
11	10	comcom7 442	. . . . . 6 (c ∩ d) C (b^⊥ ∩ c^⊥ )
12	11	comcom 435	. . . . 5 (b^⊥ ∩ c^⊥ ) C (c ∩ d)
13		leao2 155	. . . . . . . 8 (c ∩ d) ≤ (d ∪ a)
14		oran 79	. . . . . . . 8 (d ∪ a) = (d^⊥ ∩ a^⊥ )^⊥
15	13, 14	lbtr 131	. . . . . . 7 (c ∩ d) ≤ (d^⊥ ∩ a^⊥ )^⊥
16	15	lecom 172	. . . . . 6 (c ∩ d) C (d^⊥ ∩ a^⊥ )^⊥
17	16	comcom7 442	. . . . 5 (c ∩ d) C (d^⊥ ∩ a^⊥ )
18		leao3 156	. . . . . . . . 9 (a ∩ b) ≤ (d ∪ a)
19	18, 14	lbtr 131	. . . . . . . 8 (a ∩ b) ≤ (d^⊥ ∩ a^⊥ )^⊥
20	19	lecom 172	. . . . . . 7 (a ∩ b) C (d^⊥ ∩ a^⊥ )^⊥
21	20	comcom7 442	. . . . . 6 (a ∩ b) C (d^⊥ ∩ a^⊥ )
22	21	comcom 435	. . . . 5 (d^⊥ ∩ a^⊥ ) C (a ∩ b)
23		leao2 155	. . . . . . . 8 (a ∩ b) ≤ (b ∪ c)
24	23, 8	lbtr 131	. . . . . . 7 (a ∩ b) ≤ (b^⊥ ∩ c^⊥ )^⊥
25	24	lecom 172	. . . . . 6 (a ∩ b) C (b^⊥ ∩ c^⊥ )^⊥
26	25	comcom7 442	. . . . 5 (a ∩ b) C (b^⊥ ∩ c^⊥ )
27	12, 17, 22, 26	mh2 866	. . . 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 68	. . . . . . . 8 ((c^⊥ ∩ d^⊥ ) ∩ (a^⊥ ∩ b^⊥ )) = ((a^⊥ ∩ b^⊥ ) ∩ (c^⊥ ∩ d^⊥ ))
29		ancom 68	. . . . . . . . . 10 (b^⊥ ∩ c^⊥ ) = (c^⊥ ∩ b^⊥ )
30	29	ran 71	. . . . . . . . 9 ((b^⊥ ∩ c^⊥ ) ∩ (d^⊥ ∩ a^⊥ )) = ((c^⊥ ∩ b^⊥ ) ∩ (d^⊥ ∩ a^⊥ ))
31		an4 78	. . . . . . . . 9 ((c^⊥ ∩ b^⊥ ) ∩ (d^⊥ ∩ a^⊥ )) = ((c^⊥ ∩ d^⊥ ) ∩ (b^⊥ ∩ a^⊥ ))
32		ancom 68	. . . . . . . . . 10 (b^⊥ ∩ a^⊥ ) = (a^⊥ ∩ b^⊥ )
33	32	lan 70	. . . . . . . . 9 ((c^⊥ ∩ d^⊥ ) ∩ (b^⊥ ∩ a^⊥ )) = ((c^⊥ ∩ d^⊥ ) ∩ (a^⊥ ∩ b^⊥ ))
34	30, 31, 33	3tr 62	. . . . . . . 8 ((b^⊥ ∩ c^⊥ ) ∩ (d^⊥ ∩ a^⊥ )) = ((c^⊥ ∩ d^⊥ ) ∩ (a^⊥ ∩ b^⊥ ))
35		anass 69	. . . . . . . 8 (((a^⊥ ∩ b^⊥ ) ∩ c^⊥ ) ∩ d^⊥ ) = ((a^⊥ ∩ b^⊥ ) ∩ (c^⊥ ∩ d^⊥ ))
36	28, 34, 35	3tr1 60	. . . . . . 7 ((b^⊥ ∩ c^⊥ ) ∩ (d^⊥ ∩ a^⊥ )) = (((a^⊥ ∩ b^⊥ ) ∩ c^⊥ ) ∩ d^⊥ )
37		ancom 68	. . . . . . . 8 ((b^⊥ ∩ c^⊥ ) ∩ (a ∩ b)) = ((a ∩ b) ∩ (b^⊥ ∩ c^⊥ ))
38		anass 69	. . . . . . . 8 ((a ∩ b) ∩ (b^⊥ ∩ c^⊥ )) = (a ∩ (b ∩ (b^⊥ ∩ c^⊥ )))
39		dff 93	. . . . . . . . . . . . 13 0 = (b ∩ b^⊥ )
40	39	ran 71	. . . . . . . . . . . 12 (0 ∩ c^⊥ ) = ((b ∩ b^⊥ ) ∩ c^⊥ )
41	40	ax-r1 34	. . . . . . . . . . 11 ((b ∩ b^⊥ ) ∩ c^⊥ ) = (0 ∩ c^⊥ )
42		anass 69	. . . . . . . . . . 11 ((b ∩ b^⊥ ) ∩ c^⊥ ) = (b ∩ (b^⊥ ∩ c^⊥ ))
43		an0r 101	. . . . . . . . . . 11 (0 ∩ c^⊥ ) = 0
44	41, 42, 43	3tr2 61	. . . . . . . . . 10 (b ∩ (b^⊥ ∩ c^⊥ )) = 0
45	44	lan 70	. . . . . . . . 9 (a ∩ (b ∩ (b^⊥ ∩ c^⊥ ))) = (a ∩ 0)
46		an0 100	. . . . . . . . 9 (a ∩ 0) = 0
47	45, 46	ax-r2 35	. . . . . . . 8 (a ∩ (b ∩ (b^⊥ ∩ c^⊥ ))) = 0
48	37, 38, 47	3tr 62	. . . . . . 7 ((b^⊥ ∩ c^⊥ ) ∩ (a ∩ b)) = 0
49	36, 48	2or 67	. . . . . 6 (((b^⊥ ∩ c^⊥ ) ∩ (d^⊥ ∩ a^⊥ )) ∪ ((b^⊥ ∩ c^⊥ ) ∩ (a ∩ b))) = ((((a^⊥ ∩ b^⊥ ) ∩ c^⊥ ) ∩ d^⊥ ) ∪ 0)
50		or0 94	. . . . . 6 ((((a^⊥ ∩ b^⊥ ) ∩ c^⊥ ) ∩ d^⊥ ) ∪ 0) = (((a^⊥ ∩ b^⊥ ) ∩ c^⊥ ) ∩ d^⊥ )
51	49, 50	ax-r2 35	. . . . 5 (((b^⊥ ∩ c^⊥ ) ∩ (d^⊥ ∩ a^⊥ )) ∪ ((b^⊥ ∩ c^⊥ ) ∩ (a ∩ b))) = (((a^⊥ ∩ b^⊥ ) ∩ c^⊥ ) ∩ d^⊥ )
52		anass 69	. . . . . . . 8 ((c ∩ d) ∩ (d^⊥ ∩ a^⊥ )) = (c ∩ (d ∩ (d^⊥ ∩ a^⊥ )))
53		anass 69	. . . . . . . . . . 11 ((d ∩ d^⊥ ) ∩ a^⊥ ) = (d ∩ (d^⊥ ∩ a^⊥ ))
54	53	ax-r1 34	. . . . . . . . . 10 (d ∩ (d^⊥ ∩ a^⊥ )) = ((d ∩ d^⊥ ) ∩ a^⊥ )
55		an0r 101	. . . . . . . . . . . . 13 (0 ∩ a^⊥ ) = 0
56	55	ax-r1 34	. . . . . . . . . . . 12 0 = (0 ∩ a^⊥ )
57		dff 93	. . . . . . . . . . . . 13 0 = (d ∩ d^⊥ )
58	57	ran 71	. . . . . . . . . . . 12 (0 ∩ a^⊥ ) = ((d ∩ d^⊥ ) ∩ a^⊥ )
59	56, 58	ax-r2 35	. . . . . . . . . . 11 0 = ((d ∩ d^⊥ ) ∩ a^⊥ )
60	59	ax-r1 34	. . . . . . . . . 10 ((d ∩ d^⊥ ) ∩ a^⊥ ) = 0
61	54, 60	ax-r2 35	. . . . . . . . 9 (d ∩ (d^⊥ ∩ a^⊥ )) = 0
62	61	lan 70	. . . . . . . 8 (c ∩ (d ∩ (d^⊥ ∩ a^⊥ ))) = (c ∩ 0)
63		an0 100	. . . . . . . 8 (c ∩ 0) = 0
64	52, 62, 63	3tr 62	. . . . . . 7 ((c ∩ d) ∩ (d^⊥ ∩ a^⊥ )) = 0
65		ancom 68	. . . . . . . 8 ((c ∩ d) ∩ (a ∩ b)) = ((a ∩ b) ∩ (c ∩ d))
66		anass 69	. . . . . . . . 9 (((a ∩ b) ∩ c) ∩ d) = ((a ∩ b) ∩ (c ∩ d))
67	66	ax-r1 34	. . . . . . . 8 ((a ∩ b) ∩ (c ∩ d)) = (((a ∩ b) ∩ c) ∩ d)
68	65, 67	ax-r2 35	. . . . . . 7 ((c ∩ d) ∩ (a ∩ b)) = (((a ∩ b) ∩ c) ∩ d)
69	64, 68	2or 67	. . . . . 6 (((c ∩ d) ∩ (d^⊥ ∩ a^⊥ )) ∪ ((c ∩ d) ∩ (a ∩ b))) = (0 ∪ (((a ∩ b) ∩ c) ∩ d))
70		or0r 95	. . . . . 6 (0 ∪ (((a ∩ b) ∩ c) ∩ d)) = (((a ∩ b) ∩ c) ∩ d)
71	69, 70	ax-r2 35	. . . . 5 (((c ∩ d) ∩ (d^⊥ ∩ a^⊥ )) ∪ ((c ∩ d) ∩ (a ∩ b))) = (((a ∩ b) ∩ c) ∩ d)
72	51, 71	2or 67	. . . 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 30	. . . 4 ((((a^⊥ ∩ b^⊥ ) ∩ c^⊥ ) ∩ d^⊥ ) ∪ (((a ∩ b) ∩ c) ∩ d)) = ((((a ∩ b) ∩ c) ∩ d) ∪ (((a^⊥ ∩ b^⊥ ) ∩ c^⊥ ) ∩ d^⊥ ))
74	27, 72, 73	3tr 62	. . 3 (((b^⊥ ∩ c^⊥ ) ∪ (c ∩ d)) ∩ ((d^⊥ ∩ a^⊥ ) ∪ (a ∩ b))) = ((((a ∩ b) ∩ c) ∩ d) ∪ (((a^⊥ ∩ b^⊥ ) ∩ c^⊥ ) ∩ d^⊥ ))
75	1, 6, 74	3tr 62	. 2 ((((b →₂c) ∩ (c →₁d)) ∩ (a →₁b)) ∩ (d →₂a)) = ((((a ∩ b) ∩ c) ∩ d) ∪ (((a^⊥ ∩ b^⊥ ) ∩ c^⊥ ) ∩ d^⊥ ))
76		anass 69	. . . 4 (((a →₁b) ∩ (b →₂c)) ∩ (c →₁d)) = ((a →₁b) ∩ ((b →₂c) ∩ (c →₁d)))
77		ancom 68	. . . 4 ((a →₁b) ∩ ((b →₂c) ∩ (c →₁d))) = (((b →₂c) ∩ (c →₁d)) ∩ (a →₁b))
78	76, 77	ax-r2 35	. . 3 (((a →₁b) ∩ (b →₂c)) ∩ (c →₁d)) = (((b →₂c) ∩ (c →₁d)) ∩ (a →₁b))
79	78	ran 71	. 2 ((((a →₁b) ∩ (b →₂c)) ∩ (c →₁d)) ∩ (d →₂a)) = ((((b →₂c) ∩ (c →₁d)) ∩ (a →₁b)) ∩ (d →₂a))
80		bi4 822	. 2 (((a ≡ b) ∩ (b ≡ c)) ∩ (c ≡ d)) = ((((a ∩ b) ∩ c) ∩ d) ∪ (((a^⊥ ∩ b^⊥ ) ∩ c^⊥ ) ∩ d^⊥ ))
81	75, 79, 80	3tr1 60	1 ((((a →₁b) ∩ (b →₂c)) ∩ (c →₁d)) ∩ (d →₂a)) = (((a ≡ b) ∩ (b ≡ c)) ∩ (c ≡ d))

Colors of variables: term

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

This theorem is referenced by: oago3.29 871 oago3.21x 872

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

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

metamath.org