Metamath Proof Explorer


Theorem mndifsplit

Description: Lemma for maducoeval2 . (Contributed by SO, 16-Jul-2018)

Ref Expression
Hypotheses mndifsplit.b
|- B = ( Base ` M )
mndifsplit.0g
|- .0. = ( 0g ` M )
mndifsplit.pg
|- .+ = ( +g ` M )
Assertion mndifsplit
|- ( ( M e. Mnd /\ A e. B /\ -. ( ph /\ ps ) ) -> if ( ( ph \/ ps ) , A , .0. ) = ( if ( ph , A , .0. ) .+ if ( ps , A , .0. ) ) )

Proof

Step Hyp Ref Expression
1 mndifsplit.b
 |-  B = ( Base ` M )
2 mndifsplit.0g
 |-  .0. = ( 0g ` M )
3 mndifsplit.pg
 |-  .+ = ( +g ` M )
4 pm2.21
 |-  ( -. ( ph /\ ps ) -> ( ( ph /\ ps ) -> if ( ( ph \/ ps ) , A , .0. ) = ( if ( ph , A , .0. ) .+ if ( ps , A , .0. ) ) ) )
5 4 imp
 |-  ( ( -. ( ph /\ ps ) /\ ( ph /\ ps ) ) -> if ( ( ph \/ ps ) , A , .0. ) = ( if ( ph , A , .0. ) .+ if ( ps , A , .0. ) ) )
6 5 3ad2antl3
 |-  ( ( ( M e. Mnd /\ A e. B /\ -. ( ph /\ ps ) ) /\ ( ph /\ ps ) ) -> if ( ( ph \/ ps ) , A , .0. ) = ( if ( ph , A , .0. ) .+ if ( ps , A , .0. ) ) )
7 1 3 2 mndrid
 |-  ( ( M e. Mnd /\ A e. B ) -> ( A .+ .0. ) = A )
8 7 3adant3
 |-  ( ( M e. Mnd /\ A e. B /\ -. ( ph /\ ps ) ) -> ( A .+ .0. ) = A )
9 8 adantr
 |-  ( ( ( M e. Mnd /\ A e. B /\ -. ( ph /\ ps ) ) /\ ( ph /\ -. ps ) ) -> ( A .+ .0. ) = A )
10 iftrue
 |-  ( ph -> if ( ph , A , .0. ) = A )
11 iffalse
 |-  ( -. ps -> if ( ps , A , .0. ) = .0. )
12 10 11 oveqan12d
 |-  ( ( ph /\ -. ps ) -> ( if ( ph , A , .0. ) .+ if ( ps , A , .0. ) ) = ( A .+ .0. ) )
13 12 adantl
 |-  ( ( ( M e. Mnd /\ A e. B /\ -. ( ph /\ ps ) ) /\ ( ph /\ -. ps ) ) -> ( if ( ph , A , .0. ) .+ if ( ps , A , .0. ) ) = ( A .+ .0. ) )
14 iftrue
 |-  ( ( ph \/ ps ) -> if ( ( ph \/ ps ) , A , .0. ) = A )
15 14 orcs
 |-  ( ph -> if ( ( ph \/ ps ) , A , .0. ) = A )
16 15 ad2antrl
 |-  ( ( ( M e. Mnd /\ A e. B /\ -. ( ph /\ ps ) ) /\ ( ph /\ -. ps ) ) -> if ( ( ph \/ ps ) , A , .0. ) = A )
17 9 13 16 3eqtr4rd
 |-  ( ( ( M e. Mnd /\ A e. B /\ -. ( ph /\ ps ) ) /\ ( ph /\ -. ps ) ) -> if ( ( ph \/ ps ) , A , .0. ) = ( if ( ph , A , .0. ) .+ if ( ps , A , .0. ) ) )
18 1 3 2 mndlid
 |-  ( ( M e. Mnd /\ A e. B ) -> ( .0. .+ A ) = A )
19 18 3adant3
 |-  ( ( M e. Mnd /\ A e. B /\ -. ( ph /\ ps ) ) -> ( .0. .+ A ) = A )
