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 )