Quantum Logic Explorer

Quantum Logic Explorer

< Previous Next >
Related theorems
GIF version

Theorem ska4 415

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

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

**Proof of Theorem ska4**
Step	Hyp	Ref	Expression
1		dfnb 87	. . 3 (a ≡ b)^⊥ = ((a ∪ b) ∩ (a^⊥ ∪ b^⊥ ))
2		dfb 86	. . 3 ((a ∩ c) ≡ (b ∩ c)) = (((a ∩ c) ∩ (b ∩ c)) ∪ ((a ∩ c)^⊥ ∩ (b ∩ c)^⊥ ))
3	1, 2	2or 67	. 2 ((a ≡ b)^⊥ ∪ ((a ∩ c) ≡ (b ∩ c))) = (((a ∪ b) ∩ (a^⊥ ∪ b^⊥ )) ∪ (((a ∩ c) ∩ (b ∩ c)) ∪ ((a ∩ c)^⊥ ∩ (b ∩ c)^⊥ )))
4		ax-a2 30	. 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 31	. . 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 138	. . . . . . . . 9 (((a ∩ c)^⊥ ∩ (b ∩ c)^⊥ ) ∪ (a ∪ b)) ≤ 1
7		df-t 40	. . . . . . . . . . 11 1 = ((a^⊥ ∩ b^⊥ ) ∪ (a^⊥ ∩ b^⊥ )^⊥ )
8		oran 79	. . . . . . . . . . . . 13 (a ∪ b) = (a^⊥ ∩ b^⊥ )^⊥
9	8	lor 66	. . . . . . . . . . . 12 ((a^⊥ ∩ b^⊥ ) ∪ (a ∪ b)) = ((a^⊥ ∩ b^⊥ ) ∪ (a^⊥ ∩ b^⊥ )^⊥ )
10	9	ax-r1 34	. . . . . . . . . . 11 ((a^⊥ ∩ b^⊥ ) ∪ (a^⊥ ∩ b^⊥ )^⊥ ) = ((a^⊥ ∩ b^⊥ ) ∪ (a ∪ b))
11	7, 10	ax-r2 35	. . . . . . . . . 10 1 = ((a^⊥ ∩ b^⊥ ) ∪ (a ∪ 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^⊥ ) ∪ (a ∪ b)) ≤ (((a ∩ c)^⊥ ∩ (b ∩ c)^⊥ ) ∪ (a ∪ b))
18	11, 17	bltr 130	. . . . . . . . 9 1 ≤ (((a ∩ c)^⊥ ∩ (b ∩ c)^⊥ ) ∪ (a ∪ b))
19	6, 18	lebi 137	. . . . . . . 8 (((a ∩ c)^⊥ ∩ (b ∩ c)^⊥ ) ∪ (a ∪ b)) = 1
20	19	ran 71	. . . . . . 7 ((((a ∩ c)^⊥ ∩ (b ∩ c)^⊥ ) ∪ (a ∪ b)) ∩ (((a ∩ c)^⊥ ∩ (b ∩ c)^⊥ ) ∪ (a^⊥ ∪ b^⊥ ))) = (1 ∩ (((a ∩ c)^⊥ ∩ (b ∩ c)^⊥ ) ∪ (a^⊥ ∪ b^⊥ )))
21		ancom 68	. . . . . . 7 (1 ∩ (((a ∩ c)^⊥ ∩ (b ∩ c)^⊥ ) ∪ (a^⊥ ∪ b^⊥ ))) = ((((a ∩ c)^⊥ ∩ (b ∩ c)^⊥ ) ∪ (a^⊥ ∪ b^⊥ )) ∩ 1)
22		an1 98	. . . . . . 7 ((((a ∩ c)^⊥ ∩ (b ∩ c)^⊥ ) ∪ (a^⊥ ∪ b^⊥ )) ∩ 1) = (((a ∩ c)^⊥ ∩ (b ∩ c)^⊥ ) ∪ (a^⊥ ∪ b^⊥ ))
23	20, 21, 22	3tr 62	. . . . . 6 ((((a ∩ c)^⊥ ∩ (b ∩ c)^⊥ ) ∪ (a ∪ b)) ∩ (((a ∩ c)^⊥ ∩ (b ∩ c)^⊥ ) ∪ (a^⊥ ∪ b^⊥ ))) = (((a ∩ c)^⊥ ∩ (b ∩ c)^⊥ ) ∪ (a^⊥ ∪ b^⊥ ))
24	23	lor 66	. . . . 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 138	. . . . . 6 (((a ∩ c) ∩ (b ∩ c)) ∪ (((a ∩ c)^⊥ ∩ (b ∩ c)^⊥ ) ∪ (a^⊥ ∪ b^⊥ ))) ≤ 1
26		df-t 40	. . . . . . . 8 1 = (((a ∩ b) ∩ c) ∪ ((a ∩ b) ∩ c)^⊥ )
27		anandir 107	. . . . . . . . 9 ((a ∩ b) ∩ c) = ((a ∩ c) ∩ (b ∩ c))
28		oran3 85	. . . . . . . . . . . . 13 (a^⊥ ∪ b^⊥ ) = (a ∩ b)^⊥
29	28	ax-r5 37	. . . . . . . . . . . 12 ((a^⊥ ∪ b^⊥ ) ∪ c^⊥ ) = ((a ∩ b)^⊥ ∪ c^⊥ )
30		oran3 85	. . . . . . . . . . . 12 ((a ∩ b)^⊥ ∪ c^⊥ ) = ((a ∩ b) ∩ c)^⊥
31	29, 30	ax-r2 35	. . . . . . . . . . 11 ((a^⊥ ∪ b^⊥ ) ∪ c^⊥ ) = ((a ∩ b) ∩ c)^⊥
32	31	ax-r1 34	. . . . . . . . . 10 ((a ∩ b) ∩ c)^⊥ = ((a^⊥ ∪ b^⊥ ) ∪ c^⊥ )
33		ax-a2 30	. . . . . . . . . 10 ((a^⊥ ∪ b^⊥ ) ∪ c^⊥ ) = (c^⊥ ∪ (a^⊥ ∪ b^⊥ ))
34	32, 33	ax-r2 35	. . . . . . . . 9 ((a ∩ b) ∩ c)^⊥ = (c^⊥ ∪ (a^⊥ ∪ b^⊥ ))
35	27, 34	2or 67	. . . . . . . 8 (((a ∩ b) ∩ c) ∪ ((a ∩ b) ∩ c)^⊥ ) = (((a ∩ c) ∩ (b ∩ c)) ∪ (c^⊥ ∪ (a^⊥ ∪ b^⊥ )))
36	26, 35	ax-r2 35	. . . . . . 7 1 = (((a ∩ c) ∩ (b ∩ c)) ∪ (c^⊥ ∪ (a^⊥ ∪ 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^⊥ ∪ (a^⊥ ∪ b^⊥ )) ≤ (((a ∩ c)^⊥ ∩ (b ∩ c)^⊥ ) ∪ (a^⊥ ∪ b^⊥ ))
43	42	lelor 158	. . . . . . 7 (((a ∩ c) ∩ (b ∩ c)) ∪ (c^⊥ ∪ (a^⊥ ∪ b^⊥ ))) ≤ (((a ∩ c) ∩ (b ∩ c)) ∪ (((a ∩ c)^⊥ ∩ (b ∩ c)^⊥ ) ∪ (a^⊥ ∪ b^⊥ )))
44	36, 43	bltr 130	. . . . . 6 1 ≤ (((a ∩ c) ∩ (b ∩ c)) ∪ (((a ∩ c)^⊥ ∩ (b ∩ c)^⊥ ) ∪ (a^⊥ ∪ b^⊥ )))
45	25, 44	lebi 137	. . . . 5 (((a ∩ c) ∩ (b ∩ c)) ∪ (((a ∩ c)^⊥ ∩ (b ∩ c)^⊥ ) ∪ (a^⊥ ∪ b^⊥ ))) = 1
46	24, 45	ax-r2 35	. . . 4 (((a ∩ c) ∩ (b ∩ c)) ∪ ((((a ∩ c)^⊥ ∩ (b ∩ c)^⊥ ) ∪ (a ∪ b)) ∩ (((a ∩ c)^⊥ ∩ (b ∩ c)^⊥ ) ∪ (a^⊥ ∪ b^⊥ )))) = 1
47		wlea 370	. . . . . . . . . . 11 ((a ∩ c) ≤₂a) = 1
48		wleo 369	. . . . . . . . . . 11 (a ≤₂(a ∪ b)) = 1
49	47, 48	wletr 378	. . . . . . . . . 10 ((a ∩ c) ≤₂(a ∪ b)) = 1
50	49	wlecom 391	. . . . . . . . 9 C ((a ∩ c), (a ∪ b)) = 1
51	50	wcomcom 396	. . . . . . . 8 C ((a ∪ b), (a ∩ c)) = 1
52	51	wcomcom2 397	. . . . . . 7 C ((a ∪ b), (a ∩ c)^⊥ ) = 1
53		wlea 370	. . . . . . . . . . 11 ((b ∩ c) ≤₂b) = 1
54		wleo 369	. . . . . . . . . . . 12 (b ≤₂(b ∪ a)) = 1
55		ax-a2 30	. . . . . . . . . . . . 13 (b ∪ a) = (a ∪ b)
56	55	bi1 110	. . . . . . . . . . . 12 ((b ∪ a) ≡ (a ∪ b)) = 1
57	54, 56	wlbtr 380	. . . . . . . . . . 11 (b ≤₂(a ∪ b)) = 1
58	53, 57	wletr 378	. . . . . . . . . 10 ((b ∩ c) ≤₂(a ∪ b)) = 1
59	58	wlecom 391	. . . . . . . . 9 C ((b ∩ c), (a ∪ b)) = 1
60	59	wcomcom 396	. . . . . . . 8 C ((a ∪ b), (b ∩ c)) = 1
61	60	wcomcom2 397	. . . . . . 7 C ((a ∪ b), (b ∩ c)^⊥ ) = 1
62	52, 61	wcom2an 410	. . . . . 6 C ((a ∪ b), ((a ∩ c)^⊥ ∩ (b ∩ c)^⊥ )) = 1
63		wcomorr 394	. . . . . . . . 9 C (a, (a ∪ b)) = 1
64	63	wcomcom 396	. . . . . . . 8 C ((a ∪ b), a) = 1
65	64	wcomcom2 397	. . . . . . 7 C ((a ∪ b), a^⊥ ) = 1
66		wcomorr 394	. . . . . . . . . 10 C (b, (b ∪ a)) = 1
67	66, 56	wcbtr 393	. . . . . . . . 9 C (b, (a ∪ b)) = 1
68	67	wcomcom 396	. . . . . . . 8 C ((a ∪ b), b) = 1
69	68	wcomcom2 397	. . . . . . 7 C ((a ∪ b), b^⊥ ) = 1
70	65, 69	wcom2or 409	. . . . . 6 C ((a ∪ b), (a^⊥ ∪ b^⊥ )) = 1
71	62, 70	wfh4 408	. . . . 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 350	. . . 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 198	. . 3 (((a ∩ c) ∩ (b ∩ c)) ∪ (((a ∩ c)^⊥ ∩ (b ∩ c)^⊥ ) ∪ ((a ∪ b) ∩ (a^⊥ ∪ b^⊥ )))) = 1
74	5, 73	ax-r2 35	. 2 ((((a ∩ c) ∩ (b ∩ c)) ∪ ((a ∩ c)^⊥ ∩ (b ∩ c)^⊥ )) ∪ ((a ∪ b) ∩ (a^⊥ ∪ b^⊥ ))) = 1
75	3, 4, 74	3tr 62	1 ((a ≡ b)^⊥ ∪ ((a ∩ c) ≡ (b ∩ c))) = 1

Colors of variables: term

Syntax hints: = wb 1 ^⊥ wn 4 ≡ tb 5 ∪ wo 6 ∩ wa 7 1wt 9

This theorem is referenced by: wom2 416 u3lemax4 778

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