20 19 adantr
 |-  ( ( ( M e. Mnd /\ A e. B /\ -. ( ph /\ ps ) ) /\ ( -. ph /\ ps ) ) -> ( .0. .+ A ) = A )
21 iffalse
 |-  ( -. ph -> if ( ph , A , .0. ) = .0. )
22 iftrue
 |-  ( ps -> if ( ps , A , .0. ) = A )
23 21 22 oveqan12d
 |-  ( ( -. ph /\ ps ) -> ( if ( ph , A , .0. ) .+ if ( ps , A , .0. ) ) = ( .0. .+ A ) )
24 23 adantl
 |-  ( ( ( M e. Mnd /\ A e. B /\ -. ( ph /\ ps ) ) /\ ( -. ph /\ ps ) ) -> ( if ( ph , A , .0. ) .+ if ( ps , A , .0. ) ) = ( .0. .+ A ) )
25 14 olcs
 |-  ( ps -> if ( ( ph \/ ps ) , A , .0. ) = A )
26 25 ad2antll
 |-  ( ( ( M e. Mnd /\ A e. B /\ -. ( ph /\ ps ) ) /\ ( -. ph /\ ps ) ) -> if ( ( ph \/ ps ) , A , .0. ) = A )
27 20 24 26 3eqtr4rd
 |-  ( ( ( M e. Mnd /\ A e. B /\ -. ( ph /\ ps ) ) /\ ( -. ph /\ ps ) ) -> if ( ( ph \/ ps ) , A , .0. ) = ( if ( ph , A , .0. ) .+ if ( ps , A , .0. ) ) )
28 simp1
 |-  ( ( M e. Mnd /\ A e. B /\ -. ( ph /\ ps ) ) -> M e. Mnd )
29 1 2 mndidcl
 |-  ( M e. Mnd -> .0. e. B )
30 1 3 2 mndlid
 |-  ( ( M e. Mnd /\ .0. e. B ) -> ( .0. .+ .0. ) = .0. )
31 28 29 30 syl2anc2
 |-  ( ( M e. Mnd /\ A e. B /\ -. ( ph /\ ps ) ) -> ( .0. .+ .0. ) = .0. )
32 31 adantr
 |-  ( ( ( M e. Mnd /\ A e. B /\ -. ( ph /\ ps ) ) /\ ( -. ph /\ -. ps ) ) -> ( .0. .+ .0. ) = .0. )
33 21 11 oveqan12d
 |-  ( ( -. ph /\ -. ps ) -> ( if ( ph , A , .0. ) .+ if ( ps , A , .0. ) ) = ( .0. .+ .0. ) )
34 33 adantl
 |-  ( ( ( M e. Mnd /\ A e. B /\ -. ( ph /\ ps ) ) /\ ( -. ph /\ -. ps ) ) -> ( if ( ph , A , .0. ) .+ if ( ps , A , .0. ) ) = ( .0. .+ .0. ) )
35 ioran
 |-  ( -. ( ph \/ ps ) <-> ( -. ph /\ -. ps ) )
36 iffalse
 |-  ( -. ( ph \/ ps ) -> if ( ( ph \/ ps ) , A , .0. ) = .0. )
37 35 36 sylbir
 |-  ( ( -. ph /\ -. ps ) -> if ( ( ph \/ ps ) , A , .0. ) = .0. )
38 37 adantl
 |-  ( ( ( M e. Mnd /\ A e. B /\ -. ( ph /\ ps ) ) /\ ( -. ph /\ -. ps ) ) -> if ( ( ph \/ ps ) , A , .0. ) = .0. )
39 32 34 38 3eqtr4rd
 |-  ( ( ( M e. Mnd /\ A e. B /\ -. ( ph /\ ps ) ) /\ ( -. ph /\ -. ps ) ) -> if ( ( ph \/ ps ) , A , .0. ) = ( if ( ph , A , .0. ) .+ if ( ps , A , .0. ) ) )
40 6 17 27 39 4casesdan
 |-  ( ( M e. Mnd /\ A e. B /\ -. ( ph /\ ps ) ) -> if ( ( ph \/ ps ) , A , .0. ) = ( if ( ph , A , .0. ) .+ if ( ps , A , .0. ) ) )