Theorem ofcs1

Description: Letterwise operations on a single letter word. (Contributed by Thierry Arnoux, 7-Oct-2018)

	Ref	Expression
Assertion	ofcs1	|- ( ( A e. S /\ B e. T ) -> ( <" A "> oFC R B ) = <" ( A R B ) "> )

Proof

Step	Hyp	Ref	Expression
1		snex	|- { 0 } e. _V
2	1	a1i	|- ( ( A e. S /\ B e. T ) -> { 0 } e. _V )
3		simpr	|- ( ( A e. S /\ B e. T ) -> B e. T )
4		simpll	|- ( ( ( A e. S /\ B e. T ) /\ i e. { 0 } ) -> A e. S )
5		s1val	|- ( A e. S -> <" A "> = { <. 0 , A >. } )
6		0nn0	|- 0 e. NN0
7		fmptsn	|- ( ( 0 e. NN0 /\ A e. S ) -> { <. 0 , A >. } = ( i e. { 0 } |-> A ) )
8	6 7	mpan	|- ( A e. S -> { <. 0 , A >. } = ( i e. { 0 } |-> A ) )
9	5 8	eqtrd	|- ( A e. S -> <" A "> = ( i e. { 0 } |-> A ) )
10	9	adantr	|- ( ( A e. S /\ B e. T ) -> <" A "> = ( i e. { 0 } |-> A ) )
11	2 3 4 10	ofcfval2	|- ( ( A e. S /\ B e. T ) -> ( <" A "> oFC R B ) = ( i e. { 0 } |-> ( A R B ) ) )
12		ovex	|- ( A R B ) e. _V
13		s1val	|- ( ( A R B ) e. _V -> <" ( A R B ) "> = { <. 0 , ( A R B ) >. } )
14	12 13	ax-mp	|- <" ( A R B ) "> = { <. 0 , ( A R B ) >. }
15		fmptsn	|- ( ( 0 e. NN0 /\ ( A R B ) e. _V ) -> { <. 0 , ( A R B ) >. } = ( i e. { 0 } |-> ( A R B ) ) )
16	6 12 15	mp2an	|- { <. 0 , ( A R B ) >. } = ( i e. { 0 } |-> ( A R B ) )
17	14 16	eqtri	|- <" ( A R B ) "> = ( i e. { 0 } |-> ( A R B ) )
18	11 17	eqtr4di	|- ( ( A e. S /\ B e. T ) -> ( <" A "> oFC R B ) = <" ( A R B ) "> )