lmodprop2d

Description: If two structures have the same components (properties), one is a left module iff the other one is. This version of lmodpropd also breaks up the components of the scalar ring. (Contributed by Mario Carneiro, 27-Jun-2015)

	Ref	Expression
Hypotheses	lmodprop2d.b1	$⊢ φ \to B = {Base}_{K}$
	lmodprop2d.b2	$⊢ φ \to B = {Base}_{L}$
	lmodprop2d.f	$⊢ F = Scalar (K)$
	lmodprop2d.g	$⊢ G = Scalar (L)$
	lmodprop2d.p1	$⊢ φ \to P = {Base}_{F}$
	lmodprop2d.p2	$⊢ φ \to P = {Base}_{G}$
	lmodprop2d.1	$⊢ (φ \land (x \in B \land y \in B)) \to x +_{K} y = x +_{L} y$
	lmodprop2d.2	$⊢ (φ \land (x \in P \land y \in P)) \to x +_{F} y = x +_{G} y$
	lmodprop2d.3	$⊢ (φ \land (x \in P \land y \in P)) \to x \cdot_{F} y = x \cdot_{G} y$
	lmodprop2d.4	$⊢ (φ \land (x \in P \land y \in B)) \to x \cdot_{K} y = x \cdot_{L} y$
Assertion	lmodprop2d	$⊢ φ \to (K \in LMod \leftrightarrow L \in LMod)$

Proof

