Metamath Proof Explorer

Theorem qusmgm

Description: Prove that a quotient structure is a unital magma. (Contributed by Thierry Arnoux, 31-Aug-2026)

Ref Expression
Hypotheses qusmgm.u 
|- ( ph -> U = ( R /s .~ ) )
qusmgm.v 
|- ( ph -> V = ( Base ` R ) )
qusmgm.p 
|- .+ = ( +g ` R )
qusmgm.r 
|- ( ph -> .~ Er V )
qusmgm.x 
|- ( ph -> R e. X )
qusmgm.e 
|- ( ph -> ( ( a .~ p /\ b .~ q ) -> ( a .+ b ) .~ ( p .+ q ) ) )
qusmgm.1 
|- ( ( ph /\ x e. V /\ y e. V ) -> ( x .+ y ) e. V )
qusmgm.2 
|- ( ph -> .0. e. V )
qusmgm.3 
|- ( ( ph /\ x e. V ) -> ( .0. .+ x ) .~ x )
qusmgm.4 
|- ( ( ph /\ x e. V ) -> ( x .+ .0. ) .~ x )
Assertion qusmgm 
|- ( ph -> ( U e. Mgm /\ [ .0. ] .~ = ( 0g ` U ) ) )

Proof

Step Hyp Ref Expression
1 qusmgm.u 
 |-  ( ph -> U = ( R /s .~ ) )
2 qusmgm.v 
 |-  ( ph -> V = ( Base ` R ) )
3 qusmgm.p 
 |-  .+ = ( +g ` R )
4 qusmgm.r 
 |-  ( ph -> .~ Er V )
5 qusmgm.x 
 |-  ( ph -> R e. X )
6 qusmgm.e 
 |-  ( ph -> ( ( a .~ p /\ b .~ q ) -> ( a .+ b ) .~ ( p .+ q ) ) )
7 qusmgm.1 
 |-  ( ( ph /\ x e. V /\ y e. V ) -> ( x .+ y ) e. V )
8 qusmgm.2 
 |-  ( ph -> .0. e. V )
9 qusmgm.3 
 |-  ( ( ph /\ x e. V ) -> ( .0. .+ x ) .~ x )
10 qusmgm.4 
 |-  ( ( ph /\ x e. V ) -> ( x .+ .0. ) .~ x )
11 eqid 
 |-  ( u e. V |-> [ u ] .~ ) = ( u e. V |-> [ u ] .~ )
12 fvex 
 |-  ( Base ` R ) e. _V
13 2 12 eqeltrdi 
 |-  ( ph -> V e. _V )
14 erex 
 |-  ( .~ Er V -> ( V e. _V -> .~ e. _V ) )
15 4 13 14 sylc 
 |-  ( ph -> .~ e. _V )
16 1 2 11 15 5 qusval 
 |-  ( ph -> U = ( ( u e. V |-> [ u ] .~ ) "s R ) )
17 1 2 11 15 5 quslem 
 |-  ( ph -> ( u e. V |-> [ u ] .~ ) : V -onto-> ( V /. .~ ) )
18 7 3expb 
 |-  ( ( ph /\ ( x e. V /\ y e. V ) ) -> ( x .+ y ) e. V )
19 4 13 11 18 6 ercpbl 
 |-  ( ( ph /\ ( a e. V /\ b e. V ) /\ ( p e. V /\ q e. V ) ) -> ( ( ( ( u e. V |-> [ u ] .~ ) ` a ) = ( ( u e. V |-> [ u ] .~ ) ` p ) /\ ( ( u e. V |-> [ u ] .~ ) ` b ) = ( ( u e. V |-> [ u ] .~ ) ` q ) ) -> ( ( u e. V |-> [ u ] .~ ) ` ( a .+ b ) ) = ( ( u e. V |-> [ u ] .~ ) ` ( p .+ q ) ) ) )
20 4 adantr 
 |-  ( ( ph /\ x e. V ) -> .~ Er V )
21 20 9 erthi 
 |-  ( ( ph /\ x e. V ) -> [ ( .0. .+ x ) ] .~ = [ x ] .~ )
22 13 adantr 
 |-  ( ( ph /\ x e. V ) -> V e. _V )
23 20 22 11 divsfval 
 |-  ( ( ph /\ x e. V ) -> ( ( u e. V |-> [ u ] .~ ) ` ( .0. .+ x ) ) = [ ( .0. .+ x ) ] .~ )
24 20 22 11 divsfval 
 |-  ( ( ph /\ x e. V ) -> ( ( u e. V |-> [ u ] .~ ) ` x ) = [ x ] .~ )
25 21 23 24 3eqtr4d 
 |-  ( ( ph /\ x e. V ) -> ( ( u e. V |-> [ u ] .~ ) ` ( .0. .+ x ) ) = ( ( u e. V |-> [ u ] .~ ) ` x ) )
26 20 10 erthi 
 |-  ( ( ph /\ x e. V ) -> [ ( x .+ .0. ) ] .~ = [ x ] .~ )
27 20 22 11 divsfval 
 |-  ( ( ph /\ x e. V ) -> ( ( u e. V |-> [ u ] .~ ) ` ( x .+ .0. ) ) = [ ( x .+ .0. ) ] .~ )
28 26 27 24 3eqtr4d 
 |-  ( ( ph /\ x e. V ) -> ( ( u e. V |-> [ u ] .~ ) ` ( x .+ .0. ) ) = ( ( u e. V |-> [ u ] .~ ) ` x ) )
29 16 2 3 17 19 5 7 8 25 28 imasmgm2 
 |-  ( ph -> ( U e. Mgm /\ ( ( u e. V |-> [ u ] .~ ) ` .0. ) = ( 0g ` U ) ) )
30 4 13 11 divsfval 
 |-  ( ph -> ( ( u e. V |-> [ u ] .~ ) ` .0. ) = [ .0. ] .~ )
31 30 eqcomd 
 |-  ( ph -> [ .0. ] .~ = ( ( u e. V |-> [ u ] .~ ) ` .0. ) )
32 31 eqeq1d 
 |-  ( ph -> ( [ .0. ] .~ = ( 0g ` U ) <-> ( ( u e. V |-> [ u ] .~ ) ` .0. ) = ( 0g ` U ) ) )
33 32 anbi2d 
 |-  ( ph -> ( ( U e. Mgm /\ [ .0. ] .~ = ( 0g ` U ) ) <-> ( U e. Mgm /\ ( ( u e. V |-> [ u ] .~ ) ` .0. ) = ( 0g ` U ) ) ) )
34 29 33 mpbird 
 |-  ( ph -> ( U e. Mgm /\ [ .0. ] .~ = ( 0g ` U ) ) )