dpjf - Metamath Proof Explorer

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

Theorem dpjf 20303

Description: The 𝑋-th index projection is a function from the direct product to the 𝑋-th factor. (Contributed by Mario Carneiro, 26-Apr-2016.)

**Hypotheses**
Ref	Expression
dpjfval.1	⊢ (𝜑 → 𝐺dom DProd 𝑆)
dpjfval.2	⊢ (𝜑 → dom 𝑆 = 𝐼)
dpjfval.p	⊢ 𝑃 = (𝐺dProj𝑆)
dpjf.3	⊢ (𝜑 → 𝑋 ∈ 𝐼)

**Assertion**
Ref	Expression
dpjf	⊢ (𝜑 → (𝑃‘𝑋):(𝐺 DProd 𝑆)⟶(𝑆‘𝑋))

**Proof of Theorem dpjf**
Step	Hyp	Ref	Expression
1		eqid 2763	. . 3 ⊢ (+_g‘𝐺) = (+_g‘𝐺)
2		eqid 2763	. . 3 ⊢ (LSSum‘𝐺) = (LSSum‘𝐺)
3		eqid 2763	. . 3 ⊢ (0_g‘𝐺) = (0_g‘𝐺)
4		eqid 2763	. . 3 ⊢ (Cntz‘𝐺) = (Cntz‘𝐺)
5		dpjfval.1	. . . . 5 ⊢ (𝜑 → 𝐺dom DProd 𝑆)
6		dpjfval.2	. . . . 5 ⊢ (𝜑 → dom 𝑆 = 𝐼)
7	5, 6	dprdf2 20253	. . . 4 ⊢ (𝜑 → 𝑆:𝐼⟶(SubGrp‘𝐺))
8		dpjf.3	. . . 4 ⊢ (𝜑 → 𝑋 ∈ 𝐼)
9	7, 8	ffvelcdmd 7109	. . 3 ⊢ (𝜑 → (𝑆‘𝑋) ∈ (SubGrp‘𝐺))
10		difssd 4076	. . . . . 6 ⊢ (𝜑 → (𝐼 ∖ {𝑋}) ⊆ 𝐼)
11	5, 6, 10	dprdres 20274	. . . . 5 ⊢ (𝜑 → (𝐺dom DProd (𝑆 ↾ (𝐼 ∖ {𝑋})) ∧ (𝐺 DProd (𝑆 ↾ (𝐼 ∖ {𝑋}))) ⊆ (𝐺 DProd 𝑆)))
12	11	simpld 500	. . . 4 ⊢ (𝜑 → 𝐺dom DProd (𝑆 ↾ (𝐼 ∖ {𝑋})))
13		dprdsubg 20270	. . . 4 ⊢ (𝐺dom DProd (𝑆 ↾ (𝐼 ∖ {𝑋})) → (𝐺 DProd (𝑆 ↾ (𝐼 ∖ {𝑋}))) ∈ (SubGrp‘𝐺))
14	12, 13	syl 18	. . 3 ⊢ (𝜑 → (𝐺 DProd (𝑆 ↾ (𝐼 ∖ {𝑋}))) ∈ (SubGrp‘𝐺))
15	5, 6, 8, 3	dpjdisj 20299	. . 3 ⊢ (𝜑 → ((𝑆‘𝑋) ∩ (𝐺 DProd (𝑆 ↾ (𝐼 ∖ {𝑋})))) = {(0_g‘𝐺)})
16	5, 6, 8, 4	dpjcntz 20298	. . 3 ⊢ (𝜑 → (𝑆‘𝑋) ⊆ ((Cntz‘𝐺)‘(𝐺 DProd (𝑆 ↾ (𝐼 ∖ {𝑋})))))
17		eqid 2763	. . 3 ⊢ (proj₁‘𝐺) = (proj₁‘𝐺)
18	1, 2, 3, 4, 9, 14, 15, 16, 17	pj1f 19941	. 2 ⊢ (𝜑 → ((𝑆‘𝑋)(proj₁‘𝐺)(𝐺 DProd (𝑆 ↾ (𝐼 ∖ {𝑋})))):((𝑆‘𝑋)(LSSum‘𝐺)(𝐺 DProd (𝑆 ↾ (𝐼 ∖ {𝑋}))))⟶(𝑆‘𝑋))
19		dpjfval.p	. . . 4 ⊢ 𝑃 = (𝐺dProj𝑆)
20	5, 6, 19, 17, 8	dpjval 20302	. . 3 ⊢ (𝜑 → (𝑃‘𝑋) = ((𝑆‘𝑋)(proj₁‘𝐺)(𝐺 DProd (𝑆 ↾ (𝐼 ∖ {𝑋})))))
21	5, 6, 8, 2	dpjlsm 20300	. . 3 ⊢ (𝜑 → (𝐺 DProd 𝑆) = ((𝑆‘𝑋)(LSSum‘𝐺)(𝐺 DProd (𝑆 ↾ (𝐼 ∖ {𝑋})))))
22	20, 21	feq12d 6719	. 2 ⊢ (𝜑 → ((𝑃‘𝑋):(𝐺 DProd 𝑆)⟶(𝑆‘𝑋) ↔ ((𝑆‘𝑋)(proj₁‘𝐺)(𝐺 DProd (𝑆 ↾ (𝐼 ∖ {𝑋})))):((𝑆‘𝑋)(LSSum‘𝐺)(𝐺 DProd (𝑆 ↾ (𝐼 ∖ {𝑋}))))⟶(𝑆‘𝑋)))
23	18, 22	mpbird 260	1 ⊢ (𝜑 → (𝑃‘𝑋):(𝐺 DProd 𝑆)⟶(𝑆‘𝑋))

