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

Theorem ablsimpgfindlem1 20020
Description: Lemma for ablsimpgfind 20023. An element of an abelian finite simple group which doesn't square to the identity has finite order. (Contributed by Rohan Ridenour, 3-Aug-2023.) (Proof shortened by Rohan Ridenour, 31-Oct-2023.)
Hypotheses
Ref Expression
ablsimpgfindlem1.1 ๐ต = (Baseโ€˜๐บ)
ablsimpgfindlem1.2 0 = (0gโ€˜๐บ)
ablsimpgfindlem1.3 ยท = (.gโ€˜๐บ)
ablsimpgfindlem1.4 ๐‘‚ = (odโ€˜๐บ)
ablsimpgfindlem1.5 (๐œ‘ โ†’ ๐บ โˆˆ Abel)
ablsimpgfindlem1.6 (๐œ‘ โ†’ ๐บ โˆˆ SimpGrp)
Assertion
Ref Expression
ablsimpgfindlem1 (((๐œ‘ โˆง ๐‘ฅ โˆˆ ๐ต) โˆง (2 ยท ๐‘ฅ) โ‰  0 ) โ†’ (๐‘‚โ€˜๐‘ฅ) โ‰  0)
Distinct variable groups:   ๐œ‘,๐‘ฅ   ๐‘ฅ, 0   ๐‘ฅ,๐ต
Allowed substitution hints:   ยท (๐‘ฅ)   ๐บ(๐‘ฅ)   ๐‘‚(๐‘ฅ)

