This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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. ) ) )