Metamath Proof Explorer


Theorem mplsubglem

Description: If A is an ideal of sets (a nonempty collection closed under subset and binary union) of the set D of finite bags (the primary applications being A = Fin and A = ~P B for some B ), then the set of all power series whose coefficient functions are supported on an element of A is a subgroup of the set of all power series. (Contributed by Mario Carneiro, 12-Jan-2015) (Revised by AV, 16-Jul-2019)

Ref Expression
Hypotheses mplsubglem.s 𝑆 = ( 𝐼 mPwSer 𝑅 )
mplsubglem.b 𝐵 = ( Base ‘ 𝑆 )
mplsubglem.z 0 = ( 0g𝑅 )
mplsubglem.d 𝐷 = { 𝑓 ∈ ( ℕ0m 𝐼 ) ∣ ( 𝑓 “ ℕ ) ∈ Fin }
mplsubglem.i ( 𝜑𝐼𝑊 )
mplsubglem.0 ( 𝜑 → ∅ ∈ 𝐴 )
mplsubglem.a ( ( 𝜑 ∧ ( 𝑥𝐴𝑦𝐴 ) ) → ( 𝑥𝑦 ) ∈ 𝐴 )
mplsubglem.y ( ( 𝜑 ∧ ( 𝑥𝐴𝑦𝑥 ) ) → 𝑦𝐴 )
mplsubglem.u ( 𝜑𝑈 = { 𝑔𝐵 ∣ ( 𝑔 supp 0 ) ∈ 𝐴 } )
mplsubglem.r ( 𝜑𝑅 ∈ Grp )
Assertion mplsubglem ( 𝜑𝑈 ∈ ( SubGrp ‘ 𝑆 ) )

Proof

