Metamath Proof Explorer


Theorem mndifsplit

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

Ref Expression
Hypotheses mndifsplit.b 𝐵 = ( Base ‘ 𝑀 )
mndifsplit.0g 0 = ( 0g𝑀 )
mndifsplit.pg + = ( +g𝑀 )
Assertion mndifsplit ( ( 𝑀 ∈ Mnd ∧ 𝐴𝐵 ∧ ¬ ( 𝜑𝜓 ) ) → if ( ( 𝜑𝜓 ) , 𝐴 , 0 ) = ( if ( 𝜑 , 𝐴 , 0 ) + if ( 𝜓 , 𝐴 , 0 ) ) )

Proof

Step Hyp Ref Expression
1 mndifsplit.b 𝐵 = ( Base ‘ 𝑀 )
2 mndifsplit.0g 0 = ( 0g𝑀 )
3 mndifsplit.pg + = ( +g𝑀 )
4 pm2.21 ( ¬ ( 𝜑𝜓 ) → ( ( 𝜑𝜓 ) → if ( ( 𝜑𝜓 ) , 𝐴 , 0 ) = ( if ( 𝜑 , 𝐴 , 0 ) + if ( 𝜓 , 𝐴 , 0 ) ) ) )
5 4 imp ( ( ¬ ( 𝜑𝜓 ) ∧ ( 𝜑𝜓 ) ) → if ( ( 𝜑𝜓 ) , 𝐴 , 0 ) = ( if ( 𝜑 , 𝐴 , 0 ) + if ( 𝜓 , 𝐴 , 0 ) ) )
6 5 3ad2antl3 ( ( ( 𝑀 ∈ Mnd ∧ 𝐴𝐵 ∧ ¬ ( 𝜑𝜓 ) ) ∧ ( 𝜑𝜓 ) ) → if ( ( 𝜑𝜓 ) , 𝐴 , 0 ) = ( if ( 𝜑 , 𝐴 , 0 ) + if ( 𝜓 , 𝐴 , 0 ) ) )
7 1 3 2 mndrid ( ( 𝑀 ∈ Mnd ∧ 𝐴𝐵 ) → ( 𝐴 + 0 ) = 𝐴 )
8 7 3adant3 ( ( 𝑀 ∈ Mnd ∧ 𝐴𝐵 ∧ ¬ ( 𝜑𝜓 ) ) → ( 𝐴 + 0 ) = 𝐴 )
9 8 adantr ( ( ( 𝑀 ∈ Mnd ∧ 𝐴𝐵 ∧ ¬ ( 𝜑𝜓 ) ) ∧ ( 𝜑 ∧ ¬ 𝜓 ) ) → ( 𝐴 + 0 ) = 𝐴 )
10 iftrue ( 𝜑 → if ( 𝜑 , 𝐴 , 0 ) = 𝐴 )
11 iffalse ( ¬ 𝜓 → if ( 𝜓 , 𝐴 , 0 ) = 0 )
12 10 11 oveqan12d ( ( 𝜑 ∧ ¬ 𝜓 ) → ( if ( 𝜑 , 𝐴 , 0 ) + if ( 𝜓 , 𝐴 , 0 ) ) = ( 𝐴 + 0 ) )
13 12 adantl ( ( ( 𝑀 ∈ Mnd ∧ 𝐴𝐵 ∧ ¬ ( 𝜑𝜓 ) ) ∧ ( 𝜑 ∧ ¬ 𝜓 ) ) → ( if ( 𝜑 , 𝐴 , 0 ) + if ( 𝜓 , 𝐴 , 0 ) ) = ( 𝐴 + 0 ) )
14 iftrue ( ( 𝜑𝜓 ) → if ( ( 𝜑𝜓 ) , 𝐴 , 0 ) = 𝐴 )
15 14 orcs ( 𝜑 → if ( ( 𝜑𝜓 ) , 𝐴 , 0 ) = 𝐴 )
16 15 ad2antrl ( ( ( 𝑀 ∈ Mnd ∧ 𝐴𝐵 ∧ ¬ ( 𝜑𝜓 ) ) ∧ ( 𝜑 ∧ ¬ 𝜓 ) ) → if ( ( 𝜑𝜓 ) , 𝐴 , 0 ) = 𝐴 )
17 9 13 16 3eqtr4rd ( ( ( 𝑀 ∈ Mnd ∧ 𝐴𝐵 ∧ ¬ ( 𝜑𝜓 ) ) ∧ ( 𝜑 ∧ ¬ 𝜓 ) ) → if ( ( 𝜑𝜓 ) , 𝐴 , 0 ) = ( if ( 𝜑 , 𝐴 , 0 ) + if ( 𝜓 , 𝐴 , 0 ) ) )
18 1 3 2 mndlid ( ( 𝑀 ∈ Mnd ∧ 𝐴𝐵 ) → ( 0 + 𝐴 ) = 𝐴 )
19 18 3adant3 ( ( 𝑀 ∈ Mnd ∧ 𝐴𝐵 ∧ ¬ ( 𝜑𝜓 ) ) → ( 0 + 𝐴 ) = 𝐴 )
20 19 adantr ( ( ( 𝑀 ∈ Mnd ∧ 𝐴𝐵 ∧ ¬ ( 𝜑𝜓 ) ) ∧ ( ¬ 𝜑𝜓 ) ) → ( 0 + 𝐴 ) = 𝐴 )
21 iffalse ( ¬ 𝜑 → if ( 𝜑 , 𝐴 , 0 ) = 0 )
22 iftrue ( 𝜓 → if ( 𝜓 , 𝐴 , 0 ) = 𝐴 )
23 21 22 oveqan12d ( ( ¬ 𝜑𝜓 ) → ( if ( 𝜑 , 𝐴 , 0 ) + if ( 𝜓 , 𝐴 , 0 ) ) = ( 0 + 𝐴 ) )
24 23 adantl ( ( ( 𝑀 ∈ Mnd ∧ 𝐴𝐵 ∧ ¬ ( 𝜑𝜓 ) ) ∧ ( ¬ 𝜑𝜓 ) ) → ( if ( 𝜑 , 𝐴 , 0 ) + if ( 𝜓 , 𝐴 , 0 ) ) = ( 0 + 𝐴 ) )
25 14 olcs ( 𝜓 → if ( ( 𝜑𝜓 ) , 𝐴 , 0 ) = 𝐴 )
26 25 ad2antll ( ( ( 𝑀 ∈ Mnd ∧ 𝐴𝐵 ∧ ¬ ( 𝜑𝜓 ) ) ∧ ( ¬ 𝜑𝜓 ) ) → if ( ( 𝜑𝜓 ) , 𝐴 , 0 ) = 𝐴 )
27 20 24 26 3eqtr4rd ( ( ( 𝑀 ∈ Mnd ∧ 𝐴𝐵 ∧ ¬ ( 𝜑𝜓 ) ) ∧ ( ¬ 𝜑𝜓 ) ) → if ( ( 𝜑𝜓 ) , 𝐴 , 0 ) = ( if ( 𝜑 , 𝐴 , 0 ) + if ( 𝜓 , 𝐴 , 0 ) ) )
28 simp1 ( ( 𝑀 ∈ Mnd ∧ 𝐴𝐵 ∧ ¬ ( 𝜑𝜓 ) ) → 𝑀 ∈ Mnd )
29 1 2 mndidcl ( 𝑀 ∈ Mnd → 0𝐵 )
30 1 3 2 mndlid ( ( 𝑀 ∈ Mnd ∧ 0𝐵 ) → ( 0 + 0 ) = 0 )
31 28 29 30 syl2anc2 ( ( 𝑀 ∈ Mnd ∧ 𝐴𝐵 ∧ ¬ ( 𝜑𝜓 ) ) → ( 0 + 0 ) = 0 )
32 31 adantr ( ( ( 𝑀 ∈ Mnd ∧ 𝐴𝐵 ∧ ¬ ( 𝜑𝜓 ) ) ∧ ( ¬ 𝜑 ∧ ¬ 𝜓 ) ) → ( 0 + 0 ) = 0 )
33 21 11 oveqan12d ( ( ¬ 𝜑 ∧ ¬ 𝜓 ) → ( if ( 𝜑 , 𝐴 , 0 ) + if ( 𝜓 , 𝐴 , 0 ) ) = ( 0 + 0 ) )
34 33 adantl ( ( ( 𝑀 ∈ Mnd ∧ 𝐴𝐵 ∧ ¬ ( 𝜑𝜓 ) ) ∧ ( ¬ 𝜑 ∧ ¬ 𝜓 ) ) → ( if ( 𝜑 , 𝐴 , 0 ) + if ( 𝜓 , 𝐴 , 0 ) ) = ( 0 + 0 ) )
35 ioran ( ¬ ( 𝜑𝜓 ) ↔ ( ¬ 𝜑 ∧ ¬ 𝜓 ) )
36 iffalse ( ¬ ( 𝜑𝜓 ) → if ( ( 𝜑𝜓 ) , 𝐴 , 0 ) = 0 )
37 35 36 sylbir ( ( ¬ 𝜑 ∧ ¬ 𝜓 ) → if ( ( 𝜑𝜓 ) , 𝐴 , 0 ) = 0 )
38 37 adantl ( ( ( 𝑀 ∈ Mnd ∧ 𝐴𝐵 ∧ ¬ ( 𝜑𝜓 ) ) ∧ ( ¬ 𝜑 ∧ ¬ 𝜓 ) ) → if ( ( 𝜑𝜓 ) , 𝐴 , 0 ) = 0 )
39 32 34 38 3eqtr4rd ( ( ( 𝑀 ∈ Mnd ∧ 𝐴𝐵 ∧ ¬ ( 𝜑𝜓 ) ) ∧ ( ¬ 𝜑 ∧ ¬ 𝜓 ) ) → if ( ( 𝜑𝜓 ) , 𝐴 , 0 ) = ( if ( 𝜑 , 𝐴 , 0 ) + if ( 𝜓 , 𝐴 , 0 ) ) )
40 6 17 27 39 4casesdan ( ( 𝑀 ∈ Mnd ∧ 𝐴𝐵 ∧ ¬ ( 𝜑𝜓 ) ) → if ( ( 𝜑𝜓 ) , 𝐴 , 0 ) = ( if ( 𝜑 , 𝐴 , 0 ) + if ( 𝜓 , 𝐴 , 0 ) ) )