Theorem fh2 452

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 166	. . 3 ((b ^ a) v (b ^ c)) =< (b ^ (a v c))
2		oran 79	. . . . . . . . . . 11 ((b ^ a) v (b ^ c)) = ((b ^ a)_|_ ^ (b ^ c)_|_)_|_
3		df-a 39	. . . . . . . . . . . . . 14 (b ^ a) = (b_|_ v a_|_)_|_
4	3	con2 64	. . . . . . . . . . . . 13 (b ^ a)_|_ = (b_|_ v a_|_)
5	4	ran 71	. . . . . . . . . . . 12 ((b ^ a)_|_ ^ (b ^ c)_|_) = ((b_|_ v a_|_) ^ (b ^ c)_|_)
6	5	ax-r4 36	. . . . . . . . . . 11 ((b ^ a)_|_ ^ (b ^ c)_|_)_|_ = ((b_|_ v a_|_) ^ (b ^ c)_|_)_|_
7	2, 6	ax-r2 35	. . . . . . . . . 10 ((b ^ a) v (b ^ c)) = ((b_|_ v a_|_) ^ (b ^ c)_|_)_|_
8	7	con2 64	. . . . . . . . 9 ((b ^ a) v (b ^ c))_|_ = ((b_|_ v a_|_) ^ (b ^ c)_|_)
9	8	lan 70	. . . . . . . 8 ((b ^ (a v c)) ^ ((b ^ a) v (b ^ c))_|_) = ((b ^ (a v c)) ^ ((b_|_ v a_|_) ^ (b ^ c)_|_))
10		an4 78	. . . . . . . . 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 435	. . . . . . . . . . . . 13 b C a
13	12	comcom2 175	. . . . . . . . . . . 12 b C a_|_
14	13	com3ii 439	. . . . . . . . . . 11 (b ^ (b_|_ v a_|_)) = (b ^ a_|_)
15		ancom 68	. . . . . . . . . . 11 (b ^ a_|_) = (a_|_ ^ b)
16	14, 15	ax-r2 35	. . . . . . . . . 10 (b ^ (b_|_ v a_|_)) = (a_|_ ^ b)
17	16	ran 71	. . . . . . . . 9 ((b ^ (b_|_ v a_|_)) ^ ((a v c) ^ (b ^ c)_|_)) = ((a_|_ ^ b) ^ ((a v c) ^ (b ^ c)_|_))
18	10, 17	ax-r2 35	. . . . . . . 8 ((b ^ (a v c)) ^ ((b_|_ v a_|_) ^ (b ^ c)_|_)) = ((a_|_ ^ b) ^ ((a v c) ^ (b ^ c)_|_))
19	9, 18	ax-r2 35	. . . . . . 7 ((b ^ (a v c)) ^ ((b ^ a) v (b ^ c))_|_) = ((a_|_ ^ b) ^ ((a v c) ^ (b ^ c)_|_))
20		an4 78	. . . . . . 7 ((a_|_ ^ b) ^ ((a v c) ^ (b ^ c)_|_)) = ((a_|_ ^ (a v c)) ^ (b ^ (b ^ c)_|_))
21	19, 20	ax-r2 35	. . . . . 6 ((b ^ (a v c)) ^ ((b ^ a) v (b ^ c))_|_) = ((a_|_ ^ (a v c)) ^ (b ^ (b ^ c)_|_))
22		ax-a1 29	. . . . . . . . . 10 a = a_|__|_
23	22	ax-r5 37	. . . . . . . . 9 (a v c) = (a_|__|_ v c)
24	23	lan 70	. . . . . . . 8 (a_|_ ^ (a v c)) = (a_|_ ^ (a_|__|_ v c))
25		fh.2	. . . . . . . . . 10 a C c
26	25	comcom3 436	. . . . . . . . 9 a_|_ C c
27	26	com3ii 439	. . . . . . . 8 (a_|_ ^ (a_|__|_ v c)) = (a_|_ ^ c)
28	24, 27	ax-r2 35	. . . . . . 7 (a_|_ ^ (a v c)) = (a_|_ ^ c)
29	28	ran 71	. . . . . 6 ((a_|_ ^ (a v c)) ^ (b ^ (b ^ c)_|_)) = ((a_|_ ^ c) ^ (b ^ (b ^ c)_|_))
30	21, 29	ax-r2 35	. . . . 5 ((b ^ (a v c)) ^ ((b ^ a) v (b ^ c))_|_) = ((a_|_ ^ c) ^ (b ^ (b ^ c)_|_))
31		anass 69	. . . . 5 ((a_|_ ^ c) ^ (b ^ (b ^ c)_|_)) = (a_|_ ^ (c ^ (b ^ (b ^ c)_|_)))
32	30, 31	ax-r2 35	. . . 4 ((b ^ (a v c)) ^ ((b ^ a) v (b ^ c))_|_) = (a_|_ ^ (c ^ (b ^ (b ^ c)_|_)))
33		anass 69	. . . . . . . 8 ((b ^ c) ^ (b ^ c)_|_) = (b ^ (c ^ (b ^ c)_|_))
34	33	ax-r1 34	. . . . . . 7 (b ^ (c ^ (b ^ c)_|_)) = ((b ^ c) ^ (b ^ c)_|_)
35		an12 74	. . . . . . 7 (c ^ (b ^ (b ^ c)_|_)) = (b ^ (c ^ (b ^ c)_|_))
36		dff 93	. . . . . . 7 0 = ((b ^ c) ^ (b ^ c)_|_)
37	34, 35, 36	3tr1 60	. . . . . 6 (c ^ (b ^ (b ^ c)_|_)) = 0
38	37	lan 70	. . . . 5 (a_|_ ^ (c ^ (b ^ (b ^ c)_|_))) = (a_|_ ^ 0)
39		an0 100	. . . . 5 (a_|_ ^ 0) = 0
40	38, 39	ax-r2 35	. . . 4 (a_|_ ^ (c ^ (b ^ (b ^ c)_|_))) = 0
41	32, 40	ax-r2 35	. . 3 ((b ^ (a v c)) ^ ((b ^ a) v (b ^ c))_|_) = 0
42	1, 41	oml3 434	. 2 ((b ^ a) v (b ^ c)) = (b ^ (a v c))
43	42	ax-r1 34	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 10

This theorem is referenced by:  fh4 454  fh2r 456  fh2c 459  i3bi 478  ud3lem1a 548  ud4lem1a 559  ud4lem1b 560  ud5lem1a 568  ud5lem1b 569  ud5lem3a 573  ud5lem3b 574  u1lemle2 697  u2lemle2 698  u4lemle2 700  u21lembi 709  u1lem4 739  u4lem6 750  u3lem11 768  u3lem13b 772  2oath1 808  oale 811  mlalem 814  bi3 821  bi4 822  imp3 823  elimcons 850  mhlemlem1 856  mhlem 858  marsdenlem2 863  oas 905

This theorem was proved from axioms:  ax-a1 29  ax-a2 30  ax-a3 31  ax-a4 32  ax-a5 33  ax-r1 34  ax-r2 35  ax-r4 36  ax-r5 37  ax-r3 421

This theorem depends on definitions:  df-b 38  df-a 39  df-t 40  df-f 41  df-le1 122  df-le2 123  df-c1 124  df-c2 125

metamath.org