nmdvr - Metamath Proof Explorer

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

Theorem nmdvr 23362

Description: The norm of a division in a nonzero normed ring. (Contributed by Mario Carneiro, 5-Oct-2015.)

**Hypotheses**
Ref	Expression
nmdvr.x	⊢ 𝑋 = (Base‘𝑅)
nmdvr.n	⊢ 𝑁 = (norm‘𝑅)
nmdvr.u	⊢ 𝑈 = (Unit‘𝑅)
nmdvr.d	⊢ / = (/_r‘𝑅)

**Assertion**
Ref	Expression
nmdvr	⊢ (((𝑅 ∈ NrmRing ∧ 𝑅 ∈ NzRing) ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑈)) → (𝑁‘(𝐴 / 𝐵)) = ((𝑁‘𝐴) / (𝑁‘𝐵)))

**Proof of Theorem nmdvr**
Step	Hyp	Ref	Expression
1		simpll 767	. . . 4 ⊢ (((𝑅 ∈ NrmRing ∧ 𝑅 ∈ NzRing) ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑈)) → 𝑅 ∈ NrmRing)
2		simprl 771	. . . 4 ⊢ (((𝑅 ∈ NrmRing ∧ 𝑅 ∈ NzRing) ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑈)) → 𝐴 ∈ 𝑋)
3		nrgring 23355	. . . . . 6 ⊢ (𝑅 ∈ NrmRing → 𝑅 ∈ Ring)
4	3	ad2antrr 726	. . . . 5 ⊢ (((𝑅 ∈ NrmRing ∧ 𝑅 ∈ NzRing) ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑈)) → 𝑅 ∈ Ring)
5		simprr 773	. . . . 5 ⊢ (((𝑅 ∈ NrmRing ∧ 𝑅 ∈ NzRing) ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑈)) → 𝐵 ∈ 𝑈)
6		nmdvr.u	. . . . . 6 ⊢ 𝑈 = (Unit‘𝑅)
7		eqid 2759	. . . . . 6 ⊢ (inv_r‘𝑅) = (inv_r‘𝑅)
8		nmdvr.x	. . . . . 6 ⊢ 𝑋 = (Base‘𝑅)
9	6, 7, 8	ringinvcl 19487	. . . . 5 ⊢ ((𝑅 ∈ Ring ∧ 𝐵 ∈ 𝑈) → ((inv_r‘𝑅)‘𝐵) ∈ 𝑋)
10	4, 5, 9	syl2anc 588	. . . 4 ⊢ (((𝑅 ∈ NrmRing ∧ 𝑅 ∈ NzRing) ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑈)) → ((inv_r‘𝑅)‘𝐵) ∈ 𝑋)
11		nmdvr.n	. . . . 5 ⊢ 𝑁 = (norm‘𝑅)
12		eqid 2759	. . . . 5 ⊢ (._r‘𝑅) = (._r‘𝑅)
13	8, 11, 12	nmmul 23356	. . . 4 ⊢ ((𝑅 ∈ NrmRing ∧ 𝐴 ∈ 𝑋 ∧ ((inv_r‘𝑅)‘𝐵) ∈ 𝑋) → (𝑁‘(𝐴(._r‘𝑅)((inv_r‘𝑅)‘𝐵))) = ((𝑁‘𝐴) · (𝑁‘((inv_r‘𝑅)‘𝐵))))
14	1, 2, 10, 13	syl3anc 1369	. . 3 ⊢ (((𝑅 ∈ NrmRing ∧ 𝑅 ∈ NzRing) ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑈)) → (𝑁‘(𝐴(._r‘𝑅)((inv_r‘𝑅)‘𝐵))) = ((𝑁‘𝐴) · (𝑁‘((inv_r‘𝑅)‘𝐵))))
15		simplr 769	. . . . 5 ⊢ (((𝑅 ∈ NrmRing ∧ 𝑅 ∈ NzRing) ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑈)) → 𝑅 ∈ NzRing)
16	11, 6, 7	nminvr 23361	. . . . 5 ⊢ ((𝑅 ∈ NrmRing ∧ 𝑅 ∈ NzRing ∧ 𝐵 ∈ 𝑈) → (𝑁‘((inv_r‘𝑅)‘𝐵)) = (1 / (𝑁‘𝐵)))
17	1, 15, 5, 16	syl3anc 1369	. . . 4 ⊢ (((𝑅 ∈ NrmRing ∧ 𝑅 ∈ NzRing) ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑈)) → (𝑁‘((inv_r‘𝑅)‘𝐵)) = (1 / (𝑁‘𝐵)))
18	17	oveq2d 7164	. . 3 ⊢ (((𝑅 ∈ NrmRing ∧ 𝑅 ∈ NzRing) ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑈)) → ((𝑁‘𝐴) · (𝑁‘((inv_r‘𝑅)‘𝐵))) = ((𝑁‘𝐴) · (1 / (𝑁‘𝐵))))
19	14, 18	eqtrd 2794	. 2 ⊢ (((𝑅 ∈ NrmRing ∧ 𝑅 ∈ NzRing) ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑈)) → (𝑁‘(𝐴(._r‘𝑅)((inv_r‘𝑅)‘𝐵))) = ((𝑁‘𝐴) · (1 / (𝑁‘𝐵))))
20		nmdvr.d	. . . . 5 ⊢ / = (/_r‘𝑅)
21	8, 12, 6, 7, 20	dvrval 19496	. . . 4 ⊢ ((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑈) → (𝐴 / 𝐵) = (𝐴(._r‘𝑅)((inv_r‘𝑅)‘𝐵)))
22	21	adantl 486	. . 3 ⊢ (((𝑅 ∈ NrmRing ∧ 𝑅 ∈ NzRing) ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑈)) → (𝐴 / 𝐵) = (𝐴(._r‘𝑅)((inv_r‘𝑅)‘𝐵)))
23	22	fveq2d 6660	. 2 ⊢ (((𝑅 ∈ NrmRing ∧ 𝑅 ∈ NzRing) ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑈)) → (𝑁‘(𝐴 / 𝐵)) = (𝑁‘(𝐴(._r‘𝑅)((inv_r‘𝑅)‘𝐵))))
24		nrgngp 23354	. . . . . 6 ⊢ (𝑅 ∈ NrmRing → 𝑅 ∈ NrmGrp)
25	24	ad2antrr 726	. . . . 5 ⊢ (((𝑅 ∈ NrmRing ∧ 𝑅 ∈ NzRing) ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑈)) → 𝑅 ∈ NrmGrp)
26	8, 11	nmcl 23308	. . . . 5 ⊢ ((𝑅 ∈ NrmGrp ∧ 𝐴 ∈ 𝑋) → (𝑁‘𝐴) ∈ ℝ)
27	25, 2, 26	syl2anc 588	. . . 4 ⊢ (((𝑅 ∈ NrmRing ∧ 𝑅 ∈ NzRing) ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑈)) → (𝑁‘𝐴) ∈ ℝ)
28	27	recnd 10697	. . 3 ⊢ (((𝑅 ∈ NrmRing ∧ 𝑅 ∈ NzRing) ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑈)) → (𝑁‘𝐴) ∈ ℂ)
29	8, 6	unitss 19471	. . . . . 6 ⊢ 𝑈 ⊆ 𝑋
30	29, 5	sseldi 3891	. . . . 5 ⊢ (((𝑅 ∈ NrmRing ∧ 𝑅 ∈ NzRing) ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑈)) → 𝐵 ∈ 𝑋)
31	8, 11	nmcl 23308	. . . . 5 ⊢ ((𝑅 ∈ NrmGrp ∧ 𝐵 ∈ 𝑋) → (𝑁‘𝐵) ∈ ℝ)
32	25, 30, 31	syl2anc 588	. . . 4 ⊢ (((𝑅 ∈ NrmRing ∧ 𝑅 ∈ NzRing) ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑈)) → (𝑁‘𝐵) ∈ ℝ)
33	32	recnd 10697	. . 3 ⊢ (((𝑅 ∈ NrmRing ∧ 𝑅 ∈ NzRing) ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑈)) → (𝑁‘𝐵) ∈ ℂ)
34	11, 6	unitnmn0 23360	. . . . 5 ⊢ ((𝑅 ∈ NrmRing ∧ 𝑅 ∈ NzRing ∧ 𝐵 ∈ 𝑈) → (𝑁‘𝐵) ≠ 0)
35	34	3expa 1116	. . . 4 ⊢ (((𝑅 ∈ NrmRing ∧ 𝑅 ∈ NzRing) ∧ 𝐵 ∈ 𝑈) → (𝑁‘𝐵) ≠ 0)
36	35	adantrl 716	. . 3 ⊢ (((𝑅 ∈ NrmRing ∧ 𝑅 ∈ NzRing) ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑈)) → (𝑁‘𝐵) ≠ 0)
37	28, 33, 36	divrecd 11447	. 2 ⊢ (((𝑅 ∈ NrmRing ∧ 𝑅 ∈ NzRing) ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑈)) → ((𝑁‘𝐴) / (𝑁‘𝐵)) = ((𝑁‘𝐴) · (1 / (𝑁‘𝐵))))
38	19, 23, 37	3eqtr4d 2804	1 ⊢ (((𝑅 ∈ NrmRing ∧ 𝑅 ∈ NzRing) ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑈)) → (𝑁‘(𝐴 / 𝐵)) = ((𝑁‘𝐴) / (𝑁‘𝐵)))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ∧ wa 400 = wceq 1539 ∈ wcel 2112 ≠ wne 2952 ‘cfv 6333 (class class class)co 7148 ℝcr 10564 0cc0 10565 1c1 10566 · cmul 10570 / cdiv 11325 Basecbs 16531 ._rcmulr 16614 Ringcrg 19355 Unitcui 19450 inv_rcinvr 19482 /_rcdvr 19493 NzRingcnzr 20088 normcnm 23268 NrmGrpcngp 23269 NrmRingcnrg 23271

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1798 ax-4 1812 ax-5 1912 ax-6 1971 ax-7 2016 ax-8 2114 ax-9 2122 ax-10 2143 ax-11 2159 ax-12 2176 ax-ext 2730 ax-rep 5154 ax-sep 5167 ax-nul 5174 ax-pow 5232 ax-pr 5296 ax-un 7457 ax-cnex 10621 ax-resscn 10622 ax-1cn 10623 ax-icn 10624 ax-addcl 10625 ax-addrcl 10626 ax-mulcl 10627 ax-mulrcl 10628 ax-mulcom 10629 ax-addass 10630 ax-mulass 10631 ax-distr 10632 ax-i2m1 10633 ax-1ne0 10634 ax-1rid 10635 ax-rnegex 10636 ax-rrecex 10637 ax-cnre 10638 ax-pre-lttri 10639 ax-pre-lttrn 10640 ax-pre-ltadd 10641 ax-pre-mulgt0 10642 ax-pre-sup 10643

