mulgnn0subcl

Description: Closure of the group multiple (exponentiation) operation in a submonoid. (Contributed by Mario Carneiro, 10-Jan-2015)

Step	Hyp	Ref	Expression
1		mulgnnsubcl.b	\|- B = ( Base ` G )
2		mulgnnsubcl.t	\|- .x. = ( .g ` G )
3		mulgnnsubcl.p	\|- .+ = ( +g ` G )
4		mulgnnsubcl.g	\|- ( ph -> G e. V )
5		mulgnnsubcl.s	\|- ( ph -> S C_ B )
6		mulgnnsubcl.c	\|- ( ( ph /\ x e. S /\ y e. S ) -> ( x .+ y ) e. S )
7		mulgnn0subcl.z	\|- .0. = ( 0g ` G )
8		mulgnn0subcl.c	\|- ( ph -> .0. e. S )
9	1 2 3 4 5 6	mulgnnsubcl	\|- ( ( ph /\ N e. NN /\ X e. S ) -> ( N .x. X ) e. S )
10	9	3expa	\|- ( ( ( ph /\ N e. NN ) /\ X e. S ) -> ( N .x. X ) e. S )
11	10	an32s	\|- ( ( ( ph /\ X e. S ) /\ N e. NN ) -> ( N .x. X ) e. S )
12	11	3adantl2	\|- ( ( ( ph /\ N e. NN0 /\ X e. S ) /\ N e. NN ) -> ( N .x. X ) e. S )
13		oveq1	\|- ( N = 0 -> ( N .x. X ) = ( 0 .x. X ) )
14	5	3ad2ant1	\|- ( ( ph /\ N e. NN0 /\ X e. S ) -> S C_ B )
15		simp3	\|- ( ( ph /\ N e. NN0 /\ X e. S ) -> X e. S )
16	14 15	sseldd	\|- ( ( ph /\ N e. NN0 /\ X e. S ) -> X e. B )
17	1 7 2	mulg0	\|- ( X e. B -> ( 0 .x. X ) = .0. )
18	16 17	syl	\|- ( ( ph /\ N e. NN0 /\ X e. S ) -> ( 0 .x. X ) = .0. )
19	13 18	sylan9eqr	\|- ( ( ( ph /\ N e. NN0 /\ X e. S ) /\ N = 0 ) -> ( N .x. X ) = .0. )
20	8	3ad2ant1	\|- ( ( ph /\ N e. NN0 /\ X e. S ) -> .0. e. S )
21	20	adantr	\|- ( ( ( ph /\ N e. NN0 /\ X e. S ) /\ N = 0 ) -> .0. e. S )
22	19 21	eqeltrd	\|- ( ( ( ph /\ N e. NN0 /\ X e. S ) /\ N = 0 ) -> ( N .x. X ) e. S )
23		simp2	\|- ( ( ph /\ N e. NN0 /\ X e. S ) -> N e. NN0 )
24		elnn0	\|- ( N e. NN0 <-> ( N e. NN \/ N = 0 ) )
25	23 24	sylib	\|- ( ( ph /\ N e. NN0 /\ X e. S ) -> ( N e. NN \/ N = 0 ) )
26	12 22 25	mpjaodan	\|- ( ( ph /\ N e. NN0 /\ X e. S ) -> ( N .x. X ) e. S )

Metamath Proof Explorer