Metamath Proof Explorer


Theorem cycsubg

Description: The cyclic group generated by A is the smallest subgroup containing A . (Contributed by Mario Carneiro, 13-Jan-2015)

Ref Expression
Hypotheses cycsubg.x โŠข ๐‘‹ = ( Base โ€˜ ๐บ )
cycsubg.t โŠข ยท = ( .g โ€˜ ๐บ )
cycsubg.f โŠข ๐น = ( ๐‘ฅ โˆˆ โ„ค โ†ฆ ( ๐‘ฅ ยท ๐ด ) )
Assertion cycsubg ( ( ๐บ โˆˆ Grp โˆง ๐ด โˆˆ ๐‘‹ ) โ†’ ran ๐น = โˆฉ { ๐‘  โˆˆ ( SubGrp โ€˜ ๐บ ) โˆฃ ๐ด โˆˆ ๐‘  } )

Proof

Step Hyp Ref Expression
1 cycsubg.x โŠข ๐‘‹ = ( Base โ€˜ ๐บ )
2 cycsubg.t โŠข ยท = ( .g โ€˜ ๐บ )
3 cycsubg.f โŠข ๐น = ( ๐‘ฅ โˆˆ โ„ค โ†ฆ ( ๐‘ฅ ยท ๐ด ) )
4 ssintab โŠข ( ran ๐น โŠ† โˆฉ { ๐‘  โˆฃ ( ๐‘  โˆˆ ( SubGrp โ€˜ ๐บ ) โˆง ๐ด โˆˆ ๐‘  ) } โ†” โˆ€ ๐‘  ( ( ๐‘  โˆˆ ( SubGrp โ€˜ ๐บ ) โˆง ๐ด โˆˆ ๐‘  ) โ†’ ran ๐น โŠ† ๐‘  ) )
5 1 2 3 cycsubgss โŠข ( ( ๐‘  โˆˆ ( SubGrp โ€˜ ๐บ ) โˆง ๐ด โˆˆ ๐‘  ) โ†’ ran ๐น โŠ† ๐‘  )
6 4 5 mpgbir โŠข ran ๐น โŠ† โˆฉ { ๐‘  โˆฃ ( ๐‘  โˆˆ ( SubGrp โ€˜ ๐บ ) โˆง ๐ด โˆˆ ๐‘  ) }
7 df-rab โŠข { ๐‘  โˆˆ ( SubGrp โ€˜ ๐บ ) โˆฃ ๐ด โˆˆ ๐‘  } = { ๐‘  โˆฃ ( ๐‘  โˆˆ ( SubGrp โ€˜ ๐บ ) โˆง ๐ด โˆˆ ๐‘  ) }
8 7 inteqi โŠข โˆฉ { ๐‘  โˆˆ ( SubGrp โ€˜ ๐บ ) โˆฃ ๐ด โˆˆ ๐‘  } = โˆฉ { ๐‘  โˆฃ ( ๐‘  โˆˆ ( SubGrp โ€˜ ๐บ ) โˆง ๐ด โˆˆ ๐‘  ) }
9 6 8 sseqtrri โŠข ran ๐น โŠ† โˆฉ { ๐‘  โˆˆ ( SubGrp โ€˜ ๐บ ) โˆฃ ๐ด โˆˆ ๐‘  }
10 9 a1i โŠข ( ( ๐บ โˆˆ Grp โˆง ๐ด โˆˆ ๐‘‹ ) โ†’ ran ๐น โŠ† โˆฉ { ๐‘  โˆˆ ( SubGrp โ€˜ ๐บ ) โˆฃ ๐ด โˆˆ ๐‘  } )
11 1 2 3 cycsubgcl โŠข ( ( ๐บ โˆˆ Grp โˆง ๐ด โˆˆ ๐‘‹ ) โ†’ ( ran ๐น โˆˆ ( SubGrp โ€˜ ๐บ ) โˆง ๐ด โˆˆ ran ๐น ) )
12 eleq2 โŠข ( ๐‘  = ran ๐น โ†’ ( ๐ด โˆˆ ๐‘  โ†” ๐ด โˆˆ ran ๐น ) )
13 12 elrab โŠข ( ran ๐น โˆˆ { ๐‘  โˆˆ ( SubGrp โ€˜ ๐บ ) โˆฃ ๐ด โˆˆ ๐‘  } โ†” ( ran ๐น โˆˆ ( SubGrp โ€˜ ๐บ ) โˆง ๐ด โˆˆ ran ๐น ) )
14 11 13 sylibr โŠข ( ( ๐บ โˆˆ Grp โˆง ๐ด โˆˆ ๐‘‹ ) โ†’ ran ๐น โˆˆ { ๐‘  โˆˆ ( SubGrp โ€˜ ๐บ ) โˆฃ ๐ด โˆˆ ๐‘  } )
15 intss1 โŠข ( ran ๐น โˆˆ { ๐‘  โˆˆ ( SubGrp โ€˜ ๐บ ) โˆฃ ๐ด โˆˆ ๐‘  } โ†’ โˆฉ { ๐‘  โˆˆ ( SubGrp โ€˜ ๐บ ) โˆฃ ๐ด โˆˆ ๐‘  } โŠ† ran ๐น )
16 14 15 syl โŠข ( ( ๐บ โˆˆ Grp โˆง ๐ด โˆˆ ๐‘‹ ) โ†’ โˆฉ { ๐‘  โˆˆ ( SubGrp โ€˜ ๐บ ) โˆฃ ๐ด โˆˆ ๐‘  } โŠ† ran ๐น )
17 10 16 eqssd โŠข ( ( ๐บ โˆˆ Grp โˆง ๐ด โˆˆ ๐‘‹ ) โ†’ ran ๐น = โˆฉ { ๐‘  โˆˆ ( SubGrp โ€˜ ๐บ ) โˆฃ ๐ด โˆˆ ๐‘  } )