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

Theorem dprd2dlem2 19440
Description: The direct product of a collection of direct products. (Contributed by Mario Carneiro, 26-Apr-2016.)
Hypotheses
Ref Expression
dprd2d.1 (𝜑 → Rel 𝐴)
dprd2d.2 (𝜑𝑆:𝐴⟶(SubGrp‘𝐺))
dprd2d.3 (𝜑 → dom 𝐴𝐼)
dprd2d.4 ((𝜑𝑖𝐼) → 𝐺dom DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))
dprd2d.5 (𝜑𝐺dom DProd (𝑖𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))))
dprd2d.k 𝐾 = (mrCls‘(SubGrp‘𝐺))
Assertion
Ref Expression
dprd2dlem2 ((𝜑𝑋𝐴) → (𝑆𝑋) ⊆ (𝐺 DProd (𝑗 ∈ (𝐴 “ {(1st𝑋)}) ↦ ((1st𝑋)𝑆𝑗))))
Distinct variable groups:   𝑖,𝑗,𝐴   𝑖,𝐺,𝑗   𝑖,𝐼   𝑖,𝐾   𝜑,𝑖,𝑗   𝑆,𝑖,𝑗   𝑖,𝑋,𝑗
Allowed substitution hints:   𝐼(𝑗)   𝐾(𝑗)

