Theorem fh2 470

Description: Foulis-Holland Theorem.

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 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

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

Copyright terms: Public domain