Quantum Logic Explorer

Quantum Logic Explorer

< Previous Next >
Related theorems
GIF version

Theorem ud5lem3 576

Description: Lemma for unified disjunction.

**Assertion**
Ref	Expression
ud5lem3	((a →₅b) →₅(a ∪ (a^⊥ ∩ b))) = (a ∪ b)

**Proof of Theorem ud5lem3**
Step	Hyp	Ref	Expression
1		df-i5 47	. 2 ((a →₅b) →₅(a ∪ (a^⊥ ∩ b))) = ((((a →₅b) ∩ (a ∪ (a^⊥ ∩ b))) ∪ ((a →₅b)^⊥ ∩ (a ∪ (a^⊥ ∩ b)))) ∪ ((a →₅b)^⊥ ∩ (a ∪ (a^⊥ ∩ b))^⊥ ))
2		ud5lem3a 573	. . . . 5 ((a →₅b) ∩ (a ∪ (a^⊥ ∩ b))) = ((a ∩ b) ∪ (a^⊥ ∩ b))
3		ud5lem3b 574	. . . . 5 ((a →₅b)^⊥ ∩ (a ∪ (a^⊥ ∩ b))) = (a ∩ (a^⊥ ∪ b^⊥ ))
4	2, 3	2or 67	. . . 4 (((a →₅b) ∩ (a ∪ (a^⊥ ∩ b))) ∪ ((a →₅b)^⊥ ∩ (a ∪ (a^⊥ ∩ b)))) = (((a ∩ b) ∪ (a^⊥ ∩ b)) ∪ (a ∩ (a^⊥ ∪ b^⊥ )))
5		ud5lem3c 575	. . . 4 ((a →₅b)^⊥ ∩ (a ∪ (a^⊥ ∩ b))^⊥ ) = (((a ∪ b) ∩ (a ∪ b^⊥ )) ∩ a^⊥ )
6	4, 5	2or 67	. . 3 ((((a →₅b) ∩ (a ∪ (a^⊥ ∩ b))) ∪ ((a →₅b)^⊥ ∩ (a ∪ (a^⊥ ∩ b)))) ∪ ((a →₅b)^⊥ ∩ (a ∪ (a^⊥ ∩ b))^⊥ )) = ((((a ∩ b) ∪ (a^⊥ ∩ b)) ∪ (a ∩ (a^⊥ ∪ b^⊥ ))) ∪ (((a ∪ b) ∩ (a ∪ b^⊥ )) ∩ a^⊥ ))
7		ax-a3 31	. . . 4 ((((a ∩ b) ∪ (a^⊥ ∩ b)) ∪ (a ∩ (a^⊥ ∪ b^⊥ ))) ∪ (((a ∪ b) ∩ (a ∪ b^⊥ )) ∩ a^⊥ )) = (((a ∩ b) ∪ (a^⊥ ∩ b)) ∪ ((a ∩ (a^⊥ ∪ b^⊥ )) ∪ (((a ∪ b) ∩ (a ∪ b^⊥ )) ∩ a^⊥ )))
8		or4 77	. . . . 5 (((a ∩ b) ∪ (a^⊥ ∩ b)) ∪ ((a ∩ (a^⊥ ∪ b^⊥ )) ∪ (((a ∪ b) ∩ (a ∪ b^⊥ )) ∩ a^⊥ ))) = (((a ∩ b) ∪ (a ∩ (a^⊥ ∪ b^⊥ ))) ∪ ((a^⊥ ∩ b) ∪ (((a ∪ b) ∩ (a ∪ b^⊥ )) ∩ a^⊥ )))
9		comanr1 446	. . . . . . . . 9 a C (a ∩ b)
10		comorr 176	. . . . . . . . . 10 a^⊥ C (a^⊥ ∪ b^⊥ )
11	10	comcom6 441	. . . . . . . . 9 a C (a^⊥ ∪ b^⊥ )
12	9, 11	fh4 454	. . . . . . . 8 ((a ∩ b) ∪ (a ∩ (a^⊥ ∪ b^⊥ ))) = (((a ∩ b) ∪ a) ∩ ((a ∩ b) ∪ (a^⊥ ∪ b^⊥ )))
13		ax-a2 30	. . . . . . . . . . 11 ((a ∩ b) ∪ a) = (a ∪ (a ∩ b))
14		a5b 112	. . . . . . . . . . 11 (a ∪ (a ∩ b)) = a
15	13, 14	ax-r2 35	. . . . . . . . . 10 ((a ∩ b) ∪ a) = a
16		df-a 39	. . . . . . . . . . . . . 14 (a ∩ b) = (a^⊥ ∪ b^⊥ )^⊥
17	16	ax-r1 34	. . . . . . . . . . . . 13 (a^⊥ ∪ b^⊥ )^⊥ = (a ∩ b)
18	17	con3 65	. . . . . . . . . . . 12 (a^⊥ ∪ b^⊥ ) = (a ∩ b)^⊥
19	18	lor 66	. . . . . . . . . . 11 ((a ∩ b) ∪ (a^⊥ ∪ b^⊥ )) = ((a ∩ b) ∪ (a ∩ b)^⊥ )
20		df-t 40	. . . . . . . . . . . 12 1 = ((a ∩ b) ∪ (a ∩ b)^⊥ )
21	20	ax-r1 34	. . . . . . . . . . 11 ((a ∩ b) ∪ (a ∩ b)^⊥ ) = 1
22	19, 21	ax-r2 35	. . . . . . . . . 10 ((a ∩ b) ∪ (a^⊥ ∪ b^⊥ )) = 1
23	15, 22	2an 72	. . . . . . . . 9 (((a ∩ b) ∪ a) ∩ ((a ∩ b) ∪ (a^⊥ ∪ b^⊥ ))) = (a ∩ 1)
24		an1 98	. . . . . . . . 9 (a ∩ 1) = a
25	23, 24	ax-r2 35	. . . . . . . 8 (((a ∩ b) ∪ a) ∩ ((a ∩ b) ∪ (a^⊥ ∪ b^⊥ ))) = a
26	12, 25	ax-r2 35	. . . . . . 7 ((a ∩ b) ∪ (a ∩ (a^⊥ ∪ b^⊥ ))) = a
27		coman1 177	. . . . . . . . . . . 12 (a^⊥ ∩ b) C a^⊥
28	27	comcom7 442	. . . . . . . . . . 11 (a^⊥ ∩ b) C a
29		coman2 178	. . . . . . . . . . 11 (a^⊥ ∩ b) C b
30	28, 29	com2or 465	. . . . . . . . . 10 (a^⊥ ∩ b) C (a ∪ b)
31	29	comcom2 175	. . . . . . . . . . 11 (a^⊥ ∩ b) C b^⊥
32	28, 31	com2or 465	. . . . . . . . . 10 (a^⊥ ∩ b) C (a ∪ b^⊥ )
33	30, 32	com2an 466	. . . . . . . . 9 (a^⊥ ∩ b) C ((a ∪ b) ∩ (a ∪ b^⊥ ))
34	33, 27	fh3 453	. . . . . . . 8 ((a^⊥ ∩ b) ∪ (((a ∪ b) ∩ (a ∪ b^⊥ )) ∩ a^⊥ )) = (((a^⊥ ∩ b) ∪ ((a ∪ b) ∩ (a ∪ b^⊥ ))) ∩ ((a^⊥ ∩ b) ∪ a^⊥ ))
35		comor1 443	. . . . . . . . . . . . . 14 (a ∪ b) C a
36	35	comcom2 175	. . . . . . . . . . . . 13 (a ∪ b) C a^⊥
37		comor2 444	. . . . . . . . . . . . 13 (a ∪ b) C b
38	36, 37	com2an 466	. . . . . . . . . . . 12 (a ∪ b) C (a^⊥ ∩ b)
39	37	comcom2 175	. . . . . . . . . . . . 13 (a ∪ b) C b^⊥
40	35, 39	com2or 465	. . . . . . . . . . . 12 (a ∪ b) C (a ∪ b^⊥ )
41	38, 40	fh4 454	. . . . . . . . . . 11 ((a^⊥ ∩ b) ∪ ((a ∪ b) ∩ (a ∪ b^⊥ ))) = (((a^⊥ ∩ b) ∪ (a ∪ b)) ∩ ((a^⊥ ∩ b) ∪ (a ∪ b^⊥ )))
42	36, 37	fh3r 457	. . . . . . . . . . . . . 14 ((a^⊥ ∩ b) ∪ (a ∪ b)) = ((a^⊥ ∪ (a ∪ b)) ∩ (b ∪ (a ∪ b)))
43		ax-a2 30	. . . . . . . . . . . . . . . 16 (a^⊥ ∪ (a ∪ b)) = ((a ∪ b) ∪ a^⊥ )
44		or12 73	. . . . . . . . . . . . . . . . 17 (b ∪ (a ∪ b)) = (a ∪ (b ∪ b))
45		oridm 102	. . . . . . . . . . . . . . . . . 18 (b ∪ b) = b
46	45	lor 66	. . . . . . . . . . . . . . . . 17 (a ∪ (b ∪ b)) = (a ∪ b)
47	44, 46	ax-r2 35	. . . . . . . . . . . . . . . 16 (b ∪ (a ∪ b)) = (a ∪ b)
48	43, 47	2an 72	. . . . . . . . . . . . . . 15 ((a^⊥ ∪ (a ∪ b)) ∩ (b ∪ (a ∪ b))) = (((a ∪ b) ∪ a^⊥ ) ∩ (a ∪ b))
49		ancom 68	. . . . . . . . . . . . . . . 16 (((a ∪ b) ∪ a^⊥ ) ∩ (a ∪ b)) = ((a ∪ b) ∩ ((a ∪ b) ∪ a^⊥ ))
50		a5c 113	. . . . . . . . . . . . . . . 16 ((a ∪ b) ∩ ((a ∪ b) ∪ a^⊥ )) = (a ∪ b)
51	49, 50	ax-r2 35	. . . . . . . . . . . . . . 15 (((a ∪ b) ∪ a^⊥ ) ∩ (a ∪ b)) = (a ∪ b)
52	48, 51	ax-r2 35	. . . . . . . . . . . . . 14 ((a^⊥ ∪ (a ∪ b)) ∩ (b ∪ (a ∪ b))) = (a ∪ b)
53	42, 52	ax-r2 35	. . . . . . . . . . . . 13 ((a^⊥ ∩ b) ∪ (a ∪ b)) = (a ∪ b)
54		anor2 81	. . . . . . . . . . . . . . . . 17 (a^⊥ ∩ b) = (a ∪ b^⊥ )^⊥
55	54	ax-r1 34	. . . . . . . . . . . . . . . 16 (a ∪ b^⊥ )^⊥ = (a^⊥ ∩ b)
56	55	con3 65	. . . . . . . . . . . . . . 15 (a ∪ b^⊥ ) = (a^⊥ ∩ b)^⊥
57	56	lor 66	. . . . . . . . . . . . . 14 ((a^⊥ ∩ b) ∪ (a ∪ b^⊥ )) = ((a^⊥ ∩ b) ∪ (a^⊥ ∩ b)^⊥ )
58		df-t 40	. . . . . . . . . . . . . . 15 1 = ((a^⊥ ∩ b) ∪ (a^⊥ ∩ b)^⊥ )
59	58	ax-r1 34	. . . . . . . . . . . . . 14 ((a^⊥ ∩ b) ∪ (a^⊥ ∩ b)^⊥ ) = 1
60	57, 59	ax-r2 35	. . . . . . . . . . . . 13 ((a^⊥ ∩ b) ∪ (a ∪ b^⊥ )) = 1
61	53, 60	2an 72	. . . . . . . . . . . 12 (((a^⊥ ∩ b) ∪ (a ∪ b)) ∩ ((a^⊥ ∩ b) ∪ (a ∪ b^⊥ ))) = ((a ∪ b) ∩ 1)
62		an1 98	. . . . . . . . . . . 12 ((a ∪ b) ∩ 1) = (a ∪ b)
63	61, 62	ax-r2 35	. . . . . . . . . . 11 (((a^⊥ ∩ b) ∪ (a ∪ b)) ∩ ((a^⊥ ∩ b) ∪ (a ∪ b^⊥ ))) = (a ∪ b)
64	41, 63	ax-r2 35	. . . . . . . . . 10 ((a^⊥ ∩ b) ∪ ((a ∪ b) ∩ (a ∪ b^⊥ ))) = (a ∪ b)
65		ax-a2 30	. . . . . . . . . . 11 ((a^⊥ ∩ b) ∪ a^⊥ ) = (a^⊥ ∪ (a^⊥ ∩ b))
66		a5b 112	. . . . . . . . . . 11 (a^⊥ ∪ (a^⊥ ∩ b)) = a^⊥
67	65, 66	ax-r2 35	. . . . . . . . . 10 ((a^⊥ ∩ b) ∪ a^⊥ ) = a^⊥
68	64, 67	2an 72	. . . . . . . . 9 (((a^⊥ ∩ b) ∪ ((a ∪ b) ∩ (a ∪ b^⊥ ))) ∩ ((a^⊥ ∩ b) ∪ a^⊥ )) = ((a ∪ b) ∩ a^⊥ )
69		ancom 68	. . . . . . . . 9 ((a ∪ b) ∩ a^⊥ ) = (a^⊥ ∩ (a ∪ b))
70	68, 69	ax-r2 35	. . . . . . . 8 (((a^⊥ ∩ b) ∪ ((a ∪ b) ∩ (a ∪ b^⊥ ))) ∩ ((a^⊥ ∩ b) ∪ a^⊥ )) = (a^⊥ ∩ (a ∪ b))
71	34, 70	ax-r2 35	. . . . . . 7 ((a^⊥ ∩ b) ∪ (((a ∪ b) ∩ (a ∪ b^⊥ )) ∩ a^⊥ )) = (a^⊥ ∩ (a ∪ b))
72	26, 71	2or 67	. . . . . 6 (((a ∩ b) ∪ (a ∩ (a^⊥ ∪ b^⊥ ))) ∪ ((a^⊥ ∩ b) ∪ (((a ∪ b) ∩ (a ∪ b^⊥ )) ∩ a^⊥ ))) = (a ∪ (a^⊥ ∩ (a ∪ b)))
73		oml 427	. . . . . 6 (a ∪ (a^⊥ ∩ (a ∪ b))) = (a ∪ b)
74	72, 73	ax-r2 35	. . . . 5 (((a ∩ b) ∪ (a ∩ (a^⊥ ∪ b^⊥ ))) ∪ ((a^⊥ ∩ b) ∪ (((a ∪ b) ∩ (a ∪ b^⊥ )) ∩ a^⊥ ))) = (a ∪ b)
75	8, 74	ax-r2 35	. . . 4 (((a ∩ b) ∪ (a^⊥ ∩ b)) ∪ ((a ∩ (a^⊥ ∪ b^⊥ )) ∪ (((a ∪ b) ∩ (a ∪ b^⊥ )) ∩ a^⊥ ))) = (a ∪ b)
76	7, 75	ax-r2 35	. . 3 ((((a ∩ b) ∪ (a^⊥ ∩ b)) ∪ (a ∩ (a^⊥ ∪ b^⊥ ))) ∪ (((a ∪ b) ∩ (a ∪ b^⊥ )) ∩ a^⊥ )) = (a ∪ b)
77	6, 76	ax-r2 35	. 2 ((((a →₅b) ∩ (a ∪ (a^⊥ ∩ b))) ∪ ((a →₅b)^⊥ ∩ (a ∪ (a^⊥ ∩ b)))) ∪ ((a →₅b)^⊥ ∩ (a ∪ (a^⊥ ∩ b))^⊥ )) = (a ∪ b)
78	1, 77	ax-r2 35	1 ((a →₅b) →₅(a ∪ (a^⊥ ∩ b))) = (a ∪ b)

Colors of variables: term

Syntax hints: = wb 1 ^⊥ wn 4 ∪ wo 6 ∩ wa 7 1wt 9 →₅wi5 17

This theorem is referenced by: ud5 581

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

metamath.org