Theorem comanblem2 871

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

Assertion

Ref	Expression
comanblem2	((a ∩ b) ∩ ((a ≡ c) ∩ (b ≡ c))) = ((a ∩ b) ∩ c)

Proof of Theorem comanblem2

Step	Hyp	Ref	Expression
1		dfb 94	. . . 4 (a ≡ c) = ((a ∩ c) ∪ (a⊥ ∩ c⊥ ))
2		dfb 94	. . . 4 (b ≡ c) = ((b ∩ c) ∪ (b⊥ ∩ c⊥ ))
3	1, 2	2an 79	. . 3 ((a ≡ c) ∩ (b ≡ c)) = (((a ∩ c) ∪ (a⊥ ∩ c⊥ )) ∩ ((b ∩ c) ∪ (b⊥ ∩ c⊥ )))
4	3	lan 77	. 2 ((a ∩ b) ∩ ((a ≡ c) ∩ (b ≡ c))) = ((a ∩ b) ∩ (((a ∩ c) ∪ (a⊥ ∩ c⊥ )) ∩ ((b ∩ c) ∪ (b⊥ ∩ c⊥ ))))
5		comanr1 464	. . . . . 6 a C (a ∩ c)
6		comanr1 464	. . . . . . 7 a⊥ C (a⊥ ∩ c⊥ )
7	6	comcom6 459	. . . . . 6 a C (a⊥ ∩ c⊥ )
8	5, 7	fh1 469	. . . . 5 (a ∩ ((a ∩ c) ∪ (a⊥ ∩ c⊥ ))) = ((a ∩ (a ∩ c)) ∪ (a ∩ (a⊥ ∩ c⊥ )))
9		anass 76	. . . . . . . 8 ((a ∩ a) ∩ c) = (a ∩ (a ∩ c))
10	9	ax-r1 35	. . . . . . 7 (a ∩ (a ∩ c)) = ((a ∩ a) ∩ c)
11		anidm 111	. . . . . . . 8 (a ∩ a) = a
12	11	ran 78	. . . . . . 7 ((a ∩ a) ∩ c) = (a ∩ c)
13	10, 12	ax-r2 36	. . . . . 6 (a ∩ (a ∩ c)) = (a ∩ c)
14		dff 101	. . . . . . . . 9 0 = (a ∩ a⊥ )
15	14	ran 78	. . . . . . . 8 (0 ∩ c⊥ ) = ((a ∩ a⊥ ) ∩ c⊥ )
16	15	ax-r1 35	. . . . . . 7 ((a ∩ a⊥ ) ∩ c⊥ ) = (0 ∩ c⊥ )
17		anass 76	. . . . . . 7 ((a ∩ a⊥ ) ∩ c⊥ ) = (a ∩ (a⊥ ∩ c⊥ ))
18		an0r 109	. . . . . . 7 (0 ∩ c⊥ ) = 0
19	16, 17, 18	3tr2 64	. . . . . 6 (a ∩ (a⊥ ∩ c⊥ )) = 0
20	13, 19	2or 72	. . . . 5 ((a ∩ (a ∩ c)) ∪ (a ∩ (a⊥ ∩ c⊥ ))) = ((a ∩ c) ∪ 0)
21		or0 102	. . . . 5 ((a ∩ c) ∪ 0) = (a ∩ c)
22	8, 20, 21	3tr 65	. . . 4 (a ∩ ((a ∩ c) ∪ (a⊥ ∩ c⊥ ))) = (a ∩ c)
23		comanr1 464	. . . . . 6 b C (b ∩ c)
24		comanr1 464	. . . . . . 7 b⊥ C (b⊥ ∩ c⊥ )
25	24	comcom6 459	. . . . . 6 b C (b⊥ ∩ c⊥ )
26	23, 25	fh1 469	. . . . 5 (b ∩ ((b ∩ c) ∪ (b⊥ ∩ c⊥ ))) = ((b ∩ (b ∩ c)) ∪ (b ∩ (b⊥ ∩ c⊥ )))
27		anass 76	. . . . . . . 8 ((b ∩ b) ∩ c) = (b ∩ (b ∩ c))
28	27	ax-r1 35	. . . . . . 7 (b ∩ (b ∩ c)) = ((b ∩ b) ∩ c)
29		anidm 111	. . . . . . . 8 (b ∩ b) = b
30	29	ran 78	. . . . . . 7 ((b ∩ b) ∩ c) = (b ∩ c)
31	28, 30	ax-r2 36	. . . . . 6 (b ∩ (b ∩ c)) = (b ∩ c)
32		dff 101	. . . . . . . . 9 0 = (b ∩ b⊥ )
33	32	ran 78	. . . . . . . 8 (0 ∩ c⊥ ) = ((b ∩ b⊥ ) ∩ c⊥ )
34	33	ax-r1 35	. . . . . . 7 ((b ∩ b⊥ ) ∩ c⊥ ) = (0 ∩ c⊥ )
35		anass 76	. . . . . . 7 ((b ∩ b⊥ ) ∩ c⊥ ) = (b ∩ (b⊥ ∩ c⊥ ))
36	34, 35, 18	3tr2 64	. . . . . 6 (b ∩ (b⊥ ∩ c⊥ )) = 0
37	31, 36	2or 72	. . . . 5 ((b ∩ (b ∩ c)) ∪ (b ∩ (b⊥ ∩ c⊥ ))) = ((b ∩ c) ∪ 0)
38		or0 102	. . . . 5 ((b ∩ c) ∪ 0) = (b ∩ c)
39	26, 37, 38	3tr 65	. . . 4 (b ∩ ((b ∩ c) ∪ (b⊥ ∩ c⊥ ))) = (b ∩ c)
40	22, 39	2an 79	. . 3 ((a ∩ ((a ∩ c) ∪ (a⊥ ∩ c⊥ ))) ∩ (b ∩ ((b ∩ c) ∪ (b⊥ ∩ c⊥ )))) = ((a ∩ c) ∩ (b ∩ c))
41		an4 86	. . 3 ((a ∩ b) ∩ (((a ∩ c) ∪ (a⊥ ∩ c⊥ )) ∩ ((b ∩ c) ∪ (b⊥ ∩ c⊥ )))) = ((a ∩ ((a ∩ c) ∪ (a⊥ ∩ c⊥ ))) ∩ (b ∩ ((b ∩ c) ∪ (b⊥ ∩ c⊥ ))))
42		anandir 115	. . 3 ((a ∩ b) ∩ c) = ((a ∩ c) ∩ (b ∩ c))
43	40, 41, 42	3tr1 63	. 2 ((a ∩ b) ∩ (((a ∩ c) ∪ (a⊥ ∩ c⊥ )) ∩ ((b ∩ c) ∪ (b⊥ ∩ c⊥ )))) = ((a ∩ b) ∩ c)
44	4, 43	ax-r2 36	1 ((a ∩ b) ∩ ((a ≡ c) ∩ (b ≡ c))) = ((a ∩ b) ∩ c)

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

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-le1 130  df-le2 131  df-c1 132  df-c2 133

This theorem is referenced by:  comanb  872