Metamath Proof Explorer

Theorem issubmd

Description: Deduction for proving a submonoid. (Contributed by Stefan O'Rear, 23-Aug-2015) (Revised by Stefan O'Rear, 5-Sep-2015)

Ref Expression
Hypotheses issubmd.b ⊢ B = Base M
issubmd.p ⊢ + ˙ = + M
issubmd.z ⊢ 0 ˙ = 0 M
issubmd.m ⊢ φ → M ∈ Mnd
issubmd.cz ⊢ φ → χ
issubmd.cp ⊢ φ ∧ x ∈ B ∧ y ∈ B ∧ θ ∧ τ → η
issubmd.ch ⊢ z = 0 ˙ → ψ ↔ χ
issubmd.th ⊢ z = x → ψ ↔ θ
issubmd.ta ⊢ z = y → ψ ↔ τ
issubmd.et ⊢ z = x + ˙ y → ψ ↔ η
Assertion issubmd ⊢ φ → z ∈ B | ψ ∈ SubMnd ⁡ M

Proof

Step Hyp Ref Expression
1 issubmd.b ⊢ B = Base M
2 issubmd.p ⊢ + ˙ = + M
3 issubmd.z ⊢ 0 ˙ = 0 M
4 issubmd.m ⊢ φ → M ∈ Mnd
5 issubmd.cz ⊢ φ → χ
6 issubmd.cp ⊢ φ ∧ x ∈ B ∧ y ∈ B ∧ θ ∧ τ → η
7 issubmd.ch ⊢ z = 0 ˙ → ψ ↔ χ
8 issubmd.th ⊢ z = x → ψ ↔ θ
9 issubmd.ta ⊢ z = y → ψ ↔ τ
10 issubmd.et ⊢ z = x + ˙ y → ψ ↔ η
11 ssrab2 ⊢ z ∈ B | ψ ⊆ B
12 11 a1i ⊢ φ → z ∈ B | ψ ⊆ B
13 1 3 mndidcl ⊢ M ∈ Mnd → 0 ˙ ∈ B
14 4 13 syl ⊢ φ → 0 ˙ ∈ B
15 7 14 5 elrabd ⊢ φ → 0 ˙ ∈ z ∈ B | ψ
16 8 elrab ⊢ x ∈ z ∈ B | ψ ↔ x ∈ B ∧ θ
17 9 elrab ⊢ y ∈ z ∈ B | ψ ↔ y ∈ B ∧ τ
18 16 17 anbi12i ⊢ x ∈ z ∈ B | ψ ∧ y ∈ z ∈ B | ψ ↔ x ∈ B ∧ θ ∧ y ∈ B ∧ τ
19 4 adantr ⊢ φ ∧ x ∈ B ∧ θ ∧ y ∈ B ∧ τ → M ∈ Mnd
20 simprll ⊢ φ ∧ x ∈ B ∧ θ ∧ y ∈ B ∧ τ → x ∈ B
21 simprrl ⊢ φ ∧ x ∈ B ∧ θ ∧ y ∈ B ∧ τ → y ∈ B
22 1 2 mndcl ⊢ M ∈ Mnd ∧ x ∈ B ∧ y ∈ B → x + ˙ y ∈ B
23 19 20 21 22 syl3anc ⊢ φ ∧ x ∈ B ∧ θ ∧ y ∈ B ∧ τ → x + ˙ y ∈ B
24 an4 ⊢ x ∈ B ∧ θ ∧ y ∈ B ∧ τ ↔ x ∈ B ∧ y ∈ B ∧ θ ∧ τ
25 24 6 sylan2b ⊢ φ ∧ x ∈ B ∧ θ ∧ y ∈ B ∧ τ → η
26 10 23 25 elrabd ⊢ φ ∧ x ∈ B ∧ θ ∧ y ∈ B ∧ τ → x + ˙ y ∈ z ∈ B | ψ
27 18 26 sylan2b ⊢ φ ∧ x ∈ z ∈ B | ψ ∧ y ∈ z ∈ B | ψ → x + ˙ y ∈ z ∈ B | ψ
28 27 ralrimivva ⊢ φ → ∀ x ∈ z ∈ B | ψ ∀ y ∈ z ∈ B | ψ x + ˙ y ∈ z ∈ B | ψ
29 1 3 2 issubm ⊢ M ∈ Mnd → z ∈ B | ψ ∈ SubMnd ⁡ M ↔ z ∈ B | ψ ⊆ B ∧ 0 ˙ ∈ z ∈ B | ψ ∧ ∀ x ∈ z ∈ B | ψ ∀ y ∈ z ∈ B | ψ x + ˙ y ∈ z ∈ B | ψ
30 4 29 syl ⊢ φ → z ∈ B | ψ ∈ SubMnd ⁡ M ↔ z ∈ B | ψ ⊆ B ∧ 0 ˙ ∈ z ∈ B | ψ ∧ ∀ x ∈ z ∈ B | ψ ∀ y ∈ z ∈ B | ψ x + ˙ y ∈ z ∈ B | ψ
31 12 15 28 30 mpbir3and ⊢ φ → z ∈ B | ψ ∈ SubMnd ⁡ M