This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem dpjcntz

Description: The two subgroups that appear in dpjval commute. (Contributed by Mario Carneiro, 26-Apr-2016)

Ref Expression
Hypotheses dpjfval.1 ⊢ ( 𝜑 → 𝐺 dom DProd 𝑆 )
dpjfval.2 ⊢ ( 𝜑 → dom 𝑆 = 𝐼 )
dpjlem.3 ⊢ ( 𝜑 → 𝑋 ∈ 𝐼 )
dpjcntz.z ⊢ 𝑍 = ( Cntz ‘ 𝐺 )
Assertion dpjcntz ( 𝜑 → ( 𝑆 ‘ 𝑋 ) ⊆ ( 𝑍 ‘ ( 𝐺 DProd ( 𝑆 ↾ ( 𝐼 ∖ { 𝑋 } ) ) ) ) )

Proof

Step Hyp Ref Expression
1 dpjfval.1 ⊢ ( 𝜑 → 𝐺 dom DProd 𝑆 )
2 dpjfval.2 ⊢ ( 𝜑 → dom 𝑆 = 𝐼 )
3 dpjlem.3 ⊢ ( 𝜑 → 𝑋 ∈ 𝐼 )
4 dpjcntz.z ⊢ 𝑍 = ( Cntz ‘ 𝐺 )
5 1 2 3 dpjlem ⊢ ( 𝜑 → ( 𝐺 DProd ( 𝑆 ↾ { 𝑋 } ) ) = ( 𝑆 ‘ 𝑋 ) )
6 1 2 dprdf2 ⊢ ( 𝜑 → 𝑆 : 𝐼 ⟶ ( SubGrp ‘ 𝐺 ) )
7 disjdif ⊢ ( { 𝑋 } ∩ ( 𝐼 ∖ { 𝑋 } ) ) = ∅
8 7 a1i ⊢ ( 𝜑 → ( { 𝑋 } ∩ ( 𝐼 ∖ { 𝑋 } ) ) = ∅ )
9 undif2 ⊢ ( { 𝑋 } ∪ ( 𝐼 ∖ { 𝑋 } ) ) = ( { 𝑋 } ∪ 𝐼 )
10 3 snssd ⊢ ( 𝜑 → { 𝑋 } ⊆ 𝐼 )
11 ssequn1 ⊢ ( { 𝑋 } ⊆ 𝐼 ↔ ( { 𝑋 } ∪ 𝐼 ) = 𝐼 )
12 10 11 sylib ⊢ ( 𝜑 → ( { 𝑋 } ∪ 𝐼 ) = 𝐼 )
13 9 12 eqtr2id ⊢ ( 𝜑 → 𝐼 = ( { 𝑋 } ∪ ( 𝐼 ∖ { 𝑋 } ) ) )
14 eqid ⊢ ( 0g ‘ 𝐺 ) = ( 0g ‘ 𝐺 )
15 6 8 13 4 14 dmdprdsplit ⊢ ( 𝜑 → ( 𝐺 dom DProd 𝑆 ↔ ( ( 𝐺 dom DProd ( 𝑆 ↾ { 𝑋 } ) ∧ 𝐺 dom DProd ( 𝑆 ↾ ( 𝐼 ∖ { 𝑋 } ) ) ) ∧ ( 𝐺 DProd ( 𝑆 ↾ { 𝑋 } ) ) ⊆ ( 𝑍 ‘ ( 𝐺 DProd ( 𝑆 ↾ ( 𝐼 ∖ { 𝑋 } ) ) ) ) ∧ ( ( 𝐺 DProd ( 𝑆 ↾ { 𝑋 } ) ) ∩ ( 𝐺 DProd ( 𝑆 ↾ ( 𝐼 ∖ { 𝑋 } ) ) ) ) = { ( 0g ‘ 𝐺 ) } ) ) )
16 1 15 mpbid ⊢ ( 𝜑 → ( ( 𝐺 dom DProd ( 𝑆 ↾ { 𝑋 } ) ∧ 𝐺 dom DProd ( 𝑆 ↾ ( 𝐼 ∖ { 𝑋 } ) ) ) ∧ ( 𝐺 DProd ( 𝑆 ↾ { 𝑋 } ) ) ⊆ ( 𝑍 ‘ ( 𝐺 DProd ( 𝑆 ↾ ( 𝐼 ∖ { 𝑋 } ) ) ) ) ∧ ( ( 𝐺 DProd ( 𝑆 ↾ { 𝑋 } ) ) ∩ ( 𝐺 DProd ( 𝑆 ↾ ( 𝐼 ∖ { 𝑋 } ) ) ) ) = { ( 0g ‘ 𝐺 ) } ) )
17 16 simp2d ⊢ ( 𝜑 → ( 𝐺 DProd ( 𝑆 ↾ { 𝑋 } ) ) ⊆ ( 𝑍 ‘ ( 𝐺 DProd ( 𝑆 ↾ ( 𝐼 ∖ { 𝑋 } ) ) ) ) )
18 5 17 eqsstrrd ⊢ ( 𝜑 → ( 𝑆 ‘ 𝑋 ) ⊆ ( 𝑍 ‘ ( 𝐺 DProd ( 𝑆 ↾ ( 𝐼 ∖ { 𝑋 } ) ) ) ) )