Step	Hyp	Ref	Expression
1		lmodprop2d.b1	$⊢ φ \to B = {Base}_{K}$
2		lmodprop2d.b2	$⊢ φ \to B = {Base}_{L}$
3		lmodprop2d.f	$⊢ F = Scalar (K)$
4		lmodprop2d.g	$⊢ G = Scalar (L)$
5		lmodprop2d.p1	$⊢ φ \to P = {Base}_{F}$
6		lmodprop2d.p2	$⊢ φ \to P = {Base}_{G}$
7		lmodprop2d.1	$⊢ (φ \land (x \in B \land y \in B)) \to x +_{K} y = x +_{L} y$
8		lmodprop2d.2	$⊢ (φ \land (x \in P \land y \in P)) \to x +_{F} y = x +_{G} y$
9		lmodprop2d.3	$⊢ (φ \land (x \in P \land y \in P)) \to x \cdot_{F} y = x \cdot_{G} y$
10		lmodprop2d.4	$⊢ (φ \land (x \in P \land y \in B)) \to x \cdot_{K} y = x \cdot_{L} y$
11		lmodgrp	$⊢ K \in LMod \to K \in Grp$
12	11	a1i	$⊢ φ \to (K \in LMod \to K \in Grp)$
13		eqid	$⊢ {Base}_{K} = {Base}_{K}$
14		eqid	$⊢ +_{K} = +_{K}$
15		eqid	$⊢ \cdot_{K} = \cdot_{K}$
16		eqid	$⊢ {Base}_{F} = {Base}_{F}$
17		eqid	$⊢ +_{F} = +_{F}$
18		eqid	$⊢ \cdot_{F} = \cdot_{F}$
19		eqid	$⊢ 1_{F} = 1_{F}$
20	13 14 15 3 16 17 18 19	islmod	$⊢ K \in LMod \leftrightarrow (K \in Grp \land F \in Ring \land \forall q \in {Base}_{F} \forall r \in {Base}_{F} \forall z \in {Base}_{K} \forall w \in {Base}_{K} ((r \cdot_{K} w \in {Base}_{K} \land r \cdot_{K} (w +_{K} z) = (r \cdot_{K} w) +_{K} (r \cdot_{K} z) \land (q +_{F} r) \cdot_{K} w = (q \cdot_{K} w) +_{K} (r \cdot_{K} w)) \land ((q \cdot_{F} r) \cdot_{K} w = q \cdot_{K} (r \cdot_{K} w) \land 1_{F} \cdot_{K} w = w)))$
21	20	simp2bi	$⊢ K \in LMod \to F \in Ring$
22	21	a1i	$⊢ φ \to (K \in LMod \to F \in Ring)$
23		simplr	$⊢ ((φ \land K \in LMod) \land (x \in P \land y \in B)) \to K \in LMod$
24		simprl	$⊢ ((φ \land K \in LMod) \land (x \in P \land y \in B)) \to x \in P$
25	5	ad2antrr	$⊢ ((φ \land K \in LMod) \land (x \in P \land y \in B)) \to P = {Base}_{F}$
26	24 25	eleqtrd	$⊢ ((φ \land K \in LMod) \land (x \in P \land y \in B)) \to x \in {Base}_{F}$
27		simprr	$⊢ ((φ \land K \in LMod) \land (x \in P \land y \in B)) \to y \in B$
28	1	ad2antrr	$⊢ ((φ \land K \in LMod) \land (x \in P \land y \in B)) \to B = {Base}_{K}$
29	27 28	eleqtrd	$⊢ ((φ \land K \in LMod) \land (x \in P \land y \in B)) \to y \in {Base}_{K}$
30	13 3 15 16	lmodvscl	$⊢ (K \in LMod \land x \in {Base}_{F} \land y \in {Base}_{K}) \to x \cdot_{K} y \in {Base}_{K}$
31	23 26 29 30	syl3anc	$⊢ ((φ \land K \in LMod) \land (x \in P \land y \in B)) \to x \cdot_{K} y \in {Base}_{K}$
32	31 28	eleqtrrd	$⊢ ((φ \land K \in LMod) \land (x \in P \land y \in B)) \to x \cdot_{K} y \in B$
33	32	ralrimivva	$⊢ (φ \land K \in LMod) \to \forall x \in P \forall y \in B x \cdot_{K} y \in B$
34	33	ex	$⊢ φ \to (K \in LMod \to \forall x \in P \forall y \in B x \cdot_{K} y \in B)$
35	12 22 34	3jcad	$⊢ φ \to (K \in LMod \to (K \in Grp \land F \in Ring \land \forall x \in P \forall y \in B x \cdot_{K} y \in B))$
36		lmodgrp	$⊢ L \in LMod \to L \in Grp$
37	1 2 7	grppropd	$⊢ φ \to (K \in Grp \leftrightarrow L \in Grp)$
38	36 37	syl5ibr	$⊢ φ \to (L \in LMod \to K \in Grp)$
39		eqid	$⊢ {Base}_{L} = {Base}_{L}$
40		eqid	$⊢ +_{L} = +_{L}$
41		eqid	$⊢ \cdot_{L} = \cdot_{L}$
42		eqid	$⊢ {Base}_{G} = {Base}_{G}$
43		eqid	$⊢ +_{G} = +_{G}$
44		eqid	$⊢ \cdot_{G} = \cdot_{G}$
45		eqid	$⊢ 1_{G} = 1_{G}$
46	39 40 41 4 42 43 44 45	islmod	$⊢ L \in LMod \leftrightarrow (L \in Grp \land G \in Ring \land \forall q \in {Base}_{G} \forall r \in {Base}_{G} \forall z \in {Base}_{L} \forall w \in {Base}_{L} ((r \cdot_{L} w \in {Base}_{L} \land r \cdot_{L} (w +_{L} z) = (r \cdot_{L} w) +_{L} (r \cdot_{L} z) \land (q +_{G} r) \cdot_{L} w = (q \cdot_{L} w) +_{L} (r \cdot_{L} w)) \land ((q \cdot_{G} r) \cdot_{L} w = q \cdot_{L} (r \cdot_{L} w) \land 1_{G} \cdot_{L} w = w)))$
47	46	simp2bi	$⊢ L \in LMod \to G \in Ring$
48	5 6 8 9	ringpropd	$⊢ φ \to (F \in Ring \leftrightarrow G \in Ring)$
49	47 48	syl5ibr	$⊢ φ \to (L \in LMod \to F \in Ring)$
50		simplr	$⊢ ((φ \land L \in LMod) \land (x \in P \land y \in B)) \to L \in LMod$
51		simprl	$⊢ ((φ \land L \in LMod) \land (x \in P \land y \in B)) \to x \in P$
52	6	ad2antrr	$⊢ ((φ \land L \in LMod) \land (x \in P \land y \in B)) \to P = {Base}_{G}$
53	51 52	eleqtrd	$⊢ ((φ \land L \in LMod) \land (x \in P \land y \in B)) \to x \in {Base}_{G}$
54		simprr	$⊢ ((φ \land L \in LMod) \land (x \in P \land y \in B)) \to y \in B$
55	2	ad2antrr	$⊢ ((φ \land L \in LMod) \land (x \in P \land y \in B)) \to B = {Base}_{L}$
56	54 55	eleqtrd	$⊢ ((φ \land L \in LMod) \land (x \in P \land y \in B)) \to y \in {Base}_{L}$
57	39 4 41 42	lmodvscl	$⊢ (L \in LMod \land x \in {Base}_{G} \land y \in {Base}_{L}) \to x \cdot_{L} y \in {Base}_{L}$
58	50 53 56 57	syl3anc	$⊢ ((φ \land L \in LMod) \land (x \in P \land y \in B)) \to x \cdot_{L} y \in {Base}_{L}$
59	10	adantlr	$⊢ ((φ \land L \in LMod) \land (x \in P \land y \in B)) \to x \cdot_{K} y = x \cdot_{L} y$
60	58 59 55	3eltr4d	$⊢ ((φ \land L \in LMod) \land (x \in P \land y \in B)) \to x \cdot_{K} y \in B$
61	60	ralrimivva	$⊢ (φ \land L \in LMod) \to \forall x \in P \forall y \in B x \cdot_{K} y \in B$
62	61	ex	$⊢ φ \to (L \in LMod \to \forall x \in P \forall y \in B x \cdot_{K} y \in B)$
63	38 49 62	3jcad	$⊢ φ \to (L \in LMod \to (K \in Grp \land F \in Ring \land \forall x \in P \forall y \in B x \cdot_{K} y \in B))$
64	37	adantr	$⊢ (φ \land (K \in Grp \land F \in Ring \land \forall x \in P \forall y \in B x \cdot_{K} y \in B)) \to (K \in Grp \leftrightarrow L \in Grp)$
65	48	adantr	$⊢ (φ \land (K \in Grp \land F \in Ring \land \forall x \in P \forall y \in B x \cdot_{K} y \in B)) \to (F \in Ring \leftrightarrow G \in Ring)$
66		simpll	$⊢ ((φ \land (K \in Grp \land F \in Ring \land \forall x \in P \forall y \in B x \cdot_{K} y \in B)) \land ((q \in P \land r \in P) \land (z \in B \land w \in B))) \to φ$
67		simprlr	$⊢ ((φ \land (K \in Grp \land F \in Ring \land \forall x \in P \forall y \in B x \cdot_{K} y \in B)) \land ((q \in P \land r \in P) \land (z \in B \land w \in B))) \to r \in P$
68		simprrr	$⊢ ((φ \land (K \in Grp \land F \in Ring \land \forall x \in P \forall y \in B x \cdot_{K} y \in B)) \land ((q \in P \land r \in P) \land (z \in B \land w \in B))) \to w \in B$
69	10	oveqrspc2v	$⊢ (φ \land (r \in P \land w \in B)) \to r \cdot_{K} w = r \cdot_{L} w$
70	66 67 68 69	syl12anc	$⊢ ((φ \land (K \in Grp \land F \in Ring \land \forall x \in P \forall y \in B x \cdot_{K} y \in B)) \land ((q \in P \land r \in P) \land (z \in B \land w \in B))) \to r \cdot_{K} w = r \cdot_{L} w$
71	70	eleq1d	$⊢ ((φ \land (K \in Grp \land F \in Ring \land \forall x \in P \forall y \in B x \cdot_{K} y \in B)) \land ((q \in P \land r \in P) \land (z \in B \land w \in B))) \to (r \cdot_{K} w \in B \leftrightarrow r \cdot_{L} w \in B)$
72		simplr1	$⊢ ((φ \land (K \in Grp \land F \in Ring \land \forall x \in P \forall y \in B x \cdot_{K} y \in B)) \land ((q \in P \land r \in P) \land (z \in B \land w \in B))) \to K \in Grp$
73	1	ad2antrr	$⊢ ((φ \land (K \in Grp \land F \in Ring \land \forall x \in P \forall y \in B x \cdot_{K} y \in B)) \land ((q \in P \land r \in P) \land (z \in B \land w \in B))) \to B = {Base}_{K}$
74	68 73	eleqtrd	$⊢ ((φ \land (K \in Grp \land F \in Ring \land \forall x \in P \forall y \in B x \cdot_{K} y \in B)) \land ((q \in P \land r \in P) \land (z \in B \land w \in B))) \to w \in {Base}_{K}$
75		simprrl	$⊢ ((φ \land (K \in Grp \land F \in Ring \land \forall x \in P \forall y \in B x \cdot_{K} y \in B)) \land ((q \in P \land r \in P) \land (z \in B \land w \in B))) \to z \in B$
76	75 73	eleqtrd	$⊢ ((φ \land (K \in Grp \land F \in Ring \land \forall x \in P \forall y \in B x \cdot_{K} y \in B)) \land ((q \in P \land r \in P) \land (z \in B \land w \in B))) \to z \in {Base}_{K}$
77	13 14	grpcl	$⊢ (K \in Grp \land w \in {Base}_{K} \land z \in {Base}_{K}) \to w +_{K} z \in {Base}_{K}$
78	72 74 76 77	syl3anc	$⊢ ((φ \land (K \in Grp \land F \in Ring \land \forall x \in P \forall y \in B x \cdot_{K} y \in B)) \land ((q \in P \land r \in P) \land (z \in B \land w \in B))) \to w +_{K} z \in {Base}_{K}$
79	78 73	eleqtrrd	$⊢ ((φ \land (K \in Grp \land F \in Ring \land \forall x \in P \forall y \in B x \cdot_{K} y \in B)) \land ((q \in P \land r \in P) \land (z \in B \land w \in B))) \to w +_{K} z \in B$
80	10	oveqrspc2v	$⊢ (φ \land (r \in P \land w +_{K} z \in B)) \to r \cdot_{K} (w +_{K} z) = r \cdot_{L} (w +_{K} z)$
81	66 67 79 80	syl12anc	$⊢ ((φ \land (K \in Grp \land F \in Ring \land \forall x \in P \forall y \in B x \cdot_{K} y \in B)) \land ((q \in P \land r \in P) \land (z \in B \land w \in B))) \to r \cdot_{K} (w +_{K} z) = r \cdot_{L} (w +_{K} z)$
82	7	oveqrspc2v	$⊢ (φ \land (w \in B \land z \in B)) \to w +_{K} z = w +_{L} z$
83	66 68 75 82	syl12anc	$⊢ ((φ \land (K \in Grp \land F \in Ring \land \forall x \in P \forall y \in B x \cdot_{K} y \in B)) \land ((q \in P \land r \in P) \land (z \in B \land w \in B))) \to w +_{K} z = w +_{L} z$
84	83	oveq2d	$⊢ ((φ \land (K \in Grp \land F \in Ring \land \forall x \in P \forall y \in B x \cdot_{K} y \in B)) \land ((q \in P \land r \in P) \land (z \in B \land w \in B))) \to r \cdot_{L} (w +_{K} z) = r \cdot_{L} (w +_{L} z)$
85	81 84	eqtrd	$⊢ ((φ \land (K \in Grp \land F \in Ring \land \forall x \in P \forall y \in B x \cdot_{K} y \in B)) \land ((q \in P \land r \in P) \land (z \in B \land w \in B))) \to r \cdot_{K} (w +_{K} z) = r \cdot_{L} (w +_{L} z)$
86		simplr3	$⊢ ((φ \land (K \in Grp \land F \in Ring \land \forall x \in P \forall y \in B x \cdot_{K} y \in B)) \land ((q \in P \land r \in P) \land (z \in B \land w \in B))) \to \forall x \in P \forall y \in B x \cdot_{K} y \in B$
87		ovrspc2v	$⊢ ((r \in P \land w \in B) \land \forall x \in P \forall y \in B x \cdot_{K} y \in B) \to r \cdot_{K} w \in B$
88	67 68 86 87	syl21anc	$⊢ ((φ \land (K \in Grp \land F \in Ring \land \forall x \in P \forall y \in B x \cdot_{K} y \in B)) \land ((q \in P \land r \in P) \land (z \in B \land w \in B))) \to r \cdot_{K} w \in B$
89		ovrspc2v	$⊢ ((r \in P \land z \in B) \land \forall x \in P \forall y \in B x \cdot_{K} y \in B) \to r \cdot_{K} z \in B$
90	67 75 86 89	syl21anc	$⊢ ((φ \land (K \in Grp \land F \in Ring \land \forall x \in P \forall y \in B x \cdot_{K} y \in B)) \land ((q \in P \land r \in P) \land (z \in B \land w \in B))) \to r \cdot_{K} z \in B$
91	7	oveqrspc2v	$⊢ (φ \land (r \cdot_{K} w \in B \land r \cdot_{K} z \in B)) \to (r \cdot_{K} w) +_{K} (r \cdot_{K} z) = (r \cdot_{K} w) +_{L} (r \cdot_{K} z)$
92	66 88 90 91	syl12anc	$⊢ ((φ \land (K \in Grp \land F \in Ring \land \forall x \in P \forall y \in B x \cdot_{K} y \in B)) \land ((q \in P \land r \in P) \land (z \in B \land w \in B))) \to (r \cdot_{K} w) +_{K} (r \cdot_{K} z) = (r \cdot_{K} w) +_{L} (r \cdot_{K} z)$
93	10	oveqrspc2v	$⊢ (φ \land (r \in P \land z \in B)) \to r \cdot_{K} z = r \cdot_{L} z$
94	66 67 75 93	syl12anc	$⊢ ((φ \land (K \in Grp \land F \in Ring \land \forall x \in P \forall y \in B x \cdot_{K} y \in B)) \land ((q \in P \land r \in P) \land (z \in B \land w \in B))) \to r \cdot_{K} z = r \cdot_{L} z$
95	70 94	oveq12d	$⊢ ((φ \land (K \in Grp \land F \in Ring \land \forall x \in P \forall y \in B x \cdot_{K} y \in B)) \land ((q \in P \land r \in P) \land (z \in B \land w \in B))) \to (r \cdot_{K} w) +_{L} (r \cdot_{K} z) = (r \cdot_{L} w) +_{L} (r \cdot_{L} z)$
96	92 95	eqtrd	$⊢ ((φ \land (K \in Grp \land F \in Ring \land \forall x \in P \forall y \in B x \cdot_{K} y \in B)) \land ((q \in P \land r \in P) \land (z \in B \land w \in B))) \to (r \cdot_{K} w) +_{K} (r \cdot_{K} z) = (r \cdot_{L} w) +_{L} (r \cdot_{L} z)$
97	85 96	eqeq12d	$⊢ ((φ \land (K \in Grp \land F \in Ring \land \forall x \in P \forall y \in B x \cdot_{K} y \in B)) \land ((q \in P \land r \in P) \land (z \in B \land w \in B))) \to (r \cdot_{K} (w +_{K} z) = (r \cdot_{K} w) +_{K} (r \cdot_{K} z) \leftrightarrow r \cdot_{L} (w +_{L} z) = (r \cdot_{L} w) +_{L} (r \cdot_{L} z))$
98		simplr2	$⊢ ((φ \land (K \in Grp \land F \in Ring \land \forall x \in P \forall y \in B x \cdot_{K} y \in B)) \land ((q \in P \land r \in P) \land (z \in B \land w \in B))) \to F \in Ring$
99		simprll	$⊢ ((φ \land (K \in Grp \land F \in Ring \land \forall x \in P \forall y \in B x \cdot_{K} y \in B)) \land ((q \in P \land r \in P) \land (z \in B \land w \in B))) \to q \in P$
100	5	ad2antrr	$⊢ ((φ \land (K \in Grp \land F \in Ring \land \forall x \in P \forall y \in B x \cdot_{K} y \in B)) \land ((q \in P \land r \in P) \land (z \in B \land w \in B))) \to P = {Base}_{F}$
101	99 100	eleqtrd	$⊢ ((φ \land (K \in Grp \land F \in Ring \land \forall x \in P \forall y \in B x \cdot_{K} y \in B)) \land ((q \in P \land r \in P) \land (z \in B \land w \in B))) \to q \in {Base}_{F}$
102	67 100	eleqtrd	$⊢ ((φ \land (K \in Grp \land F \in Ring \land \forall x \in P \forall y \in B x \cdot_{K} y \in B)) \land ((q \in P \land r \in P) \land (z \in B \land w \in B))) \to r \in {Base}_{F}$
103	16 17	ringacl	$⊢ (F \in Ring \land q \in {Base}_{F} \land r \in {Base}_{F}) \to q +_{F} r \in {Base}_{F}$
104	98 101 102 103	syl3anc	$⊢ ((φ \land (K \in Grp \land F \in Ring \land \forall x \in P \forall y \in B x \cdot_{K} y \in B)) \land ((q \in P \land r \in P) \land (z \in B \land w \in B))) \to q +_{F} r \in {Base}_{F}$
105	104 100	eleqtrrd	$⊢ ((φ \land (K \in Grp \land F \in Ring \land \forall x \in P \forall y \in B x \cdot_{K} y \in B)) \land ((q \in P \land r \in P) \land (z \in B \land w \in B))) \to q +_{F} r \in P$
106	10	oveqrspc2v	$⊢ (φ \land (q +_{F} r \in P \land w \in B)) \to (q +_{F} r) \cdot_{K} w = (q +_{F} r) \cdot_{L} w$
107	66 105 68 106	syl12anc	$⊢ ((φ \land (K \in Grp \land F \in Ring \land \forall x \in P \forall y \in B x \cdot_{K} y \in B)) \land ((q \in P \land r \in P) \land (z \in B \land w \in B))) \to (q +_{F} r) \cdot_{K} w = (q +_{F} r) \cdot_{L} w$
108	8	oveqrspc2v	$⊢ (φ \land (q \in P \land r \in P)) \to q +_{F} r = q +_{G} r$
109	108	ad2ant2r	$⊢ ((φ \land (K \in Grp \land F \in Ring \land \forall x \in P \forall y \in B x \cdot_{K} y \in B)) \land ((q \in P \land r \in P) \land (z \in B \land w \in B))) \to q +_{F} r = q +_{G} r$
110	109	oveq1d	$⊢ ((φ \land (K \in Grp \land F \in Ring \land \forall x \in P \forall y \in B x \cdot_{K} y \in B)) \land ((q \in P \land r \in P) \land (z \in B \land w \in B))) \to (q +_{F} r) \cdot_{L} w = (q +_{G} r) \cdot_{L} w$
111	107 110	eqtrd	$⊢ ((φ \land (K \in Grp \land F \in Ring \land \forall x \in P \forall y \in B x \cdot_{K} y \in B)) \land ((q \in P \land r \in P) \land (z \in B \land w \in B))) \to (q +_{F} r) \cdot_{K} w = (q +_{G} r) \cdot_{L} w$
112		ovrspc2v	$⊢ ((q \in P \land w \in B) \land \forall x \in P \forall y \in B x \cdot_{K} y \in B) \to q \cdot_{K} w \in B$
113	99 68 86 112	syl21anc	$⊢ ((φ \land (K \in Grp \land F \in Ring \land \forall x \in P \forall y \in B x \cdot_{K} y \in B)) \land ((q \in P \land r \in P) \land (z \in B \land w \in B))) \to q \cdot_{K} w \in B$
114	7	oveqrspc2v	$⊢ (φ \land (q \cdot_{K} w \in B \land r \cdot_{K} w \in B)) \to (q \cdot_{K} w) +_{K} (r \cdot_{K} w) = (q \cdot_{K} w) +_{L} (r \cdot_{K} w)$
115	66 113 88 114	syl12anc	$⊢ ((φ \land (K \in Grp \land F \in Ring \land \forall x \in P \forall y \in B x \cdot_{K} y \in B)) \land ((q \in P \land r \in P) \land (z \in B \land w \in B))) \to (q \cdot_{K} w) +_{K} (r \cdot_{K} w) = (q \cdot_{K} w) +_{L} (r \cdot_{K} w)$
116	10	oveqrspc2v	$⊢ (φ \land (q \in P \land w \in B)) \to q \cdot_{K} w = q \cdot_{L} w$
117	66 99 68 116	syl12anc	$⊢ ((φ \land (K \in Grp \land F \in Ring \land \forall x \in P \forall y \in B x \cdot_{K} y \in B)) \land ((q \in P \land r \in P) \land (z \in B \land w \in B))) \to q \cdot_{K} w = q \cdot_{L} w$
118	117 70	oveq12d	$⊢ ((φ \land (K \in Grp \land F \in Ring \land \forall x \in P \forall y \in B x \cdot_{K} y \in B)) \land ((q \in P \land r \in P) \land (z \in B \land w \in B))) \to (q \cdot_{K} w) +_{L} (r \cdot_{K} w) = (q \cdot_{L} w) +_{L} (r \cdot_{L} w)$
119	115 118	eqtrd	$⊢ ((φ \land (K \in Grp \land F \in Ring \land \forall x \in P \forall y \in B x \cdot_{K} y \in B)) \land ((q \in P \land r \in P) \land (z \in B \land w \in B))) \to (q \cdot_{K} w) +_{K} (r \cdot_{K} w) = (q \cdot_{L} w) +_{L} (r \cdot_{L} w)$
120	111 119	eqeq12d	$⊢ ((φ \land (K \in Grp \land F \in Ring \land \forall x \in P \forall y \in B x \cdot_{K} y \in B)) \land ((q \in P \land r \in P) \land (z \in B \land w \in B))) \to ((q +_{F} r) \cdot_{K} w = (q \cdot_{K} w) +_{K} (r \cdot_{K} w) \leftrightarrow (q +_{G} r) \cdot_{L} w = (q \cdot_{L} w) +_{L} (r \cdot_{L} w))$
121	71 97 120	3anbi123d	$⊢ ((φ \land (K \in Grp \land F \in Ring \land \forall x \in P \forall y \in B x \cdot_{K} y \in B)) \land ((q \in P \land r \in P) \land (z \in B \land w \in B))) \to ((r \cdot_{K} w \in B \land r \cdot_{K} (w +_{K} z) = (r \cdot_{K} w) +_{K} (r \cdot_{K} z) \land (q +_{F} r) \cdot_{K} w = (q \cdot_{K} w) +_{K} (r \cdot_{K} w)) \leftrightarrow (r \cdot_{L} w \in B \land r \cdot_{L} (w +_{L} z) = (r \cdot_{L} w) +_{L} (r \cdot_{L} z) \land (q +_{G} r) \cdot_{L} w = (q \cdot_{L} w) +_{L} (r \cdot_{L} w)))$
122	16 18	ringcl	$⊢ (F \in Ring \land q \in {Base}_{F} \land r \in {Base}_{F}) \to q \cdot_{F} r \in {Base}_{F}$
123	98 101 102 122	syl3anc	$⊢ ((φ \land (K \in Grp \land F \in Ring \land \forall x \in P \forall y \in B x \cdot_{K} y \in B)) \land ((q \in P \land r \in P) \land (z \in B \land w \in B))) \to q \cdot_{F} r \in {Base}_{F}$
124	123 100	eleqtrrd	$⊢ ((φ \land (K \in Grp \land F \in Ring \land \forall x \in P \forall y \in B x \cdot_{K} y \in B)) \land ((q \in P \land r \in P) \land (z \in B \land w \in B))) \to q \cdot_{F} r \in P$
125	10	oveqrspc2v	$⊢ (φ \land (q \cdot_{F} r \in P \land w \in B)) \to (q \cdot_{F} r) \cdot_{K} w = (q \cdot_{F} r) \cdot_{L} w$
126	66 124 68 125	syl12anc	$⊢ ((φ \land (K \in Grp \land F \in Ring \land \forall x \in P \forall y \in B x \cdot_{K} y \in B)) \land ((q \in P \land r \in P) \land (z \in B \land w \in B))) \to (q \cdot_{F} r) \cdot_{K} w = (q \cdot_{F} r) \cdot_{L} w$
127	9	oveqrspc2v	$⊢ (φ \land (q \in P \land r \in P)) \to q \cdot_{F} r = q \cdot_{G} r$
128	127	ad2ant2r	$⊢ ((φ \land (K \in Grp \land F \in Ring \land \forall x \in P \forall y \in B x \cdot_{K} y \in B)) \land ((q \in P \land r \in P) \land (z \in B \land w \in B))) \to q \cdot_{F} r = q \cdot_{G} r$
129	128	oveq1d	$⊢ ((φ \land (K \in Grp \land F \in Ring \land \forall x \in P \forall y \in B x \cdot_{K} y \in B)) \land ((q \in P \land r \in P) \land (z \in B \land w \in B))) \to (q \cdot_{F} r) \cdot_{L} w = (q \cdot_{G} r) \cdot_{L} w$
130	126 129	eqtrd	$⊢ ((φ \land (K \in Grp \land F \in Ring \land \forall x \in P \forall y \in B x \cdot_{K} y \in B)) \land ((q \in P \land r \in P) \land (z \in B \land w \in B))) \to (q \cdot_{F} r) \cdot_{K} w = (q \cdot_{G} r) \cdot_{L} w$
131	10	oveqrspc2v	$⊢ (φ \land (q \in P \land r \cdot_{K} w \in B)) \to q \cdot_{K} (r \cdot_{K} w) = q \cdot_{L} (r \cdot_{K} w)$
132	66 99 88 131	syl12anc	$⊢ ((φ \land (K \in Grp \land F \in Ring \land \forall x \in P \forall y \in B x \cdot_{K} y \in B)) \land ((q \in P \land r \in P) \land (z \in B \land w \in B))) \to q \cdot_{K} (r \cdot_{K} w) = q \cdot_{L} (r \cdot_{K} w)$
133	70	oveq2d	$⊢ ((φ \land (K \in Grp \land F \in Ring \land \forall x \in P \forall y \in B x \cdot_{K} y \in B)) \land ((q \in P \land r \in P) \land (z \in B \land w \in B))) \to q \cdot_{L} (r \cdot_{K} w) = q \cdot_{L} (r \cdot_{L} w)$
134	132 133	eqtrd	$⊢ ((φ \land (K \in Grp \land F \in Ring \land \forall x \in P \forall y \in B x \cdot_{K} y \in B)) \land ((q \in P \land r \in P) \land (z \in B \land w \in B))) \to q \cdot_{K} (r \cdot_{K} w) = q \cdot_{L} (r \cdot_{L} w)$
135	130 134	eqeq12d	$⊢ ((φ \land (K \in Grp \land F \in Ring \land \forall x \in P \forall y \in B x \cdot_{K} y \in B)) \land ((q \in P \land r \in P) \land (z \in B \land w \in B))) \to ((q \cdot_{F} r) \cdot_{K} w = q \cdot_{K} (r \cdot_{K} w) \leftrightarrow (q \cdot_{G} r) \cdot_{L} w = q \cdot_{L} (r \cdot_{L} w))$
136	16 19	ringidcl	$⊢ F \in Ring \to 1_{F} \in {Base}_{F}$
137	98 136	syl	$⊢ ((φ \land (K \in Grp \land F \in Ring \land \forall x \in P \forall y \in B x \cdot_{K} y \in B)) \land ((q \in P \land r \in P) \land (z \in B \land w \in B))) \to 1_{F} \in {Base}_{F}$
138	137 100	eleqtrrd	$⊢ ((φ \land (K \in Grp \land F \in Ring \land \forall x \in P \forall y \in B x \cdot_{K} y \in B)) \land ((q \in P \land r \in P) \land (z \in B \land w \in B))) \to 1_{F} \in P$
139	10	oveqrspc2v	$⊢ (φ \land (1_{F} \in P \land w \in B)) \to 1_{F} \cdot_{K} w = 1_{F} \cdot_{L} w$
140	66 138 68 139	syl12anc	$⊢ ((φ \land (K \in Grp \land F \in Ring \land \forall x \in P \forall y \in B x \cdot_{K} y \in B)) \land ((q \in P \land r \in P) \land (z \in B \land w \in B))) \to 1_{F} \cdot_{K} w = 1_{F} \cdot_{L} w$
141	5 6 9	rngidpropd	$⊢ φ \to 1_{F} = 1_{G}$
142	141	ad2antrr	$⊢ ((φ \land (K \in Grp \land F \in Ring \land \forall x \in P \forall y \in B x \cdot_{K} y \in B)) \land ((q \in P \land r \in P) \land (z \in B \land w \in B))) \to 1_{F} = 1_{G}$
143	142	oveq1d	$⊢ ((φ \land (K \in Grp \land F \in Ring \land \forall x \in P \forall y \in B x \cdot_{K} y \in B)) \land ((q \in P \land r \in P) \land (z \in B \land w \in B))) \to 1_{F} \cdot_{L} w = 1_{G} \cdot_{L} w$
144	140 143	eqtrd	$⊢ ((φ \land (K \in Grp \land F \in Ring \land \forall x \in P \forall y \in B x \cdot_{K} y \in B)) \land ((q \in P \land r \in P) \land (z \in B \land w \in B))) \to 1_{F} \cdot_{K} w = 1_{G} \cdot_{L} w$
145	144	eqeq1d	$⊢ ((φ \land (K \in Grp \land F \in Ring \land \forall x \in P \forall y \in B x \cdot_{K} y \in B)) \land ((q \in P \land r \in P) \land (z \in B \land w \in B))) \to (1_{F} \cdot_{K} w = w \leftrightarrow 1_{G} \cdot_{L} w = w)$
146	135 145	anbi12d	$⊢ ((φ \land (K \in Grp \land F \in Ring \land \forall x \in P \forall y \in B x \cdot_{K} y \in B)) \land ((q \in P \land r \in P) \land (z \in B \land w \in B))) \to (((q \cdot_{F} r) \cdot_{K} w = q \cdot_{K} (r \cdot_{K} w) \land 1_{F} \cdot_{K} w = w) \leftrightarrow ((q \cdot_{G} r) \cdot_{L} w = q \cdot_{L} (r \cdot_{L} w) \land 1_{G} \cdot_{L} w = w))$
147	121 146	anbi12d	$⊢ ((φ \land (K \in Grp \land F \in Ring \land \forall x \in P \forall y \in B x \cdot_{K} y \in B)) \land ((q \in P \land r \in P) \land (z \in B \land w \in B))) \to (((r \cdot_{K} w \in B \land r \cdot_{K} (w +_{K} z) = (r \cdot_{K} w) +_{K} (r \cdot_{K} z) \land (q +_{F} r) \cdot_{K} w = (q \cdot_{K} w) +_{K} (r \cdot_{K} w)) \land ((q \cdot_{F} r) \cdot_{K} w = q \cdot_{K} (r \cdot_{K} w) \land 1_{F} \cdot_{K} w = w)) \leftrightarrow ((r \cdot_{L} w \in B \land r \cdot_{L} (w +_{L} z) = (r \cdot_{L} w) +_{L} (r \cdot_{L} z) \land (q +_{G} r) \cdot_{L} w = (q \cdot_{L} w) +_{L} (r \cdot_{L} w)) \land ((q \cdot_{G} r) \cdot_{L} w = q \cdot_{L} (r \cdot_{L} w) \land 1_{G} \cdot_{L} w = w)))$
148	147	anassrs	$⊢ (((φ \land (K \in Grp \land F \in Ring \land \forall x \in P \forall y \in B x \cdot_{K} y \in B)) \land (q \in P \land r \in P)) \land (z \in B \land w \in B)) \to (((r \cdot_{K} w \in B \land r \cdot_{K} (w +_{K} z) = (r \cdot_{K} w) +_{K} (r \cdot_{K} z) \land (q +_{F} r) \cdot_{K} w = (q \cdot_{K} w) +_{K} (r \cdot_{K} w)) \land ((q \cdot_{F} r) \cdot_{K} w = q \cdot_{K} (r \cdot_{K} w) \land 1_{F} \cdot_{K} w = w)) \leftrightarrow ((r \cdot_{L} w \in B \land r \cdot_{L} (w +_{L} z) = (r \cdot_{L} w) +_{L} (r \cdot_{L} z) \land (q +_{G} r) \cdot_{L} w = (q \cdot_{L} w) +_{L} (r \cdot_{L} w)) \land ((q \cdot_{G} r) \cdot_{L} w = q \cdot_{L} (r \cdot_{L} w) \land 1_{G} \cdot_{L} w = w)))$
149	148	2ralbidva	$⊢ ((φ \land (K \in Grp \land F \in Ring \land \forall x \in P \forall y \in B x \cdot_{K} y \in B)) \land (q \in P \land r \in P)) \to (\forall z \in B \forall w \in B ((r \cdot_{K} w \in B \land r \cdot_{K} (w +_{K} z) = (r \cdot_{K} w) +_{K} (r \cdot_{K} z) \land (q +_{F} r) \cdot_{K} w = (q \cdot_{K} w) +_{K} (r \cdot_{K} w)) \land ((q \cdot_{F} r) \cdot_{K} w = q \cdot_{K} (r \cdot_{K} w) \land 1_{F} \cdot_{K} w = w)) \leftrightarrow \forall z \in B \forall w \in B ((r \cdot_{L} w \in B \land r \cdot_{L} (w +_{L} z) = (r \cdot_{L} w) +_{L} (r \cdot_{L} z) \land (q +_{G} r) \cdot_{L} w = (q \cdot_{L} w) +_{L} (r \cdot_{L} w)) \land ((q \cdot_{G} r) \cdot_{L} w = q \cdot_{L} (r \cdot_{L} w) \land 1_{G} \cdot_{L} w = w)))$
150	149	2ralbidva	$⊢ (φ \land (K \in Grp \land F \in Ring \land \forall x \in P \forall y \in B x \cdot_{K} y \in B)) \to (\forall q \in P \forall r \in P \forall z \in B \forall w \in B ((r \cdot_{K} w \in B \land r \cdot_{K} (w +_{K} z) = (r \cdot_{K} w) +_{K} (r \cdot_{K} z) \land (q +_{F} r) \cdot_{K} w = (q \cdot_{K} w) +_{K} (r \cdot_{K} w)) \land ((q \cdot_{F} r) \cdot_{K} w = q \cdot_{K} (r \cdot_{K} w) \land 1_{F} \cdot_{K} w = w)) \leftrightarrow \forall q \in P \forall r \in P \forall z \in B \forall w \in B ((r \cdot_{L} w \in B \land r \cdot_{L} (w +_{L} z) = (r \cdot_{L} w) +_{L} (r \cdot_{L} z) \land (q +_{G} r) \cdot_{L} w = (q \cdot_{L} w) +_{L} (r \cdot_{L} w)) \land ((q \cdot_{G} r) \cdot_{L} w = q \cdot_{L} (r \cdot_{L} w) \land 1_{G} \cdot_{L} w = w)))$
151	5	adantr	$⊢ (φ \land (K \in Grp \land F \in Ring \land \forall x \in P \forall y \in B x \cdot_{K} y \in B)) \to P = {Base}_{F}$
152	1	adantr	$⊢ (φ \land (K \in Grp \land F \in Ring \land \forall x \in P \forall y \in B x \cdot_{K} y \in B)) \to B = {Base}_{K}$
153	152	eleq2d	$⊢ (φ \land (K \in Grp \land F \in Ring \land \forall x \in P \forall y \in B x \cdot_{K} y \in B)) \to (r \cdot_{K} w \in B \leftrightarrow r \cdot_{K} w \in {Base}_{K})$
154	153	3anbi1d	$⊢ (φ \land (K \in Grp \land F \in Ring \land \forall x \in P \forall y \in B x \cdot_{K} y \in B)) \to ((r \cdot_{K} w \in B \land r \cdot_{K} (w +_{K} z) = (r \cdot_{K} w) +_{K} (r \cdot_{K} z) \land (q +_{F} r) \cdot_{K} w = (q \cdot_{K} w) +_{K} (r \cdot_{K} w)) \leftrightarrow (r \cdot_{K} w \in {Base}_{K} \land r \cdot_{K} (w +_{K} z) = (r \cdot_{K} w) +_{K} (r \cdot_{K} z) \land (q +_{F} r) \cdot_{K} w = (q \cdot_{K} w) +_{K} (r \cdot_{K} w)))$
155	154	anbi1d	$⊢ (φ \land (K \in Grp \land F \in Ring \land \forall x \in P \forall y \in B x \cdot_{K} y \in B)) \to (((r \cdot_{K} w \in B \land r \cdot_{K} (w +_{K} z) = (r \cdot_{K} w) +_{K} (r \cdot_{K} z) \land (q +_{F} r) \cdot_{K} w = (q \cdot_{K} w) +_{K} (r \cdot_{K} w)) \land ((q \cdot_{F} r) \cdot_{K} w = q \cdot_{K} (r \cdot_{K} w) \land 1_{F} \cdot_{K} w = w)) \leftrightarrow ((r \cdot_{K} w \in {Base}_{K} \land r \cdot_{K} (w +_{K} z) = (r \cdot_{K} w) +_{K} (r \cdot_{K} z) \land (q +_{F} r) \cdot_{K} w = (q \cdot_{K} w) +_{K} (r \cdot_{K} w)) \land ((q \cdot_{F} r) \cdot_{K} w = q \cdot_{K} (r \cdot_{K} w) \land 1_{F} \cdot_{K} w = w)))$
156	152 155	raleqbidv	$⊢ (φ \land (K \in Grp \land F \in Ring \land \forall x \in P \forall y \in B x \cdot_{K} y \in B)) \to (\forall w \in B ((r \cdot_{K} w \in B \land r \cdot_{K} (w +_{K} z) = (r \cdot_{K} w) +_{K} (r \cdot_{K} z) \land (q +_{F} r) \cdot_{K} w = (q \cdot_{K} w) +_{K} (r \cdot_{K} w)) \land ((q \cdot_{F} r) \cdot_{K} w = q \cdot_{K} (r \cdot_{K} w) \land 1_{F} \cdot_{K} w = w)) \leftrightarrow \forall w \in {Base}_{K} ((r \cdot_{K} w \in {Base}_{K} \land r \cdot_{K} (w +_{K} z) = (r \cdot_{K} w) +_{K} (r \cdot_{K} z) \land (q +_{F} r) \cdot_{K} w = (q \cdot_{K} w) +_{K} (r \cdot_{K} w)) \land ((q \cdot_{F} r) \cdot_{K} w = q \cdot_{K} (r \cdot_{K} w) \land 1_{F} \cdot_{K} w = w)))$
157	152 156	raleqbidv	$⊢ (φ \land (K \in Grp \land F \in Ring \land \forall x \in P \forall y \in B x \cdot_{K} y \in B)) \to (\forall z \in B \forall w \in B ((r \cdot_{K} w \in B \land r \cdot_{K} (w +_{K} z) = (r \cdot_{K} w) +_{K} (r \cdot_{K} z) \land (q +_{F} r) \cdot_{K} w = (q \cdot_{K} w) +_{K} (r \cdot_{K} w)) \land ((q \cdot_{F} r) \cdot_{K} w = q \cdot_{K} (r \cdot_{K} w) \land 1_{F} \cdot_{K} w = w)) \leftrightarrow \forall z \in {Base}_{K} \forall w \in {Base}_{K} ((r \cdot_{K} w \in {Base}_{K} \land r \cdot_{K} (w +_{K} z) = (r \cdot_{K} w) +_{K} (r \cdot_{K} z) \land (q +_{F} r) \cdot_{K} w = (q \cdot_{K} w) +_{K} (r \cdot_{K} w)) \land ((q \cdot_{F} r) \cdot_{K} w = q \cdot_{K} (r \cdot_{K} w) \land 1_{F} \cdot_{K} w = w)))$
158	151 157	raleqbidv	$⊢ (φ \land (K \in Grp \land F \in Ring \land \forall x \in P \forall y \in B x \cdot_{K} y \in B)) \to (\forall r \in P \forall z \in B \forall w \in B ((r \cdot_{K} w \in B \land r \cdot_{K} (w +_{K} z) = (r \cdot_{K} w) +_{K} (r \cdot_{K} z) \land (q +_{F} r) \cdot_{K} w = (q \cdot_{K} w) +_{K} (r \cdot_{K} w)) \land ((q \cdot_{F} r) \cdot_{K} w = q \cdot_{K} (r \cdot_{K} w) \land 1_{F} \cdot_{K} w = w)) \leftrightarrow \forall r \in {Base}_{F} \forall z \in {Base}_{K} \forall w \in {Base}_{K} ((r \cdot_{K} w \in {Base}_{K} \land r \cdot_{K} (w +_{K} z) = (r \cdot_{K} w) +_{K} (r \cdot_{K} z) \land (q +_{F} r) \cdot_{K} w = (q \cdot_{K} w) +_{K} (r \cdot_{K} w)) \land ((q \cdot_{F} r) \cdot_{K} w = q \cdot_{K} (r \cdot_{K} w) \land 1_{F} \cdot_{K} w = w)))$
159	151 158	raleqbidv	$⊢ (φ \land (K \in Grp \land F \in Ring \land \forall x \in P \forall y \in B x \cdot_{K} y \in B)) \to (\forall q \in P \forall r \in P \forall z \in B \forall w \in B ((r \cdot_{K} w \in B \land r \cdot_{K} (w +_{K} z) = (r \cdot_{K} w) +_{K} (r \cdot_{K} z) \land (q +_{F} r) \cdot_{K} w = (q \cdot_{K} w) +_{K} (r \cdot_{K} w)) \land ((q \cdot_{F} r) \cdot_{K} w = q \cdot_{K} (r \cdot_{K} w) \land 1_{F} \cdot_{K} w = w)) \leftrightarrow \forall q \in {Base}_{F} \forall r \in {Base}_{F} \forall z \in {Base}_{K} \forall w \in {Base}_{K} ((r \cdot_{K} w \in {Base}_{K} \land r \cdot_{K} (w +_{K} z) = (r \cdot_{K} w) +_{K} (r \cdot_{K} z) \land (q +_{F} r) \cdot_{K} w = (q \cdot_{K} w) +_{K} (r \cdot_{K} w)) \land ((q \cdot_{F} r) \cdot_{K} w = q \cdot_{K} (r \cdot_{K} w) \land 1_{F} \cdot_{K} w = w)))$
160	6	adantr	$⊢ (φ \land (K \in Grp \land F \in Ring \land \forall x \in P \forall y \in B x \cdot_{K} y \in B)) \to P = {Base}_{G}$
161	2	adantr	$⊢ (φ \land (K \in Grp \land F \in Ring \land \forall x \in P \forall y \in B x \cdot_{K} y \in B)) \to B = {Base}_{L}$
162	161	eleq2d	$⊢ (φ \land (K \in Grp \land F \in Ring \land \forall x \in P \forall y \in B x \cdot_{K} y \in B)) \to (r \cdot_{L} w \in B \leftrightarrow r \cdot_{L} w \in {Base}_{L})$
163	162	3anbi1d	$⊢ (φ \land (K \in Grp \land F \in Ring \land \forall x \in P \forall y \in B x \cdot_{K} y \in B)) \to ((r \cdot_{L} w \in B \land r \cdot_{L} (w +_{L} z) = (r \cdot_{L} w) +_{L} (r \cdot_{L} z) \land (q +_{G} r) \cdot_{L} w = (q \cdot_{L} w) +_{L} (r \cdot_{L} w)) \leftrightarrow (r \cdot_{L} w \in {Base}_{L} \land r \cdot_{L} (w +_{L} z) = (r \cdot_{L} w) +_{L} (r \cdot_{L} z) \land (q +_{G} r) \cdot_{L} w = (q \cdot_{L} w) +_{L} (r \cdot_{L} w)))$
164	163	anbi1d	$⊢ (φ \land (K \in Grp \land F \in Ring \land \forall x \in P \forall y \in B x \cdot_{K} y \in B)) \to (((r \cdot_{L} w \in B \land r \cdot_{L} (w +_{L} z) = (r \cdot_{L} w) +_{L} (r \cdot_{L} z) \land (q +_{G} r) \cdot_{L} w = (q \cdot_{L} w) +_{L} (r \cdot_{L} w)) \land ((q \cdot_{G} r) \cdot_{L} w = q \cdot_{L} (r \cdot_{L} w) \land 1_{G} \cdot_{L} w = w)) \leftrightarrow ((r \cdot_{L} w \in {Base}_{L} \land r \cdot_{L} (w +_{L} z) = (r \cdot_{L} w) +_{L} (r \cdot_{L} z) \land (q +_{G} r) \cdot_{L} w = (q \cdot_{L} w) +_{L} (r \cdot_{L} w)) \land ((q \cdot_{G} r) \cdot_{L} w = q \cdot_{L} (r \cdot_{L} w) \land 1_{G} \cdot_{L} w = w)))$
165	161 164	raleqbidv	$⊢ (φ \land (K \in Grp \land F \in Ring \land \forall x \in P \forall y \in B x \cdot_{K} y \in B)) \to (\forall w \in B ((r \cdot_{L} w \in B \land r \cdot_{L} (w +_{L} z) = (r \cdot_{L} w) +_{L} (r \cdot_{L} z) \land (q +_{G} r) \cdot_{L} w = (q \cdot_{L} w) +_{L} (r \cdot_{L} w)) \land ((q \cdot_{G} r) \cdot_{L} w = q \cdot_{L} (r \cdot_{L} w) \land 1_{G} \cdot_{L} w = w)) \leftrightarrow \forall w \in {Base}_{L} ((r \cdot_{L} w \in {Base}_{L} \land r \cdot_{L} (w +_{L} z) = (r \cdot_{L} w) +_{L} (r \cdot_{L} z) \land (q +_{G} r) \cdot_{L} w = (q \cdot_{L} w) +_{L} (r \cdot_{L} w)) \land ((q \cdot_{G} r) \cdot_{L} w = q \cdot_{L} (r \cdot_{L} w) \land 1_{G} \cdot_{L} w = w)))$
166	161 165	raleqbidv	$⊢ (φ \land (K \in Grp \land F \in Ring \land \forall x \in P \forall y \in B x \cdot_{K} y \in B)) \to (\forall z \in B \forall w \in B ((r \cdot_{L} w \in B \land r \cdot_{L} (w +_{L} z) = (r \cdot_{L} w) +_{L} (r \cdot_{L} z) \land (q +_{G} r) \cdot_{L} w = (q \cdot_{L} w) +_{L} (r \cdot_{L} w)) \land ((q \cdot_{G} r) \cdot_{L} w = q \cdot_{L} (r \cdot_{L} w) \land 1_{G} \cdot_{L} w = w)) \leftrightarrow \forall z \in {Base}_{L} \forall w \in {Base}_{L} ((r \cdot_{L} w \in {Base}_{L} \land r \cdot_{L} (w +_{L} z) = (r \cdot_{L} w) +_{L} (r \cdot_{L} z) \land (q +_{G} r) \cdot_{L} w = (q \cdot_{L} w) +_{L} (r \cdot_{L} w)) \land ((q \cdot_{G} r) \cdot_{L} w = q \cdot_{L} (r \cdot_{L} w) \land 1_{G} \cdot_{L} w = w)))$
167	160 166	raleqbidv	$⊢ (φ \land (K \in Grp \land F \in Ring \land \forall x \in P \forall y \in B x \cdot_{K} y \in B)) \to (\forall r \in P \forall z \in B \forall w \in B ((r \cdot_{L} w \in B \land r \cdot_{L} (w +_{L} z) = (r \cdot_{L} w) +_{L} (r \cdot_{L} z) \land (q +_{G} r) \cdot_{L} w = (q \cdot_{L} w) +_{L} (r \cdot_{L} w)) \land ((q \cdot_{G} r) \cdot_{L} w = q \cdot_{L} (r \cdot_{L} w) \land 1_{G} \cdot_{L} w = w)) \leftrightarrow \forall r \in {Base}_{G} \forall z \in {Base}_{L} \forall w \in {Base}_{L} ((r \cdot_{L} w \in {Base}_{L} \land r \cdot_{L} (w +_{L} z) = (r \cdot_{L} w) +_{L} (r \cdot_{L} z) \land (q +_{G} r) \cdot_{L} w = (q \cdot_{L} w) +_{L} (r \cdot_{L} w)) \land ((q \cdot_{G} r) \cdot_{L} w = q \cdot_{L} (r \cdot_{L} w) \land 1_{G} \cdot_{L} w = w)))$
168	160 167	raleqbidv	$⊢ (φ \land (K \in Grp \land F \in Ring \land \forall x \in P \forall y \in B x \cdot_{K} y \in B)) \to (\forall q \in P \forall r \in P \forall z \in B \forall w \in B ((r \cdot_{L} w \in B \land r \cdot_{L} (w +_{L} z) = (r \cdot_{L} w) +_{L} (r \cdot_{L} z) \land (q +_{G} r) \cdot_{L} w = (q \cdot_{L} w) +_{L} (r \cdot_{L} w)) \land ((q \cdot_{G} r) \cdot_{L} w = q \cdot_{L} (r \cdot_{L} w) \land 1_{G} \cdot_{L} w = w)) \leftrightarrow \forall q \in {Base}_{G} \forall r \in {Base}_{G} \forall z \in {Base}_{L} \forall w \in {Base}_{L} ((r \cdot_{L} w \in {Base}_{L} \land r \cdot_{L} (w +_{L} z) = (r \cdot_{L} w) +_{L} (r \cdot_{L} z) \land (q +_{G} r) \cdot_{L} w = (q \cdot_{L} w) +_{L} (r \cdot_{L} w)) \land ((q \cdot_{G} r) \cdot_{L} w = q \cdot_{L} (r \cdot_{L} w) \land 1_{G} \cdot_{L} w = w)))$
169	150 159 168	3bitr3d	$⊢ (φ \land (K \in Grp \land F \in Ring \land \forall x \in P \forall y \in B x \cdot_{K} y \in B)) \to (\forall q \in {Base}_{F} \forall r \in {Base}_{F} \forall z \in {Base}_{K} \forall w \in {Base}_{K} ((r \cdot_{K} w \in {Base}_{K} \land r \cdot_{K} (w +_{K} z) = (r \cdot_{K} w) +_{K} (r \cdot_{K} z) \land (q +_{F} r) \cdot_{K} w = (q \cdot_{K} w) +_{K} (r \cdot_{K} w)) \land ((q \cdot_{F} r) \cdot_{K} w = q \cdot_{K} (r \cdot_{K} w) \land 1_{F} \cdot_{K} w = w)) \leftrightarrow \forall q \in {Base}_{G} \forall r \in {Base}_{G} \forall z \in {Base}_{L} \forall w \in {Base}_{L} ((r \cdot_{L} w \in {Base}_{L} \land r \cdot_{L} (w +_{L} z) = (r \cdot_{L} w) +_{L} (r \cdot_{L} z) \land (q +_{G} r) \cdot_{L} w = (q \cdot_{L} w) +_{L} (r \cdot_{L} w)) \land ((q \cdot_{G} r) \cdot_{L} w = q \cdot_{L} (r \cdot_{L} w) \land 1_{G} \cdot_{L} w = w)))$
170	64 65 169	3anbi123d	$⊢ (φ \land (K \in Grp \land F \in Ring \land \forall x \in P \forall y \in B x \cdot_{K} y \in B)) \to ((K \in Grp \land F \in Ring \land \forall q \in {Base}_{F} \forall r \in {Base}_{F} \forall z \in {Base}_{K} \forall w \in {Base}_{K} ((r \cdot_{K} w \in {Base}_{K} \land r \cdot_{K} (w +_{K} z) = (r \cdot_{K} w) +_{K} (r \cdot_{K} z) \land (q +_{F} r) \cdot_{K} w = (q \cdot_{K} w) +_{K} (r \cdot_{K} w)) \land ((q \cdot_{F} r) \cdot_{K} w = q \cdot_{K} (r \cdot_{K} w) \land 1_{F} \cdot_{K} w = w))) \leftrightarrow (L \in Grp \land G \in Ring \land \forall q \in {Base}_{G} \forall r \in {Base}_{G} \forall z \in {Base}_{L} \forall w \in {Base}_{L} ((r \cdot_{L} w \in {Base}_{L} \land r \cdot_{L} (w +_{L} z) = (r \cdot_{L} w) +_{L} (r \cdot_{L} z) \land (q +_{G} r) \cdot_{L} w = (q \cdot_{L} w) +_{L} (r \cdot_{L} w)) \land ((q \cdot_{G} r) \cdot_{L} w = q \cdot_{L} (r \cdot_{L} w) \land 1_{G} \cdot_{L} w = w))))$
171	170 20 46	3bitr4g	$⊢ (φ \land (K \in Grp \land F \in Ring \land \forall x \in P \forall y \in B x \cdot_{K} y \in B)) \to (K \in LMod \leftrightarrow L \in LMod)$
172	171	ex	$⊢ φ \to ((K \in Grp \land F \in Ring \land \forall x \in P \forall y \in B x \cdot_{K} y \in B) \to (K \in LMod \leftrightarrow L \in LMod))$
173	35 63 172	pm5.21ndd	$⊢ φ \to (K \in LMod \leftrightarrow L \in LMod)$

Metamath Proof Explorer

Theorem lmodprop2d

Proof