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 ⊢ 𝐵 = ( 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 ) ) )