Theorem ska4 433

Description: Soundness theorem for Kalmbach's quantum propositional logic axiom KA4. (Contributed by NM, 9-Nov-1998.)

Assertion

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

Proof of Theorem ska4

Step	Hyp	Ref	Expression
1		dfnb 95	. . 3 (a ≡ b)⊥ = ((a ∪ b) ∩ (a⊥ ∪ b⊥ ))
2		dfb 94	. . 3 ((a ∩ c) ≡ (b ∩ c)) = (((a ∩ c) ∩ (b ∩ c)) ∪ ((a ∩ c)⊥ ∩ (b ∩ c)⊥ ))
3	1, 2	2or 72	. 2 ((a ≡ b)⊥ ∪ ((a ∩ c) ≡ (b ∩ c))) = (((a ∪ b) ∩ (a⊥ ∪ b⊥ )) ∪ (((a ∩ c) ∩ (b ∩ c)) ∪ ((a ∩ c)⊥ ∩ (b ∩ c)⊥ )))
4		ax-a2 31	. 2 (((a ∪ b) ∩ (a⊥ ∪ b⊥ )) ∪ (((a ∩ c) ∩ (b ∩ c)) ∪ ((a ∩ c)⊥ ∩ (b ∩ c)⊥ ))) = ((((a ∩ c) ∩ (b ∩ c)) ∪ ((a ∩ c)⊥ ∩ (b ∩ c)⊥ )) ∪ ((a ∪ b) ∩ (a⊥ ∪ b⊥ )))
5		ax-a3 32	. . 3 ((((a ∩ c) ∩ (b ∩ c)) ∪ ((a ∩ c)⊥ ∩ (b ∩ c)⊥ )) ∪ ((a ∪ b) ∩ (a⊥ ∪ b⊥ ))) = (((a ∩ c) ∩ (b ∩ c)) ∪ (((a ∩ c)⊥ ∩ (b ∩ c)⊥ ) ∪ ((a ∪ b) ∩ (a⊥ ∪ b⊥ ))))
6		le1 146	. . . . . . . . 9 (((a ∩ c)⊥ ∩ (b ∩ c)⊥ ) ∪ (a ∪ b)) ≤ 1
7		df-t 41	. . . . . . . . . . 11 1 = ((a⊥ ∩ b⊥ ) ∪ (a⊥ ∩ b⊥ )⊥ )
8		oran 87	. . . . . . . . . . . . 13 (a ∪ b) = (a⊥ ∩ b⊥ )⊥
9	8	lor 70	. . . . . . . . . . . 12 ((a⊥ ∩ b⊥ ) ∪ (a ∪ b)) = ((a⊥ ∩ b⊥ ) ∪ (a⊥ ∩ b⊥ )⊥ )
10	9	ax-r1 35	. . . . . . . . . . 11 ((a⊥ ∩ b⊥ ) ∪ (a⊥ ∩ b⊥ )⊥ ) = ((a⊥ ∩ b⊥ ) ∪ (a ∪ b))
11	7, 10	ax-r2 36	. . . . . . . . . 10 1 = ((a⊥ ∩ b⊥ ) ∪ (a ∪ 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⊥ ) ∪ (a ∪ b)) ≤ (((a ∩ c)⊥ ∩ (b ∩ c)⊥ ) ∪ (a ∪ b))
18	11, 17	bltr 138	. . . . . . . . 9 1 ≤ (((a ∩ c)⊥ ∩ (b ∩ c)⊥ ) ∪ (a ∪ b))
19	6, 18	lebi 145	. . . . . . . 8 (((a ∩ c)⊥ ∩ (b ∩ c)⊥ ) ∪ (a ∪ b)) = 1
20	19	ran 78	. . . . . . 7 ((((a ∩ c)⊥ ∩ (b ∩ c)⊥ ) ∪ (a ∪ b)) ∩ (((a ∩ c)⊥ ∩ (b ∩ c)⊥ ) ∪ (a⊥ ∪ b⊥ ))) = (1 ∩ (((a ∩ c)⊥ ∩ (b ∩ c)⊥ ) ∪ (a⊥ ∪ b⊥ )))
21		ancom 74	. . . . . . 7 (1 ∩ (((a ∩ c)⊥ ∩ (b ∩ c)⊥ ) ∪ (a⊥ ∪ b⊥ ))) = ((((a ∩ c)⊥ ∩ (b ∩ c)⊥ ) ∪ (a⊥ ∪ b⊥ )) ∩ 1)
22		an1 106	. . . . . . 7 ((((a ∩ c)⊥ ∩ (b ∩ c)⊥ ) ∪ (a⊥ ∪ b⊥ )) ∩ 1) = (((a ∩ c)⊥ ∩ (b ∩ c)⊥ ) ∪ (a⊥ ∪ b⊥ ))
23	20, 21, 22	3tr 65	. . . . . 6 ((((a ∩ c)⊥ ∩ (b ∩ c)⊥ ) ∪ (a ∪ b)) ∩ (((a ∩ c)⊥ ∩ (b ∩ c)⊥ ) ∪ (a⊥ ∪ b⊥ ))) = (((a ∩ c)⊥ ∩ (b ∩ c)⊥ ) ∪ (a⊥ ∪ b⊥ ))
24	23	lor 70	. . . . 5 (((a ∩ c) ∩ (b ∩ c)) ∪ ((((a ∩ c)⊥ ∩ (b ∩ c)⊥ ) ∪ (a ∪ b)) ∩ (((a ∩ c)⊥ ∩ (b ∩ c)⊥ ) ∪ (a⊥ ∪ b⊥ )))) = (((a ∩ c) ∩ (b ∩ c)) ∪ (((a ∩ c)⊥ ∩ (b ∩ c)⊥ ) ∪ (a⊥ ∪ b⊥ )))
25		le1 146	. . . . . 6 (((a ∩ c) ∩ (b ∩ c)) ∪ (((a ∩ c)⊥ ∩ (b ∩ c)⊥ ) ∪ (a⊥ ∪ b⊥ ))) ≤ 1
26		df-t 41	. . . . . . . 8 1 = (((a ∩ b) ∩ c) ∪ ((a ∩ b) ∩ c)⊥ )
27		anandir 115	. . . . . . . . 9 ((a ∩ b) ∩ c) = ((a ∩ c) ∩ (b ∩ c))
28		oran3 93	. . . . . . . . . . . . 13 (a⊥ ∪ b⊥ ) = (a ∩ b)⊥
29	28	ax-r5 38	. . . . . . . . . . . 12 ((a⊥ ∪ b⊥ ) ∪ c⊥ ) = ((a ∩ b)⊥ ∪ c⊥ )
30		oran3 93	. . . . . . . . . . . 12 ((a ∩ b)⊥ ∪ c⊥ ) = ((a ∩ b) ∩ c)⊥
31	29, 30	ax-r2 36	. . . . . . . . . . 11 ((a⊥ ∪ b⊥ ) ∪ c⊥ ) = ((a ∩ b) ∩ c)⊥
32	31	ax-r1 35	. . . . . . . . . 10 ((a ∩ b) ∩ c)⊥ = ((a⊥ ∪ b⊥ ) ∪ c⊥ )
33		ax-a2 31	. . . . . . . . . 10 ((a⊥ ∪ b⊥ ) ∪ c⊥ ) = (c⊥ ∪ (a⊥ ∪ b⊥ ))
34	32, 33	ax-r2 36	. . . . . . . . 9 ((a ∩ b) ∩ c)⊥ = (c⊥ ∪ (a⊥ ∪ b⊥ ))
35	27, 34	2or 72	. . . . . . . 8 (((a ∩ b) ∩ c) ∪ ((a ∩ b) ∩ c)⊥ ) = (((a ∩ c) ∩ (b ∩ c)) ∪ (c⊥ ∪ (a⊥ ∪ b⊥ )))
36	26, 35	ax-r2 36	. . . . . . 7 1 = (((a ∩ c) ∩ (b ∩ c)) ∪ (c⊥ ∪ (a⊥ ∪ 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⊥ ∪ (a⊥ ∪ b⊥ )) ≤ (((a ∩ c)⊥ ∩ (b ∩ c)⊥ ) ∪ (a⊥ ∪ b⊥ ))
43	42	lelor 166	. . . . . . 7 (((a ∩ c) ∩ (b ∩ c)) ∪ (c⊥ ∪ (a⊥ ∪ b⊥ ))) ≤ (((a ∩ c) ∩ (b ∩ c)) ∪ (((a ∩ c)⊥ ∩ (b ∩ c)⊥ ) ∪ (a⊥ ∪ b⊥ )))
44	36, 43	bltr 138	. . . . . 6 1 ≤ (((a ∩ c) ∩ (b ∩ c)) ∪ (((a ∩ c)⊥ ∩ (b ∩ c)⊥ ) ∪ (a⊥ ∪ b⊥ )))
45	25, 44	lebi 145	. . . . 5 (((a ∩ c) ∩ (b ∩ c)) ∪ (((a ∩ c)⊥ ∩ (b ∩ c)⊥ ) ∪ (a⊥ ∪ b⊥ ))) = 1
46	24, 45	ax-r2 36	. . . 4 (((a ∩ c) ∩ (b ∩ c)) ∪ ((((a ∩ c)⊥ ∩ (b ∩ c)⊥ ) ∪ (a ∪ b)) ∩ (((a ∩ c)⊥ ∩ (b ∩ c)⊥ ) ∪ (a⊥ ∪ b⊥ )))) = 1
47		wlea 388	. . . . . . . . . . 11 ((a ∩ c) ≤2 a) = 1
48		wleo 387	. . . . . . . . . . 11 (a ≤2 (a ∪ b)) = 1
49	47, 48	wletr 396	. . . . . . . . . 10 ((a ∩ c) ≤2 (a ∪ b)) = 1
50	49	wlecom 409	. . . . . . . . 9 C ((a ∩ c), (a ∪ b)) = 1
51	50	wcomcom 414	. . . . . . . 8 C ((a ∪ b), (a ∩ c)) = 1
52	51	wcomcom2 415	. . . . . . 7 C ((a ∪ b), (a ∩ c)⊥ ) = 1
53		wlea 388	. . . . . . . . . . 11 ((b ∩ c) ≤2 b) = 1
54		wleo 387	. . . . . . . . . . . 12 (b ≤2 (b ∪ a)) = 1
55		ax-a2 31	. . . . . . . . . . . . 13 (b ∪ a) = (a ∪ b)
56	55	bi1 118	. . . . . . . . . . . 12 ((b ∪ a) ≡ (a ∪ b)) = 1
57	54, 56	wlbtr 398	. . . . . . . . . . 11 (b ≤2 (a ∪ b)) = 1
58	53, 57	wletr 396	. . . . . . . . . 10 ((b ∩ c) ≤2 (a ∪ b)) = 1
59	58	wlecom 409	. . . . . . . . 9 C ((b ∩ c), (a ∪ b)) = 1
60	59	wcomcom 414	. . . . . . . 8 C ((a ∪ b), (b ∩ c)) = 1
61	60	wcomcom2 415	. . . . . . 7 C ((a ∪ b), (b ∩ c)⊥ ) = 1
62	52, 61	wcom2an 428	. . . . . 6 C ((a ∪ b), ((a ∩ c)⊥ ∩ (b ∩ c)⊥ )) = 1
63		wcomorr 412	. . . . . . . . 9 C (a, (a ∪ b)) = 1
64	63	wcomcom 414	. . . . . . . 8 C ((a ∪ b), a) = 1
65	64	wcomcom2 415	. . . . . . 7 C ((a ∪ b), a⊥ ) = 1
66		wcomorr 412	. . . . . . . . . 10 C (b, (b ∪ a)) = 1
67	66, 56	wcbtr 411	. . . . . . . . 9 C (b, (a ∪ b)) = 1
68	67	wcomcom 414	. . . . . . . 8 C ((a ∪ b), b) = 1
69	68	wcomcom2 415	. . . . . . 7 C ((a ∪ b), b⊥ ) = 1
70	65, 69	wcom2or 427	. . . . . 6 C ((a ∪ b), (a⊥ ∪ b⊥ )) = 1
71	62, 70	wfh4 426	. . . . 5 ((((a ∩ c)⊥ ∩ (b ∩ c)⊥ ) ∪ ((a ∪ b) ∩ (a⊥ ∪ b⊥ ))) ≡ ((((a ∩ c)⊥ ∩ (b ∩ c)⊥ ) ∪ (a ∪ b)) ∩ (((a ∩ c)⊥ ∩ (b ∩ c)⊥ ) ∪ (a⊥ ∪ b⊥ )))) = 1
72	71	wlor 368	. . . 4 ((((a ∩ c) ∩ (b ∩ c)) ∪ (((a ∩ c)⊥ ∩ (b ∩ c)⊥ ) ∪ ((a ∪ b) ∩ (a⊥ ∪ b⊥ )))) ≡ (((a ∩ c) ∩ (b ∩ c)) ∪ ((((a ∩ c)⊥ ∩ (b ∩ c)⊥ ) ∪ (a ∪ b)) ∩ (((a ∩ c)⊥ ∩ (b ∩ c)⊥ ) ∪ (a⊥ ∪ b⊥ ))))) = 1
73	46, 72	wwbmpr 206	. . 3 (((a ∩ c) ∩ (b ∩ c)) ∪ (((a ∩ c)⊥ ∩ (b ∩ c)⊥ ) ∪ ((a ∪ b) ∩ (a⊥ ∪ b⊥ )))) = 1
74	5, 73	ax-r2 36	. 2 ((((a ∩ c) ∩ (b ∩ c)) ∪ ((a ∩ c)⊥ ∩ (b ∩ c)⊥ )) ∪ ((a ∪ b) ∩ (a⊥ ∪ b⊥ ))) = 1
75	3, 4, 74	3tr 65	1 ((a ≡ b)⊥ ∪ ((a ∩ c) ≡ (b ∩ c))) = 1

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

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:  wom2  434  u3lemax4  796