| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | eqidd 2738 | . 2
⊢ (𝜑 → (𝐺 ↾s {𝑎 ∈ 𝐵 ∣ ({𝑎} ⊕ 𝑁) ∈ 𝐹}) = (𝐺 ↾s {𝑎 ∈ 𝐵 ∣ ({𝑎} ⊕ 𝑁) ∈ 𝐹})) | 
| 2 |  | eqidd 2738 | . 2
⊢ (𝜑 → (0g‘𝐺) = (0g‘𝐺)) | 
| 3 |  | eqidd 2738 | . 2
⊢ (𝜑 → (+g‘𝐺) = (+g‘𝐺)) | 
| 4 |  | ssrab2 4080 | . . . 4
⊢ {𝑎 ∈ 𝐵 ∣ ({𝑎} ⊕ 𝑁) ∈ 𝐹} ⊆ 𝐵 | 
| 5 | 4 | a1i 11 | . . 3
⊢ (𝜑 → {𝑎 ∈ 𝐵 ∣ ({𝑎} ⊕ 𝑁) ∈ 𝐹} ⊆ 𝐵) | 
| 6 |  | nsgmgclem.b | . . 3
⊢ 𝐵 = (Base‘𝐺) | 
| 7 | 5, 6 | sseqtrdi 4024 | . 2
⊢ (𝜑 → {𝑎 ∈ 𝐵 ∣ ({𝑎} ⊕ 𝑁) ∈ 𝐹} ⊆ (Base‘𝐺)) | 
| 8 |  | sneq 4636 | . . . . 5
⊢ (𝑎 = (0g‘𝐺) → {𝑎} = {(0g‘𝐺)}) | 
| 9 | 8 | oveq1d 7446 | . . . 4
⊢ (𝑎 = (0g‘𝐺) → ({𝑎} ⊕ 𝑁) = ({(0g‘𝐺)} ⊕ 𝑁)) | 
| 10 | 9 | eleq1d 2826 | . . 3
⊢ (𝑎 = (0g‘𝐺) → (({𝑎} ⊕ 𝑁) ∈ 𝐹 ↔ ({(0g‘𝐺)} ⊕ 𝑁) ∈ 𝐹)) | 
| 11 |  | nsgmgclem.n | . . . . . 6
⊢ (𝜑 → 𝑁 ∈ (NrmSGrp‘𝐺)) | 
| 12 |  | nsgsubg 19176 | . . . . . 6
⊢ (𝑁 ∈ (NrmSGrp‘𝐺) → 𝑁 ∈ (SubGrp‘𝐺)) | 
| 13 | 11, 12 | syl 17 | . . . . 5
⊢ (𝜑 → 𝑁 ∈ (SubGrp‘𝐺)) | 
| 14 |  | subgrcl 19149 | . . . . 5
⊢ (𝑁 ∈ (SubGrp‘𝐺) → 𝐺 ∈ Grp) | 
| 15 | 13, 14 | syl 17 | . . . 4
⊢ (𝜑 → 𝐺 ∈ Grp) | 
| 16 |  | eqid 2737 | . . . . 5
⊢
(0g‘𝐺) = (0g‘𝐺) | 
| 17 | 6, 16 | grpidcl 18983 | . . . 4
⊢ (𝐺 ∈ Grp →
(0g‘𝐺)
∈ 𝐵) | 
| 18 | 15, 17 | syl 17 | . . 3
⊢ (𝜑 → (0g‘𝐺) ∈ 𝐵) | 
| 19 |  | nsgmgclem.p | . . . . . 6
⊢  ⊕ =
(LSSum‘𝐺) | 
| 20 | 16, 19 | lsm02 19690 | . . . . 5
⊢ (𝑁 ∈ (SubGrp‘𝐺) →
({(0g‘𝐺)}
⊕
𝑁) = 𝑁) | 
| 21 | 13, 20 | syl 17 | . . . 4
⊢ (𝜑 →
({(0g‘𝐺)}
⊕
𝑁) = 𝑁) | 
| 22 |  | nsgmgclem.f | . . . . 5
⊢ (𝜑 → 𝐹 ∈ (SubGrp‘𝑄)) | 
| 23 |  | nsgmgclem.q | . . . . . 6
⊢ 𝑄 = (𝐺 /s (𝐺 ~QG 𝑁)) | 
| 24 | 23 | nsgqus0 33438 | . . . . 5
⊢ ((𝑁 ∈ (NrmSGrp‘𝐺) ∧ 𝐹 ∈ (SubGrp‘𝑄)) → 𝑁 ∈ 𝐹) | 
| 25 | 11, 22, 24 | syl2anc 584 | . . . 4
⊢ (𝜑 → 𝑁 ∈ 𝐹) | 
| 26 | 21, 25 | eqeltrd 2841 | . . 3
⊢ (𝜑 →
({(0g‘𝐺)}
⊕
𝑁) ∈ 𝐹) | 
| 27 | 10, 18, 26 | elrabd 3694 | . 2
⊢ (𝜑 → (0g‘𝐺) ∈ {𝑎 ∈ 𝐵 ∣ ({𝑎} ⊕ 𝑁) ∈ 𝐹}) | 
| 28 |  | sneq 4636 | . . . . . 6
⊢ (𝑎 = (𝑥(+g‘𝐺)𝑦) → {𝑎} = {(𝑥(+g‘𝐺)𝑦)}) | 
| 29 | 28 | oveq1d 7446 | . . . . 5
⊢ (𝑎 = (𝑥(+g‘𝐺)𝑦) → ({𝑎} ⊕ 𝑁) = ({(𝑥(+g‘𝐺)𝑦)} ⊕ 𝑁)) | 
| 30 | 29 | eleq1d 2826 | . . . 4
⊢ (𝑎 = (𝑥(+g‘𝐺)𝑦) → (({𝑎} ⊕ 𝑁) ∈ 𝐹 ↔ ({(𝑥(+g‘𝐺)𝑦)} ⊕ 𝑁) ∈ 𝐹)) | 
| 31 | 15 | ad2antrr 726 | . . . . 5
⊢ (((𝜑 ∧ 𝑥 ∈ {𝑎 ∈ 𝐵 ∣ ({𝑎} ⊕ 𝑁) ∈ 𝐹}) ∧ 𝑦 ∈ {𝑎 ∈ 𝐵 ∣ ({𝑎} ⊕ 𝑁) ∈ 𝐹}) → 𝐺 ∈ Grp) | 
| 32 |  | elrabi 3687 | . . . . . 6
⊢ (𝑥 ∈ {𝑎 ∈ 𝐵 ∣ ({𝑎} ⊕ 𝑁) ∈ 𝐹} → 𝑥 ∈ 𝐵) | 
| 33 | 32 | ad2antlr 727 | . . . . 5
⊢ (((𝜑 ∧ 𝑥 ∈ {𝑎 ∈ 𝐵 ∣ ({𝑎} ⊕ 𝑁) ∈ 𝐹}) ∧ 𝑦 ∈ {𝑎 ∈ 𝐵 ∣ ({𝑎} ⊕ 𝑁) ∈ 𝐹}) → 𝑥 ∈ 𝐵) | 
| 34 |  | elrabi 3687 | . . . . . 6
⊢ (𝑦 ∈ {𝑎 ∈ 𝐵 ∣ ({𝑎} ⊕ 𝑁) ∈ 𝐹} → 𝑦 ∈ 𝐵) | 
| 35 | 34 | adantl 481 | . . . . 5
⊢ (((𝜑 ∧ 𝑥 ∈ {𝑎 ∈ 𝐵 ∣ ({𝑎} ⊕ 𝑁) ∈ 𝐹}) ∧ 𝑦 ∈ {𝑎 ∈ 𝐵 ∣ ({𝑎} ⊕ 𝑁) ∈ 𝐹}) → 𝑦 ∈ 𝐵) | 
| 36 |  | eqid 2737 | . . . . . 6
⊢
(+g‘𝐺) = (+g‘𝐺) | 
| 37 | 6, 36 | grpcl 18959 | . . . . 5
⊢ ((𝐺 ∈ Grp ∧ 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) → (𝑥(+g‘𝐺)𝑦) ∈ 𝐵) | 
| 38 | 31, 33, 35, 37 | syl3anc 1373 | . . . 4
⊢ (((𝜑 ∧ 𝑥 ∈ {𝑎 ∈ 𝐵 ∣ ({𝑎} ⊕ 𝑁) ∈ 𝐹}) ∧ 𝑦 ∈ {𝑎 ∈ 𝐵 ∣ ({𝑎} ⊕ 𝑁) ∈ 𝐹}) → (𝑥(+g‘𝐺)𝑦) ∈ 𝐵) | 
| 39 | 13 | ad2antrr 726 | . . . . . 6
⊢ (((𝜑 ∧ 𝑥 ∈ {𝑎 ∈ 𝐵 ∣ ({𝑎} ⊕ 𝑁) ∈ 𝐹}) ∧ 𝑦 ∈ {𝑎 ∈ 𝐵 ∣ ({𝑎} ⊕ 𝑁) ∈ 𝐹}) → 𝑁 ∈ (SubGrp‘𝐺)) | 
| 40 | 6, 19, 39, 38 | quslsm 33433 | . . . . 5
⊢ (((𝜑 ∧ 𝑥 ∈ {𝑎 ∈ 𝐵 ∣ ({𝑎} ⊕ 𝑁) ∈ 𝐹}) ∧ 𝑦 ∈ {𝑎 ∈ 𝐵 ∣ ({𝑎} ⊕ 𝑁) ∈ 𝐹}) → [(𝑥(+g‘𝐺)𝑦)](𝐺 ~QG 𝑁) = ({(𝑥(+g‘𝐺)𝑦)} ⊕ 𝑁)) | 
| 41 | 11 | ad2antrr 726 | . . . . . . 7
⊢ (((𝜑 ∧ 𝑥 ∈ {𝑎 ∈ 𝐵 ∣ ({𝑎} ⊕ 𝑁) ∈ 𝐹}) ∧ 𝑦 ∈ {𝑎 ∈ 𝐵 ∣ ({𝑎} ⊕ 𝑁) ∈ 𝐹}) → 𝑁 ∈ (NrmSGrp‘𝐺)) | 
| 42 |  | eqid 2737 | . . . . . . . 8
⊢
(+g‘𝑄) = (+g‘𝑄) | 
| 43 | 23, 6, 36, 42 | qusadd 19206 | . . . . . . 7
⊢ ((𝑁 ∈ (NrmSGrp‘𝐺) ∧ 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) → ([𝑥](𝐺 ~QG 𝑁)(+g‘𝑄)[𝑦](𝐺 ~QG 𝑁)) = [(𝑥(+g‘𝐺)𝑦)](𝐺 ~QG 𝑁)) | 
| 44 | 41, 33, 35, 43 | syl3anc 1373 | . . . . . 6
⊢ (((𝜑 ∧ 𝑥 ∈ {𝑎 ∈ 𝐵 ∣ ({𝑎} ⊕ 𝑁) ∈ 𝐹}) ∧ 𝑦 ∈ {𝑎 ∈ 𝐵 ∣ ({𝑎} ⊕ 𝑁) ∈ 𝐹}) → ([𝑥](𝐺 ~QG 𝑁)(+g‘𝑄)[𝑦](𝐺 ~QG 𝑁)) = [(𝑥(+g‘𝐺)𝑦)](𝐺 ~QG 𝑁)) | 
| 45 | 22 | ad2antrr 726 | . . . . . . 7
⊢ (((𝜑 ∧ 𝑥 ∈ {𝑎 ∈ 𝐵 ∣ ({𝑎} ⊕ 𝑁) ∈ 𝐹}) ∧ 𝑦 ∈ {𝑎 ∈ 𝐵 ∣ ({𝑎} ⊕ 𝑁) ∈ 𝐹}) → 𝐹 ∈ (SubGrp‘𝑄)) | 
| 46 | 6, 19, 39, 33 | quslsm 33433 | . . . . . . . 8
⊢ (((𝜑 ∧ 𝑥 ∈ {𝑎 ∈ 𝐵 ∣ ({𝑎} ⊕ 𝑁) ∈ 𝐹}) ∧ 𝑦 ∈ {𝑎 ∈ 𝐵 ∣ ({𝑎} ⊕ 𝑁) ∈ 𝐹}) → [𝑥](𝐺 ~QG 𝑁) = ({𝑥} ⊕ 𝑁)) | 
| 47 |  | sneq 4636 | . . . . . . . . . . . . 13
⊢ (𝑎 = 𝑥 → {𝑎} = {𝑥}) | 
| 48 | 47 | oveq1d 7446 | . . . . . . . . . . . 12
⊢ (𝑎 = 𝑥 → ({𝑎} ⊕ 𝑁) = ({𝑥} ⊕ 𝑁)) | 
| 49 | 48 | eleq1d 2826 | . . . . . . . . . . 11
⊢ (𝑎 = 𝑥 → (({𝑎} ⊕ 𝑁) ∈ 𝐹 ↔ ({𝑥} ⊕ 𝑁) ∈ 𝐹)) | 
| 50 | 49 | elrab 3692 | . . . . . . . . . 10
⊢ (𝑥 ∈ {𝑎 ∈ 𝐵 ∣ ({𝑎} ⊕ 𝑁) ∈ 𝐹} ↔ (𝑥 ∈ 𝐵 ∧ ({𝑥} ⊕ 𝑁) ∈ 𝐹)) | 
| 51 | 50 | simprbi 496 | . . . . . . . . 9
⊢ (𝑥 ∈ {𝑎 ∈ 𝐵 ∣ ({𝑎} ⊕ 𝑁) ∈ 𝐹} → ({𝑥} ⊕ 𝑁) ∈ 𝐹) | 
| 52 | 51 | ad2antlr 727 | . . . . . . . 8
⊢ (((𝜑 ∧ 𝑥 ∈ {𝑎 ∈ 𝐵 ∣ ({𝑎} ⊕ 𝑁) ∈ 𝐹}) ∧ 𝑦 ∈ {𝑎 ∈ 𝐵 ∣ ({𝑎} ⊕ 𝑁) ∈ 𝐹}) → ({𝑥} ⊕ 𝑁) ∈ 𝐹) | 
| 53 | 46, 52 | eqeltrd 2841 | . . . . . . 7
⊢ (((𝜑 ∧ 𝑥 ∈ {𝑎 ∈ 𝐵 ∣ ({𝑎} ⊕ 𝑁) ∈ 𝐹}) ∧ 𝑦 ∈ {𝑎 ∈ 𝐵 ∣ ({𝑎} ⊕ 𝑁) ∈ 𝐹}) → [𝑥](𝐺 ~QG 𝑁) ∈ 𝐹) | 
| 54 | 6, 19, 39, 35 | quslsm 33433 | . . . . . . . 8
⊢ (((𝜑 ∧ 𝑥 ∈ {𝑎 ∈ 𝐵 ∣ ({𝑎} ⊕ 𝑁) ∈ 𝐹}) ∧ 𝑦 ∈ {𝑎 ∈ 𝐵 ∣ ({𝑎} ⊕ 𝑁) ∈ 𝐹}) → [𝑦](𝐺 ~QG 𝑁) = ({𝑦} ⊕ 𝑁)) | 
| 55 |  | sneq 4636 | . . . . . . . . . . . . 13
⊢ (𝑎 = 𝑦 → {𝑎} = {𝑦}) | 
| 56 | 55 | oveq1d 7446 | . . . . . . . . . . . 12
⊢ (𝑎 = 𝑦 → ({𝑎} ⊕ 𝑁) = ({𝑦} ⊕ 𝑁)) | 
| 57 | 56 | eleq1d 2826 | . . . . . . . . . . 11
⊢ (𝑎 = 𝑦 → (({𝑎} ⊕ 𝑁) ∈ 𝐹 ↔ ({𝑦} ⊕ 𝑁) ∈ 𝐹)) | 
| 58 | 57 | elrab 3692 | . . . . . . . . . 10
⊢ (𝑦 ∈ {𝑎 ∈ 𝐵 ∣ ({𝑎} ⊕ 𝑁) ∈ 𝐹} ↔ (𝑦 ∈ 𝐵 ∧ ({𝑦} ⊕ 𝑁) ∈ 𝐹)) | 
| 59 | 58 | simprbi 496 | . . . . . . . . 9
⊢ (𝑦 ∈ {𝑎 ∈ 𝐵 ∣ ({𝑎} ⊕ 𝑁) ∈ 𝐹} → ({𝑦} ⊕ 𝑁) ∈ 𝐹) | 
| 60 | 59 | adantl 481 | . . . . . . . 8
⊢ (((𝜑 ∧ 𝑥 ∈ {𝑎 ∈ 𝐵 ∣ ({𝑎} ⊕ 𝑁) ∈ 𝐹}) ∧ 𝑦 ∈ {𝑎 ∈ 𝐵 ∣ ({𝑎} ⊕ 𝑁) ∈ 𝐹}) → ({𝑦} ⊕ 𝑁) ∈ 𝐹) | 
| 61 | 54, 60 | eqeltrd 2841 | . . . . . . 7
⊢ (((𝜑 ∧ 𝑥 ∈ {𝑎 ∈ 𝐵 ∣ ({𝑎} ⊕ 𝑁) ∈ 𝐹}) ∧ 𝑦 ∈ {𝑎 ∈ 𝐵 ∣ ({𝑎} ⊕ 𝑁) ∈ 𝐹}) → [𝑦](𝐺 ~QG 𝑁) ∈ 𝐹) | 
| 62 | 42 | subgcl 19154 | . . . . . . 7
⊢ ((𝐹 ∈ (SubGrp‘𝑄) ∧ [𝑥](𝐺 ~QG 𝑁) ∈ 𝐹 ∧ [𝑦](𝐺 ~QG 𝑁) ∈ 𝐹) → ([𝑥](𝐺 ~QG 𝑁)(+g‘𝑄)[𝑦](𝐺 ~QG 𝑁)) ∈ 𝐹) | 
| 63 | 45, 53, 61, 62 | syl3anc 1373 | . . . . . 6
⊢ (((𝜑 ∧ 𝑥 ∈ {𝑎 ∈ 𝐵 ∣ ({𝑎} ⊕ 𝑁) ∈ 𝐹}) ∧ 𝑦 ∈ {𝑎 ∈ 𝐵 ∣ ({𝑎} ⊕ 𝑁) ∈ 𝐹}) → ([𝑥](𝐺 ~QG 𝑁)(+g‘𝑄)[𝑦](𝐺 ~QG 𝑁)) ∈ 𝐹) | 
| 64 | 44, 63 | eqeltrrd 2842 | . . . . 5
⊢ (((𝜑 ∧ 𝑥 ∈ {𝑎 ∈ 𝐵 ∣ ({𝑎} ⊕ 𝑁) ∈ 𝐹}) ∧ 𝑦 ∈ {𝑎 ∈ 𝐵 ∣ ({𝑎} ⊕ 𝑁) ∈ 𝐹}) → [(𝑥(+g‘𝐺)𝑦)](𝐺 ~QG 𝑁) ∈ 𝐹) | 
| 65 | 40, 64 | eqeltrrd 2842 | . . . 4
⊢ (((𝜑 ∧ 𝑥 ∈ {𝑎 ∈ 𝐵 ∣ ({𝑎} ⊕ 𝑁) ∈ 𝐹}) ∧ 𝑦 ∈ {𝑎 ∈ 𝐵 ∣ ({𝑎} ⊕ 𝑁) ∈ 𝐹}) → ({(𝑥(+g‘𝐺)𝑦)} ⊕ 𝑁) ∈ 𝐹) | 
| 66 | 30, 38, 65 | elrabd 3694 | . . 3
⊢ (((𝜑 ∧ 𝑥 ∈ {𝑎 ∈ 𝐵 ∣ ({𝑎} ⊕ 𝑁) ∈ 𝐹}) ∧ 𝑦 ∈ {𝑎 ∈ 𝐵 ∣ ({𝑎} ⊕ 𝑁) ∈ 𝐹}) → (𝑥(+g‘𝐺)𝑦) ∈ {𝑎 ∈ 𝐵 ∣ ({𝑎} ⊕ 𝑁) ∈ 𝐹}) | 
| 67 | 66 | 3impa 1110 | . 2
⊢ ((𝜑 ∧ 𝑥 ∈ {𝑎 ∈ 𝐵 ∣ ({𝑎} ⊕ 𝑁) ∈ 𝐹} ∧ 𝑦 ∈ {𝑎 ∈ 𝐵 ∣ ({𝑎} ⊕ 𝑁) ∈ 𝐹}) → (𝑥(+g‘𝐺)𝑦) ∈ {𝑎 ∈ 𝐵 ∣ ({𝑎} ⊕ 𝑁) ∈ 𝐹}) | 
| 68 |  | sneq 4636 | . . . . . . 7
⊢ (𝑎 = ((invg‘𝐺)‘𝑥) → {𝑎} = {((invg‘𝐺)‘𝑥)}) | 
| 69 | 68 | oveq1d 7446 | . . . . . 6
⊢ (𝑎 = ((invg‘𝐺)‘𝑥) → ({𝑎} ⊕ 𝑁) = ({((invg‘𝐺)‘𝑥)} ⊕ 𝑁)) | 
| 70 | 69 | eleq1d 2826 | . . . . 5
⊢ (𝑎 = ((invg‘𝐺)‘𝑥) → (({𝑎} ⊕ 𝑁) ∈ 𝐹 ↔ ({((invg‘𝐺)‘𝑥)} ⊕ 𝑁) ∈ 𝐹)) | 
| 71 |  | eqid 2737 | . . . . . . . 8
⊢
(invg‘𝐺) = (invg‘𝐺) | 
| 72 | 6, 71 | grpinvcl 19005 | . . . . . . 7
⊢ ((𝐺 ∈ Grp ∧ 𝑥 ∈ 𝐵) → ((invg‘𝐺)‘𝑥) ∈ 𝐵) | 
| 73 | 15, 72 | sylan 580 | . . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → ((invg‘𝐺)‘𝑥) ∈ 𝐵) | 
| 74 | 73 | adantr 480 | . . . . 5
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐵) ∧ ({𝑥} ⊕ 𝑁) ∈ 𝐹) → ((invg‘𝐺)‘𝑥) ∈ 𝐵) | 
| 75 |  | eqid 2737 | . . . . . . . . . 10
⊢
(invg‘𝑄) = (invg‘𝑄) | 
| 76 | 23, 6, 71, 75 | qusinv 19208 | . . . . . . . . 9
⊢ ((𝑁 ∈ (NrmSGrp‘𝐺) ∧ 𝑥 ∈ 𝐵) → ((invg‘𝑄)‘[𝑥](𝐺 ~QG 𝑁)) = [((invg‘𝐺)‘𝑥)](𝐺 ~QG 𝑁)) | 
| 77 | 11, 76 | sylan 580 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → ((invg‘𝑄)‘[𝑥](𝐺 ~QG 𝑁)) = [((invg‘𝐺)‘𝑥)](𝐺 ~QG 𝑁)) | 
| 78 | 13 | adantr 480 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → 𝑁 ∈ (SubGrp‘𝐺)) | 
| 79 |  | simpr 484 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → 𝑥 ∈ 𝐵) | 
| 80 | 6, 19, 78, 79 | quslsm 33433 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → [𝑥](𝐺 ~QG 𝑁) = ({𝑥} ⊕ 𝑁)) | 
| 81 | 80 | fveq2d 6910 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → ((invg‘𝑄)‘[𝑥](𝐺 ~QG 𝑁)) = ((invg‘𝑄)‘({𝑥} ⊕ 𝑁))) | 
| 82 | 6, 19, 78, 73 | quslsm 33433 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → [((invg‘𝐺)‘𝑥)](𝐺 ~QG 𝑁) = ({((invg‘𝐺)‘𝑥)} ⊕ 𝑁)) | 
| 83 | 77, 81, 82 | 3eqtr3d 2785 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → ((invg‘𝑄)‘({𝑥} ⊕ 𝑁)) = ({((invg‘𝐺)‘𝑥)} ⊕ 𝑁)) | 
| 84 | 83 | adantr 480 | . . . . . 6
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐵) ∧ ({𝑥} ⊕ 𝑁) ∈ 𝐹) → ((invg‘𝑄)‘({𝑥} ⊕ 𝑁)) = ({((invg‘𝐺)‘𝑥)} ⊕ 𝑁)) | 
| 85 | 22 | ad2antrr 726 | . . . . . . 7
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐵) ∧ ({𝑥} ⊕ 𝑁) ∈ 𝐹) → 𝐹 ∈ (SubGrp‘𝑄)) | 
| 86 |  | simpr 484 | . . . . . . 7
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐵) ∧ ({𝑥} ⊕ 𝑁) ∈ 𝐹) → ({𝑥} ⊕ 𝑁) ∈ 𝐹) | 
| 87 | 75 | subginvcl 19153 | . . . . . . 7
⊢ ((𝐹 ∈ (SubGrp‘𝑄) ∧ ({𝑥} ⊕ 𝑁) ∈ 𝐹) → ((invg‘𝑄)‘({𝑥} ⊕ 𝑁)) ∈ 𝐹) | 
| 88 | 85, 86, 87 | syl2anc 584 | . . . . . 6
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐵) ∧ ({𝑥} ⊕ 𝑁) ∈ 𝐹) → ((invg‘𝑄)‘({𝑥} ⊕ 𝑁)) ∈ 𝐹) | 
| 89 | 84, 88 | eqeltrrd 2842 | . . . . 5
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐵) ∧ ({𝑥} ⊕ 𝑁) ∈ 𝐹) → ({((invg‘𝐺)‘𝑥)} ⊕ 𝑁) ∈ 𝐹) | 
| 90 | 70, 74, 89 | elrabd 3694 | . . . 4
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐵) ∧ ({𝑥} ⊕ 𝑁) ∈ 𝐹) → ((invg‘𝐺)‘𝑥) ∈ {𝑎 ∈ 𝐵 ∣ ({𝑎} ⊕ 𝑁) ∈ 𝐹}) | 
| 91 | 90 | anasss 466 | . . 3
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ ({𝑥} ⊕ 𝑁) ∈ 𝐹)) → ((invg‘𝐺)‘𝑥) ∈ {𝑎 ∈ 𝐵 ∣ ({𝑎} ⊕ 𝑁) ∈ 𝐹}) | 
| 92 | 50, 91 | sylan2b 594 | . 2
⊢ ((𝜑 ∧ 𝑥 ∈ {𝑎 ∈ 𝐵 ∣ ({𝑎} ⊕ 𝑁) ∈ 𝐹}) → ((invg‘𝐺)‘𝑥) ∈ {𝑎 ∈ 𝐵 ∣ ({𝑎} ⊕ 𝑁) ∈ 𝐹}) | 
| 93 | 1, 2, 3, 7, 27, 67, 92, 15 | issubgrpd2 19160 | 1
⊢ (𝜑 → {𝑎 ∈ 𝐵 ∣ ({𝑎} ⊕ 𝑁) ∈ 𝐹} ∈ (SubGrp‘𝐺)) |