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

Theorem dprd2d2 18367
 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 5190 . . . . . 6 Rel ({𝑖} × 𝐽)
21rgenw 2919 . . . . 5 𝑖𝐼 Rel ({𝑖} × 𝐽)
3 reliun 5202 . . . . 5 (Rel 𝑖𝐼 ({𝑖} × 𝐽) ↔ ∀𝑖𝐼 Rel ({𝑖} × 𝐽))
42, 3mpbir 221 . . . 4 Rel 𝑖𝐼 ({𝑖} × 𝐽)
54a1i 11 . . 3 (𝜑 → Rel 𝑖𝐼 ({𝑖} × 𝐽))
6 dprd2d2.1 . . . . 5 ((𝜑 ∧ (𝑖𝐼𝑗𝐽)) → 𝑆 ∈ (SubGrp‘𝐺))
76ralrimivva 2965 . . . 4 (𝜑 → ∀𝑖𝐼𝑗𝐽 𝑆 ∈ (SubGrp‘𝐺))
8 eqid 2621 . . . . 5 (𝑖𝐼, 𝑗𝐽𝑆) = (𝑖𝐼, 𝑗𝐽𝑆)
98fmpt2x 7184 . . . 4 (∀𝑖𝐼𝑗𝐽 𝑆 ∈ (SubGrp‘𝐺) ↔ (𝑖𝐼, 𝑗𝐽𝑆): 𝑖𝐼 ({𝑖} × 𝐽)⟶(SubGrp‘𝐺))
107, 9sylib 208 . . 3 (𝜑 → (𝑖𝐼, 𝑗𝐽𝑆): 𝑖𝐼 ({𝑖} × 𝐽)⟶(SubGrp‘𝐺))
11 dmiun 5295 . . . 4 dom 𝑖𝐼 ({𝑖} × 𝐽) = 𝑖𝐼 dom ({𝑖} × 𝐽)
12 dmxpss 5526 . . . . . . 7 dom ({𝑖} × 𝐽) ⊆ {𝑖}
13 simpr 477 . . . . . . . 8 ((𝜑𝑖𝐼) → 𝑖𝐼)
1413snssd 4311 . . . . . . 7 ((𝜑𝑖𝐼) → {𝑖} ⊆ 𝐼)
1512, 14syl5ss 3595 . . . . . 6 ((𝜑𝑖𝐼) → dom ({𝑖} × 𝐽) ⊆ 𝐼)
1615ralrimiva 2960 . . . . 5 (𝜑 → ∀𝑖𝐼 dom ({𝑖} × 𝐽) ⊆ 𝐼)
17 iunss 4529 . . . . 5 ( 𝑖𝐼 dom ({𝑖} × 𝐽) ⊆ 𝐼 ↔ ∀𝑖𝐼 dom ({𝑖} × 𝐽) ⊆ 𝐼)
1816, 17sylibr 224 . . . 4 (𝜑 𝑖𝐼 dom ({𝑖} × 𝐽) ⊆ 𝐼)
1911, 18syl5eqss 3630 . . 3 (𝜑 → dom 𝑖𝐼 ({𝑖} × 𝐽) ⊆ 𝐼)
20 dprd2d2.2 . . . . . . 7 ((𝜑𝑖𝐼) → 𝐺dom DProd (𝑗𝐽𝑆))
21 simprl 793 . . . . . . . . . 10 ((𝜑 ∧ (𝑖𝐼𝑗𝐽)) → 𝑖𝐼)
22 simprr 795 . . . . . . . . . 10 ((𝜑 ∧ (𝑖𝐼𝑗𝐽)) → 𝑗𝐽)
238ovmpt4g 6739 . . . . . . . . . 10 ((𝑖𝐼𝑗𝐽𝑆 ∈ (SubGrp‘𝐺)) → (𝑖(𝑖𝐼, 𝑗𝐽𝑆)𝑗) = 𝑆)
2421, 22, 6, 23syl3anc 1323 . . . . . . . . 9 ((𝜑 ∧ (𝑖𝐼𝑗𝐽)) → (𝑖(𝑖𝐼, 𝑗𝐽𝑆)𝑗) = 𝑆)
2524anassrs 679 . . . . . . . 8 (((𝜑𝑖𝐼) ∧ 𝑗𝐽) → (𝑖(𝑖𝐼, 𝑗𝐽𝑆)𝑗) = 𝑆)
2625mpteq2dva 4706 . . . . . . 7 ((𝜑𝑖𝐼) → (𝑗𝐽 ↦ (𝑖(𝑖𝐼, 𝑗𝐽𝑆)𝑗)) = (𝑗𝐽𝑆))
2720, 26breqtrrd 4643 . . . . . 6 ((𝜑𝑖𝐼) → 𝐺dom DProd (𝑗𝐽 ↦ (𝑖(𝑖𝐼, 𝑗𝐽𝑆)𝑗)))
2827ralrimiva 2960 . . . . 5 (𝜑 → ∀𝑖𝐼 𝐺dom DProd (𝑗𝐽 ↦ (𝑖(𝑖𝐼, 𝑗𝐽𝑆)𝑗)))
29 nfcv 2761 . . . . . . 7 𝑖𝐺
30 nfcv 2761 . . . . . . 7 𝑖dom DProd
31 nfcsb1v 3531 . . . . . . . 8 𝑖𝑥 / 𝑖𝐽
32 nfcv 2761 . . . . . . . . 9 𝑖𝑥
33 nfmpt21 6678 . . . . . . . . 9 𝑖(𝑖𝐼, 𝑗𝐽𝑆)
34 nfcv 2761 . . . . . . . . 9 𝑖𝑗
3532, 33, 34nfov 6633 . . . . . . . 8 𝑖(𝑥(𝑖𝐼, 𝑗𝐽𝑆)𝑗)
3631, 35nfmpt 4708 . . . . . . 7 𝑖(𝑗𝑥 / 𝑖𝐽 ↦ (𝑥(𝑖𝐼, 𝑗𝐽𝑆)𝑗))
3729, 30, 36nfbr 4661 . . . . . 6 𝑖 𝐺dom DProd (𝑗𝑥 / 𝑖𝐽 ↦ (𝑥(𝑖𝐼, 𝑗𝐽𝑆)𝑗))
38 csbeq1a 3524 . . . . . . . 8 (𝑖 = 𝑥𝐽 = 𝑥 / 𝑖𝐽)
39 oveq1 6614 . . . . . . . 8 (𝑖 = 𝑥 → (𝑖(𝑖𝐼, 𝑗𝐽𝑆)𝑗) = (𝑥(𝑖𝐼, 𝑗𝐽𝑆)𝑗))
4038, 39mpteq12dv 4695 . . . . . . 7 (𝑖 = 𝑥 → (𝑗𝐽 ↦ (𝑖(𝑖𝐼, 𝑗𝐽𝑆)𝑗)) = (𝑗𝑥 / 𝑖𝐽 ↦ (𝑥(𝑖𝐼, 𝑗𝐽𝑆)𝑗)))
4140breq2d 4627 . . . . . 6 (𝑖 = 𝑥 → (𝐺dom DProd (𝑗𝐽 ↦ (𝑖(𝑖𝐼, 𝑗𝐽𝑆)𝑗)) ↔ 𝐺dom DProd (𝑗𝑥 / 𝑖𝐽 ↦ (𝑥(𝑖𝐼, 𝑗𝐽𝑆)𝑗))))
4237, 41rspc 3289 . . . . 5 (𝑥𝐼 → (∀𝑖𝐼 𝐺dom DProd (𝑗𝐽 ↦ (𝑖(𝑖𝐼, 𝑗𝐽𝑆)𝑗)) → 𝐺dom DProd (𝑗𝑥 / 𝑖𝐽 ↦ (𝑥(𝑖𝐼, 𝑗𝐽𝑆)𝑗))))
4328, 42mpan9 486 . . . 4 ((𝜑𝑥𝐼) → 𝐺dom DProd (𝑗𝑥 / 𝑖𝐽 ↦ (𝑥(𝑖𝐼, 𝑗𝐽𝑆)𝑗)))
44 nfcv 2761 . . . . . 6 𝑦(𝑥(𝑖𝐼, 𝑗𝐽𝑆)𝑗)
45 nfcv 2761 . . . . . . 7 𝑗𝑥
46 nfmpt22 6679 . . . . . . 7 𝑗(𝑖𝐼, 𝑗𝐽𝑆)
47 nfcv 2761 . . . . . . 7 𝑗𝑦
4845, 46, 47nfov 6633 . . . . . 6 𝑗(𝑥(𝑖𝐼, 𝑗𝐽𝑆)𝑦)
49 oveq2 6615 . . . . . 6 (𝑗 = 𝑦 → (𝑥(𝑖𝐼, 𝑗𝐽𝑆)𝑗) = (𝑥(𝑖𝐼, 𝑗𝐽𝑆)𝑦))
5044, 48, 49cbvmpt 4711 . . . . 5 (𝑗𝑥 / 𝑖𝐽 ↦ (𝑥(𝑖𝐼, 𝑗𝐽𝑆)𝑗)) = (𝑦𝑥 / 𝑖𝐽 ↦ (𝑥(𝑖𝐼, 𝑗𝐽𝑆)𝑦))
51 nfv 1840 . . . . . . . . . . . . 13 𝑖 𝑗 = 𝑧
5231nfcri 2755 . . . . . . . . . . . . 13 𝑖 𝑗𝑥 / 𝑖𝐽
5351, 52nfan 1825 . . . . . . . . . . . 12 𝑖(𝑗 = 𝑧𝑗𝑥 / 𝑖𝐽)
5438eleq2d 2684 . . . . . . . . . . . . 13 (𝑖 = 𝑥 → (𝑗𝐽𝑗𝑥 / 𝑖𝐽))
5554anbi2d 739 . . . . . . . . . . . 12 (𝑖 = 𝑥 → ((𝑗 = 𝑧𝑗𝐽) ↔ (𝑗 = 𝑧𝑗𝑥 / 𝑖𝐽)))
5653, 55equsexv 2106 . . . . . . . . . . 11 (∃𝑖(𝑖 = 𝑥 ∧ (𝑗 = 𝑧𝑗𝐽)) ↔ (𝑗 = 𝑧𝑗𝑥 / 𝑖𝐽))
57 simprl 793 . . . . . . . . . . . . . . . 16 (((𝜑𝑥𝐼) ∧ (𝑖 = 𝑥𝑗 = 𝑧)) → 𝑖 = 𝑥)
58 simplr 791 . . . . . . . . . . . . . . . 16 (((𝜑𝑥𝐼) ∧ (𝑖 = 𝑥𝑗 = 𝑧)) → 𝑥𝐼)
5957, 58eqeltrd 2698 . . . . . . . . . . . . . . 15 (((𝜑𝑥𝐼) ∧ (𝑖 = 𝑥𝑗 = 𝑧)) → 𝑖𝐼)
6059biantrurd 529 . . . . . . . . . . . . . 14 (((𝜑𝑥𝐼) ∧ (𝑖 = 𝑥𝑗 = 𝑧)) → (𝑗𝐽 ↔ (𝑖𝐼𝑗𝐽)))
6160pm5.32da 672 . . . . . . . . . . . . 13 ((𝜑𝑥𝐼) → (((𝑖 = 𝑥𝑗 = 𝑧) ∧ 𝑗𝐽) ↔ ((𝑖 = 𝑥𝑗 = 𝑧) ∧ (𝑖𝐼𝑗𝐽))))
62 anass 680 . . . . . . . . . . . . 13 (((𝑖 = 𝑥𝑗 = 𝑧) ∧ 𝑗𝐽) ↔ (𝑖 = 𝑥 ∧ (𝑗 = 𝑧𝑗𝐽)))
63 eqcom 2628 . . . . . . . . . . . . . . 15 (⟨𝑥, 𝑧⟩ = ⟨𝑖, 𝑗⟩ ↔ ⟨𝑖, 𝑗⟩ = ⟨𝑥, 𝑧⟩)
64 vex 3189 . . . . . . . . . . . . . . . 16 𝑖 ∈ V
65 vex 3189 . . . . . . . . . . . . . . . 16 𝑗 ∈ V
6664, 65opth 4907 . . . . . . . . . . . . . . 15 (⟨𝑖, 𝑗⟩ = ⟨𝑥, 𝑧⟩ ↔ (𝑖 = 𝑥𝑗 = 𝑧))
6763, 66bitr2i 265 . . . . . . . . . . . . . 14 ((𝑖 = 𝑥𝑗 = 𝑧) ↔ ⟨𝑥, 𝑧⟩ = ⟨𝑖, 𝑗⟩)
6867anbi1i 730 . . . . . . . . . . . . 13 (((𝑖 = 𝑥𝑗 = 𝑧) ∧ (𝑖𝐼𝑗𝐽)) ↔ (⟨𝑥, 𝑧⟩ = ⟨𝑖, 𝑗⟩ ∧ (𝑖𝐼𝑗𝐽)))
6961, 62, 683bitr3g 302 . . . . . . . . . . . 12 ((𝜑𝑥𝐼) → ((𝑖 = 𝑥 ∧ (𝑗 = 𝑧𝑗𝐽)) ↔ (⟨𝑥, 𝑧⟩ = ⟨𝑖, 𝑗⟩ ∧ (𝑖𝐼𝑗𝐽))))
7069exbidv 1847 . . . . . . . . . . 11 ((𝜑𝑥𝐼) → (∃𝑖(𝑖 = 𝑥 ∧ (𝑗 = 𝑧𝑗𝐽)) ↔ ∃𝑖(⟨𝑥, 𝑧⟩ = ⟨𝑖, 𝑗⟩ ∧ (𝑖𝐼𝑗𝐽))))
7156, 70syl5bbr 274 . . . . . . . . . 10 ((𝜑𝑥𝐼) → ((𝑗 = 𝑧𝑗𝑥 / 𝑖𝐽) ↔ ∃𝑖(⟨𝑥, 𝑧⟩ = ⟨𝑖, 𝑗⟩ ∧ (𝑖𝐼𝑗𝐽))))
7271exbidv 1847 . . . . . . . . 9 ((𝜑𝑥𝐼) → (∃𝑗(𝑗 = 𝑧𝑗𝑥 / 𝑖𝐽) ↔ ∃𝑗𝑖(⟨𝑥, 𝑧⟩ = ⟨𝑖, 𝑗⟩ ∧ (𝑖𝐼𝑗𝐽))))
73 vex 3189 . . . . . . . . . 10 𝑧 ∈ V
74 eleq1 2686 . . . . . . . . . 10 (𝑗 = 𝑧 → (𝑗𝑥 / 𝑖𝐽𝑧𝑥 / 𝑖𝐽))
7573, 74ceqsexv 3228 . . . . . . . . 9 (∃𝑗(𝑗 = 𝑧𝑗𝑥 / 𝑖𝐽) ↔ 𝑧𝑥 / 𝑖𝐽)
76 excom 2039 . . . . . . . . 9 (∃𝑗𝑖(⟨𝑥, 𝑧⟩ = ⟨𝑖, 𝑗⟩ ∧ (𝑖𝐼𝑗𝐽)) ↔ ∃𝑖𝑗(⟨𝑥, 𝑧⟩ = ⟨𝑖, 𝑗⟩ ∧ (𝑖𝐼𝑗𝐽)))
7772, 75, 763bitr3g 302 . . . . . . . 8 ((𝜑𝑥𝐼) → (𝑧𝑥 / 𝑖𝐽 ↔ ∃𝑖𝑗(⟨𝑥, 𝑧⟩ = ⟨𝑖, 𝑗⟩ ∧ (𝑖𝐼𝑗𝐽))))
78 elrelimasn 5450 . . . . . . . . . 10 (Rel 𝑖𝐼 ({𝑖} × 𝐽) → (𝑧 ∈ ( 𝑖𝐼 ({𝑖} × 𝐽) “ {𝑥}) ↔ 𝑥 𝑖𝐼 ({𝑖} × 𝐽)𝑧))
794, 78ax-mp 5 . . . . . . . . 9 (𝑧 ∈ ( 𝑖𝐼 ({𝑖} × 𝐽) “ {𝑥}) ↔ 𝑥 𝑖𝐼 ({𝑖} × 𝐽)𝑧)
80 df-br 4616 . . . . . . . . 9 (𝑥 𝑖𝐼 ({𝑖} × 𝐽)𝑧 ↔ ⟨𝑥, 𝑧⟩ ∈ 𝑖𝐼 ({𝑖} × 𝐽))
81 eliunxp 5221 . . . . . . . . 9 (⟨𝑥, 𝑧⟩ ∈ 𝑖𝐼 ({𝑖} × 𝐽) ↔ ∃𝑖𝑗(⟨𝑥, 𝑧⟩ = ⟨𝑖, 𝑗⟩ ∧ (𝑖𝐼𝑗𝐽)))
8279, 80, 813bitri 286 . . . . . . . 8 (𝑧 ∈ ( 𝑖𝐼 ({𝑖} × 𝐽) “ {𝑥}) ↔ ∃𝑖𝑗(⟨𝑥, 𝑧⟩ = ⟨𝑖, 𝑗⟩ ∧ (𝑖𝐼𝑗𝐽)))
8377, 82syl6bbr 278 . . . . . . 7 ((𝜑𝑥𝐼) → (𝑧𝑥 / 𝑖𝐽𝑧 ∈ ( 𝑖𝐼 ({𝑖} × 𝐽) “ {𝑥})))
8483eqrdv 2619 . . . . . 6 ((𝜑𝑥𝐼) → 𝑥 / 𝑖𝐽 = ( 𝑖𝐼 ({𝑖} × 𝐽) “ {𝑥}))
8584mpteq1d 4700 . . . . 5 ((𝜑𝑥𝐼) → (𝑦𝑥 / 𝑖𝐽 ↦ (𝑥(𝑖𝐼, 𝑗𝐽𝑆)𝑦)) = (𝑦 ∈ ( 𝑖𝐼 ({𝑖} × 𝐽) “ {𝑥}) ↦ (𝑥(𝑖𝐼, 𝑗𝐽𝑆)𝑦)))
8650, 85syl5eq 2667 . . . 4 ((𝜑𝑥𝐼) → (𝑗𝑥 / 𝑖𝐽 ↦ (𝑥(𝑖𝐼, 𝑗𝐽𝑆)𝑗)) = (𝑦 ∈ ( 𝑖𝐼 ({𝑖} × 𝐽) “ {𝑥}) ↦ (𝑥(𝑖𝐼, 𝑗𝐽𝑆)𝑦)))
8743, 86breqtrd 4641 . . 3 ((𝜑𝑥𝐼) → 𝐺dom DProd (𝑦 ∈ ( 𝑖𝐼 ({𝑖} × 𝐽) “ {𝑥}) ↦ (𝑥(𝑖𝐼, 𝑗𝐽𝑆)𝑦)))
88 dprd2d2.3 . . . . 5 (𝜑𝐺dom DProd (𝑖𝐼 ↦ (𝐺 DProd (𝑗𝐽𝑆))))
8926oveq2d 6623 . . . . . 6 ((𝜑𝑖𝐼) → (𝐺 DProd (𝑗𝐽 ↦ (𝑖(𝑖𝐼, 𝑗𝐽𝑆)𝑗))) = (𝐺 DProd (𝑗𝐽𝑆)))
9089mpteq2dva 4706 . . . . 5 (𝜑 → (𝑖𝐼 ↦ (𝐺 DProd (𝑗𝐽 ↦ (𝑖(𝑖𝐼, 𝑗𝐽𝑆)𝑗)))) = (𝑖𝐼 ↦ (𝐺 DProd (𝑗𝐽𝑆))))
9188, 90breqtrrd 4643 . . . 4 (𝜑𝐺dom DProd (𝑖𝐼 ↦ (𝐺 DProd (𝑗𝐽 ↦ (𝑖(𝑖𝐼, 𝑗𝐽𝑆)𝑗)))))
92 nfcv 2761 . . . . . 6 𝑥(𝐺 DProd (𝑗𝐽 ↦ (𝑖(𝑖𝐼, 𝑗𝐽𝑆)𝑗)))
93 nfcv 2761 . . . . . . 7 𝑖 DProd
9429, 93, 36nfov 6633 . . . . . 6 𝑖(𝐺 DProd (𝑗𝑥 / 𝑖𝐽 ↦ (𝑥(𝑖𝐼, 𝑗𝐽𝑆)𝑗)))
9540oveq2d 6623 . . . . . 6 (𝑖 = 𝑥 → (𝐺 DProd (𝑗𝐽 ↦ (𝑖(𝑖𝐼, 𝑗𝐽𝑆)𝑗))) = (𝐺 DProd (𝑗𝑥 / 𝑖𝐽 ↦ (𝑥(𝑖𝐼, 𝑗𝐽𝑆)𝑗))))
9692, 94, 95cbvmpt 4711 . . . . 5 (𝑖𝐼 ↦ (𝐺 DProd (𝑗𝐽 ↦ (𝑖(𝑖𝐼, 𝑗𝐽𝑆)𝑗)))) = (𝑥𝐼 ↦ (𝐺 DProd (𝑗𝑥 / 𝑖𝐽 ↦ (𝑥(𝑖𝐼, 𝑗𝐽𝑆)𝑗))))
9786oveq2d 6623 . . . . . 6 ((𝜑𝑥𝐼) → (𝐺 DProd (𝑗𝑥 / 𝑖𝐽 ↦ (𝑥(𝑖𝐼, 𝑗𝐽𝑆)𝑗))) = (𝐺 DProd (𝑦 ∈ ( 𝑖𝐼 ({𝑖} × 𝐽) “ {𝑥}) ↦ (𝑥(𝑖𝐼, 𝑗𝐽𝑆)𝑦))))
9897mpteq2dva 4706 . . . . 5 (𝜑 → (𝑥𝐼 ↦ (𝐺 DProd (𝑗𝑥 / 𝑖𝐽 ↦ (𝑥(𝑖𝐼, 𝑗𝐽𝑆)𝑗)))) = (𝑥𝐼 ↦ (𝐺 DProd (𝑦 ∈ ( 𝑖𝐼 ({𝑖} × 𝐽) “ {𝑥}) ↦ (𝑥(𝑖𝐼, 𝑗𝐽𝑆)𝑦)))))
9996, 98syl5eq 2667 . . . 4 (𝜑 → (𝑖𝐼 ↦ (𝐺 DProd (𝑗𝐽 ↦ (𝑖(𝑖𝐼, 𝑗𝐽𝑆)𝑗)))) = (𝑥𝐼 ↦ (𝐺 DProd (𝑦 ∈ ( 𝑖𝐼 ({𝑖} × 𝐽) “ {𝑥}) ↦ (𝑥(𝑖𝐼, 𝑗𝐽𝑆)𝑦)))))
10091, 99breqtrd 4641 . . 3 (𝜑𝐺dom DProd (𝑥𝐼 ↦ (𝐺 DProd (𝑦 ∈ ( 𝑖𝐼 ({𝑖} × 𝐽) “ {𝑥}) ↦ (𝑥(𝑖𝐼, 𝑗𝐽𝑆)𝑦)))))
101 eqid 2621 . . 3 (mrCls‘(SubGrp‘𝐺)) = (mrCls‘(SubGrp‘𝐺))
1025, 10, 19, 87, 100, 101dprd2da 18365 . 2 (𝜑𝐺dom DProd (𝑖𝐼, 𝑗𝐽𝑆))
1035, 10, 19, 87, 100, 101dprd2db 18366 . . 3 (𝜑 → (𝐺 DProd (𝑖𝐼, 𝑗𝐽𝑆)) = (𝐺 DProd (𝑥𝐼 ↦ (𝐺 DProd (𝑦 ∈ ( 𝑖𝐼 ({𝑖} × 𝐽) “ {𝑥}) ↦ (𝑥(𝑖𝐼, 𝑗𝐽𝑆)𝑦))))))
10499, 90eqtr3d 2657 . . . 4 (𝜑 → (𝑥𝐼 ↦ (𝐺 DProd (𝑦 ∈ ( 𝑖𝐼 ({𝑖} × 𝐽) “ {𝑥}) ↦ (𝑥(𝑖𝐼, 𝑗𝐽𝑆)𝑦)))) = (𝑖𝐼 ↦ (𝐺 DProd (𝑗𝐽𝑆))))
105104oveq2d 6623 . . 3 (𝜑 → (𝐺 DProd (𝑥𝐼 ↦ (𝐺 DProd (𝑦 ∈ ( 𝑖𝐼 ({𝑖} × 𝐽) “ {𝑥}) ↦ (𝑥(𝑖𝐼, 𝑗𝐽𝑆)𝑦))))) = (𝐺 DProd (𝑖𝐼 ↦ (𝐺 DProd (𝑗𝐽𝑆)))))
106103, 105eqtrd 2655 . 2 (𝜑 → (𝐺 DProd (𝑖𝐼, 𝑗𝐽𝑆)) = (𝐺 DProd (𝑖𝐼 ↦ (𝐺 DProd (𝑗𝐽𝑆)))))
107102, 106jca 554 1 (𝜑 → (𝐺dom DProd (𝑖𝐼, 𝑗𝐽𝑆) ∧ (𝐺 DProd (𝑖𝐼, 𝑗𝐽𝑆)) = (𝐺 DProd (𝑖𝐼 ↦ (𝐺 DProd (𝑗𝐽𝑆))))))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 196   ∧ wa 384   = wceq 1480  ∃wex 1701   ∈ wcel 1987  ∀wral 2907  ⦋csb 3515   ⊆ wss 3556  {csn 4150  ⟨cop 4156  ∪ ciun 4487   class class class wbr 4615   ↦ cmpt 4675   × cxp 5074  dom cdm 5076   “ cima 5079  Rel wrel 5081  ⟶wf 5845  ‘cfv 5849  (class class class)co 6607   ↦ cmpt2 6609  mrClscmrc 16167  SubGrpcsubg 17512   DProd cdprd 18316 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-8 1989  ax-9 1996  ax-10 2016  ax-11 2031  ax-12 2044  ax-13 2245  ax-ext 2601  ax-rep 4733  ax-sep 4743  ax-nul 4751  ax-pow 4805  ax-pr 4869  ax-un 6905  ax-inf2 8485  ax-cnex 9939  ax-resscn 9940  ax-1cn 9941  ax-icn 9942  ax-addcl 9943  ax-addrcl 9944  ax-mulcl 9945  ax-mulrcl 9946  ax-mulcom 9947  ax-addass 9948  ax-mulass 9949  ax-distr 9950  ax-i2m1 9951  ax-1ne0 9952  ax-1rid 9953  ax-rnegex 9954  ax-rrecex 9955  ax-cnre 9956  ax-pre-lttri 9957  ax-pre-lttrn 9958  ax-pre-ltadd 9959  ax-pre-mulgt0 9960 This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3or 1037  df-3an 1038  df-tru 1483  df-ex 1702  df-nf 1707  df-sb 1878  df-eu 2473  df-mo 2474  df-clab 2608  df-cleq 2614  df-clel 2617  df-nfc 2750  df-ne 2791  df-nel 2894  df-ral 2912  df-rex 2913  df-reu 2914  df-rmo 2915  df-rab 2916  df-v 3188  df-sbc 3419  df-csb 3516  df-dif 3559  df-un 3561  df-in 3563  df-ss 3570  df-pss 3572  df-nul 3894  df-if 4061  df-pw 4134  df-sn 4151  df-pr 4153  df-tp 4155  df-op 4157  df-uni 4405  df-int 4443  df-iun 4489  df-iin 4490  df-br 4616  df-opab 4676  df-mpt 4677  df-tr 4715  df-eprel 4987  df-id 4991  df-po 4997  df-so 4998  df-fr 5035  df-se 5036  df-we 5037  df-xp 5082  df-rel 5083  df-cnv 5084  df-co 5085  df-dm 5086  df-rn 5087  df-res 5088  df-ima 5089  df-pred 5641  df-ord 5687  df-on 5688  df-lim 5689  df-suc 5690  df-iota 5812  df-fun 5851  df-fn 5852  df-f 5853  df-f1 5854  df-fo 5855  df-f1o 5856  df-fv 5857  df-isom 5858  df-riota 6568  df-ov 6610  df-oprab 6611  df-mpt2 6612  df-of 6853  df-om 7016  df-1st 7116  df-2nd 7117  df-supp 7244  df-tpos 7300  df-wrecs 7355  df-recs 7416  df-rdg 7454  df-1o 7508  df-oadd 7512  df-er 7690  df-map 7807  df-ixp 7856  df-en 7903  df-dom 7904  df-sdom 7905  df-fin 7906  df-fsupp 8223  df-oi 8362  df-card 8712  df-pnf 10023  df-mnf 10024  df-xr 10025  df-ltxr 10026  df-le 10027  df-sub 10215  df-neg 10216  df-nn 10968  df-2 11026  df-n0 11240  df-z 11325  df-uz 11635  df-fz 12272  df-fzo 12410  df-seq 12745  df-hash 13061  df-ndx 15787  df-slot 15788  df-base 15789  df-sets 15790  df-ress 15791  df-plusg 15878  df-0g 16026  df-gsum 16027  df-mre 16170  df-mrc 16171  df-acs 16173  df-mgm 17166  df-sgrp 17208  df-mnd 17219  df-mhm 17259  df-submnd 17260  df-grp 17349  df-minusg 17350  df-sbg 17351  df-mulg 17465  df-subg 17515  df-ghm 17582  df-gim 17625  df-cntz 17674  df-oppg 17700  df-lsm 17975  df-cmn 18119  df-dprd 18318 This theorem is referenced by:  ablfaclem2  18409
 Copyright terms: Public domain W3C validator