Theorem comanblem1 870

Description: Lemma for biconditional commutation law. (Contributed by NM, 1-Dec-1999.)

Assertion

Ref	Expression
comanblem1	((a ≡ c) ∩ (b ≡ c)) = (((a ∪ c)⊥ ∪ ((a ∩ b) ∩ c)) ∩ (b →1 c))

Proof of Theorem comanblem1

Step	Hyp	Ref	Expression
1		an4 86	. 2 (((a →1 c) ∩ (c →1 a)) ∩ ((b →1 c) ∩ (c →1 b))) = (((a →1 c) ∩ (b →1 c)) ∩ ((c →1 a) ∩ (c →1 b)))
2		u1lembi 720	. . 3 ((a →1 c) ∩ (c →1 a)) = (a ≡ c)
3		u1lembi 720	. . 3 ((b →1 c) ∩ (c →1 b)) = (b ≡ c)
4	2, 3	2an 79	. 2 (((a →1 c) ∩ (c →1 a)) ∩ ((b →1 c) ∩ (c →1 b))) = ((a ≡ c) ∩ (b ≡ c))
5		an32 83	. . 3 (((a →1 c) ∩ (b →1 c)) ∩ ((c →1 a) ∩ (c →1 b))) = (((a →1 c) ∩ ((c →1 a) ∩ (c →1 b))) ∩ (b →1 c))
6		df-i1 44	. . . . . . . 8 (c →1 a) = (c⊥ ∪ (c ∩ a))
7		df-i1 44	. . . . . . . 8 (c →1 b) = (c⊥ ∪ (c ∩ b))
8	6, 7	2an 79	. . . . . . 7 ((c →1 a) ∩ (c →1 b)) = ((c⊥ ∪ (c ∩ a)) ∩ (c⊥ ∪ (c ∩ b)))
9		comanr1 464	. . . . . . . . . 10 c C (c ∩ a)
10	9	comcom3 454	. . . . . . . . 9 c⊥ C (c ∩ a)
11		comanr1 464	. . . . . . . . . 10 c C (c ∩ b)
12	11	comcom3 454	. . . . . . . . 9 c⊥ C (c ∩ b)
13	10, 12	fh3 471	. . . . . . . 8 (c⊥ ∪ ((c ∩ a) ∩ (c ∩ b))) = ((c⊥ ∪ (c ∩ a)) ∩ (c⊥ ∪ (c ∩ b)))
14	13	ax-r1 35	. . . . . . 7 ((c⊥ ∪ (c ∩ a)) ∩ (c⊥ ∪ (c ∩ b))) = (c⊥ ∪ ((c ∩ a) ∩ (c ∩ b)))
15	8, 14	ax-r2 36	. . . . . 6 ((c →1 a) ∩ (c →1 b)) = (c⊥ ∪ ((c ∩ a) ∩ (c ∩ b)))
16	15	lan 77	. . . . 5 ((a →1 c) ∩ ((c →1 a) ∩ (c →1 b))) = ((a →1 c) ∩ (c⊥ ∪ ((c ∩ a) ∩ (c ∩ b))))
17		df-i1 44	. . . . . 6 (a →1 c) = (a⊥ ∪ (a ∩ c))
18	17	ran 78	. . . . 5 ((a →1 c) ∩ (c⊥ ∪ ((c ∩ a) ∩ (c ∩ b)))) = ((a⊥ ∪ (a ∩ c)) ∩ (c⊥ ∪ ((c ∩ a) ∩ (c ∩ b))))
19		lea 160	. . . . . . . . 9 ((c ∩ a) ∩ (c ∩ b)) ≤ (c ∩ a)
20		ancom 74	. . . . . . . . . 10 (c ∩ a) = (a ∩ c)
21		leor 159	. . . . . . . . . 10 (a ∩ c) ≤ (a⊥ ∪ (a ∩ c))
22	20, 21	bltr 138	. . . . . . . . 9 (c ∩ a) ≤ (a⊥ ∪ (a ∩ c))
23	19, 22	letr 137	. . . . . . . 8 ((c ∩ a) ∩ (c ∩ b)) ≤ (a⊥ ∪ (a ∩ c))
24	23	lecom 180	. . . . . . 7 ((c ∩ a) ∩ (c ∩ b)) C (a⊥ ∪ (a ∩ c))
25	10, 12	com2an 484	. . . . . . . 8 c⊥ C ((c ∩ a) ∩ (c ∩ b))
26	25	comcom 453	. . . . . . 7 ((c ∩ a) ∩ (c ∩ b)) C c⊥
27	24, 26	fh2c 477	. . . . . 6 ((a⊥ ∪ (a ∩ c)) ∩ (c⊥ ∪ ((c ∩ a) ∩ (c ∩ b)))) = (((a⊥ ∪ (a ∩ c)) ∩ c⊥ ) ∪ ((a⊥ ∪ (a ∩ c)) ∩ ((c ∩ a) ∩ (c ∩ b))))
28		coman2 186	. . . . . . . . . 10 (a ∩ c) C c
29	28	comcom2 183	. . . . . . . . 9 (a ∩ c) C c⊥
30		coman1 185	. . . . . . . . . 10 (a ∩ c) C a
31	30	comcom2 183	. . . . . . . . 9 (a ∩ c) C a⊥
32	29, 31	fh2rc 480	. . . . . . . 8 ((a⊥ ∪ (a ∩ c)) ∩ c⊥ ) = ((a⊥ ∩ c⊥ ) ∪ ((a ∩ c) ∩ c⊥ ))
33		anass 76	. . . . . . . . . 10 ((a ∩ c) ∩ c⊥ ) = (a ∩ (c ∩ c⊥ ))
34		dff 101	. . . . . . . . . . . 12 0 = (c ∩ c⊥ )
35	34	lan 77	. . . . . . . . . . 11 (a ∩ 0) = (a ∩ (c ∩ c⊥ ))
36	35	ax-r1 35	. . . . . . . . . 10 (a ∩ (c ∩ c⊥ )) = (a ∩ 0)
37		an0 108	. . . . . . . . . 10 (a ∩ 0) = 0
38	33, 36, 37	3tr 65	. . . . . . . . 9 ((a ∩ c) ∩ c⊥ ) = 0
39	38	lor 70	. . . . . . . 8 ((a⊥ ∩ c⊥ ) ∪ ((a ∩ c) ∩ c⊥ )) = ((a⊥ ∩ c⊥ ) ∪ 0)
40		or0 102	. . . . . . . . 9 ((a⊥ ∩ c⊥ ) ∪ 0) = (a⊥ ∩ c⊥ )
41		anor3 90	. . . . . . . . 9 (a⊥ ∩ c⊥ ) = (a ∪ c)⊥
42	40, 41	ax-r2 36	. . . . . . . 8 ((a⊥ ∩ c⊥ ) ∪ 0) = (a ∪ c)⊥
43	32, 39, 42	3tr 65	. . . . . . 7 ((a⊥ ∪ (a ∩ c)) ∩ c⊥ ) = (a ∪ c)⊥
44		ancom 74	. . . . . . . . . 10 (a ∩ c) = (c ∩ a)
45		comanr1 464	. . . . . . . . . 10 (c ∩ a) C ((c ∩ a) ∩ (c ∩ b))
46	44, 45	bctr 181	. . . . . . . . 9 (a ∩ c) C ((c ∩ a) ∩ (c ∩ b))
47	46, 31	fh2rc 480	. . . . . . . 8 ((a⊥ ∪ (a ∩ c)) ∩ ((c ∩ a) ∩ (c ∩ b))) = ((a⊥ ∩ ((c ∩ a) ∩ (c ∩ b))) ∪ ((a ∩ c) ∩ ((c ∩ a) ∩ (c ∩ b))))
48		anandi 114	. . . . . . . . . . . 12 (c ∩ (a ∩ b)) = ((c ∩ a) ∩ (c ∩ b))
49	48	ax-r1 35	. . . . . . . . . . 11 ((c ∩ a) ∩ (c ∩ b)) = (c ∩ (a ∩ b))
50		ancom 74	. . . . . . . . . . 11 (c ∩ (a ∩ b)) = ((a ∩ b) ∩ c)
51	49, 50	ax-r2 36	. . . . . . . . . 10 ((c ∩ a) ∩ (c ∩ b)) = ((a ∩ b) ∩ c)
52	51	lan 77	. . . . . . . . 9 (a⊥ ∩ ((c ∩ a) ∩ (c ∩ b))) = (a⊥ ∩ ((a ∩ b) ∩ c))
53	51	lan 77	. . . . . . . . . 10 ((a ∩ c) ∩ ((c ∩ a) ∩ (c ∩ b))) = ((a ∩ c) ∩ ((a ∩ b) ∩ c))
54		ancom 74	. . . . . . . . . 10 ((a ∩ c) ∩ ((a ∩ b) ∩ c)) = (((a ∩ b) ∩ c) ∩ (a ∩ c))
55		lea 160	. . . . . . . . . . . 12 (a ∩ b) ≤ a
56	55	leran 153	. . . . . . . . . . 11 ((a ∩ b) ∩ c) ≤ (a ∩ c)
57	56	df2le2 136	. . . . . . . . . 10 (((a ∩ b) ∩ c) ∩ (a ∩ c)) = ((a ∩ b) ∩ c)
58	53, 54, 57	3tr 65	. . . . . . . . 9 ((a ∩ c) ∩ ((c ∩ a) ∩ (c ∩ b))) = ((a ∩ b) ∩ c)
59	52, 58	2or 72	. . . . . . . 8 ((a⊥ ∩ ((c ∩ a) ∩ (c ∩ b))) ∪ ((a ∩ c) ∩ ((c ∩ a) ∩ (c ∩ b)))) = ((a⊥ ∩ ((a ∩ b) ∩ c)) ∪ ((a ∩ b) ∩ c))
60		lear 161	. . . . . . . . 9 (a⊥ ∩ ((a ∩ b) ∩ c)) ≤ ((a ∩ b) ∩ c)
61	60	df-le2 131	. . . . . . . 8 ((a⊥ ∩ ((a ∩ b) ∩ c)) ∪ ((a ∩ b) ∩ c)) = ((a ∩ b) ∩ c)
62	47, 59, 61	3tr 65	. . . . . . 7 ((a⊥ ∪ (a ∩ c)) ∩ ((c ∩ a) ∩ (c ∩ b))) = ((a ∩ b) ∩ c)
63	43, 62	2or 72	. . . . . 6 (((a⊥ ∪ (a ∩ c)) ∩ c⊥ ) ∪ ((a⊥ ∪ (a ∩ c)) ∩ ((c ∩ a) ∩ (c ∩ b)))) = ((a ∪ c)⊥ ∪ ((a ∩ b) ∩ c))
64	27, 63	ax-r2 36	. . . . 5 ((a⊥ ∪ (a ∩ c)) ∩ (c⊥ ∪ ((c ∩ a) ∩ (c ∩ b)))) = ((a ∪ c)⊥ ∪ ((a ∩ b) ∩ c))
65	16, 18, 64	3tr 65	. . . 4 ((a →1 c) ∩ ((c →1 a) ∩ (c →1 b))) = ((a ∪ c)⊥ ∪ ((a ∩ b) ∩ c))
66	65	ran 78	. . 3 (((a →1 c) ∩ ((c →1 a) ∩ (c →1 b))) ∩ (b →1 c)) = (((a ∪ c)⊥ ∪ ((a ∩ b) ∩ c)) ∩ (b →1 c))
67	5, 66	ax-r2 36	. 2 (((a →1 c) ∩ (b →1 c)) ∩ ((c →1 a) ∩ (c →1 b))) = (((a ∪ c)⊥ ∪ ((a ∩ b) ∩ c)) ∩ (b →1 c))
68	1, 4, 67	3tr2 64	1 ((a ≡ c) ∩ (b ≡ c)) = (((a ∪ c)⊥ ∪ ((a ∩ b) ∩ c)) ∩ (b →1 c))

Syntax hints:   = wb 1  ^⊥ wn 4   ≡ tb 5   ∪ wo 6   ∩ wa 7  0wf 9   →₁ wi1 12

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  ax-r3 439

This theorem depends on definitions:  df-b 39  df-a 40  df-t 41  df-f 42  df-i1 44  df-le1 130  df-le2 131  df-c1 132  df-c2 133

This theorem is referenced by:  comanb  872