Metamath Proof Explorer


Theorem psrbagaddclOLD

Description: Obsolete version of psrbagaddcl as of 7-Aug-2024. (Contributed by Mario Carneiro, 9-Jan-2015) (New usage is discouraged.) (Proof modification is discouraged.)

Ref Expression
Hypothesis psrbag.d D = f 0 I | f -1 Fin
Assertion psrbagaddclOLD I V F D G D F + f G D

Proof

Step Hyp Ref Expression
1 psrbag.d D = f 0 I | f -1 Fin
2 nn0addcl x 0 y 0 x + y 0
3 2 adantl I V F D G D x 0 y 0 x + y 0
4 simp2 I V F D G D F D
5 1 psrbag I V F D F : I 0 F -1 Fin
6 5 3ad2ant1 I V F D G D F D F : I 0 F -1 Fin
7 4 6 mpbid I V F D G D F : I 0 F -1 Fin
8 7 simpld I V F D G D F : I 0
9 simp3 I V F D G D G D
10 1 psrbag I V G D G : I 0 G -1 Fin
11 10 3ad2ant1 I V F D G D G D G : I 0 G -1 Fin
12 9 11 mpbid I V F D G D G : I 0 G -1 Fin
13 12 simpld I V F D G D G : I 0
14 simp1 I V F D G D I V
15 inidm I I = I
16 3 8 13 14 14 15 off I V F D G D F + f G : I 0
17 frnnn0supp I V F + f G : I 0 F + f G supp 0 = F + f G -1
18 14 16 17 syl2anc I V F D G D F + f G supp 0 = F + f G -1
19 fvexd I V F D G D x I F x V
20 fvexd I V F D G D x I G x V
21 8 feqmptd I V F D G D F = x I F x
22 13 feqmptd I V F D G D G = x I G x
23 14 19 20 21 22 offval2 I V F D G D F + f G = x I F x + G x
24 23 oveq1d I V F D G D F + f G supp 0 = x I F x + G x supp 0
25 18 24 eqtr3d I V F D G D F + f G -1 = x I F x + G x supp 0
26 frnnn0supp I V F : I 0 F supp 0 = F -1
27 14 8 26 syl2anc I V F D G D F supp 0 = F -1
28 7 simprd I V F D G D F -1 Fin
29 27 28 eqeltrd I V F D G D F supp 0 Fin
30 frnnn0supp I V G : I 0 G supp 0 = G -1
31 14 13 30 syl2anc I V F D G D G supp 0 = G -1
32 12 simprd I V F D G D G -1 Fin
33 31 32 eqeltrd I V F D G D G supp 0 Fin
34 unfi F supp 0 Fin G supp 0 Fin supp 0 F supp 0 G Fin
35 29 33 34 syl2anc I V F D G D supp 0 F supp 0 G Fin
36 ssun1 F supp 0 supp 0 F supp 0 G
37 36 a1i I V F D G D F supp 0 supp 0 F supp 0 G
38 c0ex 0 V
39 38 a1i I V F D G D 0 V
40 8 37 14 39 suppssr I V F D G D x I supp 0 F supp 0 G F x = 0
41 ssun2 G supp 0 supp 0 F supp 0 G
42 41 a1i I V F D G D G supp 0 supp 0 F supp 0 G
43 13 42 14 39 suppssr I V F D G D x I supp 0 F supp 0 G G x = 0
44 40 43 oveq12d I V F D G D x I supp 0 F supp 0 G F x + G x = 0 + 0
45 00id 0 + 0 = 0
46 44 45 eqtrdi I V F D G D x I supp 0 F supp 0 G F x + G x = 0
47 46 14 suppss2 I V F D G D x I F x + G x supp 0 supp 0 F supp 0 G
48 35 47 ssfid I V F D G D x I F x + G x supp 0 Fin
49 25 48 eqeltrd I V F D G D F + f G -1 Fin
50 1 psrbag I V F + f G D F + f G : I 0 F + f G -1 Fin
51 50 3ad2ant1 I V F D G D F + f G D F + f G : I 0 F + f G -1 Fin
52 16 49 51 mpbir2and I V F D G D F + f G D