Theorem fh2 456

Description: Foulis-Holland Theorem.

Hypotheses

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

Assertion

Ref	Expression
fh2	(b ^ (a v c)) = ((b ^ a) v (b ^ c))

Proof of Theorem fh2

Step	Hyp	Ref	Expression
1		ledi 168	. . 3 ((b ^ a) v (b ^ c)) =< (b ^ (a v c))
2		oran 81	. . . . . . . . . . 11 ((b ^ a) v (b ^ c)) = ((b ^ a)' ^ (b ^ c)')'
3		df-a 40	. . . . . . . . . . . . . 14 (b ^ a) = (b' v a')'
4	3	con2 65	. . . . . . . . . . . . 13 (b ^ a)' = (b' v a')
5	4	ran 72	. . . . . . . . . . . 12 ((b ^ a)' ^ (b ^ c)') = ((b' v a') ^ (b ^ c)')
6	5	ax-r4 37	. . . . . . . . . . 11 ((b ^ a)' ^ (b ^ c)')' = ((b' v a') ^ (b ^ c)')'
7	2, 6	ax-r2 36	. . . . . . . . . 10 ((b ^ a) v (b ^ c)) = ((b' v a') ^ (b ^ c)')'
8	7	con2 65	. . . . . . . . 9 ((b ^ a) v (b ^ c))' = ((b' v a') ^ (b ^ c)')
9	8	lan 71	. . . . . . . 8 ((b ^ (a v c)) ^ ((b ^ a) v (b ^ c))') = ((b ^ (a v c)) ^ ((b' v a') ^ (b ^ c)'))
10		an4 80	. . . . . . . . 9 ((b ^ (a v c)) ^ ((b' v a') ^ (b ^ c)')) = ((b ^ (b' v a')) ^ ((a v c) ^ (b ^ c)'))
11		fh.1	. . . . . . . . . . . . . 14 a C b
12	11	comcom 439	. . . . . . . . . . . . 13 b C a
13	12	comcom2 177	. . . . . . . . . . . 12 b C a'
14	13	com3ii 443	. . . . . . . . . . 11 (b ^ (b' v a')) = (b ^ a')
15		ancom 69	. . . . . . . . . . 11 (b ^ a') = (a' ^ b)
16	14, 15	ax-r2 36	. . . . . . . . . 10 (b ^ (b' v a')) = (a' ^ b)
17	16	ran 72	. . . . . . . . 9 ((b ^ (b' v a')) ^ ((a v c) ^ (b ^ c)')) = ((a' ^ b) ^ ((a v c) ^ (b ^ c)'))
18	10, 17	ax-r2 36	. . . . . . . 8 ((b ^ (a v c)) ^ ((b' v a') ^ (b ^ c)')) = ((a' ^ b) ^ ((a v c) ^ (b ^ c)'))
19	9, 18	ax-r2 36	. . . . . . 7 ((b ^ (a v c)) ^ ((b ^ a) v (b ^ c))') = ((a' ^ b) ^ ((a v c) ^ (b ^ c)'))
20		an4 80	. . . . . . 7 ((a' ^ b) ^ ((a v c) ^ (b ^ c)')) = ((a' ^ (a v c)) ^ (b ^ (b ^ c)'))
21	19, 20	ax-r2 36	. . . . . 6 ((b ^ (a v c)) ^ ((b ^ a) v (b ^ c))') = ((a' ^ (a v c)) ^ (b ^ (b ^ c)'))
22		ax-a1 30	. . . . . . . . . 10 a = a''
23	22	ax-r5 38	. . . . . . . . 9 (a v c) = (a'' v c)
24	23	lan 71	. . . . . . . 8 (a' ^ (a v c)) = (a' ^ (a'' v c))
25		fh.2	. . . . . . . . . 10 a C c
26	25	comcom3 440	. . . . . . . . 9 a' C c
27	26	com3ii 443	. . . . . . . 8 (a' ^ (a'' v c)) = (a' ^ c)
28	24, 27	ax-r2 36	. . . . . . 7 (a' ^ (a v c)) = (a' ^ c)
29	28	ran 72	. . . . . 6 ((a' ^ (a v c)) ^ (b ^ (b ^ c)')) = ((a' ^ c) ^ (b ^ (b ^ c)'))
30	21, 29	ax-r2 36	. . . . 5 ((b ^ (a v c)) ^ ((b ^ a) v (b ^ c))') = ((a' ^ c) ^ (b ^ (b ^ c)'))
31		anass 70	. . . . 5 ((a' ^ c) ^ (b ^ (b ^ c)')) = (a' ^ (c ^ (b ^ (b ^ c)')))
32	30, 31	ax-r2 36	. . . 4 ((b ^ (a v c)) ^ ((b ^ a) v (b ^ c))') = (a' ^ (c ^ (b ^ (b ^ c)')))
33		anass 70	. . . . . . . 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 75	. . . . . . 7 (c ^ (b ^ (b ^ c)')) = (b ^ (c ^ (b ^ c)'))
36		dff 95	. . . . . . 7 0 = ((b ^ c) ^ (b ^ c)')
37	34, 35, 36	3tr1 61	. . . . . 6 (c ^ (b ^ (b ^ c)')) = 0
38	37	lan 71	. . . . 5 (a' ^ (c ^ (b ^ (b ^ c)'))) = (a' ^ 0)
39		an0 102	. . . . 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 v c)) ^ ((b ^ a) v (b ^ c))') = 0
42	1, 41	oml3 438	. 2 ((b ^ a) v (b ^ c)) = (b ^ (a v c))
43	42	ax-r1 35	1 (b ^ (a v c)) = ((b ^ a) v (b ^ c))

Syntax hints:   = wb 1   C wc 3  'wn 4   v wo 6   ^ wa 7  0wf 9

This theorem is referenced by:  fh4 458  fh2r 460  fh2c 463  i3bi 482  ud3lem1a 552  ud4lem1a 563  ud4lem1b 564  ud5lem1a 572  ud5lem1b 573  ud5lem3a 577  ud5lem3b 578  u1lemle2 701  u2lemle2 702  u4lemle2 704  u21lembi 713  u1lem4 743  u4lem6 754  u3lem11 772  u3lem13b 776  2oath1 812  oale 815  mlalem 818  bi3 825  bi4 826  imp3 827  elimcons 854  mhlemlem1 860  mhlem 862  marsdenlem2 867  e2astlem1 881  oas 911

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 425

This theorem depends on definitions:  df-b 39  df-a 40  df-t 41  df-f 42  df-le1 124  df-le2 125  df-c1 126  df-c2 127

Copyright terms: Public domain