Theorem lem3.3.7i3e2 1067

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

Assertion

Ref	Expression
lem3.3.7i3e2	(a ≡3 (a ∩ b)) = ((a ∩ b) ≡3 a)

Proof of Theorem lem3.3.7i3e2

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

Syntax hints:   = wb 1  ^⊥ wn 4   ∪ wo 6   ∩ wa 7  1wt 8   ≡₃ wid3 20

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-id3 52  df-le1 130  df-le2 131

This theorem is referenced by: (None)