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

Theorem ringurd 20082
Description: Deduce the unity element of a ring from its properties. (Contributed by Thierry Arnoux, 6-Sep-2016.)
Hypotheses
Ref Expression
ringurd.b (๐œ‘ โ†’ ๐ต = (Baseโ€˜๐‘…))
ringurd.p (๐œ‘ โ†’ ยท = (.rโ€˜๐‘…))
ringurd.z (๐œ‘ โ†’ 1 โˆˆ ๐ต)
ringurd.i ((๐œ‘ โˆง ๐‘ฅ โˆˆ ๐ต) โ†’ ( 1 ยท ๐‘ฅ) = ๐‘ฅ)
ringurd.j ((๐œ‘ โˆง ๐‘ฅ โˆˆ ๐ต) โ†’ (๐‘ฅ ยท 1 ) = ๐‘ฅ)
Assertion
Ref Expression
ringurd (๐œ‘ โ†’ 1 = (1rโ€˜๐‘…))
Distinct variable groups:   ๐‘ฅ,๐ต   ๐‘ฅ,๐‘…   ๐‘ฅ, 1   ๐‘ฅ, ยท   ๐œ‘,๐‘ฅ

Proof of Theorem ringurd
Dummy variable ๐‘’ is distinct from all other variables.
StepHypRef Expression
1 eqid 2724 . . 3 (Baseโ€˜๐‘…) = (Baseโ€˜๐‘…)
2 eqid 2724 . . 3 (.rโ€˜๐‘…) = (.rโ€˜๐‘…)
3 eqid 2724 . . 3 (1rโ€˜๐‘…) = (1rโ€˜๐‘…)
41, 2, 3dfur2 20081 . 2 (1rโ€˜๐‘…) = (โ„ฉ๐‘’(๐‘’ โˆˆ (Baseโ€˜๐‘…) โˆง โˆ€๐‘ฅ โˆˆ (Baseโ€˜๐‘…)((๐‘’(.rโ€˜๐‘…)๐‘ฅ) = ๐‘ฅ โˆง (๐‘ฅ(.rโ€˜๐‘…)๐‘’) = ๐‘ฅ)))
5 ringurd.z . . . 4 (๐œ‘ โ†’ 1 โˆˆ ๐ต)
6 ringurd.b . . . 4 (๐œ‘ โ†’ ๐ต = (Baseโ€˜๐‘…))
75, 6eleqtrd 2827 . . 3 (๐œ‘ โ†’ 1 โˆˆ (Baseโ€˜๐‘…))
8 ringurd.i . . . . . 6 ((๐œ‘ โˆง ๐‘ฅ โˆˆ ๐ต) โ†’ ( 1 ยท ๐‘ฅ) = ๐‘ฅ)
9 ringurd.j . . . . . 6 ((๐œ‘ โˆง ๐‘ฅ โˆˆ ๐ต) โ†’ (๐‘ฅ ยท 1 ) = ๐‘ฅ)
108, 9jca 511 . . . . 5 ((๐œ‘ โˆง ๐‘ฅ โˆˆ ๐ต) โ†’ (( 1 ยท ๐‘ฅ) = ๐‘ฅ โˆง (๐‘ฅ ยท 1 ) = ๐‘ฅ))
1110ralrimiva 3138 . . . 4 (๐œ‘ โ†’ โˆ€๐‘ฅ โˆˆ ๐ต (( 1 ยท ๐‘ฅ) = ๐‘ฅ โˆง (๐‘ฅ ยท 1 ) = ๐‘ฅ))
12 ringurd.p . . . . . . . . 9 (๐œ‘ โ†’ ยท = (.rโ€˜๐‘…))
1312adantr 480 . . . . . . . 8 ((๐œ‘ โˆง ๐‘ฅ โˆˆ ๐ต) โ†’ ยท = (.rโ€˜๐‘…))
1413oveqd 7419 . . . . . . 7 ((๐œ‘ โˆง ๐‘ฅ โˆˆ ๐ต) โ†’ ( 1 ยท ๐‘ฅ) = ( 1 (.rโ€˜๐‘…)๐‘ฅ))
1514eqeq1d 2726 . . . . . 6 ((๐œ‘ โˆง ๐‘ฅ โˆˆ ๐ต) โ†’ (( 1 ยท ๐‘ฅ) = ๐‘ฅ โ†” ( 1 (.rโ€˜๐‘…)๐‘ฅ) = ๐‘ฅ))
1613oveqd 7419 . . . . . . 7 ((๐œ‘ โˆง ๐‘ฅ โˆˆ ๐ต) โ†’ (๐‘ฅ ยท 1 ) = (๐‘ฅ(.rโ€˜๐‘…) 1 ))
1716eqeq1d 2726 . . . . . 6 ((๐œ‘ โˆง ๐‘ฅ โˆˆ ๐ต) โ†’ ((๐‘ฅ ยท 1 ) = ๐‘ฅ โ†” (๐‘ฅ(.rโ€˜๐‘…) 1 ) = ๐‘ฅ))
1815, 17anbi12d 630 . . . . 5 ((๐œ‘ โˆง ๐‘ฅ โˆˆ ๐ต) โ†’ ((( 1 ยท ๐‘ฅ) = ๐‘ฅ โˆง (๐‘ฅ ยท 1 ) = ๐‘ฅ) โ†” (( 1 (.rโ€˜๐‘…)๐‘ฅ) = ๐‘ฅ โˆง (๐‘ฅ(.rโ€˜๐‘…) 1 ) = ๐‘ฅ)))
196, 18raleqbidva 3319 . . . 4 (๐œ‘ โ†’ (โˆ€๐‘ฅ โˆˆ ๐ต (( 1 ยท ๐‘ฅ) = ๐‘ฅ โˆง (๐‘ฅ ยท 1 ) = ๐‘ฅ) โ†” โˆ€๐‘ฅ โˆˆ (Baseโ€˜๐‘…)(( 1 (.rโ€˜๐‘…)๐‘ฅ) = ๐‘ฅ โˆง (๐‘ฅ(.rโ€˜๐‘…) 1 ) = ๐‘ฅ)))
2011, 19mpbid 231 . . 3 (๐œ‘ โ†’ โˆ€๐‘ฅ โˆˆ (Baseโ€˜๐‘…)(( 1 (.rโ€˜๐‘…)๐‘ฅ) = ๐‘ฅ โˆง (๐‘ฅ(.rโ€˜๐‘…) 1 ) = ๐‘ฅ))
216eleq2d 2811 . . . . . . . 8 (๐œ‘ โ†’ (๐‘’ โˆˆ ๐ต โ†” ๐‘’ โˆˆ (Baseโ€˜๐‘…)))
2213oveqd 7419 . . . . . . . . . . 11 ((๐œ‘ โˆง ๐‘ฅ โˆˆ ๐ต) โ†’ (๐‘’ ยท ๐‘ฅ) = (๐‘’(.rโ€˜๐‘…)๐‘ฅ))
2322eqeq1d 2726 . . . . . . . . . 10 ((๐œ‘ โˆง ๐‘ฅ โˆˆ ๐ต) โ†’ ((๐‘’ ยท ๐‘ฅ) = ๐‘ฅ โ†” (๐‘’(.rโ€˜๐‘…)๐‘ฅ) = ๐‘ฅ))
2413oveqd 7419 . . . . . . . . . . 11 ((๐œ‘ โˆง ๐‘ฅ โˆˆ ๐ต) โ†’ (๐‘ฅ ยท ๐‘’) = (๐‘ฅ(.rโ€˜๐‘…)๐‘’))
2524eqeq1d 2726 . . . . . . . . . 10 ((๐œ‘ โˆง ๐‘ฅ โˆˆ ๐ต) โ†’ ((๐‘ฅ ยท ๐‘’) = ๐‘ฅ โ†” (๐‘ฅ(.rโ€˜๐‘…)๐‘’) = ๐‘ฅ))
2623, 25anbi12d 630 . . . . . . . . 9 ((๐œ‘ โˆง ๐‘ฅ โˆˆ ๐ต) โ†’ (((๐‘’ ยท ๐‘ฅ) = ๐‘ฅ โˆง (๐‘ฅ ยท ๐‘’) = ๐‘ฅ) โ†” ((๐‘’(.rโ€˜๐‘…)๐‘ฅ) = ๐‘ฅ โˆง (๐‘ฅ(.rโ€˜๐‘…)๐‘’) = ๐‘ฅ)))
276, 26raleqbidva 3319 . . . . . . . 8 (๐œ‘ โ†’ (โˆ€๐‘ฅ โˆˆ ๐ต ((๐‘’ ยท ๐‘ฅ) = ๐‘ฅ โˆง (๐‘ฅ ยท ๐‘’) = ๐‘ฅ) โ†” โˆ€๐‘ฅ โˆˆ (Baseโ€˜๐‘…)((๐‘’(.rโ€˜๐‘…)๐‘ฅ) = ๐‘ฅ โˆง (๐‘ฅ(.rโ€˜๐‘…)๐‘’) = ๐‘ฅ)))
2821, 27anbi12d 630 . . . . . . 7 (๐œ‘ โ†’ ((๐‘’ โˆˆ ๐ต โˆง โˆ€๐‘ฅ โˆˆ ๐ต ((๐‘’ ยท ๐‘ฅ) = ๐‘ฅ โˆง (๐‘ฅ ยท ๐‘’) = ๐‘ฅ)) โ†” (๐‘’ โˆˆ (Baseโ€˜๐‘…) โˆง โˆ€๐‘ฅ โˆˆ (Baseโ€˜๐‘…)((๐‘’(.rโ€˜๐‘…)๐‘ฅ) = ๐‘ฅ โˆง (๐‘ฅ(.rโ€˜๐‘…)๐‘’) = ๐‘ฅ))))
298ralrimiva 3138 . . . . . . . . . . . 12 (๐œ‘ โ†’ โˆ€๐‘ฅ โˆˆ ๐ต ( 1 ยท ๐‘ฅ) = ๐‘ฅ)
3029adantr 480 . . . . . . . . . . 11 ((๐œ‘ โˆง ๐‘’ โˆˆ ๐ต) โ†’ โˆ€๐‘ฅ โˆˆ ๐ต ( 1 ยท ๐‘ฅ) = ๐‘ฅ)
31 simpr 484 . . . . . . . . . . . 12 ((๐œ‘ โˆง ๐‘’ โˆˆ ๐ต) โ†’ ๐‘’ โˆˆ ๐ต)
32 simpr 484 . . . . . . . . . . . . . 14 (((๐œ‘ โˆง ๐‘’ โˆˆ ๐ต) โˆง ๐‘ฅ = ๐‘’) โ†’ ๐‘ฅ = ๐‘’)
3332oveq2d 7418 . . . . . . . . . . . . 13 (((๐œ‘ โˆง ๐‘’ โˆˆ ๐ต) โˆง ๐‘ฅ = ๐‘’) โ†’ ( 1 ยท ๐‘ฅ) = ( 1 ยท ๐‘’))
3433, 32eqeq12d 2740 . . . . . . . . . . . 12 (((๐œ‘ โˆง ๐‘’ โˆˆ ๐ต) โˆง ๐‘ฅ = ๐‘’) โ†’ (( 1 ยท ๐‘ฅ) = ๐‘ฅ โ†” ( 1 ยท ๐‘’) = ๐‘’))
3531, 34rspcdv 3596 . . . . . . . . . . 11 ((๐œ‘ โˆง ๐‘’ โˆˆ ๐ต) โ†’ (โˆ€๐‘ฅ โˆˆ ๐ต ( 1 ยท ๐‘ฅ) = ๐‘ฅ โ†’ ( 1 ยท ๐‘’) = ๐‘’))
3630, 35mpd 15 . . . . . . . . . 10 ((๐œ‘ โˆง ๐‘’ โˆˆ ๐ต) โ†’ ( 1 ยท ๐‘’) = ๐‘’)
3736adantrr 714 . . . . . . . . 9 ((๐œ‘ โˆง (๐‘’ โˆˆ ๐ต โˆง โˆ€๐‘ฅ โˆˆ ๐ต ((๐‘’ ยท ๐‘ฅ) = ๐‘ฅ โˆง (๐‘ฅ ยท ๐‘’) = ๐‘ฅ))) โ†’ ( 1 ยท ๐‘’) = ๐‘’)
385adantr 480 . . . . . . . . . 10 ((๐œ‘ โˆง (๐‘’ โˆˆ ๐ต โˆง โˆ€๐‘ฅ โˆˆ ๐ต ((๐‘’ ยท ๐‘ฅ) = ๐‘ฅ โˆง (๐‘ฅ ยท ๐‘’) = ๐‘ฅ))) โ†’ 1 โˆˆ ๐ต)
39 simprr 770 . . . . . . . . . 10 ((๐œ‘ โˆง (๐‘’ โˆˆ ๐ต โˆง โˆ€๐‘ฅ โˆˆ ๐ต ((๐‘’ ยท ๐‘ฅ) = ๐‘ฅ โˆง (๐‘ฅ ยท ๐‘’) = ๐‘ฅ))) โ†’ โˆ€๐‘ฅ โˆˆ ๐ต ((๐‘’ ยท ๐‘ฅ) = ๐‘ฅ โˆง (๐‘ฅ ยท ๐‘’) = ๐‘ฅ))
40 oveq2 7410 . . . . . . . . . . . . . 14 (๐‘ฅ = 1 โ†’ (๐‘’ ยท ๐‘ฅ) = (๐‘’ ยท 1 ))
41 id 22 . . . . . . . . . . . . . 14 (๐‘ฅ = 1 โ†’ ๐‘ฅ = 1 )
4240, 41eqeq12d 2740 . . . . . . . . . . . . 13 (๐‘ฅ = 1 โ†’ ((๐‘’ ยท ๐‘ฅ) = ๐‘ฅ โ†” (๐‘’ ยท 1 ) = 1 ))
43 oveq1 7409 . . . . . . . . . . . . . 14 (๐‘ฅ = 1 โ†’ (๐‘ฅ ยท ๐‘’) = ( 1 ยท ๐‘’))
4443, 41eqeq12d 2740 . . . . . . . . . . . . 13 (๐‘ฅ = 1 โ†’ ((๐‘ฅ ยท ๐‘’) = ๐‘ฅ โ†” ( 1 ยท ๐‘’) = 1 ))
4542, 44anbi12d 630 . . . . . . . . . . . 12 (๐‘ฅ = 1 โ†’ (((๐‘’ ยท ๐‘ฅ) = ๐‘ฅ โˆง (๐‘ฅ ยท ๐‘’) = ๐‘ฅ) โ†” ((๐‘’ ยท 1 ) = 1 โˆง ( 1 ยท ๐‘’) = 1 )))
4645rspcva 3602 . . . . . . . . . . 11 (( 1 โˆˆ ๐ต โˆง โˆ€๐‘ฅ โˆˆ ๐ต ((๐‘’ ยท ๐‘ฅ) = ๐‘ฅ โˆง (๐‘ฅ ยท ๐‘’) = ๐‘ฅ)) โ†’ ((๐‘’ ยท 1 ) = 1 โˆง ( 1 ยท ๐‘’) = 1 ))
4746simprd 495 . . . . . . . . . 10 (( 1 โˆˆ ๐ต โˆง โˆ€๐‘ฅ โˆˆ ๐ต ((๐‘’ ยท ๐‘ฅ) = ๐‘ฅ โˆง (๐‘ฅ ยท ๐‘’) = ๐‘ฅ)) โ†’ ( 1 ยท ๐‘’) = 1 )
4838, 39, 47syl2anc 583 . . . . . . . . 9 ((๐œ‘ โˆง (๐‘’ โˆˆ ๐ต โˆง โˆ€๐‘ฅ โˆˆ ๐ต ((๐‘’ ยท ๐‘ฅ) = ๐‘ฅ โˆง (๐‘ฅ ยท ๐‘’) = ๐‘ฅ))) โ†’ ( 1 ยท ๐‘’) = 1 )
4937, 48eqtr3d 2766 . . . . . . . 8 ((๐œ‘ โˆง (๐‘’ โˆˆ ๐ต โˆง โˆ€๐‘ฅ โˆˆ ๐ต ((๐‘’ ยท ๐‘ฅ) = ๐‘ฅ โˆง (๐‘ฅ ยท ๐‘’) = ๐‘ฅ))) โ†’ ๐‘’ = 1 )
5049ex 412 . . . . . . 7 (๐œ‘ โ†’ ((๐‘’ โˆˆ ๐ต โˆง โˆ€๐‘ฅ โˆˆ ๐ต ((๐‘’ ยท ๐‘ฅ) = ๐‘ฅ โˆง (๐‘ฅ ยท ๐‘’) = ๐‘ฅ)) โ†’ ๐‘’ = 1 ))
5128, 50sylbird 260 . . . . . 6 (๐œ‘ โ†’ ((๐‘’ โˆˆ (Baseโ€˜๐‘…) โˆง โˆ€๐‘ฅ โˆˆ (Baseโ€˜๐‘…)((๐‘’(.rโ€˜๐‘…)๐‘ฅ) = ๐‘ฅ โˆง (๐‘ฅ(.rโ€˜๐‘…)๐‘’) = ๐‘ฅ)) โ†’ ๐‘’ = 1 ))
5251alrimiv 1922 . . . . 5 (๐œ‘ โ†’ โˆ€๐‘’((๐‘’ โˆˆ (Baseโ€˜๐‘…) โˆง โˆ€๐‘ฅ โˆˆ (Baseโ€˜๐‘…)((๐‘’(.rโ€˜๐‘…)๐‘ฅ) = ๐‘ฅ โˆง (๐‘ฅ(.rโ€˜๐‘…)๐‘’) = ๐‘ฅ)) โ†’ ๐‘’ = 1 ))
53 eleq1 2813 . . . . . . 7 (๐‘’ = 1 โ†’ (๐‘’ โˆˆ (Baseโ€˜๐‘…) โ†” 1 โˆˆ (Baseโ€˜๐‘…)))
54 oveq1 7409 . . . . . . . . 9 (๐‘’ = 1 โ†’ (๐‘’(.rโ€˜๐‘…)๐‘ฅ) = ( 1 (.rโ€˜๐‘…)๐‘ฅ))
5554eqeq1d 2726 . . . . . . . 8 (๐‘’ = 1 โ†’ ((๐‘’(.rโ€˜๐‘…)๐‘ฅ) = ๐‘ฅ โ†” ( 1 (.rโ€˜๐‘…)๐‘ฅ) = ๐‘ฅ))
5655ovanraleqv 7426 . . . . . . 7 (๐‘’ = 1 โ†’ (โˆ€๐‘ฅ โˆˆ (Baseโ€˜๐‘…)((๐‘’(.rโ€˜๐‘…)๐‘ฅ) = ๐‘ฅ โˆง (๐‘ฅ(.rโ€˜๐‘…)๐‘’) = ๐‘ฅ) โ†” โˆ€๐‘ฅ โˆˆ (Baseโ€˜๐‘…)(( 1 (.rโ€˜๐‘…)๐‘ฅ) = ๐‘ฅ โˆง (๐‘ฅ(.rโ€˜๐‘…) 1 ) = ๐‘ฅ)))
5753, 56anbi12d 630 . . . . . 6 (๐‘’ = 1 โ†’ ((๐‘’ โˆˆ (Baseโ€˜๐‘…) โˆง โˆ€๐‘ฅ โˆˆ (Baseโ€˜๐‘…)((๐‘’(.rโ€˜๐‘…)๐‘ฅ) = ๐‘ฅ โˆง (๐‘ฅ(.rโ€˜๐‘…)๐‘’) = ๐‘ฅ)) โ†” ( 1 โˆˆ (Baseโ€˜๐‘…) โˆง โˆ€๐‘ฅ โˆˆ (Baseโ€˜๐‘…)(( 1 (.rโ€˜๐‘…)๐‘ฅ) = ๐‘ฅ โˆง (๐‘ฅ(.rโ€˜๐‘…) 1 ) = ๐‘ฅ))))
5857eqeu 3695 . . . . 5 (( 1 โˆˆ (Baseโ€˜๐‘…) โˆง ( 1 โˆˆ (Baseโ€˜๐‘…) โˆง โˆ€๐‘ฅ โˆˆ (Baseโ€˜๐‘…)(( 1 (.rโ€˜๐‘…)๐‘ฅ) = ๐‘ฅ โˆง (๐‘ฅ(.rโ€˜๐‘…) 1 ) = ๐‘ฅ)) โˆง โˆ€๐‘’((๐‘’ โˆˆ (Baseโ€˜๐‘…) โˆง โˆ€๐‘ฅ โˆˆ (Baseโ€˜๐‘…)((๐‘’(.rโ€˜๐‘…)๐‘ฅ) = ๐‘ฅ โˆง (๐‘ฅ(.rโ€˜๐‘…)๐‘’) = ๐‘ฅ)) โ†’ ๐‘’ = 1 )) โ†’ โˆƒ!๐‘’(๐‘’ โˆˆ (Baseโ€˜๐‘…) โˆง โˆ€๐‘ฅ โˆˆ (Baseโ€˜๐‘…)((๐‘’(.rโ€˜๐‘…)๐‘ฅ) = ๐‘ฅ โˆง (๐‘ฅ(.rโ€˜๐‘…)๐‘’) = ๐‘ฅ)))
597, 7, 20, 52, 58syl121anc 1372 . . . 4 (๐œ‘ โ†’ โˆƒ!๐‘’(๐‘’ โˆˆ (Baseโ€˜๐‘…) โˆง โˆ€๐‘ฅ โˆˆ (Baseโ€˜๐‘…)((๐‘’(.rโ€˜๐‘…)๐‘ฅ) = ๐‘ฅ โˆง (๐‘ฅ(.rโ€˜๐‘…)๐‘’) = ๐‘ฅ)))
6057iota2 6523 . . . 4 (( 1 โˆˆ ๐ต โˆง โˆƒ!๐‘’(๐‘’ โˆˆ (Baseโ€˜๐‘…) โˆง โˆ€๐‘ฅ โˆˆ (Baseโ€˜๐‘…)((๐‘’(.rโ€˜๐‘…)๐‘ฅ) = ๐‘ฅ โˆง (๐‘ฅ(.rโ€˜๐‘…)๐‘’) = ๐‘ฅ))) โ†’ (( 1 โˆˆ (Baseโ€˜๐‘…) โˆง โˆ€๐‘ฅ โˆˆ (Baseโ€˜๐‘…)(( 1 (.rโ€˜๐‘…)๐‘ฅ) = ๐‘ฅ โˆง (๐‘ฅ(.rโ€˜๐‘…) 1 ) = ๐‘ฅ)) โ†” (โ„ฉ๐‘’(๐‘’ โˆˆ (Baseโ€˜๐‘…) โˆง โˆ€๐‘ฅ โˆˆ (Baseโ€˜๐‘…)((๐‘’(.rโ€˜๐‘…)๐‘ฅ) = ๐‘ฅ โˆง (๐‘ฅ(.rโ€˜๐‘…)๐‘’) = ๐‘ฅ))) = 1 ))
615, 59, 60syl2anc 583 . . 3 (๐œ‘ โ†’ (( 1 โˆˆ (Baseโ€˜๐‘…) โˆง โˆ€๐‘ฅ โˆˆ (Baseโ€˜๐‘…)(( 1 (.rโ€˜๐‘…)๐‘ฅ) = ๐‘ฅ โˆง (๐‘ฅ(.rโ€˜๐‘…) 1 ) = ๐‘ฅ)) โ†” (โ„ฉ๐‘’(๐‘’ โˆˆ (Baseโ€˜๐‘…) โˆง โˆ€๐‘ฅ โˆˆ (Baseโ€˜๐‘…)((๐‘’(.rโ€˜๐‘…)๐‘ฅ) = ๐‘ฅ โˆง (๐‘ฅ(.rโ€˜๐‘…)๐‘’) = ๐‘ฅ))) = 1 ))
627, 20, 61mpbi2and 709 . 2 (๐œ‘ โ†’ (โ„ฉ๐‘’(๐‘’ โˆˆ (Baseโ€˜๐‘…) โˆง โˆ€๐‘ฅ โˆˆ (Baseโ€˜๐‘…)((๐‘’(.rโ€˜๐‘…)๐‘ฅ) = ๐‘ฅ โˆง (๐‘ฅ(.rโ€˜๐‘…)๐‘’) = ๐‘ฅ))) = 1 )
634, 62eqtr2id 2777 1 (๐œ‘ โ†’ 1 = (1rโ€˜๐‘…))
Colors of variables: wff setvar class
Syntax hints:   โ†’ wi 4   โ†” wb 205   โˆง wa 395  โˆ€wal 1531   = wceq 1533   โˆˆ wcel 2098  โˆƒ!weu 2554  โˆ€wral 3053  โ„ฉcio 6484  โ€˜cfv 6534  (class class class)co 7402  Basecbs 17145  .rcmulr 17199  1rcur 20078
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-10 2129  ax-11 2146  ax-12 2163  ax-ext 2695  ax-sep 5290  ax-nul 5297  ax-pow 5354  ax-pr 5418  ax-un 7719  ax-cnex 11163  ax-resscn 11164  ax-1cn 11165  ax-icn 11166  ax-addcl 11167  ax-addrcl 11168  ax-mulcl 11169  ax-mulrcl 11170  ax-mulcom 11171  ax-addass 11172  ax-mulass 11173  ax-distr 11174  ax-i2m1 11175  ax-1ne0 11176  ax-1rid 11177  ax-rnegex 11178  ax-rrecex 11179  ax-cnre 11180  ax-pre-lttri 11181  ax-pre-lttrn 11182  ax-pre-ltadd 11183  ax-pre-mulgt0 11184
This theorem depends on definitions:  df-bi 206  df-an 396  df-or 845  df-3or 1085  df-3an 1086  df-tru 1536  df-fal 1546  df-ex 1774  df-nf 1778  df-sb 2060  df-mo 2526  df-eu 2555  df-clab 2702  df-cleq 2716  df-clel 2802  df-nfc 2877  df-ne 2933  df-nel 3039  df-ral 3054  df-rex 3063  df-reu 3369  df-rab 3425  df-v 3468  df-sbc 3771  df-csb 3887  df-dif 3944  df-un 3946  df-in 3948  df-ss 3958  df-pss 3960  df-nul 4316  df-if 4522  df-pw 4597  df-sn 4622  df-pr 4624  df-op 4628  df-uni 4901  df-iun 4990  df-br 5140  df-opab 5202  df-mpt 5223  df-tr 5257  df-id 5565  df-eprel 5571  df-po 5579  df-so 5580  df-fr 5622  df-we 5624  df-xp 5673  df-rel 5674  df-cnv 5675  df-co 5676  df-dm 5677  df-rn 5678  df-res 5679  df-ima 5680  df-pred 6291  df-ord 6358  df-on 6359  df-lim 6360  df-suc 6361  df-iota 6486  df-fun 6536  df-fn 6537  df-f 6538  df-f1 6539  df-fo 6540  df-f1o 6541  df-fv 6542  df-riota 7358  df-ov 7405  df-oprab 7406  df-mpo 7407  df-om 7850  df-2nd 7970  df-frecs 8262  df-wrecs 8293  df-recs 8367  df-rdg 8406  df-er 8700  df-en 8937  df-dom 8938  df-sdom 8939  df-pnf 11248  df-mnf 11249  df-xr 11250  df-ltxr 11251  df-le 11252  df-sub 11444  df-neg 11445  df-nn 12211  df-2 12273  df-sets 17098  df-slot 17116  df-ndx 17128  df-base 17146  df-plusg 17211  df-0g 17388  df-mgp 20032  df-ur 20079
This theorem is referenced by:  rngisomring1  20362  ress1r  32852
  Copyright terms: Public domain W3C validator