This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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