Theorem fh1 469

Description: Foulis-Holland Theorem. (Contributed by NM, 29-Aug-1997.)

Hypotheses

Ref	Expression
fh.1	a C b
fh.2	a C c

Assertion

Ref	Expression
fh1	(a ∩ (b ∪ c)) = ((a ∩ b) ∪ (a ∩ c))

Proof of Theorem fh1

Step	Hyp	Ref	Expression
1		ledi 174	. . 3 ((a ∩ b) ∪ (a ∩ c)) ≤ (a ∩ (b ∪ c))
2		ancom 74	. . . . . 6 (a ∩ (b ∪ c)) = ((b ∪ c) ∩ a)
3		df-a 40	. . . . . . . . 9 (a ∩ b) = (a⊥ ∪ b⊥ )⊥
4		df-a 40	. . . . . . . . 9 (a ∩ c) = (a⊥ ∪ c⊥ )⊥
5	3, 4	2or 72	. . . . . . . 8 ((a ∩ b) ∪ (a ∩ c)) = ((a⊥ ∪ b⊥ )⊥ ∪ (a⊥ ∪ c⊥ )⊥ )
6		df-a 40	. . . . . . . . . 10 ((a⊥ ∪ b⊥ ) ∩ (a⊥ ∪ c⊥ )) = ((a⊥ ∪ b⊥ )⊥ ∪ (a⊥ ∪ c⊥ )⊥ )⊥
7	6	ax-r1 35	. . . . . . . . 9 ((a⊥ ∪ b⊥ )⊥ ∪ (a⊥ ∪ c⊥ )⊥ )⊥ = ((a⊥ ∪ b⊥ ) ∩ (a⊥ ∪ c⊥ ))
8	7	con3 68	. . . . . . . 8 ((a⊥ ∪ b⊥ )⊥ ∪ (a⊥ ∪ c⊥ )⊥ ) = ((a⊥ ∪ b⊥ ) ∩ (a⊥ ∪ c⊥ ))⊥
9	5, 8	ax-r2 36	. . . . . . 7 ((a ∩ b) ∪ (a ∩ c)) = ((a⊥ ∪ b⊥ ) ∩ (a⊥ ∪ c⊥ ))⊥
10	9	con2 67	. . . . . 6 ((a ∩ b) ∪ (a ∩ c))⊥ = ((a⊥ ∪ b⊥ ) ∩ (a⊥ ∪ c⊥ ))
11	2, 10	2an 79	. . . . 5 ((a ∩ (b ∪ c)) ∩ ((a ∩ b) ∪ (a ∩ c))⊥ ) = (((b ∪ c) ∩ a) ∩ ((a⊥ ∪ b⊥ ) ∩ (a⊥ ∪ c⊥ )))
12		anass 76	. . . . . . 7 (((b ∪ c) ∩ a) ∩ ((a⊥ ∪ b⊥ ) ∩ (a⊥ ∪ c⊥ ))) = ((b ∪ c) ∩ (a ∩ ((a⊥ ∪ b⊥ ) ∩ (a⊥ ∪ c⊥ ))))
13		fh.1	. . . . . . . . . . . 12 a C b
14	13	comcom2 183	. . . . . . . . . . 11 a C b⊥
15	14	com3ii 457	. . . . . . . . . 10 (a ∩ (a⊥ ∪ b⊥ )) = (a ∩ b⊥ )
16		fh.2	. . . . . . . . . . . 12 a C c
17	16	comcom2 183	. . . . . . . . . . 11 a C c⊥
18	17	com3ii 457	. . . . . . . . . 10 (a ∩ (a⊥ ∪ c⊥ )) = (a ∩ c⊥ )
19	15, 18	2an 79	. . . . . . . . 9 ((a ∩ (a⊥ ∪ b⊥ )) ∩ (a ∩ (a⊥ ∪ c⊥ ))) = ((a ∩ b⊥ ) ∩ (a ∩ c⊥ ))
20		anandi 114	. . . . . . . . 9 (a ∩ ((a⊥ ∪ b⊥ ) ∩ (a⊥ ∪ c⊥ ))) = ((a ∩ (a⊥ ∪ b⊥ )) ∩ (a ∩ (a⊥ ∪ c⊥ )))
21		anandi 114	. . . . . . . . 9 (a ∩ (b⊥ ∩ c⊥ )) = ((a ∩ b⊥ ) ∩ (a ∩ c⊥ ))
22	19, 20, 21	3tr1 63	. . . . . . . 8 (a ∩ ((a⊥ ∪ b⊥ ) ∩ (a⊥ ∪ c⊥ ))) = (a ∩ (b⊥ ∩ c⊥ ))
23	22	lan 77	. . . . . . 7 ((b ∪ c) ∩ (a ∩ ((a⊥ ∪ b⊥ ) ∩ (a⊥ ∪ c⊥ )))) = ((b ∪ c) ∩ (a ∩ (b⊥ ∩ c⊥ )))
24	12, 23	ax-r2 36	. . . . . 6 (((b ∪ c) ∩ a) ∩ ((a⊥ ∪ b⊥ ) ∩ (a⊥ ∪ c⊥ ))) = ((b ∪ c) ∩ (a ∩ (b⊥ ∩ c⊥ )))
25		an12 81	. . . . . 6 ((b ∪ c) ∩ (a ∩ (b⊥ ∩ c⊥ ))) = (a ∩ ((b ∪ c) ∩ (b⊥ ∩ c⊥ )))
26	24, 25	ax-r2 36	. . . . 5 (((b ∪ c) ∩ a) ∩ ((a⊥ ∪ b⊥ ) ∩ (a⊥ ∪ c⊥ ))) = (a ∩ ((b ∪ c) ∩ (b⊥ ∩ c⊥ )))
27	11, 26	ax-r2 36	. . . 4 ((a ∩ (b ∪ c)) ∩ ((a ∩ b) ∪ (a ∩ c))⊥ ) = (a ∩ ((b ∪ c) ∩ (b⊥ ∩ c⊥ )))
28		oran 87	. . . . . . . . . 10 (b ∪ c) = (b⊥ ∩ c⊥ )⊥
29	28	ax-r1 35	. . . . . . . . 9 (b⊥ ∩ c⊥ )⊥ = (b ∪ c)
30	29	con3 68	. . . . . . . 8 (b⊥ ∩ c⊥ ) = (b ∪ c)⊥
31	30	lan 77	. . . . . . 7 ((b ∪ c) ∩ (b⊥ ∩ c⊥ )) = ((b ∪ c) ∩ (b ∪ c)⊥ )
32		dff 101	. . . . . . . 8 0 = ((b ∪ c) ∩ (b ∪ c)⊥ )
33	32	ax-r1 35	. . . . . . 7 ((b ∪ c) ∩ (b ∪ c)⊥ ) = 0
34	31, 33	ax-r2 36	. . . . . 6 ((b ∪ c) ∩ (b⊥ ∩ c⊥ )) = 0
35	34	lan 77	. . . . 5 (a ∩ ((b ∪ c) ∩ (b⊥ ∩ c⊥ ))) = (a ∩ 0)
36		an0 108	. . . . 5 (a ∩ 0) = 0
37	35, 36	ax-r2 36	. . . 4 (a ∩ ((b ∪ c) ∩ (b⊥ ∩ c⊥ ))) = 0
38	27, 37	ax-r2 36	. . 3 ((a ∩ (b ∪ c)) ∩ ((a ∩ b) ∪ (a ∩ c))⊥ ) = 0
39	1, 38	oml3 452	. 2 ((a ∩ b) ∪ (a ∩ c)) = (a ∩ (b ∪ c))
40	39	ax-r1 35	1 (a ∩ (b ∪ c)) = ((a ∩ b) ∪ (a ∩ c))

Syntax hints:   = wb 1   C wc 3  ^⊥ wn 4   ∪ 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:  fh3  471  fh1r  473  com2or  483  nbdi  486  oml4  487  gsth  489  i3bi  496  dfi3b  499  i3lem1  504  lem4  511  i3abs3  524  i3orlem7  558  i3orlem8  559  ud3lem1b  567  ud4lem1a  577  ud4lem1d  580  u5lemaa  604  u3lemc4  703  u4lemle2  718  u5lemle2  719  u5lembi  725  u12lembi  726  u24lem  770  u3lem13a  789  bi1o1a  798  3vded21  817  3vded3  819  comanblem2  871  mhlem1  877  mlaconjolem  885  lem4.6.2e1  1082