Step |
Hyp |
Ref |
Expression |
1 |
|
lcvexch.s |
⊢ 𝑆 = ( LSubSp ‘ 𝑊 ) |
2 |
|
lcvexch.p |
⊢ ⊕ = ( LSSum ‘ 𝑊 ) |
3 |
|
lcvexch.c |
⊢ 𝐶 = ( ⋖L ‘ 𝑊 ) |
4 |
|
lcvexch.w |
⊢ ( 𝜑 → 𝑊 ∈ LMod ) |
5 |
|
lcvexch.t |
⊢ ( 𝜑 → 𝑇 ∈ 𝑆 ) |
6 |
|
lcvexch.u |
⊢ ( 𝜑 → 𝑈 ∈ 𝑆 ) |
7 |
|
lcvexch.g |
⊢ ( 𝜑 → ( 𝑇 ∩ 𝑈 ) 𝐶 𝑈 ) |
8 |
1
|
lssincl |
⊢ ( ( 𝑊 ∈ LMod ∧ 𝑇 ∈ 𝑆 ∧ 𝑈 ∈ 𝑆 ) → ( 𝑇 ∩ 𝑈 ) ∈ 𝑆 ) |
9 |
4 5 6 8
|
syl3anc |
⊢ ( 𝜑 → ( 𝑇 ∩ 𝑈 ) ∈ 𝑆 ) |
10 |
1 3 4 9 6 7
|
lcvpss |
⊢ ( 𝜑 → ( 𝑇 ∩ 𝑈 ) ⊊ 𝑈 ) |
11 |
1 2 3 4 5 6
|
lcvexchlem1 |
⊢ ( 𝜑 → ( 𝑇 ⊊ ( 𝑇 ⊕ 𝑈 ) ↔ ( 𝑇 ∩ 𝑈 ) ⊊ 𝑈 ) ) |
12 |
10 11
|
mpbird |
⊢ ( 𝜑 → 𝑇 ⊊ ( 𝑇 ⊕ 𝑈 ) ) |
13 |
|
simp3l |
⊢ ( ( 𝜑 ∧ 𝑠 ∈ 𝑆 ∧ ( 𝑇 ⊆ 𝑠 ∧ 𝑠 ⊆ ( 𝑇 ⊕ 𝑈 ) ) ) → 𝑇 ⊆ 𝑠 ) |
14 |
13
|
ssrind |
⊢ ( ( 𝜑 ∧ 𝑠 ∈ 𝑆 ∧ ( 𝑇 ⊆ 𝑠 ∧ 𝑠 ⊆ ( 𝑇 ⊕ 𝑈 ) ) ) → ( 𝑇 ∩ 𝑈 ) ⊆ ( 𝑠 ∩ 𝑈 ) ) |
15 |
|
inss2 |
⊢ ( 𝑠 ∩ 𝑈 ) ⊆ 𝑈 |
16 |
14 15
|
jctir |
⊢ ( ( 𝜑 ∧ 𝑠 ∈ 𝑆 ∧ ( 𝑇 ⊆ 𝑠 ∧ 𝑠 ⊆ ( 𝑇 ⊕ 𝑈 ) ) ) → ( ( 𝑇 ∩ 𝑈 ) ⊆ ( 𝑠 ∩ 𝑈 ) ∧ ( 𝑠 ∩ 𝑈 ) ⊆ 𝑈 ) ) |
17 |
7
|
3ad2ant1 |
⊢ ( ( 𝜑 ∧ 𝑠 ∈ 𝑆 ∧ ( 𝑇 ⊆ 𝑠 ∧ 𝑠 ⊆ ( 𝑇 ⊕ 𝑈 ) ) ) → ( 𝑇 ∩ 𝑈 ) 𝐶 𝑈 ) |
18 |
1 3 4 9 6
|
lcvbr3 |
⊢ ( 𝜑 → ( ( 𝑇 ∩ 𝑈 ) 𝐶 𝑈 ↔ ( ( 𝑇 ∩ 𝑈 ) ⊊ 𝑈 ∧ ∀ 𝑟 ∈ 𝑆 ( ( ( 𝑇 ∩ 𝑈 ) ⊆ 𝑟 ∧ 𝑟 ⊆ 𝑈 ) → ( 𝑟 = ( 𝑇 ∩ 𝑈 ) ∨ 𝑟 = 𝑈 ) ) ) ) ) |
19 |
18
|
adantr |
⊢ ( ( 𝜑 ∧ 𝑠 ∈ 𝑆 ) → ( ( 𝑇 ∩ 𝑈 ) 𝐶 𝑈 ↔ ( ( 𝑇 ∩ 𝑈 ) ⊊ 𝑈 ∧ ∀ 𝑟 ∈ 𝑆 ( ( ( 𝑇 ∩ 𝑈 ) ⊆ 𝑟 ∧ 𝑟 ⊆ 𝑈 ) → ( 𝑟 = ( 𝑇 ∩ 𝑈 ) ∨ 𝑟 = 𝑈 ) ) ) ) ) |
20 |
4
|
adantr |
⊢ ( ( 𝜑 ∧ 𝑠 ∈ 𝑆 ) → 𝑊 ∈ LMod ) |
21 |
|
simpr |
⊢ ( ( 𝜑 ∧ 𝑠 ∈ 𝑆 ) → 𝑠 ∈ 𝑆 ) |
22 |
6
|
adantr |
⊢ ( ( 𝜑 ∧ 𝑠 ∈ 𝑆 ) → 𝑈 ∈ 𝑆 ) |
23 |
1
|
lssincl |
⊢ ( ( 𝑊 ∈ LMod ∧ 𝑠 ∈ 𝑆 ∧ 𝑈 ∈ 𝑆 ) → ( 𝑠 ∩ 𝑈 ) ∈ 𝑆 ) |
24 |
20 21 22 23
|
syl3anc |
⊢ ( ( 𝜑 ∧ 𝑠 ∈ 𝑆 ) → ( 𝑠 ∩ 𝑈 ) ∈ 𝑆 ) |
25 |
|
sseq2 |
⊢ ( 𝑟 = ( 𝑠 ∩ 𝑈 ) → ( ( 𝑇 ∩ 𝑈 ) ⊆ 𝑟 ↔ ( 𝑇 ∩ 𝑈 ) ⊆ ( 𝑠 ∩ 𝑈 ) ) ) |
26 |
|
sseq1 |
⊢ ( 𝑟 = ( 𝑠 ∩ 𝑈 ) → ( 𝑟 ⊆ 𝑈 ↔ ( 𝑠 ∩ 𝑈 ) ⊆ 𝑈 ) ) |
27 |
25 26
|
anbi12d |
⊢ ( 𝑟 = ( 𝑠 ∩ 𝑈 ) → ( ( ( 𝑇 ∩ 𝑈 ) ⊆ 𝑟 ∧ 𝑟 ⊆ 𝑈 ) ↔ ( ( 𝑇 ∩ 𝑈 ) ⊆ ( 𝑠 ∩ 𝑈 ) ∧ ( 𝑠 ∩ 𝑈 ) ⊆ 𝑈 ) ) ) |
28 |
|
eqeq1 |
⊢ ( 𝑟 = ( 𝑠 ∩ 𝑈 ) → ( 𝑟 = ( 𝑇 ∩ 𝑈 ) ↔ ( 𝑠 ∩ 𝑈 ) = ( 𝑇 ∩ 𝑈 ) ) ) |
29 |
|
eqeq1 |
⊢ ( 𝑟 = ( 𝑠 ∩ 𝑈 ) → ( 𝑟 = 𝑈 ↔ ( 𝑠 ∩ 𝑈 ) = 𝑈 ) ) |
30 |
28 29
|
orbi12d |
⊢ ( 𝑟 = ( 𝑠 ∩ 𝑈 ) → ( ( 𝑟 = ( 𝑇 ∩ 𝑈 ) ∨ 𝑟 = 𝑈 ) ↔ ( ( 𝑠 ∩ 𝑈 ) = ( 𝑇 ∩ 𝑈 ) ∨ ( 𝑠 ∩ 𝑈 ) = 𝑈 ) ) ) |
31 |
27 30
|
imbi12d |
⊢ ( 𝑟 = ( 𝑠 ∩ 𝑈 ) → ( ( ( ( 𝑇 ∩ 𝑈 ) ⊆ 𝑟 ∧ 𝑟 ⊆ 𝑈 ) → ( 𝑟 = ( 𝑇 ∩ 𝑈 ) ∨ 𝑟 = 𝑈 ) ) ↔ ( ( ( 𝑇 ∩ 𝑈 ) ⊆ ( 𝑠 ∩ 𝑈 ) ∧ ( 𝑠 ∩ 𝑈 ) ⊆ 𝑈 ) → ( ( 𝑠 ∩ 𝑈 ) = ( 𝑇 ∩ 𝑈 ) ∨ ( 𝑠 ∩ 𝑈 ) = 𝑈 ) ) ) ) |
32 |
31
|
rspcv |
⊢ ( ( 𝑠 ∩ 𝑈 ) ∈ 𝑆 → ( ∀ 𝑟 ∈ 𝑆 ( ( ( 𝑇 ∩ 𝑈 ) ⊆ 𝑟 ∧ 𝑟 ⊆ 𝑈 ) → ( 𝑟 = ( 𝑇 ∩ 𝑈 ) ∨ 𝑟 = 𝑈 ) ) → ( ( ( 𝑇 ∩ 𝑈 ) ⊆ ( 𝑠 ∩ 𝑈 ) ∧ ( 𝑠 ∩ 𝑈 ) ⊆ 𝑈 ) → ( ( 𝑠 ∩ 𝑈 ) = ( 𝑇 ∩ 𝑈 ) ∨ ( 𝑠 ∩ 𝑈 ) = 𝑈 ) ) ) ) |
33 |
24 32
|
syl |
⊢ ( ( 𝜑 ∧ 𝑠 ∈ 𝑆 ) → ( ∀ 𝑟 ∈ 𝑆 ( ( ( 𝑇 ∩ 𝑈 ) ⊆ 𝑟 ∧ 𝑟 ⊆ 𝑈 ) → ( 𝑟 = ( 𝑇 ∩ 𝑈 ) ∨ 𝑟 = 𝑈 ) ) → ( ( ( 𝑇 ∩ 𝑈 ) ⊆ ( 𝑠 ∩ 𝑈 ) ∧ ( 𝑠 ∩ 𝑈 ) ⊆ 𝑈 ) → ( ( 𝑠 ∩ 𝑈 ) = ( 𝑇 ∩ 𝑈 ) ∨ ( 𝑠 ∩ 𝑈 ) = 𝑈 ) ) ) ) |
34 |
33
|
adantld |
⊢ ( ( 𝜑 ∧ 𝑠 ∈ 𝑆 ) → ( ( ( 𝑇 ∩ 𝑈 ) ⊊ 𝑈 ∧ ∀ 𝑟 ∈ 𝑆 ( ( ( 𝑇 ∩ 𝑈 ) ⊆ 𝑟 ∧ 𝑟 ⊆ 𝑈 ) → ( 𝑟 = ( 𝑇 ∩ 𝑈 ) ∨ 𝑟 = 𝑈 ) ) ) → ( ( ( 𝑇 ∩ 𝑈 ) ⊆ ( 𝑠 ∩ 𝑈 ) ∧ ( 𝑠 ∩ 𝑈 ) ⊆ 𝑈 ) → ( ( 𝑠 ∩ 𝑈 ) = ( 𝑇 ∩ 𝑈 ) ∨ ( 𝑠 ∩ 𝑈 ) = 𝑈 ) ) ) ) |
35 |
19 34
|
sylbid |
⊢ ( ( 𝜑 ∧ 𝑠 ∈ 𝑆 ) → ( ( 𝑇 ∩ 𝑈 ) 𝐶 𝑈 → ( ( ( 𝑇 ∩ 𝑈 ) ⊆ ( 𝑠 ∩ 𝑈 ) ∧ ( 𝑠 ∩ 𝑈 ) ⊆ 𝑈 ) → ( ( 𝑠 ∩ 𝑈 ) = ( 𝑇 ∩ 𝑈 ) ∨ ( 𝑠 ∩ 𝑈 ) = 𝑈 ) ) ) ) |
36 |
35
|
3adant3 |
⊢ ( ( 𝜑 ∧ 𝑠 ∈ 𝑆 ∧ ( 𝑇 ⊆ 𝑠 ∧ 𝑠 ⊆ ( 𝑇 ⊕ 𝑈 ) ) ) → ( ( 𝑇 ∩ 𝑈 ) 𝐶 𝑈 → ( ( ( 𝑇 ∩ 𝑈 ) ⊆ ( 𝑠 ∩ 𝑈 ) ∧ ( 𝑠 ∩ 𝑈 ) ⊆ 𝑈 ) → ( ( 𝑠 ∩ 𝑈 ) = ( 𝑇 ∩ 𝑈 ) ∨ ( 𝑠 ∩ 𝑈 ) = 𝑈 ) ) ) ) |
37 |
17 36
|
mpd |
⊢ ( ( 𝜑 ∧ 𝑠 ∈ 𝑆 ∧ ( 𝑇 ⊆ 𝑠 ∧ 𝑠 ⊆ ( 𝑇 ⊕ 𝑈 ) ) ) → ( ( ( 𝑇 ∩ 𝑈 ) ⊆ ( 𝑠 ∩ 𝑈 ) ∧ ( 𝑠 ∩ 𝑈 ) ⊆ 𝑈 ) → ( ( 𝑠 ∩ 𝑈 ) = ( 𝑇 ∩ 𝑈 ) ∨ ( 𝑠 ∩ 𝑈 ) = 𝑈 ) ) ) |
38 |
16 37
|
mpd |
⊢ ( ( 𝜑 ∧ 𝑠 ∈ 𝑆 ∧ ( 𝑇 ⊆ 𝑠 ∧ 𝑠 ⊆ ( 𝑇 ⊕ 𝑈 ) ) ) → ( ( 𝑠 ∩ 𝑈 ) = ( 𝑇 ∩ 𝑈 ) ∨ ( 𝑠 ∩ 𝑈 ) = 𝑈 ) ) |
39 |
|
oveq1 |
⊢ ( ( 𝑠 ∩ 𝑈 ) = ( 𝑇 ∩ 𝑈 ) → ( ( 𝑠 ∩ 𝑈 ) ⊕ 𝑇 ) = ( ( 𝑇 ∩ 𝑈 ) ⊕ 𝑇 ) ) |
40 |
4
|
3ad2ant1 |
⊢ ( ( 𝜑 ∧ 𝑠 ∈ 𝑆 ∧ ( 𝑇 ⊆ 𝑠 ∧ 𝑠 ⊆ ( 𝑇 ⊕ 𝑈 ) ) ) → 𝑊 ∈ LMod ) |
41 |
5
|
3ad2ant1 |
⊢ ( ( 𝜑 ∧ 𝑠 ∈ 𝑆 ∧ ( 𝑇 ⊆ 𝑠 ∧ 𝑠 ⊆ ( 𝑇 ⊕ 𝑈 ) ) ) → 𝑇 ∈ 𝑆 ) |
42 |
6
|
3ad2ant1 |
⊢ ( ( 𝜑 ∧ 𝑠 ∈ 𝑆 ∧ ( 𝑇 ⊆ 𝑠 ∧ 𝑠 ⊆ ( 𝑇 ⊕ 𝑈 ) ) ) → 𝑈 ∈ 𝑆 ) |
43 |
|
simp2 |
⊢ ( ( 𝜑 ∧ 𝑠 ∈ 𝑆 ∧ ( 𝑇 ⊆ 𝑠 ∧ 𝑠 ⊆ ( 𝑇 ⊕ 𝑈 ) ) ) → 𝑠 ∈ 𝑆 ) |
44 |
|
simp3r |
⊢ ( ( 𝜑 ∧ 𝑠 ∈ 𝑆 ∧ ( 𝑇 ⊆ 𝑠 ∧ 𝑠 ⊆ ( 𝑇 ⊕ 𝑈 ) ) ) → 𝑠 ⊆ ( 𝑇 ⊕ 𝑈 ) ) |
45 |
1 2 3 40 41 42 43 13 44
|
lcvexchlem3 |
⊢ ( ( 𝜑 ∧ 𝑠 ∈ 𝑆 ∧ ( 𝑇 ⊆ 𝑠 ∧ 𝑠 ⊆ ( 𝑇 ⊕ 𝑈 ) ) ) → ( ( 𝑠 ∩ 𝑈 ) ⊕ 𝑇 ) = 𝑠 ) |
46 |
1
|
lsssssubg |
⊢ ( 𝑊 ∈ LMod → 𝑆 ⊆ ( SubGrp ‘ 𝑊 ) ) |
47 |
4 46
|
syl |
⊢ ( 𝜑 → 𝑆 ⊆ ( SubGrp ‘ 𝑊 ) ) |
48 |
47 9
|
sseldd |
⊢ ( 𝜑 → ( 𝑇 ∩ 𝑈 ) ∈ ( SubGrp ‘ 𝑊 ) ) |
49 |
47 5
|
sseldd |
⊢ ( 𝜑 → 𝑇 ∈ ( SubGrp ‘ 𝑊 ) ) |
50 |
|
inss1 |
⊢ ( 𝑇 ∩ 𝑈 ) ⊆ 𝑇 |
51 |
50
|
a1i |
⊢ ( 𝜑 → ( 𝑇 ∩ 𝑈 ) ⊆ 𝑇 ) |
52 |
2
|
lsmss1 |
⊢ ( ( ( 𝑇 ∩ 𝑈 ) ∈ ( SubGrp ‘ 𝑊 ) ∧ 𝑇 ∈ ( SubGrp ‘ 𝑊 ) ∧ ( 𝑇 ∩ 𝑈 ) ⊆ 𝑇 ) → ( ( 𝑇 ∩ 𝑈 ) ⊕ 𝑇 ) = 𝑇 ) |
53 |
48 49 51 52
|
syl3anc |
⊢ ( 𝜑 → ( ( 𝑇 ∩ 𝑈 ) ⊕ 𝑇 ) = 𝑇 ) |
54 |
53
|
3ad2ant1 |
⊢ ( ( 𝜑 ∧ 𝑠 ∈ 𝑆 ∧ ( 𝑇 ⊆ 𝑠 ∧ 𝑠 ⊆ ( 𝑇 ⊕ 𝑈 ) ) ) → ( ( 𝑇 ∩ 𝑈 ) ⊕ 𝑇 ) = 𝑇 ) |
55 |
45 54
|
eqeq12d |
⊢ ( ( 𝜑 ∧ 𝑠 ∈ 𝑆 ∧ ( 𝑇 ⊆ 𝑠 ∧ 𝑠 ⊆ ( 𝑇 ⊕ 𝑈 ) ) ) → ( ( ( 𝑠 ∩ 𝑈 ) ⊕ 𝑇 ) = ( ( 𝑇 ∩ 𝑈 ) ⊕ 𝑇 ) ↔ 𝑠 = 𝑇 ) ) |
56 |
39 55
|
syl5ib |
⊢ ( ( 𝜑 ∧ 𝑠 ∈ 𝑆 ∧ ( 𝑇 ⊆ 𝑠 ∧ 𝑠 ⊆ ( 𝑇 ⊕ 𝑈 ) ) ) → ( ( 𝑠 ∩ 𝑈 ) = ( 𝑇 ∩ 𝑈 ) → 𝑠 = 𝑇 ) ) |
57 |
|
oveq1 |
⊢ ( ( 𝑠 ∩ 𝑈 ) = 𝑈 → ( ( 𝑠 ∩ 𝑈 ) ⊕ 𝑇 ) = ( 𝑈 ⊕ 𝑇 ) ) |
58 |
|
lmodabl |
⊢ ( 𝑊 ∈ LMod → 𝑊 ∈ Abel ) |
59 |
4 58
|
syl |
⊢ ( 𝜑 → 𝑊 ∈ Abel ) |
60 |
47 6
|
sseldd |
⊢ ( 𝜑 → 𝑈 ∈ ( SubGrp ‘ 𝑊 ) ) |
61 |
2
|
lsmcom |
⊢ ( ( 𝑊 ∈ Abel ∧ 𝑈 ∈ ( SubGrp ‘ 𝑊 ) ∧ 𝑇 ∈ ( SubGrp ‘ 𝑊 ) ) → ( 𝑈 ⊕ 𝑇 ) = ( 𝑇 ⊕ 𝑈 ) ) |
62 |
59 60 49 61
|
syl3anc |
⊢ ( 𝜑 → ( 𝑈 ⊕ 𝑇 ) = ( 𝑇 ⊕ 𝑈 ) ) |
63 |
62
|
3ad2ant1 |
⊢ ( ( 𝜑 ∧ 𝑠 ∈ 𝑆 ∧ ( 𝑇 ⊆ 𝑠 ∧ 𝑠 ⊆ ( 𝑇 ⊕ 𝑈 ) ) ) → ( 𝑈 ⊕ 𝑇 ) = ( 𝑇 ⊕ 𝑈 ) ) |
64 |
45 63
|
eqeq12d |
⊢ ( ( 𝜑 ∧ 𝑠 ∈ 𝑆 ∧ ( 𝑇 ⊆ 𝑠 ∧ 𝑠 ⊆ ( 𝑇 ⊕ 𝑈 ) ) ) → ( ( ( 𝑠 ∩ 𝑈 ) ⊕ 𝑇 ) = ( 𝑈 ⊕ 𝑇 ) ↔ 𝑠 = ( 𝑇 ⊕ 𝑈 ) ) ) |
65 |
57 64
|
syl5ib |
⊢ ( ( 𝜑 ∧ 𝑠 ∈ 𝑆 ∧ ( 𝑇 ⊆ 𝑠 ∧ 𝑠 ⊆ ( 𝑇 ⊕ 𝑈 ) ) ) → ( ( 𝑠 ∩ 𝑈 ) = 𝑈 → 𝑠 = ( 𝑇 ⊕ 𝑈 ) ) ) |
66 |
56 65
|
orim12d |
⊢ ( ( 𝜑 ∧ 𝑠 ∈ 𝑆 ∧ ( 𝑇 ⊆ 𝑠 ∧ 𝑠 ⊆ ( 𝑇 ⊕ 𝑈 ) ) ) → ( ( ( 𝑠 ∩ 𝑈 ) = ( 𝑇 ∩ 𝑈 ) ∨ ( 𝑠 ∩ 𝑈 ) = 𝑈 ) → ( 𝑠 = 𝑇 ∨ 𝑠 = ( 𝑇 ⊕ 𝑈 ) ) ) ) |
67 |
38 66
|
mpd |
⊢ ( ( 𝜑 ∧ 𝑠 ∈ 𝑆 ∧ ( 𝑇 ⊆ 𝑠 ∧ 𝑠 ⊆ ( 𝑇 ⊕ 𝑈 ) ) ) → ( 𝑠 = 𝑇 ∨ 𝑠 = ( 𝑇 ⊕ 𝑈 ) ) ) |
68 |
67
|
3exp |
⊢ ( 𝜑 → ( 𝑠 ∈ 𝑆 → ( ( 𝑇 ⊆ 𝑠 ∧ 𝑠 ⊆ ( 𝑇 ⊕ 𝑈 ) ) → ( 𝑠 = 𝑇 ∨ 𝑠 = ( 𝑇 ⊕ 𝑈 ) ) ) ) ) |
69 |
68
|
ralrimiv |
⊢ ( 𝜑 → ∀ 𝑠 ∈ 𝑆 ( ( 𝑇 ⊆ 𝑠 ∧ 𝑠 ⊆ ( 𝑇 ⊕ 𝑈 ) ) → ( 𝑠 = 𝑇 ∨ 𝑠 = ( 𝑇 ⊕ 𝑈 ) ) ) ) |
70 |
1 2
|
lsmcl |
⊢ ( ( 𝑊 ∈ LMod ∧ 𝑇 ∈ 𝑆 ∧ 𝑈 ∈ 𝑆 ) → ( 𝑇 ⊕ 𝑈 ) ∈ 𝑆 ) |
71 |
4 5 6 70
|
syl3anc |
⊢ ( 𝜑 → ( 𝑇 ⊕ 𝑈 ) ∈ 𝑆 ) |
72 |
1 3 4 5 71
|
lcvbr3 |
⊢ ( 𝜑 → ( 𝑇 𝐶 ( 𝑇 ⊕ 𝑈 ) ↔ ( 𝑇 ⊊ ( 𝑇 ⊕ 𝑈 ) ∧ ∀ 𝑠 ∈ 𝑆 ( ( 𝑇 ⊆ 𝑠 ∧ 𝑠 ⊆ ( 𝑇 ⊕ 𝑈 ) ) → ( 𝑠 = 𝑇 ∨ 𝑠 = ( 𝑇 ⊕ 𝑈 ) ) ) ) ) ) |
73 |
12 69 72
|
mpbir2and |
⊢ ( 𝜑 → 𝑇 𝐶 ( 𝑇 ⊕ 𝑈 ) ) |