MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  dprd2d2 Structured version   Visualization version   GIF version

Theorem dprd2d2 18641
Description: The direct product of a collection of direct products. (Contributed by Mario Carneiro, 26-Apr-2016.)
Hypotheses
Ref Expression
dprd2d2.1 ((𝜑 ∧ (𝑖𝐼𝑗𝐽)) → 𝑆 ∈ (SubGrp‘𝐺))
dprd2d2.2 ((𝜑𝑖𝐼) → 𝐺dom DProd (𝑗𝐽𝑆))
dprd2d2.3 (𝜑𝐺dom DProd (𝑖𝐼 ↦ (𝐺 DProd (𝑗𝐽𝑆))))
Assertion
Ref Expression
dprd2d2 (𝜑 → (𝐺dom DProd (𝑖𝐼, 𝑗𝐽𝑆) ∧ (𝐺 DProd (𝑖𝐼, 𝑗𝐽𝑆)) = (𝐺 DProd (𝑖𝐼 ↦ (𝐺 DProd (𝑗𝐽𝑆))))))
Distinct variable groups:   𝑖,𝑗,𝐺   𝑖,𝐼,𝑗   𝑗,𝐽   𝜑,𝑖,𝑗
Allowed substitution hints:   𝑆(𝑖,𝑗)   𝐽(𝑖)

