Step |
Hyp |
Ref |
Expression |
1 |
|
grplsm0l.b |
⊢ 𝐵 = ( Base ‘ 𝐺 ) |
2 |
|
grplsm0l.p |
⊢ ⊕ = ( LSSum ‘ 𝐺 ) |
3 |
|
grplsm0l.0 |
⊢ 0 = ( 0g ‘ 𝐺 ) |
4 |
1 3
|
grpidcl |
⊢ ( 𝐺 ∈ Grp → 0 ∈ 𝐵 ) |
5 |
4
|
snssd |
⊢ ( 𝐺 ∈ Grp → { 0 } ⊆ 𝐵 ) |
6 |
|
eqid |
⊢ ( +g ‘ 𝐺 ) = ( +g ‘ 𝐺 ) |
7 |
1 6 2
|
lsmelvalx |
⊢ ( ( 𝐺 ∈ Grp ∧ { 0 } ⊆ 𝐵 ∧ 𝐴 ⊆ 𝐵 ) → ( 𝑥 ∈ ( { 0 } ⊕ 𝐴 ) ↔ ∃ 𝑜 ∈ { 0 } ∃ 𝑎 ∈ 𝐴 𝑥 = ( 𝑜 ( +g ‘ 𝐺 ) 𝑎 ) ) ) |
8 |
7
|
3expa |
⊢ ( ( ( 𝐺 ∈ Grp ∧ { 0 } ⊆ 𝐵 ) ∧ 𝐴 ⊆ 𝐵 ) → ( 𝑥 ∈ ( { 0 } ⊕ 𝐴 ) ↔ ∃ 𝑜 ∈ { 0 } ∃ 𝑎 ∈ 𝐴 𝑥 = ( 𝑜 ( +g ‘ 𝐺 ) 𝑎 ) ) ) |
9 |
8
|
an32s |
⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝐴 ⊆ 𝐵 ) ∧ { 0 } ⊆ 𝐵 ) → ( 𝑥 ∈ ( { 0 } ⊕ 𝐴 ) ↔ ∃ 𝑜 ∈ { 0 } ∃ 𝑎 ∈ 𝐴 𝑥 = ( 𝑜 ( +g ‘ 𝐺 ) 𝑎 ) ) ) |
10 |
5 9
|
mpidan |
⊢ ( ( 𝐺 ∈ Grp ∧ 𝐴 ⊆ 𝐵 ) → ( 𝑥 ∈ ( { 0 } ⊕ 𝐴 ) ↔ ∃ 𝑜 ∈ { 0 } ∃ 𝑎 ∈ 𝐴 𝑥 = ( 𝑜 ( +g ‘ 𝐺 ) 𝑎 ) ) ) |
11 |
10
|
3adant3 |
⊢ ( ( 𝐺 ∈ Grp ∧ 𝐴 ⊆ 𝐵 ∧ 𝐴 ≠ ∅ ) → ( 𝑥 ∈ ( { 0 } ⊕ 𝐴 ) ↔ ∃ 𝑜 ∈ { 0 } ∃ 𝑎 ∈ 𝐴 𝑥 = ( 𝑜 ( +g ‘ 𝐺 ) 𝑎 ) ) ) |
12 |
|
simpl1 |
⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝐴 ⊆ 𝐵 ∧ 𝐴 ≠ ∅ ) ∧ 𝑎 ∈ 𝐴 ) → 𝐺 ∈ Grp ) |
13 |
|
simp2 |
⊢ ( ( 𝐺 ∈ Grp ∧ 𝐴 ⊆ 𝐵 ∧ 𝐴 ≠ ∅ ) → 𝐴 ⊆ 𝐵 ) |
14 |
13
|
sselda |
⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝐴 ⊆ 𝐵 ∧ 𝐴 ≠ ∅ ) ∧ 𝑎 ∈ 𝐴 ) → 𝑎 ∈ 𝐵 ) |
15 |
1 6 3
|
grplid |
⊢ ( ( 𝐺 ∈ Grp ∧ 𝑎 ∈ 𝐵 ) → ( 0 ( +g ‘ 𝐺 ) 𝑎 ) = 𝑎 ) |
16 |
12 14 15
|
syl2anc |
⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝐴 ⊆ 𝐵 ∧ 𝐴 ≠ ∅ ) ∧ 𝑎 ∈ 𝐴 ) → ( 0 ( +g ‘ 𝐺 ) 𝑎 ) = 𝑎 ) |
17 |
16
|
eqeq2d |
⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝐴 ⊆ 𝐵 ∧ 𝐴 ≠ ∅ ) ∧ 𝑎 ∈ 𝐴 ) → ( 𝑥 = ( 0 ( +g ‘ 𝐺 ) 𝑎 ) ↔ 𝑥 = 𝑎 ) ) |
18 |
|
equcom |
⊢ ( 𝑥 = 𝑎 ↔ 𝑎 = 𝑥 ) |
19 |
17 18
|
bitrdi |
⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝐴 ⊆ 𝐵 ∧ 𝐴 ≠ ∅ ) ∧ 𝑎 ∈ 𝐴 ) → ( 𝑥 = ( 0 ( +g ‘ 𝐺 ) 𝑎 ) ↔ 𝑎 = 𝑥 ) ) |
20 |
19
|
rexbidva |
⊢ ( ( 𝐺 ∈ Grp ∧ 𝐴 ⊆ 𝐵 ∧ 𝐴 ≠ ∅ ) → ( ∃ 𝑎 ∈ 𝐴 𝑥 = ( 0 ( +g ‘ 𝐺 ) 𝑎 ) ↔ ∃ 𝑎 ∈ 𝐴 𝑎 = 𝑥 ) ) |
21 |
3
|
fvexi |
⊢ 0 ∈ V |
22 |
|
oveq1 |
⊢ ( 𝑜 = 0 → ( 𝑜 ( +g ‘ 𝐺 ) 𝑎 ) = ( 0 ( +g ‘ 𝐺 ) 𝑎 ) ) |
23 |
22
|
eqeq2d |
⊢ ( 𝑜 = 0 → ( 𝑥 = ( 𝑜 ( +g ‘ 𝐺 ) 𝑎 ) ↔ 𝑥 = ( 0 ( +g ‘ 𝐺 ) 𝑎 ) ) ) |
24 |
23
|
rexbidv |
⊢ ( 𝑜 = 0 → ( ∃ 𝑎 ∈ 𝐴 𝑥 = ( 𝑜 ( +g ‘ 𝐺 ) 𝑎 ) ↔ ∃ 𝑎 ∈ 𝐴 𝑥 = ( 0 ( +g ‘ 𝐺 ) 𝑎 ) ) ) |
25 |
21 24
|
rexsn |
⊢ ( ∃ 𝑜 ∈ { 0 } ∃ 𝑎 ∈ 𝐴 𝑥 = ( 𝑜 ( +g ‘ 𝐺 ) 𝑎 ) ↔ ∃ 𝑎 ∈ 𝐴 𝑥 = ( 0 ( +g ‘ 𝐺 ) 𝑎 ) ) |
26 |
|
risset |
⊢ ( 𝑥 ∈ 𝐴 ↔ ∃ 𝑎 ∈ 𝐴 𝑎 = 𝑥 ) |
27 |
20 25 26
|
3bitr4g |
⊢ ( ( 𝐺 ∈ Grp ∧ 𝐴 ⊆ 𝐵 ∧ 𝐴 ≠ ∅ ) → ( ∃ 𝑜 ∈ { 0 } ∃ 𝑎 ∈ 𝐴 𝑥 = ( 𝑜 ( +g ‘ 𝐺 ) 𝑎 ) ↔ 𝑥 ∈ 𝐴 ) ) |
28 |
11 27
|
bitrd |
⊢ ( ( 𝐺 ∈ Grp ∧ 𝐴 ⊆ 𝐵 ∧ 𝐴 ≠ ∅ ) → ( 𝑥 ∈ ( { 0 } ⊕ 𝐴 ) ↔ 𝑥 ∈ 𝐴 ) ) |
29 |
28
|
eqrdv |
⊢ ( ( 𝐺 ∈ Grp ∧ 𝐴 ⊆ 𝐵 ∧ 𝐴 ≠ ∅ ) → ( { 0 } ⊕ 𝐴 ) = 𝐴 ) |