Metamath Proof Explorer

Theorem dprd2d2

Description: The direct product of a collection of direct products. (Contributed by Mario Carneiro, 26-Apr-2016)

Ref Expression
Hypotheses dprd2d2.1 ⊢ ( ( 𝜑 ∧ ( 𝑖 ∈ 𝐼 ∧ 𝑗 ∈ 𝐽 ) ) → 𝑆 ∈ ( SubGrp ‘ 𝐺 ) )
dprd2d2.2 ⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝐼 ) → 𝐺 dom DProd ( 𝑗 ∈ 𝐽 ↦ 𝑆 ) )
dprd2d2.3 ⊢ ( 𝜑 → 𝐺 dom DProd ( 𝑖 ∈ 𝐼 ↦ ( 𝐺 DProd ( 𝑗 ∈ 𝐽 ↦ 𝑆 ) ) ) )
Assertion dprd2d2 ( 𝜑 → ( 𝐺 dom DProd ( 𝑖 ∈ 𝐼 , 𝑗 ∈ 𝐽 ↦ 𝑆 ) ∧ ( 𝐺 DProd ( 𝑖 ∈ 𝐼 , 𝑗 ∈ 𝐽 ↦ 𝑆 ) ) = ( 𝐺 DProd ( 𝑖 ∈ 𝐼 ↦ ( 𝐺 DProd ( 𝑗 ∈ 𝐽 ↦ 𝑆 ) ) ) ) ) )

Proof

