Theorem lem3.3.7i4e2 1070

Description: Equation 3.7 of [PavMeg1999] p. 9. The variable i in the paper is set to 4, 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.7i4e2	(a ≡4 (a ∩ b)) = ((a ∩ b) ≡4 a)

Proof of Theorem lem3.3.7i4e2

Step	Hyp	Ref	Expression
1		lear 161	. . . . . 6 (a ∩ (a ∩ b)) ≤ (a ∩ b)
2		lea 160	. . . . . . 7 (a ∩ b) ≤ a
3		leid 148	. . . . . . 7 (a ∩ b) ≤ (a ∩ b)
4	2, 3	ler2an 173	. . . . . 6 (a ∩ b) ≤ (a ∩ (a ∩ b))
5	1, 4	lebi 145	. . . . 5 (a ∩ (a ∩ b)) = (a ∩ b)
6	5	lor 70	. . . 4 ((a ∩ b)⊥ ∪ (a ∩ (a ∩ b))) = ((a ∩ b)⊥ ∪ (a ∩ b))
7	6	lan 77	. . 3 ((a⊥ ∪ (a ∩ b)) ∩ ((a ∩ b)⊥ ∪ (a ∩ (a ∩ b)))) = ((a⊥ ∪ (a ∩ b)) ∩ ((a ∩ b)⊥ ∪ (a ∩ b)))
8	3	sklem 230	. . . 4 ((a ∩ b)⊥ ∪ (a ∩ b)) = 1
9	8	lan 77	. . 3 ((a⊥ ∪ (a ∩ b)) ∩ ((a ∩ b)⊥ ∪ (a ∩ b))) = ((a⊥ ∪ (a ∩ b)) ∩ 1)
10		an1 106	. . . 4 ((a⊥ ∪ (a ∩ b)) ∩ 1) = (a⊥ ∪ (a ∩ b))
11	2	df2le2 136	. . . . . . 7 ((a ∩ b) ∩ a) = (a ∩ b)
12	11	ax-r1 35	. . . . . 6 (a ∩ b) = ((a ∩ b) ∩ a)
13	12	lor 70	. . . . 5 (a⊥ ∪ (a ∩ b)) = (a⊥ ∪ ((a ∩ b) ∩ a))
14		an1r 107	. . . . . 6 (1 ∩ (a⊥ ∪ ((a ∩ b) ∩ a))) = (a⊥ ∪ ((a ∩ b) ∩ a))
15	14	ax-r1 35	. . . . 5 (a⊥ ∪ ((a ∩ b) ∩ a)) = (1 ∩ (a⊥ ∪ ((a ∩ b) ∩ a)))
16	13, 15	ax-r2 36	. . . 4 (a⊥ ∪ (a ∩ b)) = (1 ∩ (a⊥ ∪ ((a ∩ b) ∩ a)))
17	2	sklem 230	. . . . . 6 ((a ∩ b)⊥ ∪ a) = 1
18	17	ax-r1 35	. . . . 5 1 = ((a ∩ b)⊥ ∪ a)
19	18	ran 78	. . . 4 (1 ∩ (a⊥ ∪ ((a ∩ b) ∩ a))) = (((a ∩ b)⊥ ∪ a) ∩ (a⊥ ∪ ((a ∩ b) ∩ a)))
20	10, 16, 19	3tr 65	. . 3 ((a⊥ ∪ (a ∩ b)) ∩ 1) = (((a ∩ b)⊥ ∪ a) ∩ (a⊥ ∪ ((a ∩ b) ∩ a)))
21	7, 9, 20	3tr 65	. 2 ((a⊥ ∪ (a ∩ b)) ∩ ((a ∩ b)⊥ ∪ (a ∩ (a ∩ b)))) = (((a ∩ b)⊥ ∪ a) ∩ (a⊥ ∪ ((a ∩ b) ∩ a)))
22		df-id4 53	. 2 (a ≡4 (a ∩ b)) = ((a⊥ ∪ (a ∩ b)) ∩ ((a ∩ b)⊥ ∪ (a ∩ (a ∩ b))))
23		df-id4 53	. 2 ((a ∩ b) ≡4 a) = (((a ∩ b)⊥ ∪ a) ∩ (a⊥ ∪ ((a ∩ b) ∩ a)))
24	21, 22, 23	3tr1 63	1 (a ≡4 (a ∩ b)) = ((a ∩ b) ≡4 a)

Syntax hints:   = wb 1  ^⊥ wn 4   ∪ wo 6   ∩ wa 7  1wt 8   ≡₄ wid4 21

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-id4 53  df-le1 130  df-le2 131

This theorem is referenced by: (None)