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

Theorem dprdfcntz 18338
Description: A function on the elements of an internal direct product has pairwise commuting values. (Contributed by Mario Carneiro, 25-Apr-2016.) (Revised by AV, 11-Jul-2019.)
Hypotheses
Ref Expression
dprdff.w 𝑊 = {X𝑖𝐼 (𝑆𝑖) ∣ finSupp 0 }
dprdff.1 (𝜑𝐺dom DProd 𝑆)
dprdff.2 (𝜑 → dom 𝑆 = 𝐼)
dprdff.3 (𝜑𝐹𝑊)
dprdfcntz.z 𝑍 = (Cntz‘𝐺)
Assertion
Ref Expression
dprdfcntz (𝜑 → ran 𝐹 ⊆ (𝑍‘ran 𝐹))
Distinct variable groups:   ,𝐹   ,𝑖,𝐼   0 ,   𝑆,,𝑖
Allowed substitution hints:   𝜑(,𝑖)   𝐹(𝑖)   𝐺(,𝑖)   𝑊(,𝑖)   0 (𝑖)   𝑍(,𝑖)

Proof of Theorem dprdfcntz
Dummy variables 𝑦 𝑧 𝑥 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 dprdff.w . . . . 5 𝑊 = {X𝑖𝐼 (𝑆𝑖) ∣ finSupp 0 }
2 dprdff.1 . . . . 5 (𝜑𝐺dom DProd 𝑆)
3 dprdff.2 . . . . 5 (𝜑 → dom 𝑆 = 𝐼)
4 dprdff.3 . . . . 5 (𝜑𝐹𝑊)
5 eqid 2621 . . . . 5 (Base‘𝐺) = (Base‘𝐺)
61, 2, 3, 4, 5dprdff 18335 . . . 4 (𝜑𝐹:𝐼⟶(Base‘𝐺))
7 ffn 6004 . . . 4 (𝐹:𝐼⟶(Base‘𝐺) → 𝐹 Fn 𝐼)
86, 7syl 17 . . 3 (𝜑𝐹 Fn 𝐼)
96ffvelrnda 6317 . . . . 5 ((𝜑𝑦𝐼) → (𝐹𝑦) ∈ (Base‘𝐺))
10 simpr 477 . . . . . . . . . 10 ((((𝜑𝑦𝐼) ∧ 𝑧𝐼) ∧ 𝑦 = 𝑧) → 𝑦 = 𝑧)
1110fveq2d 6154 . . . . . . . . 9 ((((𝜑𝑦𝐼) ∧ 𝑧𝐼) ∧ 𝑦 = 𝑧) → (𝐹𝑦) = (𝐹𝑧))
1210eqcomd 2627 . . . . . . . . . 10 ((((𝜑𝑦𝐼) ∧ 𝑧𝐼) ∧ 𝑦 = 𝑧) → 𝑧 = 𝑦)
1312fveq2d 6154 . . . . . . . . 9 ((((𝜑𝑦𝐼) ∧ 𝑧𝐼) ∧ 𝑦 = 𝑧) → (𝐹𝑧) = (𝐹𝑦))
1411, 13oveq12d 6625 . . . . . . . 8 ((((𝜑𝑦𝐼) ∧ 𝑧𝐼) ∧ 𝑦 = 𝑧) → ((𝐹𝑦)(+g𝐺)(𝐹𝑧)) = ((𝐹𝑧)(+g𝐺)(𝐹𝑦)))
152ad3antrrr 765 . . . . . . . . . . 11 ((((𝜑𝑦𝐼) ∧ 𝑧𝐼) ∧ 𝑦𝑧) → 𝐺dom DProd 𝑆)
163ad3antrrr 765 . . . . . . . . . . 11 ((((𝜑𝑦𝐼) ∧ 𝑧𝐼) ∧ 𝑦𝑧) → dom 𝑆 = 𝐼)
17 simpllr 798 . . . . . . . . . . 11 ((((𝜑𝑦𝐼) ∧ 𝑧𝐼) ∧ 𝑦𝑧) → 𝑦𝐼)
18 simplr 791 . . . . . . . . . . 11 ((((𝜑𝑦𝐼) ∧ 𝑧𝐼) ∧ 𝑦𝑧) → 𝑧𝐼)
19 simpr 477 . . . . . . . . . . 11 ((((𝜑𝑦𝐼) ∧ 𝑧𝐼) ∧ 𝑦𝑧) → 𝑦𝑧)
20 dprdfcntz.z . . . . . . . . . . 11 𝑍 = (Cntz‘𝐺)
2115, 16, 17, 18, 19, 20dprdcntz 18331 . . . . . . . . . 10 ((((𝜑𝑦𝐼) ∧ 𝑧𝐼) ∧ 𝑦𝑧) → (𝑆𝑦) ⊆ (𝑍‘(𝑆𝑧)))
221, 2, 3, 4dprdfcl 18336 . . . . . . . . . . 11 ((𝜑𝑦𝐼) → (𝐹𝑦) ∈ (𝑆𝑦))
2322ad2antrr 761 . . . . . . . . . 10 ((((𝜑𝑦𝐼) ∧ 𝑧𝐼) ∧ 𝑦𝑧) → (𝐹𝑦) ∈ (𝑆𝑦))
2421, 23sseldd 3585 . . . . . . . . 9 ((((𝜑𝑦𝐼) ∧ 𝑧𝐼) ∧ 𝑦𝑧) → (𝐹𝑦) ∈ (𝑍‘(𝑆𝑧)))
251, 2, 3, 4dprdfcl 18336 . . . . . . . . . . 11 ((𝜑𝑧𝐼) → (𝐹𝑧) ∈ (𝑆𝑧))
2625adantlr 750 . . . . . . . . . 10 (((𝜑𝑦𝐼) ∧ 𝑧𝐼) → (𝐹𝑧) ∈ (𝑆𝑧))
2726adantr 481 . . . . . . . . 9 ((((𝜑𝑦𝐼) ∧ 𝑧𝐼) ∧ 𝑦𝑧) → (𝐹𝑧) ∈ (𝑆𝑧))
28 eqid 2621 . . . . . . . . . 10 (+g𝐺) = (+g𝐺)
2928, 20cntzi 17686 . . . . . . . . 9 (((𝐹𝑦) ∈ (𝑍‘(𝑆𝑧)) ∧ (𝐹𝑧) ∈ (𝑆𝑧)) → ((𝐹𝑦)(+g𝐺)(𝐹𝑧)) = ((𝐹𝑧)(+g𝐺)(𝐹𝑦)))
3024, 27, 29syl2anc 692 . . . . . . . 8 ((((𝜑𝑦𝐼) ∧ 𝑧𝐼) ∧ 𝑦𝑧) → ((𝐹𝑦)(+g𝐺)(𝐹𝑧)) = ((𝐹𝑧)(+g𝐺)(𝐹𝑦)))
3114, 30pm2.61dane 2877 . . . . . . 7 (((𝜑𝑦𝐼) ∧ 𝑧𝐼) → ((𝐹𝑦)(+g𝐺)(𝐹𝑧)) = ((𝐹𝑧)(+g𝐺)(𝐹𝑦)))
3231ralrimiva 2960 . . . . . 6 ((𝜑𝑦𝐼) → ∀𝑧𝐼 ((𝐹𝑦)(+g𝐺)(𝐹𝑧)) = ((𝐹𝑧)(+g𝐺)(𝐹𝑦)))
338adantr 481 . . . . . . 7 ((𝜑𝑦𝐼) → 𝐹 Fn 𝐼)
34 oveq2 6615 . . . . . . . . 9 (𝑥 = (𝐹𝑧) → ((𝐹𝑦)(+g𝐺)𝑥) = ((𝐹𝑦)(+g𝐺)(𝐹𝑧)))
35 oveq1 6614 . . . . . . . . 9 (𝑥 = (𝐹𝑧) → (𝑥(+g𝐺)(𝐹𝑦)) = ((𝐹𝑧)(+g𝐺)(𝐹𝑦)))
3634, 35eqeq12d 2636 . . . . . . . 8 (𝑥 = (𝐹𝑧) → (((𝐹𝑦)(+g𝐺)𝑥) = (𝑥(+g𝐺)(𝐹𝑦)) ↔ ((𝐹𝑦)(+g𝐺)(𝐹𝑧)) = ((𝐹𝑧)(+g𝐺)(𝐹𝑦))))
3736ralrn 6320 . . . . . . 7 (𝐹 Fn 𝐼 → (∀𝑥 ∈ ran 𝐹((𝐹𝑦)(+g𝐺)𝑥) = (𝑥(+g𝐺)(𝐹𝑦)) ↔ ∀𝑧𝐼 ((𝐹𝑦)(+g𝐺)(𝐹𝑧)) = ((𝐹𝑧)(+g𝐺)(𝐹𝑦))))
3833, 37syl 17 . . . . . 6 ((𝜑𝑦𝐼) → (∀𝑥 ∈ ran 𝐹((𝐹𝑦)(+g𝐺)𝑥) = (𝑥(+g𝐺)(𝐹𝑦)) ↔ ∀𝑧𝐼 ((𝐹𝑦)(+g𝐺)(𝐹𝑧)) = ((𝐹𝑧)(+g𝐺)(𝐹𝑦))))
3932, 38mpbird 247 . . . . 5 ((𝜑𝑦𝐼) → ∀𝑥 ∈ ran 𝐹((𝐹𝑦)(+g𝐺)𝑥) = (𝑥(+g𝐺)(𝐹𝑦)))
40 frn 6012 . . . . . . . 8 (𝐹:𝐼⟶(Base‘𝐺) → ran 𝐹 ⊆ (Base‘𝐺))
416, 40syl 17 . . . . . . 7 (𝜑 → ran 𝐹 ⊆ (Base‘𝐺))
4241adantr 481 . . . . . 6 ((𝜑𝑦𝐼) → ran 𝐹 ⊆ (Base‘𝐺))
435, 28, 20elcntz 17679 . . . . . 6 (ran 𝐹 ⊆ (Base‘𝐺) → ((𝐹𝑦) ∈ (𝑍‘ran 𝐹) ↔ ((𝐹𝑦) ∈ (Base‘𝐺) ∧ ∀𝑥 ∈ ran 𝐹((𝐹𝑦)(+g𝐺)𝑥) = (𝑥(+g𝐺)(𝐹𝑦)))))
4442, 43syl 17 . . . . 5 ((𝜑𝑦𝐼) → ((𝐹𝑦) ∈ (𝑍‘ran 𝐹) ↔ ((𝐹𝑦) ∈ (Base‘𝐺) ∧ ∀𝑥 ∈ ran 𝐹((𝐹𝑦)(+g𝐺)𝑥) = (𝑥(+g𝐺)(𝐹𝑦)))))
459, 39, 44mpbir2and 956 . . . 4 ((𝜑𝑦𝐼) → (𝐹𝑦) ∈ (𝑍‘ran 𝐹))
4645ralrimiva 2960 . . 3 (𝜑 → ∀𝑦𝐼 (𝐹𝑦) ∈ (𝑍‘ran 𝐹))
47 ffnfv 6346 . . 3 (𝐹:𝐼⟶(𝑍‘ran 𝐹) ↔ (𝐹 Fn 𝐼 ∧ ∀𝑦𝐼 (𝐹𝑦) ∈ (𝑍‘ran 𝐹)))
488, 46, 47sylanbrc 697 . 2 (𝜑𝐹:𝐼⟶(𝑍‘ran 𝐹))
49 frn 6012 . 2 (𝐹:𝐼⟶(𝑍‘ran 𝐹) → ran 𝐹 ⊆ (𝑍‘ran 𝐹))
5048, 49syl 17 1 (𝜑 → ran 𝐹 ⊆ (𝑍‘ran 𝐹))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196  wa 384   = wceq 1480  wcel 1987  wne 2790  wral 2907  {crab 2911  wss 3556   class class class wbr 4615  dom cdm 5076  ran crn 5077   Fn wfn 5844  wf 5845  cfv 5849  (class class class)co 6607  Xcixp 7855   finSupp cfsupp 8222  Basecbs 15784  +gcplusg 15865  Cntzccntz 17672   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
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  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-rab 2916  df-v 3188  df-sbc 3419  df-csb 3516  df-dif 3559  df-un 3561  df-in 3563  df-ss 3570  df-nul 3894  df-if 4061  df-pw 4134  df-sn 4151  df-pr 4153  df-op 4157  df-uni 4405  df-iun 4489  df-br 4616  df-opab 4676  df-mpt 4677  df-id 4991  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-iota 5812  df-fun 5851  df-fn 5852  df-f 5853  df-f1 5854  df-fo 5855  df-f1o 5856  df-fv 5857  df-ov 6610  df-oprab 6611  df-mpt2 6612  df-1st 7116  df-2nd 7117  df-ixp 7856  df-subg 17515  df-cntz 17674  df-dprd 18318
This theorem is referenced by:  dprdssv  18339  dprdfinv  18342  dprdfadd  18343  dprdfeq0  18345  dprdlub  18349  dmdprdsplitlem  18360  dpjidcl  18381
  Copyright terms: Public domain W3C validator