Theorem qqhval2lem 24318

Description: Lemma for qqhval2 24319 (Contributed by Thierry Arnoux, 29-Oct-2017.)

Hypotheses

Ref	Expression
qqhval2.0	|- B = ( Base ` R )
qqhval2.1	|- ./ = (/r ` R )
qqhval2.2	|- L = ( ZRHom ` R )

Assertion

Ref	Expression
qqhval2lem	|- ( ( ( R e. DivRing /\ (chr ` R ) = 0 ) /\ ( X e. ZZ /\ Y e. ZZ /\ Y =/= 0 ) ) -> ( ( L ` (numer ` ( X / Y ) ) ) ./ ( L ` (denom ` ( X / Y ) ) ) ) = ( ( L ` X ) ./ ( L ` Y ) ) )

Proof of Theorem qqhval2lem

Step	Hyp	Ref	Expression
1		drngrng 15797	. . . . 5 |- ( R e. DivRing -> R e. Ring )
2		eqid 2404	. . . . . 6 |- (ℂfld ↾s ZZ ) = (ℂfld ↾s ZZ )
3		qqhval2.2	. . . . . 6 |- L = ( ZRHom ` R )
4	2, 3	zrhrhm 16748	. . . . 5 |- ( R e. Ring -> L e. ( (ℂfld ↾s ZZ ) RingHom R ) )
5	1, 4	syl 16	. . . 4 |- ( R e. DivRing -> L e. ( (ℂfld ↾s ZZ ) RingHom R ) )
6	5	ad2antrr 707	. . 3 |- ( ( ( R e. DivRing /\ (chr ` R ) = 0 ) /\ ( X e. ZZ /\ Y e. ZZ /\ Y =/= 0 ) ) -> L e. ( (ℂfld ↾s ZZ ) RingHom R ) )
7		simpr1 963	. . . . . 6 |- ( ( ( R e. DivRing /\ (chr ` R ) = 0 ) /\ ( X e. ZZ /\ Y e. ZZ /\ Y =/= 0 ) ) -> X e. ZZ )
8		simpr2 964	. . . . . 6 |- ( ( ( R e. DivRing /\ (chr ` R ) = 0 ) /\ ( X e. ZZ /\ Y e. ZZ /\ Y =/= 0 ) ) -> Y e. ZZ )
9	7, 8	gcdcld 12973	. . . . 5 |- ( ( ( R e. DivRing /\ (chr ` R ) = 0 ) /\ ( X e. ZZ /\ Y e. ZZ /\ Y =/= 0 ) ) -> ( X gcd Y ) e. NN0 )
10	9	nn0zd 10329	. . . 4 |- ( ( ( R e. DivRing /\ (chr ` R ) = 0 ) /\ ( X e. ZZ /\ Y e. ZZ /\ Y =/= 0 ) ) -> ( X gcd Y ) e. ZZ )
11		simpr3 965	. . . . 5 |- ( ( ( R e. DivRing /\ (chr ` R ) = 0 ) /\ ( X e. ZZ /\ Y e. ZZ /\ Y =/= 0 ) ) -> Y =/= 0 )
12		gcdeq0 12976	. . . . . . . . 9 |- ( ( X e. ZZ /\ Y e. ZZ ) -> ( ( X gcd Y ) = 0 <-> ( X = 0 /\ Y = 0 ) ) )
13	12	simplbda 608	. . . . . . . 8 |- ( ( ( X e. ZZ /\ Y e. ZZ ) /\ ( X gcd Y ) = 0 ) -> Y = 0 )
14	13	ex 424	. . . . . . 7 |- ( ( X e. ZZ /\ Y e. ZZ ) -> ( ( X gcd Y ) = 0 -> Y = 0 ) )
15	14	necon3d 2605	. . . . . 6 |- ( ( X e. ZZ /\ Y e. ZZ ) -> ( Y =/= 0 -> ( X gcd Y ) =/= 0 ) )
16	15	imp 419	. . . . 5 |- ( ( ( X e. ZZ /\ Y e. ZZ ) /\ Y =/= 0 ) -> ( X gcd Y ) =/= 0 )
17	7, 8, 11, 16	syl21anc 1183	. . . 4 |- ( ( ( R e. DivRing /\ (chr ` R ) = 0 ) /\ ( X e. ZZ /\ Y e. ZZ /\ Y =/= 0 ) ) -> ( X gcd Y ) =/= 0 )
18		gcddvds 12970	. . . . . 6 |- ( ( X e. ZZ /\ Y e. ZZ ) -> ( ( X gcd Y ) || X /\ ( X gcd Y ) || Y ) )
19	7, 8, 18	syl2anc 643	. . . . 5 |- ( ( ( R e. DivRing /\ (chr ` R ) = 0 ) /\ ( X e. ZZ /\ Y e. ZZ /\ Y =/= 0 ) ) -> ( ( X gcd Y ) || X /\ ( X gcd Y ) || Y ) )
20	19	simpld 446	. . . 4 |- ( ( ( R e. DivRing /\ (chr ` R ) = 0 ) /\ ( X e. ZZ /\ Y e. ZZ /\ Y =/= 0 ) ) -> ( X gcd Y ) || X )
21		dvdsval2 12810	. . . . 5 |- ( ( ( X gcd Y ) e. ZZ /\ ( X gcd Y ) =/= 0 /\ X e. ZZ ) -> ( ( X gcd Y ) || X <-> ( X / ( X gcd Y ) ) e. ZZ ) )
22	21	biimpa 471	. . . 4 |- ( ( ( ( X gcd Y ) e. ZZ /\ ( X gcd Y ) =/= 0 /\ X e. ZZ ) /\ ( X gcd Y ) || X ) -> ( X / ( X gcd Y ) ) e. ZZ )
23	10, 17, 7, 20, 22	syl31anc 1187	. . 3 |- ( ( ( R e. DivRing /\ (chr ` R ) = 0 ) /\ ( X e. ZZ /\ Y e. ZZ /\ Y =/= 0 ) ) -> ( X / ( X gcd Y ) ) e. ZZ )
24	19	simprd 450	. . . 4 |- ( ( ( R e. DivRing /\ (chr ` R ) = 0 ) /\ ( X e. ZZ /\ Y e. ZZ /\ Y =/= 0 ) ) -> ( X gcd Y ) || Y )
25		dvdsval2 12810	. . . . 5 |- ( ( ( X gcd Y ) e. ZZ /\ ( X gcd Y ) =/= 0 /\ Y e. ZZ ) -> ( ( X gcd Y ) || Y <-> ( Y / ( X gcd Y ) ) e. ZZ ) )
26	25	biimpa 471	. . . 4 |- ( ( ( ( X gcd Y ) e. ZZ /\ ( X gcd Y ) =/= 0 /\ Y e. ZZ ) /\ ( X gcd Y ) || Y ) -> ( Y / ( X gcd Y ) ) e. ZZ )
27	10, 17, 8, 24, 26	syl31anc 1187	. . 3 |- ( ( ( R e. DivRing /\ (chr ` R ) = 0 ) /\ ( X e. ZZ /\ Y e. ZZ /\ Y =/= 0 ) ) -> ( Y / ( X gcd Y ) ) e. ZZ )
28	2	zzsbase 24216	. . . . . . 7 |- ZZ = ( Base ` (ℂfld ↾s ZZ ) )
29		qqhval2.0	. . . . . . 7 |- B = ( Base ` R )
30	28, 29	rhmf 15782	. . . . . 6 |- ( L e. ( (ℂfld ↾s ZZ ) RingHom R ) -> L : ZZ --> B )
31	6, 30	syl 16	. . . . 5 |- ( ( ( R e. DivRing /\ (chr ` R ) = 0 ) /\ ( X e. ZZ /\ Y e. ZZ /\ Y =/= 0 ) ) -> L : ZZ --> B )
32	31, 27	ffvelrnd 5830	. . . 4 |- ( ( ( R e. DivRing /\ (chr ` R ) = 0 ) /\ ( X e. ZZ /\ Y e. ZZ /\ Y =/= 0 ) ) -> ( L ` ( Y / ( X gcd Y ) ) ) e. B )
33		ffn 5550	. . . . . 6 |- ( L : ZZ --> B -> L Fn ZZ )
34	31, 33	syl 16	. . . . 5 |- ( ( ( R e. DivRing /\ (chr ` R ) = 0 ) /\ ( X e. ZZ /\ Y e. ZZ /\ Y =/= 0 ) ) -> L Fn ZZ )
35	8	zcnd 10332	. . . . . . . 8 |- ( ( ( R e. DivRing /\ (chr ` R ) = 0 ) /\ ( X e. ZZ /\ Y e. ZZ /\ Y =/= 0 ) ) -> Y e. CC )
36	10	zcnd 10332	. . . . . . . 8 |- ( ( ( R e. DivRing /\ (chr ` R ) = 0 ) /\ ( X e. ZZ /\ Y e. ZZ /\ Y =/= 0 ) ) -> ( X gcd Y ) e. CC )
37	35, 36, 11, 17	divne0d 9762	. . . . . . 7 |- ( ( ( R e. DivRing /\ (chr ` R ) = 0 ) /\ ( X e. ZZ /\ Y e. ZZ /\ Y =/= 0 ) ) -> ( Y / ( X gcd Y ) ) =/= 0 )
38		ovex 6065	. . . . . . . . 9 |- ( Y / ( X gcd Y ) ) e. _V
39	38	elsnc 3797	. . . . . . . 8 |- ( ( Y / ( X gcd Y ) ) e. { 0 } <-> ( Y / ( X gcd Y ) ) = 0 )
40	39	necon3bbii 2598	. . . . . . 7 |- ( -. ( Y / ( X gcd Y ) ) e. { 0 } <-> ( Y / ( X gcd Y ) ) =/= 0 )
41	37, 40	sylibr 204	. . . . . 6 |- ( ( ( R e. DivRing /\ (chr ` R ) = 0 ) /\ ( X e. ZZ /\ Y e. ZZ /\ Y =/= 0 ) ) -> -. ( Y / ( X gcd Y ) ) e. { 0 } )
42	1	ad2antrr 707	. . . . . . 7 |- ( ( ( R e. DivRing /\ (chr ` R ) = 0 ) /\ ( X e. ZZ /\ Y e. ZZ /\ Y =/= 0 ) ) -> R e. Ring )
43		simplr 732	. . . . . . 7 |- ( ( ( R e. DivRing /\ (chr ` R ) = 0 ) /\ ( X e. ZZ /\ Y e. ZZ /\ Y =/= 0 ) ) -> (chr ` R ) = 0 )
44		eqid 2404	. . . . . . . . 9 |- ( 0g ` R ) = ( 0g ` R )
45	29, 3, 44	zrhker 24314	. . . . . . . 8 |- ( R e. Ring -> ( (chr ` R ) = 0 <-> ( `' L " { ( 0g ` R ) } ) = { 0 } ) )
46	45	biimpa 471	. . . . . . 7 |- ( ( R e. Ring /\ (chr ` R ) = 0 ) -> ( `' L " { ( 0g ` R ) } ) = { 0 } )
47	42, 43, 46	syl2anc 643	. . . . . 6 |- ( ( ( R e. DivRing /\ (chr ` R ) = 0 ) /\ ( X e. ZZ /\ Y e. ZZ /\ Y =/= 0 ) ) -> ( `' L " { ( 0g ` R ) } ) = { 0 } )
48	41, 47	neleqtrrd 2500	. . . . 5 |- ( ( ( R e. DivRing /\ (chr ` R ) = 0 ) /\ ( X e. ZZ /\ Y e. ZZ /\ Y =/= 0 ) ) -> -. ( Y / ( X gcd Y ) ) e. ( `' L " { ( 0g ` R ) } ) )
49		elpreima 5809	. . . . . . . . 9 |- ( L Fn ZZ -> ( ( Y / ( X gcd Y ) ) e. ( `' L " { ( 0g ` R ) } ) <-> ( ( Y / ( X gcd Y ) ) e. ZZ /\ ( L ` ( Y / ( X gcd Y ) ) ) e. { ( 0g ` R ) } ) ) )
50	49	baibd 876	. . . . . . . 8 |- ( ( L Fn ZZ /\ ( Y / ( X gcd Y ) ) e. ZZ ) -> ( ( Y / ( X gcd Y ) ) e. ( `' L " { ( 0g ` R ) } ) <-> ( L ` ( Y / ( X gcd Y ) ) ) e. { ( 0g ` R ) } ) )
51	50	biimprd 215	. . . . . . 7 |- ( ( L Fn ZZ /\ ( Y / ( X gcd Y ) ) e. ZZ ) -> ( ( L ` ( Y / ( X gcd Y ) ) ) e. { ( 0g ` R ) } -> ( Y / ( X gcd Y ) ) e. ( `' L " { ( 0g ` R ) } ) ) )
52	51	con3and 429	. . . . . 6 |- ( ( ( L Fn ZZ /\ ( Y / ( X gcd Y ) ) e. ZZ ) /\ -. ( Y / ( X gcd Y ) ) e. ( `' L " { ( 0g ` R ) } ) ) -> -. ( L ` ( Y / ( X gcd Y ) ) ) e. { ( 0g ` R ) } )
53		fvex 5701	. . . . . . . 8 |- ( L ` ( Y / ( X gcd Y ) ) ) e. _V
54	53	elsnc 3797	. . . . . . 7 |- ( ( L ` ( Y / ( X gcd Y ) ) ) e. { ( 0g ` R ) } <-> ( L ` ( Y / ( X gcd Y ) ) ) = ( 0g ` R ) )
55	54	necon3bbii 2598	. . . . . 6 |- ( -. ( L ` ( Y / ( X gcd Y ) ) ) e. { ( 0g ` R ) } <-> ( L ` ( Y / ( X gcd Y ) ) ) =/= ( 0g ` R ) )
56	52, 55	sylib 189	. . . . 5 |- ( ( ( L Fn ZZ /\ ( Y / ( X gcd Y ) ) e. ZZ ) /\ -. ( Y / ( X gcd Y ) ) e. ( `' L " { ( 0g ` R ) } ) ) -> ( L ` ( Y / ( X gcd Y ) ) ) =/= ( 0g ` R ) )
57	34, 27, 48, 56	syl21anc 1183	. . . 4 |- ( ( ( R e. DivRing /\ (chr ` R ) = 0 ) /\ ( X e. ZZ /\ Y e. ZZ /\ Y =/= 0 ) ) -> ( L ` ( Y / ( X gcd Y ) ) ) =/= ( 0g ` R ) )
58		eqid 2404	. . . . . 6 |- (Unit ` R ) = (Unit ` R )
59	29, 58, 44	drngunit 15795	. . . . 5 |- ( R e. DivRing -> ( ( L ` ( Y / ( X gcd Y ) ) ) e. (Unit ` R ) <-> ( ( L ` ( Y / ( X gcd Y ) ) ) e. B /\ ( L ` ( Y / ( X gcd Y ) ) ) =/= ( 0g ` R ) ) ) )
60	59	ad2antrr 707	. . . 4 |- ( ( ( R e. DivRing /\ (chr ` R ) = 0 ) /\ ( X e. ZZ /\ Y e. ZZ /\ Y =/= 0 ) ) -> ( ( L ` ( Y / ( X gcd Y ) ) ) e. (Unit ` R ) <-> ( ( L ` ( Y / ( X gcd Y ) ) ) e. B /\ ( L ` ( Y / ( X gcd Y ) ) ) =/= ( 0g ` R ) ) ) )
61	32, 57, 60	mpbir2and 889	. . 3 |- ( ( ( R e. DivRing /\ (chr ` R ) = 0 ) /\ ( X e. ZZ /\ Y e. ZZ /\ Y =/= 0 ) ) -> ( L ` ( Y / ( X gcd Y ) ) ) e. (Unit ` R ) )
62	31, 10	ffvelrnd 5830	. . . 4 |- ( ( ( R e. DivRing /\ (chr ` R ) = 0 ) /\ ( X e. ZZ /\ Y e. ZZ /\ Y =/= 0 ) ) -> ( L ` ( X gcd Y ) ) e. B )
63		ovex 6065	. . . . . . . . 9 |- ( X gcd Y ) e. _V
64	63	elsnc 3797	. . . . . . . 8 |- ( ( X gcd Y ) e. { 0 } <-> ( X gcd Y ) = 0 )
65	64	necon3bbii 2598	. . . . . . 7 |- ( -. ( X gcd Y ) e. { 0 } <-> ( X gcd Y ) =/= 0 )
66	17, 65	sylibr 204	. . . . . 6 |- ( ( ( R e. DivRing /\ (chr ` R ) = 0 ) /\ ( X e. ZZ /\ Y e. ZZ /\ Y =/= 0 ) ) -> -. ( X gcd Y ) e. { 0 } )
67	66, 47	neleqtrrd 2500	. . . . 5 |- ( ( ( R e. DivRing /\ (chr ` R ) = 0 ) /\ ( X e. ZZ /\ Y e. ZZ /\ Y =/= 0 ) ) -> -. ( X gcd Y ) e. ( `' L " { ( 0g ` R ) } ) )
68		elpreima 5809	. . . . . . . . 9 |- ( L Fn ZZ -> ( ( X gcd Y ) e. ( `' L " { ( 0g ` R ) } ) <-> ( ( X gcd Y ) e. ZZ /\ ( L ` ( X gcd Y ) ) e. { ( 0g ` R ) } ) ) )
69	68	baibd 876	. . . . . . . 8 |- ( ( L Fn ZZ /\ ( X gcd Y ) e. ZZ ) -> ( ( X gcd Y ) e. ( `' L " { ( 0g ` R ) } ) <-> ( L ` ( X gcd Y ) ) e. { ( 0g ` R ) } ) )
70	69	biimprd 215	. . . . . . 7 |- ( ( L Fn ZZ /\ ( X gcd Y ) e. ZZ ) -> ( ( L ` ( X gcd Y ) ) e. { ( 0g ` R ) } -> ( X gcd Y ) e. ( `' L " { ( 0g ` R ) } ) ) )
71	70	con3and 429	. . . . . 6 |- ( ( ( L Fn ZZ /\ ( X gcd Y ) e. ZZ ) /\ -. ( X gcd Y ) e. ( `' L " { ( 0g ` R ) } ) ) -> -. ( L ` ( X gcd Y ) ) e. { ( 0g ` R ) } )
72		fvex 5701	. . . . . . . 8 |- ( L ` ( X gcd Y ) ) e. _V
73	72	elsnc 3797	. . . . . . 7 |- ( ( L ` ( X gcd Y ) ) e. { ( 0g ` R ) } <-> ( L ` ( X gcd Y ) ) = ( 0g ` R ) )
74	73	necon3bbii 2598	. . . . . 6 |- ( -. ( L ` ( X gcd Y ) ) e. { ( 0g ` R ) } <-> ( L ` ( X gcd Y ) ) =/= ( 0g ` R ) )
75	71, 74	sylib 189	. . . . 5 |- ( ( ( L Fn ZZ /\ ( X gcd Y ) e. ZZ ) /\ -. ( X gcd Y ) e. ( `' L " { ( 0g ` R ) } ) ) -> ( L ` ( X gcd Y ) ) =/= ( 0g ` R ) )
76	34, 10, 67, 75	syl21anc 1183	. . . 4 |- ( ( ( R e. DivRing /\ (chr ` R ) = 0 ) /\ ( X e. ZZ /\ Y e. ZZ /\ Y =/= 0 ) ) -> ( L ` ( X gcd Y ) ) =/= ( 0g ` R ) )
77	29, 58, 44	drngunit 15795	. . . . 5 |- ( R e. DivRing -> ( ( L ` ( X gcd Y ) ) e. (Unit ` R ) <-> ( ( L ` ( X gcd Y ) ) e. B /\ ( L ` ( X gcd Y ) ) =/= ( 0g ` R ) ) ) )
78	77	ad2antrr 707	. . . 4 |- ( ( ( R e. DivRing /\ (chr ` R ) = 0 ) /\ ( X e. ZZ /\ Y e. ZZ /\ Y =/= 0 ) ) -> ( ( L ` ( X gcd Y ) ) e. (Unit ` R ) <-> ( ( L ` ( X gcd Y ) ) e. B /\ ( L ` ( X gcd Y ) ) =/= ( 0g ` R ) ) ) )
79	62, 76, 78	mpbir2and 889	. . 3 |- ( ( ( R e. DivRing /\ (chr ` R ) = 0 ) /\ ( X e. ZZ /\ Y e. ZZ /\ Y =/= 0 ) ) -> ( L ` ( X gcd Y ) ) e. (Unit ` R ) )
80		qqhval2.1	. . . 4 |- ./ = (/r ` R )
81	2	zzsmulr 24219	. . . 4 |- x. = ( .r ` (ℂfld ↾s ZZ ) )
82	58, 28, 80, 81	rhmdvd 24212	. . 3 |- ( ( L e. ( (ℂfld ↾s ZZ ) RingHom R ) /\ ( ( X / ( X gcd Y ) ) e. ZZ /\ ( Y / ( X gcd Y ) ) e. ZZ /\ ( X gcd Y ) e. ZZ ) /\ ( ( L ` ( Y / ( X gcd Y ) ) ) e. (Unit ` R ) /\ ( L ` ( X gcd Y ) ) e. (Unit ` R ) ) ) -> ( ( L ` ( X / ( X gcd Y ) ) ) ./ ( L ` ( Y / ( X gcd Y ) ) ) ) = ( ( L ` ( ( X / ( X gcd Y ) ) x. ( X gcd Y ) ) ) ./ ( L ` ( ( Y / ( X gcd Y ) ) x. ( X gcd Y ) ) ) ) )
83	6, 23, 27, 10, 61, 79, 82	syl132anc 1202	. 2 |- ( ( ( R e. DivRing /\ (chr ` R ) = 0 ) /\ ( X e. ZZ /\ Y e. ZZ /\ Y =/= 0 ) ) -> ( ( L ` ( X / ( X gcd Y ) ) ) ./ ( L ` ( Y / ( X gcd Y ) ) ) ) = ( ( L ` ( ( X / ( X gcd Y ) ) x. ( X gcd Y ) ) ) ./ ( L ` ( ( Y / ( X gcd Y ) ) x. ( X gcd Y ) ) ) ) )
84		divnumden 13095	. . . . . . . 8 |- ( ( X e. ZZ /\ Y e. NN ) -> ( (numer ` ( X / Y ) ) = ( X / ( X gcd Y ) ) /\ (denom ` ( X / Y ) ) = ( Y / ( X gcd Y ) ) ) )
85	7, 84	sylan 458	. . . . . . 7 |- ( ( ( ( R e. DivRing /\ (chr ` R ) = 0 ) /\ ( X e. ZZ /\ Y e. ZZ /\ Y =/= 0 ) ) /\ Y e. NN ) -> ( (numer ` ( X / Y ) ) = ( X / ( X gcd Y ) ) /\ (denom ` ( X / Y ) ) = ( Y / ( X gcd Y ) ) ) )
86	85	simpld 446	. . . . . 6 |- ( ( ( ( R e. DivRing /\ (chr ` R ) = 0 ) /\ ( X e. ZZ /\ Y e. ZZ /\ Y =/= 0 ) ) /\ Y e. NN ) -> (numer ` ( X / Y ) ) = ( X / ( X gcd Y ) ) )
87	86	eqcomd 2409	. . . . 5 |- ( ( ( ( R e. DivRing /\ (chr ` R ) = 0 ) /\ ( X e. ZZ /\ Y e. ZZ /\ Y =/= 0 ) ) /\ Y e. NN ) -> ( X / ( X gcd Y ) ) = (numer ` ( X / Y ) ) )
88	87	fveq2d 5691	. . . 4 |- ( ( ( ( R e. DivRing /\ (chr ` R ) = 0 ) /\ ( X e. ZZ /\ Y e. ZZ /\ Y =/= 0 ) ) /\ Y e. NN ) -> ( L ` ( X / ( X gcd Y ) ) ) = ( L ` (numer ` ( X / Y ) ) ) )
89	85	simprd 450	. . . . . 6 |- ( ( ( ( R e. DivRing /\ (chr ` R ) = 0 ) /\ ( X e. ZZ /\ Y e. ZZ /\ Y =/= 0 ) ) /\ Y e. NN ) -> (denom ` ( X / Y ) ) = ( Y / ( X gcd Y ) ) )
90	89	eqcomd 2409	. . . . 5 |- ( ( ( ( R e. DivRing /\ (chr ` R ) = 0 ) /\ ( X e. ZZ /\ Y e. ZZ /\ Y =/= 0 ) ) /\ Y e. NN ) -> ( Y / ( X gcd Y ) ) = (denom ` ( X / Y ) ) )
91	90	fveq2d 5691	. . . 4 |- ( ( ( ( R e. DivRing /\ (chr ` R ) = 0 ) /\ ( X e. ZZ /\ Y e. ZZ /\ Y =/= 0 ) ) /\ Y e. NN ) -> ( L ` ( Y / ( X gcd Y ) ) ) = ( L ` (denom ` ( X / Y ) ) ) )
92	88, 91	oveq12d 6058	. . 3 |- ( ( ( ( R e. DivRing /\ (chr ` R ) = 0 ) /\ ( X e. ZZ /\ Y e. ZZ /\ Y =/= 0 ) ) /\ Y e. NN ) -> ( ( L ` ( X / ( X gcd Y ) ) ) ./ ( L ` ( Y / ( X gcd Y ) ) ) ) = ( ( L ` (numer ` ( X / Y ) ) ) ./ ( L ` (denom ` ( X / Y ) ) ) ) )
93	23	adantr 452	. . . . . . . . 9 |- ( ( ( ( R e. DivRing /\ (chr ` R ) = 0 ) /\ ( X e. ZZ /\ Y e. ZZ /\ Y =/= 0 ) ) /\ -u Y e. NN ) -> ( X / ( X gcd Y ) ) e. ZZ )
94	93	zcnd 10332	. . . . . . . 8 |- ( ( ( ( R e. DivRing /\ (chr ` R ) = 0 ) /\ ( X e. ZZ /\ Y e. ZZ /\ Y =/= 0 ) ) /\ -u Y e. NN ) -> ( X / ( X gcd Y ) ) e. CC )
95	94	mulm1d 9441	. . . . . . 7 |- ( ( ( ( R e. DivRing /\ (chr ` R ) = 0 ) /\ ( X e. ZZ /\ Y e. ZZ /\ Y =/= 0 ) ) /\ -u Y e. NN ) -> ( -u 1 x. ( X / ( X gcd Y ) ) ) = -u ( X / ( X gcd Y ) ) )
96		neg1cn 10023	. . . . . . . . 9 |- -u 1 e. CC
97	96	a1i 11	. . . . . . . 8 |- ( ( ( ( R e. DivRing /\ (chr ` R ) = 0 ) /\ ( X e. ZZ /\ Y e. ZZ /\ Y =/= 0 ) ) /\ -u Y e. NN ) -> -u 1 e. CC )
98	97, 94	mulcomd 9065	. . . . . . 7 |- ( ( ( ( R e. DivRing /\ (chr ` R ) = 0 ) /\ ( X e. ZZ /\ Y e. ZZ /\ Y =/= 0 ) ) /\ -u Y e. NN ) -> ( -u 1 x. ( X / ( X gcd Y ) ) ) = ( ( X / ( X gcd Y ) ) x. -u 1 ) )
99	95, 98	eqtr3d 2438	. . . . . 6 |- ( ( ( ( R e. DivRing /\ (chr ` R ) = 0 ) /\ ( X e. ZZ /\ Y e. ZZ /\ Y =/= 0 ) ) /\ -u Y e. NN ) -> -u ( X / ( X gcd Y ) ) = ( ( X / ( X gcd Y ) ) x. -u 1 ) )
100	99	fveq2d 5691	. . . . 5 |- ( ( ( ( R e. DivRing /\ (chr ` R ) = 0 ) /\ ( X e. ZZ /\ Y e. ZZ /\ Y =/= 0 ) ) /\ -u Y e. NN ) -> ( L ` -u ( X / ( X gcd Y ) ) ) = ( L ` ( ( X / ( X gcd Y ) ) x. -u 1 ) ) )
101	27	adantr 452	. . . . . . . . 9 |- ( ( ( ( R e. DivRing /\ (chr ` R ) = 0 ) /\ ( X e. ZZ /\ Y e. ZZ /\ Y =/= 0 ) ) /\ -u Y e. NN ) -> ( Y / ( X gcd Y ) ) e. ZZ )
102	101	zcnd 10332	. . . . . . . 8 |- ( ( ( ( R e. DivRing /\ (chr ` R ) = 0 ) /\ ( X e. ZZ /\ Y e. ZZ /\ Y =/= 0 ) ) /\ -u Y e. NN ) -> ( Y / ( X gcd Y ) ) e. CC )
103	102	mulm1d 9441	. . . . . . 7 |- ( ( ( ( R e. DivRing /\ (chr ` R ) = 0 ) /\ ( X e. ZZ /\ Y e. ZZ /\ Y =/= 0 ) ) /\ -u Y e. NN ) -> ( -u 1 x. ( Y / ( X gcd Y ) ) ) = -u ( Y / ( X gcd Y ) ) )
104	97, 102	mulcomd 9065	. . . . . . 7 |- ( ( ( ( R e. DivRing /\ (chr ` R ) = 0 ) /\ ( X e. ZZ /\ Y e. ZZ /\ Y =/= 0 ) ) /\ -u Y e. NN ) -> ( -u 1 x. ( Y / ( X gcd Y ) ) ) = ( ( Y / ( X gcd Y ) ) x. -u 1 ) )
105	103, 104	eqtr3d 2438	. . . . . 6 |- ( ( ( ( R e. DivRing /\ (chr ` R ) = 0 ) /\ ( X e. ZZ /\ Y e. ZZ /\ Y =/= 0 ) ) /\ -u Y e. NN ) -> -u ( Y / ( X gcd Y ) ) = ( ( Y / ( X gcd Y ) ) x. -u 1 ) )
106	105	fveq2d 5691	. . . . 5 |- ( ( ( ( R e. DivRing /\ (chr ` R ) = 0 ) /\ ( X e. ZZ /\ Y e. ZZ /\ Y =/= 0 ) ) /\ -u Y e. NN ) -> ( L ` -u ( Y / ( X gcd Y ) ) ) = ( L ` ( ( Y / ( X gcd Y ) ) x. -u 1 ) ) )
107	100, 106	oveq12d 6058	. . . 4 |- ( ( ( ( R e. DivRing /\ (chr ` R ) = 0 ) /\ ( X e. ZZ /\ Y e. ZZ /\ Y =/= 0 ) ) /\ -u Y e. NN ) -> ( ( L ` -u ( X / ( X gcd Y ) ) ) ./ ( L ` -u ( Y / ( X gcd Y ) ) ) ) = ( ( L ` ( ( X / ( X gcd Y ) ) x. -u 1 ) ) ./ ( L ` ( ( Y / ( X gcd Y ) ) x. -u 1 ) ) ) )
108	7	adantr 452	. . . . . . . 8 |- ( ( ( ( R e. DivRing /\ (chr ` R ) = 0 ) /\ ( X e. ZZ /\ Y e. ZZ /\ Y =/= 0 ) ) /\ -u Y e. NN ) -> X e. ZZ )
109	8	adantr 452	. . . . . . . 8 |- ( ( ( ( R e. DivRing /\ (chr ` R ) = 0 ) /\ ( X e. ZZ /\ Y e. ZZ /\ Y =/= 0 ) ) /\ -u Y e. NN ) -> Y e. ZZ )
110		simpr 448	. . . . . . . 8 |- ( ( ( ( R e. DivRing /\ (chr ` R ) = 0 ) /\ ( X e. ZZ /\ Y e. ZZ /\ Y =/= 0 ) ) /\ -u Y e. NN ) -> -u Y e. NN )
111		divnumden2 24114	. . . . . . . 8 |- ( ( X e. ZZ /\ Y e. ZZ /\ -u Y e. NN ) -> ( (numer ` ( X / Y ) ) = -u ( X / ( X gcd Y ) ) /\ (denom ` ( X / Y ) ) = -u ( Y / ( X gcd Y ) ) ) )
112	108, 109, 110, 111	syl3anc 1184	. . . . . . 7 |- ( ( ( ( R e. DivRing /\ (chr ` R ) = 0 ) /\ ( X e. ZZ /\ Y e. ZZ /\ Y =/= 0 ) ) /\ -u Y e. NN ) -> ( (numer ` ( X / Y ) ) = -u ( X / ( X gcd Y ) ) /\ (denom ` ( X / Y ) ) = -u ( Y / ( X gcd Y ) ) ) )
113	112	simpld 446	. . . . . 6 |- ( ( ( ( R e. DivRing /\ (chr ` R ) = 0 ) /\ ( X e. ZZ /\ Y e. ZZ /\ Y =/= 0 ) ) /\ -u Y e. NN ) -> (numer ` ( X / Y ) ) = -u ( X / ( X gcd Y ) ) )
114	113	fveq2d 5691	. . . . 5 |- ( ( ( ( R e. DivRing /\ (chr ` R ) = 0 ) /\ ( X e. ZZ /\ Y e. ZZ /\ Y =/= 0 ) ) /\ -u Y e. NN ) -> ( L ` (numer ` ( X / Y ) ) ) = ( L ` -u ( X / ( X gcd Y ) ) ) )
115	112	simprd 450	. . . . . 6 |- ( ( ( ( R e. DivRing /\ (chr ` R ) = 0 ) /\ ( X e. ZZ /\ Y e. ZZ /\ Y =/= 0 ) ) /\ -u Y e. NN ) -> (denom ` ( X / Y ) ) = -u ( Y / ( X gcd Y ) ) )
116	115	fveq2d 5691	. . . . 5 |- ( ( ( ( R e. DivRing /\ (chr ` R ) = 0 ) /\ ( X e. ZZ /\ Y e. ZZ /\ Y =/= 0 ) ) /\ -u Y e. NN ) -> ( L ` (denom ` ( X / Y ) ) ) = ( L ` -u ( Y / ( X gcd Y ) ) ) )
117	114, 116	oveq12d 6058	. . . 4 |- ( ( ( ( R e. DivRing /\ (chr ` R ) = 0 ) /\ ( X e. ZZ /\ Y e. ZZ /\ Y =/= 0 ) ) /\ -u Y e. NN ) -> ( ( L ` (numer ` ( X / Y ) ) ) ./ ( L ` (denom ` ( X / Y ) ) ) ) = ( ( L ` -u ( X / ( X gcd Y ) ) ) ./ ( L ` -u ( Y / ( X gcd Y ) ) ) ) )
118	6	adantr 452	. . . . 5 |- ( ( ( ( R e. DivRing /\ (chr ` R ) = 0 ) /\ ( X e. ZZ /\ Y e. ZZ /\ Y =/= 0 ) ) /\ -u Y e. NN ) -> L e. ( (ℂfld ↾s ZZ ) RingHom R ) )
119		1z 10267	. . . . . . 7 |- 1 e. ZZ
120	119	a1i 11	. . . . . 6 |- ( ( ( ( R e. DivRing /\ (chr ` R ) = 0 ) /\ ( X e. ZZ /\ Y e. ZZ /\ Y =/= 0 ) ) /\ -u Y e. NN ) -> 1 e. ZZ )
121	120	znegcld 10333	. . . . 5 |- ( ( ( ( R e. DivRing /\ (chr ` R ) = 0 ) /\ ( X e. ZZ /\ Y e. ZZ /\ Y =/= 0 ) ) /\ -u Y e. NN ) -> -u 1 e. ZZ )
122	61	adantr 452	. . . . 5 |- ( ( ( ( R e. DivRing /\ (chr ` R ) = 0 ) /\ ( X e. ZZ /\ Y e. ZZ /\ Y =/= 0 ) ) /\ -u Y e. NN ) -> ( L ` ( Y / ( X gcd Y ) ) ) e. (Unit ` R ) )
123		znegcl 10269	. . . . . . . . 9 |- ( 1 e. ZZ -> -u 1 e. ZZ )
124	119, 123	ax-mp 8	. . . . . . . 8 |- -u 1 e. ZZ
125		ax-1cn 9004	. . . . . . . . . 10 |- 1 e. CC
126	125	absnegi 12158	. . . . . . . . 9 |- ( abs ` -u 1 ) = ( abs ` 1 )
127		abs1 12057	. . . . . . . . 9 |- ( abs ` 1 ) = 1
128	126, 127	eqtri 2424	. . . . . . . 8 |- ( abs ` -u 1 ) = 1
129	2	zrngunit 16720	. . . . . . . 8 |- ( -u 1 e. (Unit ` (ℂfld ↾s ZZ ) ) <-> ( -u 1 e. ZZ /\ ( abs ` -u 1 ) = 1 ) )
130	124, 128, 129	mpbir2an 887	. . . . . . 7 |- -u 1 e. (Unit ` (ℂfld ↾s ZZ ) )
131	130	a1i 11	. . . . . 6 |- ( ( ( ( R e. DivRing /\ (chr ` R ) = 0 ) /\ ( X e. ZZ /\ Y e. ZZ /\ Y =/= 0 ) ) /\ -u Y e. NN ) -> -u 1 e. (Unit ` (ℂfld ↾s ZZ ) ) )
132		elrhmunit 24211	. . . . . 6 |- ( ( L e. ( (ℂfld ↾s ZZ ) RingHom R ) /\ -u 1 e. (Unit ` (ℂfld ↾s ZZ ) ) ) -> ( L ` -u 1 ) e. (Unit ` R ) )
133	118, 131, 132	syl2anc 643	. . . . 5 |- ( ( ( ( R e. DivRing /\ (chr ` R ) = 0 ) /\ ( X e. ZZ /\ Y e. ZZ /\ Y =/= 0 ) ) /\ -u Y e. NN ) -> ( L ` -u 1 ) e. (Unit ` R ) )
134	58, 28, 80, 81	rhmdvd 24212	. . . . 5 |- ( ( L e. ( (ℂfld ↾s ZZ ) RingHom R ) /\ ( ( X / ( X gcd Y ) ) e. ZZ /\ ( Y / ( X gcd Y ) ) e. ZZ /\ -u 1 e. ZZ ) /\ ( ( L ` ( Y / ( X gcd Y ) ) ) e. (Unit ` R ) /\ ( L ` -u 1 ) e. (Unit ` R ) ) ) -> ( ( L ` ( X / ( X gcd Y ) ) ) ./ ( L ` ( Y / ( X gcd Y ) ) ) ) = ( ( L ` ( ( X / ( X gcd Y ) ) x. -u 1 ) ) ./ ( L ` ( ( Y / ( X gcd Y ) ) x. -u 1 ) ) ) )
135	118, 93, 101, 121, 122, 133, 134	syl132anc 1202	. . . 4 |- ( ( ( ( R e. DivRing /\ (chr ` R ) = 0 ) /\ ( X e. ZZ /\ Y e. ZZ /\ Y =/= 0 ) ) /\ -u Y e. NN ) -> ( ( L ` ( X / ( X gcd Y ) ) ) ./ ( L ` ( Y / ( X gcd Y ) ) ) ) = ( ( L ` ( ( X / ( X gcd Y ) ) x. -u 1 ) ) ./ ( L ` ( ( Y / ( X gcd Y ) ) x. -u 1 ) ) ) )
136	107, 117, 135	3eqtr4rd 2447	. . 3 |- ( ( ( ( R e. DivRing /\ (chr ` R ) = 0 ) /\ ( X e. ZZ /\ Y e. ZZ /\ Y =/= 0 ) ) /\ -u Y e. NN ) -> ( ( L ` ( X / ( X gcd Y ) ) ) ./ ( L ` ( Y / ( X gcd Y ) ) ) ) = ( ( L ` (numer ` ( X / Y ) ) ) ./ ( L ` (denom ` ( X / Y ) ) ) ) )
137		simp3 959	. . . . . 6 |- ( ( X e. ZZ /\ Y e. ZZ /\ Y =/= 0 ) -> Y =/= 0 )
138	137	neneqd 2583	. . . . 5 |- ( ( X e. ZZ /\ Y e. ZZ /\ Y =/= 0 ) -> -. Y = 0 )
139		simp2 958	. . . . . . . 8 |- ( ( X e. ZZ /\ Y e. ZZ /\ Y =/= 0 ) -> Y e. ZZ )
140		elz 10240	. . . . . . . 8 |- ( Y e. ZZ <-> ( Y e. RR /\ ( Y = 0 \/ Y e. NN \/ -u Y e. NN ) ) )
141	139, 140	sylib 189	. . . . . . 7 |- ( ( X e. ZZ /\ Y e. ZZ /\ Y =/= 0 ) -> ( Y e. RR /\ ( Y = 0 \/ Y e. NN \/ -u Y e. NN ) ) )
142	141	simprd 450	. . . . . 6 |- ( ( X e. ZZ /\ Y e. ZZ /\ Y =/= 0 ) -> ( Y = 0 \/ Y e. NN \/ -u Y e. NN ) )
143		3orass 939	. . . . . 6 |- ( ( Y = 0 \/ Y e. NN \/ -u Y e. NN ) <-> ( Y = 0 \/ ( Y e. NN \/ -u Y e. NN ) ) )
144	142, 143	sylib 189	. . . . 5 |- ( ( X e. ZZ /\ Y e. ZZ /\ Y =/= 0 ) -> ( Y = 0 \/ ( Y e. NN \/ -u Y e. NN ) ) )
145		orel1 372	. . . . 5 |- ( -. Y = 0 -> ( ( Y = 0 \/ ( Y e. NN \/ -u Y e. NN ) ) -> ( Y e. NN \/ -u Y e. NN ) ) )
146	138, 144, 145	sylc 58	. . . 4 |- ( ( X e. ZZ /\ Y e. ZZ /\ Y =/= 0 ) -> ( Y e. NN \/ -u Y e. NN ) )
147	146	adantl 453	. . 3 |- ( ( ( R e. DivRing /\ (chr ` R ) = 0 ) /\ ( X e. ZZ /\ Y e. ZZ /\ Y =/= 0 ) ) -> ( Y e. NN \/ -u Y e. NN ) )
148	92, 136, 147	mpjaodan 762	. 2 |- ( ( ( R e. DivRing /\ (chr ` R ) = 0 ) /\ ( X e. ZZ /\ Y e. ZZ /\ Y =/= 0 ) ) -> ( ( L ` ( X / ( X gcd Y ) ) ) ./ ( L ` ( Y / ( X gcd Y ) ) ) ) = ( ( L ` (numer ` ( X / Y ) ) ) ./ ( L ` (denom ` ( X / Y ) ) ) ) )
149	7	zcnd 10332	. . . . 5 |- ( ( ( R e. DivRing /\ (chr ` R ) = 0 ) /\ ( X e. ZZ /\ Y e. ZZ /\ Y =/= 0 ) ) -> X e. CC )
150	149, 36, 17	divcan1d 9747	. . . 4 |- ( ( ( R e. DivRing /\ (chr ` R ) = 0 ) /\ ( X e. ZZ /\ Y e. ZZ /\ Y =/= 0 ) ) -> ( ( X / ( X gcd Y ) ) x. ( X gcd Y ) ) = X )
151	150	fveq2d 5691	. . 3 |- ( ( ( R e. DivRing /\ (chr ` R ) = 0 ) /\ ( X e. ZZ /\ Y e. ZZ /\ Y =/= 0 ) ) -> ( L ` ( ( X / ( X gcd Y ) ) x. ( X gcd Y ) ) ) = ( L ` X ) )
152	35, 36, 17	divcan1d 9747	. . . 4 |- ( ( ( R e. DivRing /\ (chr ` R ) = 0 ) /\ ( X e. ZZ /\ Y e. ZZ /\ Y =/= 0 ) ) -> ( ( Y / ( X gcd Y ) ) x. ( X gcd Y ) ) = Y )
153	152	fveq2d 5691	. . 3 |- ( ( ( R e. DivRing /\ (chr ` R ) = 0 ) /\ ( X e. ZZ /\ Y e. ZZ /\ Y =/= 0 ) ) -> ( L ` ( ( Y / ( X gcd Y ) ) x. ( X gcd Y ) ) ) = ( L ` Y ) )
154	151, 153	oveq12d 6058	. 2 |- ( ( ( R e. DivRing /\ (chr ` R ) = 0 ) /\ ( X e. ZZ /\ Y e. ZZ /\ Y =/= 0 ) ) -> ( ( L ` ( ( X / ( X gcd Y ) ) x. ( X gcd Y ) ) ) ./ ( L ` ( ( Y / ( X gcd Y ) ) x. ( X gcd Y ) ) ) ) = ( ( L ` X ) ./ ( L ` Y ) ) )
155	83, 148, 154	3eqtr3d 2444	1 |- ( ( ( R e. DivRing /\ (chr ` R ) = 0 ) /\ ( X e. ZZ /\ Y e. ZZ /\ Y =/= 0 ) ) -> ( ( L ` (numer ` ( X / Y ) ) ) ./ ( L ` (denom ` ( X / Y ) ) ) ) = ( ( L ` X ) ./ ( L ` Y ) ) )

Syntax hints:   -. wn 3   -> wi 4   <-> wb 177   \/ wo 358   /\ wa 359   \/ w3o 935   /\ w3a 936   = wceq 1649   e. wcel 1721   =/= wne 2567   {csn 3774   class class class wbr 4172   `'ccnv 4836   "cima 4840   Fn wfn 5408   -->wf 5409   ` cfv 5413  (class class class)co 6040   CCcc 8944   RRcr 8945   0cc0 8946   1c1 8947   x. cmul 8951   -ucneg 9248   / cdiv 9633   NNcn 9956   ZZcz 10238   abscabs 11994   || cdivides 12807   gcd cgcd 12961  numercnumer 13080  denomcdenom 13081   Basecbs 13424   ↾_s cress 13425   0gc0g 13678   Ringcrg 15615  Unitcui 15699  /_rcdvr 15742   RingHom crh 15772   DivRingcdr 15790  ℂ_fldccnfld 16658   ZRHomczrh 16733  chrcchr 16735

This theorem is referenced by:  qqhval2  24319  qqhvq  24324

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-13 1723  ax-14 1725  ax-6 1740  ax-7 1745  ax-11 1757  ax-12 1946  ax-ext 2385  ax-rep 4280  ax-sep 4290  ax-nul 4298  ax-pow 4337  ax-pr 4363  ax-un 4660  ax-inf2 7552  ax-cnex 9002  ax-resscn 9003  ax-1cn 9004  ax-icn 9005  ax-addcl 9006  ax-addrcl 9007  ax-mulcl 9008  ax-mulrcl 9009  ax-mulcom 9010  ax-addass 9011  ax-mulass 9012  ax-distr 9013  ax-i2m1 9014  ax-1ne0 9015  ax-1rid 9016  ax-rnegex 9017  ax-rrecex 9018  ax-cnre 9019  ax-pre-lttri 9020  ax-pre-lttrn 9021  ax-pre-ltadd 9022  ax-pre-mulgt0 9023  ax-pre-sup 9024  ax-addf 9025  ax-mulf 9026

This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-3or 937  df-3an 938  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-eu 2258  df-mo 2259  df-clab 2391  df-cleq 2397  df-clel 2400  df-nfc 2529  df-ne 2569  df-nel 2570  df-ral 2671  df-rex 2672  df-reu 2673  df-rmo 2674  df-rab 2675  df-v 2918  df-sbc 3122  df-csb 3212  df-dif 3283  df-un 3285  df-in 3287  df-ss 3294  df-pss 3296  df-nul 3589  df-if 3700  df-pw 3761  df-sn 3780  df-pr 3781  df-tp 3782  df-op 3783  df-uni 3976  df-int 4011  df-iun 4055  df-br 4173  df-opab 4227  df-mpt 4228  df-tr 4263  df-eprel 4454  df-id 4458  df-po 4463  df-so 4464  df-fr 4501  df-we 4503  df-ord 4544  df-on 4545  df-lim 4546  df-suc 4547  df-om 4805  df-xp 4843  df-rel 4844  df-cnv 4845  df-co 4846  df-dm 4847  df-rn 4848  df-res 4849  df-ima 4850  df-iota 5377  df-fun 5415  df-fn 5416  df-f 5417  df-f1 5418  df-fo 5419  df-f1o 5420  df-fv 5421  df-ov 6043  df-oprab 6044  df-mpt2 6045  df-1st 6308  df-2nd 6309  df-tpos 6438  df-riota 6508  df-recs 6592  df-rdg 6627  df-1o 6683  df-oadd 6687  df-er 6864  df-map 6979  df-en 7069  df-dom 7070  df-sdom 7071  df-fin 7072  df-sup 7404  df-pnf 9078  df-mnf 9079  df-xr 9080  df-ltxr 9081  df-le 9082  df-sub 9249  df-neg 9250  df-div 9634  df-nn 9957  df-2 10014  df-3 10015  df-4 10016  df-5 10017  df-6 10018  df-7 10019  df-8 10020  df-9 10021  df-10 10022  df-n0 10178  df-z 10239  df-dec 10339  df-uz 10445  df-q 10531  df-rp 10569  df-fz 11000  df-fl 11157  df-mod 11206  df-seq 11279  df-exp 11338  df-cj 11859  df-re 11860  df-im 11861  df-sqr 11995  df-abs 11996  df-dvds 12808  df-gcd 12962  df-numer 13082  df-denom 13083  df-gz 13253  df-struct 13426  df-ndx 13427  df-slot 13428  df-base 13429  df-sets 13430  df-ress 13431  df-plusg 13497  df-mulr 13498  df-starv 13499  df-tset 13503  df-ple 13504  df-ds 13506  df-unif 13507  df-0g 13682  df-mnd 14645  df-mhm 14693  df-grp 14767  df-minusg 14768  df-sbg 14769  df-mulg 14770  df-subg 14896  df-ghm 14959  df-od 15122  df-cmn 15369  df-mgp 15604  df-rng 15618  df-cring 15619  df-ur 15620  df-oppr 15683  df-dvdsr 15701  df-unit 15702  df-invr 15732  df-dvr 15743  df-rnghom 15774  df-drng 15792  df-subrg 15821  df-cnfld 16659  df-zrh 16737  df-chr 16739