grplactfval - Metamath Proof Explorer

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

Theorem grplactfval 17638

Description: The left group action of element 𝐴 of group 𝐺. (Contributed by Paul Chapman, 18-Mar-2008.)

**Hypotheses**
Ref	Expression
grplact.1	⊢ 𝐹 = (𝑔 ∈ 𝑋 ↦ (𝑎 ∈ 𝑋 ↦ (𝑔 + 𝑎)))
grplact.2	⊢ 𝑋 = (Base‘𝐺)

**Assertion**
Ref	Expression
grplactfval	⊢ (𝐴 ∈ 𝑋 → (𝐹‘𝐴) = (𝑎 ∈ 𝑋 ↦ (𝐴 + 𝑎)))

Distinct variable groups: 𝑔,𝑎,𝐴 𝐺,𝑎,𝑔 + ,𝑎,𝑔 𝑋,𝑎,𝑔 Allowed substitution hints: 𝐹(𝑔,𝑎)

**Proof of Theorem grplactfval**
Step	Hyp	Ref	Expression
1		oveq1 6772	. . 3 ⊢ (𝑔 = 𝐴 → (𝑔 + 𝑎) = (𝐴 + 𝑎))
2	1	mpteq2dv 4853	. 2 ⊢ (𝑔 = 𝐴 → (𝑎 ∈ 𝑋 ↦ (𝑔 + 𝑎)) = (𝑎 ∈ 𝑋 ↦ (𝐴 + 𝑎)))
3		grplact.1	. 2 ⊢ 𝐹 = (𝑔 ∈ 𝑋 ↦ (𝑎 ∈ 𝑋 ↦ (𝑔 + 𝑎)))
4		grplact.2	. . . 4 ⊢ 𝑋 = (Base‘𝐺)
5		fvex 6314	. . . 4 ⊢ (Base‘𝐺) ∈ V
6	4, 5	eqeltri 2799	. . 3 ⊢ 𝑋 ∈ V
7	6	mptex 6602	. 2 ⊢ (𝑎 ∈ 𝑋 ↦ (𝐴 + 𝑎)) ∈ V
8	2, 3, 7	fvmpt 6396	1 ⊢ (𝐴 ∈ 𝑋 → (𝐹‘𝐴) = (𝑎 ∈ 𝑋 ↦ (𝐴 + 𝑎)))

Colors of variables: wff setvar class

Syntax hints: → wi 4 = wceq 1596 ∈ wcel 2103 Vcvv 3304 ↦ cmpt 4837 ‘cfv 6001 (class class class)co 6765 Basecbs 15980

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1835 ax-4 1850 ax-5 1952 ax-6 2018 ax-7 2054 ax-9 2112 ax-10 2132 ax-11 2147 ax-12 2160 ax-13 2355 ax-ext 2704 ax-rep 4879 ax-sep 4889 ax-nul 4897 ax-pr 5011

This theorem depends on definitions: df-bi 197 df-or 384 df-an 385 df-3an 1074 df-tru 1599 df-ex 1818 df-nf 1823 df-sb 2011 df-eu 2575 df-mo 2576 df-clab 2711 df-cleq 2717 df-clel 2720 df-nfc 2855 df-ne 2897 df-ral 3019 df-rex 3020 df-reu 3021 df-rab 3023 df-v 3306 df-sbc 3542 df-csb 3640 df-dif 3683 df-un 3685 df-in 3687 df-ss 3694 df-nul 4024 df-if 4195 df-sn 4286 df-pr 4288 df-op 4292 df-uni 4545 df-iun 4630 df-br 4761 df-opab 4821 df-mpt 4838 df-id 5128 df-xp 5224 df-rel 5225 df-cnv 5226 df-co 5227 df-dm 5228 df-rn 5229 df-res 5230 df-ima 5231 df-iota 5964 df-fun 6003 df-fn 6004 df-f 6005 df-f1 6006 df-fo 6007 df-f1o 6008 df-fv 6009 df-ov 6768

This theorem is referenced by: grplactval 17639 grplactcnv 17640 eqglact 17767 eqgen 17769 tgplacthmeo 22029 tgpconncompeqg 22037