This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem cnsubmlem

Description: Lemma for nn0subm and friends. (Contributed by Mario Carneiro, 18-Jun-2015)

Ref Expression
Hypotheses cnsubglem.1 
|- ( x e. A -> x e. CC )
cnsubglem.2 
|- ( ( x e. A /\ y e. A ) -> ( x + y ) e. A )
cnsubmlem.3 
|- 0 e. A
Assertion cnsubmlem 
|- A e. ( SubMnd ` CCfld )

Proof

Step Hyp Ref Expression
1 cnsubglem.1 
 |-  ( x e. A -> x e. CC )
2 cnsubglem.2 
 |-  ( ( x e. A /\ y e. A ) -> ( x + y ) e. A )
3 cnsubmlem.3 
 |-  0 e. A
4 1 ssriv 
 |-  A C_ CC
5 2 rgen2 
 |-  A. x e. A A. y e. A ( x + y ) e. A
6 cnring 
 |-  CCfld e. Ring
7 ringmnd 
 |-  ( CCfld e. Ring -> CCfld e. Mnd )
8 cnfldbas 
 |-  CC = ( Base ` CCfld )
9 cnfld0 
 |-  0 = ( 0g ` CCfld )
10 cnfldadd 
 |-  + = ( +g ` CCfld )
11 8 9 10 issubm 
 |-  ( CCfld e. Mnd -> ( A e. ( SubMnd ` CCfld ) <-> ( A C_ CC /\ 0 e. A /\ A. x e. A A. y e. A ( x + y ) e. A ) ) )
12 6 7 11 mp2b 
 |-  ( A e. ( SubMnd ` CCfld ) <-> ( A C_ CC /\ 0 e. A /\ A. x e. A A. y e. A ( x + y ) e. A ) )
13 4 3 5 12 mpbir3an 
 |-  A e. ( SubMnd ` CCfld )