Quantum Logic Explorer

Quantum Logic Explorer

< Previous Next >
Related theorems
GIF version

Theorem u24lem 752

Description: Lemma for unified implication study.

**Assertion**
Ref	Expression
u24lem	((a →₂b) ∩ (a →₄b)) = (a →₅b)

**Proof of Theorem u24lem**
Step	Hyp	Ref	Expression
1		df-i2 44	. . 3 (a →₂b) = (b ∪ (a^⊥ ∩ b^⊥ ))
2	1	ran 71	. 2 ((a →₂b) ∩ (a →₄b)) = ((b ∪ (a^⊥ ∩ b^⊥ )) ∩ (a →₄b))
3		u4lemc1 665	. . . 4 b C (a →₄b)
4		comanr2 447	. . . . 5 b^⊥ C (a^⊥ ∩ b^⊥ )
5	4	comcom6 441	. . . 4 b C (a^⊥ ∩ b^⊥ )
6	3, 5	fh2r 456	. . 3 ((b ∪ (a^⊥ ∩ b^⊥ )) ∩ (a →₄b)) = ((b ∩ (a →₄b)) ∪ ((a^⊥ ∩ b^⊥ ) ∩ (a →₄b)))
7		ancom 68	. . . . . 6 (b ∩ (a →₄b)) = ((a →₄b) ∩ b)
8		ancom 68	. . . . . 6 ((a →₄b) ∩ b) = (b ∩ (a →₄b))
9	7, 8	ax-r2 35	. . . . 5 (b ∩ (a →₄b)) = (b ∩ (a →₄b))
10		anass 69	. . . . . 6 ((a^⊥ ∩ b^⊥ ) ∩ (a →₄b)) = (a^⊥ ∩ (b^⊥ ∩ (a →₄b)))
11		ancom 68	. . . . . . . . 9 (b^⊥ ∩ (a →₄b)) = ((a →₄b) ∩ b^⊥ )
12		u4lemanb 600	. . . . . . . . 9 ((a →₄b) ∩ b^⊥ ) = ((a^⊥ ∪ b) ∩ b^⊥ )
13	11, 12	ax-r2 35	. . . . . . . 8 (b^⊥ ∩ (a →₄b)) = ((a^⊥ ∪ b) ∩ b^⊥ )
14	13	lan 70	. . . . . . 7 (a^⊥ ∩ (b^⊥ ∩ (a →₄b))) = (a^⊥ ∩ ((a^⊥ ∪ b) ∩ b^⊥ ))
15		anass 69	. . . . . . . . 9 ((a^⊥ ∩ (a^⊥ ∪ b)) ∩ b^⊥ ) = (a^⊥ ∩ ((a^⊥ ∪ b) ∩ b^⊥ ))
16	15	ax-r1 34	. . . . . . . 8 (a^⊥ ∩ ((a^⊥ ∪ b) ∩ b^⊥ )) = ((a^⊥ ∩ (a^⊥ ∪ b)) ∩ b^⊥ )
17		a5c 113	. . . . . . . . . 10 (a^⊥ ∩ (a^⊥ ∪ b)) = a^⊥
18	17	ran 71	. . . . . . . . 9 ((a^⊥ ∩ (a^⊥ ∪ b)) ∩ b^⊥ ) = (a^⊥ ∩ b^⊥ )
19		ancom 68	. . . . . . . . 9 (a^⊥ ∩ b^⊥ ) = (b^⊥ ∩ a^⊥ )
20	18, 19	ax-r2 35	. . . . . . . 8 ((a^⊥ ∩ (a^⊥ ∪ b)) ∩ b^⊥ ) = (b^⊥ ∩ a^⊥ )
21	16, 20	ax-r2 35	. . . . . . 7 (a^⊥ ∩ ((a^⊥ ∪ b) ∩ b^⊥ )) = (b^⊥ ∩ a^⊥ )
22	14, 21	ax-r2 35	. . . . . 6 (a^⊥ ∩ (b^⊥ ∩ (a →₄b))) = (b^⊥ ∩ a^⊥ )
23	10, 22	ax-r2 35	. . . . 5 ((a^⊥ ∩ b^⊥ ) ∩ (a →₄b)) = (b^⊥ ∩ a^⊥ )
24	9, 23	2or 67	. . . 4 ((b ∩ (a →₄b)) ∪ ((a^⊥ ∩ b^⊥ ) ∩ (a →₄b))) = ((b ∩ (a →₄b)) ∪ (b^⊥ ∩ a^⊥ ))
25		comanr1 446	. . . . . . 7 b^⊥ C (b^⊥ ∩ a^⊥ )
26	25	comcom6 441	. . . . . 6 b C (b^⊥ ∩ a^⊥ )
27	26, 3	fh4r 458	. . . . 5 ((b ∩ (a →₄b)) ∪ (b^⊥ ∩ a^⊥ )) = ((b ∪ (b^⊥ ∩ a^⊥ )) ∩ ((a →₄b) ∪ (b^⊥ ∩ a^⊥ )))
28	3, 26	com2or 465	. . . . . . 7 b C ((a →₄b) ∪ (b^⊥ ∩ a^⊥ ))
29	28, 26	fh2r 456	. . . . . 6 ((b ∪ (b^⊥ ∩ a^⊥ )) ∩ ((a →₄b) ∪ (b^⊥ ∩ a^⊥ ))) = ((b ∩ ((a →₄b) ∪ (b^⊥ ∩ a^⊥ ))) ∪ ((b^⊥ ∩ a^⊥ ) ∩ ((a →₄b) ∪ (b^⊥ ∩ a^⊥ ))))
30	3, 26	fh1 451	. . . . . . . . 9 (b ∩ ((a →₄b) ∪ (b^⊥ ∩ a^⊥ ))) = ((b ∩ (a →₄b)) ∪ (b ∩ (b^⊥ ∩ a^⊥ )))
31		u4lemab 595	. . . . . . . . . . . 12 ((a →₄b) ∩ b) = ((a ∩ b) ∪ (a^⊥ ∩ b))
32	7, 31	ax-r2 35	. . . . . . . . . . 11 (b ∩ (a →₄b)) = ((a ∩ b) ∪ (a^⊥ ∩ b))
33	32	ax-r5 37	. . . . . . . . . 10 ((b ∩ (a →₄b)) ∪ (b ∩ (b^⊥ ∩ a^⊥ ))) = (((a ∩ b) ∪ (a^⊥ ∩ b)) ∪ (b ∩ (b^⊥ ∩ a^⊥ )))
34		id 58	. . . . . . . . . 10 (((a ∩ b) ∪ (a^⊥ ∩ b)) ∪ (b ∩ (b^⊥ ∩ a^⊥ ))) = (((a ∩ b) ∪ (a^⊥ ∩ b)) ∪ (b ∩ (b^⊥ ∩ a^⊥ )))
35	33, 34	ax-r2 35	. . . . . . . . 9 ((b ∩ (a →₄b)) ∪ (b ∩ (b^⊥ ∩ a^⊥ ))) = (((a ∩ b) ∪ (a^⊥ ∩ b)) ∪ (b ∩ (b^⊥ ∩ a^⊥ )))
36	30, 35	ax-r2 35	. . . . . . . 8 (b ∩ ((a →₄b) ∪ (b^⊥ ∩ a^⊥ ))) = (((a ∩ b) ∪ (a^⊥ ∩ b)) ∪ (b ∩ (b^⊥ ∩ a^⊥ )))
37		leor 151	. . . . . . . . 9 (b^⊥ ∩ a^⊥ ) ≤ ((a →₄b) ∪ (b^⊥ ∩ a^⊥ ))
38	37	df2le2 128	. . . . . . . 8 ((b^⊥ ∩ a^⊥ ) ∩ ((a →₄b) ∪ (b^⊥ ∩ a^⊥ ))) = (b^⊥ ∩ a^⊥ )
39	36, 38	2or 67	. . . . . . 7 ((b ∩ ((a →₄b) ∪ (b^⊥ ∩ a^⊥ ))) ∪ ((b^⊥ ∩ a^⊥ ) ∩ ((a →₄b) ∪ (b^⊥ ∩ a^⊥ )))) = ((((a ∩ b) ∪ (a^⊥ ∩ b)) ∪ (b ∩ (b^⊥ ∩ a^⊥ ))) ∪ (b^⊥ ∩ a^⊥ ))
40		ax-a3 31	. . . . . . . 8 ((((a ∩ b) ∪ (a^⊥ ∩ b)) ∪ (b ∩ (b^⊥ ∩ a^⊥ ))) ∪ (b^⊥ ∩ a^⊥ )) = (((a ∩ b) ∪ (a^⊥ ∩ b)) ∪ ((b ∩ (b^⊥ ∩ a^⊥ )) ∪ (b^⊥ ∩ a^⊥ )))
41		lear 153	. . . . . . . . . . . 12 (b ∩ (b^⊥ ∩ a^⊥ )) ≤ (b^⊥ ∩ a^⊥ )
42	41	df-le2 123	. . . . . . . . . . 11 ((b ∩ (b^⊥ ∩ a^⊥ )) ∪ (b^⊥ ∩ a^⊥ )) = (b^⊥ ∩ a^⊥ )
43		ancom 68	. . . . . . . . . . 11 (b^⊥ ∩ a^⊥ ) = (a^⊥ ∩ b^⊥ )
44	42, 43	ax-r2 35	. . . . . . . . . 10 ((b ∩ (b^⊥ ∩ a^⊥ )) ∪ (b^⊥ ∩ a^⊥ )) = (a^⊥ ∩ b^⊥ )
45	44	lor 66	. . . . . . . . 9 (((a ∩ b) ∪ (a^⊥ ∩ b)) ∪ ((b ∩ (b^⊥ ∩ a^⊥ )) ∪ (b^⊥ ∩ a^⊥ ))) = (((a ∩ b) ∪ (a^⊥ ∩ b)) ∪ (a^⊥ ∩ b^⊥ ))
46		df-i5 47	. . . . . . . . . . 11 (a →₅b) = (((a ∩ b) ∪ (a^⊥ ∩ b)) ∪ (a^⊥ ∩ b^⊥ ))
47	46	ax-r1 34	. . . . . . . . . 10 (((a ∩ b) ∪ (a^⊥ ∩ b)) ∪ (a^⊥ ∩ b^⊥ )) = (a →₅b)
48		id 58	. . . . . . . . . 10 (a →₅b) = (a →₅b)
49	47, 48	ax-r2 35	. . . . . . . . 9 (((a ∩ b) ∪ (a^⊥ ∩ b)) ∪ (a^⊥ ∩ b^⊥ )) = (a →₅b)
50	45, 49	ax-r2 35	. . . . . . . 8 (((a ∩ b) ∪ (a^⊥ ∩ b)) ∪ ((b ∩ (b^⊥ ∩ a^⊥ )) ∪ (b^⊥ ∩ a^⊥ ))) = (a →₅b)
51	40, 50	ax-r2 35	. . . . . . 7 ((((a ∩ b) ∪ (a^⊥ ∩ b)) ∪ (b ∩ (b^⊥ ∩ a^⊥ ))) ∪ (b^⊥ ∩ a^⊥ )) = (a →₅b)
52	39, 51	ax-r2 35	. . . . . 6 ((b ∩ ((a →₄b) ∪ (b^⊥ ∩ a^⊥ ))) ∪ ((b^⊥ ∩ a^⊥ ) ∩ ((a →₄b) ∪ (b^⊥ ∩ a^⊥ )))) = (a →₅b)
53	29, 52	ax-r2 35	. . . . 5 ((b ∪ (b^⊥ ∩ a^⊥ )) ∩ ((a →₄b) ∪ (b^⊥ ∩ a^⊥ ))) = (a →₅b)
54	27, 53	ax-r2 35	. . . 4 ((b ∩ (a →₄b)) ∪ (b^⊥ ∩ a^⊥ )) = (a →₅b)
55	24, 54	ax-r2 35	. . 3 ((b ∩ (a →₄b)) ∪ ((a^⊥ ∩ b^⊥ ) ∩ (a →₄b))) = (a →₅b)
56	6, 55	ax-r2 35	. 2 ((b ∪ (a^⊥ ∩ b^⊥ )) ∩ (a →₄b)) = (a →₅b)
57	2, 56	ax-r2 35	1 ((a →₂b) ∩ (a →₄b)) = (a →₅b)

Colors of variables: term

Syntax hints: = wb 1 ^⊥ wn 4 ∪ wo 6 ∩ wa 7 →₂wi2 14 →₄wi4 16 →₅wi5 17

This theorem is referenced by: negant5 845

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

metamath.org