Proof of Theorem ablsimpgfindlem1
Dummy variable ๐‘ฆ is distinct from all other variables.
StepHypRef Expression
1 ablsimpgfindlem1.1 . . . 4 ๐ต = (Baseโ€˜๐บ)
2 ablsimpgfindlem1.2 . . . 4 0 = (0gโ€˜๐บ)
3 ablsimpgfindlem1.3 . . . 4 ยท = (.gโ€˜๐บ)
4 ablsimpgfindlem1.5 . . . . 5 (๐œ‘ โ†’ ๐บ โˆˆ Abel)
543ad2ant1 1131 . . . 4 ((๐œ‘ โˆง ๐‘ฅ โˆˆ ๐ต โˆง (2 ยท ๐‘ฅ) โ‰  0 ) โ†’ ๐บ โˆˆ Abel)
6 ablsimpgfindlem1.6 . . . . 5 (๐œ‘ โ†’ ๐บ โˆˆ SimpGrp)
763ad2ant1 1131 . . . 4 ((๐œ‘ โˆง ๐‘ฅ โˆˆ ๐ต โˆง (2 ยท ๐‘ฅ) โ‰  0 ) โ†’ ๐บ โˆˆ SimpGrp)
86simpggrpd 20008 . . . . . 6 (๐œ‘ โ†’ ๐บ โˆˆ Grp)
983ad2ant1 1131 . . . . 5 ((๐œ‘ โˆง ๐‘ฅ โˆˆ ๐ต โˆง (2 ยท ๐‘ฅ) โ‰  0 ) โ†’ ๐บ โˆˆ Grp)
10 2z 12600 . . . . . 6 2 โˆˆ โ„ค
1110a1i 11 . . . . 5 ((๐œ‘ โˆง ๐‘ฅ โˆˆ ๐ต โˆง (2 ยท ๐‘ฅ) โ‰  0 ) โ†’ 2 โˆˆ โ„ค)
12 simp2 1135 . . . . 5 ((๐œ‘ โˆง ๐‘ฅ โˆˆ ๐ต โˆง (2 ยท ๐‘ฅ) โ‰  0 ) โ†’ ๐‘ฅ โˆˆ ๐ต)
131, 3, 9, 11, 12mulgcld 19014 . . . 4 ((๐œ‘ โˆง ๐‘ฅ โˆˆ ๐ต โˆง (2 ยท ๐‘ฅ) โ‰  0 ) โ†’ (2 ยท ๐‘ฅ) โˆˆ ๐ต)
14 simp3 1136 . . . . 5 ((๐œ‘ โˆง ๐‘ฅ โˆˆ ๐ต โˆง (2 ยท ๐‘ฅ) โ‰  0 ) โ†’ (2 ยท ๐‘ฅ) โ‰  0 )
1514neneqd 2943 . . . 4 ((๐œ‘ โˆง ๐‘ฅ โˆˆ ๐ต โˆง (2 ยท ๐‘ฅ) โ‰  0 ) โ†’ ยฌ (2 ยท ๐‘ฅ) = 0 )
161, 2, 3, 5, 7, 13, 15, 12ablsimpg1gend 20018 . . 3 ((๐œ‘ โˆง ๐‘ฅ โˆˆ ๐ต โˆง (2 ยท ๐‘ฅ) โ‰  0 ) โ†’ โˆƒ๐‘ฆ โˆˆ โ„ค ๐‘ฅ = (๐‘ฆ ยท (2 ยท ๐‘ฅ)))
17 simprr 769 . . . . . 6 (((๐œ‘ โˆง ๐‘ฅ โˆˆ ๐ต โˆง (2 ยท ๐‘ฅ) โ‰  0 ) โˆง (๐‘ฆ โˆˆ โ„ค โˆง ๐‘ฅ = (๐‘ฆ ยท (2 ยท ๐‘ฅ)))) โ†’ ๐‘ฅ = (๐‘ฆ ยท (2 ยท ๐‘ฅ)))
18 simpl2 1190 . . . . . . 7 (((๐œ‘ โˆง ๐‘ฅ โˆˆ ๐ต โˆง (2 ยท ๐‘ฅ) โ‰  0 ) โˆง (๐‘ฆ โˆˆ โ„ค โˆง ๐‘ฅ = (๐‘ฆ ยท (2 ยท ๐‘ฅ)))) โ†’ ๐‘ฅ โˆˆ ๐ต)
191, 3mulg1 18999 . . . . . . 7 (๐‘ฅ โˆˆ ๐ต โ†’ (1 ยท ๐‘ฅ) = ๐‘ฅ)
2018, 19syl 17 . . . . . 6 (((๐œ‘ โˆง ๐‘ฅ โˆˆ ๐ต โˆง (2 ยท ๐‘ฅ) โ‰  0 ) โˆง (๐‘ฆ โˆˆ โ„ค โˆง ๐‘ฅ = (๐‘ฆ ยท (2 ยท ๐‘ฅ)))) โ†’ (1 ยท ๐‘ฅ) = ๐‘ฅ)
219adantr 479 . . . . . . 7 (((๐œ‘ โˆง ๐‘ฅ โˆˆ ๐ต โˆง (2 ยท ๐‘ฅ) โ‰  0 ) โˆง (๐‘ฆ โˆˆ โ„ค โˆง ๐‘ฅ = (๐‘ฆ ยท (2 ยท ๐‘ฅ)))) โ†’ ๐บ โˆˆ Grp)
22 simprl 767 . . . . . . 7 (((๐œ‘ โˆง ๐‘ฅ โˆˆ ๐ต โˆง (2 ยท ๐‘ฅ) โ‰  0 ) โˆง (๐‘ฆ โˆˆ โ„ค โˆง ๐‘ฅ = (๐‘ฆ ยท (2 ยท ๐‘ฅ)))) โ†’ ๐‘ฆ โˆˆ โ„ค)
2310a1i 11 . . . . . . 7 (((๐œ‘ โˆง ๐‘ฅ โˆˆ ๐ต โˆง (2 ยท ๐‘ฅ) โ‰  0 ) โˆง (๐‘ฆ โˆˆ โ„ค โˆง ๐‘ฅ = (๐‘ฆ ยท (2 ยท ๐‘ฅ)))) โ†’ 2 โˆˆ โ„ค)
241, 3mulgassr 19030 . . . . . . 7 ((๐บ โˆˆ Grp โˆง (๐‘ฆ โˆˆ โ„ค โˆง 2 โˆˆ โ„ค โˆง ๐‘ฅ โˆˆ ๐ต)) โ†’ ((2 ยท ๐‘ฆ) ยท ๐‘ฅ) = (๐‘ฆ ยท (2 ยท ๐‘ฅ)))
2521, 22, 23, 18, 24syl13anc 1370 . . . . . 6 (((๐œ‘ โˆง ๐‘ฅ โˆˆ ๐ต โˆง (2 ยท ๐‘ฅ) โ‰  0 ) โˆง (๐‘ฆ โˆˆ โ„ค โˆง ๐‘ฅ = (๐‘ฆ ยท (2 ยท ๐‘ฅ)))) โ†’ ((2 ยท ๐‘ฆ) ยท ๐‘ฅ) = (๐‘ฆ ยท (2 ยท ๐‘ฅ)))
2617, 20, 253eqtr4rd 2781 . . . . 5 (((๐œ‘ โˆง ๐‘ฅ โˆˆ ๐ต โˆง (2 ยท ๐‘ฅ) โ‰  0 ) โˆง (๐‘ฆ โˆˆ โ„ค โˆง ๐‘ฅ = (๐‘ฆ ยท (2 ยท ๐‘ฅ)))) โ†’ ((2 ยท ๐‘ฆ) ยท ๐‘ฅ) = (1 ยท ๐‘ฅ))
2723, 22zmulcld 12678 . . . . . 6 (((๐œ‘ โˆง ๐‘ฅ โˆˆ ๐ต โˆง (2 ยท ๐‘ฅ) โ‰  0 ) โˆง (๐‘ฆ โˆˆ โ„ค โˆง ๐‘ฅ = (๐‘ฆ ยท (2 ยท ๐‘ฅ)))) โ†’ (2 ยท ๐‘ฆ) โˆˆ โ„ค)
28 1zzd 12599 . . . . . 6 (((๐œ‘ โˆง ๐‘ฅ โˆˆ ๐ต โˆง (2 ยท ๐‘ฅ) โ‰  0 ) โˆง (๐‘ฆ โˆˆ โ„ค โˆง ๐‘ฅ = (๐‘ฆ ยท (2 ยท ๐‘ฅ)))) โ†’ 1 โˆˆ โ„ค)
29 ablsimpgfindlem1.4 . . . . . . 7 ๐‘‚ = (odโ€˜๐บ)
301, 29, 3, 2odcong 19460 . . . . . 6 ((๐บ โˆˆ Grp โˆง ๐‘ฅ โˆˆ ๐ต โˆง ((2 ยท ๐‘ฆ) โˆˆ โ„ค โˆง 1 โˆˆ โ„ค)) โ†’ ((๐‘‚โ€˜๐‘ฅ) โˆฅ ((2 ยท ๐‘ฆ) โˆ’ 1) โ†” ((2 ยท ๐‘ฆ) ยท ๐‘ฅ) = (1 ยท ๐‘ฅ)))
3121, 18, 27, 28, 30syl112anc 1372 . . . . 5 (((๐œ‘ โˆง ๐‘ฅ โˆˆ ๐ต โˆง (2 ยท ๐‘ฅ) โ‰  0 ) โˆง (๐‘ฆ โˆˆ โ„ค โˆง ๐‘ฅ = (๐‘ฆ ยท (2 ยท ๐‘ฅ)))) โ†’ ((๐‘‚โ€˜๐‘ฅ) โˆฅ ((2 ยท ๐‘ฆ) โˆ’ 1) โ†” ((2 ยท ๐‘ฆ) ยท ๐‘ฅ) = (1 ยท ๐‘ฅ)))
3226, 31mpbird 256 . . . 4 (((๐œ‘ โˆง ๐‘ฅ โˆˆ ๐ต โˆง (2 ยท ๐‘ฅ) โ‰  0 ) โˆง (๐‘ฆ โˆˆ โ„ค โˆง ๐‘ฅ = (๐‘ฆ ยท (2 ยท ๐‘ฅ)))) โ†’ (๐‘‚โ€˜๐‘ฅ) โˆฅ ((2 ยท ๐‘ฆ) โˆ’ 1))
33 0zd 12576 . . . . . 6 (((๐œ‘ โˆง ๐‘ฅ โˆˆ ๐ต โˆง (2 ยท ๐‘ฅ) โ‰  0 ) โˆง (๐‘ฆ โˆˆ โ„ค โˆง ๐‘ฅ = (๐‘ฆ ยท (2 ยท ๐‘ฅ)))) โ†’ 0 โˆˆ โ„ค)
34 zneo 12651 . . . . . . . . 9 ((๐‘ฆ โˆˆ โ„ค โˆง 0 โˆˆ โ„ค) โ†’ (2 ยท ๐‘ฆ) โ‰  ((2 ยท 0) + 1))
35 2t0e0 12387 . . . . . . . . . . . 12 (2 ยท 0) = 0
3635oveq1i 7423 . . . . . . . . . . 11 ((2 ยท 0) + 1) = (0 + 1)
37 0p1e1 12340 . . . . . . . . . . 11 (0 + 1) = 1
3836, 37eqtri 2758 . . . . . . . . . 10 ((2 ยท 0) + 1) = 1
3938a1i 11 . . . . . . . . 9 ((๐‘ฆ โˆˆ โ„ค โˆง 0 โˆˆ โ„ค) โ†’ ((2 ยท 0) + 1) = 1)
4034, 39neeqtrd 3008 . . . . . . . 8 ((๐‘ฆ โˆˆ โ„ค โˆง 0 โˆˆ โ„ค) โ†’ (2 ยท ๐‘ฆ) โ‰  1)
41 oveq1 7420 . . . . . . . . . . . . 13 (((2 ยท ๐‘ฆ) โˆ’ 1) = 0 โ†’ (((2 ยท ๐‘ฆ) โˆ’ 1) + 1) = (0 + 1))
4241, 37eqtr2di 2787 . . . . . . . . . . . 12 (((2 ยท ๐‘ฆ) โˆ’ 1) = 0 โ†’ 1 = (((2 ยท ๐‘ฆ) โˆ’ 1) + 1))
4342adantl 480 . . . . . . . . . . 11 ((๐‘ฆ โˆˆ โ„ค โˆง ((2 ยท ๐‘ฆ) โˆ’ 1) = 0) โ†’ 1 = (((2 ยท ๐‘ฆ) โˆ’ 1) + 1))
44 2cnd 12296 . . . . . . . . . . . . 13 (๐‘ฆ โˆˆ โ„ค โ†’ 2 โˆˆ โ„‚)
45 zcn 12569 . . . . . . . . . . . . 13 (๐‘ฆ โˆˆ โ„ค โ†’ ๐‘ฆ โˆˆ โ„‚)
4644, 45mulcld 11240 . . . . . . . . . . . 12 (๐‘ฆ โˆˆ โ„ค โ†’ (2 ยท ๐‘ฆ) โˆˆ โ„‚)
47 1cnd 11215 . . . . . . . . . . . 12 (((2 ยท ๐‘ฆ) โˆ’ 1) = 0 โ†’ 1 โˆˆ โ„‚)
48 npcan 11475 . . . . . . . . . . . 12 (((2 ยท ๐‘ฆ) โˆˆ โ„‚ โˆง 1 โˆˆ โ„‚) โ†’ (((2 ยท ๐‘ฆ) โˆ’ 1) + 1) = (2 ยท ๐‘ฆ))
4946, 47, 48syl2an 594 . . . . . . . . . . 11 ((๐‘ฆ โˆˆ โ„ค โˆง ((2 ยท ๐‘ฆ) โˆ’ 1) = 0) โ†’ (((2 ยท ๐‘ฆ) โˆ’ 1) + 1) = (2 ยท ๐‘ฆ))
5043, 49eqtr2d 2771 . . . . . . . . . 10 ((๐‘ฆ โˆˆ โ„ค โˆง ((2 ยท ๐‘ฆ) โˆ’ 1) = 0) โ†’ (2 ยท ๐‘ฆ) = 1)
5150ex 411 . . . . . . . . 9 (๐‘ฆ โˆˆ โ„ค โ†’ (((2 ยท ๐‘ฆ) โˆ’ 1) = 0 โ†’ (2 ยท ๐‘ฆ) = 1))
5251necon3ad 2951 . . . . . . . 8 (๐‘ฆ โˆˆ โ„ค โ†’ ((2 ยท ๐‘ฆ) โ‰  1 โ†’ ยฌ ((2 ยท ๐‘ฆ) โˆ’ 1) = 0))
5340, 52syl5 34 . . . . . . 7 (๐‘ฆ โˆˆ โ„ค โ†’ ((๐‘ฆ โˆˆ โ„ค โˆง 0 โˆˆ โ„ค) โ†’ ยฌ ((2 ยท ๐‘ฆ) โˆ’ 1) = 0))
5453anabsi5 665 . . . . . 6 ((๐‘ฆ โˆˆ โ„ค โˆง 0 โˆˆ โ„ค) โ†’ ยฌ ((2 ยท ๐‘ฆ) โˆ’ 1) = 0)
5522, 33, 54syl2anc 582 . . . . 5 (((๐œ‘ โˆง ๐‘ฅ โˆˆ ๐ต โˆง (2 ยท ๐‘ฅ) โ‰  0 ) โˆง (๐‘ฆ โˆˆ โ„ค โˆง ๐‘ฅ = (๐‘ฆ ยท (2 ยท ๐‘ฅ)))) โ†’ ยฌ ((2 ยท ๐‘ฆ) โˆ’ 1) = 0)
5627, 28zsubcld 12677 . . . . . 6 (((๐œ‘ โˆง ๐‘ฅ โˆˆ ๐ต โˆง (2 ยท ๐‘ฅ) โ‰  0 ) โˆง (๐‘ฆ โˆˆ โ„ค โˆง ๐‘ฅ = (๐‘ฆ ยท (2 ยท ๐‘ฅ)))) โ†’ ((2 ยท ๐‘ฆ) โˆ’ 1) โˆˆ โ„ค)
57 0dvds 16226 . . . . . 6 (((2 ยท ๐‘ฆ) โˆ’ 1) โˆˆ โ„ค โ†’ (0 โˆฅ ((2 ยท ๐‘ฆ) โˆ’ 1) โ†” ((2 ยท ๐‘ฆ) โˆ’ 1) = 0))
5856, 57syl 17 . . . . 5 (((๐œ‘ โˆง ๐‘ฅ โˆˆ ๐ต โˆง (2 ยท ๐‘ฅ) โ‰  0 ) โˆง (๐‘ฆ โˆˆ โ„ค โˆง ๐‘ฅ = (๐‘ฆ ยท (2 ยท ๐‘ฅ)))) โ†’ (0 โˆฅ ((2 ยท ๐‘ฆ) โˆ’ 1) โ†” ((2 ยท ๐‘ฆ) โˆ’ 1) = 0))
5955, 58mtbird 324 . . . 4 (((๐œ‘ โˆง ๐‘ฅ โˆˆ ๐ต โˆง (2 ยท ๐‘ฅ) โ‰  0 ) โˆง (๐‘ฆ โˆˆ โ„ค โˆง ๐‘ฅ = (๐‘ฆ ยท (2 ยท ๐‘ฅ)))) โ†’ ยฌ 0 โˆฅ ((2 ยท ๐‘ฆ) โˆ’ 1))
60 nbrne2 5169 . . . 4 (((๐‘‚โ€˜๐‘ฅ) โˆฅ ((2 ยท ๐‘ฆ) โˆ’ 1) โˆง ยฌ 0 โˆฅ ((2 ยท ๐‘ฆ) โˆ’ 1)) โ†’ (๐‘‚โ€˜๐‘ฅ) โ‰  0)
6132, 59, 60syl2anc 582 . . 3 (((๐œ‘ โˆง ๐‘ฅ โˆˆ ๐ต โˆง (2 ยท ๐‘ฅ) โ‰  0 ) โˆง (๐‘ฆ โˆˆ โ„ค โˆง ๐‘ฅ = (๐‘ฆ ยท (2 ยท ๐‘ฅ)))) โ†’ (๐‘‚โ€˜๐‘ฅ) โ‰  0)
6216, 61rexlimddv 3159 . 2 ((๐œ‘ โˆง ๐‘ฅ โˆˆ ๐ต โˆง (2 ยท ๐‘ฅ) โ‰  0 ) โ†’ (๐‘‚โ€˜๐‘ฅ) โ‰  0)
63623expa 1116 1 (((๐œ‘ โˆง ๐‘ฅ โˆˆ ๐ต) โˆง (2 ยท ๐‘ฅ) โ‰  0 ) โ†’ (๐‘‚โ€˜๐‘ฅ) โ‰  0)
Colors of variables: wff setvar class
Syntax hints:  ยฌ wn 3   โ†’ wi 4   โ†” wb 205   โˆง wa 394   โˆง w3a 1085   = wceq 1539   โˆˆ wcel 2104   โ‰  wne 2938   class class class wbr 5149  โ€˜cfv 6544  (class class class)co 7413  โ„‚cc 11112  0cc0 11114  1c1 11115   + caddc 11117   ยท cmul 11119   โˆ’ cmin 11450  2c2 12273  โ„คcz 12564   โˆฅ cdvds 16203  Basecbs 17150  0gc0g 17391  Grpcgrp 18857  .gcmg 18988  odcod 19435  Abelcabl 19692  SimpGrpcsimpg 20003
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 1911  ax-6 1969  ax-7 2009  ax-8 2106  ax-9 2114  ax-10 2135  ax-11 2152  ax-12 2169  ax-ext 2701  ax-sep 5300  ax-nul 5307  ax-pow 5364  ax-pr 5428  ax-un 7729  ax-cnex 11170  ax-resscn 11171  ax-1cn 11172  ax-icn 11173  ax-addcl 11174  ax-addrcl 11175  ax-mulcl 11176  ax-mulrcl 11177  ax-mulcom 11178  ax-addass 11179  ax-mulass 11180  ax-distr 11181  ax-i2m1 11182  ax-1ne0 11183  ax-1rid 11184  ax-rnegex 11185  ax-rrecex 11186  ax-cnre 11187  ax-pre-lttri 11188  ax-pre-lttrn 11189  ax-pre-ltadd 11190  ax-pre-mulgt0 11191  ax-pre-sup 11192
This theorem depends on definitions:  df-bi 206  df-an 395  df-or 844  df-3or 1086  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2532  df-eu 2561  df-clab 2708  df-cleq 2722  df-clel 2808  df-nfc 2883  df-ne 2939  df-nel 3045  df-ral 3060  df-rex 3069  df-rmo 3374  df-reu 3375  df-rab 3431  df-v 3474  df-sbc 3779  df-csb 3895  df-dif 3952  df-un 3954  df-in 3956  df-ss 3966  df-pss 3968  df-nul 4324  df-if 4530  df-pw 4605  df-sn 4630  df-pr 4632  df-op 4636  df-uni 4910  df-iun 5000  df-br 5150  df-opab 5212  df-mpt 5233  df-tr 5267  df-id 5575  df-eprel 5581  df-po 5589  df-so 5590  df-fr 5632  df-we 5634  df-xp 5683  df-rel 5684  df-cnv 5685  df-co 5686  df-dm 5687  df-rn 5688  df-res 5689  df-ima 5690  df-pred 6301  df-ord 6368  df-on 6369  df-lim 6370  df-suc 6371  df-iota 6496  df-fun 6546  df-fn 6547  df-f 6548  df-f1 6549  df-fo 6550  df-f1o 6551  df-fv 6552  df-riota 7369  df-ov 7416  df-oprab 7417  df-mpo 7418  df-om 7860  df-1st 7979  df-2nd 7980  df-frecs 8270  df-wrecs 8301  df-recs 8375  df-rdg 8414  df-1o 8470  df-2o 8471  df-er 8707  df-en 8944  df-dom 8945  df-sdom 8946  df-fin 8947  df-sup 9441  df-inf 9442  df-pnf 11256  df-mnf 11257  df-xr 11258  df-ltxr 11259  df-le 11260  df-sub 11452  df-neg 11453  df-div 11878  df-nn 12219  df-2 12281  df-3 12282  df-n0 12479  df-z 12565  df-uz 12829  df-rp 12981  df-fz 13491  df-fl 13763  df-mod 13841  df-seq 13973  df-exp 14034  df-cj 15052  df-re 15053  df-im 15054  df-sqrt 15188  df-abs 15189  df-dvds 16204  df-sets 17103  df-slot 17121  df-ndx 17133  df-base 17151  df-ress 17180  df-plusg 17216  df-0g 17393  df-mgm 18567  df-sgrp 18646  df-mnd 18662  df-submnd 18708  df-grp 18860  df-minusg 18861  df-sbg 18862  df-mulg 18989  df-subg 19041  df-nsg 19042  df-od 19439  df-cmn 19693  df-abl 19694  df-simpg 20004
This theorem is referenced by:  ablsimpgfind  20023
  Copyright terms: Public domain W3C validator