Users' Mathboxes Mathbox for Thierry Arnoux < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  nsgqusf1olem3 Structured version   Visualization version   GIF version

Theorem nsgqusf1olem3 32233
Description: Lemma for nsgqusf1o 32234. (Contributed by Thierry Arnoux, 4-Aug-2024.)
Hypotheses
Ref Expression
nsgqusf1o.b 𝐡 = (Baseβ€˜πΊ)
nsgqusf1o.s 𝑆 = {β„Ž ∈ (SubGrpβ€˜πΊ) ∣ 𝑁 βŠ† β„Ž}
nsgqusf1o.t 𝑇 = (SubGrpβ€˜π‘„)
nsgqusf1o.1 ≀ = (leβ€˜(toIncβ€˜π‘†))
nsgqusf1o.2 ≲ = (leβ€˜(toIncβ€˜π‘‡))
nsgqusf1o.q 𝑄 = (𝐺 /s (𝐺 ~QG 𝑁))
nsgqusf1o.p βŠ• = (LSSumβ€˜πΊ)
nsgqusf1o.e 𝐸 = (β„Ž ∈ 𝑆 ↦ ran (π‘₯ ∈ β„Ž ↦ ({π‘₯} βŠ• 𝑁)))
nsgqusf1o.f 𝐹 = (𝑓 ∈ 𝑇 ↦ {π‘Ž ∈ 𝐡 ∣ ({π‘Ž} βŠ• 𝑁) ∈ 𝑓})
nsgqusf1o.n (πœ‘ β†’ 𝑁 ∈ (NrmSGrpβ€˜πΊ))
Assertion
Ref Expression
nsgqusf1olem3 (πœ‘ β†’ ran 𝐹 = 𝑆)
Distinct variable groups:   βŠ• ,π‘Ž,𝑓,β„Ž,π‘₯   𝐡,π‘Ž,𝑓,β„Ž,π‘₯   𝐸,π‘Ž,𝑓,β„Ž,π‘₯   𝑓,𝐹,β„Ž,π‘₯   𝐺,π‘Ž,𝑓,β„Ž,π‘₯   𝑁,π‘Ž,𝑓,β„Ž,π‘₯   𝑄,π‘Ž,𝑓,β„Ž,π‘₯   𝑆,π‘Ž,𝑓,β„Ž,π‘₯   𝑇,π‘Ž,𝑓,β„Ž,π‘₯   πœ‘,π‘Ž,𝑓,β„Ž,π‘₯
Allowed substitution hints:   𝐹(π‘Ž)   ≀ (π‘₯,𝑓,β„Ž,π‘Ž)   ≲ (π‘₯,𝑓,β„Ž,π‘Ž)

