Theorem ellkr2

Description: Membership in the kernel of a functional. (Contributed by NM, 12-Jan-2015)

	Ref	Expression
Hypotheses	lkrfval2.v	|- V = ( Base ` W )
	lkrfval2.d	|- D = ( Scalar ` W )
	lkrfval2.o	|- .0. = ( 0g ` D )
	lkrfval2.f	|- F = ( LFnl ` W )
	lkrfval2.k	|- K = ( LKer ` W )
	ellkr2.w	|- ( ph -> W e. Y )
	ellkr2.g	|- ( ph -> G e. F )
	ellkr2.x	|- ( ph -> X e. V )
Assertion	ellkr2	|- ( ph -> ( X e. ( K ` G ) <-> ( G ` X ) = .0. ) )

Proof

Step	Hyp	Ref	Expression
1		lkrfval2.v	|- V = ( Base ` W )
2		lkrfval2.d	|- D = ( Scalar ` W )
3		lkrfval2.o	|- .0. = ( 0g ` D )
4		lkrfval2.f	|- F = ( LFnl ` W )
5		lkrfval2.k	|- K = ( LKer ` W )
6		ellkr2.w	|- ( ph -> W e. Y )
7		ellkr2.g	|- ( ph -> G e. F )
8		ellkr2.x	|- ( ph -> X e. V )
9	1 2 3 4 5	ellkr	|- ( ( W e. Y /\ G e. F ) -> ( X e. ( K ` G ) <-> ( X e. V /\ ( G ` X ) = .0. ) ) )
10	6 7 9	syl2anc	|- ( ph -> ( X e. ( K ` G ) <-> ( X e. V /\ ( G ` X ) = .0. ) ) )
11	8	biantrurd	|- ( ph -> ( ( G ` X ) = .0. <-> ( X e. V /\ ( G ` X ) = .0. ) ) )
12	10 11	bitr4d	|- ( ph -> ( X e. ( K ` G ) <-> ( G ` X ) = .0. ) )