qusvscpbl - Mathbox for Thierry Arnoux

	Mathbox for Thierry Arnoux		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > Mathboxes > qusvscpbl		Structured version Visualization version GIF version

Theorem qusvscpbl 33371

Description: The quotient map distributes over the scalar multiplication. (Contributed by Thierry Arnoux, 18-May-2023.)

**Hypotheses**
Ref	Expression
eqgvscpbl.v	⊢ 𝐵 = (Base‘𝑀)
eqgvscpbl.e	⊢ ∼ = (𝑀 ~_QG 𝐺)
eqgvscpbl.s	⊢ 𝑆 = (Base‘(Scalar‘𝑀))
eqgvscpbl.p	⊢ · = ( ·_𝑠 ‘𝑀)
eqgvscpbl.m	⊢ (𝜑 → 𝑀 ∈ LMod)
eqgvscpbl.g	⊢ (𝜑 → 𝐺 ∈ (LSubSp‘𝑀))
eqgvscpbl.k	⊢ (𝜑 → 𝐾 ∈ 𝑆)
qusvsval.n	⊢ 𝑁 = (𝑀 /_s (𝑀 ~_QG 𝐺))
qusvsval.m	⊢ ∙ = ( ·_𝑠 ‘𝑁)
qusvscpbl.f	⊢ 𝐹 = (𝑥 ∈ 𝐵 ↦ [𝑥](𝑀 ~_QG 𝐺))
qusvscpbl.u	⊢ (𝜑 → 𝑈 ∈ 𝐵)
qusvscpbl.v	⊢ (𝜑 → 𝑉 ∈ 𝐵)

**Assertion**
Ref	Expression
qusvscpbl	⊢ (𝜑 → ((𝐹‘𝑈) = (𝐹‘𝑉) → (𝐹‘(𝐾 · 𝑈)) = (𝐹‘(𝐾 · 𝑉))))

Distinct variable groups: 𝑥,𝐵 𝑥,𝐺 𝑥,𝐾 𝑥,𝑀 𝑥,𝑈 𝑥,𝑉 𝜑,𝑥 𝑥, · Allowed substitution hints: ∼ (𝑥) 𝑆(𝑥) ∙ (𝑥) 𝐹(𝑥) 𝑁(𝑥)

