Step |
Hyp |
Ref |
Expression |
1 |
|
lsmsnorb.1 |
⊢ 𝐵 = ( Base ‘ 𝐺 ) |
2 |
|
lsmsnorb.2 |
⊢ + = ( +g ‘ 𝐺 ) |
3 |
|
lsmsnorb.3 |
⊢ ⊕ = ( LSSum ‘ 𝐺 ) |
4 |
|
lsmsnorb.4 |
⊢ ∼ = { 〈 𝑥 , 𝑦 〉 ∣ ( { 𝑥 , 𝑦 } ⊆ 𝐵 ∧ ∃ 𝑔 ∈ 𝐴 ( 𝑔 + 𝑥 ) = 𝑦 ) } |
5 |
|
lsmsnorb.5 |
⊢ ( 𝜑 → 𝐺 ∈ Mnd ) |
6 |
|
lsmsnorb.6 |
⊢ ( 𝜑 → 𝐴 ⊆ 𝐵 ) |
7 |
|
lsmsnorb.7 |
⊢ ( 𝜑 → 𝑋 ∈ 𝐵 ) |
8 |
7
|
snssd |
⊢ ( 𝜑 → { 𝑋 } ⊆ 𝐵 ) |
9 |
1 3
|
lsmssv |
⊢ ( ( 𝐺 ∈ Mnd ∧ 𝐴 ⊆ 𝐵 ∧ { 𝑋 } ⊆ 𝐵 ) → ( 𝐴 ⊕ { 𝑋 } ) ⊆ 𝐵 ) |
10 |
5 6 8 9
|
syl3anc |
⊢ ( 𝜑 → ( 𝐴 ⊕ { 𝑋 } ) ⊆ 𝐵 ) |
11 |
10
|
sselda |
⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝐴 ⊕ { 𝑋 } ) ) → 𝑘 ∈ 𝐵 ) |
12 |
|
df-ec |
⊢ [ 𝑋 ] ∼ = ( ∼ “ { 𝑋 } ) |
13 |
|
imassrn |
⊢ ( ∼ “ { 𝑋 } ) ⊆ ran ∼ |
14 |
4
|
rneqi |
⊢ ran ∼ = ran { 〈 𝑥 , 𝑦 〉 ∣ ( { 𝑥 , 𝑦 } ⊆ 𝐵 ∧ ∃ 𝑔 ∈ 𝐴 ( 𝑔 + 𝑥 ) = 𝑦 ) } |
15 |
|
rnopab |
⊢ ran { 〈 𝑥 , 𝑦 〉 ∣ ( { 𝑥 , 𝑦 } ⊆ 𝐵 ∧ ∃ 𝑔 ∈ 𝐴 ( 𝑔 + 𝑥 ) = 𝑦 ) } = { 𝑦 ∣ ∃ 𝑥 ( { 𝑥 , 𝑦 } ⊆ 𝐵 ∧ ∃ 𝑔 ∈ 𝐴 ( 𝑔 + 𝑥 ) = 𝑦 ) } |
16 |
|
vex |
⊢ 𝑥 ∈ V |
17 |
|
vex |
⊢ 𝑦 ∈ V |
18 |
16 17
|
prss |
⊢ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ↔ { 𝑥 , 𝑦 } ⊆ 𝐵 ) |
19 |
18
|
biimpri |
⊢ ( { 𝑥 , 𝑦 } ⊆ 𝐵 → ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) |
20 |
19
|
simprd |
⊢ ( { 𝑥 , 𝑦 } ⊆ 𝐵 → 𝑦 ∈ 𝐵 ) |
21 |
20
|
adantr |
⊢ ( ( { 𝑥 , 𝑦 } ⊆ 𝐵 ∧ ∃ 𝑔 ∈ 𝐴 ( 𝑔 + 𝑥 ) = 𝑦 ) → 𝑦 ∈ 𝐵 ) |
22 |
21
|
exlimiv |
⊢ ( ∃ 𝑥 ( { 𝑥 , 𝑦 } ⊆ 𝐵 ∧ ∃ 𝑔 ∈ 𝐴 ( 𝑔 + 𝑥 ) = 𝑦 ) → 𝑦 ∈ 𝐵 ) |
23 |
22
|
abssi |
⊢ { 𝑦 ∣ ∃ 𝑥 ( { 𝑥 , 𝑦 } ⊆ 𝐵 ∧ ∃ 𝑔 ∈ 𝐴 ( 𝑔 + 𝑥 ) = 𝑦 ) } ⊆ 𝐵 |
24 |
15 23
|
eqsstri |
⊢ ran { 〈 𝑥 , 𝑦 〉 ∣ ( { 𝑥 , 𝑦 } ⊆ 𝐵 ∧ ∃ 𝑔 ∈ 𝐴 ( 𝑔 + 𝑥 ) = 𝑦 ) } ⊆ 𝐵 |
25 |
14 24
|
eqsstri |
⊢ ran ∼ ⊆ 𝐵 |
26 |
13 25
|
sstri |
⊢ ( ∼ “ { 𝑋 } ) ⊆ 𝐵 |
27 |
26
|
a1i |
⊢ ( 𝜑 → ( ∼ “ { 𝑋 } ) ⊆ 𝐵 ) |
28 |
12 27
|
eqsstrid |
⊢ ( 𝜑 → [ 𝑋 ] ∼ ⊆ 𝐵 ) |
29 |
28
|
sselda |
⊢ ( ( 𝜑 ∧ 𝑘 ∈ [ 𝑋 ] ∼ ) → 𝑘 ∈ 𝐵 ) |
30 |
4
|
gaorb |
⊢ ( 𝑋 ∼ 𝑘 ↔ ( 𝑋 ∈ 𝐵 ∧ 𝑘 ∈ 𝐵 ∧ ∃ ℎ ∈ 𝐴 ( ℎ + 𝑋 ) = 𝑘 ) ) |
31 |
7
|
anim1i |
⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐵 ) → ( 𝑋 ∈ 𝐵 ∧ 𝑘 ∈ 𝐵 ) ) |
32 |
31
|
biantrurd |
⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐵 ) → ( ∃ ℎ ∈ 𝐴 ( ℎ + 𝑋 ) = 𝑘 ↔ ( ( 𝑋 ∈ 𝐵 ∧ 𝑘 ∈ 𝐵 ) ∧ ∃ ℎ ∈ 𝐴 ( ℎ + 𝑋 ) = 𝑘 ) ) ) |
33 |
|
df-3an |
⊢ ( ( 𝑋 ∈ 𝐵 ∧ 𝑘 ∈ 𝐵 ∧ ∃ ℎ ∈ 𝐴 ( ℎ + 𝑋 ) = 𝑘 ) ↔ ( ( 𝑋 ∈ 𝐵 ∧ 𝑘 ∈ 𝐵 ) ∧ ∃ ℎ ∈ 𝐴 ( ℎ + 𝑋 ) = 𝑘 ) ) |
34 |
32 33
|
bitr4di |
⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐵 ) → ( ∃ ℎ ∈ 𝐴 ( ℎ + 𝑋 ) = 𝑘 ↔ ( 𝑋 ∈ 𝐵 ∧ 𝑘 ∈ 𝐵 ∧ ∃ ℎ ∈ 𝐴 ( ℎ + 𝑋 ) = 𝑘 ) ) ) |
35 |
30 34
|
bitr4id |
⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐵 ) → ( 𝑋 ∼ 𝑘 ↔ ∃ ℎ ∈ 𝐴 ( ℎ + 𝑋 ) = 𝑘 ) ) |
36 |
|
vex |
⊢ 𝑘 ∈ V |
37 |
7
|
adantr |
⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐵 ) → 𝑋 ∈ 𝐵 ) |
38 |
|
elecg |
⊢ ( ( 𝑘 ∈ V ∧ 𝑋 ∈ 𝐵 ) → ( 𝑘 ∈ [ 𝑋 ] ∼ ↔ 𝑋 ∼ 𝑘 ) ) |
39 |
36 37 38
|
sylancr |
⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐵 ) → ( 𝑘 ∈ [ 𝑋 ] ∼ ↔ 𝑋 ∼ 𝑘 ) ) |
40 |
5
|
adantr |
⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐵 ) → 𝐺 ∈ Mnd ) |
41 |
6
|
adantr |
⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐵 ) → 𝐴 ⊆ 𝐵 ) |
42 |
1 2 3 40 41 37
|
elgrplsmsn |
⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐵 ) → ( 𝑘 ∈ ( 𝐴 ⊕ { 𝑋 } ) ↔ ∃ ℎ ∈ 𝐴 𝑘 = ( ℎ + 𝑋 ) ) ) |
43 |
|
eqcom |
⊢ ( 𝑘 = ( ℎ + 𝑋 ) ↔ ( ℎ + 𝑋 ) = 𝑘 ) |
44 |
43
|
rexbii |
⊢ ( ∃ ℎ ∈ 𝐴 𝑘 = ( ℎ + 𝑋 ) ↔ ∃ ℎ ∈ 𝐴 ( ℎ + 𝑋 ) = 𝑘 ) |
45 |
42 44
|
bitrdi |
⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐵 ) → ( 𝑘 ∈ ( 𝐴 ⊕ { 𝑋 } ) ↔ ∃ ℎ ∈ 𝐴 ( ℎ + 𝑋 ) = 𝑘 ) ) |
46 |
35 39 45
|
3bitr4rd |
⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐵 ) → ( 𝑘 ∈ ( 𝐴 ⊕ { 𝑋 } ) ↔ 𝑘 ∈ [ 𝑋 ] ∼ ) ) |
47 |
11 29 46
|
eqrdav |
⊢ ( 𝜑 → ( 𝐴 ⊕ { 𝑋 } ) = [ 𝑋 ] ∼ ) |