Theorem ska4 433

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 95	. . 3 (a == b)' = ((a v b) ^ (a' v b'))
2		dfb 94	. . 3 ((a ^ c) == (b ^ c)) = (((a ^ c) ^ (b ^ c)) v ((a ^ c)' ^ (b ^ c)'))
3	1, 2	2or 72	. 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 31	. 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 32	. . 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 146	. . . . . . . . 9 (((a ^ c)' ^ (b ^ c)') v (a v b)) =< 1
7		df-t 41	. . . . . . . . . . 11 1 = ((a' ^ b') v (a' ^ b')')
8		oran 87	. . . . . . . . . . . . 13 (a v b) = (a' ^ b')'
9	8	lor 70	. . . . . . . . . . . 12 ((a' ^ b') v (a v b)) = ((a' ^ b') v (a' ^ b')')
10	9	ax-r1 35	. . . . . . . . . . 11 ((a' ^ b') v (a' ^ b')') = ((a' ^ b') v (a v b))
11	7, 10	ax-r2 36	. . . . . . . . . 10 1 = ((a' ^ b') v (a v b))
12		lea 160	. . . . . . . . . . . . 13 (a ^ c) =< a
13	12	lecon 154	. . . . . . . . . . . 12 a' =< (a ^ c)'
14		lea 160	. . . . . . . . . . . . 13 (b ^ c) =< b
15	14	lecon 154	. . . . . . . . . . . 12 b' =< (b ^ c)'
16	13, 15	le2an 169	. . . . . . . . . . 11 (a' ^ b') =< ((a ^ c)' ^ (b ^ c)')
17	16	leror 152	. . . . . . . . . 10 ((a' ^ b') v (a v b)) =< (((a ^ c)' ^ (b ^ c)') v (a v b))
18	11, 17	bltr 138	. . . . . . . . 9 1 =< (((a ^ c)' ^ (b ^ c)') v (a v b))
19	6, 18	lebi 145	. . . . . . . 8 (((a ^ c)' ^ (b ^ c)') v (a v b)) = 1
20	19	ran 78	. . . . . . 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 74	. . . . . . 7 (1 ^ (((a ^ c)' ^ (b ^ c)') v (a' v b'))) = ((((a ^ c)' ^ (b ^ c)') v (a' v b')) ^ 1)
22		an1 106	. . . . . . 7 ((((a ^ c)' ^ (b ^ c)') v (a' v b')) ^ 1) = (((a ^ c)' ^ (b ^ c)') v (a' v b'))
23	20, 21, 22	3tr 65	. . . . . 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 70	. . . . 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 146	. . . . . 6 (((a ^ c) ^ (b ^ c)) v (((a ^ c)' ^ (b ^ c)') v (a' v b'))) =< 1
26		df-t 41	. . . . . . . 8 1 = (((a ^ b) ^ c) v ((a ^ b) ^ c)')
27		anandir 115	. . . . . . . . 9 ((a ^ b) ^ c) = ((a ^ c) ^ (b ^ c))
28		oran3 93	. . . . . . . . . . . . 13 (a' v b') = (a ^ b)'
29	28	ax-r5 38	. . . . . . . . . . . 12 ((a' v b') v c') = ((a ^ b)' v c')
30		oran3 93	. . . . . . . . . . . 12 ((a ^ b)' v c') = ((a ^ b) ^ c)'
31	29, 30	ax-r2 36	. . . . . . . . . . 11 ((a' v b') v c') = ((a ^ b) ^ c)'
32	31	ax-r1 35	. . . . . . . . . 10 ((a ^ b) ^ c)' = ((a' v b') v c')
33		ax-a2 31	. . . . . . . . . 10 ((a' v b') v c') = (c' v (a' v b'))
34	32, 33	ax-r2 36	. . . . . . . . 9 ((a ^ b) ^ c)' = (c' v (a' v b'))
35	27, 34	2or 72	. . . . . . . 8 (((a ^ b) ^ c) v ((a ^ b) ^ c)') = (((a ^ c) ^ (b ^ c)) v (c' v (a' v b')))
36	26, 35	ax-r2 36	. . . . . . 7 1 = (((a ^ c) ^ (b ^ c)) v (c' v (a' v b')))
37		lear 161	. . . . . . . . . . 11 (a ^ c) =< c
38	37	lecon 154	. . . . . . . . . 10 c' =< (a ^ c)'
39		lear 161	. . . . . . . . . . 11 (b ^ c) =< c
40	39	lecon 154	. . . . . . . . . 10 c' =< (b ^ c)'
41	38, 40	ler2an 173	. . . . . . . . 9 c' =< ((a ^ c)' ^ (b ^ c)')
42	41	leror 152	. . . . . . . 8 (c' v (a' v b')) =< (((a ^ c)' ^ (b ^ c)') v (a' v b'))
43	42	lelor 166	. . . . . . 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 138	. . . . . 6 1 =< (((a ^ c) ^ (b ^ c)) v (((a ^ c)' ^ (b ^ c)') v (a' v b')))
45	25, 44	lebi 145	. . . . 5 (((a ^ c) ^ (b ^ c)) v (((a ^ c)' ^ (b ^ c)') v (a' v b'))) = 1
46	24, 45	ax-r2 36	. . . 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 388	. . . . . . . . . . 11 ((a ^ c) =<2 a) = 1
48		wleo 387	. . . . . . . . . . 11 (a =<2 (a v b)) = 1
49	47, 48	wletr 396	. . . . . . . . . 10 ((a ^ c) =<2 (a v b)) = 1
50	49	wlecom 409	. . . . . . . . 9 C ((a ^ c), (a v b)) = 1
51	50	wcomcom 414	. . . . . . . 8 C ((a v b), (a ^ c)) = 1
52	51	wcomcom2 415	. . . . . . 7 C ((a v b), (a ^ c)') = 1
53		wlea 388	. . . . . . . . . . 11 ((b ^ c) =<2 b) = 1
54		wleo 387	. . . . . . . . . . . 12 (b =<2 (b v a)) = 1
55		ax-a2 31	. . . . . . . . . . . . 13 (b v a) = (a v b)
56	55	bi1 118	. . . . . . . . . . . 12 ((b v a) == (a v b)) = 1
57	54, 56	wlbtr 398	. . . . . . . . . . 11 (b =<2 (a v b)) = 1
58	53, 57	wletr 396	. . . . . . . . . 10 ((b ^ c) =<2 (a v b)) = 1
59	58	wlecom 409	. . . . . . . . 9 C ((b ^ c), (a v b)) = 1
60	59	wcomcom 414	. . . . . . . 8 C ((a v b), (b ^ c)) = 1
61	60	wcomcom2 415	. . . . . . 7 C ((a v b), (b ^ c)') = 1
62	52, 61	wcom2an 428	. . . . . 6 C ((a v b), ((a ^ c)' ^ (b ^ c)')) = 1
63		wcomorr 412	. . . . . . . . 9 C (a, (a v b)) = 1
64	63	wcomcom 414	. . . . . . . 8 C ((a v b), a) = 1
65	64	wcomcom2 415	. . . . . . 7 C ((a v b), a') = 1
66		wcomorr 412	. . . . . . . . . 10 C (b, (b v a)) = 1
67	66, 56	wcbtr 411	. . . . . . . . 9 C (b, (a v b)) = 1
68	67	wcomcom 414	. . . . . . . 8 C ((a v b), b) = 1
69	68	wcomcom2 415	. . . . . . 7 C ((a v b), b') = 1
70	65, 69	wcom2or 427	. . . . . 6 C ((a v b), (a' v b')) = 1
71	62, 70	wfh4 426	. . . . 5 ((((a ^ c)' ^ (b ^ c)') v ((