| Step | Hyp | Ref
| Expression |
| 1 | | grplsm0l.b |
. . . . . . 7
⊢ 𝐵 = (Base‘𝐺) |
| 2 | | grplsm0l.0 |
. . . . . . 7
⊢ 0 =
(0g‘𝐺) |
| 3 | 1, 2 | grpidcl 18983 |
. . . . . 6
⊢ (𝐺 ∈ Grp → 0 ∈ 𝐵) |
| 4 | 3 | snssd 4809 |
. . . . 5
⊢ (𝐺 ∈ Grp → { 0 } ⊆
𝐵) |
| 5 | | eqid 2737 |
. . . . . . . 8
⊢
(+g‘𝐺) = (+g‘𝐺) |
| 6 | | grplsm0l.p |
. . . . . . . 8
⊢ ⊕ =
(LSSum‘𝐺) |
| 7 | 1, 5, 6 | lsmelvalx 19658 |
. . . . . . 7
⊢ ((𝐺 ∈ Grp ∧ { 0 } ⊆
𝐵 ∧ 𝐴 ⊆ 𝐵) → (𝑥 ∈ ({ 0 } ⊕ 𝐴) ↔ ∃𝑜 ∈ { 0 }∃𝑎 ∈ 𝐴 𝑥 = (𝑜(+g‘𝐺)𝑎))) |
| 8 | 7 | 3expa 1119 |
. . . . . 6
⊢ (((𝐺 ∈ Grp ∧ { 0 } ⊆
𝐵) ∧ 𝐴 ⊆ 𝐵) → (𝑥 ∈ ({ 0 } ⊕ 𝐴) ↔ ∃𝑜 ∈ { 0 }∃𝑎 ∈ 𝐴 𝑥 = (𝑜(+g‘𝐺)𝑎))) |
| 9 | 8 | an32s 652 |
. . . . 5
⊢ (((𝐺 ∈ Grp ∧ 𝐴 ⊆ 𝐵) ∧ { 0 } ⊆ 𝐵) → (𝑥 ∈ ({ 0 } ⊕ 𝐴) ↔ ∃𝑜 ∈ { 0 }∃𝑎 ∈ 𝐴 𝑥 = (𝑜(+g‘𝐺)𝑎))) |
| 10 | 4, 9 | mpidan 689 |
. . . 4
⊢ ((𝐺 ∈ Grp ∧ 𝐴 ⊆ 𝐵) → (𝑥 ∈ ({ 0 } ⊕ 𝐴) ↔ ∃𝑜 ∈ { 0 }∃𝑎 ∈ 𝐴 𝑥 = (𝑜(+g‘𝐺)𝑎))) |
| 11 | 10 | 3adant3 1133 |
. . 3
⊢ ((𝐺 ∈ Grp ∧ 𝐴 ⊆ 𝐵 ∧ 𝐴 ≠ ∅) → (𝑥 ∈ ({ 0 } ⊕ 𝐴) ↔ ∃𝑜 ∈ { 0 }∃𝑎 ∈ 𝐴 𝑥 = (𝑜(+g‘𝐺)𝑎))) |
| 12 | | simpl1 1192 |
. . . . . . . 8
⊢ (((𝐺 ∈ Grp ∧ 𝐴 ⊆ 𝐵 ∧ 𝐴 ≠ ∅) ∧ 𝑎 ∈ 𝐴) → 𝐺 ∈ Grp) |
| 13 | | simp2 1138 |
. . . . . . . . 9
⊢ ((𝐺 ∈ Grp ∧ 𝐴 ⊆ 𝐵 ∧ 𝐴 ≠ ∅) → 𝐴 ⊆ 𝐵) |
| 14 | 13 | sselda 3983 |
. . . . . . . 8
⊢ (((𝐺 ∈ Grp ∧ 𝐴 ⊆ 𝐵 ∧ 𝐴 ≠ ∅) ∧ 𝑎 ∈ 𝐴) → 𝑎 ∈ 𝐵) |
| 15 | 1, 5, 2 | grplid 18985 |
. . . . . . . 8
⊢ ((𝐺 ∈ Grp ∧ 𝑎 ∈ 𝐵) → ( 0 (+g‘𝐺)𝑎) = 𝑎) |
| 16 | 12, 14, 15 | syl2anc 584 |
. . . . . . 7
⊢ (((𝐺 ∈ Grp ∧ 𝐴 ⊆ 𝐵 ∧ 𝐴 ≠ ∅) ∧ 𝑎 ∈ 𝐴) → ( 0 (+g‘𝐺)𝑎) = 𝑎) |
| 17 | 16 | eqeq2d 2748 |
. . . . . 6
⊢ (((𝐺 ∈ Grp ∧ 𝐴 ⊆ 𝐵 ∧ 𝐴 ≠ ∅) ∧ 𝑎 ∈ 𝐴) → (𝑥 = ( 0 (+g‘𝐺)𝑎) ↔ 𝑥 = 𝑎)) |
| 18 | | equcom 2017 |
. . . . . 6
⊢ (𝑥 = 𝑎 ↔ 𝑎 = 𝑥) |
| 19 | 17, 18 | bitrdi 287 |
. . . . 5
⊢ (((𝐺 ∈ Grp ∧ 𝐴 ⊆ 𝐵 ∧ 𝐴 ≠ ∅) ∧ 𝑎 ∈ 𝐴) → (𝑥 = ( 0 (+g‘𝐺)𝑎) ↔ 𝑎 = 𝑥)) |
| 20 | 19 | rexbidva 3177 |
. . . 4
⊢ ((𝐺 ∈ Grp ∧ 𝐴 ⊆ 𝐵 ∧ 𝐴 ≠ ∅) → (∃𝑎 ∈ 𝐴 𝑥 = ( 0 (+g‘𝐺)𝑎) ↔ ∃𝑎 ∈ 𝐴 𝑎 = 𝑥)) |
| 21 | 2 | fvexi 6920 |
. . . . 5
⊢ 0 ∈
V |
| 22 | | oveq1 7438 |
. . . . . . 7
⊢ (𝑜 = 0 → (𝑜(+g‘𝐺)𝑎) = ( 0 (+g‘𝐺)𝑎)) |
| 23 | 22 | eqeq2d 2748 |
. . . . . 6
⊢ (𝑜 = 0 → (𝑥 = (𝑜(+g‘𝐺)𝑎) ↔ 𝑥 = ( 0 (+g‘𝐺)𝑎))) |
| 24 | 23 | rexbidv 3179 |
. . . . 5
⊢ (𝑜 = 0 → (∃𝑎 ∈ 𝐴 𝑥 = (𝑜(+g‘𝐺)𝑎) ↔ ∃𝑎 ∈ 𝐴 𝑥 = ( 0 (+g‘𝐺)𝑎))) |
| 25 | 21, 24 | rexsn 4682 |
. . . 4
⊢
(∃𝑜 ∈ {
0
}∃𝑎 ∈ 𝐴 𝑥 = (𝑜(+g‘𝐺)𝑎) ↔ ∃𝑎 ∈ 𝐴 𝑥 = ( 0 (+g‘𝐺)𝑎)) |
| 26 | | risset 3233 |
. . . 4
⊢ (𝑥 ∈ 𝐴 ↔ ∃𝑎 ∈ 𝐴 𝑎 = 𝑥) |
| 27 | 20, 25, 26 | 3bitr4g 314 |
. . 3
⊢ ((𝐺 ∈ Grp ∧ 𝐴 ⊆ 𝐵 ∧ 𝐴 ≠ ∅) → (∃𝑜 ∈ { 0 }∃𝑎 ∈ 𝐴 𝑥 = (𝑜(+g‘𝐺)𝑎) ↔ 𝑥 ∈ 𝐴)) |
| 28 | 11, 27 | bitrd 279 |
. 2
⊢ ((𝐺 ∈ Grp ∧ 𝐴 ⊆ 𝐵 ∧ 𝐴 ≠ ∅) → (𝑥 ∈ ({ 0 } ⊕ 𝐴) ↔ 𝑥 ∈ 𝐴)) |
| 29 | 28 | eqrdv 2735 |
1
⊢ ((𝐺 ∈ Grp ∧ 𝐴 ⊆ 𝐵 ∧ 𝐴 ≠ ∅) → ({ 0 } ⊕ 𝐴) = 𝐴) |