Metamath Proof Explorer

Theorem dprdf1o

Description: Rearrange the index set of a direct product family. (Contributed by Mario Carneiro, 25-Apr-2016)

Ref Expression
Hypotheses dprdf1o.1 ⊢ ( 𝜑 → 𝐺 dom DProd 𝑆 )
dprdf1o.2 ⊢ ( 𝜑 → dom 𝑆 = 𝐼 )
dprdf1o.3 ⊢ ( 𝜑 → 𝐹 : 𝐽 –1-1-onto→ 𝐼 )
Assertion dprdf1o ( 𝜑 → ( 𝐺 dom DProd ( 𝑆 ∘ 𝐹 ) ∧ ( 𝐺 DProd ( 𝑆 ∘ 𝐹 ) ) = ( 𝐺 DProd 𝑆 ) ) )

Proof

Step Hyp Ref Expression
1 dprdf1o.1 ⊢ ( 𝜑 → 𝐺 dom DProd 𝑆 )
2 dprdf1o.2 ⊢ ( 𝜑 → dom 𝑆 = 𝐼 )
3 dprdf1o.3 ⊢ ( 𝜑 → 𝐹 : 𝐽 –1-1-onto→ 𝐼 )
4 eqid ⊢ ( Cntz ‘ 𝐺 ) = ( Cntz ‘ 𝐺 )
5 eqid ⊢ ( 0g ‘ 𝐺 ) = ( 0g ‘ 𝐺 )
6 eqid ⊢ ( mrCls ‘ ( SubGrp ‘ 𝐺 ) ) = ( mrCls ‘ ( SubGrp ‘ 𝐺 ) )
7 dprdgrp ⊢ ( 𝐺 dom DProd 𝑆 → 𝐺 ∈ Grp )
8 1 7 syl ⊢ ( 𝜑 → 𝐺 ∈ Grp )
9 f1of1 ⊢ ( 𝐹 : 𝐽 –1-1-onto→ 𝐼 → 𝐹 : 𝐽 –1-1→ 𝐼 )
10 3 9 syl ⊢ ( 𝜑 → 𝐹 : 𝐽 –1-1→ 𝐼 )
11 1 2 dprddomcld ⊢ ( 𝜑 → 𝐼 ∈ V )
12 f1dmex ⊢ ( ( 𝐹 : 𝐽 –1-1→ 𝐼 ∧ 𝐼 ∈ V ) → 𝐽 ∈ V )
13 10 11 12 syl2anc ⊢ ( 𝜑 → 𝐽 ∈ V )
14 1 2 dprdf2 ⊢ ( 𝜑 → 𝑆 : 𝐼 ⟶ ( SubGrp ‘ 𝐺 ) )
15 f1of ⊢ ( 𝐹 : 𝐽 –1-1-onto→ 𝐼 → 𝐹 : 𝐽 ⟶ 𝐼 )
16 3 15 syl ⊢ ( 𝜑 → 𝐹 : 𝐽 ⟶ 𝐼 )
17 fco ⊢ ( ( 𝑆 : 𝐼 ⟶ ( SubGrp ‘ 𝐺 ) ∧ 𝐹 : 𝐽 ⟶ 𝐼 ) → ( 𝑆 ∘ 𝐹 ) : 𝐽 ⟶ ( SubGrp ‘ 𝐺 ) )
18 14 16 17 syl2anc ⊢ ( 𝜑 → ( 𝑆 ∘ 𝐹 ) : 𝐽 ⟶ ( SubGrp ‘ 𝐺 ) )
19 1 adantr ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝐽 ∧ 𝑥 ≠ 𝑦 ) ) → 𝐺 dom DProd 𝑆 )
20 2 adantr ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝐽 ∧ 𝑥 ≠ 𝑦 ) ) → dom 𝑆 = 𝐼 )
21 16 adantr ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝐽 ∧ 𝑥 ≠ 𝑦 ) ) → 𝐹 : 𝐽 ⟶ 𝐼 )
22 simpr1 ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝐽 ∧ 𝑥 ≠ 𝑦 ) ) → 𝑥 ∈ 𝐽 )
23 21 22 ffvelrnd ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝐽 ∧ 𝑥 ≠ 𝑦 ) ) → ( 𝐹 ‘ 𝑥 ) ∈ 𝐼 )
24 simpr2 ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝐽 ∧ 𝑥 ≠ 𝑦 ) ) → 𝑦 ∈ 𝐽 )
25 21 24 ffvelrnd ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝐽 ∧ 𝑥 ≠ 𝑦 ) ) → ( 𝐹 ‘ 𝑦 ) ∈ 𝐼 )
26 simpr3 ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝐽 ∧ 𝑥 ≠ 𝑦 ) ) → 𝑥 ≠ 𝑦 )
27 10 adantr ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝐽 ∧ 𝑥 ≠ 𝑦 ) ) → 𝐹 : 𝐽 –1-1→ 𝐼 )
28 f1fveq ⊢ ( ( 𝐹 : 𝐽 –1-1→ 𝐼 ∧ ( 𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝐽 ) ) → ( ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) ↔ 𝑥 = 𝑦 ) )
29 27 22 24 28 syl12anc ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝐽 ∧ 𝑥 ≠ 𝑦 ) ) → ( ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) ↔ 𝑥 = 𝑦 ) )
30 29 necon3bid ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝐽 ∧ 𝑥 ≠ 𝑦 ) ) → ( ( 𝐹 ‘ 𝑥 ) ≠ ( 𝐹 ‘ 𝑦 ) ↔ 𝑥 ≠ 𝑦 ) )
31 26 30 mpbird ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝐽 ∧ 𝑥 ≠ 𝑦 ) ) → ( 𝐹 ‘ 𝑥 ) ≠ ( 𝐹 ‘ 𝑦 ) )
32 19 20 23 25 31 4 dprdcntz ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝐽 ∧ 𝑥 ≠ 𝑦 ) ) → ( 𝑆 ‘ ( 𝐹 ‘ 𝑥 ) ) ⊆ ( ( Cntz ‘ 𝐺 ) ‘ ( 𝑆 ‘ ( 𝐹 ‘ 𝑦 ) ) ) )
33 fvco3 ⊢ ( ( 𝐹 : 𝐽 ⟶ 𝐼 ∧ 𝑥 ∈ 𝐽 ) → ( ( 𝑆 ∘ 𝐹 ) ‘ 𝑥 ) = ( 𝑆 ‘ ( 𝐹 ‘ 𝑥 ) ) )
34 21 22 33 syl2anc ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝐽 ∧ 𝑥 ≠ 𝑦 ) ) → ( ( 𝑆 ∘ 𝐹 ) ‘ 𝑥 ) = ( 𝑆 ‘ ( 𝐹 ‘ 𝑥 ) ) )
35 fvco3 ⊢ ( ( 𝐹 : 𝐽 ⟶ 𝐼 ∧ 𝑦 ∈ 𝐽 ) → ( ( 𝑆 ∘ 𝐹 ) ‘ 𝑦 ) = ( 𝑆 ‘ ( 𝐹 ‘ 𝑦 ) ) )
36 21 24 35 syl2anc ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝐽 ∧ 𝑥 ≠ 𝑦 ) ) → ( ( 𝑆 ∘ 𝐹 ) ‘ 𝑦 ) = ( 𝑆 ‘ ( 𝐹 ‘ 𝑦 ) ) )
37 36 fveq2d ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝐽 ∧ 𝑥 ≠ 𝑦 ) ) → ( ( Cntz ‘ 𝐺 ) ‘ ( ( 𝑆 ∘ 𝐹 ) ‘ 𝑦 ) ) = ( ( Cntz ‘ 𝐺 ) ‘ ( 𝑆 ‘ ( 𝐹 ‘ 𝑦 ) ) ) )
38 32 34 37 3sstr4d ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝐽 ∧ 𝑥 ≠ 𝑦 ) ) → ( ( 𝑆 ∘ 𝐹 ) ‘ 𝑥 ) ⊆ ( ( Cntz ‘ 𝐺 ) ‘ ( ( 𝑆 ∘ 𝐹 ) ‘ 𝑦 ) ) )
39 16 33 sylan ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐽 ) → ( ( 𝑆 ∘ 𝐹 ) ‘ 𝑥 ) = ( 𝑆 ‘ ( 𝐹 ‘ 𝑥 ) ) )
40 imaco ⊢ ( ( 𝑆 ∘ 𝐹 ) “ ( 𝐽 ∖ { 𝑥 } ) ) = ( 𝑆 “ ( 𝐹 “ ( 𝐽 ∖ { 𝑥 } ) ) )
41 3 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐽 ) → 𝐹 : 𝐽 –1-1-onto→ 𝐼 )
42 dff1o3 ⊢ ( 𝐹 : 𝐽 –1-1-onto→ 𝐼 ↔ ( 𝐹 : 𝐽 –onto→ 𝐼 ∧ Fun ◡ 𝐹 ) )
43 42 simprbi ⊢ ( 𝐹 : 𝐽 –1-1-onto→ 𝐼 → Fun ◡ 𝐹 )
44 imadif ⊢ ( Fun ◡ 𝐹 → ( 𝐹 “ ( 𝐽 ∖ { 𝑥 } ) ) = ( ( 𝐹 “ 𝐽 ) ∖ ( 𝐹 “ { 𝑥 } ) ) )
45 41 43 44 3syl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐽 ) → ( 𝐹 “ ( 𝐽 ∖ { 𝑥 } ) ) = ( ( 𝐹 “ 𝐽 ) ∖ ( 𝐹 “ { 𝑥 } ) ) )
46 f1ofo ⊢ ( 𝐹 : 𝐽 –1-1-onto→ 𝐼 → 𝐹 : 𝐽 –onto→ 𝐼 )
47 foima ⊢ ( 𝐹 : 𝐽 –onto→ 𝐼 → ( 𝐹 “ 𝐽 ) = 𝐼 )
48 41 46 47 3syl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐽 ) → ( 𝐹 “ 𝐽 ) = 𝐼 )
49 f1ofn ⊢ ( 𝐹 : 𝐽 –1-1-onto→ 𝐼 → 𝐹 Fn 𝐽 )
50 3 49 syl ⊢ ( 𝜑 → 𝐹 Fn 𝐽 )
51 fnsnfv ⊢ ( ( 𝐹 Fn 𝐽 ∧ 𝑥 ∈ 𝐽 ) → { ( 𝐹 ‘ 𝑥 ) } = ( 𝐹 “ { 𝑥 } ) )
52 50 51 sylan ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐽 ) → { ( 𝐹 ‘ 𝑥 ) } = ( 𝐹 “ { 𝑥 } ) )
53 52 eqcomd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐽 ) → ( 𝐹 “ { 𝑥 } ) = { ( 𝐹 ‘ 𝑥 ) } )
54 48 53 difeq12d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐽 ) → ( ( 𝐹 “ 𝐽 ) ∖ ( 𝐹 “ { 𝑥 } ) ) = ( 𝐼 ∖ { ( 𝐹 ‘ 𝑥 ) } ) )
55 45 54 eqtrd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐽 ) → ( 𝐹 “ ( 𝐽 ∖ { 𝑥 } ) ) = ( 𝐼 ∖ { ( 𝐹 ‘ 𝑥 ) } ) )
56 55 imaeq2d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐽 ) → ( 𝑆 “ ( 𝐹 “ ( 𝐽 ∖ { 𝑥 } ) ) ) = ( 𝑆 “ ( 𝐼 ∖ { ( 𝐹 ‘ 𝑥 ) } ) ) )
57 40 56 syl5eq ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐽 ) → ( ( 𝑆 ∘ 𝐹 ) “ ( 𝐽 ∖ { 𝑥 } ) ) = ( 𝑆 “ ( 𝐼 ∖ { ( 𝐹 ‘ 𝑥 ) } ) ) )
58 57 unieqd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐽 ) → ∪ ( ( 𝑆 ∘ 𝐹 ) “ ( 𝐽 ∖ { 𝑥 } ) ) = ∪ ( 𝑆 “ ( 𝐼 ∖ { ( 𝐹 ‘ 𝑥 ) } ) ) )
59 58 fveq2d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐽 ) → ( ( mrCls ‘ ( SubGrp ‘ 𝐺 ) ) ‘ ∪ ( ( 𝑆 ∘ 𝐹 ) “ ( 𝐽 ∖ { 𝑥 } ) ) ) = ( ( mrCls ‘ ( SubGrp ‘ 𝐺 ) ) ‘ ∪ ( 𝑆 “ ( 𝐼 ∖ { ( 𝐹 ‘ 𝑥 ) } ) ) ) )
60 39 59 ineq12d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐽 ) → ( ( ( 𝑆 ∘ 𝐹 ) ‘ 𝑥 ) ∩ ( ( mrCls ‘ ( SubGrp ‘ 𝐺 ) ) ‘ ∪ ( ( 𝑆 ∘ 𝐹 ) “ ( 𝐽 ∖ { 𝑥 } ) ) ) ) = ( ( 𝑆 ‘ ( 𝐹 ‘ 𝑥 ) ) ∩ ( ( mrCls ‘ ( SubGrp ‘ 𝐺 ) ) ‘ ∪ ( 𝑆 “ ( 𝐼 ∖ { ( 𝐹 ‘ 𝑥 ) } ) ) ) ) )
61 1 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐽 ) → 𝐺 dom DProd 𝑆 )
62 2 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐽 ) → dom 𝑆 = 𝐼 )
63 16 ffvelrnda ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐽 ) → ( 𝐹 ‘ 𝑥 ) ∈ 𝐼 )
64 61 62 63 5 6 dprddisj ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐽 ) → ( ( 𝑆 ‘ ( 𝐹 ‘ 𝑥 ) ) ∩ ( ( mrCls ‘ ( SubGrp ‘ 𝐺 ) ) ‘ ∪ ( 𝑆 “ ( 𝐼 ∖ { ( 𝐹 ‘ 𝑥 ) } ) ) ) ) = { ( 0g ‘ 𝐺 ) } )
65 60 64 eqtrd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐽 ) → ( ( ( 𝑆 ∘ 𝐹 ) ‘ 𝑥 ) ∩ ( ( mrCls ‘ ( SubGrp ‘ 𝐺 ) ) ‘ ∪ ( ( 𝑆 ∘ 𝐹 ) “ ( 𝐽 ∖ { 𝑥 } ) ) ) ) = { ( 0g ‘ 𝐺 ) } )
66 eqimss ⊢ ( ( ( ( 𝑆 ∘ 𝐹 ) ‘ 𝑥 ) ∩ ( ( mrCls ‘ ( SubGrp ‘ 𝐺 ) ) ‘ ∪ ( ( 𝑆 ∘ 𝐹 ) “ ( 𝐽 ∖ { 𝑥 } ) ) ) ) = { ( 0g ‘ 𝐺 ) } → ( ( ( 𝑆 ∘ 𝐹 ) ‘ 𝑥 ) ∩ ( ( mrCls ‘ ( SubGrp ‘ 𝐺 ) ) ‘ ∪ ( ( 𝑆 ∘ 𝐹 ) “ ( 𝐽 ∖ { 𝑥 } ) ) ) ) ⊆ { ( 0g ‘ 𝐺 ) } )
67 65 66 syl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐽 ) → ( ( ( 𝑆 ∘ 𝐹 ) ‘ 𝑥 ) ∩ ( ( mrCls ‘ ( SubGrp ‘ 𝐺 ) ) ‘ ∪ ( ( 𝑆 ∘ 𝐹 ) “ ( 𝐽 ∖ { 𝑥 } ) ) ) ) ⊆ { ( 0g ‘ 𝐺 ) } )
68 4 5 6 8 13 18 38 67 dmdprdd ⊢ ( 𝜑 → 𝐺 dom DProd ( 𝑆 ∘ 𝐹 ) )
69 rnco2 ⊢ ran ( 𝑆 ∘ 𝐹 ) = ( 𝑆 “ ran 𝐹 )
70 forn ⊢ ( 𝐹 : 𝐽 –onto→ 𝐼 → ran 𝐹 = 𝐼 )
71 3 46 70 3syl ⊢ ( 𝜑 → ran 𝐹 = 𝐼 )
72 71 imaeq2d ⊢ ( 𝜑 → ( 𝑆 “ ran 𝐹 ) = ( 𝑆 “ 𝐼 ) )
73 ffn ⊢ ( 𝑆 : 𝐼 ⟶ ( SubGrp ‘ 𝐺 ) → 𝑆 Fn 𝐼 )
74 fnima ⊢ ( 𝑆 Fn 𝐼 → ( 𝑆 “ 𝐼 ) = ran 𝑆 )
75 14 73 74 3syl ⊢ ( 𝜑 → ( 𝑆 “ 𝐼 ) = ran 𝑆 )
76 72 75 eqtrd ⊢ ( 𝜑 → ( 𝑆 “ ran 𝐹 ) = ran 𝑆 )
77 69 76 syl5eq ⊢ ( 𝜑 → ran ( 𝑆 ∘ 𝐹 ) = ran 𝑆 )
78 77 unieqd ⊢ ( 𝜑 → ∪ ran ( 𝑆 ∘ 𝐹 ) = ∪ ran 𝑆 )
79 78 fveq2d ⊢ ( 𝜑 → ( ( mrCls ‘ ( SubGrp ‘ 𝐺 ) ) ‘ ∪ ran ( 𝑆 ∘ 𝐹 ) ) = ( ( mrCls ‘ ( SubGrp ‘ 𝐺 ) ) ‘ ∪ ran 𝑆 ) )
80 6 dprdspan ⊢ ( 𝐺 dom DProd ( 𝑆 ∘ 𝐹 ) → ( 𝐺 DProd ( 𝑆 ∘ 𝐹 ) ) = ( ( mrCls ‘ ( SubGrp ‘ 𝐺 ) ) ‘ ∪ ran ( 𝑆 ∘ 𝐹 ) ) )
81 68 80 syl ⊢ ( 𝜑 → ( 𝐺 DProd ( 𝑆 ∘ 𝐹 ) ) = ( ( mrCls ‘ ( SubGrp ‘ 𝐺 ) ) ‘ ∪ ran ( 𝑆 ∘ 𝐹 ) ) )
82 6 dprdspan ⊢ ( 𝐺 dom DProd 𝑆 → ( 𝐺 DProd 𝑆 ) = ( ( mrCls ‘ ( SubGrp ‘ 𝐺 ) ) ‘ ∪ ran 𝑆 ) )
83 1 82 syl ⊢ ( 𝜑 → ( 𝐺 DProd 𝑆 ) = ( ( mrCls ‘ ( SubGrp ‘ 𝐺 ) ) ‘ ∪ ran 𝑆 ) )
84 79 81 83 3eqtr4d ⊢ ( 𝜑 → ( 𝐺 DProd ( 𝑆 ∘ 𝐹 ) ) = ( 𝐺 DProd 𝑆 ) )
85 68 84 jca ⊢ ( 𝜑 → ( 𝐺 dom DProd ( 𝑆 ∘ 𝐹 ) ∧ ( 𝐺 DProd ( 𝑆 ∘ 𝐹 ) ) = ( 𝐺 DProd 𝑆 ) ) )