Proof of Theorem dprd2dlem2
StepHypRef Expression
1 df-ov 7225 . . 3 ((1st𝑋)𝑆(2nd𝑋)) = (𝑆‘⟨(1st𝑋), (2nd𝑋)⟩)
2 dprd2d.1 . . . . . . . 8 (𝜑 → Rel 𝐴)
3 1st2nd 7819 . . . . . . . 8 ((Rel 𝐴𝑋𝐴) → 𝑋 = ⟨(1st𝑋), (2nd𝑋)⟩)
42, 3sylan 583 . . . . . . 7 ((𝜑𝑋𝐴) → 𝑋 = ⟨(1st𝑋), (2nd𝑋)⟩)
5 simpr 488 . . . . . . 7 ((𝜑𝑋𝐴) → 𝑋𝐴)
64, 5eqeltrrd 2840 . . . . . 6 ((𝜑𝑋𝐴) → ⟨(1st𝑋), (2nd𝑋)⟩ ∈ 𝐴)
7 df-br 5063 . . . . . 6 ((1st𝑋)𝐴(2nd𝑋) ↔ ⟨(1st𝑋), (2nd𝑋)⟩ ∈ 𝐴)
86, 7sylibr 237 . . . . 5 ((𝜑𝑋𝐴) → (1st𝑋)𝐴(2nd𝑋))
92adantr 484 . . . . . 6 ((𝜑𝑋𝐴) → Rel 𝐴)
10 elrelimasn 5962 . . . . . 6 (Rel 𝐴 → ((2nd𝑋) ∈ (𝐴 “ {(1st𝑋)}) ↔ (1st𝑋)𝐴(2nd𝑋)))
119, 10syl 17 . . . . 5 ((𝜑𝑋𝐴) → ((2nd𝑋) ∈ (𝐴 “ {(1st𝑋)}) ↔ (1st𝑋)𝐴(2nd𝑋)))
128, 11mpbird 260 . . . 4 ((𝜑𝑋𝐴) → (2nd𝑋) ∈ (𝐴 “ {(1st𝑋)}))
13 oveq2 7230 . . . . 5 (𝑗 = (2nd𝑋) → ((1st𝑋)𝑆𝑗) = ((1st𝑋)𝑆(2nd𝑋)))
14 eqid 2738 . . . . 5 (𝑗 ∈ (𝐴 “ {(1st𝑋)}) ↦ ((1st𝑋)𝑆𝑗)) = (𝑗 ∈ (𝐴 “ {(1st𝑋)}) ↦ ((1st𝑋)𝑆𝑗))
15 ovex 7255 . . . . 5 ((1st𝑋)𝑆𝑗) ∈ V
1613, 14, 15fvmpt3i 6832 . . . 4 ((2nd𝑋) ∈ (𝐴 “ {(1st𝑋)}) → ((𝑗 ∈ (𝐴 “ {(1st𝑋)}) ↦ ((1st𝑋)𝑆𝑗))‘(2nd𝑋)) = ((1st𝑋)𝑆(2nd𝑋)))
1712, 16syl 17 . . 3 ((𝜑𝑋𝐴) → ((𝑗 ∈ (𝐴 “ {(1st𝑋)}) ↦ ((1st𝑋)𝑆𝑗))‘(2nd𝑋)) = ((1st𝑋)𝑆(2nd𝑋)))
184fveq2d 6730 . . 3 ((𝜑𝑋𝐴) → (𝑆𝑋) = (𝑆‘⟨(1st𝑋), (2nd𝑋)⟩))
191, 17, 183eqtr4a 2805 . 2 ((𝜑𝑋𝐴) → ((𝑗 ∈ (𝐴 “ {(1st𝑋)}) ↦ ((1st𝑋)𝑆𝑗))‘(2nd𝑋)) = (𝑆𝑋))
20 sneq 4560 . . . . . . 7 (𝑖 = (1st𝑋) → {𝑖} = {(1st𝑋)})
2120imaeq2d 5938 . . . . . 6 (𝑖 = (1st𝑋) → (𝐴 “ {𝑖}) = (𝐴 “ {(1st𝑋)}))
22 oveq1 7229 . . . . . 6 (𝑖 = (1st𝑋) → (𝑖𝑆𝑗) = ((1st𝑋)𝑆𝑗))
2321, 22mpteq12dv 5149 . . . . 5 (𝑖 = (1st𝑋) → (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)) = (𝑗 ∈ (𝐴 “ {(1st𝑋)}) ↦ ((1st𝑋)𝑆𝑗)))
2423breq2d 5074 . . . 4 (𝑖 = (1st𝑋) → (𝐺dom DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)) ↔ 𝐺dom DProd (𝑗 ∈ (𝐴 “ {(1st𝑋)}) ↦ ((1st𝑋)𝑆𝑗))))
25 dprd2d.4 . . . . . 6 ((𝜑𝑖𝐼) → 𝐺dom DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))
2625ralrimiva 3106 . . . . 5 (𝜑 → ∀𝑖𝐼 𝐺dom DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))
2726adantr 484 . . . 4 ((𝜑𝑋𝐴) → ∀𝑖𝐼 𝐺dom DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))
28 dprd2d.3 . . . . . 6 (𝜑 → dom 𝐴𝐼)
2928adantr 484 . . . . 5 ((𝜑𝑋𝐴) → dom 𝐴𝐼)
30 1stdm 7820 . . . . . 6 ((Rel 𝐴𝑋𝐴) → (1st𝑋) ∈ dom 𝐴)
312, 30sylan 583 . . . . 5 ((𝜑𝑋𝐴) → (1st𝑋) ∈ dom 𝐴)
3229, 31sseldd 3911 . . . 4 ((𝜑𝑋𝐴) → (1st𝑋) ∈ 𝐼)
3324, 27, 32rspcdva 3546 . . 3 ((𝜑𝑋𝐴) → 𝐺dom DProd (𝑗 ∈ (𝐴 “ {(1st𝑋)}) ↦ ((1st𝑋)𝑆𝑗)))
3415, 14dmmpti 6531 . . . 4 dom (𝑗 ∈ (𝐴 “ {(1st𝑋)}) ↦ ((1st𝑋)𝑆𝑗)) = (𝐴 “ {(1st𝑋)})
3534a1i 11 . . 3 ((𝜑𝑋𝐴) → dom (𝑗 ∈ (𝐴 “ {(1st𝑋)}) ↦ ((1st𝑋)𝑆𝑗)) = (𝐴 “ {(1st𝑋)}))
3633, 35, 12dprdub 19425 . 2 ((𝜑𝑋𝐴) → ((𝑗 ∈ (𝐴 “ {(1st𝑋)}) ↦ ((1st𝑋)𝑆𝑗))‘(2nd𝑋)) ⊆ (𝐺 DProd (𝑗 ∈ (𝐴 “ {(1st𝑋)}) ↦ ((1st𝑋)𝑆𝑗))))
3719, 36eqsstrrd 3949 1 ((𝜑𝑋𝐴) → (𝑆𝑋) ⊆ (𝐺 DProd (𝑗 ∈ (𝐴 “ {(1st𝑋)}) ↦ ((1st𝑋)𝑆𝑗))))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 209  wa 399   = wceq 1543  wcel 2111  wral 3062  wss 3875  {csn 4550  cop 4556   class class class wbr 5062  cmpt 5144  dom cdm 5560  cima 5563  Rel wrel 5565  wf 6385  cfv 6389  (class class class)co 7222  1st c1st 7768  2nd c2nd 7769  mrClscmrc 17099  SubGrpcsubg 18550   DProd cdprd 19393
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2016  ax-8 2113  ax-9 2121  ax-10 2142  ax-11 2159  ax-12 2176  ax-ext 2709  ax-rep 5188  ax-sep 5201  ax-nul 5208  ax-pow 5267  ax-pr 5331  ax-un 7532  ax-cnex 10798  ax-resscn 10799  ax-1cn 10800  ax-icn 10801  ax-addcl 10802  ax-addrcl 10803  ax-mulcl 10804  ax-mulrcl 10805  ax-mulcom 10806  ax-addass 10807  ax-mulass 10808  ax-distr 10809  ax-i2m1 10810  ax-1ne0 10811  ax-1rid 10812  ax-rnegex 10813  ax-rrecex 10814  ax-cnre 10815  ax-pre-lttri 10816  ax-pre-lttrn 10817  ax-pre-ltadd 10818  ax-pre-mulgt0 10819
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 848  df-3or 1090  df-3an 1091  df-tru 1546  df-fal 1556  df-ex 1788  df-nf 1792  df-sb 2072  df-mo 2540  df-eu 2569  df-clab 2716  df-cleq 2730  df-clel 2817  df-nfc 2887  df-ne 2942  df-nel 3048  df-ral 3067  df-rex 3068  df-reu 3069  df-rmo 3070  df-rab 3071  df-v 3417  df-sbc 3704  df-csb 3821  df-dif 3878  df-un 3880  df-in 3882  df-ss 3892  df-pss 3894  df-nul 4247  df-if 4449  df-pw 4524  df-sn 4551  df-pr 4553  df-tp 4555  df-op 4557  df-uni 4829  df-int 4869  df-iun 4915  df-iin 4916  df-br 5063  df-opab 5125  df-mpt 5145  df-tr 5171  df-id 5464  df-eprel 5469  df-po 5477  df-so 5478  df-fr 5518  df-se 5519  df-we 5520  df-xp 5566  df-rel 5567  df-cnv 5568  df-co 5569  df-dm 5570  df-rn 5571  df-res 5572  df-ima 5573  df-pred 6169  df-ord 6225  df-on 6226  df-lim 6227  df-suc 6228  df-iota 6347  df-fun 6391  df-fn 6392  df-f 6393  df-f1 6394  df-fo 6395  df-f1o 6396  df-fv 6397  df-isom 6398  df-riota 7179  df-ov 7225  df-oprab 7226  df-mpo 7227  df-om 7654  df-1st 7770  df-2nd 7771  df-supp 7913  df-wrecs 8056  df-recs 8117  df-rdg 8155  df-1o 8211  df-er 8400  df-ixp 8588  df-en 8636  df-dom 8637  df-sdom 8638  df-fin 8639  df-fsupp 8999  df-oi 9139  df-card 9568  df-pnf 10882  df-mnf 10883  df-xr 10884  df-ltxr 10885  df-le 10886  df-sub 11077  df-neg 11078  df-nn 11844  df-2 11906  df-n0 12104  df-z 12190  df-uz 12452  df-fz 13109  df-fzo 13252  df-seq 13588  df-hash 13910  df-sets 16730  df-slot 16748  df-ndx 16758  df-base 16774  df-ress 16798  df-plusg 16828  df-0g 16959  df-gsum 16960  df-mre 17102  df-mrc 17103  df-acs 17105  df-mgm 18127  df-sgrp 18176  df-mnd 18187  df-submnd 18232  df-grp 18381  df-mulg 18502  df-subg 18553  df-cntz 18724  df-cmn 19185  df-dprd 19395
This theorem is referenced by:  dprd2dlem1  19441  dprd2da  19442
  Copyright terms: Public domain W3C validator