Step Hyp Ref Expression
1 dprd2d2.1 ⊢ ( ( 𝜑 ∧ ( 𝑖 ∈ 𝐼 ∧ 𝑗 ∈ 𝐽 ) ) → 𝑆 ∈ ( SubGrp ‘ 𝐺 ) )
2 dprd2d2.2 ⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝐼 ) → 𝐺 dom DProd ( 𝑗 ∈ 𝐽 ↦ 𝑆 ) )
3 dprd2d2.3 ⊢ ( 𝜑 → 𝐺 dom DProd ( 𝑖 ∈ 𝐼 ↦ ( 𝐺 DProd ( 𝑗 ∈ 𝐽 ↦ 𝑆 ) ) ) )
4 relxp ⊢ Rel ( { 𝑖 } × 𝐽 )
5 4 rgenw ⊢ ∀ 𝑖 ∈ 𝐼 Rel ( { 𝑖 } × 𝐽 )
6 reliun ⊢ ( Rel ∪ 𝑖 ∈ 𝐼 ( { 𝑖 } × 𝐽 ) ↔ ∀ 𝑖 ∈ 𝐼 Rel ( { 𝑖 } × 𝐽 ) )
7 5 6 mpbir ⊢ Rel ∪ 𝑖 ∈ 𝐼 ( { 𝑖 } × 𝐽 )
8 7 a1i ⊢ ( 𝜑 → Rel ∪ 𝑖 ∈ 𝐼 ( { 𝑖 } × 𝐽 ) )
9 1 ralrimivva ⊢ ( 𝜑 → ∀ 𝑖 ∈ 𝐼 ∀ 𝑗 ∈ 𝐽 𝑆 ∈ ( SubGrp ‘ 𝐺 ) )
10 eqid ⊢ ( 𝑖 ∈ 𝐼 , 𝑗 ∈ 𝐽 ↦ 𝑆 ) = ( 𝑖 ∈ 𝐼 , 𝑗 ∈ 𝐽 ↦ 𝑆 )
11 10 fmpox ⊢ ( ∀ 𝑖 ∈ 𝐼 ∀ 𝑗 ∈ 𝐽 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ↔ ( 𝑖 ∈ 𝐼 , 𝑗 ∈ 𝐽 ↦ 𝑆 ) : ∪ 𝑖 ∈ 𝐼 ( { 𝑖 } × 𝐽 ) ⟶ ( SubGrp ‘ 𝐺 ) )
12 9 11 sylib ⊢ ( 𝜑 → ( 𝑖 ∈ 𝐼 , 𝑗 ∈ 𝐽 ↦ 𝑆 ) : ∪ 𝑖 ∈ 𝐼 ( { 𝑖 } × 𝐽 ) ⟶ ( SubGrp ‘ 𝐺 ) )
13 dmiun ⊢ dom ∪ 𝑖 ∈ 𝐼 ( { 𝑖 } × 𝐽 ) = ∪ 𝑖 ∈ 𝐼 dom ( { 𝑖 } × 𝐽 )
14 dmxpss ⊢ dom ( { 𝑖 } × 𝐽 ) ⊆ { 𝑖 }
15 simpr ⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝐼 ) → 𝑖 ∈ 𝐼 )
16 15 snssd ⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝐼 ) → { 𝑖 } ⊆ 𝐼 )
17 14 16 sstrid ⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝐼 ) → dom ( { 𝑖 } × 𝐽 ) ⊆ 𝐼 )
18 17 ralrimiva ⊢ ( 𝜑 → ∀ 𝑖 ∈ 𝐼 dom ( { 𝑖 } × 𝐽 ) ⊆ 𝐼 )
19 iunss ⊢ ( ∪ 𝑖 ∈ 𝐼 dom ( { 𝑖 } × 𝐽 ) ⊆ 𝐼 ↔ ∀ 𝑖 ∈ 𝐼 dom ( { 𝑖 } × 𝐽 ) ⊆ 𝐼 )
20 18 19 sylibr ⊢ ( 𝜑 → ∪ 𝑖 ∈ 𝐼 dom ( { 𝑖 } × 𝐽 ) ⊆ 𝐼 )
21 13 20 eqsstrid ⊢ ( 𝜑 → dom ∪ 𝑖 ∈ 𝐼 ( { 𝑖 } × 𝐽 ) ⊆ 𝐼 )
22 simprl ⊢ ( ( 𝜑 ∧ ( 𝑖 ∈ 𝐼 ∧ 𝑗 ∈ 𝐽 ) ) → 𝑖 ∈ 𝐼 )
23 simprr ⊢ ( ( 𝜑 ∧ ( 𝑖 ∈ 𝐼 ∧ 𝑗 ∈ 𝐽 ) ) → 𝑗 ∈ 𝐽 )
24 10 ovmpt4g ⊢ ( ( 𝑖 ∈ 𝐼 ∧ 𝑗 ∈ 𝐽 ∧ 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ) → ( 𝑖 ( 𝑖 ∈ 𝐼 , 𝑗 ∈ 𝐽 ↦ 𝑆 ) 𝑗 ) = 𝑆 )
25 22 23 1 24 syl3anc ⊢ ( ( 𝜑 ∧ ( 𝑖 ∈ 𝐼 ∧ 𝑗 ∈ 𝐽 ) ) → ( 𝑖 ( 𝑖 ∈ 𝐼 , 𝑗 ∈ 𝐽 ↦ 𝑆 ) 𝑗 ) = 𝑆 )
26 25 anassrs ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ 𝐼 ) ∧ 𝑗 ∈ 𝐽 ) → ( 𝑖 ( 𝑖 ∈ 𝐼 , 𝑗 ∈ 𝐽 ↦ 𝑆 ) 𝑗 ) = 𝑆 )
27 26 mpteq2dva ⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝐼 ) → ( 𝑗 ∈ 𝐽 ↦ ( 𝑖 ( 𝑖 ∈ 𝐼 , 𝑗 ∈ 𝐽 ↦ 𝑆 ) 𝑗 ) ) = ( 𝑗 ∈ 𝐽 ↦ 𝑆 ) )
28 2 27 breqtrrd ⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝐼 ) → 𝐺 dom DProd ( 𝑗 ∈ 𝐽 ↦ ( 𝑖 ( 𝑖 ∈ 𝐼 , 𝑗 ∈ 𝐽 ↦ 𝑆 ) 𝑗 ) ) )
29 28 ralrimiva ⊢ ( 𝜑 → ∀ 𝑖 ∈ 𝐼 𝐺 dom DProd ( 𝑗 ∈ 𝐽 ↦ ( 𝑖 ( 𝑖 ∈ 𝐼 , 𝑗 ∈ 𝐽 ↦ 𝑆 ) 𝑗 ) ) )
30 nfcv ⊢ Ⅎ 𝑖 𝐺
31 nfcv ⊢ Ⅎ 𝑖 dom DProd
32 nfcsb1v ⊢ Ⅎ 𝑖 ⦋ 𝑥 / 𝑖 ⦌ 𝐽
33 nfcv ⊢ Ⅎ 𝑖 𝑥
34 nfmpo1 ⊢ Ⅎ 𝑖 ( 𝑖 ∈ 𝐼 , 𝑗 ∈ 𝐽 ↦ 𝑆 )
35 nfcv ⊢ Ⅎ 𝑖 𝑗
36 33 34 35 nfov ⊢ Ⅎ 𝑖 ( 𝑥 ( 𝑖 ∈ 𝐼 , 𝑗 ∈ 𝐽 ↦ 𝑆 ) 𝑗 )
37 32 36 nfmpt ⊢ Ⅎ 𝑖 ( 𝑗 ∈ ⦋ 𝑥 / 𝑖 ⦌ 𝐽 ↦ ( 𝑥 ( 𝑖 ∈ 𝐼 , 𝑗 ∈ 𝐽 ↦ 𝑆 ) 𝑗 ) )
38 30 31 37 nfbr ⊢ Ⅎ 𝑖 𝐺 dom DProd ( 𝑗 ∈ ⦋ 𝑥 / 𝑖 ⦌ 𝐽 ↦ ( 𝑥 ( 𝑖 ∈ 𝐼 , 𝑗 ∈ 𝐽 ↦ 𝑆 ) 𝑗 ) )
39 csbeq1a ⊢ ( 𝑖 = 𝑥 → 𝐽 = ⦋ 𝑥 / 𝑖 ⦌ 𝐽 )
40 oveq1 ⊢ ( 𝑖 = 𝑥 → ( 𝑖 ( 𝑖 ∈ 𝐼 , 𝑗 ∈ 𝐽 ↦ 𝑆 ) 𝑗 ) = ( 𝑥 ( 𝑖 ∈ 𝐼 , 𝑗 ∈ 𝐽 ↦ 𝑆 ) 𝑗 ) )
41 39 40 mpteq12dv ⊢ ( 𝑖 = 𝑥 → ( 𝑗 ∈ 𝐽 ↦ ( 𝑖 ( 𝑖 ∈ 𝐼 , 𝑗 ∈ 𝐽 ↦ 𝑆 ) 𝑗 ) ) = ( 𝑗 ∈ ⦋ 𝑥 / 𝑖 ⦌ 𝐽 ↦ ( 𝑥 ( 𝑖 ∈ 𝐼 , 𝑗 ∈ 𝐽 ↦ 𝑆 ) 𝑗 ) ) )
42 41 breq2d ⊢ ( 𝑖 = 𝑥 → ( 𝐺 dom DProd ( 𝑗 ∈ 𝐽 ↦ ( 𝑖 ( 𝑖 ∈ 𝐼 , 𝑗 ∈ 𝐽 ↦ 𝑆 ) 𝑗 ) ) ↔ 𝐺 dom DProd ( 𝑗 ∈ ⦋ 𝑥 / 𝑖 ⦌ 𝐽 ↦ ( 𝑥 ( 𝑖 ∈ 𝐼 , 𝑗 ∈ 𝐽 ↦ 𝑆 ) 𝑗 ) ) ) )
43 38 42 rspc ⊢ ( 𝑥 ∈ 𝐼 → ( ∀ 𝑖 ∈ 𝐼 𝐺 dom DProd ( 𝑗 ∈ 𝐽 ↦ ( 𝑖 ( 𝑖 ∈ 𝐼 , 𝑗 ∈ 𝐽 ↦ 𝑆 ) 𝑗 ) ) → 𝐺 dom DProd ( 𝑗 ∈ ⦋ 𝑥 / 𝑖 ⦌ 𝐽 ↦ ( 𝑥 ( 𝑖 ∈ 𝐼 , 𝑗 ∈ 𝐽 ↦ 𝑆 ) 𝑗 ) ) ) )
44 29 43 mpan9 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐼 ) → 𝐺 dom DProd ( 𝑗 ∈ ⦋ 𝑥 / 𝑖 ⦌ 𝐽 ↦ ( 𝑥 ( 𝑖 ∈ 𝐼 , 𝑗 ∈ 𝐽 ↦ 𝑆 ) 𝑗 ) ) )
45 nfcv ⊢ Ⅎ 𝑦 ( 𝑥 ( 𝑖 ∈ 𝐼 , 𝑗 ∈ 𝐽 ↦ 𝑆 ) 𝑗 )
46 nfcv ⊢ Ⅎ 𝑗 𝑥
47 nfmpo2 ⊢ Ⅎ 𝑗 ( 𝑖 ∈ 𝐼 , 𝑗 ∈ 𝐽 ↦ 𝑆 )
48 nfcv ⊢ Ⅎ 𝑗 𝑦
49 46 47 48 nfov ⊢ Ⅎ 𝑗 ( 𝑥 ( 𝑖 ∈ 𝐼 , 𝑗 ∈ 𝐽 ↦ 𝑆 ) 𝑦 )
50 oveq2 ⊢ ( 𝑗 = 𝑦 → ( 𝑥 ( 𝑖 ∈ 𝐼 , 𝑗 ∈ 𝐽 ↦ 𝑆 ) 𝑗 ) = ( 𝑥 ( 𝑖 ∈ 𝐼 , 𝑗 ∈ 𝐽 ↦ 𝑆 ) 𝑦 ) )
51 45 49 50 cbvmpt ⊢ ( 𝑗 ∈ ⦋ 𝑥 / 𝑖 ⦌ 𝐽 ↦ ( 𝑥 ( 𝑖 ∈ 𝐼 , 𝑗 ∈ 𝐽 ↦ 𝑆 ) 𝑗 ) ) = ( 𝑦 ∈ ⦋ 𝑥 / 𝑖 ⦌ 𝐽 ↦ ( 𝑥 ( 𝑖 ∈ 𝐼 , 𝑗 ∈ 𝐽 ↦ 𝑆 ) 𝑦 ) )
52 nfv ⊢ Ⅎ 𝑖 𝑗 = 𝑧
53 32 nfcri ⊢ Ⅎ 𝑖 𝑗 ∈ ⦋ 𝑥 / 𝑖 ⦌ 𝐽
54 52 53 nfan ⊢ Ⅎ 𝑖 ( 𝑗 = 𝑧 ∧ 𝑗 ∈ ⦋ 𝑥 / 𝑖 ⦌ 𝐽 )
55 39 eleq2d ⊢ ( 𝑖 = 𝑥 → ( 𝑗 ∈ 𝐽 ↔ 𝑗 ∈ ⦋ 𝑥 / 𝑖 ⦌ 𝐽 ) )
56 55 anbi2d ⊢ ( 𝑖 = 𝑥 → ( ( 𝑗 = 𝑧 ∧ 𝑗 ∈ 𝐽 ) ↔ ( 𝑗 = 𝑧 ∧ 𝑗 ∈ ⦋ 𝑥 / 𝑖 ⦌ 𝐽 ) ) )
57 54 56 equsexv ⊢ ( ∃ 𝑖 ( 𝑖 = 𝑥 ∧ ( 𝑗 = 𝑧 ∧ 𝑗 ∈ 𝐽 ) ) ↔ ( 𝑗 = 𝑧 ∧ 𝑗 ∈ ⦋ 𝑥 / 𝑖 ⦌ 𝐽 ) )
58 simprl ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐼 ) ∧ ( 𝑖 = 𝑥 ∧ 𝑗 = 𝑧 ) ) → 𝑖 = 𝑥 )
59 simplr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐼 ) ∧ ( 𝑖 = 𝑥 ∧ 𝑗 = 𝑧 ) ) → 𝑥 ∈ 𝐼 )
60 58 59 eqeltrd ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐼 ) ∧ ( 𝑖 = 𝑥 ∧ 𝑗 = 𝑧 ) ) → 𝑖 ∈ 𝐼 )
61 60 biantrurd ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐼 ) ∧ ( 𝑖 = 𝑥 ∧ 𝑗 = 𝑧 ) ) → ( 𝑗 ∈ 𝐽 ↔ ( 𝑖 ∈ 𝐼 ∧ 𝑗 ∈ 𝐽 ) ) )
62 61 pm5.32da ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐼 ) → ( ( ( 𝑖 = 𝑥 ∧ 𝑗 = 𝑧 ) ∧ 𝑗 ∈ 𝐽 ) ↔ ( ( 𝑖 = 𝑥 ∧ 𝑗 = 𝑧 ) ∧ ( 𝑖 ∈ 𝐼 ∧ 𝑗 ∈ 𝐽 ) ) ) )
63 anass ⊢ ( ( ( 𝑖 = 𝑥 ∧ 𝑗 = 𝑧 ) ∧ 𝑗 ∈ 𝐽 ) ↔ ( 𝑖 = 𝑥 ∧ ( 𝑗 = 𝑧 ∧ 𝑗 ∈ 𝐽 ) ) )
64 eqcom ⊢ ( ⟨ 𝑥 , 𝑧 ⟩ = ⟨ 𝑖 , 𝑗 ⟩ ↔ ⟨ 𝑖 , 𝑗 ⟩ = ⟨ 𝑥 , 𝑧 ⟩ )
65 vex ⊢ 𝑖 ∈ V
66 vex ⊢ 𝑗 ∈ V
67 65 66 opth ⊢ ( ⟨ 𝑖 , 𝑗 ⟩ = ⟨ 𝑥 , 𝑧 ⟩ ↔ ( 𝑖 = 𝑥 ∧ 𝑗 = 𝑧 ) )
68 64 67 bitr2i ⊢ ( ( 𝑖 = 𝑥 ∧ 𝑗 = 𝑧 ) ↔ ⟨ 𝑥 , 𝑧 ⟩ = ⟨ 𝑖 , 𝑗 ⟩ )
69 68 anbi1i ⊢ ( ( ( 𝑖 = 𝑥 ∧ 𝑗 = 𝑧 ) ∧ ( 𝑖 ∈ 𝐼 ∧ 𝑗 ∈ 𝐽 ) ) ↔ ( ⟨ 𝑥 , 𝑧 ⟩ = ⟨ 𝑖 , 𝑗 ⟩ ∧ ( 𝑖 ∈ 𝐼 ∧ 𝑗 ∈ 𝐽 ) ) )
70 62 63 69 3bitr3g ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐼 ) → ( ( 𝑖 = 𝑥 ∧ ( 𝑗 = 𝑧 ∧ 𝑗 ∈ 𝐽 ) ) ↔ ( ⟨ 𝑥 , 𝑧 ⟩ = ⟨ 𝑖 , 𝑗 ⟩ ∧ ( 𝑖 ∈ 𝐼 ∧ 𝑗 ∈ 𝐽 ) ) ) )
71 70 exbidv ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐼 ) → ( ∃ 𝑖 ( 𝑖 = 𝑥 ∧ ( 𝑗 = 𝑧 ∧ 𝑗 ∈ 𝐽 ) ) ↔ ∃ 𝑖 ( ⟨ 𝑥 , 𝑧 ⟩ = ⟨ 𝑖 , 𝑗 ⟩ ∧ ( 𝑖 ∈ 𝐼 ∧ 𝑗 ∈ 𝐽 ) ) ) )
72 57 71 bitr3id ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐼 ) → ( ( 𝑗 = 𝑧 ∧ 𝑗 ∈ ⦋ 𝑥 / 𝑖 ⦌ 𝐽 ) ↔ ∃ 𝑖 ( ⟨ 𝑥 , 𝑧 ⟩ = ⟨ 𝑖 , 𝑗 ⟩ ∧ ( 𝑖 ∈ 𝐼 ∧ 𝑗 ∈ 𝐽 ) ) ) )
73 72 exbidv ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐼 ) → ( ∃ 𝑗 ( 𝑗 = 𝑧 ∧ 𝑗 ∈ ⦋ 𝑥 / 𝑖 ⦌ 𝐽 ) ↔ ∃ 𝑗 ∃ 𝑖 ( ⟨ 𝑥 , 𝑧 ⟩ = ⟨ 𝑖 , 𝑗 ⟩ ∧ ( 𝑖 ∈ 𝐼 ∧ 𝑗 ∈ 𝐽 ) ) ) )
74 vex ⊢ 𝑧 ∈ V
75 eleq1w ⊢ ( 𝑗 = 𝑧 → ( 𝑗 ∈ ⦋ 𝑥 / 𝑖 ⦌ 𝐽 ↔ 𝑧 ∈ ⦋ 𝑥 / 𝑖 ⦌ 𝐽 ) )
76 74 75 ceqsexv ⊢ ( ∃ 𝑗 ( 𝑗 = 𝑧 ∧ 𝑗 ∈ ⦋ 𝑥 / 𝑖 ⦌ 𝐽 ) ↔ 𝑧 ∈ ⦋ 𝑥 / 𝑖 ⦌ 𝐽 )
77 excom ⊢ ( ∃ 𝑗 ∃ 𝑖 ( ⟨ 𝑥 , 𝑧 ⟩ = ⟨ 𝑖 , 𝑗 ⟩ ∧ ( 𝑖 ∈ 𝐼 ∧ 𝑗 ∈ 𝐽 ) ) ↔ ∃ 𝑖 ∃ 𝑗 ( ⟨ 𝑥 , 𝑧 ⟩ = ⟨ 𝑖 , 𝑗 ⟩ ∧ ( 𝑖 ∈ 𝐼 ∧ 𝑗 ∈ 𝐽 ) ) )
78 73 76 77 3bitr3g ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐼 ) → ( 𝑧 ∈ ⦋ 𝑥 / 𝑖 ⦌ 𝐽 ↔ ∃ 𝑖 ∃ 𝑗 ( ⟨ 𝑥 , 𝑧 ⟩ = ⟨ 𝑖 , 𝑗 ⟩ ∧ ( 𝑖 ∈ 𝐼 ∧ 𝑗 ∈ 𝐽 ) ) ) )
79 elrelimasn ⊢ ( Rel ∪ 𝑖 ∈ 𝐼 ( { 𝑖 } × 𝐽 ) → ( 𝑧 ∈ ( ∪ 𝑖 ∈ 𝐼 ( { 𝑖 } × 𝐽 ) “ { 𝑥 } ) ↔ 𝑥 ∪ 𝑖 ∈ 𝐼 ( { 𝑖 } × 𝐽 ) 𝑧 ) )
80 7 79 ax-mp ⊢ ( 𝑧 ∈ ( ∪ 𝑖 ∈ 𝐼 ( { 𝑖 } × 𝐽 ) “ { 𝑥 } ) ↔ 𝑥 ∪ 𝑖 ∈ 𝐼 ( { 𝑖 } × 𝐽 ) 𝑧 )
81 df-br ⊢ ( 𝑥 ∪ 𝑖 ∈ 𝐼 ( { 𝑖 } × 𝐽 ) 𝑧 ↔ ⟨ 𝑥 , 𝑧 ⟩ ∈ ∪ 𝑖 ∈ 𝐼 ( { 𝑖 } × 𝐽 ) )
82 eliunxp ⊢ ( ⟨ 𝑥 , 𝑧 ⟩ ∈ ∪ 𝑖 ∈ 𝐼 ( { 𝑖 } × 𝐽 ) ↔ ∃ 𝑖 ∃ 𝑗 ( ⟨ 𝑥 , 𝑧 ⟩ = ⟨ 𝑖 , 𝑗 ⟩ ∧ ( 𝑖 ∈ 𝐼 ∧ 𝑗 ∈ 𝐽 ) ) )
83 80 81 82 3bitri ⊢ ( 𝑧 ∈ ( ∪ 𝑖 ∈ 𝐼 ( { 𝑖 } × 𝐽 ) “ { 𝑥 } ) ↔ ∃ 𝑖 ∃ 𝑗 ( ⟨ 𝑥 , 𝑧 ⟩ = ⟨ 𝑖 , 𝑗 ⟩ ∧ ( 𝑖 ∈ 𝐼 ∧ 𝑗 ∈ 𝐽 ) ) )
84 78 83 bitr4di ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐼 ) → ( 𝑧 ∈ ⦋ 𝑥 / 𝑖 ⦌ 𝐽 ↔ 𝑧 ∈ ( ∪ 𝑖 ∈ 𝐼 ( { 𝑖 } × 𝐽 ) “ { 𝑥 } ) ) )
85 84 eqrdv ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐼 ) → ⦋ 𝑥 / 𝑖 ⦌ 𝐽 = ( ∪ 𝑖 ∈ 𝐼 ( { 𝑖 } × 𝐽 ) “ { 𝑥 } ) )
86 85 mpteq1d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐼 ) → ( 𝑦 ∈ ⦋ 𝑥 / 𝑖 ⦌ 𝐽 ↦ ( 𝑥 ( 𝑖 ∈ 𝐼 , 𝑗 ∈ 𝐽 ↦ 𝑆 ) 𝑦 ) ) = ( 𝑦 ∈ ( ∪ 𝑖 ∈ 𝐼 ( { 𝑖 } × 𝐽 ) “ { 𝑥 } ) ↦ ( 𝑥 ( 𝑖 ∈ 𝐼 , 𝑗 ∈ 𝐽 ↦ 𝑆 ) 𝑦 ) ) )
87 51 86 syl5eq ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐼 ) → ( 𝑗 ∈ ⦋ 𝑥 / 𝑖 ⦌ 𝐽 ↦ ( 𝑥 ( 𝑖 ∈ 𝐼 , 𝑗 ∈ 𝐽 ↦ 𝑆 ) 𝑗 ) ) = ( 𝑦 ∈ ( ∪ 𝑖 ∈ 𝐼 ( { 𝑖 } × 𝐽 ) “ { 𝑥 } ) ↦ ( 𝑥 ( 𝑖 ∈ 𝐼 , 𝑗 ∈ 𝐽 ↦ 𝑆 ) 𝑦 ) ) )
88 44 87 breqtrd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐼 ) → 𝐺 dom DProd ( 𝑦 ∈ ( ∪ 𝑖 ∈ 𝐼 ( { 𝑖 } × 𝐽 ) “ { 𝑥 } ) ↦ ( 𝑥 ( 𝑖 ∈ 𝐼 , 𝑗 ∈ 𝐽 ↦ 𝑆 ) 𝑦 ) ) )
89 27 oveq2d ⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝐼 ) → ( 𝐺 DProd ( 𝑗 ∈ 𝐽 ↦ ( 𝑖 ( 𝑖 ∈ 𝐼 , 𝑗 ∈ 𝐽 ↦ 𝑆 ) 𝑗 ) ) ) = ( 𝐺 DProd ( 𝑗 ∈ 𝐽 ↦ 𝑆 ) ) )
90 89 mpteq2dva ⊢ ( 𝜑 → ( 𝑖 ∈ 𝐼 ↦ ( 𝐺 DProd ( 𝑗 ∈ 𝐽 ↦ ( 𝑖 ( 𝑖 ∈ 𝐼 , 𝑗 ∈ 𝐽 ↦ 𝑆 ) 𝑗 ) ) ) ) = ( 𝑖 ∈ 𝐼 ↦ ( 𝐺 DProd ( 𝑗 ∈ 𝐽 ↦ 𝑆 ) ) ) )
91 3 90 breqtrrd ⊢ ( 𝜑 → 𝐺 dom DProd ( 𝑖 ∈ 𝐼 ↦ ( 𝐺 DProd ( 𝑗 ∈ 𝐽 ↦ ( 𝑖 ( 𝑖 ∈ 𝐼 , 𝑗 ∈ 𝐽 ↦ 𝑆 ) 𝑗 ) ) ) ) )
92 nfcv ⊢ Ⅎ 𝑥 ( 𝐺 DProd ( 𝑗 ∈ 𝐽 ↦ ( 𝑖 ( 𝑖 ∈ 𝐼 , 𝑗 ∈ 𝐽 ↦ 𝑆 ) 𝑗 ) ) )
93 nfcv ⊢ Ⅎ 𝑖 DProd
94 30 93 37 nfov ⊢ Ⅎ 𝑖 ( 𝐺 DProd ( 𝑗 ∈ ⦋ 𝑥 / 𝑖 ⦌ 𝐽 ↦ ( 𝑥 ( 𝑖 ∈ 𝐼 , 𝑗 ∈ 𝐽 ↦ 𝑆 ) 𝑗 ) ) )
95 41 oveq2d ⊢ ( 𝑖 = 𝑥 → ( 𝐺 DProd ( 𝑗 ∈ 𝐽 ↦ ( 𝑖 ( 𝑖 ∈ 𝐼 , 𝑗 ∈ 𝐽 ↦ 𝑆 ) 𝑗 ) ) ) = ( 𝐺 DProd ( 𝑗 ∈ ⦋ 𝑥 / 𝑖 ⦌ 𝐽 ↦ ( 𝑥 ( 𝑖 ∈ 𝐼 , 𝑗 ∈ 𝐽 ↦ 𝑆 ) 𝑗 ) ) ) )
96 92 94 95 cbvmpt ⊢ ( 𝑖 ∈ 𝐼 ↦ ( 𝐺 DProd ( 𝑗 ∈ 𝐽 ↦ ( 𝑖 ( 𝑖 ∈ 𝐼 , 𝑗 ∈ 𝐽 ↦ 𝑆 ) 𝑗 ) ) ) ) = ( 𝑥 ∈ 𝐼 ↦ ( 𝐺 DProd ( 𝑗 ∈ ⦋ 𝑥 / 𝑖 ⦌ 𝐽 ↦ ( 𝑥 ( 𝑖 ∈ 𝐼 , 𝑗 ∈ 𝐽 ↦ 𝑆 ) 𝑗 ) ) ) )
97 87 oveq2d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐼 ) → ( 𝐺 DProd ( 𝑗 ∈ ⦋ 𝑥 / 𝑖 ⦌ 𝐽 ↦ ( 𝑥 ( 𝑖 ∈ 𝐼 , 𝑗 ∈ 𝐽 ↦ 𝑆 ) 𝑗 ) ) ) = ( 𝐺 DProd ( 𝑦 ∈ ( ∪ 𝑖 ∈ 𝐼 ( { 𝑖 } × 𝐽 ) “ { 𝑥 } ) ↦ ( 𝑥 ( 𝑖 ∈ 𝐼 , 𝑗 ∈ 𝐽 ↦ 𝑆 ) 𝑦 ) ) ) )
98 97 mpteq2dva ⊢ ( 𝜑 → ( 𝑥 ∈ 𝐼 ↦ ( 𝐺 DProd ( 𝑗 ∈ ⦋ 𝑥 / 𝑖 ⦌ 𝐽 ↦ ( 𝑥 ( 𝑖 ∈ 𝐼 , 𝑗 ∈ 𝐽 ↦ 𝑆 ) 𝑗 ) ) ) ) = ( 𝑥 ∈ 𝐼 ↦ ( 𝐺 DProd ( 𝑦 ∈ ( ∪ 𝑖 ∈ 𝐼 ( { 𝑖 } × 𝐽 ) “ { 𝑥 } ) ↦ ( 𝑥 ( 𝑖 ∈ 𝐼 , 𝑗 ∈ 𝐽 ↦ 𝑆 ) 𝑦 ) ) ) ) )
99 96 98 syl5eq ⊢ ( 𝜑 → ( 𝑖 ∈ 𝐼 ↦ ( 𝐺 DProd ( 𝑗 ∈ 𝐽 ↦ ( 𝑖 ( 𝑖 ∈ 𝐼 , 𝑗 ∈ 𝐽 ↦ 𝑆 ) 𝑗 ) ) ) ) = ( 𝑥 ∈ 𝐼 ↦ ( 𝐺 DProd ( 𝑦 ∈ ( ∪ 𝑖 ∈ 𝐼 ( { 𝑖 } × 𝐽 ) “ { 𝑥 } ) ↦ ( 𝑥 ( 𝑖 ∈ 𝐼 , 𝑗 ∈ 𝐽 ↦ 𝑆 ) 𝑦 ) ) ) ) )
100 91 99 breqtrd ⊢ ( 𝜑 → 𝐺 dom DProd ( 𝑥 ∈ 𝐼 ↦ ( 𝐺 DProd ( 𝑦 ∈ ( ∪ 𝑖 ∈ 𝐼 ( { 𝑖 } × 𝐽 ) “ { 𝑥 } ) ↦ ( 𝑥 ( 𝑖 ∈ 𝐼 , 𝑗 ∈ 𝐽 ↦ 𝑆 ) 𝑦 ) ) ) ) )
101 eqid ⊢ ( mrCls ‘ ( SubGrp ‘ 𝐺 ) ) = ( mrCls ‘ ( SubGrp ‘ 𝐺 ) )
102 8 12 21 88 100 101 dprd2da ⊢ ( 𝜑 → 𝐺 dom DProd ( 𝑖 ∈ 𝐼 , 𝑗 ∈ 𝐽 ↦ 𝑆 ) )
103 8 12 21 88 100 101 dprd2db ⊢ ( 𝜑 → ( 𝐺 DProd ( 𝑖 ∈ 𝐼 , 𝑗 ∈ 𝐽 ↦ 𝑆 ) ) = ( 𝐺 DProd ( 𝑥 ∈ 𝐼 ↦ ( 𝐺 DProd ( 𝑦 ∈ ( ∪ 𝑖 ∈ 𝐼 ( { 𝑖 } × 𝐽 ) “ { 𝑥 } ) ↦ ( 𝑥 ( 𝑖 ∈ 𝐼 , 𝑗 ∈ 𝐽 ↦ 𝑆 ) 𝑦 ) ) ) ) ) )
104 99 90 eqtr3d ⊢ ( 𝜑 → ( 𝑥 ∈ 𝐼 ↦ ( 𝐺 DProd ( 𝑦 ∈ ( ∪ 𝑖 ∈ 𝐼 ( { 𝑖 } × 𝐽 ) “ { 𝑥 } ) ↦ ( 𝑥 ( 𝑖 ∈ 𝐼 , 𝑗 ∈ 𝐽 ↦ 𝑆 ) 𝑦 ) ) ) ) = ( 𝑖 ∈ 𝐼 ↦ ( 𝐺 DProd ( 𝑗 ∈ 𝐽 ↦ 𝑆 ) ) ) )
105 104 oveq2d ⊢ ( 𝜑 → ( 𝐺 DProd ( 𝑥 ∈ 𝐼 ↦ ( 𝐺 DProd ( 𝑦 ∈ ( ∪ 𝑖 ∈ 𝐼 ( { 𝑖 } × 𝐽 ) “ { 𝑥 } ) ↦ ( 𝑥 ( 𝑖 ∈ 𝐼 , 𝑗 ∈ 𝐽 ↦ 𝑆 ) 𝑦 ) ) ) ) ) = ( 𝐺 DProd ( 𝑖 ∈ 𝐼 ↦ ( 𝐺 DProd ( 𝑗 ∈ 𝐽 ↦ 𝑆 ) ) ) ) )
106 103 105 eqtrd ⊢ ( 𝜑 → ( 𝐺 DProd ( 𝑖 ∈ 𝐼 , 𝑗 ∈ 𝐽 ↦ 𝑆 ) ) = ( 𝐺 DProd ( 𝑖 ∈ 𝐼 ↦ ( 𝐺 DProd ( 𝑗 ∈ 𝐽 ↦ 𝑆 ) ) ) ) )
107 102 106 jca ⊢ ( 𝜑 → ( 𝐺 dom DProd ( 𝑖 ∈ 𝐼 , 𝑗 ∈ 𝐽 ↦ 𝑆 ) ∧ ( 𝐺 DProd ( 𝑖 ∈ 𝐼 , 𝑗 ∈ 𝐽 ↦ 𝑆 ) ) = ( 𝐺 DProd ( 𝑖 ∈ 𝐼 ↦ ( 𝐺 DProd ( 𝑗 ∈ 𝐽 ↦ 𝑆 ) ) ) ) ) )