This theorem depends on definitions: df-bi 210 df-an 401 df-or 846 df-3or 1086 df-3an 1087 df-tru 1542 df-fal 1552 df-ex 1783 df-nf 1787 df-sb 2071 df-mo 2558 df-eu 2589 df-clab 2737 df-cleq 2751 df-clel 2831 df-nfc 2902 df-ne 2953 df-nel 3057 df-ral 3076 df-rex 3077 df-reu 3078 df-rmo 3079 df-rab 3080 df-v 3412 df-sbc 3698 df-csb 3807 df-dif 3862 df-un 3864 df-in 3866 df-ss 3876 df-pss 3878 df-nul 4227 df-if 4419 df-pw 4494 df-sn 4521 df-pr 4523 df-tp 4525 df-op 4527 df-uni 4797 df-iun 4883 df-br 5031 df-opab 5093 df-mpt 5111 df-tr 5137 df-id 5428 df-eprel 5433 df-po 5441 df-so 5442 df-fr 5481 df-we 5483 df-xp 5528 df-rel 5529 df-cnv 5530 df-co 5531 df-dm 5532 df-rn 5533 df-res 5534 df-ima 5535 df-pred 6124 df-ord 6170 df-on 6171 df-lim 6172 df-suc 6173 df-iota 6292 df-fun 6335 df-fn 6336 df-f 6337 df-f1 6338 df-fo 6339 df-f1o 6340 df-fv 6341 df-riota 7106 df-ov 7151 df-oprab 7152 df-mpo 7153 df-om 7578 df-1st 7691 df-2nd 7692 df-tpos 7900 df-wrecs 7955 df-recs 8016 df-rdg 8054 df-er 8297 df-map 8416 df-en 8526 df-dom 8527 df-sdom 8528 df-sup 8929 df-inf 8930 df-pnf 10705 df-mnf 10706 df-xr 10707 df-ltxr 10708 df-le 10709 df-sub 10900 df-neg 10901 df-div 11326 df-nn 11665 df-2 11727 df-3 11728 df-n0 11925 df-z 12011 df-uz 12273 df-q 12379 df-rp 12421 df-xneg 12538 df-xadd 12539 df-xmul 12540 df-ico 12775 df-ndx 16534 df-slot 16535 df-base 16537 df-sets 16538 df-ress 16539 df-plusg 16626 df-mulr 16627 df-0g 16763 df-topgen 16765 df-mgm 17908 df-sgrp 17957 df-mnd 17968 df-grp 18162 df-minusg 18163 df-mgp 19298 df-ur 19310 df-ring 19357 df-oppr 19434 df-dvdsr 19452 df-unit 19453 df-invr 19483 df-dvr 19494 df-abv 19646 df-nzr 20089 df-psmet 20148 df-xmet 20149 df-met 20150 df-bl 20151 df-mopn 20152 df-top 21584 df-topon 21601 df-topsp 21623 df-bases 21636 df-xms 23012 df-ms 23013 df-nm 23274 df-ngp 23275 df-nrg 23277

This theorem is referenced by: qqhnm 31449

W3C validator