Proof of Theorem nsgqusf1olem3
| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | nsgqusf1o.f | . . . . 5
⊢ 𝐹 = (𝑓 ∈ 𝑇 ↦ {𝑎 ∈ 𝐵 ∣ ({𝑎} ⊕ 𝑁) ∈ 𝑓}) | 
| 2 | 1 | elrnmpt 5968 | . . . 4
⊢ (ℎ ∈ V → (ℎ ∈ ran 𝐹 ↔ ∃𝑓 ∈ 𝑇 ℎ = {𝑎 ∈ 𝐵 ∣ ({𝑎} ⊕ 𝑁) ∈ 𝑓})) | 
| 3 | 2 | elv 3484 | . . 3
⊢ (ℎ ∈ ran 𝐹 ↔ ∃𝑓 ∈ 𝑇 ℎ = {𝑎 ∈ 𝐵 ∣ ({𝑎} ⊕ 𝑁) ∈ 𝑓}) | 
| 4 |  | nsgqusf1o.s | . . . . 5
⊢ 𝑆 = {ℎ ∈ (SubGrp‘𝐺) ∣ 𝑁 ⊆ ℎ} | 
| 5 | 4 | reqabi 3459 | . . . 4
⊢ (ℎ ∈ 𝑆 ↔ (ℎ ∈ (SubGrp‘𝐺) ∧ 𝑁 ⊆ ℎ)) | 
| 6 |  | nsgqusf1o.b | . . . . . . . 8
⊢ 𝐵 = (Base‘𝐺) | 
| 7 |  | nsgqusf1o.t | . . . . . . . 8
⊢ 𝑇 = (SubGrp‘𝑄) | 
| 8 |  | nsgqusf1o.1 | . . . . . . . 8
⊢  ≤ =
(le‘(toInc‘𝑆)) | 
| 9 |  | nsgqusf1o.2 | . . . . . . . 8
⊢  ≲ =
(le‘(toInc‘𝑇)) | 
| 10 |  | nsgqusf1o.q | . . . . . . . 8
⊢ 𝑄 = (𝐺 /s (𝐺 ~QG 𝑁)) | 
| 11 |  | nsgqusf1o.p | . . . . . . . 8
⊢  ⊕ =
(LSSum‘𝐺) | 
| 12 |  | nsgqusf1o.e | . . . . . . . 8
⊢ 𝐸 = (ℎ ∈ 𝑆 ↦ ran (𝑥 ∈ ℎ ↦ ({𝑥} ⊕ 𝑁))) | 
| 13 |  | nsgqusf1o.n | . . . . . . . 8
⊢ (𝜑 → 𝑁 ∈ (NrmSGrp‘𝐺)) | 
| 14 | 6, 4, 7, 8, 9, 10,
11, 12, 1, 13 | nsgqusf1olem1 33442 | . . . . . . 7
⊢ (((𝜑 ∧ ℎ ∈ (SubGrp‘𝐺)) ∧ 𝑁 ⊆ ℎ) → ran (𝑥 ∈ ℎ ↦ ({𝑥} ⊕ 𝑁)) ∈ 𝑇) | 
| 15 |  | eleq2 2829 | . . . . . . . . . 10
⊢ (𝑓 = ran (𝑥 ∈ ℎ ↦ ({𝑥} ⊕ 𝑁)) → (({𝑎} ⊕ 𝑁) ∈ 𝑓 ↔ ({𝑎} ⊕ 𝑁) ∈ ran (𝑥 ∈ ℎ ↦ ({𝑥} ⊕ 𝑁)))) | 
| 16 | 15 | rabbidv 3443 | . . . . . . . . 9
⊢ (𝑓 = ran (𝑥 ∈ ℎ ↦ ({𝑥} ⊕ 𝑁)) → {𝑎 ∈ 𝐵 ∣ ({𝑎} ⊕ 𝑁) ∈ 𝑓} = {𝑎 ∈ 𝐵 ∣ ({𝑎} ⊕ 𝑁) ∈ ran (𝑥 ∈ ℎ ↦ ({𝑥} ⊕ 𝑁))}) | 
| 17 | 16 | eqeq2d 2747 | . . . . . . . 8
⊢ (𝑓 = ran (𝑥 ∈ ℎ ↦ ({𝑥} ⊕ 𝑁)) → (ℎ = {𝑎 ∈ 𝐵 ∣ ({𝑎} ⊕ 𝑁) ∈ 𝑓} ↔ ℎ = {𝑎 ∈ 𝐵 ∣ ({𝑎} ⊕ 𝑁) ∈ ran (𝑥 ∈ ℎ ↦ ({𝑥} ⊕ 𝑁))})) | 
| 18 | 17 | adantl 481 | . . . . . . 7
⊢ ((((𝜑 ∧ ℎ ∈ (SubGrp‘𝐺)) ∧ 𝑁 ⊆ ℎ) ∧ 𝑓 = ran (𝑥 ∈ ℎ ↦ ({𝑥} ⊕ 𝑁))) → (ℎ = {𝑎 ∈ 𝐵 ∣ ({𝑎} ⊕ 𝑁) ∈ 𝑓} ↔ ℎ = {𝑎 ∈ 𝐵 ∣ ({𝑎} ⊕ 𝑁) ∈ ran (𝑥 ∈ ℎ ↦ ({𝑥} ⊕ 𝑁))})) | 
| 19 |  | nfv 1913 | . . . . . . . . . . . 12
⊢
Ⅎ𝑥(((𝜑 ∧ ℎ ∈ (SubGrp‘𝐺)) ∧ 𝑁 ⊆ ℎ) ∧ 𝑎 ∈ 𝐵) | 
| 20 |  | nfmpt1 5249 | . . . . . . . . . . . . . 14
⊢
Ⅎ𝑥(𝑥 ∈ ℎ ↦ ({𝑥} ⊕ 𝑁)) | 
| 21 | 20 | nfrn 5962 | . . . . . . . . . . . . 13
⊢
Ⅎ𝑥ran
(𝑥 ∈ ℎ ↦ ({𝑥} ⊕ 𝑁)) | 
| 22 | 21 | nfel2 2923 | . . . . . . . . . . . 12
⊢
Ⅎ𝑥({𝑎} ⊕ 𝑁) ∈ ran (𝑥 ∈ ℎ ↦ ({𝑥} ⊕ 𝑁)) | 
| 23 | 19, 22 | nfan 1898 | . . . . . . . . . . 11
⊢
Ⅎ𝑥((((𝜑 ∧ ℎ ∈ (SubGrp‘𝐺)) ∧ 𝑁 ⊆ ℎ) ∧ 𝑎 ∈ 𝐵) ∧ ({𝑎} ⊕ 𝑁) ∈ ran (𝑥 ∈ ℎ ↦ ({𝑥} ⊕ 𝑁))) | 
| 24 |  | nsgsubg 19177 | . . . . . . . . . . . . . . . . . 18
⊢ (𝑁 ∈ (NrmSGrp‘𝐺) → 𝑁 ∈ (SubGrp‘𝐺)) | 
| 25 | 13, 24 | syl 17 | . . . . . . . . . . . . . . . . 17
⊢ (𝜑 → 𝑁 ∈ (SubGrp‘𝐺)) | 
| 26 |  | subgrcl 19150 | . . . . . . . . . . . . . . . . 17
⊢ (𝑁 ∈ (SubGrp‘𝐺) → 𝐺 ∈ Grp) | 
| 27 | 25, 26 | syl 17 | . . . . . . . . . . . . . . . 16
⊢ (𝜑 → 𝐺 ∈ Grp) | 
| 28 | 27 | ad4antr 732 | . . . . . . . . . . . . . . 15
⊢
(((((𝜑 ∧ ℎ ∈ (SubGrp‘𝐺)) ∧ 𝑁 ⊆ ℎ) ∧ 𝑎 ∈ 𝐵) ∧ 𝑥 ∈ ℎ) → 𝐺 ∈ Grp) | 
| 29 | 28 | adantr 480 | . . . . . . . . . . . . . 14
⊢
((((((𝜑 ∧ ℎ ∈ (SubGrp‘𝐺)) ∧ 𝑁 ⊆ ℎ) ∧ 𝑎 ∈ 𝐵) ∧ 𝑥 ∈ ℎ) ∧ ({𝑎} ⊕ 𝑁) = ({𝑥} ⊕ 𝑁)) → 𝐺 ∈ Grp) | 
| 30 | 6 | subgss 19146 | . . . . . . . . . . . . . . . . 17
⊢ (ℎ ∈ (SubGrp‘𝐺) → ℎ ⊆ 𝐵) | 
| 31 | 30 | ad3antlr 731 | . . . . . . . . . . . . . . . 16
⊢ ((((𝜑 ∧ ℎ ∈ (SubGrp‘𝐺)) ∧ 𝑁 ⊆ ℎ) ∧ 𝑎 ∈ 𝐵) → ℎ ⊆ 𝐵) | 
| 32 | 31 | sselda 3982 | . . . . . . . . . . . . . . 15
⊢
(((((𝜑 ∧ ℎ ∈ (SubGrp‘𝐺)) ∧ 𝑁 ⊆ ℎ) ∧ 𝑎 ∈ 𝐵) ∧ 𝑥 ∈ ℎ) → 𝑥 ∈ 𝐵) | 
| 33 | 32 | adantr 480 | . . . . . . . . . . . . . 14
⊢
((((((𝜑 ∧ ℎ ∈ (SubGrp‘𝐺)) ∧ 𝑁 ⊆ ℎ) ∧ 𝑎 ∈ 𝐵) ∧ 𝑥 ∈ ℎ) ∧ ({𝑎} ⊕ 𝑁) = ({𝑥} ⊕ 𝑁)) → 𝑥 ∈ 𝐵) | 
| 34 |  | simplr 768 | . . . . . . . . . . . . . . 15
⊢
(((((𝜑 ∧ ℎ ∈ (SubGrp‘𝐺)) ∧ 𝑁 ⊆ ℎ) ∧ 𝑎 ∈ 𝐵) ∧ 𝑥 ∈ ℎ) → 𝑎 ∈ 𝐵) | 
| 35 | 34 | adantr 480 | . . . . . . . . . . . . . 14
⊢
((((((𝜑 ∧ ℎ ∈ (SubGrp‘𝐺)) ∧ 𝑁 ⊆ ℎ) ∧ 𝑎 ∈ 𝐵) ∧ 𝑥 ∈ ℎ) ∧ ({𝑎} ⊕ 𝑁) = ({𝑥} ⊕ 𝑁)) → 𝑎 ∈ 𝐵) | 
| 36 |  | eqid 2736 | . . . . . . . . . . . . . . 15
⊢
(+g‘𝐺) = (+g‘𝐺) | 
| 37 |  | eqid 2736 | . . . . . . . . . . . . . . 15
⊢
(invg‘𝐺) = (invg‘𝐺) | 
| 38 | 6, 36, 37 | grpasscan1 19020 | . . . . . . . . . . . . . 14
⊢ ((𝐺 ∈ Grp ∧ 𝑥 ∈ 𝐵 ∧ 𝑎 ∈ 𝐵) → (𝑥(+g‘𝐺)(((invg‘𝐺)‘𝑥)(+g‘𝐺)𝑎)) = 𝑎) | 
| 39 | 29, 33, 35, 38 | syl3anc 1372 | . . . . . . . . . . . . 13
⊢
((((((𝜑 ∧ ℎ ∈ (SubGrp‘𝐺)) ∧ 𝑁 ⊆ ℎ) ∧ 𝑎 ∈ 𝐵) ∧ 𝑥 ∈ ℎ) ∧ ({𝑎} ⊕ 𝑁) = ({𝑥} ⊕ 𝑁)) → (𝑥(+g‘𝐺)(((invg‘𝐺)‘𝑥)(+g‘𝐺)𝑎)) = 𝑎) | 
| 40 |  | simp-5r 785 | . . . . . . . . . . . . . 14
⊢
((((((𝜑 ∧ ℎ ∈ (SubGrp‘𝐺)) ∧ 𝑁 ⊆ ℎ) ∧ 𝑎 ∈ 𝐵) ∧ 𝑥 ∈ ℎ) ∧ ({𝑎} ⊕ 𝑁) = ({𝑥} ⊕ 𝑁)) → ℎ ∈ (SubGrp‘𝐺)) | 
| 41 |  | simplr 768 | . . . . . . . . . . . . . 14
⊢
((((((𝜑 ∧ ℎ ∈ (SubGrp‘𝐺)) ∧ 𝑁 ⊆ ℎ) ∧ 𝑎 ∈ 𝐵) ∧ 𝑥 ∈ ℎ) ∧ ({𝑎} ⊕ 𝑁) = ({𝑥} ⊕ 𝑁)) → 𝑥 ∈ ℎ) | 
| 42 |  | simp-4r 783 | . . . . . . . . . . . . . . 15
⊢
((((((𝜑 ∧ ℎ ∈ (SubGrp‘𝐺)) ∧ 𝑁 ⊆ ℎ) ∧ 𝑎 ∈ 𝐵) ∧ 𝑥 ∈ ℎ) ∧ ({𝑎} ⊕ 𝑁) = ({𝑥} ⊕ 𝑁)) → 𝑁 ⊆ ℎ) | 
| 43 | 6 | subgss 19146 | . . . . . . . . . . . . . . . . . 18
⊢ (𝑁 ∈ (SubGrp‘𝐺) → 𝑁 ⊆ 𝐵) | 
| 44 | 25, 43 | syl 17 | . . . . . . . . . . . . . . . . 17
⊢ (𝜑 → 𝑁 ⊆ 𝐵) | 
| 45 | 44 | ad5antr 734 | . . . . . . . . . . . . . . . 16
⊢
((((((𝜑 ∧ ℎ ∈ (SubGrp‘𝐺)) ∧ 𝑁 ⊆ ℎ) ∧ 𝑎 ∈ 𝐵) ∧ 𝑥 ∈ ℎ) ∧ ({𝑎} ⊕ 𝑁) = ({𝑥} ⊕ 𝑁)) → 𝑁 ⊆ 𝐵) | 
| 46 |  | eqid 2736 | . . . . . . . . . . . . . . . . . . . . 21
⊢ (𝐺 ~QG 𝑁) = (𝐺 ~QG 𝑁) | 
| 47 | 6, 46 | eqger 19197 | . . . . . . . . . . . . . . . . . . . 20
⊢ (𝑁 ∈ (SubGrp‘𝐺) → (𝐺 ~QG 𝑁) Er 𝐵) | 
| 48 | 25, 47 | syl 17 | . . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → (𝐺 ~QG 𝑁) Er 𝐵) | 
| 49 | 48 | ad4antr 732 | . . . . . . . . . . . . . . . . . 18
⊢
(((((𝜑 ∧ ℎ ∈ (SubGrp‘𝐺)) ∧ 𝑁 ⊆ ℎ) ∧ 𝑎 ∈ 𝐵) ∧ 𝑥 ∈ ℎ) → (𝐺 ~QG 𝑁) Er 𝐵) | 
| 50 | 49 | adantr 480 | . . . . . . . . . . . . . . . . 17
⊢
((((((𝜑 ∧ ℎ ∈ (SubGrp‘𝐺)) ∧ 𝑁 ⊆ ℎ) ∧ 𝑎 ∈ 𝐵) ∧ 𝑥 ∈ ℎ) ∧ ({𝑎} ⊕ 𝑁) = ({𝑥} ⊕ 𝑁)) → (𝐺 ~QG 𝑁) Er 𝐵) | 
| 51 | 49, 34 | erth 8797 | . . . . . . . . . . . . . . . . . . 19
⊢
(((((𝜑 ∧ ℎ ∈ (SubGrp‘𝐺)) ∧ 𝑁 ⊆ ℎ) ∧ 𝑎 ∈ 𝐵) ∧ 𝑥 ∈ ℎ) → (𝑎(𝐺 ~QG 𝑁)𝑥 ↔ [𝑎](𝐺 ~QG 𝑁) = [𝑥](𝐺 ~QG 𝑁))) | 
| 52 | 25 | ad4antr 732 | . . . . . . . . . . . . . . . . . . . . 21
⊢
(((((𝜑 ∧ ℎ ∈ (SubGrp‘𝐺)) ∧ 𝑁 ⊆ ℎ) ∧ 𝑎 ∈ 𝐵) ∧ 𝑥 ∈ ℎ) → 𝑁 ∈ (SubGrp‘𝐺)) | 
| 53 | 6, 11, 52, 34 | quslsm 33434 | . . . . . . . . . . . . . . . . . . . 20
⊢
(((((𝜑 ∧ ℎ ∈ (SubGrp‘𝐺)) ∧ 𝑁 ⊆ ℎ) ∧ 𝑎 ∈ 𝐵) ∧ 𝑥 ∈ ℎ) → [𝑎](𝐺 ~QG 𝑁) = ({𝑎} ⊕ 𝑁)) | 
| 54 | 6, 11, 52, 32 | quslsm 33434 | . . . . . . . . . . . . . . . . . . . 20
⊢
(((((𝜑 ∧ ℎ ∈ (SubGrp‘𝐺)) ∧ 𝑁 ⊆ ℎ) ∧ 𝑎 ∈ 𝐵) ∧ 𝑥 ∈ ℎ) → [𝑥](𝐺 ~QG 𝑁) = ({𝑥} ⊕ 𝑁)) | 
| 55 | 53, 54 | eqeq12d 2752 | . . . . . . . . . . . . . . . . . . 19
⊢
(((((𝜑 ∧ ℎ ∈ (SubGrp‘𝐺)) ∧ 𝑁 ⊆ ℎ) ∧ 𝑎 ∈ 𝐵) ∧ 𝑥 ∈ ℎ) → ([𝑎](𝐺 ~QG 𝑁) = [𝑥](𝐺 ~QG 𝑁) ↔ ({𝑎} ⊕ 𝑁) = ({𝑥} ⊕ 𝑁))) | 
| 56 | 51, 55 | bitrd 279 | . . . . . . . . . . . . . . . . . 18
⊢
(((((𝜑 ∧ ℎ ∈ (SubGrp‘𝐺)) ∧ 𝑁 ⊆ ℎ) ∧ 𝑎 ∈ 𝐵) ∧ 𝑥 ∈ ℎ) → (𝑎(𝐺 ~QG 𝑁)𝑥 ↔ ({𝑎} ⊕ 𝑁) = ({𝑥} ⊕ 𝑁))) | 
| 57 | 56 | biimpar 477 | . . . . . . . . . . . . . . . . 17
⊢
((((((𝜑 ∧ ℎ ∈ (SubGrp‘𝐺)) ∧ 𝑁 ⊆ ℎ) ∧ 𝑎 ∈ 𝐵) ∧ 𝑥 ∈ ℎ) ∧ ({𝑎} ⊕ 𝑁) = ({𝑥} ⊕ 𝑁)) → 𝑎(𝐺 ~QG 𝑁)𝑥) | 
| 58 | 50, 57 | ersym 8758 | . . . . . . . . . . . . . . . 16
⊢
((((((𝜑 ∧ ℎ ∈ (SubGrp‘𝐺)) ∧ 𝑁 ⊆ ℎ) ∧ 𝑎 ∈ 𝐵) ∧ 𝑥 ∈ ℎ) ∧ ({𝑎} ⊕ 𝑁) = ({𝑥} ⊕ 𝑁)) → 𝑥(𝐺 ~QG 𝑁)𝑎) | 
| 59 | 6, 37, 36, 46 | eqgval 19196 | . . . . . . . . . . . . . . . . . 18
⊢ ((𝐺 ∈ Grp ∧ 𝑁 ⊆ 𝐵) → (𝑥(𝐺 ~QG 𝑁)𝑎 ↔ (𝑥 ∈ 𝐵 ∧ 𝑎 ∈ 𝐵 ∧ (((invg‘𝐺)‘𝑥)(+g‘𝐺)𝑎) ∈ 𝑁))) | 
| 60 | 59 | biimpa 476 | . . . . . . . . . . . . . . . . 17
⊢ (((𝐺 ∈ Grp ∧ 𝑁 ⊆ 𝐵) ∧ 𝑥(𝐺 ~QG 𝑁)𝑎) → (𝑥 ∈ 𝐵 ∧ 𝑎 ∈ 𝐵 ∧ (((invg‘𝐺)‘𝑥)(+g‘𝐺)𝑎) ∈ 𝑁)) | 
| 61 | 60 | simp3d 1144 | . . . . . . . . . . . . . . . 16
⊢ (((𝐺 ∈ Grp ∧ 𝑁 ⊆ 𝐵) ∧ 𝑥(𝐺 ~QG 𝑁)𝑎) → (((invg‘𝐺)‘𝑥)(+g‘𝐺)𝑎) ∈ 𝑁) | 
| 62 | 29, 45, 58, 61 | syl21anc 837 | . . . . . . . . . . . . . . 15
⊢
((((((𝜑 ∧ ℎ ∈ (SubGrp‘𝐺)) ∧ 𝑁 ⊆ ℎ) ∧ 𝑎 ∈ 𝐵) ∧ 𝑥 ∈ ℎ) ∧ ({𝑎} ⊕ 𝑁) = ({𝑥} ⊕ 𝑁)) → (((invg‘𝐺)‘𝑥)(+g‘𝐺)𝑎) ∈ 𝑁) | 
| 63 | 42, 62 | sseldd 3983 | . . . . . . . . . . . . . 14
⊢
((((((𝜑 ∧ ℎ ∈ (SubGrp‘𝐺)) ∧ 𝑁 ⊆ ℎ) ∧ 𝑎 ∈ 𝐵) ∧ 𝑥 ∈ ℎ) ∧ ({𝑎} ⊕ 𝑁) = ({𝑥} ⊕ 𝑁)) → (((invg‘𝐺)‘𝑥)(+g‘𝐺)𝑎) ∈ ℎ) | 
| 64 | 36 | subgcl 19155 | . . . . . . . . . . . . . 14
⊢ ((ℎ ∈ (SubGrp‘𝐺) ∧ 𝑥 ∈ ℎ ∧ (((invg‘𝐺)‘𝑥)(+g‘𝐺)𝑎) ∈ ℎ) → (𝑥(+g‘𝐺)(((invg‘𝐺)‘𝑥)(+g‘𝐺)𝑎)) ∈ ℎ) | 
| 65 | 40, 41, 63, 64 | syl3anc 1372 | . . . . . . . . . . . . 13
⊢
((((((𝜑 ∧ ℎ ∈ (SubGrp‘𝐺)) ∧ 𝑁 ⊆ ℎ) ∧ 𝑎 ∈ 𝐵) ∧ 𝑥 ∈ ℎ) ∧ ({𝑎} ⊕ 𝑁) = ({𝑥} ⊕ 𝑁)) → (𝑥(+g‘𝐺)(((invg‘𝐺)‘𝑥)(+g‘𝐺)𝑎)) ∈ ℎ) | 
| 66 | 39, 65 | eqeltrrd 2841 | . . . . . . . . . . . 12
⊢
((((((𝜑 ∧ ℎ ∈ (SubGrp‘𝐺)) ∧ 𝑁 ⊆ ℎ) ∧ 𝑎 ∈ 𝐵) ∧ 𝑥 ∈ ℎ) ∧ ({𝑎} ⊕ 𝑁) = ({𝑥} ⊕ 𝑁)) → 𝑎 ∈ ℎ) | 
| 67 | 66 | adantllr 719 | . . . . . . . . . . 11
⊢
(((((((𝜑 ∧ ℎ ∈ (SubGrp‘𝐺)) ∧ 𝑁 ⊆ ℎ) ∧ 𝑎 ∈ 𝐵) ∧ ({𝑎} ⊕ 𝑁) ∈ ran (𝑥 ∈ ℎ ↦ ({𝑥} ⊕ 𝑁))) ∧ 𝑥 ∈ ℎ) ∧ ({𝑎} ⊕ 𝑁) = ({𝑥} ⊕ 𝑁)) → 𝑎 ∈ ℎ) | 
| 68 |  | eqid 2736 | . . . . . . . . . . . . . 14
⊢ (𝑥 ∈ ℎ ↦ ({𝑥} ⊕ 𝑁)) = (𝑥 ∈ ℎ ↦ ({𝑥} ⊕ 𝑁)) | 
| 69 |  | ovex 7465 | . . . . . . . . . . . . . 14
⊢ ({𝑥} ⊕ 𝑁) ∈ V | 
| 70 | 68, 69 | elrnmpti 5972 | . . . . . . . . . . . . 13
⊢ (({𝑎} ⊕ 𝑁) ∈ ran (𝑥 ∈ ℎ ↦ ({𝑥} ⊕ 𝑁)) ↔ ∃𝑥 ∈ ℎ ({𝑎} ⊕ 𝑁) = ({𝑥} ⊕ 𝑁)) | 
| 71 | 70 | biimpi 216 | . . . . . . . . . . . 12
⊢ (({𝑎} ⊕ 𝑁) ∈ ran (𝑥 ∈ ℎ ↦ ({𝑥} ⊕ 𝑁)) → ∃𝑥 ∈ ℎ ({𝑎} ⊕ 𝑁) = ({𝑥} ⊕ 𝑁)) | 
| 72 | 71 | adantl 481 | . . . . . . . . . . 11
⊢
(((((𝜑 ∧ ℎ ∈ (SubGrp‘𝐺)) ∧ 𝑁 ⊆ ℎ) ∧ 𝑎 ∈ 𝐵) ∧ ({𝑎} ⊕ 𝑁) ∈ ran (𝑥 ∈ ℎ ↦ ({𝑥} ⊕ 𝑁))) → ∃𝑥 ∈ ℎ ({𝑎} ⊕ 𝑁) = ({𝑥} ⊕ 𝑁)) | 
| 73 | 23, 67, 72 | r19.29af 3267 | . . . . . . . . . 10
⊢
(((((𝜑 ∧ ℎ ∈ (SubGrp‘𝐺)) ∧ 𝑁 ⊆ ℎ) ∧ 𝑎 ∈ 𝐵) ∧ ({𝑎} ⊕ 𝑁) ∈ ran (𝑥 ∈ ℎ ↦ ({𝑥} ⊕ 𝑁))) → 𝑎 ∈ ℎ) | 
| 74 |  | simpr 484 | . . . . . . . . . . 11
⊢
(((((𝜑 ∧ ℎ ∈ (SubGrp‘𝐺)) ∧ 𝑁 ⊆ ℎ) ∧ 𝑎 ∈ 𝐵) ∧ 𝑎 ∈ ℎ) → 𝑎 ∈ ℎ) | 
| 75 |  | ovexd 7467 | . . . . . . . . . . 11
⊢
(((((𝜑 ∧ ℎ ∈ (SubGrp‘𝐺)) ∧ 𝑁 ⊆ ℎ) ∧ 𝑎 ∈ 𝐵) ∧ 𝑎 ∈ ℎ) → ({𝑎} ⊕ 𝑁) ∈ V) | 
| 76 |  | sneq 4635 | . . . . . . . . . . . . . 14
⊢ (𝑥 = 𝑎 → {𝑥} = {𝑎}) | 
| 77 | 76 | oveq1d 7447 | . . . . . . . . . . . . 13
⊢ (𝑥 = 𝑎 → ({𝑥} ⊕ 𝑁) = ({𝑎} ⊕ 𝑁)) | 
| 78 | 77 | eqcomd 2742 | . . . . . . . . . . . 12
⊢ (𝑥 = 𝑎 → ({𝑎} ⊕ 𝑁) = ({𝑥} ⊕ 𝑁)) | 
| 79 | 78 | adantl 481 | . . . . . . . . . . 11
⊢
((((((𝜑 ∧ ℎ ∈ (SubGrp‘𝐺)) ∧ 𝑁 ⊆ ℎ) ∧ 𝑎 ∈ 𝐵) ∧ 𝑎 ∈ ℎ) ∧ 𝑥 = 𝑎) → ({𝑎} ⊕ 𝑁) = ({𝑥} ⊕ 𝑁)) | 
| 80 | 68, 74, 75, 79 | elrnmptdv 5975 | . . . . . . . . . 10
⊢
(((((𝜑 ∧ ℎ ∈ (SubGrp‘𝐺)) ∧ 𝑁 ⊆ ℎ) ∧ 𝑎 ∈ 𝐵) ∧ 𝑎 ∈ ℎ) → ({𝑎} ⊕ 𝑁) ∈ ran (𝑥 ∈ ℎ ↦ ({𝑥} ⊕ 𝑁))) | 
| 81 | 73, 80 | impbida 800 | . . . . . . . . 9
⊢ ((((𝜑 ∧ ℎ ∈ (SubGrp‘𝐺)) ∧ 𝑁 ⊆ ℎ) ∧ 𝑎 ∈ 𝐵) → (({𝑎} ⊕ 𝑁) ∈ ran (𝑥 ∈ ℎ ↦ ({𝑥} ⊕ 𝑁)) ↔ 𝑎 ∈ ℎ)) | 
| 82 | 81 | rabbidva 3442 | . . . . . . . 8
⊢ (((𝜑 ∧ ℎ ∈ (SubGrp‘𝐺)) ∧ 𝑁 ⊆ ℎ) → {𝑎 ∈ 𝐵 ∣ ({𝑎} ⊕ 𝑁) ∈ ran (𝑥 ∈ ℎ ↦ ({𝑥} ⊕ 𝑁))} = {𝑎 ∈ 𝐵 ∣ 𝑎 ∈ ℎ}) | 
| 83 | 30 | adantl 481 | . . . . . . . . . 10
⊢ ((𝜑 ∧ ℎ ∈ (SubGrp‘𝐺)) → ℎ ⊆ 𝐵) | 
| 84 |  | dfss7 4250 | . . . . . . . . . 10
⊢ (ℎ ⊆ 𝐵 ↔ {𝑎 ∈ 𝐵 ∣ 𝑎 ∈ ℎ} = ℎ) | 
| 85 | 83, 84 | sylib 218 | . . . . . . . . 9
⊢ ((𝜑 ∧ ℎ ∈ (SubGrp‘𝐺)) → {𝑎 ∈ 𝐵 ∣ 𝑎 ∈ ℎ} = ℎ) | 
| 86 | 85 | adantr 480 | . . . . . . . 8
⊢ (((𝜑 ∧ ℎ ∈ (SubGrp‘𝐺)) ∧ 𝑁 ⊆ ℎ) → {𝑎 ∈ 𝐵 ∣ 𝑎 ∈ ℎ} = ℎ) | 
| 87 | 82, 86 | eqtr2d 2777 | . . . . . . 7
⊢ (((𝜑 ∧ ℎ ∈ (SubGrp‘𝐺)) ∧ 𝑁 ⊆ ℎ) → ℎ = {𝑎 ∈ 𝐵 ∣ ({𝑎} ⊕ 𝑁) ∈ ran (𝑥 ∈ ℎ ↦ ({𝑥} ⊕ 𝑁))}) | 
| 88 | 14, 18, 87 | rspcedvd 3623 | . . . . . 6
⊢ (((𝜑 ∧ ℎ ∈ (SubGrp‘𝐺)) ∧ 𝑁 ⊆ ℎ) → ∃𝑓 ∈ 𝑇 ℎ = {𝑎 ∈ 𝐵 ∣ ({𝑎} ⊕ 𝑁) ∈ 𝑓}) | 
| 89 | 88 | anasss 466 | . . . . 5
⊢ ((𝜑 ∧ (ℎ ∈ (SubGrp‘𝐺) ∧ 𝑁 ⊆ ℎ)) → ∃𝑓 ∈ 𝑇 ℎ = {𝑎 ∈ 𝐵 ∣ ({𝑎} ⊕ 𝑁) ∈ 𝑓}) | 
| 90 | 13 | adantr 480 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑓 ∈ 𝑇) → 𝑁 ∈ (NrmSGrp‘𝐺)) | 
| 91 | 7 | eleq2i 2832 | . . . . . . . . . . . 12
⊢ (𝑓 ∈ 𝑇 ↔ 𝑓 ∈ (SubGrp‘𝑄)) | 
| 92 | 91 | biimpi 216 | . . . . . . . . . . 11
⊢ (𝑓 ∈ 𝑇 → 𝑓 ∈ (SubGrp‘𝑄)) | 
| 93 | 92 | adantl 481 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑓 ∈ 𝑇) → 𝑓 ∈ (SubGrp‘𝑄)) | 
| 94 | 6, 10, 11, 90, 93 | nsgmgclem 33440 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑓 ∈ 𝑇) → {𝑎 ∈ 𝐵 ∣ ({𝑎} ⊕ 𝑁) ∈ 𝑓} ∈ (SubGrp‘𝐺)) | 
| 95 | 94 | adantr 480 | . . . . . . . 8
⊢ (((𝜑 ∧ 𝑓 ∈ 𝑇) ∧ ℎ = {𝑎 ∈ 𝐵 ∣ ({𝑎} ⊕ 𝑁) ∈ 𝑓}) → {𝑎 ∈ 𝐵 ∣ ({𝑎} ⊕ 𝑁) ∈ 𝑓} ∈ (SubGrp‘𝐺)) | 
| 96 |  | eleq1 2828 | . . . . . . . . 9
⊢ (ℎ = {𝑎 ∈ 𝐵 ∣ ({𝑎} ⊕ 𝑁) ∈ 𝑓} → (ℎ ∈ (SubGrp‘𝐺) ↔ {𝑎 ∈ 𝐵 ∣ ({𝑎} ⊕ 𝑁) ∈ 𝑓} ∈ (SubGrp‘𝐺))) | 
| 97 | 96 | adantl 481 | . . . . . . . 8
⊢ (((𝜑 ∧ 𝑓 ∈ 𝑇) ∧ ℎ = {𝑎 ∈ 𝐵 ∣ ({𝑎} ⊕ 𝑁) ∈ 𝑓}) → (ℎ ∈ (SubGrp‘𝐺) ↔ {𝑎 ∈ 𝐵 ∣ ({𝑎} ⊕ 𝑁) ∈ 𝑓} ∈ (SubGrp‘𝐺))) | 
| 98 | 95, 97 | mpbird 257 | . . . . . . 7
⊢ (((𝜑 ∧ 𝑓 ∈ 𝑇) ∧ ℎ = {𝑎 ∈ 𝐵 ∣ ({𝑎} ⊕ 𝑁) ∈ 𝑓}) → ℎ ∈ (SubGrp‘𝐺)) | 
| 99 | 44 | adantr 480 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑓 ∈ 𝑇) → 𝑁 ⊆ 𝐵) | 
| 100 | 25 | ad2antrr 726 | . . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑓 ∈ 𝑇) ∧ 𝑎 ∈ 𝑁) → 𝑁 ∈ (SubGrp‘𝐺)) | 
| 101 |  | simpr 484 | . . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑓 ∈ 𝑇) ∧ 𝑎 ∈ 𝑁) → 𝑎 ∈ 𝑁) | 
| 102 | 11 | grplsmid 33433 | . . . . . . . . . . . 12
⊢ ((𝑁 ∈ (SubGrp‘𝐺) ∧ 𝑎 ∈ 𝑁) → ({𝑎} ⊕ 𝑁) = 𝑁) | 
| 103 | 100, 101,
102 | syl2anc 584 | . . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑓 ∈ 𝑇) ∧ 𝑎 ∈ 𝑁) → ({𝑎} ⊕ 𝑁) = 𝑁) | 
| 104 | 10 | nsgqus0 33439 | . . . . . . . . . . . . 13
⊢ ((𝑁 ∈ (NrmSGrp‘𝐺) ∧ 𝑓 ∈ (SubGrp‘𝑄)) → 𝑁 ∈ 𝑓) | 
| 105 | 90, 93, 104 | syl2anc 584 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑓 ∈ 𝑇) → 𝑁 ∈ 𝑓) | 
| 106 | 105 | adantr 480 | . . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑓 ∈ 𝑇) ∧ 𝑎 ∈ 𝑁) → 𝑁 ∈ 𝑓) | 
| 107 | 103, 106 | eqeltrd 2840 | . . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑓 ∈ 𝑇) ∧ 𝑎 ∈ 𝑁) → ({𝑎} ⊕ 𝑁) ∈ 𝑓) | 
| 108 | 99, 107 | ssrabdv 4073 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑓 ∈ 𝑇) → 𝑁 ⊆ {𝑎 ∈ 𝐵 ∣ ({𝑎} ⊕ 𝑁) ∈ 𝑓}) | 
| 109 | 108 | adantr 480 | . . . . . . . 8
⊢ (((𝜑 ∧ 𝑓 ∈ 𝑇) ∧ ℎ = {𝑎 ∈ 𝐵 ∣ ({𝑎} ⊕ 𝑁) ∈ 𝑓}) → 𝑁 ⊆ {𝑎 ∈ 𝐵 ∣ ({𝑎} ⊕ 𝑁) ∈ 𝑓}) | 
| 110 |  | simpr 484 | . . . . . . . 8
⊢ (((𝜑 ∧ 𝑓 ∈ 𝑇) ∧ ℎ = {𝑎 ∈ 𝐵 ∣ ({𝑎} ⊕ 𝑁) ∈ 𝑓}) → ℎ = {𝑎 ∈ 𝐵 ∣ ({𝑎} ⊕ 𝑁) ∈ 𝑓}) | 
| 111 | 109, 110 | sseqtrrd 4020 | . . . . . . 7
⊢ (((𝜑 ∧ 𝑓 ∈ 𝑇) ∧ ℎ = {𝑎 ∈ 𝐵 ∣ ({𝑎} ⊕ 𝑁) ∈ 𝑓}) → 𝑁 ⊆ ℎ) | 
| 112 | 98, 111 | jca 511 | . . . . . 6
⊢ (((𝜑 ∧ 𝑓 ∈ 𝑇) ∧ ℎ = {𝑎 ∈ 𝐵 ∣ ({𝑎} ⊕ 𝑁) ∈ 𝑓}) → (ℎ ∈ (SubGrp‘𝐺) ∧ 𝑁 ⊆ ℎ)) | 
| 113 | 112 | r19.29an 3157 | . . . . 5
⊢ ((𝜑 ∧ ∃𝑓 ∈ 𝑇 ℎ = {𝑎 ∈ 𝐵 ∣ ({𝑎} ⊕ 𝑁) ∈ 𝑓}) → (ℎ ∈ (SubGrp‘𝐺) ∧ 𝑁 ⊆ ℎ)) | 
| 114 | 89, 113 | impbida 800 | . . . 4
⊢ (𝜑 → ((ℎ ∈ (SubGrp‘𝐺) ∧ 𝑁 ⊆ ℎ) ↔ ∃𝑓 ∈ 𝑇 ℎ = {𝑎 ∈ 𝐵 ∣ ({𝑎} ⊕ 𝑁) ∈ 𝑓})) | 
| 115 | 5, 114 | bitrid 283 | . . 3
⊢ (𝜑 → (ℎ ∈ 𝑆 ↔ ∃𝑓 ∈ 𝑇 ℎ = {𝑎 ∈ 𝐵 ∣ ({𝑎} ⊕ 𝑁) ∈ 𝑓})) | 
| 116 | 3, 115 | bitr4id 290 | . 2
⊢ (𝜑 → (ℎ ∈ ran 𝐹 ↔ ℎ ∈ 𝑆)) | 
| 117 | 116 | eqrdv 2734 | 1
⊢ (𝜑 → ran 𝐹 = 𝑆) |