Step |
Hyp |
Ref |
Expression |
1 |
|
lsmelvalm.m |
|- .- = ( -g ` G ) |
2 |
|
lsmelvalm.p |
|- .(+) = ( LSSum ` G ) |
3 |
|
lsmelvalm.t |
|- ( ph -> T e. ( SubGrp ` G ) ) |
4 |
|
lsmelvalm.u |
|- ( ph -> U e. ( SubGrp ` G ) ) |
5 |
|
lsmelvalmi.x |
|- ( ph -> X e. T ) |
6 |
|
lsmelvalmi.y |
|- ( ph -> Y e. U ) |
7 |
|
eqidd |
|- ( ph -> ( X .- Y ) = ( X .- Y ) ) |
8 |
|
rspceov |
|- ( ( X e. T /\ Y e. U /\ ( X .- Y ) = ( X .- Y ) ) -> E. x e. T E. y e. U ( X .- Y ) = ( x .- y ) ) |
9 |
5 6 7 8
|
syl3anc |
|- ( ph -> E. x e. T E. y e. U ( X .- Y ) = ( x .- y ) ) |
10 |
1 2 3 4
|
lsmelvalm |
|- ( ph -> ( ( X .- Y ) e. ( T .(+) U ) <-> E. x e. T E. y e. U ( X .- Y ) = ( x .- y ) ) ) |
11 |
9 10
|
mpbird |
|- ( ph -> ( X .- Y ) e. ( T .(+) U ) ) |