Metamath Proof Explorer


Theorem eldprdi

Description: The domain of definition of the internal direct product, which states that S is a family of subgroups that mutually commute and have trivial intersections. (Contributed by Mario Carneiro, 25-Apr-2016) (Revised by AV, 14-Jul-2019)

Ref Expression
Hypotheses eldprdi.0 0 = ( 0g𝐺 )
eldprdi.w 𝑊 = { X 𝑖𝐼 ( 𝑆𝑖 ) ∣ finSupp 0 }
eldprdi.1 ( 𝜑𝐺 dom DProd 𝑆 )
eldprdi.2 ( 𝜑 → dom 𝑆 = 𝐼 )
eldprdi.3 ( 𝜑𝐹𝑊 )
Assertion eldprdi ( 𝜑 → ( 𝐺 Σg 𝐹 ) ∈ ( 𝐺 DProd 𝑆 ) )

Proof

Step Hyp Ref Expression
1 eldprdi.0 0 = ( 0g𝐺 )
2 eldprdi.w 𝑊 = { X 𝑖𝐼 ( 𝑆𝑖 ) ∣ finSupp 0 }
3 eldprdi.1 ( 𝜑𝐺 dom DProd 𝑆 )
4 eldprdi.2 ( 𝜑 → dom 𝑆 = 𝐼 )
5 eldprdi.3 ( 𝜑𝐹𝑊 )
6 eqid ( 𝐺 Σg 𝐹 ) = ( 𝐺 Σg 𝐹 )
7 oveq2 ( 𝑓 = 𝐹 → ( 𝐺 Σg 𝑓 ) = ( 𝐺 Σg 𝐹 ) )
8 7 rspceeqv ( ( 𝐹𝑊 ∧ ( 𝐺 Σg 𝐹 ) = ( 𝐺 Σg 𝐹 ) ) → ∃ 𝑓𝑊 ( 𝐺 Σg 𝐹 ) = ( 𝐺 Σg 𝑓 ) )
9 5 6 8 sylancl ( 𝜑 → ∃ 𝑓𝑊 ( 𝐺 Σg 𝐹 ) = ( 𝐺 Σg 𝑓 ) )
10 1 2 eldprd ( dom 𝑆 = 𝐼 → ( ( 𝐺 Σg 𝐹 ) ∈ ( 𝐺 DProd 𝑆 ) ↔ ( 𝐺 dom DProd 𝑆 ∧ ∃ 𝑓𝑊 ( 𝐺 Σg 𝐹 ) = ( 𝐺 Σg 𝑓 ) ) ) )
11 4 10 syl ( 𝜑 → ( ( 𝐺 Σg 𝐹 ) ∈ ( 𝐺 DProd 𝑆 ) ↔ ( 𝐺 dom DProd 𝑆 ∧ ∃ 𝑓𝑊 ( 𝐺 Σg 𝐹 ) = ( 𝐺 Σg 𝑓 ) ) ) )
12 3 9 11 mpbir2and ( 𝜑 → ( 𝐺 Σg 𝐹 ) ∈ ( 𝐺 DProd 𝑆 ) )