Theorem woml6 418

Description: Variant of weakly orthomodular law.

Assertion

Ref	Expression
woml6	((a ->1 b)_|_ v (a ->2 b)) = 1

Proof of Theorem woml6

Step	Hyp	Ref	Expression
1		df-i1 43	. . . . . 6 (a ->1 b) = (a_|_ v (a ^ b))
2		df-a 39	. . . . . . 7 (a ^ b) = (a_|_ v b_|_)_|_
3	2	lor 66	. . . . . 6 (a_|_ v (a ^ b)) = (a_|_ v (a_|_ v b_|_)_|_)
4	1, 3	ax-r2 35	. . . . 5 (a ->1 b) = (a_|_ v (a_|_ v b_|_)_|_)
5	4	ax-r4 36	. . . 4 (a ->1 b)_|_ = (a_|_ v (a_|_ v b_|_)_|_)_|_
6		df-a 39	. . . . 5 (a ^ (a_|_ v b_|_)) = (a_|_ v (a_|_ v b_|_)_|_)_|_
7	6	ax-r1 34	. . . 4 (a_|_ v (a_|_ v b_|_)_|_)_|_ = (a ^ (a_|_ v b_|_))
8	5, 7	ax-r2 35	. . 3 (a ->1 b)_|_ = (a ^ (a_|_ v b_|_))
9		df-i2 44	. . 3 (a ->2 b) = (b v (a_|_ ^ b_|_))
10	8, 9	2or 67	. 2 ((a ->1 b)_|_ v (a ->2 b)) = ((a ^ (a_|_ v b_|_)) v (b v (a_|_ ^ b_|_)))
11		ax-a2 30	. . . . 5 ((a ^ (a_|_ v b_|_)) v b) = (b v (a ^ (a_|_ v b_|_)))
12		ancom 68	. . . . . 6 (a ^ (a_|_ v b_|_)) = ((a_|_ v b_|_) ^ a)
13	12	lor 66	. . . . 5 (b v (a ^ (a_|_ v b_|_))) = (b v ((a_|_ v b_|_) ^ a))
14	11, 13	ax-r2 35	. . . 4 ((a ^ (a_|_ v b_|_)) v b) = (b v ((a_|_ v b_|_) ^ a))
15	14	ax-r5 37	. . 3 (((a ^ (a_|_ v b_|_)) v b) v (a_|_ ^ b_|_)) = ((b v ((a_|_ v b_|_) ^ a)) v (a_|_ ^ b_|_))
16		ax-a3 31	. . 3 (((a ^ (a_|_ v b_|_)) v b) v (a_|_ ^ b_|_)) = ((a ^ (a_|_ v b_|_)) v (b v (a_|_ ^ b_|_)))
17		1b 109	. . . . 5 (1 == ((b v ((a_|_ v b_|_) ^ a)) v (a_|_ ^ b_|_))) = ((b v ((a_|_ v b_|_) ^ a)) v (a_|_ ^ b_|_))
18	17	ax-r1 34	. . . 4 ((b v ((a_|_ v b_|_) ^ a)) v (a_|_ ^ b_|_)) = (1 == ((b v ((a_|_ v b_|_) ^ a)) v (a_|_ ^ b_|_)))
19		wcomorr 394	. . . . . . . . . . . 12 C (b_|_, (b_|_ v a_|_)) = 1
20		ax-a2 30	. . . . . . . . . . . . 13 (b_|_ v a_|_) = (a_|_ v b_|_)
21	20	bi1 110	. . . . . . . . . . . 12 ((b_|_ v a_|_) == (a_|_ v b_|_)) = 1
22	19, 21	wcbtr 393	. . . . . . . . . . 11 C (b_|_, (a_|_ v b_|_)) = 1
23	22	wcomcom 396	. . . . . . . . . 10 C ((a_|_ v b_|_), b_|_) = 1
24	23	wcomcom3 398	. . . . . . . . 9 C ((a_|_ v b_|_)_|_, b_|_) = 1
25	24	wcomcom5 402	. . . . . . . 8 C ((a_|_ v b_|_), b) = 1
26		wcomorr 394	. . . . . . . . . . 11 C (a_|_, (a_|_ v b_|_)) = 1
27	26	wcomcom 396	. . . . . . . . . 10 C ((a_|_ v b_|_), a_|_) = 1
28	27	wcomcom3 398	. . . . . . . . 9 C ((a_|_ v b_|_)_|_, a_|_) = 1
29	28	wcomcom5 402	. . . . . . . 8 C ((a_|_ v b_|_), a) = 1
30	25, 29	wfh4 408	. . . . . . 7 ((b v ((a_|_ v b_|_) ^ a)) == ((b v (a_|_ v b_|_)) ^ (b v a))) = 1
31	30	wr5-2v 348	. . . . . 6 (((b v ((a_|_ v b_|_) ^ a)) v (a_|_ ^ b_|_)) == (((b v (a_|_ v b_|_)) ^ (b v a)) v (a_|_ ^ b_|_))) = 1
32		or12 73	. . . . . . . . . . . . 13 (b v (a_|_ v b_|_)) = (a_|_ v (b v b_|_))
33		df-t 40	. . . . . . . . . . . . . . 15 1 = (b v b_|_)
34	33	lor 66	. . . . . . . . . . . . . 14 (a_|_ v 1) = (a_|_ v (b v b_|_))
35	34	ax-r1 34	. . . . . . . . . . . . 13 (a_|_ v (b v b_|_)) = (a_|_ v 1)
36		or1 96	. . . . . . . . . . . . 13 (a_|_ v 1) = 1
37	32, 35, 36	3tr 62	. . . . . . . . . . . 12 (b v (a_|_ v b_|_)) = 1
38	37	ran 71	. . . . . . . . . . 11 ((b v (a_|_ v b_|_)) ^ (b v a)) = (1 ^ (b v a))
39		ancom 68	. . . . . . . . . . 11 (1 ^ (b v a)) = ((b v a) ^ 1)
40	38, 39	ax-r2 35	. . . . . . . . . 10 ((b v (a_|_ v b_|_)) ^ (b v a)) = ((b v a) ^ 1)
41		an1 98	. . . . . . . . . 10 ((b v a) ^ 1) = (b v a)
42		ax-a2 30	. . . . . . . . . 10 (b v a) = (a v b)
43	40, 41, 42	3tr 62	. . . . . . . . 9 ((b v (a_|_ v b_|_)) ^ (b v a)) = (a v b)
44		anor3 82	. . . . . . . . 9 (a_|_ ^ b_|_) = (a v b)_|_
45	43, 44	2or 67	. . . . . . . 8 (((b v (a_|_ v b_|_)) ^ (b v a)) v (a_|_ ^ b_|_)) = ((a v b) v (a v b)_|_)
46		df-t 40	. . . . . . . . 9 1 = ((a v b) v (a v b)_|_)
47	46	ax-r1 34	. . . . . . . 8 ((a v b) v (a v b)_|_) = 1
48	45, 47	ax-r2 35	. . . . . . 7 (((b v (a_|_ v b_|_)) ^ (b v a)) v (a_|_ ^ b_|_)) = 1
49	48	bi1 110	. . . . . 6 ((((b v (a_|_ v b_|_)) ^ (b v a)) v (a_|_ ^ b_|_)) == 1) = 1
50	31, 49	wr2 353	. . . . 5 (((b v ((a_|_ v b_|_) ^ a)) v (a_|_ ^ b_|_)) == 1) = 1
51	50	wr1 189	. . . 4 (1 == ((b v ((a_|_ v b_|_) ^ a)) v (a_|_ ^ b_|_))) = 1
52	18, 51	ax-r2 35	. . 3 ((b v ((a_|_ v b_|_) ^ a)) v (a_|_ ^ b_|_)) = 1
53	15, 16, 52	3tr2 61	. 2 ((a ^ (a_|_ v b_|_)) v (b v (a_|_ ^ b_|_))) = 1
54	10, 53	ax-r2 35	1 ((a ->1 b)_|_ v (a ->2 b)) = 1

Syntax hints:   = wb 1  _|_wn 4   == tb 5   v wo 6   ^ wa 7  1wt 9   ->1 wi1 13   ->2 wi2 14

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

This theorem depends on definitions:  df-b 38  df-a 39  df-t 40  df-f 41  df-i1 43  df-i2 44  df-le 121  df-le1 122  df-le2 123  df-cmtr 126

metamath.org