**Proof of Theorem qusvscpbl**
Step	Hyp	Ref	Expression
1		eqgvscpbl.v	. . . 4 ⊢ 𝐵 = (Base‘𝑀)
2		eqid 2736	. . . 4 ⊢ (𝑀 ~_QG 𝐺) = (𝑀 ~_QG 𝐺)
3		eqgvscpbl.s	. . . 4 ⊢ 𝑆 = (Base‘(Scalar‘𝑀))
4		eqgvscpbl.p	. . . 4 ⊢ · = ( ·_𝑠 ‘𝑀)
5		eqgvscpbl.m	. . . 4 ⊢ (𝜑 → 𝑀 ∈ LMod)
6		eqgvscpbl.g	. . . 4 ⊢ (𝜑 → 𝐺 ∈ (LSubSp‘𝑀))
7		eqgvscpbl.k	. . . 4 ⊢ (𝜑 → 𝐾 ∈ 𝑆)
8	1, 2, 3, 4, 5, 6, 7	eqgvscpbl 33370	. . 3 ⊢ (𝜑 → (𝑈(𝑀 ~_QG 𝐺)𝑉 → (𝐾 · 𝑈)(𝑀 ~_QG 𝐺)(𝐾 · 𝑉)))
9		eqid 2736	. . . . . . 7 ⊢ (LSubSp‘𝑀) = (LSubSp‘𝑀)
10	9	lsssubg 20919	. . . . . 6 ⊢ ((𝑀 ∈ LMod ∧ 𝐺 ∈ (LSubSp‘𝑀)) → 𝐺 ∈ (SubGrp‘𝑀))
11	5, 6, 10	syl2anc 584	. . . . 5 ⊢ (𝜑 → 𝐺 ∈ (SubGrp‘𝑀))
12	1, 2	eqger 19166	. . . . 5 ⊢ (𝐺 ∈ (SubGrp‘𝑀) → (𝑀 ~_QG 𝐺) Er 𝐵)
13	11, 12	syl 17	. . . 4 ⊢ (𝜑 → (𝑀 ~_QG 𝐺) Er 𝐵)
14		qusvscpbl.u	. . . 4 ⊢ (𝜑 → 𝑈 ∈ 𝐵)
15	13, 14	erth 8775	. . 3 ⊢ (𝜑 → (𝑈(𝑀 ~_QG 𝐺)𝑉 ↔ [𝑈](𝑀 ~_QG 𝐺) = [𝑉](𝑀 ~_QG 𝐺)))
16		eqid 2736	. . . . . 6 ⊢ (Scalar‘𝑀) = (Scalar‘𝑀)
17	1, 16, 4, 3	lmodvscl 20840	. . . . 5 ⊢ ((𝑀 ∈ LMod ∧ 𝐾 ∈ 𝑆 ∧ 𝑈 ∈ 𝐵) → (𝐾 · 𝑈) ∈ 𝐵)
18	5, 7, 14, 17	syl3anc 1373	. . . 4 ⊢ (𝜑 → (𝐾 · 𝑈) ∈ 𝐵)
19	13, 18	erth 8775	. . 3 ⊢ (𝜑 → ((𝐾 · 𝑈)(𝑀 ~_QG 𝐺)(𝐾 · 𝑉) ↔ [(𝐾 · 𝑈)](𝑀 ~_QG 𝐺) = [(𝐾 · 𝑉)](𝑀 ~_QG 𝐺)))
20	8, 15, 19	3imtr3d 293	. 2 ⊢ (𝜑 → ([𝑈](𝑀 ~_QG 𝐺) = [𝑉](𝑀 ~_QG 𝐺) → [(𝐾 · 𝑈)](𝑀 ~_QG 𝐺) = [(𝐾 · 𝑉)](𝑀 ~_QG 𝐺)))
21		eceq1 8763	. . . . 5 ⊢ (𝑥 = 𝑈 → [𝑥](𝑀 ~_QG 𝐺) = [𝑈](𝑀 ~_QG 𝐺))
22		qusvscpbl.f	. . . . 5 ⊢ 𝐹 = (𝑥 ∈ 𝐵 ↦ [𝑥](𝑀 ~_QG 𝐺))
23		ovex 7443	. . . . . 6 ⊢ (𝑀 ~_QG 𝐺) ∈ V
24		ecexg 8728	. . . . . 6 ⊢ ((𝑀 ~_QG 𝐺) ∈ V → [𝑈](𝑀 ~_QG 𝐺) ∈ V)
25	23, 24	ax-mp 5	. . . . 5 ⊢ [𝑈](𝑀 ~_QG 𝐺) ∈ V
26	21, 22, 25	fvmpt 6991	. . . 4 ⊢ (𝑈 ∈ 𝐵 → (𝐹‘𝑈) = [𝑈](𝑀 ~_QG 𝐺))
27	14, 26	syl 17	. . 3 ⊢ (𝜑 → (𝐹‘𝑈) = [𝑈](𝑀 ~_QG 𝐺))
28		qusvscpbl.v	. . . 4 ⊢ (𝜑 → 𝑉 ∈ 𝐵)
29		eceq1 8763	. . . . 5 ⊢ (𝑥 = 𝑉 → [𝑥](𝑀 ~_QG 𝐺) = [𝑉](𝑀 ~_QG 𝐺))
30		ecexg 8728	. . . . . 6 ⊢ ((𝑀 ~_QG 𝐺) ∈ V → [𝑉](𝑀 ~_QG 𝐺) ∈ V)
31	23, 30	ax-mp 5	. . . . 5 ⊢ [𝑉](𝑀 ~_QG 𝐺) ∈ V
32	29, 22, 31	fvmpt 6991	. . . 4 ⊢ (𝑉 ∈ 𝐵 → (𝐹‘𝑉) = [𝑉](𝑀 ~_QG 𝐺))
33	28, 32	syl 17	. . 3 ⊢ (𝜑 → (𝐹‘𝑉) = [𝑉](𝑀 ~_QG 𝐺))
34	27, 33	eqeq12d 2752	. 2 ⊢ (𝜑 → ((𝐹‘𝑈) = (𝐹‘𝑉) ↔ [𝑈](𝑀 ~_QG 𝐺) = [𝑉](𝑀 ~_QG 𝐺)))
35		eceq1 8763	. . . . 5 ⊢ (𝑥 = (𝐾 · 𝑈) → [𝑥](𝑀 ~_QG 𝐺) = [(𝐾 · 𝑈)](𝑀 ~_QG 𝐺))
36		ecexg 8728	. . . . . 6 ⊢ ((𝑀 ~_QG 𝐺) ∈ V → [(𝐾 · 𝑈)](𝑀 ~_QG 𝐺) ∈ V)
37	23, 36	ax-mp 5	. . . . 5 ⊢ [(𝐾 · 𝑈)](𝑀 ~_QG 𝐺) ∈ V
38	35, 22, 37	fvmpt 6991	. . . 4 ⊢ ((𝐾 · 𝑈) ∈ 𝐵 → (𝐹‘(𝐾 · 𝑈)) = [(𝐾 · 𝑈)](𝑀 ~_QG 𝐺))
39	18, 38	syl 17	. . 3 ⊢ (𝜑 → (𝐹‘(𝐾 · 𝑈)) = [(𝐾 · 𝑈)](𝑀 ~_QG 𝐺))
40	1, 16, 4, 3	lmodvscl 20840	. . . . 5 ⊢ ((𝑀 ∈ LMod ∧ 𝐾 ∈ 𝑆 ∧ 𝑉 ∈ 𝐵) → (𝐾 · 𝑉) ∈ 𝐵)
41	5, 7, 28, 40	syl3anc 1373	. . . 4 ⊢ (𝜑 → (𝐾 · 𝑉) ∈ 𝐵)
42		eceq1 8763	. . . . 5 ⊢ (𝑥 = (𝐾 · 𝑉) → [𝑥](𝑀 ~_QG 𝐺) = [(𝐾 · 𝑉)](𝑀 ~_QG 𝐺))
43		ecexg 8728	. . . . . 6 ⊢ ((𝑀 ~_QG 𝐺) ∈ V → [(𝐾 · 𝑉)](𝑀 ~_QG 𝐺) ∈ V)
44	23, 43	ax-mp 5	. . . . 5 ⊢ [(𝐾 · 𝑉)](𝑀 ~_QG 𝐺) ∈ V
45	42, 22, 44	fvmpt 6991	. . . 4 ⊢ ((𝐾 · 𝑉) ∈ 𝐵 → (𝐹‘(𝐾 · 𝑉)) = [(𝐾 · 𝑉)](𝑀 ~_QG 𝐺))
46	41, 45	syl 17	. . 3 ⊢ (𝜑 → (𝐹‘(𝐾 · 𝑉)) = [(𝐾 · 𝑉)](𝑀 ~_QG 𝐺))
47	39, 46	eqeq12d 2752	. 2 ⊢ (𝜑 → ((𝐹‘(𝐾 · 𝑈)) = (𝐹‘(𝐾 · 𝑉)) ↔ [(𝐾 · 𝑈)](𝑀 ~_QG 𝐺) = [(𝐾 · 𝑉)](𝑀 ~_QG 𝐺)))
48	20, 34, 47	3imtr4d 294	1 ⊢ (𝜑 → ((𝐹‘𝑈) = (𝐹‘𝑉) → (𝐹‘(𝐾 · 𝑈)) = (𝐹‘(𝐾 · 𝑉))))

