Quantum Logic Explorer

Quantum Logic Explorer

< Previous Next >
Related theorems
GIF version

Theorem bi4 822

Description: Chained biconditional.

**Assertion**
Ref	Expression
bi4	(((a ≡ b) ∩ (b ≡ c)) ∩ (c ≡ d)) = ((((a ∩ b) ∩ c) ∩ d) ∪ (((a^⊥ ∩ b^⊥ ) ∩ c^⊥ ) ∩ d^⊥ ))

**Proof of Theorem bi4**
Step	Hyp	Ref	Expression
1		bi3 821	. . 3 ((a ≡ b) ∩ (b ≡ c)) = (((a ∩ b) ∩ c) ∪ ((a^⊥ ∩ b^⊥ ) ∩ c^⊥ ))
2		u12lembi 708	. . . 4 ((c →₁d) ∩ (d →₂c)) = (c ≡ d)
3	2	ax-r1 34	. . 3 (c ≡ d) = ((c →₁d) ∩ (d →₂c))
4	1, 3	2an 72	. 2 (((a ≡ b) ∩ (b ≡ c)) ∩ (c ≡ d)) = ((((a ∩ b) ∩ c) ∪ ((a^⊥ ∩ b^⊥ ) ∩ c^⊥ )) ∩ ((c →₁d) ∩ (d →₂c)))
5		df-i1 43	. . . . . 6 (c →₁d) = (c^⊥ ∪ (c ∩ d))
6	5	lan 70	. . . . 5 ((((a ∩ b) ∩ c) ∪ ((a^⊥ ∩ b^⊥ ) ∩ c^⊥ )) ∩ (c →₁d)) = ((((a ∩ b) ∩ c) ∪ ((a^⊥ ∩ b^⊥ ) ∩ c^⊥ )) ∩ (c^⊥ ∪ (c ∩ d)))
7		leao2 155	. . . . . . 7 ((a^⊥ ∩ b^⊥ ) ∩ c^⊥ ) ≤ (c^⊥ ∪ (c ∩ d))
8	7	lecom 172	. . . . . 6 ((a^⊥ ∩ b^⊥ ) ∩ c^⊥ ) C (c^⊥ ∪ (c ∩ d))
9		leao4 157	. . . . . . . . . 10 ((a ∩ b) ∩ c) ≤ ((a^⊥ ∩ b^⊥ )^⊥ ∪ c)
10		oran2 84	. . . . . . . . . 10 ((a^⊥ ∩ b^⊥ )^⊥ ∪ c) = ((a^⊥ ∩ b^⊥ ) ∩ c^⊥ )^⊥
11	9, 10	lbtr 131	. . . . . . . . 9 ((a ∩ b) ∩ c) ≤ ((a^⊥ ∩ b^⊥ ) ∩ c^⊥ )^⊥
12	11	lecom 172	. . . . . . . 8 ((a ∩ b) ∩ c) C ((a^⊥ ∩ b^⊥ ) ∩ c^⊥ )^⊥
13	12	comcom 435	. . . . . . 7 ((a^⊥ ∩ b^⊥ ) ∩ c^⊥ )^⊥ C ((a ∩ b) ∩ c)
14	13	comcom6 441	. . . . . 6 ((a^⊥ ∩ b^⊥ ) ∩ c^⊥ ) C ((a ∩ b) ∩ c)
15	8, 14	fh2rc 462	. . . . 5 ((((a ∩ b) ∩ c) ∪ ((a^⊥ ∩ b^⊥ ) ∩ c^⊥ )) ∩ (c^⊥ ∪ (c ∩ d))) = ((((a ∩ b) ∩ c) ∩ (c^⊥ ∪ (c ∩ d))) ∪ (((a^⊥ ∩ b^⊥ ) ∩ c^⊥ ) ∩ (c^⊥ ∪ (c ∩ d))))
16		comanr2 447	. . . . . . . . 9 c C ((a ∩ b) ∩ c)
17	16	comcom3 436	. . . . . . . 8 c^⊥ C ((a ∩ b) ∩ c)
18		comanr1 446	. . . . . . . . 9 c C (c ∩ d)
19	18	comcom3 436	. . . . . . . 8 c^⊥ C (c ∩ d)
20	17, 19	fh2 452	. . . . . . 7 (((a ∩ b) ∩ c) ∩ (c^⊥ ∪ (c ∩ d))) = ((((a ∩ b) ∩ c) ∩ c^⊥ ) ∪ (((a ∩ b) ∩ c) ∩ (c ∩ d)))
21		anass 69	. . . . . . . . 9 (((a ∩ b) ∩ c) ∩ c^⊥ ) = ((a ∩ b) ∩ (c ∩ c^⊥ ))
22		dff 93	. . . . . . . . . . 11 0 = (c ∩ c^⊥ )
23	22	lan 70	. . . . . . . . . 10 ((a ∩ b) ∩ 0) = ((a ∩ b) ∩ (c ∩ c^⊥ ))
24	23	ax-r1 34	. . . . . . . . 9 ((a ∩ b) ∩ (c ∩ c^⊥ )) = ((a ∩ b) ∩ 0)
25		an0 100	. . . . . . . . 9 ((a ∩ b) ∩ 0) = 0
26	21, 24, 25	3tr 62	. . . . . . . 8 (((a ∩ b) ∩ c) ∩ c^⊥ ) = 0
27		anass 69	. . . . . . . . . 10 ((((a ∩ b) ∩ c) ∩ c) ∩ d) = (((a ∩ b) ∩ c) ∩ (c ∩ d))
28	27	ax-r1 34	. . . . . . . . 9 (((a ∩ b) ∩ c) ∩ (c ∩ d)) = ((((a ∩ b) ∩ c) ∩ c) ∩ d)
29		anass 69	. . . . . . . . . . 11 (((a ∩ b) ∩ c) ∩ c) = ((a ∩ b) ∩ (c ∩ c))
30		anidm 103	. . . . . . . . . . . 12 (c ∩ c) = c
31	30	lan 70	. . . . . . . . . . 11 ((a ∩ b) ∩ (c ∩ c)) = ((a ∩ b) ∩ c)
32	29, 31	ax-r2 35	. . . . . . . . . 10 (((a ∩ b) ∩ c) ∩ c) = ((a ∩ b) ∩ c)
33	32	ran 71	. . . . . . . . 9 ((((a ∩ b) ∩ c) ∩ c) ∩ d) = (((a ∩ b) ∩ c) ∩ d)
34	28, 33	ax-r2 35	. . . . . . . 8 (((a ∩ b) ∩ c) ∩ (c ∩ d)) = (((a ∩ b) ∩ c) ∩ d)
35	26, 34	2or 67	. . . . . . 7 ((((a ∩ b) ∩ c) ∩ c^⊥ ) ∪ (((a ∩ b) ∩ c) ∩ (c ∩ d))) = (0 ∪ (((a ∩ b) ∩ c) ∩ d))
36		or0r 95	. . . . . . 7 (0 ∪ (((a ∩ b) ∩ c) ∩ d)) = (((a ∩ b) ∩ c) ∩ d)
37	20, 35, 36	3tr 62	. . . . . 6 (((a ∩ b) ∩ c) ∩ (c^⊥ ∪ (c ∩ d))) = (((a ∩ b) ∩ c) ∩ d)
38		comanr2 447	. . . . . . . 8 c^⊥ C ((a^⊥ ∩ b^⊥ ) ∩ c^⊥ )
39	38, 19	fh2 452	. . . . . . 7 (((a^⊥ ∩ b^⊥ ) ∩ c^⊥ ) ∩ (c^⊥ ∪ (c ∩ d))) = ((((a^⊥ ∩ b^⊥ ) ∩ c^⊥ ) ∩ c^⊥ ) ∪ (((a^⊥ ∩ b^⊥ ) ∩ c^⊥ ) ∩ (c ∩ d)))
40		anass 69	. . . . . . . . 9 (((a^⊥ ∩ b^⊥ ) ∩ c^⊥ ) ∩ c^⊥ ) = ((a^⊥ ∩ b^⊥ ) ∩ (c^⊥ ∩ c^⊥ ))
41		anidm 103	. . . . . . . . . 10 (c^⊥ ∩ c^⊥ ) = c^⊥
42	41	lan 70	. . . . . . . . 9 ((a^⊥ ∩ b^⊥ ) ∩ (c^⊥ ∩ c^⊥ )) = ((a^⊥ ∩ b^⊥ ) ∩ c^⊥ )
43	40, 42	ax-r2 35	. . . . . . . 8 (((a^⊥ ∩ b^⊥ ) ∩ c^⊥ ) ∩ c^⊥ ) = ((a^⊥ ∩ b^⊥ ) ∩ c^⊥ )
44		an4 78	. . . . . . . . 9 (((a^⊥ ∩ b^⊥ ) ∩ c^⊥ ) ∩ (c ∩ d)) = (((a^⊥ ∩ b^⊥ ) ∩ c) ∩ (c^⊥ ∩ d))
45		anass 69	. . . . . . . . 9 (((a^⊥ ∩ b^⊥ ) ∩ c) ∩ (c^⊥ ∩ d)) = ((a^⊥ ∩ b^⊥ ) ∩ (c ∩ (c^⊥ ∩ d)))
46	22	ran 71	. . . . . . . . . . . . 13 (0 ∩ d) = ((c ∩ c^⊥ ) ∩ d)
47	46	ax-r1 34	. . . . . . . . . . . 12 ((c ∩ c^⊥ ) ∩ d) = (0 ∩ d)
48		anass 69	. . . . . . . . . . . 12 ((c ∩ c^⊥ ) ∩ d) = (c ∩ (c^⊥ ∩ d))
49		an0r 101	. . . . . . . . . . . 12 (0 ∩ d) = 0
50	47, 48, 49	3tr2 61	. . . . . . . . . . 11 (c ∩ (c^⊥ ∩ d)) = 0
51	50	lan 70	. . . . . . . . . 10 ((a^⊥ ∩ b^⊥ ) ∩ (c ∩ (c^⊥ ∩ d))) = ((a^⊥ ∩ b^⊥ ) ∩ 0)
52		an0 100	. . . . . . . . . 10 ((a^⊥ ∩ b^⊥ ) ∩ 0) = 0
53	51, 52	ax-r2 35	. . . . . . . . 9 ((a^⊥ ∩ b^⊥ ) ∩ (c ∩ (c^⊥ ∩ d))) = 0
54	44, 45, 53	3tr 62	. . . . . . . 8 (((a^⊥ ∩ b^⊥ ) ∩ c^⊥ ) ∩ (c ∩ d)) = 0
55	43, 54	2or 67	. . . . . . 7 ((((a^⊥ ∩ b^⊥ ) ∩ c^⊥ ) ∩ c^⊥ ) ∪ (((a^⊥ ∩ b^⊥ ) ∩ c^⊥ ) ∩ (c ∩ d))) = (((a^⊥ ∩ b^⊥ ) ∩ c^⊥ ) ∪ 0)
56		or0 94	. . . . . . 7 (((a^⊥ ∩ b^⊥ ) ∩ c^⊥ ) ∪ 0) = ((a^⊥ ∩ b^⊥ ) ∩ c^⊥ )
57	39, 55, 56	3tr 62	. . . . . 6 (((a^⊥ ∩ b^⊥ ) ∩ c^⊥ ) ∩ (c^⊥ ∪ (c ∩ d))) = ((a^⊥ ∩ b^⊥ ) ∩ c^⊥ )
58	37, 57	2or 67	. . . . 5 ((((a ∩ b) ∩ c) ∩ (c^⊥ ∪ (c ∩ d))) ∪ (((a^⊥ ∩ b^⊥ ) ∩ c^⊥ ) ∩ (c^⊥ ∪ (c ∩ d)))) = ((((a ∩ b) ∩ c) ∩ d) ∪ ((a^⊥ ∩ b^⊥ ) ∩ c^⊥ ))
59	6, 15, 58	3tr 62	. . . 4 ((((a ∩ b) ∩ c) ∪ ((a^⊥ ∩ b^⊥ ) ∩ c^⊥ )) ∩ (c →₁d)) = ((((a ∩ b) ∩ c) ∩ d) ∪ ((a^⊥ ∩ b^⊥ ) ∩ c^⊥ ))
60	59	ran 71	. . 3 (((((a ∩ b) ∩ c) ∪ ((a^⊥ ∩ b^⊥ ) ∩ c^⊥ )) ∩ (c →₁d)) ∩ (d →₂c)) = (((((a ∩ b) ∩ c) ∩ d) ∪ ((a^⊥ ∩ b^⊥ ) ∩ c^⊥ )) ∩ (d →₂c))
61		anass 69	. . 3 (((((a ∩ b) ∩ c) ∪ ((a^⊥ ∩ b^⊥ ) ∩ c^⊥ )) ∩ (c →₁d)) ∩ (d →₂c)) = ((((a ∩ b) ∩ c) ∪ ((a^⊥ ∩ b^⊥ ) ∩ c^⊥ )) ∩ ((c →₁d) ∩ (d →₂c)))
62		anass 69	. . . . . . . 8 ((((a ∩ b) ∩ c) ∩ d) ∩ (d →₂c)) = (((a ∩ b) ∩ c) ∩ (d ∩ (d →₂c)))
63		an4 78	. . . . . . . 8 (((a ∩ b) ∩ c) ∩ (d ∩ (d →₂c))) = (((a ∩ b) ∩ d) ∩ (c ∩ (d →₂c)))
64		ancom 68	. . . . . . . . . . 11 (c ∩ (d →₂c)) = ((d →₂c) ∩ c)
65		u2lemab 593	. . . . . . . . . . 11 ((d →₂c) ∩ c) = c
66	64, 65	ax-r2 35	. . . . . . . . . 10 (c ∩ (d →₂c)) = c
67	66	lan 70	. . . . . . . . 9 (((a ∩ b) ∩ d) ∩ (c ∩ (d →₂c))) = (((a ∩ b) ∩ d) ∩ c)
68		an32 76	. . . . . . . . 9 (((a ∩ b) ∩ d) ∩ c) = (((a ∩ b) ∩ c) ∩ d)
69	67, 68	ax-r2 35	. . . . . . . 8 (((a ∩ b) ∩ d) ∩ (c ∩ (d →₂c))) = (((a ∩ b) ∩ c) ∩ d)
70	62, 63, 69	3tr 62	. . . . . . 7 ((((a ∩ b) ∩ c) ∩ d) ∩ (d →₂c)) = (((a ∩ b) ∩ c) ∩ d)
71	70	df2le1 127	. . . . . 6 (((a ∩ b) ∩ c) ∩ d) ≤ (d →₂c)
72	71	lecom 172	. . . . 5 (((a ∩ b) ∩ c) ∩ d) C (d →₂c)
73		an32 76	. . . . . . . . 9 (((a ∩ b) ∩ c) ∩ d) = (((a ∩ b) ∩ d) ∩ c)
74		leao4 157	. . . . . . . . 9 (((a ∩ b) ∩ d) ∩ c) ≤ ((a^⊥ ∩ b^⊥ )^⊥ ∪ c)
75	73, 74	bltr 130	. . . . . . . 8 (((a ∩ b) ∩ c) ∩ d) ≤ ((a^⊥ ∩ b^⊥ )^⊥ ∪ c)
76	75, 10	lbtr 131	. . . . . . 7 (((a ∩ b) ∩ c) ∩ d) ≤ ((a^⊥ ∩ b^⊥ ) ∩ c^⊥ )^⊥
77	76	lecom 172	. . . . . 6 (((a ∩ b) ∩ c) ∩ d) C ((a^⊥ ∩ b^⊥ ) ∩ c^⊥ )^⊥
78	77	comcom7 442	. . . . 5 (((a ∩ b) ∩ c) ∩ d) C ((a^⊥ ∩ b^⊥ ) ∩ c^⊥ )
79	72, 78	fh2r 456	. . . 4 (((((a ∩ b) ∩ c) ∩ d) ∪ ((a^⊥ ∩ b^⊥ ) ∩ c^⊥ )) ∩ (d →₂c)) = (((((a ∩ b) ∩ c) ∩ d) ∩ (d →₂c)) ∪ (((a^⊥ ∩ b^⊥ ) ∩ c^⊥ ) ∩ (d →₂c)))
80		anass 69	. . . . . 6 (((a^⊥ ∩ b^⊥ ) ∩ c^⊥ ) ∩ (d →₂c)) = ((a^⊥ ∩ b^⊥ ) ∩ (c^⊥ ∩ (d →₂c)))
81		ancom 68	. . . . . . . 8 (c^⊥ ∩ (d →₂c)) = ((d →₂c) ∩ c^⊥ )
82		u2lemanb 598	. . . . . . . 8 ((d →₂c) ∩ c^⊥ ) = (d^⊥ ∩ c^⊥ )
83	81, 82	ax-r2 35	. . . . . . 7 (c^⊥ ∩ (d →₂c)) = (d^⊥ ∩ c^⊥ )
84	83	lan 70	. . . . . 6 ((a^⊥ ∩ b^⊥ ) ∩ (c^⊥ ∩ (d →₂c))) = ((a^⊥ ∩ b^⊥ ) ∩ (d^⊥ ∩ c^⊥ ))
85		an12 74	. . . . . . 7 ((a^⊥ ∩ b^⊥ ) ∩ (d^⊥ ∩ c^⊥ )) = (d^⊥ ∩ ((a^⊥ ∩ b^⊥ ) ∩ c^⊥ ))
86		ancom 68	. . . . . . 7 (d^⊥ ∩ ((a^⊥ ∩ b^⊥ ) ∩ c^⊥ )) = (((a^⊥ ∩ b^⊥ ) ∩ c^⊥ ) ∩ d^⊥ )
87	85, 86	ax-r2 35	. . . . . 6 ((a^⊥ ∩ b^⊥ ) ∩ (d^⊥ ∩ c^⊥ )) = (((a^⊥ ∩ b^⊥ ) ∩ c^⊥ ) ∩ d^⊥ )
88	80, 84, 87	3tr 62	. . . . 5 (((a^⊥ ∩ b^⊥ ) ∩ c^⊥ ) ∩ (d →₂c)) = (((a^⊥ ∩ b^⊥ ) ∩ c^⊥ ) ∩ d^⊥ )
89	70, 88	2or 67	. . . 4 (((((a ∩ b) ∩ c) ∩ d) ∩ (d →₂c)) ∪ (((a^⊥ ∩ b^⊥ ) ∩ c^⊥ ) ∩ (d →₂c))) = ((((a ∩ b) ∩ c) ∩ d) ∪ (((a^⊥ ∩ b^⊥ ) ∩ c^⊥ ) ∩ d^⊥ ))
90	79, 89	ax-r2 35	. . 3 (((((a ∩ b) ∩ c) ∩ d) ∪ ((a^⊥ ∩ b^⊥ ) ∩ c^⊥ )) ∩ (d →₂c)) = ((((a ∩ b) ∩ c) ∩ d) ∪ (((a^⊥ ∩ b^⊥ ) ∩ c^⊥ ) ∩ d^⊥ ))
91	60, 61, 90	3tr2 61	. 2 ((((a ∩ b) ∩ c) ∪ ((a^⊥ ∩ b^⊥ ) ∩ c^⊥ )) ∩ ((c →₁d) ∩ (d →₂c))) = ((((a ∩ b) ∩ c) ∩ d) ∪ (((a^⊥ ∩ b^⊥ ) ∩ c^⊥ ) ∩ d^⊥ ))
92	4, 91	ax-r2 35	1 (((a ≡ b) ∩ (b ≡ c)) ∩ (c ≡ d)) = ((((a ∩ b) ∩ c) ∩ d) ∪ (((a^⊥ ∩ b^⊥ ) ∩ 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: mhcor1 870

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