Metamath Proof Explorer

Theorem atomli

Description: An assertion holding in atomic orthomodular lattices that is equivalent to the exchange axiom. Proposition 3.2.17 of PtakPulmannova p. 66. (Contributed by NM, 24-Jun-2004) (New usage is discouraged.)

Ref Expression
Hypothesis atoml.1 
|- A e. CH
Assertion atomli 
|- ( B e. HAtoms -> ( ( A vH B ) i^i ( _|_ ` A ) ) e. ( HAtoms u. { 0H } ) )

Proof

Step Hyp Ref Expression
1 atoml.1 
 |-  A e. CH
2 atelch 
 |-  ( B e. HAtoms -> B e. CH )
3 chjcl 
 |-  ( ( A e. CH /\ B e. CH ) -> ( A vH B ) e. CH )
4 1 2 3 sylancr 
 |-  ( B e. HAtoms -> ( A vH B ) e. CH )
5 1 choccli 
 |-  ( _|_ ` A ) e. CH
6 chincl 
 |-  ( ( ( A vH B ) e. CH /\ ( _|_ ` A ) e. CH ) -> ( ( A vH B ) i^i ( _|_ ` A ) ) e. CH )
7 4 5 6 sylancl 
 |-  ( B e. HAtoms -> ( ( A vH B ) i^i ( _|_ ` A ) ) e. CH )
8 hatomic 
 |-  ( ( ( ( A vH B ) i^i ( _|_ ` A ) ) e. CH /\ ( ( A vH B ) i^i ( _|_ ` A ) ) =/= 0H ) -> E. x e. HAtoms x C_ ( ( A vH B ) i^i ( _|_ ` A ) ) )
9 7 8 sylan 
 |-  ( ( B e. HAtoms /\ ( ( A vH B ) i^i ( _|_ ` A ) ) =/= 0H ) -> E. x e. HAtoms x C_ ( ( A vH B ) i^i ( _|_ ` A ) ) )
10 atelch 
 |-  ( x e. HAtoms -> x e. CH )
11 inss2 
 |-  ( ( A vH B ) i^i ( _|_ ` A ) ) C_ ( _|_ ` A )
12 sstr 
 |-  ( ( x C_ ( ( A vH B ) i^i ( _|_ ` A ) ) /\ ( ( A vH B ) i^i ( _|_ ` A ) ) C_ ( _|_ ` A ) ) -> x C_ ( _|_ ` A ) )
13 11 12 mpan2 
 |-  ( x C_ ( ( A vH B ) i^i ( _|_ ` A ) ) -> x C_ ( _|_ ` A ) )
14 1 pjococi 
 |-  ( _|_ ` ( _|_ ` A ) ) = A
15 14 oveq1i 
 |-  ( ( _|_ ` ( _|_ ` A ) ) vH x ) = ( A vH x )
16 15 ineq1i 
 |-  ( ( ( _|_ ` ( _|_ ` A ) ) vH x ) i^i ( _|_ ` A ) ) = ( ( A vH x ) i^i ( _|_ ` A ) )
17 incom 
 |-  ( ( ( _|_ ` ( _|_ ` A ) ) vH x ) i^i ( _|_ ` A ) ) = ( ( _|_ ` A ) i^i ( ( _|_ ` ( _|_ ` A ) ) vH x ) )
18 16 17 eqtr3i 
 |-  ( ( A vH x ) i^i ( _|_ ` A ) ) = ( ( _|_ ` A ) i^i ( ( _|_ ` ( _|_ ` A ) ) vH x ) )