Proof of Theorem dprd2d2
Dummy variables 𝑥 𝑦 𝑧 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 relxp 5281 . . . . . 6 Rel ({𝑖} × 𝐽)
21rgenw 3060 . . . . 5 𝑖𝐼 Rel ({𝑖} × 𝐽)
3 reliun 5393 . . . . 5 (Rel 𝑖𝐼 ({𝑖} × 𝐽) ↔ ∀𝑖𝐼 Rel ({𝑖} × 𝐽))
42, 3mpbir 221 . . . 4 Rel 𝑖𝐼 ({𝑖} × 𝐽)
54a1i 11 . . 3 (𝜑 → Rel 𝑖𝐼 ({𝑖} × 𝐽))
6 dprd2d2.1 . . . . 5 ((𝜑 ∧ (𝑖𝐼𝑗𝐽)) → 𝑆 ∈ (SubGrp‘𝐺))
76ralrimivva 3107 . . . 4 (𝜑 → ∀𝑖𝐼𝑗𝐽 𝑆 ∈ (SubGrp‘𝐺))
8 eqid 2758 . . . . 5 (𝑖𝐼, 𝑗𝐽𝑆) = (𝑖𝐼, 𝑗𝐽𝑆)
98fmpt2x 7402 . . . 4 (∀𝑖𝐼𝑗𝐽 𝑆 ∈ (SubGrp‘𝐺) ↔ (𝑖𝐼, 𝑗𝐽𝑆): 𝑖𝐼 ({𝑖} × 𝐽)⟶(SubGrp‘𝐺))
107, 9sylib 208 . . 3 (𝜑 → (𝑖𝐼, 𝑗𝐽𝑆): 𝑖𝐼 ({𝑖} × 𝐽)⟶(SubGrp‘𝐺))
11 dmiun 5486 . . . 4 dom 𝑖𝐼 ({𝑖} × 𝐽) = 𝑖𝐼 dom ({𝑖} × 𝐽)
12 dmxpss 5721 . . . . . . 7 dom ({𝑖} × 𝐽) ⊆ {𝑖}
13 simpr 479 . . . . . . . 8 ((𝜑𝑖𝐼) → 𝑖𝐼)
1413snssd 4483 . . . . . . 7 ((𝜑𝑖𝐼) → {𝑖} ⊆ 𝐼)
1512, 14syl5ss 3753 . . . . . 6 ((𝜑𝑖𝐼) → dom ({𝑖} × 𝐽) ⊆ 𝐼)
1615ralrimiva 3102 . . . . 5 (𝜑 → ∀𝑖𝐼 dom ({𝑖} × 𝐽) ⊆ 𝐼)
17 iunss 4711 . . . . 5 ( 𝑖𝐼 dom ({𝑖} × 𝐽) ⊆ 𝐼 ↔ ∀𝑖𝐼 dom ({𝑖} × 𝐽) ⊆ 𝐼)
1816, 17sylibr 224 . . . 4 (𝜑 𝑖𝐼 dom ({𝑖} × 𝐽) ⊆ 𝐼)
1911, 18syl5eqss 3788 . . 3 (𝜑 → dom 𝑖𝐼 ({𝑖} × 𝐽) ⊆ 𝐼)
20 dprd2d2.2 . . . . . . 7 ((𝜑𝑖𝐼) → 𝐺dom DProd (𝑗𝐽𝑆))
21 simprl 811 . . . . . . . . . 10 ((𝜑 ∧ (𝑖𝐼𝑗𝐽)) → 𝑖𝐼)
22 simprr 813 . . . . . . . . . 10 ((𝜑 ∧ (𝑖𝐼𝑗𝐽)) → 𝑗𝐽)
238ovmpt4g 6946 . . . . . . . . . 10 ((𝑖𝐼𝑗𝐽𝑆 ∈ (SubGrp‘𝐺)) → (𝑖(𝑖𝐼, 𝑗𝐽𝑆)𝑗) = 𝑆)
2421, 22, 6, 23syl3anc 1477 . . . . . . . . 9 ((𝜑 ∧ (𝑖𝐼𝑗𝐽)) → (𝑖(𝑖𝐼, 𝑗𝐽𝑆)𝑗) = 𝑆)
2524anassrs 683 . . . . . . . 8 (((𝜑𝑖𝐼) ∧ 𝑗𝐽) → (𝑖(𝑖𝐼, 𝑗𝐽𝑆)𝑗) = 𝑆)
2625mpteq2dva 4894 . . . . . . 7 ((𝜑𝑖𝐼) → (𝑗𝐽 ↦ (𝑖(𝑖𝐼, 𝑗𝐽𝑆)𝑗)) = (𝑗𝐽𝑆))
2720, 26breqtrrd 4830 . . . . . 6 ((𝜑𝑖𝐼) → 𝐺dom DProd (𝑗𝐽 ↦ (𝑖(𝑖𝐼, 𝑗𝐽𝑆)𝑗)))
2827ralrimiva 3102 . . . . 5 (𝜑 → ∀𝑖𝐼 𝐺dom DProd (𝑗𝐽 ↦ (𝑖(𝑖𝐼, 𝑗𝐽𝑆)𝑗)))
29 nfcv 2900 . . . . . . 7 𝑖𝐺
30 nfcv 2900 . . . . . . 7 𝑖dom DProd
31 nfcsb1v 3688 . . . . . . . 8 𝑖𝑥 / 𝑖𝐽
32 nfcv 2900 . . . . . . . . 9 𝑖𝑥
33 nfmpt21 6885 . . . . . . . . 9 𝑖(𝑖𝐼, 𝑗𝐽𝑆)
34 nfcv 2900 . . . . . . . . 9 𝑖𝑗
3532, 33, 34nfov 6837 . . . . . . . 8 𝑖(𝑥(𝑖𝐼, 𝑗𝐽𝑆)𝑗)
3631, 35nfmpt 4896 . . . . . . 7 𝑖(𝑗𝑥 / 𝑖𝐽 ↦ (𝑥(𝑖𝐼, 𝑗𝐽𝑆)𝑗))
3729, 30, 36nfbr 4849 . . . . . 6 𝑖 𝐺dom DProd (𝑗𝑥 / 𝑖𝐽 ↦ (𝑥(𝑖𝐼, 𝑗𝐽𝑆)𝑗))
38 csbeq1a 3681 . . . . . . . 8 (𝑖 = 𝑥𝐽 = 𝑥 / 𝑖𝐽)
39 oveq1 6818 . . . . . . . 8 (𝑖 = 𝑥 → (𝑖(𝑖𝐼, 𝑗𝐽𝑆)𝑗) = (𝑥(𝑖𝐼, 𝑗𝐽𝑆)𝑗))
4038, 39mpteq12dv 4883 . . . . . . 7 (𝑖 = 𝑥 → (𝑗𝐽 ↦ (𝑖(𝑖𝐼, 𝑗𝐽𝑆)𝑗)) = (𝑗𝑥 / 𝑖𝐽 ↦ (𝑥(𝑖𝐼, 𝑗𝐽𝑆)𝑗)))
4140breq2d 4814 . . . . . 6 (𝑖 = 𝑥 → (𝐺dom DProd (𝑗𝐽 ↦ (𝑖(𝑖𝐼, 𝑗𝐽𝑆)𝑗)) ↔ 𝐺dom DProd (𝑗𝑥 / 𝑖𝐽 ↦ (𝑥(𝑖𝐼, 𝑗𝐽𝑆)𝑗))))
4237, 41rspc 3441 . . . . 5 (𝑥𝐼 → (∀𝑖𝐼 𝐺dom DProd (𝑗𝐽 ↦ (𝑖(𝑖𝐼, 𝑗𝐽𝑆)𝑗)) → 𝐺dom DProd (𝑗𝑥 / 𝑖𝐽 ↦ (𝑥(𝑖𝐼, 𝑗𝐽𝑆)𝑗))))
4328, 42mpan9 487 . . . 4 ((𝜑𝑥𝐼) → 𝐺dom DProd (𝑗𝑥 / 𝑖𝐽 ↦ (𝑥(𝑖𝐼, 𝑗𝐽𝑆)𝑗)))
44 nfcv 2900 . . . . . 6 𝑦(𝑥(𝑖𝐼, 𝑗𝐽𝑆)𝑗)
45 nfcv 2900 . . . . . . 7 𝑗𝑥
46 nfmpt22 6886 . . . . . . 7 𝑗(𝑖𝐼, 𝑗𝐽𝑆)
47 nfcv 2900 . . . . . . 7 𝑗𝑦
4845, 46, 47nfov 6837 . . . . . 6 𝑗(𝑥(𝑖𝐼, 𝑗𝐽𝑆)𝑦)
49 oveq2 6819 . . . . . 6 (𝑗 = 𝑦 → (𝑥(𝑖𝐼, 𝑗𝐽𝑆)𝑗) = (𝑥(𝑖𝐼, 𝑗𝐽𝑆)𝑦))
5044, 48, 49cbvmpt 4899 . . . . 5 (𝑗𝑥 / 𝑖𝐽 ↦ (𝑥(𝑖𝐼, 𝑗𝐽𝑆)𝑗)) = (𝑦𝑥 / 𝑖𝐽 ↦ (𝑥(𝑖𝐼, 𝑗𝐽𝑆)𝑦))
51 nfv 1990 . . . . . . . . . . . . 13 𝑖 𝑗 = 𝑧
5231nfcri 2894 . . . . . . . . . . . . 13 𝑖 𝑗𝑥 / 𝑖𝐽
5351, 52nfan 1975 . . . . . . . . . . . 12 𝑖(𝑗 = 𝑧𝑗𝑥 / 𝑖𝐽)
5438eleq2d 2823 . . . . . . . . . . . . 13 (𝑖 = 𝑥 → (𝑗𝐽𝑗𝑥 / 𝑖𝐽))
5554anbi2d 742 . . . . . . . . . . . 12 (𝑖 = 𝑥 → ((𝑗 = 𝑧𝑗𝐽) ↔ (𝑗 = 𝑧𝑗𝑥 / 𝑖𝐽)))
5653, 55equsexv 2254 . . . . . . . . . . 11 (∃𝑖(𝑖 = 𝑥 ∧ (𝑗 = 𝑧𝑗𝐽)) ↔ (𝑗 = 𝑧𝑗𝑥 / 𝑖𝐽))
57 simprl 811 . . . . . . . . . . . . . . . 16 (((𝜑𝑥𝐼) ∧ (𝑖 = 𝑥𝑗 = 𝑧)) → 𝑖 = 𝑥)
58 simplr 809 . . . . . . . . . . . . . . . 16 (((𝜑𝑥𝐼) ∧ (𝑖 = 𝑥𝑗 = 𝑧)) → 𝑥𝐼)
5957, 58eqeltrd 2837 . . . . . . . . . . . . . . 15 (((𝜑𝑥𝐼) ∧ (𝑖 = 𝑥𝑗 = 𝑧)) → 𝑖𝐼)
6059biantrurd 530 . . . . . . . . . . . . . 14 (((𝜑𝑥𝐼) ∧ (𝑖 = 𝑥𝑗 = 𝑧)) → (𝑗𝐽 ↔ (𝑖𝐼𝑗𝐽)))
6160pm5.32da 676 . . . . . . . . . . . . 13 ((𝜑𝑥𝐼) → (((𝑖 = 𝑥𝑗 = 𝑧) ∧ 𝑗𝐽) ↔ ((𝑖 = 𝑥𝑗 = 𝑧) ∧ (𝑖𝐼𝑗𝐽))))
62 anass 684 . . . . . . . . . . . . 13 (((𝑖 = 𝑥𝑗 = 𝑧) ∧ 𝑗𝐽) ↔ (𝑖 = 𝑥 ∧ (𝑗 = 𝑧𝑗𝐽)))
63 eqcom 2765 . . . . . . . . . . . . . . 15 (⟨𝑥, 𝑧⟩ = ⟨𝑖, 𝑗⟩ ↔ ⟨𝑖, 𝑗⟩ = ⟨𝑥, 𝑧⟩)
64 vex 3341 . . . . . . . . . . . . . . . 16 𝑖 ∈ V
65 vex 3341 . . . . . . . . . . . . . . . 16 𝑗 ∈ V
6664, 65opth 5091 . . . . . . . . . . . . . . 15 (⟨𝑖, 𝑗⟩ = ⟨𝑥, 𝑧⟩ ↔ (𝑖 = 𝑥𝑗 = 𝑧))
6763, 66bitr2i 265 . . . . . . . . . . . . . 14 ((𝑖 = 𝑥𝑗 = 𝑧) ↔ ⟨𝑥, 𝑧⟩ = ⟨𝑖, 𝑗⟩)
6867anbi1i 733 . . . . . . . . . . . . 13 (((𝑖 = 𝑥𝑗 = 𝑧) ∧ (𝑖𝐼𝑗𝐽)) ↔ (⟨𝑥, 𝑧⟩ = ⟨𝑖, 𝑗⟩ ∧ (𝑖𝐼𝑗𝐽)))
6961, 62, 683bitr3g 302 . . . . . . . . . . . 12 ((𝜑𝑥𝐼) → ((𝑖 = 𝑥 ∧ (𝑗 = 𝑧𝑗𝐽)) ↔ (⟨𝑥, 𝑧⟩ = ⟨𝑖, 𝑗⟩ ∧ (𝑖𝐼𝑗𝐽))))
7069exbidv 1997 . . . . . . . . . . 11 ((𝜑𝑥𝐼) → (∃𝑖(𝑖 = 𝑥 ∧ (𝑗 = 𝑧𝑗𝐽)) ↔ ∃𝑖(⟨𝑥, 𝑧⟩ = ⟨𝑖, 𝑗⟩ ∧ (𝑖𝐼𝑗𝐽))))
7156, 70syl5bbr 274 . . . . . . . . . 10 ((𝜑𝑥𝐼) → ((𝑗 = 𝑧𝑗𝑥 / 𝑖𝐽) ↔ ∃𝑖(⟨𝑥, 𝑧⟩ = ⟨𝑖, 𝑗⟩ ∧ (𝑖𝐼𝑗𝐽))))
7271exbidv 1997 . . . . . . . . 9 ((𝜑𝑥𝐼) → (∃𝑗(𝑗 = 𝑧𝑗𝑥 / 𝑖𝐽) ↔ ∃𝑗𝑖(⟨𝑥, 𝑧⟩ = ⟨𝑖, 𝑗⟩ ∧ (𝑖𝐼𝑗𝐽))))
73 vex 3341 . . . . . . . . . 10 𝑧 ∈ V
74 eleq1w 2820 . . . . . . . . . 10 (𝑗 = 𝑧 → (𝑗𝑥 / 𝑖𝐽𝑧𝑥 / 𝑖𝐽))
7573, 74ceqsexv 3380 . . . . . . . . 9 (∃𝑗(𝑗 = 𝑧𝑗𝑥 / 𝑖𝐽) ↔ 𝑧𝑥 / 𝑖𝐽)
76 excom 2189 . . . . . . . . 9 (∃𝑗𝑖(⟨𝑥, 𝑧⟩ = ⟨𝑖, 𝑗⟩ ∧ (𝑖𝐼𝑗𝐽)) ↔ ∃𝑖𝑗(⟨𝑥, 𝑧⟩ = ⟨𝑖, 𝑗⟩ ∧ (𝑖𝐼𝑗𝐽)))
7772, 75, 763bitr3g 302 . . . . . . . 8 ((𝜑𝑥𝐼) → (𝑧𝑥 / 𝑖𝐽 ↔ ∃𝑖𝑗(⟨𝑥, 𝑧⟩ = ⟨𝑖, 𝑗⟩ ∧ (𝑖𝐼𝑗𝐽))))
78 elrelimasn 5645 . . . . . . . . . 10 (Rel 𝑖𝐼 ({𝑖} × 𝐽) → (𝑧 ∈ ( 𝑖𝐼 ({𝑖} × 𝐽) “ {𝑥}) ↔ 𝑥 𝑖𝐼 ({𝑖} × 𝐽)𝑧))
794, 78ax-mp 5 . . . . . . . . 9 (𝑧 ∈ ( 𝑖𝐼 ({𝑖} × 𝐽) “ {𝑥}) ↔ 𝑥 𝑖𝐼 ({𝑖} × 𝐽)𝑧)
80 df-br 4803 . . . . . . . . 9 (𝑥 𝑖𝐼 ({𝑖} × 𝐽)𝑧 ↔ ⟨𝑥, 𝑧⟩ ∈ 𝑖𝐼 ({𝑖} × 𝐽))
81 eliunxp 5413 . . . . . . . . 9 (⟨𝑥, 𝑧⟩ ∈ 𝑖𝐼 ({𝑖} × 𝐽) ↔ ∃𝑖𝑗(⟨𝑥, 𝑧⟩ = ⟨𝑖, 𝑗⟩ ∧ (𝑖𝐼𝑗𝐽)))
8279, 80, 813bitri 286 . . . . . . . 8 (𝑧 ∈ ( 𝑖𝐼 ({𝑖} × 𝐽) “ {𝑥}) ↔ ∃𝑖𝑗(⟨𝑥, 𝑧⟩ = ⟨𝑖, 𝑗⟩ ∧ (𝑖𝐼𝑗𝐽)))
8377, 82syl6bbr 278 . . . . . . 7 ((𝜑𝑥𝐼) → (𝑧𝑥 / 𝑖𝐽𝑧 ∈ ( 𝑖𝐼 ({𝑖} × 𝐽) “ {𝑥})))
8483eqrdv 2756 . . . . . 6 ((𝜑𝑥𝐼) → 𝑥 / 𝑖𝐽 = ( 𝑖𝐼 ({𝑖} × 𝐽) “ {𝑥}))
8584mpteq1d 4888 . . . . 5 ((𝜑𝑥𝐼) → (𝑦𝑥 / 𝑖𝐽 ↦ (𝑥(𝑖𝐼, 𝑗𝐽𝑆)𝑦)) = (𝑦 ∈ ( 𝑖𝐼 ({𝑖} × 𝐽) “ {𝑥}) ↦ (𝑥(𝑖𝐼, 𝑗𝐽𝑆)𝑦)))
8650, 85syl5eq 2804 . . . 4 ((𝜑𝑥𝐼) → (𝑗𝑥 / 𝑖𝐽 ↦ (𝑥(𝑖𝐼, 𝑗𝐽𝑆)𝑗)) = (𝑦 ∈ ( 𝑖𝐼 ({𝑖} × 𝐽) “ {𝑥}) ↦ (𝑥(𝑖𝐼, 𝑗𝐽𝑆)𝑦)))
8743, 86breqtrd 4828 . . 3 ((𝜑𝑥𝐼) → 𝐺dom DProd (𝑦 ∈ ( 𝑖𝐼 ({𝑖} × 𝐽) “ {𝑥}) ↦ (𝑥(𝑖𝐼, 𝑗𝐽𝑆)𝑦)))
88 dprd2d2.3 . . . . 5 (𝜑𝐺dom DProd (𝑖𝐼 ↦ (𝐺 DProd (𝑗𝐽𝑆))))
8926oveq2d 6827 . . . . . 6 ((𝜑𝑖𝐼) → (𝐺 DProd (𝑗𝐽 ↦ (𝑖(𝑖𝐼, 𝑗𝐽𝑆)𝑗))) = (𝐺 DProd (𝑗𝐽𝑆)))
9089mpteq2dva 4894 . . . . 5 (𝜑 → (𝑖𝐼 ↦ (𝐺 DProd (𝑗𝐽 ↦ (𝑖(𝑖𝐼, 𝑗𝐽𝑆)𝑗)))) = (𝑖𝐼 ↦ (𝐺 DProd (𝑗𝐽𝑆))))
9188, 90breqtrrd 4830 . . . 4 (𝜑𝐺dom DProd (𝑖𝐼 ↦ (𝐺 DProd (𝑗𝐽 ↦ (𝑖(𝑖𝐼, 𝑗𝐽𝑆)𝑗)))))
92 nfcv 2900 . . . . . 6 𝑥(𝐺 DProd (𝑗𝐽 ↦ (𝑖(𝑖𝐼, 𝑗𝐽𝑆)𝑗)))
93 nfcv 2900 . . . . . . 7 𝑖 DProd
9429, 93, 36nfov 6837 . . . . . 6 𝑖(𝐺 DProd (𝑗𝑥 / 𝑖𝐽 ↦ (𝑥(𝑖𝐼, 𝑗𝐽𝑆)𝑗)))
9540oveq2d 6827 . . . . . 6 (𝑖 = 𝑥 → (𝐺 DProd (𝑗𝐽 ↦ (𝑖(𝑖𝐼, 𝑗𝐽𝑆)𝑗))) = (𝐺 DProd (𝑗𝑥 / 𝑖𝐽 ↦ (𝑥(𝑖𝐼, 𝑗𝐽𝑆)𝑗))))
9692, 94, 95cbvmpt 4899 . . . . 5 (𝑖𝐼 ↦ (𝐺 DProd (𝑗𝐽 ↦ (𝑖(𝑖𝐼, 𝑗𝐽𝑆)𝑗)))) = (𝑥𝐼 ↦ (𝐺 DProd (𝑗𝑥 / 𝑖𝐽 ↦ (𝑥(𝑖𝐼, 𝑗𝐽𝑆)𝑗))))
9786oveq2d 6827 . . . . . 6 ((𝜑𝑥𝐼) → (𝐺 DProd (𝑗𝑥 / 𝑖𝐽 ↦ (𝑥(𝑖𝐼, 𝑗𝐽𝑆)𝑗))) = (𝐺 DProd (𝑦 ∈ ( 𝑖𝐼 ({𝑖} × 𝐽) “ {𝑥}) ↦ (𝑥(𝑖𝐼, 𝑗𝐽𝑆)𝑦))))
9897mpteq2dva 4894 . . . . 5 (𝜑 → (𝑥𝐼 ↦ (𝐺 DProd (𝑗𝑥 / 𝑖𝐽 ↦ (𝑥(𝑖𝐼, 𝑗𝐽𝑆)𝑗)))) = (𝑥𝐼 ↦ (𝐺 DProd (𝑦 ∈ ( 𝑖𝐼 ({𝑖} × 𝐽) “ {𝑥}) ↦ (𝑥(𝑖𝐼, 𝑗𝐽𝑆)𝑦)))))
9996, 98syl5eq 2804 . . . 4 (𝜑 → (𝑖𝐼 ↦ (𝐺 DProd (𝑗𝐽 ↦ (𝑖(𝑖𝐼, 𝑗𝐽𝑆)𝑗)))) = (𝑥𝐼 ↦ (𝐺 DProd (𝑦 ∈ ( 𝑖𝐼 ({𝑖} × 𝐽) “ {𝑥}) ↦ (𝑥(𝑖𝐼, 𝑗𝐽𝑆)𝑦)))))
10091, 99breqtrd 4828 . . 3 (𝜑𝐺dom DProd (𝑥𝐼 ↦ (𝐺 DProd (𝑦 ∈ ( 𝑖𝐼 ({𝑖} × 𝐽) “ {𝑥}) ↦ (𝑥(𝑖𝐼, 𝑗𝐽𝑆)𝑦)))))
101 eqid 2758 . . 3 (mrCls‘(SubGrp‘𝐺)) = (mrCls‘(SubGrp‘𝐺))
1025, 10, 19, 87, 100, 101dprd2da 18639 . 2 (𝜑𝐺dom DProd (𝑖𝐼, 𝑗𝐽𝑆))
1035, 10, 19, 87, 100, 101dprd2db 18640 . . 3 (𝜑 → (𝐺 DProd (𝑖𝐼, 𝑗𝐽𝑆)) = (𝐺 DProd (𝑥𝐼 ↦ (𝐺 DProd (𝑦 ∈ ( 𝑖𝐼 ({𝑖} × 𝐽) “ {𝑥}) ↦ (𝑥(𝑖𝐼, 𝑗𝐽𝑆)𝑦))))))
10499, 90eqtr3d 2794 . . . 4 (𝜑 → (𝑥𝐼 ↦ (𝐺 DProd (𝑦 ∈ ( 𝑖𝐼 ({𝑖} × 𝐽) “ {𝑥}) ↦ (𝑥(𝑖𝐼, 𝑗𝐽𝑆)𝑦)))) = (𝑖𝐼 ↦ (𝐺 DProd (𝑗𝐽𝑆))))
105104oveq2d 6827 . . 3 (𝜑 → (𝐺 DProd (𝑥𝐼 ↦ (𝐺 DProd (𝑦 ∈ ( 𝑖𝐼 ({𝑖} × 𝐽) “ {𝑥}) ↦ (𝑥(𝑖𝐼, 𝑗𝐽𝑆)𝑦))))) = (𝐺 DProd (𝑖𝐼 ↦ (𝐺 DProd (𝑗𝐽𝑆)))))
106103, 105eqtrd 2792 . 2 (𝜑 → (𝐺 DProd (𝑖𝐼, 𝑗𝐽𝑆)) = (𝐺 DProd (𝑖𝐼 ↦ (𝐺 DProd (𝑗𝐽𝑆)))))
107102, 106jca 555 1 (𝜑 → (𝐺dom DProd (𝑖𝐼, 𝑗𝐽𝑆) ∧ (𝐺 DProd (𝑖𝐼, 𝑗𝐽𝑆)) = (𝐺 DProd (𝑖𝐼 ↦ (𝐺 DProd (𝑗𝐽𝑆))))))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196  wa 383   = wceq 1630  wex 1851  wcel 2137  wral 3048  csb 3672  wss 3713  {csn 4319  cop 4325   ciun 4670   class class class wbr 4802  cmpt 4879   × cxp 5262  dom cdm 5264  cima 5267  Rel wrel 5269  wf 6043  cfv 6047  (class class class)co 6811  cmpt2 6813  mrClscmrc 16443  SubGrpcsubg 17787   DProd cdprd 18590
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1869  ax-4 1884  ax-5 1986  ax-6 2052  ax-7 2088  ax-8 2139  ax-9 2146  ax-10 2166  ax-11 2181  ax-12 2194  ax-13 2389  ax-ext 2738  ax-rep 4921  ax-sep 4931  ax-nul 4939  ax-pow 4990  ax-pr 5053  ax-un 7112  ax-inf2 8709  ax-cnex 10182  ax-resscn 10183  ax-1cn 10184  ax-icn 10185  ax-addcl 10186  ax-addrcl 10187  ax-mulcl 10188  ax-mulrcl 10189  ax-mulcom 10190  ax-addass 10191  ax-mulass 10192  ax-distr 10193  ax-i2m1 10194  ax-1ne0 10195  ax-1rid 10196  ax-rnegex 10197  ax-rrecex 10198  ax-cnre 10199  ax-pre-lttri 10200  ax-pre-lttrn 10201  ax-pre-ltadd 10202  ax-pre-mulgt0 10203
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3or 1073  df-3an 1074  df-tru 1633  df-ex 1852  df-nf 1857  df-sb 2045  df-eu 2609  df-mo 2610  df-clab 2745  df-cleq 2751  df-clel 2754  df-nfc 2889  df-ne 2931  df-nel 3034  df-ral 3053  df-rex 3054  df-reu 3055  df-rmo 3056  df-rab 3057  df-v 3340  df-sbc 3575  df-csb 3673  df-dif 3716  df-un 3718  df-in 3720  df-ss 3727  df-pss 3729  df-nul 4057  df-if 4229  df-pw 4302  df-sn 4320  df-pr 4322  df-tp 4324  df-op 4326  df-uni 4587  df-int 4626  df-iun 4672  df-iin 4673  df-br 4803  df-opab 4863  df-mpt 4880  df-tr 4903  df-id 5172  df-eprel 5177  df-po 5185  df-so 5186  df-fr 5223  df-se 5224  df-we 5225  df-xp 5270  df-rel 5271  df-cnv 5272  df-co 5273  df-dm 5274  df-rn 5275  df-res 5276  df-ima 5277  df-pred 5839  df-ord 5885  df-on 5886  df-lim 5887  df-suc 5888  df-iota 6010  df-fun 6049  df-fn 6050  df-f 6051  df-f1 6052  df-fo 6053  df-f1o 6054  df-fv 6055  df-isom 6056  df-riota 6772  df-ov 6814  df-oprab 6815  df-mpt2 6816  df-of 7060  df-om 7229  df-1st 7331  df-2nd 7332  df-supp 7462  df-tpos 7519  df-wrecs 7574  df-recs 7635  df-rdg 7673  df-1o 7727  df-oadd 7731  df-er 7909  df-map 8023  df-ixp 8073  df-en 8120  df-dom 8121  df-sdom 8122  df-fin 8123  df-fsupp 8439  df-oi 8578  df-card 8953  df-pnf 10266  df-mnf 10267  df-xr 10268  df-ltxr 10269  df-le 10270  df-sub 10458  df-neg 10459  df-nn 11211  df-2 11269  df-n0 11483  df-z 11568  df-uz 11878  df-fz 12518  df-fzo 12658  df-seq 12994  df-hash 13310  df-ndx 16060  df-slot 16061  df-base 16063  df-sets 16064  df-ress 16065  df-plusg 16154  df-0g 16302  df-gsum 16303  df-mre 16446  df-mrc 16447  df-acs 16449  df-mgm 17441  df-sgrp 17483  df-mnd 17494  df-mhm 17534  df-submnd 17535  df-grp 17624  df-minusg 17625  df-sbg 17626  df-mulg 17740  df-subg 17790  df-ghm 17857  df-gim 17900  df-cntz 17948  df-oppg 17974  df-lsm 18249  df-cmn 18393  df-dprd 18592
This theorem is referenced by:  ablfaclem2  18683
  Copyright terms: Public domain W3C validator