Metamath Proof Explorer


Theorem dprd0

Description: The empty family is an internal direct product, the product of which is the trivial subgroup. (Contributed by Mario Carneiro, 25-Apr-2016)

Ref Expression
Hypothesis dprd0.0 0 = ( 0g𝐺 )
Assertion dprd0 ( 𝐺 ∈ Grp → ( 𝐺 dom DProd ∅ ∧ ( 𝐺 DProd ∅ ) = { 0 } ) )

Proof

Step Hyp Ref Expression
1 dprd0.0 0 = ( 0g𝐺 )
2 0ex ∅ ∈ V
3 1 dprdz ( ( 𝐺 ∈ Grp ∧ ∅ ∈ V ) → ( 𝐺 dom DProd ( 𝑥 ∈ ∅ ↦ { 0 } ) ∧ ( 𝐺 DProd ( 𝑥 ∈ ∅ ↦ { 0 } ) ) = { 0 } ) )
4 2 3 mpan2 ( 𝐺 ∈ Grp → ( 𝐺 dom DProd ( 𝑥 ∈ ∅ ↦ { 0 } ) ∧ ( 𝐺 DProd ( 𝑥 ∈ ∅ ↦ { 0 } ) ) = { 0 } ) )
5 mpt0 ( 𝑥 ∈ ∅ ↦ { 0 } ) = ∅
6 5 breq2i ( 𝐺 dom DProd ( 𝑥 ∈ ∅ ↦ { 0 } ) ↔ 𝐺 dom DProd ∅ )
7 5 oveq2i ( 𝐺 DProd ( 𝑥 ∈ ∅ ↦ { 0 } ) ) = ( 𝐺 DProd ∅ )
8 7 eqeq1i ( ( 𝐺 DProd ( 𝑥 ∈ ∅ ↦ { 0 } ) ) = { 0 } ↔ ( 𝐺 DProd ∅ ) = { 0 } )
9 6 8 anbi12i ( ( 𝐺 dom DProd ( 𝑥 ∈ ∅ ↦ { 0 } ) ∧ ( 𝐺 DProd ( 𝑥 ∈ ∅ ↦ { 0 } ) ) = { 0 } ) ↔ ( 𝐺 dom DProd ∅ ∧ ( 𝐺 DProd ∅ ) = { 0 } ) )
10 4 9 sylib ( 𝐺 ∈ Grp → ( 𝐺 dom DProd ∅ ∧ ( 𝐺 DProd ∅ ) = { 0 } ) )