Quantum Logic Explorer

Quantum Logic Explorer

< Previous Next >
Related theorems
GIF version

Theorem comanblem1 852

Description: Lemma for biconditional commutation law.

**Assertion**
Ref	Expression
comanblem1	((a ≡ c) ∩ (b ≡ c)) = (((a ∪ c)^⊥ ∪ ((a ∩ b) ∩ c)) ∩ (b →₁c))

**Proof of Theorem comanblem1**
Step	Hyp	Ref	Expression
1		an4 78	. 2 (((a →₁c) ∩ (c →₁a)) ∩ ((b →₁c) ∩ (c →₁b))) = (((a →₁c) ∩ (b →₁c)) ∩ ((c →₁a) ∩ (c →₁b)))
2		u1lembi 702	. . 3 ((a →₁c) ∩ (c →₁a)) = (a ≡ c)
3		u1lembi 702	. . 3 ((b →₁c) ∩ (c →₁b)) = (b ≡ c)
4	2, 3	2an 72	. 2 (((a →₁c) ∩ (c →₁a)) ∩ ((b →₁c) ∩ (c →₁b))) = ((a ≡ c) ∩ (b ≡ c))
5		an32 76	. . 3 (((a →₁c) ∩ (b →₁c)) ∩ ((c →₁a) ∩ (c →₁b))) = (((a →₁c) ∩ ((c →₁a) ∩ (c →₁b))) ∩ (b →₁c))
6		df-i1 43	. . . . . . . 8 (c →₁a) = (c^⊥ ∪ (c ∩ a))
7		df-i1 43	. . . . . . . 8 (c →₁b) = (c^⊥ ∪ (c ∩ b))
8	6, 7	2an 72	. . . . . . 7 ((c →₁a) ∩ (c →₁b)) = ((c^⊥ ∪ (c ∩ a)) ∩ (c^⊥ ∪ (c ∩ b)))
9		comanr1 446	. . . . . . . . . 10 c C (c ∩ a)
10	9	comcom3 436	. . . . . . . . 9 c^⊥ C (c ∩ a)
11		comanr1 446	. . . . . . . . . 10 c C (c ∩ b)
12	11	comcom3 436	. . . . . . . . 9 c^⊥ C (c ∩ b)
13	10, 12	fh3 453	. . . . . . . 8 (c^⊥ ∪ ((c ∩ a) ∩ (c ∩ b))) = ((c^⊥ ∪ (c ∩ a)) ∩ (c^⊥ ∪ (c ∩ b)))
14	13	ax-r1 34	. . . . . . 7 ((c^⊥ ∪ (c ∩ a)) ∩ (c^⊥ ∪ (c ∩ b))) = (c^⊥ ∪ ((c ∩ a) ∩ (c ∩ b)))
15	8, 14	ax-r2 35	. . . . . 6 ((c →₁a) ∩ (c →₁b)) = (c^⊥ ∪ ((c ∩ a) ∩ (c ∩ b)))
16	15	lan 70	. . . . 5 ((a →₁c) ∩ ((c →₁a) ∩ (c →₁b))) = ((a →₁c) ∩ (c^⊥ ∪ ((c ∩ a) ∩ (c ∩ b))))
17		df-i1 43	. . . . . 6 (a →₁c) = (a^⊥ ∪ (a ∩ c))
18	17	ran 71	. . . . 5 ((a →₁c) ∩ (c^⊥ ∪ ((c ∩ a) ∩ (c ∩ b)))) = ((a^⊥ ∪ (a ∩ c)) ∩ (c^⊥ ∪ ((c ∩ a) ∩ (c ∩ b))))
19		lea 152	. . . . . . . . 9 ((c ∩ a) ∩ (c ∩ b)) ≤ (c ∩ a)
20		ancom 68	. . . . . . . . . 10 (c ∩ a) = (a ∩ c)
21		leor 151	. . . . . . . . . 10 (a ∩ c) ≤ (a^⊥ ∪ (a ∩ c))
22	20, 21	bltr 130	. . . . . . . . 9 (c ∩ a) ≤ (a^⊥ ∪ (a ∩ c))
23	19, 22	letr 129	. . . . . . . 8 ((c ∩ a) ∩ (c ∩ b)) ≤ (a^⊥ ∪ (a ∩ c))
24	23	lecom 172	. . . . . . 7 ((c ∩ a) ∩ (c ∩ b)) C (a^⊥ ∪ (a ∩ c))
25	10, 12	com2an 466	. . . . . . . 8 c^⊥ C ((c ∩ a) ∩ (c ∩ b))
26	25	comcom 435	. . . . . . 7 ((c ∩ a) ∩ (c ∩ b)) C c^⊥
27	24, 26	fh2c 459	. . . . . 6 ((a^⊥ ∪ (a ∩ c)) ∩ (c^⊥ ∪ ((c ∩ a) ∩ (c ∩ b)))) = (((a^⊥ ∪ (a ∩ c)) ∩ c^⊥ ) ∪ ((a^⊥ ∪ (a ∩ c)) ∩ ((c ∩ a) ∩ (c ∩ b))))
28		coman2 178	. . . . . . . . . 10 (a ∩ c) C c
29	28	comcom2 175	. . . . . . . . 9 (a ∩ c) C c^⊥
30		coman1 177	. . . . . . . . . 10 (a ∩ c) C a
31	30	comcom2 175	. . . . . . . . 9 (a ∩ c) C a^⊥
32	29, 31	fh2rc 462	. . . . . . . 8 ((a^⊥ ∪ (a ∩ c)) ∩ c^⊥ ) = ((a^⊥ ∩ c^⊥ ) ∪ ((a ∩ c) ∩ c^⊥ ))
33		anass 69	. . . . . . . . . 10 ((a ∩ c) ∩ c^⊥ ) = (a ∩ (c ∩ c^⊥ ))
34		dff 93	. . . . . . . . . . . 12 0 = (c ∩ c^⊥ )
35	34	lan 70	. . . . . . . . . . 11 (a ∩ 0) = (a ∩ (c ∩ c^⊥ ))
36	35	ax-r1 34	. . . . . . . . . 10 (a ∩ (c ∩ c^⊥ )) = (a ∩ 0)
37		an0 100	. . . . . . . . . 10 (a ∩ 0) = 0
38	33, 36, 37	3tr 62	. . . . . . . . 9 ((a ∩ c) ∩ c^⊥ ) = 0
39	38	lor 66	. . . . . . . 8 ((a^⊥ ∩ c^⊥ ) ∪ ((a ∩ c) ∩ c^⊥ )) = ((a^⊥ ∩ c^⊥ ) ∪ 0)
40		or0 94	. . . . . . . . 9 ((a^⊥ ∩ c^⊥ ) ∪ 0) = (a^⊥ ∩ c^⊥ )
41		anor3 82	. . . . . . . . 9 (a^⊥ ∩ c^⊥ ) = (a ∪ c)^⊥
42	40, 41	ax-r2 35	. . . . . . . 8 ((a^⊥ ∩ c^⊥ ) ∪ 0) = (a ∪ c)^⊥
43	32, 39, 42	3tr 62	. . . . . . 7 ((a^⊥ ∪ (a ∩ c)) ∩ c^⊥ ) = (a ∪ c)^⊥
44		ancom 68	. . . . . . . . . 10 (a ∩ c) = (c ∩ a)
45		comanr1 446	. . . . . . . . . 10 (c ∩ a) C ((c ∩ a) ∩ (c ∩ b))
46	44, 45	bctr 173	. . . . . . . . 9 (a ∩ c) C ((c ∩ a) ∩ (c ∩ b))
47	46, 31	fh2rc 462	. . . . . . . 8 ((a^⊥ ∪ (a ∩ c)) ∩ ((c ∩ a) ∩ (c ∩ b))) = ((a^⊥ ∩ ((c ∩ a) ∩ (c ∩ b))) ∪ ((a ∩ c) ∩ ((c ∩ a) ∩ (c ∩ b))))
48		anandi 106	. . . . . . . . . . . 12 (c ∩ (a ∩ b)) = ((c ∩ a) ∩ (c ∩ b))
49	48	ax-r1 34	. . . . . . . . . . 11 ((c ∩ a) ∩ (c ∩ b)) = (c ∩ (a ∩ b))
50		ancom 68	. . . . . . . . . . 11 (c ∩ (a ∩ b)) = ((a ∩ b) ∩ c)
51	49, 50	ax-r2 35	. . . . . . . . . 10 ((c ∩ a) ∩ (c ∩ b)) = ((a ∩ b) ∩ c)
52	51	lan 70	. . . . . . . . 9 (a^⊥ ∩ ((c ∩ a) ∩ (c ∩ b))) = (a^⊥ ∩ ((a ∩ b) ∩ c))
53	51	lan 70	. . . . . . . . . 10 ((a ∩ c) ∩ ((c ∩ a) ∩ (c ∩ b))) = ((a ∩ c) ∩ ((a ∩ b) ∩ c))
54		ancom 68	. . . . . . . . . 10 ((a ∩ c) ∩ ((a ∩ b) ∩ c)) = (((a ∩ b) ∩ c) ∩ (a ∩ c))
55		lea 152	. . . . . . . . . . . 12 (a ∩ b) ≤ a
56	55	leran 145	. . . . . . . . . . 11 ((a ∩ b) ∩ c) ≤ (a ∩ c)
57	56	df2le2 128	. . . . . . . . . 10 (((a ∩ b) ∩ c) ∩ (a ∩ c)) = ((a ∩ b) ∩ c)
58	53, 54, 57	3tr 62	. . . . . . . . 9 ((a ∩ c) ∩ ((c ∩ a) ∩ (c ∩ b))) = ((a ∩ b) ∩ c)
59	52, 58	2or 67	. . . . . . . 8 ((a^⊥ ∩ ((c ∩ a) ∩ (c ∩ b))) ∪ ((a ∩ c) ∩ ((c ∩ a) ∩ (c ∩ b)))) = ((a^⊥ ∩ ((a ∩ b) ∩ c)) ∪ ((a ∩ b) ∩ c))
60		lear 153	. . . . . . . . 9 (a^⊥ ∩ ((a ∩ b) ∩ c)) ≤ ((a ∩ b) ∩ c)
61	60	df-le2 123	. . . . . . . 8 ((a^⊥ ∩ ((a ∩ b) ∩ c)) ∪ ((a ∩ b) ∩ c)) = ((a ∩ b) ∩ c)
62	47, 59, 61	3tr 62	. . . . . . 7 ((a^⊥ ∪ (a ∩ c)) ∩ ((c ∩ a) ∩ (c ∩ b))) = ((a ∩ b) ∩ c)
63	43, 62	2or 67	. . . . . 6 (((a^⊥ ∪ (a ∩ c)) ∩ c^⊥ ) ∪ ((a^⊥ ∪ (a ∩ c)) ∩ ((c ∩ a) ∩ (c ∩ b)))) = ((a ∪ c)^⊥ ∪ ((a ∩ b) ∩ c))
64	27, 63	ax-r2 35	. . . . 5 ((a^⊥ ∪ (a ∩ c)) ∩ (c^⊥ ∪ ((c ∩ a) ∩ (c ∩ b)))) = ((a ∪ c)^⊥ ∪ ((a ∩ b) ∩ c))
65	16, 18, 64	3tr 62	. . . 4 ((a →₁c) ∩ ((c →₁a) ∩ (c →₁b))) = ((a ∪ c)^⊥ ∪ ((a ∩ b) ∩ c))
66	65	ran 71	. . 3 (((a →₁c) ∩ ((c →₁a) ∩ (c →₁b))) ∩ (b →₁c)) = (((a ∪ c)^⊥ ∪ ((a ∩ b) ∩ c)) ∩ (b →₁c))
67	5, 66	ax-r2 35	. 2 (((a →₁c) ∩ (b →₁c)) ∩ ((c →₁a) ∩ (c →₁b))) = (((a ∪ c)^⊥ ∪ ((a ∩ b) ∩ c)) ∩ (b →₁c))
68	1, 4, 67	3tr2 61	1 ((a ≡ c) ∩ (b ≡ c)) = (((a ∪ c)^⊥ ∪ ((a ∩ b) ∩ c)) ∩ (b →₁c))

Colors of variables: term

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

This theorem is referenced by: comanb 854

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-le1 122 df-le2 123 df-c1 124 df-c2 125

metamath.org