Step Hyp Ref Expression
1 mplsubglem.s 𝑆 = ( 𝐼 mPwSer 𝑅 )
2 mplsubglem.b 𝐵 = ( Base ‘ 𝑆 )
3 mplsubglem.z 0 = ( 0g𝑅 )
4 mplsubglem.d 𝐷 = { 𝑓 ∈ ( ℕ0m 𝐼 ) ∣ ( 𝑓 “ ℕ ) ∈ Fin }
5 mplsubglem.i ( 𝜑𝐼𝑊 )
6 mplsubglem.0 ( 𝜑 → ∅ ∈ 𝐴 )
7 mplsubglem.a ( ( 𝜑 ∧ ( 𝑥𝐴𝑦𝐴 ) ) → ( 𝑥𝑦 ) ∈ 𝐴 )
8 mplsubglem.y ( ( 𝜑 ∧ ( 𝑥𝐴𝑦𝑥 ) ) → 𝑦𝐴 )
9 mplsubglem.u ( 𝜑𝑈 = { 𝑔𝐵 ∣ ( 𝑔 supp 0 ) ∈ 𝐴 } )
10 mplsubglem.r ( 𝜑𝑅 ∈ Grp )
11 ssrab2 { 𝑔𝐵 ∣ ( 𝑔 supp 0 ) ∈ 𝐴 } ⊆ 𝐵
12 9 11 eqsstrdi ( 𝜑𝑈𝐵 )
13 1 5 10 4 3 2 psr0cl ( 𝜑 → ( 𝐷 × { 0 } ) ∈ 𝐵 )
14 eqid ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 )
15 14 3 grpidcl ( 𝑅 ∈ Grp → 0 ∈ ( Base ‘ 𝑅 ) )
16 fconst6g ( 0 ∈ ( Base ‘ 𝑅 ) → ( 𝐷 × { 0 } ) : 𝐷 ⟶ ( Base ‘ 𝑅 ) )
17 10 15 16 3syl ( 𝜑 → ( 𝐷 × { 0 } ) : 𝐷 ⟶ ( Base ‘ 𝑅 ) )
18 eldifi ( 𝑢 ∈ ( 𝐷 ∖ ∅ ) → 𝑢𝐷 )
19 3 fvexi 0 ∈ V
20 19 fvconst2 ( 𝑢𝐷 → ( ( 𝐷 × { 0 } ) ‘ 𝑢 ) = 0 )
21 18 20 syl ( 𝑢 ∈ ( 𝐷 ∖ ∅ ) → ( ( 𝐷 × { 0 } ) ‘ 𝑢 ) = 0 )
22 21 adantl ( ( 𝜑𝑢 ∈ ( 𝐷 ∖ ∅ ) ) → ( ( 𝐷 × { 0 } ) ‘ 𝑢 ) = 0 )
23 17 22 suppss ( 𝜑 → ( ( 𝐷 × { 0 } ) supp 0 ) ⊆ ∅ )
24 ss0 ( ( ( 𝐷 × { 0 } ) supp 0 ) ⊆ ∅ → ( ( 𝐷 × { 0 } ) supp 0 ) = ∅ )
25 23 24 syl ( 𝜑 → ( ( 𝐷 × { 0 } ) supp 0 ) = ∅ )
26 25 6 eqeltrd ( 𝜑 → ( ( 𝐷 × { 0 } ) supp 0 ) ∈ 𝐴 )
27 9 eleq2d ( 𝜑 → ( ( 𝐷 × { 0 } ) ∈ 𝑈 ↔ ( 𝐷 × { 0 } ) ∈ { 𝑔𝐵 ∣ ( 𝑔 supp 0 ) ∈ 𝐴 } ) )
28 oveq1 ( 𝑔 = ( 𝐷 × { 0 } ) → ( 𝑔 supp 0 ) = ( ( 𝐷 × { 0 } ) supp 0 ) )
29 28 eleq1d ( 𝑔 = ( 𝐷 × { 0 } ) → ( ( 𝑔 supp 0 ) ∈ 𝐴 ↔ ( ( 𝐷 × { 0 } ) supp 0 ) ∈ 𝐴 ) )
30 29 elrab ( ( 𝐷 × { 0 } ) ∈ { 𝑔𝐵 ∣ ( 𝑔 supp 0 ) ∈ 𝐴 } ↔ ( ( 𝐷 × { 0 } ) ∈ 𝐵 ∧ ( ( 𝐷 × { 0 } ) supp 0 ) ∈ 𝐴 ) )
31 27 30 bitrdi ( 𝜑 → ( ( 𝐷 × { 0 } ) ∈ 𝑈 ↔ ( ( 𝐷 × { 0 } ) ∈ 𝐵 ∧ ( ( 𝐷 × { 0 } ) supp 0 ) ∈ 𝐴 ) ) )
32 13 26 31 mpbir2and ( 𝜑 → ( 𝐷 × { 0 } ) ∈ 𝑈 )
33 32 ne0d ( 𝜑𝑈 ≠ ∅ )
34 eqid ( +g𝑆 ) = ( +g𝑆 )
35 10 ad2antrr ( ( ( 𝜑𝑢𝑈 ) ∧ 𝑣𝑈 ) → 𝑅 ∈ Grp )
36 9 eleq2d ( 𝜑 → ( 𝑢𝑈𝑢 ∈ { 𝑔𝐵 ∣ ( 𝑔 supp 0 ) ∈ 𝐴 } ) )
37 oveq1 ( 𝑔 = 𝑢 → ( 𝑔 supp 0 ) = ( 𝑢 supp 0 ) )
38 37 eleq1d ( 𝑔 = 𝑢 → ( ( 𝑔 supp 0 ) ∈ 𝐴 ↔ ( 𝑢 supp 0 ) ∈ 𝐴 ) )
39 38 elrab ( 𝑢 ∈ { 𝑔𝐵 ∣ ( 𝑔 supp 0 ) ∈ 𝐴 } ↔ ( 𝑢𝐵 ∧ ( 𝑢 supp 0 ) ∈ 𝐴 ) )
40 36 39 bitrdi ( 𝜑 → ( 𝑢𝑈 ↔ ( 𝑢𝐵 ∧ ( 𝑢 supp 0 ) ∈ 𝐴 ) ) )
41 40 biimpa ( ( 𝜑𝑢𝑈 ) → ( 𝑢𝐵 ∧ ( 𝑢 supp 0 ) ∈ 𝐴 ) )
42 41 simpld ( ( 𝜑𝑢𝑈 ) → 𝑢𝐵 )
43 42 adantr ( ( ( 𝜑𝑢𝑈 ) ∧ 𝑣𝑈 ) → 𝑢𝐵 )
44 9 adantr ( ( 𝜑𝑢𝑈 ) → 𝑈 = { 𝑔𝐵 ∣ ( 𝑔 supp 0 ) ∈ 𝐴 } )
45 44 eleq2d ( ( 𝜑𝑢𝑈 ) → ( 𝑣𝑈𝑣 ∈ { 𝑔𝐵 ∣ ( 𝑔 supp 0 ) ∈ 𝐴 } ) )
46 oveq1 ( 𝑔 = 𝑣 → ( 𝑔 supp 0 ) = ( 𝑣 supp 0 ) )
47 46 eleq1d ( 𝑔 = 𝑣 → ( ( 𝑔 supp 0 ) ∈ 𝐴 ↔ ( 𝑣 supp 0 ) ∈ 𝐴 ) )
48 47 elrab ( 𝑣 ∈ { 𝑔𝐵 ∣ ( 𝑔 supp 0 ) ∈ 𝐴 } ↔ ( 𝑣𝐵 ∧ ( 𝑣 supp 0 ) ∈ 𝐴 ) )
49 45 48 bitrdi ( ( 𝜑𝑢𝑈 ) → ( 𝑣𝑈 ↔ ( 𝑣𝐵 ∧ ( 𝑣 supp 0 ) ∈ 𝐴 ) ) )
50 49 biimpa ( ( ( 𝜑𝑢𝑈 ) ∧ 𝑣𝑈 ) → ( 𝑣𝐵 ∧ ( 𝑣 supp 0 ) ∈ 𝐴 ) )
51 50 simpld ( ( ( 𝜑𝑢𝑈 ) ∧ 𝑣𝑈 ) → 𝑣𝐵 )
52 1 2 34 35 43 51 psraddcl ( ( ( 𝜑𝑢𝑈 ) ∧ 𝑣𝑈 ) → ( 𝑢 ( +g𝑆 ) 𝑣 ) ∈ 𝐵 )
53 ovexd ( ( ( 𝜑𝑢𝑈 ) ∧ 𝑣𝑈 ) → ( ( 𝑢 ( +g𝑆 ) 𝑣 ) supp 0 ) ∈ V )
54 sseq2 ( 𝑥 = ( ( 𝑢 supp 0 ) ∪ ( 𝑣 supp 0 ) ) → ( 𝑦𝑥𝑦 ⊆ ( ( 𝑢 supp 0 ) ∪ ( 𝑣 supp 0 ) ) ) )
55 54 imbi1d ( 𝑥 = ( ( 𝑢 supp 0 ) ∪ ( 𝑣 supp 0 ) ) → ( ( 𝑦𝑥𝑦𝐴 ) ↔ ( 𝑦 ⊆ ( ( 𝑢 supp 0 ) ∪ ( 𝑣 supp 0 ) ) → 𝑦𝐴 ) ) )
56 55 albidv ( 𝑥 = ( ( 𝑢 supp 0 ) ∪ ( 𝑣 supp 0 ) ) → ( ∀ 𝑦 ( 𝑦𝑥𝑦𝐴 ) ↔ ∀ 𝑦 ( 𝑦 ⊆ ( ( 𝑢 supp 0 ) ∪ ( 𝑣 supp 0 ) ) → 𝑦𝐴 ) ) )
57 8 expr ( ( 𝜑𝑥𝐴 ) → ( 𝑦𝑥𝑦𝐴 ) )
58 57 alrimiv ( ( 𝜑𝑥𝐴 ) → ∀ 𝑦 ( 𝑦𝑥𝑦𝐴 ) )
59 58 ralrimiva ( 𝜑 → ∀ 𝑥𝐴𝑦 ( 𝑦𝑥𝑦𝐴 ) )
60 59 ad2antrr ( ( ( 𝜑𝑢𝑈 ) ∧ 𝑣𝑈 ) → ∀ 𝑥𝐴𝑦 ( 𝑦𝑥𝑦𝐴 ) )
61 41 simprd ( ( 𝜑𝑢𝑈 ) → ( 𝑢 supp 0 ) ∈ 𝐴 )
62 61 adantr ( ( ( 𝜑𝑢𝑈 ) ∧ 𝑣𝑈 ) → ( 𝑢 supp 0 ) ∈ 𝐴 )
63 50 simprd ( ( ( 𝜑𝑢𝑈 ) ∧ 𝑣𝑈 ) → ( 𝑣 supp 0 ) ∈ 𝐴 )
64 7 ralrimivva ( 𝜑 → ∀ 𝑥𝐴𝑦𝐴 ( 𝑥𝑦 ) ∈ 𝐴 )
65 64 ad2antrr ( ( ( 𝜑𝑢𝑈 ) ∧ 𝑣𝑈 ) → ∀ 𝑥𝐴𝑦𝐴 ( 𝑥𝑦 ) ∈ 𝐴 )
66 uneq1 ( 𝑥 = ( 𝑢 supp 0 ) → ( 𝑥𝑦 ) = ( ( 𝑢 supp 0 ) ∪ 𝑦 ) )
67 66 eleq1d ( 𝑥 = ( 𝑢 supp 0 ) → ( ( 𝑥𝑦 ) ∈ 𝐴 ↔ ( ( 𝑢 supp 0 ) ∪ 𝑦 ) ∈ 𝐴 ) )
68 uneq2 ( 𝑦 = ( 𝑣 supp 0 ) → ( ( 𝑢 supp 0 ) ∪ 𝑦 ) = ( ( 𝑢 supp 0 ) ∪ ( 𝑣 supp 0 ) ) )
69 68 eleq1d ( 𝑦 = ( 𝑣 supp 0 ) → ( ( ( 𝑢 supp 0 ) ∪ 𝑦 ) ∈ 𝐴 ↔ ( ( 𝑢 supp 0 ) ∪ ( 𝑣 supp 0 ) ) ∈ 𝐴 ) )
70 67 69 rspc2va ( ( ( ( 𝑢 supp 0 ) ∈ 𝐴 ∧ ( 𝑣 supp 0 ) ∈ 𝐴 ) ∧ ∀ 𝑥𝐴𝑦𝐴 ( 𝑥𝑦 ) ∈ 𝐴 ) → ( ( 𝑢 supp 0 ) ∪ ( 𝑣 supp 0 ) ) ∈ 𝐴 )
71 62 63 65 70 syl21anc ( ( ( 𝜑𝑢𝑈 ) ∧ 𝑣𝑈 ) → ( ( 𝑢 supp 0 ) ∪ ( 𝑣 supp 0 ) ) ∈ 𝐴 )
72 56 60 71 rspcdva ( ( ( 𝜑𝑢𝑈 ) ∧ 𝑣𝑈 ) → ∀ 𝑦 ( 𝑦 ⊆ ( ( 𝑢 supp 0 ) ∪ ( 𝑣 supp 0 ) ) → 𝑦𝐴 ) )
73 1 14 4 2 52 psrelbas ( ( ( 𝜑𝑢𝑈 ) ∧ 𝑣𝑈 ) → ( 𝑢 ( +g𝑆 ) 𝑣 ) : 𝐷 ⟶ ( Base ‘ 𝑅 ) )
74 eqid ( +g𝑅 ) = ( +g𝑅 )
75 1 2 74 34 43 51 psradd ( ( ( 𝜑𝑢𝑈 ) ∧ 𝑣𝑈 ) → ( 𝑢 ( +g𝑆 ) 𝑣 ) = ( 𝑢f ( +g𝑅 ) 𝑣 ) )
76 75 fveq1d ( ( ( 𝜑𝑢𝑈 ) ∧ 𝑣𝑈 ) → ( ( 𝑢 ( +g𝑆 ) 𝑣 ) ‘ 𝑘 ) = ( ( 𝑢f ( +g𝑅 ) 𝑣 ) ‘ 𝑘 ) )
77 76 adantr ( ( ( ( 𝜑𝑢𝑈 ) ∧ 𝑣𝑈 ) ∧ 𝑘 ∈ ( 𝐷 ∖ ( ( 𝑢 supp 0 ) ∪ ( 𝑣 supp 0 ) ) ) ) → ( ( 𝑢 ( +g𝑆 ) 𝑣 ) ‘ 𝑘 ) = ( ( 𝑢f ( +g𝑅 ) 𝑣 ) ‘ 𝑘 ) )
78 eldifi ( 𝑘 ∈ ( 𝐷 ∖ ( ( 𝑢 supp 0 ) ∪ ( 𝑣 supp 0 ) ) ) → 𝑘𝐷 )
79 1 14 4 2 42 psrelbas ( ( 𝜑𝑢𝑈 ) → 𝑢 : 𝐷 ⟶ ( Base ‘ 𝑅 ) )
80 79 adantr ( ( ( 𝜑𝑢𝑈 ) ∧ 𝑣𝑈 ) → 𝑢 : 𝐷 ⟶ ( Base ‘ 𝑅 ) )
81 80 ffnd ( ( ( 𝜑𝑢𝑈 ) ∧ 𝑣𝑈 ) → 𝑢 Fn 𝐷 )
82 1 14 4 2 51 psrelbas ( ( ( 𝜑𝑢𝑈 ) ∧ 𝑣𝑈 ) → 𝑣 : 𝐷 ⟶ ( Base ‘ 𝑅 ) )
83 82 ffnd ( ( ( 𝜑𝑢𝑈 ) ∧ 𝑣𝑈 ) → 𝑣 Fn 𝐷 )
84 ovex ( ℕ0m 𝐼 ) ∈ V
85 4 84 rabex2 𝐷 ∈ V
86 85 a1i ( ( ( 𝜑𝑢𝑈 ) ∧ 𝑣𝑈 ) → 𝐷 ∈ V )
87 inidm ( 𝐷𝐷 ) = 𝐷
88 eqidd ( ( ( ( 𝜑𝑢𝑈 ) ∧ 𝑣𝑈 ) ∧ 𝑘𝐷 ) → ( 𝑢𝑘 ) = ( 𝑢𝑘 ) )
89 eqidd ( ( ( ( 𝜑𝑢𝑈 ) ∧ 𝑣𝑈 ) ∧ 𝑘𝐷 ) → ( 𝑣𝑘 ) = ( 𝑣𝑘 ) )
90 81 83 86 86 87 88 89 ofval ( ( ( ( 𝜑𝑢𝑈 ) ∧ 𝑣𝑈 ) ∧ 𝑘𝐷 ) → ( ( 𝑢f ( +g𝑅 ) 𝑣 ) ‘ 𝑘 ) = ( ( 𝑢𝑘 ) ( +g𝑅 ) ( 𝑣𝑘 ) ) )
91 78 90 sylan2 ( ( ( ( 𝜑𝑢𝑈 ) ∧ 𝑣𝑈 ) ∧ 𝑘 ∈ ( 𝐷 ∖ ( ( 𝑢 supp 0 ) ∪ ( 𝑣 supp 0 ) ) ) ) → ( ( 𝑢f ( +g𝑅 ) 𝑣 ) ‘ 𝑘 ) = ( ( 𝑢𝑘 ) ( +g𝑅 ) ( 𝑣𝑘 ) ) )
92 ssun1 ( 𝑢 supp 0 ) ⊆ ( ( 𝑢 supp 0 ) ∪ ( 𝑣 supp 0 ) )
93 sscon ( ( 𝑢 supp 0 ) ⊆ ( ( 𝑢 supp 0 ) ∪ ( 𝑣 supp 0 ) ) → ( 𝐷 ∖ ( ( 𝑢 supp 0 ) ∪ ( 𝑣 supp 0 ) ) ) ⊆ ( 𝐷 ∖ ( 𝑢 supp 0 ) ) )
94 92 93 ax-mp ( 𝐷 ∖ ( ( 𝑢 supp 0 ) ∪ ( 𝑣 supp 0 ) ) ) ⊆ ( 𝐷 ∖ ( 𝑢 supp 0 ) )
95 94 sseli ( 𝑘 ∈ ( 𝐷 ∖ ( ( 𝑢 supp 0 ) ∪ ( 𝑣 supp 0 ) ) ) → 𝑘 ∈ ( 𝐷 ∖ ( 𝑢 supp 0 ) ) )
96 ssidd ( ( 𝜑𝑢𝑈 ) → ( 𝑢 supp 0 ) ⊆ ( 𝑢 supp 0 ) )
97 85 a1i ( ( 𝜑𝑢𝑈 ) → 𝐷 ∈ V )
98 19 a1i ( ( 𝜑𝑢𝑈 ) → 0 ∈ V )
99 79 96 97 98 suppssr ( ( ( 𝜑𝑢𝑈 ) ∧ 𝑘 ∈ ( 𝐷 ∖ ( 𝑢 supp 0 ) ) ) → ( 𝑢𝑘 ) = 0 )
100 99 adantlr ( ( ( ( 𝜑𝑢𝑈 ) ∧ 𝑣𝑈 ) ∧ 𝑘 ∈ ( 𝐷 ∖ ( 𝑢 supp 0 ) ) ) → ( 𝑢𝑘 ) = 0 )
101 95 100 sylan2 ( ( ( ( 𝜑𝑢𝑈 ) ∧ 𝑣𝑈 ) ∧ 𝑘 ∈ ( 𝐷 ∖ ( ( 𝑢 supp 0 ) ∪ ( 𝑣 supp 0 ) ) ) ) → ( 𝑢𝑘 ) = 0 )
102 ssun2 ( 𝑣 supp 0 ) ⊆ ( ( 𝑢 supp 0 ) ∪ ( 𝑣 supp 0 ) )
103 sscon ( ( 𝑣 supp 0 ) ⊆ ( ( 𝑢 supp 0 ) ∪ ( 𝑣 supp 0 ) ) → ( 𝐷 ∖ ( ( 𝑢 supp 0 ) ∪ ( 𝑣 supp 0 ) ) ) ⊆ ( 𝐷 ∖ ( 𝑣 supp 0 ) ) )
104 102 103 ax-mp ( 𝐷 ∖ ( ( 𝑢 supp 0 ) ∪ ( 𝑣 supp 0 ) ) ) ⊆ ( 𝐷 ∖ ( 𝑣 supp 0 ) )
105 104 sseli ( 𝑘 ∈ ( 𝐷 ∖ ( ( 𝑢 supp 0 ) ∪ ( 𝑣 supp 0 ) ) ) → 𝑘 ∈ ( 𝐷 ∖ ( 𝑣 supp 0 ) ) )
106 ssidd ( ( ( 𝜑𝑢𝑈 ) ∧ 𝑣𝑈 ) → ( 𝑣 supp 0 ) ⊆ ( 𝑣 supp 0 ) )
107 19 a1i ( ( ( 𝜑𝑢𝑈 ) ∧ 𝑣𝑈 ) → 0 ∈ V )
108 82 106 86 107 suppssr ( ( ( ( 𝜑𝑢𝑈 ) ∧ 𝑣𝑈 ) ∧ 𝑘 ∈ ( 𝐷 ∖ ( 𝑣 supp 0 ) ) ) → ( 𝑣𝑘 ) = 0 )
109 105 108 sylan2 ( ( ( ( 𝜑𝑢𝑈 ) ∧ 𝑣𝑈 ) ∧ 𝑘 ∈ ( 𝐷 ∖ ( ( 𝑢 supp 0 ) ∪ ( 𝑣 supp 0 ) ) ) ) → ( 𝑣𝑘 ) = 0 )
110 101 109 oveq12d ( ( ( ( 𝜑𝑢𝑈 ) ∧ 𝑣𝑈 ) ∧ 𝑘 ∈ ( 𝐷 ∖ ( ( 𝑢 supp 0 ) ∪ ( 𝑣 supp 0 ) ) ) ) → ( ( 𝑢𝑘 ) ( +g𝑅 ) ( 𝑣𝑘 ) ) = ( 0 ( +g𝑅 ) 0 ) )
111 14 74 3 grplid ( ( 𝑅 ∈ Grp ∧ 0 ∈ ( Base ‘ 𝑅 ) ) → ( 0 ( +g𝑅 ) 0 ) = 0 )
112 35 15 111 syl2anc2 ( ( ( 𝜑𝑢𝑈 ) ∧ 𝑣𝑈 ) → ( 0 ( +g𝑅 ) 0 ) = 0 )
113 112 adantr ( ( ( ( 𝜑𝑢𝑈 ) ∧ 𝑣𝑈 ) ∧ 𝑘 ∈ ( 𝐷 ∖ ( ( 𝑢 supp 0 ) ∪ ( 𝑣 supp 0 ) ) ) ) → ( 0 ( +g𝑅 ) 0 ) = 0 )
114 110 113 eqtrd ( ( ( ( 𝜑𝑢𝑈 ) ∧ 𝑣𝑈 ) ∧ 𝑘 ∈ ( 𝐷 ∖ ( ( 𝑢 supp 0 ) ∪ ( 𝑣 supp 0 ) ) ) ) → ( ( 𝑢𝑘 ) ( +g𝑅 ) ( 𝑣𝑘 ) ) = 0 )
115 77 91 114 3eqtrd ( ( ( ( 𝜑𝑢𝑈 ) ∧ 𝑣𝑈 ) ∧ 𝑘 ∈ ( 𝐷 ∖ ( ( 𝑢 supp 0 ) ∪ ( 𝑣 supp 0 ) ) ) ) → ( ( 𝑢 ( +g𝑆 ) 𝑣 ) ‘ 𝑘 ) = 0 )
116 73 115 suppss ( ( ( 𝜑𝑢𝑈 ) ∧ 𝑣𝑈 ) → ( ( 𝑢 ( +g𝑆 ) 𝑣 ) supp 0 ) ⊆ ( ( 𝑢 supp 0 ) ∪ ( 𝑣 supp 0 ) ) )
117 sseq1 ( 𝑦 = ( ( 𝑢 ( +g𝑆 ) 𝑣 ) supp 0 ) → ( 𝑦 ⊆ ( ( 𝑢 supp 0 ) ∪ ( 𝑣 supp 0 ) ) ↔ ( ( 𝑢 ( +g𝑆 ) 𝑣 ) supp 0 ) ⊆ ( ( 𝑢 supp 0 ) ∪ ( 𝑣 supp 0 ) ) ) )
118 eleq1 ( 𝑦 = ( ( 𝑢 ( +g𝑆 ) 𝑣 ) supp 0 ) → ( 𝑦𝐴 ↔ ( ( 𝑢 ( +g𝑆 ) 𝑣 ) supp 0 ) ∈ 𝐴 ) )
119 117 118 imbi12d ( 𝑦 = ( ( 𝑢 ( +g𝑆 ) 𝑣 ) supp 0 ) → ( ( 𝑦 ⊆ ( ( 𝑢 supp 0 ) ∪ ( 𝑣 supp 0 ) ) → 𝑦𝐴 ) ↔ ( ( ( 𝑢 ( +g𝑆 ) 𝑣 ) supp 0 ) ⊆ ( ( 𝑢 supp 0 ) ∪ ( 𝑣 supp 0 ) ) → ( ( 𝑢 ( +g𝑆 ) 𝑣 ) supp 0 ) ∈ 𝐴 ) ) )
120 119 spcgv ( ( ( 𝑢 ( +g𝑆 ) 𝑣 ) supp 0 ) ∈ V → ( ∀ 𝑦 ( 𝑦 ⊆ ( ( 𝑢 supp 0 ) ∪ ( 𝑣 supp 0 ) ) → 𝑦𝐴 ) → ( ( ( 𝑢 ( +g𝑆 ) 𝑣 ) supp 0 ) ⊆ ( ( 𝑢 supp 0 ) ∪ ( 𝑣 supp 0 ) ) → ( ( 𝑢 ( +g𝑆 ) 𝑣 ) supp 0 ) ∈ 𝐴 ) ) )
121 53 72 116 120 syl3c ( ( ( 𝜑𝑢𝑈 ) ∧ 𝑣𝑈 ) → ( ( 𝑢 ( +g𝑆 ) 𝑣 ) supp 0 ) ∈ 𝐴 )
122 9 ad2antrr ( ( ( 𝜑𝑢𝑈 ) ∧ 𝑣𝑈 ) → 𝑈 = { 𝑔𝐵 ∣ ( 𝑔 supp 0 ) ∈ 𝐴 } )
123 122 eleq2d ( ( ( 𝜑𝑢𝑈 ) ∧ 𝑣𝑈 ) → ( ( 𝑢 ( +g𝑆 ) 𝑣 ) ∈ 𝑈 ↔ ( 𝑢 ( +g𝑆 ) 𝑣 ) ∈ { 𝑔𝐵 ∣ ( 𝑔 supp 0 ) ∈ 𝐴 } ) )
124 oveq1 ( 𝑔 = ( 𝑢 ( +g𝑆 ) 𝑣 ) → ( 𝑔 supp 0 ) = ( ( 𝑢 ( +g𝑆 ) 𝑣 ) supp 0 ) )
125 124 eleq1d ( 𝑔 = ( 𝑢 ( +g𝑆 ) 𝑣 ) → ( ( 𝑔 supp 0 ) ∈ 𝐴 ↔ ( ( 𝑢 ( +g𝑆 ) 𝑣 ) supp 0 ) ∈ 𝐴 ) )
126 125 elrab ( ( 𝑢 ( +g𝑆 ) 𝑣 ) ∈ { 𝑔𝐵 ∣ ( 𝑔 supp 0 ) ∈ 𝐴 } ↔ ( ( 𝑢 ( +g𝑆 ) 𝑣 ) ∈ 𝐵 ∧ ( ( 𝑢 ( +g𝑆 ) 𝑣 ) supp 0 ) ∈ 𝐴 ) )
127 123 126 bitrdi ( ( ( 𝜑𝑢𝑈 ) ∧ 𝑣𝑈 ) → ( ( 𝑢 ( +g𝑆 ) 𝑣 ) ∈ 𝑈 ↔ ( ( 𝑢 ( +g𝑆 ) 𝑣 ) ∈ 𝐵 ∧ ( ( 𝑢 ( +g𝑆 ) 𝑣 ) supp 0 ) ∈ 𝐴 ) ) )
128 52 121 127 mpbir2and ( ( ( 𝜑𝑢𝑈 ) ∧ 𝑣𝑈 ) → ( 𝑢 ( +g𝑆 ) 𝑣 ) ∈ 𝑈 )
129 128 ralrimiva ( ( 𝜑𝑢𝑈 ) → ∀ 𝑣𝑈 ( 𝑢 ( +g𝑆 ) 𝑣 ) ∈ 𝑈 )
130 1 5 10 psrgrp ( 𝜑𝑆 ∈ Grp )
131 eqid ( invg𝑆 ) = ( invg𝑆 )
132 2 131 grpinvcl ( ( 𝑆 ∈ Grp ∧ 𝑢𝐵 ) → ( ( invg𝑆 ) ‘ 𝑢 ) ∈ 𝐵 )
133 130 42 132 syl2an2r ( ( 𝜑𝑢𝑈 ) → ( ( invg𝑆 ) ‘ 𝑢 ) ∈ 𝐵 )
134 ovexd ( ( 𝜑𝑢𝑈 ) → ( ( ( invg𝑆 ) ‘ 𝑢 ) supp 0 ) ∈ V )
135 sseq2 ( 𝑥 = ( 𝑢 supp 0 ) → ( 𝑦𝑥𝑦 ⊆ ( 𝑢 supp 0 ) ) )
136 135 imbi1d ( 𝑥 = ( 𝑢 supp 0 ) → ( ( 𝑦𝑥𝑦𝐴 ) ↔ ( 𝑦 ⊆ ( 𝑢 supp 0 ) → 𝑦𝐴 ) ) )
137 136 albidv ( 𝑥 = ( 𝑢 supp 0 ) → ( ∀ 𝑦 ( 𝑦𝑥𝑦𝐴 ) ↔ ∀ 𝑦 ( 𝑦 ⊆ ( 𝑢 supp 0 ) → 𝑦𝐴 ) ) )
138 59 adantr ( ( 𝜑𝑢𝑈 ) → ∀ 𝑥𝐴𝑦 ( 𝑦𝑥𝑦𝐴 ) )
139 137 138 61 rspcdva ( ( 𝜑𝑢𝑈 ) → ∀ 𝑦 ( 𝑦 ⊆ ( 𝑢 supp 0 ) → 𝑦𝐴 ) )
140 5 adantr ( ( 𝜑𝑢𝑈 ) → 𝐼𝑊 )
141 10 adantr ( ( 𝜑𝑢𝑈 ) → 𝑅 ∈ Grp )
142 eqid ( invg𝑅 ) = ( invg𝑅 )
143 1 140 141 4 142 2 131 42 psrneg ( ( 𝜑𝑢𝑈 ) → ( ( invg𝑆 ) ‘ 𝑢 ) = ( ( invg𝑅 ) ∘ 𝑢 ) )
144 143 oveq1d ( ( 𝜑𝑢𝑈 ) → ( ( ( invg𝑆 ) ‘ 𝑢 ) supp 0 ) = ( ( ( invg𝑅 ) ∘ 𝑢 ) supp 0 ) )
145 14 142 grpinvfn ( invg𝑅 ) Fn ( Base ‘ 𝑅 )
146 145 a1i ( ( 𝜑𝑢𝑈 ) → ( invg𝑅 ) Fn ( Base ‘ 𝑅 ) )
147 3 142 grpinvid ( 𝑅 ∈ Grp → ( ( invg𝑅 ) ‘ 0 ) = 0 )
148 141 147 syl ( ( 𝜑𝑢𝑈 ) → ( ( invg𝑅 ) ‘ 0 ) = 0 )
149 146 79 97 98 148 suppcoss ( ( 𝜑𝑢𝑈 ) → ( ( ( invg𝑅 ) ∘ 𝑢 ) supp 0 ) ⊆ ( 𝑢 supp 0 ) )
150 144 149 eqsstrd ( ( 𝜑𝑢𝑈 ) → ( ( ( invg𝑆 ) ‘ 𝑢 ) supp 0 ) ⊆ ( 𝑢 supp 0 ) )
151 sseq1 ( 𝑦 = ( ( ( invg𝑆 ) ‘ 𝑢 ) supp 0 ) → ( 𝑦 ⊆ ( 𝑢 supp 0 ) ↔ ( ( ( invg𝑆 ) ‘ 𝑢 ) supp 0 ) ⊆ ( 𝑢 supp 0 ) ) )
152 eleq1 ( 𝑦 = ( ( ( invg𝑆 ) ‘ 𝑢 ) supp 0 ) → ( 𝑦𝐴 ↔ ( ( ( invg𝑆 ) ‘ 𝑢 ) supp 0 ) ∈ 𝐴 ) )
153 151 152 imbi12d ( 𝑦 = ( ( ( invg𝑆 ) ‘ 𝑢 ) supp 0 ) → ( ( 𝑦 ⊆ ( 𝑢 supp 0 ) → 𝑦𝐴 ) ↔ ( ( ( ( invg𝑆 ) ‘ 𝑢 ) supp 0 ) ⊆ ( 𝑢 supp 0 ) → ( ( ( invg𝑆 ) ‘ 𝑢 ) supp 0 ) ∈ 𝐴 ) ) )
154 153 spcgv ( ( ( ( invg𝑆 ) ‘ 𝑢 ) supp 0 ) ∈ V → ( ∀ 𝑦 ( 𝑦 ⊆ ( 𝑢 supp 0 ) → 𝑦𝐴 ) → ( ( ( ( invg𝑆 ) ‘ 𝑢 ) supp 0 ) ⊆ ( 𝑢 supp 0 ) → ( ( ( invg𝑆 ) ‘ 𝑢 ) supp 0 ) ∈ 𝐴 ) ) )
155 134 139 150 154 syl3c ( ( 𝜑𝑢𝑈 ) → ( ( ( invg𝑆 ) ‘ 𝑢 ) supp 0 ) ∈ 𝐴 )
156 44 eleq2d ( ( 𝜑𝑢𝑈 ) → ( ( ( invg𝑆 ) ‘ 𝑢 ) ∈ 𝑈 ↔ ( ( invg𝑆 ) ‘ 𝑢 ) ∈ { 𝑔𝐵 ∣ ( 𝑔 supp 0 ) ∈ 𝐴 } ) )
157 oveq1 ( 𝑔 = ( ( invg𝑆 ) ‘ 𝑢 ) → ( 𝑔 supp 0 ) = ( ( ( invg𝑆 ) ‘ 𝑢 ) supp 0 ) )
158 157 eleq1d ( 𝑔 = ( ( invg𝑆 ) ‘ 𝑢 ) → ( ( 𝑔 supp 0 ) ∈ 𝐴 ↔ ( ( ( invg𝑆 ) ‘ 𝑢 ) supp 0 ) ∈ 𝐴 ) )
159 158 elrab ( ( ( invg𝑆 ) ‘ 𝑢 ) ∈ { 𝑔𝐵 ∣ ( 𝑔 supp 0 ) ∈ 𝐴 } ↔ ( ( ( invg𝑆 ) ‘ 𝑢 ) ∈ 𝐵 ∧ ( ( ( invg𝑆 ) ‘ 𝑢 ) supp 0 ) ∈ 𝐴 ) )
160 156 159 bitrdi ( ( 𝜑𝑢𝑈 ) → ( ( ( invg𝑆 ) ‘ 𝑢 ) ∈ 𝑈 ↔ ( ( ( invg𝑆 ) ‘ 𝑢 ) ∈ 𝐵 ∧ ( ( ( invg𝑆 ) ‘ 𝑢 ) supp 0 ) ∈ 𝐴 ) ) )
161 133 155 160 mpbir2and ( ( 𝜑𝑢𝑈 ) → ( ( invg𝑆 ) ‘ 𝑢 ) ∈ 𝑈 )
162 129 161 jca ( ( 𝜑𝑢𝑈 ) → ( ∀ 𝑣𝑈 ( 𝑢 ( +g𝑆 ) 𝑣 ) ∈ 𝑈 ∧ ( ( invg𝑆 ) ‘ 𝑢 ) ∈ 𝑈 ) )
163 162 ralrimiva ( 𝜑 → ∀ 𝑢𝑈 ( ∀ 𝑣𝑈 ( 𝑢 ( +g𝑆 ) 𝑣 ) ∈ 𝑈 ∧ ( ( invg𝑆 ) ‘ 𝑢 ) ∈ 𝑈 ) )
164 2 34 131 issubg2 ( 𝑆 ∈ Grp → ( 𝑈 ∈ ( SubGrp ‘ 𝑆 ) ↔ ( 𝑈𝐵𝑈 ≠ ∅ ∧ ∀ 𝑢𝑈 ( ∀ 𝑣𝑈 ( 𝑢 ( +g𝑆 ) 𝑣 ) ∈ 𝑈 ∧ ( ( invg𝑆 ) ‘ 𝑢 ) ∈ 𝑈 ) ) ) )
165 130 164 syl ( 𝜑 → ( 𝑈 ∈ ( SubGrp ‘ 𝑆 ) ↔ ( 𝑈𝐵𝑈 ≠ ∅ ∧ ∀ 𝑢𝑈 ( ∀ 𝑣𝑈 ( 𝑢 ( +g𝑆 ) 𝑣 ) ∈ 𝑈 ∧ ( ( invg𝑆 ) ‘ 𝑢 ) ∈ 𝑈 ) ) ) )
166 12 33 163 165 mpbir3and ( 𝜑𝑈 ∈ ( SubGrp ‘ 𝑆 ) )