Metamath Proof Explorer


Theorem lsmelvalm

Description: Subgroup sum membership analogue of lsmelval using vector subtraction. TODO: any way to shorten proof? (Contributed by NM, 16-Mar-2015) (Revised by Mario Carneiro, 19-Apr-2016)

Ref Expression
Hypotheses lsmelvalm.m
|- .- = ( -g ` G )
lsmelvalm.p
|- .(+) = ( LSSum ` G )
lsmelvalm.t
|- ( ph -> T e. ( SubGrp ` G ) )
lsmelvalm.u
|- ( ph -> U e. ( SubGrp ` G ) )
Assertion lsmelvalm
|- ( ph -> ( X e. ( T .(+) U ) <-> E. y e. T E. z e. U X = ( y .- z ) ) )

Proof

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 eqid
 |-  ( +g ` G ) = ( +g ` G )
6 5 2 lsmelval
 |-  ( ( T e. ( SubGrp ` G ) /\ U e. ( SubGrp ` G ) ) -> ( X e. ( T .(+) U ) <-> E. y e. T E. x e. U X = ( y ( +g ` G ) x ) ) )
7 3 4 6 syl2anc
 |-  ( ph -> ( X e. ( T .(+) U ) <-> E. y e. T E. x e. U X = ( y ( +g ` G ) x ) ) )
8 4 adantr
 |-  ( ( ph /\ y e. T ) -> U e. ( SubGrp ` G ) )
9 eqid
 |-  ( invg ` G ) = ( invg ` G )
10 9 subginvcl
 |-  ( ( U e. ( SubGrp ` G ) /\ x e. U ) -> ( ( invg ` G ) ` x ) e. U )