Colors of variables: wff setvar class

Syntax hints: → wi 4 = wceq 1540 ∈ wcel 2109 Vcvv 3464 class class class wbr 5124 ↦ cmpt 5206 ‘cfv 6536 (class class class)co 7410 Er wer 8721 [cec 8722 Basecbs 17233 Scalarcsca 17279 ·_𝑠 cvsca 17280 /_s cqus 17524 SubGrpcsubg 19108 ~_QG cqg 19110 LModclmod 20822 LSubSpclss 20893

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1910 ax-6 1967 ax-7 2008 ax-8 2111 ax-9 2119 ax-10 2142 ax-11 2158 ax-12 2178 ax-ext 2708 ax-sep 5271 ax-nul 5281 ax-pow 5340 ax-pr 5407 ax-un 7734 ax-cnex 11190 ax-resscn 11191 ax-1cn 11192 ax-icn 11193 ax-addcl 11194 ax-addrcl 11195 ax-mulcl 11196 ax-mulrcl 11197 ax-mulcom 11198 ax-addass 11199 ax-mulass 11200 ax-distr 11201 ax-i2m1 11202 ax-1ne0 11203 ax-1rid 11204 ax-rnegex 11205 ax-rrecex 11206 ax-cnre 11207 ax-pre-lttri 11208 ax-pre-lttrn 11209 ax-pre-ltadd 11210 ax-pre-mulgt0 11211

This theorem depends on definitions: df-bi 207 df-an 396 df-or 848 df-3or 1087 df-3an 1088 df-tru 1543 df-fal 1553 df-ex 1780 df-nf 1784 df-sb 2066 df-mo 2540 df-eu 2569 df-clab 2715 df-cleq 2728 df-clel 2810 df-nfc 2886 df-ne 2934 df-nel 3038 df-ral 3053 df-rex 3062 df-rmo 3364 df-reu 3365 df-rab 3421 df-v 3466 df-sbc 3771 df-csb 3880 df-dif 3934 df-un 3936 df-in 3938 df-ss 3948 df-pss 3951 df-nul 4314 df-if 4506 df-pw 4582 df-sn 4607 df-pr 4609 df-op 4613 df-uni 4889 df-iun 4974 df-br 5125 df-opab 5187 df-mpt 5207 df-tr 5235 df-id 5553 df-eprel 5558 df-po 5566 df-so 5567 df-fr 5611 df-we 5613 df-xp 5665 df-rel 5666 df-cnv 5667 df-co 5668 df-dm 5669 df-rn 5670 df-res 5671 df-ima 5672 df-pred 6295 df-ord 6360 df-on 6361 df-lim 6362 df-suc 6363 df-iota 6489 df-fun 6538 df-fn 6539 df-f 6540 df-f1 6541 df-fo 6542 df-f1o 6543 df-fv 6544 df-riota 7367 df-ov 7413 df-oprab 7414 df-mpo 7415 df-om 7867 df-1st 7993 df-2nd 7994 df-frecs 8285 df-wrecs 8316 df-recs 8390 df-rdg 8429 df-er 8724 df-ec 8726 df-en 8965 df-dom 8966 df-sdom 8967 df-pnf 11276 df-mnf 11277 df-xr 11278 df-ltxr 11279 df-le 11280 df-sub 11473 df-neg 11474 df-nn 12246 df-2 12308 df-sets 17188 df-slot 17206 df-ndx 17218 df-base 17234 df-ress 17257 df-plusg 17289 df-0g 17460 df-mgm 18623 df-sgrp 18702 df-mnd 18718 df-grp 18924 df-minusg 18925 df-sbg 18926 df-subg 19111 df-eqg 19113 df-cmn 19768 df-abl 19769 df-mgp 20106 df-rng 20118 df-ur 20147 df-ring 20200 df-lmod 20824 df-lss 20894

This theorem is referenced by: qusvsval 33372 quslmod 33378 quslmhm 33379

W3C validator