Step |
Hyp |
Ref |
Expression |
1 |
|
lsmsnorb2.1 |
⊢ 𝐵 = ( Base ‘ 𝐺 ) |
2 |
|
lsmsnorb2.2 |
⊢ + = ( +g ‘ 𝐺 ) |
3 |
|
lsmsnorb2.3 |
⊢ ⊕ = ( LSSum ‘ 𝐺 ) |
4 |
|
lsmsnorb2.4 |
⊢ ∼ = { 〈 𝑥 , 𝑦 〉 ∣ ( { 𝑥 , 𝑦 } ⊆ 𝐵 ∧ ∃ 𝑔 ∈ 𝐴 ( 𝑥 + 𝑔 ) = 𝑦 ) } |
5 |
|
lsmsnorb2.5 |
⊢ ( 𝜑 → 𝐺 ∈ Mnd ) |
6 |
|
lsmsnorb2.6 |
⊢ ( 𝜑 → 𝐴 ⊆ 𝐵 ) |
7 |
|
lsmsnorb2.7 |
⊢ ( 𝜑 → 𝑋 ∈ 𝐵 ) |
8 |
|
eqid |
⊢ ( oppg ‘ 𝐺 ) = ( oppg ‘ 𝐺 ) |
9 |
8 3
|
oppglsm |
⊢ ( 𝐴 ( LSSum ‘ ( oppg ‘ 𝐺 ) ) { 𝑋 } ) = ( { 𝑋 } ⊕ 𝐴 ) |
10 |
8 1
|
oppgbas |
⊢ 𝐵 = ( Base ‘ ( oppg ‘ 𝐺 ) ) |
11 |
|
eqid |
⊢ ( +g ‘ ( oppg ‘ 𝐺 ) ) = ( +g ‘ ( oppg ‘ 𝐺 ) ) |
12 |
|
eqid |
⊢ ( LSSum ‘ ( oppg ‘ 𝐺 ) ) = ( LSSum ‘ ( oppg ‘ 𝐺 ) ) |
13 |
2 8 11
|
oppgplus |
⊢ ( 𝑔 ( +g ‘ ( oppg ‘ 𝐺 ) ) 𝑥 ) = ( 𝑥 + 𝑔 ) |
14 |
13
|
eqeq1i |
⊢ ( ( 𝑔 ( +g ‘ ( oppg ‘ 𝐺 ) ) 𝑥 ) = 𝑦 ↔ ( 𝑥 + 𝑔 ) = 𝑦 ) |
15 |
14
|
rexbii |
⊢ ( ∃ 𝑔 ∈ 𝐴 ( 𝑔 ( +g ‘ ( oppg ‘ 𝐺 ) ) 𝑥 ) = 𝑦 ↔ ∃ 𝑔 ∈ 𝐴 ( 𝑥 + 𝑔 ) = 𝑦 ) |
16 |
15
|
anbi2i |
⊢ ( ( { 𝑥 , 𝑦 } ⊆ 𝐵 ∧ ∃ 𝑔 ∈ 𝐴 ( 𝑔 ( +g ‘ ( oppg ‘ 𝐺 ) ) 𝑥 ) = 𝑦 ) ↔ ( { 𝑥 , 𝑦 } ⊆ 𝐵 ∧ ∃ 𝑔 ∈ 𝐴 ( 𝑥 + 𝑔 ) = 𝑦 ) ) |
17 |
16
|
opabbii |
⊢ { 〈 𝑥 , 𝑦 〉 ∣ ( { 𝑥 , 𝑦 } ⊆ 𝐵 ∧ ∃ 𝑔 ∈ 𝐴 ( 𝑔 ( +g ‘ ( oppg ‘ 𝐺 ) ) 𝑥 ) = 𝑦 ) } = { 〈 𝑥 , 𝑦 〉 ∣ ( { 𝑥 , 𝑦 } ⊆ 𝐵 ∧ ∃ 𝑔 ∈ 𝐴 ( 𝑥 + 𝑔 ) = 𝑦 ) } |
18 |
4 17
|
eqtr4i |
⊢ ∼ = { 〈 𝑥 , 𝑦 〉 ∣ ( { 𝑥 , 𝑦 } ⊆ 𝐵 ∧ ∃ 𝑔 ∈ 𝐴 ( 𝑔 ( +g ‘ ( oppg ‘ 𝐺 ) ) 𝑥 ) = 𝑦 ) } |
19 |
8
|
oppgmnd |
⊢ ( 𝐺 ∈ Mnd → ( oppg ‘ 𝐺 ) ∈ Mnd ) |
20 |
5 19
|
syl |
⊢ ( 𝜑 → ( oppg ‘ 𝐺 ) ∈ Mnd ) |
21 |
10 11 12 18 20 6 7
|
lsmsnorb |
⊢ ( 𝜑 → ( 𝐴 ( LSSum ‘ ( oppg ‘ 𝐺 ) ) { 𝑋 } ) = [ 𝑋 ] ∼ ) |
22 |
9 21
|
eqtr3id |
⊢ ( 𝜑 → ( { 𝑋 } ⊕ 𝐴 ) = [ 𝑋 ] ∼ ) |