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 ⊢ 𝐷 = { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ 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 ⊢ 𝐷 = { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ 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 ⊢ ( ℕ0 ↑m 𝐼 ) ∈ 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 ‘ 𝑆 ) )