Metamath Proof Explorer

Theorem dprdcntz2

Description: The function S is a family of subgroups. (Contributed by Mario Carneiro, 26-Apr-2016)

Ref Expression
Hypotheses dprdcntz2.1 ⊢ ( 𝜑 → 𝐺 dom DProd 𝑆 )
dprdcntz2.2 ⊢ ( 𝜑 → dom 𝑆 = 𝐼 )
dprdcntz2.c ⊢ ( 𝜑 → 𝐶 ⊆ 𝐼 )
dprdcntz2.d ⊢ ( 𝜑 → 𝐷 ⊆ 𝐼 )
dprdcntz2.i ⊢ ( 𝜑 → ( 𝐶 ∩ 𝐷 ) = ∅ )
dprdcntz2.z ⊢ 𝑍 = ( Cntz ‘ 𝐺 )
Assertion dprdcntz2 ( 𝜑 → ( 𝐺 DProd ( 𝑆 ↾ 𝐶 ) ) ⊆ ( 𝑍 ‘ ( 𝐺 DProd ( 𝑆 ↾ 𝐷 ) ) ) )

Proof

Step Hyp Ref Expression
1 dprdcntz2.1 ⊢ ( 𝜑 → 𝐺 dom DProd 𝑆 )
2 dprdcntz2.2 ⊢ ( 𝜑 → dom 𝑆 = 𝐼 )
3 dprdcntz2.c ⊢ ( 𝜑 → 𝐶 ⊆ 𝐼 )
4 dprdcntz2.d ⊢ ( 𝜑 → 𝐷 ⊆ 𝐼 )
5 dprdcntz2.i ⊢ ( 𝜑 → ( 𝐶 ∩ 𝐷 ) = ∅ )
6 dprdcntz2.z ⊢ 𝑍 = ( Cntz ‘ 𝐺 )
7 1 2 3 dprdres ⊢ ( 𝜑 → ( 𝐺 dom DProd ( 𝑆 ↾ 𝐶 ) ∧ ( 𝐺 DProd ( 𝑆 ↾ 𝐶 ) ) ⊆ ( 𝐺 DProd 𝑆 ) ) )
8 7 simpld ⊢ ( 𝜑 → 𝐺 dom DProd ( 𝑆 ↾ 𝐶 ) )
9 dmres ⊢ dom ( 𝑆 ↾ 𝐶 ) = ( 𝐶 ∩ dom 𝑆 )
10 3 2 sseqtrrd ⊢ ( 𝜑 → 𝐶 ⊆ dom 𝑆 )
11 df-ss ⊢ ( 𝐶 ⊆ dom 𝑆 ↔ ( 𝐶 ∩ dom 𝑆 ) = 𝐶 )
12 10 11 sylib ⊢ ( 𝜑 → ( 𝐶 ∩ dom 𝑆 ) = 𝐶 )
13 9 12 syl5eq ⊢ ( 𝜑 → dom ( 𝑆 ↾ 𝐶 ) = 𝐶 )
14 dprdgrp ⊢ ( 𝐺 dom DProd 𝑆 → 𝐺 ∈ Grp )
15 1 14 syl ⊢ ( 𝜑 → 𝐺 ∈ Grp )
16 eqid ⊢ ( Base ‘ 𝐺 ) = ( Base ‘ 𝐺 )
17 16 dprdssv ⊢ ( 𝐺 DProd ( 𝑆 ↾ 𝐷 ) ) ⊆ ( Base ‘ 𝐺 )
18 16 6 cntzsubg ⊢ ( ( 𝐺 ∈ Grp ∧ ( 𝐺 DProd ( 𝑆 ↾ 𝐷 ) ) ⊆ ( Base ‘ 𝐺 ) ) → ( 𝑍 ‘ ( 𝐺 DProd ( 𝑆 ↾ 𝐷 ) ) ) ∈ ( SubGrp ‘ 𝐺 ) )
19 15 17 18 sylancl ⊢ ( 𝜑 → ( 𝑍 ‘ ( 𝐺 DProd ( 𝑆 ↾ 𝐷 ) ) ) ∈ ( SubGrp ‘ 𝐺 ) )
20 fvres ⊢ ( 𝑥 ∈ 𝐶 → ( ( 𝑆 ↾ 𝐶 ) ‘ 𝑥 ) = ( 𝑆 ‘ 𝑥 ) )
21 20 adantl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐶 ) → ( ( 𝑆 ↾ 𝐶 ) ‘ 𝑥 ) = ( 𝑆 ‘ 𝑥 ) )
22 1 2 4 dprdres ⊢ ( 𝜑 → ( 𝐺 dom DProd ( 𝑆 ↾ 𝐷 ) ∧ ( 𝐺 DProd ( 𝑆 ↾ 𝐷 ) ) ⊆ ( 𝐺 DProd 𝑆 ) ) )
23 22 simpld ⊢ ( 𝜑 → 𝐺 dom DProd ( 𝑆 ↾ 𝐷 ) )
24 23 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐶 ) → 𝐺 dom DProd ( 𝑆 ↾ 𝐷 ) )
25 dprdsubg ⊢ ( 𝐺 dom DProd ( 𝑆 ↾ 𝐷 ) → ( 𝐺 DProd ( 𝑆 ↾ 𝐷 ) ) ∈ ( SubGrp ‘ 𝐺 ) )
26 24 25 syl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐶 ) → ( 𝐺 DProd ( 𝑆 ↾ 𝐷 ) ) ∈ ( SubGrp ‘ 𝐺 ) )
27 3 sselda ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐶 ) → 𝑥 ∈ 𝐼 )
28 1 2 dprdf2 ⊢ ( 𝜑 → 𝑆 : 𝐼 ⟶ ( SubGrp ‘ 𝐺 ) )
29 28 ffvelrnda ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐼 ) → ( 𝑆 ‘ 𝑥 ) ∈ ( SubGrp ‘ 𝐺 ) )
30 27 29 syldan ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐶 ) → ( 𝑆 ‘ 𝑥 ) ∈ ( SubGrp ‘ 𝐺 ) )
31 dmres ⊢ dom ( 𝑆 ↾ 𝐷 ) = ( 𝐷 ∩ dom 𝑆 )
32 4 2 sseqtrrd ⊢ ( 𝜑 → 𝐷 ⊆ dom 𝑆 )
33 df-ss ⊢ ( 𝐷 ⊆ dom 𝑆 ↔ ( 𝐷 ∩ dom 𝑆 ) = 𝐷 )
34 32 33 sylib ⊢ ( 𝜑 → ( 𝐷 ∩ dom 𝑆 ) = 𝐷 )
35 31 34 syl5eq ⊢ ( 𝜑 → dom ( 𝑆 ↾ 𝐷 ) = 𝐷 )
36 35 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐶 ) → dom ( 𝑆 ↾ 𝐷 ) = 𝐷 )
37 15 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐶 ) → 𝐺 ∈ Grp )
38 16 subgss ⊢ ( ( 𝑆 ‘ 𝑥 ) ∈ ( SubGrp ‘ 𝐺 ) → ( 𝑆 ‘ 𝑥 ) ⊆ ( Base ‘ 𝐺 ) )
39 30 38 syl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐶 ) → ( 𝑆 ‘ 𝑥 ) ⊆ ( Base ‘ 𝐺 ) )
40 16 6 cntzsubg ⊢ ( ( 𝐺 ∈ Grp ∧ ( 𝑆 ‘ 𝑥 ) ⊆ ( Base ‘ 𝐺 ) ) → ( 𝑍 ‘ ( 𝑆 ‘ 𝑥 ) ) ∈ ( SubGrp ‘ 𝐺 ) )
41 37 39 40 syl2anc ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐶 ) → ( 𝑍 ‘ ( 𝑆 ‘ 𝑥 ) ) ∈ ( SubGrp ‘ 𝐺 ) )
42 fvres ⊢ ( 𝑦 ∈ 𝐷 → ( ( 𝑆 ↾ 𝐷 ) ‘ 𝑦 ) = ( 𝑆 ‘ 𝑦 ) )
43 42 adantl ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐶 ) ∧ 𝑦 ∈ 𝐷 ) → ( ( 𝑆 ↾ 𝐷 ) ‘ 𝑦 ) = ( 𝑆 ‘ 𝑦 ) )
44 1 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐶 ) ∧ 𝑦 ∈ 𝐷 ) → 𝐺 dom DProd 𝑆 )
45 2 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐶 ) ∧ 𝑦 ∈ 𝐷 ) → dom 𝑆 = 𝐼 )
46 4 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐶 ) → 𝐷 ⊆ 𝐼 )
47 46 sselda ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐶 ) ∧ 𝑦 ∈ 𝐷 ) → 𝑦 ∈ 𝐼 )
48 27 adantr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐶 ) ∧ 𝑦 ∈ 𝐷 ) → 𝑥 ∈ 𝐼 )
49 simpr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐶 ) ∧ 𝑦 ∈ 𝐷 ) → 𝑦 ∈ 𝐷 )
50 noel ⊢ ¬ 𝑥 ∈ ∅
51 elin ⊢ ( 𝑥 ∈ ( 𝐶 ∩ 𝐷 ) ↔ ( 𝑥 ∈ 𝐶 ∧ 𝑥 ∈ 𝐷 ) )
52 5 eleq2d ⊢ ( 𝜑 → ( 𝑥 ∈ ( 𝐶 ∩ 𝐷 ) ↔ 𝑥 ∈ ∅ ) )
53 51 52 bitr3id ⊢ ( 𝜑 → ( ( 𝑥 ∈ 𝐶 ∧ 𝑥 ∈ 𝐷 ) ↔ 𝑥 ∈ ∅ ) )
54 50 53 mtbiri ⊢ ( 𝜑 → ¬ ( 𝑥 ∈ 𝐶 ∧ 𝑥 ∈ 𝐷 ) )
55 imnan ⊢ ( ( 𝑥 ∈ 𝐶 → ¬ 𝑥 ∈ 𝐷 ) ↔ ¬ ( 𝑥 ∈ 𝐶 ∧ 𝑥 ∈ 𝐷 ) )
56 54 55 sylibr ⊢ ( 𝜑 → ( 𝑥 ∈ 𝐶 → ¬ 𝑥 ∈ 𝐷 ) )
57 56 imp ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐶 ) → ¬ 𝑥 ∈ 𝐷 )
58 57 adantr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐶 ) ∧ 𝑦 ∈ 𝐷 ) → ¬ 𝑥 ∈ 𝐷 )
59 nelne2 ⊢ ( ( 𝑦 ∈ 𝐷 ∧ ¬ 𝑥 ∈ 𝐷 ) → 𝑦 ≠ 𝑥 )
60 49 58 59 syl2anc ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐶 ) ∧ 𝑦 ∈ 𝐷 ) → 𝑦 ≠ 𝑥 )
61 44 45 47 48 60 6 dprdcntz ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐶 ) ∧ 𝑦 ∈ 𝐷 ) → ( 𝑆 ‘ 𝑦 ) ⊆ ( 𝑍 ‘ ( 𝑆 ‘ 𝑥 ) ) )
62 43 61 eqsstrd ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐶 ) ∧ 𝑦 ∈ 𝐷 ) → ( ( 𝑆 ↾ 𝐷 ) ‘ 𝑦 ) ⊆ ( 𝑍 ‘ ( 𝑆 ‘ 𝑥 ) ) )
63 24 36 41 62 dprdlub ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐶 ) → ( 𝐺 DProd ( 𝑆 ↾ 𝐷 ) ) ⊆ ( 𝑍 ‘ ( 𝑆 ‘ 𝑥 ) ) )
64 6 26 30 63 cntzrecd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐶 ) → ( 𝑆 ‘ 𝑥 ) ⊆ ( 𝑍 ‘ ( 𝐺 DProd ( 𝑆 ↾ 𝐷 ) ) ) )
65 21 64 eqsstrd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐶 ) → ( ( 𝑆 ↾ 𝐶 ) ‘ 𝑥 ) ⊆ ( 𝑍 ‘ ( 𝐺 DProd ( 𝑆 ↾ 𝐷 ) ) ) )
66 8 13 19 65 dprdlub ⊢ ( 𝜑 → ( 𝐺 DProd ( 𝑆 ↾ 𝐶 ) ) ⊆ ( 𝑍 ‘ ( 𝐺 DProd ( 𝑆 ↾ 𝐷 ) ) ) )