Colors of variables: wff setvar class

This proof depends on syntax axioms: → wi 4 = wceq 1570 ∈ wcel 2147 ⊆ wss 3900 ∖ cdif 4048 {csn 4588 class class class wbr 5106 dom cdm 5655 ↾ cres 5657 ⟶wf 6554 ‘cfv 6558 (class class class)co 7443 +_gcplusg 17457 0_gc0g 17639 SubGrpcsubg 19359 Cntzccntz 19559 LSSumclsm 19878 proj₁cpj1 19879 DProd cdprd 20239 dProjcdpj 20240

This proof depends on axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1828 ax-4 1842 ax-5 1945 ax-6 2002 ax-7 2043 ax-8 2149 ax-9 2157 ax-10 2180 ax-11 2197 ax-12 2216 ax-ext 2735 ax-rep 5235 ax-sep 5252 ax-nul 5263 ax-pow 5331 ax-pr 5395 ax-un 7775 ax-cnex 11283 ax-resscn 11284 ax-1cn 11285 ax-icn 11286 ax-addcl 11287 ax-addrcl 11288 ax-mulcl 11289 ax-mulrcl 11290 ax-mulcom 11291 ax-addass 11292 ax-mulass 11293 ax-distr 11294 ax-i2m1 11295 ax-1ne0 11296 ax-1rid 11297 ax-rnegex 11298 ax-rrecex 11299 ax-cnre 11300 ax-pre-lttri 11301 ax-pre-lttrn 11302 ax-pre-ltadd 11303 ax-pre-mulgt0 11304

This proof depends on definitions: df-bi 210 df-an 402 df-or 862 df-3or 1104 df-3an 1105 df-tru 1573 df-fal 1583 df-ex 1813 df-nf 1817 df-sb 2102 df-mo 2567 df-eu 2597 df-clab 2742 df-cleq 2755 df-clel 2839 df-nfc 2913 df-ne 2960 df-nel 3066 df-ral 3081 df-rex 3091 df-rmo 3369 df-reu 3370 df-rab 3417 df-v 3456 df-sbc 3743 df-csb 3852 df-ss 3901 df-pss 4017 df-dif 4050 df-in 4094 df-un 4154 df-nul 4282 df-if 4486 df-pw 4562 df-sn 4589 df-pr 4591 df-op 4839 df-uni 4871 df-int 4911 df-iun 4956 df-iin 4957 df-br 5107 df-opab 5171 df-mpt 5190 df-tr 5216 df-id 5550 df-eprel 5555 df-po 5563 df-so 5564 df-fr 5608 df-se 5609 df-we 5610 df-xp 5661 df-rel 5662 df-cnv 5663 df-co 5664 df-dm 5665 df-rn 5666 df-res 5667 df-ima 5668 df-pred 6322 df-ord 6383 df-on 6384 df-lim 6385 df-suc 6386 df-iota 6512 df-fun 6560 df-fn 6561 df-f 6562 df-f1 6563 df-fo 6564 df-f1o 6565 df-fv 6566 df-isom 6567 df-riota 7400 df-ov 7446 df-oprab 7447 df-mpo 7448 df-of 7717 df-om 7902 df-1st 8025 df-2nd 8026 df-supp 8205 df-tpos 8271 df-frecs 8327 df-wrecs 8358 df-recs 8407 df-rdg 8446 df-1o 8504 df-2o 8505 df-er 8745 df-map 8877 df-ixp 8954 df-en 9002 df-dom 9003 df-sdom 9004 df-fin 9005 df-fsupp 9382 df-oi 9531 df-card 10047 df-pnf 11372 df-mnf 11373 df-xr 11374 df-ltxr 11375 df-le 11376 df-sub 11570 df-neg 11571 df-nn 12363 df-2 12432 df-n0 12634 df-z 12721 df-uz 12993 df-fz 13667 df-fzo 13816 df-seq 14172 df-hash 14502 df-sets 17371 df-slot 17389 df-ndx 17401 df-base 17417 df-ress 17438 df-plusg 17470 df-0g 17641 df-gsum 17642 df-mre 17785 df-mrc 17786 df-acs 17788 df-mgm 18845 df-sgrp 18937 df-mnd 18953 df-mhm 19007 df-submnd 19008 df-grp 19176 df-minusg 19177 df-sbg 19178 df-mulg 19307 df-subg 19362 df-ghm 19457 df-gim 19502 df-cntz 19561 df-oppg 19590 df-lsm 19880 df-pj1 19881 df-cmn 20026 df-dprd 20241 df-dpj 20242

This theorem is used by: dpjidcl 20304 dpjghm2 20310 dchrptlem2 27622

W3C validator