11 8 10 sylan
 |-  ( ( ( ph /\ y e. T ) /\ x e. U ) -> ( ( invg ` G ) ` x ) e. U )
12 eqid
 |-  ( Base ` G ) = ( Base ` G )
13 subgrcl
 |-  ( T e. ( SubGrp ` G ) -> G e. Grp )
14 3 13 syl
 |-  ( ph -> G e. Grp )
15 14 ad2antrr
 |-  ( ( ( ph /\ y e. T ) /\ x e. U ) -> G e. Grp )
16 12 subgss
 |-  ( T e. ( SubGrp ` G ) -> T C_ ( Base ` G ) )
17 3 16 syl
 |-  ( ph -> T C_ ( Base ` G ) )
18 17 sselda
 |-  ( ( ph /\ y e. T ) -> y e. ( Base ` G ) )
19 18 adantr
 |-  ( ( ( ph /\ y e. T ) /\ x e. U ) -> y e. ( Base ` G ) )
20 12 subgss
 |-  ( U e. ( SubGrp ` G ) -> U C_ ( Base ` G ) )
21 8 20 syl
 |-  ( ( ph /\ y e. T ) -> U C_ ( Base ` G ) )
22 21 sselda
 |-  ( ( ( ph /\ y e. T ) /\ x e. U ) -> x e. ( Base ` G ) )
23 12 5 1 9 15 19 22 grpsubinv
 |-  ( ( ( ph /\ y e. T ) /\ x e. U ) -> ( y .- ( ( invg ` G ) ` x ) ) = ( y ( +g ` G ) x ) )
24 23 eqcomd
 |-  ( ( ( ph /\ y e. T ) /\ x e. U ) -> ( y ( +g ` G ) x ) = ( y .- ( ( invg ` G ) ` x ) ) )
25 oveq2
 |-  ( z = ( ( invg ` G ) ` x ) -> ( y .- z ) = ( y .- ( ( invg ` G ) ` x ) ) )
26 25 rspceeqv
 |-  ( ( ( ( invg ` G ) ` x ) e. U /\ ( y ( +g ` G ) x ) = ( y .- ( ( invg ` G ) ` x ) ) ) -> E. z e. U ( y ( +g ` G ) x ) = ( y .- z ) )
27 11 24 26 syl2anc
 |-  ( ( ( ph /\ y e. T ) /\ x e. U ) -> E. z e. U ( y ( +g ` G ) x ) = ( y .- z ) )
28 eqeq1
 |-  ( X = ( y ( +g ` G ) x ) -> ( X = ( y .- z ) <-> ( y ( +g ` G ) x ) = ( y .- z ) ) )
29 28 rexbidv
 |-  ( X = ( y ( +g ` G ) x ) -> ( E. z e. U X = ( y .- z ) <-> E. z e. U ( y ( +g ` G ) x ) = ( y .- z ) ) )
30 27 29 syl5ibrcom
 |-  ( ( ( ph /\ y e. T ) /\ x e. U ) -> ( X = ( y ( +g ` G ) x ) -> E. z e. U X = ( y .- z ) ) )
31 30 rexlimdva
 |-  ( ( ph /\ y e. T ) -> ( E. x e. U X = ( y ( +g ` G ) x ) -> E. z e. U X = ( y .- z ) ) )
32 9 subginvcl
 |-  ( ( U e. ( SubGrp ` G ) /\ z e. U ) -> ( ( invg ` G ) ` z ) e. U )
33 8 32 sylan
 |-  ( ( ( ph /\ y e. T ) /\ z e. U ) -> ( ( invg ` G ) ` z ) e. U )
34 18 adantr
 |-  ( ( ( ph /\ y e. T ) /\ z e. U ) -> y e. ( Base ` G ) )
35 21 sselda
 |-  ( ( ( ph /\ y e. T ) /\ z e. U ) -> z e. ( Base ` G ) )
36 12 5 9 1 grpsubval
 |-  ( ( y e. ( Base ` G ) /\ z e. ( Base ` G ) ) -> ( y .- z ) = ( y ( +g ` G ) ( ( invg ` G ) ` z ) ) )
37 34 35 36 syl2anc
 |-  ( ( ( ph /\ y e. T ) /\ z e. U ) -> ( y .- z ) = ( y ( +g ` G ) ( ( invg ` G ) ` z ) ) )
38 oveq2
 |-  ( x = ( ( invg ` G ) ` z ) -> ( y ( +g ` G ) x ) = ( y ( +g ` G ) ( ( invg ` G ) ` z ) ) )
39 38 rspceeqv
 |-  ( ( ( ( invg ` G ) ` z ) e. U /\ ( y .- z ) = ( y ( +g ` G ) ( ( invg ` G ) ` z ) ) ) -> E. x e. U ( y .- z ) = ( y ( +g ` G ) x ) )
40 33 37 39 syl2anc
 |-  ( ( ( ph /\ y e. T ) /\ z e. U ) -> E. x e. U ( y .- z ) = ( y ( +g ` G ) x ) )
41 eqeq1
 |-  ( X = ( y .- z ) -> ( X = ( y ( +g ` G ) x ) <-> ( y .- z ) = ( y ( +g ` G ) x ) ) )
42 41 rexbidv
 |-  ( X = ( y .- z ) -> ( E. x e. U X = ( y ( +g ` G ) x ) <-> E. x e. U ( y .- z ) = ( y ( +g ` G ) x ) ) )
43 40 42 syl5ibrcom
 |-  ( ( ( ph /\ y e. T ) /\ z e. U ) -> ( X = ( y .- z ) -> E. x e. U X = ( y ( +g ` G ) x ) ) )
44 43 rexlimdva
 |-  ( ( ph /\ y e. T ) -> ( E. z e. U X = ( y .- z ) -> E. x e. U X = ( y ( +g ` G ) x ) ) )
45 31 44 impbid
 |-  ( ( ph /\ y e. T ) -> ( E. x e. U X = ( y ( +g ` G ) x ) <-> E. z e. U X = ( y .- z ) ) )
46 45 rexbidva
 |-  ( ph -> ( E. y e. T E. x e. U X = ( y ( +g ` G ) x ) <-> E. y e. T E. z e. U X = ( y .- z ) ) )
47 7 46 bitrd
 |-  ( ph -> ( X e. ( T .(+) U ) <-> E. y e. T E. z e. U X = ( y .- z ) ) )