| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | mplsubglem.u | . . 3
⊢ (𝜑 → 𝑈 = {𝑔 ∈ 𝐵 ∣ (𝑔 supp 0 ) ∈ 𝐴}) | 
| 2 |  | ssrab2 4080 | . . 3
⊢ {𝑔 ∈ 𝐵 ∣ (𝑔 supp 0 ) ∈ 𝐴} ⊆ 𝐵 | 
| 3 | 1, 2 | eqsstrdi 4028 | . 2
⊢ (𝜑 → 𝑈 ⊆ 𝐵) | 
| 4 |  | mplsubglem.s | . . . . 5
⊢ 𝑆 = (𝐼 mPwSer 𝑅) | 
| 5 |  | mplsubglem.i | . . . . 5
⊢ (𝜑 → 𝐼 ∈ 𝑊) | 
| 6 |  | mplsubglem.r | . . . . 5
⊢ (𝜑 → 𝑅 ∈ Grp) | 
| 7 |  | mplsubglem.d | . . . . 5
⊢ 𝐷 = {𝑓 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑓 “ ℕ) ∈
Fin} | 
| 8 |  | mplsubglem.z | . . . . 5
⊢  0 =
(0g‘𝑅) | 
| 9 |  | mplsubglem.b | . . . . 5
⊢ 𝐵 = (Base‘𝑆) | 
| 10 | 4, 5, 6, 7, 8, 9 | psr0cl 21972 | . . . 4
⊢ (𝜑 → (𝐷 × { 0 }) ∈ 𝐵) | 
| 11 |  | eqid 2737 | . . . . . . . . 9
⊢
(Base‘𝑅) =
(Base‘𝑅) | 
| 12 | 11, 8 | grpidcl 18983 | . . . . . . . 8
⊢ (𝑅 ∈ Grp → 0 ∈
(Base‘𝑅)) | 
| 13 |  | fconst6g 6797 | . . . . . . . 8
⊢ ( 0 ∈
(Base‘𝑅) →
(𝐷 × { 0 }):𝐷⟶(Base‘𝑅)) | 
| 14 | 6, 12, 13 | 3syl 18 | . . . . . . 7
⊢ (𝜑 → (𝐷 × { 0 }):𝐷⟶(Base‘𝑅)) | 
| 15 |  | eldifi 4131 | . . . . . . . . 9
⊢ (𝑢 ∈ (𝐷 ∖ ∅) → 𝑢 ∈ 𝐷) | 
| 16 | 8 | fvexi 6920 | . . . . . . . . . 10
⊢  0 ∈
V | 
| 17 | 16 | fvconst2 7224 | . . . . . . . . 9
⊢ (𝑢 ∈ 𝐷 → ((𝐷 × { 0 })‘𝑢) = 0 ) | 
| 18 | 15, 17 | syl 17 | . . . . . . . 8
⊢ (𝑢 ∈ (𝐷 ∖ ∅) → ((𝐷 × { 0 })‘𝑢) = 0 ) | 
| 19 | 18 | adantl 481 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑢 ∈ (𝐷 ∖ ∅)) → ((𝐷 × { 0 })‘𝑢) = 0 ) | 
| 20 | 14, 19 | suppss 8219 | . . . . . 6
⊢ (𝜑 → ((𝐷 × { 0 }) supp 0 ) ⊆
∅) | 
| 21 |  | ss0 4402 | . . . . . 6
⊢ (((𝐷 × { 0 }) supp 0 ) ⊆ ∅ →
((𝐷 × { 0 }) supp 0 ) =
∅) | 
| 22 | 20, 21 | syl 17 | . . . . 5
⊢ (𝜑 → ((𝐷 × { 0 }) supp 0 ) =
∅) | 
| 23 |  | mplsubglem.0 | . . . . 5
⊢ (𝜑 → ∅ ∈ 𝐴) | 
| 24 | 22, 23 | eqeltrd 2841 | . . . 4
⊢ (𝜑 → ((𝐷 × { 0 }) supp 0 ) ∈ 𝐴) | 
| 25 | 1 | eleq2d 2827 | . . . . 5
⊢ (𝜑 → ((𝐷 × { 0 }) ∈ 𝑈 ↔ (𝐷 × { 0 }) ∈ {𝑔 ∈ 𝐵 ∣ (𝑔 supp 0 ) ∈ 𝐴})) | 
| 26 |  | oveq1 7438 | . . . . . . 7
⊢ (𝑔 = (𝐷 × { 0 }) → (𝑔 supp 0 ) = ((𝐷 × { 0 }) supp 0 )) | 
| 27 | 26 | eleq1d 2826 | . . . . . 6
⊢ (𝑔 = (𝐷 × { 0 }) → ((𝑔 supp 0 ) ∈ 𝐴 ↔ ((𝐷 × { 0 }) supp 0 ) ∈ 𝐴)) | 
| 28 | 27 | elrab 3692 | . . . . 5
⊢ ((𝐷 × { 0 }) ∈ {𝑔 ∈ 𝐵 ∣ (𝑔 supp 0 ) ∈ 𝐴} ↔ ((𝐷 × { 0 }) ∈ 𝐵 ∧ ((𝐷 × { 0 }) supp 0 ) ∈ 𝐴)) | 
| 29 | 25, 28 | bitrdi 287 | . . . 4
⊢ (𝜑 → ((𝐷 × { 0 }) ∈ 𝑈 ↔ ((𝐷 × { 0 }) ∈ 𝐵 ∧ ((𝐷 × { 0 }) supp 0 ) ∈ 𝐴))) | 
| 30 | 10, 24, 29 | mpbir2and 713 | . . 3
⊢ (𝜑 → (𝐷 × { 0 }) ∈ 𝑈) | 
| 31 | 30 | ne0d 4342 | . 2
⊢ (𝜑 → 𝑈 ≠ ∅) | 
| 32 |  | eqid 2737 | . . . . . . 7
⊢
(+g‘𝑆) = (+g‘𝑆) | 
| 33 | 6 | grpmgmd 18979 | . . . . . . . 8
⊢ (𝜑 → 𝑅 ∈ Mgm) | 
| 34 | 33 | ad2antrr 726 | . . . . . . 7
⊢ (((𝜑 ∧ 𝑢 ∈ 𝑈) ∧ 𝑣 ∈ 𝑈) → 𝑅 ∈ Mgm) | 
| 35 | 1 | eleq2d 2827 | . . . . . . . . . . 11
⊢ (𝜑 → (𝑢 ∈ 𝑈 ↔ 𝑢 ∈ {𝑔 ∈ 𝐵 ∣ (𝑔 supp 0 ) ∈ 𝐴})) | 
| 36 |  | oveq1 7438 | . . . . . . . . . . . . 13
⊢ (𝑔 = 𝑢 → (𝑔 supp 0 ) = (𝑢 supp 0 )) | 
| 37 | 36 | eleq1d 2826 | . . . . . . . . . . . 12
⊢ (𝑔 = 𝑢 → ((𝑔 supp 0 ) ∈ 𝐴 ↔ (𝑢 supp 0 ) ∈ 𝐴)) | 
| 38 | 37 | elrab 3692 | . . . . . . . . . . 11
⊢ (𝑢 ∈ {𝑔 ∈ 𝐵 ∣ (𝑔 supp 0 ) ∈ 𝐴} ↔ (𝑢 ∈ 𝐵 ∧ (𝑢 supp 0 ) ∈ 𝐴)) | 
| 39 | 35, 38 | bitrdi 287 | . . . . . . . . . 10
⊢ (𝜑 → (𝑢 ∈ 𝑈 ↔ (𝑢 ∈ 𝐵 ∧ (𝑢 supp 0 ) ∈ 𝐴))) | 
| 40 | 39 | biimpa 476 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑢 ∈ 𝑈) → (𝑢 ∈ 𝐵 ∧ (𝑢 supp 0 ) ∈ 𝐴)) | 
| 41 | 40 | simpld 494 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑢 ∈ 𝑈) → 𝑢 ∈ 𝐵) | 
| 42 | 41 | adantr 480 | . . . . . . 7
⊢ (((𝜑 ∧ 𝑢 ∈ 𝑈) ∧ 𝑣 ∈ 𝑈) → 𝑢 ∈ 𝐵) | 
| 43 | 1 | adantr 480 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑢 ∈ 𝑈) → 𝑈 = {𝑔 ∈ 𝐵 ∣ (𝑔 supp 0 ) ∈ 𝐴}) | 
| 44 | 43 | eleq2d 2827 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑢 ∈ 𝑈) → (𝑣 ∈ 𝑈 ↔ 𝑣 ∈ {𝑔 ∈ 𝐵 ∣ (𝑔 supp 0 ) ∈ 𝐴})) | 
| 45 |  | oveq1 7438 | . . . . . . . . . . . 12
⊢ (𝑔 = 𝑣 → (𝑔 supp 0 ) = (𝑣 supp 0 )) | 
| 46 | 45 | eleq1d 2826 | . . . . . . . . . . 11
⊢ (𝑔 = 𝑣 → ((𝑔 supp 0 ) ∈ 𝐴 ↔ (𝑣 supp 0 ) ∈ 𝐴)) | 
| 47 | 46 | elrab 3692 | . . . . . . . . . 10
⊢ (𝑣 ∈ {𝑔 ∈ 𝐵 ∣ (𝑔 supp 0 ) ∈ 𝐴} ↔ (𝑣 ∈ 𝐵 ∧ (𝑣 supp 0 ) ∈ 𝐴)) | 
| 48 | 44, 47 | bitrdi 287 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑢 ∈ 𝑈) → (𝑣 ∈ 𝑈 ↔ (𝑣 ∈ 𝐵 ∧ (𝑣 supp 0 ) ∈ 𝐴))) | 
| 49 | 48 | biimpa 476 | . . . . . . . 8
⊢ (((𝜑 ∧ 𝑢 ∈ 𝑈) ∧ 𝑣 ∈ 𝑈) → (𝑣 ∈ 𝐵 ∧ (𝑣 supp 0 ) ∈ 𝐴)) | 
| 50 | 49 | simpld 494 | . . . . . . 7
⊢ (((𝜑 ∧ 𝑢 ∈ 𝑈) ∧ 𝑣 ∈ 𝑈) → 𝑣 ∈ 𝐵) | 
| 51 | 4, 9, 32, 34, 42, 50 | psraddcl 21958 | . . . . . 6
⊢ (((𝜑 ∧ 𝑢 ∈ 𝑈) ∧ 𝑣 ∈ 𝑈) → (𝑢(+g‘𝑆)𝑣) ∈ 𝐵) | 
| 52 |  | ovexd 7466 | . . . . . . 7
⊢ (((𝜑 ∧ 𝑢 ∈ 𝑈) ∧ 𝑣 ∈ 𝑈) → ((𝑢(+g‘𝑆)𝑣) supp 0 ) ∈
V) | 
| 53 |  | sseq2 4010 | . . . . . . . . . 10
⊢ (𝑥 = ((𝑢 supp 0 ) ∪ (𝑣 supp 0 )) → (𝑦 ⊆ 𝑥 ↔ 𝑦 ⊆ ((𝑢 supp 0 ) ∪ (𝑣 supp 0 )))) | 
| 54 | 53 | imbi1d 341 | . . . . . . . . 9
⊢ (𝑥 = ((𝑢 supp 0 ) ∪ (𝑣 supp 0 )) → ((𝑦 ⊆ 𝑥 → 𝑦 ∈ 𝐴) ↔ (𝑦 ⊆ ((𝑢 supp 0 ) ∪ (𝑣 supp 0 )) → 𝑦 ∈ 𝐴))) | 
| 55 | 54 | albidv 1920 | . . . . . . . 8
⊢ (𝑥 = ((𝑢 supp 0 ) ∪ (𝑣 supp 0 )) → (∀𝑦(𝑦 ⊆ 𝑥 → 𝑦 ∈ 𝐴) ↔ ∀𝑦(𝑦 ⊆ ((𝑢 supp 0 ) ∪ (𝑣 supp 0 )) → 𝑦 ∈ 𝐴))) | 
| 56 |  | mplsubglem.y | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ⊆ 𝑥)) → 𝑦 ∈ 𝐴) | 
| 57 | 56 | expr 456 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝑦 ⊆ 𝑥 → 𝑦 ∈ 𝐴)) | 
| 58 | 57 | alrimiv 1927 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ∀𝑦(𝑦 ⊆ 𝑥 → 𝑦 ∈ 𝐴)) | 
| 59 | 58 | ralrimiva 3146 | . . . . . . . . 9
⊢ (𝜑 → ∀𝑥 ∈ 𝐴 ∀𝑦(𝑦 ⊆ 𝑥 → 𝑦 ∈ 𝐴)) | 
| 60 | 59 | ad2antrr 726 | . . . . . . . 8
⊢ (((𝜑 ∧ 𝑢 ∈ 𝑈) ∧ 𝑣 ∈ 𝑈) → ∀𝑥 ∈ 𝐴 ∀𝑦(𝑦 ⊆ 𝑥 → 𝑦 ∈ 𝐴)) | 
| 61 | 40 | simprd 495 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑢 ∈ 𝑈) → (𝑢 supp 0 ) ∈ 𝐴) | 
| 62 | 61 | adantr 480 | . . . . . . . . 9
⊢ (((𝜑 ∧ 𝑢 ∈ 𝑈) ∧ 𝑣 ∈ 𝑈) → (𝑢 supp 0 ) ∈ 𝐴) | 
| 63 | 49 | simprd 495 | . . . . . . . . 9
⊢ (((𝜑 ∧ 𝑢 ∈ 𝑈) ∧ 𝑣 ∈ 𝑈) → (𝑣 supp 0 ) ∈ 𝐴) | 
| 64 |  | mplsubglem.a | . . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴)) → (𝑥 ∪ 𝑦) ∈ 𝐴) | 
| 65 | 64 | ralrimivva 3202 | . . . . . . . . . 10
⊢ (𝜑 → ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥 ∪ 𝑦) ∈ 𝐴) | 
| 66 | 65 | ad2antrr 726 | . . . . . . . . 9
⊢ (((𝜑 ∧ 𝑢 ∈ 𝑈) ∧ 𝑣 ∈ 𝑈) → ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥 ∪ 𝑦) ∈ 𝐴) | 
| 67 |  | uneq1 4161 | . . . . . . . . . . 11
⊢ (𝑥 = (𝑢 supp 0 ) → (𝑥 ∪ 𝑦) = ((𝑢 supp 0 ) ∪ 𝑦)) | 
| 68 | 67 | eleq1d 2826 | . . . . . . . . . 10
⊢ (𝑥 = (𝑢 supp 0 ) → ((𝑥 ∪ 𝑦) ∈ 𝐴 ↔ ((𝑢 supp 0 ) ∪ 𝑦) ∈ 𝐴)) | 
| 69 |  | uneq2 4162 | . . . . . . . . . . 11
⊢ (𝑦 = (𝑣 supp 0 ) → ((𝑢 supp 0 ) ∪ 𝑦) = ((𝑢 supp 0 ) ∪ (𝑣 supp 0 ))) | 
| 70 | 69 | eleq1d 2826 | . . . . . . . . . 10
⊢ (𝑦 = (𝑣 supp 0 ) → (((𝑢 supp 0 ) ∪ 𝑦) ∈ 𝐴 ↔ ((𝑢 supp 0 ) ∪ (𝑣 supp 0 )) ∈ 𝐴)) | 
| 71 | 68, 70 | rspc2va 3634 | . . . . . . . . 9
⊢ ((((𝑢 supp 0 ) ∈ 𝐴 ∧ (𝑣 supp 0 ) ∈ 𝐴) ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥 ∪ 𝑦) ∈ 𝐴) → ((𝑢 supp 0 ) ∪ (𝑣 supp 0 )) ∈ 𝐴) | 
| 72 | 62, 63, 66, 71 | syl21anc 838 | . . . . . . . 8
⊢ (((𝜑 ∧ 𝑢 ∈ 𝑈) ∧ 𝑣 ∈ 𝑈) → ((𝑢 supp 0 ) ∪ (𝑣 supp 0 )) ∈ 𝐴) | 
| 73 | 55, 60, 72 | rspcdva 3623 | . . . . . . 7
⊢ (((𝜑 ∧ 𝑢 ∈ 𝑈) ∧ 𝑣 ∈ 𝑈) → ∀𝑦(𝑦 ⊆ ((𝑢 supp 0 ) ∪ (𝑣 supp 0 )) → 𝑦 ∈ 𝐴)) | 
| 74 | 4, 11, 7, 9, 51 | psrelbas 21954 | . . . . . . . 8
⊢ (((𝜑 ∧ 𝑢 ∈ 𝑈) ∧ 𝑣 ∈ 𝑈) → (𝑢(+g‘𝑆)𝑣):𝐷⟶(Base‘𝑅)) | 
| 75 |  | eqid 2737 | . . . . . . . . . . . 12
⊢
(+g‘𝑅) = (+g‘𝑅) | 
| 76 | 4, 9, 75, 32, 42, 50 | psradd 21957 | . . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑢 ∈ 𝑈) ∧ 𝑣 ∈ 𝑈) → (𝑢(+g‘𝑆)𝑣) = (𝑢 ∘f
(+g‘𝑅)𝑣)) | 
| 77 | 76 | fveq1d 6908 | . . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑢 ∈ 𝑈) ∧ 𝑣 ∈ 𝑈) → ((𝑢(+g‘𝑆)𝑣)‘𝑘) = ((𝑢 ∘f
(+g‘𝑅)𝑣)‘𝑘)) | 
| 78 | 77 | adantr 480 | . . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑢 ∈ 𝑈) ∧ 𝑣 ∈ 𝑈) ∧ 𝑘 ∈ (𝐷 ∖ ((𝑢 supp 0 ) ∪ (𝑣 supp 0 )))) → ((𝑢(+g‘𝑆)𝑣)‘𝑘) = ((𝑢 ∘f
(+g‘𝑅)𝑣)‘𝑘)) | 
| 79 |  | eldifi 4131 | . . . . . . . . . 10
⊢ (𝑘 ∈ (𝐷 ∖ ((𝑢 supp 0 ) ∪ (𝑣 supp 0 ))) → 𝑘 ∈ 𝐷) | 
| 80 | 4, 11, 7, 9, 41 | psrelbas 21954 | . . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑢 ∈ 𝑈) → 𝑢:𝐷⟶(Base‘𝑅)) | 
| 81 | 80 | adantr 480 | . . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑢 ∈ 𝑈) ∧ 𝑣 ∈ 𝑈) → 𝑢:𝐷⟶(Base‘𝑅)) | 
| 82 | 81 | ffnd 6737 | . . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑢 ∈ 𝑈) ∧ 𝑣 ∈ 𝑈) → 𝑢 Fn 𝐷) | 
| 83 | 4, 11, 7, 9, 50 | psrelbas 21954 | . . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑢 ∈ 𝑈) ∧ 𝑣 ∈ 𝑈) → 𝑣:𝐷⟶(Base‘𝑅)) | 
| 84 | 83 | ffnd 6737 | . . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑢 ∈ 𝑈) ∧ 𝑣 ∈ 𝑈) → 𝑣 Fn 𝐷) | 
| 85 |  | ovex 7464 | . . . . . . . . . . . . 13
⊢
(ℕ0 ↑m 𝐼) ∈ V | 
| 86 | 7, 85 | rabex2 5341 | . . . . . . . . . . . 12
⊢ 𝐷 ∈ V | 
| 87 | 86 | a1i 11 | . . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑢 ∈ 𝑈) ∧ 𝑣 ∈ 𝑈) → 𝐷 ∈ V) | 
| 88 |  | inidm 4227 | . . . . . . . . . . 11
⊢ (𝐷 ∩ 𝐷) = 𝐷 | 
| 89 |  | eqidd 2738 | . . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑢 ∈ 𝑈) ∧ 𝑣 ∈ 𝑈) ∧ 𝑘 ∈ 𝐷) → (𝑢‘𝑘) = (𝑢‘𝑘)) | 
| 90 |  | eqidd 2738 | . . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑢 ∈ 𝑈) ∧ 𝑣 ∈ 𝑈) ∧ 𝑘 ∈ 𝐷) → (𝑣‘𝑘) = (𝑣‘𝑘)) | 
| 91 | 82, 84, 87, 87, 88, 89, 90 | ofval 7708 | . . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑢 ∈ 𝑈) ∧ 𝑣 ∈ 𝑈) ∧ 𝑘 ∈ 𝐷) → ((𝑢 ∘f
(+g‘𝑅)𝑣)‘𝑘) = ((𝑢‘𝑘)(+g‘𝑅)(𝑣‘𝑘))) | 
| 92 | 79, 91 | sylan2 593 | . . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑢 ∈ 𝑈) ∧ 𝑣 ∈ 𝑈) ∧ 𝑘 ∈ (𝐷 ∖ ((𝑢 supp 0 ) ∪ (𝑣 supp 0 )))) → ((𝑢 ∘f
(+g‘𝑅)𝑣)‘𝑘) = ((𝑢‘𝑘)(+g‘𝑅)(𝑣‘𝑘))) | 
| 93 |  | ssun1 4178 | . . . . . . . . . . . . . 14
⊢ (𝑢 supp 0 ) ⊆ ((𝑢 supp 0 ) ∪ (𝑣 supp 0 )) | 
| 94 |  | sscon 4143 | . . . . . . . . . . . . . 14
⊢ ((𝑢 supp 0 ) ⊆ ((𝑢 supp 0 ) ∪ (𝑣 supp 0 )) → (𝐷 ∖ ((𝑢 supp 0 ) ∪ (𝑣 supp 0 ))) ⊆ (𝐷 ∖ (𝑢 supp 0 ))) | 
| 95 | 93, 94 | ax-mp 5 | . . . . . . . . . . . . 13
⊢ (𝐷 ∖ ((𝑢 supp 0 ) ∪ (𝑣 supp 0 ))) ⊆ (𝐷 ∖ (𝑢 supp 0 )) | 
| 96 | 95 | sseli 3979 | . . . . . . . . . . . 12
⊢ (𝑘 ∈ (𝐷 ∖ ((𝑢 supp 0 ) ∪ (𝑣 supp 0 ))) → 𝑘 ∈ (𝐷 ∖ (𝑢 supp 0 ))) | 
| 97 |  | ssidd 4007 | . . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑢 ∈ 𝑈) → (𝑢 supp 0 ) ⊆ (𝑢 supp 0 )) | 
| 98 | 86 | a1i 11 | . . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑢 ∈ 𝑈) → 𝐷 ∈ V) | 
| 99 | 16 | a1i 11 | . . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑢 ∈ 𝑈) → 0 ∈ V) | 
| 100 | 80, 97, 98, 99 | suppssr 8220 | . . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑢 ∈ 𝑈) ∧ 𝑘 ∈ (𝐷 ∖ (𝑢 supp 0 ))) → (𝑢‘𝑘) = 0 ) | 
| 101 | 100 | adantlr 715 | . . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝑢 ∈ 𝑈) ∧ 𝑣 ∈ 𝑈) ∧ 𝑘 ∈ (𝐷 ∖ (𝑢 supp 0 ))) → (𝑢‘𝑘) = 0 ) | 
| 102 | 96, 101 | sylan2 593 | . . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑢 ∈ 𝑈) ∧ 𝑣 ∈ 𝑈) ∧ 𝑘 ∈ (𝐷 ∖ ((𝑢 supp 0 ) ∪ (𝑣 supp 0 )))) → (𝑢‘𝑘) = 0 ) | 
| 103 |  | ssun2 4179 | . . . . . . . . . . . . . 14
⊢ (𝑣 supp 0 ) ⊆ ((𝑢 supp 0 ) ∪ (𝑣 supp 0 )) | 
| 104 |  | sscon 4143 | . . . . . . . . . . . . . 14
⊢ ((𝑣 supp 0 ) ⊆ ((𝑢 supp 0 ) ∪ (𝑣 supp 0 )) → (𝐷 ∖ ((𝑢 supp 0 ) ∪ (𝑣 supp 0 ))) ⊆ (𝐷 ∖ (𝑣 supp 0 ))) | 
| 105 | 103, 104 | ax-mp 5 | . . . . . . . . . . . . 13
⊢ (𝐷 ∖ ((𝑢 supp 0 ) ∪ (𝑣 supp 0 ))) ⊆ (𝐷 ∖ (𝑣 supp 0 )) | 
| 106 | 105 | sseli 3979 | . . . . . . . . . . . 12
⊢ (𝑘 ∈ (𝐷 ∖ ((𝑢 supp 0 ) ∪ (𝑣 supp 0 ))) → 𝑘 ∈ (𝐷 ∖ (𝑣 supp 0 ))) | 
| 107 |  | ssidd 4007 | . . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑢 ∈ 𝑈) ∧ 𝑣 ∈ 𝑈) → (𝑣 supp 0 ) ⊆ (𝑣 supp 0 )) | 
| 108 | 16 | a1i 11 | . . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑢 ∈ 𝑈) ∧ 𝑣 ∈ 𝑈) → 0 ∈ V) | 
| 109 | 83, 107, 87, 108 | suppssr 8220 | . . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝑢 ∈ 𝑈) ∧ 𝑣 ∈ 𝑈) ∧ 𝑘 ∈ (𝐷 ∖ (𝑣 supp 0 ))) → (𝑣‘𝑘) = 0 ) | 
| 110 | 106, 109 | sylan2 593 | . . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑢 ∈ 𝑈) ∧ 𝑣 ∈ 𝑈) ∧ 𝑘 ∈ (𝐷 ∖ ((𝑢 supp 0 ) ∪ (𝑣 supp 0 )))) → (𝑣‘𝑘) = 0 ) | 
| 111 | 102, 110 | oveq12d 7449 | . . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑢 ∈ 𝑈) ∧ 𝑣 ∈ 𝑈) ∧ 𝑘 ∈ (𝐷 ∖ ((𝑢 supp 0 ) ∪ (𝑣 supp 0 )))) → ((𝑢‘𝑘)(+g‘𝑅)(𝑣‘𝑘)) = ( 0 (+g‘𝑅) 0 )) | 
| 112 | 6 | ad2antrr 726 | . . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑢 ∈ 𝑈) ∧ 𝑣 ∈ 𝑈) → 𝑅 ∈ Grp) | 
| 113 | 11, 75, 8 | grplid 18985 | . . . . . . . . . . . 12
⊢ ((𝑅 ∈ Grp ∧ 0 ∈
(Base‘𝑅)) → (
0
(+g‘𝑅)
0 ) =
0
) | 
| 114 | 112, 12, 113 | syl2anc2 585 | . . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑢 ∈ 𝑈) ∧ 𝑣 ∈ 𝑈) → ( 0 (+g‘𝑅) 0 ) = 0 ) | 
| 115 | 114 | adantr 480 | . . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑢 ∈ 𝑈) ∧ 𝑣 ∈ 𝑈) ∧ 𝑘 ∈ (𝐷 ∖ ((𝑢 supp 0 ) ∪ (𝑣 supp 0 )))) → ( 0
(+g‘𝑅)
0 ) =
0
) | 
| 116 | 111, 115 | eqtrd 2777 | . . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑢 ∈ 𝑈) ∧ 𝑣 ∈ 𝑈) ∧ 𝑘 ∈ (𝐷 ∖ ((𝑢 supp 0 ) ∪ (𝑣 supp 0 )))) → ((𝑢‘𝑘)(+g‘𝑅)(𝑣‘𝑘)) = 0 ) | 
| 117 | 78, 92, 116 | 3eqtrd 2781 | . . . . . . . 8
⊢ ((((𝜑 ∧ 𝑢 ∈ 𝑈) ∧ 𝑣 ∈ 𝑈) ∧ 𝑘 ∈ (𝐷 ∖ ((𝑢 supp 0 ) ∪ (𝑣 supp 0 )))) → ((𝑢(+g‘𝑆)𝑣)‘𝑘) = 0 ) | 
| 118 | 74, 117 | suppss 8219 | . . . . . . 7
⊢ (((𝜑 ∧ 𝑢 ∈ 𝑈) ∧ 𝑣 ∈ 𝑈) → ((𝑢(+g‘𝑆)𝑣) supp 0 ) ⊆ ((𝑢 supp 0 ) ∪ (𝑣 supp 0 ))) | 
| 119 |  | sseq1 4009 | . . . . . . . . 9
⊢ (𝑦 = ((𝑢(+g‘𝑆)𝑣) supp 0 ) → (𝑦 ⊆ ((𝑢 supp 0 ) ∪ (𝑣 supp 0 )) ↔ ((𝑢(+g‘𝑆)𝑣) supp 0 ) ⊆ ((𝑢 supp 0 ) ∪ (𝑣 supp 0 )))) | 
| 120 |  | eleq1 2829 | . . . . . . . . 9
⊢ (𝑦 = ((𝑢(+g‘𝑆)𝑣) supp 0 ) → (𝑦 ∈ 𝐴 ↔ ((𝑢(+g‘𝑆)𝑣) supp 0 ) ∈ 𝐴)) | 
| 121 | 119, 120 | imbi12d 344 | . . . . . . . 8
⊢ (𝑦 = ((𝑢(+g‘𝑆)𝑣) supp 0 ) → ((𝑦 ⊆ ((𝑢 supp 0 ) ∪ (𝑣 supp 0 )) → 𝑦 ∈ 𝐴) ↔ (((𝑢(+g‘𝑆)𝑣) supp 0 ) ⊆ ((𝑢 supp 0 ) ∪ (𝑣 supp 0 )) → ((𝑢(+g‘𝑆)𝑣) supp 0 ) ∈ 𝐴))) | 
| 122 | 121 | spcgv 3596 | . . . . . . 7
⊢ (((𝑢(+g‘𝑆)𝑣) supp 0 ) ∈ V →
(∀𝑦(𝑦 ⊆ ((𝑢 supp 0 ) ∪ (𝑣 supp 0 )) → 𝑦 ∈ 𝐴) → (((𝑢(+g‘𝑆)𝑣) supp 0 ) ⊆ ((𝑢 supp 0 ) ∪ (𝑣 supp 0 )) → ((𝑢(+g‘𝑆)𝑣) supp 0 ) ∈ 𝐴))) | 
| 123 | 52, 73, 118, 122 | syl3c 66 | . . . . . 6
⊢ (((𝜑 ∧ 𝑢 ∈ 𝑈) ∧ 𝑣 ∈ 𝑈) → ((𝑢(+g‘𝑆)𝑣) supp 0 ) ∈ 𝐴) | 
| 124 | 1 | ad2antrr 726 | . . . . . . . 8
⊢ (((𝜑 ∧ 𝑢 ∈ 𝑈) ∧ 𝑣 ∈ 𝑈) → 𝑈 = {𝑔 ∈ 𝐵 ∣ (𝑔 supp 0 ) ∈ 𝐴}) | 
| 125 | 124 | eleq2d 2827 | . . . . . . 7
⊢ (((𝜑 ∧ 𝑢 ∈ 𝑈) ∧ 𝑣 ∈ 𝑈) → ((𝑢(+g‘𝑆)𝑣) ∈ 𝑈 ↔ (𝑢(+g‘𝑆)𝑣) ∈ {𝑔 ∈ 𝐵 ∣ (𝑔 supp 0 ) ∈ 𝐴})) | 
| 126 |  | oveq1 7438 | . . . . . . . . 9
⊢ (𝑔 = (𝑢(+g‘𝑆)𝑣) → (𝑔 supp 0 ) = ((𝑢(+g‘𝑆)𝑣) supp 0 )) | 
| 127 | 126 | eleq1d 2826 | . . . . . . . 8
⊢ (𝑔 = (𝑢(+g‘𝑆)𝑣) → ((𝑔 supp 0 ) ∈ 𝐴 ↔ ((𝑢(+g‘𝑆)𝑣) supp 0 ) ∈ 𝐴)) | 
| 128 | 127 | elrab 3692 | . . . . . . 7
⊢ ((𝑢(+g‘𝑆)𝑣) ∈ {𝑔 ∈ 𝐵 ∣ (𝑔 supp 0 ) ∈ 𝐴} ↔ ((𝑢(+g‘𝑆)𝑣) ∈ 𝐵 ∧ ((𝑢(+g‘𝑆)𝑣) supp 0 ) ∈ 𝐴)) | 
| 129 | 125, 128 | bitrdi 287 | . . . . . 6
⊢ (((𝜑 ∧ 𝑢 ∈ 𝑈) ∧ 𝑣 ∈ 𝑈) → ((𝑢(+g‘𝑆)𝑣) ∈ 𝑈 ↔ ((𝑢(+g‘𝑆)𝑣) ∈ 𝐵 ∧ ((𝑢(+g‘𝑆)𝑣) supp 0 ) ∈ 𝐴))) | 
| 130 | 51, 123, 129 | mpbir2and 713 | . . . . 5
⊢ (((𝜑 ∧ 𝑢 ∈ 𝑈) ∧ 𝑣 ∈ 𝑈) → (𝑢(+g‘𝑆)𝑣) ∈ 𝑈) | 
| 131 | 130 | ralrimiva 3146 | . . . 4
⊢ ((𝜑 ∧ 𝑢 ∈ 𝑈) → ∀𝑣 ∈ 𝑈 (𝑢(+g‘𝑆)𝑣) ∈ 𝑈) | 
| 132 | 4, 5, 6 | psrgrp 21976 | . . . . . 6
⊢ (𝜑 → 𝑆 ∈ Grp) | 
| 133 |  | eqid 2737 | . . . . . . 7
⊢
(invg‘𝑆) = (invg‘𝑆) | 
| 134 | 9, 133 | grpinvcl 19005 | . . . . . 6
⊢ ((𝑆 ∈ Grp ∧ 𝑢 ∈ 𝐵) → ((invg‘𝑆)‘𝑢) ∈ 𝐵) | 
| 135 | 132, 41, 134 | syl2an2r 685 | . . . . 5
⊢ ((𝜑 ∧ 𝑢 ∈ 𝑈) → ((invg‘𝑆)‘𝑢) ∈ 𝐵) | 
| 136 |  | ovexd 7466 | . . . . . 6
⊢ ((𝜑 ∧ 𝑢 ∈ 𝑈) → (((invg‘𝑆)‘𝑢) supp 0 ) ∈
V) | 
| 137 |  | sseq2 4010 | . . . . . . . . 9
⊢ (𝑥 = (𝑢 supp 0 ) → (𝑦 ⊆ 𝑥 ↔ 𝑦 ⊆ (𝑢 supp 0 ))) | 
| 138 | 137 | imbi1d 341 | . . . . . . . 8
⊢ (𝑥 = (𝑢 supp 0 ) → ((𝑦 ⊆ 𝑥 → 𝑦 ∈ 𝐴) ↔ (𝑦 ⊆ (𝑢 supp 0 ) → 𝑦 ∈ 𝐴))) | 
| 139 | 138 | albidv 1920 | . . . . . . 7
⊢ (𝑥 = (𝑢 supp 0 ) → (∀𝑦(𝑦 ⊆ 𝑥 → 𝑦 ∈ 𝐴) ↔ ∀𝑦(𝑦 ⊆ (𝑢 supp 0 ) → 𝑦 ∈ 𝐴))) | 
| 140 | 59 | adantr 480 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑢 ∈ 𝑈) → ∀𝑥 ∈ 𝐴 ∀𝑦(𝑦 ⊆ 𝑥 → 𝑦 ∈ 𝐴)) | 
| 141 | 139, 140,
61 | rspcdva 3623 | . . . . . 6
⊢ ((𝜑 ∧ 𝑢 ∈ 𝑈) → ∀𝑦(𝑦 ⊆ (𝑢 supp 0 ) → 𝑦 ∈ 𝐴)) | 
| 142 | 5 | adantr 480 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑢 ∈ 𝑈) → 𝐼 ∈ 𝑊) | 
| 143 | 6 | adantr 480 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑢 ∈ 𝑈) → 𝑅 ∈ Grp) | 
| 144 |  | eqid 2737 | . . . . . . . . 9
⊢
(invg‘𝑅) = (invg‘𝑅) | 
| 145 | 4, 142, 143, 7, 144, 9, 133, 41 | psrneg 21979 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑢 ∈ 𝑈) → ((invg‘𝑆)‘𝑢) = ((invg‘𝑅) ∘ 𝑢)) | 
| 146 | 145 | oveq1d 7446 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑢 ∈ 𝑈) → (((invg‘𝑆)‘𝑢) supp 0 ) =
(((invg‘𝑅)
∘ 𝑢) supp 0
)) | 
| 147 | 11, 144 | grpinvfn 18999 | . . . . . . . . 9
⊢
(invg‘𝑅) Fn (Base‘𝑅) | 
| 148 | 147 | a1i 11 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑢 ∈ 𝑈) → (invg‘𝑅) Fn (Base‘𝑅)) | 
| 149 | 8, 144 | grpinvid 19017 | . . . . . . . . 9
⊢ (𝑅 ∈ Grp →
((invg‘𝑅)‘ 0 ) = 0 ) | 
| 150 | 143, 149 | syl 17 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑢 ∈ 𝑈) → ((invg‘𝑅)‘ 0 ) = 0 ) | 
| 151 | 148, 80, 98, 99, 150 | suppcoss 8232 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑢 ∈ 𝑈) → (((invg‘𝑅) ∘ 𝑢) supp 0 ) ⊆ (𝑢 supp 0 )) | 
| 152 | 146, 151 | eqsstrd 4018 | . . . . . 6
⊢ ((𝜑 ∧ 𝑢 ∈ 𝑈) → (((invg‘𝑆)‘𝑢) supp 0 ) ⊆ (𝑢 supp 0 )) | 
| 153 |  | sseq1 4009 | . . . . . . . 8
⊢ (𝑦 =
(((invg‘𝑆)‘𝑢) supp 0 ) → (𝑦 ⊆ (𝑢 supp 0 ) ↔
(((invg‘𝑆)‘𝑢) supp 0 ) ⊆ (𝑢 supp 0 ))) | 
| 154 |  | eleq1 2829 | . . . . . . . 8
⊢ (𝑦 =
(((invg‘𝑆)‘𝑢) supp 0 ) → (𝑦 ∈ 𝐴 ↔ (((invg‘𝑆)‘𝑢) supp 0 ) ∈ 𝐴)) | 
| 155 | 153, 154 | imbi12d 344 | . . . . . . 7
⊢ (𝑦 =
(((invg‘𝑆)‘𝑢) supp 0 ) → ((𝑦 ⊆ (𝑢 supp 0 ) → 𝑦 ∈ 𝐴) ↔ ((((invg‘𝑆)‘𝑢) supp 0 ) ⊆ (𝑢 supp 0 ) →
(((invg‘𝑆)‘𝑢) supp 0 ) ∈ 𝐴))) | 
| 156 | 155 | spcgv 3596 | . . . . . 6
⊢
((((invg‘𝑆)‘𝑢) supp 0 ) ∈ V →
(∀𝑦(𝑦 ⊆ (𝑢 supp 0 ) → 𝑦 ∈ 𝐴) → ((((invg‘𝑆)‘𝑢) supp 0 ) ⊆ (𝑢 supp 0 ) →
(((invg‘𝑆)‘𝑢) supp 0 ) ∈ 𝐴))) | 
| 157 | 136, 141,
152, 156 | syl3c 66 | . . . . 5
⊢ ((𝜑 ∧ 𝑢 ∈ 𝑈) → (((invg‘𝑆)‘𝑢) supp 0 ) ∈ 𝐴) | 
| 158 | 43 | eleq2d 2827 | . . . . . 6
⊢ ((𝜑 ∧ 𝑢 ∈ 𝑈) → (((invg‘𝑆)‘𝑢) ∈ 𝑈 ↔ ((invg‘𝑆)‘𝑢) ∈ {𝑔 ∈ 𝐵 ∣ (𝑔 supp 0 ) ∈ 𝐴})) | 
| 159 |  | oveq1 7438 | . . . . . . . 8
⊢ (𝑔 = ((invg‘𝑆)‘𝑢) → (𝑔 supp 0 ) =
(((invg‘𝑆)‘𝑢) supp 0 )) | 
| 160 | 159 | eleq1d 2826 | . . . . . . 7
⊢ (𝑔 = ((invg‘𝑆)‘𝑢) → ((𝑔 supp 0 ) ∈ 𝐴 ↔ (((invg‘𝑆)‘𝑢) supp 0 ) ∈ 𝐴)) | 
| 161 | 160 | elrab 3692 | . . . . . 6
⊢
(((invg‘𝑆)‘𝑢) ∈ {𝑔 ∈ 𝐵 ∣ (𝑔 supp 0 ) ∈ 𝐴} ↔ (((invg‘𝑆)‘𝑢) ∈ 𝐵 ∧ (((invg‘𝑆)‘𝑢) supp 0 ) ∈ 𝐴)) | 
| 162 | 158, 161 | bitrdi 287 | . . . . 5
⊢ ((𝜑 ∧ 𝑢 ∈ 𝑈) → (((invg‘𝑆)‘𝑢) ∈ 𝑈 ↔ (((invg‘𝑆)‘𝑢) ∈ 𝐵 ∧ (((invg‘𝑆)‘𝑢) supp 0 ) ∈ 𝐴))) | 
| 163 | 135, 157,
162 | mpbir2and 713 | . . . 4
⊢ ((𝜑 ∧ 𝑢 ∈ 𝑈) → ((invg‘𝑆)‘𝑢) ∈ 𝑈) | 
| 164 | 131, 163 | jca 511 | . . 3
⊢ ((𝜑 ∧ 𝑢 ∈ 𝑈) → (∀𝑣 ∈ 𝑈 (𝑢(+g‘𝑆)𝑣) ∈ 𝑈 ∧ ((invg‘𝑆)‘𝑢) ∈ 𝑈)) | 
| 165 | 164 | ralrimiva 3146 | . 2
⊢ (𝜑 → ∀𝑢 ∈ 𝑈 (∀𝑣 ∈ 𝑈 (𝑢(+g‘𝑆)𝑣) ∈ 𝑈 ∧ ((invg‘𝑆)‘𝑢) ∈ 𝑈)) | 
| 166 | 9, 32, 133 | issubg2 19159 | . . 3
⊢ (𝑆 ∈ Grp → (𝑈 ∈ (SubGrp‘𝑆) ↔ (𝑈 ⊆ 𝐵 ∧ 𝑈 ≠ ∅ ∧ ∀𝑢 ∈ 𝑈 (∀𝑣 ∈ 𝑈 (𝑢(+g‘𝑆)𝑣) ∈ 𝑈 ∧ ((invg‘𝑆)‘𝑢) ∈ 𝑈)))) | 
| 167 | 132, 166 | syl 17 | . 2
⊢ (𝜑 → (𝑈 ∈ (SubGrp‘𝑆) ↔ (𝑈 ⊆ 𝐵 ∧ 𝑈 ≠ ∅ ∧ ∀𝑢 ∈ 𝑈 (∀𝑣 ∈ 𝑈 (𝑢(+g‘𝑆)𝑣) ∈ 𝑈 ∧ ((invg‘𝑆)‘𝑢) ∈ 𝑈)))) | 
| 168 | 3, 31, 165, 167 | mpbir3and 1343 | 1
⊢ (𝜑 → 𝑈 ∈ (SubGrp‘𝑆)) |