Metamath Proof Explorer

Theorem opsqrlem3

Description: Lemma for opsqri . (Contributed by NM, 22-Aug-2006) (New usage is discouraged.)

		Ref	Expression
	Hypotheses	opsqrlem2.1	\|- T e. HrmOp
		opsqrlem2.2	\|- S = ( x e. HrmOp , y e. HrmOp \|-> ( x +op ( ( 1 / 2 ) .op ( T -op ( x o. x ) ) ) ) )
		opsqrlem2.3	\|- F = seq 1 ( S , ( NN X. { 0hop } ) )
	Assertion	opsqrlem3	\|- ( ( G e. HrmOp /\ H e. HrmOp ) -> ( G S H ) = ( G +op ( ( 1 / 2 ) .op ( T -op ( G o. G ) ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		opsqrlem2.1	\|- T e. HrmOp
2		opsqrlem2.2	\|- S = ( x e. HrmOp , y e. HrmOp \|-> ( x +op ( ( 1 / 2 ) .op ( T -op ( x o. x ) ) ) ) )
3		opsqrlem2.3	\|- F = seq 1 ( S , ( NN X. { 0hop } ) )
4		id	\|- ( z = G -> z = G )
5	4 4	coeq12d	\|- ( z = G -> ( z o. z ) = ( G o. G ) )
6	5	oveq2d	\|- ( z = G -> ( T -op ( z o. z ) ) = ( T -op ( G o. G ) ) )
7	6	oveq2d	\|- ( z = G -> ( ( 1 / 2 ) .op ( T -op ( z o. z ) ) ) = ( ( 1 / 2 ) .op ( T -op ( G o. G ) ) ) )
8	4 7	oveq12d	\|- ( z = G -> ( z +op ( ( 1 / 2 ) .op ( T -op ( z o. z ) ) ) ) = ( G +op ( ( 1 / 2 ) .op ( T -op ( G o. G ) ) ) ) )
9		eqidd	\|- ( w = H -> ( G +op ( ( 1 / 2 ) .op ( T -op ( G o. G ) ) ) ) = ( G +op ( ( 1 / 2 ) .op ( T -op ( G o. G ) ) ) ) )
10		id	\|- ( x = z -> x = z )
11	10 10	coeq12d	\|- ( x = z -> ( x o. x ) = ( z o. z ) )
12	11	oveq2d	\|- ( x = z -> ( T -op ( x o. x ) ) = ( T -op ( z o. z ) ) )
13	12	oveq2d	\|- ( x = z -> ( ( 1 / 2 ) .op ( T -op ( x o. x ) ) ) = ( ( 1 / 2 ) .op ( T -op ( z o. z ) ) ) )
14	10 13	oveq12d	\|- ( x = z -> ( x +op ( ( 1 / 2 ) .op ( T -op ( x o. x ) ) ) ) = ( z +op ( ( 1 / 2 ) .op ( T -op ( z o. z ) ) ) ) )
15		eqidd	\|- ( y = w -> ( z +op ( ( 1 / 2 ) .op ( T -op ( z o. z ) ) ) ) = ( z +op ( ( 1 / 2 ) .op ( T -op ( z o. z ) ) ) ) )
16	14 15	cbvmpov	\|- ( x e. HrmOp , y e. HrmOp \|-> ( x +op ( ( 1 / 2 ) .op ( T -op ( x o. x ) ) ) ) ) = ( z e. HrmOp , w e. HrmOp \|-> ( z +op ( ( 1 / 2 ) .op ( T -op ( z o. z ) ) ) ) )
17	2 16	eqtri	\|- S = ( z e. HrmOp , w e. HrmOp \|-> ( z +op ( ( 1 / 2 ) .op ( T -op ( z o. z ) ) ) ) )
18		ovex	\|- ( G +op ( ( 1 / 2 ) .op ( T -op ( G o. G ) ) ) ) e. _V
19	8 9 17 18	ovmpo	\|- ( ( G e. HrmOp /\ H e. HrmOp ) -> ( G S H ) = ( G +op ( ( 1 / 2 ) .op ( T -op ( G o. G ) ) ) ) )