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