Metamath Proof Explorer

Theorem dprdcntz

Description: The function S is a family having pairwise commuting values. (Contributed by Mario Carneiro, 25-Apr-2016)

Ref Expression
Hypotheses dprdcntz.1 ⊢ ( 𝜑 → 𝐺 dom DProd 𝑆 )
dprdcntz.2 ⊢ ( 𝜑 → dom 𝑆 = 𝐼 )
dprdcntz.3 ⊢ ( 𝜑 → 𝑋 ∈ 𝐼 )
dprdcntz.4 ⊢ ( 𝜑 → 𝑌 ∈ 𝐼 )
dprdcntz.5 ⊢ ( 𝜑 → 𝑋 ≠ 𝑌 )
dprdcntz.z ⊢ 𝑍 = ( Cntz ‘ 𝐺 )
Assertion dprdcntz ( 𝜑 → ( 𝑆 ‘ 𝑋 ) ⊆ ( 𝑍 ‘ ( 𝑆 ‘ 𝑌 ) ) )

Proof

Step Hyp Ref Expression
1 dprdcntz.1 ⊢ ( 𝜑 → 𝐺 dom DProd 𝑆 )
2 dprdcntz.2 ⊢ ( 𝜑 → dom 𝑆 = 𝐼 )
3 dprdcntz.3 ⊢ ( 𝜑 → 𝑋 ∈ 𝐼 )
4 dprdcntz.4 ⊢ ( 𝜑 → 𝑌 ∈ 𝐼 )
5 dprdcntz.5 ⊢ ( 𝜑 → 𝑋 ≠ 𝑌 )
6 dprdcntz.z ⊢ 𝑍 = ( Cntz ‘ 𝐺 )
7 2fveq3 ⊢ ( 𝑦 = 𝑌 → ( 𝑍 ‘ ( 𝑆 ‘ 𝑦 ) ) = ( 𝑍 ‘ ( 𝑆 ‘ 𝑌 ) ) )
8 7 sseq2d ⊢ ( 𝑦 = 𝑌 → ( ( 𝑆 ‘ 𝑋 ) ⊆ ( 𝑍 ‘ ( 𝑆 ‘ 𝑦 ) ) ↔ ( 𝑆 ‘ 𝑋 ) ⊆ ( 𝑍 ‘ ( 𝑆 ‘ 𝑌 ) ) ) )
9 sneq ⊢ ( 𝑥 = 𝑋 → { 𝑥 } = { 𝑋 } )
10 9 difeq2d ⊢ ( 𝑥 = 𝑋 → ( 𝐼 ∖ { 𝑥 } ) = ( 𝐼 ∖ { 𝑋 } ) )
11 fveq2 ⊢ ( 𝑥 = 𝑋 → ( 𝑆 ‘ 𝑥 ) = ( 𝑆 ‘ 𝑋 ) )
12 11 sseq1d ⊢ ( 𝑥 = 𝑋 → ( ( 𝑆 ‘ 𝑥 ) ⊆ ( 𝑍 ‘ ( 𝑆 ‘ 𝑦 ) ) ↔ ( 𝑆 ‘ 𝑋 ) ⊆ ( 𝑍 ‘ ( 𝑆 ‘ 𝑦 ) ) ) )
13 10 12 raleqbidv ⊢ ( 𝑥 = 𝑋 → ( ∀ 𝑦 ∈ ( 𝐼 ∖ { 𝑥 } ) ( 𝑆 ‘ 𝑥 ) ⊆ ( 𝑍 ‘ ( 𝑆 ‘ 𝑦 ) ) ↔ ∀ 𝑦 ∈ ( 𝐼 ∖ { 𝑋 } ) ( 𝑆 ‘ 𝑋 ) ⊆ ( 𝑍 ‘ ( 𝑆 ‘ 𝑦 ) ) ) )
14 1 2 dprddomcld ⊢ ( 𝜑 → 𝐼 ∈ V )
15 eqid ⊢ ( 0g ‘ 𝐺 ) = ( 0g ‘ 𝐺 )
16 eqid ⊢ ( mrCls ‘ ( SubGrp ‘ 𝐺 ) ) = ( mrCls ‘ ( SubGrp ‘ 𝐺 ) )
17 6 15 16 dmdprd ⊢ ( ( 𝐼 ∈ V ∧ dom 𝑆 = 𝐼 ) → ( 𝐺 dom DProd 𝑆 ↔ ( 𝐺 ∈ Grp ∧ 𝑆 : 𝐼 ⟶ ( SubGrp ‘ 𝐺 ) ∧ ∀ 𝑥 ∈ 𝐼 ( ∀ 𝑦 ∈ ( 𝐼 ∖ { 𝑥 } ) ( 𝑆 ‘ 𝑥 ) ⊆ ( 𝑍 ‘ ( 𝑆 ‘ 𝑦 ) ) ∧ ( ( 𝑆 ‘ 𝑥 ) ∩ ( ( mrCls ‘ ( SubGrp ‘ 𝐺 ) ) ‘ ∪ ( 𝑆 “ ( 𝐼 ∖ { 𝑥 } ) ) ) ) = { ( 0g ‘ 𝐺 ) } ) ) ) )
18 14 2 17 syl2anc ⊢ ( 𝜑 → ( 𝐺 dom DProd 𝑆 ↔ ( 𝐺 ∈ Grp ∧ 𝑆 : 𝐼 ⟶ ( SubGrp ‘ 𝐺 ) ∧ ∀ 𝑥 ∈ 𝐼 ( ∀ 𝑦 ∈ ( 𝐼 ∖ { 𝑥 } ) ( 𝑆 ‘ 𝑥 ) ⊆ ( 𝑍 ‘ ( 𝑆 ‘ 𝑦 ) ) ∧ ( ( 𝑆 ‘ 𝑥 ) ∩ ( ( mrCls ‘ ( SubGrp ‘ 𝐺 ) ) ‘ ∪ ( 𝑆 “ ( 𝐼 ∖ { 𝑥 } ) ) ) ) = { ( 0g ‘ 𝐺 ) } ) ) ) )
19 1 18 mpbid ⊢ ( 𝜑 → ( 𝐺 ∈ Grp ∧ 𝑆 : 𝐼 ⟶ ( SubGrp ‘ 𝐺 ) ∧ ∀ 𝑥 ∈ 𝐼 ( ∀ 𝑦 ∈ ( 𝐼 ∖ { 𝑥 } ) ( 𝑆 ‘ 𝑥 ) ⊆ ( 𝑍 ‘ ( 𝑆 ‘ 𝑦 ) ) ∧ ( ( 𝑆 ‘ 𝑥 ) ∩ ( ( mrCls ‘ ( SubGrp ‘ 𝐺 ) ) ‘ ∪ ( 𝑆 “ ( 𝐼 ∖ { 𝑥 } ) ) ) ) = { ( 0g ‘ 𝐺 ) } ) ) )
20 19 simp3d ⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝐼 ( ∀ 𝑦 ∈ ( 𝐼 ∖ { 𝑥 } ) ( 𝑆 ‘ 𝑥 ) ⊆ ( 𝑍 ‘ ( 𝑆 ‘ 𝑦 ) ) ∧ ( ( 𝑆 ‘ 𝑥 ) ∩ ( ( mrCls ‘ ( SubGrp ‘ 𝐺 ) ) ‘ ∪ ( 𝑆 “ ( 𝐼 ∖ { 𝑥 } ) ) ) ) = { ( 0g ‘ 𝐺 ) } ) )
21 simpl ⊢ ( ( ∀ 𝑦 ∈ ( 𝐼 ∖ { 𝑥 } ) ( 𝑆 ‘ 𝑥 ) ⊆ ( 𝑍 ‘ ( 𝑆 ‘ 𝑦 ) ) ∧ ( ( 𝑆 ‘ 𝑥 ) ∩ ( ( mrCls ‘ ( SubGrp ‘ 𝐺 ) ) ‘ ∪ ( 𝑆 “ ( 𝐼 ∖ { 𝑥 } ) ) ) ) = { ( 0g ‘ 𝐺 ) } ) → ∀ 𝑦 ∈ ( 𝐼 ∖ { 𝑥 } ) ( 𝑆 ‘ 𝑥 ) ⊆ ( 𝑍 ‘ ( 𝑆 ‘ 𝑦 ) ) )
22 21 ralimi ⊢ ( ∀ 𝑥 ∈ 𝐼 ( ∀ 𝑦 ∈ ( 𝐼 ∖ { 𝑥 } ) ( 𝑆 ‘ 𝑥 ) ⊆ ( 𝑍 ‘ ( 𝑆 ‘ 𝑦 ) ) ∧ ( ( 𝑆 ‘ 𝑥 ) ∩ ( ( mrCls ‘ ( SubGrp ‘ 𝐺 ) ) ‘ ∪ ( 𝑆 “ ( 𝐼 ∖ { 𝑥 } ) ) ) ) = { ( 0g ‘ 𝐺 ) } ) → ∀ 𝑥 ∈ 𝐼 ∀ 𝑦 ∈ ( 𝐼 ∖ { 𝑥 } ) ( 𝑆 ‘ 𝑥 ) ⊆ ( 𝑍 ‘ ( 𝑆 ‘ 𝑦 ) ) )
23 20 22 syl ⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝐼 ∀ 𝑦 ∈ ( 𝐼 ∖ { 𝑥 } ) ( 𝑆 ‘ 𝑥 ) ⊆ ( 𝑍 ‘ ( 𝑆 ‘ 𝑦 ) ) )
24 13 23 3 rspcdva ⊢ ( 𝜑 → ∀ 𝑦 ∈ ( 𝐼 ∖ { 𝑋 } ) ( 𝑆 ‘ 𝑋 ) ⊆ ( 𝑍 ‘ ( 𝑆 ‘ 𝑦 ) ) )
25 5 necomd ⊢ ( 𝜑 → 𝑌 ≠ 𝑋 )
26 eldifsn ⊢ ( 𝑌 ∈ ( 𝐼 ∖ { 𝑋 } ) ↔ ( 𝑌 ∈ 𝐼 ∧ 𝑌 ≠ 𝑋 ) )
27 4 25 26 sylanbrc ⊢ ( 𝜑 → 𝑌 ∈ ( 𝐼 ∖ { 𝑋 } ) )
28 8 24 27 rspcdva ⊢ ( 𝜑 → ( 𝑆 ‘ 𝑋 ) ⊆ ( 𝑍 ‘ ( 𝑆 ‘ 𝑌 ) ) )