Step |
Hyp |
Ref |
Expression |
1 |
|
pgpfac1.k |
⊢ 𝐾 = ( mrCls ‘ ( SubGrp ‘ 𝐺 ) ) |
2 |
|
pgpfac1.s |
⊢ 𝑆 = ( 𝐾 ‘ { 𝐴 } ) |
3 |
|
pgpfac1.b |
⊢ 𝐵 = ( Base ‘ 𝐺 ) |
4 |
|
pgpfac1.o |
⊢ 𝑂 = ( od ‘ 𝐺 ) |
5 |
|
pgpfac1.e |
⊢ 𝐸 = ( gEx ‘ 𝐺 ) |
6 |
|
pgpfac1.z |
⊢ 0 = ( 0g ‘ 𝐺 ) |
7 |
|
pgpfac1.l |
⊢ ⊕ = ( LSSum ‘ 𝐺 ) |
8 |
|
pgpfac1.p |
⊢ ( 𝜑 → 𝑃 pGrp 𝐺 ) |
9 |
|
pgpfac1.g |
⊢ ( 𝜑 → 𝐺 ∈ Abel ) |
10 |
|
pgpfac1.n |
⊢ ( 𝜑 → 𝐵 ∈ Fin ) |
11 |
|
pgpfac1.oe |
⊢ ( 𝜑 → ( 𝑂 ‘ 𝐴 ) = 𝐸 ) |
12 |
|
pgpfac1.u |
⊢ ( 𝜑 → 𝑈 ∈ ( SubGrp ‘ 𝐺 ) ) |
13 |
|
pgpfac1.au |
⊢ ( 𝜑 → 𝐴 ∈ 𝑈 ) |
14 |
|
pgpfac1.3 |
⊢ ( 𝜑 → ∀ 𝑠 ∈ ( SubGrp ‘ 𝐺 ) ( ( 𝑠 ⊊ 𝑈 ∧ 𝐴 ∈ 𝑠 ) → ∃ 𝑡 ∈ ( SubGrp ‘ 𝐺 ) ( ( 𝑆 ∩ 𝑡 ) = { 0 } ∧ ( 𝑆 ⊕ 𝑡 ) = 𝑠 ) ) ) |
15 |
|
pwfi |
⊢ ( 𝐵 ∈ Fin ↔ 𝒫 𝐵 ∈ Fin ) |
16 |
10 15
|
sylib |
⊢ ( 𝜑 → 𝒫 𝐵 ∈ Fin ) |
17 |
16
|
adantr |
⊢ ( ( 𝜑 ∧ 𝑆 ⊊ 𝑈 ) → 𝒫 𝐵 ∈ Fin ) |
18 |
3
|
subgss |
⊢ ( 𝑣 ∈ ( SubGrp ‘ 𝐺 ) → 𝑣 ⊆ 𝐵 ) |
19 |
18
|
3ad2ant2 |
⊢ ( ( ( 𝜑 ∧ 𝑆 ⊊ 𝑈 ) ∧ 𝑣 ∈ ( SubGrp ‘ 𝐺 ) ∧ ( 𝑣 ⊊ 𝑈 ∧ 𝐴 ∈ 𝑣 ) ) → 𝑣 ⊆ 𝐵 ) |
20 |
|
velpw |
⊢ ( 𝑣 ∈ 𝒫 𝐵 ↔ 𝑣 ⊆ 𝐵 ) |
21 |
19 20
|
sylibr |
⊢ ( ( ( 𝜑 ∧ 𝑆 ⊊ 𝑈 ) ∧ 𝑣 ∈ ( SubGrp ‘ 𝐺 ) ∧ ( 𝑣 ⊊ 𝑈 ∧ 𝐴 ∈ 𝑣 ) ) → 𝑣 ∈ 𝒫 𝐵 ) |
22 |
21
|
rabssdv |
⊢ ( ( 𝜑 ∧ 𝑆 ⊊ 𝑈 ) → { 𝑣 ∈ ( SubGrp ‘ 𝐺 ) ∣ ( 𝑣 ⊊ 𝑈 ∧ 𝐴 ∈ 𝑣 ) } ⊆ 𝒫 𝐵 ) |
23 |
17 22
|
ssfid |
⊢ ( ( 𝜑 ∧ 𝑆 ⊊ 𝑈 ) → { 𝑣 ∈ ( SubGrp ‘ 𝐺 ) ∣ ( 𝑣 ⊊ 𝑈 ∧ 𝐴 ∈ 𝑣 ) } ∈ Fin ) |
24 |
|
finnum |
⊢ ( { 𝑣 ∈ ( SubGrp ‘ 𝐺 ) ∣ ( 𝑣 ⊊ 𝑈 ∧ 𝐴 ∈ 𝑣 ) } ∈ Fin → { 𝑣 ∈ ( SubGrp ‘ 𝐺 ) ∣ ( 𝑣 ⊊ 𝑈 ∧ 𝐴 ∈ 𝑣 ) } ∈ dom card ) |
25 |
23 24
|
syl |
⊢ ( ( 𝜑 ∧ 𝑆 ⊊ 𝑈 ) → { 𝑣 ∈ ( SubGrp ‘ 𝐺 ) ∣ ( 𝑣 ⊊ 𝑈 ∧ 𝐴 ∈ 𝑣 ) } ∈ dom card ) |
26 |
|
ablgrp |
⊢ ( 𝐺 ∈ Abel → 𝐺 ∈ Grp ) |
27 |
9 26
|
syl |
⊢ ( 𝜑 → 𝐺 ∈ Grp ) |
28 |
3
|
subgacs |
⊢ ( 𝐺 ∈ Grp → ( SubGrp ‘ 𝐺 ) ∈ ( ACS ‘ 𝐵 ) ) |
29 |
|
acsmre |
⊢ ( ( SubGrp ‘ 𝐺 ) ∈ ( ACS ‘ 𝐵 ) → ( SubGrp ‘ 𝐺 ) ∈ ( Moore ‘ 𝐵 ) ) |
30 |
27 28 29
|
3syl |
⊢ ( 𝜑 → ( SubGrp ‘ 𝐺 ) ∈ ( Moore ‘ 𝐵 ) ) |
31 |
3
|
subgss |
⊢ ( 𝑈 ∈ ( SubGrp ‘ 𝐺 ) → 𝑈 ⊆ 𝐵 ) |
32 |
12 31
|
syl |
⊢ ( 𝜑 → 𝑈 ⊆ 𝐵 ) |
33 |
32 13
|
sseldd |
⊢ ( 𝜑 → 𝐴 ∈ 𝐵 ) |
34 |
1
|
mrcsncl |
⊢ ( ( ( SubGrp ‘ 𝐺 ) ∈ ( Moore ‘ 𝐵 ) ∧ 𝐴 ∈ 𝐵 ) → ( 𝐾 ‘ { 𝐴 } ) ∈ ( SubGrp ‘ 𝐺 ) ) |
35 |
30 33 34
|
syl2anc |
⊢ ( 𝜑 → ( 𝐾 ‘ { 𝐴 } ) ∈ ( SubGrp ‘ 𝐺 ) ) |
36 |
2 35
|
eqeltrid |
⊢ ( 𝜑 → 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ) |
37 |
36
|
adantr |
⊢ ( ( 𝜑 ∧ 𝑆 ⊊ 𝑈 ) → 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ) |
38 |
|
simpr |
⊢ ( ( 𝜑 ∧ 𝑆 ⊊ 𝑈 ) → 𝑆 ⊊ 𝑈 ) |
39 |
13
|
snssd |
⊢ ( 𝜑 → { 𝐴 } ⊆ 𝑈 ) |
40 |
39 32
|
sstrd |
⊢ ( 𝜑 → { 𝐴 } ⊆ 𝐵 ) |
41 |
30 1 40
|
mrcssidd |
⊢ ( 𝜑 → { 𝐴 } ⊆ ( 𝐾 ‘ { 𝐴 } ) ) |
42 |
41 2
|
sseqtrrdi |
⊢ ( 𝜑 → { 𝐴 } ⊆ 𝑆 ) |
43 |
|
snssg |
⊢ ( 𝐴 ∈ 𝐵 → ( 𝐴 ∈ 𝑆 ↔ { 𝐴 } ⊆ 𝑆 ) ) |
44 |
33 43
|
syl |
⊢ ( 𝜑 → ( 𝐴 ∈ 𝑆 ↔ { 𝐴 } ⊆ 𝑆 ) ) |
45 |
42 44
|
mpbird |
⊢ ( 𝜑 → 𝐴 ∈ 𝑆 ) |
46 |
45
|
adantr |
⊢ ( ( 𝜑 ∧ 𝑆 ⊊ 𝑈 ) → 𝐴 ∈ 𝑆 ) |
47 |
|
psseq1 |
⊢ ( 𝑣 = 𝑆 → ( 𝑣 ⊊ 𝑈 ↔ 𝑆 ⊊ 𝑈 ) ) |
48 |
|
eleq2 |
⊢ ( 𝑣 = 𝑆 → ( 𝐴 ∈ 𝑣 ↔ 𝐴 ∈ 𝑆 ) ) |
49 |
47 48
|
anbi12d |
⊢ ( 𝑣 = 𝑆 → ( ( 𝑣 ⊊ 𝑈 ∧ 𝐴 ∈ 𝑣 ) ↔ ( 𝑆 ⊊ 𝑈 ∧ 𝐴 ∈ 𝑆 ) ) ) |
50 |
49
|
rspcev |
⊢ ( ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ ( 𝑆 ⊊ 𝑈 ∧ 𝐴 ∈ 𝑆 ) ) → ∃ 𝑣 ∈ ( SubGrp ‘ 𝐺 ) ( 𝑣 ⊊ 𝑈 ∧ 𝐴 ∈ 𝑣 ) ) |
51 |
37 38 46 50
|
syl12anc |
⊢ ( ( 𝜑 ∧ 𝑆 ⊊ 𝑈 ) → ∃ 𝑣 ∈ ( SubGrp ‘ 𝐺 ) ( 𝑣 ⊊ 𝑈 ∧ 𝐴 ∈ 𝑣 ) ) |
52 |
|
rabn0 |
⊢ ( { 𝑣 ∈ ( SubGrp ‘ 𝐺 ) ∣ ( 𝑣 ⊊ 𝑈 ∧ 𝐴 ∈ 𝑣 ) } ≠ ∅ ↔ ∃ 𝑣 ∈ ( SubGrp ‘ 𝐺 ) ( 𝑣 ⊊ 𝑈 ∧ 𝐴 ∈ 𝑣 ) ) |
53 |
51 52
|
sylibr |
⊢ ( ( 𝜑 ∧ 𝑆 ⊊ 𝑈 ) → { 𝑣 ∈ ( SubGrp ‘ 𝐺 ) ∣ ( 𝑣 ⊊ 𝑈 ∧ 𝐴 ∈ 𝑣 ) } ≠ ∅ ) |
54 |
|
simpr1 |
⊢ ( ( ( 𝜑 ∧ 𝑆 ⊊ 𝑈 ) ∧ ( 𝑢 ⊆ { 𝑣 ∈ ( SubGrp ‘ 𝐺 ) ∣ ( 𝑣 ⊊ 𝑈 ∧ 𝐴 ∈ 𝑣 ) } ∧ 𝑢 ≠ ∅ ∧ [⊊] Or 𝑢 ) ) → 𝑢 ⊆ { 𝑣 ∈ ( SubGrp ‘ 𝐺 ) ∣ ( 𝑣 ⊊ 𝑈 ∧ 𝐴 ∈ 𝑣 ) } ) |
55 |
|
simpr2 |
⊢ ( ( ( 𝜑 ∧ 𝑆 ⊊ 𝑈 ) ∧ ( 𝑢 ⊆ { 𝑣 ∈ ( SubGrp ‘ 𝐺 ) ∣ ( 𝑣 ⊊ 𝑈 ∧ 𝐴 ∈ 𝑣 ) } ∧ 𝑢 ≠ ∅ ∧ [⊊] Or 𝑢 ) ) → 𝑢 ≠ ∅ ) |
56 |
23
|
adantr |
⊢ ( ( ( 𝜑 ∧ 𝑆 ⊊ 𝑈 ) ∧ ( 𝑢 ⊆ { 𝑣 ∈ ( SubGrp ‘ 𝐺 ) ∣ ( 𝑣 ⊊ 𝑈 ∧ 𝐴 ∈ 𝑣 ) } ∧ 𝑢 ≠ ∅ ∧ [⊊] Or 𝑢 ) ) → { 𝑣 ∈ ( SubGrp ‘ 𝐺 ) ∣ ( 𝑣 ⊊ 𝑈 ∧ 𝐴 ∈ 𝑣 ) } ∈ Fin ) |
57 |
56 54
|
ssfid |
⊢ ( ( ( 𝜑 ∧ 𝑆 ⊊ 𝑈 ) ∧ ( 𝑢 ⊆ { 𝑣 ∈ ( SubGrp ‘ 𝐺 ) ∣ ( 𝑣 ⊊ 𝑈 ∧ 𝐴 ∈ 𝑣 ) } ∧ 𝑢 ≠ ∅ ∧ [⊊] Or 𝑢 ) ) → 𝑢 ∈ Fin ) |
58 |
|
simpr3 |
⊢ ( ( ( 𝜑 ∧ 𝑆 ⊊ 𝑈 ) ∧ ( 𝑢 ⊆ { 𝑣 ∈ ( SubGrp ‘ 𝐺 ) ∣ ( 𝑣 ⊊ 𝑈 ∧ 𝐴 ∈ 𝑣 ) } ∧ 𝑢 ≠ ∅ ∧ [⊊] Or 𝑢 ) ) → [⊊] Or 𝑢 ) |
59 |
|
fin1a2lem10 |
⊢ ( ( 𝑢 ≠ ∅ ∧ 𝑢 ∈ Fin ∧ [⊊] Or 𝑢 ) → ∪ 𝑢 ∈ 𝑢 ) |
60 |
55 57 58 59
|
syl3anc |
⊢ ( ( ( 𝜑 ∧ 𝑆 ⊊ 𝑈 ) ∧ ( 𝑢 ⊆ { 𝑣 ∈ ( SubGrp ‘ 𝐺 ) ∣ ( 𝑣 ⊊ 𝑈 ∧ 𝐴 ∈ 𝑣 ) } ∧ 𝑢 ≠ ∅ ∧ [⊊] Or 𝑢 ) ) → ∪ 𝑢 ∈ 𝑢 ) |
61 |
54 60
|
sseldd |
⊢ ( ( ( 𝜑 ∧ 𝑆 ⊊ 𝑈 ) ∧ ( 𝑢 ⊆ { 𝑣 ∈ ( SubGrp ‘ 𝐺 ) ∣ ( 𝑣 ⊊ 𝑈 ∧ 𝐴 ∈ 𝑣 ) } ∧ 𝑢 ≠ ∅ ∧ [⊊] Or 𝑢 ) ) → ∪ 𝑢 ∈ { 𝑣 ∈ ( SubGrp ‘ 𝐺 ) ∣ ( 𝑣 ⊊ 𝑈 ∧ 𝐴 ∈ 𝑣 ) } ) |
62 |
61
|
ex |
⊢ ( ( 𝜑 ∧ 𝑆 ⊊ 𝑈 ) → ( ( 𝑢 ⊆ { 𝑣 ∈ ( SubGrp ‘ 𝐺 ) ∣ ( 𝑣 ⊊ 𝑈 ∧ 𝐴 ∈ 𝑣 ) } ∧ 𝑢 ≠ ∅ ∧ [⊊] Or 𝑢 ) → ∪ 𝑢 ∈ { 𝑣 ∈ ( SubGrp ‘ 𝐺 ) ∣ ( 𝑣 ⊊ 𝑈 ∧ 𝐴 ∈ 𝑣 ) } ) ) |
63 |
62
|
alrimiv |
⊢ ( ( 𝜑 ∧ 𝑆 ⊊ 𝑈 ) → ∀ 𝑢 ( ( 𝑢 ⊆ { 𝑣 ∈ ( SubGrp ‘ 𝐺 ) ∣ ( 𝑣 ⊊ 𝑈 ∧ 𝐴 ∈ 𝑣 ) } ∧ 𝑢 ≠ ∅ ∧ [⊊] Or 𝑢 ) → ∪ 𝑢 ∈ { 𝑣 ∈ ( SubGrp ‘ 𝐺 ) ∣ ( 𝑣 ⊊ 𝑈 ∧ 𝐴 ∈ 𝑣 ) } ) ) |
64 |
|
zornn0g |
⊢ ( ( { 𝑣 ∈ ( SubGrp ‘ 𝐺 ) ∣ ( 𝑣 ⊊ 𝑈 ∧ 𝐴 ∈ 𝑣 ) } ∈ dom card ∧ { 𝑣 ∈ ( SubGrp ‘ 𝐺 ) ∣ ( 𝑣 ⊊ 𝑈 ∧ 𝐴 ∈ 𝑣 ) } ≠ ∅ ∧ ∀ 𝑢 ( ( 𝑢 ⊆ { 𝑣 ∈ ( SubGrp ‘ 𝐺 ) ∣ ( 𝑣 ⊊ 𝑈 ∧ 𝐴 ∈ 𝑣 ) } ∧ 𝑢 ≠ ∅ ∧ [⊊] Or 𝑢 ) → ∪ 𝑢 ∈ { 𝑣 ∈ ( SubGrp ‘ 𝐺 ) ∣ ( 𝑣 ⊊ 𝑈 ∧ 𝐴 ∈ 𝑣 ) } ) ) → ∃ 𝑠 ∈ { 𝑣 ∈ ( SubGrp ‘ 𝐺 ) ∣ ( 𝑣 ⊊ 𝑈 ∧ 𝐴 ∈ 𝑣 ) } ∀ 𝑤 ∈ { 𝑣 ∈ ( SubGrp ‘ 𝐺 ) ∣ ( 𝑣 ⊊ 𝑈 ∧ 𝐴 ∈ 𝑣 ) } ¬ 𝑠 ⊊ 𝑤 ) |
65 |
25 53 63 64
|
syl3anc |
⊢ ( ( 𝜑 ∧ 𝑆 ⊊ 𝑈 ) → ∃ 𝑠 ∈ { 𝑣 ∈ ( SubGrp ‘ 𝐺 ) ∣ ( 𝑣 ⊊ 𝑈 ∧ 𝐴 ∈ 𝑣 ) } ∀ 𝑤 ∈ { 𝑣 ∈ ( SubGrp ‘ 𝐺 ) ∣ ( 𝑣 ⊊ 𝑈 ∧ 𝐴 ∈ 𝑣 ) } ¬ 𝑠 ⊊ 𝑤 ) |
66 |
|
psseq1 |
⊢ ( 𝑣 = 𝑤 → ( 𝑣 ⊊ 𝑈 ↔ 𝑤 ⊊ 𝑈 ) ) |
67 |
|
eleq2 |
⊢ ( 𝑣 = 𝑤 → ( 𝐴 ∈ 𝑣 ↔ 𝐴 ∈ 𝑤 ) ) |
68 |
66 67
|
anbi12d |
⊢ ( 𝑣 = 𝑤 → ( ( 𝑣 ⊊ 𝑈 ∧ 𝐴 ∈ 𝑣 ) ↔ ( 𝑤 ⊊ 𝑈 ∧ 𝐴 ∈ 𝑤 ) ) ) |
69 |
68
|
ralrab |
⊢ ( ∀ 𝑤 ∈ { 𝑣 ∈ ( SubGrp ‘ 𝐺 ) ∣ ( 𝑣 ⊊ 𝑈 ∧ 𝐴 ∈ 𝑣 ) } ¬ 𝑠 ⊊ 𝑤 ↔ ∀ 𝑤 ∈ ( SubGrp ‘ 𝐺 ) ( ( 𝑤 ⊊ 𝑈 ∧ 𝐴 ∈ 𝑤 ) → ¬ 𝑠 ⊊ 𝑤 ) ) |
70 |
69
|
rexbii |
⊢ ( ∃ 𝑠 ∈ { 𝑣 ∈ ( SubGrp ‘ 𝐺 ) ∣ ( 𝑣 ⊊ 𝑈 ∧ 𝐴 ∈ 𝑣 ) } ∀ 𝑤 ∈ { 𝑣 ∈ ( SubGrp ‘ 𝐺 ) ∣ ( 𝑣 ⊊ 𝑈 ∧ 𝐴 ∈ 𝑣 ) } ¬ 𝑠 ⊊ 𝑤 ↔ ∃ 𝑠 ∈ { 𝑣 ∈ ( SubGrp ‘ 𝐺 ) ∣ ( 𝑣 ⊊ 𝑈 ∧ 𝐴 ∈ 𝑣 ) } ∀ 𝑤 ∈ ( SubGrp ‘ 𝐺 ) ( ( 𝑤 ⊊ 𝑈 ∧ 𝐴 ∈ 𝑤 ) → ¬ 𝑠 ⊊ 𝑤 ) ) |
71 |
65 70
|
sylib |
⊢ ( ( 𝜑 ∧ 𝑆 ⊊ 𝑈 ) → ∃ 𝑠 ∈ { 𝑣 ∈ ( SubGrp ‘ 𝐺 ) ∣ ( 𝑣 ⊊ 𝑈 ∧ 𝐴 ∈ 𝑣 ) } ∀ 𝑤 ∈ ( SubGrp ‘ 𝐺 ) ( ( 𝑤 ⊊ 𝑈 ∧ 𝐴 ∈ 𝑤 ) → ¬ 𝑠 ⊊ 𝑤 ) ) |
72 |
71
|
ex |
⊢ ( 𝜑 → ( 𝑆 ⊊ 𝑈 → ∃ 𝑠 ∈ { 𝑣 ∈ ( SubGrp ‘ 𝐺 ) ∣ ( 𝑣 ⊊ 𝑈 ∧ 𝐴 ∈ 𝑣 ) } ∀ 𝑤 ∈ ( SubGrp ‘ 𝐺 ) ( ( 𝑤 ⊊ 𝑈 ∧ 𝐴 ∈ 𝑤 ) → ¬ 𝑠 ⊊ 𝑤 ) ) ) |
73 |
|
psseq1 |
⊢ ( 𝑣 = 𝑠 → ( 𝑣 ⊊ 𝑈 ↔ 𝑠 ⊊ 𝑈 ) ) |
74 |
|
eleq2 |
⊢ ( 𝑣 = 𝑠 → ( 𝐴 ∈ 𝑣 ↔ 𝐴 ∈ 𝑠 ) ) |
75 |
73 74
|
anbi12d |
⊢ ( 𝑣 = 𝑠 → ( ( 𝑣 ⊊ 𝑈 ∧ 𝐴 ∈ 𝑣 ) ↔ ( 𝑠 ⊊ 𝑈 ∧ 𝐴 ∈ 𝑠 ) ) ) |
76 |
75
|
ralrab |
⊢ ( ∀ 𝑠 ∈ { 𝑣 ∈ ( SubGrp ‘ 𝐺 ) ∣ ( 𝑣 ⊊ 𝑈 ∧ 𝐴 ∈ 𝑣 ) } ∃ 𝑡 ∈ ( SubGrp ‘ 𝐺 ) ( ( 𝑆 ∩ 𝑡 ) = { 0 } ∧ ( 𝑆 ⊕ 𝑡 ) = 𝑠 ) ↔ ∀ 𝑠 ∈ ( SubGrp ‘ 𝐺 ) ( ( 𝑠 ⊊ 𝑈 ∧ 𝐴 ∈ 𝑠 ) → ∃ 𝑡 ∈ ( SubGrp ‘ 𝐺 ) ( ( 𝑆 ∩ 𝑡 ) = { 0 } ∧ ( 𝑆 ⊕ 𝑡 ) = 𝑠 ) ) ) |
77 |
14 76
|
sylibr |
⊢ ( 𝜑 → ∀ 𝑠 ∈ { 𝑣 ∈ ( SubGrp ‘ 𝐺 ) ∣ ( 𝑣 ⊊ 𝑈 ∧ 𝐴 ∈ 𝑣 ) } ∃ 𝑡 ∈ ( SubGrp ‘ 𝐺 ) ( ( 𝑆 ∩ 𝑡 ) = { 0 } ∧ ( 𝑆 ⊕ 𝑡 ) = 𝑠 ) ) |
78 |
|
r19.29 |
⊢ ( ( ∀ 𝑠 ∈ { 𝑣 ∈ ( SubGrp ‘ 𝐺 ) ∣ ( 𝑣 ⊊ 𝑈 ∧ 𝐴 ∈ 𝑣 ) } ∃ 𝑡 ∈ ( SubGrp ‘ 𝐺 ) ( ( 𝑆 ∩ 𝑡 ) = { 0 } ∧ ( 𝑆 ⊕ 𝑡 ) = 𝑠 ) ∧ ∃ 𝑠 ∈ { 𝑣 ∈ ( SubGrp ‘ 𝐺 ) ∣ ( 𝑣 ⊊ 𝑈 ∧ 𝐴 ∈ 𝑣 ) } ∀ 𝑤 ∈ ( SubGrp ‘ 𝐺 ) ( ( 𝑤 ⊊ 𝑈 ∧ 𝐴 ∈ 𝑤 ) → ¬ 𝑠 ⊊ 𝑤 ) ) → ∃ 𝑠 ∈ { 𝑣 ∈ ( SubGrp ‘ 𝐺 ) ∣ ( 𝑣 ⊊ 𝑈 ∧ 𝐴 ∈ 𝑣 ) } ( ∃ 𝑡 ∈ ( SubGrp ‘ 𝐺 ) ( ( 𝑆 ∩ 𝑡 ) = { 0 } ∧ ( 𝑆 ⊕ 𝑡 ) = 𝑠 ) ∧ ∀ 𝑤 ∈ ( SubGrp ‘ 𝐺 ) ( ( 𝑤 ⊊ 𝑈 ∧ 𝐴 ∈ 𝑤 ) → ¬ 𝑠 ⊊ 𝑤 ) ) ) |
79 |
75
|
elrab |
⊢ ( 𝑠 ∈ { 𝑣 ∈ ( SubGrp ‘ 𝐺 ) ∣ ( 𝑣 ⊊ 𝑈 ∧ 𝐴 ∈ 𝑣 ) } ↔ ( 𝑠 ∈ ( SubGrp ‘ 𝐺 ) ∧ ( 𝑠 ⊊ 𝑈 ∧ 𝐴 ∈ 𝑠 ) ) ) |
80 |
|
ineq2 |
⊢ ( 𝑡 = 𝑣 → ( 𝑆 ∩ 𝑡 ) = ( 𝑆 ∩ 𝑣 ) ) |
81 |
80
|
eqeq1d |
⊢ ( 𝑡 = 𝑣 → ( ( 𝑆 ∩ 𝑡 ) = { 0 } ↔ ( 𝑆 ∩ 𝑣 ) = { 0 } ) ) |
82 |
|
oveq2 |
⊢ ( 𝑡 = 𝑣 → ( 𝑆 ⊕ 𝑡 ) = ( 𝑆 ⊕ 𝑣 ) ) |
83 |
82
|
eqeq1d |
⊢ ( 𝑡 = 𝑣 → ( ( 𝑆 ⊕ 𝑡 ) = 𝑠 ↔ ( 𝑆 ⊕ 𝑣 ) = 𝑠 ) ) |
84 |
81 83
|
anbi12d |
⊢ ( 𝑡 = 𝑣 → ( ( ( 𝑆 ∩ 𝑡 ) = { 0 } ∧ ( 𝑆 ⊕ 𝑡 ) = 𝑠 ) ↔ ( ( 𝑆 ∩ 𝑣 ) = { 0 } ∧ ( 𝑆 ⊕ 𝑣 ) = 𝑠 ) ) ) |
85 |
84
|
cbvrexvw |
⊢ ( ∃ 𝑡 ∈ ( SubGrp ‘ 𝐺 ) ( ( 𝑆 ∩ 𝑡 ) = { 0 } ∧ ( 𝑆 ⊕ 𝑡 ) = 𝑠 ) ↔ ∃ 𝑣 ∈ ( SubGrp ‘ 𝐺 ) ( ( 𝑆 ∩ 𝑣 ) = { 0 } ∧ ( 𝑆 ⊕ 𝑣 ) = 𝑠 ) ) |
86 |
|
simprrl |
⊢ ( ( 𝜑 ∧ ( 𝑠 ∈ ( SubGrp ‘ 𝐺 ) ∧ ( 𝑠 ⊊ 𝑈 ∧ 𝐴 ∈ 𝑠 ) ) ) → 𝑠 ⊊ 𝑈 ) |
87 |
86
|
ad2antrr |
⊢ ( ( ( ( 𝜑 ∧ ( 𝑠 ∈ ( SubGrp ‘ 𝐺 ) ∧ ( 𝑠 ⊊ 𝑈 ∧ 𝐴 ∈ 𝑠 ) ) ) ∧ 𝑣 ∈ ( SubGrp ‘ 𝐺 ) ) ∧ ( ( 𝑆 ∩ 𝑣 ) = { 0 } ∧ ( 𝑆 ⊕ 𝑣 ) = 𝑠 ∧ ∀ 𝑤 ∈ ( SubGrp ‘ 𝐺 ) ( ( 𝑤 ⊊ 𝑈 ∧ 𝐴 ∈ 𝑤 ) → ¬ 𝑠 ⊊ 𝑤 ) ) ) → 𝑠 ⊊ 𝑈 ) |
88 |
|
simpr2 |
⊢ ( ( ( ( 𝜑 ∧ ( 𝑠 ∈ ( SubGrp ‘ 𝐺 ) ∧ ( 𝑠 ⊊ 𝑈 ∧ 𝐴 ∈ 𝑠 ) ) ) ∧ 𝑣 ∈ ( SubGrp ‘ 𝐺 ) ) ∧ ( ( 𝑆 ∩ 𝑣 ) = { 0 } ∧ ( 𝑆 ⊕ 𝑣 ) = 𝑠 ∧ ∀ 𝑤 ∈ ( SubGrp ‘ 𝐺 ) ( ( 𝑤 ⊊ 𝑈 ∧ 𝐴 ∈ 𝑤 ) → ¬ 𝑠 ⊊ 𝑤 ) ) ) → ( 𝑆 ⊕ 𝑣 ) = 𝑠 ) |
89 |
88
|
psseq1d |
⊢ ( ( ( ( 𝜑 ∧ ( 𝑠 ∈ ( SubGrp ‘ 𝐺 ) ∧ ( 𝑠 ⊊ 𝑈 ∧ 𝐴 ∈ 𝑠 ) ) ) ∧ 𝑣 ∈ ( SubGrp ‘ 𝐺 ) ) ∧ ( ( 𝑆 ∩ 𝑣 ) = { 0 } ∧ ( 𝑆 ⊕ 𝑣 ) = 𝑠 ∧ ∀ 𝑤 ∈ ( SubGrp ‘ 𝐺 ) ( ( 𝑤 ⊊ 𝑈 ∧ 𝐴 ∈ 𝑤 ) → ¬ 𝑠 ⊊ 𝑤 ) ) ) → ( ( 𝑆 ⊕ 𝑣 ) ⊊ 𝑈 ↔ 𝑠 ⊊ 𝑈 ) ) |
90 |
87 89
|
mpbird |
⊢ ( ( ( ( 𝜑 ∧ ( 𝑠 ∈ ( SubGrp ‘ 𝐺 ) ∧ ( 𝑠 ⊊ 𝑈 ∧ 𝐴 ∈ 𝑠 ) ) ) ∧ 𝑣 ∈ ( SubGrp ‘ 𝐺 ) ) ∧ ( ( 𝑆 ∩ 𝑣 ) = { 0 } ∧ ( 𝑆 ⊕ 𝑣 ) = 𝑠 ∧ ∀ 𝑤 ∈ ( SubGrp ‘ 𝐺 ) ( ( 𝑤 ⊊ 𝑈 ∧ 𝐴 ∈ 𝑤 ) → ¬ 𝑠 ⊊ 𝑤 ) ) ) → ( 𝑆 ⊕ 𝑣 ) ⊊ 𝑈 ) |
91 |
|
pssdif |
⊢ ( ( 𝑆 ⊕ 𝑣 ) ⊊ 𝑈 → ( 𝑈 ∖ ( 𝑆 ⊕ 𝑣 ) ) ≠ ∅ ) |
92 |
|
n0 |
⊢ ( ( 𝑈 ∖ ( 𝑆 ⊕ 𝑣 ) ) ≠ ∅ ↔ ∃ 𝑏 𝑏 ∈ ( 𝑈 ∖ ( 𝑆 ⊕ 𝑣 ) ) ) |
93 |
91 92
|
sylib |
⊢ ( ( 𝑆 ⊕ 𝑣 ) ⊊ 𝑈 → ∃ 𝑏 𝑏 ∈ ( 𝑈 ∖ ( 𝑆 ⊕ 𝑣 ) ) ) |
94 |
90 93
|
syl |
⊢ ( ( ( ( 𝜑 ∧ ( 𝑠 ∈ ( SubGrp ‘ 𝐺 ) ∧ ( 𝑠 ⊊ 𝑈 ∧ 𝐴 ∈ 𝑠 ) ) ) ∧ 𝑣 ∈ ( SubGrp ‘ 𝐺 ) ) ∧ ( ( 𝑆 ∩ 𝑣 ) = { 0 } ∧ ( 𝑆 ⊕ 𝑣 ) = 𝑠 ∧ ∀ 𝑤 ∈ ( SubGrp ‘ 𝐺 ) ( ( 𝑤 ⊊ 𝑈 ∧ 𝐴 ∈ 𝑤 ) → ¬ 𝑠 ⊊ 𝑤 ) ) ) → ∃ 𝑏 𝑏 ∈ ( 𝑈 ∖ ( 𝑆 ⊕ 𝑣 ) ) ) |
95 |
8
|
ad3antrrr |
⊢ ( ( ( ( 𝜑 ∧ ( 𝑠 ∈ ( SubGrp ‘ 𝐺 ) ∧ ( 𝑠 ⊊ 𝑈 ∧ 𝐴 ∈ 𝑠 ) ) ) ∧ 𝑣 ∈ ( SubGrp ‘ 𝐺 ) ) ∧ ( ( ( 𝑆 ∩ 𝑣 ) = { 0 } ∧ ( 𝑆 ⊕ 𝑣 ) = 𝑠 ∧ ∀ 𝑤 ∈ ( SubGrp ‘ 𝐺 ) ( ( 𝑤 ⊊ 𝑈 ∧ 𝐴 ∈ 𝑤 ) → ¬ 𝑠 ⊊ 𝑤 ) ) ∧ 𝑏 ∈ ( 𝑈 ∖ ( 𝑆 ⊕ 𝑣 ) ) ) ) → 𝑃 pGrp 𝐺 ) |
96 |
9
|
ad3antrrr |
⊢ ( ( ( ( 𝜑 ∧ ( 𝑠 ∈ ( SubGrp ‘ 𝐺 ) ∧ ( 𝑠 ⊊ 𝑈 ∧ 𝐴 ∈ 𝑠 ) ) ) ∧ 𝑣 ∈ ( SubGrp ‘ 𝐺 ) ) ∧ ( ( ( 𝑆 ∩ 𝑣 ) = { 0 } ∧ ( 𝑆 ⊕ 𝑣 ) = 𝑠 ∧ ∀ 𝑤 ∈ ( SubGrp ‘ 𝐺 ) ( ( 𝑤 ⊊ 𝑈 ∧ 𝐴 ∈ 𝑤 ) → ¬ 𝑠 ⊊ 𝑤 ) ) ∧ 𝑏 ∈ ( 𝑈 ∖ ( 𝑆 ⊕ 𝑣 ) ) ) ) → 𝐺 ∈ Abel ) |
97 |
10
|
ad3antrrr |
⊢ ( ( ( ( 𝜑 ∧ ( 𝑠 ∈ ( SubGrp ‘ 𝐺 ) ∧ ( 𝑠 ⊊ 𝑈 ∧ 𝐴 ∈ 𝑠 ) ) ) ∧ 𝑣 ∈ ( SubGrp ‘ 𝐺 ) ) ∧ ( ( ( 𝑆 ∩ 𝑣 ) = { 0 } ∧ ( 𝑆 ⊕ 𝑣 ) = 𝑠 ∧ ∀ 𝑤 ∈ ( SubGrp ‘ 𝐺 ) ( ( 𝑤 ⊊ 𝑈 ∧ 𝐴 ∈ 𝑤 ) → ¬ 𝑠 ⊊ 𝑤 ) ) ∧ 𝑏 ∈ ( 𝑈 ∖ ( 𝑆 ⊕ 𝑣 ) ) ) ) → 𝐵 ∈ Fin ) |
98 |
11
|
ad3antrrr |
⊢ ( ( ( ( 𝜑 ∧ ( 𝑠 ∈ ( SubGrp ‘ 𝐺 ) ∧ ( 𝑠 ⊊ 𝑈 ∧ 𝐴 ∈ 𝑠 ) ) ) ∧ 𝑣 ∈ ( SubGrp ‘ 𝐺 ) ) ∧ ( ( ( 𝑆 ∩ 𝑣 ) = { 0 } ∧ ( 𝑆 ⊕ 𝑣 ) = 𝑠 ∧ ∀ 𝑤 ∈ ( SubGrp ‘ 𝐺 ) ( ( 𝑤 ⊊ 𝑈 ∧ 𝐴 ∈ 𝑤 ) → ¬ 𝑠 ⊊ 𝑤 ) ) ∧ 𝑏 ∈ ( 𝑈 ∖ ( 𝑆 ⊕ 𝑣 ) ) ) ) → ( 𝑂 ‘ 𝐴 ) = 𝐸 ) |
99 |
12
|
ad3antrrr |
⊢ ( ( ( ( 𝜑 ∧ ( 𝑠 ∈ ( SubGrp ‘ 𝐺 ) ∧ ( 𝑠 ⊊ 𝑈 ∧ 𝐴 ∈ 𝑠 ) ) ) ∧ 𝑣 ∈ ( SubGrp ‘ 𝐺 ) ) ∧ ( ( ( 𝑆 ∩ 𝑣 ) = { 0 } ∧ ( 𝑆 ⊕ 𝑣 ) = 𝑠 ∧ ∀ 𝑤 ∈ ( SubGrp ‘ 𝐺 ) ( ( 𝑤 ⊊ 𝑈 ∧ 𝐴 ∈ 𝑤 ) → ¬ 𝑠 ⊊ 𝑤 ) ) ∧ 𝑏 ∈ ( 𝑈 ∖ ( 𝑆 ⊕ 𝑣 ) ) ) ) → 𝑈 ∈ ( SubGrp ‘ 𝐺 ) ) |
100 |
13
|
ad3antrrr |
⊢ ( ( ( ( 𝜑 ∧ ( 𝑠 ∈ ( SubGrp ‘ 𝐺 ) ∧ ( 𝑠 ⊊ 𝑈 ∧ 𝐴 ∈ 𝑠 ) ) ) ∧ 𝑣 ∈ ( SubGrp ‘ 𝐺 ) ) ∧ ( ( ( 𝑆 ∩ 𝑣 ) = { 0 } ∧ ( 𝑆 ⊕ 𝑣 ) = 𝑠 ∧ ∀ 𝑤 ∈ ( SubGrp ‘ 𝐺 ) ( ( 𝑤 ⊊ 𝑈 ∧ 𝐴 ∈ 𝑤 ) → ¬ 𝑠 ⊊ 𝑤 ) ) ∧ 𝑏 ∈ ( 𝑈 ∖ ( 𝑆 ⊕ 𝑣 ) ) ) ) → 𝐴 ∈ 𝑈 ) |
101 |
|
simplr |
⊢ ( ( ( ( 𝜑 ∧ ( 𝑠 ∈ ( SubGrp ‘ 𝐺 ) ∧ ( 𝑠 ⊊ 𝑈 ∧ 𝐴 ∈ 𝑠 ) ) ) ∧ 𝑣 ∈ ( SubGrp ‘ 𝐺 ) ) ∧ ( ( ( 𝑆 ∩ 𝑣 ) = { 0 } ∧ ( 𝑆 ⊕ 𝑣 ) = 𝑠 ∧ ∀ 𝑤 ∈ ( SubGrp ‘ 𝐺 ) ( ( 𝑤 ⊊ 𝑈 ∧ 𝐴 ∈ 𝑤 ) → ¬ 𝑠 ⊊ 𝑤 ) ) ∧ 𝑏 ∈ ( 𝑈 ∖ ( 𝑆 ⊕ 𝑣 ) ) ) ) → 𝑣 ∈ ( SubGrp ‘ 𝐺 ) ) |
102 |
|
simprl1 |
⊢ ( ( ( ( 𝜑 ∧ ( 𝑠 ∈ ( SubGrp ‘ 𝐺 ) ∧ ( 𝑠 ⊊ 𝑈 ∧ 𝐴 ∈ 𝑠 ) ) ) ∧ 𝑣 ∈ ( SubGrp ‘ 𝐺 ) ) ∧ ( ( ( 𝑆 ∩ 𝑣 ) = { 0 } ∧ ( 𝑆 ⊕ 𝑣 ) = 𝑠 ∧ ∀ 𝑤 ∈ ( SubGrp ‘ 𝐺 ) ( ( 𝑤 ⊊ 𝑈 ∧ 𝐴 ∈ 𝑤 ) → ¬ 𝑠 ⊊ 𝑤 ) ) ∧ 𝑏 ∈ ( 𝑈 ∖ ( 𝑆 ⊕ 𝑣 ) ) ) ) → ( 𝑆 ∩ 𝑣 ) = { 0 } ) |
103 |
90
|
adantrr |
⊢ ( ( ( ( 𝜑 ∧ ( 𝑠 ∈ ( SubGrp ‘ 𝐺 ) ∧ ( 𝑠 ⊊ 𝑈 ∧ 𝐴 ∈ 𝑠 ) ) ) ∧ 𝑣 ∈ ( SubGrp ‘ 𝐺 ) ) ∧ ( ( ( 𝑆 ∩ 𝑣 ) = { 0 } ∧ ( 𝑆 ⊕ 𝑣 ) = 𝑠 ∧ ∀ 𝑤 ∈ ( SubGrp ‘ 𝐺 ) ( ( 𝑤 ⊊ 𝑈 ∧ 𝐴 ∈ 𝑤 ) → ¬ 𝑠 ⊊ 𝑤 ) ) ∧ 𝑏 ∈ ( 𝑈 ∖ ( 𝑆 ⊕ 𝑣 ) ) ) ) → ( 𝑆 ⊕ 𝑣 ) ⊊ 𝑈 ) |
104 |
103
|
pssssd |
⊢ ( ( ( ( 𝜑 ∧ ( 𝑠 ∈ ( SubGrp ‘ 𝐺 ) ∧ ( 𝑠 ⊊ 𝑈 ∧ 𝐴 ∈ 𝑠 ) ) ) ∧ 𝑣 ∈ ( SubGrp ‘ 𝐺 ) ) ∧ ( ( ( 𝑆 ∩ 𝑣 ) = { 0 } ∧ ( 𝑆 ⊕ 𝑣 ) = 𝑠 ∧ ∀ 𝑤 ∈ ( SubGrp ‘ 𝐺 ) ( ( 𝑤 ⊊ 𝑈 ∧ 𝐴 ∈ 𝑤 ) → ¬ 𝑠 ⊊ 𝑤 ) ) ∧ 𝑏 ∈ ( 𝑈 ∖ ( 𝑆 ⊕ 𝑣 ) ) ) ) → ( 𝑆 ⊕ 𝑣 ) ⊆ 𝑈 ) |
105 |
|
simprl3 |
⊢ ( ( ( ( 𝜑 ∧ ( 𝑠 ∈ ( SubGrp ‘ 𝐺 ) ∧ ( 𝑠 ⊊ 𝑈 ∧ 𝐴 ∈ 𝑠 ) ) ) ∧ 𝑣 ∈ ( SubGrp ‘ 𝐺 ) ) ∧ ( ( ( 𝑆 ∩ 𝑣 ) = { 0 } ∧ ( 𝑆 ⊕ 𝑣 ) = 𝑠 ∧ ∀ 𝑤 ∈ ( SubGrp ‘ 𝐺 ) ( ( 𝑤 ⊊ 𝑈 ∧ 𝐴 ∈ 𝑤 ) → ¬ 𝑠 ⊊ 𝑤 ) ) ∧ 𝑏 ∈ ( 𝑈 ∖ ( 𝑆 ⊕ 𝑣 ) ) ) ) → ∀ 𝑤 ∈ ( SubGrp ‘ 𝐺 ) ( ( 𝑤 ⊊ 𝑈 ∧ 𝐴 ∈ 𝑤 ) → ¬ 𝑠 ⊊ 𝑤 ) ) |
106 |
88
|
adantrr |
⊢ ( ( ( ( 𝜑 ∧ ( 𝑠 ∈ ( SubGrp ‘ 𝐺 ) ∧ ( 𝑠 ⊊ 𝑈 ∧ 𝐴 ∈ 𝑠 ) ) ) ∧ 𝑣 ∈ ( SubGrp ‘ 𝐺 ) ) ∧ ( ( ( 𝑆 ∩ 𝑣 ) = { 0 } ∧ ( 𝑆 ⊕ 𝑣 ) = 𝑠 ∧ ∀ 𝑤 ∈ ( SubGrp ‘ 𝐺 ) ( ( 𝑤 ⊊ 𝑈 ∧ 𝐴 ∈ 𝑤 ) → ¬ 𝑠 ⊊ 𝑤 ) ) ∧ 𝑏 ∈ ( 𝑈 ∖ ( 𝑆 ⊕ 𝑣 ) ) ) ) → ( 𝑆 ⊕ 𝑣 ) = 𝑠 ) |
107 |
|
psseq1 |
⊢ ( ( 𝑆 ⊕ 𝑣 ) = 𝑠 → ( ( 𝑆 ⊕ 𝑣 ) ⊊ 𝑦 ↔ 𝑠 ⊊ 𝑦 ) ) |
108 |
107
|
notbid |
⊢ ( ( 𝑆 ⊕ 𝑣 ) = 𝑠 → ( ¬ ( 𝑆 ⊕ 𝑣 ) ⊊ 𝑦 ↔ ¬ 𝑠 ⊊ 𝑦 ) ) |
109 |
108
|
imbi2d |
⊢ ( ( 𝑆 ⊕ 𝑣 ) = 𝑠 → ( ( ( 𝑦 ⊊ 𝑈 ∧ 𝐴 ∈ 𝑦 ) → ¬ ( 𝑆 ⊕ 𝑣 ) ⊊ 𝑦 ) ↔ ( ( 𝑦 ⊊ 𝑈 ∧ 𝐴 ∈ 𝑦 ) → ¬ 𝑠 ⊊ 𝑦 ) ) ) |
110 |
109
|
ralbidv |
⊢ ( ( 𝑆 ⊕ 𝑣 ) = 𝑠 → ( ∀ 𝑦 ∈ ( SubGrp ‘ 𝐺 ) ( ( 𝑦 ⊊ 𝑈 ∧ 𝐴 ∈ 𝑦 ) → ¬ ( 𝑆 ⊕ 𝑣 ) ⊊ 𝑦 ) ↔ ∀ 𝑦 ∈ ( SubGrp ‘ 𝐺 ) ( ( 𝑦 ⊊ 𝑈 ∧ 𝐴 ∈ 𝑦 ) → ¬ 𝑠 ⊊ 𝑦 ) ) ) |
111 |
|
psseq1 |
⊢ ( 𝑦 = 𝑤 → ( 𝑦 ⊊ 𝑈 ↔ 𝑤 ⊊ 𝑈 ) ) |
112 |
|
eleq2 |
⊢ ( 𝑦 = 𝑤 → ( 𝐴 ∈ 𝑦 ↔ 𝐴 ∈ 𝑤 ) ) |
113 |
111 112
|
anbi12d |
⊢ ( 𝑦 = 𝑤 → ( ( 𝑦 ⊊ 𝑈 ∧ 𝐴 ∈ 𝑦 ) ↔ ( 𝑤 ⊊ 𝑈 ∧ 𝐴 ∈ 𝑤 ) ) ) |
114 |
|
psseq2 |
⊢ ( 𝑦 = 𝑤 → ( 𝑠 ⊊ 𝑦 ↔ 𝑠 ⊊ 𝑤 ) ) |
115 |
114
|
notbid |
⊢ ( 𝑦 = 𝑤 → ( ¬ 𝑠 ⊊ 𝑦 ↔ ¬ 𝑠 ⊊ 𝑤 ) ) |
116 |
113 115
|
imbi12d |
⊢ ( 𝑦 = 𝑤 → ( ( ( 𝑦 ⊊ 𝑈 ∧ 𝐴 ∈ 𝑦 ) → ¬ 𝑠 ⊊ 𝑦 ) ↔ ( ( 𝑤 ⊊ 𝑈 ∧ 𝐴 ∈ 𝑤 ) → ¬ 𝑠 ⊊ 𝑤 ) ) ) |
117 |
116
|
cbvralvw |
⊢ ( ∀ 𝑦 ∈ ( SubGrp ‘ 𝐺 ) ( ( 𝑦 ⊊ 𝑈 ∧ 𝐴 ∈ 𝑦 ) → ¬ 𝑠 ⊊ 𝑦 ) ↔ ∀ 𝑤 ∈ ( SubGrp ‘ 𝐺 ) ( ( 𝑤 ⊊ 𝑈 ∧ 𝐴 ∈ 𝑤 ) → ¬ 𝑠 ⊊ 𝑤 ) ) |
118 |
110 117
|
bitrdi |
⊢ ( ( 𝑆 ⊕ 𝑣 ) = 𝑠 → ( ∀ 𝑦 ∈ ( SubGrp ‘ 𝐺 ) ( ( 𝑦 ⊊ 𝑈 ∧ 𝐴 ∈ 𝑦 ) → ¬ ( 𝑆 ⊕ 𝑣 ) ⊊ 𝑦 ) ↔ ∀ 𝑤 ∈ ( SubGrp ‘ 𝐺 ) ( ( 𝑤 ⊊ 𝑈 ∧ 𝐴 ∈ 𝑤 ) → ¬ 𝑠 ⊊ 𝑤 ) ) ) |
119 |
106 118
|
syl |
⊢ ( ( ( ( 𝜑 ∧ ( 𝑠 ∈ ( SubGrp ‘ 𝐺 ) ∧ ( 𝑠 ⊊ 𝑈 ∧ 𝐴 ∈ 𝑠 ) ) ) ∧ 𝑣 ∈ ( SubGrp ‘ 𝐺 ) ) ∧ ( ( ( 𝑆 ∩ 𝑣 ) = { 0 } ∧ ( 𝑆 ⊕ 𝑣 ) = 𝑠 ∧ ∀ 𝑤 ∈ ( SubGrp ‘ 𝐺 ) ( ( 𝑤 ⊊ 𝑈 ∧ 𝐴 ∈ 𝑤 ) → ¬ 𝑠 ⊊ 𝑤 ) ) ∧ 𝑏 ∈ ( 𝑈 ∖ ( 𝑆 ⊕ 𝑣 ) ) ) ) → ( ∀ 𝑦 ∈ ( SubGrp ‘ 𝐺 ) ( ( 𝑦 ⊊ 𝑈 ∧ 𝐴 ∈ 𝑦 ) → ¬ ( 𝑆 ⊕ 𝑣 ) ⊊ 𝑦 ) ↔ ∀ 𝑤 ∈ ( SubGrp ‘ 𝐺 ) ( ( 𝑤 ⊊ 𝑈 ∧ 𝐴 ∈ 𝑤 ) → ¬ 𝑠 ⊊ 𝑤 ) ) ) |
120 |
105 119
|
mpbird |
⊢ ( ( ( ( 𝜑 ∧ ( 𝑠 ∈ ( SubGrp ‘ 𝐺 ) ∧ ( 𝑠 ⊊ 𝑈 ∧ 𝐴 ∈ 𝑠 ) ) ) ∧ 𝑣 ∈ ( SubGrp ‘ 𝐺 ) ) ∧ ( ( ( 𝑆 ∩ 𝑣 ) = { 0 } ∧ ( 𝑆 ⊕ 𝑣 ) = 𝑠 ∧ ∀ 𝑤 ∈ ( SubGrp ‘ 𝐺 ) ( ( 𝑤 ⊊ 𝑈 ∧ 𝐴 ∈ 𝑤 ) → ¬ 𝑠 ⊊ 𝑤 ) ) ∧ 𝑏 ∈ ( 𝑈 ∖ ( 𝑆 ⊕ 𝑣 ) ) ) ) → ∀ 𝑦 ∈ ( SubGrp ‘ 𝐺 ) ( ( 𝑦 ⊊ 𝑈 ∧ 𝐴 ∈ 𝑦 ) → ¬ ( 𝑆 ⊕ 𝑣 ) ⊊ 𝑦 ) ) |
121 |
|
simprr |
⊢ ( ( ( ( 𝜑 ∧ ( 𝑠 ∈ ( SubGrp ‘ 𝐺 ) ∧ ( 𝑠 ⊊ 𝑈 ∧ 𝐴 ∈ 𝑠 ) ) ) ∧ 𝑣 ∈ ( SubGrp ‘ 𝐺 ) ) ∧ ( ( ( 𝑆 ∩ 𝑣 ) = { 0 } ∧ ( 𝑆 ⊕ 𝑣 ) = 𝑠 ∧ ∀ 𝑤 ∈ ( SubGrp ‘ 𝐺 ) ( ( 𝑤 ⊊ 𝑈 ∧ 𝐴 ∈ 𝑤 ) → ¬ 𝑠 ⊊ 𝑤 ) ) ∧ 𝑏 ∈ ( 𝑈 ∖ ( 𝑆 ⊕ 𝑣 ) ) ) ) → 𝑏 ∈ ( 𝑈 ∖ ( 𝑆 ⊕ 𝑣 ) ) ) |
122 |
|
eqid |
⊢ ( .g ‘ 𝐺 ) = ( .g ‘ 𝐺 ) |
123 |
1 2 3 4 5 6 7 95 96 97 98 99 100 101 102 104 120 121 122
|
pgpfac1lem4 |
⊢ ( ( ( ( 𝜑 ∧ ( 𝑠 ∈ ( SubGrp ‘ 𝐺 ) ∧ ( 𝑠 ⊊ 𝑈 ∧ 𝐴 ∈ 𝑠 ) ) ) ∧ 𝑣 ∈ ( SubGrp ‘ 𝐺 ) ) ∧ ( ( ( 𝑆 ∩ 𝑣 ) = { 0 } ∧ ( 𝑆 ⊕ 𝑣 ) = 𝑠 ∧ ∀ 𝑤 ∈ ( SubGrp ‘ 𝐺 ) ( ( 𝑤 ⊊ 𝑈 ∧ 𝐴 ∈ 𝑤 ) → ¬ 𝑠 ⊊ 𝑤 ) ) ∧ 𝑏 ∈ ( 𝑈 ∖ ( 𝑆 ⊕ 𝑣 ) ) ) ) → ∃ 𝑡 ∈ ( SubGrp ‘ 𝐺 ) ( ( 𝑆 ∩ 𝑡 ) = { 0 } ∧ ( 𝑆 ⊕ 𝑡 ) = 𝑈 ) ) |
124 |
123
|
expr |
⊢ ( ( ( ( 𝜑 ∧ ( 𝑠 ∈ ( SubGrp ‘ 𝐺 ) ∧ ( 𝑠 ⊊ 𝑈 ∧ 𝐴 ∈ 𝑠 ) ) ) ∧ 𝑣 ∈ ( SubGrp ‘ 𝐺 ) ) ∧ ( ( 𝑆 ∩ 𝑣 ) = { 0 } ∧ ( 𝑆 ⊕ 𝑣 ) = 𝑠 ∧ ∀ 𝑤 ∈ ( SubGrp ‘ 𝐺 ) ( ( 𝑤 ⊊ 𝑈 ∧ 𝐴 ∈ 𝑤 ) → ¬ 𝑠 ⊊ 𝑤 ) ) ) → ( 𝑏 ∈ ( 𝑈 ∖ ( 𝑆 ⊕ 𝑣 ) ) → ∃ 𝑡 ∈ ( SubGrp ‘ 𝐺 ) ( ( 𝑆 ∩ 𝑡 ) = { 0 } ∧ ( 𝑆 ⊕ 𝑡 ) = 𝑈 ) ) ) |
125 |
124
|
exlimdv |
⊢ ( ( ( ( 𝜑 ∧ ( 𝑠 ∈ ( SubGrp ‘ 𝐺 ) ∧ ( 𝑠 ⊊ 𝑈 ∧ 𝐴 ∈ 𝑠 ) ) ) ∧ 𝑣 ∈ ( SubGrp ‘ 𝐺 ) ) ∧ ( ( 𝑆 ∩ 𝑣 ) = { 0 } ∧ ( 𝑆 ⊕ 𝑣 ) = 𝑠 ∧ ∀ 𝑤 ∈ ( SubGrp ‘ 𝐺 ) ( ( 𝑤 ⊊ 𝑈 ∧ 𝐴 ∈ 𝑤 ) → ¬ 𝑠 ⊊ 𝑤 ) ) ) → ( ∃ 𝑏 𝑏 ∈ ( 𝑈 ∖ ( 𝑆 ⊕ 𝑣 ) ) → ∃ 𝑡 ∈ ( SubGrp ‘ 𝐺 ) ( ( 𝑆 ∩ 𝑡 ) = { 0 } ∧ ( 𝑆 ⊕ 𝑡 ) = 𝑈 ) ) ) |
126 |
94 125
|
mpd |
⊢ ( ( ( ( 𝜑 ∧ ( 𝑠 ∈ ( SubGrp ‘ 𝐺 ) ∧ ( 𝑠 ⊊ 𝑈 ∧ 𝐴 ∈ 𝑠 ) ) ) ∧ 𝑣 ∈ ( SubGrp ‘ 𝐺 ) ) ∧ ( ( 𝑆 ∩ 𝑣 ) = { 0 } ∧ ( 𝑆 ⊕ 𝑣 ) = 𝑠 ∧ ∀ 𝑤 ∈ ( SubGrp ‘ 𝐺 ) ( ( 𝑤 ⊊ 𝑈 ∧ 𝐴 ∈ 𝑤 ) → ¬ 𝑠 ⊊ 𝑤 ) ) ) → ∃ 𝑡 ∈ ( SubGrp ‘ 𝐺 ) ( ( 𝑆 ∩ 𝑡 ) = { 0 } ∧ ( 𝑆 ⊕ 𝑡 ) = 𝑈 ) ) |
127 |
126
|
3exp2 |
⊢ ( ( ( 𝜑 ∧ ( 𝑠 ∈ ( SubGrp ‘ 𝐺 ) ∧ ( 𝑠 ⊊ 𝑈 ∧ 𝐴 ∈ 𝑠 ) ) ) ∧ 𝑣 ∈ ( SubGrp ‘ 𝐺 ) ) → ( ( 𝑆 ∩ 𝑣 ) = { 0 } → ( ( 𝑆 ⊕ 𝑣 ) = 𝑠 → ( ∀ 𝑤 ∈ ( SubGrp ‘ 𝐺 ) ( ( 𝑤 ⊊ 𝑈 ∧ 𝐴 ∈ 𝑤 ) → ¬ 𝑠 ⊊ 𝑤 ) → ∃ 𝑡 ∈ ( SubGrp ‘ 𝐺 ) ( ( 𝑆 ∩ 𝑡 ) = { 0 } ∧ ( 𝑆 ⊕ 𝑡 ) = 𝑈 ) ) ) ) ) |
128 |
127
|
impd |
⊢ ( ( ( 𝜑 ∧ ( 𝑠 ∈ ( SubGrp ‘ 𝐺 ) ∧ ( 𝑠 ⊊ 𝑈 ∧ 𝐴 ∈ 𝑠 ) ) ) ∧ 𝑣 ∈ ( SubGrp ‘ 𝐺 ) ) → ( ( ( 𝑆 ∩ 𝑣 ) = { 0 } ∧ ( 𝑆 ⊕ 𝑣 ) = 𝑠 ) → ( ∀ 𝑤 ∈ ( SubGrp ‘ 𝐺 ) ( ( 𝑤 ⊊ 𝑈 ∧ 𝐴 ∈ 𝑤 ) → ¬ 𝑠 ⊊ 𝑤 ) → ∃ 𝑡 ∈ ( SubGrp ‘ 𝐺 ) ( ( 𝑆 ∩ 𝑡 ) = { 0 } ∧ ( 𝑆 ⊕ 𝑡 ) = 𝑈 ) ) ) ) |
129 |
128
|
rexlimdva |
⊢ ( ( 𝜑 ∧ ( 𝑠 ∈ ( SubGrp ‘ 𝐺 ) ∧ ( 𝑠 ⊊ 𝑈 ∧ 𝐴 ∈ 𝑠 ) ) ) → ( ∃ 𝑣 ∈ ( SubGrp ‘ 𝐺 ) ( ( 𝑆 ∩ 𝑣 ) = { 0 } ∧ ( 𝑆 ⊕ 𝑣 ) = 𝑠 ) → ( ∀ 𝑤 ∈ ( SubGrp ‘ 𝐺 ) ( ( 𝑤 ⊊ 𝑈 ∧ 𝐴 ∈ 𝑤 ) → ¬ 𝑠 ⊊ 𝑤 ) → ∃ 𝑡 ∈ ( SubGrp ‘ 𝐺 ) ( ( 𝑆 ∩ 𝑡 ) = { 0 } ∧ ( 𝑆 ⊕ 𝑡 ) = 𝑈 ) ) ) ) |
130 |
85 129
|
syl5bi |
⊢ ( ( 𝜑 ∧ ( 𝑠 ∈ ( SubGrp ‘ 𝐺 ) ∧ ( 𝑠 ⊊ 𝑈 ∧ 𝐴 ∈ 𝑠 ) ) ) → ( ∃ 𝑡 ∈ ( SubGrp ‘ 𝐺 ) ( ( 𝑆 ∩ 𝑡 ) = { 0 } ∧ ( 𝑆 ⊕ 𝑡 ) = 𝑠 ) → ( ∀ 𝑤 ∈ ( SubGrp ‘ 𝐺 ) ( ( 𝑤 ⊊ 𝑈 ∧ 𝐴 ∈ 𝑤 ) → ¬ 𝑠 ⊊ 𝑤 ) → ∃ 𝑡 ∈ ( SubGrp ‘ 𝐺 ) ( ( 𝑆 ∩ 𝑡 ) = { 0 } ∧ ( 𝑆 ⊕ 𝑡 ) = 𝑈 ) ) ) ) |
131 |
130
|
impd |
⊢ ( ( 𝜑 ∧ ( 𝑠 ∈ ( SubGrp ‘ 𝐺 ) ∧ ( 𝑠 ⊊ 𝑈 ∧ 𝐴 ∈ 𝑠 ) ) ) → ( ( ∃ 𝑡 ∈ ( SubGrp ‘ 𝐺 ) ( ( 𝑆 ∩ 𝑡 ) = { 0 } ∧ ( 𝑆 ⊕ 𝑡 ) = 𝑠 ) ∧ ∀ 𝑤 ∈ ( SubGrp ‘ 𝐺 ) ( ( 𝑤 ⊊ 𝑈 ∧ 𝐴 ∈ 𝑤 ) → ¬ 𝑠 ⊊ 𝑤 ) ) → ∃ 𝑡 ∈ ( SubGrp ‘ 𝐺 ) ( ( 𝑆 ∩ 𝑡 ) = { 0 } ∧ ( 𝑆 ⊕ 𝑡 ) = 𝑈 ) ) ) |
132 |
79 131
|
sylan2b |
⊢ ( ( 𝜑 ∧ 𝑠 ∈ { 𝑣 ∈ ( SubGrp ‘ 𝐺 ) ∣ ( 𝑣 ⊊ 𝑈 ∧ 𝐴 ∈ 𝑣 ) } ) → ( ( ∃ 𝑡 ∈ ( SubGrp ‘ 𝐺 ) ( ( 𝑆 ∩ 𝑡 ) = { 0 } ∧ ( 𝑆 ⊕ 𝑡 ) = 𝑠 ) ∧ ∀ 𝑤 ∈ ( SubGrp ‘ 𝐺 ) ( ( 𝑤 ⊊ 𝑈 ∧ 𝐴 ∈ 𝑤 ) → ¬ 𝑠 ⊊ 𝑤 ) ) → ∃ 𝑡 ∈ ( SubGrp ‘ 𝐺 ) ( ( 𝑆 ∩ 𝑡 ) = { 0 } ∧ ( 𝑆 ⊕ 𝑡 ) = 𝑈 ) ) ) |
133 |
132
|
rexlimdva |
⊢ ( 𝜑 → ( ∃ 𝑠 ∈ { 𝑣 ∈ ( SubGrp ‘ 𝐺 ) ∣ ( 𝑣 ⊊ 𝑈 ∧ 𝐴 ∈ 𝑣 ) } ( ∃ 𝑡 ∈ ( SubGrp ‘ 𝐺 ) ( ( 𝑆 ∩ 𝑡 ) = { 0 } ∧ ( 𝑆 ⊕ 𝑡 ) = 𝑠 ) ∧ ∀ 𝑤 ∈ ( SubGrp ‘ 𝐺 ) ( ( 𝑤 ⊊ 𝑈 ∧ 𝐴 ∈ 𝑤 ) → ¬ 𝑠 ⊊ 𝑤 ) ) → ∃ 𝑡 ∈ ( SubGrp ‘ 𝐺 ) ( ( 𝑆 ∩ 𝑡 ) = { 0 } ∧ ( 𝑆 ⊕ 𝑡 ) = 𝑈 ) ) ) |
134 |
78 133
|
syl5 |
⊢ ( 𝜑 → ( ( ∀ 𝑠 ∈ { 𝑣 ∈ ( SubGrp ‘ 𝐺 ) ∣ ( 𝑣 ⊊ 𝑈 ∧ 𝐴 ∈ 𝑣 ) } ∃ 𝑡 ∈ ( SubGrp ‘ 𝐺 ) ( ( 𝑆 ∩ 𝑡 ) = { 0 } ∧ ( 𝑆 ⊕ 𝑡 ) = 𝑠 ) ∧ ∃ 𝑠 ∈ { 𝑣 ∈ ( SubGrp ‘ 𝐺 ) ∣ ( 𝑣 ⊊ 𝑈 ∧ 𝐴 ∈ 𝑣 ) } ∀ 𝑤 ∈ ( SubGrp ‘ 𝐺 ) ( ( 𝑤 ⊊ 𝑈 ∧ 𝐴 ∈ 𝑤 ) → ¬ 𝑠 ⊊ 𝑤 ) ) → ∃ 𝑡 ∈ ( SubGrp ‘ 𝐺 ) ( ( 𝑆 ∩ 𝑡 ) = { 0 } ∧ ( 𝑆 ⊕ 𝑡 ) = 𝑈 ) ) ) |
135 |
77 134
|
mpand |
⊢ ( 𝜑 → ( ∃ 𝑠 ∈ { 𝑣 ∈ ( SubGrp ‘ 𝐺 ) ∣ ( 𝑣 ⊊ 𝑈 ∧ 𝐴 ∈ 𝑣 ) } ∀ 𝑤 ∈ ( SubGrp ‘ 𝐺 ) ( ( 𝑤 ⊊ 𝑈 ∧ 𝐴 ∈ 𝑤 ) → ¬ 𝑠 ⊊ 𝑤 ) → ∃ 𝑡 ∈ ( SubGrp ‘ 𝐺 ) ( ( 𝑆 ∩ 𝑡 ) = { 0 } ∧ ( 𝑆 ⊕ 𝑡 ) = 𝑈 ) ) ) |
136 |
72 135
|
syld |
⊢ ( 𝜑 → ( 𝑆 ⊊ 𝑈 → ∃ 𝑡 ∈ ( SubGrp ‘ 𝐺 ) ( ( 𝑆 ∩ 𝑡 ) = { 0 } ∧ ( 𝑆 ⊕ 𝑡 ) = 𝑈 ) ) ) |
137 |
6
|
0subg |
⊢ ( 𝐺 ∈ Grp → { 0 } ∈ ( SubGrp ‘ 𝐺 ) ) |
138 |
27 137
|
syl |
⊢ ( 𝜑 → { 0 } ∈ ( SubGrp ‘ 𝐺 ) ) |
139 |
138
|
adantr |
⊢ ( ( 𝜑 ∧ 𝑆 = 𝑈 ) → { 0 } ∈ ( SubGrp ‘ 𝐺 ) ) |
140 |
6
|
subg0cl |
⊢ ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) → 0 ∈ 𝑆 ) |
141 |
36 140
|
syl |
⊢ ( 𝜑 → 0 ∈ 𝑆 ) |
142 |
141
|
snssd |
⊢ ( 𝜑 → { 0 } ⊆ 𝑆 ) |
143 |
142
|
adantr |
⊢ ( ( 𝜑 ∧ 𝑆 = 𝑈 ) → { 0 } ⊆ 𝑆 ) |
144 |
|
sseqin2 |
⊢ ( { 0 } ⊆ 𝑆 ↔ ( 𝑆 ∩ { 0 } ) = { 0 } ) |
145 |
143 144
|
sylib |
⊢ ( ( 𝜑 ∧ 𝑆 = 𝑈 ) → ( 𝑆 ∩ { 0 } ) = { 0 } ) |
146 |
7
|
lsmss2 |
⊢ ( ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ { 0 } ∈ ( SubGrp ‘ 𝐺 ) ∧ { 0 } ⊆ 𝑆 ) → ( 𝑆 ⊕ { 0 } ) = 𝑆 ) |
147 |
36 138 142 146
|
syl3anc |
⊢ ( 𝜑 → ( 𝑆 ⊕ { 0 } ) = 𝑆 ) |
148 |
147
|
eqeq1d |
⊢ ( 𝜑 → ( ( 𝑆 ⊕ { 0 } ) = 𝑈 ↔ 𝑆 = 𝑈 ) ) |
149 |
148
|
biimpar |
⊢ ( ( 𝜑 ∧ 𝑆 = 𝑈 ) → ( 𝑆 ⊕ { 0 } ) = 𝑈 ) |
150 |
|
ineq2 |
⊢ ( 𝑡 = { 0 } → ( 𝑆 ∩ 𝑡 ) = ( 𝑆 ∩ { 0 } ) ) |
151 |
150
|
eqeq1d |
⊢ ( 𝑡 = { 0 } → ( ( 𝑆 ∩ 𝑡 ) = { 0 } ↔ ( 𝑆 ∩ { 0 } ) = { 0 } ) ) |
152 |
|
oveq2 |
⊢ ( 𝑡 = { 0 } → ( 𝑆 ⊕ 𝑡 ) = ( 𝑆 ⊕ { 0 } ) ) |
153 |
152
|
eqeq1d |
⊢ ( 𝑡 = { 0 } → ( ( 𝑆 ⊕ 𝑡 ) = 𝑈 ↔ ( 𝑆 ⊕ { 0 } ) = 𝑈 ) ) |
154 |
151 153
|
anbi12d |
⊢ ( 𝑡 = { 0 } → ( ( ( 𝑆 ∩ 𝑡 ) = { 0 } ∧ ( 𝑆 ⊕ 𝑡 ) = 𝑈 ) ↔ ( ( 𝑆 ∩ { 0 } ) = { 0 } ∧ ( 𝑆 ⊕ { 0 } ) = 𝑈 ) ) ) |
155 |
154
|
rspcev |
⊢ ( ( { 0 } ∈ ( SubGrp ‘ 𝐺 ) ∧ ( ( 𝑆 ∩ { 0 } ) = { 0 } ∧ ( 𝑆 ⊕ { 0 } ) = 𝑈 ) ) → ∃ 𝑡 ∈ ( SubGrp ‘ 𝐺 ) ( ( 𝑆 ∩ 𝑡 ) = { 0 } ∧ ( 𝑆 ⊕ 𝑡 ) = 𝑈 ) ) |
156 |
139 145 149 155
|
syl12anc |
⊢ ( ( 𝜑 ∧ 𝑆 = 𝑈 ) → ∃ 𝑡 ∈ ( SubGrp ‘ 𝐺 ) ( ( 𝑆 ∩ 𝑡 ) = { 0 } ∧ ( 𝑆 ⊕ 𝑡 ) = 𝑈 ) ) |
157 |
156
|
ex |
⊢ ( 𝜑 → ( 𝑆 = 𝑈 → ∃ 𝑡 ∈ ( SubGrp ‘ 𝐺 ) ( ( 𝑆 ∩ 𝑡 ) = { 0 } ∧ ( 𝑆 ⊕ 𝑡 ) = 𝑈 ) ) ) |
158 |
1
|
mrcsscl |
⊢ ( ( ( SubGrp ‘ 𝐺 ) ∈ ( Moore ‘ 𝐵 ) ∧ { 𝐴 } ⊆ 𝑈 ∧ 𝑈 ∈ ( SubGrp ‘ 𝐺 ) ) → ( 𝐾 ‘ { 𝐴 } ) ⊆ 𝑈 ) |
159 |
30 39 12 158
|
syl3anc |
⊢ ( 𝜑 → ( 𝐾 ‘ { 𝐴 } ) ⊆ 𝑈 ) |
160 |
2 159
|
eqsstrid |
⊢ ( 𝜑 → 𝑆 ⊆ 𝑈 ) |
161 |
|
sspss |
⊢ ( 𝑆 ⊆ 𝑈 ↔ ( 𝑆 ⊊ 𝑈 ∨ 𝑆 = 𝑈 ) ) |
162 |
160 161
|
sylib |
⊢ ( 𝜑 → ( 𝑆 ⊊ 𝑈 ∨ 𝑆 = 𝑈 ) ) |
163 |
136 157 162
|
mpjaod |
⊢ ( 𝜑 → ∃ 𝑡 ∈ ( SubGrp ‘ 𝐺 ) ( ( 𝑆 ∩ 𝑡 ) = { 0 } ∧ ( 𝑆 ⊕ 𝑡 ) = 𝑈 ) ) |