Description: The domain of the internal direct product operation is a relation. (Contributed by Mario Carneiro, 25-Apr-2016) (Proof shortened by AV, 11-Jul-2019)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | reldmdprd | ⊢ Rel dom DProd |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | df-dprd | ⊢ DProd = ( 𝑔 ∈ Grp , 𝑠 ∈ { ℎ ∣ ( ℎ : dom ℎ ⟶ ( SubGrp ‘ 𝑔 ) ∧ ∀ 𝑥 ∈ dom ℎ ( ∀ 𝑦 ∈ ( dom ℎ ∖ { 𝑥 } ) ( ℎ ‘ 𝑥 ) ⊆ ( ( Cntz ‘ 𝑔 ) ‘ ( ℎ ‘ 𝑦 ) ) ∧ ( ( ℎ ‘ 𝑥 ) ∩ ( ( mrCls ‘ ( SubGrp ‘ 𝑔 ) ) ‘ ∪ ( ℎ “ ( dom ℎ ∖ { 𝑥 } ) ) ) ) = { ( 0g ‘ 𝑔 ) } ) ) } ↦ ran ( 𝑓 ∈ { ℎ ∈ X 𝑥 ∈ dom 𝑠 ( 𝑠 ‘ 𝑥 ) ∣ ℎ finSupp ( 0g ‘ 𝑔 ) } ↦ ( 𝑔 Σg 𝑓 ) ) ) | |
| 2 | 1 | reldmmpo | ⊢ Rel dom DProd |