Theorem ska4 415

Description: Soundness theorem for Kalmbach's quantum propositional logic axiom KA4.

Assertion

Ref	Expression
ska4	((a == b)_|_ v ((a ^ c) == (b ^ c))) = 1

Proof of Theorem ska4

Step	Hyp	Ref	Expression
1		dfnb 87	. . 3 (a == b)_|_ = ((a v b) ^ (a_|_ v b_|_))
2		dfb 86	. . 3 ((a ^ c) == (b ^ c)) = (((a ^ c) ^ (b ^ c)) v ((a ^ c)_|_ ^ (b ^ c)_|_))
3	1, 2	2or 67	. 2 ((a == b)_|_ v ((a ^ c) == (b ^ c))) = (((a v b) ^ (a_|_ v b_|_)) v (((a ^ c) ^ (b ^ c)) v ((a ^ c)_|_ ^ (b ^ c)_|_)))
4		ax-a2 30	. 2 (((a v b) ^ (a_|_ v b_|_)) v (((a ^ c) ^ (b ^ c)) v ((a ^ c)_|_ ^ (b ^ c)_|_))) = ((((a ^ c) ^ (b ^ c)) v ((a ^ c)_|_ ^ (b ^ c)_|_)) v ((a v b) ^ (a_|_ v b_|_)))
5		ax-a3 31	. . 3 ((((a ^ c) ^ (b ^ c)) v ((a ^ c)_|_ ^ (b ^ c)_|_)) v ((a v b) ^ (a_|_ v b_|_))) = (((a ^ c) ^ (b ^ c)) v (((a ^ c)_|_ ^ (b ^ c)_|_) v ((a v b) ^ (a_|_ v b_|_))))
6		le1 138	. . . . . . . . 9 (((a ^ c)_|_ ^ (b ^ c)_|_) v (a v b)) =< 1
7		df-t 40	. . . . . . . . . . 11 1 = ((a_|_ ^ b_|_) v (a_|_ ^ b_|_)_|_)
8		oran 79	. . . . . . . . . . . . 13 (a v b) = (a_|_ ^ b_|_)_|_
9	8	lor 66	. . . . . . . . . . . 12 ((a_|_ ^ b_|_) v (a v b)) = ((a_|_ ^ b_|_) v (a_|_ ^ b_|_)_|_)
10	9	ax-r1 34	. . . . . . . . . . 11 ((a_|_ ^ b_|_) v (a_|_ ^ b_|_)_|_) = ((a_|_ ^ b_|_) v (a v b))
11	7, 10	ax-r2 35	. . . . . . . . . 10 1 = ((a_|_ ^ b_|_) v (a v b))
12		lea 152	. . . . . . . . . . . . 13 (a ^ c) =< a
13	12	lecon 146	. . . . . . . . . . . 12 a_|_ =< (a ^ c)_|_
14		lea 152	. . . . . . . . . . . . 13 (b ^ c) =< b
15	14	lecon 146	. . . . . . . . . . . 12 b_|_ =< (b ^ c)_|_
16	13, 15	le2an 161	. . . . . . . . . . 11 (a_|_ ^ b_|_) =< ((a ^ c)_|_ ^ (b ^ c)_|_)
17	16	leror 144	. . . . . . . . . 10 ((a_|_ ^ b_|_) v (a v b)) =< (((a ^ c)_|_ ^ (b ^ c)_|_) v (a v b))
18	11, 17	bltr 130	. . . . . . . . 9 1 =< (((a ^ c)_|_ ^ (b ^ c)_|_) v (a v b))
19	6, 18	lebi 137	. . . . . . . 8 (((a ^ c)_|_ ^ (b ^ c)_|_) v (a v b)) = 1
20	19	ran 71	. . . . . . 7 ((((a ^ c)_|_ ^ (b ^ c)_|_) v (a v b)) ^ (((a ^ c)_|_ ^ (b ^ c)_|_) v (a_|_ v b_|_))) = (1 ^ (((a ^ c)_|_ ^ (b ^ c)_|_) v (a_|_ v b_|_)))
21		ancom 68	. . . . . . 7 (1 ^ (((a ^ c)_|_ ^ (b ^ c)_|_) v (a_|_ v b_|_))) = ((((a ^ c)_|_ ^ (b ^ c)_|_) v (a_|_ v b_|_)) ^ 1)
22		an1 98	. . . . . . 7 ((((a ^ c)_|_ ^ (b ^ c)_|_) v (a_|_ v b_|_)) ^ 1) = (((a ^ c)_|_ ^ (b ^ c)_|_) v (a_|_ v b_|_))
23	20, 21, 22	3tr 62	. . . . . 6 ((((a ^ c)_|_ ^ (b ^ c)_|_) v (a v b)) ^ (((a ^ c)_|_ ^ (b ^ c)_|_) v (a_|_ v b_|_))) = (((a ^ c)_|_ ^ (b ^ c)_|_) v (a_|_ v b_|_))
24	23	lor 66	. . . . 5 (((a ^ c) ^ (b ^ c)) v ((((a ^ c)_|_ ^ (b ^ c)_|_) v (a v b)) ^ (((a ^ c)_|_ ^ (b ^ c)_|_) v (a_|_ v b_|_)))) = (((a ^ c) ^ (b ^ c)) v (((a ^ c)_|_ ^ (b ^ c)_|_) v (a_|_ v b_|_)))
25		le1 138	. . . . . 6 (((a ^ c) ^ (b ^ c)) v (((a ^ c)_|_ ^ (b ^ c)_|_) v (a_|_ v b_|_))) =< 1
26		df-t 40	. . . . . . . 8 1 = (((a ^ b) ^ c) v ((a ^ b) ^ c)_|_)
27		anandir 107	. . . . . . . . 9 ((a ^ b) ^ c) = ((a ^ c) ^ (b ^ c))
28		oran3 85	. . . . . . . . . . . . 13 (a_|_ v b_|_) = (a ^ b)_|_
29	28	ax-r5 37	. . . . . . . . . . . 12 ((a_|_ v b_|_) v c_|_) = ((a ^ b)_|_ v c_|_)
30		oran3 85	. . . . . . . . . . . 12 ((a ^ b)_|_ v c_|_) = ((a ^ b) ^ c)_|_
31	29, 30	ax-r2 35	. . . . . . . . . . 11 ((a_|_ v b_|_) v c_|_) = ((a ^ b) ^ c)_|_
32	31	ax-r1 34	. . . . . . . . . 10 ((a ^ b) ^ c)_|_ = ((a_|_ v b_|_) v c_|_)
33		ax-a2 30	. . . . . . . . . 10 ((a_|_ v b_|_) v c_|_) = (c_|_ v (a_|_ v b_|_))
34	32, 33	ax-r2 35	. . . . . . . . 9 ((a ^ b) ^ c)_|_ = (c_|_ v (a_|_ v b_|_))
35	27, 34	2or 67	. . . . . . . 8 (((a ^ b) ^ c) v ((a ^ b) ^ c)_|_) = (((a ^ c) ^ (b ^ c)) v (c_|_ v (a_|_ v b_|_)))
36	26, 35	ax-r2 35	. . . . . . 7 1 = (((a ^ c) ^ (b ^ c)) v (c_|_ v (a_|_ v b_|_)))
37		lear 153	. . . . . . . . . . 11 (a ^ c) =< c
38	37	lecon 146	. . . . . . . . . 10 c_|_ =< (a ^ c)_|_
39		lear 153	. . . . . . . . . . 11 (b ^ c) =< c
40	39	lecon 146	. . . . . . . . . 10 c_|_ =< (b ^ c)_|_
41	38, 40	ler2an 165	. . . . . . . . 9 c_|_ =< ((a ^ c)_|_ ^ (b ^ c)_|_)
42	41	leror 144	. . . . . . . 8 (c_|_ v (a_|_ v b_|_)) =< (((a ^ c)_|_ ^ (b ^ c)_|_) v (a_|_ v b_|_))
43	42	lelor 158	. . . . . . 7 (((a ^ c) ^ (b ^ c)) v (c_|_ v (a_|_ v b_|_))) =< (((a ^ c) ^ (b ^ c)) v (((a ^ c)_|_ ^ (b ^ c)_|_) v (a_|_ v b_|_)))
44	36, 43	bltr 130	. . . . . 6 1 =< (((a ^ c) ^ (b ^ c)) v (((a ^ c)_|_ ^ (b ^ c)_|_) v (a_|_ v b_|_)))
45	25, 44	lebi 137	. . . . 5 (((a ^ c) ^ (b ^ c)) v (((a ^ c)_|_ ^ (b ^ c)_|_) v (a_|_ v b_|_))) = 1
46	24, 45	ax-r2 35	. . . 4 (((a ^ c) ^ (b ^ c)) v ((((a ^ c)_|_ ^ (b ^ c)_|_) v (a v b)) ^ (((a ^ c)_|_ ^ (b ^ c)_|_) v (a_|_ v b_|_)))) = 1
47		wlea 370	. . . . . . . . . . 11 ((a ^ c) =<2 a) = 1
48		wleo 369	. . . . . . . . . . 11 (a =<2 (a v b)) = 1
49	47, 48	wletr 378	. . . . . . . . . 10 ((a ^ c) =<2 (a v b)) = 1
50	49	wlecom 391	. . . . . . . . 9 C ((a ^ c), (a v b)) = 1
51	50	wcomcom 396	. . . . . . . 8 C ((a v b), (a ^ c)) = 1
52	51	wcomcom2 397	. . . . . . 7 C ((a v b), (a ^ c)_|_) = 1
53		wlea 370	. . . . . . . . . . 11 ((b ^ c) =<2 b) = 1
54		wleo 369	. . . . . . . . . . . 12 (b =<2 (b v a)) = 1
55		ax-a2 30	. . . . . . . . . . . . 13 (b v a) = (a v b)
56	55	bi1 110	. . . . . . . . . . . 12 ((b v a) == (a v b)) = 1
57	54, 56	wlbtr 380	. . . . . . . . . . 11 (b =<2 (a v b)) = 1
58	53, 57	wletr 378	. . . . . . . . . 10 ((b ^ c) =<2 (a v b)) = 1
59	58	wlecom 391	. . . . . . . . 9 C ((b ^ c), (a v b)) = 1
60	59	wcomcom 396	. . . . . . . 8 C ((a v b), (b ^ c)) = 1
61	60	wcomcom2 397	. . . . . . 7 C ((a v b), (b ^ c)_|_) = 1
62	52, 61	wcom2an 410	. . . . . 6 C ((a v b), ((a ^ c)_|_ ^ (b ^ c)_|_)) = 1
63		wcomorr 394	. . . . . . . . 9 C (a, (a v b)) = 1
64	63	wcomcom 396	. . . . . . . 8 C ((a v b), a) = 1
65	64	wcomcom2 397	. . . . . . 7 C ((a v b), a_|_) = 1
66		wcomorr 394	. . . . . . . . . 10 C (b, (b v a)) = 1
67	66, 56	wcbtr 393	. . . . . . . . 9 C (b, (a v b)) = 1
68	67	wcomcom 396	. . . . . . . 8 C ((a v b), b) = 1
69	68	wcomcom2 397	. . . . . . 7 C ((a v b), b_|_) = 1
70	65, 69	wcom2or 409	. . . . . 6 C ((a v b), (a_|_ v b_|_)) = 1
71	62, 70	wfh4 408	. . . . 5 ((((a ^ c)_|_ ^ (b ^ c)_|_) v ((a v b) ^ (a_|_ v b_|_))) == ((((a ^ c)_|_ ^ (b ^ c)_|_) v (a v b)) ^ (