Theorem fh4 472

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
fh4	(b ∪ (a ∩ c)) = ((b ∪ a) ∩ (b ∪ c))

Proof of Theorem fh4

Step	Hyp	Ref	Expression
1		fh.1	. . . . 5 a C b
2	1	comcom4 455	. . . 4 a⊥ C b⊥
3		fh.2	. . . . 5 a C c
4	3	comcom4 455	. . . 4 a⊥ C c⊥
5	2, 4	fh2 470	. . 3 (b⊥ ∩ (a⊥ ∪ c⊥ )) = ((b⊥ ∩ a⊥ ) ∪ (b⊥ ∩ c⊥ ))
6		anor2 89	. . . 4 (b⊥ ∩ (a⊥ ∪ c⊥ )) = (b ∪ (a⊥ ∪ c⊥ )⊥ )⊥
7		df-a 40	. . . . . . 7 (a ∩ c) = (a⊥ ∪ c⊥ )⊥
8	7	ax-r1 35	. . . . . 6 (a⊥ ∪ c⊥ )⊥ = (a ∩ c)
9	8	lor 70	. . . . 5 (b ∪ (a⊥ ∪ c⊥ )⊥ ) = (b ∪ (a ∩ c))
10	9	ax-r4 37	. . . 4 (b ∪ (a⊥ ∪ c⊥ )⊥ )⊥ = (b ∪ (a ∩ c))⊥
11	6, 10	ax-r2 36	. . 3 (b⊥ ∩ (a⊥ ∪ c⊥ )) = (b ∪ (a ∩ c))⊥
12		oran 87	. . . 4 ((b⊥ ∩ a⊥ ) ∪ (b⊥ ∩ c⊥ )) = ((b⊥ ∩ a⊥ )⊥ ∩ (b⊥ ∩ c⊥ )⊥ )⊥
13		oran 87	. . . . . . 7 (b ∪ a) = (b⊥ ∩ a⊥ )⊥
14		oran 87	. . . . . . 7 (b ∪ c) = (b⊥ ∩ c⊥ )⊥
15	13, 14	2an 79	. . . . . 6 ((b ∪ a) ∩ (b ∪ c)) = ((b⊥ ∩ a⊥ )⊥ ∩ (b⊥ ∩ c⊥ )⊥ )
16	15	ax-r1 35	. . . . 5 ((b⊥ ∩ a⊥ )⊥ ∩ (b⊥ ∩ c⊥ )⊥ ) = ((b ∪ a) ∩ (b ∪ c))
17	16	ax-r4 37	. . . 4 ((b⊥ ∩ a⊥ )⊥ ∩ (b⊥ ∩ c⊥ )⊥ )⊥ = ((b ∪ a) ∩ (b ∪ c))⊥
18	12, 17	ax-r2 36	. . 3 ((b⊥ ∩ a⊥ ) ∪ (b⊥ ∩ c⊥ )) = ((b ∪ a) ∩ (b ∪ c))⊥
19	5, 11, 18	3tr2 64	. 2 (b ∪ (a ∩ c))⊥ = ((b ∪ a) ∩ (b ∪ c))⊥
20	19	con1 66	1 (b ∪ (a ∩ c)) = ((b ∪ a) ∩ (b ∪ c))

Syntax hints:   = wb 1   C wc 3  ^⊥ wn 4   ∪ wo 6   ∩ wa 7

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:  fh4r  476  fh4c  478  df2i3  498  i3abs3  524  i3con  551  ud3lem1c  568  ud4lem1c  579  ud4lem1  581  ud5lem1  589  ud5lem3  594  u5lemaa  604  u4lemona  628  u3lemob  632  u3lemonb  637  u1lemc4  701  u2lemc4  702  u3lemc4  703  u4lemc4  704  u5lemc4  705  u4lem1  737  u2lem3  750  u1lem4  757  u4lem5  764  u5lem5  765  u4lem6  768  u5lem6  769  u3lem11  786  orbi  842  e2ast2  894