Theorem lem3.3.7i2e2 1064

Description: Equation 3.7 of [PavMeg1999] p. 9. The variable i in the paper is set to 2, and this is the second part of the equation. (Contributed by Roy F. Longton, 3-Jul-2005.)

Assertion

Ref	Expression
lem3.3.7i2e2	(a ≡2 (a ∩ b)) = ((a ∩ b) ≡2 a)

Proof of Theorem lem3.3.7i2e2

Step	Hyp	Ref	Expression
1		oran3 93	. . . . . 6 (a⊥ ∪ b⊥ ) = (a ∩ b)⊥
2	1	ax-r1 35	. . . . 5 (a ∩ b)⊥ = (a⊥ ∪ b⊥ )
3	2	lor 70	. . . 4 (a ∪ (a ∩ b)⊥ ) = (a ∪ (a⊥ ∪ b⊥ ))
4	3	ran 78	. . 3 ((a ∪ (a ∩ b)⊥ ) ∩ ((a ∩ b) ∪ (a⊥ ∩ (a ∩ b)⊥ ))) = ((a ∪ (a⊥ ∪ b⊥ )) ∩ ((a ∩ b) ∪ (a⊥ ∩ (a ∩ b)⊥ )))
5		ax-a3 32	. . . . 5 ((a ∪ a⊥ ) ∪ b⊥ ) = (a ∪ (a⊥ ∪ b⊥ ))
6	5	ax-r1 35	. . . 4 (a ∪ (a⊥ ∪ b⊥ )) = ((a ∪ a⊥ ) ∪ b⊥ )
7	6	ran 78	. . 3 ((a ∪ (a⊥ ∪ b⊥ )) ∩ ((a ∩ b) ∪ (a⊥ ∩ (a ∩ b)⊥ ))) = (((a ∪ a⊥ ) ∪ b⊥ ) ∩ ((a ∩ b) ∪ (a⊥ ∩ (a ∩ b)⊥ )))
8		df-t 41	. . . . . . 7 1 = (a ∪ a⊥ )
9	8	ax-r1 35	. . . . . 6 (a ∪ a⊥ ) = 1
10	9	ax-r5 38	. . . . 5 ((a ∪ a⊥ ) ∪ b⊥ ) = (1 ∪ b⊥ )
11	10	ran 78	. . . 4 (((a ∪ a⊥ ) ∪ b⊥ ) ∩ ((a ∩ b) ∪ (a⊥ ∩ (a ∩ b)⊥ ))) = ((1 ∪ b⊥ ) ∩ ((a ∩ b) ∪ (a⊥ ∩ (a ∩ b)⊥ )))
12		or1r 105	. . . . 5 (1 ∪ b⊥ ) = 1
13	12	ran 78	. . . 4 ((1 ∪ b⊥ ) ∩ ((a ∩ b) ∪ (a⊥ ∩ (a ∩ b)⊥ ))) = (1 ∩ ((a ∩ b) ∪ (a⊥ ∩ (a ∩ b)⊥ )))
14		an1r 107	. . . . 5 (1 ∩ ((a ∩ b) ∪ (a⊥ ∩ (a ∩ b)⊥ ))) = ((a ∩ b) ∪ (a⊥ ∩ (a ∩ b)⊥ ))
15		anor3 90	. . . . . 6 (a⊥ ∩ (a ∩ b)⊥ ) = (a ∪ (a ∩ b))⊥
16	15	lor 70	. . . . 5 ((a ∩ b) ∪ (a⊥ ∩ (a ∩ b)⊥ )) = ((a ∩ b) ∪ (a ∪ (a ∩ b))⊥ )
17		orabs 120	. . . . . . . 8 (a ∪ (a ∩ b)) = a
18	17	ax-r4 37	. . . . . . 7 (a ∪ (a ∩ b))⊥ = a⊥
19	18	lor 70	. . . . . 6 ((a ∩ b) ∪ (a ∪ (a ∩ b))⊥ ) = ((a ∩ b) ∪ a⊥ )
20		an1 106	. . . . . . . . 9 (((a ∩ b) ∪ a⊥ ) ∩ 1) = ((a ∩ b) ∪ a⊥ )
21	20	ax-r1 35	. . . . . . . 8 ((a ∩ b) ∪ a⊥ ) = (((a ∩ b) ∪ a⊥ ) ∩ 1)
22	8	lan 77	. . . . . . . 8 (((a ∩ b) ∪ a⊥ ) ∩ 1) = (((a ∩ b) ∪ a⊥ ) ∩ (a ∪ a⊥ ))
23	21, 22	ax-r2 36	. . . . . . 7 ((a ∩ b) ∪ a⊥ ) = (((a ∩ b) ∪ a⊥ ) ∩ (a ∪ a⊥ ))
24		lea 160	. . . . . . . . . . . 12 (a ∩ b) ≤ a
25	24	df-le2 131	. . . . . . . . . . 11 ((a ∩ b) ∪ a) = a
26	25	ax-r1 35	. . . . . . . . . 10 a = ((a ∩ b) ∪ a)
27	26	ax-r4 37	. . . . . . . . 9 a⊥ = ((a ∩ b) ∪ a)⊥
28	27	lor 70	. . . . . . . 8 (a ∪ a⊥ ) = (a ∪ ((a ∩ b) ∪ a)⊥ )
29	28	lan 77	. . . . . . 7 (((a ∩ b) ∪ a⊥ ) ∩ (a ∪ a⊥ )) = (((a ∩ b) ∪ a⊥ ) ∩ (a ∪ ((a ∩ b) ∪ a)⊥ ))
30		anor3 90	. . . . . . . . . 10 ((a ∩ b)⊥ ∩ a⊥ ) = ((a ∩ b) ∪ a)⊥
31	30	ax-r1 35	. . . . . . . . 9 ((a ∩ b) ∪ a)⊥ = ((a ∩ b)⊥ ∩ a⊥ )
32	31	lor 70	. . . . . . . 8 (a ∪ ((a ∩ b) ∪ a)⊥ ) = (a ∪ ((a ∩ b)⊥ ∩ a⊥ ))
33	32	lan 77	. . . . . . 7 (((a ∩ b) ∪ a⊥ ) ∩ (a ∪ ((a ∩ b) ∪ a)⊥ )) = (((a ∩ b) ∪ a⊥ ) ∩ (a ∪ ((a ∩ b)⊥ ∩ a⊥ )))
34	23, 29, 33	3tr 65	. . . . . 6 ((a ∩ b) ∪ a⊥ ) = (((a ∩ b) ∪ a⊥ ) ∩ (a ∪ ((a ∩ b)⊥ ∩ a⊥ )))
35	19, 34	ax-r2 36	. . . . 5 ((a ∩ b) ∪ (a ∪ (a ∩ b))⊥ ) = (((a ∩ b) ∪ a⊥ ) ∩ (a ∪ ((a ∩ b)⊥ ∩ a⊥ )))
36	14, 16, 35	3tr 65	. . . 4 (1 ∩ ((a ∩ b) ∪ (a⊥ ∩ (a ∩ b)⊥ ))) = (((a ∩ b) ∪ a⊥ ) ∩ (a ∪ ((a ∩ b)⊥ ∩ a⊥ )))
37	11, 13, 36	3tr 65	. . 3 (((a ∪ a⊥ ) ∪ b⊥ ) ∩ ((a ∩ b) ∪ (a⊥ ∩ (a ∩ b)⊥ ))) = (((a ∩ b) ∪ a⊥ ) ∩ (a ∪ ((a ∩ b)⊥ ∩ a⊥ )))
38	4, 7, 37	3tr 65	. 2 ((a ∪ (a ∩ b)⊥ ) ∩ ((a ∩ b) ∪ (a⊥ ∩ (a ∩ b)⊥ ))) = (((a ∩ b) ∪ a⊥ ) ∩ (a ∪ ((a ∩ b)⊥ ∩ a⊥ )))
39		df-id2 51	. 2 (a ≡2 (a ∩ b)) = ((a ∪ (a ∩ b)⊥ ) ∩ ((a ∩ b) ∪ (a⊥ ∩ (a ∩ b)⊥ )))
40		df-id2 51	. 2 ((a ∩ b) ≡2 a) = (((a ∩ b) ∪ a⊥ ) ∩ (a ∪ ((a ∩ b)⊥ ∩ a⊥ )))
41	38, 39, 40	3tr1 63	1 (a ≡2 (a ∩ b)) = ((a ∩ b) ≡2 a)

Syntax hints:   = wb 1  ^⊥ wn 4   ∪ wo 6   ∩ wa 7  1wt 8   ≡₂ wid2 19

This theorem was proved from axioms:  ax-a1 30  ax-a2 31  ax-a3 32  ax-a4 33  ax-a5 34  ax-r1 35  ax-r2 36  ax-r4 37  ax-r5 38

This theorem depends on definitions:  df-a 40  df-t 41  df-f 42  df-id2 51  df-le1 130  df-le2 131

This theorem is referenced by: (None)