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

Theorem dprd2d2 19821
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 5651 . . . . . 6 Rel ({𝑖} × 𝐽)
21rgenw 3068 . . . . 5 𝑖𝐼 Rel ({𝑖} × 𝐽)
3 reliun 5772 . . . . 5 (Rel 𝑖𝐼 ({𝑖} × 𝐽) ↔ ∀𝑖𝐼 Rel ({𝑖} × 𝐽))
42, 3mpbir 230 . . . 4 Rel 𝑖𝐼 ({𝑖} × 𝐽)
54a1i 11 . . 3 (𝜑 → Rel 𝑖𝐼 ({𝑖} × 𝐽))
6 dprd2d2.1 . . . . 5 ((𝜑 ∧ (𝑖𝐼𝑗𝐽)) → 𝑆 ∈ (SubGrp‘𝐺))
76ralrimivva 3197 . . . 4 (𝜑 → ∀𝑖𝐼𝑗𝐽 𝑆 ∈ (SubGrp‘𝐺))
8 eqid 2736 . . . . 5 (𝑖𝐼, 𝑗𝐽𝑆) = (𝑖𝐼, 𝑗𝐽𝑆)
98fmpox 7998 . . . 4 (∀𝑖𝐼𝑗𝐽 𝑆 ∈ (SubGrp‘𝐺) ↔ (𝑖𝐼, 𝑗𝐽𝑆): 𝑖𝐼 ({𝑖} × 𝐽)⟶(SubGrp‘𝐺))
107, 9sylib 217 . . 3 (𝜑 → (𝑖𝐼, 𝑗𝐽𝑆): 𝑖𝐼 ({𝑖} × 𝐽)⟶(SubGrp‘𝐺))
11 dmiun 5869 . . . 4 dom 𝑖𝐼 ({𝑖} × 𝐽) = 𝑖𝐼 dom ({𝑖} × 𝐽)
12 dmxpss 6123 . . . . . . 7 dom ({𝑖} × 𝐽) ⊆ {𝑖}
13 simpr 485 . . . . . . . 8 ((𝜑𝑖𝐼) → 𝑖𝐼)
1413snssd 4769 . . . . . . 7 ((𝜑𝑖𝐼) → {𝑖} ⊆ 𝐼)
1512, 14sstrid 3955 . . . . . 6 ((𝜑𝑖𝐼) → dom ({𝑖} × 𝐽) ⊆ 𝐼)
1615ralrimiva 3143 . . . . 5 (𝜑 → ∀𝑖𝐼 dom ({𝑖} × 𝐽) ⊆ 𝐼)
17 iunss 5005 . . . . 5 ( 𝑖𝐼 dom ({𝑖} × 𝐽) ⊆ 𝐼 ↔ ∀𝑖𝐼 dom ({𝑖} × 𝐽) ⊆ 𝐼)
1816, 17sylibr 233 . . . 4 (𝜑 𝑖𝐼 dom ({𝑖} × 𝐽) ⊆ 𝐼)
1911, 18eqsstrid 3992 . . 3 (𝜑 → dom 𝑖𝐼 ({𝑖} × 𝐽) ⊆ 𝐼)
20 dprd2d2.2 . . . . . . 7 ((𝜑𝑖𝐼) → 𝐺dom DProd (𝑗𝐽𝑆))
21 simprl 769 . . . . . . . . . 10 ((𝜑 ∧ (𝑖𝐼𝑗𝐽)) → 𝑖𝐼)
22 simprr 771 . . . . . . . . . 10 ((𝜑 ∧ (𝑖𝐼𝑗𝐽)) → 𝑗𝐽)
238ovmpt4g 7501 . . . . . . . . . 10 ((𝑖𝐼𝑗𝐽𝑆 ∈ (SubGrp‘𝐺)) → (𝑖(𝑖𝐼, 𝑗𝐽𝑆)𝑗) = 𝑆)
2421, 22, 6, 23syl3anc 1371 . . . . . . . . 9 ((𝜑 ∧ (𝑖𝐼𝑗𝐽)) → (𝑖(𝑖𝐼, 𝑗𝐽𝑆)𝑗) = 𝑆)
2524anassrs 468 . . . . . . . 8 (((𝜑𝑖𝐼) ∧ 𝑗𝐽) → (𝑖(𝑖𝐼, 𝑗𝐽𝑆)𝑗) = 𝑆)
2625mpteq2dva 5205 . . . . . . 7 ((𝜑𝑖𝐼) → (𝑗𝐽 ↦ (𝑖(𝑖𝐼, 𝑗𝐽𝑆)𝑗)) = (𝑗𝐽𝑆))
2720, 26breqtrrd 5133 . . . . . 6 ((𝜑𝑖𝐼) → 𝐺dom DProd (𝑗𝐽 ↦ (𝑖(𝑖𝐼, 𝑗𝐽𝑆)𝑗)))
2827ralrimiva 3143 . . . . 5 (𝜑 → ∀𝑖𝐼 𝐺dom DProd (𝑗𝐽 ↦ (𝑖(𝑖𝐼, 𝑗𝐽𝑆)𝑗)))
29 nfcv 2907 . . . . . . 7 𝑖𝐺
30 nfcv 2907 . . . . . . 7 𝑖dom DProd
31 nfcsb1v 3880 . . . . . . . 8 𝑖𝑥 / 𝑖𝐽
32 nfcv 2907 . . . . . . . . 9 𝑖𝑥
33 nfmpo1 7436 . . . . . . . . 9 𝑖(𝑖𝐼, 𝑗𝐽𝑆)
34 nfcv 2907 . . . . . . . . 9 𝑖𝑗
3532, 33, 34nfov 7386 . . . . . . . 8 𝑖(𝑥(𝑖𝐼, 𝑗𝐽𝑆)𝑗)
3631, 35nfmpt 5212 . . . . . . 7 𝑖(𝑗𝑥 / 𝑖𝐽 ↦ (𝑥(𝑖𝐼, 𝑗𝐽𝑆)𝑗))
3729, 30, 36nfbr 5152 . . . . . 6 𝑖 𝐺dom DProd (𝑗𝑥 / 𝑖𝐽 ↦ (𝑥(𝑖𝐼, 𝑗𝐽𝑆)𝑗))
38 csbeq1a 3869 . . . . . . . 8 (𝑖 = 𝑥𝐽 = 𝑥 / 𝑖𝐽)
39 oveq1 7363 . . . . . . . 8 (𝑖 = 𝑥 → (𝑖(𝑖𝐼, 𝑗𝐽𝑆)𝑗) = (𝑥(𝑖𝐼, 𝑗𝐽𝑆)𝑗))
4038, 39mpteq12dv 5196 . . . . . . 7 (𝑖 = 𝑥 → (𝑗𝐽 ↦ (𝑖(𝑖𝐼, 𝑗𝐽𝑆)𝑗)) = (𝑗𝑥 / 𝑖𝐽 ↦ (𝑥(𝑖𝐼, 𝑗𝐽𝑆)𝑗)))
4140breq2d 5117 . . . . . 6 (𝑖 = 𝑥 → (𝐺dom DProd (𝑗𝐽 ↦ (𝑖(𝑖𝐼, 𝑗𝐽𝑆)𝑗)) ↔ 𝐺dom DProd (𝑗𝑥 / 𝑖𝐽 ↦ (𝑥(𝑖𝐼, 𝑗𝐽𝑆)𝑗))))
4237, 41rspc 3569 . . . . 5 (𝑥𝐼 → (∀𝑖𝐼 𝐺dom DProd (𝑗𝐽 ↦ (𝑖(𝑖𝐼, 𝑗𝐽𝑆)𝑗)) → 𝐺dom DProd (𝑗𝑥 / 𝑖𝐽 ↦ (𝑥(𝑖𝐼, 𝑗𝐽𝑆)𝑗))))
4328, 42mpan9 507 . . . 4 ((𝜑𝑥𝐼) → 𝐺dom DProd (𝑗𝑥 / 𝑖𝐽 ↦ (𝑥(𝑖𝐼, 𝑗𝐽𝑆)𝑗)))
44 nfcv 2907 . . . . . 6 𝑦(𝑥(𝑖𝐼, 𝑗𝐽𝑆)𝑗)
45 nfcv 2907 . . . . . . 7 𝑗𝑥
46 nfmpo2 7437 . . . . . . 7 𝑗(𝑖𝐼, 𝑗𝐽𝑆)
47 nfcv 2907 . . . . . . 7 𝑗𝑦
4845, 46, 47nfov 7386 . . . . . 6 𝑗(𝑥(𝑖𝐼, 𝑗𝐽𝑆)𝑦)
49 oveq2 7364 . . . . . 6 (𝑗 = 𝑦 → (𝑥(𝑖𝐼, 𝑗𝐽𝑆)𝑗) = (𝑥(𝑖𝐼, 𝑗𝐽𝑆)𝑦))
5044, 48, 49cbvmpt 5216 . . . . 5 (𝑗𝑥 / 𝑖𝐽 ↦ (𝑥(𝑖𝐼, 𝑗𝐽𝑆)𝑗)) = (𝑦𝑥 / 𝑖𝐽 ↦ (𝑥(𝑖𝐼, 𝑗𝐽𝑆)𝑦))
51 nfv 1917 . . . . . . . . . . . . 13 𝑖 𝑗 = 𝑧
5231nfcri 2894 . . . . . . . . . . . . 13 𝑖 𝑗𝑥 / 𝑖𝐽
5351, 52nfan 1902 . . . . . . . . . . . 12 𝑖(𝑗 = 𝑧𝑗𝑥 / 𝑖𝐽)
5438eleq2d 2823 . . . . . . . . . . . . 13 (𝑖 = 𝑥 → (𝑗𝐽𝑗𝑥 / 𝑖𝐽))
5554anbi2d 629 . . . . . . . . . . . 12 (𝑖 = 𝑥 → ((𝑗 = 𝑧𝑗𝐽) ↔ (𝑗 = 𝑧𝑗𝑥 / 𝑖𝐽)))
5653, 55equsexv 2259 . . . . . . . . . . 11 (∃𝑖(𝑖 = 𝑥 ∧ (𝑗 = 𝑧𝑗𝐽)) ↔ (𝑗 = 𝑧𝑗𝑥 / 𝑖𝐽))
57 simprl 769 . . . . . . . . . . . . . . . 16 (((𝜑𝑥𝐼) ∧ (𝑖 = 𝑥𝑗 = 𝑧)) → 𝑖 = 𝑥)
58 simplr 767 . . . . . . . . . . . . . . . 16 (((𝜑𝑥𝐼) ∧ (𝑖 = 𝑥𝑗 = 𝑧)) → 𝑥𝐼)
5957, 58eqeltrd 2838 . . . . . . . . . . . . . . 15 (((𝜑𝑥𝐼) ∧ (𝑖 = 𝑥𝑗 = 𝑧)) → 𝑖𝐼)
6059biantrurd 533 . . . . . . . . . . . . . 14 (((𝜑𝑥𝐼) ∧ (𝑖 = 𝑥𝑗 = 𝑧)) → (𝑗𝐽 ↔ (𝑖𝐼𝑗𝐽)))
6160pm5.32da 579 . . . . . . . . . . . . 13 ((𝜑𝑥𝐼) → (((𝑖 = 𝑥𝑗 = 𝑧) ∧ 𝑗𝐽) ↔ ((𝑖 = 𝑥𝑗 = 𝑧) ∧ (𝑖𝐼𝑗𝐽))))
62 anass 469 . . . . . . . . . . . . 13 (((𝑖 = 𝑥𝑗 = 𝑧) ∧ 𝑗𝐽) ↔ (𝑖 = 𝑥 ∧ (𝑗 = 𝑧𝑗𝐽)))
63 eqcom 2743 . . . . . . . . . . . . . . 15 (⟨𝑥, 𝑧⟩ = ⟨𝑖, 𝑗⟩ ↔ ⟨𝑖, 𝑗⟩ = ⟨𝑥, 𝑧⟩)
64 vex 3449 . . . . . . . . . . . . . . . 16 𝑖 ∈ V
65 vex 3449 . . . . . . . . . . . . . . . 16 𝑗 ∈ V
6664, 65opth 5433 . . . . . . . . . . . . . . 15 (⟨𝑖, 𝑗⟩ = ⟨𝑥, 𝑧⟩ ↔ (𝑖 = 𝑥𝑗 = 𝑧))
6763, 66bitr2i 275 . . . . . . . . . . . . . 14 ((𝑖 = 𝑥𝑗 = 𝑧) ↔ ⟨𝑥, 𝑧⟩ = ⟨𝑖, 𝑗⟩)
6867anbi1i 624 . . . . . . . . . . . . 13 (((𝑖 = 𝑥𝑗 = 𝑧) ∧ (𝑖𝐼𝑗𝐽)) ↔ (⟨𝑥, 𝑧⟩ = ⟨𝑖, 𝑗⟩ ∧ (𝑖𝐼𝑗𝐽)))
6961, 62, 683bitr3g 312 . . . . . . . . . . . 12 ((𝜑𝑥𝐼) → ((𝑖 = 𝑥 ∧ (𝑗 = 𝑧𝑗𝐽)) ↔ (⟨𝑥, 𝑧⟩ = ⟨𝑖, 𝑗⟩ ∧ (𝑖𝐼𝑗𝐽))))
7069exbidv 1924 . . . . . . . . . . 11 ((𝜑𝑥𝐼) → (∃𝑖(𝑖 = 𝑥 ∧ (𝑗 = 𝑧𝑗𝐽)) ↔ ∃𝑖(⟨𝑥, 𝑧⟩ = ⟨𝑖, 𝑗⟩ ∧ (𝑖𝐼𝑗𝐽))))
7156, 70bitr3id 284 . . . . . . . . . 10 ((𝜑𝑥𝐼) → ((𝑗 = 𝑧𝑗𝑥 / 𝑖𝐽) ↔ ∃𝑖(⟨𝑥, 𝑧⟩ = ⟨𝑖, 𝑗⟩ ∧ (𝑖𝐼𝑗𝐽))))
7271exbidv 1924 . . . . . . . . 9 ((𝜑𝑥𝐼) → (∃𝑗(𝑗 = 𝑧𝑗𝑥 / 𝑖𝐽) ↔ ∃𝑗𝑖(⟨𝑥, 𝑧⟩ = ⟨𝑖, 𝑗⟩ ∧ (𝑖𝐼𝑗𝐽))))
73 vex 3449 . . . . . . . . . 10 𝑧 ∈ V
74 eleq1w 2820 . . . . . . . . . 10 (𝑗 = 𝑧 → (𝑗𝑥 / 𝑖𝐽𝑧𝑥 / 𝑖𝐽))
7573, 74ceqsexv 3494 . . . . . . . . 9 (∃𝑗(𝑗 = 𝑧𝑗𝑥 / 𝑖𝐽) ↔ 𝑧𝑥 / 𝑖𝐽)
76 excom 2162 . . . . . . . . 9 (∃𝑗𝑖(⟨𝑥, 𝑧⟩ = ⟨𝑖, 𝑗⟩ ∧ (𝑖𝐼𝑗𝐽)) ↔ ∃𝑖𝑗(⟨𝑥, 𝑧⟩ = ⟨𝑖, 𝑗⟩ ∧ (𝑖𝐼𝑗𝐽)))
7772, 75, 763bitr3g 312 . . . . . . . 8 ((𝜑𝑥𝐼) → (𝑧𝑥 / 𝑖𝐽 ↔ ∃𝑖𝑗(⟨𝑥, 𝑧⟩ = ⟨𝑖, 𝑗⟩ ∧ (𝑖𝐼𝑗𝐽))))
78 elrelimasn 6037 . . . . . . . . . 10 (Rel 𝑖𝐼 ({𝑖} × 𝐽) → (𝑧 ∈ ( 𝑖𝐼 ({𝑖} × 𝐽) “ {𝑥}) ↔ 𝑥 𝑖𝐼 ({𝑖} × 𝐽)𝑧))
794, 78ax-mp 5 . . . . . . . . 9 (𝑧 ∈ ( 𝑖𝐼 ({𝑖} × 𝐽) “ {𝑥}) ↔ 𝑥 𝑖𝐼 ({𝑖} × 𝐽)𝑧)
80 df-br 5106 . . . . . . . . 9 (𝑥 𝑖𝐼 ({𝑖} × 𝐽)𝑧 ↔ ⟨𝑥, 𝑧⟩ ∈ 𝑖𝐼 ({𝑖} × 𝐽))
81 eliunxp 5793 . . . . . . . . 9 (⟨𝑥, 𝑧⟩ ∈ 𝑖𝐼 ({𝑖} × 𝐽) ↔ ∃𝑖𝑗(⟨𝑥, 𝑧⟩ = ⟨𝑖, 𝑗⟩ ∧ (𝑖𝐼𝑗𝐽)))
8279, 80, 813bitri 296 . . . . . . . 8 (𝑧 ∈ ( 𝑖𝐼 ({𝑖} × 𝐽) “ {𝑥}) ↔ ∃𝑖𝑗(⟨𝑥, 𝑧⟩ = ⟨𝑖, 𝑗⟩ ∧ (𝑖𝐼𝑗𝐽)))
8377, 82bitr4di 288 . . . . . . 7 ((𝜑𝑥𝐼) → (𝑧𝑥 / 𝑖𝐽𝑧 ∈ ( 𝑖𝐼 ({𝑖} × 𝐽) “ {𝑥})))
8483eqrdv 2734 . . . . . 6 ((𝜑𝑥𝐼) → 𝑥 / 𝑖𝐽 = ( 𝑖𝐼 ({𝑖} × 𝐽) “ {𝑥}))
8584mpteq1d 5200 . . . . 5 ((𝜑𝑥𝐼) → (𝑦𝑥 / 𝑖𝐽 ↦ (𝑥(𝑖𝐼, 𝑗𝐽𝑆)𝑦)) = (𝑦 ∈ ( 𝑖𝐼 ({𝑖} × 𝐽) “ {𝑥}) ↦ (𝑥(𝑖𝐼, 𝑗𝐽𝑆)𝑦)))
8650, 85eqtrid 2788 . . . 4 ((𝜑𝑥𝐼) → (𝑗𝑥 / 𝑖𝐽 ↦ (𝑥(𝑖𝐼, 𝑗𝐽𝑆)𝑗)) = (𝑦 ∈ ( 𝑖𝐼 ({𝑖} × 𝐽) “ {𝑥}) ↦ (𝑥(𝑖𝐼, 𝑗𝐽𝑆)𝑦)))
8743, 86breqtrd 5131 . . 3 ((𝜑𝑥𝐼) → 𝐺dom DProd (𝑦 ∈ ( 𝑖𝐼 ({𝑖} × 𝐽) “ {𝑥}) ↦ (𝑥(𝑖𝐼, 𝑗𝐽𝑆)𝑦)))
88 dprd2d2.3 . . . . 5 (𝜑𝐺dom DProd (𝑖𝐼 ↦ (𝐺 DProd (𝑗𝐽𝑆))))
8926oveq2d 7372 . . . . . 6 ((𝜑𝑖𝐼) → (𝐺 DProd (𝑗𝐽 ↦ (𝑖(𝑖𝐼, 𝑗𝐽𝑆)𝑗))) = (𝐺 DProd (𝑗𝐽𝑆)))
9089mpteq2dva 5205 . . . . 5 (𝜑 → (𝑖𝐼 ↦ (𝐺 DProd (𝑗𝐽 ↦ (𝑖(𝑖𝐼, 𝑗𝐽𝑆)𝑗)))) = (𝑖𝐼 ↦ (𝐺 DProd (𝑗𝐽𝑆))))
9188, 90breqtrrd 5133 . . . 4 (𝜑𝐺dom DProd (𝑖𝐼 ↦ (𝐺 DProd (𝑗𝐽 ↦ (𝑖(𝑖𝐼, 𝑗𝐽𝑆)𝑗)))))
92 nfcv 2907 . . . . . 6 𝑥(𝐺 DProd (𝑗𝐽 ↦ (𝑖(𝑖𝐼, 𝑗𝐽𝑆)𝑗)))
93 nfcv 2907 . . . . . . 7 𝑖 DProd
9429, 93, 36nfov 7386 . . . . . 6 𝑖(𝐺 DProd (𝑗𝑥 / 𝑖𝐽 ↦ (𝑥(𝑖𝐼, 𝑗𝐽𝑆)𝑗)))
9540oveq2d 7372 . . . . . 6 (𝑖 = 𝑥 → (𝐺 DProd (𝑗𝐽 ↦ (𝑖(𝑖𝐼, 𝑗𝐽𝑆)𝑗))) = (𝐺 DProd (𝑗𝑥 / 𝑖𝐽 ↦ (𝑥(𝑖𝐼, 𝑗𝐽𝑆)𝑗))))
9692, 94, 95cbvmpt 5216 . . . . 5 (𝑖𝐼 ↦ (𝐺 DProd (𝑗𝐽 ↦ (𝑖(𝑖𝐼, 𝑗𝐽𝑆)𝑗)))) = (𝑥𝐼 ↦ (𝐺 DProd (𝑗𝑥 / 𝑖𝐽 ↦ (𝑥(𝑖𝐼, 𝑗𝐽𝑆)𝑗))))
9786oveq2d 7372 . . . . . 6 ((𝜑𝑥𝐼) → (𝐺 DProd (𝑗𝑥 / 𝑖𝐽 ↦ (𝑥(𝑖𝐼, 𝑗𝐽𝑆)𝑗))) = (𝐺 DProd (𝑦 ∈ ( 𝑖𝐼 ({𝑖} × 𝐽) “ {𝑥}) ↦ (𝑥(𝑖𝐼, 𝑗𝐽𝑆)𝑦))))
9897mpteq2dva 5205 . . . . 5 (𝜑 → (𝑥𝐼 ↦ (𝐺 DProd (𝑗𝑥 / 𝑖𝐽 ↦ (𝑥(𝑖𝐼, 𝑗𝐽𝑆)𝑗)))) = (𝑥𝐼 ↦ (𝐺 DProd (𝑦 ∈ ( 𝑖𝐼 ({𝑖} × 𝐽) “ {𝑥}) ↦ (𝑥(𝑖𝐼, 𝑗𝐽𝑆)𝑦)))))
9996, 98eqtrid 2788 . . . 4 (𝜑 → (𝑖𝐼 ↦ (𝐺 DProd (𝑗𝐽 ↦ (𝑖(𝑖𝐼, 𝑗𝐽𝑆)𝑗)))) = (𝑥𝐼 ↦ (𝐺 DProd (𝑦 ∈ ( 𝑖𝐼 ({𝑖} × 𝐽) “ {𝑥}) ↦ (𝑥(𝑖𝐼, 𝑗𝐽𝑆)𝑦)))))
10091, 99breqtrd 5131 . . 3 (𝜑𝐺dom DProd (𝑥𝐼 ↦ (𝐺 DProd (𝑦 ∈ ( 𝑖𝐼 ({𝑖} × 𝐽) “ {𝑥}) ↦ (𝑥(𝑖𝐼, 𝑗𝐽𝑆)𝑦)))))
101 eqid 2736 . . 3 (mrCls‘(SubGrp‘𝐺)) = (mrCls‘(SubGrp‘𝐺))
1025, 10, 19, 87, 100, 101dprd2da 19819 . 2 (𝜑𝐺dom DProd (𝑖𝐼, 𝑗𝐽𝑆))
1035, 10, 19, 87, 100, 101dprd2db 19820 . . 3 (𝜑 → (𝐺 DProd (𝑖𝐼, 𝑗𝐽𝑆)) = (𝐺 DProd (𝑥𝐼 ↦ (𝐺 DProd (𝑦 ∈ ( 𝑖𝐼 ({𝑖} × 𝐽) “ {𝑥}) ↦ (𝑥(𝑖𝐼, 𝑗𝐽𝑆)𝑦))))))
10499, 90eqtr3d 2778 . . . 4 (𝜑 → (𝑥𝐼 ↦ (𝐺 DProd (𝑦 ∈ ( 𝑖𝐼 ({𝑖} × 𝐽) “ {𝑥}) ↦ (𝑥(𝑖𝐼, 𝑗𝐽𝑆)𝑦)))) = (𝑖𝐼 ↦ (𝐺 DProd (𝑗𝐽𝑆))))
105104oveq2d 7372 . . 3 (𝜑 → (𝐺 DProd (𝑥𝐼 ↦ (𝐺 DProd (𝑦 ∈ ( 𝑖𝐼 ({𝑖} × 𝐽) “ {𝑥}) ↦ (𝑥(𝑖𝐼, 𝑗𝐽𝑆)𝑦))))) = (𝐺 DProd (𝑖𝐼 ↦ (𝐺 DProd (𝑗𝐽𝑆)))))
106103, 105eqtrd 2776 . 2 (𝜑 → (𝐺 DProd (𝑖𝐼, 𝑗𝐽𝑆)) = (𝐺 DProd (𝑖𝐼 ↦ (𝐺 DProd (𝑗𝐽𝑆)))))
107102, 106jca 512 1 (𝜑 → (𝐺dom DProd (𝑖𝐼, 𝑗𝐽𝑆) ∧ (𝐺 DProd (𝑖𝐼, 𝑗𝐽𝑆)) = (𝐺 DProd (𝑖𝐼 ↦ (𝐺 DProd (𝑗𝐽𝑆))))))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205  wa 396   = wceq 1541  wex 1781  wcel 2106  wral 3064  csb 3855  wss 3910  {csn 4586  cop 4592   ciun 4954   class class class wbr 5105  cmpt 5188   × cxp 5631  dom cdm 5633  cima 5636  Rel wrel 5638  wf 6492  cfv 6496  (class class class)co 7356  cmpo 7358  mrClscmrc 17462  SubGrpcsubg 18920   DProd cdprd 19770
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2707  ax-rep 5242  ax-sep 5256  ax-nul 5263  ax-pow 5320  ax-pr 5384  ax-un 7671  ax-cnex 11106  ax-resscn 11107  ax-1cn 11108  ax-icn 11109  ax-addcl 11110  ax-addrcl 11111  ax-mulcl 11112  ax-mulrcl 11113  ax-mulcom 11114  ax-addass 11115  ax-mulass 11116  ax-distr 11117  ax-i2m1 11118  ax-1ne0 11119  ax-1rid 11120  ax-rnegex 11121  ax-rrecex 11122  ax-cnre 11123  ax-pre-lttri 11124  ax-pre-lttrn 11125  ax-pre-ltadd 11126  ax-pre-mulgt0 11127
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3or 1088  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2538  df-eu 2567  df-clab 2714  df-cleq 2728  df-clel 2814  df-nfc 2889  df-ne 2944  df-nel 3050  df-ral 3065  df-rex 3074  df-rmo 3353  df-reu 3354  df-rab 3408  df-v 3447  df-sbc 3740  df-csb 3856  df-dif 3913  df-un 3915  df-in 3917  df-ss 3927  df-pss 3929  df-nul 4283  df-if 4487  df-pw 4562  df-sn 4587  df-pr 4589  df-op 4593  df-uni 4866  df-int 4908  df-iun 4956  df-iin 4957  df-br 5106  df-opab 5168  df-mpt 5189  df-tr 5223  df-id 5531  df-eprel 5537  df-po 5545  df-so 5546  df-fr 5588  df-se 5589  df-we 5590  df-xp 5639  df-rel 5640  df-cnv 5641  df-co 5642  df-dm 5643  df-rn 5644  df-res 5645  df-ima 5646  df-pred 6253  df-ord 6320  df-on 6321  df-lim 6322  df-suc 6323  df-iota 6448  df-fun 6498  df-fn 6499  df-f 6500  df-f1 6501  df-fo 6502  df-f1o 6503  df-fv 6504  df-isom 6505  df-riota 7312  df-ov 7359  df-oprab 7360  df-mpo 7361  df-of 7616  df-om 7802  df-1st 7920  df-2nd 7921  df-supp 8092  df-tpos 8156  df-frecs 8211  df-wrecs 8242  df-recs 8316  df-rdg 8355  df-1o 8411  df-er 8647  df-map 8766  df-ixp 8835  df-en 8883  df-dom 8884  df-sdom 8885  df-fin 8886  df-fsupp 9305  df-oi 9445  df-card 9874  df-pnf 11190  df-mnf 11191  df-xr 11192  df-ltxr 11193  df-le 11194  df-sub 11386  df-neg 11387  df-nn 12153  df-2 12215  df-n0 12413  df-z 12499  df-uz 12763  df-fz 13424  df-fzo 13567  df-seq 13906  df-hash 14230  df-sets 17035  df-slot 17053  df-ndx 17065  df-base 17083  df-ress 17112  df-plusg 17145  df-0g 17322  df-gsum 17323  df-mre 17465  df-mrc 17466  df-acs 17468  df-mgm 18496  df-sgrp 18545  df-mnd 18556  df-mhm 18600  df-submnd 18601  df-grp 18750  df-minusg 18751  df-sbg 18752  df-mulg 18871  df-subg 18923  df-ghm 19004  df-gim 19047  df-cntz 19095  df-oppg 19122  df-lsm 19416  df-cmn 19562  df-dprd 19772
This theorem is referenced by:  ablfaclem2  19863
  Copyright terms: Public domain W3C validator