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 ) ) )