Theorem ssipeq

Description: The inner product on a subspace equals the inner product on the parent space. (Contributed by AV, 19-Oct-2021)

	Ref	Expression
Hypotheses	ssipeq.x	|- X = ( W |`s U )
	ssipeq.i	|- ., = ( .i ` W )
	ssipeq.p	|- P = ( .i ` X )
Assertion	ssipeq	|- ( U e. S -> P = ., )

Proof

Step	Hyp	Ref	Expression
1		ssipeq.x	|- X = ( W |`s U )
2		ssipeq.i	|- ., = ( .i ` W )
3		ssipeq.p	|- P = ( .i ` X )
4	1 2	ressip	|- ( U e. S -> ., = ( .i ` X ) )
5	3 4	eqtr4id	|- ( U e. S -> P = ., )