Quantum Logic Explorer

Quantum Logic Explorer

< Previous Next >
Related theorems
GIF version

Theorem lem4 493

Description: Lemma 4 of Kalmbach p. 240.

**Assertion**
Ref	Expression
lem4	(a →₃(a →₃b)) = (a^⊥ ∪ b)

**Proof of Theorem lem4**
Step	Hyp	Ref	Expression
1		df-i3 45	. 2 (a →₃(a →₃b)) = (((a^⊥ ∩ (a →₃b)) ∪ (a^⊥ ∩ (a →₃b)^⊥ )) ∪ (a ∩ (a^⊥ ∪ (a →₃b))))
2		df-i3 45	. . . . . . . 8 (a →₃b) = (((a^⊥ ∩ b) ∪ (a^⊥ ∩ b^⊥ )) ∪ (a ∩ (a^⊥ ∪ b)))
3	2	lan 70	. . . . . . 7 (a^⊥ ∩ (a →₃b)) = (a^⊥ ∩ (((a^⊥ ∩ b) ∪ (a^⊥ ∩ b^⊥ )) ∪ (a ∩ (a^⊥ ∪ b))))
4		lea 152	. . . . . . . . . . . . 13 (a^⊥ ∩ b) ≤ a^⊥
5		lea 152	. . . . . . . . . . . . 13 (a^⊥ ∩ b^⊥ ) ≤ a^⊥
6	4, 5	le2or 160	. . . . . . . . . . . 12 ((a^⊥ ∩ b) ∪ (a^⊥ ∩ b^⊥ )) ≤ (a^⊥ ∪ a^⊥ )
7		oridm 102	. . . . . . . . . . . 12 (a^⊥ ∪ a^⊥ ) = a^⊥
8	6, 7	lbtr 131	. . . . . . . . . . 11 ((a^⊥ ∩ b) ∪ (a^⊥ ∩ b^⊥ )) ≤ a^⊥
9	8	lecom 172	. . . . . . . . . 10 ((a^⊥ ∩ b) ∪ (a^⊥ ∩ b^⊥ )) C a^⊥
10	9	comcom 435	. . . . . . . . 9 a^⊥ C ((a^⊥ ∩ b) ∪ (a^⊥ ∩ b^⊥ ))
11		lea 152	. . . . . . . . . . . 12 (a ∩ (a^⊥ ∪ b)) ≤ a
12	11	lecom 172	. . . . . . . . . . 11 (a ∩ (a^⊥ ∪ b)) C a
13	12	comcom 435	. . . . . . . . . 10 a C (a ∩ (a^⊥ ∪ b))
14	13	comcom3 436	. . . . . . . . 9 a^⊥ C (a ∩ (a^⊥ ∪ b))
15	10, 14	fh1 451	. . . . . . . 8 (a^⊥ ∩ (((a^⊥ ∩ b) ∪ (a^⊥ ∩ b^⊥ )) ∪ (a ∩ (a^⊥ ∪ b)))) = ((a^⊥ ∩ ((a^⊥ ∩ b) ∪ (a^⊥ ∩ b^⊥ ))) ∪ (a^⊥ ∩ (a ∩ (a^⊥ ∪ b))))
16		ancom 68	. . . . . . . . . . 11 ((a^⊥ ∩ a) ∩ (a^⊥ ∪ b)) = ((a^⊥ ∪ b) ∩ (a^⊥ ∩ a))
17		anass 69	. . . . . . . . . . 11 ((a^⊥ ∩ a) ∩ (a^⊥ ∪ b)) = (a^⊥ ∩ (a ∩ (a^⊥ ∪ b)))
18		dff 93	. . . . . . . . . . . . . . 15 0 = (a ∩ a^⊥ )
19		ancom 68	. . . . . . . . . . . . . . 15 (a ∩ a^⊥ ) = (a^⊥ ∩ a)
20	18, 19	ax-r2 35	. . . . . . . . . . . . . 14 0 = (a^⊥ ∩ a)
21	20	lan 70	. . . . . . . . . . . . 13 ((a^⊥ ∪ b) ∩ 0) = ((a^⊥ ∪ b) ∩ (a^⊥ ∩ a))
22	21	ax-r1 34	. . . . . . . . . . . 12 ((a^⊥ ∪ b) ∩ (a^⊥ ∩ a)) = ((a^⊥ ∪ b) ∩ 0)
23		an0 100	. . . . . . . . . . . 12 ((a^⊥ ∪ b) ∩ 0) = 0
24	22, 23	ax-r2 35	. . . . . . . . . . 11 ((a^⊥ ∪ b) ∩ (a^⊥ ∩ a)) = 0
25	16, 17, 24	3tr2 61	. . . . . . . . . 10 (a^⊥ ∩ (a ∩ (a^⊥ ∪ b))) = 0
26	25	lor 66	. . . . . . . . 9 ((a^⊥ ∩ ((a^⊥ ∩ b) ∪ (a^⊥ ∩ b^⊥ ))) ∪ (a^⊥ ∩ (a ∩ (a^⊥ ∪ b)))) = ((a^⊥ ∩ ((a^⊥ ∩ b) ∪ (a^⊥ ∩ b^⊥ ))) ∪ 0)
27		or0 94	. . . . . . . . . 10 ((a^⊥ ∩ ((a^⊥ ∩ b) ∪ (a^⊥ ∩ b^⊥ ))) ∪ 0) = (a^⊥ ∩ ((a^⊥ ∩ b) ∪ (a^⊥ ∩ b^⊥ )))
28		ancom 68	. . . . . . . . . . 11 (a^⊥ ∩ ((a^⊥ ∩ b) ∪ (a^⊥ ∩ b^⊥ ))) = (((a^⊥ ∩ b) ∪ (a^⊥ ∩ b^⊥ )) ∩ a^⊥ )
29	8	df2le2 128	. . . . . . . . . . 11 (((a^⊥ ∩ b) ∪ (a^⊥ ∩ b^⊥ )) ∩ a^⊥ ) = ((a^⊥ ∩ b) ∪ (a^⊥ ∩ b^⊥ ))
30	28, 29	ax-r2 35	. . . . . . . . . 10 (a^⊥ ∩ ((a^⊥ ∩ b) ∪ (a^⊥ ∩ b^⊥ ))) = ((a^⊥ ∩ b) ∪ (a^⊥ ∩ b^⊥ ))
31	27, 30	ax-r2 35	. . . . . . . . 9 ((a^⊥ ∩ ((a^⊥ ∩ b) ∪ (a^⊥ ∩ b^⊥ ))) ∪ 0) = ((a^⊥ ∩ b) ∪ (a^⊥ ∩ b^⊥ ))
32	26, 31	ax-r2 35	. . . . . . . 8 ((a^⊥ ∩ ((a^⊥ ∩ b) ∪ (a^⊥ ∩ b^⊥ ))) ∪ (a^⊥ ∩ (a ∩ (a^⊥ ∪ b)))) = ((a^⊥ ∩ b) ∪ (a^⊥ ∩ b^⊥ ))
33	15, 32	ax-r2 35	. . . . . . 7 (a^⊥ ∩ (((a^⊥ ∩ b) ∪ (a^⊥ ∩ b^⊥ )) ∪ (a ∩ (a^⊥ ∪ b)))) = ((a^⊥ ∩ b) ∪ (a^⊥ ∩ b^⊥ ))
34	3, 33	ax-r2 35	. . . . . 6 (a^⊥ ∩ (a →₃b)) = ((a^⊥ ∩ b) ∪ (a^⊥ ∩ b^⊥ ))
35	2	lor 66	. . . . . . . . 9 (a ∪ (a →₃b)) = (a ∪ (((a^⊥ ∩ b) ∪ (a^⊥ ∩ b^⊥ )) ∪ (a ∩ (a^⊥ ∪ b))))
36		orordi 104	. . . . . . . . . 10 (a ∪ (((a^⊥ ∩ b) ∪ (a^⊥ ∩ b^⊥ )) ∪ (a ∩ (a^⊥ ∪ b)))) = ((a ∪ ((a^⊥ ∩ b) ∪ (a^⊥ ∩ b^⊥ ))) ∪ (a ∪ (a ∩ (a^⊥ ∪ b))))
37		a5b 112	. . . . . . . . . . . 12 (a ∪ (a ∩ (a^⊥ ∪ b))) = a
38	37	lor 66	. . . . . . . . . . 11 ((a ∪ ((a^⊥ ∩ b) ∪ (a^⊥ ∩ b^⊥ ))) ∪ (a ∪ (a ∩ (a^⊥ ∪ b)))) = ((a ∪ ((a^⊥ ∩ b) ∪ (a^⊥ ∩ b^⊥ ))) ∪ a)
39		or32 75	. . . . . . . . . . . 12 ((a ∪ ((a^⊥ ∩ b) ∪ (a^⊥ ∩ b^⊥ ))) ∪ a) = ((a ∪ a) ∪ ((a^⊥ ∩ b) ∪ (a^⊥ ∩ b^⊥ )))
40		oridm 102	. . . . . . . . . . . . 13 (a ∪ a) = a
41	40	ax-r5 37	. . . . . . . . . . . 12 ((a ∪ a) ∪ ((a^⊥ ∩ b) ∪ (a^⊥ ∩ b^⊥ ))) = (a ∪ ((a^⊥ ∩ b) ∪ (a^⊥ ∩ b^⊥ )))
42	39, 41	ax-r2 35	. . . . . . . . . . 11 ((a ∪ ((a^⊥ ∩ b) ∪ (a^⊥ ∩ b^⊥ ))) ∪ a) = (a ∪ ((a^⊥ ∩ b) ∪ (a^⊥ ∩ b^⊥ )))
43	38, 42	ax-r2 35	. . . . . . . . . 10 ((a ∪ ((a^⊥ ∩ b) ∪ (a^⊥ ∩ b^⊥ ))) ∪ (a ∪ (a ∩ (a^⊥ ∪ b)))) = (a ∪ ((a^⊥ ∩ b) ∪ (a^⊥ ∩ b^⊥ )))
44	36, 43	ax-r2 35	. . . . . . . . 9 (a ∪ (((a^⊥ ∩ b) ∪ (a^⊥ ∩ b^⊥ )) ∪ (a ∩ (a^⊥ ∪ b)))) = (a ∪ ((a^⊥ ∩ b) ∪ (a^⊥ ∩ b^⊥ )))
45	35, 44	ax-r2 35	. . . . . . . 8 (a ∪ (a →₃b)) = (a ∪ ((a^⊥ ∩ b) ∪ (a^⊥ ∩ b^⊥ )))
46	45	ax-r4 36	. . . . . . 7 (a ∪ (a →₃b))^⊥ = (a ∪ ((a^⊥ ∩ b) ∪ (a^⊥ ∩ b^⊥ )))^⊥
47		oran 79	. . . . . . . 8 (a ∪ (a →₃b)) = (a^⊥ ∩ (a →₃b)^⊥ )^⊥
48	47	con2 64	. . . . . . 7 (a ∪ (a →₃b))^⊥ = (a^⊥ ∩ (a →₃b)^⊥ )
49		oran 79	. . . . . . . . 9 (a ∪ ((a^⊥ ∩ b) ∪ (a^⊥ ∩ b^⊥ ))) = (a^⊥ ∩ ((a^⊥ ∩ b) ∪ (a^⊥ ∩ b^⊥ ))^⊥ )^⊥
50	49	con2 64	. . . . . . . 8 (a ∪ ((a^⊥ ∩ b) ∪ (a^⊥ ∩ b^⊥ )))^⊥ = (a^⊥ ∩ ((a^⊥ ∩ b) ∪ (a^⊥ ∩ b^⊥ ))^⊥ )
51		ancom 68	. . . . . . . 8 (a^⊥ ∩ ((a^⊥ ∩ b) ∪ (a^⊥ ∩ b^⊥ ))^⊥ ) = (((a^⊥ ∩ b) ∪ (a^⊥ ∩ b^⊥ ))^⊥ ∩ a^⊥ )
52	50, 51	ax-r2 35	. . . . . . 7 (a ∪ ((a^⊥ ∩ b) ∪ (a^⊥ ∩ b^⊥ )))^⊥ = (((a^⊥ ∩ b) ∪ (a^⊥ ∩ b^⊥ ))^⊥ ∩ a^⊥ )
53	46, 48, 52	3tr2 61	. . . . . 6 (a^⊥ ∩ (a →₃b)^⊥ ) = (((a^⊥ ∩ b) ∪ (a^⊥ ∩ b^⊥ ))^⊥ ∩ a^⊥ )
54	34, 53	2or 67	. . . . 5 ((a^⊥ ∩ (a →₃b)) ∪ (a^⊥ ∩ (a →₃b)^⊥ )) = (((a^⊥ ∩ b) ∪ (a^⊥ ∩ b^⊥ )) ∪ (((a^⊥ ∩ b) ∪ (a^⊥ ∩ b^⊥ ))^⊥ ∩ a^⊥ ))
55	8	oml2 433	. . . . 5 (((a^⊥ ∩ b) ∪ (a^⊥ ∩ b^⊥ )) ∪ (((a^⊥ ∩ b) ∪ (a^⊥ ∩ b^⊥ ))^⊥ ∩ a^⊥ )) = a^⊥
56	54, 55	ax-r2 35	. . . 4 ((a^⊥ ∩ (a →₃b)) ∪ (a^⊥ ∩ (a →₃b)^⊥ )) = a^⊥
57	2	lor 66	. . . . . . 7 (a^⊥ ∪ (a →₃b)) = (a^⊥ ∪ (((a^⊥ ∩ b) ∪ (a^⊥ ∩ b^⊥ )) ∪ (a ∩ (a^⊥ ∪ b))))
58		ax-a3 31	. . . . . . . . 9 ((a^⊥ ∪ ((a^⊥ ∩ b) ∪ (a^⊥ ∩ b^⊥ ))) ∪ (a ∩ (a^⊥ ∪ b))) = (a^⊥ ∪ (((a^⊥ ∩ b) ∪ (a^⊥ ∩ b^⊥ )) ∪ (a ∩ (a^⊥ ∪ b))))
59	58	ax-r1 34	. . . . . . . 8 (a^⊥ ∪ (((a^⊥ ∩ b) ∪ (a^⊥ ∩ b^⊥ )) ∪ (a ∩ (a^⊥ ∪ b)))) = ((a^⊥ ∪ ((a^⊥ ∩ b) ∪ (a^⊥ ∩ b^⊥ ))) ∪ (a ∩ (a^⊥ ∪ b)))
60		orordi 104	. . . . . . . . . 10 (a^⊥ ∪ ((a^⊥ ∩ b) ∪ (a^⊥ ∩ b^⊥ ))) = ((a^⊥ ∪ (a^⊥ ∩ b)) ∪ (a^⊥ ∪ (a^⊥ ∩ b^⊥ )))
61		a5b 112	. . . . . . . . . . . 12 (a^⊥ ∪ (a^⊥ ∩ b)) = a^⊥
62		a5b 112	. . . . . . . . . . . 12 (a^⊥ ∪ (a^⊥ ∩ b^⊥ )) = a^⊥
63	61, 62	2or 67	. . . . . . . . . . 11 ((a^⊥ ∪ (a^⊥ ∩ b)) ∪ (a^⊥ ∪ (a^⊥ ∩ b^⊥ ))) = (a^⊥ ∪ a^⊥ )
64	63, 7	ax-r2 35	. . . . . . . . . 10 ((a^⊥ ∪ (a^⊥ ∩ b)) ∪ (a^⊥ ∪ (a^⊥ ∩ b^⊥ ))) = a^⊥
65	60, 64	ax-r2 35	. . . . . . . . 9 (a^⊥ ∪ ((a^⊥ ∩ b) ∪ (a^⊥ ∩ b^⊥ ))) = a^⊥
66	65	ax-r5 37	. . . . . . . 8 ((a^⊥ ∪ ((a^⊥ ∩ b) ∪ (a^⊥ ∩ b^⊥ ))) ∪ (a ∩ (a^⊥ ∪ b))) = (a^⊥ ∪ (a ∩ (a^⊥ ∪ b)))
67	59, 66	ax-r2 35	. . . . . . 7 (a^⊥ ∪ (((a^⊥ ∩ b) ∪ (a^⊥ ∩ b^⊥ )) ∪ (a ∩ (a^⊥ ∪ b)))) = (a^⊥ ∪ (a ∩ (a^⊥ ∪ b)))
68	57, 67	ax-r2 35	. . . . . 6 (a^⊥ ∪ (a →₃b)) = (a^⊥ ∪ (a ∩ (a^⊥ ∪ b)))
69		omln 428	. . . . . 6 (a^⊥ ∪ (a ∩ (a^⊥ ∪ b))) = (a^⊥ ∪ b)
70	68, 69	ax-r2 35	. . . . 5 (a^⊥ ∪ (a →₃b)) = (a^⊥ ∪ b)
71	70	lan 70	. . . 4 (a ∩ (a^⊥ ∪ (a →₃b))) = (a ∩ (a^⊥ ∪ b))
72	56, 71	2or 67	. . 3 (((a^⊥ ∩ (a →₃b)) ∪ (a^⊥ ∩ (a →₃b)^⊥ )) ∪ (a ∩ (a^⊥ ∪ (a →₃b)))) = (a^⊥ ∪ (a ∩ (a^⊥ ∪ b)))
73	72, 69	ax-r2 35	. 2 (((a^⊥ ∩ (a →₃b)) ∪ (a^⊥ ∩ (a →₃b)^⊥ )) ∪ (a ∩ (a^⊥ ∪ (a →₃b)))) = (a^⊥ ∪ b)
74	1, 73	ax-r2 35	1 (a →₃(a →₃b)) = (a^⊥ ∪ b)

Colors of variables: term

Syntax hints: = wb 1 ^⊥ wn 4 ∪ wo 6 ∩ wa 7 0wf 10 →₃wi3 15

This theorem is referenced by: i0i3 494 i3i0 495 ska14 496 i3abs1 504 i3abs3 506 i3th1 525 i3th2 526 i3th3 527 i3th5 529 i3th7 531 i3th8 532 u3lem4 740 u3lem12 770 u3lemax4 778 u3lemax5 779

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

metamath.org