let K be Field; :: thesis: for F being K -monomorphic Field
for f being Monomorphism of K,F st K,F are_disjoint holds
emb_iso f is multiplicative
let F be K -monomorphic Field; :: thesis: for f being Monomorphism of K,F st K,F are_disjoint holds
emb_iso f is multiplicative
let f be Monomorphism of K,F; :: thesis: ( K,F are_disjoint implies emb_iso f is multiplicative )
assume AS: K,F are_disjoint ; :: thesis: emb_iso f is multiplicative
set g = emb_iso f;
set R = embField f;

now :: thesis: for a, b being Element of (embField f) holds (emb_iso f) . (a * b) = ((emb_iso f) . a) * ((emb_iso f) . b)

let a, b be Element of (embField f); :: thesis: (emb_iso f) . (b₁ * b₂) = ((emb_iso f) . b₁) * ((emb_iso f) . b₂)
reconsider x = a, y = b as Element of carr f by defemb;

per cases ( ( x in [#] K & y in [#] K ) or x = 0. K or y = 0. K or ( x in [#] K & x <> 0. K & not y in [#] K ) or ( y in [#] K & y <> 0. K & not x in [#] K ) or ( not x in [#] K & not y in [#] K & the multF of F . (x,y) in rng f ) or ( not x in [#] K & not y in [#] K & not the multF of F . (x,y) in rng f ) ) ;

suppose A1: ( x in [#] K & y in [#] K ) ; :: thesis: (emb_iso f) . (b₁ * b₂) = ((emb_iso f) . b₁) * ((emb_iso f) . b₂)

then reconsider a1 = a, b1 = b as Element of K ;
B: a * b = a1 * b1 by Lm11;
( a in K & b in K ) by A1;
then C: ( (emb_iso f) . a = f . a & (emb_iso f) . b = f . b ) by defiso;
a * b in K by B;
hence (emb_iso f) . (a * b) = f . (a * b) by defiso
.= ((emb_iso f) . a) * ((emb_iso f) . b) by C, B, GROUP_6:def 6 ;
:: thesis: verum

end;

suppose A2: ( x = 0. K or y = 0. K ) ; :: thesis: (emb_iso f) . (b₁ * b₂) = ((emb_iso f) . b₁) * ((emb_iso f) . b₂)

B: a * b = (multemb f) . (x,y) by defemb
.= multemb (f,x,y) by defmult
.= 0. K by A2, defmultf ;
X: 0. K in K ;

per cases ( x = 0. K or y = 0. K ) by A2;

suppose x = 0. K ; :: thesis: (emb_iso f) . (b₁ * b₂) = ((emb_iso f) . b₁) * ((emb_iso f) . b₂)

then C: (emb_iso f) . a = f . (0. K) by X, defiso
.= 0. F by RING_2:6 ;
thus (emb_iso f) . (a * b) = f . (0. K) by B, X, defiso
.= ((emb_iso f) . a) * ((emb_iso f) . b) by C, RING_2:6 ; :: thesis: verum

end;

suppose y = 0. K ; :: thesis: (emb_iso f) . (b₁ * b₂) = ((emb_iso f) . b₁) * ((emb_iso f) . b₂)

then C: (emb_iso f) . b = f . (0. K) by X, defiso
.= 0. F by RING_2:6 ;
thus (emb_iso f) . (a * b) = f . (0. K) by B, X, defiso
.= ((emb_iso f) . a) * ((emb_iso f) . b) by C, RING_2:6 ; :: thesis: verum

end;

end;

end;

suppose A: ( x in [#] K & x <> 0. K & not y in [#] K ) ; :: thesis: (emb_iso f) . (b₁ * b₂) = ((emb_iso f) . b₁) * ((emb_iso f) . b₂)

then reconsider a1 = a as Element of K ;
reconsider b1 = b as Element of F by A, Lm1;
reconsider fa = f . a1 as Element of F ;
B: a * b = fa * b1 by AS, A, Lm10;
( a in K & not b in K ) by A;
then C: ( (emb_iso f) . a = f . a & (emb_iso f) . b = b ) by defiso;
not a * b in K by AS, A, Lm10;
hence (emb_iso f) . (a * b) = ((emb_iso f) . a) * ((emb_iso f) . b) by B, C, defiso; :: thesis: verum

end;

suppose A: ( y in [#] K & y <> 0. K & not x in [#] K ) ; :: thesis: (emb_iso f) . (b₁ * b₂) = ((emb_iso f) . b₁) * ((emb_iso f) . b₂)

then reconsider b1 = b as Element of K ;
reconsider a1 = a as Element of F by A, Lm1;
reconsider fb = f . b1 as Element of F ;
B: a * b = a1 * fb by AS, A, Lm10;
( b in K & not a in K ) by A;
then C: ( (emb_iso f) . a = a & (emb_iso f) . b = f . b ) by defiso;
not a * b in K by AS, A, Lm10;
hence (emb_iso f) . (a * b) = ((emb_iso f) . a) * ((emb_iso f) . b) by B, C, defiso; :: thesis: verum

end;

suppose A: ( not x in [#] K & not y in [#] K & the multF of F . (x,y) in rng f ) ; :: thesis: (emb_iso f) . (b₁ * b₂) = ((emb_iso f) . b₁) * ((emb_iso f) . b₂)

then reconsider a1 = a, b1 = b as Element of F by Lm1;
C: a * b = (f ") . (a1 * b1) by A, Lm13;
( not a in K & not b in K ) by A;
then D: ( (emb_iso f) . a = a & (emb_iso f) . b = b ) by defiso;
a1 * b1 in dom (f ") by A, FUNCT_1:33;
then (f ") . (a1 * b1) in rng (f ") by FUNCT_1:3;
then (f ") . (a1 * b1) in K ;
hence (emb_iso f) . (a * b) = f . ((f ") . (a1 * b1)) by C, defiso
.= ((emb_iso f) . a) * ((emb_iso f) . b) by D, A, FUNCT_1:35 ;
:: thesis: verum

end;

suppose A: ( not x in [#] K & not y in [#] K & not the multF of F . (x,y) in rng f ) ; :: thesis: (emb_iso f) . (b₁ * b₂) = ((emb_iso f) . b₁) * ((emb_iso f) . b₂)

then reconsider a1 = a, b1 = b as Element of F by Lm1;
C: a * b = a1 * b1 by AS, A, Lm12;
( not a in K & not b in K ) by A;
then D: ( (emb_iso f) . a = a & (emb_iso f) . b = b ) by defiso;
not a1 * b1 in K by AS, XBOOLE_0:def 4;
hence (emb_iso f) . (a * b) = ((emb_iso f) . a) * ((emb_iso f) . b) by D, C, defiso; :: thesis: verum

end;

end;

end;

hence emb_iso f is multiplicative ; :: thesis: verum