Description: The internal direct product of a family of subgroups is a subgroup. (Contributed by Mario Carneiro, 25-Apr-2016)
Ref | Expression | ||
---|---|---|---|
Assertion | dprdsubg | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | eqid | |
|
2 | 1 | dprdssv | |
3 | 2 | a1i | |
4 | eqid | |
|
5 | eqid | |
|
6 | id | |
|
7 | eqidd | |
|
8 | fvex | |
|
9 | fnconstg | |
|
10 | 8 9 | mp1i | |
11 | 8 | fvconst2 | |
12 | 11 | adantl | |
13 | dprdf | |
|
14 | 13 | ffvelcdmda | |
15 | 4 | subg0cl | |
16 | 14 15 | syl | |
17 | 12 16 | eqeltrd | |
18 | 17 | ralrimiva | |
19 | df-nel | |
|
20 | dprddomprc | |
|
21 | 19 20 | sylbir | |
22 | 21 | con4i | |
23 | 8 | a1i | |
24 | 22 23 | fczfsuppd | |
25 | 5 6 7 | dprdw | |
26 | 10 18 24 25 | mpbir3and | |
27 | 4 5 6 7 26 | eldprdi | |
28 | 27 | ne0d | |
29 | eqid | |
|
30 | 4 5 | eldprd | |
31 | 30 | baibd | |
32 | 4 5 | eldprd | |
33 | 32 | baibd | |
34 | 31 33 | anbi12d | |
35 | 29 34 | mpan | |
36 | reeanv | |
|
37 | simpl | |
|
38 | eqidd | |
|
39 | simprl | |
|
40 | simprr | |
|
41 | eqid | |
|
42 | 4 5 37 38 39 40 41 | dprdfsub | |
43 | 42 | simprd | |
44 | 42 | simpld | |
45 | 4 5 37 38 44 | eldprdi | |
46 | 43 45 | eqeltrrd | |
47 | oveq12 | |
|
48 | 47 | eleq1d | |
49 | 46 48 | syl5ibrcom | |
50 | 49 | rexlimdvva | |
51 | 36 50 | biimtrrid | |
52 | 35 51 | sylbid | |
53 | 52 | ralrimivv | |
54 | dprdgrp | |
|
55 | 1 41 | issubg4 | |
56 | 54 55 | syl | |
57 | 3 28 53 56 | mpbir3and | |