Metamath Proof Explorer

Theorem oppglsm

Description: The subspace sum operation in the opposite group. (Contributed by Mario Carneiro, 19-Apr-2016) (Proof shortened by AV, 2-Mar-2024)

Ref Expression
Hypotheses oppglsm.o 
|- O = ( oppG ` G )
oppglsm.p 
|- .(+) = ( LSSum ` G )
Assertion oppglsm 
|- ( T ( LSSum ` O ) U ) = ( U .(+) T )

Proof

Step Hyp Ref Expression
1 oppglsm.o 
 |-  O = ( oppG ` G )
2 oppglsm.p 
 |-  .(+) = ( LSSum ` G )
3 1 fvexi 
 |-  O e. _V
4 eqid 
 |-  ( Base ` G ) = ( Base ` G )
5 1 4 oppgbas 
 |-  ( Base ` G ) = ( Base ` O )
6 eqid 
 |-  ( +g ` O ) = ( +g ` O )
7 eqid 
 |-  ( LSSum ` O ) = ( LSSum ` O )
8 5 6 7 lsmfval 
 |-  ( O e. _V -> ( LSSum ` O ) = ( t e. ~P ( Base ` G ) , u e. ~P ( Base ` G ) |-> ran ( x e. t , y e. u |-> ( x ( +g ` O ) y ) ) ) )
9 3 8 ax-mp 
 |-  ( LSSum ` O ) = ( t e. ~P ( Base ` G ) , u e. ~P ( Base ` G ) |-> ran ( x e. t , y e. u |-> ( x ( +g ` O ) y ) ) )
10 eqid 
 |-  ( +g ` G ) = ( +g ` G )
11 4 10 2 lsmfval 
 |-  ( G e. _V -> .(+) = ( u e. ~P ( Base ` G ) , t e. ~P ( Base ` G ) |-> ran ( y e. u , x e. t |-> ( y ( +g ` G ) x ) ) ) )
12 11 tposeqd 
 |-  ( G e. _V -> tpos .(+) = tpos ( u e. ~P ( Base ` G ) , t e. ~P ( Base ` G ) |-> ran ( y e. u , x e. t |-> ( y ( +g ` G ) x ) ) ) )
13 eqid 
 |-  ( y e. u , x e. t |-> ( y ( +g ` G ) x ) ) = ( y e. u , x e. t |-> ( y ( +g ` G ) x ) )
14 13 reldmmpo 
 |-  Rel dom ( y e. u , x e. t |-> ( y ( +g ` G ) x ) )
15 13 mpofun 
 |-  Fun ( y e. u , x e. t |-> ( y ( +g ` G ) x ) )
16 funforn 
 |-  ( Fun ( y e. u , x e. t |-> ( y ( +g ` G ) x ) ) <-> ( y e. u , x e. t |-> ( y ( +g ` G ) x ) ) : dom ( y e. u , x e. t |-> ( y ( +g ` G ) x ) ) -onto-> ran ( y e. u , x e. t |-> ( y ( +g ` G ) x ) ) )
17 15 16 mpbi 
 |-  ( y e. u , x e. t |-> ( y ( +g ` G ) x ) ) : dom ( y e. u , x e. t |-> ( y ( +g ` G ) x ) ) -onto-> ran ( y e. u , x e. t |-> ( y ( +g ` G ) x ) )
18 tposfo2 
 |-  ( Rel dom ( y e. u , x e. t |-> ( y ( +g ` G ) x ) ) -> ( ( y e. u , x e. t |-> ( y ( +g ` G ) x ) ) : dom ( y e. u , x e. t |-> ( y ( +g ` G ) x ) ) -onto-> ran ( y e. u , x e. t |-> ( y ( +g ` G ) x ) ) -> tpos ( y e. u , x e. t |-> ( y ( +g ` G ) x ) ) : `' dom ( y e. u , x e. t |-> ( y ( +g ` G ) x ) ) -onto-> ran ( y e. u , x e. t |-> ( y ( +g ` G ) x ) ) ) )
19 14 17 18 mp2 
 |-  tpos ( y e. u , x e. t |-> ( y ( +g ` G ) x ) ) : `' dom ( y e. u , x e. t |-> ( y ( +g ` G ) x ) ) -onto-> ran ( y e. u , x e. t |-> ( y ( +g ` G ) x ) )
20 forn 
 |-  ( tpos ( y e. u , x e. t |-> ( y ( +g ` G ) x ) ) : `' dom ( y e. u , x e. t |-> ( y ( +g ` G ) x ) ) -onto-> ran ( y e. u , x e. t |-> ( y ( +g ` G ) x ) ) -> ran tpos ( y e. u , x e. t |-> ( y ( +g ` G ) x ) ) = ran ( y e. u , x e. t |-> ( y ( +g ` G ) x ) ) )
21 19 20 ax-mp 
 |-  ran tpos ( y e. u , x e. t |-> ( y ( +g ` G ) x ) ) = ran ( y e. u , x e. t |-> ( y ( +g ` G ) x ) )
22 10 1 6 oppgplus 
 |-  ( x ( +g ` O ) y ) = ( y ( +g ` G ) x )
23 22 eqcomi 
 |-  ( y ( +g ` G ) x ) = ( x ( +g ` O ) y )
24 23 a1i 
 |-  ( ( y e. u /\ x e. t ) -> ( y ( +g ` G ) x ) = ( x ( +g ` O ) y ) )
25 24 mpoeq3ia 
 |-  ( y e. u , x e. t |-> ( y ( +g ` G ) x ) ) = ( y e. u , x e. t |-> ( x ( +g ` O ) y ) )
26 25 tposmpo 
 |-  tpos ( y e. u , x e. t |-> ( y ( +g ` G ) x ) ) = ( x e. t , y e. u |-> ( x ( +g ` O ) y ) )
27 26 rneqi 
 |-  ran tpos ( y e. u , x e. t |-> ( y ( +g ` G ) x ) ) = ran ( x e. t , y e. u |-> ( x ( +g ` O ) y ) )
28 21 27 eqtr3i 
 |-  ran ( y e. u , x e. t |-> ( y ( +g ` G ) x ) ) = ran ( x e. t , y e. u |-> ( x ( +g ` O ) y ) )
29 28 a1i 
 |-  ( ( u e. ~P ( Base ` G ) /\ t e. ~P ( Base ` G ) ) -> ran ( y e. u , x e. t |-> ( y ( +g ` G ) x ) ) = ran ( x e. t , y e. u |-> ( x ( +g ` O ) y ) ) )
30 29 mpoeq3ia 
 |-  ( u e. ~P ( Base ` G ) , t e. ~P ( Base ` G ) |-> ran ( y e. u , x e. t |-> ( y ( +g ` G ) x ) ) ) = ( u e. ~P ( Base ` G ) , t e. ~P ( Base ` G ) |-> ran ( x e. t , y e. u |-> ( x ( +g ` O ) y ) ) )
31 30 tposmpo 
 |-  tpos ( u e. ~P ( Base ` G ) , t e. ~P ( Base ` G ) |-> ran ( y e. u , x e. t |-> ( y ( +g ` G ) x ) ) ) = ( t e. ~P ( Base ` G ) , u e. ~P ( Base ` G ) |-> ran ( x e. t , y e. u |-> ( x ( +g ` O ) y ) ) )
32 12 31 eqtrdi 
 |-  ( G e. _V -> tpos .(+) = ( t e. ~P ( Base ` G ) , u e. ~P ( Base ` G ) |-> ran ( x e. t , y e. u |-> ( x ( +g ` O ) y ) ) ) )
33 9 32 eqtr4id 
 |-  ( G e. _V -> ( LSSum ` O ) = tpos .(+) )
34 33 oveqd 
 |-  ( G e. _V -> ( T ( LSSum ` O ) U ) = ( T tpos .(+) U ) )
35 ovtpos 
 |-  ( T tpos .(+) U ) = ( U .(+) T )
36 34 35 eqtrdi 
 |-  ( G e. _V -> ( T ( LSSum ` O ) U ) = ( U .(+) T ) )
37 eqid 
 |-  ( t e. ~P ( Base ` G ) , u e. ~P ( Base ` G ) |-> (/) ) = ( t e. ~P ( Base ` G ) , u e. ~P ( Base ` G ) |-> (/) )
38 0ex 
 |-  (/) e. _V
39 eqidd 
 |-  ( ( t = T /\ u = U ) -> (/) = (/) )
40 37 38 39 elovmpo 
 |-  ( x e. ( T ( t e. ~P ( Base ` G ) , u e. ~P ( Base ` G ) |-> (/) ) U ) <-> ( T e. ~P ( Base ` G ) /\ U e. ~P ( Base ` G ) /\ x e. (/) ) )
41 40 simp3bi 
 |-  ( x e. ( T ( t e. ~P ( Base ` G ) , u e. ~P ( Base ` G ) |-> (/) ) U ) -> x e. (/) )
42 41 ssriv 
 |-  ( T ( t e. ~P ( Base ` G ) , u e. ~P ( Base ` G ) |-> (/) ) U ) C_ (/)
43 ss0 
 |-  ( ( T ( t e. ~P ( Base ` G ) , u e. ~P ( Base ` G ) |-> (/) ) U ) C_ (/) -> ( T ( t e. ~P ( Base ` G ) , u e. ~P ( Base ` G ) |-> (/) ) U ) = (/) )
44 42 43 ax-mp 
 |-  ( T ( t e. ~P ( Base ` G ) , u e. ~P ( Base ` G ) |-> (/) ) U ) = (/)
45 elpwi 
 |-  ( t e. ~P ( Base ` G ) -> t C_ ( Base ` G ) )
46 45 3ad2ant2 
 |-  ( ( -. G e. _V /\ t e. ~P ( Base ` G ) /\ u e. ~P ( Base ` G ) ) -> t C_ ( Base ` G ) )
47 fvprc 
 |-  ( -. G e. _V -> ( Base ` G ) = (/) )
48 47 3ad2ant1 
 |-  ( ( -. G e. _V /\ t e. ~P ( Base ` G ) /\ u e. ~P ( Base ` G ) ) -> ( Base ` G ) = (/) )
49 46 48 sseqtrd 
 |-  ( ( -. G e. _V /\ t e. ~P ( Base ` G ) /\ u e. ~P ( Base ` G ) ) -> t C_ (/) )
50 ss0 
 |-  ( t C_ (/) -> t = (/) )
51 49 50 syl 
 |-  ( ( -. G e. _V /\ t e. ~P ( Base ` G ) /\ u e. ~P ( Base ` G ) ) -> t = (/) )
52 51 orcd 
 |-  ( ( -. G e. _V /\ t e. ~P ( Base ` G ) /\ u e. ~P ( Base ` G ) ) -> ( t = (/) \/ u = (/) ) )
53 0mpo0 
 |-  ( ( t = (/) \/ u = (/) ) -> ( x e. t , y e. u |-> ( x ( +g ` O ) y ) ) = (/) )
54 52 53 syl 
 |-  ( ( -. G e. _V /\ t e. ~P ( Base ` G ) /\ u e. ~P ( Base ` G ) ) -> ( x e. t , y e. u |-> ( x ( +g ` O ) y ) ) = (/) )
55 54 rneqd 
 |-  ( ( -. G e. _V /\ t e. ~P ( Base ` G ) /\ u e. ~P ( Base ` G ) ) -> ran ( x e. t , y e. u |-> ( x ( +g ` O ) y ) ) = ran (/) )
56 rn0 
 |-  ran (/) = (/)
57 55 56 eqtrdi 
 |-  ( ( -. G e. _V /\ t e. ~P ( Base ` G ) /\ u e. ~P ( Base ` G ) ) -> ran ( x e. t , y e. u |-> ( x ( +g ` O ) y ) ) = (/) )
58 57 mpoeq3dva 
 |-  ( -. G e. _V -> ( t e. ~P ( Base ` G ) , u e. ~P ( Base ` G ) |-> ran ( x e. t , y e. u |-> ( x ( +g ` O ) y ) ) ) = ( t e. ~P ( Base ` G ) , u e. ~P ( Base ` G ) |-> (/) ) )
59 9 58 syl5eq 
 |-  ( -. G e. _V -> ( LSSum ` O ) = ( t e. ~P ( Base ` G ) , u e. ~P ( Base ` G ) |-> (/) ) )
60 59 oveqd 
 |-  ( -. G e. _V -> ( T ( LSSum ` O ) U ) = ( T ( t e. ~P ( Base ` G ) , u e. ~P ( Base ` G ) |-> (/) ) U ) )
61 fvprc 
 |-  ( -. G e. _V -> ( LSSum ` G ) = (/) )
62 2 61 syl5eq 
 |-  ( -. G e. _V -> .(+) = (/) )
63 62 oveqd 
 |-  ( -. G e. _V -> ( U .(+) T ) = ( U (/) T ) )
64 0ov 
 |-  ( U (/) T ) = (/)
65 63 64 eqtrdi 
 |-  ( -. G e. _V -> ( U .(+) T ) = (/) )
66 44 60 65 3eqtr4a 
 |-  ( -. G e. _V -> ( T ( LSSum ` O ) U ) = ( U .(+) T ) )
67 36 66 pm2.61i 
 |-  ( T ( LSSum ` O ) U ) = ( U .(+) T )