Theorem lem3.3.7i1e2 1061

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

Assertion

Ref	Expression
lem3.3.7i1e2	(a ≡1 (a ∩ b)) = ((a ∩ b) ≡1 a)

Proof of Theorem lem3.3.7i1e2

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⊥ ∪ (a ∩ (a ∩ b)))) = ((a ∪ (a⊥ ∪ b⊥ )) ∩ (a⊥ ∪ (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⊥ ∪ (a ∩ (a ∩ b)))) = (((a ∪ a⊥ ) ∪ b⊥ ) ∩ (a⊥ ∪ (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⊥ ∪ (a ∩ (a ∩ b)))) = ((1 ∪ b⊥ ) ∩ (a⊥ ∪ (a ∩ (a ∩ b))))
12		or1r 105	. . . . 5 (1 ∪ b⊥ ) = 1
13	12	ran 78	. . . 4 ((1 ∪ b⊥ ) ∩ (a⊥ ∪ (a ∩ (a ∩ b)))) = (1 ∩ (a⊥ ∪ (a ∩ (a ∩ b))))
14		an1r 107	. . . . 5 (1 ∩ (a⊥ ∪ (a ∩ (a ∩ b)))) = (a⊥ ∪ (a ∩ (a ∩ b)))
15		anass 76	. . . . . . 7 ((a ∩ a) ∩ b) = (a ∩ (a ∩ b))
16	15	ax-r1 35	. . . . . 6 (a ∩ (a ∩ b)) = ((a ∩ a) ∩ b)
17	16	lor 70	. . . . 5 (a⊥ ∪ (a ∩ (a ∩ b))) = (a⊥ ∪ ((a ∩ a) ∩ b))
18		anidm 111	. . . . . . . 8 (a ∩ a) = a
19	18	ran 78	. . . . . . 7 ((a ∩ a) ∩ b) = (a ∩ b)
20	19	lor 70	. . . . . 6 (a⊥ ∪ ((a ∩ a) ∩ b)) = (a⊥ ∪ (a ∩ b))
21		ax-a2 31	. . . . . . . . 9 (a⊥ ∪ (a ∩ b)) = ((a ∩ b) ∪ a⊥ )
22		an1 106	. . . . . . . . . 10 (((a ∩ b) ∪ a⊥ ) ∩ 1) = ((a ∩ b) ∪ a⊥ )
23	22	ax-r1 35	. . . . . . . . 9 ((a ∩ b) ∪ a⊥ ) = (((a ∩ b) ∪ a⊥ ) ∩ 1)
24		df-t 41	. . . . . . . . . 10 1 = ((a ∩ b) ∪ (a ∩ b)⊥ )
25	24	lan 77	. . . . . . . . 9 (((a ∩ b) ∪ a⊥ ) ∩ 1) = (((a ∩ b) ∪ a⊥ ) ∩ ((a ∩ b) ∪ (a ∩ b)⊥ ))
26	21, 23, 25	3tr 65	. . . . . . . 8 (a⊥ ∪ (a ∩ b)) = (((a ∩ b) ∪ a⊥ ) ∩ ((a ∩ b) ∪ (a ∩ b)⊥ ))
27		ax-a2 31	. . . . . . . . 9 ((a ∩ b) ∪ (a ∩ b)⊥ ) = ((a ∩ b)⊥ ∪ (a ∩ b))
28	27	lan 77	. . . . . . . 8 (((a ∩ b) ∪ a⊥ ) ∩ ((a ∩ b) ∪ (a ∩ b)⊥ )) = (((a ∩ b) ∪ a⊥ ) ∩ ((a ∩ b)⊥ ∪ (a ∩ b)))
29	18	ax-r1 35	. . . . . . . . . . 11 a = (a ∩ a)
30	29	ran 78	. . . . . . . . . 10 (a ∩ b) = ((a ∩ a) ∩ b)
31	30	lor 70	. . . . . . . . 9 ((a ∩ b)⊥ ∪ (a ∩ b)) = ((a ∩ b)⊥ ∪ ((a ∩ a) ∩ b))
32	31	lan 77	. . . . . . . 8 (((a ∩ b) ∪ a⊥ ) ∩ ((a ∩ b)⊥ ∪ (a ∩ b))) = (((a ∩ b) ∪ a⊥ ) ∩ ((a ∩ b)⊥ ∪ ((a ∩ a) ∩ b)))
33	26, 28, 32	3tr 65	. . . . . . 7 (a⊥ ∪ (a ∩ b)) = (((a ∩ b) ∪ a⊥ ) ∩ ((a ∩ b)⊥ ∪ ((a ∩ a) ∩ b)))
34	15	lor 70	. . . . . . . 8 ((a ∩ b)⊥ ∪ ((a ∩ a) ∩ b)) = ((a ∩ b)⊥ ∪ (a ∩ (a ∩ b)))
35	34	lan 77	. . . . . . 7 (((a ∩ b) ∪ a⊥ ) ∩ ((a ∩ b)⊥ ∪ ((a ∩ a) ∩ b))) = (((a ∩ b) ∪ a⊥ ) ∩ ((a ∩ b)⊥ ∪ (a ∩ (a ∩ b))))
36		ancom 74	. . . . . . . . . 10 (a ∩ b) = (b ∩ a)
37	36	lan 77	. . . . . . . . 9 (a ∩ (a ∩ b)) = (a ∩ (b ∩ a))
38	37	lor 70	. . . . . . . 8 ((a ∩ b)⊥ ∪ (a ∩ (a ∩ b))) = ((a ∩ b)⊥ ∪ (a ∩ (b ∩ a)))
39	38	lan 77	. . . . . . 7 (((a ∩ b) ∪ a⊥ ) ∩ ((a ∩ b)⊥ ∪ (a ∩ (a ∩ b)))) = (((a ∩ b) ∪ a⊥ ) ∩ ((a ∩ b)⊥ ∪ (a ∩ (b ∩ a))))
40	33, 35, 39	3tr 65	. . . . . 6 (a⊥ ∪ (a ∩ b)) = (((a ∩ b) ∪ a⊥ ) ∩ ((a ∩ b)⊥ ∪ (a ∩ (b ∩ a))))
41		anass 76	. . . . . . . . 9 ((a ∩ b) ∩ a) = (a ∩ (b ∩ a))
42	41	ax-r1 35	. . . . . . . 8 (a ∩ (b ∩ a)) = ((a ∩ b) ∩ a)
43	42	lor 70	. . . . . . 7 ((a ∩ b)⊥ ∪ (a ∩ (b ∩ a))) = ((a ∩ b)⊥ ∪ ((a ∩ b) ∩ a))
44	43	lan 77	. . . . . 6 (((a ∩ b) ∪ a⊥ ) ∩ ((a ∩ b)⊥ ∪ (a ∩ (b ∩ a)))) = (((a ∩ b) ∪ a⊥ ) ∩ ((a ∩ b)⊥ ∪ ((a ∩ b) ∩ a)))
45	20, 40, 44	3tr 65	. . . . 5 (a⊥ ∪ ((a ∩ a) ∩ b)) = (((a ∩ b) ∪ a⊥ ) ∩ ((a ∩ b)⊥ ∪ ((a ∩ b) ∩ a)))
46	14, 17, 45	3tr 65	. . . 4 (1 ∩ (a⊥ ∪ (a ∩ (a ∩ b)))) = (((a ∩ b) ∪ a⊥ ) ∩ ((a ∩ b)⊥ ∪ ((a ∩ b) ∩ a)))
47	11, 13, 46	3tr 65	. . 3 (((a ∪ a⊥ ) ∪ b⊥ ) ∩ (a⊥ ∪ (a ∩ (a ∩ b)))) = (((a ∩ b) ∪ a⊥ ) ∩ ((a ∩ b)⊥ ∪ ((a ∩ b) ∩ a)))
48	4, 7, 47	3tr 65	. 2 ((a ∪ (a ∩ b)⊥ ) ∩ (a⊥ ∪ (a ∩ (a ∩ b)))) = (((a ∩ b) ∪ a⊥ ) ∩ ((a ∩ b)⊥ ∪ ((a ∩ b) ∩ a)))
49		df-id1 50	. 2 (a ≡1 (a ∩ b)) = ((a ∪ (a ∩ b)⊥ ) ∩ (a⊥ ∪ (a ∩ (a ∩ b))))
50		df-id1 50	. 2 ((a ∩ b) ≡1 a) = (((a ∩ b) ∪ a⊥ ) ∩ ((a ∩ b)⊥ ∪ ((a ∩ b) ∩ a)))
51	48, 49, 50	3tr1 63	1 (a ≡1 (a ∩ b)) = ((a ∩ b) ≡1 a)

This proof depends on syntax axioms:   = wb 1  ^⊥ wn 4   ∪ wo 6   ∩ wa 7  1wt 8   ≡₁ wid1 18

This proof depends on 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 proof depends on definitions:  df-a 40  df-t 41  df-f 42  df-id1 50

This theorem is used by: (None)