Theorem atoml 10309

Description: An assertion holding in atomic orthomodular lattices that is equivalent to the exchange axiom. Proposition 3.2.17 of [PtakPulmannova] p. 66.

Hypothesis

Ref	Expression
atoml.1	|- A e. CH

Assertion

Ref	Expression
atoml	|- (B e. Atoms -> ((A vH B) i^i (_|_` A)) e. (Atoms u. {0H}))

Proof of Theorem atoml

Step	Hyp	Ref	Expression
1		atelch 10271	. . . . . . . . 9 |- (B e. Atoms -> B e. CH)
2		atoml.1	. . . . . . . . . 10 |- A e. CH
3		chjclt 9329	. . . . . . . . . 10 |- ((A e. CH /\ B e. CH) -> (A vH B) e. CH)
4	2, 3	mpan 695	. . . . . . . . 9 |- (B e. CH -> (A vH B) e. CH)
5	1, 4	syl 10	. . . . . . . 8 |- (B e. Atoms -> (A vH B) e. CH)
6	2	choccl 9185	. . . . . . . . 9 |- (_|_` A) e. CH
7		chinclt 9422	. . . . . . . . 9 |- (((A vH B) e. CH /\ (_|_` A) e. CH) -> ((A vH B) i^i (_|_` A)) e. CH)
8	6, 7	mpan2 696	. . . . . . . 8 |- ((A vH B) e. CH -> ((A vH B) i^i (_|_` A)) e. CH)
9		hatomict 10287	. . . . . . . . 9 |- ((((A vH B) i^i (_|_` A)) e. CH /\ ((A vH B) i^i (_|_` A)) =/= 0H) -> E.x e. Atoms x (_ ((A vH B) i^i (_|_` A)))
10	9	ex 373	. . . . . . . 8 |- (((A vH B) i^i (_|_` A)) e. CH -> (((A vH B) i^i (_|_` A)) =/= 0H -> E.x e. Atoms x (_ ((A vH B) i^i (_|_` A))))
11	5, 8, 10	3syl 20	. . . . . . 7 |- (B e. Atoms -> (((A vH B) i^i (_|_` A)) =/= 0H -> E.x e. Atoms x (_ ((A vH B) i^i (_|_` A))))
12	11	imp 350	. . . . . 6 |- ((B e. Atoms /\ ((A vH B) i^i (_|_` A)) =/= 0H) -> E.x e. Atoms x (_ ((A vH B) i^i (_|_` A)))
13		pjoml3t 9555	. . . . . . . . . . . . . . . . . . . 20 |- (((_|_` A) e. CH /\ x e. CH) -> (x (_ (_|_` A) -> ((_|_` A) i^i ((_|_` (_|_` A)) vH x)) = x))
14	6, 13	mpan 695	. . . . . . . . . . . . . . . . . . 19 |- (x e. CH -> (x (_ (_|_` A) -> ((_|_` A) i^i ((_|_` (_|_` A)) vH x)) = x))
15	14	imp 350	. . . . . . . . . . . . . . . . . 18 |- ((x e. CH /\ x (_ (_|_` A)) -> ((_|_` A) i^i ((_|_` (_|_` A)) vH x)) = x)
16	2	pjococ 9270	. . . . . . . . . . . . . . . . . . . . 21 |- (_|_` (_|_` A)) = A
17	16	opreq1i 3971	. . . . . . . . . . . . . . . . . . . 20 |- ((_|_` (_|_` A)) vH x) = (A vH x)
18	17	ineq1i 2213	. . . . . . . . . . . . . . . . . . 19 |- (((_|_` (_|_` A)) vH x) i^i (_|_` A)) = ((A vH x) i^i (_|_` A))
19		incom 2208	. . . . . . . . . . . . . . . . . . 19 |- (((_|_` (_|_` A)) vH x) i^i (_|_` A)) = ((_|_` A) i^i ((_|_` (_|_` A)) vH x))
20	18, 19	eqtr3 1497	. . . . . . . . . . . . . . . . . 18 |- ((A vH x) i^i (_|_` A)) = ((_|_` A) i^i ((_|_` (_|_` A)) vH x))
21	15, 20	syl5eq 1519	. . . . . . . . . . . . . . . . 17 |- ((x e. CH /\ x (_ (_|_` A)) -> ((A vH x) i^i (_|_` A)) = x)
22		atelch 10271	. . . . . . . . . . . . . . . . 17 |- (x e. Atoms -> x e. CH)
23		inss2 2231	. . . . . . . . . . . . . . . . . 18 |- ((A vH B) i^i (_|_` A)) (_ (_|_` A)
24		sstr 2072	. . . . . . . . . . . . . . . . . 18 |- ((x (_ ((A vH B) i^i (_|_` A)) /\ ((A vH B) i^i (_|_` A)) (_ (_|_` A)) -> x (_ (_|_` A))
25	23, 24	mpan2 696	. . . . . . . . . . . . . . . . 17 |- (x (_ ((A vH B) i^i (_|_` A)) -> x (_ (_|_` A))
26	21, 22, 25	syl2an 454	. . . . . . . . . . . . . . . 16 |- ((x e. Atoms /\ x (_ ((A vH B) i^i (_|_` A))) -> ((A vH x) i^i (_|_` A)) = x)
27	26	ad2ant2lr 410	. . . . . . . . . . . . . . 15 |- (((B e. Atoms /\ x e. Atoms) /\ (x (_ ((A vH B) i^i (_|_` A)) /\ ((A vH B) i^i (_|_` A)) =/= 0H)) -> ((A vH x) i^i (_|_` A)) = x)
28		chub1t 9430	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ((A e. CH /\ B e. CH) -> A (_ (A vH B))
29	2, 28	mpan 695	. . . . . . . . . . . . . . . . . . . . . . 23 |- (B e. CH -> A (_ (A vH B))
30	29	adantr 389	. . . . . . . . . . . . . . . . . . . . . 22 |- ((B e. CH /\ x e. CH) -> A (_ (A vH B))
31		chlubt 9432	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ((A e. CH /\ x e. CH /\ (A vH B) e. CH) -> ((A (_ (A vH B) /\ x (_ (A vH B)) <-> (A vH x) (_ (A vH B)))
32	2, 31	mp3an1 903	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ((x e. CH /\ (A vH B) e. CH) -> ((A (_ (A vH B) /\ x (_ (A vH B)) <-> (A vH x) (_ (A vH B)))
33	32, 4	sylan2 451	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ((x e. CH /\ B e. CH) -> ((A (_ (A vH B) /\ x (_ (A vH B)) <-> (A vH x) (_ (A vH B)))
34	33	biimpd 153	. . . . . . . . . . . . . . . . . . . . . . 23 |- ((x e. CH /\ B e. CH) -> ((A (_ (A vH B) /\ x (_ (A vH B)) -> (A vH x) (_ (A vH B)))
35	34	ancoms 436	. . . . . . . . . . . . . . . . . . . . . 22 |- ((B e. CH /\ x e. CH) -> ((A (_ (A vH B) /\ x (_ (A vH B)) -> (A vH x) (_ (A vH B)))
36	30, 35	mpand 701	. . . . . . . . . . . . . . . . . . . . 21 |- ((B e. CH /\ x e. CH) -> (x (_ (A vH B) -> (A vH x) (_ (A vH B)))
37	36, 1, 22	syl2an 454	. . . . . . . . . . . . . . . . . . . 20 |- ((B e. Atoms /\ x e. Atoms) -> (x (_ (A vH B) -> (A vH x) (_ (A vH B)))
38	37	imp 350	. . . . . . . . . . . . . . . . . . 19 |- (((B e. Atoms /\ x e. Atoms) /\ x (_ (A vH B)) -> (A vH x) (_ (A vH B))
39		inss1 2230	. . . . . . . . . . . . . . . . . . . 20 |- ((A vH B) i^i (_|_` A)) (_ (A vH B)
40		sstr 2072	. . . . . . . . . . . . . . . . . . . 20 |- ((x (_ ((A vH B) i^i (_|_` A)) /\ ((A vH B) i^i (_|_` A)) (_ (A vH B)) -> x (_ (A vH B))
41	39, 40	mpan2 696	. . . . . . . . . . . . . . . . . . 19 |- (x (_ ((A vH B) i^i (_|_` A)) -> x (_ (A vH B))
42	38, 41	sylan2 451	. . . . . . . . . . . . . . . . . 18 |- (((B e. Atoms /\ x e. Atoms) /\ x (_ ((A vH B) i^i (_|_` A))) -> (A vH x) (_ (A vH B))
43	42	adantrr 395	. . . . . . . . . . . . . . . . 17 |- (((B e. Atoms /\ x e. Atoms) /\ (x (_ ((A vH B) i^i (_|_` A)) /\ ((A vH B) i^i (_|_` A)) =/= 0H)) -> (A vH x) (_ (A vH B))
44		chlubt 9432	. . . . . . . . . . . . . . . . . . . . . . 23 |- ((A e. CH /\ B e. CH /\ (A vH x) e. CH) -> ((A (_ (A vH x) /\ B (_ (A vH x)) <-> (A vH B) (_ (A vH x)))
45	2, 44	mp3an1 903	. . . . . . . . . . . . . . . . . . . . . 22 |- ((B e. CH /\ (A vH x) e. CH) -> ((A (_ (A vH x) /\ B (_ (A vH x)) <-> (A vH B) (_ (A vH x)))
46	45	biimpd 153	. . . . . . . . . . . . . . . . . . . . 21 |- ((B e. CH /\ (A vH x) e. CH) -> ((A (_ (A vH x) /\ B (_ (A vH x)) -> (A vH B) (_ (A vH x)))
47	46	exp3a 375	. . . . . . . . . . . . . . . . . . . 20 |- ((B e. CH /\ (A vH x) e. CH) -> (A (_ (A vH x) -> (B (_ (A vH x) -> (A vH B) (_ (A vH x))))
48	47	com23 32	. . . . . . . . . . . . . . . . . . 19 |- ((B e. CH /\ (A vH x) e. CH) -> (B (_ (A vH x) -> (A (_ (A vH x) -> (A vH B) (_ (A vH x))))
49	48	imp 350	. . . . . . . . . . . . . . . . . 18 |- (((B e. CH /\ (A vH x) e. CH) /\ B (_ (A vH x)) -> (A (_ (A vH x) -> (A vH B) (_ (A vH x)))
50		chjclt 9329	. . . . . . . . . . . . . . . . . . . . . . 23 |- ((A e. CH /\ x e. CH) -> (A vH x) e. CH)
51	2, 50	mpan 695	. . . . . . . . . . . . . . . . . . . . . 22 |- (x e. CH -> (A vH x) e. CH)
52	22, 51	syl 10	. . . . . . . . . . . . . . . . . . . . 21 |- (x e. Atoms -> (A vH x) e. CH)
53	1, 52	anim12i 333	. . . . . . . . . . . . . . . . . . . 20 |- ((B e. Atoms /\ x e. Atoms) -> (B e. CH /\ (A vH x) e. CH))
54	53	adantr 389	. . . . . . . . . . . . . . . . . . 19 |- (((B e. Atoms /\ x e. Atoms) /\ (x (_ ((A vH B) i^i (_|_` A)) /\ ((A vH B) i^i (_|_` A)) =/= 0H)) -> (B e. CH /\ (A vH x) e. CH))
55		atexcht 10308	. . . . . . . . . . . . . . . . . . . . 21 |- ((A e. CH /\ x e. Atoms /\ B e. Atoms) -> ((x (_ (A vH B) /\ (A i^i x) = 0H) -> B (_ (A vH x)))
56	2, 55	mp3an1 903	. . . . . . . . . . . . . . . . . . . 20 |- ((x e. Atoms /\ B e. Atoms) -> ((x (_ (A vH B) /\ (A i^i x) = 0H) -> B (_ (A vH x)))
57		pm3.22 438	. . . . . . . . . . . . . . . . . . . . 21 |- ((B e. Atoms /\ x e.