Proof of Theorem isngp2
Step | Hyp | Ref
| Expression |
1 | | isngp.n |
. . 3
⊢ 𝑁 = (norm‘𝐺) |
2 | | isngp.z |
. . 3
⊢ − =
(-g‘𝐺) |
3 | | isngp.d |
. . 3
⊢ 𝐷 = (dist‘𝐺) |
4 | 1, 2, 3 | isngp 22210 |
. 2
⊢ (𝐺 ∈ NrmGrp ↔ (𝐺 ∈ Grp ∧ 𝐺 ∈ MetSp ∧ (𝑁 ∘ − ) ⊆ 𝐷)) |
5 | | isngp2.e |
. . . . . . 7
⊢ 𝐸 = (𝐷 ↾ (𝑋 × 𝑋)) |
6 | | resss 5342 |
. . . . . . 7
⊢ (𝐷 ↾ (𝑋 × 𝑋)) ⊆ 𝐷 |
7 | 5, 6 | eqsstri 3598 |
. . . . . 6
⊢ 𝐸 ⊆ 𝐷 |
8 | | sseq1 3589 |
. . . . . 6
⊢ ((𝑁 ∘ − ) = 𝐸 → ((𝑁 ∘ − ) ⊆ 𝐷 ↔ 𝐸 ⊆ 𝐷)) |
9 | 7, 8 | mpbiri 247 |
. . . . 5
⊢ ((𝑁 ∘ − ) = 𝐸 → (𝑁 ∘ − ) ⊆ 𝐷) |
10 | | isngp2.x |
. . . . . . . . . . . . 13
⊢ 𝑋 = (Base‘𝐺) |
11 | 3 | reseq1i 5313 |
. . . . . . . . . . . . . 14
⊢ (𝐷 ↾ (𝑋 × 𝑋)) = ((dist‘𝐺) ↾ (𝑋 × 𝑋)) |
12 | 5, 11 | eqtri 2632 |
. . . . . . . . . . . . 13
⊢ 𝐸 = ((dist‘𝐺) ↾ (𝑋 × 𝑋)) |
13 | 10, 12 | msmet 22072 |
. . . . . . . . . . . 12
⊢ (𝐺 ∈ MetSp → 𝐸 ∈ (Met‘𝑋)) |
14 | 1, 10, 3, 5 | nmf2 22207 |
. . . . . . . . . . . 12
⊢ ((𝐺 ∈ Grp ∧ 𝐸 ∈ (Met‘𝑋)) → 𝑁:𝑋⟶ℝ) |
15 | 13, 14 | sylan2 490 |
. . . . . . . . . . 11
⊢ ((𝐺 ∈ Grp ∧ 𝐺 ∈ MetSp) → 𝑁:𝑋⟶ℝ) |
16 | 15 | adantr 480 |
. . . . . . . . . 10
⊢ (((𝐺 ∈ Grp ∧ 𝐺 ∈ MetSp) ∧ (𝑁 ∘ − ) ⊆ 𝐷) → 𝑁:𝑋⟶ℝ) |
17 | 10, 2 | grpsubf 17317 |
. . . . . . . . . . 11
⊢ (𝐺 ∈ Grp → − :(𝑋 × 𝑋)⟶𝑋) |
18 | 17 | ad2antrr 758 |
. . . . . . . . . 10
⊢ (((𝐺 ∈ Grp ∧ 𝐺 ∈ MetSp) ∧ (𝑁 ∘ − ) ⊆ 𝐷) → − :(𝑋 × 𝑋)⟶𝑋) |
19 | | fco 5971 |
. . . . . . . . . 10
⊢ ((𝑁:𝑋⟶ℝ ∧ − :(𝑋 × 𝑋)⟶𝑋) → (𝑁 ∘ − ):(𝑋 × 𝑋)⟶ℝ) |
20 | 16, 18, 19 | syl2anc 691 |
. . . . . . . . 9
⊢ (((𝐺 ∈ Grp ∧ 𝐺 ∈ MetSp) ∧ (𝑁 ∘ − ) ⊆ 𝐷) → (𝑁 ∘ − ):(𝑋 × 𝑋)⟶ℝ) |
21 | | fdm 5964 |
. . . . . . . . 9
⊢ ((𝑁 ∘ − ):(𝑋 × 𝑋)⟶ℝ → dom (𝑁 ∘ − ) = (𝑋 × 𝑋)) |
22 | 20, 21 | syl 17 |
. . . . . . . 8
⊢ (((𝐺 ∈ Grp ∧ 𝐺 ∈ MetSp) ∧ (𝑁 ∘ − ) ⊆ 𝐷) → dom (𝑁 ∘ − ) = (𝑋 × 𝑋)) |
23 | 22 | reseq2d 5317 |
. . . . . . 7
⊢ (((𝐺 ∈ Grp ∧ 𝐺 ∈ MetSp) ∧ (𝑁 ∘ − ) ⊆ 𝐷) → (𝐸 ↾ dom (𝑁 ∘ − )) = (𝐸 ↾ (𝑋 × 𝑋))) |
24 | 10, 12 | msf 22073 |
. . . . . . . . . 10
⊢ (𝐺 ∈ MetSp → 𝐸:(𝑋 × 𝑋)⟶ℝ) |
25 | 24 | ad2antlr 759 |
. . . . . . . . 9
⊢ (((𝐺 ∈ Grp ∧ 𝐺 ∈ MetSp) ∧ (𝑁 ∘ − ) ⊆ 𝐷) → 𝐸:(𝑋 × 𝑋)⟶ℝ) |
26 | | ffun 5961 |
. . . . . . . . 9
⊢ (𝐸:(𝑋 × 𝑋)⟶ℝ → Fun 𝐸) |
27 | 25, 26 | syl 17 |
. . . . . . . 8
⊢ (((𝐺 ∈ Grp ∧ 𝐺 ∈ MetSp) ∧ (𝑁 ∘ − ) ⊆ 𝐷) → Fun 𝐸) |
28 | | simpr 476 |
. . . . . . . . . 10
⊢ (((𝐺 ∈ Grp ∧ 𝐺 ∈ MetSp) ∧ (𝑁 ∘ − ) ⊆ 𝐷) → (𝑁 ∘ − ) ⊆ 𝐷) |
29 | | ssv 3588 |
. . . . . . . . . . . 12
⊢ ℝ
⊆ V |
30 | | fss 5969 |
. . . . . . . . . . . 12
⊢ (((𝑁 ∘ − ):(𝑋 × 𝑋)⟶ℝ ∧ ℝ ⊆ V)
→ (𝑁 ∘ −
):(𝑋 × 𝑋)⟶V) |
31 | 20, 29, 30 | sylancl 693 |
. . . . . . . . . . 11
⊢ (((𝐺 ∈ Grp ∧ 𝐺 ∈ MetSp) ∧ (𝑁 ∘ − ) ⊆ 𝐷) → (𝑁 ∘ − ):(𝑋 × 𝑋)⟶V) |
32 | | fssxp 5973 |
. . . . . . . . . . 11
⊢ ((𝑁 ∘ − ):(𝑋 × 𝑋)⟶V → (𝑁 ∘ − ) ⊆ ((𝑋 × 𝑋) × V)) |
33 | 31, 32 | syl 17 |
. . . . . . . . . 10
⊢ (((𝐺 ∈ Grp ∧ 𝐺 ∈ MetSp) ∧ (𝑁 ∘ − ) ⊆ 𝐷) → (𝑁 ∘ − ) ⊆ ((𝑋 × 𝑋) × V)) |
34 | 28, 33 | ssind 3799 |
. . . . . . . . 9
⊢ (((𝐺 ∈ Grp ∧ 𝐺 ∈ MetSp) ∧ (𝑁 ∘ − ) ⊆ 𝐷) → (𝑁 ∘ − ) ⊆ (𝐷 ∩ ((𝑋 × 𝑋) × V))) |
35 | | df-res 5050 |
. . . . . . . . . 10
⊢ (𝐷 ↾ (𝑋 × 𝑋)) = (𝐷 ∩ ((𝑋 × 𝑋) × V)) |
36 | 5, 35 | eqtri 2632 |
. . . . . . . . 9
⊢ 𝐸 = (𝐷 ∩ ((𝑋 × 𝑋) × V)) |
37 | 34, 36 | syl6sseqr 3615 |
. . . . . . . 8
⊢ (((𝐺 ∈ Grp ∧ 𝐺 ∈ MetSp) ∧ (𝑁 ∘ − ) ⊆ 𝐷) → (𝑁 ∘ − ) ⊆ 𝐸) |
38 | | funssres 5844 |
. . . . . . . 8
⊢ ((Fun
𝐸 ∧ (𝑁 ∘ − ) ⊆ 𝐸) → (𝐸 ↾ dom (𝑁 ∘ − )) = (𝑁 ∘ − )) |
39 | 27, 37, 38 | syl2anc 691 |
. . . . . . 7
⊢ (((𝐺 ∈ Grp ∧ 𝐺 ∈ MetSp) ∧ (𝑁 ∘ − ) ⊆ 𝐷) → (𝐸 ↾ dom (𝑁 ∘ − )) = (𝑁 ∘ − )) |
40 | | ffn 5958 |
. . . . . . . 8
⊢ (𝐸:(𝑋 × 𝑋)⟶ℝ → 𝐸 Fn (𝑋 × 𝑋)) |
41 | | fnresdm 5914 |
. . . . . . . 8
⊢ (𝐸 Fn (𝑋 × 𝑋) → (𝐸 ↾ (𝑋 × 𝑋)) = 𝐸) |
42 | 25, 40, 41 | 3syl 18 |
. . . . . . 7
⊢ (((𝐺 ∈ Grp ∧ 𝐺 ∈ MetSp) ∧ (𝑁 ∘ − ) ⊆ 𝐷) → (𝐸 ↾ (𝑋 × 𝑋)) = 𝐸) |
43 | 23, 39, 42 | 3eqtr3d 2652 |
. . . . . 6
⊢ (((𝐺 ∈ Grp ∧ 𝐺 ∈ MetSp) ∧ (𝑁 ∘ − ) ⊆ 𝐷) → (𝑁 ∘ − ) = 𝐸) |
44 | 43 | ex 449 |
. . . . 5
⊢ ((𝐺 ∈ Grp ∧ 𝐺 ∈ MetSp) → ((𝑁 ∘ − ) ⊆ 𝐷 → (𝑁 ∘ − ) = 𝐸)) |
45 | 9, 44 | impbid2 215 |
. . . 4
⊢ ((𝐺 ∈ Grp ∧ 𝐺 ∈ MetSp) → ((𝑁 ∘ − ) = 𝐸 ↔ (𝑁 ∘ − ) ⊆ 𝐷)) |
46 | 45 | pm5.32i 667 |
. . 3
⊢ (((𝐺 ∈ Grp ∧ 𝐺 ∈ MetSp) ∧ (𝑁 ∘ − ) = 𝐸) ↔ ((𝐺 ∈ Grp ∧ 𝐺 ∈ MetSp) ∧ (𝑁 ∘ − ) ⊆ 𝐷)) |
47 | | df-3an 1033 |
. . 3
⊢ ((𝐺 ∈ Grp ∧ 𝐺 ∈ MetSp ∧ (𝑁 ∘ − ) = 𝐸) ↔ ((𝐺 ∈ Grp ∧ 𝐺 ∈ MetSp) ∧ (𝑁 ∘ − ) = 𝐸)) |
48 | | df-3an 1033 |
. . 3
⊢ ((𝐺 ∈ Grp ∧ 𝐺 ∈ MetSp ∧ (𝑁 ∘ − ) ⊆ 𝐷) ↔ ((𝐺 ∈ Grp ∧ 𝐺 ∈ MetSp) ∧ (𝑁 ∘ − ) ⊆ 𝐷)) |
49 | 46, 47, 48 | 3bitr4i 291 |
. 2
⊢ ((𝐺 ∈ Grp ∧ 𝐺 ∈ MetSp ∧ (𝑁 ∘ − ) = 𝐸) ↔ (𝐺 ∈ Grp ∧ 𝐺 ∈ MetSp ∧ (𝑁 ∘ − ) ⊆ 𝐷)) |
50 | 4, 49 | bitr4i 266 |
1
⊢ (𝐺 ∈ NrmGrp ↔ (𝐺 ∈ Grp ∧ 𝐺 ∈ MetSp ∧ (𝑁 ∘ − ) = 𝐸)) |