Quantum Logic Explorer

Quantum Logic Explorer

< Previous Next >
Related theorems
GIF version

Theorem cancellem 873

Description: Lemma for cancellation law eliminating →₁ consequent.

**Hypothesis**
Ref	Expression
cancel.1	((d ∪ (a →₁c)) →₁c) = ((d ∪ (b →₁c)) →₁c)

**Assertion**
Ref	Expression
cancellem	(d ∪ (a →₁c)) ≤ (d ∪ (b →₁c))

**Proof of Theorem cancellem**
Step	Hyp	Ref	Expression
1		i1abs 783	. . 3 (((d ∪ (a →₁c)) →₁c)^⊥ ∪ ((d ∪ (a →₁c)) ∩ c)) = (d ∪ (a →₁c))
2	1	ax-r1 34	. 2 (d ∪ (a →₁c)) = (((d ∪ (a →₁c)) →₁c)^⊥ ∪ ((d ∪ (a →₁c)) ∩ c))
3		leo 150	. . . . 5 (d ∪ (b →₁c))^⊥ ≤ ((d ∪ (b →₁c))^⊥ ∪ ((d ∪ (b →₁c)) ∩ c))
4		cancel.1	. . . . . . 7 ((d ∪ (a →₁c)) →₁c) = ((d ∪ (b →₁c)) →₁c)
5		df-i1 43	. . . . . . 7 ((d ∪ (b →₁c)) →₁c) = ((d ∪ (b →₁c))^⊥ ∪ ((d ∪ (b →₁c)) ∩ c))
6	4, 5	ax-r2 35	. . . . . 6 ((d ∪ (a →₁c)) →₁c) = ((d ∪ (b →₁c))^⊥ ∪ ((d ∪ (b →₁c)) ∩ c))
7	6	ax-r1 34	. . . . 5 ((d ∪ (b →₁c))^⊥ ∪ ((d ∪ (b →₁c)) ∩ c)) = ((d ∪ (a →₁c)) →₁c)
8	3, 7	lbtr 131	. . . 4 (d ∪ (b →₁c))^⊥ ≤ ((d ∪ (a →₁c)) →₁c)
9	8	lecon2 148	. . 3 ((d ∪ (a →₁c)) →₁c)^⊥ ≤ (d ∪ (b →₁c))
10		leor 151	. . . . . 6 ((d ∪ (a →₁c)) ∩ c) ≤ ((d ∪ (a →₁c))^⊥ ∪ ((d ∪ (a →₁c)) ∩ c))
11		df-i1 43	. . . . . . . 8 ((d ∪ (a →₁c)) →₁c) = ((d ∪ (a →₁c))^⊥ ∪ ((d ∪ (a →₁c)) ∩ c))
12	11	ax-r1 34	. . . . . . 7 ((d ∪ (a →₁c))^⊥ ∪ ((d ∪ (a →₁c)) ∩ c)) = ((d ∪ (a →₁c)) →₁c)
13	12, 4	ax-r2 35	. . . . . 6 ((d ∪ (a →₁c))^⊥ ∪ ((d ∪ (a →₁c)) ∩ c)) = ((d ∪ (b →₁c)) →₁c)
14	10, 13	lbtr 131	. . . . 5 ((d ∪ (a →₁c)) ∩ c) ≤ ((d ∪ (b →₁c)) →₁c)
15		lear 153	. . . . 5 ((d ∪ (a →₁c)) ∩ c) ≤ c
16	14, 15	ler2an 165	. . . 4 ((d ∪ (a →₁c)) ∩ c) ≤ (((d ∪ (b →₁c)) →₁c) ∩ c)
17		coman2 178	. . . . . . 7 ((d ∪ (b →₁c)) ∩ c) C c
18		coman1 177	. . . . . . . 8 ((d ∪ (b →₁c)) ∩ c) C (d ∪ (b →₁c))
19	18	comcom2 175	. . . . . . 7 ((d ∪ (b →₁c)) ∩ c) C (d ∪ (b →₁c))^⊥
20	17, 19	fh2rc 462	. . . . . 6 (((d ∪ (b →₁c))^⊥ ∪ ((d ∪ (b →₁c)) ∩ c)) ∩ c) = (((d ∪ (b →₁c))^⊥ ∩ c) ∪ (((d ∪ (b →₁c)) ∩ c) ∩ c))
21	5	ran 71	. . . . . 6 (((d ∪ (b →₁c)) →₁c) ∩ c) = (((d ∪ (b →₁c))^⊥ ∪ ((d ∪ (b →₁c)) ∩ c)) ∩ c)
22		id 58	. . . . . 6 (((d ∪ (b →₁c))^⊥ ∩ c) ∪ (((d ∪ (b →₁c)) ∩ c) ∩ c)) = (((d ∪ (b →₁c))^⊥ ∩ c) ∪ (((d ∪ (b →₁c)) ∩ c) ∩ c))
23	20, 21, 22	3tr1 60	. . . . 5 (((d ∪ (b →₁c)) →₁c) ∩ c) = (((d ∪ (b →₁c))^⊥ ∩ c) ∪ (((d ∪ (b →₁c)) ∩ c) ∩ c))
24		leao4 157	. . . . . . . 8 ((d^⊥ ∩ (b ∩ c)^⊥ ) ∩ (b ∩ c)) ≤ (b^⊥ ∪ (b ∩ c))
25	24	lerr 142	. . . . . . 7 ((d^⊥ ∩ (b ∩ c)^⊥ ) ∩ (b ∩ c)) ≤ (d ∪ (b^⊥ ∪ (b ∩ c)))
26		df-i1 43	. . . . . . . . . . . 12 (b →₁c) = (b^⊥ ∪ (b ∩ c))
27	26	lor 66	. . . . . . . . . . 11 (d ∪ (b →₁c)) = (d ∪ (b^⊥ ∪ (b ∩ c)))
28	27	ax-r4 36	. . . . . . . . . 10 (d ∪ (b →₁c))^⊥ = (d ∪ (b^⊥ ∪ (b ∩ c)))^⊥
29		an12 74	. . . . . . . . . . . 12 (b ∩ (d^⊥ ∩ (b ∩ c)^⊥ )) = (d^⊥ ∩ (b ∩ (b ∩ c)^⊥ ))
30		anor1 80	. . . . . . . . . . . . 13 (b ∩ (b ∩ c)^⊥ ) = (b^⊥ ∪ (b ∩ c))^⊥
31	30	lan 70	. . . . . . . . . . . 12 (d^⊥ ∩ (b ∩ (b ∩ c)^⊥ )) = (d^⊥ ∩ (b^⊥ ∪ (b ∩ c))^⊥ )
32		anor3 82	. . . . . . . . . . . 12 (d^⊥ ∩ (b^⊥ ∪ (b ∩ c))^⊥ ) = (d ∪ (b^⊥ ∪ (b ∩ c)))^⊥
33	29, 31, 32	3tr 62	. . . . . . . . . . 11 (b ∩ (d^⊥ ∩ (b ∩ c)^⊥ )) = (d ∪ (b^⊥ ∪ (b ∩ c)))^⊥
34	33	ax-r1 34	. . . . . . . . . 10 (d ∪ (b^⊥ ∪ (b ∩ c)))^⊥ = (b ∩ (d^⊥ ∩ (b ∩ c)^⊥ ))
35		ancom 68	. . . . . . . . . 10 (b ∩ (d^⊥ ∩ (b ∩ c)^⊥ )) = ((d^⊥ ∩ (b ∩ c)^⊥ ) ∩ b)
36	28, 34, 35	3tr 62	. . . . . . . . 9 (d ∪ (b →₁c))^⊥ = ((d^⊥ ∩ (b ∩ c)^⊥ ) ∩ b)
37	36	ran 71	. . . . . . . 8 ((d ∪ (b →₁c))^⊥ ∩ c) = (((d^⊥ ∩ (b ∩ c)^⊥ ) ∩ b) ∩ c)
38		anass 69	. . . . . . . 8 (((d^⊥ ∩ (b ∩ c)^⊥ ) ∩ b) ∩ c) = ((d^⊥ ∩ (b ∩ c)^⊥ ) ∩ (b ∩ c))
39	37, 38	ax-r2 35	. . . . . . 7 ((d ∪ (b →₁c))^⊥ ∩ c) = ((d^⊥ ∩ (b ∩ c)^⊥ ) ∩ (b ∩ c))
40	25, 39, 27	le3tr1 132	. . . . . 6 ((d ∪ (b →₁c))^⊥ ∩ c) ≤ (d ∪ (b →₁c))
41		lea 152	. . . . . . 7 ((d ∪ (b →₁c)) ∩ c) ≤ (d ∪ (b →₁c))
42	41	lel 143	. . . . . 6 (((d ∪ (b →₁c)) ∩ c) ∩ c) ≤ (d ∪ (b →₁c))
43	40, 42	lel2or 162	. . . . 5 (((d ∪ (b →₁c))^⊥ ∩ c) ∪ (((d ∪ (b →₁c)) ∩ c) ∩ c)) ≤ (d ∪ (b →₁c))
44	23, 43	bltr 130	. . . 4 (((d ∪ (b →₁c)) →₁c) ∩ c) ≤ (d ∪ (b →₁c))
45	16, 44	letr 129	. . 3 ((d ∪ (a →₁c)) ∩ c) ≤ (d ∪ (b →₁c))
46	9, 45	lel2or 162	. 2 (((d ∪ (a →₁c)) →₁c)^⊥ ∪ ((d ∪ (a →₁c)) ∩ c)) ≤ (d ∪ (b →₁c))
47	2, 46	bltr 130	1 (d ∪ (a →₁c)) ≤ (d ∪ (b →₁c))

Colors of variables: term

Syntax hints: = wb 1 ≤ wle 2 ^⊥ wn 4 ∪ wo 6 ∩ wa 7 →₁wi1 13

This theorem is referenced by: cancel 874

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