Theorem wfh2 424

Description: Weak structural analog of Foulis-Holland Theorem. (Contributed by NM, 13-Oct-1997.)

Hypotheses

Ref	Expression
wfh.1	C (a, b) = 1
wfh.2	C (a, c) = 1

Assertion

Ref	Expression
wfh2	((b ∩ (a ∪ c)) ≡ ((b ∩ a) ∪ (b ∩ c))) = 1

Proof of Theorem wfh2

Step	Hyp	Ref	Expression
1		wledi 405	. . 3 (((b ∩ a) ∪ (b ∩ c)) ≤2 (b ∩ (a ∪ c))) = 1
2		oran 87	. . . . . . . . . . . 12 ((b ∩ a) ∪ (b ∩ c)) = ((b ∩ a)⊥ ∩ (b ∩ c)⊥ )⊥
3	2	bi1 118	. . . . . . . . . . 11 (((b ∩ a) ∪ (b ∩ c)) ≡ ((b ∩ a)⊥ ∩ (b ∩ c)⊥ )⊥ ) = 1
4		df-a 40	. . . . . . . . . . . . . . 15 (b ∩ a) = (b⊥ ∪ a⊥ )⊥
5	4	bi1 118	. . . . . . . . . . . . . 14 ((b ∩ a) ≡ (b⊥ ∪ a⊥ )⊥ ) = 1
6	5	wcon2 208	. . . . . . . . . . . . 13 ((b ∩ a)⊥ ≡ (b⊥ ∪ a⊥ )) = 1
7	6	wran 369	. . . . . . . . . . . 12 (((b ∩ a)⊥ ∩ (b ∩ c)⊥ ) ≡ ((b⊥ ∪ a⊥ ) ∩ (b ∩ c)⊥ )) = 1
8	7	wr4 199	. . . . . . . . . . 11 (((b ∩ a)⊥ ∩ (b ∩ c)⊥ )⊥ ≡ ((b⊥ ∪ a⊥ ) ∩ (b ∩ c)⊥ )⊥ ) = 1
9	3, 8	wr2 371	. . . . . . . . . 10 (((b ∩ a) ∪ (b ∩ c)) ≡ ((b⊥ ∪ a⊥ ) ∩ (b ∩ c)⊥ )⊥ ) = 1
10	9	wcon2 208	. . . . . . . . 9 (((b ∩ a) ∪ (b ∩ c))⊥ ≡ ((b⊥ ∪ a⊥ ) ∩ (b ∩ c)⊥ )) = 1
11	10	wlan 370	. . . . . . . 8 (((b ∩ (a ∪ c)) ∩ ((b ∩ a) ∪ (b ∩ c))⊥ ) ≡ ((b ∩ (a ∪ c)) ∩ ((b⊥ ∪ a⊥ ) ∩ (b ∩ c)⊥ ))) = 1
12		an4 86	. . . . . . . . . 10 ((b ∩ (a ∪ c)) ∩ ((b⊥ ∪ a⊥ ) ∩ (b ∩ c)⊥ )) = ((b ∩ (b⊥ ∪ a⊥ )) ∩ ((a ∪ c) ∩ (b ∩ c)⊥ ))
13	12	bi1 118	. . . . . . . . 9 (((b ∩ (a ∪ c)) ∩ ((b⊥ ∪ a⊥ ) ∩ (b ∩ c)⊥ )) ≡ ((b ∩ (b⊥ ∪ a⊥ )) ∩ ((a ∪ c) ∩ (b ∩ c)⊥ ))) = 1
14		wfh.1	. . . . . . . . . . . . . 14 C (a, b) = 1
15	14	wcomcom 414	. . . . . . . . . . . . 13 C (b, a) = 1
16	15	wcomcom2 415	. . . . . . . . . . . 12 C (b, a⊥ ) = 1
17	16	wcom3ii 419	. . . . . . . . . . 11 ((b ∩ (b⊥ ∪ a⊥ )) ≡ (b ∩ a⊥ )) = 1
18		ancom 74	. . . . . . . . . . . 12 (b ∩ a⊥ ) = (a⊥ ∩ b)
19	18	bi1 118	. . . . . . . . . . 11 ((b ∩ a⊥ ) ≡ (a⊥ ∩ b)) = 1
20	17, 19	wr2 371	. . . . . . . . . 10 ((b ∩ (b⊥ ∪ a⊥ )) ≡ (a⊥ ∩ b)) = 1
21	20	wran 369	. . . . . . . . 9 (((b ∩ (b⊥ ∪ a⊥ )) ∩ ((a ∪ c) ∩ (b ∩ c)⊥ )) ≡ ((a⊥ ∩ b) ∩ ((a ∪ c) ∩ (b ∩ c)⊥ ))) = 1
22	13, 21	wr2 371	. . . . . . . 8 (((b ∩ (a ∪ c)) ∩ ((b⊥ ∪ a⊥ ) ∩ (b ∩ c)⊥ )) ≡ ((a⊥ ∩ b) ∩ ((a ∪ c) ∩ (b ∩ c)⊥ ))) = 1
23	11, 22	wr2 371	. . . . . . 7 (((b ∩ (a ∪ c)) ∩ ((b ∩ a) ∪ (b ∩ c))⊥ ) ≡ ((a⊥ ∩ b) ∩ ((a ∪ c) ∩ (b ∩ c)⊥ ))) = 1
24		an4 86	. . . . . . . 8 ((a⊥ ∩ b) ∩ ((a ∪ c) ∩ (b ∩ c)⊥ )) = ((a⊥ ∩ (a ∪ c)) ∩ (b ∩ (b ∩ c)⊥ ))
25	24	bi1 118	. . . . . . 7 (((a⊥ ∩ b) ∩ ((a ∪ c) ∩ (b ∩ c)⊥ )) ≡ ((a⊥ ∩ (a ∪ c)) ∩ (b ∩ (b ∩ c)⊥ ))) = 1
26	23, 25	wr2 371	. . . . . 6 (((b ∩ (a ∪ c)) ∩ ((b ∩ a) ∪ (b ∩ c))⊥ ) ≡ ((a⊥ ∩ (a ∪ c)) ∩ (b ∩ (b ∩ c)⊥ ))) = 1
27		ax-a1 30	. . . . . . . . . . 11 a = a⊥ ⊥
28	27	bi1 118	. . . . . . . . . 10 (a ≡ a⊥ ⊥ ) = 1
29	28	wr5-2v 366	. . . . . . . . 9 ((a ∪ c) ≡ (a⊥ ⊥ ∪ c)) = 1
30	29	wlan 370	. . . . . . . 8 ((a⊥ ∩ (a ∪ c)) ≡ (a⊥ ∩ (a⊥ ⊥ ∪ c))) = 1
31		wfh.2	. . . . . . . . . 10 C (a, c) = 1
32	31	wcomcom3 416	. . . . . . . . 9 C (a⊥ , c) = 1
33	32	wcom3ii 419	. . . . . . . 8 ((a⊥ ∩ (a⊥ ⊥ ∪ c)) ≡ (a⊥ ∩ c)) = 1
34	30, 33	wr2 371	. . . . . . 7 ((a⊥ ∩ (a ∪ c)) ≡ (a⊥ ∩ c)) = 1
35	34	wran 369	. . . . . 6 (((a⊥ ∩ (a ∪ c)) ∩ (b ∩ (b ∩ c)⊥ )) ≡ ((a⊥ ∩ c) ∩ (b ∩ (b ∩ c)⊥ ))) = 1
36	26, 35	wr2 371	. . . . 5 (((b ∩ (a ∪ c)) ∩ ((b ∩ a) ∪ (b ∩ c))⊥ ) ≡ ((a⊥ ∩ c) ∩ (b ∩ (b ∩ c)⊥ ))) = 1
37		anass 76	. . . . . 6 ((a⊥ ∩ c) ∩ (b ∩ (b ∩ c)⊥ )) = (a⊥ ∩ (c ∩ (b ∩ (b ∩ c)⊥ )))
38	37	bi1 118	. . . . 5 (((a⊥ ∩ c) ∩ (b ∩ (b ∩ c)⊥ )) ≡ (a⊥ ∩ (c ∩ (b ∩ (b ∩ c)⊥ )))) = 1
39	36, 38	wr2 371	. . . 4 (((b ∩ (a ∪ c)) ∩ ((b ∩ a) ∪ (b ∩ c))⊥ ) ≡ (a⊥ ∩ (c ∩ (b ∩ (b ∩ c)⊥ )))) = 1
40		anass 76	. . . . . . . . 9 ((b ∩ c) ∩ (b ∩ c)⊥ ) = (b ∩ (c ∩ (b ∩ c)⊥ ))
41	40	bi1 118	. . . . . . . 8 (((b ∩ c) ∩ (b ∩ c)⊥ ) ≡ (b ∩ (c ∩ (b ∩ c)⊥ ))) = 1
42	41	wr1 197	. . . . . . 7 ((b ∩ (c ∩ (b ∩ c)⊥ )) ≡ ((b ∩ c) ∩ (b ∩ c)⊥ )) = 1
43		an12 81	. . . . . . . 8 (c ∩ (b ∩ (b ∩ c)⊥ )) = (b ∩ (c ∩ (b ∩ c)⊥ ))
44	43	bi1 118	. . . . . . 7 ((c ∩ (b ∩ (b ∩ c)⊥ )) ≡ (b ∩ (c ∩ (b ∩ c)⊥ ))) = 1
45		dff 101	. . . . . . . 8 0 = ((b ∩ c) ∩ (b ∩ c)⊥ )
46	45	bi1 118	. . . . . . 7 (0 ≡ ((b ∩ c) ∩ (b ∩ c)⊥ )) = 1
47	42, 44, 46	w3tr1 374	. . . . . 6 ((c ∩ (b ∩ (b ∩ c)⊥ )) ≡ 0) = 1
48	47	wlan 370	. . . . 5 ((a⊥ ∩ (c ∩ (b ∩ (b ∩ c)⊥ ))) ≡ (a⊥ ∩ 0)) = 1
49		an0 108	. . . . . 6 (a⊥ ∩ 0) = 0
50	49	bi1 118	. . . . 5 ((a⊥ ∩ 0) ≡ 0) = 1
51	48, 50	wr2 371	. . . 4 ((a⊥ ∩ (c ∩ (b ∩ (b ∩ c)⊥ ))) ≡ 0) = 1
52	39, 51	wr2 371	. . 3 (((b ∩ (a ∪ c)) ∩ ((b ∩ a) ∪ (b ∩ c))⊥ ) ≡ 0) = 1
53	1, 52	wom5 381	. 2 (((b ∩ a) ∪ (b ∩ c)) ≡ (b ∩ (a ∪ c))) = 1
54	53	wr1 197	1 ((b ∩ (a ∪ c)) ≡ ((b ∩ a) ∪ (b ∩ c))) = 1

This proof depends on syntax axioms:   = wb 1  ^⊥ wn 4   ≡ tb 5   ∪ wo 6   ∩ wa 7  1wt 8  0wf 9   C wcmtr 29

This proof depends on 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-wom 361

This proof depends on definitions:  df-b 39  df-a 40  df-t 41  df-f 42  df-i1 44  df-i2 45  df-le 129  df-le1 130  df-le2 131  df-cmtr 134

This theorem is used by:  wfh4  426