19 pjoml3 
 |-  ( ( ( _|_ ` A ) e. CH /\ x e. CH ) -> ( x C_ ( _|_ ` A ) -> ( ( _|_ ` A ) i^i ( ( _|_ ` ( _|_ ` A ) ) vH x ) ) = x ) )
20 5 19 mpan 
 |-  ( x e. CH -> ( x C_ ( _|_ ` A ) -> ( ( _|_ ` A ) i^i ( ( _|_ ` ( _|_ ` A ) ) vH x ) ) = x ) )
21 20 imp 
 |-  ( ( x e. CH /\ x C_ ( _|_ ` A ) ) -> ( ( _|_ ` A ) i^i ( ( _|_ ` ( _|_ ` A ) ) vH x ) ) = x )
22 18 21 syl5eq 
 |-  ( ( x e. CH /\ x C_ ( _|_ ` A ) ) -> ( ( A vH x ) i^i ( _|_ ` A ) ) = x )
23 10 13 22 syl2an 
 |-  ( ( x e. HAtoms /\ x C_ ( ( A vH B ) i^i ( _|_ ` A ) ) ) -> ( ( A vH x ) i^i ( _|_ ` A ) ) = x )
24 23 ad2ant2lr 
 |-  ( ( ( B e. HAtoms /\ x e. HAtoms ) /\ ( x C_ ( ( A vH B ) i^i ( _|_ ` A ) ) /\ ( ( A vH B ) i^i ( _|_ ` A ) ) =/= 0H ) ) -> ( ( A vH x ) i^i ( _|_ ` A ) ) = x )
25 inss1 
 |-  ( ( A vH B ) i^i ( _|_ ` A ) ) C_ ( A vH B )
26 sstr 
 |-  ( ( x C_ ( ( A vH B ) i^i ( _|_ ` A ) ) /\ ( ( A vH B ) i^i ( _|_ ` A ) ) C_ ( A vH B ) ) -> x C_ ( A vH B ) )
27 25 26 mpan2 
 |-  ( x C_ ( ( A vH B ) i^i ( _|_ ` A ) ) -> x C_ ( A vH B ) )
28 chub1 
 |-  ( ( A e. CH /\ B e. CH ) -> A C_ ( A vH B ) )
29 1 28 mpan 
 |-  ( B e. CH -> A C_ ( A vH B ) )
30 29 adantr 
 |-  ( ( B e. CH /\ x e. CH ) -> A C_ ( A vH B ) )
31 1 3 mpan 
 |-  ( B e. CH -> ( A vH B ) e. CH )
32 chlub 
 |-  ( ( A e. CH /\ x e. CH /\ ( A vH B ) e. CH ) -> ( ( A C_ ( A vH B ) /\ x C_ ( A vH B ) ) <-> ( A vH x ) C_ ( A vH B ) ) )
33 1 32 mp3an1 
 |-  ( ( x e. CH /\ ( A vH B ) e. CH ) -> ( ( A C_ ( A vH B ) /\ x C_ ( A vH B ) ) <-> ( A vH x ) C_ ( A vH B ) ) )
34 31 33 sylan2 
 |-  ( ( x e. CH /\ B e. CH ) -> ( ( A C_ ( A vH B ) /\ x C_ ( A vH B ) ) <-> ( A vH x ) C_ ( A vH B ) ) )
35 34 biimpd 
 |-  ( ( x e. CH /\ B e. CH ) -> ( ( A C_ ( A vH B ) /\ x C_ ( A vH B ) ) -> ( A vH x ) C_ ( A vH B ) ) )
36 35 ancoms 
 |-  ( ( B e. CH /\ x e. CH ) -> ( ( A C_ ( A vH B ) /\ x C_ ( A vH B ) ) -> ( A vH x ) C_ ( A vH B ) ) )
37 30 36 mpand 
 |-  ( ( B e. CH /\ x e. CH ) -> ( x C_ ( A vH B ) -> ( A vH x ) C_ ( A vH B ) ) )
38 2 10 37 syl2an 
 |-  ( ( B e. HAtoms /\ x e. HAtoms ) -> ( x C_ ( A vH B ) -> ( A vH x ) C_ ( A vH B ) ) )
39 38 imp 
 |-  ( ( ( B e. HAtoms /\ x e. HAtoms ) /\ x C_ ( A vH B ) ) -> ( A vH x ) C_ ( A vH B ) )
40 27 39 sylan2 
 |-  ( ( ( B e. HAtoms /\ x e. HAtoms ) /\ x C_ ( ( A vH B ) i^i ( _|_ ` A ) ) ) -> ( A vH x ) C_ ( A vH B ) )
41 40 adantrr 
 |-  ( ( ( B e. HAtoms /\ x e. HAtoms ) /\ ( x C_ ( ( A vH B ) i^i ( _|_ ` A ) ) /\ ( ( A vH B ) i^i ( _|_ ` A ) ) =/= 0H ) ) -> ( A vH x ) C_ ( A vH B ) )
42 chjcl 
 |-  ( ( A e. CH /\ x e. CH ) -> ( A vH x ) e. CH )
43 1 10 42 sylancr 
 |-  ( x e. HAtoms -> ( A vH x ) e. CH )
44 2 43 anim12i 
 |-  ( ( B e. HAtoms /\ x e. HAtoms ) -> ( B e. CH /\ ( A vH x ) e. CH ) )
45 44 adantr 
 |-  ( ( ( B e. HAtoms /\ x e. HAtoms ) /\ ( x C_ ( ( A vH B ) i^i ( _|_ ` A ) ) /\ ( ( A vH B ) i^i ( _|_ ` A ) ) =/= 0H ) ) -> ( B e. CH /\ ( A vH x ) e. CH ) )
46 chub1 
 |-  ( ( A e. CH /\ x e. CH ) -> A C_ ( A vH x ) )
47 1 10 46 sylancr 
 |-  ( x e. HAtoms -> A C_ ( A vH x ) )
48 47 ad2antlr 
 |-  ( ( ( B e. HAtoms /\ x e. HAtoms ) /\ ( x C_ ( ( A vH B ) i^i ( _|_ ` A ) ) /\ ( ( A vH B ) i^i ( _|_ ` A ) ) =/= 0H ) ) -> A C_ ( A vH x ) )
49 pm3.22 
 |-  ( ( B e. HAtoms /\ x e. HAtoms ) -> ( x e. HAtoms /\ B e. HAtoms ) )
50 49 adantr 
 |-  ( ( ( B e. HAtoms /\ x e. HAtoms ) /\ ( x C_ ( ( A vH B ) i^i ( _|_ ` A ) ) /\ ( ( A vH B ) i^i ( _|_ ` A ) ) =/= 0H ) ) -> ( x e. HAtoms /\ B e. HAtoms ) )
51 27 adantl 
 |-  ( ( x e. HAtoms /\ x C_ ( ( A vH B ) i^i ( _|_ ` A ) ) ) -> x C_ ( A vH B ) )
52 incom 
 |-  ( A i^i x ) = ( x i^i A )
53 chsh 
 |-  ( x e. CH -> x e. SH )
54 1 chshii 
 |-  A e. SH
55 orthin 
 |-  ( ( x e. SH /\ A e. SH ) -> ( x C_ ( _|_ ` A ) -> ( x i^i A ) = 0H ) )
56 53 54 55 sylancl 
 |-  ( x e. CH -> ( x C_ ( _|_ ` A ) -> ( x i^i A ) = 0H ) )
57 56 imp 
 |-  ( ( x e. CH /\ x C_ ( _|_ ` A ) ) -> ( x i^i A ) = 0H )
58 52 57 syl5eq 
 |-  ( ( x e. CH /\ x C_ ( _|_ ` A ) ) -> ( A i^i x ) = 0H )
59 10 13 58 syl2an 
 |-  ( ( x e. HAtoms /\ x C_ ( ( A vH B ) i^i ( _|_ ` A ) ) ) -> ( A i^i x ) = 0H )
60 51 59 jca 
 |-  ( ( x e. HAtoms /\ x C_ ( ( A vH B ) i^i ( _|_ ` A ) ) ) -> ( x C_ ( A vH B ) /\ ( A i^i x ) = 0H ) )
61 60 ad2ant2lr 
 |-  ( ( ( B e. HAtoms /\ x e. HAtoms ) /\ ( x C_ ( ( A vH B ) i^i ( _|_ ` A ) ) /\ ( ( A vH B ) i^i ( _|_ ` A ) ) =/= 0H ) ) -> ( x C_ ( A vH B ) /\ ( A i^i x ) = 0H ) )
62 atexch 
 |-  ( ( A e. CH /\ x e. HAtoms /\ B e. HAtoms ) -> ( ( x C_ ( A vH B ) /\ ( A i^i x ) = 0H ) -> B C_ ( A vH x ) ) )
63 1 62 mp3an1 
 |-  ( ( x e. HAtoms /\ B e. HAtoms ) -> ( ( x C_ ( A vH B ) /\ ( A i^i x ) = 0H ) -> B C_ ( A vH x ) ) )
64 50 61 63 sylc 
 |-  ( ( ( B e. HAtoms /\ x e. HAtoms ) /\ ( x C_ ( ( A vH B ) i^i ( _|_ ` A ) ) /\ ( ( A vH B ) i^i ( _|_ ` A ) ) =/= 0H ) ) -> B C_ ( A vH x ) )
65 chlub 
 |-  ( ( A e. CH /\ B e. CH /\ ( A vH x ) e. CH ) -> ( ( A C_ ( A vH x ) /\ B C_ ( A vH x ) ) <-> ( A vH B ) C_ ( A vH x ) ) )
66 1 65 mp3an1 
 |-  ( ( B e. CH /\ ( A vH x ) e. CH ) -> ( ( A C_ ( A vH x ) /\ B C_ ( A vH x ) ) <-> ( A vH B ) C_ ( A vH x ) ) )
67 66 biimpd 
 |-  ( ( B e. CH /\ ( A vH x ) e. CH ) -> ( ( A C_ ( A vH x ) /\ B C_ ( A vH x ) ) -> ( A vH B ) C_ ( A vH x ) ) )
68 67 expd 
 |-  ( ( B e. CH /\ ( A vH x ) e. CH ) -> ( A C_ ( A vH x ) -> ( B C_ ( A vH x ) -> ( A vH B ) C_ ( A vH x ) ) ) )
69 45 48 64 68 syl3c 
 |-  ( ( ( B e. HAtoms /\ x e. HAtoms ) /\ ( x C_ ( ( A vH B ) i^i ( _|_ ` A ) ) /\ ( ( A vH B ) i^i ( _|_ ` A ) ) =/= 0H ) ) -> ( A vH B ) C_ ( A vH x ) )
70 41 69 eqssd 
 |-  ( ( ( B e. HAtoms /\ x e. HAtoms ) /\ ( x C_ ( ( A vH B ) i^i ( _|_ ` A ) ) /\ ( ( A vH B ) i^i ( _|_ ` A ) ) =/= 0H ) ) -> ( A vH x ) = ( A vH B ) )
71 70 ineq1d 
 |-  ( ( ( B e. HAtoms /\ x e. HAtoms ) /\ ( x C_ ( ( A vH B ) i^i ( _|_ ` A ) ) /\ ( ( A vH B ) i^i ( _|_ ` A ) ) =/= 0H ) ) -> ( ( A vH x ) i^i ( _|_ ` A ) ) = ( ( A vH B ) i^i ( _|_ ` A ) ) )
72 24 71 eqtr3d 
 |-  ( ( ( B e. HAtoms /\ x e. HAtoms ) /\ ( x C_ ( ( A vH B ) i^i ( _|_ ` A ) ) /\ ( ( A vH B ) i^i ( _|_ ` A ) ) =/= 0H ) ) -> x = ( ( A vH B ) i^i ( _|_ ` A ) ) )
73 72 eleq1d 
 |-  ( ( ( B e. HAtoms /\ x e. HAtoms ) /\ ( x C_ ( ( A vH B ) i^i ( _|_ ` A ) ) /\ ( ( A vH B ) i^i ( _|_ ` A ) ) =/= 0H ) ) -> ( x e. HAtoms <-> ( ( A vH B ) i^i ( _|_ ` A ) ) e. HAtoms ) )
74 73 exp43 
 |-  ( B e. HAtoms -> ( x e. HAtoms -> ( x C_ ( ( A vH B ) i^i ( _|_ ` A ) ) -> ( ( ( A vH B ) i^i ( _|_ ` A ) ) =/= 0H -> ( x e. HAtoms <-> ( ( A vH B ) i^i ( _|_ ` A ) ) e. HAtoms ) ) ) ) )
75 74 com24 
 |-  ( B e. HAtoms -> ( ( ( A vH B ) i^i ( _|_ ` A ) ) =/= 0H -> ( x C_ ( ( A vH B ) i^i ( _|_ ` A ) ) -> ( x e. HAtoms -> ( x e. HAtoms <-> ( ( A vH B ) i^i ( _|_ ` A ) ) e. HAtoms ) ) ) ) )
76 75 imp31 
 |-  ( ( ( B e. HAtoms /\ ( ( A vH B ) i^i ( _|_ ` A ) ) =/= 0H ) /\ x C_ ( ( A vH B ) i^i ( _|_ ` A ) ) ) -> ( x e. HAtoms -> ( x e. HAtoms <-> ( ( A vH B ) i^i ( _|_ ` A ) ) e. HAtoms ) ) )
77 76 ibd 
 |-  ( ( ( B e. HAtoms /\ ( ( A vH B ) i^i ( _|_ ` A ) ) =/= 0H ) /\ x C_ ( ( A vH B ) i^i ( _|_ ` A ) ) ) -> ( x e. HAtoms -> ( ( A vH B ) i^i ( _|_ ` A ) ) e. HAtoms ) )
78 77 ex 
 |-  ( ( B e. HAtoms /\ ( ( A vH B ) i^i ( _|_ ` A ) ) =/= 0H ) -> ( x C_ ( ( A vH B ) i^i ( _|_ ` A ) ) -> ( x e. HAtoms -> ( ( A vH B ) i^i ( _|_ ` A ) ) e. HAtoms ) ) )
79 78 com23 
 |-  ( ( B e. HAtoms /\ ( ( A vH B ) i^i ( _|_ ` A ) ) =/= 0H ) -> ( x e. HAtoms -> ( x C_ ( ( A vH B ) i^i ( _|_ ` A ) ) -> ( ( A vH B ) i^i ( _|_ ` A ) ) e. HAtoms ) ) )
80 79 rexlimdv 
 |-  ( ( B e. HAtoms /\ ( ( A vH B ) i^i ( _|_ ` A ) ) =/= 0H ) -> ( E. x e. HAtoms x C_ ( ( A vH B ) i^i ( _|_ ` A ) ) -> ( ( A vH B ) i^i ( _|_ ` A ) ) e. HAtoms ) )
81 9 80 mpd 
 |-  ( ( B e. HAtoms /\ ( ( A vH B ) i^i ( _|_ ` A ) ) =/= 0H ) -> ( ( A vH B ) i^i ( _|_ ` A ) ) e. HAtoms )
82 81 ex 
 |-  ( B e. HAtoms -> ( ( ( A vH B ) i^i ( _|_ ` A ) ) =/= 0H -> ( ( A vH B ) i^i ( _|_ ` A ) ) e. HAtoms ) )
83 82 necon1bd 
 |-  ( B e. HAtoms -> ( -. ( ( A vH B ) i^i ( _|_ ` A ) ) e. HAtoms -> ( ( A vH B ) i^i ( _|_ ` A ) ) = 0H ) )
84 83 orrd 
 |-  ( B e. HAtoms -> ( ( ( A vH B ) i^i ( _|_ ` A ) ) e. HAtoms \/ ( ( A vH B ) i^i ( _|_ ` A ) ) = 0H ) )
85 elun 
 |-  ( ( ( A vH B ) i^i ( _|_ ` A ) ) e. ( HAtoms u. { 0H } ) <-> ( ( ( A vH B ) i^i ( _|_ ` A ) ) e. HAtoms \/ ( ( A vH B ) i^i ( _|_ ` A ) ) e. { 0H } ) )
86 fvex 
 |-  ( _|_ ` A ) e. _V
87 86 inex2 
 |-  ( ( A vH B ) i^i ( _|_ ` A ) ) e. _V
88 87 elsn 
 |-  ( ( ( A vH B ) i^i ( _|_ ` A ) ) e. { 0H } <-> ( ( A vH B ) i^i ( _|_ ` A ) ) = 0H )
89 88 orbi2i 
 |-  ( ( ( ( A vH B ) i^i ( _|_ ` A ) ) e. HAtoms \/ ( ( A vH B ) i^i ( _|_ ` A ) ) e. { 0H } ) <-> ( ( ( A vH B ) i^i ( _|_ ` A ) ) e. HAtoms \/ ( ( A vH B ) i^i ( _|_ ` A ) ) = 0H ) )
90 85 89 bitri 
 |-  ( ( ( A vH B ) i^i ( _|_ ` A ) ) e. ( HAtoms u. { 0H } ) <-> ( ( ( A vH B ) i^i ( _|_ ` A ) ) e. HAtoms \/ ( ( A vH B ) i^i ( _|_ ` A ) ) = 0H ) )
91 84 90 sylibr 
 |-  ( B e. HAtoms -> ( ( A vH B ) i^i ( _|_ ` A ) ) e. ( HAtoms u. { 0H } ) )