Theorem fh2 470

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

Proof of Theorem fh2

Step	Hyp	Ref	Expression
1		ledi 174	. . 3 ((b ∩ a) ∪ (b ∩ c)) ≤ (b ∩ (a ∪ c))
2		oran 87	. . . . . . . . . . 11 ((b ∩ a) ∪ (b ∩ c)) = ((b ∩ a)⊥ ∩ (b ∩ c)⊥ )⊥
3		df-a 40	. . . . . . . . . . . . . 14 (b ∩ a) = (b⊥ ∪ a⊥ )⊥
4	3	con2 67	. . . . . . . . . . . . 13 (b ∩ a)⊥ = (b⊥ ∪ a⊥ )
5	4	ran 78	. . . . . . . . . . . 12 ((b ∩ a)⊥ ∩ (b ∩ c)⊥ ) = ((b⊥ ∪ a⊥ ) ∩ (b ∩ c)⊥ )
6	5	ax-r4 37	. . . . . . . . . . 11 ((b ∩ a)⊥ ∩ (b ∩ c)⊥ )⊥ = ((b⊥ ∪ a⊥ ) ∩ (b ∩ c)⊥ )⊥
7	2, 6	ax-r2 36	. . . . . . . . . 10 ((b ∩ a) ∪ (b ∩ c)) = ((b⊥ ∪ a⊥ ) ∩ (b ∩ c)⊥ )⊥
8	7	con2 67	. . . . . . . . 9 ((b ∩ a) ∪ (b ∩ c))⊥ = ((b⊥ ∪ a⊥ ) ∩ (b ∩ c)⊥ )
9	8	lan 77	. . . . . . . 8 ((b ∩ (a ∪ c)) ∩ ((b ∩ a) ∪ (b ∩ c))⊥ ) = ((b ∩ (a ∪ c)) ∩ ((b⊥ ∪ a⊥ ) ∩ (b ∩ c)⊥ ))
10		an4 86	. . . . . . . . 9 ((b ∩ (a ∪ c)) ∩ ((b⊥ ∪ a⊥ ) ∩ (b ∩ c)⊥ )) = ((b ∩ (b⊥ ∪ a⊥ )) ∩ ((a ∪ c) ∩ (b ∩ c)⊥ ))
11		fh.1	. . . . . . . . . . . . . 14 a C b
12	11	comcom 453	. . . . . . . . . . . . 13 b C a
13	12	comcom2 183	. . . . . . . . . . . 12 b C a⊥
14	13	com3ii 457	. . . . . . . . . . 11 (b ∩ (b⊥ ∪ a⊥ )) = (b ∩ a⊥ )
15		ancom 74	. . . . . . . . . . 11 (b ∩ a⊥ ) = (a⊥ ∩ b)
16	14, 15	ax-r2 36	. . . . . . . . . 10 (b ∩ (b⊥ ∪ a⊥ )) = (a⊥ ∩ b)
17	16	ran 78	. . . . . . . . 9 ((b ∩ (b⊥ ∪ a⊥ )) ∩ ((a ∪ c) ∩ (b ∩ c)⊥ )) = ((a⊥ ∩ b) ∩ ((a ∪ c) ∩ (b ∩ c)⊥ ))
18	10, 17	ax-r2 36	. . . . . . . 8 ((b ∩ (a ∪ c)) ∩ ((b⊥ ∪ a⊥ ) ∩ (b ∩ c)⊥ )) = ((a⊥ ∩ b) ∩ ((a ∪ c) ∩ (b ∩ c)⊥ ))
19	9, 18	ax-r2 36	. . . . . . 7 ((b ∩ (a ∪ c)) ∩ ((b ∩ a) ∪ (b ∩ c))⊥ ) = ((a⊥ ∩ b) ∩ ((a ∪ c) ∩ (b ∩ c)⊥ ))
20		an4 86	. . . . . . 7 ((a⊥ ∩ b) ∩ ((a ∪ c) ∩ (b ∩ c)⊥ )) = ((a⊥ ∩ (a ∪ c)) ∩ (b ∩ (b ∩ c)⊥ ))
21	19, 20	ax-r2 36	. . . . . 6 ((b ∩ (a ∪ c)) ∩ ((b ∩ a) ∪ (b ∩ c))⊥ ) = ((a⊥ ∩ (a ∪ c)) ∩ (b ∩ (b ∩ c)⊥ ))
22		ax-a1 30	. . . . . . . . . 10 a = a⊥ ⊥
23	22	ax-r5 38	. . . . . . . . 9 (a ∪ c) = (a⊥ ⊥ ∪ c)
24	23	lan 77	. . . . . . . 8 (a⊥ ∩ (a ∪ c)) = (a⊥ ∩ (a⊥ ⊥ ∪ c))
25		fh.2	. . . . . . . . . 10 a C c
26	25	comcom3 454	. . . . . . . . 9 a⊥ C c
27	26	com3ii 457	. . . . . . . 8 (a⊥ ∩ (a⊥ ⊥ ∪ c)) = (a⊥ ∩ c)
28	24, 27	ax-r2 36	. . . . . . 7 (a⊥ ∩ (a ∪ c)) = (a⊥ ∩ c)
29	28	ran 78	. . . . . 6 ((a⊥ ∩ (a ∪ c)) ∩ (b ∩ (b ∩ c)⊥ )) = ((a⊥ ∩ c) ∩ (b ∩ (b ∩ c)⊥ ))
30	21, 29	ax-r2 36	. . . . 5 ((b ∩ (a ∪ c)) ∩ ((b ∩ a) ∪ (b ∩ c))⊥ ) = ((a⊥ ∩ c) ∩ (b ∩ (b ∩ c)⊥ ))
31		anass 76	. . . . 5 ((a⊥ ∩ c) ∩ (b ∩ (b ∩ c)⊥ )) = (a⊥ ∩ (c ∩ (b ∩ (b ∩ c)⊥ )))
32	30, 31	ax-r2 36	. . . 4 ((b ∩ (a ∪ c)) ∩ ((b ∩ a) ∪ (b ∩ c))⊥ ) = (a⊥ ∩ (c ∩ (b ∩ (b ∩ c)⊥ )))
33		anass 76	. . . . . . . 8 ((b ∩ c) ∩ (b ∩ c)⊥ ) = (b ∩ (c ∩ (b ∩ c)⊥ ))
34	33	ax-r1 35	. . . . . . 7 (b ∩ (c ∩ (b ∩ c)⊥ )) = ((b ∩ c) ∩ (b ∩ c)⊥ )
35		an12 81	. . . . . . 7 (c ∩ (b ∩ (b ∩ c)⊥ )) = (b ∩ (c ∩ (b ∩ c)⊥ ))
36		dff 101	. . . . . . 7 0 = ((b ∩ c) ∩ (b ∩ c)⊥ )
37	34, 35, 36	3tr1 63	. . . . . 6 (c ∩ (b ∩ (b ∩ c)⊥ )) = 0
38	37	lan 77	. . . . 5 (a⊥ ∩ (c ∩ (b ∩ (b ∩ c)⊥ ))) = (a⊥ ∩ 0)
39		an0 108	. . . . 5 (a⊥ ∩ 0) = 0
40	38, 39	ax-r2 36	. . . 4 (a⊥ ∩ (c ∩ (b ∩ (b ∩ c)⊥ ))) = 0
41	32, 40	ax-r2 36	. . 3 ((b ∩ (a ∪ c)) ∩ ((b ∩ a) ∪ (b ∩ c))⊥ ) = 0
42	1, 41	oml3 452	. 2 ((b ∩ a) ∪ (b ∩ c)) = (b ∩ (a ∪ c))
43	42	ax-r1 35	1 (b ∩ (a ∪ c)) = ((b ∩ a) ∪ (b ∩ 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:  fh4  472  fh2r  474  fh2c  477  i3bi  496  ud3lem1a  566  ud4lem1a  577  ud4lem1b  578  ud5lem1a  586  ud5lem1b  587  ud5lem3a  591  ud5lem3b  592  u1lemle2  715  u2lemle2  716  u4lemle2  718  u21lembi  727  u1lem4  757  u4lem6  768  u3lem11  786  u3lem13b  790  2oath1  826  oale  829  mlalem  832  bi3  839  bi4  840  imp3  841  elimcons  868  mhlemlem1  874  mhlem  876  marsdenlem2  881  e2astlem1  895  oas  925