Proof of Theorem nsgqusf1olem3
StepHypRef Expression
1 nsgqusf1o.f . . . . 5 𝐹 = (𝑓 ∈ 𝑇 ↦ {π‘Ž ∈ 𝐡 ∣ ({π‘Ž} βŠ• 𝑁) ∈ 𝑓})
21elrnmpt 5916 . . . 4 (β„Ž ∈ V β†’ (β„Ž ∈ ran 𝐹 ↔ βˆƒπ‘“ ∈ 𝑇 β„Ž = {π‘Ž ∈ 𝐡 ∣ ({π‘Ž} βŠ• 𝑁) ∈ 𝑓}))
32elv 3454 . . 3 (β„Ž ∈ ran 𝐹 ↔ βˆƒπ‘“ ∈ 𝑇 β„Ž = {π‘Ž ∈ 𝐡 ∣ ({π‘Ž} βŠ• 𝑁) ∈ 𝑓})
4 nsgqusf1o.s . . . . 5 𝑆 = {β„Ž ∈ (SubGrpβ€˜πΊ) ∣ 𝑁 βŠ† β„Ž}
54reqabi 3432 . . . 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β€˜πΊ))
146, 4, 7, 8, 9, 10, 11, 12, 1, 13nsgqusf1olem1 32231 . . . . . . 7 (((πœ‘ ∧ β„Ž ∈ (SubGrpβ€˜πΊ)) ∧ 𝑁 βŠ† β„Ž) β†’ ran (π‘₯ ∈ β„Ž ↦ ({π‘₯} βŠ• 𝑁)) ∈ 𝑇)
15 eleq2 2827 . . . . . . . . . 10 (𝑓 = ran (π‘₯ ∈ β„Ž ↦ ({π‘₯} βŠ• 𝑁)) β†’ (({π‘Ž} βŠ• 𝑁) ∈ 𝑓 ↔ ({π‘Ž} βŠ• 𝑁) ∈ ran (π‘₯ ∈ β„Ž ↦ ({π‘₯} βŠ• 𝑁))))
1615rabbidv 3418 . . . . . . . . 9 (𝑓 = ran (π‘₯ ∈ β„Ž ↦ ({π‘₯} βŠ• 𝑁)) β†’ {π‘Ž ∈ 𝐡 ∣ ({π‘Ž} βŠ• 𝑁) ∈ 𝑓} = {π‘Ž ∈ 𝐡 ∣ ({π‘Ž} βŠ• 𝑁) ∈ ran (π‘₯ ∈ β„Ž ↦ ({π‘₯} βŠ• 𝑁))})
1716eqeq2d 2748 . . . . . . . 8 (𝑓 = ran (π‘₯ ∈ β„Ž ↦ ({π‘₯} βŠ• 𝑁)) β†’ (β„Ž = {π‘Ž ∈ 𝐡 ∣ ({π‘Ž} βŠ• 𝑁) ∈ 𝑓} ↔ β„Ž = {π‘Ž ∈ 𝐡 ∣ ({π‘Ž} βŠ• 𝑁) ∈ ran (π‘₯ ∈ β„Ž ↦ ({π‘₯} βŠ• 𝑁))}))
1817adantl 483 . . . . . . 7 ((((πœ‘ ∧ β„Ž ∈ (SubGrpβ€˜πΊ)) ∧ 𝑁 βŠ† β„Ž) ∧ 𝑓 = ran (π‘₯ ∈ β„Ž ↦ ({π‘₯} βŠ• 𝑁))) β†’ (β„Ž = {π‘Ž ∈ 𝐡 ∣ ({π‘Ž} βŠ• 𝑁) ∈ 𝑓} ↔ β„Ž = {π‘Ž ∈ 𝐡 ∣ ({π‘Ž} βŠ• 𝑁) ∈ ran (π‘₯ ∈ β„Ž ↦ ({π‘₯} βŠ• 𝑁))}))
19 nfv 1918 . . . . . . . . . . . 12 β„²π‘₯(((πœ‘ ∧ β„Ž ∈ (SubGrpβ€˜πΊ)) ∧ 𝑁 βŠ† β„Ž) ∧ π‘Ž ∈ 𝐡)
20 nfmpt1 5218 . . . . . . . . . . . . . 14 β„²π‘₯(π‘₯ ∈ β„Ž ↦ ({π‘₯} βŠ• 𝑁))
2120nfrn 5912 . . . . . . . . . . . . 13 β„²π‘₯ran (π‘₯ ∈ β„Ž ↦ ({π‘₯} βŠ• 𝑁))
2221nfel2 2926 . . . . . . . . . . . 12 β„²π‘₯({π‘Ž} βŠ• 𝑁) ∈ ran (π‘₯ ∈ β„Ž ↦ ({π‘₯} βŠ• 𝑁))
2319, 22nfan 1903 . . . . . . . . . . 11 β„²π‘₯((((πœ‘ ∧ β„Ž ∈ (SubGrpβ€˜πΊ)) ∧ 𝑁 βŠ† β„Ž) ∧ π‘Ž ∈ 𝐡) ∧ ({π‘Ž} βŠ• 𝑁) ∈ ran (π‘₯ ∈ β„Ž ↦ ({π‘₯} βŠ• 𝑁)))
24 nsgsubg 18967 . . . . . . . . . . . . . . . . . 18 (𝑁 ∈ (NrmSGrpβ€˜πΊ) β†’ 𝑁 ∈ (SubGrpβ€˜πΊ))
2513, 24syl 17 . . . . . . . . . . . . . . . . 17 (πœ‘ β†’ 𝑁 ∈ (SubGrpβ€˜πΊ))
26 subgrcl 18940 . . . . . . . . . . . . . . . . 17 (𝑁 ∈ (SubGrpβ€˜πΊ) β†’ 𝐺 ∈ Grp)
2725, 26syl 17 . . . . . . . . . . . . . . . 16 (πœ‘ β†’ 𝐺 ∈ Grp)
2827ad4antr 731 . . . . . . . . . . . . . . 15 (((((πœ‘ ∧ β„Ž ∈ (SubGrpβ€˜πΊ)) ∧ 𝑁 βŠ† β„Ž) ∧ π‘Ž ∈ 𝐡) ∧ π‘₯ ∈ β„Ž) β†’ 𝐺 ∈ Grp)
2928adantr 482 . . . . . . . . . . . . . 14 ((((((πœ‘ ∧ β„Ž ∈ (SubGrpβ€˜πΊ)) ∧ 𝑁 βŠ† β„Ž) ∧ π‘Ž ∈ 𝐡) ∧ π‘₯ ∈ β„Ž) ∧ ({π‘Ž} βŠ• 𝑁) = ({π‘₯} βŠ• 𝑁)) β†’ 𝐺 ∈ Grp)
306subgss 18936 . . . . . . . . . . . . . . . . 17 (β„Ž ∈ (SubGrpβ€˜πΊ) β†’ β„Ž βŠ† 𝐡)
3130ad3antlr 730 . . . . . . . . . . . . . . . 16 ((((πœ‘ ∧ β„Ž ∈ (SubGrpβ€˜πΊ)) ∧ 𝑁 βŠ† β„Ž) ∧ π‘Ž ∈ 𝐡) β†’ β„Ž βŠ† 𝐡)
3231sselda 3949 . . . . . . . . . . . . . . 15 (((((πœ‘ ∧ β„Ž ∈ (SubGrpβ€˜πΊ)) ∧ 𝑁 βŠ† β„Ž) ∧ π‘Ž ∈ 𝐡) ∧ π‘₯ ∈ β„Ž) β†’ π‘₯ ∈ 𝐡)
3332adantr 482 . . . . . . . . . . . . . 14 ((((((πœ‘ ∧ β„Ž ∈ (SubGrpβ€˜πΊ)) ∧ 𝑁 βŠ† β„Ž) ∧ π‘Ž ∈ 𝐡) ∧ π‘₯ ∈ β„Ž) ∧ ({π‘Ž} βŠ• 𝑁) = ({π‘₯} βŠ• 𝑁)) β†’ π‘₯ ∈ 𝐡)
34 simplr 768 . . . . . . . . . . . . . . 15 (((((πœ‘ ∧ β„Ž ∈ (SubGrpβ€˜πΊ)) ∧ 𝑁 βŠ† β„Ž) ∧ π‘Ž ∈ 𝐡) ∧ π‘₯ ∈ β„Ž) β†’ π‘Ž ∈ 𝐡)
3534adantr 482 . . . . . . . . . . . . . 14 ((((((πœ‘ ∧ β„Ž ∈ (SubGrpβ€˜πΊ)) ∧ 𝑁 βŠ† β„Ž) ∧ π‘Ž ∈ 𝐡) ∧ π‘₯ ∈ β„Ž) ∧ ({π‘Ž} βŠ• 𝑁) = ({π‘₯} βŠ• 𝑁)) β†’ π‘Ž ∈ 𝐡)
36 eqid 2737 . . . . . . . . . . . . . . 15 (+gβ€˜πΊ) = (+gβ€˜πΊ)
37 eqid 2737 . . . . . . . . . . . . . . 15 (invgβ€˜πΊ) = (invgβ€˜πΊ)
386, 36, 37grpasscan1 18817 . . . . . . . . . . . . . 14 ((𝐺 ∈ Grp ∧ π‘₯ ∈ 𝐡 ∧ π‘Ž ∈ 𝐡) β†’ (π‘₯(+gβ€˜πΊ)(((invgβ€˜πΊ)β€˜π‘₯)(+gβ€˜πΊ)π‘Ž)) = π‘Ž)
3929, 33, 35, 38syl3anc 1372 . . . . . . . . . . . . 13 ((((((πœ‘ ∧ β„Ž ∈ (SubGrpβ€˜πΊ)) ∧ 𝑁 βŠ† β„Ž) ∧ π‘Ž ∈ 𝐡) ∧ π‘₯ ∈ β„Ž) ∧ ({π‘Ž} βŠ• 𝑁) = ({π‘₯} βŠ• 𝑁)) β†’ (π‘₯(+gβ€˜πΊ)(((invgβ€˜πΊ)β€˜π‘₯)(+gβ€˜πΊ)π‘Ž)) = π‘Ž)
40 simp-5r 785 . . . . . . . . . . . . . 14 ((((((πœ‘ ∧ β„Ž ∈ (SubGrpβ€˜πΊ)) ∧ 𝑁 βŠ† β„Ž) ∧ π‘Ž ∈ 𝐡) ∧ π‘₯ ∈ β„Ž) ∧ ({π‘Ž} βŠ• 𝑁) = ({π‘₯} βŠ• 𝑁)) β†’ β„Ž ∈ (SubGrpβ€˜πΊ))
41 simplr 768 . . . . . . . . . . . . . 14 ((((((πœ‘ ∧ β„Ž ∈ (SubGrpβ€˜πΊ)) ∧ 𝑁 βŠ† β„Ž) ∧ π‘Ž ∈ 𝐡) ∧ π‘₯ ∈ β„Ž) ∧ ({π‘Ž} βŠ• 𝑁) = ({π‘₯} βŠ• 𝑁)) β†’ π‘₯ ∈ β„Ž)
42 simp-4r 783 . . . . . . . . . . . . . . 15 ((((((πœ‘ ∧ β„Ž ∈ (SubGrpβ€˜πΊ)) ∧ 𝑁 βŠ† β„Ž) ∧ π‘Ž ∈ 𝐡) ∧ π‘₯ ∈ β„Ž) ∧ ({π‘Ž} βŠ• 𝑁) = ({π‘₯} βŠ• 𝑁)) β†’ 𝑁 βŠ† β„Ž)
436subgss 18936 . . . . . . . . . . . . . . . . . 18 (𝑁 ∈ (SubGrpβ€˜πΊ) β†’ 𝑁 βŠ† 𝐡)
4425, 43syl 17 . . . . . . . . . . . . . . . . 17 (πœ‘ β†’ 𝑁 βŠ† 𝐡)
4544ad5antr 733 . . . . . . . . . . . . . . . 16 ((((((πœ‘ ∧ β„Ž ∈ (SubGrpβ€˜πΊ)) ∧ 𝑁 βŠ† β„Ž) ∧ π‘Ž ∈ 𝐡) ∧ π‘₯ ∈ β„Ž) ∧ ({π‘Ž} βŠ• 𝑁) = ({π‘₯} βŠ• 𝑁)) β†’ 𝑁 βŠ† 𝐡)
46 eqid 2737 . . . . . . . . . . . . . . . . . . . . 21 (𝐺 ~QG 𝑁) = (𝐺 ~QG 𝑁)
476, 46eqger 18987 . . . . . . . . . . . . . . . . . . . 20 (𝑁 ∈ (SubGrpβ€˜πΊ) β†’ (𝐺 ~QG 𝑁) Er 𝐡)
4825, 47syl 17 . . . . . . . . . . . . . . . . . . 19 (πœ‘ β†’ (𝐺 ~QG 𝑁) Er 𝐡)
4948ad4antr 731 . . . . . . . . . . . . . . . . . 18 (((((πœ‘ ∧ β„Ž ∈ (SubGrpβ€˜πΊ)) ∧ 𝑁 βŠ† β„Ž) ∧ π‘Ž ∈ 𝐡) ∧ π‘₯ ∈ β„Ž) β†’ (𝐺 ~QG 𝑁) Er 𝐡)
5049adantr 482 . . . . . . . . . . . . . . . . 17 ((((((πœ‘ ∧ β„Ž ∈ (SubGrpβ€˜πΊ)) ∧ 𝑁 βŠ† β„Ž) ∧ π‘Ž ∈ 𝐡) ∧ π‘₯ ∈ β„Ž) ∧ ({π‘Ž} βŠ• 𝑁) = ({π‘₯} βŠ• 𝑁)) β†’ (𝐺 ~QG 𝑁) Er 𝐡)
5149, 34erth 8704 . . . . . . . . . . . . . . . . . . 19 (((((πœ‘ ∧ β„Ž ∈ (SubGrpβ€˜πΊ)) ∧ 𝑁 βŠ† β„Ž) ∧ π‘Ž ∈ 𝐡) ∧ π‘₯ ∈ β„Ž) β†’ (π‘Ž(𝐺 ~QG 𝑁)π‘₯ ↔ [π‘Ž](𝐺 ~QG 𝑁) = [π‘₯](𝐺 ~QG 𝑁)))
5225ad4antr 731 . . . . . . . . . . . . . . . . . . . . 21 (((((πœ‘ ∧ β„Ž ∈ (SubGrpβ€˜πΊ)) ∧ 𝑁 βŠ† β„Ž) ∧ π‘Ž ∈ 𝐡) ∧ π‘₯ ∈ β„Ž) β†’ 𝑁 ∈ (SubGrpβ€˜πΊ))
536, 11, 52, 34quslsm 32226 . . . . . . . . . . . . . . . . . . . 20 (((((πœ‘ ∧ β„Ž ∈ (SubGrpβ€˜πΊ)) ∧ 𝑁 βŠ† β„Ž) ∧ π‘Ž ∈ 𝐡) ∧ π‘₯ ∈ β„Ž) β†’ [π‘Ž](𝐺 ~QG 𝑁) = ({π‘Ž} βŠ• 𝑁))
546, 11, 52, 32quslsm 32226 . . . . . . . . . . . . . . . . . . . 20 (((((πœ‘ ∧ β„Ž ∈ (SubGrpβ€˜πΊ)) ∧ 𝑁 βŠ† β„Ž) ∧ π‘Ž ∈ 𝐡) ∧ π‘₯ ∈ β„Ž) β†’ [π‘₯](𝐺 ~QG 𝑁) = ({π‘₯} βŠ• 𝑁))
5553, 54eqeq12d 2753 . . . . . . . . . . . . . . . . . . 19 (((((πœ‘ ∧ β„Ž ∈ (SubGrpβ€˜πΊ)) ∧ 𝑁 βŠ† β„Ž) ∧ π‘Ž ∈ 𝐡) ∧ π‘₯ ∈ β„Ž) β†’ ([π‘Ž](𝐺 ~QG 𝑁) = [π‘₯](𝐺 ~QG 𝑁) ↔ ({π‘Ž} βŠ• 𝑁) = ({π‘₯} βŠ• 𝑁)))
5651, 55bitrd 279 . . . . . . . . . . . . . . . . . 18 (((((πœ‘ ∧ β„Ž ∈ (SubGrpβ€˜πΊ)) ∧ 𝑁 βŠ† β„Ž) ∧ π‘Ž ∈ 𝐡) ∧ π‘₯ ∈ β„Ž) β†’ (π‘Ž(𝐺 ~QG 𝑁)π‘₯ ↔ ({π‘Ž} βŠ• 𝑁) = ({π‘₯} βŠ• 𝑁)))
5756biimpar 479 . . . . . . . . . . . . . . . . 17 ((((((πœ‘ ∧ β„Ž ∈ (SubGrpβ€˜πΊ)) ∧ 𝑁 βŠ† β„Ž) ∧ π‘Ž ∈ 𝐡) ∧ π‘₯ ∈ β„Ž) ∧ ({π‘Ž} βŠ• 𝑁) = ({π‘₯} βŠ• 𝑁)) β†’ π‘Ž(𝐺 ~QG 𝑁)π‘₯)
5850, 57ersym 8667 . . . . . . . . . . . . . . . 16 ((((((πœ‘ ∧ β„Ž ∈ (SubGrpβ€˜πΊ)) ∧ 𝑁 βŠ† β„Ž) ∧ π‘Ž ∈ 𝐡) ∧ π‘₯ ∈ β„Ž) ∧ ({π‘Ž} βŠ• 𝑁) = ({π‘₯} βŠ• 𝑁)) β†’ π‘₯(𝐺 ~QG 𝑁)π‘Ž)
596, 37, 36, 46eqgval 18986 . . . . . . . . . . . . . . . . . 18 ((𝐺 ∈ Grp ∧ 𝑁 βŠ† 𝐡) β†’ (π‘₯(𝐺 ~QG 𝑁)π‘Ž ↔ (π‘₯ ∈ 𝐡 ∧ π‘Ž ∈ 𝐡 ∧ (((invgβ€˜πΊ)β€˜π‘₯)(+gβ€˜πΊ)π‘Ž) ∈ 𝑁)))
6059biimpa 478 . . . . . . . . . . . . . . . . 17 (((𝐺 ∈ Grp ∧ 𝑁 βŠ† 𝐡) ∧ π‘₯(𝐺 ~QG 𝑁)π‘Ž) β†’ (π‘₯ ∈ 𝐡 ∧ π‘Ž ∈ 𝐡 ∧ (((invgβ€˜πΊ)β€˜π‘₯)(+gβ€˜πΊ)π‘Ž) ∈ 𝑁))
6160simp3d 1145 . . . . . . . . . . . . . . . 16 (((𝐺 ∈ Grp ∧ 𝑁 βŠ† 𝐡) ∧ π‘₯(𝐺 ~QG 𝑁)π‘Ž) β†’ (((invgβ€˜πΊ)β€˜π‘₯)(+gβ€˜πΊ)π‘Ž) ∈ 𝑁)
6229, 45, 58, 61syl21anc 837 . . . . . . . . . . . . . . 15 ((((((πœ‘ ∧ β„Ž ∈ (SubGrpβ€˜πΊ)) ∧ 𝑁 βŠ† β„Ž) ∧ π‘Ž ∈ 𝐡) ∧ π‘₯ ∈ β„Ž) ∧ ({π‘Ž} βŠ• 𝑁) = ({π‘₯} βŠ• 𝑁)) β†’ (((invgβ€˜πΊ)β€˜π‘₯)(+gβ€˜πΊ)π‘Ž) ∈ 𝑁)
6342, 62sseldd 3950 . . . . . . . . . . . . . 14 ((((((πœ‘ ∧ β„Ž ∈ (SubGrpβ€˜πΊ)) ∧ 𝑁 βŠ† β„Ž) ∧ π‘Ž ∈ 𝐡) ∧ π‘₯ ∈ β„Ž) ∧ ({π‘Ž} βŠ• 𝑁) = ({π‘₯} βŠ• 𝑁)) β†’ (((invgβ€˜πΊ)β€˜π‘₯)(+gβ€˜πΊ)π‘Ž) ∈ β„Ž)
6436subgcl 18945 . . . . . . . . . . . . . 14 ((β„Ž ∈ (SubGrpβ€˜πΊ) ∧ π‘₯ ∈ β„Ž ∧ (((invgβ€˜πΊ)β€˜π‘₯)(+gβ€˜πΊ)π‘Ž) ∈ β„Ž) β†’ (π‘₯(+gβ€˜πΊ)(((invgβ€˜πΊ)β€˜π‘₯)(+gβ€˜πΊ)π‘Ž)) ∈ β„Ž)
6540, 41, 63, 64syl3anc 1372 . . . . . . . . . . . . 13 ((((((πœ‘ ∧ β„Ž ∈ (SubGrpβ€˜πΊ)) ∧ 𝑁 βŠ† β„Ž) ∧ π‘Ž ∈ 𝐡) ∧ π‘₯ ∈ β„Ž) ∧ ({π‘Ž} βŠ• 𝑁) = ({π‘₯} βŠ• 𝑁)) β†’ (π‘₯(+gβ€˜πΊ)(((invgβ€˜πΊ)β€˜π‘₯)(+gβ€˜πΊ)π‘Ž)) ∈ β„Ž)
6639, 65eqeltrrd 2839 . . . . . . . . . . . 12 ((((((πœ‘ ∧ β„Ž ∈ (SubGrpβ€˜πΊ)) ∧ 𝑁 βŠ† β„Ž) ∧ π‘Ž ∈ 𝐡) ∧ π‘₯ ∈ β„Ž) ∧ ({π‘Ž} βŠ• 𝑁) = ({π‘₯} βŠ• 𝑁)) β†’ π‘Ž ∈ β„Ž)
6766adantllr 718 . . . . . . . . . . 11 (((((((πœ‘ ∧ β„Ž ∈ (SubGrpβ€˜πΊ)) ∧ 𝑁 βŠ† β„Ž) ∧ π‘Ž ∈ 𝐡) ∧ ({π‘Ž} βŠ• 𝑁) ∈ ran (π‘₯ ∈ β„Ž ↦ ({π‘₯} βŠ• 𝑁))) ∧ π‘₯ ∈ β„Ž) ∧ ({π‘Ž} βŠ• 𝑁) = ({π‘₯} βŠ• 𝑁)) β†’ π‘Ž ∈ β„Ž)
68 eqid 2737 . . . . . . . . . . . . . 14 (π‘₯ ∈ β„Ž ↦ ({π‘₯} βŠ• 𝑁)) = (π‘₯ ∈ β„Ž ↦ ({π‘₯} βŠ• 𝑁))
69 ovex 7395 . . . . . . . . . . . . . 14 ({π‘₯} βŠ• 𝑁) ∈ V
7068, 69elrnmpti 5920 . . . . . . . . . . . . 13 (({π‘Ž} βŠ• 𝑁) ∈ ran (π‘₯ ∈ β„Ž ↦ ({π‘₯} βŠ• 𝑁)) ↔ βˆƒπ‘₯ ∈ β„Ž ({π‘Ž} βŠ• 𝑁) = ({π‘₯} βŠ• 𝑁))
7170biimpi 215 . . . . . . . . . . . 12 (({π‘Ž} βŠ• 𝑁) ∈ ran (π‘₯ ∈ β„Ž ↦ ({π‘₯} βŠ• 𝑁)) β†’ βˆƒπ‘₯ ∈ β„Ž ({π‘Ž} βŠ• 𝑁) = ({π‘₯} βŠ• 𝑁))
7271adantl 483 . . . . . . . . . . 11 (((((πœ‘ ∧ β„Ž ∈ (SubGrpβ€˜πΊ)) ∧ 𝑁 βŠ† β„Ž) ∧ π‘Ž ∈ 𝐡) ∧ ({π‘Ž} βŠ• 𝑁) ∈ ran (π‘₯ ∈ β„Ž ↦ ({π‘₯} βŠ• 𝑁))) β†’ βˆƒπ‘₯ ∈ β„Ž ({π‘Ž} βŠ• 𝑁) = ({π‘₯} βŠ• 𝑁))
7323, 67, 72r19.29af 3254 . . . . . . . . . 10 (((((πœ‘ ∧ β„Ž ∈ (SubGrpβ€˜πΊ)) ∧ 𝑁 βŠ† β„Ž) ∧ π‘Ž ∈ 𝐡) ∧ ({π‘Ž} βŠ• 𝑁) ∈ ran (π‘₯ ∈ β„Ž ↦ ({π‘₯} βŠ• 𝑁))) β†’ π‘Ž ∈ β„Ž)
74 simpr 486 . . . . . . . . . . 11 (((((πœ‘ ∧ β„Ž ∈ (SubGrpβ€˜πΊ)) ∧ 𝑁 βŠ† β„Ž) ∧ π‘Ž ∈ 𝐡) ∧ π‘Ž ∈ β„Ž) β†’ π‘Ž ∈ β„Ž)
75 ovexd 7397 . . . . . . . . . . 11 (((((πœ‘ ∧ β„Ž ∈ (SubGrpβ€˜πΊ)) ∧ 𝑁 βŠ† β„Ž) ∧ π‘Ž ∈ 𝐡) ∧ π‘Ž ∈ β„Ž) β†’ ({π‘Ž} βŠ• 𝑁) ∈ V)
76 sneq 4601 . . . . . . . . . . . . . 14 (π‘₯ = π‘Ž β†’ {π‘₯} = {π‘Ž})
7776oveq1d 7377 . . . . . . . . . . . . 13 (π‘₯ = π‘Ž β†’ ({π‘₯} βŠ• 𝑁) = ({π‘Ž} βŠ• 𝑁))
7877eqcomd 2743 . . . . . . . . . . . 12 (π‘₯ = π‘Ž β†’ ({π‘Ž} βŠ• 𝑁) = ({π‘₯} βŠ• 𝑁))
7978adantl 483 . . . . . . . . . . 11 ((((((πœ‘ ∧ β„Ž ∈ (SubGrpβ€˜πΊ)) ∧ 𝑁 βŠ† β„Ž) ∧ π‘Ž ∈ 𝐡) ∧ π‘Ž ∈ β„Ž) ∧ π‘₯ = π‘Ž) β†’ ({π‘Ž} βŠ• 𝑁) = ({π‘₯} βŠ• 𝑁))
8068, 74, 75, 79elrnmptdv 5922 . . . . . . . . . 10 (((((πœ‘ ∧ β„Ž ∈ (SubGrpβ€˜πΊ)) ∧ 𝑁 βŠ† β„Ž) ∧ π‘Ž ∈ 𝐡) ∧ π‘Ž ∈ β„Ž) β†’ ({π‘Ž} βŠ• 𝑁) ∈ ran (π‘₯ ∈ β„Ž ↦ ({π‘₯} βŠ• 𝑁)))
8173, 80impbida 800 . . . . . . . . 9 ((((πœ‘ ∧ β„Ž ∈ (SubGrpβ€˜πΊ)) ∧ 𝑁 βŠ† β„Ž) ∧ π‘Ž ∈ 𝐡) β†’ (({π‘Ž} βŠ• 𝑁) ∈ ran (π‘₯ ∈ β„Ž ↦ ({π‘₯} βŠ• 𝑁)) ↔ π‘Ž ∈ β„Ž))
8281rabbidva 3417 . . . . . . . 8 (((πœ‘ ∧ β„Ž ∈ (SubGrpβ€˜πΊ)) ∧ 𝑁 βŠ† β„Ž) β†’ {π‘Ž ∈ 𝐡 ∣ ({π‘Ž} βŠ• 𝑁) ∈ ran (π‘₯ ∈ β„Ž ↦ ({π‘₯} βŠ• 𝑁))} = {π‘Ž ∈ 𝐡 ∣ π‘Ž ∈ β„Ž})
8330adantl 483 . . . . . . . . . 10 ((πœ‘ ∧ β„Ž ∈ (SubGrpβ€˜πΊ)) β†’ β„Ž βŠ† 𝐡)
84 dfss7 4205 . . . . . . . . . 10 (β„Ž βŠ† 𝐡 ↔ {π‘Ž ∈ 𝐡 ∣ π‘Ž ∈ β„Ž} = β„Ž)
8583, 84sylib 217 . . . . . . . . 9 ((πœ‘ ∧ β„Ž ∈ (SubGrpβ€˜πΊ)) β†’ {π‘Ž ∈ 𝐡 ∣ π‘Ž ∈ β„Ž} = β„Ž)
8685adantr 482 . . . . . . . 8 (((πœ‘ ∧ β„Ž ∈ (SubGrpβ€˜πΊ)) ∧ 𝑁 βŠ† β„Ž) β†’ {π‘Ž ∈ 𝐡 ∣ π‘Ž ∈ β„Ž} = β„Ž)
8782, 86eqtr2d 2778 . . . . . . 7 (((πœ‘ ∧ β„Ž ∈ (SubGrpβ€˜πΊ)) ∧ 𝑁 βŠ† β„Ž) β†’ β„Ž = {π‘Ž ∈ 𝐡 ∣ ({π‘Ž} βŠ• 𝑁) ∈ ran (π‘₯ ∈ β„Ž ↦ ({π‘₯} βŠ• 𝑁))})
8814, 18, 87rspcedvd 3586 . . . . . 6 (((πœ‘ ∧ β„Ž ∈ (SubGrpβ€˜πΊ)) ∧ 𝑁 βŠ† β„Ž) β†’ βˆƒπ‘“ ∈ 𝑇 β„Ž = {π‘Ž ∈ 𝐡 ∣ ({π‘Ž} βŠ• 𝑁) ∈ 𝑓})
8988anasss 468 . . . . 5 ((πœ‘ ∧ (β„Ž ∈ (SubGrpβ€˜πΊ) ∧ 𝑁 βŠ† β„Ž)) β†’ βˆƒπ‘“ ∈ 𝑇 β„Ž = {π‘Ž ∈ 𝐡 ∣ ({π‘Ž} βŠ• 𝑁) ∈ 𝑓})
9013adantr 482 . . . . . . . . . 10 ((πœ‘ ∧ 𝑓 ∈ 𝑇) β†’ 𝑁 ∈ (NrmSGrpβ€˜πΊ))
917eleq2i 2830 . . . . . . . . . . . 12 (𝑓 ∈ 𝑇 ↔ 𝑓 ∈ (SubGrpβ€˜π‘„))
9291biimpi 215 . . . . . . . . . . 11 (𝑓 ∈ 𝑇 β†’ 𝑓 ∈ (SubGrpβ€˜π‘„))
9392adantl 483 . . . . . . . . . 10 ((πœ‘ ∧ 𝑓 ∈ 𝑇) β†’ 𝑓 ∈ (SubGrpβ€˜π‘„))
946, 10, 11, 90, 93nsgmgclem 32229 . . . . . . . . 9 ((πœ‘ ∧ 𝑓 ∈ 𝑇) β†’ {π‘Ž ∈ 𝐡 ∣ ({π‘Ž} βŠ• 𝑁) ∈ 𝑓} ∈ (SubGrpβ€˜πΊ))
9594adantr 482 . . . . . . . 8 (((πœ‘ ∧ 𝑓 ∈ 𝑇) ∧ β„Ž = {π‘Ž ∈ 𝐡 ∣ ({π‘Ž} βŠ• 𝑁) ∈ 𝑓}) β†’ {π‘Ž ∈ 𝐡 ∣ ({π‘Ž} βŠ• 𝑁) ∈ 𝑓} ∈ (SubGrpβ€˜πΊ))
96 eleq1 2826 . . . . . . . . 9 (β„Ž = {π‘Ž ∈ 𝐡 ∣ ({π‘Ž} βŠ• 𝑁) ∈ 𝑓} β†’ (β„Ž ∈ (SubGrpβ€˜πΊ) ↔ {π‘Ž ∈ 𝐡 ∣ ({π‘Ž} βŠ• 𝑁) ∈ 𝑓} ∈ (SubGrpβ€˜πΊ)))
9796adantl 483 . . . . . . . 8 (((πœ‘ ∧ 𝑓 ∈ 𝑇) ∧ β„Ž = {π‘Ž ∈ 𝐡 ∣ ({π‘Ž} βŠ• 𝑁) ∈ 𝑓}) β†’ (β„Ž ∈ (SubGrpβ€˜πΊ) ↔ {π‘Ž ∈ 𝐡 ∣ ({π‘Ž} βŠ• 𝑁) ∈ 𝑓} ∈ (SubGrpβ€˜πΊ)))
9895, 97mpbird 257 . . . . . . 7 (((πœ‘ ∧ 𝑓 ∈ 𝑇) ∧ β„Ž = {π‘Ž ∈ 𝐡 ∣ ({π‘Ž} βŠ• 𝑁) ∈ 𝑓}) β†’ β„Ž ∈ (SubGrpβ€˜πΊ))
9944adantr 482 . . . . . . . . . 10 ((πœ‘ ∧ 𝑓 ∈ 𝑇) β†’ 𝑁 βŠ† 𝐡)
10025ad2antrr 725 . . . . . . . . . . . 12 (((πœ‘ ∧ 𝑓 ∈ 𝑇) ∧ π‘Ž ∈ 𝑁) β†’ 𝑁 ∈ (SubGrpβ€˜πΊ))
101 simpr 486 . . . . . . . . . . . 12 (((πœ‘ ∧ 𝑓 ∈ 𝑇) ∧ π‘Ž ∈ 𝑁) β†’ π‘Ž ∈ 𝑁)
10211grplsmid 32225 . . . . . . . . . . . 12 ((𝑁 ∈ (SubGrpβ€˜πΊ) ∧ π‘Ž ∈ 𝑁) β†’ ({π‘Ž} βŠ• 𝑁) = 𝑁)
103100, 101, 102syl2anc 585 . . . . . . . . . . 11 (((πœ‘ ∧ 𝑓 ∈ 𝑇) ∧ π‘Ž ∈ 𝑁) β†’ ({π‘Ž} βŠ• 𝑁) = 𝑁)
10410nsgqus0 32228 . . . . . . . . . . . . 13 ((𝑁 ∈ (NrmSGrpβ€˜πΊ) ∧ 𝑓 ∈ (SubGrpβ€˜π‘„)) β†’ 𝑁 ∈ 𝑓)
10590, 93, 104syl2anc 585 . . . . . . . . . . . 12 ((πœ‘ ∧ 𝑓 ∈ 𝑇) β†’ 𝑁 ∈ 𝑓)
106105adantr 482 . . . . . . . . . . 11 (((πœ‘ ∧ 𝑓 ∈ 𝑇) ∧ π‘Ž ∈ 𝑁) β†’ 𝑁 ∈ 𝑓)
107103, 106eqeltrd 2838 . . . . . . . . . 10 (((πœ‘ ∧ 𝑓 ∈ 𝑇) ∧ π‘Ž ∈ 𝑁) β†’ ({π‘Ž} βŠ• 𝑁) ∈ 𝑓)
10899, 107ssrabdv 4036 . . . . . . . . 9 ((πœ‘ ∧ 𝑓 ∈ 𝑇) β†’ 𝑁 βŠ† {π‘Ž ∈ 𝐡 ∣ ({π‘Ž} βŠ• 𝑁) ∈ 𝑓})
109108adantr 482 . . . . . . . 8 (((πœ‘ ∧ 𝑓 ∈ 𝑇) ∧ β„Ž = {π‘Ž ∈ 𝐡 ∣ ({π‘Ž} βŠ• 𝑁) ∈ 𝑓}) β†’ 𝑁 βŠ† {π‘Ž ∈ 𝐡 ∣ ({π‘Ž} βŠ• 𝑁) ∈ 𝑓})
110 simpr 486 . . . . . . . 8 (((πœ‘ ∧ 𝑓 ∈ 𝑇) ∧ β„Ž = {π‘Ž ∈ 𝐡 ∣ ({π‘Ž} βŠ• 𝑁) ∈ 𝑓}) β†’ β„Ž = {π‘Ž ∈ 𝐡 ∣ ({π‘Ž} βŠ• 𝑁) ∈ 𝑓})
111109, 110sseqtrrd 3990 . . . . . . 7 (((πœ‘ ∧ 𝑓 ∈ 𝑇) ∧ β„Ž = {π‘Ž ∈ 𝐡 ∣ ({π‘Ž} βŠ• 𝑁) ∈ 𝑓}) β†’ 𝑁 βŠ† β„Ž)
11298, 111jca 513 . . . . . 6 (((πœ‘ ∧ 𝑓 ∈ 𝑇) ∧ β„Ž = {π‘Ž ∈ 𝐡 ∣ ({π‘Ž} βŠ• 𝑁) ∈ 𝑓}) β†’ (β„Ž ∈ (SubGrpβ€˜πΊ) ∧ 𝑁 βŠ† β„Ž))
113112r19.29an 3156 . . . . 5 ((πœ‘ ∧ βˆƒπ‘“ ∈ 𝑇 β„Ž = {π‘Ž ∈ 𝐡 ∣ ({π‘Ž} βŠ• 𝑁) ∈ 𝑓}) β†’ (β„Ž ∈ (SubGrpβ€˜πΊ) ∧ 𝑁 βŠ† β„Ž))
11489, 113impbida 800 . . . 4 (πœ‘ β†’ ((β„Ž ∈ (SubGrpβ€˜πΊ) ∧ 𝑁 βŠ† β„Ž) ↔ βˆƒπ‘“ ∈ 𝑇 β„Ž = {π‘Ž ∈ 𝐡 ∣ ({π‘Ž} βŠ• 𝑁) ∈ 𝑓}))
1155, 114bitrid 283 . . 3 (πœ‘ β†’ (β„Ž ∈ 𝑆 ↔ βˆƒπ‘“ ∈ 𝑇 β„Ž = {π‘Ž ∈ 𝐡 ∣ ({π‘Ž} βŠ• 𝑁) ∈ 𝑓}))
1163, 115bitr4id 290 . 2 (πœ‘ β†’ (β„Ž ∈ ran 𝐹 ↔ β„Ž ∈ 𝑆))
117116eqrdv 2735 1 (πœ‘ β†’ ran 𝐹 = 𝑆)
Colors of variables: wff setvar class
Syntax hints:   β†’ wi 4   ↔ wb 205   ∧ wa 397   ∧ w3a 1088   = wceq 1542   ∈ wcel 2107  βˆƒwrex 3074  {crab 3410  Vcvv 3448   βŠ† wss 3915  {csn 4591   class class class wbr 5110   ↦ cmpt 5193  ran crn 5639  β€˜cfv 6501  (class class class)co 7362   Er wer 8652  [cec 8653  Basecbs 17090  +gcplusg 17140  lecple 17147   /s cqus 17394  toInccipo 18423  Grpcgrp 18755  invgcminusg 18756  SubGrpcsubg 18929  NrmSGrpcnsg 18930   ~QG cqg 18931  LSSumclsm 19423
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2708  ax-rep 5247  ax-sep 5261  ax-nul 5268  ax-pow 5325  ax-pr 5389  ax-un 7677  ax-cnex 11114  ax-resscn 11115  ax-1cn 11116  ax-icn 11117  ax-addcl 11118  ax-addrcl 11119  ax-mulcl 11120  ax-mulrcl 11121  ax-mulcom 11122  ax-addass 11123  ax-mulass 11124  ax-distr 11125  ax-i2m1 11126  ax-1ne0 11127  ax-1rid 11128  ax-rnegex 11129  ax-rrecex 11130  ax-cnre 11131  ax-pre-lttri 11132  ax-pre-lttrn 11133  ax-pre-ltadd 11134  ax-pre-mulgt0 11135
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3or 1089  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-nf 1787  df-sb 2069  df-mo 2539  df-eu 2568  df-clab 2715  df-cleq 2729  df-clel 2815  df-nfc 2890  df-ne 2945  df-nel 3051  df-ral 3066  df-rex 3075  df-rmo 3356  df-reu 3357  df-rab 3411  df-v 3450  df-sbc 3745  df-csb 3861  df-dif 3918  df-un 3920  df-in 3922  df-ss 3932  df-pss 3934  df-nul 4288  df-if 4492  df-pw 4567  df-sn 4592  df-pr 4594  df-tp 4596  df-op 4598  df-uni 4871  df-iun 4961  df-br 5111  df-opab 5173  df-mpt 5194  df-tr 5228  df-id 5536  df-eprel 5542  df-po 5550  df-so 5551  df-fr 5593  df-we 5595  df-xp 5644  df-rel 5645  df-cnv 5646  df-co 5647  df-dm 5648  df-rn 5649  df-res 5650  df-ima 5651  df-pred 6258  df-ord 6325  df-on 6326  df-lim 6327  df-suc 6328  df-iota 6453  df-fun 6503  df-fn 6504  df-f 6505  df-f1 6506  df-fo 6507  df-f1o 6508  df-fv 6509  df-riota 7318  df-ov 7365  df-oprab 7366  df-mpo 7367  df-om 7808  df-1st 7926  df-2nd 7927  df-tpos 8162  df-frecs 8217  df-wrecs 8248  df-recs 8322  df-rdg 8361  df-1o 8417  df-er 8655  df-ec 8657  df-qs 8661  df-en 8891  df-dom 8892  df-sdom 8893  df-fin 8894  df-sup 9385  df-inf 9386  df-pnf 11198  df-mnf 11199  df-xr 11200  df-ltxr 11201  df-le 11202  df-sub 11394  df-neg 11395  df-nn 12161  df-2 12223  df-3 12224  df-4 12225  df-5 12226  df-6 12227  df-7 12228  df-8 12229  df-9 12230  df-n0 12421  df-z 12507  df-dec 12626  df-uz 12771  df-fz 13432  df-struct 17026  df-sets 17043  df-slot 17061  df-ndx 17073  df-base 17091  df-ress 17120  df-plusg 17153  df-mulr 17154  df-sca 17156  df-vsca 17157  df-ip 17158  df-tset 17159  df-ple 17160  df-ds 17162  df-0g 17330  df-imas 17397  df-qus 17398  df-mgm 18504  df-sgrp 18553  df-mnd 18564  df-submnd 18609  df-grp 18758  df-minusg 18759  df-subg 18932  df-nsg 18933  df-eqg 18934  df-oppg 19131  df-lsm 19425
This theorem is referenced by:  nsgqusf1o  32234
  Copyright terms: Public domain W3C validator