# 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. ) ) )`
` |-  ( ( ( 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 )`
` |-  ( ( M e. Mnd /\ A e. B /\ -. ( ph /\ ps ) ) -> ( A .+ .0. ) = A )`
` |-  ( ( ( 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. ) )`
` |-  ( ( ( 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 )`
` |-  ( ( ( 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 )`
` |-  ( ( M e. Mnd /\ A e. B /\ -. ( ph /\ ps ) ) -> ( .0. .+ A ) = A )`
` |-  ( ( ( 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 ) )`
` |-  ( ( ( 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 )`
` |-  ( ( ( 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. )`
` |-  ( ( ( 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. ) )`
` |-  ( ( ( M e. Mnd /\ A e. B /\ -. ( ph /\ ps ) ) /\ ( -. ph /\ -. ps ) ) -> ( if ( ph , A , .0. ) .+ if ( ps , A , .0. ) ) = ( .0. .+ .0. ) )`
` |-  ( -. ( ph \/ ps ) <-> ( -. ph /\ -. ps ) )`
` |-  ( -. ( ph \/ ps ) -> if ( ( ph \/ ps ) , A , .0. ) = .0. )`
` |-  ( ( -. ph /\ -. ps ) -> if ( ( ph \/ ps ) , A , .0. ) = .0. )`
` |-  ( ( ( M e. Mnd /\ A e. B /\ -. ( ph /\ ps ) ) /\ ( -. ph /\ -. ps ) ) -> if ( ( ph \/ ps ) , A , .0. ) = .0. )`
` |-  ( ( ( M e. Mnd /\ A e. B /\ -. ( ph /\ ps ) ) /\ ( -. ph /\ -. ps ) ) -> if ( ( ph \/ ps ) , A , .0. ) = ( if ( ph , A , .0. ) .+ if ( ps , A , .0. ) ) )`
` |-  ( ( M e. Mnd /\ A e. B /\ -. ( ph /\ ps ) ) -> if ( ( ph \/ ps ) , A , .0. ) = ( if ( ph , A , .0. ) .+ if ( ps , A , .0. ) ) )`