Theorem ipasslem3

Description: Lemma for ipassi . Show the inner product associative law for all integers. (Contributed by NM, 27-Apr-2007) (New usage is discouraged.)

	Ref	Expression
Hypotheses	ip1i.1	|- X = ( BaseSet ` U )
	ip1i.2	|- G = ( +v ` U )
	ip1i.4	|- S = ( .sOLD ` U )
	ip1i.7	|- P = ( .iOLD ` U )
	ip1i.9	|- U e. CPreHilOLD
	ipasslem1.b	|- B e. X
Assertion	ipasslem3	|- ( ( N e. ZZ /\ A e. X ) -> ( ( N S A ) P B ) = ( N x. ( A P B ) ) )

Proof

Step	Hyp	Ref	Expression
1		ip1i.1	|- X = ( BaseSet ` U )
2		ip1i.2	|- G = ( +v ` U )
3		ip1i.4	|- S = ( .sOLD ` U )
4		ip1i.7	|- P = ( .iOLD ` U )
5		ip1i.9	|- U e. CPreHilOLD
6		ipasslem1.b	|- B e. X
7		elznn0nn	|- ( N e. ZZ <-> ( N e. NN0 \/ ( N e. RR /\ -u N e. NN ) ) )
8	1 2 3 4 5 6	ipasslem1	|- ( ( N e. NN0 /\ A e. X ) -> ( ( N S A ) P B ) = ( N x. ( A P B ) ) )
9		nnnn0	|- ( -u N e. NN -> -u N e. NN0 )
10	1 2 3 4 5 6	ipasslem2	|- ( ( -u N e. NN0 /\ A e. X ) -> ( ( -u -u N S A ) P B ) = ( -u -u N x. ( A P B ) ) )
11	9 10	sylan	|- ( ( -u N e. NN /\ A e. X ) -> ( ( -u -u N S A ) P B ) = ( -u -u N x. ( A P B ) ) )
12	11	adantll	|- ( ( ( N e. RR /\ -u N e. NN ) /\ A e. X ) -> ( ( -u -u N S A ) P B ) = ( -u -u N x. ( A P B ) ) )
13		recn	|- ( N e. RR -> N e. CC )
14	13	negnegd	|- ( N e. RR -> -u -u N = N )
15	14	oveq1d	|- ( N e. RR -> ( -u -u N S A ) = ( N S A ) )
16	15	oveq1d	|- ( N e. RR -> ( ( -u -u N S A ) P B ) = ( ( N S A ) P B ) )
17	16	ad2antrr	|- ( ( ( N e. RR /\ -u N e. NN ) /\ A e. X ) -> ( ( -u -u N S A ) P B ) = ( ( N S A ) P B ) )
18	14	oveq1d	|- ( N e. RR -> ( -u -u N x. ( A P B ) ) = ( N x. ( A P B ) ) )
19	18	ad2antrr	|- ( ( ( N e. RR /\ -u N e. NN ) /\ A e. X ) -> ( -u -u N x. ( A P B ) ) = ( N x. ( A P B ) ) )
20	12 17 19	3eqtr3d	|- ( ( ( N e. RR /\ -u N e. NN ) /\ A e. X ) -> ( ( N S A ) P B ) = ( N x. ( A P B ) ) )
21	8 20	jaoian	|- ( ( ( N e. NN0 \/ ( N e. RR /\ -u N e. NN ) ) /\ A e. X ) -> ( ( N S A ) P B ) = ( N x. ( A P B ) ) )
22	7 21	sylanb	|- ( ( N e. ZZ /\ A e. X ) -> ( ( N S A ) P B ) = ( N x. ( A P B ) ) )