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 ˙ = 0 M
mndifsplit.pg ⊢ + ˙ = + M
Assertion mndifsplit ⊢ M ∈ Mnd ∧ A ∈ B ∧ ¬ φ ∧ ψ → if φ ∨ ψ A 0 ˙ = if φ A 0 ˙ + ˙ if ψ A 0 ˙

Proof

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